Copy over implementation of Unify from Bergamot
This commit is contained in:
parent
4c8e62d7a3
commit
dc797e941a
12
spago.dhall
12
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.
|
to generate this file without the comments in this block.
|
||||||
-}
|
-}
|
||||||
{ name = "unifyt"
|
{ name = "unifyt"
|
||||||
, dependencies = [ "prelude" ]
|
, dependencies =
|
||||||
|
[ "control"
|
||||||
|
, "foldable-traversable"
|
||||||
|
, "lazy"
|
||||||
|
, "maybe"
|
||||||
|
, "newtype"
|
||||||
|
, "ordered-collections"
|
||||||
|
, "prelude"
|
||||||
|
, "transformers"
|
||||||
|
, "tuples"
|
||||||
|
]
|
||||||
, packages = ./packages.dhall
|
, packages = ./packages.dhall
|
||||||
, sources = [ "src/**/*.purs", "test/**/*.purs" ]
|
, sources = [ "src/**/*.purs", "test/**/*.purs" ]
|
||||||
}
|
}
|
||||||
|
|
45
src/Control/Monad/Unify/Class.purs
Normal file
45
src/Control/Monad/Unify/Class.purs
Normal file
|
@ -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
|
95
src/Control/Monad/Unify/Trans.purs
Normal file
95
src/Control/Monad/Unify/Trans.purs
Normal file
|
@ -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 }
|
|
@ -2,9 +2,5 @@ module Main where
|
||||||
|
|
||||||
import Prelude
|
import Prelude
|
||||||
|
|
||||||
import Effect (Effect)
|
main :: Unit
|
||||||
import Effect.Console (log)
|
main = unit
|
||||||
|
|
||||||
main :: Effect Unit
|
|
||||||
main = do
|
|
||||||
log "🍝"
|
|
||||||
|
|
|
@ -2,10 +2,5 @@ module Test.Main where
|
||||||
|
|
||||||
import Prelude
|
import Prelude
|
||||||
|
|
||||||
import Effect (Effect)
|
main :: Unit
|
||||||
import Effect.Class.Console (log)
|
main = unit
|
||||||
|
|
||||||
main :: Effect Unit
|
|
||||||
main = do
|
|
||||||
log "🍝"
|
|
||||||
log "You should add some tests."
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user