unification-fd 0.6.0 → 0.7.0

raw patch · 13 files changed

+644/−410 lines, 13 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• README +2/−2
• VERSION +6/−0
• src/Control/Monad/EitherK.hs +28/−8
• src/Control/Monad/MaybeK.hs +26/−7
• src/Control/Monad/State/UnificationExtras.hs +2/−0
• src/Control/Unification.hs +377/−263
• src/Control/Unification/IntVar.hs +5/−7
• src/Control/Unification/Ranked.hs +48/−42
• src/Control/Unification/Ranked/IntVar.hs +5/−5
• src/Control/Unification/Ranked/STVar.hs +10/−9
• src/Control/Unification/STVar.hs +8/−7
• src/Control/Unification/Types.hs +125/−58
• unification-fd.cabal +2/−2

@@ -48,8 +48,8 @@     Rank2Types     MultiParamTypeClasses     FunctionalDependencies -- Alas, necessary for type inference-    FlexibleContexts       -- Generally necessary for practical use of MPTCs-    FlexibleInstances      -- Generally necessary for practical use of MPTCs+    FlexibleContexts       -- Necessary for practical use of MPTCs+    FlexibleInstances      -- Necessary for practical use of MPTCs     UndecidableInstances   -- Needed for Show instances due to two-level types  ----------------------------------------------------------- fin.

@@ -1,3 +1,9 @@+0.7.0 (2012-xx-xx):+    - Control.Unification: changed the type of seenAs to ensure that variables can only be seen as structure.+    - Renamed MutTerm to UTerm (and MutVar to UVar)+    - Replaced the Variable.eqVar method by plain old Eq.(==)+    - Control.Unification: added getFreeVarsAll, applyBindingsAll, freshenAll+    - Swapped type argument order for MutTerm, so that it can be a functor etc. Also changed BindingMonad, UnificationFailure, Rank, and RankedBindingMonad for consistency. 0.6.0 (2012-02-17):     - Removed the phantom type argument for Variables. 0.5.0 (2011-07-12):

@@ -3,7 +3,7 @@ {-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleInstances #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2011.06.30+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Monad.EitherK -- License     :  BSD@@ -108,8 +108,10 @@     fmap f (EK m) = EK (\k -> m (k . f))  instance Applicative (EitherK e) where-    pure  = return-    (<*>) = ap+    pure   = return+    (<*>)  = ap+    (*>)   = (>>)+    x <* y = x >>= \a -> y >> return a  instance Monad (EitherK e) where     return a   = EK (\k -> k a)@@ -152,14 +154,29 @@ toEitherKT (Right a) = return a  --- TODO: isn't there a better implementation that doesn't lose shortcircuiting? -- | Lift an @EitherK@ into an @EitherKT@. liftEitherK :: (Monad m) => EitherK e a -> EitherKT e m a {-# INLINE liftEitherK #-} liftEitherK = toEitherKT . runEitherK+--+-- With the above implementation, when @liftEitherK x@ is forced+-- it will force not only @x = EK m@, but will also force @m@. If+-- we want to force only @x@ and to defer @m@, then we should use+-- the following implementation instead:+--+-- > liftEitherK (EK m) = EKT (\k -> either (return . Left) k (m Right))+--+-- Or if we want to defer both @m@ and @x@, then we could use:+--+-- > liftEitherK x = EKT (\k -> either (return . Left) k (runEitherK x))+--+-- However, all versions need to reify @m@ at some point, and+-- therefore will lose short-circuiting. This is necessary since+-- given some @k :: a -> m (Either e r)@ we have no way of constructing+-- the needed @k' :: a -> Either e r@ from it without prematurely+-- executing the side-effects.  --- TODO: is there a better implementation? -- | Lower an @EitherKT@ into an @EitherK@. lowerEitherK :: (Monad m) => EitherKT e m a -> m (EitherK e a) {-# INLINE lowerEitherK #-}@@ -191,14 +208,17 @@     fmap f (EKT m) = EKT (\k -> m (k . f))  instance Applicative (EitherKT e m) where-    pure  = return-    (<*>) = ap+    pure   = return+    (<*>)  = ap+    (*>)   = (>>)+    x <* y = x >>= \a -> y >> return a  instance Monad (EitherKT e m) where     return a    = EKT (\k -> k a)     EKT m >>= f = EKT (\k -> m (\a -> case f a of EKT n -> n k)) --- TODO: is there any way to define catchEitherKT so it only requires Applicative m?+-- I'm pretty sure it's impossible to define a @(<|>)@ which only+-- requires @Applicative m@. instance (Monad m, Monoid e) => Alternative (EitherKT e m) where     empty = mzero     (<|>) = mplus

@@ -2,7 +2,7 @@ {-# LANGUAGE Rank2Types, MultiParamTypeClasses #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2011.06.30+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Monad.MaybeK -- License     :  BSD@@ -86,8 +86,10 @@     fmap f (MK m) = MK (\k -> m (k . f))  instance Applicative MaybeK where-    pure  = return-    (<*>) = ap+    pure   = return+    (<*>)  = ap+    (*>)   = (>>)+    x <* y = x >>= \a -> y >> return a  instance Monad MaybeK where     return a   = MK (\k -> k a)@@ -127,14 +129,29 @@ toMaybeKT (Just a) = return a  --- TODO: isn't there a better implementation that doesn't lose shortcircuiting? -- | Lift an @MaybeK@ into an @MaybeKT@. liftMaybeK :: (Monad m) => MaybeK a -> MaybeKT m a {-# INLINE liftMaybeK #-} liftMaybeK = toMaybeKT . runMaybeK+--+-- With the above implementation, when @liftMaybeK x@ is forced it+-- will force not only @x = MK m@, but will also force @m@. If we+-- want to force only @x@ and to defer @m@, then we should use the+-- following implementation instead:+--+-- > liftMaybeK (MK m) = MKT (\k -> maybe (return Nothing) k (m Just))+--+-- Or if we want to defer both @m@ and @x@, then we could use:+--+-- > liftMaybeK x = MKT (\k -> maybe (return Nothing) k (runMaybeK x))+--+-- However, all versions need to reify @m@ at some point, and+-- therefore will lose short-circuiting. This is necessary since+-- given some @k :: a -> m (Maybe r)@ we have no way of constructing+-- the needed @k' :: a -> Maybe r@ from it without prematurely+-- executing the side-effects.  --- TODO: is there a better implementation? -- | Lower an @MaybeKT@ into an @MaybeK@. lowerMaybeK :: (Monad m) => MaybeKT m a -> m (MaybeK a) {-# INLINE lowerMaybeK #-}@@ -145,8 +162,10 @@     fmap f (MKT m) = MKT (\k -> m (k . f))  instance Applicative (MaybeKT m) where-    pure  = return-    (<*>) = ap+    pure   = return+    (<*>)  = ap+    (*>)   = (>>)+    x <* y = x >>= \a -> y >> return a  instance Monad (MaybeKT m) where     return a    = MKT (\k -> k a)

@@ -35,12 +35,14 @@ -- | Lift a reader into a state monad. More particularly, this -- allows disabling mutability in a local context within @StateT@. liftReaderT :: (Monad m) => ReaderT e m a -> StateT e m a+{-# INLINE liftReaderT #-} liftReaderT r = StateT $ \e -> liftM (\a -> (a,e)) (runReaderT r e)   -- | Lift a reader into a state monad. More particularly, this -- allows disabling mutability in a local context within @State@. liftReader :: Reader e a -> State e a+{-# INLINE liftReader #-} liftReader = liftReaderT  

@@ -1,7 +1,7 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}-{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-} -------------------------------------------------------------------                                                  ~ 2012.02.17+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Unification -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton@@ -27,8 +27,8 @@ module Control.Unification     (     -- * Data types, classes, etc-    -- ** Mutable terms-      MutTerm(..)+    -- ** Unification terms+      UTerm(..)     , freeze     , unfreeze     -- ** Errors@@ -60,12 +60,19 @@     , unifyOccurs     , subsumes     +    -- * Operations on many terms+    , getFreeVarsAll+    , applyBindingsAll+    , freshenAll+    -- subsumesAll -- to ensure that there's a single coherent substitution allowing the schema to subsume all the terms in some collection. +     -- * Helper functions     -- | Client code should not need to use these functions, but     -- they are exposed just in case they are needed.     , fullprune     , semiprune     , occursIn+    -- TODO: add a post-hoc occurs check in order to have a version of unify which is fast, yet is also guaranteed to fail when it ought to (rather than deferring the failure until later, as the current unify does).     ) where  import Prelude@@ -75,6 +82,7 @@ import qualified Data.IntSet as IS import Data.Foldable import Data.Traversable+import Control.Monad.Identity (Identity(..)) import Control.Applicative import Control.Monad       (MonadPlus(..)) import Control.Monad.Trans (MonadTrans(..))@@ -93,18 +101,16 @@ -- the chain is unbound), and return that end. -- -- N.B., this is almost never the function you want. Cf., 'semiprune'.-fullprune :: (BindingMonad v t m) => MutTerm v t -> m (MutTerm v t)-fullprune t0 =-    case t0 of-    MutTerm _ -> return t0-    MutVar  v -> do-        mb <- lookupVar v-        case mb of-            Nothing -> return t0-            Just t  -> do-                finalTerm <- fullprune t-                v `bindVar` finalTerm-                return finalTerm+fullprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)+fullprune t0@(UTerm _ ) = return t0+fullprune t0@(UVar  v0) = do+    mb <- lookupVar v0+    case mb of+        Nothing -> return t0+        Just t  -> do+            finalTerm <- fullprune t+            v0 `bindVar` finalTerm+            return finalTerm   -- N.B., this assumes there are no directly-cyclic chains!@@ -114,24 +120,21 @@ -- bound or not. This allows detecting many cases where multiple -- variables point to the same term, thereby allowing us to avoid -- re-unifying the term they point to.-semiprune :: (BindingMonad v t m) => MutTerm v t -> m (MutTerm v t)-semiprune =-    \t0 ->-        case t0 of-        MutTerm _  -> return t0-        MutVar  v0 -> loop t0 v0+semiprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)+semiprune t0@(UTerm _ ) = return t0+semiprune t0@(UVar  v0) = loop t0 v0     where     -- We pass the @t@ for @v@ in order to add just a little more sharing.-    loop t v = do-        mb <- lookupVar v+    loop t0 v0 = do+        mb <- lookupVar v0         case mb of-            Nothing -> return t-            Just t' -> -                case t' of-                MutTerm _  -> return t-                MutVar  v' -> do-                    finalVar <- loop t' v'-                    v `bindVar` finalVar+            Nothing -> return t0+            Just t  -> +                case t  of+                UTerm _  -> return t0+                UVar  v  -> do+                    finalVar <- loop t v+                    v0 `bindVar` finalVar                     return finalVar  @@ -139,32 +142,36 @@ -- Since occurs checks only make sense when we're about to bind the -- variable to the term, we do not bother checking for the possibility -- of the variable occuring bound in the term.-occursIn :: (BindingMonad v t m) => v -> MutTerm v t -> m Bool-occursIn v t0 = do-    t <- fullprune t0-    case t of-        MutTerm t' -> or <$> mapM (v `occursIn`) t' -- TODO: use foldlM instead-        MutVar  v' -> return $! v `eqVar` v'+occursIn :: (BindingMonad t v m) => v -> UTerm t v -> m Bool+{-# INLINE occursIn #-}+occursIn v0 t0 = do+    t0 <- fullprune t0+    case t0 of+        UTerm t -> or <$> mapM (v0 `occursIn`) t+            -- TODO: benchmark the following for shortcircuiting+            -- > Traversable.foldlM (\b t' -> if b then return True else v0 `occursIn` t') t+        UVar  v -> return $! v0 == v   -- TODO: use IM.insertWith or the like to do this in one pass+-- -- | Update the visited-set with a seclaration that a variable has -- been seen with a given binding, or throw 'OccursIn' if the -- variable has already been seen. seenAs-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => v               -- ^-    -> MutTerm v t     -- ^-    -> StateT (IM.IntMap (MutTerm v t)) (e m) ()+    => v -- ^+    -> t (UTerm t v) -- ^+    -> StateT (IM.IntMap (t (UTerm t v))) (e m) () -- ^ {-# INLINE seenAs #-}-seenAs v t = do+seenAs v0 t0 = do     seenVars <- get-    case IM.lookup (getVarID v) seenVars of-        Just t' -> lift . throwError $ OccursIn v t'-        Nothing -> put $! IM.insert (getVarID v) t seenVars+    case IM.lookup (getVarID v0) seenVars of+        Just t  -> lift . throwError $ OccursIn v0 (UTerm t)+        Nothing -> put $! IM.insert (getVarID v0) t0 seenVars  ---------------------------------------------------------------- ----------------------------------------------------------------@@ -178,18 +185,41 @@ -- TODO: Figure out how to abstract the left-catamorphism from these.  --- | Walk a term and determine what variables are still free. N.B.,+-- | Walk a term and determine which variables are still free. N.B., -- this function does not detect cyclic terms (i.e., throw errors), -- but it will return the correct answer for them in finite time.-getFreeVars :: (BindingMonad v t m) => MutTerm v t -> m [v]-getFreeVars =-    \t -> IM.elems <$> evalStateT (loop t) IS.empty+getFreeVars :: (BindingMonad t v m) => UTerm t v -> m [v]+getFreeVars = getFreeVarsAll . Identity+++-- TODO: Should we return the IntMap instead?+--+-- | Same as 'getFreeVars', but works on several terms simultaneously.+-- This is more efficient than getting the free variables for each+-- of the terms separately because we can make use of sharing across+-- the whole collection. That is, each time we move to the next+-- term, we still remember the bound variables we've already looked+-- at (and therefore do not need to traverse, since we've already+-- seen whatever free variables there are down there); whereas we+-- would forget between each call to @getFreeVars@.+--+-- /Since: 0.7.0/+getFreeVarsAll+    :: (BindingMonad t v m, Foldable s)+    => s (UTerm t v) -> m [v]+getFreeVarsAll ts0 =+    IM.elems <$> evalStateT (loopAll ts0) IS.empty     where+    -- TODO: is that the most efficient direction/associativity?+    loopAll = foldrM (\t r -> IM.union r <$> loop t) IM.empty+         loop t0 = do-        t1 <- lift $ semiprune t0-        case t1 of-            MutTerm t -> fold <$> mapM loop t -- TODO: use foldlM instead?-            MutVar  v -> do+        t0 <- lift $ semiprune t0+        case t0 of+            UTerm t -> fold <$> mapM loop t+                -- TODO: benchmark using the following instead:+                -- > foldMapM f = foldlM (\a b -> mappend a <$> f b) mempty+            UVar  v -> do                 seenVars <- get                 let i = getVarID v                 if IS.member i seenVars@@ -212,21 +242,38 @@ -- If any cyclic bindings are detected, then an 'OccursIn' exception -- will be thrown. applyBindings-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t       -- ^-    -> e m (MutTerm v t) -- ^-applyBindings =-    \t -> evalStateT (loop t) IM.empty+    => UTerm t v       -- ^+    -> e m (UTerm t v) -- ^+applyBindings = fmap runIdentity . applyBindingsAll . Identity+++-- | Same as 'applyBindings', but works on several terms simultaneously.+-- This function preserves sharing across the entire collection of+-- terms, whereas applying the bindings to each term separately+-- would only preserve sharing within each term.+--+-- /Since: 0.7.0/+applyBindingsAll+    ::  ( BindingMonad t v m+        , MonadTrans e+        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+        , MonadError (UnificationFailure t v) (e m)+        , Traversable s+        )+    => s (UTerm t v)       -- ^+    -> e m (s (UTerm t v)) -- ^+applyBindingsAll ts0 = evalStateT (mapM loop ts0) IM.empty     where     loop t0 = do-        t1 <- lift . lift $ semiprune t0-        case t1 of-            MutTerm t -> MutTerm <$> mapM loop t-            MutVar  v -> do+        t0 <- lift . lift $ semiprune t0+        case t0 of+            UTerm t -> UTerm <$> mapM loop t+            UVar  v -> do                 let i = getVarID v                 mb <- IM.lookup i <$> get                 case mb of@@ -235,7 +282,7 @@                     Nothing -> do                         mb' <- lift . lift $ lookupVar v                         case mb' of-                            Nothing -> return t1+                            Nothing -> return t0                             Just t  -> do                                 modify' . IM.insert i $ Left t                                 t' <- loop t@@ -251,21 +298,47 @@ -- If any cyclic bindings are detected, then an 'OccursIn' exception -- will be thrown. freshen-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t       -- ^-    -> e m (MutTerm v t) -- ^-freshen =-    \t -> evalStateT (loop t) IM.empty+    => UTerm t v       -- ^+    -> e m (UTerm t v) -- ^+freshen = fmap runIdentity . freshenAll . Identity+++-- | Same as 'freshen', but works on several terms simultaneously.+-- This is different from freshening each term separately, because+-- @freshenAll@ preserves the relationship between the terms. For+-- instance, the result of+--+-- > mapM freshen [UVar 1, UVar 1]+--+-- would be @[UVar 2, UVar 3]@ or something alpha-equivalent, whereas+-- the result of+--+-- > freshenAll [UVar 1, UVar 1]+--+-- would be @[UVar 2, UVar 2]@ or something alpha-equivalent.+--+-- /Since: 0.7.0/+freshenAll+    ::  ( BindingMonad t v m+        , MonadTrans e+        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+        , MonadError (UnificationFailure t v) (e m)+        , Traversable s+        )+    => s (UTerm t v)       -- ^+    -> e m (s (UTerm t v)) -- ^+freshenAll ts0 = evalStateT (mapM loop ts0) IM.empty     where     loop t0 = do-        t1 <- lift . lift $ semiprune t0-        case t1 of-            MutTerm t -> MutTerm <$> mapM loop t-            MutVar  v -> do+        t0 <- lift . lift $ semiprune t0+        case t0 of+            UTerm t -> UTerm <$> mapM loop t+            UVar  v -> do                 let i = getVarID v                 seenVars <- get                 case IM.lookup i seenVars of@@ -275,13 +348,13 @@                         mb <- lift . lift $ lookupVar v                         case mb of                             Nothing -> do-                                v' <- lift . lift $ MutVar <$> freeVar+                                v' <- lift . lift $ UVar <$> freeVar                                 put $! IM.insert i (Right v') seenVars                                 return v'                             Just t  -> do                                 put $! IM.insert i (Left t) seenVars                                 t' <- loop t-                                v' <- lift . lift $ MutVar <$> newVar t'+                                v' <- lift . lift $ UVar <$> newVar t'                                 modify' $ IM.insert i (Right v')                                 return v' @@ -291,53 +364,66 @@  -- | 'equals' (===)-    :: (BindingMonad v t m)-    => MutTerm v t  -- ^-    -> MutTerm v t  -- ^-    -> m Bool       -- ^+    :: (BindingMonad t v m)+    => UTerm t v  -- ^+    -> UTerm t v  -- ^+    -> m Bool     -- ^ (===) = equals+{-# INLINE (===) #-} infix 4 ===, `equals`   -- | 'equiv' (=~=)-    :: (BindingMonad v t m)-    => MutTerm v t               -- ^-    -> MutTerm v t               -- ^+    :: (BindingMonad t v m)+    => UTerm t v                 -- ^+    -> UTerm t v                 -- ^     -> m (Maybe (IM.IntMap Int)) -- ^ (=~=) = equiv+{-# INLINE (=~=) #-} infix 4 =~=, `equiv`   -- | 'unify' (=:=)-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t       -- ^-    -> MutTerm v t       -- ^-    -> e m (MutTerm v t) -- ^+    => UTerm t v       -- ^+    -> UTerm t v       -- ^+    -> e m (UTerm t v) -- ^ (=:=) = unify+{-# INLINE (=:=) #-} infix 4 =:=, `unify`   -- | 'subsumes' (<:=)-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t -- ^-    -> MutTerm v t -- ^-    -> e m Bool+    => UTerm t v -- ^+    -> UTerm t v -- ^+    -> e m Bool  -- ^ (<:=) = subsumes+{-# INLINE (<:=) #-} infix 4 <:=, `subsumes`  ---------------------------------------------------------------- +{- BUG:+If we don't use anything special, then there's a 2x overhead for+calling 'equals' (and probably the rest of them too). If we add a+SPECIALIZE pragma, or if we try to use MaybeT instead of MaybeKT+then that jumps up to 4x overhead. However, if we add an INLINE+pragma then it gets faster than the same implementation in the+benchmark file. I've no idea what's going on here...+-}+ -- TODO: should we offer a variant which gives the reason for failure? -- -- | Determine if two terms are structurally equal. This is essentially@@ -346,39 +432,45 @@ -- function does not consider alpha-variance, and thus variables -- with different names are considered unequal. Cf., 'equiv'. equals-    :: (BindingMonad v t m)-    => MutTerm v t  -- ^-    -> MutTerm v t  -- ^-    -> m Bool       -- ^-equals =-    \tl tr -> do-        mb <- runMaybeKT (loop tl tr)-        case mb of-            Nothing -> return False-            Just () -> return True+    :: (BindingMonad t v m)+    => UTerm t v  -- ^+    -> UTerm t v  -- ^+    -> m Bool     -- ^+equals tl0 tr0 = do+    mb <- runMaybeKT (loop tl0 tr0)+    case mb of+        Nothing -> return False+        Just () -> return True     where     loop tl0 tr0 = do-        tl <- lift $ semiprune tl0-        tr <- lift $ semiprune tr0-        case (tl, tr) of-            (MutVar vl', MutVar vr')-                | vl' `eqVar` vr' -> return () -- success-                | otherwise       -> do-                    mtl <- lift $ lookupVar vl'-                    mtr <- lift $ lookupVar vr'+        tl0 <- lift $ semiprune tl0+        tr0 <- lift $ semiprune tr0+        case (tl0, tr0) of+            (UVar vl, UVar vr)+                | vl == vr  -> return () -- success+                | otherwise -> do+                    mtl <- lift $ lookupVar vl+                    mtr <- lift $ lookupVar vr                     case (mtl, mtr) of-                        (Nothing,  Nothing ) -> mzero-                        (Nothing,  Just _  ) -> mzero-                        (Just _,   Nothing ) -> mzero-                        (Just tl', Just tr') -> loop tl' tr' -- TODO: should just jump to match-            (MutVar  _,   MutTerm _  ) -> mzero-            (MutTerm _,   MutVar  _  ) -> mzero-            (MutTerm tl', MutTerm tr') ->-                case zipMatch tl' tr' of-                Nothing  -> mzero-                Just tlr -> mapM_ (uncurry loop) tlr+                        (Nothing,         Nothing)         -> mzero+                        (Nothing,         Just _ )         -> mzero+                        (Just _,          Nothing)         -> mzero+                        (Just (UTerm tl), Just (UTerm tr)) -> match tl tr+                        _ -> error _impossible_equals+            (UVar  _,  UTerm _ ) -> mzero+            (UTerm _,  UVar  _ ) -> mzero+            (UTerm tl, UTerm tr) -> match tl tr+    +    match tl tr =+        case zipMatch tl tr of+        Nothing  -> mzero+        Just tlr -> mapM_ (uncurry loop) tlr +_impossible_equals :: String+{-# NOINLINE _impossible_equals #-}+_impossible_equals = "equals: the impossible happened" + -- TODO: is that the most helpful return type? -- -- | Determine if two terms are structurally equivalent; that is,@@ -386,20 +478,19 @@ -- mapping from variable IDs of the left term to variable IDs of -- the right term, indicating the renaming used. equiv-    :: (BindingMonad v t m)-    => MutTerm v t               -- ^-    -> MutTerm v t               -- ^+    :: (BindingMonad t v m)+    => UTerm t v                 -- ^+    -> UTerm t v                 -- ^     -> m (Maybe (IM.IntMap Int)) -- ^-equiv =-    \tl tr -> runMaybeKT (execStateT (loop tl tr) IM.empty)+equiv tl0 tr0 = runMaybeKT (execStateT (loop tl0 tr0) IM.empty)     where     loop tl0 tr0 = do-        tl <- lift . lift $ fullprune tl0-        tr <- lift . lift $ fullprune tr0-        case (tl, tr) of-            (MutVar vl',  MutVar  vr') -> do-                let il = getVarID vl'-                let ir = getVarID vr'+        tl0 <- lift . lift $ fullprune tl0+        tr0 <- lift . lift $ fullprune tr0+        case (tl0, tr0) of+            (UVar vl,  UVar  vr) -> do+                let il = getVarID vl+                let ir = getVarID vr                 xs <- get                 case IM.lookup il xs of                     Just x@@ -407,10 +498,10 @@                         | otherwise -> lift mzero                     Nothing         -> put $! IM.insert il ir xs             -            (MutVar _,    MutTerm _  ) -> lift mzero-            (MutTerm _,   MutVar  _  ) -> lift mzero-            (MutTerm tl', MutTerm tr') ->-                case zipMatch tl' tr' of+            (UVar  _,  UTerm _ ) -> lift mzero+            (UTerm _,  UVar  _ ) -> lift mzero+            (UTerm tl, UTerm tr) ->+                case zipMatch tl tr of                 Nothing  -> lift mzero                 Just tlr -> mapM_ (uncurry loop) tlr @@ -425,14 +516,14 @@ -- it slow, it's asymptotically slow since it can cause the same -- subterm to be traversed multiple times. unifyOccurs-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t       -- ^-    -> MutTerm v t       -- ^-    -> e m (MutTerm v t) -- ^+    => UTerm t v       -- ^+    -> UTerm t v       -- ^+    -> e m (UTerm t v) -- ^ unifyOccurs = loop     where     {-# INLINE (=:) #-}@@ -447,61 +538,70 @@          -- TODO: cf todos in 'unify'     loop tl0 tr0 = do-        tl <- lift $ semiprune tl0-        tr <- lift $ semiprune tr0-        case (tl, tr) of-            (MutVar vl', MutVar vr')-                | vl' `eqVar` vr' -> return tr-                | otherwise       -> do-                    mtl <- lift $ lookupVar vl'-                    mtr <- lift $ lookupVar vr'+        tl0 <- lift $ semiprune tl0+        tr0 <- lift $ semiprune tr0+        case (tl0, tr0) of+            (UVar vl, UVar vr)+                | vl == vr  -> return tr0+                | otherwise -> do+                    mtl <- lift $ lookupVar vl+                    mtr <- lift $ lookupVar vr                     case (mtl, mtr) of-                        (Nothing,  Nothing ) -> do-                            vl' =: tr-                            return tr-                        (Nothing,  Just _  ) -> do-                            vl' `acyclicBindVar` tr-                            return tr-                        (Just _  , Nothing ) -> do-                            vr' `acyclicBindVar` tl-                            return tl-                        (Just tl', Just tr') -> do-                            t <- loop tl' tr'-                            vr' =: t-                            vl' =: tr-                            return tr+                        (Nothing, Nothing) -> do+                            vl =: tr0+                            return tr0+                        (Nothing, Just _ ) -> do+                            vl `acyclicBindVar` tr0+                            return tr0+                        (Just _ , Nothing) -> do+                            vr `acyclicBindVar` tl0+                            return tl0+                        (Just (UTerm tl), Just (UTerm tr)) -> do+                            t <- match tl tr+                            vr =: t+                            vl =: tr0+                            return tr0+                        _ -> error _impossible_unifyOccurs             -            (MutVar vl', MutTerm _) -> do-                mtl <- lift $ lookupVar vl'+            (UVar vl, UTerm tr) -> do+                mtl <- lift $ lookupVar vl                 case mtl of                     Nothing  -> do-                        vl' `acyclicBindVar` tr-                        return tl-                    Just tl' -> do-                        t <- loop tl' tr-                        vl' =: t-                        return tl+                        vl `acyclicBindVar` tr0+                        return tl0+                    Just (UTerm tl) -> do+                        t <- match tl tr+                        vl =: t+                        return tl0+                    _ -> error _impossible_unifyOccurs             -            (MutTerm _, MutVar vr') -> do-                mtr <- lift $ lookupVar vr'+            (UTerm tl, UVar vr) -> do+                mtr <- lift $ lookupVar vr                 case mtr of                     Nothing  -> do-                        vr' `acyclicBindVar` tl-                        return tr-                    Just tr' -> do-                        t <- loop tl tr'-                        vr' =: t-                        return tr+                        vr `acyclicBindVar` tl0+                        return tr0+                    Just (UTerm tr) -> do+                        t <- match tl tr+                        vr =: t+                        return tr0+                    _ -> error _impossible_unifyOccurs             -            (MutTerm tl', MutTerm tr') ->-                case zipMatch tl' tr' of-                Nothing  -> throwError $ TermMismatch tl' tr'-                Just tlr -> MutTerm <$> mapM (uncurry loop) tlr+            (UTerm tl, UTerm tr) -> match tl tr+    +    match tl tr =+        case zipMatch tl tr of+        Nothing  -> throwError $ TermMismatch tl tr+        Just tlr -> UTerm <$> mapM (uncurry loop) tlr +_impossible_unifyOccurs :: String+{-# NOINLINE _impossible_unifyOccurs #-}+_impossible_unifyOccurs = "unifyOccurs: the impossible happened" + ---------------------------------------------------------------- -- TODO: verify correctness, especially for the visited-set stuff.--- TODO: return Maybe(MutTerm v t) in the loop so we can avoid updating bindings trivially+-- TODO: return Maybe(UTerm t v) in the loop so we can avoid updating bindings trivially -- TODO: figure out why unifyOccurs is so much faster on pure ground terms!! The only difference there is in lifting over StateT... --  -- | Unify two terms, or throw an error with an explanation of why@@ -511,70 +611,78 @@ -- aggressive opportunistic observable sharing, so it will be more -- efficient to use it in future calculations than either argument. unify-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t       -- ^-    -> MutTerm v t       -- ^-    -> e m (MutTerm v t) -- ^-unify =-    \tl tr -> evalStateT (loop tl tr) IM.empty+    => UTerm t v       -- ^+    -> UTerm t v       -- ^+    -> e m (UTerm t v) -- ^+unify tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty     where     {-# INLINE (=:) #-}     v =: t = lift . lift $ v `bindVar` t          -- TODO: would it be beneficial to manually fuse @x <- lift m; y <- lift n@ to @(x,y) <- lift (m;n)@ everywhere we can?     loop tl0 tr0 = do-        tl <- lift . lift $ semiprune tl0-        tr <- lift . lift $ semiprune tr0-        case (tl, tr) of-            (MutVar vl', MutVar vr')-                | vl' `eqVar` vr' -> return tr-                | otherwise       -> do-                    mtl <- lift . lift $ lookupVar vl'-                    mtr <- lift . lift $ lookupVar vr'+        tl0 <- lift . lift $ semiprune tl0+        tr0 <- lift . lift $ semiprune tr0+        case (tl0, tr0) of+            (UVar vl, UVar vr)+                | vl == vr  -> return tr0+                | otherwise -> do+                    mtl <- lift . lift $ lookupVar vl+                    mtr <- lift . lift $ lookupVar vr                     case (mtl, mtr) of-                        (Nothing,  Nothing ) -> do vl' =: tr ; return tr-                        (Nothing,  Just _  ) -> do vl' =: tr ; return tr-                        (Just _  , Nothing ) -> do vr' =: tl ; return tl-                        (Just tl', Just tr') -> do+                        (Nothing, Nothing) -> do vl =: tr0 ; return tr0+                        (Nothing, Just _ ) -> do vl =: tr0 ; return tr0+                        (Just _ , Nothing) -> do vr =: tl0 ; return tl0+                        (Just (UTerm tl), Just (UTerm tr)) -> do                             t <- localState $ do-                                vl' `seenAs` tl'-                                vr' `seenAs` tr'-                                loop tl' tr' -- TODO: should just jump to match-                            vr' =: t-                            vl' =: tr-                            return tr+                                vl `seenAs` tl+                                vr `seenAs` tr+                                match tl tr+                            vr =: t+                            vl =: tr0+                            return tr0+                        _ -> error _impossible_unify             -            (MutVar vl', MutTerm _) -> do+            (UVar vl, UTerm tr) -> do                 t <- do-                    mtl <- lift . lift $ lookupVar vl'+                    mtl <- lift . lift $ lookupVar vl                     case mtl of-                        Nothing  -> return tr-                        Just tl' -> localState $ do-                            vl' `seenAs` tl'-                            loop tl' tr -- TODO: should just jump to match-                vl' =: t-                return tl+                        Nothing         -> return tr0+                        Just (UTerm tl) -> localState $ do+                            vl `seenAs` tl+                            match tl tr+                        _ -> error _impossible_unify+                vl =: t+                return tl0             -            (MutTerm _, MutVar vr') -> do+            (UTerm tl, UVar vr) -> do                 t <- do-                    mtr <- lift . lift $ lookupVar vr'+                    mtr <- lift . lift $ lookupVar vr                     case mtr of-                        Nothing  -> return tl-                        Just tr' -> localState $ do-                            vr' `seenAs` tr'-                            loop tl tr' -- TODO: should just jump to match-                vr' =: t-                return tr+                        Nothing         -> return tl0+                        Just (UTerm tr) -> localState $ do+                            vr `seenAs` tr+                            match tl tr+                        _ -> error _impossible_unify+                vr =: t+                return tr0             -            (MutTerm tl', MutTerm tr') ->-                case zipMatch tl' tr' of-                Nothing  -> lift . throwError $ TermMismatch tl' tr'-                Just tlr -> MutTerm <$> mapM (uncurry loop) tlr+            (UTerm tl, UTerm tr) -> match tl tr+    +    match tl tr =+        case zipMatch tl tr of+        Nothing  -> lift . throwError $ TermMismatch tl tr+        Just tlr -> UTerm <$> mapM (uncurry loop) tlr +_impossible_unify :: String+{-# NOINLINE _impossible_unify #-}+_impossible_unify = "unify: the impossible happened"+ ---------------------------------------------------------------- -- TODO: can we find an efficient way to return the bindings directly instead of altering the monadic bindings? Maybe another StateT IntMap taking getVarID to the variable and its pseudo-bound term? --@@ -598,55 +706,61 @@ -- or else requires specifying too much about the implementation -- of variables. subsumes-    ::  ( BindingMonad v t m+    ::  ( BindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t -- ^-    -> MutTerm v t -- ^-    -> e m Bool-subsumes =-    \tl tr -> evalStateT (loop tl tr) IM.empty+    => UTerm t v -- ^+    -> UTerm t v -- ^+    -> e m Bool  -- ^+subsumes tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty     where     {-# INLINE (=:) #-}     v =: t = lift . lift $ do v `bindVar` t ; return True          -- TODO: cf todos in 'unify'     loop tl0 tr0 = do-        tl <- lift . lift $ semiprune tl0-        tr <- lift . lift $ semiprune tr0-        case (tl, tr) of-            (MutVar vl', MutVar vr')-                | vl' `eqVar` vr' -> return True-                | otherwise       -> do-                    mtl <- lift . lift $ lookupVar vl'-                    mtr <- lift . lift $ lookupVar vr'+        tl0 <- lift . lift $ semiprune tl0+        tr0 <- lift . lift $ semiprune tr0+        case (tl0, tr0) of+            (UVar vl, UVar vr)+                | vl == vr  -> return True+                | otherwise -> do+                    mtl <- lift . lift $ lookupVar vl+                    mtr <- lift . lift $ lookupVar vr                     case (mtl, mtr) of-                        (Nothing,  Nothing ) -> vl' =: tr-                        (Nothing,  Just _  ) -> vl' =: tr-                        (Just _  , Nothing ) -> return False-                        (Just tl', Just tr') ->+                        (Nothing,         Nothing)         -> vl =: tr0+                        (Nothing,         Just _ )         -> vl =: tr0+                        (Just _ ,         Nothing)         -> return False+                        (Just (UTerm tl), Just (UTerm tr)) ->                             localState $ do-                                vl' `seenAs` tl'-                                vr' `seenAs` tr'-                                loop tl' tr'+                                vl `seenAs` tl+                                vr `seenAs` tr+                                match tl tr+                        _ -> error _impossible_subsumes             -            (MutVar vl',  MutTerm _  ) -> do-                mtl <- lift . lift $ lookupVar vl'+            (UVar vl,  UTerm tr) -> do+                mtl <- lift . lift $ lookupVar vl                 case mtl of-                    Nothing  -> vl' =: tr-                    Just tl' -> localState $ do-                        vl' `seenAs` tl'-                        loop tl' tr+                    Nothing         -> vl =: tr0+                    Just (UTerm tl) -> localState $ do+                        vl `seenAs` tl+                        match tl tr+                    _ -> error _impossible_subsumes             -            (MutTerm _,   MutVar  _  ) -> return False+            (UTerm _,  UVar  _ ) -> return False             -            (MutTerm tl', MutTerm tr') ->-                case zipMatch tl' tr' of-                Nothing  -> return False-                Just tlr -> and <$> mapM (uncurry loop) tlr+            (UTerm tl, UTerm tr) -> match tl tr     +    match tl tr =+        case zipMatch tl tr of+        Nothing  -> return False+        Just tlr -> and <$> mapM (uncurry loop) tlr -- TODO: use foldlM?++_impossible_subsumes :: String+{-# NOINLINE _impossible_subsumes #-}+_impossible_subsumes = "subsumes: the impossible happened"  ---------------------------------------------------------------- ----------------------------------------------------------- fin.

@@ -4,7 +4,7 @@            #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2012.02.17+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Unification.IntVar -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton@@ -57,7 +57,7 @@ -- N.B., because this implementation is pure, we can use it for -- both ranked and unranked monads. newtype IntVar = IntVar Int-    deriving (Show)+    deriving (Show, Eq)  {- -- BUG: This part works, but we'd want to change Show IntBindingState too.@@ -74,8 +74,6 @@ -}  instance Variable IntVar where-    eqVar (IntVar i) (IntVar j) = i == j-         getVarID (IntVar v) = v  @@ -83,11 +81,11 @@ -- | Binding state for 'IntVar'. data IntBindingState t = IntBindingState     { nextFreeVar :: {-# UNPACK #-} !Int-    , varBindings :: IM.IntMap (MutTerm IntVar t)+    , varBindings :: IM.IntMap (UTerm t IntVar)     }  -- Can't derive this because it's an UndecidableInstance-instance (Show (t (MutTerm IntVar t))) =>+instance (Show (t (UTerm t IntVar))) =>     Show (IntBindingState t)     where     show (IntBindingState nr bs) =@@ -174,7 +172,7 @@ ----------------------------------------------------------------  instance (Unifiable t, Applicative m, Monad m) =>-    BindingMonad IntVar t (IntBindingT t m)+    BindingMonad t IntVar (IntBindingT t m)     where          lookupVar (IntVar v) = IBT $ gets (IM.lookup v . varBindings)

@@ -1,7 +1,7 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}-{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-} -------------------------------------------------------------------                                                  ~ 2011.07.11+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Unification.Ranked -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton@@ -41,6 +41,12 @@     , unify     -- unifyOccurs     -- subsumes+    +    -- * Operations on many terms+    , getFreeVarsAll+    , applyBindingsAll+    , freshenAll+    -- subsumesAll     ) where  import Prelude@@ -60,15 +66,16 @@  -- | 'unify' (=:=)-    ::  ( RankedBindingMonad v t m+    ::  ( RankedBindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t       -- ^-    -> MutTerm v t       -- ^-    -> e m (MutTerm v t) -- ^+    => UTerm t v       -- ^+    -> UTerm t v       -- ^+    -> e m (UTerm t v) -- ^ (=:=) = unify+{-# INLINE (=:=) #-} infix 4 =:=, `unify`  @@ -81,16 +88,15 @@ -- aggressive opportunistic observable sharing, so it will be more -- efficient to use it in future calculations than either argument. unify-    ::  ( RankedBindingMonad v t m+    ::  ( RankedBindingMonad t v m         , MonadTrans e         , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure v t) (e m)+        , MonadError (UnificationFailure t v) (e m)         )-    => MutTerm v t       -- ^-    -> MutTerm v t       -- ^-    -> e m (MutTerm v t) -- ^-unify =-    \tl tr -> evalStateT (loop tl tr) IM.empty+    => UTerm t v       -- ^+    -> UTerm t v       -- ^+    -> e m (UTerm t v) -- ^+unify tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty     where     -- TODO: use IM.insertWith or the like to do this in one pass     {-# INLINE seenAs #-}@@ -104,33 +110,33 @@     v =: t = bindVar v t >> return t          loop tl0 tr0 = do-        tl1 <- lift . lift $ semiprune tl0-        tr1 <- lift . lift $ semiprune tr0-        case (tl1, tr1) of-            (MutVar vl, MutVar vr)-                | vl `eqVar` vr -> return tr1-                | otherwise     -> do+        tl0 <- lift . lift $ semiprune tl0+        tr0 <- lift . lift $ semiprune tr0+        case (tl0, tr0) of+            (UVar vl, UVar vr)+                | vl == vr  -> return tr0+                | otherwise -> do                     Rank rl mtl <- lift . lift $ lookupRankVar vl                     Rank rr mtr <- lift . lift $ lookupRankVar vr                     let cmp = compare rl rr                     case (mtl, mtr) of                         (Nothing, Nothing) -> lift . lift $                             case cmp of-                            LT -> do {                    vl =: tr1 }-                            EQ -> do { incrementRank vr ; vl =: tr1 }-                            GT -> do {                    vr =: tl1 }+                            LT -> do {                    vl =: tr0 }+                            EQ -> do { incrementRank vr ; vl =: tr0 }+                            GT -> do {                    vr =: tl0 }                                                (Nothing, Just tr) -> lift . lift $                             case cmp of-                            LT -> do {                    vl =: tr1 }-                            EQ -> do { incrementRank vr ; vl =: tr1 }-                            GT -> do { vl `bindVar` tr  ; vr =: tl1 }+                            LT -> do {                    vl =: tr0 }+                            EQ -> do { incrementRank vr ; vl =: tr0 }+                            GT -> do { vl `bindVar` tr  ; vr =: tl0 }                                                  (Just tl, Nothing) -> lift . lift $                             case cmp of-                            LT -> do { vr `bindVar` tl  ; vl =: tr1 }-                            EQ -> do { incrementRank vl ; vr =: tl1 }-                            GT -> do {                    vr =: tl1 }+                            LT -> do { vr `bindVar` tl  ; vl =: tr0 }+                            EQ -> do { incrementRank vl ; vr =: tl0 }+                            GT -> do {                    vr =: tl0 }                                                  (Just tl, Just tr) -> do                             t <- localState $ do@@ -139,38 +145,38 @@                                 loop tl tr                             lift . lift $                                 case cmp of-                                LT -> do { vr `bindVar` t        ; vl =: tr1 }-                                EQ -> do { incrementBindVar vl t ; vr =: tl1 }-                                GT -> do { vl `bindVar` t        ; vr =: tl1 }+                                LT -> do { vr `bindVar` t        ; vl =: tr0 }+                                EQ -> do { incrementBindVar vl t ; vr =: tl0 }+                                GT -> do { vl `bindVar` t        ; vr =: tl0 }             -            (MutVar vl, MutTerm _) -> do+            (UVar vl, UTerm _) -> do                 t <- do                     mtl <- lift . lift $ lookupVar vl                     case mtl of-                        Nothing -> return tr1+                        Nothing -> return tr0                         Just tl -> localState $ do                             vl `seenAs` tl-                            loop tl tr1+                            loop tl tr0                 lift . lift $ do                     vl `bindVar` t-                    return tl1+                    return tl0             -            (MutTerm _, MutVar vr) -> do+            (UTerm _, UVar vr) -> do                 t <- do                     mtr <- lift . lift $ lookupVar vr                     case mtr of-                        Nothing -> return tl1+                        Nothing -> return tl0                         Just tr -> localState $ do                             vr `seenAs` tr-                            loop tl1 tr+                            loop tl0 tr                 lift . lift $ do                     vr `bindVar` t-                    return tr1+                    return tr0             -            (MutTerm tl, MutTerm tr) ->+            (UTerm tl, UTerm tr) ->                 case zipMatch tl tr of                 Nothing  -> lift . throwError $ TermMismatch tl tr-                Just tlr -> MutTerm <$> mapM (uncurry loop) tlr+                Just tlr -> UTerm <$> mapM (uncurry loop) tlr  ---------------------------------------------------------------- ----------------------------------------------------------- fin.

@@ -4,7 +4,7 @@            #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2011.07.06+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Unification.Ranked.IntVar -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton@@ -40,11 +40,11 @@ -- | Ranked binding state for 'IntVar'. data IntRBindingState t = IntRBindingState     { nextFreeVar :: {-# UNPACK #-} !Int-    , varBindings :: IM.IntMap (Rank IntVar t)+    , varBindings :: IM.IntMap (Rank t IntVar)     }  -- Can't derive this because it's an UndecidableInstance-instance (Show (t (MutTerm IntVar t))) =>+instance (Show (t (UTerm t IntVar))) =>     Show (IntRBindingState t)     where     show (IntRBindingState nr bs) =@@ -131,7 +131,7 @@ ----------------------------------------------------------------  instance (Unifiable t, Applicative m, Monad m) =>-    BindingMonad IntVar t (IntRBindingT t m)+    BindingMonad t IntVar (IntRBindingT t m)     where          lookupVar (IntVar v) = IRBT $ do@@ -167,7 +167,7 @@           instance (Unifiable t, Applicative m, Monad m) =>-    RankedBindingMonad IntVar t (IntRBindingT t m)+    RankedBindingMonad t IntVar (IntRBindingT t m)     where     lookupRankVar (IntVar v) = IRBT $ do         mb <- gets (IM.lookup v . varBindings)

@@ -5,7 +5,7 @@            #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2012.02.17+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Unification.Ranked.STVar -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton@@ -43,19 +43,20 @@     STRVar         {-# UNPACK #-} !Int         {-# UNPACK #-} !(STRef s Word8)-        {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STRVar s t) t)))+        {-# UNPACK #-} !(STRef s (Maybe (UTerm t (STRVar s t))))  instance Show (STRVar s t) where     show (STRVar i _ _) = "STRVar " ++ show i -instance Variable (STRVar s t) where-    eqVar (STRVar i _ _) (STRVar j _ _) = i == j+instance Eq (STRVar s t) where+    (STRVar i _ _) == (STRVar j _ _) = (i == j)     -    getVarID  (STRVar i _ _) = i+instance Variable (STRVar s t) where+    getVarID (STRVar i _ _) = i   ------------------------------------------------------------------- TODO: parameterize this so we can use BacktrackST too. Or course,+-- TODO: parameterize this so we can use BacktrackST too. Of course, -- that means defining another class for STRef-like variables -- -- TODO: parameterize this so we can share the implementation for STVar and STRVar@@ -97,7 +98,7 @@  _newSTRVar     :: String-    -> Maybe (MutTerm (STRVar s t) t)+    -> Maybe (UTerm t (STRVar s t))     -> STRBinding s (STRVar s t) _newSTRVar fun mb = STRB $ do     nr <- ask@@ -113,7 +114,7 @@                 return (STRVar n rk ptr)  -instance (Unifiable t) => BindingMonad (STRVar s t) t (STRBinding s) where+instance (Unifiable t) => BindingMonad t (STRVar s t) (STRBinding s) where     lookupVar (STRVar _ _ p) = STRB . lift $ readSTRef p          freeVar  = _newSTRVar "freeVar" Nothing@@ -124,7 +125,7 @@   instance (Unifiable t) =>-    RankedBindingMonad (STRVar s t) t (STRBinding s)+    RankedBindingMonad t (STRVar s t) (STRBinding s)     where          lookupRankVar (STRVar _ r p) = STRB . lift $ do

@@ -5,7 +5,7 @@            #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2012.02.17+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Unification.STVar -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton@@ -41,15 +41,16 @@ data STVar s t =     STVar         {-# UNPACK #-} !Int-        {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STVar s t) t)))+        {-# UNPACK #-} !(STRef s (Maybe (UTerm t (STVar s t))))  instance Show (STVar s t) where     show (STVar i _) = "STVar " ++ show i +instance Eq (STVar s t) where+    (STVar i _) == (STVar j _) = (i == j)+ instance Variable (STVar s t) where-    eqVar (STVar i _) (STVar j _) = i == j-    -    getVarID  (STVar i _) = i+    getVarID (STVar i _) = i   ----------------------------------------------------------------@@ -96,7 +97,7 @@  _newSTVar     :: String-    -> Maybe (MutTerm (STVar s t) t)+    -> Maybe (UTerm t (STVar s t))     -> STBinding s (STVar s t) _newSTVar fun mb = STB $ do     nr <- ask@@ -109,7 +110,7 @@                 STVar n <$> newSTRef mb  instance (Unifiable t) =>-    BindingMonad (STVar s t) t (STBinding s)+    BindingMonad t (STVar s t) (STBinding s)     where      lookupVar (STVar _ p) = STB . lift $ readSTRef p

@@ -5,7 +5,7 @@  {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2012.02.17+--                                                  ~ 2012.03.18 -- | -- Module      :  Control.Unification.Types -- Copyright   :  Copyright (c) 2007--2012 wren ng thornton@@ -19,8 +19,8 @@ ---------------------------------------------------------------- module Control.Unification.Types     (-    -- * Mutable terms-      MutTerm(..)+    -- * Unification terms+      UTerm(..)     , freeze     , unfreeze     -- * Errors@@ -38,40 +38,94 @@  import Data.Word               (Word8) import Data.Functor.Fixedpoint (Fix(..))+import Data.Foldable           (Foldable(..)) import Data.Traversable        (Traversable(..))-import Control.Applicative     (Applicative(..), (<$>))+import Control.Applicative     (Applicative(..), (<$>), Alternative(..))+import Control.Monad           (MonadPlus(..)) import Control.Monad.Error     (Error(..)) ---------------------------------------------------------------- ---------------------------------------------------------------- +-- TODO: incorporate Ed's cheaper free monads, at least as a view.+ -- | The type of terms generated by structures @t@ over variables -- @v@. The structure type should implement 'Unifiable' and the--- variable type should implement 'Variable'. The 'Show' instance--- doesn't show the constructors, for legibility.-data MutTerm v t-    = MutVar  !v-    | MutTerm !(t (MutTerm v t))+-- variable type should implement 'Variable'.+--+-- The 'Show' instance doesn't show the constructors, in order to+-- improve legibility for large terms.+--+-- All the category theoretic instances ('Functor', 'Foldable',+-- 'Traversable',...) are provided because they are often useful;+-- however, beware that since the implementations must be pure,+-- they cannot read variables bound in the current context and+-- therefore can create incoherent results. Therefore, you should+-- apply the current bindings before using any of the functions+-- provided by those classes. +data UTerm t v+    = UVar  !v               -- ^ A unification variable.+    | UTerm !(t (UTerm t v)) -- ^ Some structure containing subterms. -instance (Show v, Show (t (MutTerm v t))) =>-    Show (MutTerm v t)-    where-    showsPrec p (MutVar  v) = showsPrec p v-    showsPrec p (MutTerm t) = showsPrec p t+instance (Show v, Show (t (UTerm t v))) => Show (UTerm t v) where+    showsPrec p (UVar  v) = showsPrec p v+    showsPrec p (UTerm t) = showsPrec p t +instance (Functor t) => Functor (UTerm t) where+    fmap f (UVar  v) = UVar  (f v)+    fmap f (UTerm t) = UTerm (fmap (fmap f) t) +instance (Foldable t) => Foldable (UTerm t) where+    foldMap f (UVar  v) = f v+    foldMap f (UTerm t) = foldMap (foldMap f) t++instance (Traversable t) => Traversable (UTerm t) where+    traverse f (UVar  v) = UVar  <$> f v+    traverse f (UTerm t) = UTerm <$> traverse (traverse f) t++-- Does this even make sense for UTerm? It'd mean (a->b) is a+-- variable type...+instance (Functor t) => Applicative (UTerm t) where+    pure                  = UVar+    UVar  a  <*> UVar  b  = UVar  (a b)+    UVar  a  <*> UTerm mb = UTerm (fmap a  <$> mb)+    UTerm ma <*> b        = UTerm ((<*> b) <$> ma)++-- Does this even make sense for UTerm? It may be helpful for+-- building terms at least; though bind is inefficient for that.+-- Should use the cheaper free...+instance (Functor t) => Monad (UTerm t) where+    return        = UVar+    UVar  v >>= f = f v+    UTerm t >>= f = UTerm ((>>= f) <$> t)++-- This really doesn't make sense for UTerm...+instance (Alternative t) => Alternative (UTerm t) where+    empty   = UTerm empty+    a <|> b = UTerm (pure a <|> pure b)++-- This really doesn't make sense for UTerm...+instance (Functor t, MonadPlus t) => MonadPlus (UTerm t) where+    mzero       = UTerm mzero+    a `mplus` b = UTerm (return a `mplus` return b)++-- There's also MonadTrans, MonadWriter, MonadReader, MonadState,+-- MonadError, MonadCont; which make even less sense for us. See+-- Ed Kmett's free package for the implementations.++ -- | /O(n)/. Embed a pure term as a mutable term.-unfreeze :: (Functor t) => Fix t -> MutTerm v t-unfreeze = MutTerm . fmap unfreeze . unFix+unfreeze :: (Functor t) => Fix t -> UTerm t v+unfreeze = UTerm . fmap unfreeze . unFix   -- | /O(n)/. Extract a pure term from a mutable term, or return -- @Nothing@ if the mutable term actually contains variables. N.B., -- this function is pure, so you should manually apply bindings -- before calling it.-freeze :: (Traversable t) => MutTerm v t -> Maybe (Fix t)-freeze (MutVar  _) = Nothing-freeze (MutTerm t) = Fix <$> mapM freeze t+freeze :: (Traversable t) => UTerm t v -> Maybe (Fix t)+freeze (UVar  _) = Nothing+freeze (UTerm t) = Fix <$> mapM freeze t   ----------------------------------------------------------------@@ -82,9 +136,9 @@ -- could be given more accurate types if we used ad-hoc combinations -- of these constructors (i.e., because they can only throw one of -- the errors), the extra complexity is not considered worth it.-data UnificationFailure v t+data UnificationFailure t v     -    = OccursIn v (MutTerm v t)+    = OccursIn v (UTerm t v)         -- ^ A cyclic term was encountered (i.e., the variable         -- occurs free in a term it would have to be bound to in         -- order to succeed). Infinite terms like this are not@@ -102,7 +156,7 @@         -- we had performed the occurs-check, in order for error         -- messages to be intelligable.     -    | TermMismatch (t (MutTerm v t)) (t (MutTerm v t))+    | TermMismatch (t (UTerm t v)) (t (UTerm t v))         -- ^ The top-most level of the terms do not match (according         -- to 'zipMatch'). In logic programming this should simply         -- be treated as unification failure; in type checking this@@ -110,21 +164,36 @@         -- with inferred type @Bar@\" error.          | UnknownError String-        -- ^ Required for the @Error@ instance, which in turn is+        -- ^ Required for the 'Error' instance, which in turn is         -- required to appease @ErrorT@ in the MTL. We do not use         -- this anywhere.   -- Can't derive this because it's an UndecidableInstance-instance (Show (t (MutTerm v t)), Show v) =>-    Show (UnificationFailure v t)+instance (Show (t (UTerm t v)), Show v) =>+    Show (UnificationFailure t v)     where-    -- TODO: implement 'showsPrec' instead-    show (OccursIn     v  t)  = "OccursIn ("++show v++") ("++show t++")"-    show (TermMismatch tl tr) = "TermMismatch ("++show tl++") ("++show tr++")"-    show (UnknownError msg)   = "UnknownError: "++msg+    showsPrec p (OccursIn v t) =+        showParen (p > 9)+            ( showString "OccursIn "+            . showsPrec 11 v+            . showString " "+            . showsPrec 11 t+            )+    showsPrec p (TermMismatch tl tr) =+        showParen (p > 9)+            ( showString "TermMismatch "+            . showsPrec 11 tl+            . showString " "+            . showsPrec 11 tr+            )+    showsPrec p (UnknownError msg) =+        showParen (p > 9)+            ( showString "UnknownError: "+            . showString msg+            ) -instance Error (UnificationFailure v t) where+instance Error (UnificationFailure t v) where     noMsg  = UnknownError ""     strMsg = UnknownError @@ -143,19 +212,19 @@     zipMatch :: t a -> t b -> Maybe (t (a,b))  --- | An implementation of unification variables.-class Variable v where-    -    -- | Determine whether two variables are equal /as variables/,-    -- without considering what they are bound to. The default-    -- implementation is:-    ---    -- > eqVar x y = getVarID x == getVarID y-    eqVar :: v -> v -> Bool-    eqVar x y = getVarID x == getVarID y+-- | An implementation of unification variables. The 'Eq' requirement+-- is to determine whether two variables are equal /as variables/,+-- without considering what they are bound to. We use 'Eq' rather+-- than having our own @eqVar@ method so that clients can make use+-- of library functions which commonly assume 'Eq'.+class (Eq v) => Variable v where          -- | Return a unique identifier for this variable, in order to     -- support the use of visited-sets instead of occurs-checks.+    -- This function must satisfy the following coherence law with+    -- respect to the 'Eq' instance:+    --+    -- @x == y@ if and only if @getVarID x == getVarID y@     getVarID :: v -> Int  @@ -172,12 +241,12 @@ -- we make the same assumptions everywhere we use @BindingMonad@.  class (Unifiable t, Variable v, Applicative m, Monad m) =>-    BindingMonad v t m | m -> v t+    BindingMonad t v m | m -> t v     where     -    -- | Given a variable pointing to @MutTerm v t@, return the+    -- | Given a variable pointing to @UTerm t v@, return the     -- term it's bound to, or @Nothing@ if the variable is unbound.-    lookupVar :: v -> m (Maybe (MutTerm v t))+    lookupVar :: v -> m (Maybe (UTerm t v))               -- | Generate a new free variable guaranteed to be fresh in@@ -189,12 +258,12 @@     -- term. The default implementation is:     --     -- > newVar t = do { v <- freeVar ; bindVar v t ; return v }-    newVar :: MutTerm v t -> m v+    newVar :: UTerm t v -> m v     newVar t = do { v <- freeVar ; bindVar v t ; return v }               -- | Bind a variable to a term, overriding any previous binding.-    bindVar :: v -> MutTerm v t -> m ()+    bindVar :: v -> UTerm t v -> m ()   ----------------------------------------------------------------@@ -208,19 +277,17 @@ -- of variables in the unification problem. Thus, A @Word8@ is -- sufficient for @2^(2^8)@ variables, which is far more than can -- be indexed by 'getVarID' even on 64-bit architectures.-data Rank v t =-    Rank {-# UNPACK #-} !Word8 !(Maybe (MutTerm v t))+data Rank t v =+    Rank {-# UNPACK #-} !Word8 !(Maybe (UTerm t v))  -- Can't derive this because it's an UndecidableInstance-instance (Show v, Show (t (MutTerm v t))) =>-    Show (Rank v t)-    where+instance (Show v, Show (t (UTerm t v))) => Show (Rank t v) where     show (Rank n mb) = "Rank "++show n++" "++show mb --- TODO: flatten the Rank.Maybe.MutTerm so that we can tell that if semiprune returns a bound variable then it's bound to a term (not another var)?+-- TODO: flatten the Rank.Maybe.UTerm so that we can tell that if semiprune returns a bound variable then it's bound to a term (not another var)?  {--instance Monoid (Rank v t) where+instance Monoid (Rank t v) where     mempty = Rank 0 Nothing     mappend (Rank l mb) (Rank r _) = Rank (max l r) mb -}@@ -232,11 +299,11 @@ -- compression is asymptotically optimal, the constant factors may -- make it worthwhile to stick with the unweighted path compression -- supported by 'BindingMonad'.--class (BindingMonad v t m) => RankedBindingMonad v t m | m -> v t where-    -- | Given a variable pointing to @MutTerm v t@, return its+class (BindingMonad t v m) => RankedBindingMonad t v m | m -> t v where+    +    -- | Given a variable pointing to @UTerm t v@, return its     -- rank and the term it's bound to.-    lookupRankVar :: v -> m (Rank v t)+    lookupRankVar :: v -> m (Rank t v)          -- | Increase the rank of a variable by one.     incrementRank :: v -> m ()@@ -244,8 +311,8 @@     -- | Bind a variable to a term and increment the rank at the     -- same time. The default implementation is:     ---    -- > incrementBindVar v t = do { incrementRank v ; bindVar v t }-    incrementBindVar :: v -> MutTerm v t -> m ()+    -- > incrementBindVar t v = do { incrementRank v ; bindVar v t }+    incrementBindVar :: v -> UTerm t v -> m ()     incrementBindVar v t = do { incrementRank v ; bindVar v t }  ----------------------------------------------------------------

@@ -1,5 +1,5 @@ ------------------------------------------------------------------- wren ng thornton <wren@community.haskell.org>    ~ 2012.02.17+-- wren ng thornton <wren@community.haskell.org>    ~ 2012.03.11 ----------------------------------------------------------------  -- By and large Cabal >=1.2 is fine; but >= 1.6 gives tested-with:@@ -8,7 +8,7 @@ Build-Type:     Simple  Name:           unification-fd-Version:        0.6.0+Version:        0.7.0 Stability:      experimental Homepage:       http://code.haskell.org/~wren/ Author:         wren ng thornton