Use a reader monad to keep track of the rules
This commit is contained in:
parent
a9fc768182
commit
49b6b537b0
|
|
@ -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" ]
|
||||
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
Loading…
Reference in New Issue