diff --git a/packages.dhall b/packages.dhall index 83e83dc..420fcbf 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 = "24298710fa940bfcf2d272bc6d5c7417f2bfccfe" + with logict.version = "c2088a696727d26cb41b2553d24f3909f0525e12" 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 = "d1e227dbed5e5af63510872b95a9417200c0d7c7" + with unifyt.version = "014d9b38c8a1742dc3039227f84e3ba06acea51b" 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 413d4c2..bd64beb 100644 --- a/src/Language/Bergamot/Syntax.purs +++ b/src/Language/Bergamot/Syntax.purs @@ -5,23 +5,23 @@ import Prelude (Unit, ($), (<<<), unit, (/=), const, flip, (+)) import Control.Plus (class Plus, empty) import Control.Monad (class Monad) import Control.Monad.State.Trans (StateT, runStateT) -import Control.Monad.State.Class (gets, modify) -import Control.Apply (class Apply, apply) +import Control.Monad.State.Class (class MonadState, gets, modify) +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.Applicative (class Applicative, pure, (*>)) import Control.Bind (class Bind, bind, (>>=)) import Control.MonadPlus (class MonadPlus) import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave) -import Control.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..)) +import Control.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..), fresh, unify, reify) import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT) -import Control.Monad.Logic.Trans (SFKT(..), runSFKT) -import Data.List (List(..), (:)) +import Control.Monad.Logic.Trans (SFKT(..), runSFKTOnce) +import Data.List (List(..), (:), fromFoldable) import Data.Functor (class Functor, (<$>), map) import Data.Eq (class Eq) import Data.Ord (class Ord) -import Data.Traversable (class Traversable, sequence, traverse) -import Data.Foldable (class Foldable, foldr, foldl, foldMap, any) +import Data.Traversable (class Traversable, sequence, traverse, oneOf) +import Data.Foldable (class Foldable, foldr, foldl, foldMap, any, intercalate) import Data.Monoid ((<>), mempty) import Data.Map (Map, lookup, insert) import Data.Map as Map @@ -39,25 +39,10 @@ data Expr v derive instance Eq v => Eq (Expr v) derive instance Functor Expr - -instance Foldable Expr where - foldr f b (Var x) = f x b - foldr f b (Atom _ xs) = foldr (\x b' -> foldr f b' x) b xs - - foldl f b (Var x) = f b x - foldl f b (Atom _ xs) = foldl (foldl f) b xs - - foldMap f (Var x) = f x - foldMap f (Atom _ xs) = foldl (<>) mempty (foldMap f <$> xs) - -instance Traversable Expr where - sequence (Var f) = Var <$> f - sequence (Atom name fs) = Atom name <$> sequence (sequence <$> fs) - - traverse f e = sequence (f <$> e) +derive instance Foldable Expr +derive instance Traversable Expr newtype IntVar = MkIntVar Int - derive instance Eq IntVar derive instance Ord IntVar @@ -80,22 +65,119 @@ instance UnificationVariable k => Unifiable k Expr where combine Nil (_:_) = (Var Fail) : Nil combine (x:xs) (y:ys) = alongside x y : combine xs ys -newtype Unifier a = MkUnifier (UnifyT IntVar Expr (SFKT Maybe) a) +-- note: unification expression ef not the same as functor-to-instantiate f, this way we can instantiate +-- things that contain expression etc. +instantiate :: forall k f ef m. Traversable f => MonadUnify k ef m => f Metavariable -> m (f k) +instantiate f = map fst $ runStateT (traverse metavariable f) Map.empty + +newtype Rule k = MkRule { name :: String, head :: Expr k, tail :: List (Expr k) } +derive instance Newtype (Rule k) _ +derive instance Functor Rule +derive instance Foldable Rule +derive instance Traversable Rule + +newtype Unifier a = MkUnifier (UnifyT IntVar Expr (SFKT List) a) derive instance Newtype (Unifier a) _ derive newtype instance Functor Unifier derive newtype instance Apply Unifier derive newtype instance Applicative Unifier +derive newtype instance Alt Unifier +derive newtype instance Plus Unifier derive newtype instance Alternative Unifier derive newtype instance Bind Unifier derive newtype instance Monad Unifier derive newtype instance MonadPlus Unifier derive newtype instance MonadUnify IntVar Expr Unifier +type Metavariable = String +type Metavariables k = Map Metavariable k + +metavariable :: forall k f m. MonadState (Metavariables k) m => MonadUnify k f m => Metavariable -> m k +metavariable s = do + r <- gets (lookup s) + case r of + Just v -> pure v + Nothing -> 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) -runUnifier :: forall a. Unifier a -> Maybe a -runUnifier m = runSFKT (runUnifyT $ un MkUnifier m) (const <<< Just) Nothing +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 + 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 + witnesses' <- traverse reifyProofTree witnesses + pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' } + +query :: Expr Metavariable -> Unifier (ProofTree IntVar) +query e = instantiate e >>= match rules >>= reifyProofTree + +runUnifier :: forall a. Unifier a -> List a +runUnifier m = runSFKTOnce (fst <$> (runUnifyT $ un MkUnifier m)) diff --git a/test/Main.purs b/test/Main.purs index dec1cde..86094cc 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -9,15 +9,5 @@ import Control.Monad.Unify.Class import Data.List import Data.Maybe -runSomeComputation :: forall m. MonadLogic m => MonadUnify IntVar Expr m => m (Expr IntVar) -runSomeComputation = do - x1 <- fresh - x2 <- fresh - let binPred = Atom "hello" $ fromFoldable [variable x1, variable x2] - let realBinPred = Atom "hello" $ fromFoldable [Atom "first" $ fromFoldable [], Atom "second" $ fromFoldable []] - unify binPred realBinPred - (unify (variable x1) (variable x2) >>= const (reify (variable x1))) `interleave` (unify (variable x1) (variable x1) >>= const (reify (variable x2))) - - -main :: Maybe (Expr IntVar) -main = runUnifier runSomeComputation +main :: List String +main = map toLatexProofTree $ runUnifier $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")