From 6a7a2eab1933d0a712265b61fb99897da45cd14d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 4 Mar 2023 22:15:37 -0800 Subject: [PATCH] Add 'gas' to cut off too-long computations --- packages.dhall | 2 +- src/Language/Bergamot/Syntax.purs | 24 +++++++++++++++--------- test/Main.purs | 5 +++-- 3 files changed, 19 insertions(+), 12 deletions(-) diff --git a/packages.dhall b/packages.dhall index 8744915..eefbced 100644 --- a/packages.dhall +++ b/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" diff --git a/src/Language/Bergamot/Syntax.purs b/src/Language/Bergamot/Syntax.purs index d895dd9..91030ce 100644 --- a/src/Language/Bergamot/Syntax.purs +++ b/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 })) diff --git a/test/Main.purs b/test/Main.purs index 1bbe04e..db781a9 100644 --- a/test/Main.purs +++ b/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")