unification-fd (empty) → 0.5.0
raw patch · 14 files changed
+2648/−0 lines, 14 filesdep +basedep +containersdep +logictsetup-changed
Dependencies added: base, containers, logict, mtl
Files
- LICENSE +45/−0
- Setup.hs +7/−0
- src/Control/Monad/EitherK.hs +219/−0
- src/Control/Monad/MaybeK.hs +180/−0
- src/Control/Monad/State/UnificationExtras.hs +66/−0
- src/Control/Unification.hs +653/−0
- src/Control/Unification/IntVar.hs +205/−0
- src/Control/Unification/Ranked.hs +177/−0
- src/Control/Unification/Ranked/IntVar.hs +189/−0
- src/Control/Unification/Ranked/STVar.hs +146/−0
- src/Control/Unification/STVar.hs +125/−0
- src/Control/Unification/Types.hs +256/−0
- src/Data/Functor/Fixedpoint.hs +305/−0
- unification-fd.cabal +75/−0
+ LICENSE view
@@ -0,0 +1,45 @@+=== Notes ===++The following license applies to all code in this package. The+module Control.Monad.MaybeK is derived from code on the Haskell+Wiki[1] which was released under a simple permissive license[2].++[1] <http://www.haskell.org/haskellwiki/Performance/Monads>+[2] <http://www.haskell.org/haskellwiki/HaskellWiki:Copyrights>+++=== unification-fd license ===++Copyright (c) 2007, 2008, 2011, wren ng thornton.+ALL RIGHTS RESERVED.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of the copyright holders nor the names of+ other contributors may be used to endorse or promote products+ derived from this software without specific prior written+ permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS+FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE+COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.+
+ Setup.hs view
@@ -0,0 +1,7 @@+#!/usr/bin/env runhaskell++module Main (main) where+import Distribution.Simple++main :: IO ()+main = defaultMain
+ src/Control/Monad/EitherK.hs view
@@ -0,0 +1,219 @@++-- The MPTCs and FlexibleInstances are only for+-- mtl:Control.Monad.Error.MonadError+{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleInstances #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.06.30+-- |+-- Module : Control.Monad.EitherK+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : provisional+-- Portability : semi-portable (Rank2Types, MPTCs, FlexibleInstances)+--+-- A continuation-passing variant of 'Either' for short-circuiting+-- at failure. This code is based on "Control.Monad.MaybeK".+----------------------------------------------------------------+module Control.Monad.EitherK+ (+ -- * The short-circuiting monad+ EitherK()+ , runEitherK+ , toEitherK+ , eitherK+ , throwEitherK+ , catchEitherK+ -- * The short-circuiting monad transformer+ , EitherKT()+ , runEitherKT+ , toEitherKT+ , liftEitherK+ , lowerEitherK+ , throwEitherKT+ , 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(..))+----------------------------------------------------------------+----------------------------------------------------------------++-- | A continuation-passing encoding of 'Either' as an error monad;+-- also known as @Codensity (Either e)@, if you're familiar with+-- that terminology. N.B., this is not the 2-continuation implementation+-- based on the Church encoding of @Either@. The latter tends to+-- have worse performance than non-continuation based implementations.+--+-- This is generally more efficient than using @Either@ (or the+-- MTL's @Error@) for two reasons. First is that it right associates+-- all binds, ensuring that bad associativity doesn't artificially+-- introduce midpoints in short-circuiting to the nearest handler.+-- Second is that it removes the need for intermediate case+-- expressions.+--+-- Another benefit over MTL's @Error@ is that it doesn't artificially+-- restrict the error type. In fact, there's no reason why @e@ must+-- denote \"errors\" per se. This could also denote computations+-- which short-circuit with the final answer, or similar methods+-- of non-local control flow.+--+-- N.B., the 'Alternative' and 'MonadPlus' instances are left-biased+-- in @a@ and monoidal in @e@. Thus, they are not commutative.+newtype EitherK e a = EK (forall r. (a -> Either e r) -> Either e r)+++-- | Execute an @EitherK@ and return the concrete @Either@ encoding.+runEitherK :: EitherK e a -> Either e a+runEitherK (EK m) = m Right+{-# INLINE runEitherK #-}+++-- | Lift an @Either@ into an @EitherK@.+toEitherK :: Either e a -> EitherK e a+toEitherK (Left e) = throwEitherK e+toEitherK (Right a) = return a+{-# INLINE toEitherK #-}+++-- | Throw an error in the @EitherK@ monad. This is identical to+-- 'throwError'.+throwEitherK :: e -> EitherK e a+throwEitherK e = EK (\_ -> Left e)+{-# INLINE throwEitherK #-}+++-- | Handle errors in the @EitherK@ monad. N.B., this type is more+-- general than that of 'catchError', allowing the type of the+-- errors to change.+catchEitherK :: EitherK e a -> (e -> EitherK f a) -> EitherK f a+catchEitherK m handler = eitherK handler return m+{-# INLINE catchEitherK #-}+++-- | A version of 'either' on @EitherK@, for convenience. N.B.,+-- using this function inserts a case match, reducing the range of+-- short-circuiting.+eitherK :: (e -> b) -> (a -> b) -> EitherK e a -> b+eitherK left right m =+ case runEitherK m of+ Left e -> left e+ Right a -> right a+{-# INLINE eitherK #-}+++instance Functor (EitherK e) where+ fmap f (EK m) = EK (\k -> m (k . f))++instance Applicative (EitherK e) where+ pure = return+ (<*>) = ap++instance Monad (EitherK e) where+ return a = EK (\k -> k a)+ EK m >>= f = EK (\k -> m (\a -> case f a of EK n -> n k))+ -- Using case instead of let seems to improve performance+ -- considerably by removing excessive laziness.++instance (Monoid e) => Alternative (EitherK e) where+ empty = mzero+ (<|>) = mplus++instance (Monoid e) => MonadPlus (EitherK e) where+ mzero = throwEitherK mempty+ m `mplus` n = catchEitherK m $ \me ->+ catchEitherK n $ \ne ->+ throwEitherK $ me `mappend` ne++instance MonadError e (EitherK e) where+ throwError = throwEitherK+ catchError = catchEitherK++----------------------------------------------------------------+----------------------------------------------------------------++-- | A monad transformer version of 'EitherK'.+newtype EitherKT e m a =+ EKT (forall r. (a -> m (Either e r)) -> m (Either e r))+++-- | Execute an @EitherKT@ and return the concrete @Either@ encoding.+runEitherKT :: (Monad m) => EitherKT e m a -> m (Either e a)+runEitherKT (EKT m) = m (return . Right)+{-# INLINE runEitherKT #-}+++-- | Lift an @Either@ into an @EitherKT@.+toEitherKT :: (Monad m) => Either e a -> EitherKT e m a+toEitherKT (Left e) = throwEitherKT e+toEitherKT (Right a) = return a+{-# INLINE toEitherKT #-}+++-- 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+liftEitherK = toEitherKT . runEitherK+{-# INLINE liftEitherK #-}+++-- TODO: is there a better implementation?+-- | Lower an @EitherKT@ into an @EitherK@.+lowerEitherK :: (Monad m) => EitherKT e m a -> m (EitherK e a)+lowerEitherK = liftM toEitherK . runEitherKT+{-# INLINE lowerEitherK #-}+++-- | Throw an error in the @EitherKT@ monad. This is identical to+-- 'throwError'.+throwEitherKT :: (Monad m) => e -> EitherKT e m a+throwEitherKT e = EKT (\_ -> return (Left e))+{-# INLINE throwEitherKT #-}+++-- | 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)+ => EitherKT e m a -> (e -> EitherKT f m a) -> EitherKT f m a+catchEitherKT m handler = EKT $ \k -> do+ ea <- runEitherKT m+ case ea of+ Left e -> case handler e of EKT m' -> m' k+ Right a -> k a+{-# INLINE catchEitherKT #-}+++instance Functor (EitherKT e m) where+ fmap f (EKT m) = EKT (\k -> m (k . f))++instance Applicative (EitherKT e m) where+ pure = return+ (<*>) = ap++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?+instance (Monad m, Monoid e) => Alternative (EitherKT e m) where+ empty = mzero+ (<|>) = mplus++instance (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+ throwError = throwEitherKT+ catchError = catchEitherKT++instance MonadTrans (EitherKT e) where+ lift m = EKT (\k -> m >>= k)++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Monad/MaybeK.hs view
@@ -0,0 +1,180 @@+-- The MPTCs is only for mtl:Control.Monad.Error.MonadError+{-# LANGUAGE Rank2Types, MultiParamTypeClasses #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.06.30+-- |+-- Module : Control.Monad.MaybeK+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : provisional+-- Portability : semi-portable (Rank2Types, MPTCs)+--+-- A continuation-passing variant of 'Maybe' for short-circuiting+-- at failure. This is based largely on code from the Haskell Wiki+-- (<http://www.haskell.org/haskellwiki/Performance/Monads>) which+-- was released under a simple permissive license+-- (<http://www.haskell.org/haskellwiki/HaskellWiki:Copyrights>).+-- However, various changes and extensions have been made, which+-- are subject to the BSD license of this package.+----------------------------------------------------------------+module Control.Monad.MaybeK+ (+ -- * The partiality monad+ MaybeK+ , runMaybeK+ , toMaybeK+ , maybeK+ -- * The partiality monad transformer+ , MaybeKT+ , runMaybeKT+ , toMaybeKT+ , liftMaybeK+ , lowerMaybeK+ ) where++import Control.Applicative (Applicative(..), Alternative(..))+import Control.Monad (MonadPlus(..), liftM, ap)+import Control.Monad.Error (MonadError(..))+import Control.Monad.Trans (MonadTrans(..))+----------------------------------------------------------------+----------------------------------------------------------------++-- | A continuation-passing encoding of 'Maybe'; also known as+-- @Codensity Maybe@, if you're familiar with that terminology.+-- N.B., this is not the 2-continuation implementation based on the+-- Church encoding of @Maybe@. The latter tends to have worse+-- performance than non-continuation based implementations.+--+-- This is generally more efficient than using @Maybe@ for two+-- reasons. First is that it right associates all binds, ensuring+-- that bad associativity doesn't artificially introduce midpoints+-- in short-circuiting to the nearest handler. Second is that it+-- removes the need for intermediate case expressions.+--+-- N.B., the 'Alternative' and 'MonadPlus' instances are left-biased+-- in @a@. Thus, they are not commutative.+newtype MaybeK a = MK (forall r. (a -> Maybe r) -> Maybe r)+++-- | Execute the @MaybeK@ and return the concrete @Maybe@ encoding.+runMaybeK :: MaybeK a -> Maybe a+runMaybeK (MK m) = m return+{-# INLINE runMaybeK #-}+++-- | Lift a @Maybe@ into @MaybeK@.+toMaybeK :: Maybe a -> MaybeK a+toMaybeK Nothing = mzero+toMaybeK (Just a) = return a+{-# INLINE toMaybeK #-}+++-- | A version of 'maybe' for convenience. This is almost identical+-- to 'mplus' but allows applying a continuation to @Just@ values+-- as well as handling @Nothing@ errors. If you only want to handle+-- the errors, use 'mplus' instead.+maybeK :: b -> (a -> b) -> MaybeK a -> b+maybeK nothing just m =+ case runMaybeK m of+ Nothing -> nothing+ Just a -> just a+{-# INLINE maybeK #-}+++instance Functor MaybeK where+ fmap f (MK m) = MK (\k -> m (k . f))++instance Applicative MaybeK where+ pure = return+ (<*>) = ap++instance Monad MaybeK where+ return a = MK (\k -> k a)+ MK m >>= f = MK (\k -> m (\a -> case f a of MK n -> n k))+ -- Using case instead of let seems to improve performance+ -- considerably by removing excessive laziness.++-- This is non-commutative, but it's the same as Alternative Maybe.+instance Alternative MaybeK where+ empty = mzero+ (<|>) = mplus++instance MonadPlus MaybeK where+ mzero = MK (\_ -> Nothing)+ m `mplus` n = maybeK n return m++instance MonadError () MaybeK where+ throwError _ = mzero+ catchError m f = maybeK (f ()) return m++----------------------------------------------------------------++-- | A monad transformer version of 'MaybeK'.+newtype MaybeKT m a = MKT (forall r . (a -> m (Maybe r)) -> m (Maybe r))+++-- | Execute a @MaybeKT@ and return the concrete @Maybe@ encoding.+runMaybeKT :: (Monad m) => MaybeKT m a -> m (Maybe a)+runMaybeKT (MKT m) = m (return . Just)+{-# INLINE runMaybeKT #-}+++-- | Lift a @Maybe@ into an @MaybeKT@.+toMaybeKT :: (Monad m) => Maybe a -> MaybeKT m a+toMaybeKT Nothing = mzero+toMaybeKT (Just a) = return a+{-# INLINE toMaybeKT #-}+++-- 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+liftMaybeK = toMaybeKT . runMaybeK+{-# INLINE liftMaybeK #-}+++-- TODO: is there a better implementation?+-- | Lower an @MaybeKT@ into an @MaybeK@.+lowerMaybeK :: (Monad m) => MaybeKT m a -> m (MaybeK a)+lowerMaybeK = liftM toMaybeK . runMaybeKT+{-# INLINE lowerMaybeK #-}+++instance Functor (MaybeKT m) where+ fmap f (MKT m) = MKT (\k -> m (k . f))++instance Applicative (MaybeKT m) where+ pure = return+ (<*>) = ap++instance Monad (MaybeKT m) where+ 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+ empty = mzero+ (<|>) = mplus++instance (Monad m) => MonadPlus (MaybeKT m) where+ mzero = MKT (\_ -> return Nothing)+ + m `mplus` n = MKT $ \k -> do+ mb <- runMaybeKT m+ case mb of+ Nothing -> case n of MKT n' -> n' k+ Just a -> k a++instance (Monad m) => MonadError () (MaybeKT m) where+ throwError _ = mzero+ catchError m f = MKT $ \k -> do+ mb <- runMaybeKT m+ case mb of+ Nothing -> case f () of MKT n -> n k+ Just a -> k a++instance MonadTrans MaybeKT where+ lift m = MKT (\k -> m >>= k)++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Monad/State/UnificationExtras.hs view
@@ -0,0 +1,66 @@++{-# LANGUAGE MultiParamTypeClasses #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.07.05+-- |+-- Module : Control.Monad.State.UnificationExtras+-- Copyright : Copyright (c) 2008--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : perpetually unstable+-- Portability : semi-portable (MPTCs)+--+-- This module defines some extra functions for "Control.Monad.State.Lazy".+-- This package really isn't the proper place for these, but we+-- need them to be somewhere.+--+-- TODO: patch transformers\/mtl-2 with these functions.+----------------------------------------------------------------+module Control.Monad.State.UnificationExtras+ (+ -- * Additional functions for MTL+ liftReader+ , liftReaderT+ , modify'+ , localState+ ) where++import Control.Monad (liftM)+import Control.Monad.Reader (Reader(), ReaderT(..))+import Control.Monad.State.Lazy (MonadState(..), State(), StateT(..))++----------------------------------------------------------------+----------------------------------------------------------------++-- | 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+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+liftReader = liftReaderT+++-- | A strict version of 'modify'.+modify' :: (MonadState s m) => (s -> s) -> m ()+modify' f = do+ s <- get+ put $! f s+{-# INLINE modify' #-}+++-- | Run a state action and undo the state changes at the end.+localState :: (MonadState s m) => m a -> m a+localState m = do+ s <- get+ x <- m+ put s+ return x+{-# INLINE localState #-}++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Unification.hs view
@@ -0,0 +1,653 @@++{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.07.11+-- |+-- Module : Control.Unification+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : experimental+-- Portability : semi-portable (MPTCs, FlexibleContexts)+--+-- This module provides first-order structural unification over+-- general structure types. It also provides the standard suite of+-- functions accompanying unification (applying bindings, getting+-- free variables, etc.).+--+-- The implementation makes use of numerous optimization techniques.+-- First, we use path compression everywhere (for weighted path+-- compression see "Control.Unification.Ranked"). Second, we replace+-- the occurs-check with visited-sets. Third, we use a technique+-- for aggressive opportunistic observable sharing; that is, we+-- track as much sharing as possible in the bindings (without+-- introducing new variables), so that we can compare bound variables+-- directly and therefore eliminate redundant unifications.+----------------------------------------------------------------+module Control.Unification+ (+ -- * Data types, classes, etc+ -- ** Mutable terms+ MutTerm(..)+ , freeze+ , unfreeze+ -- ** Errors+ , UnificationFailure(..)+ -- ** Basic type classes+ , Unifiable(..)+ , Variable(..)+ , BindingMonad(..)+ + -- * Operations on one term+ , getFreeVars+ , applyBindings+ , freshen+ -- freezeM -- apply bindings and freeze in one traversal+ -- unskolemize -- convert Skolemized variables to free variables+ -- skolemize -- convert free variables to Skolemized variables+ -- getSkolems -- compute the skolem variables in a term; helpful?+ + -- * Operations on two terms+ -- ** Symbolic names+ , (===)+ , (=~=)+ , (=:=)+ , (<:=)+ -- ** Textual names+ , equals+ , equiv+ , unify+ , unifyOccurs+ , subsumes+ + -- * Helper functions+ -- | Client code should not need to use these functions, but+ -- they are exposed just in case they are needed.+ , fullprune+ , semiprune+ , occursIn+ ) where++import Prelude+ hiding (mapM, mapM_, sequence, foldr, foldr1, foldl, foldl1, all, and, or)++import qualified Data.IntMap as IM+import qualified Data.IntSet as IS+import Data.Foldable+import Data.Traversable+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+import Control.Monad.State.UnificationExtras+import Control.Unification.Types+----------------------------------------------------------------+----------------------------------------------------------------++-- BUG: this assumes there are no directly-cyclic chains!+--+-- | Canonicalize a chain of variables so they all point directly+-- to the term at the end of the chain (or the free variable, if+-- 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+++-- BUG: this assumes there are no directly-cyclic chains!+--+-- | Canonicalize a chain of variables so they all point directly+-- to the last variable in the chain, regardless of whether it is+-- 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+ where+ -- We pass the @t@ for @v@ in order to add just a little more sharing.+ loop t v = do+ mb <- lookupVar v+ case mb of+ Nothing -> return t+ Just t' -> + case t' of+ MutTerm _ -> return t+ MutVar v' -> do+ finalVar <- loop t' v'+ v `bindVar` finalVar+ return finalVar+++-- | Determine if a variable appears free somewhere inside a term.+-- 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) -> 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'+++-- 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+ , MonadTrans e+ , MonadError (UnificationFailure v t) (e m)+ )+ => v (MutTerm v t) -- ^+ -> MutTerm v t -- ^+ -> StateT (IM.IntMap (MutTerm v t)) (e m) ()+seenAs v 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 seenAs #-}++----------------------------------------------------------------+----------------------------------------------------------------++-- TODO: these assume pure variables, hence the spine cloning; but+-- we may want to make variants for impure variables with explicit+-- rollback on backtracking.++-- TODO: See if MTL still has that overhead over doing things manually.++-- TODO: Figure out how to abstract the left-catamorphism from these.+++-- | Walk a term and determine what 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 (MutTerm v t)]+getFreeVars =+ \t -> IM.elems <$> evalStateT (loop t) IS.empty+ where+ loop t0 = do+ t1 <- lift $ semiprune t0+ case t1 of+ MutTerm t -> fold <$> mapM loop t -- TODO: use foldlM instead?+ MutVar v -> do+ seenVars <- get+ let i = getVarID v+ if IS.member i seenVars+ then return IM.empty -- no (more) free vars down here+ else do+ put $! IS.insert i seenVars+ mb <- lift $ lookupVar v+ case mb of+ Just t' -> loop t'+ Nothing -> return $ IM.singleton i v+++-- | 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.+--+-- If any cyclic bindings are detected, then an 'OccursIn' exception+-- will be thrown.+applyBindings+ :: ( BindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> e m (MutTerm v t) -- ^+applyBindings =+ \t -> evalStateT (loop t) IM.empty+ where+ loop t0 = do+ t1 <- lift . lift $ semiprune t0+ case t1 of+ MutTerm t -> MutTerm <$> mapM loop t+ MutVar v -> do+ let i = getVarID v+ mb <- IM.lookup i <$> get+ case mb of+ Just (Right t) -> return t+ Just (Left t) -> lift . throwError $ OccursIn v t+ Nothing -> do+ mb' <- lift . lift $ lookupVar v+ case mb' of+ Nothing -> return t1+ Just t -> do+ modify' . IM.insert i $ Left t+ t' <- loop t+ modify' . IM.insert i $ Right t'+ return t'+++-- | 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.+freshen+ :: ( BindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> e m (MutTerm v t) -- ^+freshen =+ \t -> evalStateT (loop t) IM.empty+ where+ loop t0 = do+ t1 <- lift . lift $ semiprune t0+ case t1 of+ MutTerm t -> MutTerm <$> mapM loop t+ MutVar v -> do+ let i = getVarID v+ seenVars <- get+ case IM.lookup i seenVars of+ Just (Right t) -> return t+ Just (Left t) -> lift . throwError $ OccursIn v t+ Nothing -> do+ mb <- lift . lift $ lookupVar v+ case mb of+ Nothing -> do+ v' <- lift . lift $ MutVar <$> 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'+ modify' $ IM.insert i (Right v')+ return v'++----------------------------------------------------------------+----------------------------------------------------------------+-- BUG: have to give the signatures for Haddock :(++-- | 'equals'+(===)+ :: (BindingMonad v t m)+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> m Bool -- ^+(===) = equals+infix 4 ===, `equals`+++-- | 'equiv'+(=~=)+ :: (BindingMonad v t m)+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> m (Maybe (IM.IntMap Int)) -- ^+(=~=) = equiv+infix 4 =~=, `equiv`+++-- | 'unify'+(=:=)+ :: ( BindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> e m (MutTerm v t) -- ^+(=:=) = unify+infix 4 =:=, `unify`+++-- | 'subsumes'+(<:=)+ :: ( BindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> e m Bool+(<:=) = subsumes+infix 4 <:=, `subsumes`++----------------------------------------------------------------++-- TODO: should we offer a variant which gives the reason for failure?+--+-- | Determine if two terms are structurally equal. This is essentially+-- equivalent to @('==')@ except that it does not require applying+-- bindings before comparing, so it is more efficient. N.B., this+-- 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+ 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'+ 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+++-- TODO: is that the most helpful return type?+--+-- | Determine if two terms are structurally equivalent; that is,+-- structurally equal modulo renaming of free variables. Returns a+-- 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 -- ^+ -> m (Maybe (IM.IntMap Int)) -- ^+equiv =+ \tl tr -> runMaybeKT (execStateT (loop tl tr) 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'+ xs <- get+ case IM.lookup il xs of+ Just x+ | x == ir -> return ()+ | 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+ Nothing -> lift mzero+ Just tlr -> mapM_ (uncurry loop) tlr+++----------------------------------------------------------------+-- Not quite unify2 from the benchmarks, since we do AOOS.+--+-- | 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+-- subterm to be traversed multiple times.+unifyOccurs+ :: ( BindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> e m (MutTerm v t) -- ^+unifyOccurs = loop+ where+ {-# INLINE (=:) #-}+ v =: t = lift $ v `bindVar` t+ + {-# INLINE acyclicBindVar #-}+ acyclicBindVar v t = do+ b <- lift $ v `occursIn` t+ if b+ then throwError $ OccursIn v t+ else v =: t+ + -- 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'+ 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+ + (MutVar vl', MutTerm _) -> 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+ + (MutTerm _, MutVar 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+ + (MutTerm tl', MutTerm tr') ->+ case zipMatch tl' tr' of+ Nothing -> throwError $ TermMismatch tl' tr'+ Just tlr -> MutTerm <$> mapM (uncurry loop) tlr+++----------------------------------------------------------------+-- 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: 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+-- unification failed. Since bindings are stored in the monad, the+-- two input terms and the output term are all equivalent if+-- unification succeeds. However, the returned value makes use of+-- aggressive opportunistic observable sharing, so it will be more+-- efficient to use it in future calculations than either argument.+unify+ :: ( BindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> e m (MutTerm v t) -- ^+unify =+ \tl tr -> evalStateT (loop tl tr) 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'+ 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+ t <- localState $ do+ vl' `seenAs` tl'+ vr' `seenAs` tr'+ loop tl' tr' -- TODO: should just jump to match+ vr' =: t+ vl' =: tr+ return tr+ + (MutVar vl', MutTerm _) -> do+ t <- do+ 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+ + (MutTerm _, MutVar vr') -> do+ t <- do+ 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+ + (MutTerm tl', MutTerm tr') ->+ case zipMatch tl' tr' of+ Nothing -> lift . throwError $ TermMismatch tl' tr'+ Just tlr -> MutTerm <$> mapM (uncurry loop) tlr++----------------------------------------------------------------+-- 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...++-- | Determine whether the left term subsumes the right term. That+-- is, whereas @(tl =:= tr)@ will compute the most general substitution+-- @s@ such that @(s tl === s tr)@, @(tl <:= tr)@ computes the most+-- general substitution @s@ such that @(s tl === tr)@. This means+-- that @tl@ is less defined than and consistent with @tr@.+--+-- /N.B./, this function updates the monadic bindings just like+-- 'unify' does. However, while the use cases for unification often+-- want to keep the bindings around, the use cases for subsumption+-- usually do not. Thus, you'll probably want to use a binding monad+-- which supports backtracking in order to undo the changes.+-- Unfortunately, leaving the monadic bindings unaltered and returning+-- the necessary substitution directly imposes a performance penalty+-- or else requires specifying too much about the implementation+-- of variables.+subsumes+ :: ( BindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> e m Bool+subsumes =+ \tl tr -> evalStateT (loop tl tr) 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'+ case (mtl, mtr) of+ (Nothing, Nothing ) -> vl' =: tr+ (Nothing, Just _ ) -> vl' =: tr+ (Just _ , Nothing ) -> return False+ (Just tl', Just tr') ->+ localState $ do+ vl' `seenAs` tl'+ vr' `seenAs` tr'+ loop tl' tr'+ + (MutVar vl', MutTerm _ ) -> do+ mtl <- lift . lift $ lookupVar vl'+ case mtl of+ Nothing -> vl' =: tr+ Just tl' -> localState $ do+ vl' `seenAs` tl'+ loop tl' tr+ + (MutTerm _, MutVar _ ) -> return False+ + (MutTerm tl', MutTerm tr') ->+ case zipMatch tl' tr' of+ Nothing -> return False+ Just tlr -> and <$> mapM (uncurry loop) tlr+ ++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Unification/IntVar.hs view
@@ -0,0 +1,205 @@++{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.07.06+-- |+-- Module : Control.Unification.IntVar+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : experimental+-- Portability : semi-portable (MPTCs,...)+--+-- This module defines a state monad for functional pointers+-- represented by integers as keys into an @IntMap@. This technique+-- was independently discovered by Dijkstra et al. This module+-- extends the approach by using a state monad transformer, which+-- can be made into a backtracking state monad by setting the+-- underlying monad to some 'MonadLogic' (part of the @logict@+-- library, described by Kiselyov et al.).+--+-- * Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)+-- /Efficient Functional Unification and Substitution/,+-- Technical Report UU-CS-2008-027, Utrecht University.+--+-- * Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and+-- Amr Sabry (2005) /Backtracking, Interleaving, and/+-- /Terminating Monad Transformers/, ICFP.+----------------------------------------------------------------+module Control.Unification.IntVar+ ( IntVar(..)+ , IntBindingState()+ , IntBindingT()+ , runIntBindingT+ , evalIntBindingT+ , execIntBindingT+ ) where++import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)++import qualified Data.IntMap as IM+import Control.Applicative+import Control.Monad (MonadPlus(..), liftM)+import Control.Monad.Trans (MonadTrans(..))+import Control.Monad.State (MonadState(..), StateT, runStateT, evalStateT, execStateT, gets)+import Control.Monad.Logic (MonadLogic(..))+import Control.Unification.Types+----------------------------------------------------------------+----------------------------------------------------------------++-- | A \"mutable\" unification variable implemented by an integer.+-- This provides an entirely pure alternative to truly mutable+-- alternatives (like @STVar@), which can make backtracking easier.+--+-- N.B., because this implementation is pure, we can use it for+-- both ranked and unranked monads.+newtype IntVar t = IntVar Int+ deriving (Show)++{-+-- BUG: This part works, but we'd want to change Show IntBindingState too.++instance Show (IntVar t) where+ show (IntVar i) = "IntVar " ++ show (boundedInt2Word i)++-- | Convert an integer to a word, via the continuous mapping that+-- preserves @minBound@ and @maxBound@.+boundedInt2Word :: Int -> Word+boundedInt2Word i+ | i < 0 = fromIntegral (i + maxBound + 1)+ | otherwise = fromIntegral i + fromIntegral (maxBound :: Int) + 1+-}++instance Variable IntVar where+ eqVar (IntVar i) (IntVar j) = i == j+ + getVarID (IntVar v) = v+++----------------------------------------------------------------+-- | Binding state for 'IntVar'.+data IntBindingState t = IntBindingState+ { nextFreeVar :: {-# UNPACK #-} !Int+ , varBindings :: IM.IntMap (MutTerm IntVar t)+ }++-- Can't derive this because it's an UndecidableInstance+instance (Show (t (MutTerm IntVar t))) =>+ Show (IntBindingState t)+ where+ show (IntBindingState nr bs) =+ "IntBindingState { nextFreeVar = "++show nr+++ ", varBindings = "++show bs++"}"++-- | The initial @IntBindingState@.+emptyIntBindingState :: IntBindingState t+emptyIntBindingState = IntBindingState minBound IM.empty+++----------------------------------------------------------------+-- | A monad for storing 'IntVar' bindings, implemented as a 'StateT'.+-- For a plain state monad, set @m = Identity@; for a backtracking+-- state monad, set @m = Logic@.+newtype IntBindingT t m a = IBT { unIBT :: StateT (IntBindingState t) m a }++-- For portability reasons, we're intentionally avoiding+-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like.++instance (Functor m) => Functor (IntBindingT t m) where+ fmap f = IBT . fmap f . unIBT++-- BUG: can't reduce dependency to Applicative because of StateT's instance.+instance (Functor m, Monad m) => Applicative (IntBindingT t m) where+ pure = IBT . pure+ x <*> y = IBT (unIBT x <*> unIBT y)+ x *> y = IBT (unIBT x *> unIBT y)+ x <* y = IBT (unIBT x <* unIBT y)++instance (Monad m) => Monad (IntBindingT t m) where+ return = IBT . return+ m >>= f = IBT (unIBT m >>= unIBT . f)++instance MonadTrans (IntBindingT t) where+ lift = IBT . lift++-- BUG: can't reduce dependency to Alternative because of StateT's instance.+instance (Functor m, MonadPlus m) => Alternative (IntBindingT t m) where+ empty = IBT empty+ x <|> y = IBT (unIBT x <|> unIBT y)++instance (MonadPlus m) => MonadPlus (IntBindingT t m) where+ mzero = IBT mzero+ mplus ml mr = IBT (mplus (unIBT ml) (unIBT mr))++instance (Monad m) => MonadState (IntBindingState t) (IntBindingT t m) where+ get = IBT get+ put = IBT . put++-- N.B., we already have (MonadLogic m) => MonadLogic (StateT s m),+-- provided that logict is compiled against the same mtl/monads-fd+-- we're getting StateT from. Otherwise we'll get a bunch of warnings+-- here.+instance (MonadLogic m) => MonadLogic (IntBindingT t m) where+ msplit (IBT m) = IBT (coerce `liftM` msplit m)+ where+ coerce Nothing = Nothing+ coerce (Just (a, m')) = Just (a, IBT m')+ + interleave (IBT l) (IBT r) = IBT (interleave l r)+ + IBT m >>- f = IBT (m >>- (unIBT . f))+ + ifte (IBT b) t (IBT f) = IBT (ifte b (unIBT . t) f)+ + once (IBT m) = IBT (once m)++----------------------------------------------------------------++runIntBindingT :: IntBindingT t m a -> m (a, IntBindingState t)+runIntBindingT (IBT m) = runStateT m emptyIntBindingState+++-- | N.B., you should explicitly apply bindings before calling this+-- function, or else the bindings will be lost+evalIntBindingT :: (Monad m) => IntBindingT t m a -> m a+evalIntBindingT (IBT m) = evalStateT m emptyIntBindingState+++execIntBindingT :: (Monad m) => IntBindingT t m a -> m (IntBindingState t)+execIntBindingT (IBT m) = execStateT m emptyIntBindingState++----------------------------------------------------------------++instance (Unifiable t, Applicative m, Monad m) =>+ BindingMonad IntVar t (IntBindingT t m)+ where+ + lookupVar (IntVar v) = IBT $ gets (IM.lookup v . varBindings)+ + freeVar = IBT $ do+ ibs <- get+ let v = nextFreeVar ibs+ if v == maxBound+ then error "freeVar: no more variables!"+ else do+ put $ ibs { nextFreeVar = v+1 }+ return $ IntVar v+ + newVar t = IBT $ do+ ibs <- get+ let v = nextFreeVar ibs+ if v == maxBound+ then error "newVar: no more variables!"+ else do+ let bs' = IM.insert v t (varBindings ibs)+ put $ ibs { nextFreeVar = v+1, varBindings = bs' }+ return $ IntVar v+ + bindVar (IntVar v) t = IBT $ do+ ibs <- get+ let bs' = IM.insert v t (varBindings ibs)+ put $ ibs { varBindings = bs' }++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Unification/Ranked.hs view
@@ -0,0 +1,177 @@++{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.07.11+-- |+-- Module : Control.Unification.Ranked+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : highly experimental+-- Portability : semi-portable (MPTCs, FlexibleContexts)+--+-- This module provides the API of "Control.Unification" except+-- using 'RankedBindingMonad' where appropriate. This module (and+-- the binding implementations for it) are highly experimental and+-- subject to change in future versions.+----------------------------------------------------------------+module Control.Unification.Ranked+ (+ -- * Data types, classes, etc+ module Control.Unification.Types+ + -- * Operations on one term+ , getFreeVars+ , applyBindings+ , freshen+ -- freezeM -- apply bindings and freeze in one traversal+ -- unskolemize -- convert Skolemized variables to free variables+ -- skolemize -- convert free variables to Skolemized variables+ -- getSkolems -- compute the skolem variables in a term; helpful?+ + -- * Operations on two terms+ -- ** Symbolic names+ , (===)+ , (=~=)+ , (=:=)+ -- (<:=)+ -- ** Textual names+ , equals+ , equiv+ , unify+ -- unifyOccurs+ -- subsumes+ ) where++import Prelude+ hiding (mapM, mapM_, sequence, foldr, foldr1, foldl, foldl1, all, or)++import qualified Data.IntMap as IM+import Data.Traversable+import Control.Applicative+import Control.Monad.Trans (MonadTrans(..))+import Control.Monad.Error (MonadError(..))+import Control.Monad.State (MonadState(..), evalStateT)+import Control.Monad.State.UnificationExtras+import Control.Unification.Types+import Control.Unification hiding (unify, (=:=))+----------------------------------------------------------------+----------------------------------------------------------------++-- | 'unify'+(=:=)+ :: ( RankedBindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> e m (MutTerm v t) -- ^+(=:=) = unify+infix 4 =:=, `unify`+++-- TODO: keep in sync as we verify correctness.+--+-- | 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+-- unification succeeds. However, the returned value makes use of+-- aggressive opportunistic observable sharing, so it will be more+-- efficient to use it in future calculations than either argument.+unify+ :: ( RankedBindingMonad v t m+ , MonadTrans e+ , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m)+ , MonadError (UnificationFailure v t) (e m)+ )+ => MutTerm v t -- ^+ -> MutTerm v t -- ^+ -> e m (MutTerm v t) -- ^+unify =+ \tl tr -> evalStateT (loop tl tr) 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+ + 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+ 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 }+ + (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 }+ + (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 }+ + (Just tl, Just tr) -> do+ t <- localState $ do+ vl `seenAs` tl+ vr `seenAs` tr+ 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 }+ + (MutVar vl, MutTerm _) -> do+ t <- do+ mtl <- lift . lift $ lookupVar vl+ case mtl of+ Nothing -> return tr1+ Just tl -> localState $ do+ vl `seenAs` tl+ loop tl tr1+ lift . lift $ do+ vl `bindVar` t+ return tl1+ + (MutTerm _, MutVar vr) -> do+ t <- do+ mtr <- lift . lift $ lookupVar vr+ case mtr of+ Nothing -> return tl1+ Just tr -> localState $ do+ vr `seenAs` tr+ loop tl1 tr+ lift . lift $ do+ vr `bindVar` t+ return tr1+ + (MutTerm tl, MutTerm tr) ->+ case zipMatch tl tr of+ Nothing -> lift . throwError $ TermMismatch tl tr+ Just tlr -> MutTerm <$> mapM (uncurry loop) tlr++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Unification/Ranked/IntVar.hs view
@@ -0,0 +1,189 @@++{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.07.06+-- |+-- Module : Control.Unification.Ranked.IntVar+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : highly experimental+-- Portability : semi-portable (MPTCs,...)+--+-- A ranked variant of "Control.Unification.IntVar".+----------------------------------------------------------------+module Control.Unification.Ranked.IntVar+ ( IntVar(..)+ , IntRBindingState()+ , IntRBindingT()+ , runIntRBindingT+ , evalIntRBindingT+ , execIntRBindingT+ ) where++import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)++import qualified Data.IntMap as IM+import Control.Applicative+import Control.Monad (MonadPlus(..), liftM)+import Control.Monad.Trans (MonadTrans(..))+import Control.Monad.State (MonadState(..), StateT, runStateT, evalStateT, execStateT, gets)+import Control.Monad.Logic (MonadLogic(..))+import Control.Unification.Types+import Control.Unification.IntVar (IntVar(..))+----------------------------------------------------------------+----------------------------------------------------------------++-- | Ranked binding state for 'IntVar'.+data IntRBindingState t = IntRBindingState+ { nextFreeVar :: {-# UNPACK #-} !Int+ , varBindings :: IM.IntMap (Rank IntVar t)+ }++-- Can't derive this because it's an UndecidableInstance+instance (Show (t (MutTerm IntVar t))) =>+ Show (IntRBindingState t)+ where+ show (IntRBindingState nr bs) =+ "IntRBindingState { nextFreeVar = "++show nr+++ ", varBindings = "++show bs++"}"++-- | The initial @IntRBindingState@.+emptyIntRBindingState :: IntRBindingState t+emptyIntRBindingState = IntRBindingState minBound IM.empty+++----------------------------------------------------------------+-- | A monad for storing 'IntVar' bindings, implemented as a 'StateT'.+-- For a plain state monad, set @m = Identity@; for a backtracking+-- state monad, set @m = Logic@.+newtype IntRBindingT t m a = IRBT { unIRBT :: StateT (IntRBindingState t) m a }++-- For portability reasons, we're intentionally avoiding+-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like.++instance (Functor m) => Functor (IntRBindingT t m) where+ fmap f = IRBT . fmap f . unIRBT++-- BUG: can't reduce dependency to Applicative because of StateT's instance.+instance (Functor m, Monad m) => Applicative (IntRBindingT t m) where+ pure = IRBT . pure+ x <*> y = IRBT (unIRBT x <*> unIRBT y)+ x *> y = IRBT (unIRBT x *> unIRBT y)+ x <* y = IRBT (unIRBT x <* unIRBT y)++instance (Monad m) => Monad (IntRBindingT t m) where+ return = IRBT . return+ m >>= f = IRBT (unIRBT m >>= unIRBT . f)++instance MonadTrans (IntRBindingT t) where+ lift = IRBT . lift++-- BUG: can't reduce dependency to Alternative because of StateT's instance.+instance (Functor m, MonadPlus m) => Alternative (IntRBindingT t m) where+ empty = IRBT empty+ x <|> y = IRBT (unIRBT x <|> unIRBT y)++instance (MonadPlus m) => MonadPlus (IntRBindingT t m) where+ mzero = IRBT mzero+ mplus ml mr = IRBT (mplus (unIRBT ml) (unIRBT mr))++instance (Monad m) => MonadState (IntRBindingState t) (IntRBindingT t m) where+ get = IRBT get+ put = IRBT . put++-- N.B., we already have (MonadLogic m) => MonadLogic (StateT s m),+-- provided that logict is compiled against the same mtl/monads-fd+-- we're getting StateT from. Otherwise we'll get a bunch of warnings+-- here.+instance (MonadLogic m) => MonadLogic (IntRBindingT t m) where+ msplit (IRBT m) = IRBT (coerce `liftM` msplit m)+ where+ coerce Nothing = Nothing+ coerce (Just (a, m')) = Just (a, IRBT m')+ + interleave (IRBT l) (IRBT r) = IRBT (interleave l r)+ + IRBT m >>- f = IRBT (m >>- (unIRBT . f))+ + ifte (IRBT b) t (IRBT f) = IRBT (ifte b (unIRBT . t) f)+ + once (IRBT m) = IRBT (once m)++----------------------------------------------------------------++runIntRBindingT :: IntRBindingT t m a -> m (a, IntRBindingState t)+runIntRBindingT (IRBT m) = runStateT m emptyIntRBindingState+++-- | N.B., you should explicitly apply bindings before calling this+-- function, or else the bindings will be lost+evalIntRBindingT :: (Monad m) => IntRBindingT t m a -> m a+evalIntRBindingT (IRBT m) = evalStateT m emptyIntRBindingState+++execIntRBindingT :: (Monad m) => IntRBindingT t m a -> m (IntRBindingState t)+execIntRBindingT (IRBT m) = execStateT m emptyIntRBindingState++----------------------------------------------------------------++instance (Unifiable t, Applicative m, Monad m) =>+ BindingMonad IntVar t (IntRBindingT t m)+ where+ + lookupVar (IntVar v) = IRBT $ do+ mb <- gets (IM.lookup v . varBindings)+ case mb of+ Nothing -> return Nothing+ Just (Rank _ mb') -> return mb'+ + freeVar = IRBT $ do+ ibs <- get+ let v = nextFreeVar ibs+ if v == maxBound+ then error "freeVar: no more variables!"+ else do+ put $ ibs { nextFreeVar = v+1 }+ return $ IntVar v+ + newVar t = IRBT $ do+ ibs <- get+ let v = nextFreeVar ibs+ if v == maxBound+ then error "newVar: no more variables!"+ else do+ let bs' = IM.insert v (Rank 0 (Just t)) (varBindings ibs)+ put $ ibs { nextFreeVar = v+1, varBindings = bs' }+ return $ IntVar v+ + bindVar (IntVar v) t = IRBT $ do+ ibs <- get+ let bs' = IM.insertWith f v (Rank 0 (Just t)) (varBindings ibs)+ f (Rank _0 jt) (Rank r _) = Rank r jt+ put $ ibs { varBindings = bs' }+ + +instance (Unifiable t, Applicative m, Monad m) =>+ RankedBindingMonad IntVar t (IntRBindingT t m)+ where+ lookupRankVar (IntVar v) = IRBT $ do+ mb <- gets (IM.lookup v . varBindings)+ case mb of+ Nothing -> return (Rank 0 Nothing)+ Just rk -> return rk+ + incrementRank (IntVar v) = IRBT $ do+ ibs <- get+ let bs' = IM.insertWith f v (Rank 1 Nothing) (varBindings ibs)+ f (Rank _1 _n) (Rank r mb) = Rank (r+1) mb+ put $ ibs { varBindings = bs' }+ + incrementBindVar (IntVar v) t = IRBT $ do+ ibs <- get+ let bs' = IM.insertWith f v (Rank 1 (Just t)) (varBindings ibs)+ f (Rank _1 jt) (Rank r _) = Rank (r+1) jt+ put $ ibs { varBindings = bs' }++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Unification/Ranked/STVar.hs view
@@ -0,0 +1,146 @@++{-# LANGUAGE Rank2Types+ , MultiParamTypeClasses+ , UndecidableInstances+ , FlexibleInstances+ #-}++{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.07.06+-- |+-- Module : Control.Unification.Ranked.STVar+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : highly experimental+-- Portability : semi-portable (Rank2Types, MPTCs,...)+--+-- A ranked variant of "Control.Unification.STVar".+----------------------------------------------------------------+module Control.Unification.Ranked.STVar+ ( STRVar()+ , STRBinding()+ , runSTRBinding+ ) where++import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)++import Data.STRef+import Data.Word (Word8)+import Control.Applicative (Applicative(..))+import Control.Monad (ap)+import Control.Monad.Trans (lift)+import Control.Monad.ST+import Control.Monad.Reader (ReaderT, runReaderT, ask)+import Control.Unification.Types+----------------------------------------------------------------+----------------------------------------------------------------++-- | A ranked unification variable implemented by 'STRef's. In+-- addition to the @STRef@ for the term itself, we also track the+-- variable's ID (to support visited-sets) and rank (to support+-- weighted path compression).+data STRVar s t a =+ STRVar+ {-# UNPACK #-} !Int+ {-# UNPACK #-} !(STRef s Word8)+ {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STRVar s t) t)))+-- BUG: can we actually unpack STRef?+-- BUG: we need a phantom @a@ to get the kinds to work out now...++instance Show (STRVar s t a) where+ show (STRVar i _ _) = "STRVar " ++ show i++instance Variable (STRVar s t) where+ eqVar (STRVar i _ _) (STRVar j _ _) = i == j+ + getVarID (STRVar i _ _) = i+++----------------------------------------------------------------+-- TODO: parameterize this so we can use BacktrackST too. Or course,+-- that means defining another class for STRef-like variables+--+-- TODO: parameterize this so we can share the implementation for STVar and STRVar+--+-- TODO: does MTL still have the overhead that'd make it worthwhile+-- to do this manually instead of using ReaderT?+--+-- | A monad for handling 'STRVar' bindings.+newtype STRBinding s a = STRB { unSTRB :: ReaderT (STRef s Int) (ST s) a }+++-- | Run the 'ST' ranked binding monad. N.B., because 'STRVar' are+-- rank-2 quantified, this guarantees that the return value has no+-- such references. However, in order to remove the references from+-- terms, you'll need to explicitly apply the bindings.+runSTRBinding :: (forall s. STRBinding s a) -> a+runSTRBinding stb =+ runST (newSTRef minBound >>= runReaderT (unSTRB stb))+++-- For portability reasons, we're intentionally avoiding+-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like.++instance Functor (STRBinding s) where+ fmap f = STRB . fmap f . unSTRB++instance Applicative (STRBinding s) where+ pure = return+ (<*>) = ap+ (*>) = (>>)+ x <* y = x >>= \a -> y >> return a++instance Monad (STRBinding s) where+ return = STRB . return+ stb >>= f = STRB (unSTRB stb >>= unSTRB . f)+++----------------------------------------------------------------++_newSTRVar+ :: String+ -> Maybe (MutTerm (STRVar s t) t)+ -> STRBinding s (STRVar s t (MutTerm (STRVar s t) t))+_newSTRVar fun mb = STRB $ do+ nr <- ask+ lift $ do+ n <- readSTRef nr+ if n == maxBound+ then error $ fun ++ ": no more variables!"+ else do+ writeSTRef nr $! n+1+ -- BUG: no applicative ST+ rk <- newSTRef 0+ ptr <- newSTRef mb+ return (STRVar n rk ptr)+++instance (Unifiable t) => BindingMonad (STRVar s t) t (STRBinding s) where+ lookupVar (STRVar _ _ p) = STRB . lift $ readSTRef p+ + freeVar = _newSTRVar "freeVar" Nothing+ + newVar t = _newSTRVar "newVar" (Just t)+ + bindVar (STRVar _ _ p) t = STRB . lift $ writeSTRef p (Just t)+++instance (Unifiable t) =>+ RankedBindingMonad (STRVar s t) t (STRBinding s)+ where+ + lookupRankVar (STRVar _ r p) = STRB . lift $ do+ n <- readSTRef r+ mb <- readSTRef p+ return (Rank n mb)+ + incrementRank (STRVar _ r _) = STRB . lift $ do+ n <- readSTRef r+ writeSTRef r $! n+1+ + -- incrementBindVar = default++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Unification/STVar.hs view
@@ -0,0 +1,125 @@++{-# LANGUAGE Rank2Types+ , MultiParamTypeClasses+ , UndecidableInstances+ , FlexibleInstances+ #-}++{-# OPTIONS_GHC -Wall -fwarn-tabs #-}+----------------------------------------------------------------+-- ~ 2011.07.06+-- |+-- Module : Control.Unification.STVar+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : experimental+-- Portability : semi-portable (Rank2Types, MPTCs,...)+--+-- This module defines an implementation of unification variables+-- using the 'ST' monad.+----------------------------------------------------------------+module Control.Unification.STVar+ ( STVar()+ , STBinding()+ , runSTBinding+ ) where++import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)++import Data.STRef+import Control.Applicative (Applicative(..), (<$>))+import Control.Monad (ap)+import Control.Monad.Trans (lift)+import Control.Monad.ST+import Control.Monad.Reader (ReaderT, runReaderT, ask)+import Control.Unification.Types+----------------------------------------------------------------+----------------------------------------------------------------++-- | Unification variables implemented by 'STRef's. In addition to+-- the @STRef@ for the term itself, we also track the variable's+-- ID (to support visited-sets).+data STVar s a =+ STVar+ {-# UNPACK #-} !Int+ {-# UNPACK #-} !(STRef s (Maybe a))+-- BUG: can we actually unpack STRef?++instance Show (STVar s a) where+ show (STVar i _) = "STVar " ++ show i++instance Variable (STVar s) where+ eqVar (STVar i _) (STVar j _) = i == j+ + getVarID (STVar i _) = i+++----------------------------------------------------------------+-- TODO: parameterize this so we can use BacktrackST too. Or course,+-- that means defining another class for STRef-like variables+--+-- TODO: parameterize this so we can share the implementation for STVar and STRVar+--+-- TODO: does MTL still have the overhead that'd make it worthwhile+-- to do this manually instead of using ReaderT?+--+-- | A monad for handling 'STVar' bindings.+newtype STBinding s a = STB { unSTB :: ReaderT (STRef s Int) (ST s) a }+++-- | Run the 'ST' ranked binding monad. N.B., because 'STVar' are+-- rank-2 quantified, this guarantees that the return value has no+-- such references. However, in order to remove the references from+-- terms, you'll need to explicitly apply the bindings and ground+-- the term.+runSTBinding :: (forall s. STBinding s a) -> a+runSTBinding stb =+ runST (newSTRef minBound >>= runReaderT (unSTB stb))+++-- For portability reasons, we're intentionally avoiding+-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like.++instance Functor (STBinding s) where+ fmap f = STB . fmap f . unSTB++instance Applicative (STBinding s) where+ pure = return+ (<*>) = ap+ (*>) = (>>)+ x <* y = x >>= \a -> y >> return a++instance Monad (STBinding s) where+ return = STB . return+ stb >>= f = STB (unSTB stb >>= unSTB . f)+++----------------------------------------------------------------++_newSTVar+ :: String+ -> Maybe (MutTerm (STVar s) t)+ -> STBinding s (STVar s (MutTerm (STVar s) t))+_newSTVar fun mb = STB $ do+ nr <- ask+ lift $ do+ n <- readSTRef nr+ if n == maxBound+ then error $ fun ++ ": no more variables!"+ else do+ writeSTRef nr $! n+1+ STVar n <$> newSTRef mb++instance (Unifiable t) => BindingMonad (STVar s) t (STBinding s) where++ lookupVar (STVar _ p) = STB . lift $ readSTRef p+ + freeVar = _newSTVar "freeVar" Nothing+ + newVar t = _newSTVar "newVar" (Just t)+ + bindVar (STVar _ p) t = STB . lift $ writeSTRef p (Just t)++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Control/Unification/Types.hs view
@@ -0,0 +1,256 @@+-- Required for Show instances+{-# LANGUAGE FlexibleContexts, UndecidableInstances #-}+-- Required more generally+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}++{-# OPTIONS_GHC -Wall -fwarn-tabs #-}++----------------------------------------------------------------+-- ~ 2011.07.11+-- |+-- Module : Control.Unification.Types+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : experimental+-- Portability : semi-portable (MPTCs, fundeps,...)+--+-- This module defines the classes and primitive types used by+-- unification and related functions.+----------------------------------------------------------------+module Control.Unification.Types+ (+ -- * Mutable terms+ MutTerm(..)+ , freeze+ , unfreeze+ -- * Errors+ , UnificationFailure(..)+ -- * Basic type classes+ , Unifiable(..)+ , Variable(..)+ , BindingMonad(..)+ -- * Weighted path compression+ , Rank(..)+ , RankedBindingMonad(..)+ ) where++import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)++import Data.Word (Word8)+import Data.Functor.Fixedpoint (Fix(..))+import Data.Traversable (Traversable(..))+import Control.Applicative (Applicative(..), (<$>))+import Control.Monad.Error (Error(..))+----------------------------------------------------------------+----------------------------------------------------------------++-- | 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 v t))+ | MutTerm !(t (MutTerm v t))+++instance (Show (v (MutTerm v t)), Show (t (MutTerm v t))) =>+ Show (MutTerm v t)+ where+ showsPrec p (MutVar v) = showsPrec p v+ showsPrec p (MutTerm t) = showsPrec p t+++-- | /O(n)/. Embed a pure term as a mutable term.+unfreeze :: (Functor t) => Fix t -> MutTerm v t+unfreeze = MutTerm . 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+++----------------------------------------------------------------+-- TODO: provide zipper context so better error messages can be generated.+--+-- | The possible failure modes that could be encountered in+-- unification and related functions. While many of the functions+-- 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+ + = OccursIn (v (MutTerm v t)) (MutTerm v t)+ -- ^ 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 (MutTerm v t)) (t (MutTerm v t))+ -- ^ 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.+ + | UnknownError String+ -- ^ 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 (MutTerm v t))) =>+ Show (UnificationFailure v t)+ 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++instance Error (UnificationFailure v t) where+ noMsg = UnknownError ""+ strMsg = UnknownError++----------------------------------------------------------------++-- | An implementation of syntactically unifiable structure. The+-- @Traversable@ constraint is there because we also require terms+-- to be functors and require the distributivity of 'sequence' or+-- 'mapM'.+class (Traversable t) => Unifiable t where+ + -- | 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))+++-- | An implementation of unification variables. Note that we do+-- not require variables to be functors. Thus, it does not matter+-- whether you give them vacuous functor instances, or use clever+-- tricks like @CoYoneda STRef@ to give them real functor instances.+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 a -> v b -> Bool+ eqVar x y = getVarID x == getVarID y+ + -- | Return a unique identifier for this variable, in order to+ -- support the use of visited-sets instead of occurs-checks.+ getVarID :: v a -> Int+++----------------------------------------------------------------++-- | The basic class for generating, reading, and writing to bindings+-- stored in a monad. These three functionalities could be split+-- apart, but are combined in order to simplify contexts. Also,+-- because most functions reading bindings will also perform path+-- compression, there's no way to distinguish \"true\" mutation+-- from mere path compression.+--+-- The superclass constraints are there to simplify contexts, since+-- 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+ where+ + -- | Given a variable pointing to @MutTerm v t@, return the+ -- term it's bound to, or @Nothing@ if the variable is unbound.+ lookupVar :: v (MutTerm v t) -> m (Maybe (MutTerm v t))+ + + -- | Generate a new free variable guaranteed to be fresh in+ -- @m@.+ freeVar :: m (v (MutTerm v t))+ + + -- | Generate a new variable (fresh in @m@) bound to the given+ -- term. The default implementation is:+ --+ -- > newVar t = do { v <- freeVar ; bindVar v t ; return v }+ newVar :: MutTerm v t -> m (v (MutTerm v t))+ 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) -> MutTerm v t -> m ()+++----------------------------------------------------------------+-- | The target of variables for 'RankedBindingMonad's. In order+-- to support weighted path compression, each variable is bound to+-- both another term (possibly) and also a \"rank\" which is related+-- to the length of the variable chain to the term it's ultimately+-- bound to.+--+-- The rank can be at most @log V@, where @V@ is the total number+-- 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))++-- Can't derive this because it's an UndecidableInstance+instance (Show (v (MutTerm v t)), Show (t (MutTerm v t))) =>+ Show (Rank v t)+ 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)?++{-+instance Monoid (Rank v t) where+ mempty = Rank 0 Nothing+ mappend (Rank l mb) (Rank r _) = Rank (max l r) mb+-}+++-- | An advanced class for 'BindingMonad's which also support+-- weighted path compression. The weightedness adds non-trivial+-- implementation complications; so even though weighted path+-- 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+ -- rank and the term it's bound to.+ lookupRankVar :: v (MutTerm v t) -> m (Rank v t)+ + -- | Increase the rank of a variable by one.+ incrementRank :: v (MutTerm v t) -> m ()+ + -- | 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) -> MutTerm v t -> m ()+ incrementBindVar v t = do { incrementRank v ; bindVar v t }++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ src/Data/Functor/Fixedpoint.hs view
@@ -0,0 +1,305 @@++-- For the Show (Fix f) instance+{-# LANGUAGE UndecidableInstances #-}+-- For 'build' and 'hmap'+{-# LANGUAGE Rank2Types #-}+-- To parse rules. The language extension is for hackery in rules.+{-# OPTIONS_GHC -O2 -fglasgow-exts #-}++{-# OPTIONS_GHC -Wall -fwarn-tabs #-}++----------------------------------------------------------------+-- 2011.07.11+-- |+-- Module : Data.Functor.Fixedpoint+-- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- License : BSD+-- Maintainer : wren@community.haskell.org+-- Stability : provisional+-- Portability : semi-portable (Rank2Types)+--+-- This module provides a fixed point operator on functor types.+-- For Haskell the least and greatest fixed points coincide, so we+-- needn't distinguish them. This abstract nonsense is helpful in+-- conjunction with other category theoretic tricks like Swierstra's+-- functor coproducts (not provided by this package). For more on+-- the utility of two-level recursive types, see:+--+-- * Tim Sheard (2001) /Generic Unification via Two-Level Types/+-- /and Paramterized Modules/, Functional Pearl, ICFP.+--+-- * Tim Sheard & Emir Pasalic (2004) /Two-Level Types and/+-- /Parameterized Modules/. JFP 14(5): 547--587. This is+-- an expanded version of Sheard (2001) with new examples.+--+-- * Wouter Swierstra (2008) /Data types a la carte/, Functional+-- Pearl. JFP 18: 423--436.+----------------------------------------------------------------++module Data.Functor.Fixedpoint+ (+ -- * Fixed point operator for functors+ Fix(..)+ -- * Maps+ , hmap, hmapM+ , ymap, ymapM+ -- * Builders+ , build+ -- * Catamorphisms+ , cata, cataM+ , ycata, ycataM+ -- * Anamorphisms+ , ana, anaM+ -- * Hylomorphisms+ , hylo, hyloM+ ) where++import Prelude hiding (mapM, sequence)+import Control.Monad hiding (mapM, sequence)+import Data.Traversable++----------------------------------------------------------------+----------------------------------------------------------------++-- | @Fix f@ is a fix point of the 'Functor' @f@. Note that in+-- Haskell the least and greatest fixed points coincide, so we don't+-- need to distinguish between @Mu f@ and @Nu f@. This type used+-- to be called @Y@, hence the naming convention for all the @yfoo@+-- functions.+--+-- This type lets us invoke category theory to get recursive types+-- and operations over them without the type checker complaining+-- about infinite types. The 'Show' instance doesn't print the+-- constructors, for legibility.+newtype Fix f = Fix { unFix :: f (Fix f) }++-- This requires UndecidableInstances because the context is larger+-- 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++instance (Eq (f (Fix f))) => Eq (Fix f) where+ Fix x == Fix y = x == y+ Fix x /= Fix y = x /= y++instance (Ord (f (Fix f))) => Ord (Fix f) where+ Fix x `compare` Fix y = x `compare` y+ Fix x > Fix y = x > y+ Fix x >= Fix y = x >= y+ Fix x <= Fix y = x <= y+ Fix x < Fix y = x < y+ Fix x `max` Fix y = Fix (max x y)+ Fix x `min` Fix y = Fix (min x y)++----------------------------------------------------------------++-- | A higher-order map taking a natural transformation @(f -> g)@+-- and lifting it to operate on @Fix@.+hmap :: (Functor f, Functor g) => (forall a. f a -> g a) -> Fix f -> Fix g+hmap eps = ana (eps . unFix)+ -- == cata (Fix . eps) -- But the anamorphism is a better producer.+{-# INLINE [0] hmap #-}++{-# RULES+"hmap id"+ hmap id = id++"hmap-compose"+ forall (eps :: forall a. g a -> h a) (eta :: forall a. f a -> g a).+ hmap eps . hmap eta = hmap (eps . eta)+ #-}+++-- | A monadic variant of 'hmap'.+hmapM+ :: (Functor f, Traversable g, Monad m)+ => (forall a. f a -> m (g a)) -> Fix f -> m (Fix g)+hmapM eps = anaM (eps . unFix)+{-# INLINE [0] hmapM #-}++{-# RULES+"hmapM return" hmapM return = return+-- "hmapM-compose" forall eps eta. hmap eps <=< hmap eta = hmapM (eps <=< eta)+ #-}+++-- | A version of 'fmap' for endomorphisms on the fixed point. That+-- is, this maps the function over the first layer of recursive+-- structure.+ymap :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f+ymap f = Fix . fmap f . unFix+{-# INLINE [0] ymap #-}++{-# RULES+"ymap id" ymap id = id+"ymap-compose" forall f g. ymap f . ymap g = ymap (f . g)+ #-}+++-- | A monadic variant of 'ymap'.+ymapM :: (Traversable f, Monad m) => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)+ymapM f = liftM Fix . mapM f . unFix+{-# INLINE ymapM #-}++{-# RULES+"ymapM id" ymapM return = return+-- "ymapM-compose" forall f g. ymapM f <=< ymapM g = ymapM (f <=< g)+ #-}+++----------------------------------------------------------------+-- BUG: this isn't as helful as normal build\/fold fusion as in Data.Functor.Fusable+--+-- | Take a Church encoding of a fixed point into the data+-- representation of the fixed point.+build :: (Functor f) => (forall r. (f r -> r) -> r) -> Fix f+build g = g Fix+{-# INLINE [0] build #-}++-- N.B., the signature is required on @g@ in order to be Rank-2.+-- The signature is required on @phi@ in order to bring @f@ into+-- scope. Otherwise we'd need -XScopedTypeVariables.+{-# RULES+"build/cata" [1]+ forall (phi :: f a -> a) (g :: forall r. (f r -> r) -> r).+ cata phi (build g) = g phi+ #-}++----------------------------------------------------------------+-- | A pure catamorphism over the least fixed point of a functor.+-- This function applies the @f@-algebra from the bottom up over+-- @Fix f@ to create some residual value.+cata :: (Functor f) => (f a -> a) -> (Fix f -> a)+cata phi = self+ where+ self = phi . fmap self . unFix+{-# INLINE [0] cata #-}++{-# RULES+"cata-refl"+ cata Fix = id++-- TODO: do we still need eta-expanded variants of rules?+"cata-compose"+ forall (eps :: forall a. f a -> g a) phi.+ cata phi . cata (Fix . eps) = cata (phi . eps)+ #-}++-- We can't really use this one because of the implication constraint+{- RULES+"cata-fusion"+ forall f phi. (f . phi) == (phi . fmap f) ==>+ f . cata phi = cata phi+-}+++-- | A catamorphism for monadic @f@-algebras. Alas, this isn't wholly+-- generic to @Functor@ since it requires distribution of @f@ over+-- @m@ (provided by 'sequence' or 'mapM' in 'Traversable').+--+-- N.B., this orders the side effects from the bottom up.+cataM :: (Traversable f, Monad m) => (f a -> m a) -> (Fix f -> m a)+cataM phiM = self+ where+ self = phiM <=< (mapM self . unFix)+{-# INLINE cataM #-}++-- TODO: other rules for cataM+{-# RULES+"cataM-refl"+ cataM (return . Fix) = return+ #-}+++-- TODO: remove this, or add similar versions for ana* and hylo*?+-- | A variant of 'cata' which restricts the return type to being+-- a new fixpoint. Though more restrictive, it can be helpful when+-- you already have an algebra which expects the outermost @Fix@.+--+-- If you don't like either @fmap@ or @cata@, then maybe this is+-- what you were thinking?+ycata :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f+ycata f = cata (f . Fix)+{-# INLINE ycata #-}+++-- TODO: remove this, or add similar versions for ana* and hylo*?+-- | Monadic variant of 'ycata'.+ycataM :: (Traversable f, Monad m)+ => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)+ycataM f = cataM (f . Fix)+{-# INLINE ycataM #-}+++----------------------------------------------------------------+-- | A pure anamorphism generating the greatest fixed point of a+-- functor. This function applies an @f@-coalgebra from the top+-- down to expand a seed into a @Fix f@.+ana :: (Functor f) => (a -> f a) -> (a -> Fix f)+ana psi = self+ where+ self = Fix . fmap self . psi+{-# INLINE [0] ana #-}+++{-# RULES+"ana-refl"+ ana unFix = id++-- BUG: I think I dualized this right...+"ana-compose"+ forall (eps :: forall a. f a -> g a) psi.+ ana (eps . unFix) . ana psi = ana (eps . psi)+ #-}++-- We can't really use this because of the implication constraint+{- RULES+-- BUG: I think I dualized this right...+"ana-fusion"+ forall f psi. (psi . f) == (fmap f . psi) ==>+ ana psi . f = ana psi+-}+++-- | An anamorphism for monadic @f@-coalgebras. Alas, this isn't+-- wholly generic to @Functor@ since it requires distribution of+-- @f@ over @m@ (provided by 'sequence' or 'mapM' in 'Traversable').+--+-- N.B., this orders the side effects from the top down.+anaM :: (Traversable f, Monad m) => (a -> m (f a)) -> (a -> m (Fix f))+anaM psiM = self+ where+ self = (liftM Fix . mapM self) <=< psiM+{-# INLINE anaM #-}+++----------------------------------------------------------------+-- Is this even worth mentioning? We can amortize the construction+-- of @Fix f@ (which we'd do anyways because of laziness), but we+-- can't fuse the @f@ away unless we inline all of @psi@, @fmap@,+-- and @phi@ at the use sites. Will inlining this definition be+-- sufficient to do that?++-- | @hylo phi psi == cata phi . ana psi@+hylo :: (Functor f) => (f b -> b) -> (a -> f a) -> (a -> b)+hylo phi psi = self+ where+ self = phi . fmap self . psi+{-# INLINE hylo #-}++-- TODO: rules for hylo?+++-- | @hyloM phiM psiM == cataM phiM <=< anaM psiM@+hyloM :: (Traversable f, Monad m)+ => (f b -> m b) -> (a -> m (f a)) -> (a -> m b)+hyloM phiM psiM = self+ where+ self = phiM <=< mapM self <=< psiM+{-# INLINE hyloM #-}++-- TODO: rules for hyloM?++----------------------------------------------------------------+----------------------------------------------------------- fin.
+ unification-fd.cabal view
@@ -0,0 +1,75 @@+----------------------------------------------------------------+-- wren ng thornton <wren@community.haskell.org> ~ 2011.07.11+----------------------------------------------------------------++Name: unification-fd+Version: 0.5.0+-- By and large Cabal >=1.2 is fine; but >= 1.6 gives tested-with:+-- and source-repository:.+Cabal-Version: >= 1.6+Build-Type: Simple+Stability: experimental+Copyright: Copyright (c) 2007--2011 wren ng thornton+License: BSD3+License-File: LICENSE+Author: wren ng thornton+Maintainer: wren@community.haskell.org+Homepage: http://code.haskell.org/~wren/+Category: Algebra, Algorithms, Compilers/Interpreters, Language, Logic, Unification+Synopsis: Simple generic unification algorithms.+Description: Simple generic unification algorithms.++Source-Repository head+ Type: darcs+ Location: http://community.haskell.org/~wren/unification-fd++----------------------------------------------------------------+Flag base4+ Default: True+ Description: base-4.0 emits "Prelude deprecated" messages in+ order to get people to be explicit about which+ version of base they use.++Flag splitBase+ Default: True+ Description: base-3.0 (GHC 6.8) broke out the packages: array,+ bytestring, containers, directory, old-locale,+ old-time, packedstring, pretty, process, random.++----------------------------------------------------------------+Library+ Hs-Source-Dirs: src+ Exposed-Modules: Data.Functor.Fixedpoint+ , Control.Monad.State.UnificationExtras+ , Control.Monad.MaybeK+ , Control.Monad.EitherK+ , Control.Unification+ , Control.Unification.Types+ , Control.Unification.STVar+ , Control.Unification.IntVar+ , Control.Unification.Ranked+ , Control.Unification.Ranked.STVar+ , Control.Unification.Ranked.IntVar+ + Build-Depends: logict >= 0.4+ -- Require a version of base with Applicative.+ -- We refuse to do without it any longer.+ , base >= 2.0+ -- Require mtl-2 instead of monads-fd; because+ -- otherwise we get a clash mixing logict with+ -- StateT. And we want stuff from monads-fd, so+ -- we can't just fail over to the older mtl.+ , mtl >= 2.0+ + if flag(base4)+ Build-Depends: base >= 4 && < 5+ else+ Build-Depends: base < 4+ + if flag(splitBase)+ Build-depends: base >= 3.0, containers+ else+ Build-depends: base < 3.0++----------------------------------------------------------------+----------------------------------------------------------- fin.