compdata 0.5.3 → 0.6

raw patch · 23 files changed

+582/−188 lines, 23 filesdep +HUnitdep +test-framework-hunitPVP ok

version bump matches the API change (PVP)

Dependencies added: HUnit, test-framework-hunit

API changes (from Hackage documentation)

Files

• compdata.cabal +7/−3
• src/Data/Comp/Automata.hs +7/−10
• src/Data/Comp/Matching.hs +3/−2
• src/Data/Comp/Multi/Equality.hs +3/−3
• src/Data/Comp/Multi/Generic.hs +10/−10
• src/Data/Comp/Multi/HFoldable.hs +2/−2
• src/Data/Comp/Multi/HFunctor.hs +4/−1
• src/Data/Comp/Multi/Number.hs +50/−0
• src/Data/Comp/Multi/Ordering.hs +2/−2
• src/Data/Comp/Multi/Show.hs +1/−1
• src/Data/Comp/Multi/Variables.hs +113/−57
• src/Data/Comp/MultiParam/HDifunctor.hs +1/−0
• src/Data/Comp/Param/Term.hs +9/−1
• src/Data/Comp/Unification.hs +7/−5
• src/Data/Comp/Variables.hs +82/−48
• testsuite/tests/Data/Comp/Examples/Comp.hs +10/−10
• testsuite/tests/Data/Comp/Examples/Multi.hs +12/−12
• testsuite/tests/Data/Comp/Examples/MultiParam.hs +4/−4
• testsuite/tests/Data/Comp/Examples/Param.hs +6/−6
• testsuite/tests/Data/Comp/Multi/Variables_Test.hs +119/−0
• testsuite/tests/Data/Comp/Multi_Test.hs +18/−0
• testsuite/tests/Data/Comp/Variables_Test.hs +106/−0
• testsuite/tests/Data/Comp_Test.hs +6/−11

@@ -1,5 +1,5 @@ Name:			compdata-Version:		0.5.3+Version:		0.6 Synopsis:            	Compositional Data Types Description: @@ -98,6 +98,9 @@   testsuite/tests/Data_Test.hs,   testsuite/tests/Data/Comp_Test.hs,   testsuite/tests/Data/Comp/Equality_Test.hs,+  testsuite/tests/Data/Comp/Variables_Test.hs,+  testsuite/tests/Data/Comp/Multi_Test.hs,+  testsuite/tests/Data/Comp/Multi/Variables_Test.hs,   testsuite/tests/Data/Comp/Examples_Test.hs,   testsuite/tests/Data/Comp/Examples/Comp.hs,   testsuite/tests/Data/Comp/Examples/Multi.hs,@@ -171,6 +174,7 @@                         Data.Comp.Automata.Product,                         Data.Comp.Number,                         Data.Comp.Thunk,+                        Data.Comp.Ops,                          Data.Comp.Multi,                         Data.Comp.Multi.Term,@@ -185,7 +189,7 @@                         Data.Comp.Multi.Ordering,                         Data.Comp.Multi.Variables,                         Data.Comp.Multi.Ops,-                        Data.Comp.Ops,+                        Data.Comp.Multi.Number,                         Data.Comp.Multi.Derive                         Data.Comp.Multi.Generic,                         Data.Comp.Multi.Desugar,@@ -281,7 +285,7 @@   Type:                 exitcode-stdio-1.0   Main-is:		Data_Test.hs   hs-source-dirs:	src testsuite/tests examples-  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, test-framework, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers+  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers  Executable benchmark   Main-is:		Benchmark.hs

@@ -26,6 +26,7 @@       QHom     , below     , above+    , pureHom     -- ** Bottom-Up State Propagation     , upTrans     , runUpHom@@ -141,17 +142,13 @@                             type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a --- -- | This type represents (pure, i.e. stateless) homomorphism by--- -- universally quantifying over the state type.--- type PHom f g = forall q . QHom f q g --- -- | This combinator runs a stateless homomorphism. (use--- -- 'Data.Comp.Algebra.appHom' instead).--- runPHom :: forall f g . (Functor f, Functor g) => PHom f g -> CxtFun f g--- runPHom hom = run where---     run :: CxtFun f g---     run (Hole x) = Hole x---     run (Term t) = appCxt (explicit () (const ()) hom (fmap run t))+-- | This function turns a stateful homomorphism with a fully+-- polymorphic state type into a (stateless) homomorphism.+pureHom :: (forall q . QHom f q g) -> Hom f g+pureHom phom t = let ?above = undefined +                     ?below = const undefined+                 in phom t  -- | This type represents transition functions of deterministic -- bottom-up tree transducers (DUTTs).

@@ -24,9 +24,10 @@ import Data.Comp.Variables import qualified Data.Map as Map import Data.Map (Map)+import Data.Traversable import Data.Foldable -import Prelude hiding (mapM_, all)+import Prelude hiding (mapM_, mapM, all)  {-| This is an auxiliary function for implementing 'matchCxt'. It behaves similarly as 'match' but is oblivious to non-linearity. Therefore, the@@ -70,7 +71,7 @@ {-| This function is similar to 'matchCxt' but instead of a context it matches a term with variables against a context.  -} -matchTerm :: (Ord v, EqF f, Eq (Cxt h f a) , Functor f, Foldable f, HasVars f v)+matchTerm :: (Ord v, EqF f, Eq (Cxt h f a) , Traversable f, HasVars f v)           => Term f -> Cxt h f a -> Maybe (CxtSubst h a f v) matchTerm t = matchCxt (varsToHoles t) 

@@ -37,8 +37,8 @@ instance Eq a => KEq (K a) where     keq (K x) (K y) = x == y -instance KEq a => Eq (A a) where-     A x == A y = x `keq`  y+instance KEq a => Eq (E a) where+     E x == E y = x `keq`  y  {-|   'EqF' is propagated through sums.@@ -69,7 +69,7 @@ consisting of corresponding components of the two functorial values. -} -heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)]+heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(E a, E b)] heqMod s t     | unit s `eqHF` unit' t = Just args     | otherwise = Nothing

@@ -30,19 +30,19 @@  -- | This function returns a list of all subterms of the given -- term. This function is similar to Uniplate's @universe@ function.-subterms :: forall f  . HFoldable f => Term f  :=> [A (Term f)]+subterms :: forall f  . HFoldable f => Term f  :=> [E (Term f)] subterms t = build (f t)-    where f :: Term f :=> (A (Term f) -> b -> b) -> b -> b-          f t cons nil = A t `cons` hfoldl (\u s -> f s cons u) nil (unTerm t)+    where f :: Term f :=> (E (Term f) -> b -> b) -> b -> b+          f t cons nil = E t `cons` hfoldl (\u s -> f s cons u) nil (unTerm t)  -- | This function returns a list of all subterms of the given term -- that are constructed from a particular functor.-subterms' :: forall f g . (HFoldable f, g :<: f) => Term f :=> [A (g (Term f))]+subterms' :: forall f g . (HFoldable f, g :<: f) => Term f :=> [E (g (Term f))] subterms' (Term t) = build (f t)-    where f :: f (Term f) :=> (A (g (Term f)) -> b -> b) -> b -> b+    where f :: f (Term f) :=> (E (g (Term f)) -> b -> b) -> b -> b           f t cons nil = let rest = hfoldl (\u (Term s) -> f s cons u) nil t                          in case proj t of-                              Just t' -> A t' `cons` rest+                              Just t' -> E t' `cons` rest                               Nothing -> rest  -- | This function transforms every subterm according to the given@@ -66,12 +66,12 @@ --     where run i@(Term t) = foldl (\s x -> s `c` run x) (q i) t query q c i@(Term t) = hfoldl (\s x -> s `c` query q c x) (q i) t -subs :: HFoldable f => Term f  :=> [A (Term f)]-subs = query (\x-> [A x]) (++)+subs :: HFoldable f => Term f  :=> [E (Term f)]+subs = query (\x-> [E x]) (++) -subs' :: (HFoldable f, g :<: f) => Term f :=> [A (g (Term f))]+subs' :: (HFoldable f, g :<: f) => Term f :=> [E (g (Term f))] subs' = mapMaybe pr . subs-        where pr (A v) = fmap A (project v)+        where pr (E v) = fmap E (project v)  -- | This function computes the generic size of the given term, -- i.e. the its number of subterm occurrences.

@@ -56,8 +56,8 @@                 mf Nothing (K y) = Just y                 mf (Just x) (K y) = Just (f x y) -htoList :: (HFoldable f) => f a :=> [A a]-htoList = hfoldr (\ n l ->  A n : l) []+htoList :: (HFoldable f) => f a :=> [E a]+htoList = hfoldr (\ n l ->  E n : l) []      kfoldr :: (HFoldable f) => (a -> b -> b) -> b -> f (K a) :=> b kfoldr f = hfoldr (\ (K x) y -> f x y)

@@ -23,6 +23,7 @@      I (..),      K (..),      A (..),+     E (..),      (:.:)(..)      ) where @@ -35,7 +36,9 @@ instance Functor (K a) where     fmap _ (K x) = K x -data A f = forall i. A {unA :: f i}+data E f = forall i. E {unE :: f i}++data A f = A {unA :: forall i. f i}  instance Eq a => Eq (K a i) where     K x == K y = x == y

@@ -0,0 +1,50 @@+{-# LANGUAGE TypeOperators #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.Number+-- Copyright   :  (c) 2012 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+-- +-- This module provides functionality to number the components of a+-- functorial value with consecutive integers.+--+--------------------------------------------------------------------------------++module Data.Comp.Multi.Number +    ( Numbered (..)+    , unNumbered+    , number+    , HTraversable ()) where++import Data.Comp.Multi.HTraversable+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.Ordering+import Data.Comp.Multi.Equality+++import Control.Monad.State+++-- | This type is used for numbering components of a functorial value.+newtype Numbered a i = Numbered (Int, a i)++unNumbered :: Numbered a :-> a+unNumbered (Numbered (_, x)) = x++instance KEq (Numbered a) where+  keq (Numbered (i,_))  (Numbered (j,_)) = i == j++instance KOrd (Numbered a) where+    kcompare (Numbered (i,_))  (Numbered (j,_)) = i `compare` j++-- | This function numbers the components of the given functorial+-- value with consecutive integers starting at 0.+number :: HTraversable f => f a :-> f (Numbered a)+number x = fst $ runState (hmapM run x) 0 where+  run b = do n <- get+             put (n+1)+             return $ Numbered (n,b)

@@ -33,8 +33,8 @@ class EqHF f => OrdHF f where     compareHF :: KOrd a => f a i -> f a j -> Ordering ---instance KOrd f => Ord (f i) where---    compare = kcompare+instance KOrd f => Ord (E f) where+    compare (E x) (E y) = kcompare x y  instance Ord a => KOrd (K a) where     kcompare (K x) (K y) = compare x y

@@ -39,7 +39,7 @@ instance (ShowHF f, HFunctor f, KShow a) => KShow (Cxt h f a) where     kshow = free showHF kshow -instance (KShow f) => Show (f i) where+instance (KShow (Cxt h f a)) => Show (Cxt h f a i) where     show = unK . kshow  instance (ShowHF f, Show p) => ShowHF (f :&: p) where

@@ -31,30 +31,64 @@     ) where  import Data.Comp.Multi.Term+import Data.Comp.Multi.Ordering+import Data.Comp.Multi.Number+import Data.Comp.Multi.Ops import Data.Comp.Multi.Algebra import Data.Comp.Multi.Derive import Data.Comp.Multi.HFunctor import Data.Comp.Multi.HFoldable+import Data.Map (Map)+import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set-import Data.Maybe  -type GSubst v a = NatM Maybe (K v) a+type GSubst v a = Map v (A a)  type CxtSubst h a f v =  GSubst v (Cxt h f a)  type Subst f v = CxtSubst NoHole (K ()) f v +type SubstFun v a = NatM Maybe (K v) a++++substFun :: Ord v => GSubst v a -> SubstFun v a+substFun s (K v) = fmap unA $ Map.lookup v s+ {-| This multiparameter class defines functors with variables. An instance   @HasVar f v@ denotes that values over @f@ might contain and bind variables of   type @v@. -} class HasVars (f  :: (* -> *) -> * -> *) v where+    -- | Indicates whether the @f@ constructor is a variable. The+    -- default implementation returns @Nothing@.     isVar :: f a :=> Maybe v     isVar _ = Nothing-    bindsVars :: f a :=> [v]-    bindsVars _ = []     +    -- | Indicates the set of variables bound by the @f@ constructor+    -- for each argument of the constructor. For example for a+    -- non-recursive let binding:+    -- @+    -- data Let i e = Let Var (e i) (e i)+    -- instance HasVars Let Var where+    --   bindsVars (Let v x y) = Map.fromList [(y, (Set.singleton v))]+    -- @+    -- If, instead, the let binding is recursive, the methods has to+    -- be implemented like this:+    -- @+    --   bindsVars (Let v x y) = Map.fromList [(x, (Set.singleton v)),+    --                                         (y, (Set.singleton v))]+    -- @+    -- This indicates that the scope of the bound variable also+    -- extends to the right-hand side of the variable binding.+    --+    -- The default implementation returns the empty map.+    bindsVars :: KOrd a => f a :=> Map (E a) (Set v)+    bindsVars _ = Map.empty++$(derive [liftSum] [''HasVars])+     -- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if -- @v@ is contained in the given set of variables.     @@ -64,66 +98,87 @@                    then Nothing                    else return v -$(derive [liftSum] [''HasVars])+-- | This combinator pairs every argument of a given constructor with+-- the set of (newly) bound variables according to the corresponding+-- 'HasVars' type class instance.+getBoundVars :: forall f a v i . (HasVars f v, HTraversable f) => f a i -> f (a :*: K (Set v)) i+getBoundVars t = let n :: f (Numbered a) i+                     n = number t+                     m :: Map (E (Numbered a)) (Set v)+                     m = bindsVars n+                     trans :: Numbered a :-> (a :*: K (Set v))+                     trans x = unNumbered x :*: (K (Map.findWithDefault Set.empty (E x) m))+                 in hfmap trans n+                    +-- | This combinator combines 'getBoundVars' with the 'mfmap' function.+hfmapBoundVars :: forall f a b v i . (HasVars f v, HTraversable f) +                  => (Set v -> a :-> b) -> f a i -> f b i+hfmapBoundVars f t = let n :: f (Numbered a) i+                         n = number t+                         m :: Map (E (Numbered a)) (Set v)+                         m = bindsVars n+                         trans :: Numbered a :-> b+                         trans x = f (Map.findWithDefault Set.empty (E x) m) (unNumbered x)+                     in hfmap trans n+                        +-- | This combinator combines 'getBoundVars' with the generic 'hfoldl' function.   +hfoldlBoundVars :: forall f a b v i . (HasVars f v, HTraversable f) +                  => (b -> Set v ->  a :=> b) -> b -> f a i -> b+hfoldlBoundVars f e t = let n :: f (Numbered a) i+                            n = number t+                            m :: Map (E (Numbered a)) (Set v)+                            m = bindsVars n+                            trans :: b -> Numbered a :=> b+                            trans x y = f x (Map.findWithDefault Set.empty (E y) m) (unNumbered y)+                       in hfoldl trans e n -instance HasVars f v => HasVars (Cxt h f) v where-    isVar (Term t) = isVar t-    isVar _ = Nothing-    bindsVars (Term t) = bindsVars t-    bindsVars _ = [] + -- Auxiliary data type, used only to define varsToHoles-data C a b i = C{ unC :: a -> b i }+newtype C a b i = C{ unC :: a -> b i } -varsToHoles :: forall f v. (HFunctor f, HasVars f v, Eq v) =>+varsToHoles :: forall f v. (HTraversable f, HasVars f v, Ord v) =>                 Term f :-> Context f (K v)-varsToHoles t = unC (cata alg t) []-    where alg :: (HFunctor f, HasVars f v, Eq v) =>-                 Alg f (C [v] (Context f (K v)))-          alg t = C $ \vars ->-              let vars' = vars ++ bindsVars t in-              case isVar t of-                Just v ->-                    -- Check for scope-                    if v `elem` vars' then-                        Term $ hfmap (`unC` vars') t-                    else-                        Hole $ K v-                Nothing ->-                    Term $ hfmap (`unC` vars') t--containsVarAlg :: (Eq v, HasVars f v, HFoldable f) => v -> Alg f (K Bool)-containsVarAlg v t = K $ v `notElem` bindsVars t &&-                         (local || kfoldl (||) False t)+varsToHoles t = unC (cata alg t) Set.empty+    where alg :: (HTraversable f, HasVars f v, Ord v) => Alg f (C (Set v) (Context f (K v)))+          alg t = C $ \vars -> case isVar t of+            Just v | v `Set.member` vars -> Hole $ K v+            _  -> Term $ hfmapBoundVars run t+              where +                run :: Set v -> C (Set v) (Context f (K v))  :-> Context f (K v)+                run newVars f = f `unC` (newVars `Set.union` vars)+                +-- | Convert variables to holes, except those that are bound.+containsVarAlg :: forall v f . (Ord v, HasVars f v, HTraversable f) => v -> Alg f (K Bool)+containsVarAlg v t = K $ hfoldlBoundVars run local t     where local = case isVar t of                     Just v' -> v == v'                     Nothing -> False+          run :: Bool -> Set v -> (K Bool i) -> Bool+          run acc vars (K b) = acc || (not (v `Set.member` vars) && b)  {-| This function checks whether a variable is contained in a context. -}-containsVar :: (Eq v, HasVars f v, HFoldable f, HFunctor f)+containsVar :: (Ord v, HasVars f v, HTraversable f, HFunctor f)             => v -> Cxt h f a :=> Bool containsVar v = unK . free (containsVarAlg v) (const $ K False) -variableListAlg :: (HasVars f v, HFoldable f, Eq v) => Alg f (K [v])-variableListAlg t = K $ filter (`notElem` bindsVars t) $ kfoldl (++) local t-    where local = case isVar t of-                    Just v -> [v]-                    Nothing -> []   {-| This function computes the list of variables occurring in a context. -}-variableList :: (HasVars f v, HFoldable f, HFunctor f, Eq v)+variableList :: (HasVars f v, HTraversable f, HFunctor f, Ord v)              => Cxt h f a :=> [v]-variableList = unK . free variableListAlg (const $ K [])+variableList = Set.toList . variables -variablesAlg :: (Ord v, HasVars f v, HFoldable f) => Alg f (K (Set v))-variablesAlg t = K $ Set.filter (`notElem` bindsVars t) $-                     kfoldl Set.union local t+-- |Algebra for checking whether a variable is contained in a term, except those+-- that are bound.+variablesAlg :: (Ord v, HasVars f v, HTraversable f) => Alg f (K (Set v))+variablesAlg t = K $ hfoldlBoundVars run local t     where local = case isVar t of                     Just v -> Set.singleton v                     Nothing -> Set.empty+          run acc bvars (K vars) = acc `Set.union` (vars `Set.difference` bvars)  {-| This function computes the set of variables occurring in a context. -}-variables :: (Ord v, HasVars f v, HFoldable f, HFunctor f)+variables :: (Ord v, HasVars f v, HTraversable f, HFunctor f)             => Cxt h f a :=> Set v variables = unK . free variablesAlg (const $ K Set.empty) @@ -137,29 +192,30 @@ {-| This function substitutes variables in a context according to a partial mapping from variables to contexts.-} class SubstVars v t a where-    substVars :: (Set v) -> GSubst v t -> a :-> a+    substVars :: SubstFun v t -> a :-> a -appSubst :: SubstVars v t a => GSubst v t -> a :-> a-appSubst = substVars Set.empty+appSubst :: (Ord v, SubstVars v t a) => GSubst v t -> a :-> a+appSubst subst = substVars (substFun subst) -instance (Ord v, HasVars f v, HFunctor f) => SubstVars v (Cxt h f a) (Cxt h f a) where+instance (Ord v, HasVars f v, HTraversable f) => SubstVars v (Cxt h f a) (Cxt h f a) where     -- have to use explicit GADT pattern matching!!-    substVars _ _ (Hole a) = Hole a-    substVars b f (Term v) = substAlg f (hfmap (substVars newBound f) v)-        where  substAlg :: (HasVars f v) => CxtSubst h a f v-                        -> Alg f (Cxt h f a)-               substAlg f t = fromMaybe (Term t) (isVar' b t >>= f . K)-               newBound = b `Set.union` Set.fromList (bindsVars v)+    substVars subst = doSubst Set.empty+      where doSubst :: Set v -> Cxt h f a :-> Cxt h f a+            doSubst _ (Hole a) = Hole a+            doSubst b (Term t) = case isVar' b t >>= subst . K of +              Just new -> new+              Nothing  -> Term $ hfmapBoundVars run t+                where run :: Set v -> Cxt h f a :-> Cxt h f a+                      run vars s = doSubst (b `Set.union` vars) s  instance (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where-    substVars b f = hfmap (substVars b f) +    substVars subst = hfmap (substVars subst)   {-| This function composes two substitutions @s1@ and @s2@. That is, applying the resulting substitution is equivalent to first applying @s2@ and then @s1@. -} -compSubst :: (Ord v, HasVars f v, HFunctor f)+compSubst :: (Ord v, HasVars f v, HTraversable f)           => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v-compSubst s1 s2 v = case s2 v of-                      Nothing -> s1 v-                      Just t -> Just $ appSubst s1 t+compSubst s1 s2 = Map.map f s2+    where f (A t) = A (appSubst s1 t)

@@ -22,6 +22,7 @@      HFunctor (..),      I (..),      K (..),+     E (..),      A (..),      (:->),      NatM

@@ -1,5 +1,5 @@ {-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,-  MultiParamTypeClasses #-}+  MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-} -------------------------------------------------------------------------------- -- | -- Module      :  Data.Comp.Param.Term@@ -24,6 +24,7 @@      Context,      simpCxt,      toCxt,+     cxtMap,      ParamFunctor(..)     ) where @@ -68,6 +69,13 @@ toCxt :: Difunctor f => Trm f a -> Cxt h f a b {-# INLINE toCxt #-} toCxt = unsafeCoerce++-- | This combinator maps a function over a context by applying the+-- function to each hole.+cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c+cxtMap f (Hole x) = Hole (f x)+cxtMap _ (Var x)  = Var x+cxtMap f (In t)   = In (dimap id (cxtMap f) t)  -- Param Functor 

@@ -22,6 +22,8 @@ import Control.Monad.Error import Control.Monad.State +import Data.Traversable+ import qualified Data.Map as Map  {-| This type represents equations between terms over a specific@@ -56,7 +58,7 @@  -- | This function applies a substitution to each term in a list of -- equations.-appSubstEq :: (Ord v,  HasVars f v, Functor f) =>+appSubstEq :: (Ord v,  HasVars f v, Traversable f) =>      Subst f v -> Equation f -> Equation f appSubstEq s (t1,t2) = (appSubst s t1,appSubst s t2) @@ -64,7 +66,7 @@ {-| This function returns the most general unifier of the given equations using the algorithm of Martelli and Montanari. -} -unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f))+unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f)       => Equations f -> m (Subst f v) unify = runUnifyM runUnify @@ -95,18 +97,18 @@ putEqs eqs = modify addEqs     where addEqs s = s {usEqs = eqs ++ usEqs s} -putBinding :: (Monad m, Ord v, HasVars f v, Functor f) => (v, Term f) -> UnifyM f v m ()+putBinding :: (Monad m, Ord v, HasVars f v, Traversable f) => (v, Term f) -> UnifyM f v m () putBinding bind = modify appSubst     where binds = Map.fromList [bind]           appSubst s = s { usEqs = map (appSubstEq binds) (usEqs s),                              usSubst = compSubst binds (usSubst s)}  -runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f))+runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f)          => UnifyM f v m () runUnify = withNextEq (\ e -> unifyStep e >> runUnify) -unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f)) +unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f)            => Equation f -> UnifyM f v m () unifyStep (s,t) = case decompose s of                     Var v1 -> case decompose t of

@@ -30,6 +30,7 @@     ) where  import Data.Comp.Term+import Data.Comp.Number import Data.Comp.Algebra import Data.Comp.Derive import Data.Foldable hiding (elem, notElem)@@ -52,72 +53,107 @@   @HasVar f v@ denotes that values over @f@ might contain and bind variables of   type @v@. -} class HasVars f v where-    -- |Indicates whether the @f@ constructor is a variable.+    -- | Indicates whether the @f@ constructor is a variable. The+    -- default implementation returns @Nothing@.     isVar :: f a -> Maybe v     isVar _ = Nothing-    -- |Indicates the set of variables bound by the @f@ constructor.-    bindsVars :: f a -> [v]-    bindsVars _ = []+    +    -- | Indicates the set of variables bound by the @f@ constructor+    -- for each argument of the constructor. For example for a+    -- non-recursive let binding:+    -- @+    -- data Let e = Let Var e e+    -- instance HasVars Let Var where+    --   bindsVars (Let v x y) = Map.fromList [(y, (Set.singleton v))]+    -- @+    -- If, instead, the let binding is recursive, the methods has to+    -- be implemented like this:+    -- @+    --   bindsVars (Let v x y) = Map.fromList [(x, (Set.singleton v)),+    --                                         (y, (Set.singleton v))]+    -- @+    -- This indicates that the scope of the bound variable also+    -- extends to the right-hand side of the variable binding.+    --+    -- The default implementation returns the empty map.+    bindsVars :: Ord a => f a -> Map a (Set v)+    bindsVars _ = Map.empty + $(derive [liftSum] [''HasVars]) -instance HasVars f v => HasVars (Cxt h f) v where-    isVar (Term t) = isVar t-    isVar _ = Nothing-    bindsVars (Term t) = bindsVars t-    bindsVars _ = []+-- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if+-- @v@ is contained in the given set of variables.+    +isVar' :: (HasVars f v, Ord v) => Set v -> f a -> Maybe v+isVar' b t = do v <- isVar t+                if v `Set.member` b+                   then Nothing+                   else return v+   +-- | This combinator pairs every argument of a given constructor with+-- the set of (newly) bound variables according to the corresponding+-- 'HasVars' type class instance.+getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a)+getBoundVars t = let n = number t+                     m = bindsVars n+                     trans x = (Map.findWithDefault Set.empty x m, unNumbered x)+                 in fmap trans n+                    +-- | This combinator combines 'getBoundVars' with the generic 'fmap' function.+fmapBoundVars :: (HasVars f v, Traversable f) => (Set v -> a -> b) -> f a -> f b+fmapBoundVars f t = let n = number t+                        m = bindsVars n+                        trans x = f (Map.findWithDefault Set.empty x m) (unNumbered x)+                    in fmap trans n                    +                    +-- | This combinator combines 'getBoundVars' with the generic 'foldl' function.   +foldlBoundVars :: (HasVars f v, Traversable f) => (b -> Set v -> a -> b) -> b -> f a -> b+foldlBoundVars f e t = let n = number t+                           m = bindsVars n+                           trans x y = f x (Map.findWithDefault Set.empty y m) (unNumbered y) +                       in foldl trans e n  -- | Convert variables to holes, except those that are bound.-varsToHoles :: (Functor f, HasVars f v, Eq v) => Term f -> Context f v-varsToHoles t = cata alg t []-    where alg :: (Functor f, HasVars f v, Eq v) => Alg f ([v] -> Context f v)-          alg t vars =-              let vars' = vars ++ bindsVars t in-              case isVar t of-                Just v ->-                    -- Check for scope-                    if v `elem` vars' then-                        Term $ fmap (\x -> x vars') t-                    else-                        Hole v-                Nothing ->-                    Term $ fmap (\x -> x vars') t+varsToHoles :: (Traversable f, HasVars f v, Ord v) => Term f -> Context f v+varsToHoles t = cata alg t Set.empty+    where alg :: (Traversable f, HasVars f v, Ord v) => Alg f (Set v -> Context f v)+          alg t vars = case isVar t of+            Just v | v `Set.member` vars -> Hole v+            _  -> Term $ fmapBoundVars run t+              where +                run newVars f = f $ newVars `Set.union` vars  -- |Algebra for checking whether a variable is contained in a term, except those -- that are bound.-containsVarAlg :: (Eq v, HasVars f v, Foldable f) => v -> Alg f Bool-containsVarAlg v t = v `notElem` bindsVars t && (local || or t)+containsVarAlg :: (Eq v, HasVars f v, Traversable f, Ord v) => v -> Alg f Bool+containsVarAlg v t = foldlBoundVars run local t     where local = case isVar t of                     Just v' -> v == v'                     Nothing -> False+          run acc vars b = acc || (not (v `Set.member` vars) && b)  {-| This function checks whether a variable is contained in a context. -}-containsVar :: (Eq v, HasVars f v, Foldable f, Functor f)+containsVar :: (Eq v, HasVars f v, Traversable f, Ord v)             => v -> Cxt h f a -> Bool containsVar v = free (containsVarAlg v) (const False)  -- |Algebra for generating a set of variables contained in a term, except those -- that are bound.-variablesAlg :: (Ord v, HasVars f v, Foldable f) => Alg f (Set v)-variablesAlg t = Set.filter (`notElem` bindsVars t) $ foldl Set.union local t+variablesAlg :: (Ord v, HasVars f v, Traversable f) => Alg f (Set v)+variablesAlg t = foldlBoundVars run local t     where local = case isVar t of                     Just v -> Set.singleton v                     Nothing -> Set.empty+          run acc bvars vars = acc `Set.union` (vars `Set.difference` bvars) --- |Algebra for generating a list of variables contained in a term, except those--- that are bound.-variableListAlg :: (Ord v, HasVars f v, Foldable f) => Alg f [v]-variableListAlg t = filter (`notElem` bindsVars t) $ foldl (++) local t-    where local = case isVar t of-                    Just v -> [v]-                    Nothing -> []   {-| This function computes the list of variables occurring in a context. -}-variableList :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> [v]-variableList = free variableListAlg (const [])+variableList :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> [v]+variableList = Set.toList . variables  {-| This function computes the set of variables occurring in a context. -}-variables :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> Set v+variables :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> Set v variables = free variablesAlg (const Set.empty)  {-| This function computes the set of variables occurring in a constant. -}@@ -136,18 +172,16 @@ appSubst subst = substVars f     where f v = Map.lookup v subst -instance (Ord v, HasVars f v, Functor f)+instance (Ord v, HasVars f v, Traversable f)     => SubstVars v (Cxt h f a) (Cxt h f a) where         -- have to use explicit GADT pattern matching!!         -- subst f = free (substAlg f) Hole-    substVars _ (Hole a) = Hole a-    substVars f (Term v) = let f' = res (bindsVars v) f in-                           substAlg f' $ fmap (substVars f') v-            where substAlg :: (HasVars f v) => (v -> Maybe (Cxt h f a))-                           -> Alg f (Cxt h f a)-                  substAlg f t = fromMaybe (Term t) (isVar t >>= f)-                  res :: Eq v => [v] -> (v -> Maybe t) -> v -> Maybe t-                  res vars f x = if x `elem` vars then Nothing else f x+  substVars subst = doSubst Set.empty+    where doSubst _ (Hole a) = Hole a+          doSubst b (Term t) = case isVar' b t >>= subst of +            Just new -> new+            Nothing  -> Term $ fmapBoundVars run t+              where run vars s = doSubst (b `Set.union` vars) s  instance (SubstVars v t a, Functor f) => SubstVars v t (f a) where     substVars f = fmap (substVars f) @@ -155,6 +189,6 @@ {-| This function composes two substitutions @s1@ and @s2@. That is, applying the resulting substitution is equivalent to first applying @s2@ and then @s1@. -}-compSubst :: (Ord v, HasVars f v, Functor f)+compSubst :: (Ord v, HasVars f v, Traversable f)           => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v compSubst s1 s2 = fmap (appSubst s1) s2 `Map.union` s1

@@ -9,8 +9,8 @@ import Data.Comp  import Test.Framework-import Test.Framework.Providers.QuickCheck2-import Test.QuickCheck+import Test.Framework.Providers.HUnit+import Test.HUnit import Test.Utils hiding (iPair)  @@ -22,10 +22,10 @@ --------------------------------------------------------------------------------  tests = testGroup "Compositional Data Types" [-         testProperty "eval" evalTest,-         testProperty "evalM" evalMTest,-         testProperty "desugarEval" desugarEvalTest,-         testProperty "desugarPos" desugarPosTest+         testCase "eval" evalTest,+         testCase "evalM" evalMTest,+         testCase "desugarEval" desugarEvalTest,+         testCase "desugarPos" desugarPosTest         ]  @@ -36,10 +36,10 @@ instance (EqF f, Eq p) => EqF (f :&: p) where     eqF (v1 :&: p1) (v2 :&: p2) = p1 == p2 && v1 `eqF` v2 -evalTest = Eval.evalEx == iConst 5-evalMTest = evalMEx == Just (iConst 5)-desugarEvalTest = Desugar.evalEx == iPair (iConst 2) (iConst 1)-desugarPosTest = desugPEx == iAPair (Pos 1 0)+evalTest = Eval.evalEx @=? iConst 5+evalMTest = evalMEx @=? Just (iConst 5)+desugarEvalTest = Desugar.evalEx @=? iPair (iConst 2) (iConst 1)+desugarPosTest = desugPEx @=? iAPair (Pos 1 0)                                     (iASnd (Pos 1 0)                                            (iAPair (Pos 1 1)                                                    (iAConst (Pos 1 2) 1)

@@ -10,8 +10,8 @@ import Data.Comp.Multi  import Test.Framework-import Test.Framework.Providers.QuickCheck2-import Test.QuickCheck+import Test.Framework.Providers.HUnit+import Test.HUnit import Test.Utils hiding (iPair)  --------------------------------------------------------------------------------@@ -19,11 +19,11 @@ --------------------------------------------------------------------------------  tests = testGroup "Generalised Compositional Data Types" [-         testProperty "eval" evalTest,-         testProperty "evalI" evalITest,-         testProperty "evalM" evalMTest,-         testProperty "desugarEval" desugarEvalTest,-         testProperty "desugarPos" desugarPosTest+         testCase "eval" evalTest,+         testCase "evalI" evalITest,+         testCase "evalM" evalMTest,+         testCase "desugarEval" desugarEvalTest,+         testCase "desugarPos" desugarPosTest         ]  @@ -34,11 +34,11 @@ instance (EqHF f, Eq p) => EqHF (f :&: p) where     eqHF (v1 :&: p1) (v2 :&: p2) = p1 == p2 && v1 `eqHF` v2 -evalTest = Eval.evalEx == iConst 2-evalITest = evalIEx == 2-evalMTest = evalMEx == Just (iConst 5)-desugarEvalTest = Desugar.evalEx == iPair (iConst 2) (iConst 1)-desugarPosTest = desugPEx == iAPair (Pos 1 0)+evalTest = Eval.evalEx @=? iConst 2+evalITest = evalIEx @=? 2+evalMTest = evalMEx @=? Just (iConst 5)+desugarEvalTest = Desugar.evalEx @=? iPair (iConst 2) (iConst 1)+desugarPosTest = desugPEx @=? iAPair (Pos 1 0)                                     (iASnd (Pos 1 0)                                     (iAPair (Pos 1 1)                                             (iAConst (Pos 1 2) 1)

@@ -7,8 +7,8 @@ import Data.Comp.MultiParam.FreshM (Name)  import Test.Framework-import Test.Framework.Providers.QuickCheck2-import Test.QuickCheck+import Test.Framework.Providers.HUnit+import Test.HUnit import Test.Utils  @@ -20,7 +20,7 @@ --------------------------------------------------------------------------------  tests = testGroup "Parametric Compositional Data Types" [-         testProperty "FOL" folTest+         testCase "FOL" folTest         ]  @@ -28,7 +28,7 @@ -- Properties -------------------------------------------------------------------------------- -folTest = show (foodFact7 :: INF Name TFormula) == "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Person(Skol6(x2)))\n" +++folTest = show (foodFact7 :: INF Name TFormula) @=? "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Person(Skol6(x2)))\n" ++           "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Eats(Skol6(x2), x2))\n" ++                                                                                         "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Person(Skol6(x2)))\n" ++                                                                                         "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Eats(Skol6(x2), x2))"

@@ -7,8 +7,8 @@ import Data.Comp.Param  import Test.Framework-import Test.Framework.Providers.QuickCheck2-import Test.QuickCheck+import Test.Framework.Providers.HUnit+import Test.HUnit import Test.Utils  @@ -20,8 +20,8 @@ --------------------------------------------------------------------------------  tests = testGroup "Parametric Compositional Data Types" [-         testProperty "names" namesTest,-         testProperty "graph" graphTest+         testCase "names" namesTest,+         testCase "graph" graphTest         ]  @@ -34,5 +34,5 @@                                      b2 <- eqD v1 v2                                      return $ b1 && b2 -namesTest = en == en' && ep == ep'-graphTest = g == g && n == 5 && f == [0,2,1,2]+namesTest = sequence_ [en @=? en', ep @=? ep']+graphTest = sequence_ [n @=? 5, f @=? [0,2,1,2]]

@@ -0,0 +1,119 @@+{-# LANGUAGE TemplateHaskell, TypeSynonymInstances, FlexibleInstances,+MultiParamTypeClasses, TypeOperators, FlexibleContexts , RankNTypes,+GADTs, ScopedTypeVariables, EmptyDataDecls#-}++module Data.Comp.Multi.Variables_Test where+++import Data.Comp.Multi.Variables+import Data.Comp.Multi.Derive+import Data.Comp.Multi.Sum+import Data.Comp.Multi.Term+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.Show ()++import Data.Map (Map)+import qualified Data.Map as Map+import Data.Set (Set)+import qualified Data.Set as Set++import Test.Framework+import Test.Framework.Providers.HUnit+import Test.HUnit++++--------------------------------------------------------------------------------+-- Definitions+--------------------------------------------------------------------------------++data Var = X | Y | Z deriving (Eq,Ord,Show)+++data Ex++type Value f = forall i . Term f i+type Expression f = Term f Ex++data Val e i where +    Abs :: Var -> e Ex -> Val e i+    Var :: Var -> Val e i+    Int :: Int -> Val e i+++data Op e i where+    App :: e Ex -> e Ex -> Op e Ex+    Plus :: e Ex -> e Ex -> Op e Ex+++data Let e i  where +             Let :: Var -> e Ex -> e Ex -> Let e Ex++data LetRec e i  where +             LetRec :: Var -> e Ex -> e Ex -> LetRec e Ex++type Sig = Op :+: Val++type SigLet = Let :+: Sig++type SigRec = LetRec :+: Sig++$(derive [makeHFunctor, makeHTraversable, makeHFoldable,+          makeEqHF, makeShowHF, smartConstructors]+         [''Op, ''Val, ''Let, ''LetRec])++instance HasVars Val Var where+    isVar (Var v) = Just v+    isVar _       = Nothing+    +    bindsVars (Abs v a) = Map.singleton (E a) (Set.singleton v)+    bindsVars _         = Map.empty++instance HasVars Op a where++instance HasVars Let Var where+    bindsVars (Let v _ a) = Map.singleton (E a) (Set.singleton v)++instance HasVars LetRec Var where+    bindsVars (LetRec v a b) = Map.fromList [(E a,vs),(E b,vs)]+        where vs = Set.singleton v++-- let x = x + 1 in (\y. y + x) z+letExp, letExp' :: Expression SigLet+letExp = iLet X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)+letExp' = iLet X (iInt 1 `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)++-- letrec x = x + 1 in (\y. y + x) z+recExp, recExp :: Expression SigRec+recExp = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)+recExp' = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)++subst :: (Val :<: f) => Subst f Var+subst = Map.fromList [(X, A $ iInt 1), (Y, A $ iInt 2), (Z, A $ iInt 3)]++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------++case_letFree = variables letExp @=? Set.fromList [Z,X]++case_recFree = variables recExp @=? Set.fromList [Z]++case_letSubst = appSubst s letExp @=? letExp'+    where s = subst :: Subst SigLet Var++case_recSubst = appSubst s recExp @=? recExp'+    where s = subst :: Subst SigRec Var++--------------------------------------------------------------------------------+-- Test Suits+--------------------------------------------------------------------------------++main = defaultMain [tests]++tests = testGroup "Variables" [+         testCase "case_letFree" case_letFree+        ,testCase "case_recFree" case_recFree+        ,testCase "case_letSubst" case_letSubst+        ,testCase "case_recSubst" case_recSubst+        ]

@@ -0,0 +1,18 @@+module Data.Comp.Multi_Test where++import Test.Framework+import qualified Data.Comp.Multi.Variables_Test++--------------------------------------------------------------------------------+-- Test Suits+--------------------------------------------------------------------------------++main = defaultMain [tests]++tests = testGroup "Multi" [+         Data.Comp.Multi.Variables_Test.tests+       ]++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------

@@ -0,0 +1,106 @@+{-# LANGUAGE TemplateHaskell, TypeSynonymInstances,+FlexibleInstances, MultiParamTypeClasses, TypeOperators, FlexibleContexts#-}++module Data.Comp.Variables_Test where+++import Data.Comp.Variables+import Data.Comp.Derive+import Data.Comp.Sum+import Data.Comp.Term+import Data.Comp.Show ()++import Data.Map (Map)+import qualified Data.Map as Map+import Data.Set (Set)+import qualified Data.Set as Set++import Test.Framework+import Test.Framework.Providers.HUnit+import Test.HUnit++++--------------------------------------------------------------------------------+-- Definitions+--------------------------------------------------------------------------------++data Var = X | Y | Z deriving (Eq,Ord,Show)+++data Val e = Abs Var e+           | Var Var+           | Int Int++data Op e = App e e+          | Plus e e++data Let e = Let Var e e++data LetRec e = LetRec Var e e++type Sig = Op :+: Val++type SigLet = Let :+: Sig++type SigRec = LetRec :+: Sig++$(derive [makeFunctor, makeTraversable, makeFoldable,+          makeEqF, makeShowF, smartConstructors]+         [''Op, ''Val, ''Let, ''LetRec])++instance HasVars Val Var where+    isVar (Var v) = Just v+    isVar _       = Nothing+    +    bindsVars (Abs v a) = Map.singleton a (Set.singleton v)+    bindsVars _         = Map.empty++instance HasVars Op a where++instance HasVars Let Var where+    bindsVars (Let v _ a) = Map.singleton a (Set.singleton v)++instance HasVars LetRec Var where+    bindsVars (LetRec v a b) = Map.fromList [(a,vs),(b,vs)]+        where vs = Set.singleton v++-- let x = x + 1 in (\y. y + x) z+letExp, letExp' :: Term SigLet+letExp = iLet X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)+letExp' = iLet X (iInt 1 `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)++-- letrec x = x + 1 in (\y. y + x) z+recExp, recExp :: Term SigRec+recExp = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)+recExp' = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)++subst :: (Val :<: f) => Subst f Var+subst = Map.fromList [(X, iInt 1), (Y, iInt 2), (Z, iInt 3)]++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------++case_letFree = Set.fromList [Z,X] @=? variables letExp++case_recFree = Set.fromList [Z] @=? variables recExp++case_letSubst = letExp' @=? appSubst s letExp+    where s = subst :: Subst SigLet Var++case_recSubst = recExp' @=? appSubst s recExp+    where s = subst :: Subst SigRec Var++--------------------------------------------------------------------------------+-- Test Suits+--------------------------------------------------------------------------------++main = defaultMain [tests]++tests = testGroup "Variables" [+         testCase "case_letFree" case_letFree+        ,testCase "case_recFree" case_recFree+        ,testCase "case_letSubst" case_letSubst+        ,testCase "case_recSubst" case_recSubst+        ]

@@ -1,18 +1,11 @@ module Data.Comp_Test where --import Data.Comp-import Data.Comp.Equality-import Data.Comp.Arbitrary ()-import Data.Comp.Show ()--import Test.Framework-import Test.Framework.Providers.QuickCheck2-import Test.QuickCheck-import Test.Utils+import Test.Framework   import qualified Data.Comp.Equality_Test import qualified Data.Comp.Examples_Test+import qualified Data.Comp.Variables_Test+import qualified Data.Comp.Multi_Test  -------------------------------------------------------------------------------- -- Test Suits@@ -22,7 +15,9 @@  tests = testGroup "Comp" [          Data.Comp.Equality_Test.tests,-         Data.Comp.Examples_Test.tests+         Data.Comp.Examples_Test.tests,+         Data.Comp.Variables_Test.tests,+         Data.Comp.Multi_Test.tests         ]  --------------------------------------------------------------------------------