From 545416fce084125cbba4a9c3b43a1994aa2d1538 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 5 Mar 2023 18:44:56 -0800 Subject: [PATCH] Split the code into proper modules --- src/Language/Bergamot/Rules.purs | 42 ++++++++++ src/Language/Bergamot/Syntax.purs | 118 ++--------------------------- src/Language/Bergamot/Unifier.purs | 78 +++++++++++++++++++ test/Main.purs | 2 + 4 files changed, 127 insertions(+), 113 deletions(-) create mode 100644 src/Language/Bergamot/Rules.purs create mode 100644 src/Language/Bergamot/Unifier.purs diff --git a/src/Language/Bergamot/Rules.purs b/src/Language/Bergamot/Rules.purs new file mode 100644 index 0000000..de5b087 --- /dev/null +++ b/src/Language/Bergamot/Rules.purs @@ -0,0 +1,42 @@ +module Language.Bergamot.Rules where + +import Prelude + +import Language.Bergamot.Syntax (Expr) + +import Control.Monad.State.Trans (runStateT) +import Control.Monad.State.Class (class MonadState, gets, modify) +import Control.Monad.Unify.Class (class MonadUnify, fresh) +import Data.List (List) +import Data.Traversable (class Traversable, traverse) +import Data.Foldable (class Foldable) +import Data.Map (Map, lookup, insert) +import Data.Map as Map +import Data.Tuple (fst) +import Data.Newtype (class Newtype) +import Data.Maybe (Maybe(..)) + +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 + +type Metavariable = String +type Metavariables k = Map Metavariable k + +newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable, witnesses :: List (ProofTree 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 + +-- 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 diff --git a/src/Language/Bergamot/Syntax.purs b/src/Language/Bergamot/Syntax.purs index 91030ce..b701f1c 100644 --- a/src/Language/Bergamot/Syntax.purs +++ b/src/Language/Bergamot/Syntax.purs @@ -2,39 +2,11 @@ module Language.Bergamot.Syntax where import Prelude -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, join, (>>=)) -import Control.MonadPlus (class MonadPlus) -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) -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) -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) +import Control.Monad.Unify.Class (class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..)) +import Data.Foldable (class Foldable) +import Data.Traversable (class Traversable) +import Data.Lazy (defer) +import Data.List (List(..), (:)) data Expr v = Var v @@ -67,83 +39,3 @@ instance UnificationVariable k => Unifiable k Expr where 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 - -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 -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 - --- >:( -instance MonadAsk UnifierEnv Unifier where - ask = MkUnifier $ MkUnifyT ask - --- >:( -instance MonadReader UnifierEnv 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) - -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 - -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 - - -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 = spend $ do - MkRule {head, tail} <- instantiate rule - _ <- unify e' head - witnesses <- traverse (match rs) tail - pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses } - -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 = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree - -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/src/Language/Bergamot/Unifier.purs b/src/Language/Bergamot/Unifier.purs new file mode 100644 index 0000000..c0112f2 --- /dev/null +++ b/src/Language/Bergamot/Unifier.purs @@ -0,0 +1,78 @@ +module Language.Bergamot.Unifier where + +import Prelude + +import Language.Bergamot.Rules (Metavariable, ProofTree(..), Rule(..), instantiate) +import Language.Bergamot.Syntax (Expr, IntVar) + +import Control.Plus (class Plus, empty) +import Control.Apply (lift2) +import Control.Alt (class Alt) +import Control.Alternative (class Alternative) +import Control.MonadPlus (class MonadPlus) +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, 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.Traversable (traverse, oneOf) +import Data.Tuple (fst) +import Data.Newtype (class Newtype, un, over2) +import Data.Maybe (Maybe) +import Data.Bifunctor (rmap) + +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 +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 + +-- >:( +instance MonadAsk UnifierEnv Unifier where + ask = MkUnifier $ MkUnifyT ask + +-- >:( +instance MonadReader UnifierEnv 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) + +spend :: forall a. Unifier a -> Unifier a +spend m = do + n <- asks _.fuel + if n > 0 then local (_ { fuel = n - 1}) m else empty + +match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar) +match rs e = oneOf $ map (matchSingle e) rs + where + matchSingle e' rule = spend $ do + MkRule {head, tail} <- instantiate rule + _ <- unify e' head + witnesses <- traverse (match rs) tail + pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses } + +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 = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree + +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 db781a9..b208b33 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -2,6 +2,8 @@ module Test.Main where import Prelude import Language.Bergamot.Syntax +import Language.Bergamot.Rules +import Language.Bergamot.Unifier import Control.Monad.Logic.Trans import Control.Monad.Logic.Class import Control.Monad.Unify.Trans