diff --git a/AUTHORS b/AUTHORS --- a/AUTHORS +++ b/AUTHORS @@ -18,6 +18,10 @@ suggsting the switch to having variables be of kind * rather than *->* +Roman Cheplyaka -- for suggesting the switching of type parameter + order on UTerm so that it actually is the free monad. And + for providing the freshenAll implementation. + === Related Work === diff --git a/VERSION b/VERSION --- a/VERSION +++ b/VERSION @@ -1,5 +1,6 @@ -0.7.0 (2012-xx-xx): - - Control.Unification: changed the type of seenAs to ensure that variables can only be seen as structure. +0.8.0 (2012-00-00): + - Control.Unification.Types: Changed the type of Unifiable.zipMatch +0.7.0 (2012-03-19): - Renamed MutTerm to UTerm (and MutVar to UVar) - Replaced the Variable.eqVar method by plain old Eq.(==) - Control.Unification: added getFreeVarsAll, applyBindingsAll, freshenAll diff --git a/src/Control/Unification.hs b/src/Control/Unification.hs --- a/src/Control/Unification.hs +++ b/src/Control/Unification.hs @@ -1,7 +1,7 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-} {-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-} ---------------------------------------------------------------- --- ~ 2012.03.18 +-- ~ 2012.03.25 -- | -- Module : Control.Unification -- Copyright : Copyright (c) 2007--2012 wren ng thornton @@ -464,7 +464,10 @@ match tl tr = case zipMatch tl tr of Nothing -> mzero - Just tlr -> mapM_ (uncurry loop) tlr + Just tlr -> mapM_ loop_ tlr + + loop_ (Left _) = return () -- success + loop_ (Right (tl,tr)) = loop tl tr _impossible_equals :: String {-# NOINLINE _impossible_equals #-} @@ -494,7 +497,7 @@ xs <- get case IM.lookup il xs of Just x - | x == ir -> return () + | x == ir -> return () -- success; no changes | otherwise -> lift mzero Nothing -> put $! IM.insert il ir xs @@ -503,7 +506,10 @@ (UTerm tl, UTerm tr) -> case zipMatch tl tr of Nothing -> lift mzero - Just tlr -> mapM_ (uncurry loop) tlr + Just tlr -> mapM_ loop_ tlr + + loop_ (Left _) = return () -- success; no changes + loop_ (Right (tl,tr)) = loop tl tr ---------------------------------------------------------------- @@ -592,7 +598,10 @@ match tl tr = case zipMatch tl tr of Nothing -> throwError $ TermMismatch tl tr - Just tlr -> UTerm <$> mapM (uncurry loop) tlr + Just tlr -> UTerm <$> mapM loop_ tlr + + loop_ (Left t) = return t + loop_ (Right (tl,tr)) = loop tl tr _impossible_unifyOccurs :: String {-# NOINLINE _impossible_unifyOccurs #-} @@ -677,7 +686,10 @@ match tl tr = case zipMatch tl tr of Nothing -> lift . throwError $ TermMismatch tl tr - Just tlr -> UTerm <$> mapM (uncurry loop) tlr + Just tlr -> UTerm <$> mapM loop_ tlr + + loop_ (Left t) = return t + loop_ (Right (tl,tr)) = loop tl tr _impossible_unify :: String {-# NOINLINE _impossible_unify #-} @@ -756,7 +768,10 @@ match tl tr = case zipMatch tl tr of Nothing -> return False - Just tlr -> and <$> mapM (uncurry loop) tlr -- TODO: use foldlM? + Just tlr -> and <$> mapM loop_ tlr -- TODO: use foldlM? + + loop_ (Left _) = return True + loop_ (Right (tl,tr)) = loop tl tr _impossible_subsumes :: String {-# NOINLINE _impossible_subsumes #-} diff --git a/src/Control/Unification/Ranked.hs b/src/Control/Unification/Ranked.hs --- a/src/Control/Unification/Ranked.hs +++ b/src/Control/Unification/Ranked.hs @@ -1,7 +1,7 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-} {-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-} ---------------------------------------------------------------- --- ~ 2012.03.18 +-- ~ 2012.03.25 -- | -- Module : Control.Unification.Ranked -- Copyright : Copyright (c) 2007--2012 wren ng thornton @@ -57,7 +57,7 @@ import Control.Applicative import Control.Monad.Trans (MonadTrans(..)) import Control.Monad.Error (MonadError(..)) -import Control.Monad.State (MonadState(..), evalStateT) +import Control.Monad.State (MonadState(..), StateT, evalStateT) import Control.Monad.State.UnificationExtras import Control.Unification.Types import Control.Unification hiding (unify, (=:=)) @@ -79,6 +79,28 @@ infix 4 =:=, `unify` +-- HACK: apparently this wasn't exported from Control.Unification; so c&p +-- 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 t v m + , MonadTrans e + , MonadError (UnificationFailure t v) (e m) + ) + => v -- ^ + -> t (UTerm t v) -- ^ + -> StateT (IM.IntMap (t (UTerm t v))) (e m) () -- ^ +{-# INLINE seenAs #-} +seenAs v0 t0 = do + seenVars <- get + case IM.lookup (getVarID v0) seenVars of + Just t -> lift . throwError $ OccursIn v0 (UTerm t) + Nothing -> put $! IM.insert (getVarID v0) t0 seenVars + + -- TODO: keep in sync as we verify correctness. -- -- | Unify two terms, or throw an error with an explanation of why @@ -98,14 +120,6 @@ -> 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 #-} - v `seenAs` t = 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 - {-# INLINE (=:) #-} v =: t = bindVar v t >> return t @@ -138,45 +152,57 @@ EQ -> do { incrementRank vl ; vr =: tl0 } GT -> do { vr =: tl0 } - (Just tl, Just tr) -> do + (Just (UTerm tl), Just (UTerm tr)) -> do t <- localState $ do vl `seenAs` tl vr `seenAs` tr - loop tl tr + match tl tr lift . lift $ case cmp of LT -> do { vr `bindVar` t ; vl =: tr0 } EQ -> do { incrementBindVar vl t ; vr =: tl0 } GT -> do { vl `bindVar` t ; vr =: tl0 } + _ -> error _impossible_unify - (UVar vl, UTerm _) -> do + (UVar vl, UTerm tr) -> do t <- do mtl <- lift . lift $ lookupVar vl case mtl of Nothing -> return tr0 - Just tl -> localState $ do + Just (UTerm tl) -> localState $ do vl `seenAs` tl - loop tl tr0 + match tl tr + _ -> error _impossible_unify lift . lift $ do vl `bindVar` t return tl0 - (UTerm _, UVar vr) -> do + (UTerm tl, UVar vr) -> do t <- do mtr <- lift . lift $ lookupVar vr case mtr of Nothing -> return tl0 - Just tr -> localState $ do + Just (UTerm tr) -> localState $ do vr `seenAs` tr - loop tl0 tr + match tl tr + _ -> error _impossible_unify lift . lift $ do vr `bindVar` t return tr0 - (UTerm tl, UTerm tr) -> - case zipMatch tl tr of - Nothing -> lift . throwError $ TermMismatch tl tr - Just tlr -> UTerm <$> 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 loop_ tlr + + loop_ (Left t) = return t + loop_ (Right (tl,tr)) = loop tl tr + +_impossible_unify :: String +{-# NOINLINE _impossible_unify #-} +_impossible_unify = "unify: the impossible happened" ---------------------------------------------------------------- ----------------------------------------------------------- fin. diff --git a/src/Control/Unification/Types.hs b/src/Control/Unification/Types.hs --- a/src/Control/Unification/Types.hs +++ b/src/Control/Unification/Types.hs @@ -5,7 +5,7 @@ {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ---------------------------------------------------------------- --- ~ 2012.03.18 +-- ~ 2012.03.25 -- | -- Module : Control.Unification.Types -- Copyright : Copyright (c) 2007--2012 wren ng thornton @@ -207,9 +207,10 @@ -- | Perform one level of equality testing for terms. If the -- term constructors are unequal then return @Nothing@; if they - -- are equal, then return the one-level spine filled with pairs - -- of subterms to be recursively checked. - zipMatch :: t a -> t b -> Maybe (t (a,b)) + -- are equal, then return the one-level spine filled with + -- resolved subterms and\/or pairs of subterms to be recursively + -- checked. + zipMatch :: t a -> t a -> Maybe (t (Either a (a,a))) -- | An implementation of unification variables. The 'Eq' requirement diff --git a/src/Data/Functor/Fixedpoint.hs b/src/Data/Functor/Fixedpoint.hs --- a/src/Data/Functor/Fixedpoint.hs +++ b/src/Data/Functor/Fixedpoint.hs @@ -7,7 +7,7 @@ {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ---------------------------------------------------------------- --- 2011.07.11 +-- 2012.07.10 -- | -- Module : Data.Functor.Fixedpoint -- Copyright : Copyright (c) 2007--2012 wren ng thornton @@ -75,7 +75,7 @@ -- than the head and so GHC can't guarantee that the instance safely -- terminates. It is in fact safe, however. instance (Show (f (Fix f))) => Show (Fix f) where - show (Fix f) = show f + showsPrec p (Fix f) = showsPrec p f instance (Eq (f (Fix f))) => Eq (Fix f) where Fix x == Fix y = x == y diff --git a/unification-fd.cabal b/unification-fd.cabal --- a/unification-fd.cabal +++ b/unification-fd.cabal @@ -1,5 +1,5 @@ ---------------------------------------------------------------- --- wren ng thornton ~ 2012.03.11 +-- wren ng thornton ~ 2012.03.25 ---------------------------------------------------------------- -- 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.7.0 +Version: 0.8.0 Stability: experimental Homepage: http://code.haskell.org/~wren/ Author: wren ng thornton