From 755d514342268effc535760a2f5ae05674f8d697 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 3 Mar 2023 23:19:52 -0800 Subject: [PATCH] Extract UnifyT into its own package and get an example going --- packages.dhall | 4 + spago.dhall | 1 + src/Language/Bergamot/Syntax.purs | 124 +++++------------------------- test/Main.purs | 21 ++++- 4 files changed, 43 insertions(+), 107 deletions(-) diff --git a/packages.dhall b/packages.dhall index 703dd67..83e83dc 100644 --- a/packages.dhall +++ b/packages.dhall @@ -106,3 +106,7 @@ in upstream with logict.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/logict.git" with logict.version = "24298710fa940bfcf2d272bc6d5c7417f2bfccfe" 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.dependencies = [ "control", "foldable-traversable", "lazy", "maybe", "newtype", "ordered-collections", "prelude", "transformers", "tuples" ] + diff --git a/spago.dhall b/spago.dhall index 445ef72..d953bde 100644 --- a/spago.dhall +++ b/spago.dhall @@ -24,6 +24,7 @@ to generate this file without the comments in this block. , "prelude" , "transformers" , "tuples" + , "unifyt" ] , packages = ./packages.dhall , sources = [ "src/**/*.purs", "test/**/*.purs" ] diff --git a/src/Language/Bergamot/Syntax.purs b/src/Language/Bergamot/Syntax.purs index 9c87741..413d4c2 100644 --- a/src/Language/Bergamot/Syntax.purs +++ b/src/Language/Bergamot/Syntax.purs @@ -13,6 +13,9 @@ 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.Trans (UnifyT(..), runUnifyT) +import Control.Monad.Logic.Trans (SFKT(..), runSFKT) import Data.List (List(..), (:)) import Data.Functor (class Functor, (<$>), map) import Data.Eq (class Eq) @@ -53,14 +56,6 @@ instance Traversable Expr where traverse f e = sequence (f <$> e) -data Stream k = StreamCons k (Lazy (Stream k)) - -pop :: forall k. Stream k -> Tuple k (Stream k) -pop (StreamCons k lks) = Tuple k (force lks) - -class Ord k <= UnificationVariable k where - variables :: Stream k - newtype IntVar = MkIntVar Int derive instance Eq IntVar @@ -70,16 +65,6 @@ instance UnificationVariable IntVar where variables = mkVarList 0 where mkVarList n = StreamCons (MkIntVar n) $ defer $ \_ -> mkVarList (n+1) -data ComparisonAction k f - = Merge k k - | Store k (f k) - | Fail - -class (UnificationVariable k, Traversable f) <= Unifiable k f where - variable :: k -> f k - squash :: f (f k) -> f k - alongside :: f k -> f k -> f (ComparisonAction k f) - instance UnificationVariable k => Unifiable k Expr where variable = Var squash (Var f) = f @@ -95,93 +80,22 @@ instance UnificationVariable k => Unifiable k Expr where combine Nil (_:_) = (Var Fail) : Nil combine (x:xs) (y:ys) = alongside x y : combine xs ys -class (Unifiable k f, MonadPlus m) <= MonadUnify k f m | m -> k, m -> f where - fresh :: m k - merge :: k -> k -> m Unit - store :: k -> f k -> m Unit - reify :: f k -> m (f k) +newtype Unifier a = MkUnifier (UnifyT IntVar Expr (SFKT Maybe) a) -unify :: forall k f m. MonadUnify k f m => f k -> f k -> m Unit -unify f1 f2 = - do - _ <- traverse process $ alongside f1 f2 - pure unit - where - process (Merge k1 k2) = merge k1 k2 - process (Store k f) = store k f - process Fail = empty +derive instance Newtype (Unifier a) _ +derive newtype instance Functor Unifier +derive newtype instance Apply Unifier +derive newtype instance Applicative 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 UnificationState k f = - { boundVariables :: Map k { equivalence :: Set k, boundTo :: Maybe (f k) } - , currentVariables :: Stream k - } +-- >:( +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 UnifyT k f m a = MkUnifyT (StateT (UnificationState k f) m a) - -derive instance Newtype (UnifyT k f m a) _ -derive instance Functor m => Functor (UnifyT k f m) - -instance Monad m => Apply (UnifyT k f m) where - apply m1 m2 = MkUnifyT $ apply (un MkUnifyT m1) (un MkUnifyT m2) - -instance Monad m => Applicative (UnifyT k f m) where - pure a = MkUnifyT $ pure a - -instance Monad m => Bind (UnifyT k f m) where - bind m f = MkUnifyT $ (un MkUnifyT m) >>= (un MkUnifyT <<< f) - -instance Monad m => Monad (UnifyT k f m) - -instance (Monad m, Alt m) => Alt (UnifyT k f m) where - alt = over2 MkUnifyT alt - -instance (Monad m, Plus m) => Plus (UnifyT k f m) where - empty = MkUnifyT empty - -instance (Monad m, Alternative m) => Alternative (UnifyT k f m) -instance (MonadPlus m) => MonadPlus (UnifyT k f m) - -instance MonadLogic m => MonadLogic (UnifyT k f m) where - msplit m = MkUnifyT $ map (map (rmap MkUnifyT)) $ msplit $ un MkUnifyT m - interleave m1 m2 = over2 MkUnifyT interleave m1 m2 - -instance (Unifiable k f, MonadPlus m) => MonadUnify k f (UnifyT k f m) where - fresh = MkUnifyT $ do - Tuple k restVariables <- gets (pop <<< _.currentVariables) - _ <- modify $ _ { currentVariables = restVariables } - pure k - merge k1 k2 = do - boundVariables <- MkUnifyT $ gets _.boundVariables - let - equivalence k = fromMaybe (singleton k) (_.equivalence <$> lookup k boundVariables) - boundTo k = lookup k boundVariables >>= _.boundTo - fullSet = equivalence k1 `union` equivalence k2 - newTerm <- - case boundTo k1 /\ boundTo k2 of - Just t1 /\ Just t2 -> unify t1 t2 >>= const (Just <$> reify t1) - Just t1 /\ Nothing -> pure $ Just t1 - Nothing /\ Just t2 -> pure $ Just t2 - Nothing /\ Nothing -> pure $ Nothing - let newMapValue = {equivalence: fullSet, boundTo: newTerm} - _ <- MkUnifyT $ modify $ _ { boundVariables = foldr (flip insert newMapValue) boundVariables fullSet } - pure unit - store k f = do - boundVariables <- MkUnifyT $ gets _.boundVariables - let fullSet = fromMaybe (singleton k) (_.equivalence <$> lookup k boundVariables) - let anyBound = any (isJust <<< (_>>=(_.boundTo)) <<< (flip lookup boundVariables)) fullSet - if anyBound - then empty - else do - let newMapValue = {equivalence: fullSet, boundTo: Just f} - _ <- MkUnifyT $ modify $ _ { boundVariables = foldr (flip insert newMapValue) boundVariables fullSet } - pure unit - reify f = - MkUnifyT $ do - boundVariables <- gets _.boundVariables - let - reify' f' = squash $ process <$> f' - process k = fromMaybe (variable k) (reify' <$> (lookup k boundVariables >>= _.boundTo)) - pure $ reify' f - -runUnifyT :: forall k f m a. Monad m => UnificationVariable k => UnifyT k f m a -> m a -runUnifyT m = fst <$> runStateT (un MkUnifyT m) { boundVariables: Map.empty, currentVariables: variables } +runUnifier :: forall a. Unifier a -> Maybe a +runUnifier m = runSFKT (runUnifyT $ un MkUnifier m) (const <<< Just) Nothing diff --git a/test/Main.purs b/test/Main.purs index 82fb9ee..dec1cde 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -1,6 +1,23 @@ module Test.Main where import Prelude +import Language.Bergamot.Syntax +import Control.Monad.Logic.Trans +import Control.Monad.Logic.Class +import Control.Monad.Unify.Trans +import Control.Monad.Unify.Class +import Data.List +import Data.Maybe -main :: Unit -main = unit +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