unification-fd 0.7.0 → 0.8.0
raw patch · 7 files changed
+86/−39 lines, 7 files
Files
- AUTHORS +4/−0
- VERSION +3/−2
- src/Control/Unification.hs +22/−7
- src/Control/Unification/Ranked.hs +48/−22
- src/Control/Unification/Types.hs +5/−4
- src/Data/Functor/Fixedpoint.hs +2/−2
- unification-fd.cabal +2/−2
AUTHORS view
@@ -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 ===
VERSION view
@@ -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
src/Control/Unification.hs view
@@ -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 #-}
src/Control/Unification/Ranked.hs view
@@ -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.
src/Control/Unification/Types.hs view
@@ -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
src/Data/Functor/Fixedpoint.hs view
@@ -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
unification-fd.cabal view
@@ -1,5 +1,5 @@ ------------------------------------------------------------------- wren ng thornton <wren@community.haskell.org> ~ 2012.03.11+-- wren ng thornton <wren@community.haskell.org> ~ 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