packages feed

compdata-param (empty) → 0.8

raw patch · 59 files changed

+5934/−0 lines, 59 filesdep +HUnitdep +basedep +compdatasetup-changed

Dependencies added: HUnit, base, compdata, compdata-param, containers, mtl, template-haskell, test-framework, test-framework-hunit, transformers

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2010--2011 Patrick Bahr, Tom Hvitved++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ compdata-param.cabal view
@@ -0,0 +1,105 @@+Name:			compdata-param+Version:		0.8+Synopsis:            	Parametric Compositional Data Types+Description:++  Based on Wouter Swierstra's Functional Pearl /Data types a la carte/+  (Journal of Functional Programming, 18(4):423-436, 2008,+  <http://dx.doi.org/10.1017/S0956796808006758>), this package+  provides a framework for defining recursive data types in a+  compositional manner with support for binders. +  .+  This package implemements /parametric compositional data types/+  (Workshop on Mathematically Structured Functional Programming, 3-24,+  2012, <http://dx.doi.org/10.4204/EPTCS.76.3>), generalising+  compositional data types (as implemented in the /compdata/ package)+  with support for parametric higher-order abstract syntax+  (PHOAS).+  .+  Examples of using parametric compositional data types are bundled+  with the package in the folder @examples@.++Category:            	Generics+License:		BSD3+License-file:		LICENSE+Author:			Patrick Bahr, Tom Hvitved+Maintainer:		paba@di.ku.dk+Build-Type:		Simple+Cabal-Version:          >=1.9.2++extra-source-files:+  -- test files+  testsuite/tests/Tests.hs+  testsuite/tests/Data/Comp/Examples_Test.hs+  testsuite/tests/Data/Comp/Examples/*.hs+  -- example files+  examples/Examples/*.hs+  examples/Examples/Multi/*.hs+++library+  Exposed-Modules:      Data.Comp.Param+                        Data.Comp.Param.Term+                        Data.Comp.Param.FreshM+                        Data.Comp.Param.Sum+                        Data.Comp.Param.Difunctor+                        Data.Comp.Param.Ditraversable+                        Data.Comp.Param.Algebra+                        Data.Comp.Param.Annotation+                        Data.Comp.Param.Ops+                        Data.Comp.Param.Equality+                        Data.Comp.Param.Ordering+                        Data.Comp.Param.Show+                        Data.Comp.Param.Derive,+                        Data.Comp.Param.Desugar+                        Data.Comp.Param.Thunk++                        Data.Comp.Param.Multi+                        Data.Comp.Param.Multi.Term+                        Data.Comp.Param.Multi.FreshM+                        Data.Comp.Param.Multi.Sum+                        Data.Comp.Param.Multi.HDifunctor+                        Data.Comp.Param.Multi.HDitraversable+                        Data.Comp.Param.Multi.Algebra+                        Data.Comp.Param.Multi.Annotation+                        Data.Comp.Param.Multi.Ops+                        Data.Comp.Param.Multi.Equality+                        Data.Comp.Param.Multi.Ordering+                        Data.Comp.Param.Multi.Show+                        Data.Comp.Param.Multi.Derive,+                        Data.Comp.Param.Multi.Desugar++  Other-Modules:        Data.Comp.Param.Derive.Difunctor+                        Data.Comp.Param.Derive.Ditraversable+                        Data.Comp.Param.Derive.Equality+                        Data.Comp.Param.Derive.Ordering+                        Data.Comp.Param.Derive.Show+                        Data.Comp.Param.Derive.SmartConstructors+                        Data.Comp.Param.Derive.SmartAConstructors+                        Data.Comp.Param.Derive.Injections+                        Data.Comp.Param.Derive.Projections++                        Data.Comp.Param.Multi.Derive.HDifunctor+                        Data.Comp.Param.Multi.Derive.Equality+                        Data.Comp.Param.Multi.Derive.Ordering+                        Data.Comp.Param.Multi.Derive.Show+                        Data.Comp.Param.Multi.Derive.SmartConstructors+                        Data.Comp.Param.Multi.Derive.SmartAConstructors+                        Data.Comp.Param.Multi.Derive.Injections+                        Data.Comp.Param.Multi.Derive.Projections++  Build-Depends:	base == 4.*, template-haskell, mtl, transformers, compdata == 0.8.*+  hs-source-dirs:	src+  ghc-options:          -W+++Test-Suite test+  Type:                 exitcode-stdio-1.0+  Main-is:		Tests.hs+  hs-source-dirs:	testsuite/tests examples+  Build-Depends:        base == 4.*, template-haskell, mtl, transformers, compdata == 0.8.*, HUnit,+                        test-framework, test-framework-hunit, containers, compdata-param++source-repository head+  type:     hg+  location: https://bitbucket.org/paba/compdata-param
+ examples/Examples/Graph.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, TemplateHaskell,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Param.Graph+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Graph representation. The example is taken from (Fegaras and Sheard,+-- Revisiting Catamorphisms over Datatypes with Embedded Functions, '96).+--+--------------------------------------------------------------------------------++module Examples.Graph where++import Data.Comp.Param+import Data.Comp.Param.Derive+import Data.Comp.Param.Show ()+import Data.Comp.Param.Equality ()++data N p a b = N p [b] -- Node+data R a b = R (a -> b) -- Recursion+data S a b = S (a -> b) b -- Sharing++$(derive [makeDifunctor, makeShowD, makeEqD, makeOrdD, smartConstructors]+         [''N, ''R, ''S])+$(derive [makeDitraversable] [''N])++type Graph p = Term (N p :+: R :+: S)++class FlatG f p where+  flatGAlg :: Alg f [p]++$(derive [liftSum] [''FlatG])++flatG :: (Difunctor f, FlatG f p) => Term f -> [p]+flatG = cata flatGAlg++instance FlatG (N p) p where+  flatGAlg (N p ps) = p : concat ps++instance FlatG R p where+  flatGAlg (R f) = f []++instance FlatG S p where+  flatGAlg (S f g) = f g++class SumG f where+  sumGAlg :: Alg f Int++$(derive [liftSum] [''SumG])++sumG :: (Difunctor f, SumG f) => Term f -> Int+sumG = cata sumGAlg++instance SumG (N Int) where+  sumGAlg (N p ps) = p + sum ps++instance SumG R where+  sumGAlg (R f) = f 0++instance SumG S where+  sumGAlg (S f g) = f g++g :: Graph Int+g = Term $ iR (\x -> iS (\z -> iN (0 :: Int) [z,iR $ \y -> iN (1 :: Int) [y,z]])+                        (iN (2 :: Int) [x]))++f :: [Int]+f = flatG g++n :: Int+n = sumG g
+ examples/Examples/Lambda.hs view
@@ -0,0 +1,131 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances, Rank2Types, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Param.Lambda+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Lambda calculus examples+--+-- We define a pretty printer, a desugaring transformation, constant folding,+-- and call-by-value interpreter for an extended variant of the simply typed+-- lambda calculus.+--+--------------------------------------------------------------------------------++module Examples.Lambda where++import Data.Comp.Param+import Data.Comp.Param.Show ()+import Data.Comp.Param.Equality ()+import Data.Comp.Param.Ordering ()+import Data.Comp.Param.Derive+import Data.Comp.Param.Desugar++data Lam a b   = Lam (a -> b)+data App a b   = App b b+data Const a b = Const Int+data Plus a b  = Plus b b+data Let a b   = Let b (a -> b)+data Err a b   = Err++type Sig       = Lam :+: App :+: Const :+: Plus :+: Let :+: Err+type Sig'      = Lam :+: App :+: Const :+: Plus :+: Err++$(derive [smartConstructors, makeDifunctor, makeShowD, makeEqD, makeOrdD]+         [''Lam, ''App, ''Const, ''Plus, ''Let, ''Err])++-- * Pretty printing+data Stream a = Cons a (Stream a)++class Pretty f where+  prettyAlg :: Alg f (Stream String -> String)++$(derive [liftSum] [''Pretty])++pretty :: (Difunctor f, Pretty f) => Term f -> String+pretty t = cata prettyAlg t (nominals 1)+    where nominals n = Cons ('x' : show n) (nominals (n + 1))++instance Pretty Lam where+  prettyAlg (Lam f) (Cons x xs) = "(\\" ++ x ++ ". " ++ f (const x) xs ++ ")"++instance Pretty App where+  prettyAlg (App e1 e2) xs = "(" ++ e1 xs ++ " " ++ e2 xs ++ ")"++instance Pretty Const where+  prettyAlg (Const n) _ = show n++instance Pretty Plus where+  prettyAlg (Plus e1 e2) xs = "(" ++ e1 xs ++ " + " ++ e2 xs ++ ")"++instance Pretty Err where+  prettyAlg Err _ = "error"++instance Pretty Let where+  prettyAlg (Let e1 e2) (Cons x xs) = "let " ++ x ++ " = " ++ e1 xs ++ " in " ++ e2 (const x) xs++-- * Desugaring+instance (Difunctor f, App :<: f, Lam :<: f) => Desugar Let f where+  desugHom' (Let e1 e2) = inject (Lam e2) `iApp` e1++-- * Constant folding+class Constf f g where+  constfAlg :: forall a. Alg f (Trm g a)++$(derive [liftSum] [''Constf])++constf :: (Difunctor f, Constf f g) => Term f -> Term g+constf t = Term (cata constfAlg t)++instance (Difunctor f, f :<: g) => Constf f g where+  constfAlg = inject . dimap Var id -- default instance++instance (Plus :<: f, Const :<: f) => Constf Plus f where+  constfAlg (Plus e1 e2) = case (project e1, project e2) of+                             (Just (Const n),Just (Const m)) -> iConst (n + m)+                             _                               -> e1 `iPlus` e2++-- * Call-by-value evaluation+data Sem m = Fun (Sem m -> m (Sem m)) | Int Int++class Monad m => Eval f m where+  evalAlg :: Alg f (m (Sem m))++$(derive [liftSum] [''Eval])++eval :: (Difunctor f, Eval f m) => Term f -> m (Sem m)+eval = cata evalAlg++instance Monad m => Eval Lam m where+  evalAlg (Lam f) = return (Fun (f . return))++instance Monad m => Eval App m where+  evalAlg (App mx my) = do x <- mx+                           case x of Fun f -> f =<< my; _ -> fail "stuck"++instance Monad m => Eval Const m where+  evalAlg (Const n) = return (Int n)++instance Monad m => Eval Plus m where+  evalAlg (Plus mx my) = do x <- mx+                            y <- my+                            case (x,y) of (Int n,Int m) -> return (Int (n + m))+                                          _             -> fail "stuck"++instance Monad m => Eval Err m where+  evalAlg Err = fail "error"++e :: Term Sig+e = Term (iLet (iConst 2) (\x -> (iLam (\y -> y `iPlus` x) `iApp` iConst 3)))++e' :: Term Sig'+e' = desugar e++evalEx :: Maybe (Sem Maybe)+evalEx = eval e'
+ examples/Examples/Multi/FOL.hs view
@@ -0,0 +1,436 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, FlexibleInstances,+  FlexibleContexts, UndecidableInstances, GADTs, KindSignatures,+  OverlappingInstances, TypeSynonymInstances, EmptyDataDecls #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.MultiParam.FOL+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- First-Order Logic a la Carte+--+-- This example illustrates how to implement First-Order Logic a la Carte+-- (Knowles, The Monad.Reader Issue 11, '08) using Generalised Parametric+-- Compositional Data Types.+--+-- Rather than using a fixed domain 'Term' for binders as Knowles, our encoding+-- uses a mutually recursive data structure for terms and formulae. This makes+-- terms modular too, and hence we only introduce variables when they are+-- actually needed in stage 5.+--+--------------------------------------------------------------------------------++module Examples.Multi.FOL where++import Data.Comp.Param.Multi hiding (Var)+import qualified Data.Comp.Param.Multi as MP+import Data.Comp.Param.Multi.Show ()+import Data.Comp.Param.Multi.Derive+import Data.Comp.Param.Multi.FreshM (Name, withName, evalFreshM)+import Data.List (intercalate)+import Data.Maybe+import Control.Monad.State+import Control.Monad.Reader++-- Phantom types indicating whether a (recursive) term is a formula or a term+data TFormula+data TTerm++-- Terms+data Const :: (* -> *) -> (* -> *) -> * -> * where+    Const :: String -> [e TTerm] -> Const a e TTerm+data Var :: (* -> *) -> (* -> *) -> * -> * where+    Var :: String -> Var a e TTerm++-- Formulae+data TT :: (* -> *) -> (* -> *) -> * -> * where+    TT :: TT a e TFormula+data FF :: (* -> *) -> (* -> *) -> * -> * where+    FF :: FF a e TFormula+data Atom :: (* -> *) -> (* -> *) -> * -> * where+    Atom :: String -> [e TTerm] -> Atom a e TFormula+data NAtom :: (* -> *) -> (* -> *) -> * -> * where+    NAtom :: String -> [e TTerm] -> NAtom a e TFormula+data Not :: (* -> *) -> (* -> *) -> * -> * where+    Not :: e TFormula -> Not a e TFormula+data Or :: (* -> *) -> (* -> *) -> * -> * where+    Or :: e TFormula -> e TFormula -> Or a e TFormula+data And :: (* -> *) -> (* -> *) -> * -> * where+    And :: e TFormula -> e TFormula -> And a e TFormula+data Impl :: (* -> *) -> (* -> *) -> * -> * where+    Impl :: e TFormula -> e TFormula -> Impl a e TFormula+data Exists :: (* -> *) -> (* -> *) -> * -> * where+    Exists :: (a TTerm -> e TFormula) -> Exists a e TFormula+data Forall :: (* -> *) -> (* -> *) -> * -> * where+    Forall :: (a TTerm -> e TFormula) -> Forall a e TFormula++$(derive [makeHDifunctor, smartConstructors]+         [''Const, ''Var, ''TT, ''FF, ''Atom, ''NAtom,+          ''Not, ''Or, ''And, ''Impl, ''Exists, ''Forall])++--------------------------------------------------------------------------------+-- (Custom) pretty printing of terms and formulae+--------------------------------------------------------------------------------++instance ShowHD Const where+  showHD (Const f t) = do ts <- mapM unK t+                          return $ f ++ "(" ++ intercalate ", " ts ++ ")"++instance ShowHD Var where+  showHD (Var x) = return x++instance ShowHD TT where+  showHD TT = return "true"++instance ShowHD FF where+  showHD FF = return "false"++instance ShowHD Atom where+  showHD (Atom p t) = do ts <- mapM unK t+                         return $ p ++ "(" ++ intercalate ", " ts ++ ")"++instance ShowHD NAtom where+  showHD (NAtom p t) = do ts <- mapM unK t+                          return $ "not " ++ p ++ "(" ++ intercalate ", " ts ++ ")"++instance ShowHD Not where+  showHD (Not (K f)) = liftM (\x -> "not (" ++ x ++ ")") f++instance ShowHD Or where+  showHD (Or (K f1) (K f2)) =+      liftM2 (\x y -> "(" ++ x ++ ") or (" ++ y ++ ")") f1 f2++instance ShowHD And where+  showHD (And (K f1) (K f2)) =+      liftM2 (\x y -> "(" ++ x ++ ") and (" ++ y ++ ")") f1 f2++instance ShowHD Impl where+  showHD (Impl (K f1) (K f2)) =+      liftM2 (\x y -> "(" ++ x ++ ") -> (" ++ y ++ ")") f1 f2++instance ShowHD Exists where+  showHD (Exists f) =+      withName (\x -> do b <- unK (f x)+                         return $ "exists " ++ show x ++ ". " ++ b)++instance ShowHD Forall where+  showHD (Forall f) =+      withName (\x -> do b <- unK (f x)+                         return $ "forall " ++ show x ++ ". " ++ b)++--------------------------------------------------------------------------------+-- Stage 0+--------------------------------------------------------------------------------++type Input = Const :+:+             TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Impl :+:+             Exists :+: Forall++foodFact :: Term Input TFormula+foodFact = Term $+  iExists (\p -> iAtom "Person" [p] `iAnd`+                 iForall (\f -> iAtom "Food" [f] `iImpl`+                                iAtom "Eats" [p,f])) `iImpl`+  iNot (iExists $ \f -> iAtom "Food" [f] `iAnd`+                        iNot (iExists $ \p -> iAtom "Person" [p] `iAnd`+                                              iAtom "Eats" [p,f]))++--------------------------------------------------------------------------------+-- Stage 1: Eliminate Implications+--------------------------------------------------------------------------------++type Stage1 = Const :+:+              TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Exists :+: Forall++class HDifunctor f => ElimImp f where+  elimImpHom :: Hom f Stage1++$(derive [liftSum] [''ElimImp])++elimImp :: Term Input :-> Term Stage1+elimImp (Term t) = Term (appHom elimImpHom t)++instance (HDifunctor f, f :<: Stage1) => ElimImp f where+  elimImpHom = simpCxt . inj++instance ElimImp Impl where+  elimImpHom (Impl f1 f2) = iNot (Hole f1) `iOr` (Hole f2)++foodFact1 :: Term Stage1 TFormula+foodFact1 = elimImp foodFact++--------------------------------------------------------------------------------+-- Stage 2: Move Negation Inwards+--------------------------------------------------------------------------------++type Stage2 = Const :+:+              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Exists :+: Forall++class HDifunctor f => Dualize f where+  dualizeHom :: f a (Cxt h Stage2 a b) :-> Cxt h Stage2 a b++$(derive [liftSum] [''Dualize])++dualize :: Trm Stage2 a :-> Trm Stage2 a+dualize = appHom (dualizeHom . hfmap Hole)++instance Dualize Const where+  dualizeHom (Const f t) = iConst f t++instance Dualize TT where+  dualizeHom TT = iFF++instance Dualize FF where+  dualizeHom FF = iTT++instance Dualize Atom where+  dualizeHom (Atom p t) = iNAtom p t++instance Dualize NAtom where+  dualizeHom (NAtom p t) = iAtom p t++instance Dualize Or where+  dualizeHom (Or f1 f2) = f1 `iAnd` f2++instance Dualize And where+  dualizeHom (And f1 f2) = f1 `iOr` f2++instance Dualize Exists where+  dualizeHom (Exists f) = inject $ Forall f++instance Dualize Forall where+  dualizeHom (Forall f) = inject $ Exists f++class PushNot f where+  pushNotAlg :: Alg f (Trm Stage2 a)++$(derive [liftSum] [''PushNot])++pushNotInwards :: Term Stage1 :-> Term Stage2+pushNotInwards t = Term (cata pushNotAlg t)++instance (HDifunctor f, f :<: Stage2) => PushNot f where+  pushNotAlg = inject . hdimap MP.Var id -- default++instance PushNot Not where+  pushNotAlg (Not f) = dualize f++foodFact2 :: Term Stage2 TFormula+foodFact2 = pushNotInwards foodFact1++--------------------------------------------------------------------------------+-- Stage 4: Skolemization+--------------------------------------------------------------------------------++type Stage4 = Const :+:+              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Forall++type Unique = Int+data UniqueSupply = UniqueSupply Unique UniqueSupply UniqueSupply++initialUniqueSupply :: UniqueSupply+initialUniqueSupply = genSupply 1+    where genSupply n = UniqueSupply n (genSupply (2 * n))+                                       (genSupply (2 * n + 1))++splitUniqueSupply :: UniqueSupply -> (UniqueSupply, UniqueSupply)+splitUniqueSupply (UniqueSupply	_ l r) = (l,r)++getUnique :: UniqueSupply -> (Unique, UniqueSupply)+getUnique (UniqueSupply n l _) = (n,l)++type Supply = State UniqueSupply+type S a = ReaderT [Trm Stage4 a TTerm] Supply++evalS :: S a b -> [Trm Stage4 a TTerm] -> UniqueSupply -> b+evalS m env = evalState (runReaderT m env)++fresh :: S a Int+fresh = do supply <- get+           let (uniq,rest) = getUnique supply+           put rest+           return uniq++freshes :: S a UniqueSupply+freshes = do supply <- get+             let (l,r) = splitUniqueSupply supply+             put r+             return l++class Skolem f where+  skolemAlg :: AlgM' (S a) f (Trm Stage4 a)++$(derive [liftSum] [''Skolem])++skolemize :: Term Stage2 :-> Term Stage4+skolemize f = Term (evalState (runReaderT (cataM' skolemAlg f) [])+                              initialUniqueSupply)++instance Skolem Const where+  skolemAlg (Const f t) = liftM (iConst f) $ mapM getCompose t++instance Skolem TT where+  skolemAlg TT = return iTT++instance Skolem FF where+  skolemAlg FF = return iFF++instance Skolem Atom where+  skolemAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t++instance Skolem NAtom where+  skolemAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t++instance Skolem Or where+  skolemAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2++instance Skolem And where+  skolemAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2++instance Skolem Forall where+  skolemAlg (Forall f) = do+    supply <- freshes+    xs <- ask+    return $ iForall $ \x -> evalS (getCompose $ f x) (x : xs) supply++instance Skolem Exists where+  skolemAlg (Exists f) = do+    uniq <- fresh+    xs <- ask+    getCompose $ f (iConst ("Skol" ++ show uniq) xs)++foodFact4 :: Term Stage4 TFormula+foodFact4 = skolemize foodFact2++--------------------------------------------------------------------------------+-- Stage 5: Prenex Normal Form+--------------------------------------------------------------------------------++type Stage5 = Const :+: Var :+:+              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And++class Prenex f where+  prenexAlg :: AlgM' (S a) f (Trm Stage5 a)++$(derive [liftSum] [''Prenex])++prenex :: Term Stage4 :-> Term Stage5+prenex f = Term (evalState (runReaderT (cataM' prenexAlg f) [])+                           initialUniqueSupply)++instance Prenex Const where+  prenexAlg (Const f t) = liftM (iConst f) $ mapM getCompose t++instance Prenex TT where+  prenexAlg TT = return iTT++instance Prenex FF where+  prenexAlg FF = return iFF++instance Prenex Atom where+  prenexAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t++instance Prenex NAtom where+  prenexAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t++instance Prenex Or where+  prenexAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2++instance Prenex And where+  prenexAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2++instance Prenex Forall where+  prenexAlg (Forall f) = do uniq <- fresh+                            getCompose $ f (iVar ('x' : show uniq))++foodFact5 :: Term Stage5 TFormula+foodFact5 = prenex foodFact4++--------------------------------------------------------------------------------+-- Stage 6: Conjunctive Normal Form+--------------------------------------------------------------------------------++type Literal a     = Trm (Const :+: Var :+: Atom :+: NAtom) a+newtype Clause a i = Clause {unClause :: [Literal a i]} -- implicit disjunction+newtype CNF a i    = CNF {unCNF :: [Clause a i]}        -- implicit conjunction++instance (HDifunctor f, ShowHD f) => Show (Trm f Name i) where+  show = evalFreshM . showHD . toCxt++instance Show (Clause Name i) where+  show c = intercalate " or " $ map show $ unClause c++instance Show (CNF Name i) where+  show c = intercalate "\n" $ map show $ unCNF c++class ToCNF f where+  cnfAlg :: f (CNF a) (CNF a) i -> [Clause a i]++$(derive [liftSum] [''ToCNF])++cnf :: Term Stage5 :-> CNF a+cnf = cata (CNF . cnfAlg)++instance ToCNF Const where+  cnfAlg (Const f t) =+      [Clause [iConst f (map (head . unClause . head . unCNF) t)]]++instance ToCNF Var where+  cnfAlg (Var x) = [Clause [iVar x]]++instance ToCNF TT where+  cnfAlg TT = []++instance ToCNF FF where+  cnfAlg FF = [Clause []]++instance ToCNF Atom where+  cnfAlg (Atom p t) =+      [Clause [iAtom p (map (head . unClause . head . unCNF) t)]]++instance ToCNF NAtom where+  cnfAlg (NAtom p t) =+      [Clause [iNAtom p (map (head . unClause . head . unCNF) t)]]++instance ToCNF And where+  cnfAlg (And f1 f2) = unCNF f1 ++ unCNF f2++instance ToCNF Or where+  cnfAlg (Or f1 f2) =+      [Clause (x ++ y) | Clause x <- unCNF f1, Clause y <- unCNF f2]++foodFact6 :: CNF a TFormula+foodFact6 = cnf foodFact5++--------------------------------------------------------------------------------+-- Stage 7: Implicative Normal Form+--------------------------------------------------------------------------------++type T              = Const :+: Var :+: Atom :+: NAtom+newtype IClause a i = IClause ([Trm T a i], -- implicit conjunction+                               [Trm T a i]) -- implicit disjunction+newtype INF a i     = INF [IClause a i]     -- implicit conjunction++instance Show (IClause Name i) where+  show (IClause (cs,ds)) = let cs' = intercalate " and " $ map show cs+                               ds' = intercalate " or " $ map show ds+                           in "(" ++ cs' ++ ") -> (" ++ ds' ++ ")"++instance Show (INF Name i) where+  show (INF fs) = intercalate "\n" $ map show fs++inf :: CNF a TFormula -> INF a TFormula+inf (CNF f) = INF $ map (toImpl . unClause) f+    where toImpl :: [Literal a TFormula] -> IClause a TFormula+          toImpl disj = IClause ([iAtom p t | NAtom p t <- mapMaybe proj1 disj],+                                 [inject t | t <- mapMaybe proj2 disj])+          proj1 :: NatM Maybe (Trm T a) (NAtom a (Trm T a))+          proj1 = project+          proj2 :: NatM Maybe (Trm T a) (Atom a (Trm T a))+          proj2 = project++foodFact7 :: INF a TFormula+foodFact7 = inf foodFact6
+ examples/Examples/Multi/Lambda.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances, Rank2Types, GADTs, KindSignatures,+  ScopedTypeVariables, TypeFamilies #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.MultiParam.Lambda+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Tagless (monadic) interpretation of extended lambda calculus+--+--------------------------------------------------------------------------------++module Examples.Multi.Lambda where++import Data.Comp.Param.Multi+import Data.Comp.Param.Multi.Show ()+import Data.Comp.Param.Multi.Equality ()+import Data.Comp.Param.Multi.Derive+import Control.Monad (liftM2)+import Control.Monad.Error (MonadError, throwError)++data Lam :: (* -> *) -> (* -> *) -> * -> * where+  Lam :: (a i -> b j) -> Lam a b (i -> j)+data App :: (* -> *) -> (* -> *) -> * -> * where+  App :: b (i -> j) -> b i -> App a b j+data Const :: (* -> *) -> (* -> *) -> * -> * where+  Const :: Int -> Const a b Int+data Plus :: (* -> *) -> (* -> *) -> * -> * where+  Plus :: b Int -> b Int -> Plus a b Int+data Err :: (* -> *) -> (* -> *) -> * -> * where+  Err :: Err a b i+type Sig = Lam :+: App :+: Const :+: Plus :+: Err++$(derive [smartConstructors, makeHDifunctor, makeShowHD, makeEqHD]+         [''Lam, ''App, ''Const, ''Plus, ''Err])++-- * Tagless interpretation+class Eval f where+  evalAlg :: f I I i -> i -- I . evalAlg :: Alg f I is the actual algebra++$(derive [liftSum] [''Eval])++eval :: (HDifunctor f, Eval f) => Term f i -> i+eval = unI . cata (I . evalAlg)++instance Eval Lam where+  evalAlg (Lam f) = unI . f . I++instance Eval App where+  evalAlg (App (I f) (I x)) = f x++instance Eval Const where+  evalAlg (Const n) = n++instance Eval Plus where+  evalAlg (Plus (I x) (I y)) = x + y++instance Eval Err where+  evalAlg Err = error "error"++-- * Tagless monadic interpretation+type family Sem (m :: * -> *) i+type instance Sem m (i -> j) = Sem m i -> m (Sem m j)+type instance Sem m Int = Int++newtype M m i = M {unM :: m (Sem m i)}++class Monad m => EvalM m f where+  evalMAlg :: f (M m) (M m) i -> m (Sem m i) -- M . evalMAlg :: Alg f (M m)++$(derive [liftSum] [''EvalM])++evalM :: (Monad m, HDifunctor f, EvalM m f) => Term f i -> m (Sem m i)+evalM = unM . cata (M . evalMAlg)++instance Monad m => EvalM m Lam where+  evalMAlg (Lam f) = return $ unM . f . M . return++instance Monad m => EvalM m App where+  evalMAlg (App (M mf) (M mx)) = do f <- mf; f =<< mx+  +instance Monad m => EvalM m Const where+  evalMAlg (Const n) = return n++instance Monad m => EvalM m Plus where+  evalMAlg (Plus (M mx) (M my)) = liftM2 (+) mx my++instance MonadError String m => EvalM m Err where+  evalMAlg Err = throwError "error" -- 'throwError' rather than 'error'++e :: Term Sig Int+e = Term ((iLam $ \x -> (iLam (\y -> y `iPlus` x) `iApp` iConst 3)) `iApp` iConst 2)++v :: Either String Int+v = evalM e++e' :: Term Sig (Int -> Int)+e' = Term iErr --(iLam id)++v' :: Either String (Int -> Either String Int)+v' = evalM e'
+ examples/Examples/Names.hs view
@@ -0,0 +1,113 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Param.Names+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- From names to parametric higher-order abstract syntax and back+--+-- The example illustrates how to convert a parse tree with explicit names into+-- an AST that uses parametric higher-order abstract syntax, and back again. The+-- example shows how we can easily convert object language binders to Haskell+-- binders, without having to worry about capture avoidance.+--+--------------------------------------------------------------------------------++module Examples.Names where++import Data.Comp.Param hiding (Var)+import qualified Data.Comp.Param as P+import Data.Comp.Param.Derive+import Data.Comp.Param.Ditraversable+import Data.Comp.Param.Show ()+import Data.Maybe+import qualified Data.Map as Map+import Control.Monad.Reader++data Lam a b  = Lam (a -> b)+data App a b  = App b b+data Lit a b  = Lit Int+data Plus a b = Plus b b+type Name     = String                 -- The type of names+data NLam a b = NLam Name b+data NVar a b = NVar Name+type SigB     = App :+: Lit :+: Plus+type SigN     = NLam :+: NVar :+: SigB -- The name signature+type SigP     = Lam :+: SigB           -- The PHOAS signature++$(derive [makeDifunctor, makeShowD, makeEqD, smartConstructors]+         [''Lam, ''App, ''Lit, ''Plus, ''NLam, ''NVar])+$(derive [makeDitraversable]+         [''App, ''Lit, ''Plus, ''NLam, ''NVar])++--------------------------------------------------------------------------------+-- Names to PHOAS translation+--------------------------------------------------------------------------------++type M f a = Reader (Map.Map Name (Trm f a))++class N2PTrans f g where+  n2pAlg :: Alg f (M g a (Trm g a))+++-- We make the lifting to sums explicit in order to make the N2PTrans+-- work with the default instance declaration further below.+instance (N2PTrans f1 g, N2PTrans f2 g) => N2PTrans (f1 :+: f2) g where+    n2pAlg = caseD n2pAlg n2pAlg++n2p :: (Difunctor f, N2PTrans f g) => Term f -> Term g+n2p t = Term $ runReader (cata n2pAlg t) Map.empty++instance (Lam :<: g) => N2PTrans NLam g where+  n2pAlg (NLam x b) = do vars <- ask+                         return $ iLam $ \y -> runReader b (Map.insert x y vars)++instance (Ditraversable f, f :<: g) => N2PTrans f g where+  n2pAlg = liftM inject . disequence . dimap (return . P.Var) id -- default++instance N2PTrans NVar g where+  n2pAlg (NVar x) = liftM fromJust (asks (Map.lookup x))++en :: Term SigN+en = Term $ iNLam "x1" $ iNLam "x2" (iNLam "x3" $ iNVar "x2") `iApp` iNVar "x1"++ep :: Term SigP+ep = n2p en++--------------------------------------------------------------------------------+-- PHOAS to names translation+--------------------------------------------------------------------------------++type M' = Reader [Name]++class P2NTrans f g where+  p2nAlg :: Alg f (M' (Trm g a))+++-- We make the lifting to sums explicit in order to make the P2NTrans+-- work with the default instance declaration further below.+instance (P2NTrans f1 g, P2NTrans f2 g) => P2NTrans (f1 :+: f2) g where+    p2nAlg = caseD p2nAlg p2nAlg+++p2n :: (Difunctor f, P2NTrans f g) => Term f -> Term g+p2n t = Term $ runReader (cata p2nAlg t) ['x' : show n | n <- [1..]]++instance (Ditraversable f, f :<: g) => P2NTrans f g where+  p2nAlg = liftM inject . disequence . dimap (return . P.Var) id -- default++instance (NLam :<: g, NVar :<: g) => P2NTrans Lam g where+  p2nAlg (Lam f) = do n:names <- ask+                      return $ iNLam n (runReader (f (return $ iNVar n)) names)++ep' :: Term SigP+ep' = Term $ iLam $ \a -> iLam (\b -> (iLam $ \_ -> b)) `iApp` a++en' :: Term SigN+en' = p2n ep'
+ examples/Examples/Thunk.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances, OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Param.Thunk+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+--------------------------------------------------------------------------------++module Examples.Thunk where++import Data.Comp.Param+import Data.Comp.Param.Show ()+import Data.Comp.Param.Derive+import Data.Comp.Param.Thunk++-- Signatures for values and operators+data Const a e = Const Int+data Lam a e = Lam (a -> e) -- Note: not e -> e+data App a e = App e e+data Op a e = Add e e | Mult e e+data Fun a e = Fun (e -> e) -- Note: not a -> e++-- Signature for the simple expression language+type Sig = Const :+: Lam :+: App :+: Op+-- Signature for values. Note the use of 'FunM' rather than 'Lam' (!)+type Value = Const :+: Fun+-- Signature for ground values.+type GValue = Const++-- Derive boilerplate code using Template Haskell+$(derive [makeDifunctor, makeEqD, makeOrdD, makeShowD, smartConstructors]+         [''Const, ''Lam, ''App, ''Op])+$(derive [makeDitraversable]+         [''Const, ''App, ''Op])++-- 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+-- @e -> m e@. The latter is needed because the input to a @Lam@ (which is+-- evaluated to a @Fun@) will determine whether or not an error should be+-- returned. Example: @(\x -> x x) 42@ will produce an error because the+-- abstraction is applied to a non-functional, whereas @(\x -> x x)(\y -> y)@+-- will not.+class EvalT f v where+  evalAlgT :: Alg f (TrmT Maybe v a)++$(derive [liftSum] [''EvalT])++-- Lift the evaluation algebra to a catamorphism+evalT :: (Difunctor f, Ditraversable v, EvalT f v) => Term f -> Maybe (Term v)+evalT t = nfT $ Term (cata evalAlgT t)++-- instance (Ditraversable f Maybe Any, f :<: v) => EvalT f v where+--   evalAlgT  = strict'++instance (Difunctor f, f :<: v) => EvalT f v where+  evalAlgT  = inject'+++instance (Const :<: v) => EvalT Op v where+  evalAlgT (Add mx my)  = thunk $ do +                            Const x <- whnfPr mx+                            Const y <- whnfPr my+                            return $ iConst $ x + y+  evalAlgT (Mult mx my) = thunk $ do +                            Const x <- whnfPr mx+                            Const y <- whnfPr my+                            return $ iConst $ x * y++instance (Fun :<: v) => EvalT App v where+  evalAlgT (App mx my) = thunk $ do +                           Fun f <- whnfPr mx+                           -- lazy+                           return $ f my+                           -- strict+                           -- liftM f $ whnf' my++instance (Fun :<: v) => EvalT Lam v where+  evalAlgT (Lam f) = inject $ Fun f++-- |Evaluation of expressions to ground values.+evalMG :: Term Sig -> Maybe (Term GValue)+evalMG e = termM $ nfPr $ eval e+  where eval :: Term Sig -> TrmT Maybe Value a+        eval = cata evalAlgT+++-- Example: evalEx = Just (iConst 12) (3 * (2 + 2) = 12)+evalMEx :: Maybe (Term GValue)+evalMEx = evalMG $ Term $ iLam (\x -> iLam $ \y -> y `iMult` (x `iAdd` x))+                   `iApp` iConst 2 `iApp` iConst 3++-- Example: type error+evalMEx' :: Maybe (Term GValue)+evalMEx' = evalMG $ Term $ iLam (\x -> iLam $ \y -> x `iMult` (x `iAdd` x))+                   `iApp` iConst 2 `iApp` (iLam (\x -> x) `iAdd` iConst 2)++-- Example: non-termination+evalMExY :: Maybe (Term GValue)+evalMExY = evalMG $ Term $ iLam (\x -> iLam $ \y -> x `iMult` (x `iAdd` x))+                   `iApp` iConst 2 `iApp` omega+    where omega = iLam (\x -> x `iApp` x) `iApp` iLam (\x -> x `iApp` x)
+ src/Data/Comp/Param.hs view
@@ -0,0 +1,32 @@+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>, Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines the infrastructure necessary to use+-- /Parametric Compositional Data Types/. Parametric Compositional Data Types +-- is an extension of Compositional Data Types with parametric+-- higher-order abstract syntax (PHOAS) for usage with binders. Examples of+-- usage are bundled with the package in the library+-- @examples\/Examples\/Param@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param (+    module Data.Comp.Param.Term+  , module Data.Comp.Param.Algebra+  , module Data.Comp.Param.Difunctor+  , module Data.Comp.Param.Sum+  , module Data.Comp.Param.Annotation+  , module Data.Comp.Param.Equality+    ) where++import Data.Comp.Param.Term+import Data.Comp.Param.Algebra+import Data.Comp.Param.Difunctor+import Data.Comp.Param.Sum+import Data.Comp.Param.Annotation+import Data.Comp.Param.Equality
+ src/Data/Comp/Param/Algebra.hs view
@@ -0,0 +1,962 @@+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,+  FlexibleContexts, CPP #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Algebra+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines the notion of algebras and catamorphisms, and their+-- generalizations to e.g. monadic versions and other (co)recursion schemes.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Algebra (+      -- * Algebras & Catamorphisms+      Alg,+      free,+      cata,+      cata',+      appCxt,+      +      -- * Monadic Algebras & Catamorphisms+      AlgM,+      algM,+      freeM,+      cataM,+      cataM',++      -- * Term Homomorphisms+      CxtFun,+      SigFun,+      Hom,+      appHom,+      appHom',+      compHom,+      appSigFun,+      appSigFun',+      compSigFun,+      compHomSigFun,+      compSigFunHom,+      hom,+      compAlg,+      compAlgSigFun,++      -- * Monadic Term Homomorphisms+      CxtFunM,+      SigFunM,+      HomM,+      SigFunMD,+      HomMD,+      sigFunM,+      appHomM,+      appTHomM,+      appHomM',+      appTHomM',+      homM,+      homMD,+      appSigFunM,+      appTSigFunM,+      appSigFunM',+      appTSigFunM',+      appSigFunMD,+      appTSigFunMD,+      compHomM,+      compHomM',+      compSigFunM,+      compSigFunHomM,+      compSigFunHomM',+      compAlgSigFunM,+      compAlgSigFunM',+      compAlgM,+      compAlgM',++      -- * Coalgebras & Anamorphisms+      Coalg,+      ana,+      CoalgM,+      anaM,++      -- * R-Algebras & Paramorphisms+      RAlg,+      para,+      RAlgM,+      paraM,++      -- * R-Coalgebras & Apomorphisms+      RCoalg,+      apo,+      RCoalgM,+      apoM,++      -- * CV-Algebras & Histomorphisms+      CVAlg,+      histo,+      CVAlgM,+      histoM,++      -- * CV-Coalgebras & Futumorphisms+      CVCoalg,+      futu,+      CVCoalg',+      futu',+      CVCoalgM,+      futuM+    ) where++import Prelude hiding (sequence, mapM)+import Control.Monad hiding (sequence, mapM)+import Data.Comp.Param.Term+import Data.Comp.Param.Ops+import Data.Comp.Param.Difunctor+import Data.Comp.Param.Ditraversable++{-| This type represents an algebra over a difunctor @f@ and carrier @a@. -}+type Alg f a = f a a -> a+++{-| Construct a catamorphism for contexts over @f@ with holes of type @b@, from+  the given algebra. -}+free :: forall h f a b. Difunctor f+        => Alg f a -> (b -> a) -> Cxt h f a b -> a+free f g = run+    where run :: Cxt h f a b -> a+          run (In t) = f (difmap run t)+          run (Hole x) = g x+          run (Var p) = p++{-| Construct a catamorphism from the given algebra. -}+cata :: forall f a. Difunctor f => Alg f a -> Term f -> a +{-# NOINLINE [1] cata #-}+cata f (Term t) = run t+    where run :: Trm f a -> a+          run (In t) = f (difmap run t)+          run (Var x) = x++{-| A generalisation of 'cata' from terms over @f@ to contexts over @f@, where+  the holes have the type of the algebra carrier. -}+cata' :: Difunctor f => Alg f a -> Cxt h f a a -> a+{-# INLINE cata' #-}+cata' f = free f id++{-| 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 (In t) = In (difmap appCxt t)+appCxt (Hole x) = x+appCxt (Var p) = Var p++{-| This type represents a monadic algebra. It is similar to 'Alg' but+  the return type is monadic. -}+type AlgM m f a = f a a -> m a++{-| Convert a monadic algebra into an ordinary algebra with a monadic+  carrier. -}+algM :: (Ditraversable f, Monad m) => AlgM m f a -> Alg f (m a)+algM f x = disequence (dimap return id x) >>= f++{-| Construct a monadic catamorphism for contexts over @f@ with holes of type+  @b@, from the given monadic algebra. -}+freeM :: forall m h f a b. (Ditraversable f, Monad m)+         => AlgM m f a -> (b -> m a) -> Cxt h f a b -> m a+freeM f g = run+    where run :: Cxt h f a b -> m a+          run (In t) = f =<< dimapM run t+          run (Hole x) = g x+          run (Var p) = return p++{-| Construct a monadic catamorphism from the given monadic algebra. -}+cataM :: forall m f a. (Ditraversable f, Monad m) => AlgM m f a -> Term f -> m a+{-# NOINLINE [1] cataM #-}+cataM algm (Term t) = run t+    where run :: Trm f a  -> m a+          run (In t) = algm =<< dimapM run t+          run (Var x) = return x++{-| A generalisation of 'cataM' from terms over @f@ to contexts over @f@, where+  the holes have the type of the monadic algebra carrier. -}+cataM' :: forall m h f a. (Ditraversable f, Monad m)+          => AlgM m f a -> Cxt h f a (m a) -> m a+{-# NOINLINE [1] cataM' #-}+cataM' f = freeM f id++{-| This type represents a context function. -}+type CxtFun f g = forall h a b. Cxt h f a b -> Cxt h g a b+++{-| This type represents a signature function. -}+type SigFun f g = forall a b. f a b -> g a b++{-| This type represents a term homomorphism. -}+type Hom f g = SigFun f (Context g)++{-| Apply a term homomorphism recursively to a term/context. -}+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 (In t) = appCxt (f (difmap run t))+    run (Hole x) = Hole x+    run (Var p) = Var p++{-| Apply a term homomorphism recursively to a term/context. -}+appHom' :: forall f g. (Difunctor g) => Hom f g -> CxtFun f g+{-# NOINLINE [1] appHom' #-}+appHom' f = run where+    run :: CxtFun f g+    run (In t) = appCxt (fmapCxt run (f t))+    run (Hole x) = Hole x+    run (Var p) = Var p++fmapCxt :: Difunctor f => (b -> b') -> Cxt h f a b -> Cxt h f a b'+fmapCxt f = run+    where run (In t) = In $ difmap run t+          run (Var a) = Var a+          run (Hole b)  = Hole $ f b++{-| Compose two term homomorphisms. -}+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 -> Hom f g -> Alg f a+compAlg alg talg = cata' alg . talg++compAlgSigFun  :: Alg g a -> SigFun f g -> Alg f a+compAlgSigFun alg sig = alg . sig+++{-| This function applies a signature function to the given context. -}+appSigFun :: forall f g. (Difunctor f) => SigFun f g -> CxtFun f g+{-# NOINLINE [1] appSigFun #-}+appSigFun f = run+    where run (In t) = In $ f $ difmap run t+          run (Var x) = Var x+          run (Hole x) = Hole x+-- implementation via term homomorphisms+--  appSigFun f = appHom $ hom f+++-- | This function applies a signature function to the given+-- context. This is a top-bottom variant of 'appSigFun'.+appSigFun' :: forall f g. (Difunctor g) => SigFun f g -> CxtFun f g+{-# NOINLINE [1] appSigFun' #-}+appSigFun' f = run+    where run (In t) = In $ difmap run $ f t+          run (Var x) = Var x+          run (Hole x) = Hole x++{-| This function composes two signature functions. -}+compSigFun :: SigFun g h -> SigFun f g -> SigFun f h+compSigFun f g = f . g++{-| This function composes a term homomorphism and a signature function. -}+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. -}+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. -}+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)++{-| This type represents a monadic context function. -}+type CxtFunM m f g = forall h . SigFunM m (Cxt h f) (Cxt h g)++{-| This type represents a monadic signature function. It is similar to+  'SigFunM' but has monadic values also in the domain. -}+type SigFunMD m f g = forall a b. f a (m b) -> m (g a b)++{-| This type represents a monadic term homomorphism. -}+type HomM m f g = SigFunM m f (Context g)++{-| This type represents a monadic term homomorphism. It is similar to+  '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+  term homomorphisms are instances of signature functions. Hence this function+  also applies to term homomorphisms. -}+sigFunM :: Monad m => SigFun f g -> SigFunM m f g+sigFunM f = return . f++{-| Lift the given signature function to a monadic term homomorphism. -}+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.+appHomM :: forall f g m. (Ditraversable f, Difunctor g, Monad m)+           => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM #-}+appHomM f = run+    where run :: CxtFunM m f g+          run (In t) = liftM appCxt . f =<< dimapM run t+          run (Hole x) = return (Hole x)+          run (Var p) = return (Var p)++{-| A restricted form of |appHomM| which only works for terms. -}+appTHomM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)+            => HomM m f g -> Term f -> m (Term g)+appTHomM f (Term t) = termM (appHomM f t)+++-- | Apply a monadic term homomorphism recursively to a+-- term/context. The monad is sequence top-down.+appHomM' :: forall f g m. (Ditraversable g, Monad m)+            => HomM m f g -> CxtFunM m f g+appHomM' f = run+    where run :: CxtFunM m f g+          run (In t)  = liftM appCxt . dimapMCxt run =<< f t+          run (Var p) = return (Var p)+          run (Hole x) = return (Hole x)++dimapMCxt :: (Ditraversable f, Monad m)+             => (b -> m b') -> Cxt h f a b -> m (Cxt h f a b')+dimapMCxt f = run+              where run (In t) = liftM In $ dimapM run t+                    run (Var a)  = return $ Var a+                    run (Hole b) = liftM Hole (f b)++{-| A restricted form of |appHomM'| which only works for terms. -}+appTHomM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g)+             => HomM m f g -> Term f -> m (Term g)+appTHomM' f (Term t) = termM (appHomM' f t)+            ++{-| This function constructs the unique monadic homomorphism from the+  initial term algebra to the given term algebra. -}+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 (In t) = liftM appCxt (f (difmap run t))+          run (Hole x) = return (Hole x)+          run (Var p) = return (Var p)++{-| This function applies a monadic signature function to the given context. -}+appSigFunM :: forall m f g. (Ditraversable f, Monad m)+              => SigFunM m f g -> CxtFunM m f g+appSigFunM f = run+    where run :: CxtFunM m f g+          run (In t) = liftM In . f =<< dimapM run t+          run (Var x) = return $ Var x+          run (Hole x) = return $ Hole x+-- implementation via term homomorphisms+--  appSigFunM f = appHomM $ hom' f++{-| A restricted form of |appSigFunM| which only works for terms. -}+appTSigFunM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)+               => SigFunM m f g -> Term f -> m (Term g)+appTSigFunM f (Term t) = termM (appSigFunM f t)++-- | This function applies a monadic signature function to the given+-- context. This is a 'top-down variant of 'appSigFunM'.+appSigFunM' :: forall m f g. (Ditraversable g, Monad m)+               => SigFunM m f g -> CxtFunM m f g+appSigFunM' f = run+    where run :: CxtFunM m f g+          run (In t) = liftM In . dimapM run =<< f t+          run (Var x) = return $ Var x+          run (Hole x) = return $ Hole x++{-| A restricted form of |appSigFunM'| which only works for terms. -}+appTSigFunM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g)+                => SigFunM m f g -> Term f -> m (Term g)+appTSigFunM' f (Term t) = termM (appSigFunM' f t)++{-| This function applies a signature function to the given context. -}+appSigFunMD :: forall f g m. (Ditraversable f, Difunctor g, Monad m)+               => SigFunMD m f g -> CxtFunM m f g+appSigFunMD f = run +    where run :: CxtFunM m f g+          run (In t) = liftM In (f (difmap run t))+          run (Hole x) = return (Hole x)+          run (Var p) = return (Var p)++{-| A restricted form of |appSigFunMD| which only works for terms. -}+appTSigFunMD :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)+                => SigFunMD m f g -> Term f -> m (Term g)+appTSigFunMD f (Term t) = termM (appSigFunMD f t)++{-| Compose two monadic term homomorphisms. -}+compHomM :: (Ditraversable g, 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. -}+compHomM' :: (Ditraversable 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. -}+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. -}+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. -}+compSigFunHomM :: (Ditraversable g, 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. -}+compSigFunHomM' :: (Ditraversable h, Monad m)+                   => 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, Monad m) => 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, Monad m) => AlgM m g 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+  monadic algebra. -}+compAlgSigFunM :: Monad m => AlgM m g a -> SigFunM m f g -> AlgM m f a+compAlgSigFunM alg talg = alg <=< talg+++{-| Compose a monadic algebra with a signature function to get a new monadic+  algebra. -}+compAlgSigFunM' :: AlgM m g a -> SigFun f g -> AlgM m f a+compAlgSigFunM' alg talg = alg . talg++{-| This function composes two monadic signature functions. -}+compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h+compSigFunM f g = f <=< g+++----------------+-- Coalgebras --+----------------++{-| This type represents a coalgebra over a difunctor @f@ and carrier @a@. The+  list of @(a,b)@s represent the parameters that may occur in the constructed+  value. The first component represents the seed of the parameter,+  and the second component is the (polymorphic) parameter itself. If @f@ is+  itself a binder, then the parameters bound by @f@ can be passed to the+  covariant argument, thereby making them available to sub terms. -}+type Coalg f a = forall b. a -> [(a,b)] -> Either b (f b (a,[(a,b)]))++{-| Construct an anamorphism from the given coalgebra. -}+ana :: Difunctor f => Coalg f a -> a -> Term f+ana f x = Term $ anaAux f x+    where anaAux :: Difunctor f => Coalg f a -> a -> (forall a. Trm f a)+          anaAux f x = run (x,[])+              where run (a,bs) = case f a bs of+                                   Left p -> Var p+                                   Right t -> In $ difmap run t++{-| This type represents a monadic coalgebra over a difunctor @f@ and carrier+  @a@. -}+type CoalgM m f a = forall b. a -> [(a,b)] -> m (Either b (f b (a,[(a,b)])))++{-| Construct a monadic anamorphism from the given monadic coalgebra. -}+anaM :: forall a m f. (Ditraversable f, Monad m)+     => CoalgM m f a -> a -> forall a. m (Trm f a)+anaM f x = run (x,[])+    where run (a,bs) = do c <- f a bs+                          case c of+                            Left p -> return $ Var p+                            Right t -> liftM In $ dimapM run t+++--------------------------------+-- R-Algebras & Paramorphisms --+--------------------------------++{-| This type represents an r-algebra over a difunctor @f@ and carrier @a@. -}+type RAlg f a = f a (Trm f a, a) -> a++{-| Construct a paramorphism from the given r-algebra. -}+para :: forall f a. Difunctor f => RAlg f a -> Term f -> a+para f (Term t) = run t+    where run :: Trm f a -> a+          run (In t) = f $ difmap (\x -> (x, run x)) t+          run (Var x) = x++{-| This type represents a monadic r-algebra over a difunctor @f@ and carrier+  @a@. -}+type RAlgM m f a = f a (Trm f a, a) -> m a+{-| Construct a monadic paramorphism from the given monadic r-algebra. -}+paraM :: forall m f a. (Ditraversable f, Monad m) => RAlgM m f a -> Term f -> m a+paraM f (Term t) = run t+    where run :: Trm f a -> m a+          run (In t) = f =<< dimapM (\x -> run x >>= \y -> return (x, y)) t+          run (Var x) = return x+++--------------------------------+-- R-Coalgebras & Apomorphisms --+--------------------------------++{-| This type represents an r-coalgebra over a difunctor @f@ and carrier @a@. -}+type RCoalg f a = forall b. a -> [(a,b)] -> Either b (f b (Either (Trm f b) (a,[(a,b)])))++{-| Construct an apomorphism from the given r-coalgebra. -}+apo :: Difunctor f => RCoalg f a -> a -> Term f+apo f x = Term (apoAux f x)+    where apoAux :: Difunctor f => RCoalg f a -> a -> (forall a. Trm f a)+          apoAux coa x = run (x,[])+              where -- run :: (a,[(a,b)]) -> Trm f b+                run (a,bs) = case coa a bs of+                               Left x -> Var x+                               Right t -> In $ difmap run' t+                -- run' :: Either (Trm f b) (a,[(a,b)]) -> Trm f b+                run' (Left t) = t+                run' (Right x) = run x++++{-| This type represents a monadic r-coalgebra over a functor @f@ and carrier+  @a@. -}+type RCoalgM m f a = forall b. a -> [(a,b)] -> m (Either b (f b (Either (Trm f b) (a,[(a,b)]))))++{-| Construct a monadic apomorphism from the given monadic r-coalgebra. -}+apoM :: forall f m a. (Ditraversable f, Monad m)+        => RCoalgM m f a -> a -> forall a. m (Trm f a)+apoM coa x = run (x,[]) +    where run (a,bs) = do+            res <- coa a bs+            case res of+              Left x -> return $ Var x+              Right t -> liftM In $ dimapM run' t+          run' (Left t) = return t+          run' (Right x) = run x+++----------------------------------+-- CV-Algebras & Histomorphisms --+----------------------------------++{-| This type represents a cv-algebra over a difunctor @f@ and carrier @a@. -}+type CVAlg f a f' = f a (Trm f' a) -> a++-- | This function applies 'projectA' at the tip of the term.+projectTip  :: DistAnn f a f' => Trm f' a -> a+projectTip (In v) = snd $ projectA v+projectTip (Var p) = p++{-| Construct a histomorphism from the given cv-algebra. -}+histo :: forall f f' a. (Difunctor f, DistAnn f a f')+         => CVAlg f a f' -> Term f -> a+histo alg = projectTip . cata run+    where run :: Alg f (Trm f' a)+          run v = In $ injectA (alg v') v'+              where v' = dimap Var id v++{-| This type represents a monadic cv-algebra over a functor @f@ and carrier+  @a@. -}+type CVAlgM m f a f' = f a (Trm f' a) -> m a++{-| Construct a monadic histomorphism from the given monadic cv-algebra. -}+histoM :: forall f f' m a. (Ditraversable f, Monad m, DistAnn f a f')+          => CVAlgM m f a f' -> Term f -> m a+histoM alg (Term t) = liftM projectTip (run t)+    where run :: Trm f a -> m (Trm f' a)+          run (In t) = do t' <- dimapM run t+                          r <- alg t'+                          return $ In $ injectA r t'+          run (Var p) = return $ Var p+++-----------------------------------+-- CV-Coalgebras & Futumorphisms --+-----------------------------------++{-| This type represents a cv-coalgebra over a difunctor @f@ and carrier @a@.+  The list of @(a,b)@s represent the parameters that may occur in the+  constructed value. The first component represents the seed of the parameter,+  and the second component is the (polymorphic) parameter itself. If @f@ is+  itself a binder, then the parameters bound by @f@ can be passed to the+  covariant argument, thereby making them available to sub terms. -}+type CVCoalg f a = forall b. a -> [(a,b)]+                 -> Either b (f b (Context f b (a,[(a,b)])))++{-| Construct a futumorphism from the given cv-coalgebra. -}+futu :: Difunctor f => CVCoalg f a -> a -> Term f+futu f x = Term (futuAux f x)+    where futuAux :: Difunctor f => CVCoalg f a -> a -> (forall a. Trm f a)+          futuAux coa x = run (x,[])+              where run (a,bs) = case coa a bs of+                                   Left p -> Var p+                                   Right t -> In $ difmap run' t+                    run' (In t) = In $ difmap run' t+                    run' (Hole x) = run x+                    run' (Var p) = Var p++{-| This type represents a monadic cv-coalgebra over a difunctor @f@ and carrier+  @a@. -}+type CVCoalgM m f a = forall b. a -> [(a,b)]+                    -> m (Either b (f b (Context f b (a,[(a,b)]))))++{-| Construct a monadic futumorphism from the given monadic cv-coalgebra. -}+futuM :: forall f a m. (Ditraversable f, Monad m) =>+         CVCoalgM m f a -> a -> forall a. m (Trm f a)+futuM coa x = run (x,[])+    where run (a,bs) = do c <- coa a bs+                          case c of +                            Left p -> return $ Var p+                            Right t -> liftM In $ dimapM run' t+          run' (In t) = liftM In $ dimapM run' t+          run' (Hole x) = run x+          run' (Var p) = return $ Var p++{-| This type represents a generalised cv-coalgebra over a difunctor @f@ and+  carrier @a@. -}+type CVCoalg' f a = forall b. a -> [(a,b)] -> Context f b (a,[(a,b)])++{-| Construct a futumorphism from the given generalised cv-coalgebra. -}+futu' :: Difunctor f => CVCoalg' f a -> a -> Term f+futu' f x = Term (futuAux' f x)+    where futuAux' :: Difunctor f => CVCoalg' f a -> a -> (forall a. Trm f a)+          futuAux' coa x = run (x,[])+              where run (a,bs) = run' $ coa a bs+                    run' (In t) = In $ difmap run' t+                    run' (Hole x) = run x+                    run' (Var p) = Var p++{--------------------------------------------+-- functions only used for rewrite rules --+-------------------------------------------++appAlgHom :: forall f g d. Difunctor g => Alg g d -> Hom f g -> Term f -> d+{-# NOINLINE [1] appAlgHom #-}+appAlgHom alg hom (Term t) = run t where+    run :: Trm f d -> d+    run (In t) = run' $ hom t+    run (Var a) = a+    run' :: Context g d (Trm f d) -> d+    run' (In t) = alg $ fmap run' t+    run' (Var a) = a+    run' (Hole x) = run x+++-- | This function applies a signature function after a term homomorphism.+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 (In t) = run' $ g t+    run (Var a) = Var a+    run (Hole h) = Hole h+    run' :: Context g a (Cxt h' f a b) -> Cxt h' h a b+    run' (In t) = In $ f $ fmap run' t+    run' (Var a) = Var a+    run' (Hole h) = run h++appAlgHomM :: forall m g f d. Ditraversable g+              => AlgM m g d -> HomM m f g -> Term f -> m d+appAlgHomM alg hom (Term t) = run t where+    run :: Trm f d -> m d+    run (In t) = run' =<< hom t+    run (Var a) = return a+    run' :: Context g d (Trm f d) -> m d+    run' (In t) = alg =<< dimapM run' t+    run' (Var a) = return a+    run' (Hole x) = run x++appHomHomM :: forall m f g h. (Ditraversable g, Difunctor h)+              => HomM m g h -> HomM m f g -> CxtFunM m f h+appHomHomM f g = run where+--    run :: CxtFunM m f h+    run (In t) = run' =<< g t+    run (Var a) = return $ Var a+    run (Hole h) = return $ Hole h+--    run' :: Context g Any (Cxt h' f Any b) -> m (Cxt h' h Any b)+    run' (In t) = liftM appCxt $ f =<< dimapM run' t+    run' (Var a) = return $ Var a+    run' (Hole h) = run h++appSigFunHomM :: forall m f g h. Ditraversable g+                 => SigFunM m g h -> HomM m f g -> CxtFunM m f h+appSigFunHomM f g = run where+--    run :: CxtFunM m f h+    run (In t) = run' =<< g t+    run (Var a) = return $ Var a+    run (Hole h) = return $ Hole h+--    run' :: Context g Any (Cxt h' f Any b) -> m (Cxt h' h Any b)+    run' (In t) = liftM In $ f =<< dimapM run' t+    run' (Var a) = return $ Var a+    run' (Hole h) = run h+++-------------------+-- rewrite rules --+-------------------++#ifndef NO_RULES+{-# RULES+  "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.+    cata a (appHom h x) = cata (compAlg 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) = appAlgHom a (hom 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;++  "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;++  "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;++  "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;++  "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;++  "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;++  "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom a (appHom h x) = appHom (compHom 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;++  "appHom'/appHom" forall (a :: Hom g h) (h :: Hom f g) x.+    appHom' a (appHom h x) = appHom (compHom 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;++  "appSigFun'/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.+    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) = 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;++  "appHom/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom f (appSigFun g x) = appHom (compHomSigFun 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;++  "appHom'/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.+    appHom' f (appSigFun' g x) =  appHom' (compHomSigFun 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/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun f (appHom g x) = appSigFunHom 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/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.+    appSigFun f (appHom' g x) = appSigFunHom 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;+    +  "appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)+                                      (h :: SigFun f1 f2) x.+    appSigFunHom f g (appSigFun h x)+    = appSigFunHom f (compHomSigFun g h) x;++  "appSigFunHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)+                                      (h :: SigFun f1 f2) x.+    appSigFunHom f g (appSigFun' h x)+    = appSigFunHom f (compHomSigFun 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;++  "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/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'/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;++  "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;++  "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;++  "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/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.+     appHomM h x >>= cataM a =  appAlgHomM 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 = appAlgHomM a (homM h) x;++  "cataM/appSigFunM'" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.+     appSigFunM' h x >>= cataM a = appAlgHomM a (homM 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/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) = appAlgHomM a (sigFunM $ hom h) x;++  "cataM/appSigFun'" forall (a :: AlgM m g d) (h :: SigFun f g) 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) = appAlgHomM a (sigFunM $ hom h) 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;++  "appHomM/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appHomM a = appHomM (compHomM 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;++  "appHomM/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appHomM a = appHomHomM a 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;++  "appHomM'/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM h x >>= appHomM' a = appHomM' (compHomM' 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;++  "appHomM'/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.+     appHomM' h x >>= appHomM' a = appHomM' (compHomM' 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;++  "appHomM/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM a (appHom h x) = appHomHomM a (sigFunM 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;++  "appHomM'/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM' a (appHom h x) = appHomM' (compHomM' 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;++  "appHomM/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM a (appHom' h x) = appHomHomM a (sigFunM 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;++  "appHomM'/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.+     appHomM' a (appHom' h x) = appHomM' (compHomM' 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/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/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 = appSigFunHomM a (homM 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'/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/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) = appSigFunHomM a (sigFunM $ hom 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/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) = appSigFunHomM a (sigFunM $ hom 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;+++  "appHom/appHomM" forall (a :: Hom g h) (h :: HomM m f g) x.+     appHomM h x >>= (return . appHom a) = appHomM (compHomM_ a h) x; #-}+#endif+-}
+ src/Data/Comp/Param/Annotation.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,+  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Annotation+-- Copyright   :  (c) 2010-2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines annotations on signatures.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Annotation+    (+     (:&:) (..),+     (:*:) (..),+     DistAnn (..),+     RemA (..),+     liftA,+     liftA',+     stripA,+     propAnn,+     propAnnM,+     ann,+     project'+    ) where++import Data.Comp.Param.Difunctor+import Data.Comp.Param.Term+import Data.Comp.Param.Sum+import Data.Comp.Param.Ops+import Data.Comp.Param.Algebra++import Control.Monad++{-| Transform a function with a domain constructed from a functor to a function+ with a domain constructed with the same functor, but with an additional+ annotation. -}+liftA :: (RemA s s') => (s' a b -> t) -> s a b -> t+liftA f v = f (remA v)++{-| Transform a function with a domain constructed from a functor to a function+  with a domain constructed with the same functor, but with an additional+  annotation. -}+liftA' :: (DistAnn s' p s, Difunctor s')+          => (s' a b -> Cxt h s' c d) -> s a b -> Cxt h s c d+liftA' f v = let (v',p) = projectA v+             in ann p (f v')++{-| Strip the annotations from a term over a functor with annotations. -}+stripA :: (RemA g f, Difunctor g) => CxtFun g f+stripA = appSigFun remA++{-| 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) +        => 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) +         => HomM m f g -> HomM m f' g'+propAnnM hom f' = liftM (ann p) (hom f)+    where (f,p) = projectA f'++{-| Annotate each node of a term with a constant value. -}+ann :: (DistAnn f p g, Difunctor f)  => p -> CxtFun f g+ann c = appSigFun (injectA c)++{-| This function is similar to 'project' but applies to signatures+with an annotation which is then ignored. -}+project' :: (RemA f f', s :<: f') => Cxt h f a b -> Maybe (s a (Cxt h f a b))+project' (In x) = proj $ remA x+project' _ = Nothing
+ src/Data/Comp/Param/Derive.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module contains functionality for automatically deriving boilerplate+-- code using Template Haskell. Examples include instances of 'Difunctor',+-- 'Difoldable', and 'Ditraversable'.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Derive+    (+     derive,+     -- |Derive boilerplate instances for parametric signatures, i.e.+     -- signatures for parametric compositional data types.++     -- ** EqD+     module Data.Comp.Param.Derive.Equality,+     -- ** OrdD+     module Data.Comp.Param.Derive.Ordering,+     -- ** ShowD+     module Data.Comp.Param.Derive.Show,+     -- ** Difunctor+     module Data.Comp.Param.Derive.Difunctor,+     -- ** Ditraversable+     module Data.Comp.Param.Derive.Ditraversable,+     -- ** Smart Constructors+     module Data.Comp.Param.Derive.SmartConstructors,+     -- ** Smart Constructors w/ Annotations+     module Data.Comp.Param.Derive.SmartAConstructors,+     -- ** Lifting to Sums+     liftSum+    ) where++import Data.Comp.Derive.Utils (derive, liftSumGen)+import Data.Comp.Param.Derive.Equality+import Data.Comp.Param.Derive.Ordering+import Data.Comp.Param.Derive.Show+import Data.Comp.Param.Derive.Difunctor+import Data.Comp.Param.Derive.Ditraversable+import Data.Comp.Param.Derive.SmartConstructors+import Data.Comp.Param.Derive.SmartAConstructors+import Data.Comp.Param.Ops ((:+:), caseD)++import Language.Haskell.TH++{-| Given the name of a type class, where the first parameter is a difunctor,+  lift it to sums of difunctors. Example: @class ShowD f where ...@ is lifted+  as @instance (ShowD f, ShowD g) => ShowD (f :+: g) where ... @. -}+liftSum :: Name -> Q [Dec]+liftSum = liftSumGen 'caseD ''(:+:)
+ src/Data/Comp/Param/Derive/Difunctor.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.Functor+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @Difunctor@.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Derive.Difunctor+    (+     Difunctor,+     makeDifunctor+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Param.Difunctor+import Language.Haskell.TH++{-| Derive an instance of 'Difunctor' for a type constructor of any parametric+  kind taking at least two arguments. -}+makeDifunctor :: Name -> Q [Dec]+makeDifunctor fname = do+  -- Comments below apply to the example where name = T, args = [a,b,c], and+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type+  -- declaration: T a b c = X c | Y a c | Z (b -> c)+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  -- coArg = c (covariant difunctor argument)+  let coArg :: Name = tyVarBndrName $ last args+  -- conArg = b (contravariant difunctor argument)+  let conArg :: Name = tyVarBndrName $ last $ init args+  -- argNames = [a]+  let argNames = map (VarT . tyVarBndrName) (init $ init args)+  -- compType = T a+  let complType = foldl AppT (ConT name) argNames+  -- classType = Difunctor (T a)+  let classType = AppT (ConT ''Difunctor) complType+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  dimapDecl <- funD 'dimap (map (dimapClause conArg coArg) constrs')+  return [InstanceD [] classType [dimapDecl]]+      where dimapClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            dimapClause conArg coArg (constr, args) = do+              fn <- newName "_f"+              gn <- newName "_g"+              varNs <- newNames (length args) "x"+              let f = varE fn+              let g = varE gn+              let fp = VarP fn+              let gp = VarP gn+              -- Pattern for the constructor+              let pat = ConP constr $ map VarP varNs+              body <- dimapArgs conArg coArg f g (zip varNs args) (conE constr)+              return $ Clause [fp, gp, pat] (NormalB body) []+            dimapArgs :: Name -> Name -> ExpQ -> ExpQ+                      -> [(Name, Type)] -> ExpQ -> ExpQ+            dimapArgs _ _ _ _ [] acc =+                acc+            dimapArgs conArg coArg f g ((x,tp):tps) acc =+                dimapArgs conArg coArg f g tps+                          (acc `appE` (dimapArg conArg coArg tp f g `appE` varE x))+            -- Given the name of the difunctor variables, a type, and the two+            -- arguments to dimap, return the expression that should be applied+            -- to the parameter of the given type.+            -- Example: dimapArg a b (a -> b) f g yields the expression+            -- [|\x -> g . x . f|]+            dimapArg :: Name -> Name -> Type -> ExpQ -> ExpQ -> ExpQ+            dimapArg conArg coArg tp f g+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) = [| id |]+                | otherwise =+                    case tp of+                      VarT a | a == conArg -> f+                             | a == coArg -> g+                      AppT (AppT ArrowT tp1) tp2 -> do+                          xn <- newName "x"+                          let ftp1 = dimapArg conArg coArg tp1 f g+                          let ftp2 = dimapArg conArg coArg tp2 f g+                          lamE [varP xn]+                               (infixE (Just ftp2)+                                       [|(.)|]+                                       (Just $ infixE (Just $ varE xn)+                                                      [|(.)|]+                                                      (Just ftp1)))+                      SigT tp' _ ->+                          dimapArg conArg coArg tp' f g+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| dimap $f $g |]+                          else+                              [| fmap $g |]
+ src/Data/Comp/Param/Derive/Ditraversable.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.Ditraversable+-- Copyright   :  (c) 2010-2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @Ditraversable@.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Derive.Ditraversable+    (+     Ditraversable,+     makeDitraversable+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Param.Ditraversable+import Data.Traversable (mapM)+import Language.Haskell.TH+import Data.Maybe+import Control.Monad hiding (mapM)+import Prelude hiding (mapM)++iter 0 _ e = e+iter n f e = iter (n-1) f (f `appE` e)++iter' n f e = run n f e+    where run 0 _ e = e+          run m f e = let f' = iter (m-1) [|fmap|] f+                        in run (m-1) f (f' `appE` e)++{-| Derive an instance of 'Traversable' for a type constructor of any+  first-order kind taking at least one argument. -}+makeDitraversable :: Name -> Q [Dec]+makeDitraversable fname = do+  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname+  let fArg = VarT . tyVarBndrName $ last args+      aArg = VarT . tyVarBndrName $ last (init args)+      funTy = foldl AppT ArrowT [aArg,fArg]+      argNames = map (VarT . tyVarBndrName) (init $ init args)+      complType = foldl AppT (ConT name) argNames+      classType = foldl1 AppT [ConT ''Ditraversable, complType]+  normConstrs <- mapM normalConExp constrs+  constrs' <- mapM (mkPatAndVars . isFarg fArg funTy) normConstrs+  mapMDecl <- funD 'dimapM (map mapMClause constrs')+  sequenceDecl <- funD 'disequence (map sequenceClause constrs')+  return [InstanceD [] classType [mapMDecl,sequenceDecl]]+      where isFarg fArg funTy (constr, args) =+                (constr, map (\t -> (t `containsType'` fArg, t `containsType'` funTy)) args)+            checksAarg aArg (_,args) = any (`containsType` aArg) args+            filterVar _ _ nonFarg ([],[]) x  = nonFarg x+            filterVar farg _ _ ([depth],[]) x = farg depth x+            filterVar _ aarg _ ([_],[depth]) x = aarg depth x+            filterVar _ _ _ _ _ = error "functor variable occurring twice in argument type"+            filterVars args varNs farg aarg nonFarg = zipWith (filterVar farg aarg nonFarg) args varNs+            mkCPat constr varNs = ConP constr $ map mkPat varNs+            mkPat = VarP+            mkPatAndVars (constr, args) =+                do varNs <- newNames (length args) "x"+                   return (conE constr, mkCPat constr varNs,+                           any (not . null . fst) args || any (not . null . snd) args, map varE varNs,+                           catMaybes $ filterVars args varNs (\x y -> Just (False,x,y)) (\x y -> Just (True, x, y)) (const Nothing))++            -- Note: the monadic versions are not defined+            -- applicatively, as this results in a considerable+            -- performance penalty (by factor 2)!+            mapMClause (con, pat,hasFargs,allVars, fvars) =+                do fn <- newName "f"+                   let f = varE fn+                       fp = if hasFargs then VarP fn else WildP+                       conAp = foldl appE con allVars+                       addDi False _ x = x+                       addDi True d x = [|dimapM $(f)|]+                       conBind (fun,d,x) y = [| $(iter d [|mapM|] (addDi fun d f)) $(varE x)  >>= $(lamE [varP x] y)|]+                   body <- foldr conBind [|return $conAp|] fvars+                   return $ Clause [fp, pat] (NormalB body) []+            sequenceClause (con, pat,hasFargs,allVars, fvars) =+                do let conAp = foldl appE con allVars+                       varE' False _ x = varE x+                       varE' True d x = appE (iter d [|fmap|] [|disequence|]) (varE x)+                       conBind (fun,d, x) y = [| $(iter' d [|sequence|] (varE' fun d x))  >>= $(lamE [varP x] y)|]+                   body <- foldr conBind [|return $conAp|] fvars+                   return $ Clause [pat] (NormalB body) []
+ src/Data/Comp/Param/Derive/Equality.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,+  ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.Equality+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @EqD@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Derive.Equality+    (+     EqD(..),+     makeEqD+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Param.FreshM hiding (Name)+import Data.Comp.Param.Equality+import Control.Monad+import Language.Haskell.TH hiding (Cxt, match)++{-| Derive an instance of 'EqD' for a type constructor of any parametric+  kind taking at least two arguments. -}+makeEqD :: Name -> Q [Dec]+makeEqD fname = do+  -- Comments below apply to the example where name = T, args = [a,b,c], and+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type+  -- declaration: T a b c = X c | Y a c | Z (b -> c)+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  -- coArg = c (covariant difunctor argument)+  let coArg :: Name = tyVarBndrName $ last args+  -- conArg = b (contravariant difunctor argument)+  let conArg :: Name = tyVarBndrName $ last $ init args+  -- argNames = [a]+  let argNames = map (VarT . tyVarBndrName) (init $ init args)+  -- compType = T a+  let complType = foldl AppT (ConT name) argNames+  -- classType = Difunctor (T a)+  let classType = AppT (ConT ''EqD) complType+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  let defC = if length constrs < 2 then+                 []+             else+                 [clause [wildP,wildP] (normalB [|return False|]) []]+  eqDDecl <- funD 'eqD (map (eqDClause conArg coArg) constrs' ++ defC)+  let context = map (\arg -> ClassP ''Eq [arg]) argNames+  return [InstanceD context classType [eqDDecl]]+      where eqDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            eqDClause conArg coArg (constr, args) = do+              varXs <- newNames (length args) "x"+              varYs <- newNames (length args) "y"+              -- Patterns for the constructors+              let patx = ConP constr $ map VarP varXs+              let paty = ConP constr $ map VarP varYs+              body <- eqDBody conArg coArg (zip3 varXs varYs args)+              return $ Clause [patx,paty] (NormalB body) []+            eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ+            eqDBody conArg coArg x =+                [|liftM and (sequence $(listE $ map (eqDB conArg coArg) x))|]+            eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ+            eqDB conArg coArg (x, y, tp)+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) =+                    [| return $ $(varE x) == $(varE y) |]+                | otherwise =+                    case tp of+                      VarT a+                          | a == coArg -> [| peq $(varE x) $(varE y) |]+                      AppT (AppT ArrowT (VarT a)) _+                          | a == conArg ->+                              [| withName (\v -> peq ($(varE x) v) ($(varE y) v)) |]+                      SigT tp' _ ->+                          eqDB conArg coArg (x, y, tp')+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| eqD $(varE x) $(varE y) |]+                          else+                              [| peq $(varE x) $(varE y) |]
+ src/Data/Comp/Param/Derive/Injections.hs view
@@ -0,0 +1,86 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.Injections+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Derive functions for signature injections.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Derive.Injections+    (+     injn,+     injectn,+     deepInjectn+    ) where++import Language.Haskell.TH hiding (Cxt)+import Data.Comp.Param.Difunctor+import Data.Comp.Param.Term+import Data.Comp.Param.Algebra (CxtFun, appSigFun)+import Data.Comp.Param.Ops ((:+:)(..), (:<:)(..))++injn :: Int -> Q [Dec]+injn n = do+  let i = mkName $ "inj" ++ show n+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]+  let gvar = mkName "g"+  let avar = mkName "a"+  let bvar = mkName "b"+  let xvar = mkName "x"+  let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]+  sequence $ sigD i (genSig fvars gvar avar bvar) : d+    where genSig fvars gvar avar bvar = do+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)+                            (map varT fvars)+            let tp' = arrowT `appT` (tp `appT` varT avar `appT` varT bvar)+                             `appT` (varT gvar `appT` varT avar `appT`+                                     varT bvar)+            forallT (map PlainTV $ gvar : avar : bvar : fvars)+                    (sequence cxt) tp'+          genDecl x n = [| case $(varE x) of+                             Inl x -> $(varE $ mkName "inj") x+                             Inr x -> $(varE $ mkName $ "inj" +++                                        if n > 2 then show (n - 1) else "") x |]+injectn :: Int -> Q [Dec]+injectn n = do+  let i = mkName ("inject" ++ show n)+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]+  let gvar = mkName "g"+  let avar = mkName "a"+  let bvar = mkName "b"+  let d = [funD i [clause [] (normalB $ genDecl n) []]]+  sequence $ sigD i (genSig fvars gvar avar bvar) : d+    where genSig fvars gvar avar bvar = do+            let hvar = mkName "h"+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)+                            (map varT fvars)+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar+                                 `appT` varT avar `appT` varT bvar+            let tp'' = arrowT `appT` (tp `appT` varT avar `appT` tp') `appT` tp'+            forallT (map PlainTV $ hvar : gvar : avar : bvar : fvars)+                    (sequence cxt) tp''+          genDecl n = [| In . $(varE $ mkName $ "inj" ++ show n) |]++deepInjectn :: Int -> Q [Dec]+deepInjectn n = do+  let i = mkName ("deepInject" ++ show n)+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]+  let gvar = mkName "g"+  let d = [funD i [clause [] (normalB $ genDecl n) []]]+  sequence $ sigD i (genSig fvars gvar) : d+    where genSig fvars gvar = do+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)+                            (map varT fvars)+            let cxt' = classP ''Difunctor [tp]+            let tp' = conT ''CxtFun `appT` tp `appT` varT gvar+            forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'+          genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
+ src/Data/Comp/Param/Derive/Ordering.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,+  ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.Ordering+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @OrdD@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Derive.Ordering+    (+     OrdD(..),+     makeOrdD+    ) where++import Data.Comp.Param.FreshM hiding (Name)+import Data.Comp.Param.Ordering+import Data.Comp.Derive.Utils+import Language.Haskell.TH hiding (Cxt)+import Control.Monad (liftM)++{-| Derive an instance of 'OrdD' for a type constructor of any parametric+  kind taking at least two arguments. -}+makeOrdD :: Name -> Q [Dec]+makeOrdD fname = do+  -- Comments below apply to the example where name = T, args = [a,b,c], and+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type+  -- declaration: T a b c = X c | Y a c | Z (b -> c)+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  -- coArg = c (covariant difunctor argument)+  let coArg :: Name = tyVarBndrName $ last args+  -- conArg = b (contravariant difunctor argument)+  let conArg :: Name = tyVarBndrName $ last $ init args+  -- argNames = [a]+  let argNames = map (VarT . tyVarBndrName) (init $ init args)+  -- compType = T a+  let complType = foldl AppT (ConT name) argNames+  -- classType = Difunctor (T a)+  let classType = AppT (ConT ''OrdD) complType+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  compareDDecl <- funD 'compareD (compareDClauses conArg coArg constrs')+  let context = map (\arg -> ClassP ''Ord [arg]) argNames+  return [InstanceD context classType [compareDDecl]]+      where compareDClauses :: Name -> Name -> [(Name,[Type])] -> [ClauseQ]+            compareDClauses _ _ [] = []+            compareDClauses conArg coArg constrs = +                let constrs' = constrs `zip` [1..]+                    constPairs = [(x,y)| x<-constrs', y <- constrs']+                in map (genClause conArg coArg) constPairs+            genClause conArg coArg ((c,n),(d,m))+                | n == m = genEqClause conArg coArg c+                | n < m = genLtClause c d+                | otherwise = genGtClause c d+            genEqClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            genEqClause conArg coArg (constr, args) = do +              varXs <- newNames (length args) "x"+              varYs <- newNames (length args) "y"+              let patX = ConP constr $ map VarP varXs+              let patY = ConP constr $ map VarP varYs+              body <- eqDBody conArg coArg (zip3 varXs varYs args)+              return $ Clause [patX, patY] (NormalB body) []+            eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ+            eqDBody conArg coArg x =+                [|liftM compList (sequence $(listE $ map (eqDB conArg coArg) x))|]+            eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ+            eqDB conArg coArg (x, y, tp)+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) =+                    [| return $ compare $(varE x) $(varE y) |]+                | otherwise =+                    case tp of+                      VarT a+                          | a == coArg -> [| pcompare $(varE x) $(varE y) |]+                      AppT (AppT ArrowT (VarT a)) _+                          | a == conArg ->+                              [| withName (\v -> pcompare ($(varE x) v) ($(varE y) v)) |]+                      SigT tp' _ ->+                          eqDB conArg coArg (x, y, tp')+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| compareD $(varE x) $(varE y) |]+                          else+                              [| pcompare $(varE x) $(varE y) |]+            genLtClause (c, _) (d, _) =+                clause [recP c [], recP d []] (normalB [| return LT |]) []+            genGtClause (c, _) (d, _) =+                clause [recP c [], recP d []] (normalB [| return GT |]) []
+ src/Data/Comp/Param/Derive/Projections.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE TemplateHaskell, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.Projections+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Derive functions for signature projections.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Derive.Projections+    (+     projn,+     projectn,+     deepProjectn+    ) where++import Language.Haskell.TH hiding (Cxt)+import Control.Monad (liftM)+import Data.Comp.Param.Ditraversable (Ditraversable)+import Data.Comp.Param.Term+import Data.Comp.Param.Algebra (appTSigFunM')+import Data.Comp.Param.Ops ((:+:)(..), (:<:)(..))++projn :: Int -> Q [Dec]+projn n = do+  let p = mkName $ "proj" ++ show n+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]+  let avar = mkName "a"+  let bvar = mkName "b"+  let xvar = mkName "x"+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar bvar) []]]+  sequence $ (sigD p $ genSig gvars avar bvar) : d+    where genSig gvars avar bvar = do+            let fvar = mkName "f"+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)+                            (map varT gvars)+            let tp' = arrowT `appT` (varT fvar `appT` varT avar `appT`+                                     varT bvar)+                             `appT` (conT ''Maybe `appT`+                                     (tp `appT` varT avar `appT` varT bvar))+            forallT (map PlainTV $ fvar : avar : bvar : gvars)+                    (sequence cxt) tp'+          genDecl x [g] a b =+            [| liftM inj (proj $(varE x)+                          :: Maybe ($(varT g `appT` varT a `appT` varT b))) |]+          genDecl x (g:gs) a b =+            [| case (proj $(varE x)+                         :: Maybe ($(varT g `appT` varT a `appT` varT b))) of+                 Just y -> Just $ inj y+                 _ -> $(genDecl x gs a b) |]+          genDecl _ _ _ _ = error "genDecl called with empty list"++projectn :: Int -> Q [Dec]+projectn n = do+  let p = mkName ("project" ++ show n)+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]+  let avar = mkName "a"+  let bvar = mkName "b"+  let xvar = mkName "x"+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]+  sequence $ (sigD p $ genSig gvars avar bvar) : d+    where genSig gvars avar bvar = do+            let fvar = mkName "f"+            let hvar = mkName "h"+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)+                            (map varT gvars)+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar+                                 `appT` varT avar `appT` varT bvar+            let tp'' = arrowT `appT` tp'+                              `appT` (conT ''Maybe `appT`+                                      (tp `appT` varT avar `appT` tp'))+            forallT (map PlainTV $ hvar : fvar : avar : bvar : gvars)+                    (sequence cxt) tp''+          genDecl x n = [| case $(varE x) of+                             Hole _ -> Nothing+                             Var _ -> Nothing+                             In t -> $(varE $ mkName $ "proj" ++ show n) t |]++deepProjectn :: Int -> Q [Dec]+deepProjectn n = do+  let p = mkName ("deepProject" ++ show n)+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]+  let d = [funD p [clause [] (normalB $ genDecl n) []]]+  sequence $ (sigD p $ genSig gvars) : d+    where genSig gvars = do+            let fvar = mkName "f"+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)+                            (map varT gvars)+            let cxt' = classP ''Ditraversable [tp]+            let tp' = arrowT `appT` (conT ''Term `appT` varT fvar)+                             `appT` (conT ''Maybe `appT` (conT ''Term `appT` tp))+            forallT (map PlainTV $ fvar : gvars) (sequence $ cxt' : cxt) tp'+          genDecl n = [| appTSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
+ src/Data/Comp/Param/Derive/Show.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,+  ScopedTypeVariables, UndecidableInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.Show+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @ShowD@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Derive.Show+    (+     ShowD(..),+     makeShowD+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Param.FreshM hiding (Name)+import qualified Data.Comp.Param.FreshM as FreshM+import Control.Monad+import Language.Haskell.TH hiding (Cxt, match)+import qualified Data.Traversable as T++{-| Signature printing. An instance @ShowD f@ gives rise to an instance+  @Show (Term f)@. -}+class ShowD f where+    showD :: f FreshM.Name (FreshM String) -> FreshM String++newtype Dummy = Dummy String++instance Show Dummy where+  show (Dummy s) = s++{-| Derive an instance of 'ShowD' for a type constructor of any parametric+  kind taking at least two arguments. -}+makeShowD :: Name -> Q [Dec]+makeShowD fname = do+  -- Comments below apply to the example where name = T, args = [a,b,c], and+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type+  -- declaration: T a b c = X c | Y a c | Z (b -> c)+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  -- coArg = c (covariant difunctor argument)+  let coArg :: Name = tyVarBndrName $ last args+  -- conArg = b (contravariant difunctor argument)+  let conArg :: Name = tyVarBndrName $ last $ init args+  -- argNames = [a]+  let argNames = map (VarT . tyVarBndrName) (init $ init args)+  -- compType = T a+  let complType = foldl AppT (ConT name) argNames+  -- classType = Difunctor (T a)+  let classType = AppT (ConT ''ShowD) complType+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  showDDecl <- funD 'showD (map (showDClause conArg coArg) constrs')+  let context = map (\arg -> ClassP ''Show [arg]) argNames+  return [InstanceD context classType [showDDecl]]+      where showDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            showDClause conArg coArg (constr, args) = do+              varXs <- newNames (length args) "x"+              -- Pattern for the constructor+              let patx = ConP constr $ map VarP varXs+              body <- showDBody (nameBase constr) conArg coArg (zip varXs args)+              return $ Clause [patx] (NormalB body) []+            showDBody :: String -> Name -> Name -> [(Name, Type)] -> ExpQ+            showDBody constr conArg coArg x =+                [|liftM (unwords . (constr :) .+                         map (\x -> if elem ' ' x then "(" ++ x ++ ")" else x))+                        (sequence $(listE $ map (showDB conArg coArg) x))|]+            showDB :: Name -> Name -> (Name, Type) -> ExpQ+            showDB conArg coArg (x, tp)+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) =+                    [| return $ show $(varE x) |]+                | otherwise =+                    case tp of+                      VarT a+                          | a == coArg -> [| $(varE x) |]+                      AppT (AppT ArrowT (VarT a)) _+                          | a == conArg ->+                              [| withName (\v -> do body <- $(varE x) v;+                                                    return $ "\\" ++ show v ++ " -> " ++ body) |]+                      SigT tp' _ ->+                          showDB conArg coArg (x, tp')+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| showD $(varE x) |]+                          else+                              [| liftM show $ T.mapM (liftM Dummy) $(varE x) |]
+ src/Data/Comp/Param/Derive/SmartAConstructors.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.SmartAConstructors+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive smart constructors with annotations for difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Derive.SmartAConstructors +    (+     smartAConstructors+    ) where++import Language.Haskell.TH hiding (Cxt)+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 annotations for a difunctor. The smart+ constructors are similar to the ordinary constructors, but a+ 'injectA . dimap Var id' is automatically inserted. -}+smartAConstructors :: Name -> Q [Dec]+smartAConstructors fname = do+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname+    let cons = map abstractConType constrs+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons+        where genSmartConstr targs tname (name, args) = do+                let bname = nameBase name+                genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args+              genSmartConstr' targs tname sname name args = do+                varNs <- newNames args "x"+                varPr <- newName "_p"+                let pats = map varP (varPr : varNs)+                    vars = map varE varNs+                    val = appE [|injectA $(varE varPr)|] $+                          appE [|inj . dimap Var id|] $ foldl appE (conE name) vars+                    function = [funD sname [clause pats (normalB [|In $val|]) []]]+                sequence function
+ src/Data/Comp/Param/Derive/SmartConstructors.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Derive.SmartConstructors+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive smart constructors for difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Derive.SmartConstructors +    (+     smartConstructors+    ) where++import Language.Haskell.TH hiding (Cxt)+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 difunctor. The smart constructors are+ similar to the ordinary constructors, but a 'inject . dimap Var id' is+ automatically inserted. -}+smartConstructors :: Name -> Q [Dec]+smartConstructors fname = do+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname+    let cons = map abstractConType constrs+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons+        where genSmartConstr targs tname (name, args) = do+                let bname = nameBase name+                genSmartConstr' targs tname (mkName $ 'i' : bname) name args+              genSmartConstr' targs tname sname name args = do+                varNs <- newNames args "x"+                let pats = map varP varNs+                    vars = map varE varNs+                    val = foldl appE (conE name) vars+                    sig = genSig targs tname sname args+                    function = [funD sname [clause pats (normalB [|inject (dimap Var id $val)|]) []]]+                sequence $ sig ++ function+              genSig targs tname sname 0 = (:[]) $ do+                hvar <- newName "h"+                fvar <- newName "f"+                avar <- newName "a"+                bvar <- newName "b"+                let targs' = init $ init targs+                    vars = hvar:fvar:avar:bvar:targs'+                    h = varT hvar+                    f = varT fvar+                    a = varT avar+                    b = varT bvar+                    ftype = foldl appT (conT tname) (map varT targs')+                    constr = classP ''(:<:) [ftype, f]+                    typ = foldl appT (conT ''Cxt) [h, f, a, b]+                    typeSig = forallT (map PlainTV vars) (sequence [constr]) typ+                sigD sname typeSig+              genSig _ _ _ _ = []
+ src/Data/Comp/Param/Desugar.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,+  UndecidableInstances, OverlappingInstances, Rank2Types, TypeOperators #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Desugar+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This modules defines the 'Desugar' type class for desugaring of terms.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Desugar where++import Data.Comp.Param+++-- |The desugaring term homomorphism.+class (Difunctor f, Difunctor g) => Desugar f g where+    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)++-- We make the lifting to sums explicit in order to make the Desugar+-- class work with the default instance declaration further below.+instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where+    desugHom = caseD desugHom desugHom++-- |Desugar a term.+desugar :: Desugar f g => Term f -> Term g+{-# INLINE desugar #-}+desugar (Term t) = Term (appHom desugHom t)++-- |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 (Term t) = Term (appHom (propAnn desugHom) t)++-- |Default desugaring instance.+instance (Difunctor f, Difunctor g, f :<: g) => Desugar f g where+    desugHom = simpCxt . inj
+ src/Data/Comp/Param/Difunctor.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Difunctor+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines difunctors (Meijer, Hutton, FPCA '95), i.e. binary type+-- constructors that are contravariant in the first argument and covariant in+-- the second argument.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Difunctor+    (+      difmap,+     Difunctor(..)+    ) where++-- | This class represents difunctors, i.e. binary type constructors that are+-- contravariant in the first argument and covariant in the second argument.+class Difunctor f where+    dimap :: (a -> b) -> (c -> d) -> f b c -> f a d++{-| The canonical example of a difunctor. -}+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 = difmap
+ src/Data/Comp/Param/Ditraversable.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Ditraversable+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines traversable difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Ditraversable+    (+     Ditraversable(..)+    ) where++import Data.Comp.Param.Difunctor++{-| Difunctors representing data structures that can be traversed from left to+  right. -}+class Difunctor f => Ditraversable f where+    dimapM :: Monad m => (b -> m c) -> f a b -> m (f a c)+    dimapM f = disequence . fmap f+    disequence :: Monad m => f a (m b) -> m (f a b)+    disequence = dimapM id
+ src/Data/Comp/Param/Equality.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,+  UndecidableInstances, IncoherentInstances, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Equality+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines equality for signatures, which lifts to equality for+-- terms.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Equality+    (+     PEq(..),+     EqD(..)+    ) where++import Data.Comp.Param.Term+import Data.Comp.Param.Sum+import Data.Comp.Param.Ops+import Data.Comp.Param.Difunctor+import Data.Comp.Param.FreshM+import Control.Monad (liftM)++-- |Equality on parametric values. The equality test is performed inside the+-- 'FreshM' monad for generating fresh identifiers.+class PEq a where+    peq :: a -> a -> FreshM Bool++instance PEq a => PEq [a] where+    peq l1 l2+        | length l1 /= length l2 = return False+        | otherwise = liftM or $ mapM (uncurry peq) $ zip l1 l2++instance Eq a => PEq a where+    peq x y = return $ x == y++{-| Signature equality. An instance @EqD f@ gives rise to an instance+  @Eq (Term f)@. The equality test is performed inside the 'FreshM' monad for+  generating fresh identifiers. -}+class EqD f where+    eqD :: PEq a => f Name a -> f Name a -> FreshM Bool++{-| 'EqD' is propagated through sums. -}+instance (EqD f, EqD g) => EqD (f :+: g) where+    eqD (Inl x) (Inl y) = eqD x y+    eqD (Inr x) (Inr y) = eqD x y+    eqD _ _ = return False++{-| From an 'EqD' difunctor an 'Eq' instance of the corresponding term type can+  be derived. -}+instance EqD f => EqD (Cxt h f) where+    eqD (In e1) (In e2) = eqD e1 e2+    eqD (Hole h1) (Hole h2) = peq h1 h2+    eqD (Var p1) (Var p2) = peq p1 p2+    eqD _ _ = return False++instance (EqD f, PEq a) => PEq (Cxt h f Name a) where+    peq = eqD++{-| Equality on terms. -}+instance (Difunctor f, EqD f) => Eq (Term f) where+    (==) (Term x) (Term y) = evalFreshM $ eqD x y
+ src/Data/Comp/Param/FreshM.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.FreshM+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines a monad for generating fresh, abstract names, useful+-- e.g. for defining equality on terms.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.FreshM+    (+     FreshM,+     Name,+     withName,+     evalFreshM+    ) where++import Control.Monad.Reader+import Control.Applicative++-- |Monad for generating fresh (abstract) names.+newtype FreshM a = FreshM{unFreshM :: Reader Int a}+    deriving (Monad, Applicative,Functor)++-- |Abstract notion of a name (the constructor is hidden).+newtype Name = Name Int+    deriving Eq++instance Show Name where+    show (Name x) = names !! x+        where baseNames = ['a'..'z']+              names = map (:[]) baseNames ++ names' 1+              names' n = map (: show n) baseNames ++ names' (n + 1)++instance Ord Name where+    compare (Name x) (Name y) = compare x y++-- |Run the given computation with the next available name.+withName :: (Name -> FreshM a) -> FreshM a+withName m = do name <- FreshM (asks Name)+                FreshM $ local ((+) 1) $ unFreshM $ m name++-- |Evaluate a computation that uses fresh names.+evalFreshM :: FreshM a -> a+evalFreshM (FreshM m) = runReader m 0
+ src/Data/Comp/Param/Multi.hs view
@@ -0,0 +1,34 @@+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>, Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines the infrastructure necessary to use+-- /Generalised Parametric Compositional Data Types/. Generalised Parametric+-- Compositional Data Types is an extension of Compositional Data Types with+-- parametric higher-order abstract syntax (PHOAS) for usage with binders, and+-- GADTs. Generalised Parametric Compositional Data Types combines Generalised+-- Compositional Data Types ("Data.Comp.Multi") and Parametric Compositional+-- Data Types ("Data.Comp.Param"). Examples of usage are bundled with the+-- package in the library @examples\/Examples\/Param.Multi@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi (+    module Data.Comp.Param.Multi.Term+  , module Data.Comp.Param.Multi.Algebra+  , module Data.Comp.Param.Multi.HDifunctor+  , module Data.Comp.Param.Multi.Sum+  , module Data.Comp.Param.Multi.Annotation+  , module Data.Comp.Param.Multi.Equality+    ) where++import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.Algebra+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.Sum+import Data.Comp.Param.Multi.Annotation+import Data.Comp.Param.Multi.Equality
+ src/Data/Comp/Param/Multi/Algebra.hs view
@@ -0,0 +1,346 @@+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,+  FlexibleContexts, CPP, KindSignatures #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Algebra+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines the notion of algebras and catamorphisms, and their+-- generalizations to e.g. monadic versions and other (co)recursion schemes.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Algebra (+      -- * Algebras & Catamorphisms+      Alg,+      free,+      cata,+      cata',+      appCxt,+      +      -- * Monadic Algebras & Catamorphisms+      AlgM,+--      algM,+      freeM,+      cataM,+      AlgM',+      Compose(..),+      freeM',+      cataM',++      -- * Term Homomorphisms+      CxtFun,+      SigFun,+      Hom,+      appHom,+      appHom',+      compHom,+      appSigFun,+      appSigFun',+      compSigFun,+      hom,+      compAlg,++      -- * Monadic Term Homomorphisms+      CxtFunM,+      SigFunM,+      HomM,+      sigFunM,+      hom',+      appHomM,+      appTHomM,+      appHomM',+      appTHomM',+      homM,+      appSigFunM,+      appTSigFunM,+      appSigFunM',+      appTSigFunM',+      compHomM,+      compSigFunM,+      compAlgM,+      compAlgM'+    ) where++import Prelude hiding (sequence, mapM)+import Control.Monad hiding (sequence, mapM)+import Data.Functor.Compose -- Functor composition+import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.HDitraversable++{-| This type represents an algebra over a difunctor @f@ and carrier @a@. -}+type Alg f a = f a a :-> a++{-| Construct a catamorphism for contexts over @f@ with holes of type @b@, from+  the given algebra. -}+free :: forall h f a b. HDifunctor f+        => Alg f a -> (b :-> a) -> Cxt h f a b :-> a+free f g = run+    where run :: Cxt h f a b :-> a+          run (In t) = f (hfmap run t)+          run (Hole x) = g x+          run (Var p) = p++{-| Construct a catamorphism from the given algebra. -}+cata :: forall f a. HDifunctor f => Alg f a -> Term f :-> a +{-# NOINLINE [1] cata #-}+cata f (Term t) = run t+    where run :: Trm f a :-> a+          run (In t) = f (hfmap run t)+          run (Var x) = x++{-| A generalisation of 'cata' from terms over @f@ to contexts over @f@, where+  the holes have the type of the algebra carrier. -}+cata' :: HDifunctor f => Alg f a -> Cxt h f a a :-> a+{-# INLINE cata' #-}+cata' f = free f id++{-| This function applies a whole context into another context. -}+appCxt :: HDifunctor f => Cxt Hole f a (Cxt h f a b) :-> Cxt h f a b+appCxt (In t) = In (hfmap appCxt t)+appCxt (Hole x) = x+appCxt (Var p) = Var p++{-| This type represents a monadic algebra. It is similar to 'Alg' but+  the return type is monadic. -}+type AlgM m f a = NatM m (f a a) a++{-| Construct a monadic catamorphism for contexts over @f@ with holes of type+  @b@, from the given monadic algebra. -}+freeM :: forall m h f a b. (HDitraversable f, Monad m)+         => AlgM m f a -> NatM m b a -> NatM m (Cxt h f a b) a+freeM f g = run+    where run :: NatM m (Cxt h f a b) a+          run (In t) = f =<< hdimapM run t+          run (Hole x) = g x+          run (Var p) = return p++{-| Construct a monadic catamorphism from the given monadic algebra. -}+cataM :: forall m f a. (HDitraversable f, Monad m)+         => AlgM m f a -> NatM m (Term f) a+{-# NOINLINE [1] cataM #-}+cataM algm (Term t) = run t+    where run :: NatM m (Trm f a) a+          run (In t) = algm =<< hdimapM run t+          run (Var x) = return x++{-| This type represents a monadic algebra, but where the covariant argument is+  also a monadic computation. -}+type AlgM' m f a = NatM m (f a (Compose m a)) a++{-| Construct a monadic catamorphism for contexts over @f@ with holes of type+  @b@, from the given monadic algebra. -}+freeM' :: forall m h f a b. (HDifunctor f, Monad m)+          => AlgM' m f a -> NatM m b a -> NatM m (Cxt h f a b) a+freeM' f g = run+    where run :: NatM m (Cxt h f a b) a+          run (In t) = f $ hfmap (Compose . run) t+          run (Hole x) = g x+          run (Var p) = return p++{-| Construct a monadic catamorphism from the given monadic algebra. -}+cataM' :: forall m f a. (HDifunctor f, Monad m)+          => AlgM' m f a -> NatM m (Term f) a+{-# NOINLINE [1] cataM' #-}+cataM' algm (Term t) = run t+    where run :: NatM m (Trm f a) a+          run (In t) = algm $ hfmap (Compose . run) t+          run (Var x) = return x++{-| This type represents a signature function. -}+type SigFun f g = forall (a :: * -> *) (b :: * -> *) . f a b :-> g a b++{-| This type represents a context function. -}+type CxtFun f g = forall h. SigFun (Cxt h f) (Cxt h g)++{-| This type represents a term homomorphism. -}+type Hom f g = SigFun f (Context g)++{-| Apply a term homomorphism recursively to a term/context. -}+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 (In t) = appCxt (f (hfmap run t))+    run (Hole x) = Hole x+    run (Var p) = Var p++-- | Apply a term homomorphism recursively to a term/context. This is+-- 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 (In t) = appCxt (hfmapCxt run (f t))+    run (Hole x) = Hole x+    run (Var p) = Var p++{-| Compose two term homomorphisms. -}+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 -> Hom f g -> Alg f a+compAlg alg talg = cata' alg . talg++{-| This function applies a signature function to the given context. -}+appSigFun :: forall f g. (HDifunctor f) => SigFun f g -> CxtFun f g+appSigFun f = run where+    run :: CxtFun f g+    run (In t) = In (f (hfmap run t))+    run (Hole x) = Hole x+    run (Var p) = Var p++{-| This function applies a signature function to the given context. -}+appSigFun' :: forall f g. (HDifunctor g) => SigFun f g -> CxtFun f g+appSigFun' f = run where+    run :: CxtFun f g+    run (In t) = In (hfmap run (f t))+    run (Hole x) = Hole x+    run (Var p) = Var p++{-| This function composes two signature functions. -}+compSigFun :: SigFun g h -> SigFun f g -> SigFun f h+compSigFun f g = f . g++{-| Lifts the given signature function to the canonical term homomorphism. -}+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)++{-| This type represents a monadic context function. -}+type CxtFunM m f g = forall h . SigFunM m (Cxt h f) (Cxt h g)++{-| This type represents a monadic term homomorphism. -}+type HomM m f g = SigFunM m f (Cxt Hole g)+++{-| Lift the given signature function to a monadic signature function. Note that+  term homomorphisms are instances of signature functions. Hence this function+  also applies to term homomorphisms. -}+sigFunM :: Monad m => SigFun f g -> SigFunM m f g+sigFunM f = return . f++{-| Lift the give monadic signature function to a monadic term homomorphism. -}+hom' :: (HDifunctor f, HDifunctor g, Monad m)+            => SigFunM m f g -> HomM m f g+hom' f = liftM  (In . hfmap Hole) . f++{-| Lift the given signature function to a monadic term homomorphism. -}+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. -}+appHomM :: forall f g m. (HDitraversable f, Monad m, HDifunctor g)+               => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM #-}+appHomM f = run+    where run :: CxtFunM m f g+          run (In t) = liftM appCxt (f =<< hdimapM run t)+          run (Hole x) = return (Hole x)+          run (Var p) = return (Var p)++{-| A restricted form of |appHomM| which only works for terms. -}+appTHomM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)+            => HomM m f g -> Term f i -> m (Term g i)+appTHomM f (Term t) = termM (appHomM f t)++-- | Apply a monadic term homomorphism recursively to a+-- term/context. This is a top-down variant of 'appHomM'.+appHomM' :: forall f g m. (HDitraversable g, Monad m)+            => HomM m f g -> CxtFunM m f g+{-# NOINLINE [1] appHomM' #-}+appHomM' f = run+    where run :: CxtFunM m f g+          run (In t) = liftM appCxt (hdimapMCxt run =<<  f t)+          run (Hole x) = return (Hole x)+          run (Var p) = return (Var p)++{-| A restricted form of |appHomM'| which only works for terms. -}+appTHomM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)+             => HomM m f g -> Term f i -> m (Term g i)+appTHomM' f (Term t) = termM (appHomM' f t)++{-| This function applies a monadic signature function to the given context. -}+appSigFunM :: forall m f g. (HDitraversable f, Monad m)+              => SigFunM m f g -> CxtFunM m f g+appSigFunM f = run+    where run :: CxtFunM m f g+          run (In t)   = liftM In (f =<< hdimapM run t)+          run (Hole x) = return (Hole x)+          run (Var p)  = return (Var p)++{-| A restricted form of |appSigFunM| which only works for terms. -}+appTSigFunM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)+               => SigFunM m f g -> Term f i -> m (Term g i)+appTSigFunM f (Term t) = termM (appSigFunM f t)++-- | This function applies a monadic signature function to the given+-- context. This is a top-down variant of 'appSigFunM'.+appSigFunM' :: forall m f g. (HDitraversable g, Monad m)+               => SigFunM m f g -> CxtFunM m f g+appSigFunM' f = run+    where run :: CxtFunM m f g+          run (In t)   = liftM In (hdimapM run =<< f t)+          run (Hole x) = return (Hole x)+          run (Var p)  = return (Var p)++{-| A restricted form of |appSigFunM'| which only works for terms. -}+appTSigFunM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)+                => SigFunM m f g -> Term f i -> m (Term g i)+appTSigFunM' f (Term t) = termM (appSigFunM' f t)++{-| Compose two monadic term homomorphisms. -}+compHomM :: (HDitraversable g, 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, Monad m) => 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, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a+compAlgM' alg talg = freeM alg return . talg++{-| This function composes two monadic signature functions. -}+compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h+compSigFunM f g a = g a >>= f++{-+#ifndef NO_RULES+{-# RULES+  "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.+    cata a (appHom h x) = cata (compAlg 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/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/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.+     cataM a (appHom h x) = cataM (compAlgM' 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+  "cata/build"  forall alg (g :: forall a . Alg f a -> a) .+                cata alg (build g) = g alg #-}+-}+#endif+-}
+ src/Data/Comp/Param/Multi/Annotation.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,+  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Annotation+-- Copyright   :  (c) 2010-2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines annotations on signatures.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Annotation+    (+     (:&:) (..),+     (:*:) (..),+     DistAnn (..),+     RemA (..),+     liftA,+     liftA',+     stripA,+     propAnn,+     propAnnM,+     ann,+     project'+    ) where++import qualified Data.Comp.Ops as O+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.Sum+import Data.Comp.Param.Multi.Ops+import Data.Comp.Param.Multi.Algebra++import Control.Monad++{-| Transform a function with a domain constructed from a higher-order difunctor+  to a function with a domain constructed with the same higher-order difunctor,+  but with an additional annotation. -}+liftA :: (RemA s s') => (s' a b :-> t) -> s a b :-> t+liftA f v = f (remA v)++{-| Transform a function with a domain constructed from a higher-order difunctor+  to a function with a domain constructed with the same higher-order difunctor,+  but with an additional annotation. -}+liftA' :: (DistAnn s' p s, HDifunctor s')+          => (s' a b :-> Cxt h s' c d) -> s a b :-> Cxt h s c d+liftA' f v = let v' O.:&: p = projectA v+             in ann p (f v')++{-| Strip the annotations from a term over a higher-order difunctor with+  annotations. -}+stripA :: (RemA g f, HDifunctor g) => CxtFun g f+stripA = appSigFun remA++{-| 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) +           => 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)+         => HomM m f g -> HomM m f' g'+propAnnM hom f' = liftM (ann p) (hom f)+    where f O.:&: p = projectA f'++{-| Annotate each node of a term with a constant value. -}+ann :: (DistAnn f p g, HDifunctor f) => p -> CxtFun f g+ann c = appSigFun (injectA c)++{-| This function is similar to 'project' but applies to signatures+  with an annotation which is then ignored. -}+project' :: (RemA f f', s :<: f') => Cxt h f a b i -> Maybe (s a (Cxt h f a b) i)+project' (In x) = proj $ remA x+project' _ = Nothing
+ src/Data/Comp/Param/Multi/Derive.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module contains functionality for automatically deriving boilerplate+-- code using Template Haskell. Examples include instances of 'HDifunctor',+-- 'ShowHD', and 'EqHD'.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Derive+    (+     derive,+     -- |Derive boilerplate instances for parametric signatures, i.e.+     -- signatures for parametric compositional data types.++     -- ** EqHD+     module Data.Comp.Param.Multi.Derive.Equality,+     -- ** OrdHD+     module Data.Comp.Param.Multi.Derive.Ordering,+     -- ** ShowHD+     module Data.Comp.Param.Multi.Derive.Show,+     -- ** HDifunctor+     module Data.Comp.Param.Multi.Derive.HDifunctor,+     -- ** Smart Constructors+     module Data.Comp.Param.Multi.Derive.SmartConstructors,+     -- ** Smart Constructors w/ Annotations+     module Data.Comp.Param.Multi.Derive.SmartAConstructors,+     -- ** Lifting to Sums+     liftSum+    ) where++import Data.Comp.Derive.Utils (derive, liftSumGen)+import Data.Comp.Param.Multi.Derive.Equality+import Data.Comp.Param.Multi.Derive.Ordering+import Data.Comp.Param.Multi.Derive.Show+import Data.Comp.Param.Multi.Derive.HDifunctor+import Data.Comp.Param.Multi.Derive.SmartConstructors+import Data.Comp.Param.Multi.Derive.SmartAConstructors+import Data.Comp.Param.Multi.Ops ((:+:), caseHD)++import Language.Haskell.TH++{-| Given the name of a type class, where the first parameter is a higher-order+  difunctor, lift it to sums of higher-order difunctors. Example:+  @class ShowHD f where ...@ is lifted as+  @instance (ShowHD f, ShowHD g) => ShowHD (f :+: g) where ... @. -}+liftSum :: Name -> Q [Dec]+liftSum = liftSumGen 'caseHD ''(:+:)
+ src/Data/Comp/Param/Multi/Derive/Equality.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,+  ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.Equality+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @EqHD@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi.Derive.Equality+    (+     EqHD(..),+     makeEqHD+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Param.Multi.FreshM hiding (Name)+import Data.Comp.Param.Multi.Equality+import Control.Monad+import Language.Haskell.TH hiding (Cxt, match)++{-| Derive an instance of 'EqHD' for a type constructor of any parametric+  kind taking at least three arguments. -}+makeEqHD :: Name -> Q [Dec]+makeEqHD fname = do+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  let args' = init args+  -- covariant argument+  let coArg :: Name = tyVarBndrName $ last args'+  -- contravariant argument+  let conArg :: Name = tyVarBndrName $ last $ init args'+  let argNames = map (VarT . tyVarBndrName) (init $ init args')+  let complType = foldl AppT (ConT name) argNames+  let classType = AppT (ConT ''EqHD) complType+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  let defC = if length constrs < 2 then+                 []+             else+                 [clause [wildP,wildP] (normalB [|return False|]) []]+  eqHDDecl <- funD 'eqHD (map (eqHDClause conArg coArg) constrs' ++ defC)+  let context = map (\arg -> ClassP ''Eq [arg]) argNames+  return [InstanceD context classType [eqHDDecl]]+      where eqHDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            eqHDClause conArg coArg (constr, args) = do+              varXs <- newNames (length args) "x"+              varYs <- newNames (length args) "y"+              -- Patterns for the constructors+              let patx = ConP constr $ map VarP varXs+              let paty = ConP constr $ map VarP varYs+              body <- eqHDBody conArg coArg (zip3 varXs varYs args)+              return $ Clause [patx,paty] (NormalB body) []+            eqHDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ+            eqHDBody conArg coArg x =+                [|liftM and (sequence $(listE $ map (eqHDB conArg coArg) x))|]+            eqHDB :: Name -> Name -> (Name, Name, Type) -> ExpQ+            eqHDB conArg coArg (x, y, tp)+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) =+                    [| return $ $(varE x) == $(varE y) |]+                | otherwise =+                    case tp of+                      AppT (VarT a) _ +                          | a == coArg -> [| peq $(varE x) $(varE y) |]+                      AppT (AppT ArrowT (AppT (VarT a) _)) _+                          | a == conArg ->+                              [| withName (\v -> peq ($(varE x) $ nameCoerce v)                                                      ($(varE y) $ nameCoerce v)) |]+                      SigT tp' _ ->+                          eqHDB conArg coArg (x, y, tp')+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| eqHD $(varE x) $(varE y) |]+                          else+                              [| peq $(varE x) $(varE y) |]
+ src/Data/Comp/Param/Multi/Derive/HDifunctor.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.HDifunctor+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @HDifunctor@.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Derive.HDifunctor+    (+     HDifunctor,+     makeHDifunctor+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Param.Multi.HDifunctor+import Language.Haskell.TH++{-| Derive an instance of 'HDifunctor' for a type constructor of any parametric+  kind taking at least three arguments. -}+makeHDifunctor :: Name -> Q [Dec]+makeHDifunctor fname = do+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  let args' = init args+  -- covariant argument+  let coArg :: Name = tyVarBndrName $ last args'+  -- contravariant argument+  let conArg :: Name = tyVarBndrName $ last $ init args'+  let argNames = map (VarT . tyVarBndrName) (init $ init args')+  let complType = foldl AppT (ConT name) argNames+  let classType = AppT (ConT ''HDifunctor) complType+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  hdimapDecl <- funD 'hdimap (map (hdimapClause conArg coArg) constrs')+  return [InstanceD [] classType [hdimapDecl]]+      where hdimapClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            hdimapClause conArg coArg (constr, args) = do+              fn <- newName "_f"+              gn <- newName "_g"+              varNs <- newNames (length args) "x"+              let f = varE fn+              let g = varE gn+              let fp = VarP fn+              let gp = VarP gn+              -- Pattern for the constructor+              let pat = ConP constr $ map VarP varNs+              body <- hdimapArgs conArg coArg f g (zip varNs args) (conE constr)+              return $ Clause [fp, gp, pat] (NormalB body) []+            hdimapArgs :: Name -> Name -> ExpQ -> ExpQ+                      -> [(Name, Type)] -> ExpQ -> ExpQ+            hdimapArgs _ _ _ _ [] acc =+                acc+            hdimapArgs conArg coArg f g ((x,tp):tps) acc =+                hdimapArgs conArg coArg f g tps+                          (acc `appE` (hdimapArg conArg coArg tp f g `appE` varE x))+            hdimapArg :: Name -> Name -> Type -> ExpQ -> ExpQ -> ExpQ+            hdimapArg conArg coArg tp f g+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) = [| id |]+                | otherwise =+                    case tp of+                      AppT (VarT a) _ | a == conArg -> f+                                      | a == coArg -> g+                      AppT (AppT ArrowT tp1) tp2 -> do+                          xn <- newName "x"+                          let ftp1 = hdimapArg conArg coArg tp1 f g+                          let ftp2 = hdimapArg conArg coArg tp2 f g+                          lamE [varP xn]+                               (infixE (Just ftp2)+                                       [|(.)|]+                                       (Just $ infixE (Just $ varE xn)+                                                      [|(.)|]+                                                      (Just ftp1)))+                      SigT tp' _ ->+                          hdimapArg conArg coArg tp' f g+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| hdimap $f $g |]+                          else+                              [| fmap $g |]
+ src/Data/Comp/Param/Multi/Derive/Injections.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.Injections+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Derive functions for signature injections.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Derive.Injections+    (+     injn,+     injectn,+     deepInjectn+    ) where++import Language.Haskell.TH hiding (Cxt)+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.Algebra (CxtFun, appSigFun)+import Data.Comp.Param.Multi.Ops ((:+:)(..), (:<:)(..))++injn :: Int -> Q [Dec]+injn n = do+  let i = mkName $ "inj" ++ show n+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]+  let gvar = mkName "g"+  let avar = mkName "a"+  let bvar = mkName "b"+  let ivar = mkName "i"+  let xvar = mkName "x"+  let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]+  sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d+    where genSig fvars gvar avar bvar ivar = do+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)+                            (map varT fvars)+            let tp' = arrowT `appT` (tp `appT` varT avar `appT`+                                     varT bvar `appT` varT ivar)+                             `appT` (varT gvar `appT` varT avar `appT`+                                     varT bvar `appT` varT ivar)+            forallT (map PlainTV $ gvar : avar : bvar : ivar : fvars)+                    (sequence cxt) tp'+          genDecl x n = [| case $(varE x) of+                             Inl x -> $(varE $ mkName "inj") x+                             Inr x -> $(varE $ mkName $ "inj" +++                                        if n > 2 then show (n - 1) else "") x |]+injectn :: Int -> Q [Dec]+injectn n = do+  let i = mkName ("inject" ++ show n)+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]+  let gvar = mkName "g"+  let avar = mkName "a"+  let bvar = mkName "b"+  let ivar = mkName "i"+  let d = [funD i [clause [] (normalB $ genDecl n) []]]+  sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d+    where genSig fvars gvar avar bvar ivar = do+            let hvar = mkName "h"+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)+                            (map varT fvars)+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar+                                 `appT` varT avar `appT` varT bvar+            let tp'' = arrowT `appT` (tp `appT` varT avar `appT`+                                      tp' `appT` varT ivar)+                              `appT` (tp' `appT` varT ivar)+            forallT (map PlainTV $ hvar : gvar : avar : bvar : ivar : fvars)+                    (sequence cxt) tp''+          genDecl n = [| In . $(varE $ mkName $ "inj" ++ show n) |]++deepInjectn :: Int -> Q [Dec]+deepInjectn n = do+  let i = mkName ("deepInject" ++ show n)+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]+  let gvar = mkName "g"+  let d = [funD i [clause [] (normalB $ genDecl n) []]]+  sequence $ sigD i (genSig fvars gvar) : d+    where genSig fvars gvar = do+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)+                            (map varT fvars)+            let cxt' = classP ''HDifunctor [tp]+            let tp' = conT ''CxtFun `appT` tp `appT` varT gvar+            forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'+          genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
+ src/Data/Comp/Param/Multi/Derive/Ordering.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,+  ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.Ordering+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @OrdHD@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi.Derive.Ordering+    (+     OrdHD(..),+     makeOrdHD+    ) where++import Data.Comp.Param.Multi.FreshM hiding (Name)+import Data.Comp.Param.Multi.Ordering+import Data.Comp.Derive.Utils+import Data.Maybe+import Data.List+import Language.Haskell.TH hiding (Cxt)+import Control.Monad (liftM)++compList :: [Ordering] -> Ordering+compList = fromMaybe EQ . find (/= EQ)++{-| Derive an instance of 'OrdHD' for a type constructor of any parametric+  kind taking at least three arguments. -}+makeOrdHD :: Name -> Q [Dec]+makeOrdHD fname = do+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  let args' = init args+  -- covariant argument+  let coArg :: Name = tyVarBndrName $ last args'+  -- contravariant argument+  let conArg :: Name = tyVarBndrName $ last $ init args'+  let argNames = map (VarT . tyVarBndrName) (init $ init args')+  let complType = foldl AppT (ConT name) argNames+  let classType = AppT (ConT ''OrdHD) complType+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  compareHDDecl <- funD 'compareHD (compareHDClauses conArg coArg constrs')+  let context = map (\arg -> ClassP ''Ord [arg]) argNames+  return [InstanceD context classType [compareHDDecl]]+      where compareHDClauses :: Name -> Name -> [(Name,[Type])] -> [ClauseQ]+            compareHDClauses _ _ [] = []+            compareHDClauses conArg coArg constrs = +                let constrs' = constrs `zip` [1..]+                    constPairs = [(x,y)| x<-constrs', y <- constrs']+                in map (genClause conArg coArg) constPairs+            genClause conArg coArg ((c,n),(d,m))+                | n == m = genEqClause conArg coArg c+                | n < m = genLtClause c d+                | otherwise = genGtClause c d+            genEqClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            genEqClause conArg coArg (constr, args) = do +              varXs <- newNames (length args) "x"+              varYs <- newNames (length args) "y"+              let patX = ConP constr $ map VarP varXs+              let patY = ConP constr $ map VarP varYs+              body <- eqDBody conArg coArg (zip3 varXs varYs args)+              return $ Clause [patX, patY] (NormalB body) []+            eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ+            eqDBody conArg coArg x =+                [|liftM compList (sequence $(listE $ map (eqDB conArg coArg) x))|]+            eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ+            eqDB conArg coArg (x, y, tp)+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) =+                    [| return $ compare $(varE x) $(varE y) |]+                | otherwise =+                    case tp of+                      AppT (VarT a) _ +                          | a == coArg -> [| pcompare $(varE x) $(varE y) |]+                      AppT (AppT ArrowT (AppT (VarT a) _)) _+                          | a == conArg ->+                              [| withName (\v -> pcompare ($(varE x) $ nameCoerce v)+                                                          ($(varE y) $ nameCoerce v)) |]+                      SigT tp' _ ->+                          eqDB conArg coArg (x, y, tp')+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| compareHD $(varE x) $(varE y) |]+                          else+                              [| pcompare $(varE x) $(varE y) |]+            genLtClause (c, _) (d, _) =+                clause [recP c [], recP d []] (normalB [| return LT |]) []+            genGtClause (c, _) (d, _) =+                clause [recP c [], recP d []] (normalB [| return GT |]) []
+ src/Data/Comp/Param/Multi/Derive/Projections.hs view
@@ -0,0 +1,108 @@+{-# LANGUAGE TemplateHaskell, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.Projections+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Derive functions for signature projections.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Derive.Projections+    (+     projn,+     projectn,+     deepProjectn+    ) where++import Language.Haskell.TH hiding (Cxt)+import Control.Monad (liftM)+import Data.Comp.Param.Multi.HDitraversable (HDitraversable)+import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.Algebra (appTSigFunM')+import Data.Comp.Param.Multi.Ops ((:+:)(..), (:<:)(..))++projn :: Int -> Q [Dec]+projn n = do+  let p = mkName $ "proj" ++ show n+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]+  let avar = mkName "a"+  let bvar = mkName "b"+  let ivar = mkName "i"+  let xvar = mkName "x"+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar bvar ivar) []]]+  sequence $ (sigD p $ genSig gvars avar bvar ivar) : d+    where genSig gvars avar bvar ivar = do+            let fvar = mkName "f"+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)+                            (map varT gvars)+            let tp' = arrowT `appT` (varT fvar `appT` varT avar `appT`+                                     varT bvar `appT` varT ivar)+                             `appT` (conT ''Maybe `appT`+                                     (tp `appT` varT avar `appT`+                                      varT bvar `appT` varT ivar))+            forallT (map PlainTV $ fvar : avar : bvar : ivar : gvars)+                    (sequence cxt) tp'+          genDecl x [g] a b i =+            [| liftM inj (proj $(varE x)+                          :: Maybe ($(varT g `appT` varT a `appT`+                                      varT b `appT` varT i))) |]+          genDecl x (g:gs) a b i =+            [| case (proj $(varE x)+                         :: Maybe ($(varT g `appT` varT a `appT`+                                     varT b `appT` varT i))) of+                 Just y -> Just $ inj y+                 _ -> $(genDecl x gs a b i) |]+          genDecl _ _ _ _ _ = error "genDecl called with empty list"++projectn :: Int -> Q [Dec]+projectn n = do+  let p = mkName ("project" ++ show n)+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]+  let avar = mkName "a"+  let bvar = mkName "b"+  let ivar = mkName "i"+  let xvar = mkName "x"+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]+  sequence $ (sigD p $ genSig gvars avar bvar ivar) : d+    where genSig gvars avar bvar ivar = do+            let fvar = mkName "f"+            let hvar = mkName "h"+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)+                            (map varT gvars)+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar+                                 `appT` varT avar `appT` varT bvar+            let tp'' = arrowT `appT` (tp' `appT` varT ivar)+                              `appT` (conT ''Maybe `appT`+                                      (tp `appT` varT avar `appT` tp' `appT`+                                       varT ivar))+            forallT (map PlainTV $ hvar : fvar : avar : bvar : ivar : gvars)+                    (sequence cxt) tp''+          genDecl x n = [| case $(varE x) of+                             Hole _ -> Nothing+                             Var _ -> Nothing+                             In t -> $(varE $ mkName $ "proj" ++ show n) t |]++deepProjectn :: Int -> Q [Dec]+deepProjectn n = do+  let p = mkName ("deepProject" ++ show n)+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]+  let d = [funD p [clause [] (normalB $ genDecl n) []]]+  sequence $ (sigD p $ genSig gvars) : d+    where genSig gvars = do+            let fvar = mkName "f"+            let ivar = mkName "i"+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)+                            (map varT gvars)+            let cxt' = classP ''HDitraversable [tp]+            let tp' = arrowT `appT` (conT ''Term `appT` varT fvar `appT` varT ivar)+                             `appT` (conT ''Maybe `appT` (conT ''Term `appT` tp `appT` varT ivar))+            forallT (map PlainTV $ fvar : ivar : gvars) (sequence $ cxt' : cxt) tp'+          genDecl n = [| appTSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
+ src/Data/Comp/Param/Multi/Derive/Show.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,+  ScopedTypeVariables, UndecidableInstances, KindSignatures #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.Show+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @ShowHD@.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi.Derive.Show+    (+     ShowHD(..),+     makeShowHD+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Param.Multi.FreshM hiding (Name)+import qualified Data.Comp.Param.Multi.FreshM as FreshM+import Data.Comp.Param.Multi.HDifunctor+import Control.Monad+import Language.Haskell.TH hiding (Cxt, match)+import qualified Data.Traversable as T++{-| Signature printing. An instance @ShowHD f@ gives rise to an instance+  @Show (Term f i)@. -}+class ShowHD f where+    showHD :: f FreshM.Name (K (FreshM String)) i -> FreshM String++newtype Dummy = Dummy String++instance Show Dummy where+  show (Dummy s) = s++{-| Derive an instance of 'ShowHD' for a type constructor of any parametric+  kind taking at least three arguments. -}+makeShowHD :: Name -> Q [Dec]+makeShowHD fname = do+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  let args' = init args+  -- covariant argument+  let coArg :: Name = tyVarBndrName $ last args'+  -- contravariant argument+  let conArg :: Name = tyVarBndrName $ last $ init args'+  let argNames = map (VarT . tyVarBndrName) (init $ init args')+  let complType = foldl AppT (ConT name) argNames+  let classType = AppT (ConT ''ShowHD) complType+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  showHDDecl <- funD 'showHD (map (showHDClause conArg coArg) constrs')+  let context = map (\arg -> ClassP ''Show [arg]) argNames+  return [InstanceD context classType [showHDDecl]]+      where showHDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ+            showHDClause conArg coArg (constr, args) = do+              varXs <- newNames (length args) "x"+              -- Pattern for the constructor+              let patx = ConP constr $ map VarP varXs+              body <- showHDBody (nameBase constr) conArg coArg (zip varXs args)+              return $ Clause [patx] (NormalB body) []+            showHDBody :: String -> Name -> Name -> [(Name, Type)] -> ExpQ+            showHDBody constr conArg coArg x =+                [|liftM (unwords . (constr :) .+                         map (\x -> if elem ' ' x then "(" ++ x ++ ")" else x))+                        (sequence $(listE $ map (showHDB conArg coArg) x))|]+            showHDB :: Name -> Name -> (Name, Type) -> ExpQ+            showHDB conArg coArg (x, tp)+                | not (containsType tp (VarT conArg)) &&+                  not (containsType tp (VarT coArg)) =+                    [| return $ show $(varE x) |]+                | otherwise =+                    case tp of+                      AppT (VarT a) _ +                          | a == coArg -> [| unK $(varE x) |]+                      AppT (AppT ArrowT (AppT (VarT a) _)) _+                          | a == conArg ->+                              [| withName (\v -> do body <- (unK . $(varE x)) v+                                                    return $ "\\" ++ show v ++ " -> " ++ body) |]+                      SigT tp' _ ->+                          showHDB conArg coArg (x, tp')+                      _ ->+                          if containsType tp (VarT conArg) then+                              [| showHD $(varE x) |]+                          else+                              [| liftM show $ T.mapM (liftM Dummy . unK) $(varE x) |]
+ src/Data/Comp/Param/Multi/Derive/SmartAConstructors.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.SmartAConstructors+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive smart constructors with annotations for higher-order+-- difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Derive.SmartAConstructors +    (+     smartAConstructors+    ) where++import Language.Haskell.TH hiding (Cxt)+import Data.Comp.Derive.Utils+import Data.Comp.Param.Multi.Ops+import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.HDifunctor++import Control.Monad++{-| Derive smart constructors with annotations for a higher-order difunctor. The+ smart constructors are similar to the ordinary constructors, but a+ 'injectA . hdimap Var id' is automatically inserted. -}+smartAConstructors :: Name -> Q [Dec]+smartAConstructors fname = do+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname+    let cons = map abstractConType constrs+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons+        where genSmartConstr targs tname (name, args) = do+                let bname = nameBase name+                genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args+              genSmartConstr' targs tname sname name args = do+                varNs <- newNames args "x"+                varPr <- newName "_p"+                let pats = map varP (varPr : varNs)+                    vars = map varE varNs+                    val = appE [|injectA $(varE varPr)|] $+                          appE [|inj . hdimap Var id|] $ foldl appE (conE name) vars+                    function = [funD sname [clause pats (normalB [|In $val|]) []]]+                sequence function
+ src/Data/Comp/Param/Multi/Derive/SmartConstructors.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Derive.SmartConstructors+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive smart constructors for higher-order difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Derive.SmartConstructors +    (+     smartConstructors+    ) where++import Language.Haskell.TH hiding (Cxt)+import Data.Comp.Derive.Utils+import Data.Comp.Param.Multi.Sum+import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.HDifunctor+import Control.Arrow ((&&&))+import Control.Monad++{-| Derive smart constructors for a higher-order difunctor. The smart+ constructors are similar to the ordinary constructors, but a+ 'inject . hdimap Var id' is automatically inserted. -}+smartConstructors :: Name -> Q [Dec]+smartConstructors fname = do+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname+    let iVar = tyVarBndrName $ last targs+    let cons = map (abstractConType &&& iTp iVar) constrs+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons+        where iTp iVar (ForallC _ cxt _) =+                  -- Check if the GADT phantom type is constrained+                  case [y | EqualP x y <- cxt, x == VarT iVar] of+                    [] -> Nothing+                    tp:_ -> Just tp+              iTp _ _ = Nothing+              genSmartConstr targs tname ((name, args), miTp) = do+                let bname = nameBase name+                genSmartConstr' targs tname (mkName $ 'i' : bname) name args miTp+              genSmartConstr' targs tname sname name args miTp = do+                varNs <- newNames args "x"+                let pats = map varP varNs+                    vars = map varE varNs+                    val = foldl appE (conE name) vars+                    sig = genSig targs tname sname args miTp+                    function = [funD sname [clause pats (normalB [|inject (hdimap Var id $val)|]) []]]+                sequence $ sig ++ function+              genSig targs tname sname 0 miTp = (:[]) $ do+                hvar <- newName "h"+                fvar <- newName "f"+                avar <- newName "a"+                bvar <- newName "b"+                ivar <- newName "i"+                let targs' = init $ init $ init targs+                    vars = hvar:fvar:avar:bvar:maybe [ivar] (const []) miTp++targs'+                    h = varT hvar+                    f = varT fvar+                    a = varT avar+                    b = varT bvar+                    i = varT ivar+                    ftype = foldl appT (conT tname) (map varT targs')+                    constr = classP ''(:<:) [ftype, f]+                    typ = foldl appT (conT ''Cxt) [h, f, a, b,maybe i return miTp]+                    typeSig = forallT (map PlainTV vars) (sequence [constr]) typ+                sigD sname typeSig+              genSig _ _ _ _ _ = []
+ src/Data/Comp/Param/Multi/Desugar.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,+  UndecidableInstances, OverlappingInstances, TypeOperators, Rank2Types #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Desugar+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This modules defines the 'Desugar' type class for desugaring of terms.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Desugar where++import Data.Comp.Param.Multi++-- |The desugaring term homomorphism.+class (HDifunctor f, HDifunctor g) => Desugar f g where+    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)++-- We make the lifting to sums explicit in order to make the Desugar+-- class work with the default instance declaration further below.+instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where+    desugHom = caseHD desugHom desugHom+++-- |Desugar a term.+desugar :: Desugar f g => Term f :-> Term g+desugar (Term t) = Term (appHom desugHom t)++-- |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 (Term t) = Term (appHom (propAnn desugHom) t)++-- |Default desugaring instance.+instance (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g where+    desugHom = simpCxt . inj
+ src/Data/Comp/Param/Multi/Equality.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,+  UndecidableInstances, IncoherentInstances, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Equality+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines equality for signatures, which lifts to equality for+-- terms.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi.Equality+    (+     PEq(..),+     EqHD(..)+    ) where++import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.Sum+import Data.Comp.Param.Multi.Ops+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.FreshM++-- |Equality on parametric values. The equality test is performed inside the+-- 'FreshM' monad for generating fresh identifiers.+class PEq a where+    peq :: a i -> a j -> FreshM Bool++instance Eq a => PEq (K a) where+    peq (K x) (K y) = return $ x == y++{-| Signature equality. An instance @EqHD f@ gives rise to an instance+  @Eq (Term f i)@. The equality test is performed inside the 'FreshM' monad for+  generating fresh identifiers. -}+class EqHD f where+    eqHD :: PEq a => f Name a i -> f Name a j -> FreshM Bool++{-| 'EqHD' is propagated through sums. -}+instance (EqHD f, EqHD g) => EqHD (f :+: g) where+    eqHD (Inl x) (Inl y) = eqHD x y+    eqHD (Inr x) (Inr y) = eqHD x y+    eqHD _ _ = return False++instance PEq Name where+   peq x y = return $ nameCoerce x == y++{-| From an 'EqHD' difunctor an 'Eq' instance of the corresponding term type can+  be derived. -}+instance EqHD f => EqHD (Cxt h f) where+    eqHD (In e1) (In e2) = eqHD e1 e2+    eqHD (Hole h1) (Hole h2) = peq h1 h2+    eqHD (Var p1) (Var p2) = peq p1 p2+    eqHD _ _ = return False++instance (EqHD f, PEq a) => PEq (Cxt h f Name a) where+    peq = eqHD++{-| Equality on terms. -}+instance (HDifunctor f, EqHD f) => Eq (Term f i) where+    (==) (Term x) (Term y) = evalFreshM $ eqHD x y
+ src/Data/Comp/Param/Multi/FreshM.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.FreshM+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines a monad for generating fresh, abstract names, useful+-- e.g. for defining equality on terms.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi.FreshM+    (+     FreshM,+     Name,+     withName,+     nameCoerce,+     evalFreshM+    ) where++import Control.Monad.Reader+import Control.Applicative++-- |Monad for generating fresh (abstract) names.+newtype FreshM a = FreshM{unFreshM :: Reader Int a}+    deriving (Monad, Functor, Applicative)++-- |Abstract notion of a name (the constructor is hidden).+newtype Name i = Name Int+    deriving Eq++instance Show (Name i) where+    show (Name x) = names !! x+        where baseNames = ['a'..'z']+              names = map (:[]) baseNames ++ names' 1+              names' n = map (: show n) baseNames ++ names' (n + 1)++instance Ord (Name i) where+    compare (Name x) (Name y) = compare x y++-- |Change the type tag of a name.+nameCoerce :: Name i -> Name j+nameCoerce (Name x) = Name x++-- |Run the given computation with the next available name.+withName :: (Name i -> FreshM a) -> FreshM a+withName m = do name <- FreshM (asks Name)+                FreshM $ local ((+) 1) $ unFreshM $ m name++-- |Evaluate a computation that uses fresh names.+evalFreshM :: FreshM a -> a+evalFreshM (FreshM m) = runReader m 0
+ src/Data/Comp/Param/Multi/HDifunctor.hs view
@@ -0,0 +1,40 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, Rank2Types,+  TypeOperators, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.HDifunctor+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines higher-order difunctors, a hybrid between higher-order+-- functors (Johann, Ghani, POPL '08), and difunctors (Meijer, Hutton, FPCA+-- '95). Higher-order difunctors are used to define signatures for+-- compositional parametric generalised data types.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.HDifunctor+    (+     HDifunctor (..),+     HFunctor (..),+     I (..),+     K (..),+     E (..),+     A (..),+     (:->),+     NatM+    ) where++import Data.Comp.Multi.HFunctor++-- | This class represents higher-order difunctors.+class HDifunctor f where+    hdimap :: (a :-> b) -> (c :-> d) -> f b c :-> f a d++-- |A higher-order difunctor gives rise to a higher-order functor when+-- restricted to a particular contravariant argument.+instance HDifunctor f => HFunctor (f a) where+    hfmap = hdimap id
+ src/Data/Comp/Param/Multi/HDitraversable.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE Rank2Types, FlexibleInstances, MultiParamTypeClasses,+  FlexibleContexts, OverlappingInstances, TypeOperators, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.HDitraversable+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines traversable higher-order difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.HDitraversable+    (+     HDitraversable (..),+     HTraversable (..)+    ) where++import Prelude hiding (mapM, sequence, foldr)+import Data.Comp.Multi.HTraversable+import Data.Comp.Param.Multi.HDifunctor++{-| HDifunctors representing data structures that can be traversed from left to+  right. -}+class HDifunctor f => HDitraversable f where+    hdimapM :: Monad m => NatM m b c -> NatM m (f a b) (f a c)
+ src/Data/Comp/Param/Multi/Ops.hs view
@@ -0,0 +1,126 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies,+  FlexibleInstances, UndecidableInstances, IncoherentInstances,+  KindSignatures, RankNTypes #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Ops+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module provides operators on higher-order difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Ops where++import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.HDitraversable+import qualified Data.Comp.Ops as O+import Control.Monad (liftM)+++-- Sums+infixr 6 :+:++-- |Formal sum of signatures (difunctors).+data (f :+: g) (a :: * -> *) (b :: * -> *) i = Inl (f a b i)+                                             | Inr (g a b i)++{-| Utility function to case on a higher-order difunctor sum, without exposing+  the internal representation of sums. -}+caseHD :: (f a b i -> c) -> (g a b i -> c) -> (f :+: g) a b i -> c+caseHD f g x = case x of+                 Inl x -> f x+                 Inr x -> g x++instance (HDifunctor f, HDifunctor g) => HDifunctor (f :+: g) where+    hdimap f g (Inl e) = Inl (hdimap f g e)+    hdimap f g (Inr e) = Inr (hdimap f g e)++instance (HDitraversable f, HDitraversable g) => HDitraversable (f :+: g) where+    hdimapM f (Inl e) = Inl `liftM` hdimapM f e+    hdimapM f (Inr e) = Inr `liftM` hdimapM f e++-- | Signature containment relation for automatic injections. The left-hand must+-- be an atomic signature, where as the right-hand side must have a list-like+-- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,+-- non-examples include @f :+: g :<: f :+: (g :+: h)@ and+-- @f :<: (f :+: g) :+: h@.+class (sub :: (* -> *) -> (* -> *) -> * -> *) :<: sup where+    inj :: sub a b :-> sup a b+    proj :: NatM Maybe (sup a b) (sub a b)++instance (:<:) f f where+    inj = id+    proj = Just++instance (:<:) f (f :+: g) where+    inj = Inl+    proj (Inl x) = Just x+    proj (Inr _) = Nothing++instance (f :<: g) => (:<:) f (h :+: g) where+    inj = Inr . inj+    proj (Inr x) = proj x+    proj (Inl _) = Nothing+++-- Products+infixr 8 :*:++-- |Formal product of signatures (higher-order difunctors).+data (f :*: g) a b = f a b :*: g a b++ffst :: (f :*: g) a b -> f a b+ffst (x :*: _) = x++fsnd :: (f :*: g) a b -> g a b +fsnd (_ :*: x) = x+++-- Constant Products+infixr 7 :&:++{-| This data type adds a constant product to a signature. -}+data (f :&: p) (a :: * -> *) (b :: * -> *) i = f a b i :&: p++instance HDifunctor f => HDifunctor (f :&: p) where+    hdimap f g (v :&: c) = hdimap f g v :&: c++instance HDitraversable f => HDitraversable (f :&: p) where+    hdimapM f (v :&: c) = liftM (:&: c) (hdimapM f v)++{-| This class defines how to distribute an annotation over a sum of+  signatures. -}+class DistAnn (s :: (* -> *) -> (* -> *) -> * -> *) p s' | s' -> s, s' -> p where+    {-| Inject an annotation over a signature. -}+    injectA :: p -> s a b :-> s' a b+    {-| Project an annotation from a signature. -}+    projectA :: s' a b :-> (s a b O.:&: p)++class RemA (s :: (* -> *) -> (* -> *) -> * -> *) s' | s -> s' where+    {-| Remove annotations from a signature. -}+    remA :: s a b :-> s' a b++instance (RemA s s') => RemA (f :&: p :+: s) (f :+: s') where+    remA (Inl (v :&: _)) = Inl v+    remA (Inr v) = Inr $ remA v++instance RemA (f :&: p) f where+    remA (v :&: _) = v++instance DistAnn f p (f :&: p) where+    injectA c v = v :&: c++    projectA (v :&: p) = v O.:&: p++instance (DistAnn s p s') => DistAnn (f :+: s) p ((f :&: p) :+: s') where+    injectA c (Inl v) = Inl (v :&: c)+    injectA c (Inr v) = Inr $ injectA c v++    projectA (Inl (v :&: p)) = Inl v O.:&: p+    projectA (Inr v) = let (v' O.:&: p) = projectA v+                       in Inr v' O.:&: p
+ src/Data/Comp/Param/Multi/Ordering.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,+  UndecidableInstances, IncoherentInstances, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Ordering+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines ordering of signatures, which lifts to ordering of+-- terms and contexts.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi.Ordering+    (+     POrd(..),+     OrdHD(..)+    ) where++import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.Sum+import Data.Comp.Param.Multi.Ops+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.FreshM+import Data.Comp.Param.Multi.Equality++-- |Ordering of parametric values.+class PEq a => POrd a where+    pcompare :: a i -> a j -> FreshM Ordering++instance Ord a => POrd (K a) where+    pcompare (K x) (K y) = return $ compare x y++{-| Signature ordering. An instance @OrdHD f@ gives rise to an instance+  @Ord (Term f)@. -}+class EqHD f => OrdHD f where+    compareHD :: POrd a => f Name a i -> f Name a j -> FreshM Ordering++{-| 'OrdHD' is propagated through sums. -}+instance (OrdHD f, OrdHD g) => OrdHD (f :+: g) where+    compareHD (Inl x) (Inl y) = compareHD x y+    compareHD (Inl _) (Inr _) = return LT+    compareHD (Inr x) (Inr y) = compareHD x y+    compareHD (Inr _) (Inl _) = return GT++{-| From an 'OrdHD' difunctor an 'Ord' instance of the corresponding term type+  can be derived. -}+instance OrdHD f => OrdHD (Cxt h f) where+    compareHD (In e1) (In e2) = compareHD e1 e2+    compareHD (Hole h1) (Hole h2) = pcompare h1 h2+    compareHD (Var p1) (Var p2) = pcompare p1 p2+    compareHD (In _) _ = return LT+    compareHD (Hole _) (In _) = return GT+    compareHD (Hole _) (Var _) = return LT+    compareHD (Var _) _ = return GT++instance POrd Name where+    pcompare x y = return $ compare (nameCoerce x) y++instance (OrdHD f, POrd a) => POrd (Cxt h f Name a) where+    pcompare = compareHD++{-| Ordering of terms. -}+instance (HDifunctor f, OrdHD f) => Ord (Term f i) where+    compare (Term x) (Term y) = evalFreshM $ compareHD x y
+ src/Data/Comp/Param/Multi/Show.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE TypeOperators, FlexibleInstances, TypeSynonymInstances,+  IncoherentInstances, UndecidableInstances, TemplateHaskell, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Show+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines showing of signatures, which lifts to showing of terms.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Multi.Show+    (+     ShowHD(..)+    ) where++import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.Ops+import Data.Comp.Param.Multi.Derive+import Data.Comp.Param.Multi.FreshM++-- Lift ShowHD to sums+$(derive [liftSum] [''ShowHD])++{-| From an 'ShowHD' higher-order difunctor an 'ShowHD' instance of the+  corresponding term type can be derived. -}+instance (HDifunctor f, ShowHD f) => ShowHD (Cxt h f) where+    showHD (In t) = showHD $ hfmap (K . showHD) t+    showHD (Hole h) = unK h+    showHD (Var p) = return $ show p++{-| Printing of terms. -}+instance (HDifunctor f, ShowHD f) => Show (Term f i) where+    show = evalFreshM . showHD . toCxt . unTerm++instance (ShowHD f, Show p) => ShowHD (f :&: p) where+    showHD (x :&: p) = do sx <- showHD x+                          return $ sx ++ " :&: " ++ show p
+ src/Data/Comp/Param/Multi/Sum.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,+  FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,+  ScopedTypeVariables, TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Sum+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module provides the infrastructure to extend signatures.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Sum+    (+     (:<:),+     (:+:),+     caseHD,++     -- * Projections for Signatures and Terms+     proj,+     proj2,+     proj3,+     proj4,+     proj5,+     proj6,+     proj7,+     proj8,+     proj9,+     proj10,+     project,+     project2,+     project3,+     project4,+     project5,+     project6,+     project7,+     project8,+     project9,+     project10,+     deepProject,+     deepProject2,+     deepProject3,+     deepProject4,+     deepProject5,+     deepProject6,+     deepProject7,+     deepProject8,+     deepProject9,+     deepProject10,++     -- * Injections for Signatures and Terms+     inj,+     inj2,+     inj3,+     inj4,+     inj5,+     inj6,+     inj7,+     inj8,+     inj9,+     inj10,+     inject,+     inject2,+     inject3,+     inject4,+     inject5,+     inject6,+     inject7,+     inject8,+     inject9,+     inject10,+     deepInject,+     deepInject2,+     deepInject3,+     deepInject4,+     deepInject5,+     deepInject6,+     deepInject7,+     deepInject8,+     deepInject9,+     deepInject10,++     injectCxt,+     liftCxt+    ) where++import Prelude hiding (sequence)+import Control.Monad hiding (sequence)+import Data.Comp.Param.Multi.Term+import Data.Comp.Param.Multi.Algebra+import Data.Comp.Param.Multi.Ops+import Data.Comp.Param.Multi.Derive.Projections+import Data.Comp.Param.Multi.Derive.Injections+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.HDitraversable++$(liftM concat $ mapM projn [2..10])++-- |Project the outermost layer of a term to a sub signature. If the signature+-- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.+project :: (g :<: f) => NatM Maybe (Cxt h f a b) (g a (Cxt h f a b))+project (In t)   = proj t+project (Hole _) = Nothing+project (Var _)  = Nothing++$(liftM concat $ mapM projectn [2..10])++-- | Tries to coerce a term/context to a term/context over a sub-signature. If+-- the signature @g@ is compound of /n/ atomic signatures, use+-- @deepProject@/n/ instead.+deepProject :: (HDitraversable g, g :<: f) => Term f i -> Maybe (Term g i)+{-# INLINE deepProject #-}+deepProject = appTSigFunM' proj++$(liftM concat $ mapM deepProjectn [2..10])+{-# INLINE deepProject2 #-}+{-# INLINE deepProject3 #-}+{-# INLINE deepProject4 #-}+{-# INLINE deepProject5 #-}+{-# INLINE deepProject6 #-}+{-# INLINE deepProject7 #-}+{-# INLINE deepProject8 #-}+{-# INLINE deepProject9 #-}+{-# INLINE deepProject10 #-}++$(liftM concat $ mapM injn [2..10])++-- |Inject a term where the outermost layer is a sub signature. If the signature+-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.+inject :: (g :<: f) => g a (Cxt h f a b) :-> Cxt h f a b+inject = In . inj++$(liftM concat $ mapM injectn [2..10])++-- |Inject a term over a sub signature to a term over larger signature. If the+-- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/+-- instead.+deepInject :: (HDifunctor g, g :<: f) => CxtFun g f+{-# INLINE deepInject #-}+deepInject = appSigFun inj++$(liftM concat $ mapM deepInjectn [2..10])+{-# INLINE deepInject2 #-}+{-# INLINE deepInject3 #-}+{-# INLINE deepInject4 #-}+{-# INLINE deepInject5 #-}+{-# INLINE deepInject6 #-}+{-# INLINE deepInject7 #-}+{-# INLINE deepInject8 #-}+{-# INLINE deepInject9 #-}+{-# INLINE deepInject10 #-}++{-| This function injects a whole context into another context. -}+injectCxt :: (HDifunctor g, g :<: f) => Cxt h g a (Cxt h f a b) :-> Cxt h f a b+injectCxt (In t) = inject $ hfmap injectCxt t+injectCxt (Hole x) = x+injectCxt (Var p) = Var p++{-| This function lifts the given functor to a context. -}+liftCxt :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a b+liftCxt g = simpCxt $ inj g++instance (Show (f a b i), Show (g a b i)) => Show ((f :+: g) a b i) where+    show (Inl v) = show v+    show (Inr v) = show v++instance (Ord (f a b i), Ord (g a b i)) => Ord ((f :+: g) a b i) where+    compare (Inl _) (Inr _) = LT+    compare (Inr _) (Inl _) = GT+    compare (Inl x) (Inl y) = compare x y+    compare (Inr x) (Inr y) = compare x y++instance (Eq (f a b i), Eq (g a b i)) => Eq ((f :+: g) a b i) where+    (Inl x) == (Inl y) = x == y+    (Inr x) == (Inr y) = x == y                   +    _ == _ = False
+ src/Data/Comp/Param/Multi/Term.hs view
@@ -0,0 +1,126 @@+{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,+  MultiParamTypeClasses, TypeOperators, ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Multi.Term+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines the central notion of /generalised parametrised terms/+-- and their generalisation to generalised parametrised contexts.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Multi.Term+    (+     Cxt(..),+     Hole,+     NoHole,+     Term(..),+     Trm,+     Context,+     simpCxt,+     toCxt,+     hfmapCxt,+     hdimapMCxt,+     ParamFunctor (..)+    ) where++import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)+import Data.Comp.Param.Multi.HDifunctor+import Data.Comp.Param.Multi.HDitraversable+import Control.Monad +import Unsafe.Coerce+import Data.Maybe (fromJust)++{-| This data type represents contexts over a signature. Contexts are terms+  containing zero or more holes, and zero or more parameters. The first+  parameter is a phantom type indicating whether the context has holes. The+  second paramater is the signature of the context, in the form of a+  "Data.Comp.Param.Multi.HDifunctor". The third parameter is the type of+  parameters, the fourth parameter is the type of holes, and the fifth+  parameter is the GADT type. -}+data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> * where+            In :: f a (Cxt h f a b) i -> Cxt h f a b i+            Hole :: b i -> Cxt Hole f a b i+            Var :: a i -> Cxt h f a b i++{-| Phantom type used to define 'Context'. -}+data Hole++{-| Phantom type used to define 'Term'. -}+data NoHole++{-| A context may contain holes. -}+type Context = Cxt Hole++{-| \"Preterms\" |-}+type Trm f a = Cxt NoHole f a (K ())++{-| A term is a context with no holes, where all occurrences of the+  contravariant parameter is fully parametric. -}+newtype Term f i = Term{unTerm :: forall a. Trm f a i}++{-| Convert a difunctorial value into a context. -}+simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b+{-# INLINE simpCxt #-}+simpCxt = In . hfmap Hole++toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b+{-# INLINE toCxt #-}+toCxt = unsafeCoerce++-- | This is an instance of 'hfmap' for 'Cxt'.+hfmapCxt :: forall h f a b b'. HDifunctor f+         => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'+hfmapCxt f = run+    where run :: Cxt h f a b :-> Cxt h f a b'+          run (In t)   = In $ hfmap run t+          run (Var a)  = Var a+          run (Hole b) = Hole $ f b++-- | This is an instance of 'hdimapM' for 'Cxt'.+hdimapMCxt :: forall h f a b b' m . (HDitraversable f, Monad m)+          => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')+hdimapMCxt f = run+    where run :: NatM m (Cxt h f a b) (Cxt h f a b')+          run (In t)   = liftM In $ hdimapM run t+          run (Var a)  = return $ Var a+          run (Hole b) = liftM Hole (f b)+          +          +          +{-| Monads for which embedded @Trm@ values, which are parametric at top level,+  can be made into monadic @Term@ values, i.e. \"pushing the parametricity+  inwards\". -}+class ParamFunctor m where+    termM :: (forall a. m (Trm f a i)) -> m (Term f i)++coerceTermM :: ParamFunctor m => (forall a. m (Trm f a i)) -> m (Term f i)+{-# INLINE coerceTermM #-}+coerceTermM t = unsafeCoerce t++{-# RULES+    "termM/coerce'" termM = coerceTermM+ #-}++instance ParamFunctor Maybe where+    {-# NOINLINE [1] termM #-}+    termM Nothing = Nothing+    termM x       = Just (Term $ fromJust x)++instance ParamFunctor (Either a) where+    {-# NOINLINE [1] termM #-}+    termM (Left x) = Left x+    termM x        = Right (Term $ fromRight x)+                             where fromRight :: Either a b -> b+                                   fromRight (Right x) = x+                                   fromRight _ = error "fromRight: Left"++instance ParamFunctor [] where+    {-# NOINLINE [1] termM #-}+    termM [] = []+    termM l  = Term (head l) : termM (tail l)
+ src/Data/Comp/Param/Ops.hs view
@@ -0,0 +1,127 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies,+  FlexibleInstances, UndecidableInstances, IncoherentInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Ops+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module provides operators on difunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Ops where++import Data.Comp.Param.Difunctor+import Data.Comp.Param.Ditraversable+import Control.Monad (liftM)+++-- Sums+infixr 6 :+:++-- |Formal sum of signatures (difunctors).+data (f :+: g) a b = Inl (f a b)+                   | Inr (g a b)++{-| Utility function to case on a difunctor sum, without exposing the internal+  representation of sums. -}+caseD :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c+caseD f g x = case x of+                Inl x -> f x+                Inr x -> g x++instance (Difunctor f, Difunctor g) => Difunctor (f :+: g) where+    dimap f g (Inl e) = Inl (dimap f g e)+    dimap f g (Inr e) = Inr (dimap f g e)++instance (Ditraversable f, Ditraversable g) => Ditraversable (f :+: g) where+    dimapM f (Inl e) = Inl `liftM` dimapM f e+    dimapM f (Inr e) = Inr `liftM` dimapM f e+    disequence (Inl e) = Inl `liftM` disequence e+    disequence (Inr e) = Inr `liftM` disequence e++-- | Signature containment relation for automatic injections. The left-hand must+-- be an atomic signature, where as the right-hand side must have a list-like+-- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,+-- non-examples include @f :+: g :<: f :+: (g :+: h)@ and+-- @f :<: (f :+: g) :+: h@.+class sub :<: sup where+  inj :: sub a b -> sup a b+  proj :: sup a b -> Maybe (sub a b)++instance (:<:) f f where+    inj = id+    proj = Just++instance (:<:) f (f :+: g) where+    inj = Inl+    proj (Inl x) = Just x+    proj (Inr _) = Nothing++instance (f :<: g) => (:<:) f (h :+: g) where+    inj = Inr . inj+    proj (Inr x) = proj x+    proj (Inl _) = Nothing+++-- Products+infixr 8 :*:++-- |Formal product of signatures (difunctors).+data (f :*: g) a b = f a b :*: g a b++ffst :: (f :*: g) a b -> f a b+ffst (x :*: _) = x++fsnd :: (f :*: g) a b -> g a b+fsnd (_ :*: x) = x+++-- Constant Products+infixr 7 :&:++{-| This data type adds a constant product to a signature. -}+data (f :&: p) a b = f a b :&: p++instance Difunctor f => Difunctor (f :&: p) where+    dimap f g (v :&: c) = dimap f g v :&: c++instance Ditraversable f => Ditraversable (f :&: p) where+    dimapM f (v :&: c) = liftM (:&: c) (dimapM f v)+    disequence (v :&: c) = liftM (:&: c) (disequence v)++{-| This class defines how to distribute an annotation over a sum of+  signatures. -}+class DistAnn s p s' | s' -> s, s' -> p where+    {-| Inject an annotation over a signature. -}+    injectA :: p -> s a b -> s' a b+    {-| Project an annotation from a signature. -}+    projectA :: s' a b -> (s a b, p)++class RemA s s' | s -> s'  where+    {-| Remove annotations from a signature. -}+    remA :: s a b -> s' a b++instance (RemA s s') => RemA (f :&: p :+: s) (f :+: s') where+    remA (Inl (v :&: _)) = Inl v+    remA (Inr v) = Inr $ remA v++instance RemA (f :&: p) f where+    remA (v :&: _) = v++instance DistAnn f p (f :&: p) where+    injectA c v = v :&: c++    projectA (v :&: p) = (v,p)++instance (DistAnn s p s') => DistAnn (f :+: s) p ((f :&: p) :+: s') where+    injectA c (Inl v) = Inl (v :&: c)+    injectA c (Inr v) = Inr $ injectA c v++    projectA (Inl (v :&: p)) = (Inl v,p)+    projectA (Inr v) = let (v',p) = projectA v+                       in  (Inr v',p)
+ src/Data/Comp/Param/Ordering.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,+  UndecidableInstances, IncoherentInstances, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Ordering+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines ordering of signatures, which lifts to ordering of+-- terms and contexts.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Ordering+    (+     POrd(..),+     OrdD(..),+     compList+    ) where++import Data.Comp.Param.Term+import Data.Comp.Param.Sum+import Data.Comp.Param.Ops+import Data.Comp.Param.Difunctor+import Data.Comp.Param.FreshM+import Data.Comp.Param.Equality+import Data.Maybe (fromMaybe)+import Data.List (find)+import Control.Monad (liftM)++-- |Ordering of parametric values.+class PEq a => POrd a where+    pcompare :: a -> a -> FreshM Ordering++instance POrd a => POrd [a] where+    pcompare l1 l2+        | length l1 < length l2 = return LT+        | length l1 > length l2 = return GT+        | otherwise = liftM compList $ mapM (uncurry pcompare) $ zip l1 l2++compList :: [Ordering] -> Ordering+compList = fromMaybe EQ . find (/= EQ)++instance Ord a => POrd a where+    pcompare x y = return $ compare x y++{-| Signature ordering. An instance @OrdD f@ gives rise to an instance+  @Ord (Term f)@. -}+class EqD f => OrdD f where+    compareD :: POrd a => f Name a -> f Name a -> FreshM Ordering++{-| 'OrdD' is propagated through sums. -}+instance (OrdD f, OrdD g) => OrdD (f :+: g) where+    compareD (Inl x) (Inl y) = compareD x y+    compareD (Inl _) (Inr _) = return LT+    compareD (Inr x) (Inr y) = compareD x y+    compareD (Inr _) (Inl _) = return GT++{-| From an 'OrdD' difunctor an 'Ord' instance of the corresponding term type+  can be derived. -}+instance OrdD f => OrdD (Cxt h f) where+    compareD (In e1) (In e2) = compareD e1 e2+    compareD (Hole h1) (Hole h2) = pcompare h1 h2+    compareD (Var p1) (Var p2) = pcompare p1 p2+    compareD (In _) _ = return LT+    compareD (Hole _) (In _) = return GT+    compareD (Hole _) (Var _) = return LT+    compareD (Var _) _ = return GT++instance (OrdD f, POrd a) => POrd (Cxt h f Name a) where+    pcompare = compareD++{-| Ordering of terms. -}+instance (Difunctor f, OrdD f) => Ord (Term f) where+    compare (Term x) (Term y) = evalFreshM $ compareD x y
+ src/Data/Comp/Param/Show.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE TypeOperators, FlexibleInstances, TypeSynonymInstances,+  IncoherentInstances, UndecidableInstances, TemplateHaskell, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Show+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines showing of signatures, which lifts to showing of terms.+--+--------------------------------------------------------------------------------+module Data.Comp.Param.Show+    (+     ShowD(..)+    ) where++import Data.Comp.Param.Term+import Data.Comp.Param.Ops+import Data.Comp.Param.Derive+import Data.Comp.Param.FreshM++-- Lift ShowD to sums+$(derive [liftSum] [''ShowD])++{-| From an 'ShowD' difunctor an 'ShowD' instance of the corresponding term type+  can be derived. -}+instance (Difunctor f, ShowD f) => ShowD (Cxt h f) where+    showD (In t) = showD $ fmap showD t+    showD (Hole h) = h+    showD (Var p) = return $ show p++{-| Printing of terms. -}+instance (Difunctor f, ShowD f) => Show (Term f) where+    show = evalFreshM . showD . toCxt . unTerm++instance (ShowD f, Show p) => ShowD (f :&: p) where+    showD (x :&: p) = do sx <- showD x+                         return $ sx ++ " :&: " ++ show p
+ src/Data/Comp/Param/Sum.hs view
@@ -0,0 +1,186 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,+  FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,+  ScopedTypeVariables, TemplateHaskell, Rank2Types #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Sum+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module provides the infrastructure to extend signatures.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Sum+    (+     (:<:),+     (:+:),+     caseD,++     -- * Projections for Signatures and Terms+     proj,+     proj2,+     proj3,+     proj4,+     proj5,+     proj6,+     proj7,+     proj8,+     proj9,+     proj10,+     project,+     project2,+     project3,+     project4,+     project5,+     project6,+     project7,+     project8,+     project9,+     project10,+     deepProject,+     deepProject2,+     deepProject3,+     deepProject4,+     deepProject5,+     deepProject6,+     deepProject7,+     deepProject8,+     deepProject9,+     deepProject10,++     -- * Injections for Signatures and Terms+     inj,+     inj2,+     inj3,+     inj4,+     inj5,+     inj6,+     inj7,+     inj8,+     inj9,+     inj10,+     inject,+     inject',+     inject2,+     inject3,+     inject4,+     inject5,+     inject6,+     inject7,+     inject8,+     inject9,+     inject10,+     deepInject,+     deepInject2,+     deepInject3,+     deepInject4,+     deepInject5,+     deepInject6,+     deepInject7,+     deepInject8,+     deepInject9,+     deepInject10,++     injectCxt,+     liftCxt+    ) where++import Prelude hiding (sequence)+import Control.Monad hiding (sequence)+import Data.Comp.Param.Term+import Data.Comp.Param.Algebra+import Data.Comp.Param.Ops+import Data.Comp.Param.Derive.Projections+import Data.Comp.Param.Derive.Injections+import Data.Comp.Param.Difunctor+import Data.Comp.Param.Ditraversable++$(liftM concat $ mapM projn [2..10])++-- |Project the outermost layer of a term to a sub signature. If the signature+-- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.+project :: (g :<: f) => Cxt h f a b -> Maybe (g a (Cxt h f a b))+project (In t) = proj t+project (Hole _) = Nothing+project (Var _) = Nothing++$(liftM concat $ mapM projectn [2..10])++-- | Tries to coerce a term/context to a term/context over a sub-signature. If+-- the signature @g@ is compound of /n/ atomic signatures, use+-- @deepProject@/n/ instead.+deepProject :: (Ditraversable g, g :<: f) => Term f -> Maybe (Term g)+{-# INLINE deepProject #-}+deepProject = appTSigFunM' proj++$(liftM concat $ mapM deepProjectn [2..10])+{-# INLINE deepProject2 #-}+{-# INLINE deepProject3 #-}+{-# INLINE deepProject4 #-}+{-# INLINE deepProject5 #-}+{-# INLINE deepProject6 #-}+{-# INLINE deepProject7 #-}+{-# INLINE deepProject8 #-}+{-# INLINE deepProject9 #-}+{-# INLINE deepProject10 #-}++$(liftM concat $ mapM injn [2..10])++-- |Inject a term where the outermost layer is a sub signature. If the signature+-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.+inject :: (g :<: f) => g a (Cxt h f a b) -> Cxt h f a b+inject = In . inj++-- |Inject a term where the outermost layer is a sub signature. If the signature+-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.+inject' :: (Difunctor g, g :<: f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a b+inject' = inject . dimap Var id++$(liftM concat $ mapM injectn [2..10])++-- |Inject a term over a sub signature to a term over larger signature. If the+-- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/+-- instead.+deepInject :: (Difunctor g, g :<: f) => Term g -> Term f+{-# INLINE deepInject #-}+deepInject (Term t) = Term (appSigFun inj t)++$(liftM concat $ mapM deepInjectn [2..10])+{-# INLINE deepInject2 #-}+{-# INLINE deepInject3 #-}+{-# INLINE deepInject4 #-}+{-# INLINE deepInject5 #-}+{-# INLINE deepInject6 #-}+{-# INLINE deepInject7 #-}+{-# INLINE deepInject8 #-}+{-# INLINE deepInject9 #-}+{-# INLINE deepInject10 #-}++{-| 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 (In t) = inject $ difmap injectCxt t+injectCxt (Hole x) = x+injectCxt (Var p) = Var p++{-| This function lifts the given functor to a context. -}+liftCxt :: (Difunctor f, g :<: f) => g a b -> Cxt Hole f a b+liftCxt g = simpCxt $ inj g++instance (Show (f a b), Show (g a b)) => Show ((f :+: g) a b) where+    show (Inl v) = show v+    show (Inr v) = show v++instance (Ord (f a b), Ord (g a b)) => Ord ((f :+: g) a b) where+    compare (Inl _) (Inr _) = LT+    compare (Inr _) (Inl _) = GT+    compare (Inl x) (Inl y) = compare x y+    compare (Inr x) (Inr y) = compare x y++instance (Eq (f a b), Eq (g a b)) => Eq ((f :+: g) a b) where+    (Inl x) == (Inl y) = x == y+    (Inr x) == (Inr y) = x == y                   +    _ == _ = False
+ src/Data/Comp/Param/Term.hs view
@@ -0,0 +1,112 @@+{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,+  MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Term+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines the central notion of /parametrised terms/ and their+-- generalisation to parametrised contexts.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Term+    (+     Cxt(..),+     Hole,+     NoHole,+     Term(..),+     Trm,+     Context,+     simpCxt,+     toCxt,+     cxtMap,+     ParamFunctor(..)+    ) where++import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)+import Data.Comp.Param.Difunctor+import Unsafe.Coerce (unsafeCoerce)++import Data.Maybe (fromJust)++{-| This data type represents contexts over a signature. Contexts are terms+  containing zero or more holes, and zero or more parameters. The first+  parameter is a phantom type indicating whether the context has holes. The+  second paramater is the signature of the context, in the form of a+  "Data.Comp.Param.Difunctor". The third parameter is the type of parameters,+  and the fourth parameter is the type of holes. -}+data Cxt :: * -> (* -> * -> *) -> * -> * -> * where+            In :: f a (Cxt h f a b) -> Cxt h f a b+            Hole :: b -> Cxt Hole f a b+            Var :: a -> Cxt h f a b++{-| Phantom type used to define 'Context'. -}+data Hole++{-| Phantom type used to define 'Term'. -}+data NoHole++{-| A context may contain holes. -}+type Context = Cxt Hole++{-| \"Preterms\" -}+type Trm f a = Cxt NoHole f a ()++{-| A term is a context with no holes, where all occurrences of the+  contravariant parameter is fully parametric. -}+newtype Term f = Term{unTerm :: forall a. Trm f a}++{-| Convert a difunctorial value into a context. -}+simpCxt :: Difunctor f => f a b -> Cxt Hole f a b+{-# INLINE simpCxt #-}+simpCxt = In . difmap Hole++toCxt :: Difunctor f => Trm f a -> Cxt h f a b+{-# INLINE toCxt #-}+toCxt = unsafeCoerce++-- | This combinator maps a function over a context by applying the+-- function to each hole.+cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c+cxtMap f (Hole x) = Hole (f x)+cxtMap _ (Var x)  = Var x+cxtMap f (In t)   = In (dimap id (cxtMap f) t)++-- Param Functor++{-| Monads for which embedded @Trm@ values, which are parametric at top level,+  can be made into monadic @Term@ values, i.e. \"pushing the parametricity+  inwards\". -}+class ParamFunctor m where+    termM :: (forall a. m (Trm f a)) -> m (Term f)++coerceTermM :: ParamFunctor m => (forall a. m (Trm f a)) -> m (Term f)+{-# INLINE coerceTermM #-}+coerceTermM t = unsafeCoerce t++{-# RULES+    "termM/coerce" termM = coerceTermM+ #-}++instance ParamFunctor Maybe where+    {-# NOINLINE [1] termM #-}+    termM Nothing = Nothing+    termM x       = Just (Term $ fromJust x)++instance ParamFunctor (Either a) where+    {-# NOINLINE [1] termM #-}+    termM (Left x) = Left x+    termM x        = Right (Term $ fromRight x)+                             where fromRight :: Either a b -> b+                                   fromRight (Right x) = x+                                   fromRight _ = error "fromRight: Left"++instance ParamFunctor [] where+    {-# NOINLINE [1] termM #-}+    termM [] = []+    termM l  = Term (head l) : termM (tail l)
+ src/Data/Comp/Param/Thunk.hs view
@@ -0,0 +1,127 @@+{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, GADTs #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Param.Thunk+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This modules defines terms & contexts with thunks, with deferred+-- monadic computations.+--+--------------------------------------------------------------------------------++module Data.Comp.Param.Thunk+    (TermT+    ,TrmT+    ,CxtT+    ,Thunk+    ,thunk+    ,whnf+    ,whnf'+    ,whnfPr+    ,nf+    ,nfT+    ,nfPr+    ,nfTPr+    ,evalStrict+    ,AlgT+    ,strict+    ,strict')+ where++import Data.Comp.Param.Term+import Data.Comp.Param.Sum+import Data.Comp.Param.Ops+import Data.Comp.Param.Algebra+import Data.Comp.Param.Ditraversable+import Data.Comp.Param.Difunctor++import Control.Monad++-- | This type represents terms with thunks.+type TermT m f = Term (Thunk m :+: f)++-- | This type represents terms with thunks.+type TrmT m f a = Trm  (Thunk m :+: f) a++-- | This type represents contexts with thunks.+type CxtT h  m f a = Cxt h (Thunk m :+: f) a++newtype Thunk m a b = Thunk (m b)++-- | This function turns a monadic computation into a thunk.+thunk :: (Thunk m :<: f) => m (Cxt h f a b) -> Cxt h f a b+thunk = inject . Thunk++-- | This function evaluates all thunks until a non-thunk node is+-- found.+whnf :: Monad m => TrmT m f a -> m (Either a (f a (TrmT m f a)))+whnf (In (Inl (Thunk m))) = m >>= whnf+whnf (In (Inr t)) = return $ Right t+whnf (Var x) = return $ Left x++whnf' :: Monad m => TrmT m f a -> m (TrmT m f a)+whnf' =  liftM (either Var inject) . whnf++-- | This function first evaluates the argument term into whnf via+-- 'whnf' and then projects the top-level signature to the desired+-- subsignature. Failure to do the projection is signalled as a+-- failure in the monad.+whnfPr :: (Monad m, g :<: f) => TrmT m f a -> m (g a (TrmT m f a))+whnfPr t = do res <- whnf t+              case res of+                Left _  -> fail "cannot project variable"+                Right t ->+                    case proj t of+                      Just res' -> return res'+                      Nothing -> fail "projection failed"+++-- | This function evaluates all thunks.+nfT :: (ParamFunctor m, Monad m, Ditraversable f) => TermT m f -> m (Term f)+nfT t = termM $ nf $ unTerm  t++-- | This function evaluates all thunks.+nf :: (Monad m, Ditraversable f) => TrmT m f a -> m (Trm f a)+nf = either (return . Var) (liftM In . dimapM nf) <=< whnf++-- | This function evaluates all thunks while simultaneously+-- projecting the term to a smaller signature. Failure to do the+-- projection is signalled as a failure in the monad as in 'whnfPr'.+nfTPr :: (ParamFunctor m, Monad m, Ditraversable g, g :<: f) => TermT m f -> m (Term g)+nfTPr t = termM $ nfPr $ unTerm t++-- | This function evaluates all thunks while simultaneously+-- projecting the term to a smaller signature. Failure to do the+-- projection is signalled as a failure in the monad as in 'whnfPr'.+nfPr :: (Monad m, Ditraversable g, g :<: f) => TrmT m f a -> m (Trm g a)+nfPr = liftM In . dimapM nfPr <=< whnfPr+++evalStrict :: (Ditraversable g, Monad m, g :<: f) => +              (g (TrmT m f a) (f a (TrmT m f a)) -> TrmT m f a)+           -> g (TrmT m f a) (TrmT m f a) -> TrmT m f a+evalStrict cont t = thunk $ do +                      t' <- dimapM (liftM (either (const Nothing) Just) . whnf) t+                      case disequence t' of+                        Nothing -> return $ inject' t+                        Just s -> return $ cont s+                      ++-- | This type represents algebras which have terms with thunks as+-- carrier.+type AlgT m f g = Alg f (TermT m g)++-- | This combinator makes the evaluation of the given functor+-- application strict by evaluating all thunks of immediate subterms.+strict :: (f :<: g, Ditraversable f, Monad m) => f a (TrmT m g a) -> TrmT m g a+strict x = thunk $ liftM inject $ dimapM whnf' x++-- | This combinator makes the evaluation of the given functor+-- application strict by evaluating all thunks of immediate subterms.+strict' :: (f :<: g, Ditraversable f, Monad m) => f (TrmT m g a) (TrmT m g a) -> TrmT m g a+strict'  = strict . dimap Var id
+ testsuite/tests/Data/Comp/Examples/MultiParam.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE TypeOperators #-}+module Data.Comp.Examples.MultiParam where++import Examples.Multi.FOL as FOL++import Data.Comp.Param.Multi+import Data.Comp.Param.Multi.FreshM (Name)++import Test.Framework+import Test.Framework.Providers.HUnit+import Test.HUnit+++++++--------------------------------------------------------------------------------+-- Test Suits+--------------------------------------------------------------------------------++tests = testGroup "Parametric Compositional Data Types" [+         testCase "FOL" folTest+        ]+++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------++folTest = show (foodFact7 :: INF Name TFormula) @=? "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Person(Skol6(x2)))\n" +++          "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Eats(Skol6(x2), x2))\n" +++                                                                                        "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Person(Skol6(x2)))\n" +++                                                                                        "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Eats(Skol6(x2), x2))"
+ testsuite/tests/Data/Comp/Examples/Param.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE TypeOperators #-}+module Data.Comp.Examples.Param where++import Examples.Names as Names+import Examples.Graph as Graph++import Data.Comp.Param++import Test.Framework+import Test.Framework.Providers.HUnit+import Test.HUnit+++++++--------------------------------------------------------------------------------+-- Test Suits+--------------------------------------------------------------------------------++tests = testGroup "Parametric Compositional Data Types" [+         testCase "names" namesTest,+         testCase "graph" graphTest+        ]+++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------++instance (EqD f, PEq p) => EqD (f :&: p) where+    eqD (v1 :&: p1) (v2 :&: p2) = do b1 <- peq p1 p2+                                     b2 <- eqD v1 v2+                                     return $ b1 && b2++namesTest = sequence_ [en @=? en', ep @=? ep']+graphTest = sequence_ [n @=? 5, f @=? [0,2,1,2]]
+ testsuite/tests/Data/Comp/Examples_Test.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE TypeOperators #-}+module Data.Comp.Examples_Test where++import qualified Data.Comp.Examples.Param as P+import qualified Data.Comp.Examples.MultiParam as MP++import Test.Framework++tests = testGroup "Examples" [+         P.tests,+         MP.tests+       ]
+ testsuite/tests/Tests.hs view
@@ -0,0 +1,18 @@+module Main where++import Test.Framework+import qualified Data.Comp.Examples_Test++--------------------------------------------------------------------------------+-- Test Suits+--------------------------------------------------------------------------------++main = defaultMain [tests]++tests = testGroup "Data.Comp" [+         Data.Comp.Examples_Test.tests+       ]++--------------------------------------------------------------------------------+-- Properties+--------------------------------------------------------------------------------