unification-fd 0.9.0 → 0.10.0

raw patch · 10 files changed

+381/−227 lines, 10 filessetup-changedPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Setup.hs +21/−1
• VERSION +11/−1
• src/Control/Monad/EitherK.hs +41/−24
• src/Control/Monad/MaybeK.hs +37/−18
• src/Control/Unification.hs +118/−78
• src/Control/Unification/Ranked.hs +35/−25
• src/Control/Unification/Ranked/STVar.hs +6/−3
• src/Control/Unification/STVar.hs +6/−3
• src/Control/Unification/Types.hs +101/−71
• unification-fd.cabal +5/−3

@@ -1,7 +1,27 @@ #!/usr/bin/env runhaskell+-- Cf. <http://www.mail-archive.com/haskell-cafe@haskell.org/msg59984.html>+-- <http://www.haskell.org/pipermail/haskell-cafe/2008-December/051785.html> +{-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-missing-signatures #-} module Main (main) where import Distribution.Simple+import Distribution.Simple.LocalBuildInfo (withPrograms)+import Distribution.Simple.Program        (userSpecifyArgs)+---------------------------------------------------------------- +-- | Define __HADDOCK__ when building documentation. main :: IO ()-main  = defaultMain+main = defaultMainWithHooks+    $ simpleUserHooks `modify_haddockHook` \oldHH pkg lbi hooks flags -> do+        +        -- Call the old haddockHook with a modified LocalBuildInfo+        (\lbi' -> oldHH pkg lbi' hooks flags)+            $ lbi `modify_withPrograms` \oldWP ->+                userSpecifyArgs "haddock" ["--optghc=-D__HADDOCK__"] oldWP+++modify_haddockHook  hooks f = hooks { haddockHook  = f (haddockHook  hooks) }+modify_withPrograms lbi   f = lbi   { withPrograms = f (withPrograms lbi)   }++----------------------------------------------------------------+----------------------------------------------------------- fin.

@@ -1,4 +1,14 @@-0.9.0 (2014-XX-XX):+0.10.0 (2014-XX-XX):+    - Cleaned up deprecation warnings re Control.Monad.Error+    - Control.Monad.EitherK: liberalized Monad restriction to+      Applicative where possible.+    - Control.Monad.MaybeK: liberalized Monad restriction to+      Applicative where possible.+    - Control.Unification.Types: Completely revamped the old+      UnificationFailure data type as the new UFailure data type+      and Fallible type class.++0.9.0 (2014-06-03):     - Control.Unification.Types: changed the fundeps on BindingMonad       and RankedBindingMonad so that things compile under GHC 7.8.2     - Data.Functor.Fixedpoint: eta-expanded RULES to avoid GHC >=

@@ -1,15 +1,23 @@ -- The MPTCs and FlexibleInstances are only for--- mtl:Control.Monad.Error.MonadError-{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleInstances #-}+-- mtl:Control.Monad.{Error,Except}.MonadError+{-# LANGUAGE CPP, Rank2Types, MultiParamTypeClasses, FlexibleInstances #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-}++-- HACK: in GHC 7.10, Haddock complains about unused imports; but,+-- if we use CPP to avoid including them under Haddock, then it+-- will fail!+#ifdef __HADDOCK__+{-# OPTIONS_GHC -fno-warn-unused-imports #-}+#endif+ -------------------------------------------------------------------                                                  ~ 2012.03.18+--                                                  ~ 2015.03.29 -- | -- Module      :  Control.Monad.EitherK -- License     :  BSD -- Maintainer  :  wren@community.haskell.org -- Stability   :  provisional--- Portability :  semi-portable (Rank2Types, MPTCs, FlexibleInstances)+-- Portability :  semi-portable (CPP, Rank2Types, MPTCs, FlexibleInstances) -- -- A continuation-passing variant of 'Either' for short-circuiting -- at failure. This code is based on "Control.Monad.MaybeK".@@ -33,11 +41,19 @@     , catchEitherKT     ) where -import Data.Monoid         (Monoid(..))-import Control.Applicative (Applicative(..), Alternative(..))-import Control.Monad       (MonadPlus(..), liftM, ap)-import Control.Monad.Trans (MonadTrans(..))-import Control.Monad.Error (MonadError(..))+#if __GLASGOW_HASKELL__ < 710+import Data.Monoid          (Monoid(..))+import Control.Applicative  (Applicative(..))+#endif+import Control.Applicative  (Alternative(..))+import Control.Monad        (MonadPlus(..), ap)+import Control.Monad.Trans  (MonadTrans(..))+#if (MIN_VERSION_mtl(2,2,1))+-- aka: transformers(0,4,1)+import Control.Monad.Except (MonadError(..))+#else+import Control.Monad.Error  (MonadError(..))+#endif ---------------------------------------------------------------- ---------------------------------------------------------------- @@ -142,20 +158,20 @@   -- | Execute an @EitherKT@ and return the concrete @Either@ encoding.-runEitherKT :: (Monad m) => EitherKT e m a -> m (Either e a)+runEitherKT :: (Applicative m) => EitherKT e m a -> m (Either e a) {-# INLINE runEitherKT #-}-runEitherKT (EKT m) = m (return . Right)+runEitherKT (EKT m) = m (pure . Right)   -- | Lift an @Either@ into an @EitherKT@.-toEitherKT :: (Monad m) => Either e a -> EitherKT e m a+toEitherKT :: (Applicative m) => Either e a -> EitherKT e m a {-# INLINE toEitherKT #-} toEitherKT (Left  e) = throwEitherKT e-toEitherKT (Right a) = return a+toEitherKT (Right a) = pure a   -- | Lift an @EitherK@ into an @EitherKT@.-liftEitherK :: (Monad m) => EitherK e a -> EitherKT e m a+liftEitherK :: (Applicative m) => EitherK e a -> EitherKT e m a {-# INLINE liftEitherK #-} liftEitherK = toEitherKT . runEitherK --@@ -178,23 +194,23 @@   -- | Lower an @EitherKT@ into an @EitherK@.-lowerEitherK :: (Monad m) => EitherKT e m a -> m (EitherK e a)+lowerEitherK :: (Applicative m) => EitherKT e m a -> m (EitherK e a) {-# INLINE lowerEitherK #-}-lowerEitherK = liftM toEitherK . runEitherKT+lowerEitherK = fmap toEitherK . runEitherKT   -- | Throw an error in the @EitherKT@ monad. This is identical to -- 'throwError'.-throwEitherKT :: (Monad m) => e -> EitherKT e m a+throwEitherKT :: (Applicative m) => e -> EitherKT e m a {-# INLINE throwEitherKT #-}-throwEitherKT e = EKT (\_ -> return (Left e))+throwEitherKT e = EKT (\_ -> pure (Left e))   -- | Handle errors in the @EitherKT@ monad. N.B., this type is more -- general than that of 'catchError', allowing the type of the -- errors to change. catchEitherKT-    :: (Monad m)+    :: (Applicative m, Monad m)     => EitherKT e m a -> (e -> EitherKT f m a) -> EitherKT f m a {-# INLINE catchEitherKT #-} catchEitherKT m handler = EKT $ \k -> do@@ -217,17 +233,18 @@     return a    = EKT (\k -> k a)     EKT m >>= f = EKT (\k -> m (\a -> case f a of EKT n -> n k)) --- 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+-- In order to define a @(<|>)@ which only requires @Applicative+-- m@ we'd need a law @m (Either e a) -> Either (m e) (m a)@; or+-- equivalently, we'd need to use a 2-CPS style.+instance (Applicative m, Monad m, Monoid e) => Alternative (EitherKT e m) where     empty = mzero     (<|>) = mplus -instance (Monad m, Monoid e) => MonadPlus (EitherKT e m) where+instance (Applicative m, Monad m, Monoid e) => MonadPlus (EitherKT e m) where     mzero       = throwEitherKT mempty     m `mplus` n = catchEitherKT m (catchEitherKT n . (throwEitherKT .) . mappend) -instance (Monad m) => MonadError e (EitherKT e m) where+instance (Applicative m, Monad m) => MonadError e (EitherKT e m) where     throwError = throwEitherKT     catchError = catchEitherKT 

@@ -1,14 +1,22 @@ -- The MPTCs is only for mtl:Control.Monad.Error.MonadError-{-# LANGUAGE Rank2Types, MultiParamTypeClasses #-}+{-# LANGUAGE CPP, Rank2Types, MultiParamTypeClasses #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-}++-- HACK: in GHC 7.10, Haddock complains about unused imports; but,+-- if we use CPP to avoid including them under Haddock, then it+-- will fail!+#ifdef __HADDOCK__+{-# OPTIONS_GHC -fno-warn-unused-imports #-}+#endif+ -------------------------------------------------------------------                                                  ~ 2012.03.18+--                                                  ~ 2015.03.29 -- | -- Module      :  Control.Monad.MaybeK -- License     :  BSD -- Maintainer  :  wren@community.haskell.org -- Stability   :  provisional--- Portability :  semi-portable (Rank2Types, MPTCs)+-- Portability :  semi-portable (CPP, Rank2Types, MPTCs) -- -- A continuation-passing variant of 'Maybe' for short-circuiting -- at failure. This is based largely on code from the Haskell Wiki@@ -33,10 +41,18 @@     , lowerMaybeK     ) where -import Control.Applicative (Applicative(..), Alternative(..))-import Control.Monad       (MonadPlus(..), liftM, ap)-import Control.Monad.Error (MonadError(..))-import Control.Monad.Trans (MonadTrans(..))+#if __GLASGOW_HASKELL__ < 710+import Control.Applicative  (Applicative(..))+#endif+import Control.Applicative  (Alternative(..))+import Control.Monad        (MonadPlus(..), ap)+import Control.Monad.Trans  (MonadTrans(..))+#if (MIN_VERSION_mtl(2,2,1))+-- aka: transformers(0,4,1)+import Control.Monad.Except (MonadError(..))+#else+import Control.Monad.Error  (MonadError(..))+#endif ---------------------------------------------------------------- ---------------------------------------------------------------- @@ -117,20 +133,20 @@   -- | Execute a @MaybeKT@ and return the concrete @Maybe@ encoding.-runMaybeKT :: (Monad m) => MaybeKT m a -> m (Maybe a)+runMaybeKT :: (Applicative m) => MaybeKT m a -> m (Maybe a) {-# INLINE runMaybeKT #-}-runMaybeKT (MKT m) = m (return . Just)+runMaybeKT (MKT m) = m (pure . Just)   -- | Lift a @Maybe@ into an @MaybeKT@.-toMaybeKT :: (Monad m) => Maybe a -> MaybeKT m a+toMaybeKT :: (Applicative m) => Maybe a -> MaybeKT m a {-# INLINE toMaybeKT #-}-toMaybeKT Nothing  = mzero-toMaybeKT (Just a) = return a+toMaybeKT Nothing  = MKT (\_ -> pure Nothing)+toMaybeKT (Just a) = pure a   -- | Lift an @MaybeK@ into an @MaybeKT@.-liftMaybeK :: (Monad m) => MaybeK a -> MaybeKT m a+liftMaybeK :: (Applicative m) => MaybeK a -> MaybeKT m a {-# INLINE liftMaybeK #-} liftMaybeK = toMaybeKT . runMaybeK --@@ -153,9 +169,9 @@   -- | Lower an @MaybeKT@ into an @MaybeK@.-lowerMaybeK :: (Monad m) => MaybeKT m a -> m (MaybeK a)+lowerMaybeK :: (Applicative m) => MaybeKT m a -> m (MaybeK a) {-# INLINE lowerMaybeK #-}-lowerMaybeK = liftM toMaybeK . runMaybeKT+lowerMaybeK = fmap toMaybeK . runMaybeKT   instance Functor (MaybeKT m) where@@ -171,11 +187,14 @@     return a    = MKT (\k -> k a)     MKT m >>= f = MKT (\k -> m (\a -> case f a of MKT n -> n k)) -instance (Monad m) => Alternative (MaybeKT m) where+-- In order to define a @(<|>)@ which only requires @Applicative+-- m@ we'd need a law @m (Either e a) -> Either (m e) (m a)@; or+-- equivalently, we'd need to use a 2-CPS style.+instance (Applicative m, Monad m) => Alternative (MaybeKT m) where     empty = mzero     (<|>) = mplus -instance (Monad m) => MonadPlus (MaybeKT m) where+instance (Applicative m, Monad m) => MonadPlus (MaybeKT m) where     mzero = MKT (\_ -> return Nothing)          m `mplus` n = MKT $ \k -> do@@ -184,7 +203,7 @@             Nothing -> case n of MKT n' -> n' k             Just a  -> k a -instance (Monad m) => MonadError () (MaybeKT m) where+instance (Applicative m, Monad m) => MonadError () (MaybeKT m) where     throwError _   = mzero     catchError m f = MKT $ \k -> do         mb <- runMaybeKT m

@@ -1,14 +1,21 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}+{-# LANGUAGE CPP, MultiParamTypeClasses, FlexibleContexts #-} {-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-}++-- HACK: in GHC 7.10, Haddock complains about unused imports; but,+-- if we use CPP to avoid including them under Haddock, then it+-- will fail!+#ifdef __HADDOCK__+{-# OPTIONS_GHC -fno-warn-unused-imports #-}+#endif -------------------------------------------------------------------                                                  ~ 2012.03.25+--                                                  ~ 2015.03.29 -- | -- Module      :  Control.Unification--- Copyright   :  Copyright (c) 2007--2014 wren gayle romano+-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano -- License     :  BSD -- Maintainer  :  wren@community.haskell.org -- Stability   :  experimental--- Portability :  semi-portable (MPTCs, FlexibleContexts)+-- Portability :  semi-portable (CPP, MPTCs, FlexibleContexts) -- -- This module provides first-order structural unification over -- general structure types. It also provides the standard suite of@@ -32,7 +39,7 @@     , freeze     , unfreeze     -- ** Errors-    , UnificationFailure(..)+    , Fallible(..)     -- ** Basic type classes     , Unifiable(..)     , Variable(..)@@ -83,11 +90,18 @@ import Data.Foldable import Data.Traversable import Control.Monad.Identity (Identity(..))+#if __GLASGOW_HASKELL__ < 710 import Control.Applicative-import Control.Monad       (MonadPlus(..))-import Control.Monad.Trans (MonadTrans(..))-import Control.Monad.Error (MonadError(..))-import Control.Monad.State (MonadState(..), StateT, evalStateT, execStateT)+#endif+import Control.Monad        (MonadPlus(..))+import Control.Monad.Trans  (MonadTrans(..))+#if (MIN_VERSION_mtl(2,2,1))+-- aka: transformers(0,4,1)+import Control.Monad.Except (MonadError(..))+#else+import Control.Monad.Error  (MonadError(..))+#endif+import Control.Monad.State  (MonadState(..), StateT, evalStateT, execStateT) import Control.Monad.MaybeK import Control.Monad.State.UnificationExtras import Control.Unification.Types@@ -153,24 +167,26 @@         UVar  v -> return $! v0 == v  +-- TODO: what was the reason for the MonadTrans madness? -- 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+-- | Update the visited-set with a declaration that a variable has+-- been seen with a given binding, or throw 'occursFailure' if the -- variable has already been seen. seenAs     ::  ( BindingMonad t v m-        , MonadTrans e-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , MonadError e (em m)         )     => v -- ^     -> t (UTerm t v) -- ^-    -> StateT (IM.IntMap (t (UTerm t v))) (e m) () -- ^+    -> StateT (IM.IntMap (t (UTerm t v))) (em m) () -- ^ {-# INLINE seenAs #-} seenAs v0 t0 = do     seenVars <- get     case IM.lookup (getVarID v0) seenVars of-        Just t  -> lift . throwError $ OccursIn v0 (UTerm t)+        Just t  -> lift . throwError $ occursFailure v0 (UTerm t)         Nothing -> put $! IM.insert (getVarID v0) t0 seenVars  ----------------------------------------------------------------@@ -232,26 +248,31 @@                             Nothing -> return $ IM.singleton i v  +-- TODO: what was the reason for the MonadTrans madness?+-- -- | Apply the current bindings from the monad so that any remaining -- variables in the result must, therefore, be free. N.B., this -- expensively clones term structure and should only be performed--- when a pure term is needed, or when 'OccursIn' exceptions must--- be forced. This function /does/ preserve sharing, however that--- sharing is no longer observed by the monad.+-- when a pure term is needed, or when 'occursFailure' exceptions+-- must be forced. This function /does/ preserve sharing, however+-- that sharing is no longer observed by the monad. ----- If any cyclic bindings are detected, then an 'OccursIn' exception--- will be thrown.+-- If any cyclic bindings are detected, then an 'occursFailure'+-- exception will be thrown. applyBindings     ::  ( BindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )     => UTerm t v       -- ^-    -> e m (UTerm t v) -- ^+    -> em m (UTerm t v) -- ^ applyBindings = fmap runIdentity . applyBindingsAll . Identity  +-- TODO: what was the reason for the MonadTrans madness?+-- -- | 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@@ -260,13 +281,14 @@ -- /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)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         , Traversable s         )-    => s (UTerm t v)       -- ^-    -> e m (s (UTerm t v)) -- ^+    => s (UTerm t v)        -- ^+    -> em m (s (UTerm t v)) -- ^ applyBindingsAll ts0 = evalStateT (mapM loop ts0) IM.empty     where     loop t0 = do@@ -278,7 +300,7 @@                 mb <- IM.lookup i <$> get                 case mb of                     Just (Right t) -> return t-                    Just (Left  t) -> lift . throwError $ OccursIn v t+                    Just (Left  t) -> lift . throwError $ occursFailure v t                     Nothing -> do                         mb' <- lift . lift $ lookupVar v                         case mb' of@@ -290,24 +312,29 @@                                 return t'  +-- TODO: what was the reason for the MonadTrans madness?+-- -- | Freshen all variables in a term, both bound and free. This -- ensures that the observability of sharing is maintained, while -- freshening the free variables. N.B., this expensively clones -- term structure and should only be performed when necessary. ----- If any cyclic bindings are detected, then an 'OccursIn' exception--- will be thrown.+-- If any cyclic bindings are detected, then an 'occursFailure'+-- exception will be thrown. freshen     ::  ( BindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )     => UTerm t v       -- ^-    -> e m (UTerm t v) -- ^+    -> em m (UTerm t v) -- ^ freshen = fmap runIdentity . freshenAll . Identity  +-- TODO: what was the reason for the MonadTrans madness?+-- -- | 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@@ -325,13 +352,14 @@ -- /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)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         , Traversable s         )-    => s (UTerm t v)       -- ^-    -> e m (s (UTerm t v)) -- ^+    => s (UTerm t v)        -- ^+    -> em m (s (UTerm t v)) -- ^ freshenAll ts0 = evalStateT (mapM loop ts0) IM.empty     where     loop t0 = do@@ -343,7 +371,7 @@                 seenVars <- get                 case IM.lookup i seenVars of                     Just (Right t) -> return t-                    Just (Left  t) -> lift . throwError $ OccursIn v t+                    Just (Left  t) -> lift . throwError $ occursFailure v t                     Nothing -> do                         mb <- lift . lift $ lookupVar v                         case mb of@@ -384,31 +412,35 @@ infix 4 =~=, `equiv`  +-- TODO: what was the reason for the MonadTrans madness? -- | 'unify' (=:=)     ::  ( BindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )-    => UTerm t v       -- ^-    -> UTerm t v       -- ^-    -> e m (UTerm t v) -- ^+    => UTerm t v        -- ^+    -> UTerm t v        -- ^+    -> em m (UTerm t v) -- ^ (=:=) = unify {-# INLINE (=:=) #-} infix 4 =:=, `unify`  +-- TODO: what was the reason for the MonadTrans madness? -- | 'subsumes' (<:=)     ::  ( BindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )     => UTerm t v -- ^     -> UTerm t v -- ^-    -> e m Bool  -- ^+    -> em m Bool -- ^ (<:=) = subsumes {-# INLINE (<:=) #-} infix 4 <:=, `subsumes`@@ -514,22 +546,24 @@  ---------------------------------------------------------------- -- Not quite unify2 from the benchmarks, since we do AOOS.+-- TODO: what was the reason for the MonadTrans madness? -- -- | A variant of 'unify' which uses 'occursIn' instead of visited-sets.--- This should only be used when eager throwing of 'OccursIn' errors--- is absolutely essential (or for testing the correctness of--- @unify@). Performing the occurs-check is expensive. Not only is--- it slow, it's asymptotically slow since it can cause the same+-- This should only be used when eager throwing of 'occursFailure'+-- errors is absolutely essential (or for testing the correctness+-- of @unify@). Performing the occurs-check is expensive. Not only+-- is it slow, it's asymptotically slow since it can cause the same -- subterm to be traversed multiple times. unifyOccurs     ::  ( BindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )-    => UTerm t v       -- ^-    -> UTerm t v       -- ^-    -> e m (UTerm t v) -- ^+    => UTerm t v        -- ^+    -> UTerm t v        -- ^+    -> em m (UTerm t v) -- ^ unifyOccurs = loop     where     {-# INLINE (=:) #-}@@ -539,7 +573,7 @@     acyclicBindVar v t = do         b <- lift $ v `occursIn` t         if b-            then throwError $ OccursIn v t+            then throwError $ occursFailure v t             else v =: t          -- TODO: cf todos in 'unify'@@ -597,7 +631,7 @@          match tl tr =         case zipMatch tl tr of-        Nothing  -> throwError $ TermMismatch tl tr+        Nothing  -> throwError $ mismatchFailure tl tr         Just tlr -> UTerm <$> mapM loop_ tlr          loop_ (Left  t)       = return t@@ -612,7 +646,8 @@ -- TODO: verify correctness, especially for the visited-set stuff. -- 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...--- +-- TODO: what was the reason for the MonadTrans madness?+-- -- | Unify two terms, or throw an error with an explanation of why -- unification failed. Since bindings are stored in the monad, the -- two input terms and the output term are all equivalent if@@ -621,13 +656,14 @@ -- efficient to use it in future calculations than either argument. unify     ::  ( BindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )-    => UTerm t v       -- ^-    -> UTerm t v       -- ^-    -> e m (UTerm t v) -- ^+    => UTerm t v        -- ^+    -> UTerm t v        -- ^+    -> em m (UTerm t v) -- ^ unify tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty     where     {-# INLINE (=:) #-}@@ -685,7 +721,7 @@          match tl tr =         case zipMatch tl tr of-        Nothing  -> lift . throwError $ TermMismatch tl tr+        Nothing  -> lift . throwError $ mismatchFailure tl tr         Just tlr -> UTerm <$> mapM loop_ tlr          loop_ (Left  t)       = return t@@ -696,11 +732,14 @@ _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?+-- 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? -- -- TODO: verify correctness -- TODO: redo with some codensity--- TODO: there should be some way to catch OccursIn errors and repair the bindings...+-- TODO: there should be some way to catch occursFailure errors and repair the bindings...+-- TODO: what was the reason for the MonadTrans madness?  -- | Determine whether the left term subsumes the right term. That -- is, whereas @(tl =:= tr)@ will compute the most general substitution@@ -719,13 +758,14 @@ -- of variables. subsumes     ::  ( BindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )     => UTerm t v -- ^     -> UTerm t v -- ^-    -> e m Bool  -- ^+    -> em m Bool -- ^ subsumes tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty     where     {-# INLINE (=:) #-}

@@ -1,14 +1,14 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}+{-# LANGUAGE CPP, MultiParamTypeClasses, FlexibleContexts #-} {-# OPTIONS_GHC -Wall -fwarn-tabs -fno-warn-name-shadowing #-} -------------------------------------------------------------------                                                  ~ 2012.03.25+--                                                  ~ 2015.03.29 -- | -- Module      :  Control.Unification.Ranked--- Copyright   :  Copyright (c) 2007--2014 wren gayle romano+-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano -- License     :  BSD -- Maintainer  :  wren@community.haskell.org -- Stability   :  highly experimental--- Portability :  semi-portable (MPTCs, FlexibleContexts)+-- Portability :  semi-portable (CPP, MPTCs, FlexibleContexts) -- -- This module provides the API of "Control.Unification" except -- using 'RankedBindingMonad' where appropriate. This module (and@@ -54,10 +54,17 @@  import qualified Data.IntMap as IM import Data.Traversable+#if __GLASGOW_HASKELL__ < 710 import Control.Applicative-import Control.Monad.Trans (MonadTrans(..))-import Control.Monad.Error (MonadError(..))-import Control.Monad.State (MonadState(..), StateT, evalStateT)+#endif+import Control.Monad.Trans  (MonadTrans(..))+#if (MIN_VERSION_mtl(2,2,1))+-- aka: transformers(0,4,1)+import Control.Monad.Except (MonadError(..))+#else+import Control.Monad.Error  (MonadError(..))+#endif+import Control.Monad.State  (MonadState(..), StateT, evalStateT) import Control.Monad.State.UnificationExtras import Control.Unification.Types import Control.Unification hiding (unify, (=:=))@@ -67,13 +74,14 @@ -- | 'unify' (=:=)     ::  ( RankedBindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )-    => UTerm t v       -- ^-    -> UTerm t v       -- ^-    -> e m (UTerm t v) -- ^+    => UTerm t v        -- ^+    -> UTerm t v        -- ^+    -> em m (UTerm t v) -- ^ (=:=) = unify {-# INLINE (=:=) #-} infix 4 =:=, `unify`@@ -83,21 +91,22 @@ -- 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+-- been seen with a given binding, or throw 'occursFailure' if the -- variable has already been seen. seenAs     ::  ( BindingMonad t v m-        , MonadTrans e-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , MonadError e (em m)         )     => v -- ^     -> t (UTerm t v) -- ^-    -> StateT (IM.IntMap (t (UTerm t v))) (e m) () -- ^+    -> StateT (IM.IntMap (t (UTerm t v))) (em m) () -- ^ {-# INLINE seenAs #-} seenAs v0 t0 = do     seenVars <- get     case IM.lookup (getVarID v0) seenVars of-        Just t  -> lift . throwError $ OccursIn v0 (UTerm t)+        Just t  -> lift . throwError $ occursFailure v0 (UTerm t)         Nothing -> put $! IM.insert (getVarID v0) t0 seenVars  @@ -111,13 +120,14 @@ -- efficient to use it in future calculations than either argument. unify     ::  ( RankedBindingMonad t v m-        , MonadTrans e-        , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)-        , MonadError (UnificationFailure t v) (e m)+        , Fallible t v e+        , MonadTrans em+        , Functor (em m) -- Grr, Monad(em m) should imply Functor(em m)+        , MonadError e (em m)         )-    => UTerm t v       -- ^-    -> UTerm t v       -- ^-    -> e m (UTerm t v) -- ^+    => UTerm t v        -- ^+    -> UTerm t v        -- ^+    -> em m (UTerm t v) -- ^ unify tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty     where     {-# INLINE (=:) #-}@@ -194,7 +204,7 @@          match tl tr =         case zipMatch tl tr of-        Nothing  -> lift . throwError $ TermMismatch tl tr+        Nothing  -> lift . throwError $ mismatchFailure tl tr         Just tlr -> UTerm <$> mapM loop_ tlr          loop_ (Left  t)       = return t

@@ -1,14 +1,15 @@-{-# LANGUAGE Rank2Types+{-# LANGUAGE CPP+           , Rank2Types            , MultiParamTypeClasses            , UndecidableInstances            , FlexibleInstances            #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2012.03.18+--                                                  ~ 2015.03.29 -- | -- Module      :  Control.Unification.Ranked.STVar--- Copyright   :  Copyright (c) 2007--2014 wren gayle romano+-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano -- License     :  BSD -- Maintainer  :  wren@community.haskell.org -- Stability   :  highly experimental@@ -26,7 +27,9 @@  import Data.STRef import Data.Word            (Word8)+#if __GLASGOW_HASKELL__ < 710 import Control.Applicative  (Applicative(..))+#endif import Control.Monad        (ap) import Control.Monad.Trans  (lift) import Control.Monad.ST

@@ -1,14 +1,15 @@-{-# LANGUAGE Rank2Types+{-# LANGUAGE CPP+           , Rank2Types            , MultiParamTypeClasses            , UndecidableInstances            , FlexibleInstances            #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -------------------------------------------------------------------                                                  ~ 2012.03.18+--                                                  ~ 2015.03.29 -- | -- Module      :  Control.Unification.STVar--- Copyright   :  Copyright (c) 2007--2014 wren gayle romano+-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano -- License     :  BSD -- Maintainer  :  wren@community.haskell.org -- Stability   :  experimental@@ -26,7 +27,9 @@ import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)  import Data.STRef+#if __GLASGOW_HASKELL__ < 710 import Control.Applicative  (Applicative(..), (<$>))+#endif import Control.Monad        (ap) import Control.Monad.Trans  (lift) import Control.Monad.ST

@@ -1,14 +1,26 @@ -- Required for Show instances {-# LANGUAGE FlexibleContexts, UndecidableInstances #-}+-- Required for cleaning up Haddock messages for GHC 7.10+{-# LANGUAGE CPP #-} -- Required more generally-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}-+{-# LANGUAGE MultiParamTypeClasses+           , FunctionalDependencies+           , FlexibleInstances+           #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-}++-- HACK: in GHC 7.10, Haddock complains about unused imports; but,+-- if we use CPP to avoid including them under Haddock, then it+-- will fail!+#ifdef __HADDOCK__+{-# OPTIONS_GHC -fno-warn-unused-imports #-}+#endif+ -------------------------------------------------------------------                                                  ~ 2014.05.28+--                                                  ~ 2015.03.29 -- | -- Module      :  Control.Unification.Types--- Copyright   :  Copyright (c) 2007--2014 wren gayle romano+-- Copyright   :  Copyright (c) 2007--2015 wren gayle romano -- License     :  BSD -- Maintainer  :  wren@community.haskell.org -- Stability   :  experimental@@ -24,7 +36,8 @@     , freeze     , unfreeze     -- * Errors-    , UnificationFailure(..)+    , Fallible(..)+    , UFailure(..)     -- * Basic type classes     , Unifiable(..)     , Variable(..)@@ -38,12 +51,16 @@  import Data.Word               (Word8) import Data.Functor.Fixedpoint (Fix(..))-import Data.Monoid             (Monoid(..), (<>))+import Data.Monoid             ((<>))+#if __GLASGOW_HASKELL__ < 710 import Data.Foldable           (Foldable(..))+#endif import Data.Traversable        (Traversable(..))-import Control.Applicative     (Applicative(..), (<$>), Alternative(..))+#if __GLASGOW_HASKELL__ < 710+import Control.Applicative     (Applicative(..), (<$>))+#endif+import Control.Applicative     (Alternative(..)) import Control.Monad           (MonadPlus(..))-import Control.Monad.Error     (Error(..)) ---------------------------------------------------------------- ---------------------------------------------------------------- @@ -138,88 +155,99 @@ -- of these constructors (i.e., because they can only throw one of -- the errors), the extra complexity is not considered worth it. ----- /Updated: 0.8.1/ added 'Functor', 'Foldable', and 'Traversable' instances.-data UnificationFailure t v-    -    = 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-        -- generally acceptable, so we do not support them. In logic-        -- programming this should simply be treated as unification-        -- failure; in type checking this should result in a \"could-        -- not construct infinite type @a = Foo a@\" error.-        ---        -- Note that since, by default, the library uses visited-sets-        -- instead of the occurs-check these errors will be thrown-        -- at the point where the cycle is dereferenced\/unrolled-        -- (e.g., when applying bindings), instead of at the time-        -- when the cycle is created. However, the arguments to-        -- this constructor should express the same context as if-        -- we had performed the occurs-check, in order for error-        -- messages to be intelligable.-    -    | 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-        -- should result in a \"could not match expected type @Foo@-        -- with inferred type @Bar@\" error.+-- This is a finally-tagless encoding of the 'UFailure' data type+-- so that we can abstract over clients adding additional domain-specific+-- failure modes, introducing monoid instances, etc.+--+-- /Since: 0.10.0/+class Fallible t v a where+    -- | 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 generally acceptable,+    -- so we do not support them. In logic programming this should+    -- simply be treated as unification failure; in type checking+    -- this should result in a \"could not construct infinite type+    -- @a = Foo a@\" error.+    --+    -- Note that since, by default, the library uses visited-sets+    -- instead of the occurs-check these errors will be thrown at+    -- the point where the cycle is dereferenced\/unrolled (e.g.,+    -- when applying bindings), instead of at the time when the+    -- cycle is created. However, the arguments to this constructor+    -- should express the same context as if we had performed the+    -- occurs-check, in order for error messages to be intelligable.+    occursFailure :: v -> UTerm t v -> a     -    | UnknownError String-        -- ^ Required for the 'Error' instance, which in turn is-        -- required to appease @ErrorT@ in the MTL. We do not use-        -- this anywhere.+    -- | 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 should+    -- result in a \"could not match expected type @Foo@ with+    -- inferred type @Bar@\" error.+    mismatchFailure :: t (UTerm t v) -> t (UTerm t v) -> a  +-- | A concrete representation for the 'Fallible' type class.+-- Whenever possible, you should prefer to keep the concrete+-- representation abstract by using the 'Fallible' class instead.+--+-- /Updated: 0.10.0/ Used to be called @UnificationFailure@. Removed+-- the @UnknownError@ constructor, and the @Control.Monad.Error.Error@+-- instance associated with it. Renamed @OccursIn@ constructor to+-- @OccursFailure@; and renamed @TermMismatch@ constructor to+-- @MismatchFailure@.+--+-- /Updated: 0.8.1/ added 'Functor', 'Foldable', and 'Traversable' instances.+data UFailure t v+    = OccursFailure v (UTerm t v)+    | MismatchFailure (t (UTerm t v)) (t (UTerm t v))+++instance Fallible t v (UFailure t v) where+    occursFailure   = OccursFailure+    mismatchFailure = MismatchFailure++ -- Can't derive this because it's an UndecidableInstance instance (Show (t (UTerm t v)), Show v) =>-    Show (UnificationFailure t v)+    Show (UFailure t v)     where-    showsPrec p (OccursIn v t) =+    showsPrec p (OccursFailure v t) =         showParen (p > 9)-            ( showString "OccursIn "+            ( showString "OccursFailure "             . showsPrec 11 v             . showString " "             . showsPrec 11 t             )-    showsPrec p (TermMismatch tl tr) =+    showsPrec p (MismatchFailure tl tr) =         showParen (p > 9)-            ( showString "TermMismatch "+            ( showString "MismatchFailure "             . showsPrec 11 tl             . showString " "             . showsPrec 11 tr             )-    showsPrec p (UnknownError msg) =-        showParen (p > 9)-            ( showString "UnknownError: "-            . showString msg-            ) --- TODO: transformers-0.4.1.0 deprecated this, use--- Control.Monad.Trans.Except instead. (transformers-0.3.0.0 is--- fine)-instance Error (UnificationFailure t v) where-    noMsg  = UnknownError ""-    strMsg = UnknownError --instance (Functor t) => Functor (UnificationFailure t) where-    fmap f (OccursIn v t)       = OccursIn (f v) (fmap f t)-    fmap f (TermMismatch tl tr) = TermMismatch (fmap f <$> tl) (fmap f <$> tr)-    fmap _ (UnknownError msg)   = UnknownError msg+instance (Functor t) => Functor (UFailure t) where+    fmap f (OccursFailure v t) =+        OccursFailure (f v) (fmap f t)+    +    fmap f (MismatchFailure tl tr) =+        MismatchFailure (fmap f <$> tl) (fmap f <$> tr) -instance (Foldable t) => Foldable (UnificationFailure t) where-    foldMap f (OccursIn v t)       = f v <> foldMap f t-    foldMap f (TermMismatch tl tr) = foldMap (foldMap f) tl-                                  <> foldMap (foldMap f) tr-    foldMap _ (UnknownError _)     = mempty+instance (Foldable t) => Foldable (UFailure t) where+    foldMap f (OccursFailure v t) =+        f v <> foldMap f t+    +    foldMap f (MismatchFailure tl tr) =+        foldMap (foldMap f) tl <> foldMap (foldMap f) tr -instance (Traversable t) => Traversable (UnificationFailure t) where-    traverse f (OccursIn v t)       = OccursIn <$> f v <*> traverse f t-    traverse f (TermMismatch tl tr) = TermMismatch <$> traverse (traverse f) tl -                                                   <*> traverse (traverse f) tr-    traverse _ (UnknownError msg)   = pure (UnknownError msg)+instance (Traversable t) => Traversable (UFailure t) where+    traverse f (OccursFailure v t) =+        OccursFailure <$> f v <*> traverse f t+    +    traverse f (MismatchFailure tl tr) =+        MismatchFailure <$> traverse (traverse f) tl+                        <*> traverse (traverse f) tr  ---------------------------------------------------------------- @@ -309,7 +337,9 @@ 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.UTerm 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 t v) where

@@ -1,5 +1,5 @@ ------------------------------------------------------------------- wren gayle romano <wren@community.haskell.org>   ~ 2014.05.28+-- wren gayle romano <wren@community.haskell.org>   ~ 2014.09.15 ----------------------------------------------------------------  -- 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.9.0+Version:        0.10.0 Stability:      experimental Homepage:       http://code.haskell.org/~wren/ Author:         wren gayle romano@@ -21,7 +21,9 @@ Synopsis:       Simple generic unification algorithms. Description:    Simple generic unification algorithms. --- No longer compiles with GHC-6.12.1 since Data.Monoid does not export (<>) in Control.Unification.Types. The backwards compatibility is not considered worth adding CPP noise...+-- No longer compiles with GHC-6.12.1 since Data.Monoid does not+-- export (<>) in Control.Unification.Types. The backwards compatibility+-- is not considered worth adding CPP noise... Tested-With:     GHC == 7.6.1, GHC == 7.6.3, GHC == 7.8.2 Extra-source-files: