184 lines
7.7 KiB
Plaintext
184 lines
7.7 KiB
Plaintext
module Language.Bergamot.Syntax where
|
|
|
|
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 (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.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(..), fresh, unify, reify)
|
|
import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
|
|
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, 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
|
|
import Data.Set (Set, singleton, union)
|
|
import Data.Tuple (Tuple(..), fst)
|
|
import Data.Tuple.Nested ((/\))
|
|
import Data.Lazy (Lazy, defer, force)
|
|
import Data.Newtype (class Newtype, un, over2)
|
|
import Data.Maybe (Maybe(..), fromMaybe, isJust)
|
|
import Data.Bifunctor (rmap)
|
|
|
|
data Expr v
|
|
= Var v
|
|
| Atom String (List (Expr v))
|
|
|
|
derive instance Eq v => Eq (Expr v)
|
|
derive instance Functor Expr
|
|
derive instance Foldable Expr
|
|
derive instance Traversable Expr
|
|
|
|
newtype IntVar = MkIntVar Int
|
|
derive instance Eq IntVar
|
|
derive instance Ord IntVar
|
|
|
|
instance UnificationVariable IntVar where
|
|
variables = mkVarList 0
|
|
where mkVarList n = StreamCons (MkIntVar n) $ defer $ \_ -> mkVarList (n+1)
|
|
|
|
instance UnificationVariable k => Unifiable k Expr where
|
|
variable = Var
|
|
squash (Var f) = f
|
|
squash (Atom name args) = Atom name $ squash <$> args
|
|
alongside (Var k1) (Var k2) = Var (Merge k1 k2)
|
|
alongside (Var k) f = Var (Store k f)
|
|
alongside f (Var k) = Var (Store k f)
|
|
alongside (Atom n1 _) (Atom n2 _) | n1 /= n2 = Var Fail
|
|
alongside (Atom n1 args1) (Atom _ args2) = Atom n1 $ combine args1 args2
|
|
where
|
|
combine Nil Nil = Nil
|
|
combine (_:_) Nil = (Var Fail) : Nil
|
|
combine Nil (_:_) = (Var Fail) : Nil
|
|
combine (x:xs) (y:ys) = alongside x y : combine xs ys
|
|
|
|
-- 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)
|
|
|
|
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))
|