compdata 0.1 → 0.2

raw patch · 34 files changed

+1037/−1355 lines, 34 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• benchmark/Benchmark.hs +38/−64
• benchmark/DataTypes/Comp.hs +23/−10
• benchmark/DataTypes/Transform.hs +53/−25
• benchmark/Functions/Comp/Desugar.hs +39/−39
• benchmark/Functions/Comp/Eval.hs +13/−30
• benchmark/Functions/Comp/Inference.hs +29/−38
• benchmark/Functions/Standard/Desugar.hs +17/−17
• benchmark/Functions/Standard/Eval.hs +4/−4
• benchmark/Functions/Standard/Inference.hs +4/−4
• benchmark/Test.hs +61/−0
• compdata.cabal +5/−9
• src/Data/Comp.hs +0/−2
• src/Data/Comp/Algebra.hs +1/−44
• src/Data/Comp/Derive.hs +0/−6
• src/Data/Comp/Derive/Arbitrary.hs +2/−2
• src/Data/Comp/Derive/ExpFunctor.hs +0/−105
• src/Data/Comp/Derive/Multi/ExpFunctor.hs +0/−94
• src/Data/Comp/Derive/Multi/Show.hs +1/−1
• src/Data/Comp/Derive/Multi/SmartConstructors.hs +5/−5
• src/Data/Comp/ExpFunctor.hs +0/−21
• src/Data/Comp/Multi.hs +99/−102
• src/Data/Comp/Multi/Algebra.hs +197/−238
• src/Data/Comp/Multi/Equality.hs +8/−8
• src/Data/Comp/Multi/ExpFunctor.hs +0/−24
• src/Data/Comp/Multi/Ops.hs +79/−84
• src/Data/Comp/Multi/Product.hs +25/−25
• src/Data/Comp/Multi/Show.hs +11/−11
• src/Data/Comp/Multi/Sum.hs +107/−126
• src/Data/Comp/Multi/Term.hs +41/−40
• src/Data/Comp/Multi/Variables.hs +93/−70
• src/Data/Comp/Ops.hs +0/−9
• src/Data/Comp/Sum.hs +0/−21
• src/Data/Comp/Term.hs +3/−3
• src/Data/Comp/Variables.hs +79/−74

@@ -22,16 +22,7 @@ sExpr :: PExpr sExpr = transSugar aExpr -aHOASExpr :: Int -> DC.HOASExpr-aHOASExpr n = (iLam $ \x -> x `iPlus` ((iLam $ \x -> x `iMult` x) `iApp` x))-              `iApp`-              ((iLam $ \x -> x `iMult` x)-               `iApp`-               (if n <= 0 then iVInt 2 else aHOASExpr (n - 1))) -sHOASExpr :: Int -> DS.HOASExpr-sHOASExpr = transHOAS . aHOASExpr- sfCoalg :: Coalg SugarSig Int sfCoalg 0 = inj $ VInt 1 sfCoalg n = let n' = n-1 in inj $ Plus n' n'@@ -52,41 +43,42 @@ standardBenchmarks :: (PExpr, SugarExpr, String) -> Benchmark standardBenchmarks  (sExpr,aExpr,n) = rnf aExpr `seq` rnf sExpr `seq` getBench (sExpr, aExpr,n)     where getBench (sExpr, aExpr,n) = bgroup n [-                 bench "Comp.desugar" (nf A.desugarExpr aExpr),-                 bench "Comp.desugarAlg" (nf A.desugarExpr2 aExpr),-                 bench "Standard.desugar" (nf S.desugar sExpr),-                 bench "Comp.desugarType" (nf A.desugarType aExpr),-                 bench "Comp.desugarType'" (nf A.desugarType' aExpr),-                 bench "Standard.desugarType" (nf S.desugarType sExpr),-                 bench "Comp.typeSugar" (nf A.typeSugar aExpr),-                 bench "Standard.typeSugar" (nf S.typeSugar sExpr),-                 bench "Comp.desugarType2" (nf A.desugarType2 aExpr),-                 bench "Comp.desugarType2'" (nf A.desugarType2' aExpr),-                 bench "Standard.desugarType2" (nf S.desugarType2 sExpr),-                 bench "Comp.typeSugar2" (nf A.typeSugar2 aExpr),-                 bench "Standard.typeSugar2" (nf S.typeSugar2 sExpr),-                 bench "Comp.desugarEval" (nf A.desugarEval aExpr),-                 bench "Comp.desugarEval'" (nf A.desugarEval' aExpr),-                 bench "Standard.desugarEval" (nf S.desugarEval sExpr),-                 bench "Comp.evalSugar" (nf A.evalSugar aExpr),-                 bench "Comp.evalDirect" (nf A.evalDirectE aExpr),-                 bench "Standard.evalSugar" (nf S.evalSugar sExpr),-                 bench "Comp.desugarEval2" (nf A.desugarEval2 aExpr),-                 bench "Comp.desugarEval2'" (nf A.desugarEval2' aExpr),-                 bench "Standard.desugarEval2" (nf S.desugarEval2 sExpr),-                 bench "Comp.evalSugar2" (nf A.evalSugar2 aExpr),-                 bench "Comp.evalDirect2" (nf A.evalDirectE2 aExpr),-                 bench "Standard.evalSugar2" (nf S.evalSugar2 sExpr),-                 bench "Comp.contVar" (nf (A.contVar 10) aExpr),-                 bench "Comp.contVar'" (nf (A.contVar' 10) aExpr),-                 bench "Comp.contVarGen" (nf (A.contVarGen 10) aExpr),-                 bench "Standard.contVar" (nf (S.contVar 10) sExpr),-                 bench "Standard.contVarGen" (nf (S.contVarGen 10) sExpr),-                 bench "Comp.freeVars" (nf A.freeVars aExpr),-                 bench "Comp.freeVars'" (nf A.freeVars' aExpr),-                 bench "Comp.freeVarsGen" (nf A.freeVarsGen aExpr),-                 bench "Standard.freeVars" (nf S.freeVars sExpr),-                 bench "Standard.freeVarsGen" (nf S.freeVarsGen sExpr)]+                 -- bench "Comp.desug" (nf A.desugExpr aExpr),+                 -- bench "Comp.desugAlg" (nf A.desugExpr2 aExpr),+                 -- bench "Standard.desug" (nf S.desug sExpr),+                 bench "Comp.desugType" (nf A.desugType aExpr),+                 bench "Comp.desugType'" (nf A.desugType' aExpr),+                 bench "Standard.desugType" (nf S.desugType sExpr),+                 -- bench "Comp.typeSugar" (nf A.typeSugar aExpr),+                 -- bench "Standard.typeSugar" (nf S.typeSugar sExpr),+                 bench "Comp.desugType2" (nf A.desugType2 aExpr),+                 bench "Comp.desugType2'" (nf A.desugType2' aExpr),+                 bench "Standard.desugType2" (nf S.desugType2 sExpr)+                 -- bench "Comp.typeSugar2" (nf A.typeSugar2 aExpr),+                 -- bench "Standard.typeSugar2" (nf S.typeSugar2 sExpr),+                 -- bench "Comp.desugEval" (nf A.desugEval aExpr),+                 -- bench "Comp.desugEval'" (nf A.desugEval' aExpr),+                 -- bench "Standard.desugEval" (nf S.desugEval sExpr),+                 -- bench "Comp.evalSugar" (nf A.evalSugar aExpr),+                 -- bench "Comp.evalDirect" (nf A.evalDirectE aExpr),+                 -- bench "Standard.evalSugar" (nf S.evalSugar sExpr),+                 -- bench "Comp.desugEval2" (nf A.desugEval2 aExpr),+                 -- bench "Comp.desugEval2'" (nf A.desugEval2' aExpr),+                 -- bench "Standard.desugEval2" (nf S.desugEval2 sExpr),+                 -- bench "Comp.evalSugar2" (nf A.evalSugar2 aExpr),+                 -- bench "Comp.evalDirect2" (nf A.evalDirectE2 aExpr),+                 -- bench "Standard.evalSugar2" (nf S.evalSugar2 sExpr),+                 -- bench "Comp.contVar" (nf (A.contVar 10) aExpr),+                 -- bench "Comp.contVar'" (nf (A.contVar' 10) aExpr),+                 -- bench "Comp.contVarGen" (nf (A.contVarGen 10) aExpr),+                 -- bench "Standard.contVar" (nf (S.contVar 10) sExpr),+                 -- bench "Standard.contVarGen" (nf (S.contVarGen 10) sExpr),+                 -- bench "Comp.freeVars" (nf A.freeVars aExpr),+                 -- bench "Comp.freeVars'" (nf A.freeVars' aExpr),+                 -- bench "Comp.freeVarsGen" (nf A.freeVarsGen aExpr),+                 -- bench "Standard.freeVars" (nf S.freeVars sExpr),+                 -- bench "Standard.freeVarsGen" (nf S.freeVarsGen sExpr)+                                      ]  randStdBenchmarks :: Int -> IO Benchmark randStdBenchmarks s = do@@ -100,30 +92,12 @@   putStr "size of the input term: "   print $ size aExpr   putStr "does it type check: "-  print (A.desugarType aExpr == Right ty)+  print (A.desugType aExpr == Right ty)   return $ standardBenchmarks (sExpr,aExpr, "random (depth: " ++ show s ++ ", size: "++ show (size aExpr) ++ ")") -hoasBenchmaks :: Int -> Benchmark-hoasBenchmaks s = bgroup ("HOAS (depth: " ++ show s ++ ")") $ getBench s-    where getBench size =-              let sExpr' = sHOASExpr size-                  aExpr' = aHOASExpr size in-              rnf aExpr' `seq` rnf sExpr' `seq`-              [bench "Comp.eval2E" -                     (nf (A.eval2E :: DC.HOASExpr -> HOASValueExpr) aExpr'),-               bench "Standard.evalHOAS" (nf S.evalHOAS sExpr')]  main = do b1 <- randStdBenchmarks 5           b2 <- randStdBenchmarks 10           b3 <- randStdBenchmarks 20           let b0 = standardBenchmarks (sExpr, aExpr, "hand-written")-          let b4 = map hoasBenchmaks [1,10,100,1000,10000]-          defaultMain $ [b0,b1,b2,b3] ++ b4--          --{--TODO - - benchmark generic functions (e.g. size, depth, breadth)---}+          defaultMain $ [b0,b1,b2,b3]

@@ -6,7 +6,8 @@   UndecidableInstances,   TypeOperators,   ScopedTypeVariables,-  TypeSynonymInstances #-}+  TypeSynonymInstances,+  DeriveFunctor#-}  module DataTypes.Comp      ( module DataTypes.Comp,@@ -21,6 +22,7 @@ import Data.Traversable import Test.QuickCheck.Arbitrary import Test.QuickCheck.Gen+import Test.QuickCheck.Property  import Control.Monad hiding (sequence_,mapM) import Prelude hiding (sequence_,mapM)@@ -46,12 +48,12 @@ data ValueT e = TInt               | TBool               | TPair e e-                deriving (Eq)+                deriving (Eq, Functor)  data Value e = VInt Int              | VBool Bool              | VPair e e-               deriving (Eq)+               deriving (Eq, Functor)  data Proj = ProjLeft | ProjRight             deriving (Eq)@@ -64,31 +66,31 @@           | And e e           | Not e           | Proj Proj e-            deriving (Eq)+            deriving (Eq, Functor)  data Sugar e = Neg e              | Minus e e              | Gt e e              | Or e e              | Impl e e-               deriving (Eq)+               deriving (Eq, Functor)  data FunT e = TFun e e-              deriving (Eq)+              deriving (Eq, Functor)  data Lam e = Lam (e -> e)  data App e = App e e-             deriving (Eq)+             deriving (Eq, Functor)  $(derive [instanceNFData, instanceArbitrary] [''Proj])  $(derive-  [instanceFunctor, instanceExpFunctor, instanceFoldable, instanceTraversable,+  [instanceFoldable, instanceTraversable,    instanceEqF, instanceNFDataF, instanceArbitraryF, smartConstructors]   [''Value, ''Op, ''Sugar, ''ValueT, ''FunT, ''App]) -$(derive [instanceExpFunctor, smartConstructors] [''Lam])+$(derive [smartConstructors] [''Lam])  instance EqF Lam where     eqF _ _ = False@@ -121,6 +123,13 @@     showF TBool = "Bool"     showF (TPair x y) = "(" ++ x ++ "," ++ y ++ ")" +instance ShowF Sugar where +    showF (Neg x) = "- " ++ x+    showF (Minus x y) = "(" ++ x ++ "-" ++ y ++ ")"+    showF (Gt x y) = "(" ++ x ++ ">" ++ y ++ ")"+    showF (Or x y) = "(" ++ x ++ "||" ++ y ++ ")"+    showF (Impl x y) = "(" ++ x ++ "->" ++ y ++ ")"+ instance ShowF Lam where      showF (Lam f) = "\\x. " ++ f "x" @@ -147,7 +156,11 @@ desize gen = sized (\n -> resize (max 0 (n-1)) gen)  genSomeTyped :: (Traversable f, GenTyped f) => Gen (Term f)-genSomeTyped = arbitrary >>= genTyped +genSomeTyped = arbitrary >>= genTyped++forAllTyped :: (GenTyped f, ShowF f, Testable prop, Traversable f) =>+               (Term f -> prop) -> Property+forAllTyped f = forAll genSomeTyped f   instance (GenTyped f, GenTyped g) => GenTyped (f :+: g) where

@@ -11,7 +11,6 @@ module DataTypes.Transform where  import Data.Comp-import Data.Comp.ExpFunctor import DataTypes.Standard as S import DataTypes.Comp @@ -49,35 +48,64 @@     transSugarAlg (Or x y) = POr x y     transSugarAlg (Impl x y) = PImpl x y -class TransHOAS f where-    transHOASAlg :: Alg f S.HOASExpr -transHOAS :: (ExpFunctor f, TransHOAS f) => Term f -> S.HOASExpr-transHOAS = cataE transHOASAlg -instance (TransHOAS f, TransHOAS g) => TransHOAS (f :+: g) where-    transHOASAlg (Inl v) = transHOASAlg v-    transHOASAlg (Inr v) = transHOASAlg v+class TransCore f where+    transCoreAlg :: Alg f OExpr -instance TransHOAS Value where-    transHOASAlg (VInt i) = HOASInt i-    transHOASAlg (VBool b) = HOASBool b-    transHOASAlg (VPair x y) = HOASPair x y+transCore :: (Functor f, TransCore f) => Term f -> OExpr+transCore = cata transCoreAlg -instance TransHOAS Op where-    transHOASAlg (Plus x y) = HOASPlus x y-    transHOASAlg (Mult x y) = HOASMult x y-    transHOASAlg (If b x y) = HOASIf b x y-    transHOASAlg (Lt x y) = HOASLt x y-    transHOASAlg (And x y) = HOASAnd x y-    transHOASAlg (Not x) = HOASNot x-    transHOASAlg (Proj p x) = HOASProj (ptrans p) x++instance (TransCore f, TransCore g) => TransCore (f :+: g) where+    transCoreAlg (Inl v) = transCoreAlg v+    transCoreAlg (Inr v) = transCoreAlg v++instance TransCore Value where+    transCoreAlg (VInt i) = OInt i+    transCoreAlg (VBool b) = OBool b+    transCoreAlg (VPair x y) = OPair x y++instance TransCore Op where+    transCoreAlg (Plus x y) = OPlus x y+    transCoreAlg (Mult x y) = OMult x y+    transCoreAlg (If b x y) = OIf b x y+    transCoreAlg (Lt x y) = OLt x y+    transCoreAlg (And x y) = OAnd x y+    transCoreAlg (Not x) = ONot x+    transCoreAlg (Proj p x) = OProj (ptrans p) x         where ptrans ProjLeft = SProjLeft               ptrans ProjRight = SProjRight-    transHOASAlg (Eq x y) = HOASEq x y+    transCoreAlg (Eq x y) = OEq x y -instance TransHOAS Lam where-    transHOASAlg (Lam f) = HOASLam $ f . HOASVal+class TransVal f where+    transValAlg :: Alg f SExpr -instance TransHOAS App where-    transHOASAlg (App x y) = HOASApp x y+transVal :: (Functor f, TransVal f) => Term f -> SExpr+transVal = cata transValAlg+++instance (TransVal f, TransVal g) => TransVal (f :+: g) where+    transValAlg (Inl v) = transValAlg v+    transValAlg (Inr v) = transValAlg v++instance TransVal Value where+    transValAlg (VInt i) = SInt i+    transValAlg (VBool b) = SBool b+    transValAlg (VPair x y) = SPair x y++class TransType f where+    transTypeAlg :: Alg f VType++transType :: (Functor f, TransType f) => Term f -> VType+transType = cata transTypeAlg+++instance (TransType f, TransType g) => TransType (f :+: g) where+    transTypeAlg (Inl v) = transTypeAlg v+    transTypeAlg (Inr v) = transTypeAlg v++instance TransType ValueT where+    transTypeAlg TInt = VTInt+    transTypeAlg TBool = VTBool+    transTypeAlg (TPair x y) = VTPair x y

@@ -16,59 +16,59 @@  -- de-sugar -class (Functor e, Traversable f) => Desugar f e where-    desugarAlg :: TermHom f e+class (Functor e, Traversable f) => Desug f e where+    desugAlg :: TermHom f e -desugarExpr :: SugarExpr -> Expr-desugarExpr = desugar+desugExpr :: SugarExpr -> Expr+desugExpr = desug -desugar :: Desugar f e => Term f -> Term e-{-# INLINE desugar #-}-desugar = appTermHom desugarAlg+desug :: Desug f e => Term f -> Term e+{-# INLINE desug #-}+desug = appTermHom desugAlg -instance (Desugar f e, Desugar g e) => Desugar (g :+: f) e where-    desugarAlg (Inl v) = desugarAlg v-    desugarAlg (Inr v) = desugarAlg v+instance (Desug f e, Desug g e) => Desug (g :+: f) e where+    desugAlg (Inl v) = desugAlg v+    desugAlg (Inr v) = desugAlg v -instance (Value :<: v, Functor v) => Desugar Value v where-    desugarAlg = liftCxt+instance (Value :<: v, Functor v) => Desug Value v where+    desugAlg = liftCxt -instance (Op :<: v, Functor v) => Desugar Op v where-    desugarAlg = liftCxt+instance (Op :<: v, Functor v) => Desug Op v where+    desugAlg = liftCxt -instance (Op :<: v, Value :<: v, Functor v) => Desugar Sugar v where-    desugarAlg (Neg x) =  iVInt (-1) `iMult` (Hole x)-    desugarAlg (Minus x y) =  (Hole x) `iPlus` ((iVInt (-1)) `iMult` (Hole y))-    desugarAlg (Gt x y) =  (Hole y) `iLt` (Hole x)-    desugarAlg (Or x y) = iNot (iNot (Hole x) `iAnd` iNot (Hole y))-    desugarAlg (Impl x y) = iNot ((Hole x) `iAnd` iNot (Hole y))+instance (Op :<: v, Value :<: v, Functor v) => Desug Sugar v where+    desugAlg (Neg x) =  iVInt (-1) `iMult` (Hole x)+    desugAlg (Minus x y) =  (Hole x) `iPlus` ((iVInt (-1)) `iMult` (Hole y))+    desugAlg (Gt x y) =  (Hole y) `iLt` (Hole x)+    desugAlg (Or x y) = iNot (iNot (Hole x) `iAnd` iNot (Hole y))+    desugAlg (Impl x y) = iNot ((Hole x) `iAnd` iNot (Hole y))   -- standard algebraic approach -class Desugar2 f g where-    desugarAlg2 :: Alg f (Term g)+class Desug2 f g where+    desugAlg2 :: Alg f (Term g) -desugarExpr2 :: SugarExpr -> Expr-desugarExpr2 = desugar2+desugExpr2 :: SugarExpr -> Expr+desugExpr2 = desug2 -desugar2 :: (Functor f, Desugar2 f g) => Term f -> Term g-desugar2 = cata desugarAlg2+desug2 :: (Functor f, Desug2 f g) => Term f -> Term g+desug2 = cata desugAlg2 -instance (Desugar2 f e, Desugar2 g e) => Desugar2 (f :+: g) e where-    desugarAlg2 (Inl v) = desugarAlg2 v-    desugarAlg2 (Inr v) = desugarAlg2 v+instance (Desug2 f e, Desug2 g e) => Desug2 (f :+: g) e where+    desugAlg2 (Inl v) = desugAlg2 v+    desugAlg2 (Inr v) = desugAlg2 v -instance (Value :<: v) => Desugar2 Value v where-    desugarAlg2 = inject+instance (Value :<: v) => Desug2 Value v where+    desugAlg2 = inject -instance (Op :<: v) => Desugar2 Op v where-    desugarAlg2 = inject+instance (Op :<: v) => Desug2 Op v where+    desugAlg2 = inject -instance (Op :<: v, Value :<: v, Functor v) => Desugar2 Sugar v where-    desugarAlg2 (Neg x) =  iVInt (-1) `iMult` x-    desugarAlg2 (Minus x y) =  x `iPlus` ((iVInt (-1)) `iMult` y)-    desugarAlg2 (Gt x y) =  y `iLt` x-    desugarAlg2 (Or x y) = iNot (iNot x `iAnd` iNot y)-    desugarAlg2 (Impl x y) = iNot (x `iAnd` iNot y)+instance (Op :<: v, Value :<: v, Functor v) => Desug2 Sugar v where+    desugAlg2 (Neg x) =  iVInt (-1) `iMult` x+    desugAlg2 (Minus x y) =  x `iPlus` ((iVInt (-1)) `iMult` y)+    desugAlg2 (Gt x y) =  y `iLt` x+    desugAlg2 (Or x y) = iNot (iNot x `iAnd` iNot y)+    desugAlg2 (Impl x y) = iNot (x `iAnd` iNot y) 

@@ -13,7 +13,6 @@ import DataTypes.Comp import Functions.Comp.Desugar import Data.Comp-import Data.Comp.ExpFunctor import Control.Monad import Data.Traversable @@ -136,15 +135,12 @@  -- evaluation2 -class ExpFunctor e => Eval2 e v where+class Functor e => Eval2 e v where     eval2Alg :: e (Term v) -> Term v  eval2 :: (Functor e, Eval2 e v) => Term e -> Term v eval2 = cata eval2Alg -eval2E :: (ExpFunctor e, Eval2 e v) => Term e -> Term v-eval2E = cataE eval2Alg- instance (Eval2 f v, Eval2 g v) => Eval2 (f :+: g) v where     eval2Alg (Inl v) = eval2Alg v     eval2Alg (Inr v) = eval2Alg v@@ -194,13 +190,7 @@     eval2Alg (Or x y) = (\ b c -> iVBool (b || c)) (coerceBool2 x) (coerceBool2 y)     eval2Alg (Impl x y) = (\ b c -> iVBool (not b || c)) (coerceBool2 x) (coerceBool2 y) -instance (Lam :<: v) => Eval2 Lam v where-    eval2Alg = inject -instance (Lam :<: v) => Eval2 App v where-    eval2Alg (App v1 v2) = (coerceLam2 v1) v2-- -- direct evaluation 2  class EvalDir2 e where@@ -259,40 +249,33 @@  -- desugar -desugarEval :: SugarExpr -> Err ValueExpr-desugarEval = eval . (desugar :: SugarExpr -> Expr)+desugEval :: SugarExpr -> Err ValueExpr+desugEval = eval . (desug :: SugarExpr -> Expr)   evalSugar :: SugarExpr -> Err ValueExpr evalSugar = eval -desugarEvalAlg  :: AlgM Err SugarSig ValueExpr-desugarEvalAlg = evalAlg  `compAlgM'` (desugarAlg :: TermHom SugarSig ExprSig)+desugEvalAlg  :: AlgM Err SugarSig ValueExpr+desugEvalAlg = evalAlg  `compAlgM'` (desugAlg :: TermHom SugarSig ExprSig)  -desugarEval' :: SugarExpr -> Err ValueExpr-desugarEval' = cataM desugarEvalAlg+desugEval' :: SugarExpr -> Err ValueExpr+desugEval' = cataM desugEvalAlg -desugarEval2 :: SugarExpr -> ValueExpr-desugarEval2 = eval2 . (desugar :: SugarExpr -> Expr)+desugEval2 :: SugarExpr -> ValueExpr+desugEval2 = eval2 . (desug :: SugarExpr -> Expr) -desugarEval2E :: SugarExpr -> ValueExpr-desugarEval2E = eval2E . (desugar :: SugarExpr -> Expr)   evalSugar2 :: SugarExpr -> ValueExpr evalSugar2 = eval2 -evalSugar2E :: SugarExpr -> ValueExpr-evalSugar2E = eval2E  -desugarEval2Alg  :: Alg SugarSig ValueExpr-desugarEval2Alg = eval2Alg  `compAlg` (desugarAlg :: TermHom SugarSig ExprSig)+desugEval2Alg  :: Alg SugarSig ValueExpr+desugEval2Alg = eval2Alg  `compAlg` (desugAlg :: TermHom SugarSig ExprSig)  -desugarEval2' :: SugarExpr -> ValueExpr-desugarEval2' = cata desugarEval2Alg--desugarEval2E' :: SugarExpr -> ValueExpr-desugarEval2E' = cataE desugarEval2Alg+desugEval2' :: SugarExpr -> ValueExpr+desugEval2' = cata desugEval2Alg

@@ -35,16 +35,11 @@     inferTypeAlg (VBool _) = return $ inject TBool     inferTypeAlg (VPair x y) = return $ inject $ TPair x y -check:: (g :<: f, Eq (g (Term f)), Monad m) =>-        g (Term f) -> Term f -> m ()-check f t = if project t == Just f then return () else fail ""--checkEq :: (Eq a, Monad m) => a -> a -> m ()-checkEq x y = if x == y then return () else fail ""- checkOp :: (g :<: f, Eq (g (Term f)), Monad m) =>            [g (Term f)] -> g (Term f) -> [Term f] -> m (Term f)-checkOp exs ret tys = sequence_ (zipWith check exs tys) >> return $ inject ret+checkOp exs et tys = if and (zipWith (\ f t -> maybe False (==f) (project t)) exs tys) +                     then return (inject et)+                     else fail""   instance (ValueT :<: t, EqF t, Monad m) => InferType Op t m where@@ -53,13 +48,15 @@     inferTypeAlg (Lt x y) = checkOp [TInt,TInt] TBool [x ,y]     inferTypeAlg (And x y) = checkOp [TBool,TBool] TBool [x ,y]     inferTypeAlg (Not x) = checkOp [TBool] TBool [x]-    inferTypeAlg (If b x y) = check TBool b >> checkEq x y >> return x-    inferTypeAlg (Eq x y) = checkEq x y >> return $ iTBool+    inferTypeAlg (If b x y) = case project b of+                                 Just TBool | x == y -> return x+                                 _ -> fail "" +    inferTypeAlg (Eq x y) = if x == y then return iTBool else fail ""     inferTypeAlg (Proj p x) = case project x of-                                Just (TPair x1 x2) -> return $+                                Just (TPair x1 x2) ->                                      case p of-                                      ProjLeft -> x1-                                      ProjRight -> x2+                                      ProjLeft -> return x1+                                      ProjRight -> return x2                                 _ -> fail ""  instance (ValueT :<: t, EqF t, Monad m) => InferType Sugar t m where@@ -69,17 +66,17 @@     inferTypeAlg (Or x y) = checkOp [TBool,TBool] TBool [x ,y]     inferTypeAlg (Impl x y) = checkOp [TBool,TBool] TBool [x ,y] -desugarType :: SugarExpr -> Err BaseType-desugarType = inferType . (desugar :: SugarExpr -> Expr)+desugType :: SugarExpr -> Err BaseType+desugType = inferType . (desug :: SugarExpr -> Expr)  typeSugar :: SugarExpr -> Err BaseType typeSugar = inferType -desugarTypeAlg  :: AlgM Err SugarSig BaseType-desugarTypeAlg = inferTypeAlg  `compAlgM'` (desugarAlg :: TermHom SugarSig ExprSig)+desugTypeAlg  :: AlgM Err SugarSig BaseType+desugTypeAlg = inferTypeAlg  `compAlgM'` (desugAlg :: TermHom SugarSig ExprSig) -desugarType' :: SugarExpr -> Err BaseType-desugarType' e = cataM desugarTypeAlg e+desugType' :: SugarExpr -> Err BaseType+desugType' e = cataM desugTypeAlg e  -- pure type inference @@ -101,19 +98,11 @@     inferTypeAlg2 (VBool _) = inject TBool     inferTypeAlg2 (VPair x y) = inject $ TPair x y -check2:: (g :<: f, Eq (g (Term f))) =>-        g (Term f) -> Term f -> a -> a-check2 f t z = if project t == Just f then z else error ""--checkEq2 :: (Eq a) => a -> a -> b -> b-checkEq2 x y z = if x == y then z else error ""--runCheck :: [a -> a] -> a -> a-runCheck = foldr (.) id- checkOp2 :: (g :<: f, Eq (g (Term f))) =>            [g (Term f)] -> g (Term f) -> [Term f] -> (Term f)-checkOp2 exs ret tys = runCheck (zipWith check2 exs tys) (inject ret)+checkOp2 exs ret tys = if and (zipWith (\ f t -> maybe False (==f) (project t)) exs tys)+                       then inject ret+                       else error ""   instance (ValueT :<: t, EqF t) => InferType2 Op t where@@ -122,8 +111,10 @@     inferTypeAlg2 (Lt x y) = checkOp2 [TInt,TInt] TBool [x ,y]     inferTypeAlg2 (And x y) = checkOp2 [TBool,TBool] TBool [x ,y]     inferTypeAlg2 (Not x) = checkOp2 [TBool] TBool [x]-    inferTypeAlg2 (If b x y) = checkEq2 x y $ check2 TBool b $ x-    inferTypeAlg2 (Eq x y) = checkEq2 x y $ iTBool+    inferTypeAlg2 (If b x y) = case project b of+                                 Just TBool | x == y -> x+                                 _ -> error ""+    inferTypeAlg2 (Eq x y) = if x == y then iTBool else error ""     inferTypeAlg2 (Proj p x) = case project x of                                 Just (TPair x1 x2) ->                                      case p of@@ -138,14 +129,14 @@     inferTypeAlg2 (Or x y) = checkOp2 [TBool,TBool] TBool [x ,y]     inferTypeAlg2 (Impl x y) = checkOp2 [TBool,TBool] TBool [x ,y] -desugarType2 :: SugarExpr -> BaseType-desugarType2 = inferType2 . (desugar :: SugarExpr -> Expr)+desugType2 :: SugarExpr -> BaseType+desugType2 = inferType2 . (desug :: SugarExpr -> Expr)  typeSugar2 :: SugarExpr -> BaseType typeSugar2 = inferType2 -desugarTypeAlg2  :: Alg SugarSig BaseType-desugarTypeAlg2 = inferTypeAlg2  `compAlg` (desugarAlg :: TermHom SugarSig ExprSig)+desugTypeAlg2  :: Alg SugarSig BaseType+desugTypeAlg2 = inferTypeAlg2  `compAlg` (desugAlg :: TermHom SugarSig ExprSig) -desugarType2' :: SugarExpr -> Err BaseType-desugarType2' e = cataM desugarTypeAlg e+desugType2' :: SugarExpr -> BaseType+desugType2' e = cata desugTypeAlg2 e

@@ -4,20 +4,20 @@  -- de-sugar -desugar :: PExpr -> OExpr-desugar (PInt i) = OInt i-desugar (PBool b) = OBool b-desugar (PPair x y) = OPair (desugar x) (desugar y)-desugar (PPlus x y) = OPlus (desugar x) (desugar y)-desugar (PMult x y) = OMult (desugar x) (desugar y)-desugar (PIf b x y) = OIf (desugar b) (desugar x) (desugar y)-desugar (PEq x y) = OEq (desugar x) (desugar y)-desugar (PLt x y) = OLt (desugar x) (desugar y)-desugar (PAnd x y) = OAnd (desugar x) (desugar y)-desugar (PNot x) = ONot (desugar x)-desugar (PProj p x) = OProj p (desugar x)-desugar (PNeg x) = OInt (-1) `OMult` (desugar x)-desugar (PMinus x y) = (desugar x) `OPlus` ((OInt (-1)) `OMult` (desugar y))-desugar (PGt x y) = (desugar y) `OLt` (desugar x)-desugar (POr x y) = ONot (ONot (desugar x) `OAnd` ONot (desugar y))-desugar (PImpl x y) = ONot ((desugar x) `OAnd` ONot (desugar y))+desug :: PExpr -> OExpr+desug (PInt i) = OInt i+desug (PBool b) = OBool b+desug (PPair x y) = OPair (desug x) (desug y)+desug (PPlus x y) = OPlus (desug x) (desug y)+desug (PMult x y) = OMult (desug x) (desug y)+desug (PIf b x y) = OIf (desug b) (desug x) (desug y)+desug (PEq x y) = OEq (desug x) (desug y)+desug (PLt x y) = OLt (desug x) (desug y)+desug (PAnd x y) = OAnd (desug x) (desug y)+desug (PNot x) = ONot (desug x)+desug (PProj p x) = OProj p (desug x)+desug (PNeg x) = OInt (-1) `OMult` (desug x)+desug (PMinus x y) = (desug x) `OPlus` ((OInt (-1)) `OMult` (desug y))+desug (PGt x y) = (desug y) `OLt` (desug x)+desug (POr x y) = ONot (ONot (desug x) `OAnd` ONot (desug y))+desug (PImpl x y) = ONot ((desug x) `OAnd` ONot (desug y))

@@ -53,8 +53,8 @@ evalSugar (POr x y) = liftM2 (\ x y -> SBool (x || y)) (evalSugar x >>= coerceBool) (evalSugar y >>= coerceBool) evalSugar (PImpl x y) = liftM2 (\ x y -> SBool (not x || y)) (evalSugar x >>= coerceBool) (evalSugar y >>= coerceBool) -desugarEval :: PExpr -> Err SExpr-desugarEval = eval . desugar+desugEval :: PExpr -> Err SExpr+desugEval = eval . desug   coerceInt2 :: SExpr -> Int@@ -107,8 +107,8 @@ evalSugar2 (POr x y) = (\ x y -> SBool (x || y)) (coerceBool2 $ evalSugar2 x) (coerceBool2 $ evalSugar2 y) evalSugar2 (PImpl x y) = (\ x y -> SBool (not x || y)) (coerceBool2 $ evalSugar2 x) (coerceBool2 $ evalSugar2 y) -desugarEval2 :: PExpr -> SExpr-desugarEval2 = eval2 . desugar+desugEval2 :: PExpr -> SExpr+desugEval2 = eval2 . desug   

@@ -75,8 +75,8 @@ typeSugar (POr x y) = checkOpP [VTBool,VTBool] VTBool [x,y] typeSugar (PImpl x y) = checkOpP [VTBool,VTBool] VTBool [x,y] -desugarType :: PExpr -> Err VType-desugarType = inferType . desugar+desugType :: PExpr -> Err VType+desugType = inferType . desug  -- non-monadic @@ -149,5 +149,5 @@ typeSugar2 (POr x y) = checkOpP2 [VTBool,VTBool] VTBool [x,y] typeSugar2 (PImpl x y) = checkOpP2 [VTBool,VTBool] VTBool [x,y] -desugarType2 :: PExpr -> VType-desugarType2 = inferType2 . desugar+desugType2 :: PExpr -> VType+desugType2 = inferType2 . desug

@@ -0,0 +1,61 @@+module Main where++import qualified Functions.Comp as A+import qualified Functions.Standard as S+import DataTypes.Comp+import DataTypes.Transform+import Test.QuickCheck+import Data.List++main = mapM_ (quickCheckWith stdArgs{maxSize=10}) allProp++allProp = map forAllTyped [prop_desug, prop_desugAlg, prop_desugType, prop_desugType', prop_typeSugar, prop_desugType2, prop_desugType2', prop_typeSugar2, prop_desugEval, prop_desugEval', prop_evalSugar, prop_evalSugar, prop_evalDirect, prop_desugEval2, prop_desugEval2', prop_evalSugar2, prop_evalDirect2, prop_freeVars, prop_freeVars', prop_freeVarsGen, prop_freeVarsGenS]+          ++ map forAllTyped [prop_contVar, prop_contVar', prop_contVarGen, prop_contVarGenS]++prop_desug x = transCore (A.desugExpr x) == S.desug (transSugar x)++prop_desugAlg x = transCore (A.desugExpr2 x) == S.desug (transSugar x)++prop_desugType x = fmap transType (A.desugType x) == S.desugType (transSugar x)++prop_desugType' x = fmap transType (A.desugType' x) == S.desugType (transSugar x)++prop_typeSugar x = fmap transType (A.typeSugar x) == S.typeSugar (transSugar x)++prop_desugType2 x = transType (A.desugType2 x) == S.desugType2 (transSugar x)++prop_desugType2' x = transType (A.desugType2' x) == S.desugType2 (transSugar x)++prop_typeSugar2 x = transType (A.typeSugar2 x) == S.typeSugar2 (transSugar x)++prop_desugEval x = fmap transVal (A.desugEval x) == S.desugEval (transSugar x)++prop_desugEval' x = fmap transVal (A.desugEval' x) == S.desugEval (transSugar x)++prop_evalSugar x = fmap transVal (A.evalSugar x) == S.evalSugar (transSugar x)++prop_evalDirect x = fmap transVal (A.evalDirect x) == S.evalSugar (transSugar x)++prop_desugEval2 x = transVal (A.desugEval2 x) == S.desugEval2 (transSugar x)++prop_desugEval2' x = transVal (A.desugEval2' x) == S.desugEval2 (transSugar x)++prop_evalSugar2 x = transVal (A.evalSugar2 x) == S.evalSugar2 (transSugar x)++prop_evalDirect2 x = transVal (A.evalDirect2 x) == S.evalSugar2 (transSugar x)++prop_contVar x v = A.contVar v x == S.contVar v (transSugar x)++prop_contVar' x v = A.contVar' v x == S.contVar v (transSugar x)++prop_contVarGen x v = A.contVarGen v x == S.contVar v (transSugar x)++prop_contVarGenS x v = S.contVarGen v (transSugar x) == S.contVar v (transSugar x)++prop_freeVars x = A.freeVars x == S.freeVars (transSugar x)++prop_freeVars' x = A.freeVars' x == S.freeVars (transSugar x)++prop_freeVarsGen x = sort (A.freeVarsGen x) == sort (S.freeVars (transSugar x))++prop_freeVarsGenS x = S.freeVarsGen (transSugar x) == S.freeVars (transSugar x)

@@ -1,5 +1,5 @@ Name:			compdata-Version:		0.1+Version:		0.2 Synopsis:            	Compositional Data Types Description: @@ -54,10 +54,6 @@      includes /short-cut fusion/ style optimisation rules which yield a      performance boost of up to factor six.   .-  *  Efficient implementation of catamorphisms on non-polynomial-     signatures that contain function types. This allows to represent-     /higher-order abstract syntax/ with compositional data types.-  .   *  Automatic derivation of instances of all relevant type classes for      using compositional data types via /Template Haskell/. This includes      instances of 'Prelude.Eq', 'Prelude.Ord' and 'Prelude.Show' that are@@ -86,6 +82,7 @@   testsuite/tests/Data/Comp/Equality_Test.hs,   testsuite/tests/Test/Utils.hs   -- benchmark files+  benchmark/Test.hs   benchmark/Benchmark.hs   benchmark/DataTypes.hs   benchmark/Functions.hs@@ -126,25 +123,24 @@                         Data.Comp.Decompose, Data.Comp.Unification,                         Data.Comp.Derive, Data.Comp.Matching, Data.Comp.Multi,                         Data.Comp.Multi.Term, Data.Comp.Multi.Sum,-                        Data.Comp.Multi.Functor, Data.Comp.Multi.ExpFunctor,+                        Data.Comp.Multi.Functor,                         Data.Comp.Multi.Foldable, Data.Comp.Multi.Traversable,                         Data.Comp.Multi.Algebra,                         Data.Comp.Multi.Product, Data.Comp.Multi.Show,                         Data.Comp.Multi.Equality, Data.Comp.Multi.Variables,-                        Data.Comp.Multi.Ops, Data.Comp.Ops, Data.Comp.ExpFunctor+                        Data.Comp.Multi.Ops, Data.Comp.Ops    Other-Modules:        Data.Comp.Derive.Utils, Data.Comp.Derive.Equality,                         Data.Comp.Derive.Ordering, Data.Comp.Derive.Arbitrary,                         Data.Comp.Derive.Show, Data.Comp.Derive.DeepSeq,                         Data.Comp.Derive.SmartConstructors,-                        Data.Comp.Derive.Foldable, Data.Comp.Derive.ExpFunctor,+                        Data.Comp.Derive.Foldable,                         Data.Comp.Derive.Traversable,                         Data.Comp.Derive.Multi.Functor,                         Data.Comp.Derive.Multi.Foldable,                         Data.Comp.Derive.Multi.Traversable,                         Data.Comp.Derive.Multi.Equality,                         Data.Comp.Derive.Multi.Show,-                        Data.Comp.Derive.Multi.ExpFunctor,                         Data.Comp.Derive.Multi.SmartConstructors    Build-Depends:	base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, th-expand-syns

@@ -27,8 +27,6 @@   -- ** Lifting Term Homomorphisms to Products   -- $ex4 -  -- ** Higher-Order Abstract Syntax-  -- $ex5     module Data.Comp.Term   , module Data.Comp.Algebra   , module Data.Comp.Sum

@@ -91,20 +91,13 @@       CVCoalg',       futu',       CVCoalgM,-      futuM,--      -- * Exponential Functors-      appTermHomE,-      cataE,-      anaE,-      appCxtE+      futuM     ) where  import Data.Comp.Term import Data.Comp.Ops import Data.Traversable import Control.Monad hiding (sequence, mapM)-import Data.Comp.ExpFunctor  import Prelude hiding (sequence, mapM) @@ -513,40 +506,7 @@     where run :: a -> Term f           run x = appCxt $ fmap run (coa x) ------------------------------ Exponential Functors ----------------------------- -{-| Catamorphism for exponential functors. The intermediate 'cataFS' originates- from <http://comonad.com/reader/2008/rotten-bananas/>. -}-cataE :: forall f a . ExpFunctor f => Alg f a -> Term f -> a-{-# NOINLINE [1] cataE #-}-cataE f = cataFS . toCxt-    where cataFS :: ExpFunctor f => Context f a -> a-          cataFS (Hole x) = x-          cataFS (Term t) = f (xmap cataFS Hole t)--{-| Anamorphism for exponential functors. -}-anaE :: forall a f . ExpFunctor f => Coalg f a -> a -> Term f-anaE f = cataE (Term . removeP) . anaFS-    where anaFS :: a -> Term (f :&: a)-          anaFS t = Term $ xmap anaFS (snd . projectP . unTerm) (f t) :&: t---- | Variant of 'appCxt' for contexts over 'ExpFunctor' signatures.-appCxtE :: (ExpFunctor f) => Context f (Cxt h f a) -> Cxt h f a-appCxtE (Hole x) = x-appCxtE (Term t) = Term (xmap appCxtE Hole t)---- | Variant of 'appTermHom' for term homomorphisms from and to--- 'ExpFunctor' signatures.-appTermHomE :: forall f g . (ExpFunctor f, ExpFunctor g) => TermHom f g-            -> Term f -> Term g-appTermHomE f = cataFS . toCxt-    where cataFS :: Context f (Term g) -> Term g-          cataFS (Hole x) = x-          cataFS (Term t) = appCxtE (f (xmap cataFS Hole t))-- ------------------- -- rewrite rules -- -------------------@@ -558,9 +518,6 @@    "appTermHom/appTermHom" forall (a :: TermHom g h) (h :: TermHom f g) x.     appTermHom a (appTermHom h x) = appTermHom (compTermHom a h) x;--  "cataE/appTermHom" forall (a :: Alg g d) (h :: TermHom f g) (x :: ExpFunctor f => Term f) .-    cataE a (appTermHom h x) = cataE (compAlg a h) x  #-}  {-# RULES 

@@ -33,8 +33,6 @@      module Data.Comp.Derive.Foldable,      -- ** Traversable      module Data.Comp.Derive.Traversable,-     -- ** ExpFunctor-     module Data.Comp.Derive.ExpFunctor,      -- ** Arbitrary      module Data.Comp.Derive.Arbitrary,      NFData(..),@@ -58,8 +56,6 @@      module Data.Comp.Derive.Multi.Foldable,      -- ** HTraversable      module Data.Comp.Derive.Multi.Traversable,-     -- ** HExpFunctor-     module Data.Comp.Derive.Multi.ExpFunctor,      -- ** Smart Constructors      module Data.Comp.Derive.Multi.SmartConstructors     ) where@@ -67,7 +63,6 @@ import Control.DeepSeq (NFData(..)) import Data.Comp.Derive.Foldable import Data.Comp.Derive.Traversable-import Data.Comp.Derive.ExpFunctor import Data.Comp.Derive.DeepSeq import Data.Comp.Derive.Show import Data.Comp.Derive.Ordering@@ -79,7 +74,6 @@ import Data.Comp.Derive.Multi.Functor import Data.Comp.Derive.Multi.Foldable import Data.Comp.Derive.Multi.Traversable-import Data.Comp.Derive.Multi.ExpFunctor import Data.Comp.Derive.Multi.SmartConstructors  import Language.Haskell.TH

@@ -106,13 +106,13 @@                                    build) |]  {-|-  This function generates a declaration for the method 'shrink' using the given constructors.+  This function generates a declaration for the method 'shrinkF' using the given constructors.   The constructors are supposed to belong to the same type. -} generateShrinkFDecl :: [Con] -> Q Dec generateShrinkFDecl constrs     = let clauses = map (generateClause.abstractConType) constrs-      in funD 'shrink clauses+      in funD 'shrinkF clauses   where generateClause (constr, n)             = do varNs <- newNames n "x"                  resVarNs <- newNames n "x'"

@@ -1,105 +0,0 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Comp.Derive.ExpFunctor--- Copyright   :  (c) 2011 Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Automatically derive instances of @ExpFunctor@.--------------------------------------------------------------------------------------module Data.Comp.Derive.ExpFunctor-    (-     ExpFunctor,-     instanceExpFunctor-    ) where--import Data.Comp.ExpFunctor-import Data.Comp.Derive.Utils-import Language.Haskell.TH--{-| Derive an instance of 'ExpFunctor' for a type constructor of any first-order-  kind taking at least one argument. -}-instanceExpFunctor :: Name -> Q [Dec]-instanceExpFunctor fname = do-  -- Comments below apply to the example where name = T, args = [a,b], and-  -- constrs = [(X,[a]), (Y,[a,b]), (Z,[b -> b])], i.e. the data type-  -- declaration: T a b = X a | Y a b | Z (b -> b)-  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname-  -- fArg = b-  let fArg :: Name = tyVarBndrName $ last args-  -- argNames = [a]-  let argNames = map (VarT . tyVarBndrName) (init args)-  -- compType = T a-  let complType = foldl AppT (ConT name) argNames-  -- classType = ExpFunctor (T a)-  let classType = AppT (ConT ''ExpFunctor) complType-  -- constrs' = [(X,[a]), (Y,[a,b]), (Z,[b -> b])]-  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs-  xmapDecl <- funD 'xmap (map (xmapClause fArg) constrs')-  return [InstanceD [] classType [xmapDecl]]-      where xmapClause :: Name -> (Name,[Type]) -> ClauseQ-            xmapClause fArg (constr, args) = do-              fn <- newName "_f"-              gn <- newName "_g"-              varNs <- newNames (length args) "x"-              let f = varE fn-              let g = varE gn-              let fp = VarP fn-              let gp = VarP gn-              -- Pattern for the constructor-              let pat = ConP constr $ map VarP varNs-              body <- xmapArgs fArg f g (zip varNs args) (conE constr)-              return $ Clause [fp, gp, pat] (NormalB body) []-            xmapArgs :: Name -> ExpQ -> ExpQ -> [(Name, Type)] -> ExpQ -> ExpQ-            xmapArgs _ _ _ [] acc =-                acc-            xmapArgs fArg f g ((x,tp):tps) acc =-                xmapArgs fArg f g tps (acc `appE`-                                       (xmapArg fArg tp f g `appE` varE x))-            -- Given the name of the functor variable, a type, and the two-            -- arguments to xmap, return the expression that should be applied-            -- to the parameter of the given type.-            -- Example: xmapArg b (b -> b) f g yields the expression-            -- [|\x -> f . x . g|]-            xmapArg :: Name -> Type -> ExpQ -> ExpQ -> ExpQ-            xmapArg fArg tp f g =-                -- No need to descend into tp if it does not contain the functor-                -- type variable-                if not $ containsType tp (VarT fArg) then-                    [|id|]-                else-                    case tp of-                      ForallT vars _ tp' ->-                          -- Check if the functor variable has been rebound-                          if any ((==) fArg . tyVarBndrName) vars then-                              [|id|]-                          else-                              xmapArg fArg tp' f g-                      VarT a ->-                          -- Apply f if we have reached the functor variable-                          if a == fArg then f else [|id|]-                      ConT _ ->-                          [|id|]-                      AppT (AppT ArrowT tp1) tp2 -> do-                          -- Note that f and g are swapped in the contravariant-                          -- type tp1-                          xn <- newName "x"-                          let ftp1 = xmapArg fArg tp1 g f-                          let ftp2 = xmapArg fArg tp2 f g-                          lamE [varP xn]-                               (infixE (Just ftp2)-                                       [|(.)|]-                                       (Just $ infixE (Just $ varE xn)-                                                      [|(.)|]-                                                      (Just ftp1)))-                      AppT _ tp' ->-                          [|fmap|] `appE` xmapArg fArg tp' f g-                      SigT tp' _ ->-                          xmapArg fArg tp' f g-                      _ ->-                          error $ "unsopported type: " ++ show tp

@@ -1,94 +0,0 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Comp.Derive.Multi.ExpFunctor--- Copyright   :  (c) 2011 Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Automatically derive instances of @HExpFunctor@.--------------------------------------------------------------------------------------module Data.Comp.Derive.Multi.ExpFunctor-    (-     HExpFunctor,-     instanceHExpFunctor-    ) where--import Data.Comp.Multi.ExpFunctor-import Data.Comp.Derive.Utils-import Language.Haskell.TH--{-| Derive an instance of 'HExpFunctor' for a type constructor of any - higher-order kind taking at least two arguments. -}-instanceHExpFunctor :: Name -> Q [Dec]-instanceHExpFunctor fname = do-  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname-  let args' = init args-  let fArg :: Name = tyVarBndrName $ last args'-  let argNames = map (VarT . tyVarBndrName) (init args')-  let complType = foldl AppT (ConT name) argNames-  let classType = AppT (ConT ''HExpFunctor) complType-  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs-  hxmapDecl <- funD 'hxmap (map (hxmapClause fArg) constrs')-  return [InstanceD [] classType [hxmapDecl]]-      where hxmapClause :: Name -> (Name,[Type]) -> ClauseQ-            hxmapClause fArg (constr, args) = do-              fn <- newName "_f"-              gn <- newName "_g"-              varNs <- newNames (length args) "x"-              let f = varE fn-              let g = varE gn-              let fp = VarP fn-              let gp = VarP gn-              -- Pattern for the constructor-              let pat = ConP constr $ map VarP varNs-              body <- hxmapArgs fArg f g (zip varNs args) (conE constr)-              return $ Clause [fp, gp, pat] (NormalB body) []-            hxmapArgs :: Name -> ExpQ -> ExpQ -> [(Name, Type)] -> ExpQ -> ExpQ-            hxmapArgs _ _ _ [] acc =-                acc-            hxmapArgs fArg f g ((x,tp):tps) acc =-                hxmapArgs fArg f g tps (acc `appE`-                                       (hxmapArg fArg tp f g `appE` varE x))-            hxmapArg :: Name -> Type -> ExpQ -> ExpQ -> ExpQ-            hxmapArg fArg tp f g =-                -- No need to descend into tp if it does not contain the -                -- higher-order functor type variable-                if not $ containsType tp (VarT fArg) then-                    [|id|]-                else-                    case tp of-                      ForallT vars _ tp' ->-                          -- Check if the variable has been rebound-                          if any ((==) fArg . tyVarBndrName) vars then-                              [|id|]-                          else-                              hxmapArg fArg tp' f g-                      (AppT (VarT a) _) ->-                          -- Apply f if we have reached the higher-order functor-                          -- variable-                          if a == fArg then f else [|id|]-                      ConT _ ->-                          [|id|]-                      AppT (AppT ArrowT tp1) tp2 -> do-                          -- Note that f and g are swapped in the contravariant-                          -- type tp1-                          xn <- newName "x"-                          let ftp1 = hxmapArg fArg tp1 g f-                          let ftp2 = hxmapArg fArg tp2 f g-                          lamE [varP xn]-                               (infixE (Just ftp2)-                                       [|(.)|]-                                       (Just $ infixE (Just $ varE xn)-                                                      [|(.)|]-                                                      (Just ftp1)))-                      AppT _ tp' ->-                          [|fmap|] `appE` hxmapArg fArg tp' f g-                      SigT tp' _ ->-                          hxmapArg fArg tp' f g-                      _ ->-                          error $ "unsopported type: " ++ show tp

@@ -27,7 +27,7 @@ {-| Signature printing. An instance @HShowF f@ gives rise to an instance   @KShow (HTerm f)@. -} class HShowF f where-    hshowF :: HAlg f (K String)+    hshowF :: Alg f (K String)     hshowF = K . hshowF'     hshowF' :: f (K String) :=> String     hshowF' = unK . hshowF

@@ -16,7 +16,7 @@ module Data.Comp.Derive.Multi.SmartConstructors      (smartHConstructors) where -import Language.Haskell.TH+import Language.Haskell.TH hiding (Cxt) import Data.Comp.Derive.Utils import Data.Comp.Multi.Sum import Data.Comp.Multi.Term@@ -25,7 +25,7 @@  {-| Derive smart constructors for a type constructor of any higher-order kind  taking at least two arguments. The smart constructors are similar to the- ordinary constructors, but an 'hinject' is automatically inserted. -}+ ordinary constructors, but an 'inject' is automatically inserted. -} smartHConstructors :: Name -> Q [Dec] smartHConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname@@ -40,7 +40,7 @@                     vars = map varE varNs                     val = foldl appE (conE name) vars                     sig = genSig targs tname sname args-                    function = [funD sname [clause pats (normalB [|hinject $val|]) []]]+                    function = [funD sname [clause pats (normalB [|inject $val|]) []]]                 sequence $ sig ++ function               genSig targs tname sname 0 = (:[]) $ do                 fvar <- newName "f"@@ -54,8 +54,8 @@                     a = varT avar                     i = varT ivar                     ftype = foldl appT (conT tname) (map varT targs')-                    constr = classP ''(:<<:) [ftype, f]-                    typ = foldl appT (conT ''HCxt) [h, f, a, i]+                    constr = classP ''(:<:) [ftype, f]+                    typ = foldl appT (conT ''Cxt) [h, f, a, i]                     typeSig = forallT (map PlainTV vars) (sequence [constr]) typ                 sigD sname typeSig               genSig _ _ _ _ = []

@@ -1,21 +0,0 @@------------------------------------------------------------------------------------ |--- Module	: Data.Comp.ExpFunctor--- Copyright 	: 2008 Edward Kmett--- License	: BSD------ Maintainer	: Tom Hvitved <hvitved@diku.dk>--- Stability	: unknown--- Portability	: unknown------ Exponential functors, see <http://comonad.com/reader/2008/rotten-bananas/>.-----------------------------------------------------------------------------------module Data.Comp.ExpFunctor-    ( ExpFunctor(..)-    ) where--{-| Exponential functors are functors that may be both covariant (as ordinary- functors) and contravariant. -}-class ExpFunctor f where-    xmap :: (a -> b) -> (b -> a) -> f a -> f b

@@ -25,9 +25,6 @@    -- ** Lifting Term Homomorphisms to Products   -- $ex4--  -- ** Higher-Order Abstract Syntax-  -- $ex5     module Data.Comp.Multi.Term   , module Data.Comp.Multi.Algebra   , module Data.Comp.Multi.Functor@@ -66,7 +63,7 @@ >   Snd        ::          e (s,t) -> Op e t > > -- Signature for the simple expression language-> type Sig = Op :++: Value+> type Sig = Op :+: Value >  > -- Derive boilerplate code using Template Haskell (GHC 7 needed) > $(derive [instanceHFunctor, instanceHShowF, smartHConstructors] @@ -74,34 +71,34 @@ >  > -- Term evaluation algebra > class Eval f v where->   evalAlg :: HAlg f (HTerm v)+>   evalAlg :: Alg f (HTerm v) > -> instance (Eval f v, Eval g v) => Eval (f :++: g) v where->   evalAlg (HInl x) = evalAlg x->   evalAlg (HInr x) = evalAlg x+> instance (Eval f v, Eval g v) => Eval (f :+: g) v where+>   evalAlg (Inl x) = evalAlg x+>   evalAlg (Inr x) = evalAlg x >  > -- Lift the evaluation algebra to a catamorphism-> eval :: (HFunctor f, Eval f v) => HTerm f :-> HTerm v-> eval = hcata evalAlg+> eval :: (HFunctor f, Eval f v) => Term f :-> Term v+> eval = cata evalAlg > -> instance (Value :<<: v) => Eval Value v where->   evalAlg = hinject+> instance (Value :<: v) => Eval Value v where+>   evalAlg = inject > -> instance (Value :<<: v) => Eval Op v where+> instance (Value :<: v) => Eval Op v where >   evalAlg (Add x y)  = iConst $ (projC x) + (projC y) >   evalAlg (Mult x y) = iConst $ (projC x) * (projC y) >   evalAlg (Fst x)    = fst $ projP x >   evalAlg (Snd x)    = snd $ projP x > -> projC :: (Value :<<: v) => HTerm v Int -> Int-> projC v = case hproject v of Just (Const n) -> n+> projC :: (Value :<: v) => Term v Int -> Int+> projC v = case project v of Just (Const n) -> n > -> projP :: (Value :<<: v) => HTerm v (s,t) -> (HTerm v s, HTerm v t)-> projP v = case hproject v of Just (Pair x y) -> (x,y)+> projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)+> projP v = case project v of Just (Pair x y) -> (x,y) >  > -- Example: evalEx = iConst 2-> evalEx :: HTerm Value Int-> evalEx = eval (iFst $ iPair (iConst 2) (iConst 1) :: HTerm Sig Int)+> evalEx :: Term Value Int+> evalEx = eval (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int) -}  {- $ex2@@ -130,7 +127,7 @@ >   Snd        ::          e (s,t) -> Op e t >  > -- Signature for the simple expression language-> type Sig = Op :++: Value+> type Sig = Op :+: Value >  > -- Derive boilerplate code using Template Haskell (GHC 7 needed) > $(derive [instanceHFunctor, instanceHTraversable, instanceHFoldable,@@ -139,20 +136,20 @@ >  > -- Monadic term evaluation algebra > class EvalM f v where->   evalAlgM :: HAlgM Maybe f (HTerm v)+>   evalAlgM :: AlgM Maybe f (Term v) > -> instance (EvalM f v, EvalM g v) => EvalM (f :++: g) v where->   evalAlgM (HInl x) = evalAlgM x->   evalAlgM (HInr x) = evalAlgM x+> instance (EvalM f v, EvalM g v) => EvalM (f :+: g) v where+>   evalAlgM (Inl x) = evalAlgM x+>   evalAlgM (Inr x) = evalAlgM x > -> evalM :: (HTraversable f, EvalM f v) => HTerm f l->                                      -> Maybe (HTerm v l)-> evalM = hcataM evalAlgM+> evalM :: (HTraversable f, EvalM f v) => Term f l+>                                      -> Maybe (Term v l)+> evalM = cataM evalAlgM > -> instance (Value :<<: v) => EvalM Value v where->   evalAlgM = return . hinject+> instance (Value :<: v) => EvalM Value v where+>   evalAlgM = return . inject > -> instance (Value :<<: v) => EvalM Op v where+> instance (Value :<: v) => EvalM Op v where >   evalAlgM (Add x y)  = do n1 <- projC x >                            n2 <- projC y >                            return $ iConst $ n1 + n2@@ -162,18 +159,18 @@ >   evalAlgM (Fst v)    = liftM fst $ projP v >   evalAlgM (Snd v)    = liftM snd $ projP v > -> projC :: (Value :<<: v) => HTerm v Int -> Maybe Int-> projC v = case hproject v of+> projC :: (Value :<: v) => Term v Int -> Maybe Int+> projC v = case project v of >             Just (Const n) -> return n; _ -> Nothing > -> projP :: (Value :<<: v) => HTerm v (a,b) -> Maybe (HTerm v a, HTerm v b)-> projP v = case hproject v of+> projP :: (Value :<: v) => Term v (a,b) -> Maybe (Term v a, Term v b)+> projP v = case project v of >             Just (Pair x y) -> return (x,y); _ -> Nothing >  > -- Example: evalMEx = Just (iConst 5)-> evalMEx :: Maybe (HTerm Value Int)+> evalMEx :: Maybe (Term Value Int) > evalMEx = evalM ((iConst 1) `iAdd`->                  (iConst 2 `iMult` iConst 2) :: HTerm Sig Int)+>                  (iConst 2 `iMult` iConst 2) :: Term Sig Int) -}  {- $ex3@@ -206,12 +203,12 @@ >            deriving Show >  > -- Signature for the simple expression language-> type Sig = Op :++: Value-> type SigP = Op :&&: Pos :++: Value :&&: Pos+> type Sig = Op :+: Value+> type SigP = Op :&: Pos :+: Value :&: Pos > > -- Signature for the simple expression language, extended with syntactic sugar-> type Sig' = Sugar :++: Op :++: Value-> type SigP' = Sugar :&&: Pos :++: Op :&&: Pos :++: Value :&&: Pos+> type Sig' = Sugar :+: Op :+: Value+> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos >  > -- Derive boilerplate code using Template Haskell (GHC 7 needed) > $(derive [instanceHFunctor, instanceHTraversable, instanceHFoldable,@@ -220,57 +217,57 @@ >  > -- Term homomorphism for desugaring of terms > class (HFunctor f, HFunctor g) => Desugar f g where->   desugHom :: HTermHom f g->   desugHom = desugHom' . hfmap HHole->   desugHom' :: HAlg f (HContext g a)->   desugHom' x = appHCxt (desugHom x)+>   desugHom :: TermHom f g+>   desugHom = desugHom' . hfmap Hole+>   desugHom' :: Alg f (Context g a)+>   desugHom' x = appCxt (desugHom x) > -> instance (Desugar f h, Desugar g h) => Desugar (f :++: g) h where->   desugHom (HInl x) = desugHom x->   desugHom (HInr x) = desugHom x->   desugHom' (HInl x) = desugHom' x->   desugHom' (HInr x) = desugHom' x+> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where+>   desugHom (Inl x) = desugHom x+>   desugHom (Inr x) = desugHom x+>   desugHom' (Inl x) = desugHom' x+>   desugHom' (Inr x) = desugHom' x > -> instance (Value :<<: v, HFunctor v) => Desugar Value v where->   desugHom = simpHCxt . hinj+> instance (Value :<: v, HFunctor v) => Desugar Value v where+>   desugHom = simpCxt . inj > -> instance (Op :<<: v, HFunctor v) => Desugar Op v where->   desugHom = simpHCxt . hinj+> instance (Op :<: v, HFunctor v) => Desugar Op v where+>   desugHom = simpCxt . inj > -> instance (Op :<<: v, Value :<<: v, HFunctor v) => Desugar Sugar v where+> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where >   desugHom' (Neg x)  = iConst (-1) `iMult` x >   desugHom' (Swap x) = iSnd x `iPair` iFst x > > -- Term evaluation algebra > class Eval f v where->   evalAlg :: HAlg f (HTerm v)+>   evalAlg :: Alg f (Term v) > -> instance (Eval f v, Eval g v) => Eval (f :++: g) v where->   evalAlg (HInl x) = evalAlg x->   evalAlg (HInr x) = evalAlg x+> instance (Eval f v, Eval g v) => Eval (f :+: g) v where+>   evalAlg (Inl x) = evalAlg x+>   evalAlg (Inr x) = evalAlg x > -> instance (Value :<<: v) => Eval Value v where->   evalAlg = hinject+> instance (Value :<: v) => Eval Value v where+>   evalAlg = inject > -> instance (Value :<<: v) => Eval Op v where+> instance (Value :<: v) => Eval Op v where >   evalAlg (Add x y)  = iConst $ (projC x) + (projC y) >   evalAlg (Mult x y) = iConst $ (projC x) * (projC y) >   evalAlg (Fst x)    = fst $ projP x >   evalAlg (Snd x)    = snd $ projP x >-> projC :: (Value :<<: v) => HTerm v Int -> Int-> projC v = case hproject v of Just (Const n) -> n+> projC :: (Value :<: v) => Term v Int -> Int+> projC v = case project v of Just (Const n) -> n >-> projP :: (Value :<<: v) => HTerm v (s,t) -> (HTerm v s, HTerm v t)-> projP v = case hproject v of Just (Pair x y) -> (x,y)+> projP :: (Value :<: v) => HTerm v (s,t) -> (HTerm v s, HTerm v t)+> projP v = case project v of Just (Pair x y) -> (x,y) > > -- Compose the evaluation algebra and the desugaring homomorphism to an > -- algebra-> eval :: HTerm Sig' :-> HTerm Value-> eval = hcata (evalAlg `compHAlg` (desugHom :: HTermHom Sig' Sig))+> eval :: Term Sig' :-> Term Value+> eval = cata (evalAlg `compAlg` (desugHom :: TermHom Sig' Sig)) >  > -- Example: evalEx = iPair (iConst 2) (iConst 1)-> evalEx :: HTerm Value (Int,Int)+> evalEx :: Term Value (Int,Int) > evalEx = eval $ iSwap $ iPair (iConst 1) (iConst 2) -} @@ -305,12 +302,12 @@ >            deriving Show >  > -- Signature for the simple expression language-> type Sig = Op :++: Value-> type SigP = Op :&&: Pos :++: Value :&&: Pos+> type Sig = Op :+: Value+> type SigP = Op :&: Pos :+: Value :&: Pos > > -- Signature for the simple expression language, extended with syntactic sugar-> type Sig' = Sugar :++: Op :++: Value-> type SigP' = Sugar :&&: Pos :++: Op :&&: Pos :++: Value :&&: Pos+> type Sig' = Sugar :+: Op :+: Value+> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos >  > -- Derive boilerplate code using Template Haskell (GHC 7 needed) > $(derive [instanceHFunctor, instanceHTraversable, instanceHFoldable,@@ -319,53 +316,53 @@ >  > -- Term homomorphism for desugaring of terms > class (HFunctor f, HFunctor g) => Desugar f g where->   desugHom :: HTermHom f g->   desugHom = desugHom' . hfmap HHole->   desugHom' :: HAlg f (HContext g a)->   desugHom' x = appHCxt (desugHom x)+>   desugHom :: TermHom f g+>   desugHom = desugHom' . hfmap Hole+>   desugHom' :: Alg f (Context g a)+>   desugHom' x = appCxt (desugHom x) > -> instance (Desugar f h, Desugar g h) => Desugar (f :++: g) h where->   desugHom (HInl x) = desugHom x->   desugHom (HInr x) = desugHom x->   desugHom' (HInl x) = desugHom' x->   desugHom' (HInr x) = desugHom' x+> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where+>   desugHom (Inl x) = desugHom x+>   desugHom (Inr x) = desugHom x+>   desugHom' (Inl x) = desugHom' x+>   desugHom' (Inr x) = desugHom' x > -> instance (Value :<<: v, HFunctor v) => Desugar Value v where->   desugHom = simpHCxt . hinj+> instance (Value :<: v, HFunctor v) => Desugar Value v where+>   desugHom = simpCxt . inj > -> instance (Op :<<: v, HFunctor v) => Desugar Op v where->   desugHom = simpHCxt . hinj+> instance (Op :<: v, HFunctor v) => Desugar Op v where+>   desugHom = simpCxt . inj > -> instance (Op :<<: v, Value :<<: v, HFunctor v) => Desugar Sugar v where+> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where >   desugHom' (Neg x)  = iConst (-1) `iMult` x >   desugHom' (Swap x) = iSnd x `iPair` iFst x > > -- Lift the desugaring term homomorphism to a catamorphism-> desug :: HTerm Sig' :-> HTerm Sig-> desug = appHTermHom desugHom+> desug :: Term Sig' :-> Term Sig+> desug = appTermHom desugHom > > -- Example: desugEx = iPair (iConst 2) (iConst 1)-> desugEx :: HTerm Sig (Int,Int)+> desugEx :: Term Sig (Int,Int) > desugEx = desug $ iSwap $ iPair (iConst 1) (iConst 2) > > -- Lift desugaring to terms annotated with source positions-> desugP :: HTerm SigP' :-> HTerm SigP-> desugP = appHTermHom (productHTermHom desugHom)+> desugP :: Term SigP' :-> Term SigP+> desugP = appTermHom (productTermHom desugHom) >-> iSwapP :: (HDistProd f p f', Sugar :<<: f) => p -> HTerm f' (a,b) -> HTerm f' (b,a)-> iSwapP p x = HTerm (hinjectP p $ hinj $ Swap x)+> iSwapP :: (DistProd f p f', Sugar :<: f) => p -> Term f' (a,b) -> Term f' (b,a)+> iSwapP p x = Term (injectP p $ inj $ Swap x) >-> iConstP :: (HDistProd f p f', Value :<<: f) => p -> Int -> HTerm f' Int-> iConstP p x = HTerm (hinjectP p $ hinj $ Const x)+> iConstP :: (DistProd f p f', Value :<: f) => p -> Int -> Term f' Int+> iConstP p x = Term (injectP p $ inj $ Const x) >-> iPairP :: (HDistProd f p f', Value :<<: f) => p -> HTerm f' a -> HTerm f' b -> HTerm f' (a,b)-> iPairP p x y = HTerm (hinjectP p $ hinj $ Pair x y)+> iPairP :: (DistProd f p f', Value :<: f) => p -> Term f' a -> Term f' b -> Term f' (a,b)+> iPairP p x y = Term (injectP p $ inj $ Pair x y) >-> iFstP :: (HDistProd f p f', Op :<<: f) => p -> HTerm f' (a,b) -> HTerm f' a-> iFstP p x = HTerm (hinjectP p $ hinj $ Fst x)+> iFstP :: (DistProd f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' a+> iFstP p x = Term (injectP p $ inj $ Fst x) >-> iSndP :: (HDistProd f p f', Op :<<: f) => p -> HTerm f' (a,b) -> HTerm f' b-> iSndP p x = HTerm (hinjectP p $ hinj $ Snd x)+> iSndP :: (DistProd f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' b+> iSndP p x = Term (injectP p $ inj $ Snd x) > > -- Example: desugPEx = iPairP (Pos 1 0) > --                            (iSndP (Pos 1 0) (iPairP (Pos 1 1)@@ -374,7 +371,7 @@ > --                            (iFstP (Pos 1 0) (iPairP (Pos 1 1) > --                                                     (iConstP (Pos 1 2) 1) > --                                                     (iConstP (Pos 1 3) 2)))-> desugPEx :: HTerm SigP (Int,Int)+> desugPEx :: Term SigP (Int,Int) > desugPEx = desugP $ iSwapP (Pos 1 0) (iPairP (Pos 1 1) (iConstP (Pos 1 2) 1) >                                                        (iConstP (Pos 1 3) 2)) -}

@@ -17,319 +17,311 @@  module Data.Comp.Multi.Algebra (       -- * Algebras & Catamorphisms-      HAlg,-      hfree,-      hcata,-      hcata',-      appHCxt,+      Alg,+      free,+      cata,+      cata',+      appCxt,              -- * Monadic Algebras & Catamorphisms-      HAlgM,+      AlgM, --      halgM,-      hfreeM,-      hcataM,-      hcataM',-      liftMHAlg,+      freeM,+      cataM,+      cataM',+      liftMAlg,        -- * Term Homomorphisms-      HCxtFun,-      HSigFun,-      HTermHom,-      appHTermHom,-      compHTermHom,-      appHSigFun,-      compHSigFun,-      htermHom,-      compHAlg,---      compHCoalg,---      compHCVCoalg,+      CxtFun,+      SigFun,+      TermHom,+      appTermHom,+      compTermHom,+      appSigFun,+      compSigFun,+      termHom,+      compAlg,+--      compCoalg,+--      compCVCoalg,        -- * Monadic Term Homomorphisms-      HCxtFunM,-      HSigFunM,-      HTermHomM,---      HSigFunM',---      HTermHomM',-      hsigFunM,---      htermHom',-      appHTermHomM,-      htermHomM,---      htermHomM',-      appHSigFunM,---      appHSigFunM',-      compHTermHomM,-      compHSigFunM,-      compHAlgM,-      compHAlgM',+      CxtFunM,+      SigFunM,+      TermHomM,+--      SigFunM',+--      TermHomM',+      sigFunM,+--      termHom',+      appTermHomM,+      termHomM,+--      termHomM',+      appSigFunM,+--      appSigFunM',+      compTermHomM,+      compSigFunM,+      compAlgM,+      compAlgM',        -- * Coalgebras & Anamorphisms-      HCoalg,-      hana,---      hana',-      HCoalgM,-      hanaM,+      Coalg,+      ana,+--      ana',+      CoalgM,+      anaM,        -- * R-Algebras & Paramorphisms-      HRAlg,-      hpara,-      HRAlgM,-      hparaM,+      RAlg,+      para,+      RAlgM,+      paraM,        -- * R-Coalgebras & Apomorphisms-      HRCoalg,-      hapo,-      HRCoalgM,-      hapoM,+      RCoalg,+      apo,+      RCoalgM,+      apoM,        -- * CV-Algebras & Histomorphisms       -- $l1---      HCVAlg,---      hhisto,---      HCVAlgM,---      hhistoM,+--      CVAlg,+--      histo,+--      CVAlgM,+--      histoM,        -- * CV-Coalgebras & Futumorphisms-      HCVCoalg,-      hfutu,---      HCVCoalg',---      hfutu',-      HCVCoalgM,-      hfutuM,--      -- * Exponential Functors-      appHTermHomE,-      hcataE,---      hanaE,-      appHCxtE+      CVCoalg,+      futu,+--      CVCoalg',+--      futu',+      CVCoalgM,+      futuM,     ) where   import Data.Comp.Multi.Term import Data.Comp.Multi.Functor import Data.Comp.Multi.Traversable-import Data.Comp.Multi.ExpFunctor import Data.Comp.Ops- import Control.Monad  -type HAlg f e = f e :-> e+type Alg f e = f e :-> e -hfree :: forall f h a b . (HFunctor f) =>-              HAlg f b -> (a :-> b) -> HCxt h f a :-> b-hfree f g = run-    where run :: HCxt h f a :-> b-          run (HHole v) = g v-          run (HTerm c) = f $ hfmap run c+free :: forall f h a b . (HFunctor f) =>+              Alg f b -> (a :-> b) -> Cxt h f a :-> b+free f g = run+    where run :: Cxt h f a :-> b+          run (Hole v) = g v+          run (Term c) = f $ hfmap run c  -hcata :: forall f a. (HFunctor f) => HAlg f a -> HTerm f :-> a-hcata f = run -    where run :: HTerm f :-> a-          run (HTerm t) = f (hfmap run t)+cata :: forall f a. HFunctor f => Alg f a -> Term f :-> a+cata f = run +    where run :: Term f :-> a+          run (Term t) = f (hfmap run t) -hcata' :: (HFunctor f) => HAlg f e -> HCxt h f e :-> e-hcata' alg = hfree alg id+cata' :: HFunctor f => Alg f e -> Cxt h f e :-> e+cata' alg = free alg id  -- | This function applies a whole context into another context. -appHCxt :: (HFunctor f) => HContext f (HCxt h f a) :-> HCxt h f a-appHCxt = hcata' HTerm+appCxt :: HFunctor f => Context f (Cxt h f a) :-> Cxt h f a+appCxt = cata' Term  -- | This function lifts a many-sorted algebra to a monadic domain.-liftMHAlg :: forall m f. (Monad m, HTraversable f) =>-            HAlg f I -> HAlg f m-liftMHAlg alg =  turn . liftM alg . hmapM run+liftMAlg :: forall m f. (Monad m, HTraversable f) =>+            Alg f I -> Alg f m+liftMAlg alg =  turn . liftM alg . hmapM run     where run :: m i -> m (I i)           run m = do x <- m                      return $ I x           turn x = do I y <- x                       return y -type HAlgM m f e = NatM m (f e) e+type AlgM m f e = NatM m (f e) e -hfreeM :: forall f m h a b. (HTraversable f, Monad m) =>-               HAlgM m f b -> NatM m a b -> NatM m (HCxt h f a)  b-hfreeM algm var = run-    where run :: NatM m (HCxt h f a) b-          run (HHole x) = var x-          run (HTerm x) = hmapM run x >>= algm+freeM :: forall f m h a b. (HTraversable f, Monad m) =>+               AlgM m f b -> NatM m a b -> NatM m (Cxt h f a)  b+freeM algm var = run+    where run :: NatM m (Cxt h f a) b+          run (Hole x) = var x+          run (Term x) = hmapM run x >>= algm --- | This is a monadic version of 'hcata'.+-- | This is a monadic version of 'cata'. -hcataM :: forall f m a. (HTraversable f, Monad m) =>-         HAlgM m f a -> NatM m (HTerm f) a--- hcataM alg h (HTerm t) = alg =<< hmapM (hcataM alg h) t-hcataM alg = run-    where run :: NatM m (HTerm f) a-          run (HTerm x) = alg =<< hmapM run x+cataM :: forall f m a. (HTraversable f, Monad m) =>+         AlgM m f a -> NatM m (Term f) a+-- cataM alg h (Term t) = alg =<< hmapM (cataM alg h) t+cataM alg = run+    where run :: NatM m (Term f) a+          run (Term x) = alg =<< hmapM run x  -hcataM' :: forall m h a f. (Monad m, HTraversable f) => HAlgM m f a -> NatM m (HCxt h f a) a--- hcataM' alg = hfreeM alg return-hcataM' f = run-    where run :: NatM m (HCxt h f a) a-          run (HHole x) = return x-          run (HTerm x) = hmapM run x >>= f+cataM' :: forall m h a f. (Monad m, HTraversable f) => AlgM m f a -> NatM m (Cxt h f a) a+-- cataM' alg = freeM alg return+cataM' f = run+    where run :: NatM m (Cxt h f a) a+          run (Hole x) = return x+          run (Term x) = hmapM run x >>= f  -- | This type represents context function. -type HCxtFun f g = forall a h. HCxt h f a :-> HCxt h g a+type CxtFun f g = forall a h. Cxt h f a :-> Cxt h g a  -- | This type represents uniform signature function specification. -type HSigFun f g = forall a. f a :-> g a+type SigFun f g = forall a. f a :-> g a   -- | This type represents a term algebra. -type HTermHom f g = HSigFun f (HContext g)+type TermHom f g = SigFun f (Context g)  -- | This function applies the given term homomorphism to a -- term/context. -appHTermHom :: (HFunctor f, HFunctor g) => HTermHom f g -> HCxtFun f g+appTermHom :: (HFunctor f, HFunctor g) => TermHom f g -> CxtFun f g -- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type--- (Functor f, Functor g) => (f (HCxt h g b) -> HContext g (HCxt h g b)) -> HCxt h f b -> HCxt h g b+-- (Functor f, Functor g) => (f (Cxt h g b) -> Context g (Cxt h g b)) -> Cxt h f b -> Cxt h g b -- would achieve the same. The given type is chosen for clarity.-appHTermHom _ (HHole b) = HHole b-appHTermHom f (HTerm t) = appHCxt . f . hfmap (appHTermHom f) $ t+appTermHom _ (Hole b) = Hole b+appTermHom f (Term t) = appCxt . f . hfmap (appTermHom f) $ t  -- | This function composes two term algebras. -compHTermHom :: (HFunctor g, HFunctor h) => HTermHom g h -> HTermHom f g -> HTermHom f h+compTermHom :: (HFunctor g, HFunctor h) => TermHom g h -> TermHom f g -> TermHom f h -- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type--- (Functor f, Functor g) => (f (HCxt h g b) -> HContext g (HCxt h g b))--- -> (a -> HCxt h f b) -> a -> HCxt h g b+-- (Functor f, Functor g) => (f (Cxt h g b) -> Context g (Cxt h g b))+-- -> (a -> Cxt h f b) -> a -> Cxt h g b -- would achieve the same. The given type is chosen for clarity.-compHTermHom f g = appHTermHom f . g+compTermHom f g = appTermHom f . g  -- | This function composes a term algebra with an algebra. -compHAlg :: (HFunctor g) => HAlg g a -> HTermHom f g -> HAlg f a-compHAlg alg talg = hcata' alg . talg+compAlg :: (HFunctor g) => Alg g a -> TermHom f g -> Alg f a+compAlg alg talg = cata' alg . talg  -- | This function applies a signature function to the given context. -appHSigFun :: (HFunctor f, HFunctor g) => HSigFun f g -> HCxtFun f g-appHSigFun f = appHTermHom $ htermHom f+appSigFun :: (HFunctor f, HFunctor g) => SigFun f g -> CxtFun f g+appSigFun f = appTermHom $ termHom f   -- | This function composes two signature functions. -compHSigFun :: HSigFun g h -> HSigFun f g -> HSigFun f h-compHSigFun f g = f . g+compSigFun :: SigFun g h -> SigFun f g -> SigFun f h+compSigFun f g = f . g     -- | Lifts the given signature function to the canonical term homomorphism.-htermHom :: (HFunctor g) => HSigFun f g -> HTermHom f g-htermHom f = simpHCxt . f+termHom :: (HFunctor g) => SigFun f g -> TermHom f g+termHom f = simpCxt . f  -- | This type represents monadic context function. -type HCxtFunM m f g = forall a h. NatM m (HCxt h f a) (HCxt h g a)+type CxtFunM m f g = forall a h. NatM m (Cxt h f a) (Cxt h g a)  -- | This type represents monadic signature functions. -type HSigFunM m f g = forall a. NatM m (f a) (g a)+type SigFunM m f g = forall a. NatM m (f a) (g a)   -- | This type represents monadic term algebras. -type HTermHomM m f g = HSigFunM m f (HContext g)+type TermHomM m f g = SigFunM m f (Context g)  -- | This function lifts the given signature function to a monadic -- signature function. Note that term algebras are instances of -- signature functions. Hence this function also applies to term -- algebras. -hsigFunM :: (Monad m) => HSigFun f g -> HSigFunM m f g-hsigFunM f = return . f+sigFunM :: (Monad m) => SigFun f g -> SigFunM m f g+sigFunM f = return . f  -- | This function lifts the give monadic signature function to a -- monadic term algebra. -htermHom' :: (HFunctor f, HFunctor g, Monad m) =>-            HSigFunM m f g -> HTermHomM m f g-htermHom' f = liftM  (HTerm . hfmap HHole) . f+termHom' :: (HFunctor f, HFunctor g, Monad m) =>+            SigFunM m f g -> TermHomM m f g+termHom' f = liftM  (Term . hfmap Hole) . f  -- | This function lifts the given signature function to a monadic -- term algebra. -htermHomM :: (HFunctor g, Monad m) => HSigFun f g -> HTermHomM m f g-htermHomM f = hsigFunM $ htermHom f+termHomM :: (HFunctor g, Monad m) => SigFun f g -> TermHomM m f g+termHomM f = sigFunM $ termHom f  -- | This function applies the given monadic term homomorphism to the -- given term/context. -appHTermHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)-         => HTermHomM m f g -> HCxtFunM m f g-appHTermHomM f = run-    where run :: NatM m (HCxt h f a) (HCxt h g a)-          run (HHole b) = return $ HHole b-          run (HTerm t) = liftM appHCxt . (>>= f) . hmapM run $ t+appTermHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)+         => TermHomM m f g -> CxtFunM m f g+appTermHomM f = run+    where run :: NatM m (Cxt h f a) (Cxt h g a)+          run (Hole b) = return $ Hole b+          run (Term t) = liftM appCxt . (>>= f) . hmapM run $ t  -- | This function applies the given monadic signature function to the -- given context. -appHSigFunM :: (HTraversable f, HFunctor g, Monad m) =>-                HSigFunM m f g -> HCxtFunM m f g-appHSigFunM f = appHTermHomM $ htermHom' f+appSigFunM :: (HTraversable f, HFunctor g, Monad m) =>+                SigFunM m f g -> CxtFunM m f g+appSigFunM f = appTermHomM $ termHom' f  -- | This function composes two monadic term algebras. -compHTermHomM :: (HTraversable g, HFunctor h, Monad m)-             => HTermHomM m g h -> HTermHomM m f g -> HTermHomM m f h-compHTermHomM f g a = g a >>= appHTermHomM f+compTermHomM :: (HTraversable g, HFunctor h, Monad m)+             => TermHomM m g h -> TermHomM m f g -> TermHomM m f h+compTermHomM f g a = g a >>= appTermHomM f  {-| This function composes a monadic term algebra with a monadic algebra -} -compHAlgM :: (HTraversable g, Monad m) => HAlgM m g a -> HTermHomM m f g -> HAlgM m f a-compHAlgM alg talg c = hcataM' alg =<< talg c+compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a+compAlgM alg talg c = cataM' alg =<< talg c  -- | This function composes a monadic term algebra with a monadic -- algebra. -compHAlgM' :: (HTraversable g, Monad m) => HAlgM m g a -> HTermHom f g -> HAlgM m f a-compHAlgM' alg talg = hcataM' alg . talg+compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> TermHom f g -> AlgM m f a+compAlgM' alg talg = cataM' alg . talg   {-| This function composes two monadic signature functions.  -} -compHSigFunM :: (Monad m) => HSigFunM m g h -> HSigFunM m f g -> HSigFunM m f h-compHSigFunM f g a = g a >>= f+compSigFunM :: (Monad m) => SigFunM m g h -> SigFunM m f g -> SigFunM m f h+compSigFunM f g a = g a >>= f   ---------------- -- Coalgebras -- ---------------- -type HCoalg f a = a :-> f a+type Coalg f a = a :-> f a  {-| This function unfolds the given value to a term using the given-unravelling function. This is the unique homomorphism @a -> HTerm f@+unravelling function. This is the unique homomorphism @a -> Term f@ from the given coalgebra of type @a -> f a@ to the final coalgebra-@HTerm f@. -}+@Term f@. -} -hana :: forall f a. HFunctor f => HCoalg f a -> a :-> HTerm f-hana f = run-    where run :: a :-> HTerm f-          run t = HTerm $ hfmap run (f t)+ana :: forall f a. HFunctor f => Coalg f a -> a :-> Term f+ana f = run+    where run :: a :-> Term f+          run t = Term $ hfmap run (f t) -type HCoalgM m f a = NatM m a (f a)+type CoalgM m f a = NatM m a (f a)  -- | This function unfolds the given value to a term using the given -- monadic unravelling function. This is the unique homomorphism @a ->--- HTerm f@ from the given coalgebra of type @a -> f a@ to the final--- coalgebra @HTerm f@.+-- Term f@ from the given coalgebra of type @a -> f a@ to the final+-- coalgebra @Term f@. -hanaM :: forall a m f. (HTraversable f, Monad m)-          => HCoalgM m f a -> NatM m a (HTerm f)-hanaM f = run -    where run :: NatM m a (HTerm f)-          run t = liftM HTerm $ f t >>= hmapM run+anaM :: forall a m f. (HTraversable f, Monad m)+          => CoalgM m f a -> NatM m a (Term f)+anaM f = run +    where run :: NatM m a (Term f)+          run t = liftM Term $ f t >>= hmapM run  -------------------------------- -- R-Algebras & Paramorphisms --@@ -338,27 +330,27 @@ -- | This type represents r-algebras over functor @f@ and with domain -- @a@. -type HRAlg f a = f (HTerm f :*: a) :-> a+type RAlg f a = f (Term f :*: a) :-> a  -- | This function constructs a paramorphism from the given r-algebra-hpara :: forall f a. (HFunctor f) => HRAlg f a -> HTerm f :-> a-hpara f = fsnd . hcata run-    where run :: HAlg f  (HTerm f :*: a)-          run t = HTerm (hfmap ffst t) :*: f t+para :: forall f a. (HFunctor f) => RAlg f a -> Term f :-> a+para f = fsnd . cata run+    where run :: Alg f  (Term f :*: a)+          run t = Term (hfmap ffst t) :*: f t  -- | This type represents monadic r-algebras over monad @m@ and -- functor @f@ and with domain @a@.-type HRAlgM m f a = NatM m (f (HTerm f :*: a)) a+type RAlgM m f a = NatM m (f (Term f :*: a)) a  -- | This function constructs a monadic paramorphism from the given -- monadic r-algebra-hparaM :: forall f m a. (HTraversable f, Monad m) => -         HRAlgM m f a -> NatM m(HTerm f)  a-hparaM f = liftM fsnd . hcataM run-    where run :: HAlgM m f (HTerm f :*: a)+paraM :: forall f m a. (HTraversable f, Monad m) => +         RAlgM m f a -> NatM m(Term f)  a+paraM f = liftM fsnd . cataM run+    where run :: AlgM m f (Term f :*: a)           run t = do             a <- f t-            return (HTerm (hfmap ffst t) :*: a)+            return (Term (hfmap ffst t) :*: a)  -------------------------------- -- R-Coalgebras & Apomorphisms --@@ -366,34 +358,34 @@  -- | This type represents r-coalgebras over functor @f@ and with -- domain @a@.-type HRCoalg f a = a :-> f (HTerm f :+: a)+type RCoalg f a = a :-> f (Term f :+: a)  -- | This function constructs an apomorphism from the given -- r-coalgebra.-hapo :: forall f a . (HFunctor f) => HRCoalg f a -> a :-> HTerm f-hapo f = run -    where run :: a :-> HTerm f-          run = HTerm . hfmap run' . f-          run' :: HTerm f :+: a :-> HTerm f+apo :: forall f a . (HFunctor f) => RCoalg f a -> a :-> Term f+apo f = run +    where run :: a :-> Term f+          run = Term . hfmap run' . f+          run' :: Term f :+: a :-> Term f           run' (Inl t) = t           run' (Inr a) = run a  -- | This type represents monadic r-coalgebras over monad @m@ and -- functor @f@ with domain @a@. -type HRCoalgM m f a = NatM m a (f (HTerm f :+: a))+type RCoalgM m f a = NatM m a (f (Term f :+: a))  -- | This function constructs a monadic apomorphism from the given -- monadic r-coalgebra.-hapoM :: forall f m a . (HTraversable f, Monad m) =>-        HRCoalgM m f a -> NatM m a (HTerm f)-hapoM f = run -    where run :: NatM m a (HTerm f)+apoM :: forall f m a . (HTraversable f, Monad m) =>+        RCoalgM m f a -> NatM m a (Term f)+apoM f = run +    where run :: NatM m a (Term f)           run a = do             t <- f a             t' <- hmapM run' t-            return $ HTerm t'-          run' :: NatM m (HTerm f :+: a)  (HTerm f)+            return $ Term t'+          run' :: NatM m (Term f :+: a)  (Term f)           run' (Inl t) = return t           run' (Inr a) = run a @@ -414,62 +406,29 @@ -- | This type represents cv-coalgebras over functor @f@ and with domain -- @a@. -type HCVCoalg f a = a :-> f (HContext f a)+type CVCoalg f a = a :-> f (Context f a)   -- | This function constructs the unique futumorphism from the given -- cv-coalgebra to the term algebra. -hfutu :: forall f a . HFunctor f => HCVCoalg f a -> a :-> HTerm f-hfutu coa = hana run . HHole-    where run :: HCoalg f (HContext f a)-          run (HHole a) = coa a-          run (HTerm v) = v+futu :: forall f a . HFunctor f => CVCoalg f a -> a :-> Term f+futu coa = ana run . Hole+    where run :: Coalg f (Context f a)+          run (Hole a) = coa a+          run (Term v) = v   -- | This type represents monadic cv-coalgebras over monad @m@ and -- functor @f@, and with domain @a@. -type HCVCoalgM m f a = NatM m a (f (HContext f a))+type CVCoalgM m f a = NatM m a (f (Context f a))  -- | This function constructs the unique monadic futumorphism from the -- given monadic cv-coalgebra to the term algebra.-hfutuM :: forall f a m . (HTraversable f, Monad m) =>-         HCVCoalgM m f a -> NatM m a (HTerm f)-hfutuM coa = hanaM run . HHole-    where run :: HCoalgM m f (HContext f a)-          run (HHole a) = coa a-          run (HTerm v) = return v-------------------------------- Exponential Functors -------------------------------{-| Catamorphism for higher-order exponential functors. -}-hcataE :: forall f a . HExpFunctor f => HAlg f a -> HTerm f :-> a-hcataE f = cataFS . toHCxt-    where cataFS :: HExpFunctor f => HContext f a :-> a-          cataFS (HHole x) = x-          cataFS (HTerm t) = f (hxmap cataFS HHole t)---{-{-| Anamorphism for higher-order exponential functors. -}-hanaE :: forall a f . HExpFunctor f => HCoalg f a -> a :-> HTerm (f :&: a)-hanaE f = run-    where run :: a :-> HTerm (f :&: a)-          run t = HTerm $ hxmap run (snd . hprojectP . unHTerm) (f t) :&: t-}---- | Variant of 'appHCxt' for contexts over 'HExpFunctor' signatures.-appHCxtE :: (HExpFunctor f) => HContext f (HCxt h f a) :-> HCxt h f a-appHCxtE (HHole x) = x-appHCxtE (HTerm t)  = HTerm (hxmap appHCxtE HHole t)---- | Variant of 'appHTermHom' for term homomorphisms from and to--- 'HExpFunctor' signatures.-appHTermHomE :: forall f g . (HExpFunctor f, HExpFunctor g) => HTermHom f g-             -> HTerm f :-> HTerm g-appHTermHomE f = cataFS . toHCxt-    where cataFS :: HContext f (HTerm g) :-> HTerm g-          cataFS (HHole x) = x-          cataFS (HTerm t) = appHCxtE (f (hxmap cataFS HHole t))+futuM :: forall f a m . (HTraversable f, Monad m) =>+         CVCoalgM m f a -> NatM m a (Term f)+futuM coa = anaM run . Hole+    where run :: CoalgM m f (Context f a)+          run (Hole a) = coa a+          run (Term v) = return v

@@ -31,25 +31,25 @@   'EqF' is propagated through sums. -} -instance (HEqF f, HEqF g) => HEqF (f :++: g) where-    heqF (HInl x) (HInl y) = heqF x y-    heqF (HInr x) (HInr y) = heqF x y+instance (HEqF f, HEqF g) => HEqF (f :+: g) where+    heqF (Inl x) (Inl y) = heqF x y+    heqF (Inr x) (Inr y) = heqF x y     heqF _ _ = False  {-|   From an 'EqF' functor an 'Eq' instance of the corresponding   term type can be derived. -}-instance (HEqF f) => HEqF (HCxt h f) where+instance (HEqF f) => HEqF (Cxt h f) where -    heqF (HTerm e1) (HTerm e2) = e1 `heqF` e2-    heqF (HHole h1) (HHole h2) = h1 `keq` h2+    heqF (Term e1) (Term e2) = e1 `heqF` e2+    heqF (Hole h1) (Hole h2) = h1 `keq` h2     heqF _ _ = False -instance (HEqF f, KEq a)  => KEq (HCxt h f a) where+instance (HEqF f, KEq a)  => KEq (Cxt h f a) where     keq = heqF -instance KEq HNothing where+instance KEq Nothing where     keq _ = undefined  

@@ -1,24 +0,0 @@-{-# LANGUAGE TypeOperators, RankNTypes #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Comp.Multi.ExpFunctor--- Copyright   :  (c) 2011 Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ This module defines higher-order exponential functors.--------------------------------------------------------------------------------------module Data.Comp.Multi.ExpFunctor-    (-      HExpFunctor(..)-    ) where--import Data.Comp.Multi.Functor--{-| Higher-order exponential functors are higher-order functors that may be both covariant (as ordinary higher-order functors) and contravariant. -}-class HExpFunctor f where-    hxmap :: (a :-> b) -> (b :-> a) -> f a :-> f b

@@ -21,144 +21,139 @@ import Data.Comp.Multi.Functor import Data.Comp.Multi.Foldable import Data.Comp.Multi.Traversable-import Data.Comp.Multi.ExpFunctor-import Data.Comp.Ops+import qualified Data.Comp.Ops as O import Control.Monad import Control.Applicative  -infixr 5 :++:+infixr 5 :+:   -- |Data type defining coproducts.-data (f :++: g) (h :: * -> *) e = HInl (f h e)-                    | HInr (g h e)--instance (HFunctor f, HFunctor g) => HFunctor (f :++: g) where-    hfmap f (HInl v) = HInl $ hfmap f v-    hfmap f (HInr v) = HInr $ hfmap f v+data (f :+: g) (h :: * -> *) e = Inl (f h e)+                    | Inr (g h e) -instance (HFoldable f, HFoldable g) => HFoldable (f :++: g) where-    hfold (HInl e) = hfold e-    hfold (HInr e) = hfold e-    hfoldMap f (HInl e) = hfoldMap f e-    hfoldMap f (HInr e) = hfoldMap f e-    hfoldr f b (HInl e) = hfoldr f b e-    hfoldr f b (HInr e) = hfoldr f b e-    hfoldl f b (HInl e) = hfoldl f b e-    hfoldl f b (HInr e) = hfoldl f b e+instance (HFunctor f, HFunctor g) => HFunctor (f :+: g) where+    hfmap f (Inl v) = Inl $ hfmap f v+    hfmap f (Inr v) = Inr $ hfmap f v -    hfoldr1 f (HInl e) = hfoldr1 f e-    hfoldr1 f (HInr e) = hfoldr1 f e-    hfoldl1 f (HInl e) = hfoldl1 f e-    hfoldl1 f (HInr e) = hfoldl1 f e+instance (HFoldable f, HFoldable g) => HFoldable (f :+: g) where+    hfold (Inl e) = hfold e+    hfold (Inr e) = hfold e+    hfoldMap f (Inl e) = hfoldMap f e+    hfoldMap f (Inr e) = hfoldMap f e+    hfoldr f b (Inl e) = hfoldr f b e+    hfoldr f b (Inr e) = hfoldr f b e+    hfoldl f b (Inl e) = hfoldl f b e+    hfoldl f b (Inr e) = hfoldl f b e -instance (HTraversable f, HTraversable g) => HTraversable (f :++: g) where-    htraverse f (HInl e) = HInl <$> htraverse f e-    htraverse f (HInr e) = HInr <$> htraverse f e-    hmapM f (HInl e) = HInl `liftM` hmapM f e-    hmapM f (HInr e) = HInr `liftM` hmapM f e+    hfoldr1 f (Inl e) = hfoldr1 f e+    hfoldr1 f (Inr e) = hfoldr1 f e+    hfoldl1 f (Inl e) = hfoldl1 f e+    hfoldl1 f (Inr e) = hfoldl1 f e -instance (HExpFunctor f, HExpFunctor g) => HExpFunctor (f :++: g) where-    hxmap f g (HInl v) = HInl $ hxmap f g v-    hxmap f g (HInr v) = HInr $ hxmap f g v+instance (HTraversable f, HTraversable g) => HTraversable (f :+: g) where+    htraverse f (Inl e) = Inl <$> htraverse f e+    htraverse f (Inr e) = Inr <$> htraverse f e+    hmapM f (Inl e) = Inl `liftM` hmapM f e+    hmapM f (Inr e) = Inr `liftM` hmapM f e  -- |The subsumption relation.-class (sub :: (* -> *) -> * -> *) :<<: sup where-    hinj :: sub a :-> sup a-    hproj :: NatM Maybe (sup a) (sub a)+class (sub :: (* -> *) -> * -> *) :<: sup where+    inj :: sub a :-> sup a+    proj :: NatM Maybe (sup a) (sub a) -instance (:<<:) f f where-    hinj = id-    hproj = Just+instance (:<:) f f where+    inj = id+    proj = Just -instance (:<<:) f (f :++: g) where-    hinj = HInl-    hproj (HInl x) = Just x-    hproj (HInr _) = Nothing+instance (:<:) f (f :+: g) where+    inj = Inl+    proj (Inl x) = Just x+    proj (Inr _) = Nothing -instance (f :<<: g) => (:<<:) f (h :++: g) where-    hinj = HInr . hinj-    hproj (HInr x) = hproj x-    hproj (HInl _) = Nothing+instance (f :<: g) => (:<:) f (h :+: g) where+    inj = Inr . inj+    proj (Inr x) = proj x+    proj (Inl _) = Nothing  -- Products -infixr 8 :**:+infixr 8 :*: -data (f :**: g) a = f a :**: g a+data (f :*: g) a = f a :*: g a  -hfst :: (f :**: g) a -> f a-hfst (x :**: _) = x+fst :: (f :*: g) a -> f a+fst (x :*: _) = x -hsnd :: (f :**: g) a -> g a-hsnd (_ :**: x) = x+snd :: (f :*: g) a -> g a+snd (_ :*: x) = x  -- Constant Products -infixr 7 :&&:+infixr 7 :&:  -- | This data type adds a constant product to a -- signature. Alternatively, this could have also been defined as -- --- @data (f :&&: a) (g ::  * -> *) e = f g e :&&: a e@+-- @data (f :&: a) (g ::  * -> *) e = f g e :&: a e@ --  -- This is too general, however, for example for 'productHTermHom'. -data (f :&&: a) (g ::  * -> *) e = f g e :&&: a+data (f :&: a) (g ::  * -> *) e = f g e :&: a  -instance (HFunctor f) => HFunctor (f :&&: a) where-    hfmap f (v :&&: c) = hfmap f v :&&: c+instance (HFunctor f) => HFunctor (f :&: a) where+    hfmap f (v :&: c) = hfmap f v :&: c -instance (HFoldable f) => HFoldable (f :&&: a) where-    hfold (v :&&: _) = hfold v-    hfoldMap f (v :&&: _) = hfoldMap f v-    hfoldr f e (v :&&: _) = hfoldr f e v-    hfoldl f e (v :&&: _) = hfoldl f e v-    hfoldr1 f (v :&&: _) = hfoldr1 f v-    hfoldl1 f (v :&&: _) = hfoldl1 f v+instance (HFoldable f) => HFoldable (f :&: a) where+    hfold (v :&: _) = hfold v+    hfoldMap f (v :&: _) = hfoldMap f v+    hfoldr f e (v :&: _) = hfoldr f e v+    hfoldl f e (v :&: _) = hfoldl f e v+    hfoldr1 f (v :&: _) = hfoldr1 f v+    hfoldl1 f (v :&: _) = hfoldl1 f v  -instance (HTraversable f) => HTraversable (f :&&: a) where-    htraverse f (v :&&: c) =  (:&&: c) <$> (htraverse f v)-    hmapM f (v :&&: c) = liftM (:&&: c) (hmapM f v)+instance (HTraversable f) => HTraversable (f :&: a) where+    htraverse f (v :&: c) =  (:&: c) <$> (htraverse f v)+    hmapM f (v :&: c) = liftM (:&: c) (hmapM f v)  -- | This class defines how to distribute a product over a sum of -- signatures. -class HDistProd (s :: (* -> *) -> * -> *) p s' | s' -> s, s' -> p where+class DistProd (s :: (* -> *) -> * -> *) p s' | s' -> s, s' -> p where              -- | This function injects a product a value over a signature.-    hinjectP :: p -> s a :-> s' a-    hprojectP :: s' a :-> (s a :&: p)+    injectP :: p -> s a :-> s' a+    projectP :: s' a :-> (s a O.:&: p)  -class HRemoveP (s :: (* -> *) -> * -> *) s' | s -> s'  where-    hremoveP :: s a :-> s' a+class RemoveP (s :: (* -> *) -> * -> *) s' | s -> s'  where+    removeP :: s a :-> s' a  -instance (HRemoveP s s') => HRemoveP (f :&&: p :++: s) (f :++: s') where-    hremoveP (HInl (v :&&: _)) = HInl v-    hremoveP (HInr v) = HInr $ hremoveP v+instance (RemoveP s s') => RemoveP (f :&: p :+: s) (f :+: s') where+    removeP (Inl (v :&: _)) = Inl v+    removeP (Inr v) = Inr $ removeP v  -instance HRemoveP (f :&&: p) f where-    hremoveP (v :&&: _) = v+instance RemoveP (f :&: p) f where+    removeP (v :&: _) = v  -instance HDistProd f p (f :&&: p) where+instance DistProd f p (f :&: p) where -    hinjectP p v = v :&&: p+    injectP p v = v :&: p -    hprojectP (v :&&: p) = v :&: p+    projectP (v :&: p) = v O.:&: p  -instance (HDistProd s p s') => HDistProd (f :++: s) p ((f :&&: p) :++: s') where-    hinjectP p (HInl v) = HInl (v :&&: p)-    hinjectP p (HInr v) = HInr $ hinjectP p v+instance (DistProd s p s') => DistProd (f :+: s) p ((f :&: p) :+: s') where+    injectP p (Inl v) = Inl (v :&: p)+    injectP p (Inr v) = Inr $ injectP p v -    hprojectP (HInl (v :&&: p)) = (HInl v :&: p)-    hprojectP (HInr v) = let (v' :&: p) = hprojectP v-                        in  (HInr v' :&: p)+    projectP (Inl (v :&: p)) = (Inl v O.:&: p)+    projectP (Inr v) = let (v' O.:&: p) = projectP v+                        in  (Inr v' O.:&: p)

@@ -15,21 +15,21 @@ --------------------------------------------------------------------------------  module Data.Comp.Multi.Product-    ( (:&&:) (..),-      HDistProd (..),-      HRemoveP (..),+    ( (:&:) (..),+      DistProd (..),+      RemoveP (..),       liftP,       constP,       liftP',       stripP,-      productHTermHom,-      hproject'+      productTermHom,+      project'     )where  import Data.Comp.Multi.Term import Data.Comp.Multi.Sum import Data.Comp.Multi.Ops-import Data.Comp.Ops+import qualified Data.Comp.Ops as O import Data.Comp.Multi.Algebra import Data.Comp.Multi.Functor @@ -42,46 +42,46 @@ -- from a functor to a function with a domain constructed with the -- same functor but with an additional product. -liftP :: (HRemoveP s s') => (s' a :-> t) -> s a :-> t-liftP f v = f (hremoveP v)+liftP :: (RemoveP s s') => (s' a :-> t) -> s a :-> t+liftP f v = f (removeP v)   -- | This function annotates each sub term of the given term with the -- given value (of type a). -constP :: (HDistProd f p g, HFunctor f, HFunctor g) -       => p -> HCxt h f a :-> HCxt h g a-constP c = appHSigFun (hinjectP c)+constP :: (DistProd f p g, HFunctor f, HFunctor g) +       => p -> Cxt h f a :-> Cxt h g a+constP c = appSigFun (injectP c)  -- | This function transforms a function with a domain constructed -- from a functor to a function with a domain constructed with the -- same functor but with an additional product. -liftP' :: (HDistProd s' p s, HFunctor s, HFunctor s')-       => (s' a :-> HCxt h s' a) -> s a :-> HCxt h s a-liftP' f v = let (v' :&: p) = hprojectP v+liftP' :: (DistProd s' p s, HFunctor s, HFunctor s')+       => (s' a :-> Cxt h s' a) -> s a :-> Cxt h s a+liftP' f v = let (v' O.:&: p) = projectP v              in constP p (f v')      {-| This function strips the products from a term over a functor whith products. -} -stripP :: (HFunctor f, HRemoveP g f, HFunctor g)-       => HCxt h g a :-> HCxt h f a-stripP = appHSigFun hremoveP+stripP :: (HFunctor f, RemoveP g f, HFunctor g)+       => Cxt h g a :-> Cxt h f a+stripP = appSigFun removeP  -productHTermHom :: (HDistProd f p f', HDistProd g p g', HFunctor g, HFunctor g') -               => HTermHom f g -> HTermHom f' g'-productHTermHom alg f' = constP p (alg f)-    where (f :&: p) = hprojectP f'+productTermHom :: (DistProd f p f', DistProd g p g', HFunctor g, HFunctor g') +               => TermHom f g -> TermHom f' g'+productTermHom alg f' = constP p (alg f)+    where (f O.:&: p) = projectP f'     --- | This function is similar to 'hproject' but applies to signatures+-- | This function is similar to 'project' but applies to signatures -- with a product which is then ignored. --- hproject' :: (HRemoveP s s',s :<<: f) =>---      NatM Maybe (HCxt h f a) (s' (HCxt h f a))-hproject' v = liftM hremoveP $ hproject v+-- project' :: (RemoveP s s',s :<: f) =>+--      NatM Maybe (Cxt h f a) (s' (Cxt h f a))+project' v = liftM removeP $ project v

@@ -26,24 +26,24 @@ import Data.Comp.Multi.Functor import Data.Comp.Derive -instance KShow HNothing where+instance KShow Nothing where     kshow _ = undefined instance KShow (K String) where     kshow = id -instance (HShowF f, HFunctor f) => HShowF (HCxt h f) where-    hshowF (HHole s) = s-    hshowF (HTerm t) = hshowF $ hfmap hshowF t+instance (HShowF f, HFunctor f) => HShowF (Cxt h f) where+    hshowF (Hole s) = s+    hshowF (Term t) = hshowF $ hfmap hshowF t -instance (HShowF f, HFunctor f, KShow a) => KShow (HCxt h f a) where-    kshow = hfree hshowF kshow+instance (HShowF f, HFunctor f, KShow a) => KShow (Cxt h f a) where+    kshow = free hshowF kshow  instance (KShow f) => Show (f i) where     show = unK . kshow -instance (HShowF f, Show p) => HShowF (f :&&: p) where-    hshowF (v :&&: p) =  K $ unK (hshowF v) ++ " :&&: " ++ show p+instance (HShowF f, Show p) => HShowF (f :&: p) where+    hshowF (v :&: p) =  K $ unK (hshowF v) ++ " :&: " ++ show p -instance (HShowF f, HShowF g) => HShowF (f :++: g) where-    hshowF (HInl f) = hshowF f-    hshowF (HInr g) = hshowF g+instance (HShowF f, HShowF g) => HShowF (f :+: g) where+    hshowF (Inl f) = hshowF f+    hshowF (Inr g) = hshowF g

@@ -16,184 +16,165 @@  module Data.Comp.Multi.Sum     (-     (:<<:)(..),-     (:++:)(..),+     (:<:)(..),+     (:+:)(..),       -- * Projections for Signatures and Terms-     hproj2,-     hproj3,-     hproject,-     hproject2,-     hproject3,-     deepHProject,-     deepHProject2,-     deepHProject3,---     deepHProject',---     deepHProject2',---     deepHProject3',+     proj2,+     proj3,+     project,+     project2,+     project3,+     deepProject,+     deepProject2,+     deepProject3,+--     deepProject',+--     deepProject2',+--     deepProject3',       -- * Injections for Signatures and Terms-     hinj2,-     hinj3,-     hinject,-     hinject2,-     hinject3,-     deepHInject,-     deepHInject2,-     deepHInject3,-     deepHInjectE,-     deepHInjectE2,-     deepHInjectE3,+     inj2,+     inj3,+     inject,+     inject2,+     inject3,+     deepInject,+     deepInject2,+     deepInject3,       -- * Injections and Projections for Constants-     hinjectHConst,-     hinjectHConst2,-     hinjectHConst3,-     hprojectHConst,-     hinjectHCxt,-     liftHCxt,-     substHHoles,---     substHHoles'+     injectConst,+     injectConst2,+     injectConst3,+     projectConst,+     injectCxt,+     liftCxt,+     substHoles,+--     substHoles'     ) where  import Data.Comp.Multi.Functor import Data.Comp.Multi.Traversable-import Data.Comp.Multi.ExpFunctor import Data.Comp.Multi.Ops import Data.Comp.Multi.Term import Data.Comp.Multi.Algebra import Control.Monad (liftM) -{-| A variant of 'hproj' for binary sum signatures.  -}-hproj2 :: forall f g1 g2 a i. (g1 :<<: f, g2 :<<: f) =>-          f a i -> Maybe (((g1 :++: g2) a) i)-hproj2 x = case hproj x of-             Just (y :: g1 a i) -> Just $ hinj y-             _ -> liftM hinj (hproj x :: Maybe (g2 a i))+{-| A variant of 'proj' for binary sum signatures.  -}+proj2 :: forall f g1 g2 a i. (g1 :<: f, g2 :<: f) =>+          f a i -> Maybe (((g1 :+: g2) a) i)+proj2 x = case proj x of+             Just (y :: g1 a i) -> Just $ inj y+             _ -> liftM inj (proj x :: Maybe (g2 a i)) -{-| A variant of 'hproj' for ternary sum signatures.  -}-hproj3 :: forall f g1 g2 g3 a i. (g1 :<<: f, g2 :<<: f, g3 :<<: f) =>-          f a i -> Maybe (((g1 :++: g2 :++: g3) a) i)-hproj3 x = case hproj x of-             Just (y :: g1 a i) -> Just $ hinj y-             _ -> case hproj x of-                    Just (y :: g2 a i) -> Just $ hinj y-                    _ -> liftM hinj (hproj x :: Maybe (g3 a i))+{-| A variant of 'proj' for ternary sum signatures.  -}+proj3 :: forall f g1 g2 g3 a i. (g1 :<: f, g2 :<: f, g3 :<: f) =>+          f a i -> Maybe (((g1 :+: g2 :+: g3) a) i)+proj3 x = case proj x of+             Just (y :: g1 a i) -> Just $ inj y+             _ -> case proj x of+                    Just (y :: g2 a i) -> Just $ inj y+                    _ -> liftM inj (proj x :: Maybe (g3 a i))  -- |Project the outermost layer of a term to a sub signature.-hproject :: (g :<<: f) => NatM Maybe (HCxt h f a)  (g (HCxt h f a))-hproject (HHole _) = Nothing-hproject (HTerm t) = hproj t+project :: (g :<: f) => NatM Maybe (Cxt h f a)  (g (Cxt h f a))+project (Hole _) = Nothing+project (Term t) = proj t  -- |Project the outermost layer of a term to a binary sub signature.-hproject2 :: (g1 :<<: f, g2 :<<: f) =>-             NatM Maybe (HCxt h f a) ((g1 :++: g2) (HCxt h f a))-hproject2 (HHole _) = Nothing-hproject2 (HTerm t) = hproj2 t+project2 :: (g1 :<: f, g2 :<: f) =>+             NatM Maybe (Cxt h f a) ((g1 :+: g2) (Cxt h f a))+project2 (Hole _) = Nothing+project2 (Term t) = proj2 t  -- |Project the outermost layer of a term to a ternary sub signature.-hproject3 :: (g1 :<<: f, g2 :<<: f, g3 :<<: f) =>-             NatM Maybe (HCxt h f a) ((g1 :++: g2 :++: g3) (HCxt h f a))-hproject3 (HHole _) = Nothing-hproject3 (HTerm t) = hproj3 t+project3 :: (g1 :<: f, g2 :<: f, g3 :<: f) =>+             NatM Maybe (Cxt h f a) ((g1 :+: g2 :+: g3) (Cxt h f a))+project3 (Hole _) = Nothing+project3 (Term t) = proj3 t  -- |Project a term to a term over a sub signature.-deepHProject :: (HTraversable f, HFunctor g, g :<<: f)-             => NatM Maybe (HCxt h f a) (HCxt h g a)-deepHProject = appHSigFunM hproj+deepProject :: (HTraversable f, HFunctor g, g :<: f)+             => NatM Maybe (Cxt h f a) (Cxt h g a)+deepProject = appSigFunM proj  -- |Project a term to a term over a binary sub signature.-deepHProject2 :: (HTraversable f, HFunctor g1, HFunctor g2,-                  g1 :<<: f, g2 :<<: f)-              => NatM Maybe (HCxt h f a) (HCxt h (g1 :++: g2) a)-deepHProject2 = appHSigFunM hproj2+deepProject2 :: (HTraversable f, HFunctor g1, HFunctor g2,+                  g1 :<: f, g2 :<: f)+              => NatM Maybe (Cxt h f a) (Cxt h (g1 :+: g2) a)+deepProject2 = appSigFunM proj2  -- |Project a term to a term over a ternary sub signature.-deepHProject3 :: (HTraversable f, HFunctor g1, HFunctor g2, HFunctor g3,-                  g1 :<<: f, g2 :<<: f, g3 :<<: f)-              => NatM Maybe (HCxt h f a) (HCxt h (g1 :++: g2 :++: g3) a)-deepHProject3 = appHSigFunM hproj3+deepProject3 :: (HTraversable f, HFunctor g1, HFunctor g2, HFunctor g3,+                  g1 :<: f, g2 :<: f, g3 :<: f)+              => NatM Maybe (Cxt h f a) (Cxt h (g1 :+: g2 :+: g3) a)+deepProject3 = appSigFunM proj3 -{-| A variant of 'hinj' for binary sum signatures.  -}-hinj2 :: (f1 :<<: g, f2 :<<: g) => (f1 :++: f2) a :-> g a-hinj2 (HInl x) = hinj x-hinj2 (HInr y) = hinj y+{-| A variant of 'inj' for binary sum signatures.  -}+inj2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) a :-> g a+inj2 (Inl x) = inj x+inj2 (Inr y) = inj y -{-| A variant of 'hinj' for ternary sum signatures.  -}-hinj3 :: (f1 :<<: g, f2 :<<: g, f3 :<<: g) => (f1 :++: f2 :++: f3) a :-> g a-hinj3 (HInl x) = hinj x-hinj3 (HInr y) = hinj2 y+{-| A variant of 'inj' for ternary sum signatures.  -}+inj3 :: (f1 :<: g, f2 :<: g, f3 :<: g) => (f1 :+: f2 :+: f3) a :-> g a+inj3 (Inl x) = inj x+inj3 (Inr y) = inj2 y  -- |Inject a term where the outermost layer is a sub signature.-hinject :: (g :<<: f) => g (HCxt h f a) :-> HCxt h f a-hinject = HTerm . hinj+inject :: (g :<: f) => g (Cxt h f a) :-> Cxt h f a+inject = Term . inj  -- |Inject a term where the outermost layer is a binary sub signature.-hinject2 :: (f1 :<<: g, f2 :<<: g) => (f1 :++: f2) (HCxt h g a) :-> HCxt h g a-hinject2 = HTerm . hinj2+inject2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) (Cxt h g a) :-> Cxt h g a+inject2 = Term . inj2  -- |Inject a term where the outermost layer is a ternary sub signature.-hinject3 :: (f1 :<<: g, f2 :<<: g, f3 :<<: g)-         => (f1 :++: f2 :++: f3) (HCxt h g a) :-> HCxt h g a-hinject3 = HTerm . hinj3+inject3 :: (f1 :<: g, f2 :<: g, f3 :<: g)+         => (f1 :+: f2 :+: f3) (Cxt h g a) :-> Cxt h g a+inject3 = Term . inj3  -- |Inject a term over a sub signature to a term over larger signature.-deepHInject :: (HFunctor g, HFunctor f, g :<<: f) => HCxt h g a :-> HCxt h f a-deepHInject = appHSigFun hinj+deepInject :: (HFunctor g, HFunctor f, g :<: f) => Cxt h g a :-> Cxt h f a+deepInject = appSigFun inj  -- |Inject a term over a binary sub signature to a term over larger signature.-deepHInject2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<<: g, f2 :<<: g)-             => HCxt h (f1 :++: f2) a :-> HCxt h g a-deepHInject2 = appHSigFun hinj2+deepInject2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g)+             => Cxt h (f1 :+: f2) a :-> Cxt h g a+deepInject2 = appSigFun inj2  -- |Inject a term over a ternary sub signature to a term over larger signature.-deepHInject3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,-                 f1 :<<: g, f2 :<<: g, f3 :<<: g)-             => HCxt h (f1 :++: f2 :++: f3) a :-> HCxt h g a-deepHInject3 = appHSigFun hinj3--{-| A variant of 'deepHInject' for exponential signatures. -}-deepHInjectE :: (HExpFunctor g, g :<<: f) => HTerm g :-> HTerm f-deepHInjectE = hcataE hinject--{-| A variant of 'deepHInject2' for exponential signatures. -}-deepHInjectE2 :: (HExpFunctor g1, HExpFunctor g2, g1 :<<: f, g2 :<<: f) =>-                 HTerm (g1 :++: g2) :-> HTerm f-deepHInjectE2 = hcataE hinject2--{-| A variant of 'deepHInject3' for exponential signatures. -}-deepHInjectE3 :: (HExpFunctor g1, HExpFunctor g2, HExpFunctor g3,-                  g1 :<<: f, g2 :<<: f, g3 :<<: f) =>-                 HTerm (g1 :++: g2 :++: g3) :-> HTerm f-deepHInjectE3 = hcataE hinject3+deepInject3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,+                 f1 :<: g, f2 :<: g, f3 :<: g)+             => Cxt h (f1 :+: f2 :+: f3) a :-> Cxt h g a+deepInject3 = appSigFun inj3  -- | This function injects a whole context into another context.-hinjectHCxt :: (HFunctor g, g :<<: f) => HCxt h' g (HCxt h f a) :-> HCxt h f a-hinjectHCxt = hcata' hinject+injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a+injectCxt = cata' inject  -- | This function lifts the given functor to a context.-liftHCxt :: (HFunctor f, g :<<: f) => g a :-> HContext f a-liftHCxt g = simpHCxt $ hinj g+liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a+liftCxt g = simpCxt $ inj g  -- | This function applies the given context with hole type @a@ to a -- family @f@ of contexts (possibly terms) indexed by @a@. That is, -- each hole @h@ is replaced by the context @f h@. -substHHoles :: (HFunctor f, HFunctor g, f :<<: g)-           => (v :-> HCxt h g a) -> HCxt h' f v :-> HCxt h g a-substHHoles f c = hinjectHCxt $ hfmap f c+substHoles :: (HFunctor f, HFunctor g, f :<: g)+           => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a+substHoles f c = injectCxt $ hfmap f c -hinjectHConst :: (HFunctor g, g :<<: f) => HConst g :-> HCxt h f a-hinjectHConst = hinject . hfmap (const undefined)+injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a+injectConst = inject . hfmap (const undefined) -hinjectHConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<<: g, f2 :<<: g)-               => HConst (f1 :++: f2) :-> HCxt h g a-hinjectHConst2 = hinject2 . hfmap (const undefined)+injectConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g)+               => Const (f1 :+: f2) :-> Cxt h g a+injectConst2 = inject2 . hfmap (const undefined) -hinjectHConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,-                   f1 :<<: g, f2 :<<: g, f3 :<<: g)-               => HConst (f1 :++: f2 :++: f3) :-> HCxt h g a-hinjectHConst3 = hinject3 . hfmap (const undefined)+injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,+                   f1 :<: g, f2 :<: g, f3 :<: g)+               => Const (f1 :+: f2 :+: f3) :-> Cxt h g a+injectConst3 = inject3 . hfmap (const undefined) -hprojectHConst :: (HFunctor g, g :<<: f) => NatM Maybe (HCxt h f a) (HConst g)-hprojectHConst = fmap (hfmap (const (K ()))) . hproject+projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)+projectConst = fmap (hfmap (const (K ()))) . project

@@ -16,73 +16,74 @@ --------------------------------------------------------------------------------  module Data.Comp.Multi.Term -    (HCxt (..),-     HHole,-     HNoHole,-     HContext,-     HNothing,-     HTerm,-     HConst,-     constHTerm,-     unHTerm,-     toHCxt,-     simpHCxt+    (Cxt (..),+     Hole,+     NoHole,+     Context,+     Nothing,+     Term,+     Const,+     constTerm,+     unTerm,+     toCxt,+     simpCxt      ) where  import Data.Comp.Multi.Functor import Unsafe.Coerce -type HConst (f :: (* -> *) -> * -> *) = f (K ())+type Const (f :: (* -> *) -> * -> *) = f (K ())  -- | This function converts a constant to a term. This assumes that -- the argument is indeed a constant, i.e. does not have a value for -- the argument type of the functor f. -constHTerm :: (HFunctor f) => HConst f :-> HTerm f-constHTerm = HTerm . hfmap (const undefined)+constTerm :: (HFunctor f) => Const f :-> Term f+constTerm = Term . hfmap (const undefined)  -- | This data type represents contexts over a signature. Contexts are -- terms containing zero or more holes. The first type parameter is--- supposed to be one of the phantom types 'HHole' and 'HNoHole'. The+-- supposed to be one of the phantom types 'Hole' and 'NoHole'. The -- second parameter is the signature of the context. The third -- parameter is the type family of the holes. The last parameter is -- the index/label. -data HCxt h f a i where-    HTerm ::  f (HCxt h f a) i -> HCxt h f a i-    HHole :: a i -> HCxt HHole f a i+data Cxt h f a i where+    Term ::  f (Cxt h f a) i -> Cxt h f a i+    Hole :: a i -> Cxt Hole f a i --- | Phantom type that signals that a 'HCxt' might contain holes.-data HHole--- | Phantom type that signals that a 'HCxt' does not contain holes.-data HNoHole+-- | Phantom type that signals that a 'Cxt' might contain holes.+data Hole+-- | Phantom type that signals that a 'Cxt' does not contain holes.+data NoHole  -- | A context might contain holes.-type HContext = HCxt HHole+type Context = Cxt Hole -{-| Phantom type family used to define 'HTerm'.  -}-data HNothing :: * -> *+{-| Phantom type family used to define 'Term'.  -}+data Nothing :: * -> * -instance Show (HNothing i) where-instance Eq (HNothing i) where-instance Ord (HNothing i) where+instance Show (Nothing i) where+instance Eq (Nothing i) where+instance Ord (Nothing i) where  -- | A (higher-order) term is a context with no holes.-type HTerm f = HCxt HNoHole f HNothing+type Term f = Cxt NoHole f Nothing  -- | This function unravels the given term at the topmost layer.-unHTerm :: HTerm f t -> f (HTerm f) t-unHTerm (HTerm t) = t+unTerm :: Term f t -> f (Term f) t+unTerm (Term t) = t -instance (HFunctor f) => HFunctor (HCxt h f) where-    hfmap f (HHole x) = HHole (f x)-    hfmap f (HTerm t) = HTerm (hfmap (hfmap f) t)+instance (HFunctor f) => HFunctor (Cxt h f) where+    hfmap f (Hole x) = Hole (f x)+    hfmap f (Term t) = Term (hfmap (hfmap f) t)  -simpHCxt :: (HFunctor f) => f a i -> HContext f a i-simpHCxt = HTerm . hfmap HHole+simpCxt :: (HFunctor f) => f a i -> Context f a i+simpCxt = Term . hfmap Hole -toHCxt :: HTerm f i -> HContext f a i-toHCxt = unsafeCoerce---toHCxt :: (HFunctor f) => HTerm f i -> HContext f a i---toHCxt (HTerm t) = HTerm $ hfmap toHCxt t+{-| Cast a term over a signature to a context over the same signature. -}+toCxt :: (HFunctor f) => Term f :-> Context f a+{-# INLINE toCxt #-}+toCxt = unsafeCoerce+-- equivalentto @Term . (hfmap toCxt) . unTerm@

@@ -10,142 +10,165 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- This module defines an abstraction notion of a variable in a term. All--- definitions are generalised versions of those in "Data.Comp.Variables".+-- This module defines an abstract notion of (bound) variables in compositional+-- data types, and capture-avoiding substitution. All definitions are+-- generalised versions of those in "Data.Comp.Variables". -- ---------------------------------------------------------------------------------module Data.Comp.Multi.Variables  where+module Data.Comp.Multi.Variables+    (+     HasVars(..),+     GSubst,+     CxtSubst,+     Subst,+     varsToHoles,+     containsVar,+     variables,+     variableList,+     variables',+     substVars,+     appSubst,+     compSubst+    ) where  import Data.Comp.Multi.Term import Data.Comp.Multi.Sum import Data.Comp.Multi.Algebra import Data.Comp.Multi.Functor import Data.Comp.Multi.Foldable- import Data.Set (Set) import qualified Data.Set as Set- import Data.Maybe  --- type HCxtSubst h a f v =  [A (v :*: (HCxt h f a))]+-- type CxtSubst h a f v =  [A (v :*: (Cxt h f a))] --- type Subst f v = HCxtSubst HNoHole HNothing f v+-- type Subst f v = CxtSubst NoHole Nothing f v  type GSubst v a = NatM Maybe (K v) a -type HCxtSubst h a f v =  GSubst v (HCxt h f a)--type Subst f v = HCxtSubst HNoHole HNothing f v+type CxtSubst h a f v =  GSubst v (Cxt h f a) -{-| This multiparameter class defines functors with variables. An-instance @HasVar f v@ denotes that values over @f@ might contain-variables of type @v@. -}+type Subst f v = CxtSubst NoHole Nothing f v +{-| 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     isVar :: f a :=> Maybe v     isVar _ = Nothing+    bindsVars :: f a :=> [v]+    bindsVars _ = [] -instance (HasVars f v, HasVars g v) => HasVars (f :++: g) v where-    isVar (HInl v) = isVar v-    isVar (HInr v) = isVar v+instance (HasVars f v, HasVars g v) => HasVars (f :+: g) v where+    isVar (Inl v) = isVar v+    isVar (Inr v) = isVar v+    bindsVars (Inl v) = bindsVars v+    bindsVars (Inr v) = bindsVars v -instance HasVars f v => HasVars (HCxt h f) v where-    isVar (HTerm t) = isVar t+instance HasVars f v => HasVars (Cxt h f) v where+    isVar (Term t) = isVar t     isVar _ = Nothing+    bindsVars (Term t) = bindsVars t+    bindsVars _ = [] -varsToHHoles :: forall f v. (HFunctor f, HasVars f v) => HTerm f :-> HContext f (K v)-varsToHHoles = hcata alg-    where alg :: HAlg f (HContext f (K v))-          alg t = case isVar t of -                    Just v -> HHole $ K v-                    Nothing -> HTerm t+-- Auxiliary data type, used only to define varsToHoles+data C a b i = C{ unC :: a -> b i } -containsVarAlg :: (Eq v, HasVars f v, HFoldable f) => v -> HAlg f (K Bool)-containsVarAlg v t = K $ local || kfoldl (||) False t +varsToHoles :: forall f v. (HFunctor f, HasVars f v, Eq 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 capture-avoidance+                    if v `elem` vars' then+                        Term $ hfmap (\x -> unC x vars') t+                    else+                        Hole $ K v+                Nothing ->+                    Term $ hfmap (\x -> unC x 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)     where local = case isVar t of                     Just v' -> v == v'                     Nothing -> False -{-| This function checks whether a variable is contained in a-context. -}-+{-| This function checks whether a variable is contained in a context. -} containsVar :: (Eq v, HasVars f v, HFoldable f, HFunctor f)-            => v -> HCxt h f a :=> Bool-containsVar v = unK . hfree (containsVarAlg v) (const $ K False)-+            => v -> Cxt h f a :=> Bool+containsVar v = unK . free (containsVarAlg v) (const $ K False) -variableListAlg :: (HasVars f v, HFoldable f)-            => HAlg f (K [v])-variableListAlg t = K $ kfoldl (++) local t+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)-            => HCxt h f a :=> [v]-variableList = unK . hfree variableListAlg (const $ K [])--+{-| This function computes the list of variables occurring in a context. -}+variableList :: (HasVars f v, HFoldable f, HFunctor f, Eq v)+             => Cxt h f a :=> [v]+variableList = unK . free variableListAlg (const $ K []) -variablesAlg :: (Ord v, HasVars f v, HFoldable f)-            => HAlg f (K (Set v))-variablesAlg t = K $ kfoldl Set.union local t+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     where local = case isVar t of                     Just v -> Set.singleton v                     Nothing -> Set.empty -{-| This function computes the set of variables occurring in a-context. -}-+{-| This function computes the set of variables occurring in a context. -} variables :: (Ord v, HasVars f v, HFoldable f, HFunctor f)-            => HCxt h f a :=> Set v-variables = unK . hfree variablesAlg (const $ K Set.empty)--{-| This function computes the set of variables occurring in a-context. -}+            => Cxt h f a :=> Set v+variables = unK . free variablesAlg (const $ K Set.empty) +{-| This function computes the set of variables occurring in a context. -} variables' :: (Ord v, HasVars f v, HFoldable f, HFunctor f)-            => HConst f :=> Set v+            => Const f :=> Set v variables' c =  case isVar c of                   Nothing -> Set.empty                   Just v -> Set.singleton v ---substAlg :: (HasVars f v) => HCxtSubst h a f v -> HAlg f (HCxt h f a)-substAlg f t = fromMaybe (HTerm t) (isVar t >>= f . K)- {-| This function substitutes variables in a context according to a partial mapping from variables to contexts.-}- class SubstVars v t a where     substVars :: GSubst v t -> a :-> a - appSubst :: SubstVars v t a => GSubst v t -> a :-> a appSubst = substVars -instance (Ord v, HasVars f v, HFunctor f) => SubstVars v (HCxt h f a) (HCxt h f a) where-    substVars f (HTerm v) = substAlg f $ hfmap (substVars f) v-    substVars _ (HHole a) = HHole a--- have to use explicit GADT pattern matching!!--- subst f = hfree (substAlg f) HHole+instance (Ord v, HasVars f v, HFunctor 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) = substAlg 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 t >>= f . K)+    -- The code below does not work with GHC 7+    -- substVars _ (Hole a) = Hole a+    -- substVars f (Term v) = let f' = res (bindsVars v) f in+    --                         substAlg f' $ hfmap (substVars 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 t >>= f . K)+    --            res :: Eq v => [v] -> GSubst v t -> GSubst v t+    --            res vars f x = if unK x `elem` vars then Nothing else f x  instance (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where     substVars f = hfmap (substVars f)  -- {-| 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)-          => HCxtSubst h a f v -> HCxtSubst h a f v -> HCxtSubst h a f v+          => 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

@@ -23,8 +23,6 @@ import Control.Applicative import Control.Monad hiding (sequence, mapM) -import Data.Comp.ExpFunctor- import Prelude hiding (foldl, mapM, sequence, foldl1, foldr1, foldr)  @@ -65,10 +63,6 @@     sequence (Inl e) = Inl `liftM` sequence e     sequence (Inr e) = Inr `liftM` sequence e -instance (ExpFunctor f, ExpFunctor g) => ExpFunctor (f :+: g) where-    xmap f g (Inl e) = Inl (xmap f g e)-    xmap f g (Inr e) = Inr (xmap f g e)- -- | Signature containment relation for automatic injections. The left-hand must -- be an atomic signature, where as the right-hand side must have a list-like -- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,@@ -131,9 +125,6 @@     sequenceA (v :&: c) = liftA (:&: c)(sequenceA v)     mapM f (v :&: c) = liftM (:&: c) (mapM f v)     sequence (v :&: c) = liftM (:&: c) (sequence v)--instance (ExpFunctor f) => ExpFunctor (f :&: a) where-    xmap f g (v :&: c) = xmap f g v :&: c  {-| This class defines how to distribute a product over a sum of signatures. -}

@@ -42,9 +42,6 @@      deepInject,      deepInject2,      deepInject3,-     deepInjectE,-     deepInjectE2,-     deepInjectE3,       -- * Injections and Projections for Constants      injectConst,@@ -60,7 +57,6 @@ import Data.Comp.Term import Data.Comp.Algebra import Data.Comp.Ops-import Data.Comp.ExpFunctor  import Control.Monad hiding (sequence) import Prelude hiding (sequence)@@ -183,23 +179,6 @@                 f1 :<: g, f2 :<: g, f3 :<: g)             => Cxt h (f1 :+: f2 :+: f3) a -> Cxt h g a deepInject3 =  appSigFun inj3--{-| A variant of 'deepInject' for exponential signatures. -}-deepInjectE :: (ExpFunctor g, g :<: f) => Term g -> Term f-deepInjectE = cataE inject--{-| A variant of 'deepInject2' for exponential signatures. -}-deepInjectE2 :: (ExpFunctor g1, ExpFunctor g2, g1 :<: f, g2 :<: f) =>-                Term (g1 :+: g2)-             -> Term f-deepInjectE2 = cataE inject2--{-| A variant of 'deepInject3' for exponential signatures. -}-deepInjectE3 :: (ExpFunctor g1, ExpFunctor g2, ExpFunctor g3,-                 g1 :<: f, g2 :<: f, g3 :<: f) =>-                Term (g1 :+: g2 :+: g3)-             -> Term f-deepInjectE3 = cataE inject3  injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a injectConst = inject . fmap (const undefined)

@@ -33,7 +33,6 @@  import Data.Traversable import Data.Foldable- import Unsafe.Coerce  import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)@@ -72,15 +71,16 @@ type Context = Cxt Hole  {-| Convert a functorial value into a context.  -}-simpCxt :: (Functor f) => f a -> Context f a+simpCxt :: Functor f => f a -> Context f a {-# INLINE simpCxt #-} simpCxt = Term . fmap Hole   {-| Cast a term over a signature to a context over the same signature. -}-toCxt :: Term f -> Cxt h f a+toCxt :: Functor f => Term f -> Cxt h f a {-# INLINE toCxt #-} toCxt = unsafeCoerce+-- equivalent to @Term . (fmap toCxt) . unTerm@  {-| Phantom type used to define 'Term'.  -} 

@@ -5,150 +5,155 @@ -- Module      :  Data.Comp.Variables -- Copyright   :  (c) 2010-2011 Patrick Bahr -- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Maintainer  :  Patrick Bahr <paba@diku.dk> and Tom Hvitved <hvitved@diku.dk> -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- This module defines an abstraction notion of a variable in compositional--- data type.+-- This module defines an abstract notion of (bound) variables in compositional+-- data types, and capture-avoiding substitution. -- ---------------------------------------------------------------------------------module Data.Comp.Variables (-  HasVars(..),-  Subst,-  CxtSubst,-  varsToHoles,-  containsVar,-  variables,-  variableList,-  variables',-  substVars,-  appSubst,-  compSubst) where+module Data.Comp.Variables+    (+     HasVars(..),+     Subst,+     CxtSubst,+     varsToHoles,+     containsVar,+     variables,+     variableList,+     variables',+     substVars,+     appSubst,+     compSubst+    ) where  import Data.Comp.Term import Data.Comp.Sum import Data.Comp.Algebra-import Data.Foldable-+import Data.Foldable hiding (elem, notElem) import Data.Maybe- import Data.Set (Set) import qualified Data.Set as Set- import Data.Map (Map) import qualified Data.Map as Map- import Prelude hiding (or, foldl)  type CxtSubst h a f v = Map v (Cxt h f a)  type Subst f v = CxtSubst NoHole Nothing f v -{-| This multiparameter class defines functors with variables. An-instance @HasVar f v@ denotes that values over @f@ might contain-variables of type @v@. -}-+{-| 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.     isVar :: f a -> Maybe v     isVar _ = Nothing+    -- |Indicates the set of variables bound by the @f@ constructor.+    bindsVars :: f a -> [v]+    bindsVars _ = []  instance (HasVars f v, HasVars g v) => HasVars (f :+: g) v where     isVar (Inl v) = isVar v     isVar (Inr v) = isVar v+    bindsVars (Inl v) = bindsVars v+    bindsVars (Inr v) = bindsVars v  instance HasVars f v => HasVars (Cxt h f) v where     isVar (Term t) = isVar t     isVar _ = Nothing+    bindsVars (Term t) = bindsVars t+    bindsVars _ = [] -varsToHoles :: (Functor f, HasVars f v) => Term f -> Context f v-varsToHoles = cata alg-    where alg t = case isVar t of -                    Just v -> Hole v-                    Nothing -> Term t+-- |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 capture-avoidance+                    if v `elem` vars' then+                        Term $ fmap (\x -> x vars') t+                    else+                        Hole v+                Nothing ->+                    Term $ fmap (\x -> x vars') t +-- |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 = local || or t +containsVarAlg v t = v `notElem` bindsVars t && (local || or t)     where local = case isVar t of                     Just v' -> v == v'                     Nothing -> False -{-| This function checks whether a variable is contained in a-context. -}-+{-| This function checks whether a variable is contained in a context. -} containsVar :: (Eq v, HasVars f v, Foldable f, Functor f)             => v -> Cxt h f a -> Bool containsVar v = free (containsVarAlg v) (const False) -variablesAlg :: (Ord v, HasVars f v, Foldable f)-            => Alg f (Set v)-variablesAlg t = foldl Set.union local t+-- |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     where local = case isVar t of                     Just v -> Set.singleton v                     Nothing -> Set.empty -variableListAlg :: (Ord v, HasVars f v, Foldable f)-            => Alg f [v]-variableListAlg t = foldl (++) local t+-- |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]+{-| 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 []) -{-| 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+{-| 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 = free variablesAlg (const Set.empty) -{-| This function computes the set of variables occurring in a-context. -}--variables' :: (Ord v, HasVars f v, Foldable f, Functor f)-            => Const f -> Set v-variables' c =  case isVar c of-                  Nothing -> Set.empty-                  Just v -> Set.singleton v---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)--{-| This function substitutes variables in a context according to a-partial mapping from variables to contexts.-}--+{-| This function computes the set of variables occurring in a constant. -}+variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v+variables' c = case isVar c of+                 Nothing -> Set.empty+                 Just v -> Set.singleton v +{-| This multiparameter class defines substitution of values of type @t@ for+  variables of type @v@ in values of type @a@. -} class SubstVars v t a where     substVars :: (v -> Maybe t) -> a -> a -+-- |Apply the given substitution. appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a appSubst subst = substVars f     where f v = Map.lookup v subst -instance (Ord v, HasVars f v, Functor f) => SubstVars v (Cxt h f a) (Cxt h f a) where-    substVars f (Term v) = substAlg f $ fmap (substVars f) v+instance (Ord v, HasVars f v, Functor 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--- have to use explicit GADT pattern matching!!--- subst f = free (substAlg f) Hole+    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  instance (SubstVars v t a, Functor f) => SubstVars v t (f a) where     substVars f = fmap (substVars f)  -- {-| 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)           => 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