From dc797e941afd2640ad3447a463458d3da175f7b6 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 3 Mar 2023 22:42:05 -0800 Subject: [PATCH] Copy over implementation of Unify from Bergamot --- spago.dhall | 12 +++- src/Control/Monad/Unify/Class.purs | 45 ++++++++++++++ src/Control/Monad/Unify/Trans.purs | 95 ++++++++++++++++++++++++++++++ src/Main.purs | 8 +-- test/Main.purs | 9 +-- 5 files changed, 155 insertions(+), 14 deletions(-) create mode 100644 src/Control/Monad/Unify/Class.purs create mode 100644 src/Control/Monad/Unify/Trans.purs diff --git a/spago.dhall b/spago.dhall index dc82a52..0361cdb 100644 --- a/spago.dhall +++ b/spago.dhall @@ -11,7 +11,17 @@ When creating a new Spago project, you can use to generate this file without the comments in this block. -} { name = "unifyt" -, dependencies = [ "prelude" ] +, dependencies = + [ "control" + , "foldable-traversable" + , "lazy" + , "maybe" + , "newtype" + , "ordered-collections" + , "prelude" + , "transformers" + , "tuples" + ] , packages = ./packages.dhall , sources = [ "src/**/*.purs", "test/**/*.purs" ] } diff --git a/src/Control/Monad/Unify/Class.purs b/src/Control/Monad/Unify/Class.purs new file mode 100644 index 0000000..3dc8103 --- /dev/null +++ b/src/Control/Monad/Unify/Class.purs @@ -0,0 +1,45 @@ +module Control.Monad.Unify.Class where + +import Prelude (Unit, unit, ($)) + +import Control.Applicative (pure) +import Control.Bind (bind) +import Control.MonadPlus (class MonadPlus, empty) +import Data.Traversable (class Traversable, traverse) +import Data.Tuple (Tuple(..)) +import Data.Lazy (Lazy, force) +import Data.Ord (class Ord) + +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 + +data ComparisonAction k f + = Merge k k + | Store k (f k) + | Fail + +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) + +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) + +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 diff --git a/src/Control/Monad/Unify/Trans.purs b/src/Control/Monad/Unify/Trans.purs new file mode 100644 index 0000000..de23008 --- /dev/null +++ b/src/Control/Monad/Unify/Trans.purs @@ -0,0 +1,95 @@ +module Control.Monad.Unify.Trans where + +import Prelude (($), (<<<), const, flip, unit) + +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.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream, pop, squash, variable, variables, reify, unify) +import Control.Apply (class Apply, apply) +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 Data.Functor (class Functor, (<$>)) +import Data.Foldable (any, foldr) +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.Newtype (class Newtype, un, over2) +import Data.Maybe (Maybe(..), fromMaybe, isJust) + +type UnificationState k f = + { boundVariables :: Map k { equivalence :: Set k, boundTo :: Maybe (f k) } + , currentVariables :: Stream k + } + +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 (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 } diff --git a/src/Main.purs b/src/Main.purs index 5c18dca..dcf3198 100644 --- a/src/Main.purs +++ b/src/Main.purs @@ -2,9 +2,5 @@ module Main where import Prelude -import Effect (Effect) -import Effect.Console (log) - -main :: Effect Unit -main = do - log "🍝" +main :: Unit +main = unit diff --git a/test/Main.purs b/test/Main.purs index f91f98c..82fb9ee 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -2,10 +2,5 @@ module Test.Main where import Prelude -import Effect (Effect) -import Effect.Class.Console (log) - -main :: Effect Unit -main = do - log "🍝" - log "You should add some tests." +main :: Unit +main = unit