diff --git a/packages.dhall b/packages.dhall index 420fcbf..8744915 100644 --- a/packages.dhall +++ b/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 = "2facde23774a6d47c45bb20425645cfafc3179e5" 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" ] diff --git a/src/Language/Bergamot/Syntax.purs b/src/Language/Bergamot/Syntax.purs index bd64beb..d895dd9 100644 --- a/src/Language/Bergamot/Syntax.purs +++ b/src/Language/Bergamot/Syntax.purs @@ -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) 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,7 @@ derive instance Functor Rule derive instance Foldable Rule derive instance Traversable Rule -newtype Unifier a = MkUnifier (UnifyT IntVar Expr (SFKT List) a) +newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT (Array (Rule Metavariable)) (SFKT List)) a) derive instance Newtype (Unifier a) _ derive newtype instance Functor Unifier @@ -90,6 +93,19 @@ derive newtype instance Monad Unifier derive newtype instance MonadPlus Unifier derive newtype instance MonadUnify IntVar Expr Unifier +-- >:( +instance MonadAsk (Array (Rule Metavariable)) Unifier where + ask = MkUnifier $ MkUnifyT ask + +-- >:( +instance MonadReader (Array (Rule Metavariable)) 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) + type Metavariable = String type Metavariables k = Map Metavariable k @@ -102,10 +118,6 @@ 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) } @@ -118,58 +130,6 @@ match rs e = oneOf $ map (matchSingle e) rs 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 +137,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 ask (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 -> List a +runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) rs)) diff --git a/test/Main.purs b/test/Main.purs index 86094cc..1bbe04e 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -9,5 +9,57 @@ import Control.Monad.Unify.Class import Data.List import Data.Maybe +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 :: List String -main = map toLatexProofTree $ runUnifier $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T") +main = map toLatexProofTree $ runUnifier rules $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")