Add 'gas' to cut off too-long computations

packages.dhall

@@ -104,9 +104,9 @@ let upstream =
 
 in  upstream
     with logict.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/logict.git"
-    with logict.version = "c2088a696727d26cb41b2553d24f3909f0525e12"
+    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 = "014d9b38c8a1742dc3039227f84e3ba06acea51b"
+    with unifyt.version = "590306964c59b8828b66b8d020283c8efaf2170b"
     with unifyt.dependencies = [ "control", "foldable-traversable", "lazy", "maybe", "newtype", "ordered-collections", "prelude", "transformers", "tuples" ]
 

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)
@@ -10,12 +10,15 @@ import Control.Apply (class Apply, apply, lift2)
 import Control.Alt (class Alt, alt)
 import Control.Alternative (class Alternative)
 import Control.Applicative (class Applicative, pure, (*>))
-import Control.Bind (class Bind, bind, (>>=))
+import Control.Bind (class Bind, bind, join, (>>=))
 import Control.MonadPlus (class MonadPlus)
+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)
 import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
 import Control.Monad.Logic.Trans (SFKT(..), runSFKTOnce)
+import Control.Monad.State.Trans (StateT(..), runStateT)
 import Data.List (List(..), (:), fromFoldable)
 import Data.Functor (class Functor, (<$>), map)
 import Data.Eq (class Eq)
@@ -76,7 +79,8 @@ derive instance Functor Rule
 derive instance Foldable Rule
 derive instance Traversable Rule
 
-newtype Unifier a = MkUnifier (UnifyT IntVar Expr (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
@@ -90,6 +94,24 @@ derive newtype instance Monad Unifier
 derive newtype instance MonadPlus Unifier
 derive newtype instance MonadUnify IntVar Expr Unifier
 
+-- >:(
+instance MonadAsk UnifierEnv Unifier where
+    ask = MkUnifier $ MkUnifyT ask
+
+-- >:(
+instance MonadReader UnifierEnv Unifier where
+    local f m = MkUnifier $ MkUnifyT $ StateT $ \s -> local f (runStateT (un MkUnifyT $ un MkUnifier m) s)
+
+-- >:(
+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
 
@@ -102,74 +124,18 @@ metavariable s = do
            v <- fresh
            modify (insert s v) *> pure v
 
--- >:(
-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)
 
 newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable, witnesses :: List (ProofTree k) }
 
 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
          pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses }
 
-rules :: Array (Rule Metavariable)
-rules =
-    [ MkRule { name: "TInt", head: tType tIntExpr tInt, tail: Nil }
-    , MkRule { name: "TString", head: tType tStringExpr tString, tail: Nil }
-    , MkRule { name: "TPlusInt", head: tType (tPlusExpr (Var "e1") (Var "e2")) tInt, tail: fromFoldable
-        [ tType (Var "e1") tInt
-        , tType (Var "e2") tInt
-        ] }
-    , MkRule { name: "TPlusString", head: tType (tPlusExpr (Var "e1") (Var "e2")) tString, tail: fromFoldable
-        [ tType (Var "e1") tString
-        , tType (Var "e2") tString
-        ] }
-    , MkRule { name: "TPair", head: tType (tProdExpr (Var "e1") (Var "e2")) (tProd (Var "t1") (Var "t2")), tail: fromFoldable
-        [ tType (Var "e1") (Var "t1")
-        , tType (Var "e2") (Var "t2")
-        ] }
-    , MkRule { name: "TFst", head: tType (tFstExpr (Var "e")) (Var "t1"), tail: fromFoldable
-        [ tType (Var "e") (tProd (Var "t1") (Var "t2"))
-        ] }
-    , MkRule { name: "TSnd", head: tType (tSndExpr (Var "e")) (Var "t2"), tail: fromFoldable
-        [ tType (Var "e") (tProd (Var "t1") (Var "t2"))
-        ] }
-    ]
-          
-tType et tt = Atom "type" $ et : tt : Nil
-tInt = Atom "int" Nil                                      
-tString = Atom "string" Nil                                
-tProd t1 t2 = Atom "prod" $ t1 : t2 : Nil
-tIntExpr = Atom "n" Nil                                    
-tStringExpr = Atom "s" Nil
-tPlusExpr et1 et2 = Atom "plus" $ et1 : et2 : Nil
-tProdExpr et1 et2 = Atom "pair" $ et1 : et2 : Nil
-tFstExpr et = Atom "fst" $ et : Nil
-tSndExpr et = Atom "snd" $ et : Nil
-
-toLatexExpr :: Expr IntVar -> String
-toLatexExpr (Atom "type" (t1 : t2 : Nil)) = toLatexExpr t1 <> " : " <> toLatexExpr t2
-toLatexExpr (Atom "int" Nil) = "\\text{int}"
-toLatexExpr (Atom "string" Nil) = "\\text{string}"
-toLatexExpr (Atom "prod" (t1 : t2 : Nil)) = toLatexExpr t1 <> "\\times" <> toLatexExpr t2
-toLatexExpr (Atom "n" Nil) = "n"
-toLatexExpr (Atom "s" Nil) = "s"
-toLatexExpr (Atom "plus" (t1 : t2 : Nil)) = toLatexExpr t1 <> " + " <> toLatexExpr t2
-toLatexExpr (Atom "pair" (t1 : t2 : Nil)) = "(" <> toLatexExpr t1 <> ", " <> toLatexExpr t2 <> ")"
-toLatexExpr (Atom "fst" (t : Nil)) = "\\text{fst}\\ " <> toLatexExpr t
-toLatexExpr (Atom "snd" (t : Nil)) = "\\text{snd}\\ " <> toLatexExpr t
-toLatexExpr (Atom s xs) = "\\text{" <> s <> "}(" <> intercalate ", " (toLatexExpr <$> xs) <> ")"
-toLatexExpr (Var _) = "?"
-
-toLatexProofTree :: ProofTree IntVar -> String
-toLatexProofTree (MkProofTree {claim, rule, witnesses}) = "\\cfrac{" <> intercalate "\\quad" (toLatexProofTree <$> witnesses) <> "}{" <> toLatexExpr claim <> "}"
-
 reifyProofTree :: ProofTree IntVar -> Unifier (ProofTree IntVar)
 reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
     claim' <- reify claim
@@ -177,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 = instantiate e >>= match rules >>= reifyProofTree
+query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
 
-runUnifier :: forall a. Unifier a -> List a
-runUnifier m = runSFKTOnce (fst <$> (runUnifyT $ un MkUnifier m))
+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

@@ -9,5 +9,58 @@ import Control.Monad.Unify.Class
 import Data.List
 import Data.Maybe
 
-main :: List String
-main = map toLatexProofTree $ runUnifier $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")
+rules :: Array (Rule Metavariable)
+rules =
+    [ MkRule { name: "TInt", head: tType tIntExpr tInt, tail: Nil }
+    , MkRule { name: "TString", head: tType tStringExpr tString, tail: Nil }
+    , MkRule { name: "TPlusInt", head: tType (tPlusExpr (Var "e1") (Var "e2")) tInt, tail: fromFoldable
+        [ tType (Var "e1") tInt
+        , tType (Var "e2") tInt
+        ] }
+    , MkRule { name: "TPlusString", head: tType (tPlusExpr (Var "e1") (Var "e2")) tString, tail: fromFoldable
+        [ tType (Var "e1") tString
+        , tType (Var "e2") tString
+        ] }
+    , MkRule { name: "TPair", head: tType (tProdExpr (Var "e1") (Var "e2")) (tProd (Var "t1") (Var "t2")), tail: fromFoldable
+        [ tType (Var "e1") (Var "t1")
+        , tType (Var "e2") (Var "t2")
+        ] }
+    , MkRule { name: "TFst", head: tType (tFstExpr (Var "e")) (Var "t1"), tail: fromFoldable
+        [ tType (Var "e") (tProd (Var "t1") (Var "t2"))
+        ] }
+    , MkRule { name: "TSnd", head: tType (tSndExpr (Var "e")) (Var "t2"), tail: fromFoldable
+        [ tType (Var "e") (tProd (Var "t1") (Var "t2"))
+        ] }
+    ]
+          
+tType et tt = Atom "type" $ et : tt : Nil
+tInt = Atom "int" Nil                                      
+tString = Atom "string" Nil                                
+tProd t1 t2 = Atom "prod" $ t1 : t2 : Nil
+tIntExpr = Atom "n" Nil                                    
+tStringExpr = Atom "s" Nil
+tPlusExpr et1 et2 = Atom "plus" $ et1 : et2 : Nil
+tProdExpr et1 et2 = Atom "pair" $ et1 : et2 : Nil
+tFstExpr et = Atom "fst" $ et : Nil
+tSndExpr et = Atom "snd" $ et : Nil
+
+toLatexExpr :: Expr IntVar -> String
+toLatexExpr (Atom "type" (t1 : t2 : Nil)) = toLatexExpr t1 <> " : " <> toLatexExpr t2
+toLatexExpr (Atom "int" Nil) = "\\text{int}"
+toLatexExpr (Atom "string" Nil) = "\\text{string}"
+toLatexExpr (Atom "prod" (t1 : t2 : Nil)) = toLatexExpr t1 <> "\\times" <> toLatexExpr t2
+toLatexExpr (Atom "n" Nil) = "n"
+toLatexExpr (Atom "s" Nil) = "s"
+toLatexExpr (Atom "plus" (t1 : t2 : Nil)) = toLatexExpr t1 <> " + " <> toLatexExpr t2
+toLatexExpr (Atom "pair" (t1 : t2 : Nil)) = "(" <> toLatexExpr t1 <> ", " <> toLatexExpr t2 <> ")"
+toLatexExpr (Atom "fst" (t : Nil)) = "\\text{fst}\\ " <> toLatexExpr t
+toLatexExpr (Atom "snd" (t : Nil)) = "\\text{snd}\\ " <> toLatexExpr t
+toLatexExpr (Atom s xs) = "\\text{" <> s <> "}(" <> intercalate ", " (toLatexExpr <$> xs) <> ")"
+toLatexExpr (Var _) = "?"
+
+toLatexProofTree :: ProofTree IntVar -> String
+toLatexProofTree (MkProofTree {claim, witnesses}) = "\\cfrac{" <> intercalate "\\quad" (toLatexProofTree <$> witnesses) <> "}{" <> toLatexExpr claim <> "}"
+
+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")