diff --git a/benchmark/Functions/Comp/Desugar.hs b/benchmark/Functions/Comp/Desugar.hs --- a/benchmark/Functions/Comp/Desugar.hs +++ b/benchmark/Functions/Comp/Desugar.hs @@ -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]) diff --git a/benchmark/Functions/Comp/Eval.hs b/benchmark/Functions/Comp/Eval.hs --- a/benchmark/Functions/Comp/Eval.hs +++ b/benchmark/Functions/Comp/Eval.hs @@ -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 diff --git a/benchmark/Functions/Comp/Inference.hs b/benchmark/Functions/Comp/Inference.hs --- a/benchmark/Functions/Comp/Inference.hs +++ b/benchmark/Functions/Comp/Inference.hs @@ -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 diff --git a/benchmark/Multi/Functions/Comp/Desugar.hs b/benchmark/Multi/Functions/Comp/Desugar.hs --- a/benchmark/Multi/Functions/Comp/Desugar.hs +++ b/benchmark/Multi/Functions/Comp/Desugar.hs @@ -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 diff --git a/benchmark/Multi/Functions/Comp/Eval.hs b/benchmark/Multi/Functions/Comp/Eval.hs --- a/benchmark/Multi/Functions/Comp/Eval.hs +++ b/benchmark/Multi/Functions/Comp/Eval.hs @@ -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 diff --git a/compdata.cabal b/compdata.cabal --- a/compdata.cabal +++ b/compdata.cabal @@ -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) diff --git a/examples/Examples/DesugarPos.hs b/examples/Examples/DesugarPos.hs --- a/examples/Examples/DesugarPos.hs +++ b/examples/Examples/DesugarPos.hs @@ -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) diff --git a/examples/Examples/GTermHom.hs b/examples/Examples/GTermHom.hs deleted file mode 100644 --- a/examples/Examples/GTermHom.hs +++ /dev/null @@ -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 --- 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 diff --git a/examples/Examples/Multi/DesugarEval.hs b/examples/Examples/Multi/DesugarEval.hs --- a/examples/Examples/Multi/DesugarEval.hs +++ b/examples/Examples/Multi/DesugarEval.hs @@ -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) diff --git a/examples/Examples/MultiParam/DesugarEval.hs b/examples/Examples/MultiParam/DesugarEval.hs --- a/examples/Examples/MultiParam/DesugarEval.hs +++ b/examples/Examples/MultiParam/DesugarEval.hs @@ -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 diff --git a/examples/Examples/MultiParam/DesugarPos.hs b/examples/Examples/MultiParam/DesugarPos.hs --- a/examples/Examples/MultiParam/DesugarPos.hs +++ b/examples/Examples/MultiParam/DesugarPos.hs @@ -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)) diff --git a/examples/Examples/MultiParam/Eval.hs b/examples/Examples/MultiParam/Eval.hs --- a/examples/Examples/MultiParam/Eval.hs +++ b/examples/Examples/MultiParam/Eval.hs @@ -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 diff --git a/examples/Examples/MultiParam/EvalI.hs b/examples/Examples/MultiParam/EvalI.hs --- a/examples/Examples/MultiParam/EvalI.hs +++ b/examples/Examples/MultiParam/EvalI.hs @@ -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) diff --git a/examples/Examples/MultiParam/EvalM.hs b/examples/Examples/MultiParam/EvalM.hs --- a/examples/Examples/MultiParam/EvalM.hs +++ b/examples/Examples/MultiParam/EvalM.hs @@ -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 diff --git a/examples/Examples/MultiParam/FOL.hs b/examples/Examples/MultiParam/FOL.hs --- a/examples/Examples/MultiParam/FOL.hs +++ b/examples/Examples/MultiParam/FOL.hs @@ -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) diff --git a/examples/Examples/Param/DesugarEval.hs b/examples/Examples/Param/DesugarEval.hs --- a/examples/Examples/Param/DesugarEval.hs +++ b/examples/Examples/Param/DesugarEval.hs @@ -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)) diff --git a/examples/Examples/Param/DesugarPos.hs b/examples/Examples/Param/DesugarPos.hs --- a/examples/Examples/Param/DesugarPos.hs +++ b/examples/Examples/Param/DesugarPos.hs @@ -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') diff --git a/examples/Examples/Param/Eval.hs b/examples/Examples/Param/Eval.hs --- a/examples/Examples/Param/Eval.hs +++ b/examples/Examples/Param/Eval.hs @@ -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 diff --git a/examples/Examples/Param/EvalM.hs b/examples/Examples/Param/EvalM.hs --- a/examples/Examples/Param/EvalM.hs +++ b/examples/Examples/Param/EvalM.hs @@ -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 diff --git a/examples/Examples/Param/Parsing.hs b/examples/Examples/Param/Parsing.hs --- a/examples/Examples/Param/Parsing.hs +++ b/examples/Examples/Param/Parsing.hs @@ -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") diff --git a/src/Data/Comp/Algebra.hs b/src/Data/Comp/Algebra.hs --- a/src/Data/Comp/Algebra.hs +++ b/src/Data/Comp/Algebra.hs @@ -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 diff --git a/src/Data/Comp/Annotation.hs b/src/Data/Comp/Annotation.hs --- a/src/Data/Comp/Annotation.hs +++ b/src/Data/Comp/Annotation.hs @@ -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' diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Automata.hs @@ -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 +-- 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' diff --git a/src/Data/Comp/Automata/Product.hs b/src/Data/Comp/Automata/Product.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Automata/Product.hs @@ -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 +-- 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) diff --git a/src/Data/Comp/Automata/Product/Derive.hs b/src/Data/Comp/Automata/Product/Derive.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Automata/Product/Derive.hs @@ -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 +-- 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 diff --git a/src/Data/Comp/Derive/SmartConstructors.hs b/src/Data/Comp/Derive/SmartConstructors.hs --- a/src/Data/Comp/Derive/SmartConstructors.hs +++ b/src/Data/Comp/Derive/SmartConstructors.hs @@ -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 diff --git a/src/Data/Comp/Desugar.hs b/src/Data/Comp/Desugar.hs --- a/src/Data/Comp/Desugar.hs +++ b/src/Data/Comp/Desugar.hs @@ -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 diff --git a/src/Data/Comp/Generic.hs b/src/Data/Comp/Generic.hs --- a/src/Data/Comp/Generic.hs +++ b/src/Data/Comp/Generic.hs @@ -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 diff --git a/src/Data/Comp/Multi.hs b/src/Data/Comp/Multi.hs --- a/src/Data/Comp/Multi.hs +++ b/src/Data/Comp/Multi.hs @@ -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) diff --git a/src/Data/Comp/Multi/Algebra.hs b/src/Data/Comp/Multi/Algebra.hs --- a/src/Data/Comp/Multi/Algebra.hs +++ b/src/Data/Comp/Multi/Algebra.hs @@ -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 diff --git a/src/Data/Comp/Multi/Annotation.hs b/src/Data/Comp/Multi/Annotation.hs --- a/src/Data/Comp/Multi/Annotation.hs +++ b/src/Data/Comp/Multi/Annotation.hs @@ -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' diff --git a/src/Data/Comp/Multi/Desugar.hs b/src/Data/Comp/Multi/Desugar.hs --- a/src/Data/Comp/Multi/Desugar.hs +++ b/src/Data/Comp/Multi/Desugar.hs @@ -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 diff --git a/src/Data/Comp/Multi/Functor.hs b/src/Data/Comp/Multi/Functor.hs --- a/src/Data/Comp/Multi/Functor.hs +++ b/src/Data/Comp/Multi/Functor.hs @@ -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 diff --git a/src/Data/Comp/Multi/Ops.hs b/src/Data/Comp/Multi/Ops.hs --- a/src/Data/Comp/Multi/Ops.hs +++ b/src/Data/Comp/Multi/Ops.hs @@ -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 diff --git a/src/Data/Comp/MultiParam/Algebra.hs b/src/Data/Comp/MultiParam/Algebra.hs --- a/src/Data/Comp/MultiParam/Algebra.hs +++ b/src/Data/Comp/MultiParam/Algebra.hs @@ -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 diff --git a/src/Data/Comp/MultiParam/Annotation.hs b/src/Data/Comp/MultiParam/Annotation.hs --- a/src/Data/Comp/MultiParam/Annotation.hs +++ b/src/Data/Comp/MultiParam/Annotation.hs @@ -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' diff --git a/src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs b/src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs --- a/src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs +++ b/src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs @@ -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 diff --git a/src/Data/Comp/MultiParam/Derive/SmartConstructors.hs b/src/Data/Comp/MultiParam/Derive/SmartConstructors.hs --- a/src/Data/Comp/MultiParam/Derive/SmartConstructors.hs +++ b/src/Data/Comp/MultiParam/Derive/SmartConstructors.hs @@ -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" diff --git a/src/Data/Comp/MultiParam/Desugar.hs b/src/Data/Comp/MultiParam/Desugar.hs --- a/src/Data/Comp/MultiParam/Desugar.hs +++ b/src/Data/Comp/MultiParam/Desugar.hs @@ -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 diff --git a/src/Data/Comp/MultiParam/HDifunctor.hs b/src/Data/Comp/MultiParam/HDifunctor.hs --- a/src/Data/Comp/MultiParam/HDifunctor.hs +++ b/src/Data/Comp/MultiParam/HDifunctor.hs @@ -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) diff --git a/src/Data/Comp/Param/Algebra.hs b/src/Data/Comp/Param/Algebra.hs --- a/src/Data/Comp/Param/Algebra.hs +++ b/src/Data/Comp/Param/Algebra.hs @@ -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 diff --git a/src/Data/Comp/Param/Annotation.hs b/src/Data/Comp/Param/Annotation.hs --- a/src/Data/Comp/Param/Annotation.hs +++ b/src/Data/Comp/Param/Annotation.hs @@ -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' diff --git a/src/Data/Comp/Param/Derive/SmartAConstructors.hs b/src/Data/Comp/Param/Derive/SmartAConstructors.hs --- a/src/Data/Comp/Param/Derive/SmartAConstructors.hs +++ b/src/Data/Comp/Param/Derive/SmartAConstructors.hs @@ -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 diff --git a/src/Data/Comp/Param/Derive/SmartConstructors.hs b/src/Data/Comp/Param/Derive/SmartConstructors.hs --- a/src/Data/Comp/Param/Derive/SmartConstructors.hs +++ b/src/Data/Comp/Param/Derive/SmartConstructors.hs @@ -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" diff --git a/src/Data/Comp/Param/Desugar.hs b/src/Data/Comp/Param/Desugar.hs --- a/src/Data/Comp/Param/Desugar.hs +++ b/src/Data/Comp/Param/Desugar.hs @@ -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 diff --git a/src/Data/Comp/Param/Difunctor.hs b/src/Data/Comp/Param/Difunctor.hs --- a/src/Data/Comp/Param/Difunctor.hs +++ b/src/Data/Comp/Param/Difunctor.hs @@ -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 diff --git a/src/Data/Comp/Param/Sum.hs b/src/Data/Comp/Param/Sum.hs --- a/src/Data/Comp/Param/Sum.hs +++ b/src/Data/Comp/Param/Sum.hs @@ -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 diff --git a/src/Data/Comp/Param/Term.hs b/src/Data/Comp/Param/Term.hs --- a/src/Data/Comp/Param/Term.hs +++ b/src/Data/Comp/Param/Term.hs @@ -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 diff --git a/src/Data/Comp/TermRewriting.hs b/src/Data/Comp/TermRewriting.hs --- a/src/Data/Comp/TermRewriting.hs +++ b/src/Data/Comp/TermRewriting.hs @@ -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 diff --git a/src/Data/Comp/Zippable.hs b/src/Data/Comp/Zippable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Zippable.hs @@ -0,0 +1,53 @@ +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.Zippable +-- Copyright : (c) 2011 Patrick Bahr +-- License : BSD3 +-- Maintainer : Patrick Bahr +-- 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 _ _ [] = [] diff --git a/testsuite/tests/Data/Comp/Examples/MultiParam.hs b/testsuite/tests/Data/Comp/Examples/MultiParam.hs --- a/testsuite/tests/Data/Comp/Examples/MultiParam.hs +++ b/testsuite/tests/Data/Comp/Examples/MultiParam.hs @@ -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) diff --git a/testsuite/tests/Data/Comp/Examples/Param.hs b/testsuite/tests/Data/Comp/Examples/Param.hs --- a/testsuite/tests/Data/Comp/Examples/Param.hs +++ b/testsuite/tests/Data/Comp/Examples/Param.hs @@ -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)