Add 'gas' to cut off too-long computations

packages.dhall

@@ -104,7 +104,7 @@ let upstream =
 
 in  upstream
     with logict.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/logict.git"
-    with logict.version = "2facde23774a6d47c45bb20425645cfafc3179e5"
+    with logict.version = "a2d2b10e86beb2769245502e7f5dec4592bb2a2a"
     with logict.dependencies = [ "control", "lists", "maybe", "prelude", "transformers", "tuples" ]
     with unifyt.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/unifyt.git"
     with unifyt.version = "590306964c59b8828b66b8d020283c8efaf2170b"

src/Language/Bergamot/Syntax.purs

@@ -1,6 +1,6 @@
 module Language.Bergamot.Syntax where
 
-import Prelude (Unit, ($), (<<<), unit, (/=), const, flip, (+))
+import Prelude
 
 import Control.Plus (class Plus, empty)
 import Control.Monad (class Monad)
@@ -12,7 +12,7 @@ import Control.Alternative (class Alternative)
 import Control.Applicative (class Applicative, pure, (*>))
 import Control.Bind (class Bind, bind, join, (>>=))
 import Control.MonadPlus (class MonadPlus)
-import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask)
+import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask, asks)
 import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave)
 import Control.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..), fresh, unify, reify)
 import Control.Monad.Reader.Trans (ReaderT, runReaderT)
@@ -79,7 +79,8 @@ derive instance Functor Rule
 derive instance Foldable Rule
 derive instance Traversable Rule
 
-newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT (Array (Rule Metavariable)) (SFKT List)) a)
+type UnifierEnv = { rules :: Array (Rule Metavariable), fuel :: Int }
+newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT UnifierEnv (SFKT Maybe)) a)
 
 derive instance Newtype (Unifier a) _
 derive newtype instance Functor Unifier
@@ -94,11 +95,11 @@ derive newtype instance MonadPlus Unifier
 derive newtype instance MonadUnify IntVar Expr Unifier
 
 -- >:(
-instance MonadAsk (Array (Rule Metavariable)) Unifier where
+instance MonadAsk UnifierEnv Unifier where
     ask = MkUnifier $ MkUnifyT ask
 
 -- >:(
-instance MonadReader (Array (Rule Metavariable)) Unifier where
+instance MonadReader UnifierEnv Unifier where
     local f m = MkUnifier $ MkUnifyT $ StateT $ \s -> local f (runStateT (un MkUnifyT $ un MkUnifier m) s)
 
 -- >:(
@@ -106,6 +107,11 @@ instance MonadLogic Unifier where
     msplit m = MkUnifier $ MkUnifyT $ map (map (rmap (MkUnifier <<< MkUnifyT))) $ msplit $ un MkUnifyT $ un MkUnifier m
     interleave = over2 MkUnifier (over2 MkUnifyT interleave)
 
+spend :: forall a. Unifier a -> Unifier a
+spend m = do
+    n <- asks _.fuel
+    if n > 0 then local (_ { fuel = n - 1}) m else empty
+
 type Metavariable = String
 type Metavariables k = Map Metavariable k
 
@@ -124,7 +130,7 @@ newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable,
 match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
 match rs e = oneOf $ map (matchSingle e) rs
     where
-      matchSingle e' rule = do
+      matchSingle e' rule = spend $ do
          MkRule {head, tail} <- instantiate rule
          _ <- unify e' head
          witnesses <- traverse (match rs) tail
@@ -137,7 +143,7 @@ reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
     pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' }
 
 query :: Expr Metavariable -> Unifier (ProofTree IntVar)
-query e = (join $ lift2 match ask (instantiate e)) >>= reifyProofTree
+query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
 
-runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> List a
-runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) rs))
+runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> Maybe a
+runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) { rules: rs, fuel: 10 }))

test/Main.purs

@@ -61,5 +61,6 @@ toLatexExpr (Var _) = "?"
 toLatexProofTree :: ProofTree IntVar -> String
 toLatexProofTree (MkProofTree {claim, witnesses}) = "\\cfrac{" <> intercalate "\\quad" (toLatexProofTree <$> witnesses) <> "}{" <> toLatexExpr claim <> "}"
 
-main :: List String
-main = map toLatexProofTree $ runUnifier rules $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")
+main :: Maybe String
+main = map toLatexProofTree $ runUnifier rules $ query $ tType (Var "e") (tProd tInt (tProd tInt tString))
+-- main = map toLatexProofTree $ runUnifier rules $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")