1 patch for repository http://community.haskell.org/~wren/unification-fd: Sun Mar 25 15:04:06 BST 2012 Francesco Mazzoli * Use typeclasses instead of manual lifting Added generic BindingMonad instances for all the types in transformers/mtl, and removed all the manual lifting in Unification.hs. New patches: [Use typeclasses instead of manual lifting Francesco Mazzoli **20120325140406 Ignore-this: 5bd5cd45210b07d6fd177af03e439c3 Added generic BindingMonad instances for all the types in transformers/mtl, and removed all the manual lifting in Unification.hs. ] hunk ./src/Control/Unification.hs 88 import Control.Monad.Identity (Identity(..)) 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) import Control.Monad.MaybeK hunk ./src/Control/Unification.hs 162 -- variable has already been seen. seenAs :: ( BindingMonad t v m - , MonadTrans e - , MonadError (UnificationFailure t v) (e m) + , MonadError (UnificationFailure t v) m ) => v -- ^ -> t (UTerm t v) -- ^ hunk ./src/Control/Unification.hs 166 - -> StateT (IM.IntMap (t (UTerm t v))) (e m) () -- ^ + -> StateT (IM.IntMap (t (UTerm t v))) m () -- ^ {-# INLINE seenAs #-} seenAs v0 t0 = do seenVars <- get hunk ./src/Control/Unification.hs 171 case IM.lookup (getVarID v0) seenVars of - Just t -> lift . throwError $ OccursIn v0 (UTerm t) + Just t -> throwError $ OccursIn v0 (UTerm t) Nothing -> put $! IM.insert (getVarID v0) t0 seenVars ---------------------------------------------------------------- hunk ./src/Control/Unification.hs 215 loopAll = foldrM (\t r -> IM.union r <$> loop t) IM.empty loop t0 = do - t0 <- lift $ semiprune t0 + t0 <- semiprune t0 case t0 of UTerm t -> fold <$> mapM loop t -- TODO: benchmark using the following instead: hunk ./src/Control/Unification.hs 227 then return IM.empty -- no (more) free vars down here else do put $! IS.insert i seenVars - mb <- lift $ lookupVar v + mb <- lookupVar v case mb of Just t' -> loop t' Nothing -> return $ IM.singleton i v hunk ./src/Control/Unification.hs 244 -- 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) + , Functor m -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure t v) m ) => UTerm t v -- ^ hunk ./src/Control/Unification.hs 248 - -> e m (UTerm t v) -- ^ + -> m (UTerm t v) -- ^ applyBindings = fmap runIdentity . applyBindingsAll . Identity hunk ./src/Control/Unification.hs 260 -- /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) + , Functor m -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure t v) m , Traversable s ) => s (UTerm t v) -- ^ hunk ./src/Control/Unification.hs 265 - -> e m (s (UTerm t v)) -- ^ + -> m (s (UTerm t v)) -- ^ applyBindingsAll ts0 = evalStateT (mapM loop ts0) IM.empty where loop t0 = do hunk ./src/Control/Unification.hs 269 - t0 <- lift . lift $ semiprune t0 + t0 <- semiprune t0 case t0 of UTerm t -> UTerm <$> mapM loop t UVar v -> do hunk ./src/Control/Unification.hs 277 mb <- IM.lookup i <$> get case mb of Just (Right t) -> return t - Just (Left t) -> lift . throwError $ OccursIn v t + Just (Left t) -> throwError $ OccursIn v t Nothing -> do hunk ./src/Control/Unification.hs 279 - mb' <- lift . lift $ lookupVar v + mb' <- lookupVar v case mb' of Nothing -> return t0 Just t -> do hunk ./src/Control/Unification.hs 298 -- 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) + , MonadError (UnificationFailure t v) m + , Functor m ) => UTerm t v -- ^ hunk ./src/Control/Unification.hs 302 - -> e m (UTerm t v) -- ^ + -> m (UTerm t v) -- ^ freshen = fmap runIdentity . freshenAll . Identity hunk ./src/Control/Unification.hs 323 -- /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) + , MonadError (UnificationFailure t v) m + , Functor m -- Grr, Monad(e m) should imply Functor(e m) , Traversable s ) => s (UTerm t v) -- ^ hunk ./src/Control/Unification.hs 328 - -> e m (s (UTerm t v)) -- ^ + -> m (s (UTerm t v)) -- ^ freshenAll ts0 = evalStateT (mapM loop ts0) IM.empty where loop t0 = do hunk ./src/Control/Unification.hs 332 - t0 <- lift . lift $ semiprune t0 + t0 <- semiprune t0 case t0 of UTerm t -> UTerm <$> mapM loop t UVar v -> do hunk ./src/Control/Unification.hs 340 seenVars <- get case IM.lookup i seenVars of Just (Right t) -> return t - Just (Left t) -> lift . throwError $ OccursIn v t + Just (Left t) -> throwError $ OccursIn v t Nothing -> do hunk ./src/Control/Unification.hs 342 - mb <- lift . lift $ lookupVar v + mb <- lookupVar v case mb of Nothing -> do hunk ./src/Control/Unification.hs 345 - v' <- lift . lift $ UVar <$> freeVar + v' <- UVar <$> freeVar put $! IM.insert i (Right v') seenVars return v' Just t -> do hunk ./src/Control/Unification.hs 351 put $! IM.insert i (Left t) seenVars t' <- loop t - v' <- lift . lift $ UVar <$> newVar t' + v' <- UVar <$> newVar t' modify' $ IM.insert i (Right v') return v' hunk ./src/Control/Unification.hs 384 -- | '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) + , Functor m -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure t v) m ) => UTerm t v -- ^ -> UTerm t v -- ^ hunk ./src/Control/Unification.hs 389 - -> e m (UTerm t v) -- ^ + -> m (UTerm t v) -- ^ (=:=) = unify {-# INLINE (=:=) #-} infix 4 =:=, `unify` hunk ./src/Control/Unification.hs 398 -- | '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) + , Functor m -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure t v) m ) => UTerm t v -- ^ -> UTerm t v -- ^ hunk ./src/Control/Unification.hs 403 - -> e m Bool -- ^ + -> m Bool -- ^ (<:=) = subsumes {-# INLINE (<:=) #-} infix 4 <:=, `subsumes` hunk ./src/Control/Unification.hs 438 Just () -> return True where loop tl0 tr0 = do - tl0 <- lift $ semiprune tl0 - tr0 <- lift $ semiprune tr0 + tl0 <- semiprune tl0 + tr0 <- semiprune tr0 case (tl0, tr0) of (UVar vl, UVar vr) | vl == vr -> return () -- success hunk ./src/Control/Unification.hs 444 | otherwise -> do - mtl <- lift $ lookupVar vl - mtr <- lift $ lookupVar vr + mtl <- lookupVar vl + mtr <- lookupVar vr case (mtl, mtr) of (Nothing, Nothing) -> mzero (Nothing, Just _ ) -> mzero hunk ./src/Control/Unification.hs 483 equiv tl0 tr0 = runMaybeKT (execStateT (loop tl0 tr0) IM.empty) where loop tl0 tr0 = do - tl0 <- lift . lift $ fullprune tl0 - tr0 <- lift . lift $ fullprune tr0 + tl0 <- fullprune tl0 + tr0 <- fullprune tr0 case (tl0, tr0) of (UVar vl, UVar vr) -> do let il = getVarID vl hunk ./src/Control/Unification.hs 493 case IM.lookup il xs of Just x | x == ir -> return () -- success; no changes - | otherwise -> lift mzero + | otherwise -> mzero Nothing -> put $! IM.insert il ir xs hunk ./src/Control/Unification.hs 496 - (UVar _, UTerm _ ) -> lift mzero - (UTerm _, UVar _ ) -> lift mzero + (UVar _, UTerm _ ) -> mzero + (UTerm _, UVar _ ) -> mzero (UTerm tl, UTerm tr) -> case zipMatch tl tr of hunk ./src/Control/Unification.hs 500 - Nothing -> lift mzero + Nothing -> mzero Just tlr -> mapM_ loop_ tlr loop_ (Left _) = return () -- success; no changes hunk ./src/Control/Unification.hs 518 -- 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) + , Functor m -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure t v) m ) => UTerm t v -- ^ -> UTerm t v -- ^ hunk ./src/Control/Unification.hs 523 - -> e m (UTerm t v) -- ^ + -> m (UTerm t v) -- ^ unifyOccurs = loop where {-# INLINE (=:) #-} hunk ./src/Control/Unification.hs 527 - v =: t = lift $ v `bindVar` t + v =: t = v `bindVar` t {-# INLINE acyclicBindVar #-} acyclicBindVar v t = do hunk ./src/Control/Unification.hs 531 - b <- lift $ v `occursIn` t + b <- v `occursIn` t if b then throwError $ OccursIn v t else v =: t hunk ./src/Control/Unification.hs 538 -- TODO: cf todos in 'unify' loop tl0 tr0 = do - tl0 <- lift $ semiprune tl0 - tr0 <- lift $ semiprune tr0 + tl0 <- semiprune tl0 + tr0 <- semiprune tr0 case (tl0, tr0) of (UVar vl, UVar vr) | vl == vr -> return tr0 hunk ./src/Control/Unification.hs 544 | otherwise -> do - mtl <- lift $ lookupVar vl - mtr <- lift $ lookupVar vr + mtl <- lookupVar vl + mtr <- lookupVar vr case (mtl, mtr) of (Nothing, Nothing) -> do vl =: tr0 hunk ./src/Control/Unification.hs 564 _ -> error _impossible_unifyOccurs (UVar vl, UTerm tr) -> do - mtl <- lift $ lookupVar vl + mtl <- lookupVar vl case mtl of Nothing -> do vl `acyclicBindVar` tr0 hunk ./src/Control/Unification.hs 576 _ -> error _impossible_unifyOccurs (UTerm tl, UVar vr) -> do - mtr <- lift $ lookupVar vr + mtr <- lookupVar vr case mtr of Nothing -> do vr `acyclicBindVar` tl0 hunk ./src/Control/Unification.hs 615 -- 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) + , Functor m -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure t v) m ) => UTerm t v -- ^ -> UTerm t v -- ^ hunk ./src/Control/Unification.hs 620 - -> e m (UTerm t v) -- ^ + -> m (UTerm t v) -- ^ unify tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty where {-# INLINE (=:) #-} hunk ./src/Control/Unification.hs 624 - v =: t = lift . lift $ v `bindVar` t + v =: t = 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 hunk ./src/Control/Unification.hs 628 - tl0 <- lift . lift $ semiprune tl0 - tr0 <- lift . lift $ semiprune tr0 + tl0 <- semiprune tl0 + tr0 <- semiprune tr0 case (tl0, tr0) of (UVar vl, UVar vr) | vl == vr -> return tr0 hunk ./src/Control/Unification.hs 634 | otherwise -> do - mtl <- lift . lift $ lookupVar vl - mtr <- lift . lift $ lookupVar vr + mtl <- lookupVar vl + mtr <- lookupVar vr case (mtl, mtr) of (Nothing, Nothing) -> do vl =: tr0 ; return tr0 (Nothing, Just _ ) -> do vl =: tr0 ; return tr0 hunk ./src/Control/Unification.hs 652 (UVar vl, UTerm tr) -> do t <- do - mtl <- lift . lift $ lookupVar vl + mtl <- lookupVar vl case mtl of Nothing -> return tr0 Just (UTerm tl) -> localState $ do hunk ./src/Control/Unification.hs 664 (UTerm tl, UVar vr) -> do t <- do - mtr <- lift . lift $ lookupVar vr + mtr <- lookupVar vr case mtr of Nothing -> return tl0 Just (UTerm tr) -> localState $ do hunk ./src/Control/Unification.hs 678 match tl tr = case zipMatch tl tr of - Nothing -> lift . throwError $ TermMismatch tl tr + Nothing -> throwError $ TermMismatch tl tr Just tlr -> UTerm <$> mapM loop_ tlr loop_ (Left t) = return t hunk ./src/Control/Unification.hs 712 -- 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) + , Functor m -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure t v) m ) => UTerm t v -- ^ -> UTerm t v -- ^ hunk ./src/Control/Unification.hs 717 - -> e m Bool -- ^ + -> m Bool -- ^ subsumes tl0 tr0 = evalStateT (loop tl0 tr0) IM.empty where {-# INLINE (=:) #-} hunk ./src/Control/Unification.hs 721 - v =: t = lift . lift $ do v `bindVar` t ; return True + v =: t = do v `bindVar` t ; return True -- TODO: cf todos in 'unify' loop tl0 tr0 = do hunk ./src/Control/Unification.hs 725 - tl0 <- lift . lift $ semiprune tl0 - tr0 <- lift . lift $ semiprune tr0 + tl0 <- semiprune tl0 + tr0 <- semiprune tr0 case (tl0, tr0) of (UVar vl, UVar vr) | vl == vr -> return True hunk ./src/Control/Unification.hs 731 | otherwise -> do - mtl <- lift . lift $ lookupVar vl - mtr <- lift . lift $ lookupVar vr + mtl <- lookupVar vl + mtr <- lookupVar vr case (mtl, mtr) of (Nothing, Nothing) -> vl =: tr0 (Nothing, Just _ ) -> vl =: tr0 hunk ./src/Control/Unification.hs 745 _ -> error _impossible_subsumes (UVar vl, UTerm tr) -> do - mtl <- lift . lift $ lookupVar vl + mtl <- lookupVar vl case mtl of Nothing -> vl =: tr0 Just (UTerm tl) -> localState $ do hunk ./src/Control/Unification/Types.hs 4 -- Required for Show instances {-# LANGUAGE FlexibleContexts, UndecidableInstances #-} -- Required more generally -{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, + FlexibleInstances #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ---------------------------------------------------------------- hunk ./src/Control/Unification/Types.hs 40 import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1) -import Data.Word (Word8) -import Data.Functor.Fixedpoint (Fix(..)) -import Data.Foldable (Foldable(..)) -import Data.Traversable (Traversable(..)) -import Control.Applicative (Applicative(..), (<$>), Alternative(..)) -import Control.Monad (MonadPlus(..)) -import Control.Monad.Error (Error(..)) +import Data.Word (Word8) +import Data.Functor.Fixedpoint (Fix(..)) +import Data.Foldable (Foldable(..)) +import Data.Monoid (Monoid) +import Data.Traversable (Traversable(..)) +import Control.Applicative (Applicative(..), (<$>), Alternative(..)) +import Control.Monad (MonadPlus(..)) +import Control.Monad.Error (Error(..), ErrorT) +import Control.Monad.List (ListT) +import Control.Monad.MaybeK (MaybeKT) +import Control.Monad.RWS (RWST) +import Control.Monad.Reader (ReaderT) +import Control.Monad.State (StateT) +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (MaybeT) +import Control.Monad.Writer (WriterT) ---------------------------------------------------------------- ---------------------------------------------------------------- hunk ./src/Control/Unification/Types.hs 279 -- | Bind a variable to a term, overriding any previous binding. bindVar :: v -> UTerm t v -> m () +instance (BindingMonad t v m) => BindingMonad t v (MaybeKT m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v + +instance (BindingMonad t v m) => BindingMonad t v (StateT s m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v + +instance (Error e, BindingMonad t v m) => BindingMonad t v (ErrorT e m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v + +instance (Monoid w, BindingMonad t v m) => BindingMonad t v (WriterT w m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v + +instance (BindingMonad t v m) => BindingMonad t v (ReaderT r m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v + +instance (BindingMonad t v m) => BindingMonad t v (ListT m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v + +instance (BindingMonad t v m) => BindingMonad t v (MaybeT m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v + +instance (Monoid w, BindingMonad t v m) => BindingMonad t v (RWST r w s m) where + lookupVar = lift . lookupVar + freeVar = lift freeVar + newVar = lift . newVar + bindVar v = lift . bindVar v ---------------------------------------------------------------- -- | The target of variables for 'RankedBindingMonad's. In order hunk ./unification-fd.cabal 67 -- StateT. And we want stuff from monads-fd, so -- we can't just fail over to the older mtl. , mtl >= 2.0 + -- MaybeT was added in 0.1.3.0 + , transformers >= 0.1.3.0 if flag(base4) Build-Depends: base >= 4 && < 5 Context: [Control.Unification.Types: Changed the type of Unifiable.zipMatch wren ng thornton **20120325100536 Ignore-this: 600127635913025d580e39c96b8b1387 ] [Added some of the experiments wren ng thornton **20120325084541 Ignore-this: d295c5aa01f4ee503a61329764fc00bd ] [AUTHORS: nudge wren ng thornton **20120319070648 Ignore-this: 3725231d41d83ca1ac07dd9edefcdf6d ] [TAG 0.7.0 wren ng thornton **20120319070137 Ignore-this: 9e3eb875751a3c00b902e7131b85a5ce ] Patch bundle hash: d722d326ed3de78497f5a08b37d31f567045210e