compdata 0.3 → 0.4

raw patch · 52 files changed

+1138/−947 lines, 52 filesdep +Stream

Dependencies added: Stream

Files

benchmark/Functions/Comp/Desugar.hs +3/−3
benchmark/Functions/Comp/Eval.hs +2/−2
benchmark/Functions/Comp/Inference.hs +2/−2
benchmark/Multi/Functions/Comp/Desugar.hs +2/−2
benchmark/Multi/Functions/Comp/Eval.hs +1/−1
compdata.cabal +6/−3
examples/Examples/DesugarPos.hs +1/−1
examples/Examples/GTermHom.hs +0/−230
examples/Examples/Multi/DesugarEval.hs +1/−1
examples/Examples/MultiParam/DesugarEval.hs +4/−5
examples/Examples/MultiParam/DesugarPos.hs +3/−3
examples/Examples/MultiParam/Eval.hs +2/−3
examples/Examples/MultiParam/EvalI.hs +1/−2
examples/Examples/MultiParam/EvalM.hs +3/−5
examples/Examples/MultiParam/FOL.hs +4/−4
examples/Examples/Param/DesugarEval.hs +5/−11
examples/Examples/Param/DesugarPos.hs +7/−9
examples/Examples/Param/Eval.hs +2/−3
examples/Examples/Param/EvalM.hs +2/−4
examples/Examples/Param/Parsing.hs +5/−5
src/Data/Comp/Algebra.hs +235/−235
src/Data/Comp/Annotation.hs +2/−2
src/Data/Comp/Automata.hs +266/−0
src/Data/Comp/Automata/Product.hs +27/−0
src/Data/Comp/Automata/Product/Derive.hs +81/−0
src/Data/Comp/Derive/SmartConstructors.hs +4/−4
src/Data/Comp/Desugar.hs +3/−3
src/Data/Comp/Generic.hs +4/−4
src/Data/Comp/Multi.hs +5/−5
src/Data/Comp/Multi/Algebra.hs +40/−40
src/Data/Comp/Multi/Annotation.hs +1/−1
src/Data/Comp/Multi/Desugar.hs +3/−3
src/Data/Comp/Multi/Functor.hs +2/−2
src/Data/Comp/Multi/Ops.hs +1/−1
src/Data/Comp/MultiParam/Algebra.hs +57/−57
src/Data/Comp/MultiParam/Annotation.hs +2/−2
src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs +7/−6
src/Data/Comp/MultiParam/Derive/SmartConstructors.hs +6/−5
src/Data/Comp/MultiParam/Desugar.hs +3/−3
src/Data/Comp/MultiParam/HDifunctor.hs +2/−2
src/Data/Comp/Param/Algebra.hs +243/−243
src/Data/Comp/Param/Annotation.hs +2/−2
src/Data/Comp/Param/Derive/SmartAConstructors.hs +6/−6
src/Data/Comp/Param/Derive/SmartConstructors.hs +6/−5
src/Data/Comp/Param/Desugar.hs +3/−3
src/Data/Comp/Param/Difunctor.hs +6/−2
src/Data/Comp/Param/Sum.hs +3/−3
src/Data/Comp/Param/Term.hs +3/−3
src/Data/Comp/TermRewriting.hs +1/−1
src/Data/Comp/Zippable.hs +53/−0
testsuite/tests/Data/Comp/Examples/MultiParam.hs +1/−1
testsuite/tests/Data/Comp/Examples/Param.hs +4/−4

benchmark/Functions/Comp/Desugar.hs view

@@ -17,7 +17,7 @@ -- de-sugar  class (Functor e, Traversable f) => Desug f e where-    desugAlg :: TermHom f e+    desugAlg :: Hom f e  desugExpr :: SugarExpr -> Expr desugExpr = desug@@ -27,11 +27,11 @@  desug :: Desug f e => Term f -> Term e {-# INLINE desug #-}-desug = appTermHom desugAlg+desug = appHom desugAlg  desug' :: Desug f e => Term f -> Term e {-# INLINE desug' #-}-desug' = appTermHom' desugAlg+desug' = appHom' desugAlg  $(derive [liftSum] [''Desug])

benchmark/Functions/Comp/Eval.hs view

@@ -245,7 +245,7 @@ evalSugar = eval  desugEvalAlg  :: AlgM Err SugarSig ValueExpr-desugEvalAlg = evalAlg  `compAlgM'` (desugAlg :: TermHom SugarSig ExprSig)+desugEvalAlg = evalAlg  `compAlgM'` (desugAlg :: Hom SugarSig ExprSig)   desugEval' :: SugarExpr -> Err ValueExpr@@ -262,7 +262,7 @@   desugEval2Alg  :: Alg SugarSig ValueExpr-desugEval2Alg = eval2Alg  `compAlg` (desugAlg :: TermHom SugarSig ExprSig)+desugEval2Alg = eval2Alg  `compAlg` (desugAlg :: Hom SugarSig ExprSig)   desugEval2' :: SugarExpr -> ValueExpr

benchmark/Functions/Comp/Inference.hs view

@@ -71,7 +71,7 @@ typeSugar = inferType  desugTypeAlg  :: AlgM Err SugarSig BaseType-desugTypeAlg = inferTypeAlg  `compAlgM'` (desugAlg :: TermHom SugarSig ExprSig)+desugTypeAlg = inferTypeAlg  `compAlgM'` (desugAlg :: Hom SugarSig ExprSig)  desugType' :: SugarExpr -> Err BaseType desugType' e = cataM desugTypeAlg e@@ -132,7 +132,7 @@ typeSugar2 = inferType2  desugTypeAlg2  :: Alg SugarSig BaseType-desugTypeAlg2 = inferTypeAlg2  `compAlg` (desugAlg :: TermHom SugarSig ExprSig)+desugTypeAlg2 = inferTypeAlg2  `compAlg` (desugAlg :: Hom SugarSig ExprSig)  desugType2' :: SugarExpr -> BaseType desugType2' e = cata desugTypeAlg2 e

benchmark/Multi/Functions/Comp/Desugar.hs view

@@ -17,7 +17,7 @@ -- de-sugar  class (HFunctor e, HFunctor f) => Desugar f e where-    desugarAlg :: HTermHom f e+    desugarAlg :: HHom f e     desugarAlg = desugarAlg' . hfmap HHole     desugarAlg' :: HAlg f (HContext e a)     desugarAlg' x = appHCxt $ desugarAlg x@@ -26,7 +26,7 @@ desugarExpr = desugar  desugar :: Desugar f e => HTerm f :-> HTerm e-desugar = appHTermHom desugarAlg+desugar = appHHom desugarAlg  instance (Desugar f e, Desugar g e) => Desugar (g :++: f) e where     desugarAlg (HInl v) = desugarAlg v

benchmark/Multi/Functions/Comp/Eval.hs view

@@ -72,7 +72,7 @@ evalSugar = eval  desugarEvalAlg  :: Alg SugarSig ValueExpr-desugarEvalAlg = evalAlg  `compAlg` (desugarAlg :: TermHom SugarSig ExprSig)+desugarEvalAlg = evalAlg  `compAlg` (desugarAlg :: Hom SugarSig ExprSig)  desugarEval' :: SugarExpr :-> ValueExpr desugarEval' e = cata desugarEvalAlg e

compdata.cabal view

@@ -1,5 +1,5 @@ Name:			compdata-Version:		0.3+Version:		0.4 Synopsis:            	Compositional Data Types Description: @@ -122,7 +122,6 @@   benchmark/Functions/Standard/Inference.hs   benchmark/Functions/Standard.hs   -- example files-  examples/Examples/GTermHom.hs   examples/Examples/Eval.hs   examples/Examples/EvalM.hs   examples/Examples/DesugarEval.hs@@ -175,6 +174,9 @@                         Data.Comp.Derive,                         Data.Comp.Matching,                         Data.Comp.Desugar,+                        Data.Comp.Automata,+                        Data.Comp.Automata.Product,+                        Data.Comp.Zippable,                          Data.Comp.Multi,                         Data.Comp.Multi.Term,@@ -238,6 +240,7 @@                         Data.Comp.Derive.Traversable,                         Data.Comp.Derive.Injections,                         Data.Comp.Derive.Projections,+                        Data.Comp.Automata.Product.Derive,                          Data.Comp.Multi.Derive.Functor,                         Data.Comp.Multi.Derive.Foldable,@@ -271,7 +274,7 @@                         Data.Comp.MultiParam.Derive.Injections,                         Data.Comp.MultiParam.Derive.Projections -  Build-Depends:	base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, th-expand-syns, transformers+  Build-Depends:	base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, th-expand-syns, transformers, Stream   hs-source-dirs:	src   ghc-options:          -W   if flag(benchmark)

examples/Examples/DesugarPos.hs view

@@ -58,7 +58,7 @@  -- Lift desugaring to terms annotated with source positions desugP :: Term SigP' -> Term SigP-desugP = appTermHom (propAnn desugHom)+desugP = appHom (propAnn desugHom)  -- Example: desugPEx = iAPair (Pos 1 0) --                            (iASnd (Pos 1 0) (iAPair (Pos 1 1)

− examples/Examples/GTermHom.hs

@@ -1,230 +0,0 @@-{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances,-  FlexibleContexts, UndecidableInstances, TemplateHaskell, TypeOperators,-  ImplicitParams, GADTs #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.GTermHom--- Copyright   :  (c) 2010-2011 Patrick Bahr--- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)-----------------------------------------------------------------------------------------module Examples.GTermHom where--import Data.Comp-import Data.Comp.Show ()-import Data.Map (Map)-import Data.Maybe-import qualified Data.Map as Map-import Control.Monad-import Data.Comp.Derive---- | An instance @a :< b@ means that @a@ is a component of @b@. @a@--- can be extracted from @b@ via the method 'ex'.-class a :< b where-    ex :: b -> a--instance a :< a where-    ex = id--instance a :< (a,b) where-    ex = fst--instance (a :< b) => a :< (a',b) where-    ex = ex . snd---- | This function provides access to components of the states from--- "below".-below :: (?below :: a -> q, p :< q) => a -> p-below = ex . ?below---- | This function provides access to components of the state from--- "above"-above :: (?above :: q, p :< q) => p-above = ex ?above---- | This type represents generalised term homomorphisms. Generalised--- term homomorphisms have access to a state that is provided--- (separately) by a DUTA or a DDTA (or both).-type GTermHom q f g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a--class Functor f => Zippable f where-    fzip :: f a -> [b] -> Maybe (f (a,b))-    fzip = fzipWith (\ x y -> (x,y))-    fzipWith :: (a -> b -> c) -> f a -> [b] -> Maybe (f c)-    fzipWith f s l = fmap (fmap $ uncurry f) (fzip s l)---- | This type represents transition functions of deterministic--- bottom-up tree transducers (DUTTs).--type UpTrans q f g = forall a. f (q,a) -> (q, Context g a)----- | This type represents transition functions of deterministic--- bottom-up tree acceptors (DUTAs).-type UpState f q = Alg f q---- | This function combines the product DUTA of the two given DUTAs.-prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p,q)-prodUpState sp sq t = (p,q) where-    p = sp $ fmap fst t-    q = sq $ fmap snd t---- | This function transforms DUTT transition function into an--- algebra.--upAlg :: (Functor g)  => UpTrans q f g -> Alg f (q, Term g)-upAlg trans = fmap appCxt . trans ---- | This function runs the given DUTT on the given term.--runUpTrans :: (Functor f, Functor g) => UpTrans q f g -> Term f -> (q, Term g)-runUpTrans = cata . upAlg---- | This function generalises 'runUpTrans' to contexts. Therefore,--- additionally, a transition function for the holes is needed.-runUpTrans' :: (Functor f, Functor g) => UpTrans q f g -> (a -> q) -> Context f a -> (q, Context g a)-runUpTrans' trans st = run where-    run (Hole a) = (st a, Hole a)-    run (Term t) = fmap appCxt $ trans $ fmap run t---- | This function composes two DUTTs.-compUpTrans :: (Functor f, Functor g, Functor h)-               => UpTrans q2 g h -> UpTrans q1 f g -> UpTrans (q1,q2) f h-compUpTrans t2 t1 x = ((q1,q2), fmap snd c2) where-    (q1, c1) = t1 $ fmap (\((q1,q2),a) -> (q1,(q2,a))) x-    (q2, c2) = runUpTrans' t2 fst c1---- | This function turns constructs a DUTT from a given generalised--- term homomorphism with the state propagated by the given DUTA.-toUpTrans :: (Functor f, Functor g) => UpState f q -> GTermHom q f g -> UpTrans q f g-toUpTrans alg f t = (q, c)-    where q = alg $ fmap fst t-          c =  fmap snd $ (let ?below = fst; ?above = q in f t)---- | This function applies a given generalised term homomorphism with--- a state space propagated by the given DUTA to a term.-upTermHom :: (Functor f, Functor g) => UpState f q -> GTermHom q f g -> Term f -> (q,Term g)-upTermHom alg h = runUpTrans (toUpTrans alg h)---- | This function generalised 'upTermHom' to contexts. To this end--- also a transition function for holes is required.-upTermHom' :: (Functor f, Functor g) => UpState f q -> GTermHom q f g -> (a -> q) -> Context f a -> (q, Context g a)-upTermHom' alg h = runUpTrans' (toUpTrans alg h)----- | This type represents transition functions of deterministic--- top-down tree transducers (DDTTs).--type DownTrans q f g = forall a. (q, f a) -> Context g (q,a)---- | This function runs the given DDTT on the given tree.-runDownTrans :: (Functor f, Functor g) => DownTrans q f g -> q -> Cxt h f a -> Cxt h g a-runDownTrans tr q t = run (q,t) where-    run (q,Term t) = appCxt $ fmap run $  tr (q, t)-    run (_,Hole a)      = Hole a---- | This function runs the given DDTT on the given tree.-runDownTrans' :: (Functor f, Functor g) => DownTrans q f g -> q -> Cxt h f a -> Cxt h g (q,a)-runDownTrans' tr q t = run (q,t) where-    run (q,Term t) = appCxt $ fmap run $  tr (q, t)-    run (q,Hole a)      = Hole (q,a)---- | This function composes two DDTTs.-compDownTrans :: (Functor f, Functor g, Functor h)-              => DownTrans p g h -> DownTrans q f g -> DownTrans (q,p) f h-compDownTrans t2 t1 ((q,p), t) = fmap (\(p, (q, a)) -> ((q,p),a)) $ runDownTrans' t2 p (t1 (q, t))----- | This type represents transition functions of deterministic--- top-down tree acceptors (DDTAs).-type DownState f q = forall a. Ord a => (q, f a) -> Map a q---- | This type is needed to construct the product of two DDTAs.-data ProdState p q = LState p-                   | RState q-                   | BState p q---- | This function constructs the product DDTA of the given two DDTAs.-prodDownState :: DownState f p -> DownState f q -> DownState f (p,q)-prodDownState sp sq ((p,q),t) = Map.map final $ Map.unionWith combine ps qs-    where ps = Map.map LState $ sp (p, t)-          qs = Map.map RState $ sq (q, t)-          combine (LState p) (RState q) = BState p q-          combine (RState q) (LState p) = BState p q-          combine _ _                   = error "unexpected merging"-          final (LState p) = (p, q)-          final (RState q) = (p, q)-          final (BState p q) = (p,q)---- | This type is used for applying a DDTAs.-newtype Numbered a = Numbered (a, Int)--instance Eq (Numbered a) where-    Numbered (_,i) == Numbered (_,j) = i == j--instance Ord (Numbered a) where-    compare (Numbered (_,i))  (Numbered (_,j)) = i `compare` j---- | This function constructs a DDTT from a given generalised term--- homomorphism with the state propagated by the given DDTA.-toDownTrans :: Zippable f => DownState f q -> GTermHom q f g -> DownTrans q f g-toDownTrans st f (q, s) = c-    where s' = fromJust $ fzipWith (curry Numbered) s [0 ..]-          qmap = st (q,s')-          qfun = \ k@(Numbered (a,_)) -> (Map.findWithDefault q k qmap ,a)-          s'' = fmap qfun s'-          c   = (let ?above = q; ?below = fst in f) s''----- | This function applies a given generalised term homomorphism with--- a state space propagated by the given DUTA to a term.-downTermHom :: (Zippable f, Functor g)-            => DownState f q -> GTermHom q f g -> q -> Term f -> Term g-downTermHom st h = runDownTrans (toDownTrans st h)------------------- Example ------------------data Str a = Str-data Base a = Char | List a--type Typ = Str :+: Base--$(derive [makeFunctor,smartConstructors, makeShowF] [''Str,''Base])--class StringType f g where-    strTypeHom :: (Bool :< q) => GTermHom q f g--$(derive [liftSum] [''StringType])--strType :: (Base :<: f, Functor f, Functor g, StringType f g)-        => Term f -> Term g-strType = snd . upTermHom isCharAlg strTypeHom--isCharAlg :: (Base :<: f) => Alg f Bool-isCharAlg t = case proj t of-                Just Char -> True-                _ -> False-    -instance (Str :<: f, Functor f) =>  StringType Str f where-    strTypeHom = simpCxt . inj--instance (Str :<:  f, Base :<: f, Functor f) =>  StringType Base f where-    strTypeHom Char = iChar-    strTypeHom (List t)-               | below t  = iStr -               | otherwise = iList $ Hole t---ex1 :: Term Typ-ex1 = iList iChar--runEx1 :: Term Typ-runEx1 = strType ex1

examples/Examples/Multi/DesugarEval.hs view

@@ -81,7 +81,7 @@ -- Compose the evaluation algebra and the desugaring homomorphism to an -- algebra eval :: Term Sig' :-> Term Value-eval = cata (evalAlg `compAlg` (desugHom :: TermHom Sig' Sig))+eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))  -- Example: evalEx = iPair (iConst 2) (iConst 1) evalEx :: Term Value (Int,Int)

examples/Examples/MultiParam/DesugarEval.hs view

@@ -60,12 +60,11 @@          [''Const, ''Lam, ''App, ''Op, ''IfThenElse, ''Sug]) $(derive [makeHFoldable, makeHTraversable]          [''Const, ''App, ''Op])-$(derive [smartConstructors] [''Fun])  instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, HDifunctor f)   => Desugar Sug f where   desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = iLam y `iApp` x+  desugHom' (Let x y) = inject (Lam y) `iApp` x  -- Term evaluation algebra class Eval f v where@@ -75,7 +74,7 @@  -- Compose the evaluation algebra and the desugaring homomorphism to an algebra eval :: Term Sig' :-> Term Value-eval = cata (evalAlg `compAlg` (desugHom :: TermHom Sig' Sig))+eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))  instance (Const :<: v) => Eval Const v where   evalAlg (Const n) = iConst n@@ -88,7 +87,7 @@   evalAlg (App x y) = (projF x) y  instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = iFun f+  evalAlg (Lam f) = inject $ Fun f  instance (Const :<: v) => Eval IfThenElse v where   evalAlg (IfThenElse c v1 v2) = if projC c /= 0 then v1 else v2@@ -105,4 +104,4 @@  -- Example: evalEx = Just (iConst -6) evalEx :: Maybe (Term GValue Int)-evalEx = evalG $ iLet (iConst 6) $ \x -> iNeg $ Place x+evalEx = evalG $ iLet (iConst 6) $ \x -> iNeg x

examples/Examples/MultiParam/DesugarPos.hs view

@@ -64,12 +64,12 @@ instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, HDifunctor f)   => Desugar Sug f where   desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = iLam y `iApp` x+  desugHom' (Let x y) = inject (Lam y) `iApp` x  -- Example: desugPEx == iAApp (Pos 1 0)--- (iALam (Pos 1 0) $ \x -> iAMult (Pos 1 2) (iAConst (Pos 1 2) (-1)) (Place x))+-- (iALam (Pos 1 0) $ \x -> iAMult (Pos 1 2) (iAConst (Pos 1 2) (-1)) x) -- (iAConst (Pos 1 1) 6) desugPEx :: Term SigP Int desugPEx = desugarA (iALet (Pos 1 0)                            (iAConst (Pos 1 1) 6)-                           (\x -> iANeg (Pos 1 2) $ Place x :: Term SigP' Int))+                           (\x -> iANeg (Pos 1 2) x :: Term SigP' Int))

examples/Examples/MultiParam/Eval.hs view

@@ -57,7 +57,6 @@          [''Const, ''Lam, ''App, ''Op]) $(derive [makeHFoldable, makeHTraversable]          [''Const, ''App, ''Op])-$(derive [smartConstructors] [''Fun])  -- Term evaluation algebra class Eval f v where@@ -80,7 +79,7 @@   evalAlg (App x y) = (projF x) y  instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = iFun f+  evalAlg (Lam f) = inject $ Fun f  projC :: (Const :<: v) => Term v Int -> Int projC v = case project v of Just (Const n) -> n@@ -94,4 +93,4 @@  -- Example: evalEx = Just (iConst 4) evalEx :: Maybe (Term GValue Int)-evalEx = evalG $ (iLam $ \x -> Place x `iAdd` Place x) `iApp` iConst 2+evalEx = evalG $ (iLam $ \x -> x `iAdd` x) `iApp` iConst 2

examples/Examples/MultiParam/EvalI.hs view

@@ -72,5 +72,4 @@  -- Example: evalEx = 4 evalEx :: Int-evalEx = eval $ ((iLam $ \x -> Place x `iAdd` Place x) `iApp` iConst 2-                 :: Term Sig Int)+evalEx = eval $ ((iLam $ \x -> x `iAdd` x) `iApp` iConst 2 :: Term Sig Int)

examples/Examples/MultiParam/EvalM.hs view

@@ -53,7 +53,6 @@          [''Const, ''Lam, ''App, ''Op]) $(derive [makeHFoldable, makeHTraversable]          [''Const, ''App, ''Op])-$(derive [smartConstructors] [''FunM])  -- Term evaluation algebra. class EvalM f v where@@ -81,7 +80,7 @@                             (getCompose . f) =<< getCompose my  instance (FunM Maybe :<: v) => EvalM Lam v where-  evalAlgM (Lam f) = return $ iFunM f+  evalAlgM (Lam f) = return $ inject $ FunM f  projC :: (Const :<: v) => Term v Int -> Maybe Int projC v = case project v of@@ -90,7 +89,7 @@ projF :: (FunM Maybe :<: v)          => Term v (i -> j) -> Maybe (Term v i -> Compose Maybe (Term v) j) projF v = case project v of-            Just (FunM f :: FunM Maybe a (Term v) (i -> j)) -> return f+            Just (FunM f :: FunM Maybe Any (Term v) (i -> j)) -> return f             _ -> Nothing  -- |Evaluation of expressions to ground values.@@ -99,6 +98,5 @@  -- Example: evalEx = Just (iConst 12) (3 * (2 + 2) = 12) evalMEx :: Maybe (Term GValue Int)-evalMEx = evalMG $ (iLam $ \x -> iLam $ \y ->-                                 Place y `iMult` (Place x `iAdd` Place x))+evalMEx = evalMG $ (iLam $ \x -> iLam $ \y -> y `iMult` (x `iAdd` x))                    `iApp` iConst 2 `iApp` iConst 3

examples/Examples/MultiParam/FOL.hs view

@@ -150,7 +150,7 @@               Exists :+: Forall  class ElimImp f where-    elimImpHom :: TermHom f Stage1+    elimImpHom :: Hom f Stage1  $(derive [liftSum] [''ElimImp]) @@ -161,7 +161,7 @@     elimImpHom (Impl f1 f2) = iNot (Hole f1) `iOr` (Hole f2)  elimImp :: Term Input :-> Term Stage1-elimImp = appTermHom elimImpHom+elimImp = appHom elimImpHom  foodFact1 :: Term Stage1 TFormula foodFact1 = elimImp foodFact@@ -174,7 +174,7 @@               Exists :+: Forall  class Dualize f where-    dualizeHom :: TermHom f Stage2+    dualizeHom :: Hom f Stage2  $(derive [liftSum] [''Dualize]) @@ -206,7 +206,7 @@     dualizeHom (Forall f) = iExists (Hole . f)  dualize :: Term Stage2 :-> Term Stage2-dualize = appTermHom dualizeHom+dualize = appHom dualizeHom  class PushNot f where     pushNotAlg :: Alg f (Term Stage2)

examples/Examples/Param/DesugarEval.hs view

@@ -51,16 +51,13 @@          [''Const, ''Lam, ''App, ''Op, ''IfThenElse, ''Sug]) $(derive [makeDitraversable]          [''Const, ''App, ''Op])-$(derive [smartConstructors] [''Fun])  instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, Difunctor f)   => Desugar Sug f where   desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = iLam y `iApp` x-  desugHom' Fix       = iLam $ \f ->-                           (iLam $ \x -> Place f `iApp` (Place x `iApp` Place x))-                           `iApp`-                           (iLam $ \x -> Place f `iApp` (Place x `iApp` Place x))+  desugHom' (Let x y) = inject (Lam y) `iApp` x+  desugHom' Fix       = iLam $ \f -> (iLam $ \x -> f `iApp` (x `iApp` x)) `iApp`+                                     (iLam $ \x -> f `iApp` (x `iApp` x))  -- Term evaluation algebra class Eval f v where@@ -86,7 +83,7 @@   evalAlg (App x y) = (projF x) y  instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = iFun f+  evalAlg (Lam f) = inject $ Fun f  instance (Const :<: v) => Eval IfThenElse v where   evalAlg (IfThenElse c v1 v2) = if projC c /= 0 then v1 else v2@@ -109,7 +106,4 @@ fact = iFix `iApp`        (iLam $ \f ->           iLam $ \n ->-              iIfThenElse-              (Place n)-              (Place n `iMult` (Place f `iApp` (Place n `iAdd` iConst (-1))))-              (iConst 1))+              iIfThenElse n  (n `iMult` (f `iApp` (n `iAdd` iConst (-1)))) (iConst 1))

examples/Examples/Param/DesugarPos.hs view

@@ -53,19 +53,17 @@ instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, Difunctor f)   => Desugar Sug f where   desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = iLam y `iApp` x-  desugHom' Fix       = iLam $ \f ->-                           (iLam $ \x -> Place f `iApp` (Place x `iApp` Place x))-                           `iApp`-                           (iLam $ \x -> Place f `iApp` (Place x `iApp` Place x))+  desugHom' (Let x y) = inject (Lam y) `iApp` x+  desugHom' Fix       = iLam $ \f -> (iLam $ \x -> f `iApp` (x `iApp` x)) `iApp`+                                     (iLam $ \x -> f `iApp` (x `iApp` x))  -- Example: desugPEx == iAApp (Pos 1 0)---          (iALam (Pos 1 0) Place)+--          (iALam (Pos 1 0) id) --          (iALam (Pos 1 1) $ \f -> --               iAApp (Pos 1 1) --                     (iALam (Pos 1 1) $ \x ->---                          iAApp (Pos 1 1) (Place f) (iAApp (Pos 1 1) (Place x) (Place x)))+--                          iAApp (Pos 1 1) f (iAApp (Pos 1 1) x x)) --                     (iALam (Pos 1 1) $ \x ->---                          iAApp (Pos 1 1) (Place f) (iAApp (Pos 1 1) (Place x) (Place x))))+--                          iAApp (Pos 1 1) f (iAApp (Pos 1 1) x  x))) desugPEx :: Term SigP-desugPEx = desugarA (iALet (Pos 1 0) (iAFix (Pos 1 1)) Place :: Term SigP')+desugPEx = desugarA (iALet (Pos 1 0) (iAFix (Pos 1 1)) id :: Term SigP')

examples/Examples/Param/Eval.hs view

@@ -45,7 +45,6 @@          [''Const, ''Lam, ''App, ''Op]) $(derive [makeDitraversable]          [''Const, ''App, ''Op])-$(derive [smartConstructors] [''Fun])  -- Term evaluation algebra class Eval f v where@@ -68,7 +67,7 @@   evalAlg (App x y) = (projF x) y  instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = iFun f+  evalAlg (Lam f) = inject $ Fun f  projC :: (Const :<: v) => Term v -> Int projC v = case project v of Just (Const n) -> n@@ -82,4 +81,4 @@  -- Example: evalEx = Just (iConst 4) evalEx :: Maybe (Term GValue)-evalEx = evalG $ (iLam $ \x -> Place x `iAdd` Place x) `iApp` iConst 2+evalEx = evalG $ (iLam $ \x -> x `iAdd` x) `iApp` iConst 2

examples/Examples/Param/EvalM.hs view

@@ -46,7 +46,6 @@          [''Const, ''Lam, ''App, ''Op]) $(derive [makeDitraversable]          [''Const, ''App, ''Op])-$(derive [smartConstructors] [''FunM])  -- Term evaluation algebra. Note that we cannot use @AlgM Maybe f (Term v)@ -- because that would force @FunM@ to have the type @e -> e@ rather than@@ -80,7 +79,7 @@                             f =<< my  instance (FunM Maybe :<: v) => EvalM Lam v where-  evalAlgM (Lam f) = return $ iFunM $ f . return+  evalAlgM (Lam f) = return $ inject $ FunM $ f . return  projC :: (Const :<: v) => Term v -> Maybe Int projC v = do Const n <- project v@@ -96,6 +95,5 @@  -- Example: evalEx = Just (iConst 12) (3 * (2 + 2) = 12) evalMEx :: Maybe (Term GValue)-evalMEx = evalMG $ (iLam $ \x -> iLam $ \y ->-                                 Place y `iMult` (Place x `iAdd` Place x))+evalMEx = evalMG $ (iLam $ \x -> iLam $ \y -> y `iMult` (x `iAdd` x))                    `iApp` iConst 2 `iApp` iConst 3

examples/Examples/Param/Parsing.hs view

@@ -50,15 +50,15 @@ $(derive [makeDifunctor, makeDitraversable, makeEqD, makeShowD, smartConstructors]          [''Const, ''Lam, ''App, ''Op, ''Abs, ''Var]) -type TransM = Reader (Map VarId Any)+type TransM f = Reader (Map VarId (Term f))  class PHOASTrans f g where-  transAlg :: Alg f (TransM (Term g))+  transAlg :: Alg f (TransM g (Term g))  $(derive [liftSum] [''PHOASTrans])  -- default translation-instance (f :<: g, Ditraversable f TransM Any) => PHOASTrans f g where+instance (f :<: g, Ditraversable f (TransM g) Any) => PHOASTrans f g where   transAlg x = liftM inject $ disequence $ dimap (return . Place) id x  instance (Lam :<: g) => PHOASTrans Abs g where@@ -66,11 +66,11 @@                           return $ iLam $ \y -> runReader b (Map.insert x y env)  instance PHOASTrans Var g where-  transAlg (Var x) = liftM (Place . fromJust) $ asks $ Map.lookup x+  transAlg (Var x) = liftM fromJust $ asks $ Map.lookup x  trans :: Term Sig -> Term Sig' trans x = runReader (cata transAlg x) Map.empty --- Example: evalEx = iLam $ \a -> iApp (iLam $ \b -> iLam $ \c -> hole b) (hole a)+-- Example: evalEx = iLam $ \a -> iApp (iLam $ \b -> iLam $ \c -> b) a transEx :: Term Sig' transEx = trans $ iAbs "y" $ (iAbs "x" $ iAbs "y" $ iVar "x") `iApp` (iVar "y")

src/Data/Comp/Algebra.hs view

@@ -32,17 +32,17 @@       -- * Term Homomorphisms       CxtFun,       SigFun,-      TermHom,-      appTermHom,-      appTermHom',-      compTermHom,+      Hom,+      appHom,+      appHom',+      compHom,       appSigFun,       appSigFun',       compSigFun,-      compSigFunTermHom,-      compTermHomSigFun,+      compSigFunHom,+      compHomSigFun,       compAlgSigFun,-      termHom,+      hom,       compAlg,       compCoalg,       compCVCoalg,@@ -50,22 +50,22 @@       -- * Monadic Term Homomorphisms       CxtFunM,       SigFunM,-      TermHomM,+      HomM,       SigFunMD,-      TermHomMD,+      HomMD,       sigFunM,-      termHom',-      appTermHomM,-      appTermHomM',-      termHomM,-      termHomMD,+      hom',+      appHomM,+      appHomM',+      homM,+      homMD,       appSigFunM,       appSigFunM',       appSigFunMD,-      compTermHomM,+      compHomM,       compSigFunM,-      compSigFunTermHomM,-      compTermHomSigFunM,+      compSigFunHomM,+      compHomSigFunM,       compAlgSigFunM,       compAlgM,       compAlgM',@@ -201,53 +201,53 @@ type SigFun f g = forall a. f a -> g a  {-| This type represents a term homomorphism. -}-type TermHom f g = SigFun f (Context g)+type Hom f g = SigFun f (Context g)  {-| This function applies the given term homomorphism to a term/context. -}-appTermHom :: forall f g . (Functor f, Functor g) => TermHom f g -> CxtFun f g-{-# NOINLINE [1] appTermHom #-}+appHom :: forall f g . (Functor f, Functor g) => Hom f g -> CxtFun f g+{-# NOINLINE [1] appHom #-} -- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type -- (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.-appTermHom f = run where+appHom f = run where     run :: CxtFun f g     run (Hole x) = Hole x     run (Term t) = appCxt (f (fmap run t))  -- | Apply a term homomorphism recursively to a term/context. This is--- a top-down variant of 'appTermHom'.-appTermHom' :: forall f g . (Functor g) => TermHom f g -> CxtFun f g-{-# NOINLINE [1] appTermHom' #-}+-- a top-down variant of 'appHom'.+appHom' :: forall f g . (Functor g) => Hom f g -> CxtFun f g+{-# NOINLINE [1] appHom' #-} -- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type -- (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.-appTermHom' f = run where+appHom' f = run where     run :: CxtFun f g     run (Hole x) = Hole x     run (Term t) = appCxt  (fmap run (f t))  {-| Compose two term homomorphisms. -}-compTermHom :: (Functor g, Functor h) => TermHom g h -> TermHom f g -> TermHom f h+compHom :: (Functor g, Functor h) => Hom g h -> Hom f g -> Hom f h -- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type -- (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.-compTermHom f g = appTermHom f . g+compHom f g = appHom f . g  {-| Compose an algebra with a term homomorphism to get a new algebra. -}-compAlg :: (Functor g) => Alg g a -> TermHom f g -> Alg f a+compAlg :: (Functor g) => Alg g a -> Hom f g -> Alg f a compAlg alg talg = cata' alg . talg  {-| Compose a term homomorphism with a coalgebra to get a cv-coalgebra. -}-compCoalg :: TermHom f g -> Coalg f a -> CVCoalg' g a+compCoalg :: Hom f g -> Coalg f a -> CVCoalg' g a compCoalg hom coa = hom . coa  {-| Compose a term homomorphism with a cv-coalgebra to get a new cv-coalgebra.  -} compCVCoalg :: (Functor f, Functor g)-  => TermHom f g -> CVCoalg' f a -> CVCoalg' g a-compCVCoalg hom coa = appTermHom hom . coa+  => Hom f g -> CVCoalg' f a -> CVCoalg' g a+compCVCoalg hom coa = appHom hom . coa   {-| This function applies a signature function to the given context. -}@@ -257,7 +257,7 @@     where run (Term t) = Term $ f $ fmap run t           run (Hole x) = Hole x -- implementation via term homomorphisms:---  appSigFun f = appTermHom_ $ termHom f+--  appSigFun f = appHom_ $ hom f  -- | This function applies a signature function to the given -- context. This is a top-down variant of 'appSigFun'.@@ -274,12 +274,12 @@  -- | This function composes a signature function with a term -- homomorphism.-compSigFunTermHom :: (Functor g) => SigFun g h -> TermHom f g -> TermHom f h-compSigFunTermHom f g = appSigFun f . g+compSigFunHom :: (Functor g) => SigFun g h -> Hom f g -> Hom f h+compSigFunHom f g = appSigFun f . g  -- | This function composes a term homomorphism with a signature function.-compTermHomSigFun :: TermHom g h -> SigFun f g -> TermHom f h-compTermHomSigFun f g = f . g+compHomSigFun :: Hom g h -> SigFun f g -> Hom f h+compHomSigFun f g = f . g  -- | This function composes an algebra with a signature function. compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a@@ -288,8 +288,8 @@  -- | Lifts the given signature function to the canonical term -- homomorphism.-termHom :: (Functor g) => SigFun f g -> TermHom f g-termHom f = simpCxt . f+hom :: (Functor g) => SigFun f g -> Hom f g+hom f = simpCxt . f  {-|   This type represents a monadic context function.@@ -305,11 +305,11 @@ type SigFunMD m f g = forall a. f (m a) -> m (g a)  {-| This type represents a monadic term homomorphism.  -}-type TermHomM m f g = SigFunM m f (Context g)+type HomM m f g = SigFunM m f (Context g)  {-| This type represents a monadic term homomorphism. It is similar to-'TermHomM' but has monadic values also in the domain. -}-type TermHomMD m f g = SigFunMD m f (Context g)+'HomM' but has monadic values also in the domain. -}+type HomMD m f g = SigFunMD m f (Context g)   {-| Lift the given signature function to a monadic signature function. Note that@@ -319,39 +319,39 @@ sigFunM f = return . f  {-| Lift the give monadic signature function to a monadic term homomorphism. -}-termHom' :: (Functor f, Functor g, Monad m) => SigFunM m f g -> TermHomM m f g-termHom' f = liftM  (Term . fmap Hole) . f+hom' :: (Functor f, Functor g, Monad m) => SigFunM m f g -> HomM m f g+hom' f = liftM  (Term . fmap Hole) . f   {-| Lift the given signature function to a monadic term homomorphism. -}-termHomM :: (Functor g, Monad m) => SigFunM m f g -> TermHomM m f g-termHomM f = liftM simpCxt . f+homM :: (Functor g, Monad m) => SigFunM m f g -> HomM m f g+homM f = liftM simpCxt . f   {-| Apply a monadic term homomorphism recursively to a term/context. -}-appTermHomM :: forall f g m . (Traversable f, Functor g, Monad m)-         => TermHomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appTermHomM #-}-appTermHomM f = run+appHomM :: forall f g m . (Traversable f, Functor g, Monad m)+         => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM #-}+appHomM f = run     where run :: Cxt h f a -> m (Cxt h g a)           run (Hole x) = return (Hole x)           run (Term t) = liftM appCxt . f =<< mapM run t  -- | Apply a monadic term homomorphism recursively to a--- term/context. This a top-down variant of 'appTermHomM'.-appTermHomM' :: forall f g m . (Traversable g, Monad m)-         => TermHomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appTermHomM' #-}-appTermHomM' f = run+-- term/context. This a top-down variant of 'appHomM'.+appHomM' :: forall f g m . (Traversable g, Monad m)+         => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM' #-}+appHomM' f = run     where run :: Cxt h f a -> m (Cxt h g a)           run (Hole x) = return (Hole x)           run (Term t) = liftM appCxt . mapM run =<< f t  {-| This function constructs the unique monadic homomorphism from the initial term algebra to the given term algebra. -}-termHomMD :: forall f g m . (Traversable f, Functor g, Monad m)-          => TermHomMD m f g -> CxtFunM m f g-termHomMD f = run +homMD :: forall f g m . (Traversable f, Functor g, Monad m)+          => HomMD m f g -> CxtFunM m f g+homMD f = run      where run :: Cxt h f a -> m (Cxt h g a)           run (Hole x) = return (Hole x)           run (Term t) = liftM appCxt (f (fmap run t))@@ -364,7 +364,7 @@     where run (Term t) = liftM Term . f =<< mapM run t           run (Hole x) = return (Hole x) -- implementation via term homomorphisms--- appSigFunM f = appTermHomM $ termHom' f+-- appSigFunM f = appHomM $ hom' f   @@ -385,29 +385,29 @@           run (Term t) = liftM Term (f (fmap run t))  {-| Compose two monadic term homomorphisms. -}-compTermHomM :: (Traversable g, Functor h, Monad m)-             => TermHomM m g h -> TermHomM m f g -> TermHomM m f h-compTermHomM f g = appTermHomM f <=< g+compHomM :: (Traversable g, Functor h, Monad m)+             => HomM m g h -> HomM m f g -> HomM m f h+compHomM f g = appHomM f <=< g  {-| Compose two monadic term homomorphisms. -}-compTermHomM' :: (Traversable h, Monad m)-                => TermHomM m g h -> TermHomM m f g -> TermHomM m f h-compTermHomM' f g = appTermHomM' f <=< g+compHomM' :: (Traversable h, Monad m)+                => HomM m g h -> HomM m f g -> HomM m f h+compHomM' f g = appHomM' f <=< g  {-| Compose two monadic term homomorphisms. -}-compTermHomM_ :: (Functor h, Functor g, Monad m)-                => TermHom g h -> TermHomM m f g -> TermHomM m f h-compTermHomM_ f g = liftM (appTermHom f) . g+compHomM_ :: (Functor h, Functor g, Monad m)+                => Hom g h -> HomM m f g -> HomM m f h+compHomM_ f g = liftM (appHom f) . g  {-| Compose a monadic algebra with a monadic term homomorphism to get a new   monadic algebra. -}-compAlgM :: (Traversable g, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a+compAlgM :: (Traversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a compAlgM alg talg = cataM' alg <=< talg   {-| Compose a monadic algebra with a term homomorphism to get a new monadic   algebra. -}-compAlgM' :: (Traversable g, Monad m) => AlgM m g a -> TermHom f g -> AlgM m f a+compAlgM' :: (Traversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a compAlgM' alg talg = cataM' alg . talg  @@ -415,19 +415,19 @@ compSigFunM :: (Monad m) => SigFunM m g h -> SigFunM m f g -> SigFunM m f h compSigFunM f g = f <=< g -compSigFunTermHomM :: (Traversable g, Functor h, Monad m)-                   => SigFunM m g h -> TermHomM m f g -> TermHomM m f h-compSigFunTermHomM f g = appSigFunM f <=< g+compSigFunHomM :: (Traversable g, Functor h, Monad m)+                   => SigFunM m g h -> HomM m f g -> HomM m f h+compSigFunHomM f g = appSigFunM f <=< g   {-| Compose two monadic term homomorphisms. -}-compSigFunTermHomM' :: (Traversable h, Monad m)-                    => SigFunM m g h -> TermHomM m f g -> TermHomM m f h-compSigFunTermHomM' f g = appSigFunM' f <=< g+compSigFunHomM' :: (Traversable h, Monad m)+                    => SigFunM m g h -> HomM m f g -> HomM m f h+compSigFunHomM' f g = appSigFunM' f <=< g  {-| This function composes two monadic signature functions.  -}-compTermHomSigFunM :: (Monad m) => TermHomM m g h -> SigFunM m f g -> TermHomM m f h-compTermHomSigFunM f g = f <=< g+compHomSigFunM :: (Monad m) => HomM m g h -> SigFunM m f g -> HomM m f h+compHomSigFunM f g = f <=< g   {-| This function composes two monadic signature functions.  -}@@ -606,8 +606,8 @@ -------------------------------------------  -appAlgTermHom :: forall f g d . (Functor g) => Alg g d -> TermHom f g -> Term f -> d-appAlgTermHom alg hom = run where+appAlgHom :: forall f g d . (Functor g) => Alg g d -> Hom f g -> Term f -> d+appAlgHom alg hom = run where     run :: Term f -> d     run (Term t) = run' $ hom t     run' :: Context g (Term f) -> d@@ -616,10 +616,10 @@   -- | This function applies a signature function after a term homomorphism.-appSigFunTermHom :: forall f g h. (Functor g)-                 => SigFun g h -> TermHom f g -> CxtFun f h-{-# NOINLINE [1] appSigFunTermHom #-}-appSigFunTermHom f g = run where+appSigFunHom :: forall f g h. (Functor g)+                 => SigFun g h -> Hom f g -> CxtFun f h+{-# NOINLINE [1] appSigFunHom #-}+appSigFunHom f g = run where     run :: CxtFun f h     run (Term t) = run' $ g $ t     run (Hole h) = Hole h@@ -630,9 +630,9 @@ -- | This function applies the given algebra bottom-up while applying -- the given term homomorphism top-down. Thereby we have no -- requirements on the source signature @f@.-appAlgTermHomM :: forall m f g a. (Traversable g, Monad m)-               => AlgM m g a -> TermHomM m f g -> Term f -> m a-appAlgTermHomM alg hom = run+appAlgHomM :: forall m f g a. (Traversable g, Monad m)+               => AlgM m g a -> HomM m f g -> Term f -> m a+appAlgHomM alg hom = run     where run :: Term f -> m a           run (Term t) = hom t >>= mapM run >>= run'           run' :: (Context g a) -> m a@@ -640,9 +640,9 @@           run' (Hole x) = return x  -appTermHomTermHomM :: forall m f g h . (Monad m, Traversable g, Functor h)-                   => TermHomM m g h -> TermHomM m f g -> CxtFunM m f h-appTermHomTermHomM f g = run where+appHomHomM :: forall m f g h . (Monad m, Traversable g, Functor h)+                   => HomM m g h -> HomM m f g -> CxtFunM m f h+appHomHomM f g = run where     run :: CxtFunM m f h     run (Term t) = run' =<< g t     run (Hole h) = return $ Hole h@@ -651,9 +651,9 @@     run' (Hole h) = run h  -appSigFunTermHomM :: forall m f g h . (Traversable g, Monad m)-                   => SigFunM m g h -> TermHomM m f g -> CxtFunM m f h-appSigFunTermHomM f g = run where+appSigFunHomM :: forall m f g h . (Traversable g, Monad m)+                   => SigFunM m g h -> HomM m f g -> CxtFunM m f h+appSigFunHomM f g = run where     run :: CxtFunM m f h     run (Term t) = run' =<< g t     run (Hole h) = return $ Hole h@@ -668,50 +668,50 @@  #ifndef NO_RULES {-# RULES-  "cata/appTermHom" forall (a :: Alg g d) (h :: TermHom f g) x.-    cata a (appTermHom h x) = cata (compAlg a h) x;+  "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.+    cata a (appHom h x) = cata (compAlg a h) x; -  "cata/appTermHom'" forall (a :: Alg g d) (h :: TermHom f g) x.-    cata a (appTermHom' h x) = appAlgTermHom a h x;+  "cata/appHom'" forall (a :: Alg g d) (h :: Hom f g) x.+    cata a (appHom' h x) = appAlgHom a h x;    "cata/appSigFun" forall (a :: Alg g d) (h :: SigFun f g) x.     cata a (appSigFun h x) = cata (compAlgSigFun a h) x;    "cata/appSigFun'" forall (a :: Alg g d) (h :: SigFun f g) x.-    cata a (appSigFun' h x) = appAlgTermHom a (termHom h) x;+    cata a (appSigFun' h x) = appAlgHom a (hom h) x; -  "cata/appSigFunTermHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    cata f (appSigFunTermHom g h x) = appAlgTermHom (compAlgSigFun f g) h x;+  "cata/appSigFunHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    cata f (appSigFunHom g h x) = appAlgHom (compAlgSigFun f g) h x; -  "appAlgTermHom/appTermHom" forall (a :: Alg h d) (f :: TermHom f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appTermHom f x) = cata (compAlg a (compTermHom h f)) x;+  "appAlgHom/appHom" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.+    appAlgHom a h (appHom f x) = cata (compAlg a (compHom h f)) x; -  "appAlgTermHom/appTermHom'" forall (a :: Alg h d) (f :: TermHom f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appTermHom' f x) = appAlgTermHom a (compTermHom h f) x;+  "appAlgHom/appHom'" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.+    appAlgHom a h (appHom' f x) = appAlgHom a (compHom h f) x; -  "appAlgTermHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appSigFun f x) = cata (compAlg a (compTermHomSigFun h f)) x;+  "appAlgHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.+    appAlgHom a h (appSigFun f x) = cata (compAlg a (compHomSigFun h f)) x; -  "appAlgTermHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appSigFun' f x) = appAlgTermHom a (compTermHomSigFun h f) x;+  "appAlgHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.+    appAlgHom a h (appSigFun' f x) = appAlgHom a (compHomSigFun h f) x; -  "appAlgTermHom/appSigFunTermHom" forall (a :: Alg i d) (f :: TermHom f g) (g :: SigFun g h)-                                          (h :: TermHom h i) x.-    appAlgTermHom a h (appSigFunTermHom g f x)-      = appAlgTermHom a (compTermHom (compTermHomSigFun h g) f) x;+  "appAlgHom/appSigFunHom" forall (a :: Alg i d) (f :: Hom f g) (g :: SigFun g h)+                                          (h :: Hom h i) x.+    appAlgHom a h (appSigFunHom g f x)+      = appAlgHom a (compHom (compHomSigFun h g) f) x; -  "appTermHom/appTermHom" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom a (appTermHom h x) = appTermHom (compTermHom a h) x;+  "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom a (appHom h x) = appHom (compHom a h) x; -  "appTermHom'/appTermHom'" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom' a (appTermHom' h x) = appTermHom' (compTermHom a h) x;+  "appHom'/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom' a (appHom' h x) = appHom' (compHom a h) x; -  "appTermHom'/appTermHom" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom' a (appTermHom h x) = appTermHom (compTermHom a h) x;+  "appHom'/appHom" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom' a (appHom h x) = appHom (compHom a h) x; -  "appTermHom/appTermHom'" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom a (appTermHom' h x) = appTermHom' (compTermHom a h) x;+  "appHom/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom a (appHom' h x) = appHom' (compHom a h) x;        "appSigFun/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.     appSigFun f (appSigFun g x) = appSigFun (compSigFun f g) x;@@ -720,207 +720,207 @@     appSigFun' f (appSigFun' g x) = appSigFun' (compSigFun f g) x;    "appSigFun/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.-    appSigFun f (appSigFun' g x) = appSigFunTermHom f (termHom g) x;+    appSigFun f (appSigFun' g x) = appSigFunHom f (hom g) x;    "appSigFun'/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.     appSigFun' f (appSigFun g x) = appSigFun (compSigFun f g) x; -  "appTermHom/appSigFun" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom f (appSigFun g x) = appTermHom (compTermHomSigFun f g) x;+  "appHom/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom f (appSigFun g x) = appHom (compHomSigFun f g) x; -  "appTermHom/appSigFun'" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom f (appSigFun' g x) =  appTermHom' (compTermHomSigFun f g) x;+  "appHom/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom f (appSigFun' g x) =  appHom' (compHomSigFun f g) x; -  "appTermHom'/appSigFun'" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom' f (appSigFun' g x) =  appTermHom' (compTermHomSigFun f g) x;+  "appHom'/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom' f (appSigFun' g x) =  appHom' (compHomSigFun f g) x; -  "appTermHom'/appSigFun" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom' f (appSigFun g x) = appTermHom (compTermHomSigFun f g) x;+  "appHom'/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom' f (appSigFun g x) = appHom (compHomSigFun f g) x;     -  "appSigFun/appTermHom" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun f (appTermHom g x) = appSigFunTermHom f g x;+  "appSigFun/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun f (appHom g x) = appSigFunHom f g x; -  "appSigFun'/appTermHom'" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun' f (appTermHom' g x) = appTermHom' (compSigFunTermHom f g) x;+  "appSigFun'/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun' f (appHom' g x) = appHom' (compSigFunHom f g) x; -  "appSigFun/appTermHom'" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun f (appTermHom' g x) = appSigFunTermHom f g x;+  "appSigFun/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun f (appHom' g x) = appSigFunHom f g x; -  "appSigFun'/appTermHom" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun' f (appTermHom g x) = appTermHom (compSigFunTermHom f g) x;+  "appSigFun'/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun' f (appHom g x) = appHom (compSigFunHom f g) x;     -  "appSigFunTermHom/appSigFun" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)+  "appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)                                       (h :: SigFun f1 f2) x.-    appSigFunTermHom f g (appSigFun h x)-    = appSigFunTermHom f (compTermHomSigFun g h) x;+    appSigFunHom f g (appSigFun h x)+    = appSigFunHom f (compHomSigFun g h) x; -  "appSigFunTermHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)+  "appSigFunHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)                                       (h :: SigFun f1 f2) x.-    appSigFunTermHom f g (appSigFun' h x)-    = appSigFunTermHom f (compTermHomSigFun g h) x;+    appSigFunHom f g (appSigFun' h x)+    = appSigFunHom f (compHomSigFun g h) x; -  "appSigFunTermHom/appTermHom" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFunTermHom f g (appTermHom h x)-    = appSigFunTermHom f (compTermHom g h) x;+  "appSigFunHom/appHom" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFunHom f g (appHom h x)+    = appSigFunHom f (compHom g h) x; -  "appSigFunTermHom/appTermHom'" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFunTermHom f g (appTermHom' h x)-    = appSigFunTermHom f (compTermHom g h) x;+  "appSigFunHom/appHom'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFunHom f g (appHom' h x)+    = appSigFunHom f (compHom g h) x; -  "appSigFun/appSigFunTermHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFun f (appSigFunTermHom g h x) = appSigFunTermHom (compSigFun f g) h x;+  "appSigFun/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFun f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x; -  "appSigFun'/appSigFunTermHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFun' f (appSigFunTermHom g h x) = appSigFunTermHom (compSigFun f g) h x;+  "appSigFun'/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFun' f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x; -  "appTermHom/appSigFunTermHom" forall (f :: TermHom f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appTermHom f (appSigFunTermHom g h x) = appTermHom' (compTermHom (compTermHomSigFun f g) h) x;+  "appHom/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appHom f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x; -  "appTermHom'/appSigFunTermHom" forall (f :: TermHom f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appTermHom' f (appSigFunTermHom g h x) = appTermHom' (compTermHom (compTermHomSigFun f g) h) x;+  "appHom'/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appHom' f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x; -  "appSigFunTermHom/appSigFunTermHom" forall (f1 :: SigFun f4 f5) (f2 :: TermHom f3 f4)-                                             (f3 :: SigFun f2 f3) (f4 :: TermHom f1 f2) x.-    appSigFunTermHom f1 f2 (appSigFunTermHom f3 f4 x)-      = appSigFunTermHom f1 (compTermHom (compTermHomSigFun f2 f3) f4) x;+  "appSigFunHom/appSigFunHom" forall (f1 :: SigFun f4 f5) (f2 :: Hom f3 f4)+                                             (f3 :: SigFun f2 f3) (f4 :: Hom f1 f2) x.+    appSigFunHom f1 f2 (appSigFunHom f3 f4 x)+      = appSigFunHom f1 (compHom (compHomSigFun f2 f3) f4) x;  #-}  {-# RULES -  "cataM/appTermHomM" forall (a :: AlgM Maybe g d) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= cataM a =  appAlgTermHomM a h x;+  "cataM/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.+     appHomM h x >>= cataM a =  appAlgHomM a h x; -  "cataM/appTermHomM'" forall (a :: AlgM Maybe g d) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= cataM a = appAlgTermHomM a h x;+  "cataM/appHomM'" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.+     appHomM' h x >>= cataM a = appAlgHomM a h x;    "cataM/appSigFunM" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.-     appSigFunM h x >>= cataM a =  appAlgTermHomM a (termHomM h) x;+     appSigFunM h x >>= cataM a =  appAlgHomM a (homM h) x;    "cataM/appSigFunM'" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= cataM a = appAlgTermHomM a (termHomM h) x;+     appSigFunM' h x >>= cataM a = appAlgHomM a (homM h) x; -  "cataM/appTermHom" forall (a :: AlgM m g d) (h :: TermHom f g) x.-     cataM a (appTermHom h x) = appAlgTermHomM a (sigFunM h) x;+  "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.+     cataM a (appHom h x) = appAlgHomM a (sigFunM h) x; -  "cataM/appTermHom'" forall (a :: AlgM m g d) (h :: TermHom f g) x.-     cataM a (appTermHom' h x) = appAlgTermHomM a (sigFunM h) x;+  "cataM/appHom'" forall (a :: AlgM m g d) (h :: Hom f g) x.+     cataM a (appHom' h x) = appAlgHomM a (sigFunM h) x;    "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.-     cataM a (appSigFun h x) = appAlgTermHomM a (sigFunM $ termHom h) x;+     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;    "cataM/appSigFun'" forall (a :: AlgM m g d) (h :: SigFun f g) x.-     cataM a (appSigFun' h x) = appAlgTermHomM a (sigFunM $ termHom h) x;+     cataM a (appSigFun' h x) = appAlgHomM a (sigFunM $ hom h) x;    "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.-     cataM a (appSigFun h x) = appAlgTermHomM a (sigFunM $ termHom h) x;+     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x; -  "cataM/appSigFunTermHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: TermHom f g) x.-     cataM a (appSigFunTermHom g f x) = appAlgTermHomM a (sigFunM $ compSigFunTermHom g f) x;+  "cataM/appSigFunHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: Hom f g) x.+     cataM a (appSigFunHom g f x) = appAlgHomM a (sigFunM $ compSigFunHom g f) x; -  "appTermHomM/appTermHomM" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appTermHomM a = appTermHomM (compTermHomM a h) x;+  "appHomM/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appHomM a = appHomM (compHomM a h) x; -  "appTermHomM/appSigFunM" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM h x >>= appTermHomM a = appTermHomM (compTermHomSigFunM a h) x;+  "appHomM/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM h x >>= appHomM a = appHomM (compHomSigFunM a h) x; -  "appTermHomM/appTermHomM'" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appTermHomM a = appTermHomTermHomM a h x;+  "appHomM/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appHomM a = appHomHomM a h x; -  "appTermHomM/appSigFunM'" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= appTermHomM a = appTermHomTermHomM a (termHomM h) x;+  "appHomM/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM' h x >>= appHomM a = appHomHomM a (homM h) x; -  "appTermHomM'/appTermHomM" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appTermHomM' a = appTermHomM' (compTermHomM' a h) x;+  "appHomM'/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appHomM' a = appHomM' (compHomM' a h) x; -  "appTermHomM'/appSigFunM" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM h x >>= appTermHomM' a = appTermHomM' (compTermHomSigFunM a h) x;+  "appHomM'/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x; -  "appTermHomM'/appTermHomM'" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appTermHomM' a = appTermHomM' (compTermHomM' a h) x;+  "appHomM'/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appHomM' a = appHomM' (compHomM' a h) x; -  "appTermHomM'/appSigFunM'" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= appTermHomM' a = appTermHomM' (compTermHomSigFunM a h) x;+  "appHomM'/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM' h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x; -  "appTermHomM/appTermHom" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM a (appTermHom h x) = appTermHomTermHomM a (sigFunM h) x;+  "appHomM/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM a (appHom h x) = appHomHomM a (sigFunM h) x; -  "appTermHomM/appSigFun" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM a (appSigFun h x) = appTermHomTermHomM a (sigFunM $ termHom h) x;+  "appHomM/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM a (appSigFun h x) = appHomHomM a (sigFunM $ hom h) x; -  "appTermHomM'/appTermHom" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM' a (appTermHom h x) = appTermHomM' (compTermHomM' a (sigFunM h)) x;+  "appHomM'/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM' a (appHom h x) = appHomM' (compHomM' a (sigFunM h)) x; -  "appTermHomM'/appSigFun" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM' a (appSigFun h x) = appTermHomM' (compTermHomSigFunM a (sigFunM h)) x;+  "appHomM'/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM' a (appSigFun h x) = appHomM' (compHomSigFunM a (sigFunM h)) x; -  "appTermHomM/appTermHom'" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM a (appTermHom' h x) = appTermHomTermHomM a (sigFunM h) x;+  "appHomM/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM a (appHom' h x) = appHomHomM a (sigFunM h) x; -  "appTermHomM/appSigFun'" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM a (appSigFun' h x) = appTermHomTermHomM a (sigFunM $ termHom h) x;+  "appHomM/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM a (appSigFun' h x) = appHomHomM a (sigFunM $ hom h) x; -  "appTermHomM'/appTermHom'" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM' a (appTermHom' h x) = appTermHomM' (compTermHomM' a (sigFunM h)) x;+  "appHomM'/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM' a (appHom' h x) = appHomM' (compHomM' a (sigFunM h)) x; -  "appTermHomM'/appSigFun'" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM' a (appSigFun' h x) = appTermHomM' (compTermHomSigFunM a (sigFunM h)) x;+  "appHomM'/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM' a (appSigFun' h x) = appHomM' (compHomSigFunM a (sigFunM h)) x; -  "appSigFunM/appTermHomM" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appSigFunM a = appSigFunTermHomM a h x;+  "appSigFunM/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appSigFunM a = appSigFunHomM a h x;    "appSigFunHomM/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.      appSigFunM h x >>= appSigFunM a = appSigFunM (compSigFunM a h) x; -  "appSigFunM/appTermHomM'" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appSigFunM a = appSigFunTermHomM a h x;+  "appSigFunM/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appSigFunM a = appSigFunHomM a h x;    "appSigFunM/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= appSigFunM a = appSigFunTermHomM a (termHomM h) x;+     appSigFunM' h x >>= appSigFunM a = appSigFunHomM a (homM h) x; -  "appSigFunM'/appTermHomM" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appSigFunM' a = appTermHomM' (compSigFunTermHomM' a h) x;+  "appSigFunM'/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;    "appSigFunM'/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.      appSigFunM h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x; -  "appSigFunM'/appTermHomM'" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appSigFunM' a = appTermHomM' (compSigFunTermHomM' a h) x;+  "appSigFunM'/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;    "appSigFunM'/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.      appSigFunM' h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x; -  "appSigFunM/appTermHom" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM a (appTermHom h x) = appSigFunTermHomM a (sigFunM h) x;+  "appSigFunM/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM a (appHom h x) = appSigFunHomM a (sigFunM h) x;    "appSigFunM/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.-     appSigFunM a (appSigFun h x) = appSigFunTermHomM a (sigFunM $ termHom h) x;+     appSigFunM a (appSigFun h x) = appSigFunHomM a (sigFunM $ hom h) x; -  "appSigFunM'/appTermHom" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM' a (appTermHom h x) = appTermHomM' (compSigFunTermHomM' a (sigFunM h)) x;+  "appSigFunM'/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM' a (appHom h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;    "appSigFunM'/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.      appSigFunM' a (appSigFun h x) = appSigFunM' (compSigFunM a (sigFunM h)) x; -  "appSigFunM/appTermHom'" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM a (appTermHom' h x) = appSigFunTermHomM a (sigFunM h) x;+  "appSigFunM/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM a (appHom' h x) = appSigFunHomM a (sigFunM h) x;    "appSigFunM/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.-     appSigFunM a (appSigFun' h x) = appSigFunTermHomM a (sigFunM $ termHom h) x;+     appSigFunM a (appSigFun' h x) = appSigFunHomM a (sigFunM $ hom h) x; -  "appSigFunM'/appTermHom'" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM' a (appTermHom' h x) = appTermHomM' (compSigFunTermHomM' a (sigFunM h)) x;+  "appSigFunM'/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM' a (appHom' h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;    "appSigFunM'/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.      appSigFunM' a (appSigFun' h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;  -  "appTermHom/appTermHomM" forall (a :: TermHom g h) (h :: TermHomM m f g) x.-     appTermHomM h x >>= (return . appTermHom a) = appTermHomM (compTermHomM_ a h) x;+  "appHom/appHomM" forall (a :: Hom g h) (h :: HomM m f g) x.+     appHomM h x >>= (return . appHom a) = appHomM (compHomM_ a h) x;  #-}  {-# RULES

src/Data/Comp/Annotation.hs view

@@ -55,14 +55,14 @@ {-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism  over the same signatures, but extended with annotations. -} propAnn :: (DistAnn f p f', DistAnn g p g', Functor g) -        => TermHom f g -> TermHom f' g'+        => Hom f g -> Hom f' g' propAnn hom f' = ann p (hom f)     where (f,p) = projectA f'  {-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic   term homomorphism over the same signatures, but extended with annotations. -} propAnnM :: (DistAnn f p f', DistAnn g p g', Functor g, Monad m) -         => TermHomM m f g -> TermHomM m f' g'+         => HomM m f g -> HomM m f' g' propAnnM hom f' = liftM (ann p) (hom f)     where (f,p) = projectA f'

+ src/Data/Comp/Automata.hs view

@@ -0,0 +1,266 @@+{-# LANGUAGE RankNTypes, FlexibleContexts, ImplicitParams, GADTs, ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Automata+-- Copyright   :  (c) 2010-2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines stateful term homomorphisms. This (slightly+-- oxymoronic) notion extends per se stateless term homomorphisms with+-- a state that is maintained separately by a bottom-up or top-down+-- tree automaton.+--+--------------------------------------------------------------------------------++module Data.Comp.Automata+    ( module Data.Comp.Automata,+      module Data.Comp.Automata.Product+    ) where++import Data.Comp.Zippable+import Data.Comp.Automata.Product+import Data.Comp.Term+import Data.Comp.Algebra+import Data.Comp.Show ()+import Data.Map (Map)+import qualified Data.Map as Map++infix 1 |->+infixr 0 &++(&) :: Ord k => Map k v -> Map k v -> Map k v+(&) = Map.union++(|->) :: k -> a -> Map k a+(|->) = Map.singleton++o :: Map k a+o = Map.empty++-- | This function provides access to components of the states from+-- "below".+below :: (?below :: a -> q, p :< q) => a -> p+below = pr . ?below++-- | This function provides access to components of the state from+-- "above"+above :: (?above :: q, p :< q) => p+above = pr ?above++-- | Turns the explicit parameters @?above@ and @?below@ into explicit+-- ones.+explicit :: q -> (a -> q) -> ((?above :: q, ?below :: a -> q) => b) -> b+explicit ab be x = x where ?above = ab; ?below = be+++-- | This type represents stateful term homomorphisms. Stateful term+-- homomorphisms have access to a state that is provided (separately)+-- by a DUTA or a DDTA (or both).+type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a+++-- | This type represents transition functions of deterministic+-- bottom-up tree transducers (DUTTs).++type UpTrans f q g = forall a. f (q,a) -> (q, Context g a)++-- | This function transforms DUTT transition function into an+-- algebra.++upAlg :: (Functor g)  => UpTrans f q g -> Alg f (q, Term g)+upAlg trans = fmap appCxt . trans ++-- | This function runs the given DUTT on the given term.++runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> (q, Term g)+runUpTrans = cata . upAlg++-- | This function generalises 'runUpTrans' to contexts. Therefore,+-- additionally, a transition function for the holes is needed.+runUpTrans' :: (Functor f, Functor g) => UpTrans f q g -> Context f (q,a) -> (q, Context g a)+runUpTrans' trans = run where+    run (Hole (q,a)) = (q, Hole a)+    run (Term t) = fmap appCxt $ trans $ fmap run t++-- | This function composes two DUTTs. (see TATA, Theorem 6.4.5)+compUpTrans :: (Functor f, Functor g, Functor h)+               => UpTrans g p h -> UpTrans f q g -> UpTrans f (q,p) h+compUpTrans t2 t1 x = ((q1,q2), c2) where+    (q1, c1) = t1 $ fmap (\((q1,q2),a) -> (q1,(q2,a))) x+    (q2, c2) = runUpTrans' t2 c1++-- | This type represents transition functions of deterministic+-- bottom-up tree acceptors (DUTAs).+type UpState f q = Alg f q++-- | Changes the state space of the DUTA using the given isomorphism.+tagUpState :: (Functor f) => (q -> p) -> (p -> q) -> UpState f q -> UpState f p+tagUpState i o s = i . s . fmap o++-- | This combinator runs the given DUTA on a term returning the final+-- state of the run.+runUpState :: (Functor f) => UpState f q -> Term f -> q+runUpState = cata++-- | This function combines the product DUTA of the two given DUTAs.+prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p,q)+prodUpState sp sq t = (p,q) where+    p = sp $ fmap fst t+    q = sq $ fmap snd t+++-- | This function constructs a DUTT from a given stateful term+-- homomorphism with the state propagated by the given DUTA.+upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g+upTrans st f t = (q, c)+    where q = st $ fmap fst t+          c = fmap snd $ explicit q fst f t++-- | This function applies a given stateful term homomorphism with+-- a state space propagated by the given DUTA to a term.+runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q,Term g)+runUpHom alg h = runUpTrans (upTrans alg h)+++-- | This type represents transition functions of generalised+-- deterministic bottom-up tree acceptors (GDUTAs) which have access+-- to an extended state space.+type DUpState f p q = forall a . (?below :: a -> p, ?above :: p, q :< p) => f a -> q++-- | This combinator turns an arbitrary DUTA into a GDUTA.+dUpState :: Functor f => UpState f q -> DUpState f p q+dUpState f = f . fmap below++-- | This combinator turns a GDUTA with the smallest possible state+-- space into a DUTA.+upState :: DUpState f q q -> UpState f q+upState f s = res where res = explicit res id f s++-- | This combinator runs a GDUTA on a term.+runDUpState :: Functor f => DUpState f q q -> Term f -> q+runDUpState = runUpState . upState++-- | This combinator constructs the product of two GDUTA.+prodDUpState :: (p :< c, q :< c)+             => DUpState f c p -> DUpState f c q -> DUpState f c (p,q)+prodDUpState sp sq t = (sp t, sq t)++(<*>) :: (p :< c, q :< c)+             => DUpState f c p -> DUpState f c q -> DUpState f c (p,q)+(<*>) = prodDUpState++++-- | This type represents transition functions of deterministic+-- top-down tree transducers (DDTTs).++type DownTrans f q g = forall a. (q, f a) -> Context g (q,a)++-- | Thsis function runs the given DDTT on the given tree.+runDownTrans :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g a+runDownTrans tr q t = run (q,t) where+    run (q,Term t) = appCxt $ fmap run $  tr (q, t)+    run (_,Hole a)      = Hole a++-- | This function runs the given DDTT on the given tree.+runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g (q,a)+runDownTrans' tr q t = run (q,t) where+    run (q,Term t) = appCxt $ fmap run $  tr (q, t)+    run (q,Hole a)      = Hole (q,a)++-- | This function composes two DDTTs. (see Z. Fülöp, H. Vogler+-- "Syntax-Directed Semantics", Theorem 3.39)+compDownTrans :: (Functor f, Functor g, Functor h)+              => DownTrans g p h -> DownTrans f q g -> DownTrans f (q,p) h+compDownTrans t2 t1 ((q,p), t) = fmap (\(p, (q, a)) -> ((q,p),a)) $ runDownTrans' t2 p (t1 (q, t))+++-- | This type represents transition functions of deterministic+-- top-down tree acceptors (DDTAs).+type DownState f q = forall a. Ord a => (q, f a) -> Map a q+++-- | Changes the state space of the DDTA using the given isomorphism.+tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p+tagDownState i o t (q,s) = fmap i $ t (o q,s)++-- | This function constructs the product DDTA of the given two DDTAs.+prodDownState :: DownState f p -> DownState f q -> DownState f (p,q)+prodDownState sp sq ((p,q),t) = prodMap p q (sp (p, t)) (sq (q, t))+++-- | This type is needed to construct the product of two DDTAs.+data ProdState p q = LState p+                   | RState q+                   | BState p q+-- | This function constructs the pointwise product of two maps each+-- with a default value.+prodMap :: (Ord i) => p -> q -> Map i p -> Map i q -> Map i (p,q)+prodMap p q mp mq = Map.map final $ Map.unionWith combine ps qs+    where ps = Map.map LState mp+          qs = Map.map RState mq+          combine (LState p) (RState q) = BState p q+          combine (RState q) (LState p) = BState p q+          combine _ _                   = error "unexpected merging"+          final (LState p) = (p, q)+          final (RState q) = (p, q)+          final (BState p q) = (p,q)++-- | Apply the given state mapping to the given functorial value by+-- adding the state to the corresponding index if it is in the map and+-- otherwise adding the provided default state.+appMap :: Zippable f => (forall i . Ord i => f i -> Map i q)+                       -> q -> f b -> f (q,b)+appMap qmap q s = fmap qfun s'+    where s' = number s+          qfun k@(Numbered (_,a)) = (Map.findWithDefault q k (qmap s') ,a)++-- | This function constructs a DDTT from a given stateful term-- homomorphism with the state propagated by the given DDTA.+downTrans :: Zippable f => DownState f q -> QHom f q g -> DownTrans f q g+downTrans st f (q, s) = explicit q fst f (appMap (curry st q) q s)+++-- | This function applies a given stateful term homomorphism with a+-- state space propagated by the given DDTA to a term.+runDownHom :: (Zippable f, Functor g)+            => DownState f q -> QHom f q g -> q -> Term f -> Term g+runDownHom st h = runDownTrans (downTrans st h)++-- | This type represents transition functions of generalised+-- deterministic top-down tree acceptors (GDDTAs) which have access+-- to an extended state space.+type DDownState f p q = forall i . (Ord i, ?below :: i -> p, ?above :: p, q :< p)+                                => f i -> Map i q++-- | This combinator turns an arbitrary DDTA into a GDDTA.+dDownState :: DownState f q -> DDownState f p q+dDownState f t = f (above,t)++-- | This combinator turns a GDDTA with the smallest possible state+-- space into a DDTA.+downState :: DDownState f q q -> DownState f q+downState f (q,s) = res+    where res = explicit q bel f s+          bel k = Map.findWithDefault q k res+++-- | This combinator constructs the product of two GDDTA.+prodDDownState :: (p :< c, q :< c)+               => DDownState f c p -> DDownState f c q -> DDownState f c (p,q)+prodDDownState sp sq t = prodMap above above (sp t) (sq t)++(>*<) :: (p :< c, q :< c, Functor f)+         => DDownState f c p -> DDownState f c q -> DDownState f c (p,q)+(>*<) = prodDDownState++runDState :: Zippable f => DUpState f (u,d) u -> DDownState f (u,d) d -> d -> Term f -> u+runDState up down d (Term t) = u where+        t' = fmap bel $ number t+        bel (Numbered (i,s)) = +            let d' = Map.findWithDefault d (Numbered (i,undefined)) m+            in Numbered (i, (runDState up down d' s, d'))+        m = explicit (u,d) unNumbered down t'+        u = explicit (u,d) unNumbered up t'

+ src/Data/Comp/Automata/Product.hs view

@@ -0,0 +1,27 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, IncoherentInstances, TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Automata.Product+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+--+--------------------------------------------------------------------------------++module Data.Comp.Automata.Product ((:<)(..)) where++import Data.Comp.Automata.Product.Derive+++instance a :< a where+    pr = id+    up = const++$(genAllInsts 7)++instance (c :< b) => c :< (a,b) where+    pr = pr . snd+    up z (x,y) = (x,up z y)

+ src/Data/Comp/Automata/Product/Derive.hs view

@@ -0,0 +1,81 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, IncoherentInstances, TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Automata.Product.Derive+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+--+--------------------------------------------------------------------------------++module Data.Comp.Automata.Product.Derive where++import Language.Haskell.TH++-- | An instance @a :< b@ means that @a@ is a component of @b@. @a@+-- can be extracted from @b@ via the method 'ex'.+class a :< b where+    pr :: b -> a+    up :: a -> b -> b++data Dir = L | R+         deriving Show++genAllInsts :: Int -> Q [Dec]+genAllInsts n = mapM genInst dirs+    where dirs = map (L:) (genDirs n)++genDirs :: Int -> [[Dir]]+genDirs 0 = [[]]+genDirs n = [] : map (L:) dirs ++ map (R:) dirs+    where dirs = genDirs (n-1)++genInst :: [Dir] -> Q Dec+genInst dir = do +  n <- newName "a"+  ty <- genType n dir+  ex <- genEx dir+  up <- genUp dir+  return $ InstanceD [] (ConT (mkName ":<") `AppT` (VarT n) `AppT` ty) [ex,up]++genType :: Name -> [Dir] -> Q Type+genType n = gen+    where gen [] = varT n+          gen (L:dir) =  gen dir `pairT` (varT =<< newName "a")+          gen (R:dir) =  (varT =<< newName "a") `pairT` gen dir ++genPat :: Name -> [Dir] -> PatQ+genPat n = gen where+    gen [] = varP n+    gen (L:dir) = tupP [gen dir,wildP]+    gen (R:dir) = tupP [wildP,gen dir]++genEx :: [Dir] -> DecQ+genEx dir = do+  n <- newName "x"+  p <- genPat n dir+  return $ FunD (mkName "pr") [Clause [p] (NormalB (VarE n)) []]++genUp :: [Dir] -> DecQ+genUp dir = do+  n <- newName "x"+  (p,e) <- genPatExp n dir+  return $ FunD (mkName "up") [Clause [VarP n,p] (NormalB e) []]++genPatExp :: Name -> [Dir] -> Q (Pat, Exp)+genPatExp n = gen where+    gen [] = return (WildP, VarE n)+    gen (d:dir) = do +      (p,e) <- gen dir +      x <- newName "x"+      return $ case d of+        L -> (TupP [p,VarP x] , TupE [e,VarE x])+        R -> (TupP [VarP x,p] , TupE [VarE x,e])+  +++pairT :: TypeQ -> TypeQ -> TypeQ+pairT x y = appT (appT (tupleT 2) x) y

src/Data/Comp/Derive/SmartConstructors.hs view

@@ -43,10 +43,10 @@                     function = [funD sname [clause pats (normalB [|inject $val|]) []]]                 sequence $ sig ++ function               genSig targs tname sname 0 = (:[]) $ do-                fvar <- newName "f"-                hvar <- newName "h"-                avar <- newName "a"-                let targs' = init targs+                let fvar = mkName "f"+                    hvar = mkName "h"+                    avar = mkName "a"+                    targs' = init targs                     vars = fvar:hvar:avar:targs'                     f = varT fvar                     h = varT hvar

src/Data/Comp/Desugar.hs view

@@ -20,7 +20,7 @@  -- |The desugaring term homomorphism. class (Functor f, Functor g) => Desugar f g where-    desugHom :: TermHom f g+    desugHom :: Hom f g     desugHom = desugHom' . fmap Hole     desugHom' :: Alg f (Context g a)     desugHom' x = appCxt (desugHom x)@@ -30,12 +30,12 @@ -- |Desugar a term. desugar :: Desugar f g => Term f -> Term g {-# INLINE desugar #-}-desugar = appTermHom desugHom+desugar = appHom desugHom  -- |Lift desugaring to annotated terms. desugarA :: (Functor f', Functor g', DistAnn f p f', DistAnn g p g',              Desugar f g) => Term f' -> Term g'-desugarA = appTermHom (propAnn desugHom)+desugarA = appHom (propAnn desugHom)  -- |Default desugaring instance. instance (Functor f, Functor g, f :<: g) => Desugar f g where

src/Data/Comp/Generic.hs view

@@ -77,7 +77,7 @@ size (Hole {}) = 0 size (Term t) = foldl (\s x -> s + size x) 1 t --- | This function computes the generic depth of the given term.-depth :: Foldable f => Cxt h f a -> Int-depth (Hole {}) = 0-depth (Term t) = 1 + foldl (\s x -> s + size x) 0 t+-- | This function computes the generic height of the given term.+height :: Foldable f => Cxt h f a -> Int+height (Hole {}) = 0+height (Term t) = 1 + foldl (\s x -> s `max` height x) 0 t

src/Data/Comp/Multi.hs view

@@ -265,7 +265,7 @@ >  > -- Term homomorphism for desugaring of terms > class (HFunctor f, HFunctor g) => Desugar f g where->   desugHom :: TermHom f g+>   desugHom :: Hom f g >   desugHom = desugHom' . hfmap Hole >   desugHom' :: Alg f (Context g a) >   desugHom' x = appCxt (desugHom x)@@ -312,7 +312,7 @@ > -- Compose the evaluation algebra and the desugaring homomorphism to an > -- algebra > eval :: Term Sig' :-> Term Value-> eval = cata (evalAlg `compAlg` (desugHom :: TermHom Sig' Sig))+> eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig)) >  > -- Example: evalEx = iPair (iConst 2) (iConst 1) > evalEx :: Term Value (Int,Int)@@ -364,7 +364,7 @@ >  > -- Term homomorphism for desugaring of terms > class (HFunctor f, HFunctor g) => Desugar f g where->   desugHom :: TermHom f g+>   desugHom :: Hom f g >   desugHom = desugHom' . hfmap Hole >   desugHom' :: Alg f (Context g a) >   desugHom' x = appCxt (desugHom x)@@ -387,7 +387,7 @@ >  > -- Lift the desugaring term homomorphism to a catamorphism > desug :: Term Sig' :-> Term Sig-> desug = appTermHom desugHom+> desug = appHom desugHom >  > -- Example: desugEx = iPair (iConst 2) (iConst 1) > desugEx :: Term Sig (Int,Int)@@ -395,7 +395,7 @@ >  > -- Lift desugaring to terms annotated with source positions > desugP :: Term SigP' :-> Term SigP-> desugP = appTermHom (propAnn desugHom)+> desugP = appHom (propAnn desugHom) >  > iSwapP :: (DistAnn f p f', Sugar :<: f) => p -> Term f' (a,b) -> Term f' (b,a) > iSwapP p x = Term (injectA p $ inj $ Swap x)

src/Data/Comp/Multi/Algebra.hs view

@@ -33,28 +33,28 @@       -- * Term Homomorphisms       CxtFun,       SigFun,-      TermHom,-      appTermHom,-      appTermHom',-      compTermHom,+      Hom,+      appHom,+      appHom',+      compHom,       appSigFun,       appSigFun',       compSigFun,-      termHom,+      hom,       compAlg,        -- * Monadic Term Homomorphisms       CxtFunM,       SigFunM,-      TermHomM,+      HomM,       sigFunM,-      termHom',-      appTermHomM,-      appTermHomM',-      termHomM,+      hom',+      appHomM,+      appHomM',+      homM,       appSigFunM,       appSigFunM',-      compTermHomM,+      compHomM,       compSigFunM,       compAlgM,       compAlgM',@@ -166,38 +166,38 @@ type CxtFun f g = forall h . SigFun (Cxt h f) (Cxt h g)  -- | This type represents term homomorphisms.-type TermHom f g = SigFun f (Context g)+type Hom f g = SigFun f (Context g)  -- | This function applies the given term homomorphism to a -- term/context.-appTermHom :: forall f g . (HFunctor f, HFunctor g) => TermHom f g -> CxtFun f g+appHom :: forall f g . (HFunctor f, HFunctor g) => Hom f g -> CxtFun f g -- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type -- (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.-appTermHom f = run where+appHom f = run where     run :: CxtFun f g     run (Hole b) = Hole b     run (Term t) = appCxt . f . hfmap run $ t   -- | This function applies the given term homomorphism to a--- term/context. This is the top-down variant of 'appTermHom'.-appTermHom' :: forall f g . (HFunctor g) => TermHom f g -> CxtFun f g-appTermHom' f = run where+-- term/context. This is the top-down variant of 'appHom'.+appHom' :: forall f g . (HFunctor g) => Hom f g -> CxtFun f g+appHom' f = run where     run :: CxtFun f g     run (Hole b) = Hole b     run (Term t) = appCxt . hfmap run . f $ t  -- | This function composes two term algebras.-compTermHom :: (HFunctor g, HFunctor h) => TermHom g h -> TermHom f g -> TermHom f h+compHom :: (HFunctor g, HFunctor h) => Hom g h -> Hom f g -> Hom f h -- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type -- (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.-compTermHom f g = appTermHom f . g+compHom f g = appHom f . g  -- | This function composes a term algebra with an algebra.-compAlg :: (HFunctor g) => Alg g a -> TermHom f g -> Alg f a+compAlg :: (HFunctor g) => Alg g a -> Hom f g -> Alg f a compAlg alg talg = cata' alg . talg  -- | This function applies a signature function to the given@@ -221,8 +221,8 @@ compSigFun f g = f . g  -- | Lifts the given signature function to the canonical term homomorphism.-termHom :: (HFunctor g) => SigFun f g -> TermHom f g-termHom f = simpCxt . f+hom :: (HFunctor g) => SigFun f g -> Hom f g+hom f = simpCxt . f  -- | This type represents monadic signature functions. type SigFunM m f g = forall a. NatM m (f a) (g a)@@ -233,7 +233,7 @@   -- | This type represents monadic term algebras.-type TermHomM m f g = SigFunM m f (Context g)+type HomM 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@@ -244,32 +244,32 @@  -- | This function lifts the give monadic signature function to a -- monadic term algebra.-termHom' :: (HFunctor f, HFunctor g, Monad m) =>-            SigFunM m f g -> TermHomM m f g-termHom' f = liftM  (Term . hfmap Hole) . f+hom' :: (HFunctor f, HFunctor g, Monad m) =>+            SigFunM m f g -> HomM m f g+hom' f = liftM  (Term . hfmap Hole) . f  -- | This function lifts the given signature function to a monadic -- term algebra. -termHomM :: (HFunctor g, Monad m) => SigFun f g -> TermHomM m f g-termHomM f = sigFunM $ termHom f+homM :: (HFunctor g, Monad m) => SigFun f g -> HomM m f g+homM f = sigFunM $ hom f  -- | This function applies the given monadic term homomorphism to the -- given term/context. -appTermHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)-         => TermHomM m f g -> CxtFunM m f g-appTermHomM f = run+appHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)+         => HomM m f g -> CxtFunM m f g+appHomM f = run     where run :: CxtFunM m f g           run (Hole b) = return $ Hole b           run (Term t) = liftM appCxt . (>>= f) . hmapM run $ t  -- | This function applies the given monadic term homomorphism to the--- given term/context. This is a top-down variant of 'appTermHomM'.+-- given term/context. This is a top-down variant of 'appHomM'. -appTermHomM' :: forall f g m . (HTraversable g, Monad m)-         => TermHomM m f g -> CxtFunM m f g-appTermHomM' f = run+appHomM' :: forall f g m . (HTraversable g, Monad m)+         => HomM m f g -> CxtFunM m f g+appHomM' f = run     where run :: CxtFunM m f g           run (Hole b) = return $ Hole b           run (Term t) = liftM appCxt . hmapM run =<< f t@@ -295,19 +295,19 @@  -- | This function composes two monadic term algebras. -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+compHomM :: (HTraversable g, HFunctor h, Monad m)+             => HomM m g h -> HomM m f g -> HomM m f h+compHomM f g a = g a >>= appHomM f  {-| This function composes a monadic term algebra with a monadic algebra -} -compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a+compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> HomM 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. -compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> TermHom f g -> AlgM m f a+compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a compAlgM' alg talg = cataM' alg . talg

src/Data/Comp/Multi/Annotation.hs view

@@ -65,7 +65,7 @@   propAnn :: (DistAnn f p f', DistAnn g p g', HFunctor g) -               => TermHom f g -> TermHom f' g'+               => Hom f g -> Hom f' g' propAnn alg f' = ann p (alg f)     where (f O.:&: p) = projectA f'

src/Data/Comp/Multi/Desugar.hs view

@@ -20,7 +20,7 @@  -- |The desugaring term homomorphism. class (HFunctor f, HFunctor g) => Desugar f g where-    desugHom :: TermHom f g+    desugHom :: Hom f g     desugHom = desugHom' . hfmap Hole     desugHom' :: Alg f (Context g a)     desugHom' x = appCxt (desugHom x)@@ -29,12 +29,12 @@  -- |Desugar a term. desugar :: Desugar f g => Term f :-> Term g-desugar = appTermHom desugHom+desugar = appHom desugHom  -- |Lift desugaring to annotated terms. desugarA :: (HFunctor f', HFunctor g', DistAnn f p f', DistAnn g p g',              Desugar f g) => Term f' :-> Term g'-desugarA = appTermHom (propAnn desugHom)+desugarA = appHom (propAnn desugHom)  -- |Default desugaring instance. instance (HFunctor f, HFunctor g, f :<: g) => Desugar f g where

src/Data/Comp/Multi/Functor.hs view

@@ -27,10 +27,10 @@      ) where  -- | The identity Functor.-data I a = I {unI :: a}+newtype I a = I {unI :: a}  -- | The parametrised constant functor.-data K a b = K {unK :: a}+newtype K a i = K {unK :: a}  instance Functor (K a) where     fmap _ (K x) = K x

src/Data/Comp/Multi/Ops.hs view

@@ -99,7 +99,7 @@ --  -- @data (f :&: a) (g ::  * -> *) e = f g e :&: a e@ -- --- This is too general, however, for example for 'productHTermHom'.+-- This is too general, however, for example for 'productHHom'.  data (f :&: a) (g ::  * -> *) e = f g e :&: a

src/Data/Comp/MultiParam/Algebra.hs view

@@ -35,28 +35,28 @@       -- * Term Homomorphisms       CxtFun,       SigFun,-      TermHom,-      appTermHom,-      appTermHom',-      compTermHom,+      Hom,+      appHom,+      appHom',+      compHom,       appSigFun,       appSigFun',       compSigFun,-      termHom,+      hom,       compAlg,        -- * Monadic Term Homomorphisms       CxtFunM,       SigFunM,-      TermHomM,+      HomM,       sigFunM,-      termHom',-      appTermHomM,-      appTermHomM',-      termHomM,+      hom',+      appHomM,+      appHomM',+      homM,       appSigFunM,       appSigFunM',-      compTermHomM,+      compHomM,       compSigFunM,       compAlgM,       compAlgM'@@ -157,36 +157,36 @@ type CxtFun f g = forall h. SigFun (Cxt h f) (Cxt h g)  {-| This type represents a term homomorphism. -}-type TermHom f g = SigFun f (Context g)+type Hom f g = SigFun f (Context g)  {-| Apply a term homomorphism recursively to a term/context. -}-appTermHom :: forall f g. (HDifunctor f, HDifunctor g)-              => TermHom f g -> CxtFun f g-{-# INLINE [1] appTermHom #-}-appTermHom f = run where+appHom :: forall f g. (HDifunctor f, HDifunctor g)+              => Hom f g -> CxtFun f g+{-# INLINE [1] appHom #-}+appHom f = run where     run :: CxtFun f g     run (Term t) = appCxt (f (hfmap run t))     run (Hole x) = Hole x     run (Place p) = Place p  -- | Apply a term homomorphism recursively to a term/context. This is--- a top-down variant of 'appTermHom'.-appTermHom' :: forall f g. (HDifunctor g)-              => TermHom f g -> CxtFun f g-{-# INLINE [1] appTermHom' #-}-appTermHom' f = run where+-- a top-down variant of 'appHom'.+appHom' :: forall f g. (HDifunctor g)+              => Hom f g -> CxtFun f g+{-# INLINE [1] appHom' #-}+appHom' f = run where     run :: CxtFun f g     run (Term t) = appCxt (hfmapCxt run (f t))     run (Hole x) = Hole x     run (Place p) = Place p  {-| Compose two term homomorphisms. -}-compTermHom :: (HDifunctor g, HDifunctor h)-               => TermHom g h -> TermHom f g -> TermHom f h-compTermHom f g = appTermHom f . g+compHom :: (HDifunctor g, HDifunctor h)+               => Hom g h -> Hom f g -> Hom f h+compHom f g = appHom f . g  {-| Compose an algebra with a term homomorphism to get a new algebra. -}-compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> TermHom f g -> Alg f a+compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> Hom f g -> Alg f a compAlg alg talg = cata' alg . talg  {-| This function applies a signature function to the given context. -}@@ -210,8 +210,8 @@ compSigFun f g = f . g  {-| Lifts the given signature function to the canonical term homomorphism. -}-termHom :: HDifunctor g => SigFun f g -> TermHom f g-termHom f = simpCxt . f+hom :: HDifunctor g => SigFun f g -> Hom f g+hom f = simpCxt . f  {-| This type represents a monadic signature function. -} type SigFunM m f g = forall a b. NatM m (f a b) (g a b)@@ -228,7 +228,7 @@   {-| This type represents a monadic term homomorphism. -}-type TermHomM m f g = SigFunM m f (Cxt Hole g)+type HomM m f g = SigFunM m f (Cxt Hole g)   {-| Lift the given signature function to a monadic signature function. Note that@@ -238,30 +238,30 @@ sigFunM f = return . f  {-| Lift the give monadic signature function to a monadic term homomorphism. -}-termHom' :: (HDifunctor f, HDifunctor g, Monad m)-            => SigFunM m f g -> TermHomM m f g-termHom' f = liftM  (Term . hfmap Hole) . f+hom' :: (HDifunctor f, HDifunctor g, Monad m)+            => SigFunM m f g -> HomM m f g+hom' f = liftM  (Term . hfmap Hole) . f  {-| Lift the given signature function to a monadic term homomorphism. -}-termHomM :: (HDifunctor g, Monad m) => SigFun f g -> TermHomM m f g-termHomM f = sigFunM $ termHom f+homM :: (HDifunctor g, Monad m) => SigFun f g -> HomM m f g+homM f = sigFunM $ hom f  {-| Apply a monadic term homomorphism recursively to a term/context. -}-appTermHomM :: forall f g m. (HDitraversable f m Any, HDifunctor g, Monad m)-               => TermHomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appTermHomM #-}-appTermHomM f = coerceCxtFunM run+appHomM :: forall f g m. (HDitraversable f m Any, HDifunctor g, Monad m)+               => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM #-}+appHomM f = coerceCxtFunM run     where run :: CxtFunM' m f g           run (Term t) = liftM appCxt (f =<< hdimapM run t)           run (Hole x) = return (Hole x)           run (Place p) = return (Place p)  -- | Apply a monadic term homomorphism recursively to a--- term/context. This is a top-down variant of 'appTermHomM'.-appTermHomM' :: forall f g m. (HDitraversable g m Any, Monad m)-               => TermHomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appTermHomM' #-}-appTermHomM' f = coerceCxtFunM run+-- term/context. This is a top-down variant of 'appHomM'.+appHomM' :: forall f g m. (HDitraversable g m Any, Monad m)+               => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM' #-}+appHomM' f = coerceCxtFunM run     where run :: CxtFunM' m f g           run (Term t) = liftM appCxt (hdimapMCxt run =<<  f t)           run (Hole x) = return (Hole x)@@ -289,20 +289,20 @@   {-| Compose two monadic term homomorphisms. -}-compTermHomM :: (HDitraversable g m Any, HDifunctor h, Monad m)-                => TermHomM m g h -> TermHomM m f g -> TermHomM m f h-compTermHomM f g = appTermHomM f <=< g+compHomM :: (HDitraversable g m Any, HDifunctor h, Monad m)+                => HomM m g h -> HomM m f g -> HomM m f h+compHomM f g = appHomM f <=< g  {-| Compose a monadic algebra with a monadic term homomorphism to get a new   monadic algebra. -} compAlgM :: (HDitraversable g m a, Monad m)-            => AlgM m g a -> TermHomM m f g -> AlgM m f a+            => AlgM m g a -> HomM m f g -> AlgM m f a compAlgM alg talg = freeM alg return <=< talg  {-| Compose a monadic algebra with a term homomorphism to get a new monadic   algebra. -} compAlgM' :: (HDitraversable g m a, Monad m) => AlgM m g a-          -> TermHom f g -> AlgM m f a+          -> Hom f g -> AlgM m f a compAlgM' alg talg = freeM alg return . talg  {-| This function composes two monadic signature functions. -}@@ -312,23 +312,23 @@  #ifndef NO_RULES {-# RULES-  "cata/appTermHom" forall (a :: Alg g d) (h :: TermHom f g) x.-    cata a (appTermHom h x) = cata (compAlg a h) x;+  "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.+    cata a (appHom h x) = cata (compAlg a h) x; -  "appTermHom/appTermHom" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom a (appTermHom h x) = appTermHom (compTermHom a h) x;+  "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom a (appHom h x) = appHom (compHom a h) x;  #-}  {- {-# RULES -  "cataM/appTermHomM" forall (a :: AlgM m g d) (h :: TermHomM m f g d) x.-     appTermHomM h x >>= cataM a = cataM (compAlgM a h) x;+  "cataM/appHomM" forall (a :: AlgM m g d) (h :: HomM m f g d) x.+     appHomM h x >>= cataM a = cataM (compAlgM a h) x; -  "cataM/appTermHom" forall (a :: AlgM m g d) (h :: TermHom f g) x.-     cataM a (appTermHom h x) = cataM (compAlgM' a h) x;+  "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.+     cataM a (appHom h x) = cataM (compAlgM' a h) x; -  "appTermHomM/appTermHomM" forall (a :: TermHomM m g h b) (h :: TermHomM m f g b) x.-    appTermHomM h x >>= appTermHomM a = appTermHomM (compTermHomM a h) x;+  "appHomM/appHomM" forall (a :: HomM m g h b) (h :: HomM m f g b) x.+    appHomM h x >>= appHomM a = appHomM (compHomM a h) x;  #-}  {-# RULES

src/Data/Comp/MultiParam/Annotation.hs view

@@ -59,14 +59,14 @@ {-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism  over the same signatures, but extended with annotations. -} propAnn :: (DistAnn f p f', DistAnn g p g', HDifunctor g) -           => TermHom f g -> TermHom f' g'+           => Hom f g -> Hom f' g' propAnn hom f' = ann p (hom f)     where f O.:&: p = projectA f'  {-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic   term homomorphism over the same signatures, but extended with annotations. -} propAnnM :: (DistAnn f p f', DistAnn g p g', HDifunctor g, Monad m)-         => TermHomM m f g -> TermHomM m f' g'+         => HomM m f g -> HomM m f' g' propAnnM hom f' = liftM (ann p) (hom f)     where f O.:&: p = projectA f'

src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs view

@@ -8,7 +8,8 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- Automatically derive smart constructors with annotations.+-- Automatically derive smart constructors with annotations for higher-order+-- difunctors. -- -------------------------------------------------------------------------------- @@ -21,13 +22,13 @@ import Data.Comp.Derive.Utils import Data.Comp.MultiParam.Ops import Data.Comp.MultiParam.Term+import Data.Comp.MultiParam.HDifunctor  import Control.Monad -{-| Derive smart constructors with products for a type constructor of any-  parametric kind taking at least three arguments. The smart constructors are-  similar to the ordinary constructors, but an 'injectA' is automatically-  inserted. -}+{-| Derive smart constructors with annotations for a higher-order difunctor. The+ smart constructors are similar to the ordinary constructors, but a+ 'injectA . hdimap Place id' is automatically inserted. -} smartAConstructors :: Name -> Q [Dec] smartAConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname@@ -42,6 +43,6 @@                 let pats = map varP (varPr : varNs)                     vars = map varE varNs                     val = appE [|injectA $(varE varPr)|] $-                          appE [|inj|] $ foldl appE (conE name) vars+                          appE [|inj . hdimap Place id|] $ foldl appE (conE name) vars                     function = [funD sname [clause pats (normalB [|Term $val|]) []]]                 sequence function

src/Data/Comp/MultiParam/Derive/SmartConstructors.hs view

@@ -8,7 +8,7 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- Automatically derive smart constructors for parametric types.+-- Automatically derive smart constructors for higher-order difunctors. -- -------------------------------------------------------------------------------- @@ -21,11 +21,12 @@ import Data.Comp.Derive.Utils import Data.Comp.MultiParam.Sum import Data.Comp.MultiParam.Term+import Data.Comp.MultiParam.HDifunctor import Control.Monad -{-| Derive smart constructors for a type constructor of any parametric kind- taking at least three arguments. The smart constructors are similar to the- ordinary constructors, but an 'inject' is automatically inserted. -}+{-| Derive smart constructors for a higher-order difunctor. The smart+ constructors are similar to the ordinary constructors, but a+ 'inject . hdimap Place id' is automatically inserted. -} smartConstructors :: Name -> Q [Dec] smartConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname@@ -47,7 +48,7 @@                     vars = map varE varNs                     val = foldl appE (conE name) vars                     sig = genSig targs tname sname args miTp-                    function = [funD sname [clause pats (normalB [|inject $val|]) []]]+                    function = [funD sname [clause pats (normalB [|inject (hdimap Place id $val)|]) []]]                 sequence $ sig ++ function               genSig targs tname sname 0 miTp = (:[]) $ do                 hvar <- newName "h"

src/Data/Comp/MultiParam/Desugar.hs view

@@ -20,7 +20,7 @@  -- |The desugaring term homomorphism. class (HDifunctor f, HDifunctor g) => Desugar f g where-    desugHom :: TermHom f g+    desugHom :: Hom f g     desugHom = desugHom' . hfmap Hole     desugHom' :: f a (Cxt h g a b) :-> Cxt h g a b     desugHom' x = appCxt (desugHom x)@@ -29,12 +29,12 @@  -- |Desugar a term. desugar :: Desugar f g => Term f :-> Term g-desugar = appTermHom desugHom+desugar = appHom desugHom  -- |Lift desugaring to annotated terms. desugarA :: (HDifunctor f', HDifunctor g', DistAnn f p f', DistAnn g p g',              Desugar f g) => Term f' :-> Term g'-desugarA = appTermHom (propAnn desugHom)+desugarA = appHom (propAnn desugHom)  -- |Default desugaring instance. instance (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g where

src/Data/Comp/MultiParam/HDifunctor.hs view

@@ -30,10 +30,10 @@ import Data.Comp.Multi.Functor (HFunctor (..))  -- | The identity functor.-data I a = I {unI :: a}+newtype I a = I {unI :: a}  -- | The parametrised constant functor.-data K a i = K {unK :: a}+newtype K a i = K {unK :: a}  instance Functor I where     fmap f (I x) = I (f x)

src/Data/Comp/Param/Algebra.hs view

@@ -32,36 +32,36 @@       -- * Term Homomorphisms       CxtFun,       SigFun,-      TermHom,-      appTermHom,-      appTermHom',-      compTermHom,+      Hom,+      appHom,+      appHom',+      compHom,       appSigFun,       appSigFun',       compSigFun,-      compTermHomSigFun,-      compSigFunTermHom,-      termHom,+      compHomSigFun,+      compSigFunHom,+      hom,       compAlg,       compAlgSigFun,        -- * Monadic Term Homomorphisms       CxtFunM,       SigFunM,-      TermHomM,+      HomM,       SigFunMD,-      TermHomMD,+      HomMD,       sigFunM,-      appTermHomM,-      appTermHomM',-      termHomM,-      termHomMD,+      appHomM,+      appHomM',+      homM,+      homMD,       appSigFunM,       appSigFunM',       appSigFunMD,-      compTermHomM,+      compHomM,       compSigFunM,-      compSigFunTermHomM,+      compSigFunHomM,       compAlgSigFunM,       compAlgSigFunM',       compAlgM,@@ -118,7 +118,7 @@         => Alg f a -> (b -> a) -> Cxt h f a b -> a free f g = run     where run :: Cxt h f a b -> a-          run (Term t) = f (fmap run t)+          run (Term t) = f (difmap run t)           run (Hole x) = g x           run (Place p) = p @@ -127,7 +127,7 @@ {-# NOINLINE [1] cata #-} cata f = run . coerceCxt     where run :: Trm f a -> a-          run (Term t) = f (fmap run t)+          run (Term t) = f (difmap run t)           run (Place x) = x  {-| A generalisation of 'cata' from terms over @f@ to contexts over @f@, where@@ -138,7 +138,7 @@  {-| This function applies a whole context into another context. -} appCxt :: Difunctor f => Context f a (Cxt h f a b) -> Cxt h f a b-appCxt (Term t) = Term (fmap appCxt t)+appCxt (Term t) = Term (difmap appCxt t) appCxt (Hole x) = x appCxt (Place p) = Place p @@ -185,36 +185,36 @@ type SigFun f g = forall a b. f a b -> g a b  {-| This type represents a term homomorphism. -}-type TermHom f g = SigFun f (Context g)+type Hom f g = SigFun f (Context g)  {-| Apply a term homomorphism recursively to a term/context. -}-appTermHom :: forall f g. (Difunctor f, Difunctor g)-              => TermHom f g -> CxtFun f g-{-# NOINLINE [1] appTermHom #-}-appTermHom f = run where+appHom :: forall f g. (Difunctor f, Difunctor g)+              => Hom f g -> CxtFun f g+{-# NOINLINE [1] appHom #-}+appHom f = run where     run :: CxtFun f g-    run (Term t) = appCxt (f (fmap run t))+    run (Term t) = appCxt (f (difmap run t))     run (Hole x) = Hole x     run (Place p) = Place p  {-| Apply a term homomorphism recursively to a term/context. -}-appTermHom' :: forall f g. (Difunctor g)-              => TermHom f g -> CxtFun f g-{-# NOINLINE [1] appTermHom' #-}-appTermHom' f = run where+appHom' :: forall f g. (Difunctor g)+              => Hom f g -> CxtFun f g+{-# NOINLINE [1] appHom' #-}+appHom' f = run where     run :: CxtFun f g     run (Term t) = appCxt (fmapCxt run (f t))     run (Hole x) = Hole x     run (Place p) = Place p  {-| Compose two term homomorphisms. -}-compTermHom :: (Difunctor g, Difunctor h)-               => TermHom g h -> TermHom f g -> TermHom f h-compTermHom f g = appTermHom f . g+compHom :: (Difunctor g, Difunctor h)+               => Hom g h -> Hom f g -> Hom f h+compHom f g = appHom f . g   {-| Compose an algebra with a term homomorphism to get a new algebra. -}-compAlg :: (Difunctor f, Difunctor g) => Alg g a -> TermHom f g -> Alg f a+compAlg :: (Difunctor f, Difunctor g) => Alg g a -> Hom f g -> Alg f a compAlg alg talg = cata' alg . talg  compAlgSigFun  :: Alg g a -> SigFun f g -> Alg f a@@ -225,11 +225,11 @@ appSigFun :: forall f g. (Difunctor f) => SigFun f g -> CxtFun f g {-# NOINLINE [1] appSigFun #-} appSigFun f = run-    where run (Term t) = Term $ f $ fmap run t+    where run (Term t) = Term $ f $ difmap run t           run (Place x) = Place x           run (Hole x) = Hole x -- implementation via term homomorphisms---  appSigFun f = appTermHom $ termHom f+--  appSigFun f = appHom $ hom f   -- | This function applies a signature function to the given@@ -237,7 +237,7 @@ appSigFun' :: forall f g. (Difunctor g) => SigFun f g -> CxtFun f g {-# NOINLINE [1] appSigFun' #-} appSigFun' f = run-    where run (Term t) = Term $ fmap run $ f t+    where run (Term t) = Term $ difmap run $ f t           run (Place x) = Place x           run (Hole x) = Hole x @@ -246,17 +246,17 @@ compSigFun f g = f . g  {-| This function composes a term homomorphism and a signature function. -}-compTermHomSigFun :: TermHom g h -> SigFun f g -> TermHom f h-compTermHomSigFun f g = f . g+compHomSigFun :: Hom g h -> SigFun f g -> Hom f h+compHomSigFun f g = f . g  {-| This function composes a term homomorphism and a signature function. -}-compSigFunTermHom :: (Difunctor g) => SigFun g h -> TermHom f g -> TermHom f h-compSigFunTermHom f g = appSigFun f . g+compSigFunHom :: (Difunctor g) => SigFun g h -> Hom f g -> Hom f h+compSigFunHom f g = appSigFun f . g   {-| Lifts the given signature function to the canonical term homomorphism. -}-termHom :: Difunctor g => SigFun f g -> TermHom f g-termHom f = simpCxt . f+hom :: Difunctor g => SigFun f g -> Hom f g+hom f = simpCxt . f  {-| This type represents a monadic signature function. -} type SigFunM m f g = forall a b. f a b -> m (g a b)@@ -275,11 +275,11 @@ type SigFunMD m f g = forall a b. f a (m b) -> m (g a b)  {-| This type represents a monadic term homomorphism. -}-type TermHomM m f g = SigFunM m f (Context g)+type HomM m f g = SigFunM m f (Context g)  {-| This type represents a monadic term homomorphism. It is similar to-  'TermHomMD but has monadic values also in the domain. -}-type TermHomMD m f g = SigFunMD m f (Context g)+  'HomMD but has monadic values also in the domain. -}+type HomMD m f g = SigFunMD m f (Context g)  {-| Lift the given signature function to a monadic signature function. Note that   term homomorphisms are instances of signature functions. Hence this function@@ -290,15 +290,15 @@   {-| Lift the given signature function to a monadic term homomorphism. -}-termHomM :: (Difunctor g, Monad m) => SigFunM m f g -> TermHomM m f g-termHomM f = liftM simpCxt . f+homM :: (Difunctor g, Monad m) => SigFunM m f g -> HomM m f g+homM f = liftM simpCxt . f  -- | Apply a monadic term homomorphism recursively to a -- term/context. The monad is sequenced bottom-up.-appTermHomM :: forall f g m. (Ditraversable f m Any, Difunctor g)-               => TermHomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appTermHomM #-}-appTermHomM f = coerceCxtFunM run+appHomM :: forall f g m. (Ditraversable f m Any, Difunctor g)+               => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM #-}+appHomM f = coerceCxtFunM run     where run :: CxtFunM' m f g           run (Term t) = liftM appCxt . f =<< dimapM run t           run (Hole x) = return (Hole x)@@ -307,9 +307,9 @@  -- | Apply a monadic term homomorphism recursively to a -- term/context. The monad is sequence top-down.-appTermHomM' :: forall f g m. (Ditraversable g m Any)-         => TermHomM m f g ->  CxtFunM m f g-appTermHomM' f = coerceCxtFunM run+appHomM' :: forall f g m. (Ditraversable g m Any)+         => HomM m f g ->  CxtFunM m f g+appHomM' f = coerceCxtFunM run     where run :: CxtFunM' m f g           run (Term t)  = liftM appCxt . dimapMCxt run =<< f t           run (Place p) = return (Place p)@@ -318,11 +318,11 @@  {-| This function constructs the unique monadic homomorphism from the   initial term algebra to the given term algebra. -}-termHomMD :: forall f g m. (Difunctor f, Difunctor g, Monad m)-             => TermHomMD m f g -> CxtFunM m f g-termHomMD f = run +homMD :: forall f g m. (Difunctor f, Difunctor g, Monad m)+             => HomMD m f g -> CxtFunM m f g+homMD f = run      where run :: CxtFunM m f g-          run (Term t) = liftM appCxt (f (fmap run t))+          run (Term t) = liftM appCxt (f (difmap run t))           run (Hole x) = return (Hole x)           run (Place p) = return (Place p) @@ -335,7 +335,7 @@           run (Place x) = return $ Place x           run (Hole x) = return $ Hole x -- implementation via term homomorphisms---  appSigFunM f = appTermHomM $ termHom' f+--  appSigFunM f = appHomM $ hom' f  -- | This function applies a monadic signature function to the given -- context. This is a 'top-down variant of 'appSigFunM'.@@ -353,49 +353,49 @@                => SigFunMD m f g -> CxtFunM m f g appSigFunMD f = run      where run :: CxtFunM m f g-          run (Term t) = liftM Term (f (fmap run t))+          run (Term t) = liftM Term (f (difmap run t))           run (Hole x) = return (Hole x)           run (Place p) = return (Place p)  {-| Compose two monadic term homomorphisms. -}-compTermHomM :: (Ditraversable g m Any, Difunctor h, Monad m)-                => TermHomM m g h -> TermHomM m f g -> TermHomM m f h-compTermHomM f g = appTermHomM f <=< g+compHomM :: (Ditraversable g m Any, Difunctor h, Monad m)+                => HomM m g h -> HomM m f g -> HomM m f h+compHomM f g = appHomM f <=< g  {-| Compose two monadic term homomorphisms. -}-compTermHomM' :: (Ditraversable h m Any, Monad m)-                => TermHomM m g h -> TermHomM m f g -> TermHomM m f h-compTermHomM' f g = appTermHomM' f <=< g+compHomM' :: (Ditraversable h m Any, Monad m)+                => HomM m g h -> HomM m f g -> HomM m f h+compHomM' f g = appHomM' f <=< g  {-| Compose two monadic term homomorphisms. -}-compTermHomM_ :: (Difunctor h, Difunctor g, Monad m)-                => TermHom g h -> TermHomM m f g -> TermHomM m f h-compTermHomM_ f g = liftM (appTermHom f) . g+compHomM_ :: (Difunctor h, Difunctor g, Monad m)+                => Hom g h -> HomM m f g -> HomM m f h+compHomM_ f g = liftM (appHom f) . g   {-| Compose two monadic term homomorphisms. -}-compTermHomSigFunM :: (Monad m) => TermHomM m g h -> SigFunM m f g -> TermHomM m f h-compTermHomSigFunM f g = f <=< g+compHomSigFunM :: (Monad m) => HomM m g h -> SigFunM m f g -> HomM m f h+compHomSigFunM f g = f <=< g  {-| Compose two monadic term homomorphisms. -}-compSigFunTermHomM :: (Ditraversable g m Any) => SigFunM m g h -> TermHomM m f g -> TermHomM m f h-compSigFunTermHomM f g = appSigFunM f <=< g+compSigFunHomM :: (Ditraversable g m Any) => SigFunM m g h -> HomM m f g -> HomM m f h+compSigFunHomM f g = appSigFunM f <=< g  {-| Compose two monadic term homomorphisms. -}-compSigFunTermHomM' :: (Ditraversable h m Any) => SigFunM m g h -> TermHomM m f g -> TermHomM m f h-compSigFunTermHomM' f g = appSigFunM' f <=< g+compSigFunHomM' :: (Ditraversable h m Any) => SigFunM m g h -> HomM m f g -> HomM m f h+compSigFunHomM' f g = appSigFunM' f <=< g  {-| Compose a monadic algebra with a monadic term homomorphism to get a new   monadic algebra. -} compAlgM :: (Ditraversable g m a, Monad m)-            => AlgM m g a -> TermHomM m f g -> AlgM m f a+            => AlgM m g a -> HomM m f g -> AlgM m f a compAlgM alg talg = freeM alg return <=< talg   {-| Compose a monadic algebra with a term homomorphism to get a new monadic   algebra. -} compAlgM' :: (Ditraversable g m a, Monad m) => AlgM m g a-          -> TermHom f g -> AlgM m f a+          -> Hom f g -> AlgM m f a compAlgM' alg talg = freeM alg return . talg  {-| Compose a monadic algebra with a monadic signature function to get a new@@ -432,7 +432,7 @@ ana f x = run (x,[])     where run (a,bs) = case f a bs of                          Left p -> Place p-                         Right t -> Term $ fmap run t+                         Right t -> Term $ difmap run t  {-| This type represents a monadic coalgebra over a difunctor @f@ and carrier   @a@. -}@@ -459,7 +459,7 @@ para :: forall f a. Difunctor f => RAlg f a -> Term f -> a para f = run . coerceCxt     where run :: Trm f a -> a-          run (Term t) = f $ fmap (\x -> (x, run x)) t+          run (Term t) = f $ difmap (\x -> (x, run x)) t           run (Place x) = x  {-| This type represents a monadic r-algebra over a difunctor @f@ and carrier@@ -487,7 +487,7 @@     where run :: (a,[(a,b)]) -> Trm f b           run (a,bs) = case coa a bs of                          Left x -> Place x-                         Right t -> Term $ fmap run' t+                         Right t -> Term $ difmap run' t           run' :: Either (Trm f b) (a,[(a,b)]) -> Trm f b           run' (Left t) = t           run' (Right x) = run x@@ -565,8 +565,8 @@ futu coa x = run (x,[])     where run (a,bs) = case coa a bs of                          Left p -> Place p-                         Right t -> Term $ fmap run' t-          run' (Term t) = Term $ fmap run' t+                         Right t -> Term $ difmap run' t+          run' (Term t) = Term $ difmap run' t           run' (Hole x) = run x           run' (Place p) = Place p @@ -595,7 +595,7 @@ futu' :: forall f a. Difunctor f => CVCoalg' f a -> a -> Term f futu' coa x = run (x,[])     where run (a,bs) = run' $ coa a bs-          run' (Term t) = Term $ fmap run' t+          run' (Term t) = Term $ difmap run' t           run' (Hole x) = run x           run' (Place p) = Place p @@ -603,35 +603,35 @@ -- functions only used for rewrite rules -- ------------------------------------------- -appAlgTermHom :: forall f g d . (Difunctor g) => Alg g d -> TermHom f g -> Term f -> d-{-# NOINLINE [1] appAlgTermHom #-}-appAlgTermHom alg hom = run . coerceCxt where+appAlgHom :: forall f g d . (Difunctor g) => Alg g d -> Hom f g -> Term f -> d+{-# NOINLINE [1] appAlgHom #-}+appAlgHom alg hom = run . coerceCxt where     run :: Trm f d -> d     run (Term t) = run' $ hom t     run (Place a) = a     run' :: Context g d (Trm f d) -> d-    run' (Term t) = alg $ fmap run' t+    run' (Term t) = alg $ difmap run' t     run' (Place a) = a     run' (Hole x) = run x   -- | This function applies a signature function after a term homomorphism.-appSigFunTermHom :: forall f g h. (Difunctor g)-                 => SigFun g h -> TermHom f g -> CxtFun f h-{-# NOINLINE [1] appSigFunTermHom #-}-appSigFunTermHom f g = run where+appSigFunHom :: forall f g h. (Difunctor g)+                 => SigFun g h -> Hom f g -> CxtFun f h+{-# NOINLINE [1] appSigFunHom #-}+appSigFunHom f g = run where     run :: CxtFun f h     run (Term t) = run' $ g t     run (Place a) = Place a     run (Hole h) = Hole h     run' :: Context g a (Cxt h' f a b) -> Cxt h' h a b-    run' (Term t) = Term $ f $ fmap run' t+    run' (Term t) = Term $ f $ difmap run' t     run' (Place a) = Place a     run' (Hole h) = run h -appAlgTermHomM :: forall m g f d . (Monad m, Ditraversable g m d)-               => AlgM m g d -> TermHomM m f g -> Term f -> m d-appAlgTermHomM alg hom = run . coerceCxt where +appAlgHomM :: forall m g f d . (Monad m, Ditraversable g m d)+               => AlgM m g d -> HomM m f g -> Term f -> m d+appAlgHomM alg hom = run . coerceCxt where      run :: Trm f d -> m d     run (Term t) = run' =<< hom t     run (Place a) = return a@@ -642,9 +642,9 @@   -appTermHomTermHomM :: forall m f g h . (Ditraversable g m Any, Difunctor h)-                   => TermHomM m g h -> TermHomM m f g -> CxtFunM m f h-appTermHomTermHomM f g = coerceCxtFunM run where+appHomHomM :: forall m f g h . (Ditraversable g m Any, Difunctor h)+                   => HomM m g h -> HomM m f g -> CxtFunM m f h+appHomHomM f g = coerceCxtFunM run where     run :: CxtFunM' m f h     run (Term t) = run' =<< g t     run (Place a) = return $ Place a@@ -654,9 +654,9 @@     run' (Place a) = return $ Place a     run' (Hole h) = run h -appSigFunTermHomM :: forall m f g h . (Ditraversable g m Any)-                   => SigFunM m g h -> TermHomM m f g -> CxtFunM m f h-appSigFunTermHomM f g = coerceCxtFunM run where+appSigFunHomM :: forall m f g h . (Ditraversable g m Any)+                   => SigFunM m g h -> HomM m f g -> CxtFunM m f h+appSigFunHomM f g = coerceCxtFunM run where     run :: CxtFunM' m f h     run (Term t) = run' =<< g t     run (Place a) = return $ Place a@@ -673,50 +673,50 @@  #ifndef NO_RULES {-# RULES-  "cata/appTermHom" forall (a :: Alg g d) (h :: TermHom f g) x.-    cata a (appTermHom h x) = cata (compAlg a h) x;+  "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.+    cata a (appHom h x) = cata (compAlg a h) x; -  "cata/appTermHom'" forall (a :: Alg g d) (h :: TermHom f g) x.-    cata a (appTermHom' h x) = appAlgTermHom a h x;+  "cata/appHom'" forall (a :: Alg g d) (h :: Hom f g) x.+    cata a (appHom' h x) = appAlgHom a h x;    "cata/appSigFun" forall (a :: Alg g d) (h :: SigFun f g) x.     cata a (appSigFun h x) = cata (compAlgSigFun a h) x;    "cata/appSigFun'" forall (a :: Alg g d) (h :: SigFun f g) x.-    cata a (appSigFun' h x) = appAlgTermHom a (termHom h) x;+    cata a (appSigFun' h x) = appAlgHom a (hom h) x; -  "cata/appSigFunTermHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    cata f (appSigFunTermHom g h x) = appAlgTermHom (compAlgSigFun f g) h x;+  "cata/appSigFunHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    cata f (appSigFunHom g h x) = appAlgHom (compAlgSigFun f g) h x; -  "appAlgTermHom/appTermHom" forall (a :: Alg h d) (f :: TermHom f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appTermHom f x) = cata (compAlg a (compTermHom h f)) x;+  "appAlgHom/appHom" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.+    appAlgHom a h (appHom f x) = cata (compAlg a (compHom h f)) x; -  "appAlgTermHom/appTermHom'" forall (a :: Alg h d) (f :: TermHom f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appTermHom' f x) = appAlgTermHom a (compTermHom h f) x;+  "appAlgHom/appHom'" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.+    appAlgHom a h (appHom' f x) = appAlgHom a (compHom h f) x; -  "appAlgTermHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appSigFun f x) = cata (compAlg a (compTermHomSigFun h f)) x;+  "appAlgHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.+    appAlgHom a h (appSigFun f x) = cata (compAlg a (compHomSigFun h f)) x; -  "appAlgTermHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: TermHom g h) x.-    appAlgTermHom a h (appSigFun' f x) = appAlgTermHom a (compTermHomSigFun h f) x;+  "appAlgHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.+    appAlgHom a h (appSigFun' f x) = appAlgHom a (compHomSigFun h f) x; -  "appAlgTermHom/appSigFunTermHom" forall (a :: Alg i d) (f :: TermHom f g) (g :: SigFun g h)-                                          (h :: TermHom h i) x.-    appAlgTermHom a h (appSigFunTermHom g f x)-      = appAlgTermHom a (compTermHom (compTermHomSigFun h g) f) x;+  "appAlgHom/appSigFunHom" forall (a :: Alg i d) (f :: Hom f g) (g :: SigFun g h)+                                          (h :: Hom h i) x.+    appAlgHom a h (appSigFunHom g f x)+      = appAlgHom a (compHom (compHomSigFun h g) f) x; -  "appTermHom/appTermHom" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom a (appTermHom h x) = appTermHom (compTermHom a h) x;+  "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom a (appHom h x) = appHom (compHom a h) x; -  "appTermHom'/appTermHom'" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom' a (appTermHom' h x) = appTermHom' (compTermHom a h) x;+  "appHom'/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom' a (appHom' h x) = appHom' (compHom a h) x; -  "appTermHom'/appTermHom" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom' a (appTermHom h x) = appTermHom (compTermHom a h) x;+  "appHom'/appHom" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom' a (appHom h x) = appHom (compHom a h) x; -  "appTermHom/appTermHom'" forall (a :: TermHom g h) (h :: TermHom f g) x.-    appTermHom a (appTermHom' h x) = appTermHom' (compTermHom a h) x;+  "appHom/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom a (appHom' h x) = appHom' (compHom a h) x;        "appSigFun/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.     appSigFun f (appSigFun g x) = appSigFun (compSigFun f g) x;@@ -725,206 +725,206 @@     appSigFun' f (appSigFun' g x) = appSigFun' (compSigFun f g) x;    "appSigFun/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.-    appSigFun f (appSigFun' g x) = appSigFunTermHom f (termHom g) x;+    appSigFun f (appSigFun' g x) = appSigFunHom f (hom g) x;    "appSigFun'/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.     appSigFun' f (appSigFun g x) = appSigFun (compSigFun f g) x; -  "appTermHom/appSigFun" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom f (appSigFun g x) = appTermHom (compTermHomSigFun f g) x;+  "appHom/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom f (appSigFun g x) = appHom (compHomSigFun f g) x; -  "appTermHom/appSigFun'" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom f (appSigFun' g x) =  appTermHom' (compTermHomSigFun f g) x;+  "appHom/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom f (appSigFun' g x) =  appHom' (compHomSigFun f g) x; -  "appTermHom'/appSigFun'" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom' f (appSigFun' g x) =  appTermHom' (compTermHomSigFun f g) x;+  "appHom'/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom' f (appSigFun' g x) =  appHom' (compHomSigFun f g) x; -  "appTermHom'/appSigFun" forall (f :: TermHom g h) (g :: SigFun f g) x.-    appTermHom' f (appSigFun g x) = appTermHom (compTermHomSigFun f g) x;+  "appHom'/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom' f (appSigFun g x) = appHom (compHomSigFun f g) x;     -  "appSigFun/appTermHom" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun f (appTermHom g x) = appSigFunTermHom f g x;+  "appSigFun/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun f (appHom g x) = appSigFunHom f g x; -  "appSigFun'/appTermHom'" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun' f (appTermHom' g x) = appTermHom' (compSigFunTermHom f g) x;+  "appSigFun'/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun' f (appHom' g x) = appHom' (compSigFunHom f g) x; -  "appSigFun/appTermHom'" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun f (appTermHom' g x) = appSigFunTermHom f g x;+  "appSigFun/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun f (appHom' g x) = appSigFunHom f g x; -  "appSigFun'/appTermHom" forall (f :: SigFun g h) (g :: TermHom f g) x.-    appSigFun' f (appTermHom g x) = appTermHom (compSigFunTermHom f g) x;+  "appSigFun'/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun' f (appHom g x) = appHom (compSigFunHom f g) x;     -  "appSigFunTermHom/appSigFun" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)+  "appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)                                       (h :: SigFun f1 f2) x.-    appSigFunTermHom f g (appSigFun h x)-    = appSigFunTermHom f (compTermHomSigFun g h) x;+    appSigFunHom f g (appSigFun h x)+    = appSigFunHom f (compHomSigFun g h) x; -  "appSigFunTermHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)+  "appSigFunHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)                                       (h :: SigFun f1 f2) x.-    appSigFunTermHom f g (appSigFun' h x)-    = appSigFunTermHom f (compTermHomSigFun g h) x;+    appSigFunHom f g (appSigFun' h x)+    = appSigFunHom f (compHomSigFun g h) x; -  "appSigFunTermHom/appTermHom" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFunTermHom f g (appTermHom h x)-    = appSigFunTermHom f (compTermHom g h) x;+  "appSigFunHom/appHom" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFunHom f g (appHom h x)+    = appSigFunHom f (compHom g h) x; -  "appSigFunTermHom/appTermHom'" forall (f :: SigFun f3 f4) (g :: TermHom f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFunTermHom f g (appTermHom' h x)-    = appSigFunTermHom f (compTermHom g h) x;+  "appSigFunHom/appHom'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFunHom f g (appHom' h x)+    = appSigFunHom f (compHom g h) x; -  "appSigFun/appSigFunTermHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFun f (appSigFunTermHom g h x) = appSigFunTermHom (compSigFun f g) h x;+  "appSigFun/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFun f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x; -  "appSigFun'/appSigFunTermHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appSigFun' f (appSigFunTermHom g h x) = appSigFunTermHom (compSigFun f g) h x;+  "appSigFun'/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appSigFun' f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x; -  "appTermHom/appSigFunTermHom" forall (f :: TermHom f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appTermHom f (appSigFunTermHom g h x) = appTermHom' (compTermHom (compTermHomSigFun f g) h) x;+  "appHom/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appHom f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x; -  "appTermHom'/appSigFunTermHom" forall (f :: TermHom f3 f4) (g :: SigFun f2 f3)-                                      (h :: TermHom f1 f2) x.-    appTermHom' f (appSigFunTermHom g h x) = appTermHom' (compTermHom (compTermHomSigFun f g) h) x;+  "appHom'/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)+                                      (h :: Hom f1 f2) x.+    appHom' f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x; -  "appSigFunTermHom/appSigFunTermHom" forall (f1 :: SigFun f4 f5) (f2 :: TermHom f3 f4)-                                             (f3 :: SigFun f2 f3) (f4 :: TermHom f1 f2) x.-    appSigFunTermHom f1 f2 (appSigFunTermHom f3 f4 x)-      = appSigFunTermHom f1 (compTermHom (compTermHomSigFun f2 f3) f4) x;+  "appSigFunHom/appSigFunHom" forall (f1 :: SigFun f4 f5) (f2 :: Hom f3 f4)+                                             (f3 :: SigFun f2 f3) (f4 :: Hom f1 f2) x.+    appSigFunHom f1 f2 (appSigFunHom f3 f4 x)+      = appSigFunHom f1 (compHom (compHomSigFun f2 f3) f4) x;  #-}  {-# RULES -  "cataM/appTermHomM" forall (a :: AlgM Maybe g d) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= cataM a =  appAlgTermHomM a h x;+  "cataM/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.+     appHomM h x >>= cataM a =  appAlgHomM a h x; -  "cataM/appTermHomM'" forall (a :: AlgM Maybe g d) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= cataM a = appAlgTermHomM a h x;+  "cataM/appHomM'" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.+     appHomM' h x >>= cataM a = appAlgHomM a h x;    "cataM/appSigFunM" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.-     appSigFunM h x >>= cataM a =  appAlgTermHomM a (termHomM h) x;+     appSigFunM h x >>= cataM a =  appAlgHomM a (homM h) x;    "cataM/appSigFunM'" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= cataM a = appAlgTermHomM a (termHomM h) x;+     appSigFunM' h x >>= cataM a = appAlgHomM a (homM h) x; -  "cataM/appTermHom" forall (a :: AlgM m g d) (h :: TermHom f g) x.-     cataM a (appTermHom h x) = appAlgTermHomM a (sigFunM h) x;+  "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.+     cataM a (appHom h x) = appAlgHomM a (sigFunM h) x; -  "cataM/appTermHom'" forall (a :: AlgM m g d) (h :: TermHom f g) x.-     cataM a (appTermHom' h x) = appAlgTermHomM a (sigFunM h) x;+  "cataM/appHom'" forall (a :: AlgM m g d) (h :: Hom f g) x.+     cataM a (appHom' h x) = appAlgHomM a (sigFunM h) x;    "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.-     cataM a (appSigFun h x) = appAlgTermHomM a (sigFunM $ termHom h) x;+     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;    "cataM/appSigFun'" forall (a :: AlgM m g d) (h :: SigFun f g) x.-     cataM a (appSigFun' h x) = appAlgTermHomM a (sigFunM $ termHom h) x;+     cataM a (appSigFun' h x) = appAlgHomM a (sigFunM $ hom h) x;    "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.-     cataM a (appSigFun h x) = appAlgTermHomM a (sigFunM $ termHom h) x;+     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x; -  "cataM/appSigFunTermHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: TermHom f g) x.-     cataM a (appSigFunTermHom g f x) = appAlgTermHomM a (sigFunM $ compSigFunTermHom g f) x;+  "cataM/appSigFunHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: Hom f g) x.+     cataM a (appSigFunHom g f x) = appAlgHomM a (sigFunM $ compSigFunHom g f) x; -  "appTermHomM/appTermHomM" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appTermHomM a = appTermHomM (compTermHomM a h) x;+  "appHomM/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appHomM a = appHomM (compHomM a h) x; -  "appTermHomM/appSigFunM" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM h x >>= appTermHomM a = appTermHomM (compTermHomSigFunM a h) x;+  "appHomM/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM h x >>= appHomM a = appHomM (compHomSigFunM a h) x; -  "appTermHomM/appTermHomM'" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appTermHomM a = appTermHomTermHomM a h x;+  "appHomM/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appHomM a = appHomHomM a h x; -  "appTermHomM/appSigFunM'" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= appTermHomM a = appTermHomTermHomM a (termHomM h) x;+  "appHomM/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM' h x >>= appHomM a = appHomHomM a (homM h) x; -  "appTermHomM'/appTermHomM" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appTermHomM' a = appTermHomM' (compTermHomM' a h) x;+  "appHomM'/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appHomM' a = appHomM' (compHomM' a h) x; -  "appTermHomM'/appSigFunM" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM h x >>= appTermHomM' a = appTermHomM' (compTermHomSigFunM a h) x;+  "appHomM'/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x; -  "appTermHomM'/appTermHomM'" forall (a :: TermHomM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appTermHomM' a = appTermHomM' (compTermHomM' a h) x;+  "appHomM'/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appHomM' a = appHomM' (compHomM' a h) x; -  "appTermHomM'/appSigFunM'" forall (a :: TermHomM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= appTermHomM' a = appTermHomM' (compTermHomSigFunM a h) x;+  "appHomM'/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.+     appSigFunM' h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x; -  "appTermHomM/appTermHom" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM a (appTermHom h x) = appTermHomTermHomM a (sigFunM h) x;+  "appHomM/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM a (appHom h x) = appHomHomM a (sigFunM h) x; -  "appTermHomM/appSigFun" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM a (appSigFun h x) = appTermHomTermHomM a (sigFunM $ termHom h) x;+  "appHomM/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM a (appSigFun h x) = appHomHomM a (sigFunM $ hom h) x; -  "appTermHomM'/appTermHom" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM' a (appTermHom h x) = appTermHomM' (compTermHomM' a (sigFunM h)) x;+  "appHomM'/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM' a (appHom h x) = appHomM' (compHomM' a (sigFunM h)) x; -  "appTermHomM'/appSigFun" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM' a (appSigFun h x) = appTermHomM' (compTermHomSigFunM a (sigFunM h)) x;+  "appHomM'/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM' a (appSigFun h x) = appHomM' (compHomSigFunM a (sigFunM h)) x; -  "appTermHomM/appTermHom'" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM a (appTermHom' h x) = appTermHomTermHomM a (sigFunM h) x;+  "appHomM/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM a (appHom' h x) = appHomHomM a (sigFunM h) x; -  "appTermHomM/appSigFun'" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM a (appSigFun' h x) = appTermHomTermHomM a (sigFunM $ termHom h) x;+  "appHomM/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM a (appSigFun' h x) = appHomHomM a (sigFunM $ hom h) x; -  "appTermHomM'/appTermHom'" forall (a :: TermHomM m g h) (h :: TermHom f g) x.-     appTermHomM' a (appTermHom' h x) = appTermHomM' (compTermHomM' a (sigFunM h)) x;+  "appHomM'/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM' a (appHom' h x) = appHomM' (compHomM' a (sigFunM h)) x; -  "appTermHomM'/appSigFun'" forall (a :: TermHomM m g h) (h :: SigFun f g) x.-     appTermHomM' a (appSigFun' h x) = appTermHomM' (compTermHomSigFunM a (sigFunM h)) x;+  "appHomM'/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.+     appHomM' a (appSigFun' h x) = appHomM' (compHomSigFunM a (sigFunM h)) x; -  "appSigFunM/appTermHomM" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appSigFunM a = appSigFunTermHomM a h x;+  "appSigFunM/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appSigFunM a = appSigFunHomM a h x;    "appSigFunHomM/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.      appSigFunM h x >>= appSigFunM a = appSigFunM (compSigFunM a h) x; -  "appSigFunM/appTermHomM'" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appSigFunM a = appSigFunTermHomM a h x;+  "appSigFunM/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appSigFunM a = appSigFunHomM a h x;    "appSigFunM/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.-     appSigFunM' h x >>= appSigFunM a = appSigFunTermHomM a (termHomM h) x;+     appSigFunM' h x >>= appSigFunM a = appSigFunHomM a (homM h) x; -  "appSigFunM'/appTermHomM" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM h x >>= appSigFunM' a = appTermHomM' (compSigFunTermHomM' a h) x;+  "appSigFunM'/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;    "appSigFunM'/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.      appSigFunM h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x; -  "appSigFunM'/appTermHomM'" forall (a :: SigFunM Maybe g h) (h :: TermHomM Maybe f g) x.-     appTermHomM' h x >>= appSigFunM' a = appTermHomM' (compSigFunTermHomM' a h) x;+  "appSigFunM'/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;    "appSigFunM'/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.      appSigFunM' h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x; -  "appSigFunM/appTermHom" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM a (appTermHom h x) = appSigFunTermHomM a (sigFunM h) x;+  "appSigFunM/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM a (appHom h x) = appSigFunHomM a (sigFunM h) x;    "appSigFunM/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.-     appSigFunM a (appSigFun h x) = appSigFunTermHomM a (sigFunM $ termHom h) x;+     appSigFunM a (appSigFun h x) = appSigFunHomM a (sigFunM $ hom h) x; -  "appSigFunM'/appTermHom" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM' a (appTermHom h x) = appTermHomM' (compSigFunTermHomM' a (sigFunM h)) x;+  "appSigFunM'/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM' a (appHom h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;    "appSigFunM'/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.      appSigFunM' a (appSigFun h x) = appSigFunM' (compSigFunM a (sigFunM h)) x; -  "appSigFunM/appTermHom'" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM a (appTermHom' h x) = appSigFunTermHomM a (sigFunM h) x;+  "appSigFunM/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM a (appHom' h x) = appSigFunHomM a (sigFunM h) x;    "appSigFunM/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.-     appSigFunM a (appSigFun' h x) = appSigFunTermHomM a (sigFunM $ termHom h) x;+     appSigFunM a (appSigFun' h x) = appSigFunHomM a (sigFunM $ hom h) x; -  "appSigFunM'/appTermHom'" forall (a :: SigFunM m g h) (h :: TermHom f g) x.-     appSigFunM' a (appTermHom' h x) = appTermHomM' (compSigFunTermHomM' a (sigFunM h)) x;+  "appSigFunM'/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.+     appSigFunM' a (appHom' h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;    "appSigFunM'/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.      appSigFunM' a (appSigFun' h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;  -  "appTermHom/appTermHomM" forall (a :: TermHom g h) (h :: TermHomM m f g) x.-     appTermHomM h x >>= (return . appTermHom a) = appTermHomM (compTermHomM_ a h) x;+  "appHom/appHomM" forall (a :: Hom g h) (h :: HomM m f g) x.+     appHomM h x >>= (return . appHom a) = appHomM (compHomM_ a h) x;  #-} #endif

src/Data/Comp/Param/Annotation.hs view

@@ -57,14 +57,14 @@ {-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism  over the same signatures, but extended with annotations. -} propAnn :: (DistAnn f p f', DistAnn g p g', Difunctor g) -        => TermHom f g -> TermHom f' g'+        => Hom f g -> Hom f' g' propAnn hom f' = ann p (hom f)     where (f,p) = projectA f'  {-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic   term homomorphism over the same signatures, but extended with annotations. -} propAnnM :: (DistAnn f p f', DistAnn g p g', Difunctor g, Monad m) -         => TermHomM m f g -> TermHomM m f' g'+         => HomM m f g -> HomM m f' g' propAnnM hom f' = liftM (ann p) (hom f)     where (f,p) = projectA f'

src/Data/Comp/Param/Derive/SmartAConstructors.hs view

@@ -8,7 +8,7 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- Automatically derive smart constructors with annotations.+-- Automatically derive smart constructors with annotations for difunctors. -- -------------------------------------------------------------------------------- @@ -21,13 +21,13 @@ import Data.Comp.Derive.Utils import Data.Comp.Param.Ops import Data.Comp.Param.Term+import Data.Comp.Param.Difunctor  import Control.Monad -{-| Derive smart constructors with products for a type constructor of any-  parametric kind taking at least two arguments. The smart constructors are-  similar to the ordinary constructors, but an 'injectA' is automatically-  inserted. -}+{-| Derive smart constructors with annotations for a difunctor. The smart+ constructors are similar to the ordinary constructors, but a+ 'injectA . dimap Place id' is automatically inserted. -} smartAConstructors :: Name -> Q [Dec] smartAConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname@@ -42,6 +42,6 @@                 let pats = map varP (varPr : varNs)                     vars = map varE varNs                     val = appE [|injectA $(varE varPr)|] $-                          appE [|inj|] $ foldl appE (conE name) vars+                          appE [|inj . dimap Place id|] $ foldl appE (conE name) vars                     function = [funD sname [clause pats (normalB [|Term $val|]) []]]                 sequence function

src/Data/Comp/Param/Derive/SmartConstructors.hs view

@@ -8,7 +8,7 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- Automatically derive smart constructors for parametric types.+-- Automatically derive smart constructors for difunctors. -- -------------------------------------------------------------------------------- @@ -21,11 +21,12 @@ import Data.Comp.Derive.Utils import Data.Comp.Param.Sum import Data.Comp.Param.Term+import Data.Comp.Param.Difunctor import Control.Monad -{-| Derive smart constructors for a type constructor of any parametric kind- taking at least two arguments. The smart constructors are similar to the- ordinary constructors, but an 'inject' is automatically inserted. -}+{-| Derive smart constructors for a difunctor. The smart constructors are+ similar to the ordinary constructors, but a 'inject . dimap Place id' is+ automatically inserted. -} smartConstructors :: Name -> Q [Dec] smartConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname@@ -40,7 +41,7 @@                     vars = map varE varNs                     val = foldl appE (conE name) vars                     sig = genSig targs tname sname args-                    function = [funD sname [clause pats (normalB [|inject $val|]) []]]+                    function = [funD sname [clause pats (normalB [|inject (dimap Place id $val)|]) []]]                 sequence $ sig ++ function               genSig targs tname sname 0 = (:[]) $ do                 hvar <- newName "h"

src/Data/Comp/Param/Desugar.hs view

@@ -20,7 +20,7 @@  -- |The desugaring term homomorphism. class (Difunctor f, Difunctor g) => Desugar f g where-    desugHom :: TermHom f g+    desugHom :: Hom f g     desugHom = desugHom' . fmap Hole     desugHom' :: f a (Cxt h g a b) -> Cxt h g a b     desugHom' x = appCxt (desugHom x)@@ -30,12 +30,12 @@ -- |Desugar a term. desugar :: Desugar f g => Term f -> Term g {-# INLINE desugar #-}-desugar = appTermHom desugHom+desugar = appHom desugHom  -- |Lift desugaring to annotated terms. desugarA :: (Difunctor f', Difunctor g', DistAnn f p f', DistAnn g p g',              Desugar f g) => Term f' -> Term g'-desugarA = appTermHom (propAnn desugHom)+desugarA = appHom (propAnn desugHom)  -- |Default desugaring instance. instance (Difunctor f, Difunctor g, f :<: g) => Desugar f g where

src/Data/Comp/Param/Difunctor.hs view

@@ -16,7 +16,8 @@  module Data.Comp.Param.Difunctor     (-     Difunctor (..)+     Difunctor (..),+     difmap     ) where  -- | This class represents difunctors, i.e. binary type constructors that are@@ -28,5 +29,8 @@ instance Difunctor (->) where     dimap f g h = g . h . f +difmap :: Difunctor f => (a -> b) -> f c a -> f c b+difmap = dimap id+ instance Difunctor f => Functor (f a) where-    fmap = dimap id+    fmap = difmap

src/Data/Comp/Param/Sum.hs view

@@ -159,7 +159,7 @@ {-# INLINE deepInject10 #-}  injectConst :: (Difunctor g, g :<: f) => Const g -> Cxt h f Any a-injectConst = inject . fmap (const undefined)+injectConst = inject . difmap (const undefined)  injectConst2 :: (Difunctor f1, Difunctor f2, Difunctor g, f1 :<: g, f2 :<: g)              => Const (f1 :+: f2) -> Cxt h g Any a@@ -171,11 +171,11 @@ injectConst3 = inject3 . fmap (const undefined)  projectConst :: (Difunctor g, g :<: f) => Cxt h f Any a -> Maybe (Const g)-projectConst = fmap (fmap (const ())) . project+projectConst = fmap (difmap (const ())) . project  {-| This function injects a whole context into another context. -} injectCxt :: (Difunctor g, g :<: f) => Cxt h g a (Cxt h f a b) -> Cxt h f a b-injectCxt (Term t) = inject $ fmap injectCxt t+injectCxt (Term t) = inject $ difmap injectCxt t injectCxt (Hole x) = x injectCxt (Place p) = Place p

src/Data/Comp/Param/Term.hs view

@@ -78,7 +78,7 @@ {-| Convert a difunctorial value into a context. -} simpCxt :: Difunctor f => f a b -> Cxt Hole f a b {-# INLINE simpCxt #-}-simpCxt = Term . fmap Hole+simpCxt = Term . difmap Hole  {-| Cast a \"pseudo-parametric\" context over a signature to a parametric   context over the same signature. The usage of 'unsafeCoerce' is safe, because@@ -98,12 +98,12 @@   argument is indeed a constant, i.e. does not have a value for the   argument type of the difunctor @f@. -} constTerm :: Difunctor f => Const f -> Term f-constTerm = Term . fmap (const undefined)+constTerm = Term . difmap (const undefined)  -- | This is an instance of 'fmap' for 'Cxt'. fmapCxt :: Difunctor f => (b -> b') -> Cxt h f a b -> Cxt h f a b' fmapCxt f = run-    where run (Term t) = Term $ fmap run t+    where run (Term t) = Term $ difmap run t           run (Place a) = Place a           run (Hole b)  = Hole $ f b

src/Data/Comp/TermRewriting.hs view

@@ -33,7 +33,7 @@  {-| This type represents /recursive program schemes/.  -} -type RPS f g  = TermHom f g+type RPS f g  = Hom f g  type Var = Int

+ src/Data/Comp/Zippable.hs view

@@ -0,0 +1,53 @@+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Zippable+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+--+--------------------------------------------------------------------------------++module Data.Comp.Zippable+    ( module Data.Comp.Zippable+    , module Data.Stream ) where++import Data.Stream (Stream(..), (<:>))++-- | Instances of this class provide a generalisation of the zip+-- function on the list functor.+class Functor f => Zippable f where+    fzip :: Stream a -> f b -> f (a,b)+    fzip = fzipWith (\ x y -> (x,y))+    fzipWith :: (a -> b -> c) -> Stream a -> f b -> f c+    fzipWith f s l = fmap (uncurry f) (fzip s l)++-- | This type is used for applying a DDTAs.+newtype Numbered a = Numbered (Int, a)++unNumbered :: Numbered a -> a+unNumbered (Numbered (_, x)) = x++instance Eq (Numbered a) where+    Numbered (i,_) == Numbered (j,_) = i == j++instance Ord (Numbered a) where+    compare (Numbered (i,_))  (Numbered (j,_)) = i `compare` j+++number :: Zippable f => f a -> f (Numbered a)+number t = fzipWith (curry Numbered) (nums 0) t+    where nums x = x `Cons` nums (x+1)++number' :: Zippable f => f a -> f (Int, a)+number' t = fzipWith num (nums 0) t+    where nums x = x <:> nums (x+1)+          num n a = (n,a)++instance Zippable [] where+    fzip (Cons x xs) (y:ys) = (x,y) : fzip xs ys+    fzip _ []  = []+    fzipWith f (Cons x xs) (y:ys) = f x y : fzipWith f xs ys+    fzipWith _ _ [] = []

testsuite/tests/Data/Comp/Examples/MultiParam.hs view

@@ -48,5 +48,5 @@ desugarEvalTest = DesugarEval.evalEx == Just (DesugarEval.iConst (-6)) desugarPosTest = DesugarPos.desugPEx ==                  DesugarPos.iAApp (DesugarPos.Pos 1 0)-                                  (DesugarPos.iALam (DesugarPos.Pos 1 0) $ \x -> DesugarPos.iAMult (DesugarPos.Pos 1 2) (DesugarPos.iAConst (DesugarPos.Pos 1 2) (-1)) (Place x))+                                  (DesugarPos.iALam (DesugarPos.Pos 1 0) $ \x -> DesugarPos.iAMult (DesugarPos.Pos 1 2) (DesugarPos.iAConst (DesugarPos.Pos 1 2) (-1)) x)                                   (DesugarPos.iAConst (DesugarPos.Pos 1 1) 6)

testsuite/tests/Data/Comp/Examples/Param.hs view

@@ -48,11 +48,11 @@ desugarEvalTest = DesugarEval.evalEx == Just (DesugarEval.iConst 720) desugarPosTest = DesugarPos.desugPEx ==                  DesugarPos.iAApp (DesugarPos.Pos 1 0)-                                  (DesugarPos.iALam (DesugarPos.Pos 1 0) Place)+                                  (DesugarPos.iALam (DesugarPos.Pos 1 0) id)                                   (DesugarPos.iALam (DesugarPos.Pos 1 1) $ \f ->                                        DesugarPos.iAApp (DesugarPos.Pos 1 1)                                                         (DesugarPos.iALam (DesugarPos.Pos 1 1) $ \x ->-                                                             DesugarPos.iAApp (DesugarPos.Pos 1 1) (Place f) (DesugarPos.iAApp (DesugarPos.Pos 1 1) (Place x) (Place x)))+                                                             DesugarPos.iAApp (DesugarPos.Pos 1 1) f (DesugarPos.iAApp (DesugarPos.Pos 1 1) x x))                                                         (DesugarPos.iALam (DesugarPos.Pos 1 1) $ \x ->-                                                             DesugarPos.iAApp (DesugarPos.Pos 1 1) (Place f) (DesugarPos.iAApp (DesugarPos.Pos 1 1) (Place x) (Place x))))-parsingTest = Parsing.transEx == (Parsing.iLam $ \a -> Parsing.iApp (Parsing.iLam $ \b -> Parsing.iLam $ \c -> Place b) (Place a))+                                                             DesugarPos.iAApp (DesugarPos.Pos 1 1) f (DesugarPos.iAApp (DesugarPos.Pos 1 1) x x)))+parsingTest = Parsing.transEx == (Parsing.iLam $ \a -> Parsing.iApp (Parsing.iLam $ \b -> Parsing.iLam $ \c -> b) a)