diff --git a/benchmark/Benchmark.hs b/benchmark/Benchmark.hs
--- a/benchmark/Benchmark.hs
+++ b/benchmark/Benchmark.hs
@@ -22,16 +22,7 @@
sExpr :: PExpr
sExpr = transSugar aExpr
-aHOASExpr :: Int -> DC.HOASExpr
-aHOASExpr n = (iLam $ \x -> x `iPlus` ((iLam $ \x -> x `iMult` x) `iApp` x))
- `iApp`
- ((iLam $ \x -> x `iMult` x)
- `iApp`
- (if n <= 0 then iVInt 2 else aHOASExpr (n - 1)))
-sHOASExpr :: Int -> DS.HOASExpr
-sHOASExpr = transHOAS . aHOASExpr
-
sfCoalg :: Coalg SugarSig Int
sfCoalg 0 = inj $ VInt 1
sfCoalg n = let n' = n-1 in inj $ Plus n' n'
@@ -52,41 +43,42 @@
standardBenchmarks :: (PExpr, SugarExpr, String) -> Benchmark
standardBenchmarks (sExpr,aExpr,n) = rnf aExpr `seq` rnf sExpr `seq` getBench (sExpr, aExpr,n)
where getBench (sExpr, aExpr,n) = bgroup n [
- bench "Comp.desugar" (nf A.desugarExpr aExpr),
- bench "Comp.desugarAlg" (nf A.desugarExpr2 aExpr),
- bench "Standard.desugar" (nf S.desugar sExpr),
- bench "Comp.desugarType" (nf A.desugarType aExpr),
- bench "Comp.desugarType'" (nf A.desugarType' aExpr),
- bench "Standard.desugarType" (nf S.desugarType sExpr),
- bench "Comp.typeSugar" (nf A.typeSugar aExpr),
- bench "Standard.typeSugar" (nf S.typeSugar sExpr),
- bench "Comp.desugarType2" (nf A.desugarType2 aExpr),
- bench "Comp.desugarType2'" (nf A.desugarType2' aExpr),
- bench "Standard.desugarType2" (nf S.desugarType2 sExpr),
- bench "Comp.typeSugar2" (nf A.typeSugar2 aExpr),
- bench "Standard.typeSugar2" (nf S.typeSugar2 sExpr),
- bench "Comp.desugarEval" (nf A.desugarEval aExpr),
- bench "Comp.desugarEval'" (nf A.desugarEval' aExpr),
- bench "Standard.desugarEval" (nf S.desugarEval sExpr),
- bench "Comp.evalSugar" (nf A.evalSugar aExpr),
- bench "Comp.evalDirect" (nf A.evalDirectE aExpr),
- bench "Standard.evalSugar" (nf S.evalSugar sExpr),
- bench "Comp.desugarEval2" (nf A.desugarEval2 aExpr),
- bench "Comp.desugarEval2'" (nf A.desugarEval2' aExpr),
- bench "Standard.desugarEval2" (nf S.desugarEval2 sExpr),
- bench "Comp.evalSugar2" (nf A.evalSugar2 aExpr),
- bench "Comp.evalDirect2" (nf A.evalDirectE2 aExpr),
- bench "Standard.evalSugar2" (nf S.evalSugar2 sExpr),
- bench "Comp.contVar" (nf (A.contVar 10) aExpr),
- bench "Comp.contVar'" (nf (A.contVar' 10) aExpr),
- bench "Comp.contVarGen" (nf (A.contVarGen 10) aExpr),
- bench "Standard.contVar" (nf (S.contVar 10) sExpr),
- bench "Standard.contVarGen" (nf (S.contVarGen 10) sExpr),
- bench "Comp.freeVars" (nf A.freeVars aExpr),
- bench "Comp.freeVars'" (nf A.freeVars' aExpr),
- bench "Comp.freeVarsGen" (nf A.freeVarsGen aExpr),
- bench "Standard.freeVars" (nf S.freeVars sExpr),
- bench "Standard.freeVarsGen" (nf S.freeVarsGen sExpr)]
+ -- bench "Comp.desug" (nf A.desugExpr aExpr),
+ -- bench "Comp.desugAlg" (nf A.desugExpr2 aExpr),
+ -- bench "Standard.desug" (nf S.desug sExpr),
+ bench "Comp.desugType" (nf A.desugType aExpr),
+ bench "Comp.desugType'" (nf A.desugType' aExpr),
+ bench "Standard.desugType" (nf S.desugType sExpr),
+ -- bench "Comp.typeSugar" (nf A.typeSugar aExpr),
+ -- bench "Standard.typeSugar" (nf S.typeSugar sExpr),
+ bench "Comp.desugType2" (nf A.desugType2 aExpr),
+ bench "Comp.desugType2'" (nf A.desugType2' aExpr),
+ bench "Standard.desugType2" (nf S.desugType2 sExpr)
+ -- bench "Comp.typeSugar2" (nf A.typeSugar2 aExpr),
+ -- bench "Standard.typeSugar2" (nf S.typeSugar2 sExpr),
+ -- bench "Comp.desugEval" (nf A.desugEval aExpr),
+ -- bench "Comp.desugEval'" (nf A.desugEval' aExpr),
+ -- bench "Standard.desugEval" (nf S.desugEval sExpr),
+ -- bench "Comp.evalSugar" (nf A.evalSugar aExpr),
+ -- bench "Comp.evalDirect" (nf A.evalDirectE aExpr),
+ -- bench "Standard.evalSugar" (nf S.evalSugar sExpr),
+ -- bench "Comp.desugEval2" (nf A.desugEval2 aExpr),
+ -- bench "Comp.desugEval2'" (nf A.desugEval2' aExpr),
+ -- bench "Standard.desugEval2" (nf S.desugEval2 sExpr),
+ -- bench "Comp.evalSugar2" (nf A.evalSugar2 aExpr),
+ -- bench "Comp.evalDirect2" (nf A.evalDirectE2 aExpr),
+ -- bench "Standard.evalSugar2" (nf S.evalSugar2 sExpr),
+ -- bench "Comp.contVar" (nf (A.contVar 10) aExpr),
+ -- bench "Comp.contVar'" (nf (A.contVar' 10) aExpr),
+ -- bench "Comp.contVarGen" (nf (A.contVarGen 10) aExpr),
+ -- bench "Standard.contVar" (nf (S.contVar 10) sExpr),
+ -- bench "Standard.contVarGen" (nf (S.contVarGen 10) sExpr),
+ -- bench "Comp.freeVars" (nf A.freeVars aExpr),
+ -- bench "Comp.freeVars'" (nf A.freeVars' aExpr),
+ -- bench "Comp.freeVarsGen" (nf A.freeVarsGen aExpr),
+ -- bench "Standard.freeVars" (nf S.freeVars sExpr),
+ -- bench "Standard.freeVarsGen" (nf S.freeVarsGen sExpr)
+ ]
randStdBenchmarks :: Int -> IO Benchmark
randStdBenchmarks s = do
@@ -100,30 +92,12 @@
putStr "size of the input term: "
print $ size aExpr
putStr "does it type check: "
- print (A.desugarType aExpr == Right ty)
+ print (A.desugType aExpr == Right ty)
return $ standardBenchmarks (sExpr,aExpr, "random (depth: " ++ show s ++ ", size: "++ show (size aExpr) ++ ")")
-hoasBenchmaks :: Int -> Benchmark
-hoasBenchmaks s = bgroup ("HOAS (depth: " ++ show s ++ ")") $ getBench s
- where getBench size =
- let sExpr' = sHOASExpr size
- aExpr' = aHOASExpr size in
- rnf aExpr' `seq` rnf sExpr' `seq`
- [bench "Comp.eval2E"
- (nf (A.eval2E :: DC.HOASExpr -> HOASValueExpr) aExpr'),
- bench "Standard.evalHOAS" (nf S.evalHOAS sExpr')]
main = do b1 <- randStdBenchmarks 5
b2 <- randStdBenchmarks 10
b3 <- randStdBenchmarks 20
let b0 = standardBenchmarks (sExpr, aExpr, "hand-written")
- let b4 = map hoasBenchmaks [1,10,100,1000,10000]
- defaultMain $ [b0,b1,b2,b3] ++ b4
-
-
-
-{-
-TODO
- - benchmark generic functions (e.g. size, depth, breadth)
-
--}
+ defaultMain $ [b0,b1,b2,b3]
diff --git a/benchmark/DataTypes/Comp.hs b/benchmark/DataTypes/Comp.hs
--- a/benchmark/DataTypes/Comp.hs
+++ b/benchmark/DataTypes/Comp.hs
@@ -6,7 +6,8 @@
UndecidableInstances,
TypeOperators,
ScopedTypeVariables,
- TypeSynonymInstances #-}
+ TypeSynonymInstances,
+ DeriveFunctor#-}
module DataTypes.Comp
( module DataTypes.Comp,
@@ -21,6 +22,7 @@
import Data.Traversable
import Test.QuickCheck.Arbitrary
import Test.QuickCheck.Gen
+import Test.QuickCheck.Property
import Control.Monad hiding (sequence_,mapM)
import Prelude hiding (sequence_,mapM)
@@ -46,12 +48,12 @@
data ValueT e = TInt
| TBool
| TPair e e
- deriving (Eq)
+ deriving (Eq, Functor)
data Value e = VInt Int
| VBool Bool
| VPair e e
- deriving (Eq)
+ deriving (Eq, Functor)
data Proj = ProjLeft | ProjRight
deriving (Eq)
@@ -64,31 +66,31 @@
| And e e
| Not e
| Proj Proj e
- deriving (Eq)
+ deriving (Eq, Functor)
data Sugar e = Neg e
| Minus e e
| Gt e e
| Or e e
| Impl e e
- deriving (Eq)
+ deriving (Eq, Functor)
data FunT e = TFun e e
- deriving (Eq)
+ deriving (Eq, Functor)
data Lam e = Lam (e -> e)
data App e = App e e
- deriving (Eq)
+ deriving (Eq, Functor)
$(derive [instanceNFData, instanceArbitrary] [''Proj])
$(derive
- [instanceFunctor, instanceExpFunctor, instanceFoldable, instanceTraversable,
+ [instanceFoldable, instanceTraversable,
instanceEqF, instanceNFDataF, instanceArbitraryF, smartConstructors]
[''Value, ''Op, ''Sugar, ''ValueT, ''FunT, ''App])
-$(derive [instanceExpFunctor, smartConstructors] [''Lam])
+$(derive [smartConstructors] [''Lam])
instance EqF Lam where
eqF _ _ = False
@@ -121,6 +123,13 @@
showF TBool = "Bool"
showF (TPair x y) = "(" ++ x ++ "," ++ y ++ ")"
+instance ShowF Sugar where
+ showF (Neg x) = "- " ++ x
+ showF (Minus x y) = "(" ++ x ++ "-" ++ y ++ ")"
+ showF (Gt x y) = "(" ++ x ++ ">" ++ y ++ ")"
+ showF (Or x y) = "(" ++ x ++ "||" ++ y ++ ")"
+ showF (Impl x y) = "(" ++ x ++ "->" ++ y ++ ")"
+
instance ShowF Lam where
showF (Lam f) = "\\x. " ++ f "x"
@@ -147,7 +156,11 @@
desize gen = sized (\n -> resize (max 0 (n-1)) gen)
genSomeTyped :: (Traversable f, GenTyped f) => Gen (Term f)
-genSomeTyped = arbitrary >>= genTyped
+genSomeTyped = arbitrary >>= genTyped
+
+forAllTyped :: (GenTyped f, ShowF f, Testable prop, Traversable f) =>
+ (Term f -> prop) -> Property
+forAllTyped f = forAll genSomeTyped f
instance (GenTyped f, GenTyped g) => GenTyped (f :+: g) where
diff --git a/benchmark/DataTypes/Transform.hs b/benchmark/DataTypes/Transform.hs
--- a/benchmark/DataTypes/Transform.hs
+++ b/benchmark/DataTypes/Transform.hs
@@ -11,7 +11,6 @@
module DataTypes.Transform where
import Data.Comp
-import Data.Comp.ExpFunctor
import DataTypes.Standard as S
import DataTypes.Comp
@@ -49,35 +48,64 @@
transSugarAlg (Or x y) = POr x y
transSugarAlg (Impl x y) = PImpl x y
-class TransHOAS f where
- transHOASAlg :: Alg f S.HOASExpr
-transHOAS :: (ExpFunctor f, TransHOAS f) => Term f -> S.HOASExpr
-transHOAS = cataE transHOASAlg
-instance (TransHOAS f, TransHOAS g) => TransHOAS (f :+: g) where
- transHOASAlg (Inl v) = transHOASAlg v
- transHOASAlg (Inr v) = transHOASAlg v
+class TransCore f where
+ transCoreAlg :: Alg f OExpr
-instance TransHOAS Value where
- transHOASAlg (VInt i) = HOASInt i
- transHOASAlg (VBool b) = HOASBool b
- transHOASAlg (VPair x y) = HOASPair x y
+transCore :: (Functor f, TransCore f) => Term f -> OExpr
+transCore = cata transCoreAlg
-instance TransHOAS Op where
- transHOASAlg (Plus x y) = HOASPlus x y
- transHOASAlg (Mult x y) = HOASMult x y
- transHOASAlg (If b x y) = HOASIf b x y
- transHOASAlg (Lt x y) = HOASLt x y
- transHOASAlg (And x y) = HOASAnd x y
- transHOASAlg (Not x) = HOASNot x
- transHOASAlg (Proj p x) = HOASProj (ptrans p) x
+
+instance (TransCore f, TransCore g) => TransCore (f :+: g) where
+ transCoreAlg (Inl v) = transCoreAlg v
+ transCoreAlg (Inr v) = transCoreAlg v
+
+instance TransCore Value where
+ transCoreAlg (VInt i) = OInt i
+ transCoreAlg (VBool b) = OBool b
+ transCoreAlg (VPair x y) = OPair x y
+
+instance TransCore Op where
+ transCoreAlg (Plus x y) = OPlus x y
+ transCoreAlg (Mult x y) = OMult x y
+ transCoreAlg (If b x y) = OIf b x y
+ transCoreAlg (Lt x y) = OLt x y
+ transCoreAlg (And x y) = OAnd x y
+ transCoreAlg (Not x) = ONot x
+ transCoreAlg (Proj p x) = OProj (ptrans p) x
where ptrans ProjLeft = SProjLeft
ptrans ProjRight = SProjRight
- transHOASAlg (Eq x y) = HOASEq x y
+ transCoreAlg (Eq x y) = OEq x y
-instance TransHOAS Lam where
- transHOASAlg (Lam f) = HOASLam $ f . HOASVal
+class TransVal f where
+ transValAlg :: Alg f SExpr
-instance TransHOAS App where
- transHOASAlg (App x y) = HOASApp x y
+transVal :: (Functor f, TransVal f) => Term f -> SExpr
+transVal = cata transValAlg
+
+
+instance (TransVal f, TransVal g) => TransVal (f :+: g) where
+ transValAlg (Inl v) = transValAlg v
+ transValAlg (Inr v) = transValAlg v
+
+instance TransVal Value where
+ transValAlg (VInt i) = SInt i
+ transValAlg (VBool b) = SBool b
+ transValAlg (VPair x y) = SPair x y
+
+class TransType f where
+ transTypeAlg :: Alg f VType
+
+transType :: (Functor f, TransType f) => Term f -> VType
+transType = cata transTypeAlg
+
+
+instance (TransType f, TransType g) => TransType (f :+: g) where
+ transTypeAlg (Inl v) = transTypeAlg v
+ transTypeAlg (Inr v) = transTypeAlg v
+
+instance TransType ValueT where
+ transTypeAlg TInt = VTInt
+ transTypeAlg TBool = VTBool
+ transTypeAlg (TPair x y) = VTPair x y
diff --git a/benchmark/Functions/Comp/Desugar.hs b/benchmark/Functions/Comp/Desugar.hs
--- a/benchmark/Functions/Comp/Desugar.hs
+++ b/benchmark/Functions/Comp/Desugar.hs
@@ -16,59 +16,59 @@
-- de-sugar
-class (Functor e, Traversable f) => Desugar f e where
- desugarAlg :: TermHom f e
+class (Functor e, Traversable f) => Desug f e where
+ desugAlg :: TermHom f e
-desugarExpr :: SugarExpr -> Expr
-desugarExpr = desugar
+desugExpr :: SugarExpr -> Expr
+desugExpr = desug
-desugar :: Desugar f e => Term f -> Term e
-{-# INLINE desugar #-}
-desugar = appTermHom desugarAlg
+desug :: Desug f e => Term f -> Term e
+{-# INLINE desug #-}
+desug = appTermHom desugAlg
-instance (Desugar f e, Desugar g e) => Desugar (g :+: f) e where
- desugarAlg (Inl v) = desugarAlg v
- desugarAlg (Inr v) = desugarAlg v
+instance (Desug f e, Desug g e) => Desug (g :+: f) e where
+ desugAlg (Inl v) = desugAlg v
+ desugAlg (Inr v) = desugAlg v
-instance (Value :<: v, Functor v) => Desugar Value v where
- desugarAlg = liftCxt
+instance (Value :<: v, Functor v) => Desug Value v where
+ desugAlg = liftCxt
-instance (Op :<: v, Functor v) => Desugar Op v where
- desugarAlg = liftCxt
+instance (Op :<: v, Functor v) => Desug Op v where
+ desugAlg = liftCxt
-instance (Op :<: v, Value :<: v, Functor v) => Desugar Sugar v where
- desugarAlg (Neg x) = iVInt (-1) `iMult` (Hole x)
- desugarAlg (Minus x y) = (Hole x) `iPlus` ((iVInt (-1)) `iMult` (Hole y))
- desugarAlg (Gt x y) = (Hole y) `iLt` (Hole x)
- desugarAlg (Or x y) = iNot (iNot (Hole x) `iAnd` iNot (Hole y))
- desugarAlg (Impl x y) = iNot ((Hole x) `iAnd` iNot (Hole y))
+instance (Op :<: v, Value :<: v, Functor v) => Desug Sugar v where
+ desugAlg (Neg x) = iVInt (-1) `iMult` (Hole x)
+ desugAlg (Minus x y) = (Hole x) `iPlus` ((iVInt (-1)) `iMult` (Hole y))
+ desugAlg (Gt x y) = (Hole y) `iLt` (Hole x)
+ desugAlg (Or x y) = iNot (iNot (Hole x) `iAnd` iNot (Hole y))
+ desugAlg (Impl x y) = iNot ((Hole x) `iAnd` iNot (Hole y))
-- standard algebraic approach
-class Desugar2 f g where
- desugarAlg2 :: Alg f (Term g)
+class Desug2 f g where
+ desugAlg2 :: Alg f (Term g)
-desugarExpr2 :: SugarExpr -> Expr
-desugarExpr2 = desugar2
+desugExpr2 :: SugarExpr -> Expr
+desugExpr2 = desug2
-desugar2 :: (Functor f, Desugar2 f g) => Term f -> Term g
-desugar2 = cata desugarAlg2
+desug2 :: (Functor f, Desug2 f g) => Term f -> Term g
+desug2 = cata desugAlg2
-instance (Desugar2 f e, Desugar2 g e) => Desugar2 (f :+: g) e where
- desugarAlg2 (Inl v) = desugarAlg2 v
- desugarAlg2 (Inr v) = desugarAlg2 v
+instance (Desug2 f e, Desug2 g e) => Desug2 (f :+: g) e where
+ desugAlg2 (Inl v) = desugAlg2 v
+ desugAlg2 (Inr v) = desugAlg2 v
-instance (Value :<: v) => Desugar2 Value v where
- desugarAlg2 = inject
+instance (Value :<: v) => Desug2 Value v where
+ desugAlg2 = inject
-instance (Op :<: v) => Desugar2 Op v where
- desugarAlg2 = inject
+instance (Op :<: v) => Desug2 Op v where
+ desugAlg2 = inject
-instance (Op :<: v, Value :<: v, Functor v) => Desugar2 Sugar v where
- desugarAlg2 (Neg x) = iVInt (-1) `iMult` x
- desugarAlg2 (Minus x y) = x `iPlus` ((iVInt (-1)) `iMult` y)
- desugarAlg2 (Gt x y) = y `iLt` x
- desugarAlg2 (Or x y) = iNot (iNot x `iAnd` iNot y)
- desugarAlg2 (Impl x y) = iNot (x `iAnd` iNot y)
+instance (Op :<: v, Value :<: v, Functor v) => Desug2 Sugar v where
+ desugAlg2 (Neg x) = iVInt (-1) `iMult` x
+ desugAlg2 (Minus x y) = x `iPlus` ((iVInt (-1)) `iMult` y)
+ desugAlg2 (Gt x y) = y `iLt` x
+ desugAlg2 (Or x y) = iNot (iNot x `iAnd` iNot y)
+ desugAlg2 (Impl x y) = iNot (x `iAnd` iNot y)
diff --git a/benchmark/Functions/Comp/Eval.hs b/benchmark/Functions/Comp/Eval.hs
--- a/benchmark/Functions/Comp/Eval.hs
+++ b/benchmark/Functions/Comp/Eval.hs
@@ -13,7 +13,6 @@
import DataTypes.Comp
import Functions.Comp.Desugar
import Data.Comp
-import Data.Comp.ExpFunctor
import Control.Monad
import Data.Traversable
@@ -136,15 +135,12 @@
-- evaluation2
-class ExpFunctor e => Eval2 e v where
+class Functor e => Eval2 e v where
eval2Alg :: e (Term v) -> Term v
eval2 :: (Functor e, Eval2 e v) => Term e -> Term v
eval2 = cata eval2Alg
-eval2E :: (ExpFunctor e, Eval2 e v) => Term e -> Term v
-eval2E = cataE eval2Alg
-
instance (Eval2 f v, Eval2 g v) => Eval2 (f :+: g) v where
eval2Alg (Inl v) = eval2Alg v
eval2Alg (Inr v) = eval2Alg v
@@ -194,13 +190,7 @@
eval2Alg (Or x y) = (\ b c -> iVBool (b || c)) (coerceBool2 x) (coerceBool2 y)
eval2Alg (Impl x y) = (\ b c -> iVBool (not b || c)) (coerceBool2 x) (coerceBool2 y)
-instance (Lam :<: v) => Eval2 Lam v where
- eval2Alg = inject
-instance (Lam :<: v) => Eval2 App v where
- eval2Alg (App v1 v2) = (coerceLam2 v1) v2
-
-
-- direct evaluation 2
class EvalDir2 e where
@@ -259,40 +249,33 @@
-- desugar
-desugarEval :: SugarExpr -> Err ValueExpr
-desugarEval = eval . (desugar :: SugarExpr -> Expr)
+desugEval :: SugarExpr -> Err ValueExpr
+desugEval = eval . (desug :: SugarExpr -> Expr)
evalSugar :: SugarExpr -> Err ValueExpr
evalSugar = eval
-desugarEvalAlg :: AlgM Err SugarSig ValueExpr
-desugarEvalAlg = evalAlg `compAlgM'` (desugarAlg :: TermHom SugarSig ExprSig)
+desugEvalAlg :: AlgM Err SugarSig ValueExpr
+desugEvalAlg = evalAlg `compAlgM'` (desugAlg :: TermHom SugarSig ExprSig)
-desugarEval' :: SugarExpr -> Err ValueExpr
-desugarEval' = cataM desugarEvalAlg
+desugEval' :: SugarExpr -> Err ValueExpr
+desugEval' = cataM desugEvalAlg
-desugarEval2 :: SugarExpr -> ValueExpr
-desugarEval2 = eval2 . (desugar :: SugarExpr -> Expr)
+desugEval2 :: SugarExpr -> ValueExpr
+desugEval2 = eval2 . (desug :: SugarExpr -> Expr)
-desugarEval2E :: SugarExpr -> ValueExpr
-desugarEval2E = eval2E . (desugar :: SugarExpr -> Expr)
evalSugar2 :: SugarExpr -> ValueExpr
evalSugar2 = eval2
-evalSugar2E :: SugarExpr -> ValueExpr
-evalSugar2E = eval2E
-desugarEval2Alg :: Alg SugarSig ValueExpr
-desugarEval2Alg = eval2Alg `compAlg` (desugarAlg :: TermHom SugarSig ExprSig)
+desugEval2Alg :: Alg SugarSig ValueExpr
+desugEval2Alg = eval2Alg `compAlg` (desugAlg :: TermHom SugarSig ExprSig)
-desugarEval2' :: SugarExpr -> ValueExpr
-desugarEval2' = cata desugarEval2Alg
-
-desugarEval2E' :: SugarExpr -> ValueExpr
-desugarEval2E' = cataE desugarEval2Alg
+desugEval2' :: SugarExpr -> ValueExpr
+desugEval2' = cata desugEval2Alg
diff --git a/benchmark/Functions/Comp/Inference.hs b/benchmark/Functions/Comp/Inference.hs
--- a/benchmark/Functions/Comp/Inference.hs
+++ b/benchmark/Functions/Comp/Inference.hs
@@ -35,16 +35,11 @@
inferTypeAlg (VBool _) = return $ inject TBool
inferTypeAlg (VPair x y) = return $ inject $ TPair x y
-check:: (g :<: f, Eq (g (Term f)), Monad m) =>
- g (Term f) -> Term f -> m ()
-check f t = if project t == Just f then return () else fail ""
-
-checkEq :: (Eq a, Monad m) => a -> a -> m ()
-checkEq x y = if x == y then return () else fail ""
-
checkOp :: (g :<: f, Eq (g (Term f)), Monad m) =>
[g (Term f)] -> g (Term f) -> [Term f] -> m (Term f)
-checkOp exs ret tys = sequence_ (zipWith check exs tys) >> return $ inject ret
+checkOp exs et tys = if and (zipWith (\ f t -> maybe False (==f) (project t)) exs tys)
+ then return (inject et)
+ else fail""
instance (ValueT :<: t, EqF t, Monad m) => InferType Op t m where
@@ -53,13 +48,15 @@
inferTypeAlg (Lt x y) = checkOp [TInt,TInt] TBool [x ,y]
inferTypeAlg (And x y) = checkOp [TBool,TBool] TBool [x ,y]
inferTypeAlg (Not x) = checkOp [TBool] TBool [x]
- inferTypeAlg (If b x y) = check TBool b >> checkEq x y >> return x
- inferTypeAlg (Eq x y) = checkEq x y >> return $ iTBool
+ inferTypeAlg (If b x y) = case project b of
+ Just TBool | x == y -> return x
+ _ -> fail ""
+ inferTypeAlg (Eq x y) = if x == y then return iTBool else fail ""
inferTypeAlg (Proj p x) = case project x of
- Just (TPair x1 x2) -> return $
+ Just (TPair x1 x2) ->
case p of
- ProjLeft -> x1
- ProjRight -> x2
+ ProjLeft -> return x1
+ ProjRight -> return x2
_ -> fail ""
instance (ValueT :<: t, EqF t, Monad m) => InferType Sugar t m where
@@ -69,17 +66,17 @@
inferTypeAlg (Or x y) = checkOp [TBool,TBool] TBool [x ,y]
inferTypeAlg (Impl x y) = checkOp [TBool,TBool] TBool [x ,y]
-desugarType :: SugarExpr -> Err BaseType
-desugarType = inferType . (desugar :: SugarExpr -> Expr)
+desugType :: SugarExpr -> Err BaseType
+desugType = inferType . (desug :: SugarExpr -> Expr)
typeSugar :: SugarExpr -> Err BaseType
typeSugar = inferType
-desugarTypeAlg :: AlgM Err SugarSig BaseType
-desugarTypeAlg = inferTypeAlg `compAlgM'` (desugarAlg :: TermHom SugarSig ExprSig)
+desugTypeAlg :: AlgM Err SugarSig BaseType
+desugTypeAlg = inferTypeAlg `compAlgM'` (desugAlg :: TermHom SugarSig ExprSig)
-desugarType' :: SugarExpr -> Err BaseType
-desugarType' e = cataM desugarTypeAlg e
+desugType' :: SugarExpr -> Err BaseType
+desugType' e = cataM desugTypeAlg e
-- pure type inference
@@ -101,19 +98,11 @@
inferTypeAlg2 (VBool _) = inject TBool
inferTypeAlg2 (VPair x y) = inject $ TPair x y
-check2:: (g :<: f, Eq (g (Term f))) =>
- g (Term f) -> Term f -> a -> a
-check2 f t z = if project t == Just f then z else error ""
-
-checkEq2 :: (Eq a) => a -> a -> b -> b
-checkEq2 x y z = if x == y then z else error ""
-
-runCheck :: [a -> a] -> a -> a
-runCheck = foldr (.) id
-
checkOp2 :: (g :<: f, Eq (g (Term f))) =>
[g (Term f)] -> g (Term f) -> [Term f] -> (Term f)
-checkOp2 exs ret tys = runCheck (zipWith check2 exs tys) (inject ret)
+checkOp2 exs ret tys = if and (zipWith (\ f t -> maybe False (==f) (project t)) exs tys)
+ then inject ret
+ else error ""
instance (ValueT :<: t, EqF t) => InferType2 Op t where
@@ -122,8 +111,10 @@
inferTypeAlg2 (Lt x y) = checkOp2 [TInt,TInt] TBool [x ,y]
inferTypeAlg2 (And x y) = checkOp2 [TBool,TBool] TBool [x ,y]
inferTypeAlg2 (Not x) = checkOp2 [TBool] TBool [x]
- inferTypeAlg2 (If b x y) = checkEq2 x y $ check2 TBool b $ x
- inferTypeAlg2 (Eq x y) = checkEq2 x y $ iTBool
+ inferTypeAlg2 (If b x y) = case project b of
+ Just TBool | x == y -> x
+ _ -> error ""
+ inferTypeAlg2 (Eq x y) = if x == y then iTBool else error ""
inferTypeAlg2 (Proj p x) = case project x of
Just (TPair x1 x2) ->
case p of
@@ -138,14 +129,14 @@
inferTypeAlg2 (Or x y) = checkOp2 [TBool,TBool] TBool [x ,y]
inferTypeAlg2 (Impl x y) = checkOp2 [TBool,TBool] TBool [x ,y]
-desugarType2 :: SugarExpr -> BaseType
-desugarType2 = inferType2 . (desugar :: SugarExpr -> Expr)
+desugType2 :: SugarExpr -> BaseType
+desugType2 = inferType2 . (desug :: SugarExpr -> Expr)
typeSugar2 :: SugarExpr -> BaseType
typeSugar2 = inferType2
-desugarTypeAlg2 :: Alg SugarSig BaseType
-desugarTypeAlg2 = inferTypeAlg2 `compAlg` (desugarAlg :: TermHom SugarSig ExprSig)
+desugTypeAlg2 :: Alg SugarSig BaseType
+desugTypeAlg2 = inferTypeAlg2 `compAlg` (desugAlg :: TermHom SugarSig ExprSig)
-desugarType2' :: SugarExpr -> Err BaseType
-desugarType2' e = cataM desugarTypeAlg e
+desugType2' :: SugarExpr -> BaseType
+desugType2' e = cata desugTypeAlg2 e
diff --git a/benchmark/Functions/Standard/Desugar.hs b/benchmark/Functions/Standard/Desugar.hs
--- a/benchmark/Functions/Standard/Desugar.hs
+++ b/benchmark/Functions/Standard/Desugar.hs
@@ -4,20 +4,20 @@
-- de-sugar
-desugar :: PExpr -> OExpr
-desugar (PInt i) = OInt i
-desugar (PBool b) = OBool b
-desugar (PPair x y) = OPair (desugar x) (desugar y)
-desugar (PPlus x y) = OPlus (desugar x) (desugar y)
-desugar (PMult x y) = OMult (desugar x) (desugar y)
-desugar (PIf b x y) = OIf (desugar b) (desugar x) (desugar y)
-desugar (PEq x y) = OEq (desugar x) (desugar y)
-desugar (PLt x y) = OLt (desugar x) (desugar y)
-desugar (PAnd x y) = OAnd (desugar x) (desugar y)
-desugar (PNot x) = ONot (desugar x)
-desugar (PProj p x) = OProj p (desugar x)
-desugar (PNeg x) = OInt (-1) `OMult` (desugar x)
-desugar (PMinus x y) = (desugar x) `OPlus` ((OInt (-1)) `OMult` (desugar y))
-desugar (PGt x y) = (desugar y) `OLt` (desugar x)
-desugar (POr x y) = ONot (ONot (desugar x) `OAnd` ONot (desugar y))
-desugar (PImpl x y) = ONot ((desugar x) `OAnd` ONot (desugar y))
+desug :: PExpr -> OExpr
+desug (PInt i) = OInt i
+desug (PBool b) = OBool b
+desug (PPair x y) = OPair (desug x) (desug y)
+desug (PPlus x y) = OPlus (desug x) (desug y)
+desug (PMult x y) = OMult (desug x) (desug y)
+desug (PIf b x y) = OIf (desug b) (desug x) (desug y)
+desug (PEq x y) = OEq (desug x) (desug y)
+desug (PLt x y) = OLt (desug x) (desug y)
+desug (PAnd x y) = OAnd (desug x) (desug y)
+desug (PNot x) = ONot (desug x)
+desug (PProj p x) = OProj p (desug x)
+desug (PNeg x) = OInt (-1) `OMult` (desug x)
+desug (PMinus x y) = (desug x) `OPlus` ((OInt (-1)) `OMult` (desug y))
+desug (PGt x y) = (desug y) `OLt` (desug x)
+desug (POr x y) = ONot (ONot (desug x) `OAnd` ONot (desug y))
+desug (PImpl x y) = ONot ((desug x) `OAnd` ONot (desug y))
diff --git a/benchmark/Functions/Standard/Eval.hs b/benchmark/Functions/Standard/Eval.hs
--- a/benchmark/Functions/Standard/Eval.hs
+++ b/benchmark/Functions/Standard/Eval.hs
@@ -53,8 +53,8 @@
evalSugar (POr x y) = liftM2 (\ x y -> SBool (x || y)) (evalSugar x >>= coerceBool) (evalSugar y >>= coerceBool)
evalSugar (PImpl x y) = liftM2 (\ x y -> SBool (not x || y)) (evalSugar x >>= coerceBool) (evalSugar y >>= coerceBool)
-desugarEval :: PExpr -> Err SExpr
-desugarEval = eval . desugar
+desugEval :: PExpr -> Err SExpr
+desugEval = eval . desug
coerceInt2 :: SExpr -> Int
@@ -107,8 +107,8 @@
evalSugar2 (POr x y) = (\ x y -> SBool (x || y)) (coerceBool2 $ evalSugar2 x) (coerceBool2 $ evalSugar2 y)
evalSugar2 (PImpl x y) = (\ x y -> SBool (not x || y)) (coerceBool2 $ evalSugar2 x) (coerceBool2 $ evalSugar2 y)
-desugarEval2 :: PExpr -> SExpr
-desugarEval2 = eval2 . desugar
+desugEval2 :: PExpr -> SExpr
+desugEval2 = eval2 . desug
diff --git a/benchmark/Functions/Standard/Inference.hs b/benchmark/Functions/Standard/Inference.hs
--- a/benchmark/Functions/Standard/Inference.hs
+++ b/benchmark/Functions/Standard/Inference.hs
@@ -75,8 +75,8 @@
typeSugar (POr x y) = checkOpP [VTBool,VTBool] VTBool [x,y]
typeSugar (PImpl x y) = checkOpP [VTBool,VTBool] VTBool [x,y]
-desugarType :: PExpr -> Err VType
-desugarType = inferType . desugar
+desugType :: PExpr -> Err VType
+desugType = inferType . desug
-- non-monadic
@@ -149,5 +149,5 @@
typeSugar2 (POr x y) = checkOpP2 [VTBool,VTBool] VTBool [x,y]
typeSugar2 (PImpl x y) = checkOpP2 [VTBool,VTBool] VTBool [x,y]
-desugarType2 :: PExpr -> VType
-desugarType2 = inferType2 . desugar
+desugType2 :: PExpr -> VType
+desugType2 = inferType2 . desug
diff --git a/benchmark/Test.hs b/benchmark/Test.hs
new file mode 100644
--- /dev/null
+++ b/benchmark/Test.hs
@@ -0,0 +1,61 @@
+module Main where
+
+import qualified Functions.Comp as A
+import qualified Functions.Standard as S
+import DataTypes.Comp
+import DataTypes.Transform
+import Test.QuickCheck
+import Data.List
+
+main = mapM_ (quickCheckWith stdArgs{maxSize=10}) allProp
+
+allProp = map forAllTyped [prop_desug, prop_desugAlg, prop_desugType, prop_desugType', prop_typeSugar, prop_desugType2, prop_desugType2', prop_typeSugar2, prop_desugEval, prop_desugEval', prop_evalSugar, prop_evalSugar, prop_evalDirect, prop_desugEval2, prop_desugEval2', prop_evalSugar2, prop_evalDirect2, prop_freeVars, prop_freeVars', prop_freeVarsGen, prop_freeVarsGenS]
+ ++ map forAllTyped [prop_contVar, prop_contVar', prop_contVarGen, prop_contVarGenS]
+
+prop_desug x = transCore (A.desugExpr x) == S.desug (transSugar x)
+
+prop_desugAlg x = transCore (A.desugExpr2 x) == S.desug (transSugar x)
+
+prop_desugType x = fmap transType (A.desugType x) == S.desugType (transSugar x)
+
+prop_desugType' x = fmap transType (A.desugType' x) == S.desugType (transSugar x)
+
+prop_typeSugar x = fmap transType (A.typeSugar x) == S.typeSugar (transSugar x)
+
+prop_desugType2 x = transType (A.desugType2 x) == S.desugType2 (transSugar x)
+
+prop_desugType2' x = transType (A.desugType2' x) == S.desugType2 (transSugar x)
+
+prop_typeSugar2 x = transType (A.typeSugar2 x) == S.typeSugar2 (transSugar x)
+
+prop_desugEval x = fmap transVal (A.desugEval x) == S.desugEval (transSugar x)
+
+prop_desugEval' x = fmap transVal (A.desugEval' x) == S.desugEval (transSugar x)
+
+prop_evalSugar x = fmap transVal (A.evalSugar x) == S.evalSugar (transSugar x)
+
+prop_evalDirect x = fmap transVal (A.evalDirect x) == S.evalSugar (transSugar x)
+
+prop_desugEval2 x = transVal (A.desugEval2 x) == S.desugEval2 (transSugar x)
+
+prop_desugEval2' x = transVal (A.desugEval2' x) == S.desugEval2 (transSugar x)
+
+prop_evalSugar2 x = transVal (A.evalSugar2 x) == S.evalSugar2 (transSugar x)
+
+prop_evalDirect2 x = transVal (A.evalDirect2 x) == S.evalSugar2 (transSugar x)
+
+prop_contVar x v = A.contVar v x == S.contVar v (transSugar x)
+
+prop_contVar' x v = A.contVar' v x == S.contVar v (transSugar x)
+
+prop_contVarGen x v = A.contVarGen v x == S.contVar v (transSugar x)
+
+prop_contVarGenS x v = S.contVarGen v (transSugar x) == S.contVar v (transSugar x)
+
+prop_freeVars x = A.freeVars x == S.freeVars (transSugar x)
+
+prop_freeVars' x = A.freeVars' x == S.freeVars (transSugar x)
+
+prop_freeVarsGen x = sort (A.freeVarsGen x) == sort (S.freeVars (transSugar x))
+
+prop_freeVarsGenS x = S.freeVarsGen (transSugar x) == S.freeVars (transSugar x)
diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
Name: compdata
-Version: 0.1
+Version: 0.2
Synopsis: Compositional Data Types
Description:
@@ -54,10 +54,6 @@
includes /short-cut fusion/ style optimisation rules which yield a
performance boost of up to factor six.
.
- * Efficient implementation of catamorphisms on non-polynomial
- signatures that contain function types. This allows to represent
- /higher-order abstract syntax/ with compositional data types.
- .
* Automatic derivation of instances of all relevant type classes for
using compositional data types via /Template Haskell/. This includes
instances of 'Prelude.Eq', 'Prelude.Ord' and 'Prelude.Show' that are
@@ -86,6 +82,7 @@
testsuite/tests/Data/Comp/Equality_Test.hs,
testsuite/tests/Test/Utils.hs
-- benchmark files
+ benchmark/Test.hs
benchmark/Benchmark.hs
benchmark/DataTypes.hs
benchmark/Functions.hs
@@ -126,25 +123,24 @@
Data.Comp.Decompose, Data.Comp.Unification,
Data.Comp.Derive, Data.Comp.Matching, Data.Comp.Multi,
Data.Comp.Multi.Term, Data.Comp.Multi.Sum,
- Data.Comp.Multi.Functor, Data.Comp.Multi.ExpFunctor,
+ Data.Comp.Multi.Functor,
Data.Comp.Multi.Foldable, Data.Comp.Multi.Traversable,
Data.Comp.Multi.Algebra,
Data.Comp.Multi.Product, Data.Comp.Multi.Show,
Data.Comp.Multi.Equality, Data.Comp.Multi.Variables,
- Data.Comp.Multi.Ops, Data.Comp.Ops, Data.Comp.ExpFunctor
+ Data.Comp.Multi.Ops, Data.Comp.Ops
Other-Modules: Data.Comp.Derive.Utils, Data.Comp.Derive.Equality,
Data.Comp.Derive.Ordering, Data.Comp.Derive.Arbitrary,
Data.Comp.Derive.Show, Data.Comp.Derive.DeepSeq,
Data.Comp.Derive.SmartConstructors,
- Data.Comp.Derive.Foldable, Data.Comp.Derive.ExpFunctor,
+ Data.Comp.Derive.Foldable,
Data.Comp.Derive.Traversable,
Data.Comp.Derive.Multi.Functor,
Data.Comp.Derive.Multi.Foldable,
Data.Comp.Derive.Multi.Traversable,
Data.Comp.Derive.Multi.Equality,
Data.Comp.Derive.Multi.Show,
- Data.Comp.Derive.Multi.ExpFunctor,
Data.Comp.Derive.Multi.SmartConstructors
Build-Depends: base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, th-expand-syns
diff --git a/src/Data/Comp.hs b/src/Data/Comp.hs
--- a/src/Data/Comp.hs
+++ b/src/Data/Comp.hs
@@ -27,8 +27,6 @@
-- ** Lifting Term Homomorphisms to Products
-- $ex4
- -- ** Higher-Order Abstract Syntax
- -- $ex5
module Data.Comp.Term
, module Data.Comp.Algebra
, module Data.Comp.Sum
diff --git a/src/Data/Comp/Algebra.hs b/src/Data/Comp/Algebra.hs
--- a/src/Data/Comp/Algebra.hs
+++ b/src/Data/Comp/Algebra.hs
@@ -91,20 +91,13 @@
CVCoalg',
futu',
CVCoalgM,
- futuM,
-
- -- * Exponential Functors
- appTermHomE,
- cataE,
- anaE,
- appCxtE
+ futuM
) where
import Data.Comp.Term
import Data.Comp.Ops
import Data.Traversable
import Control.Monad hiding (sequence, mapM)
-import Data.Comp.ExpFunctor
import Prelude hiding (sequence, mapM)
@@ -513,40 +506,7 @@
where run :: a -> Term f
run x = appCxt $ fmap run (coa x)
---------------------------
--- Exponential Functors --
---------------------------
-{-| Catamorphism for exponential functors. The intermediate 'cataFS' originates
- from . -}
-cataE :: forall f a . ExpFunctor f => Alg f a -> Term f -> a
-{-# NOINLINE [1] cataE #-}
-cataE f = cataFS . toCxt
- where cataFS :: ExpFunctor f => Context f a -> a
- cataFS (Hole x) = x
- cataFS (Term t) = f (xmap cataFS Hole t)
-
-{-| Anamorphism for exponential functors. -}
-anaE :: forall a f . ExpFunctor f => Coalg f a -> a -> Term f
-anaE f = cataE (Term . removeP) . anaFS
- where anaFS :: a -> Term (f :&: a)
- anaFS t = Term $ xmap anaFS (snd . projectP . unTerm) (f t) :&: t
-
--- | Variant of 'appCxt' for contexts over 'ExpFunctor' signatures.
-appCxtE :: (ExpFunctor f) => Context f (Cxt h f a) -> Cxt h f a
-appCxtE (Hole x) = x
-appCxtE (Term t) = Term (xmap appCxtE Hole t)
-
--- | Variant of 'appTermHom' for term homomorphisms from and to
--- 'ExpFunctor' signatures.
-appTermHomE :: forall f g . (ExpFunctor f, ExpFunctor g) => TermHom f g
- -> Term f -> Term g
-appTermHomE f = cataFS . toCxt
- where cataFS :: Context f (Term g) -> Term g
- cataFS (Hole x) = x
- cataFS (Term t) = appCxtE (f (xmap cataFS Hole t))
-
-
-------------------
-- rewrite rules --
-------------------
@@ -558,9 +518,6 @@
"appTermHom/appTermHom" forall (a :: TermHom g h) (h :: TermHom f g) x.
appTermHom a (appTermHom h x) = appTermHom (compTermHom a h) x;
-
- "cataE/appTermHom" forall (a :: Alg g d) (h :: TermHom f g) (x :: ExpFunctor f => Term f) .
- cataE a (appTermHom h x) = cataE (compAlg a h) x
#-}
{-# RULES
diff --git a/src/Data/Comp/Derive.hs b/src/Data/Comp/Derive.hs
--- a/src/Data/Comp/Derive.hs
+++ b/src/Data/Comp/Derive.hs
@@ -33,8 +33,6 @@
module Data.Comp.Derive.Foldable,
-- ** Traversable
module Data.Comp.Derive.Traversable,
- -- ** ExpFunctor
- module Data.Comp.Derive.ExpFunctor,
-- ** Arbitrary
module Data.Comp.Derive.Arbitrary,
NFData(..),
@@ -58,8 +56,6 @@
module Data.Comp.Derive.Multi.Foldable,
-- ** HTraversable
module Data.Comp.Derive.Multi.Traversable,
- -- ** HExpFunctor
- module Data.Comp.Derive.Multi.ExpFunctor,
-- ** Smart Constructors
module Data.Comp.Derive.Multi.SmartConstructors
) where
@@ -67,7 +63,6 @@
import Control.DeepSeq (NFData(..))
import Data.Comp.Derive.Foldable
import Data.Comp.Derive.Traversable
-import Data.Comp.Derive.ExpFunctor
import Data.Comp.Derive.DeepSeq
import Data.Comp.Derive.Show
import Data.Comp.Derive.Ordering
@@ -79,7 +74,6 @@
import Data.Comp.Derive.Multi.Functor
import Data.Comp.Derive.Multi.Foldable
import Data.Comp.Derive.Multi.Traversable
-import Data.Comp.Derive.Multi.ExpFunctor
import Data.Comp.Derive.Multi.SmartConstructors
import Language.Haskell.TH
diff --git a/src/Data/Comp/Derive/Arbitrary.hs b/src/Data/Comp/Derive/Arbitrary.hs
--- a/src/Data/Comp/Derive/Arbitrary.hs
+++ b/src/Data/Comp/Derive/Arbitrary.hs
@@ -106,13 +106,13 @@
build) |]
{-|
- This function generates a declaration for the method 'shrink' using the given constructors.
+ This function generates a declaration for the method 'shrinkF' using the given constructors.
The constructors are supposed to belong to the same type.
-}
generateShrinkFDecl :: [Con] -> Q Dec
generateShrinkFDecl constrs
= let clauses = map (generateClause.abstractConType) constrs
- in funD 'shrink clauses
+ in funD 'shrinkF clauses
where generateClause (constr, n)
= do varNs <- newNames n "x"
resVarNs <- newNames n "x'"
diff --git a/src/Data/Comp/Derive/ExpFunctor.hs b/src/Data/Comp/Derive/ExpFunctor.hs
deleted file mode 100644
--- a/src/Data/Comp/Derive/ExpFunctor.hs
+++ /dev/null
@@ -1,105 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
---------------------------------------------------------------------------------
--- |
--- Module : Data.Comp.Derive.ExpFunctor
--- Copyright : (c) 2011 Tom Hvitved
--- License : BSD3
--- Maintainer : Tom Hvitved
--- Stability : experimental
--- Portability : non-portable (GHC Extensions)
---
--- Automatically derive instances of @ExpFunctor@.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Derive.ExpFunctor
- (
- ExpFunctor,
- instanceExpFunctor
- ) where
-
-import Data.Comp.ExpFunctor
-import Data.Comp.Derive.Utils
-import Language.Haskell.TH
-
-{-| Derive an instance of 'ExpFunctor' for a type constructor of any first-order
- kind taking at least one argument. -}
-instanceExpFunctor :: Name -> Q [Dec]
-instanceExpFunctor fname = do
- -- Comments below apply to the example where name = T, args = [a,b], and
- -- constrs = [(X,[a]), (Y,[a,b]), (Z,[b -> b])], i.e. the data type
- -- declaration: T a b = X a | Y a b | Z (b -> b)
- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
- -- fArg = b
- let fArg :: Name = tyVarBndrName $ last args
- -- argNames = [a]
- let argNames = map (VarT . tyVarBndrName) (init args)
- -- compType = T a
- let complType = foldl AppT (ConT name) argNames
- -- classType = ExpFunctor (T a)
- let classType = AppT (ConT ''ExpFunctor) complType
- -- constrs' = [(X,[a]), (Y,[a,b]), (Z,[b -> b])]
- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
- xmapDecl <- funD 'xmap (map (xmapClause fArg) constrs')
- return [InstanceD [] classType [xmapDecl]]
- where xmapClause :: Name -> (Name,[Type]) -> ClauseQ
- xmapClause fArg (constr, args) = do
- fn <- newName "_f"
- gn <- newName "_g"
- varNs <- newNames (length args) "x"
- let f = varE fn
- let g = varE gn
- let fp = VarP fn
- let gp = VarP gn
- -- Pattern for the constructor
- let pat = ConP constr $ map VarP varNs
- body <- xmapArgs fArg f g (zip varNs args) (conE constr)
- return $ Clause [fp, gp, pat] (NormalB body) []
- xmapArgs :: Name -> ExpQ -> ExpQ -> [(Name, Type)] -> ExpQ -> ExpQ
- xmapArgs _ _ _ [] acc =
- acc
- xmapArgs fArg f g ((x,tp):tps) acc =
- xmapArgs fArg f g tps (acc `appE`
- (xmapArg fArg tp f g `appE` varE x))
- -- Given the name of the functor variable, a type, and the two
- -- arguments to xmap, return the expression that should be applied
- -- to the parameter of the given type.
- -- Example: xmapArg b (b -> b) f g yields the expression
- -- [|\x -> f . x . g|]
- xmapArg :: Name -> Type -> ExpQ -> ExpQ -> ExpQ
- xmapArg fArg tp f g =
- -- No need to descend into tp if it does not contain the functor
- -- type variable
- if not $ containsType tp (VarT fArg) then
- [|id|]
- else
- case tp of
- ForallT vars _ tp' ->
- -- Check if the functor variable has been rebound
- if any ((==) fArg . tyVarBndrName) vars then
- [|id|]
- else
- xmapArg fArg tp' f g
- VarT a ->
- -- Apply f if we have reached the functor variable
- if a == fArg then f else [|id|]
- ConT _ ->
- [|id|]
- AppT (AppT ArrowT tp1) tp2 -> do
- -- Note that f and g are swapped in the contravariant
- -- type tp1
- xn <- newName "x"
- let ftp1 = xmapArg fArg tp1 g f
- let ftp2 = xmapArg fArg tp2 f g
- lamE [varP xn]
- (infixE (Just ftp2)
- [|(.)|]
- (Just $ infixE (Just $ varE xn)
- [|(.)|]
- (Just ftp1)))
- AppT _ tp' ->
- [|fmap|] `appE` xmapArg fArg tp' f g
- SigT tp' _ ->
- xmapArg fArg tp' f g
- _ ->
- error $ "unsopported type: " ++ show tp
diff --git a/src/Data/Comp/Derive/Multi/ExpFunctor.hs b/src/Data/Comp/Derive/Multi/ExpFunctor.hs
deleted file mode 100644
--- a/src/Data/Comp/Derive/Multi/ExpFunctor.hs
+++ /dev/null
@@ -1,94 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
---------------------------------------------------------------------------------
--- |
--- Module : Data.Comp.Derive.Multi.ExpFunctor
--- Copyright : (c) 2011 Tom Hvitved
--- License : BSD3
--- Maintainer : Tom Hvitved
--- Stability : experimental
--- Portability : non-portable (GHC Extensions)
---
--- Automatically derive instances of @HExpFunctor@.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Derive.Multi.ExpFunctor
- (
- HExpFunctor,
- instanceHExpFunctor
- ) where
-
-import Data.Comp.Multi.ExpFunctor
-import Data.Comp.Derive.Utils
-import Language.Haskell.TH
-
-{-| Derive an instance of 'HExpFunctor' for a type constructor of any
- higher-order kind taking at least two arguments. -}
-instanceHExpFunctor :: Name -> Q [Dec]
-instanceHExpFunctor fname = do
- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
- let args' = init args
- let fArg :: Name = tyVarBndrName $ last args'
- let argNames = map (VarT . tyVarBndrName) (init args')
- let complType = foldl AppT (ConT name) argNames
- let classType = AppT (ConT ''HExpFunctor) complType
- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
- hxmapDecl <- funD 'hxmap (map (hxmapClause fArg) constrs')
- return [InstanceD [] classType [hxmapDecl]]
- where hxmapClause :: Name -> (Name,[Type]) -> ClauseQ
- hxmapClause fArg (constr, args) = do
- fn <- newName "_f"
- gn <- newName "_g"
- varNs <- newNames (length args) "x"
- let f = varE fn
- let g = varE gn
- let fp = VarP fn
- let gp = VarP gn
- -- Pattern for the constructor
- let pat = ConP constr $ map VarP varNs
- body <- hxmapArgs fArg f g (zip varNs args) (conE constr)
- return $ Clause [fp, gp, pat] (NormalB body) []
- hxmapArgs :: Name -> ExpQ -> ExpQ -> [(Name, Type)] -> ExpQ -> ExpQ
- hxmapArgs _ _ _ [] acc =
- acc
- hxmapArgs fArg f g ((x,tp):tps) acc =
- hxmapArgs fArg f g tps (acc `appE`
- (hxmapArg fArg tp f g `appE` varE x))
- hxmapArg :: Name -> Type -> ExpQ -> ExpQ -> ExpQ
- hxmapArg fArg tp f g =
- -- No need to descend into tp if it does not contain the
- -- higher-order functor type variable
- if not $ containsType tp (VarT fArg) then
- [|id|]
- else
- case tp of
- ForallT vars _ tp' ->
- -- Check if the variable has been rebound
- if any ((==) fArg . tyVarBndrName) vars then
- [|id|]
- else
- hxmapArg fArg tp' f g
- (AppT (VarT a) _) ->
- -- Apply f if we have reached the higher-order functor
- -- variable
- if a == fArg then f else [|id|]
- ConT _ ->
- [|id|]
- AppT (AppT ArrowT tp1) tp2 -> do
- -- Note that f and g are swapped in the contravariant
- -- type tp1
- xn <- newName "x"
- let ftp1 = hxmapArg fArg tp1 g f
- let ftp2 = hxmapArg fArg tp2 f g
- lamE [varP xn]
- (infixE (Just ftp2)
- [|(.)|]
- (Just $ infixE (Just $ varE xn)
- [|(.)|]
- (Just ftp1)))
- AppT _ tp' ->
- [|fmap|] `appE` hxmapArg fArg tp' f g
- SigT tp' _ ->
- hxmapArg fArg tp' f g
- _ ->
- error $ "unsopported type: " ++ show tp
diff --git a/src/Data/Comp/Derive/Multi/Show.hs b/src/Data/Comp/Derive/Multi/Show.hs
--- a/src/Data/Comp/Derive/Multi/Show.hs
+++ b/src/Data/Comp/Derive/Multi/Show.hs
@@ -27,7 +27,7 @@
{-| Signature printing. An instance @HShowF f@ gives rise to an instance
@KShow (HTerm f)@. -}
class HShowF f where
- hshowF :: HAlg f (K String)
+ hshowF :: Alg f (K String)
hshowF = K . hshowF'
hshowF' :: f (K String) :=> String
hshowF' = unK . hshowF
diff --git a/src/Data/Comp/Derive/Multi/SmartConstructors.hs b/src/Data/Comp/Derive/Multi/SmartConstructors.hs
--- a/src/Data/Comp/Derive/Multi/SmartConstructors.hs
+++ b/src/Data/Comp/Derive/Multi/SmartConstructors.hs
@@ -16,7 +16,7 @@
module Data.Comp.Derive.Multi.SmartConstructors
(smartHConstructors) where
-import Language.Haskell.TH
+import Language.Haskell.TH hiding (Cxt)
import Data.Comp.Derive.Utils
import Data.Comp.Multi.Sum
import Data.Comp.Multi.Term
@@ -25,7 +25,7 @@
{-| Derive smart constructors for a type constructor of any higher-order kind
taking at least two arguments. The smart constructors are similar to the
- ordinary constructors, but an 'hinject' is automatically inserted. -}
+ ordinary constructors, but an 'inject' is automatically inserted. -}
smartHConstructors :: Name -> Q [Dec]
smartHConstructors fname = do
TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname
@@ -40,7 +40,7 @@
vars = map varE varNs
val = foldl appE (conE name) vars
sig = genSig targs tname sname args
- function = [funD sname [clause pats (normalB [|hinject $val|]) []]]
+ function = [funD sname [clause pats (normalB [|inject $val|]) []]]
sequence $ sig ++ function
genSig targs tname sname 0 = (:[]) $ do
fvar <- newName "f"
@@ -54,8 +54,8 @@
a = varT avar
i = varT ivar
ftype = foldl appT (conT tname) (map varT targs')
- constr = classP ''(:<<:) [ftype, f]
- typ = foldl appT (conT ''HCxt) [h, f, a, i]
+ constr = classP ''(:<:) [ftype, f]
+ typ = foldl appT (conT ''Cxt) [h, f, a, i]
typeSig = forallT (map PlainTV vars) (sequence [constr]) typ
sigD sname typeSig
genSig _ _ _ _ = []
diff --git a/src/Data/Comp/ExpFunctor.hs b/src/Data/Comp/ExpFunctor.hs
deleted file mode 100644
--- a/src/Data/Comp/ExpFunctor.hs
+++ /dev/null
@@ -1,21 +0,0 @@
---------------------------------------------------------------------------------
--- |
--- Module : Data.Comp.ExpFunctor
--- Copyright : 2008 Edward Kmett
--- License : BSD
---
--- Maintainer : Tom Hvitved
--- Stability : unknown
--- Portability : unknown
---
--- Exponential functors, see .
---------------------------------------------------------------------------------
-
-module Data.Comp.ExpFunctor
- ( ExpFunctor(..)
- ) where
-
-{-| Exponential functors are functors that may be both covariant (as ordinary
- functors) and contravariant. -}
-class ExpFunctor f where
- xmap :: (a -> b) -> (b -> a) -> f a -> f b
diff --git a/src/Data/Comp/Multi.hs b/src/Data/Comp/Multi.hs
--- a/src/Data/Comp/Multi.hs
+++ b/src/Data/Comp/Multi.hs
@@ -25,9 +25,6 @@
-- ** Lifting Term Homomorphisms to Products
-- $ex4
-
- -- ** Higher-Order Abstract Syntax
- -- $ex5
module Data.Comp.Multi.Term
, module Data.Comp.Multi.Algebra
, module Data.Comp.Multi.Functor
@@ -66,7 +63,7 @@
> Snd :: e (s,t) -> Op e t
>
> -- Signature for the simple expression language
-> type Sig = Op :++: Value
+> type Sig = Op :+: Value
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [instanceHFunctor, instanceHShowF, smartHConstructors]
@@ -74,34 +71,34 @@
>
> -- Term evaluation algebra
> class Eval f v where
-> evalAlg :: HAlg f (HTerm v)
+> evalAlg :: Alg f (HTerm v)
>
-> instance (Eval f v, Eval g v) => Eval (f :++: g) v where
-> evalAlg (HInl x) = evalAlg x
-> evalAlg (HInr x) = evalAlg x
+> instance (Eval f v, Eval g v) => Eval (f :+: g) v where
+> evalAlg (Inl x) = evalAlg x
+> evalAlg (Inr x) = evalAlg x
>
> -- Lift the evaluation algebra to a catamorphism
-> eval :: (HFunctor f, Eval f v) => HTerm f :-> HTerm v
-> eval = hcata evalAlg
+> eval :: (HFunctor f, Eval f v) => Term f :-> Term v
+> eval = cata evalAlg
>
-> instance (Value :<<: v) => Eval Value v where
-> evalAlg = hinject
+> instance (Value :<: v) => Eval Value v where
+> evalAlg = inject
>
-> instance (Value :<<: v) => Eval Op v where
+> instance (Value :<: v) => Eval Op v where
> evalAlg (Add x y) = iConst $ (projC x) + (projC y)
> evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
> evalAlg (Fst x) = fst $ projP x
> evalAlg (Snd x) = snd $ projP x
>
-> projC :: (Value :<<: v) => HTerm v Int -> Int
-> projC v = case hproject v of Just (Const n) -> n
+> projC :: (Value :<: v) => Term v Int -> Int
+> projC v = case project v of Just (Const n) -> n
>
-> projP :: (Value :<<: v) => HTerm v (s,t) -> (HTerm v s, HTerm v t)
-> projP v = case hproject v of Just (Pair x y) -> (x,y)
+> projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)
+> projP v = case project v of Just (Pair x y) -> (x,y)
>
> -- Example: evalEx = iConst 2
-> evalEx :: HTerm Value Int
-> evalEx = eval (iFst $ iPair (iConst 2) (iConst 1) :: HTerm Sig Int)
+> evalEx :: Term Value Int
+> evalEx = eval (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int)
-}
{- $ex2
@@ -130,7 +127,7 @@
> Snd :: e (s,t) -> Op e t
>
> -- Signature for the simple expression language
-> type Sig = Op :++: Value
+> type Sig = Op :+: Value
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [instanceHFunctor, instanceHTraversable, instanceHFoldable,
@@ -139,20 +136,20 @@
>
> -- Monadic term evaluation algebra
> class EvalM f v where
-> evalAlgM :: HAlgM Maybe f (HTerm v)
+> evalAlgM :: AlgM Maybe f (Term v)
>
-> instance (EvalM f v, EvalM g v) => EvalM (f :++: g) v where
-> evalAlgM (HInl x) = evalAlgM x
-> evalAlgM (HInr x) = evalAlgM x
+> instance (EvalM f v, EvalM g v) => EvalM (f :+: g) v where
+> evalAlgM (Inl x) = evalAlgM x
+> evalAlgM (Inr x) = evalAlgM x
>
-> evalM :: (HTraversable f, EvalM f v) => HTerm f l
-> -> Maybe (HTerm v l)
-> evalM = hcataM evalAlgM
+> evalM :: (HTraversable f, EvalM f v) => Term f l
+> -> Maybe (Term v l)
+> evalM = cataM evalAlgM
>
-> instance (Value :<<: v) => EvalM Value v where
-> evalAlgM = return . hinject
+> instance (Value :<: v) => EvalM Value v where
+> evalAlgM = return . inject
>
-> instance (Value :<<: v) => EvalM Op v where
+> instance (Value :<: v) => EvalM Op v where
> evalAlgM (Add x y) = do n1 <- projC x
> n2 <- projC y
> return $ iConst $ n1 + n2
@@ -162,18 +159,18 @@
> evalAlgM (Fst v) = liftM fst $ projP v
> evalAlgM (Snd v) = liftM snd $ projP v
>
-> projC :: (Value :<<: v) => HTerm v Int -> Maybe Int
-> projC v = case hproject v of
+> projC :: (Value :<: v) => Term v Int -> Maybe Int
+> projC v = case project v of
> Just (Const n) -> return n; _ -> Nothing
>
-> projP :: (Value :<<: v) => HTerm v (a,b) -> Maybe (HTerm v a, HTerm v b)
-> projP v = case hproject v of
+> projP :: (Value :<: v) => Term v (a,b) -> Maybe (Term v a, Term v b)
+> projP v = case project v of
> Just (Pair x y) -> return (x,y); _ -> Nothing
>
> -- Example: evalMEx = Just (iConst 5)
-> evalMEx :: Maybe (HTerm Value Int)
+> evalMEx :: Maybe (Term Value Int)
> evalMEx = evalM ((iConst 1) `iAdd`
-> (iConst 2 `iMult` iConst 2) :: HTerm Sig Int)
+> (iConst 2 `iMult` iConst 2) :: Term Sig Int)
-}
{- $ex3
@@ -206,12 +203,12 @@
> deriving Show
>
> -- Signature for the simple expression language
-> type Sig = Op :++: Value
-> type SigP = Op :&&: Pos :++: Value :&&: Pos
+> type Sig = Op :+: Value
+> type SigP = Op :&: Pos :+: Value :&: Pos
>
> -- Signature for the simple expression language, extended with syntactic sugar
-> type Sig' = Sugar :++: Op :++: Value
-> type SigP' = Sugar :&&: Pos :++: Op :&&: Pos :++: Value :&&: Pos
+> type Sig' = Sugar :+: Op :+: Value
+> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [instanceHFunctor, instanceHTraversable, instanceHFoldable,
@@ -220,57 +217,57 @@
>
> -- Term homomorphism for desugaring of terms
> class (HFunctor f, HFunctor g) => Desugar f g where
-> desugHom :: HTermHom f g
-> desugHom = desugHom' . hfmap HHole
-> desugHom' :: HAlg f (HContext g a)
-> desugHom' x = appHCxt (desugHom x)
+> desugHom :: TermHom f g
+> desugHom = desugHom' . hfmap Hole
+> desugHom' :: Alg f (Context g a)
+> desugHom' x = appCxt (desugHom x)
>
-> instance (Desugar f h, Desugar g h) => Desugar (f :++: g) h where
-> desugHom (HInl x) = desugHom x
-> desugHom (HInr x) = desugHom x
-> desugHom' (HInl x) = desugHom' x
-> desugHom' (HInr x) = desugHom' x
+> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
+> desugHom (Inl x) = desugHom x
+> desugHom (Inr x) = desugHom x
+> desugHom' (Inl x) = desugHom' x
+> desugHom' (Inr x) = desugHom' x
>
-> instance (Value :<<: v, HFunctor v) => Desugar Value v where
-> desugHom = simpHCxt . hinj
+> instance (Value :<: v, HFunctor v) => Desugar Value v where
+> desugHom = simpCxt . inj
>
-> instance (Op :<<: v, HFunctor v) => Desugar Op v where
-> desugHom = simpHCxt . hinj
+> instance (Op :<: v, HFunctor v) => Desugar Op v where
+> desugHom = simpCxt . inj
>
-> instance (Op :<<: v, Value :<<: v, HFunctor v) => Desugar Sugar v where
+> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
> desugHom' (Neg x) = iConst (-1) `iMult` x
> desugHom' (Swap x) = iSnd x `iPair` iFst x
>
> -- Term evaluation algebra
> class Eval f v where
-> evalAlg :: HAlg f (HTerm v)
+> evalAlg :: Alg f (Term v)
>
-> instance (Eval f v, Eval g v) => Eval (f :++: g) v where
-> evalAlg (HInl x) = evalAlg x
-> evalAlg (HInr x) = evalAlg x
+> instance (Eval f v, Eval g v) => Eval (f :+: g) v where
+> evalAlg (Inl x) = evalAlg x
+> evalAlg (Inr x) = evalAlg x
>
-> instance (Value :<<: v) => Eval Value v where
-> evalAlg = hinject
+> instance (Value :<: v) => Eval Value v where
+> evalAlg = inject
>
-> instance (Value :<<: v) => Eval Op v where
+> instance (Value :<: v) => Eval Op v where
> evalAlg (Add x y) = iConst $ (projC x) + (projC y)
> evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
> evalAlg (Fst x) = fst $ projP x
> evalAlg (Snd x) = snd $ projP x
>
-> projC :: (Value :<<: v) => HTerm v Int -> Int
-> projC v = case hproject v of Just (Const n) -> n
+> projC :: (Value :<: v) => Term v Int -> Int
+> projC v = case project v of Just (Const n) -> n
>
-> projP :: (Value :<<: v) => HTerm v (s,t) -> (HTerm v s, HTerm v t)
-> projP v = case hproject v of Just (Pair x y) -> (x,y)
+> projP :: (Value :<: v) => HTerm v (s,t) -> (HTerm v s, HTerm v t)
+> projP v = case project v of Just (Pair x y) -> (x,y)
>
> -- Compose the evaluation algebra and the desugaring homomorphism to an
> -- algebra
-> eval :: HTerm Sig' :-> HTerm Value
-> eval = hcata (evalAlg `compHAlg` (desugHom :: HTermHom Sig' Sig))
+> eval :: Term Sig' :-> Term Value
+> eval = cata (evalAlg `compAlg` (desugHom :: TermHom Sig' Sig))
>
> -- Example: evalEx = iPair (iConst 2) (iConst 1)
-> evalEx :: HTerm Value (Int,Int)
+> evalEx :: Term Value (Int,Int)
> evalEx = eval $ iSwap $ iPair (iConst 1) (iConst 2)
-}
@@ -305,12 +302,12 @@
> deriving Show
>
> -- Signature for the simple expression language
-> type Sig = Op :++: Value
-> type SigP = Op :&&: Pos :++: Value :&&: Pos
+> type Sig = Op :+: Value
+> type SigP = Op :&: Pos :+: Value :&: Pos
>
> -- Signature for the simple expression language, extended with syntactic sugar
-> type Sig' = Sugar :++: Op :++: Value
-> type SigP' = Sugar :&&: Pos :++: Op :&&: Pos :++: Value :&&: Pos
+> type Sig' = Sugar :+: Op :+: Value
+> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [instanceHFunctor, instanceHTraversable, instanceHFoldable,
@@ -319,53 +316,53 @@
>
> -- Term homomorphism for desugaring of terms
> class (HFunctor f, HFunctor g) => Desugar f g where
-> desugHom :: HTermHom f g
-> desugHom = desugHom' . hfmap HHole
-> desugHom' :: HAlg f (HContext g a)
-> desugHom' x = appHCxt (desugHom x)
+> desugHom :: TermHom f g
+> desugHom = desugHom' . hfmap Hole
+> desugHom' :: Alg f (Context g a)
+> desugHom' x = appCxt (desugHom x)
>
-> instance (Desugar f h, Desugar g h) => Desugar (f :++: g) h where
-> desugHom (HInl x) = desugHom x
-> desugHom (HInr x) = desugHom x
-> desugHom' (HInl x) = desugHom' x
-> desugHom' (HInr x) = desugHom' x
+> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
+> desugHom (Inl x) = desugHom x
+> desugHom (Inr x) = desugHom x
+> desugHom' (Inl x) = desugHom' x
+> desugHom' (Inr x) = desugHom' x
>
-> instance (Value :<<: v, HFunctor v) => Desugar Value v where
-> desugHom = simpHCxt . hinj
+> instance (Value :<: v, HFunctor v) => Desugar Value v where
+> desugHom = simpCxt . inj
>
-> instance (Op :<<: v, HFunctor v) => Desugar Op v where
-> desugHom = simpHCxt . hinj
+> instance (Op :<: v, HFunctor v) => Desugar Op v where
+> desugHom = simpCxt . inj
>
-> instance (Op :<<: v, Value :<<: v, HFunctor v) => Desugar Sugar v where
+> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
> desugHom' (Neg x) = iConst (-1) `iMult` x
> desugHom' (Swap x) = iSnd x `iPair` iFst x
>
> -- Lift the desugaring term homomorphism to a catamorphism
-> desug :: HTerm Sig' :-> HTerm Sig
-> desug = appHTermHom desugHom
+> desug :: Term Sig' :-> Term Sig
+> desug = appTermHom desugHom
>
> -- Example: desugEx = iPair (iConst 2) (iConst 1)
-> desugEx :: HTerm Sig (Int,Int)
+> desugEx :: Term Sig (Int,Int)
> desugEx = desug $ iSwap $ iPair (iConst 1) (iConst 2)
>
> -- Lift desugaring to terms annotated with source positions
-> desugP :: HTerm SigP' :-> HTerm SigP
-> desugP = appHTermHom (productHTermHom desugHom)
+> desugP :: Term SigP' :-> Term SigP
+> desugP = appTermHom (productTermHom desugHom)
>
-> iSwapP :: (HDistProd f p f', Sugar :<<: f) => p -> HTerm f' (a,b) -> HTerm f' (b,a)
-> iSwapP p x = HTerm (hinjectP p $ hinj $ Swap x)
+> iSwapP :: (DistProd f p f', Sugar :<: f) => p -> Term f' (a,b) -> Term f' (b,a)
+> iSwapP p x = Term (injectP p $ inj $ Swap x)
>
-> iConstP :: (HDistProd f p f', Value :<<: f) => p -> Int -> HTerm f' Int
-> iConstP p x = HTerm (hinjectP p $ hinj $ Const x)
+> iConstP :: (DistProd f p f', Value :<: f) => p -> Int -> Term f' Int
+> iConstP p x = Term (injectP p $ inj $ Const x)
>
-> iPairP :: (HDistProd f p f', Value :<<: f) => p -> HTerm f' a -> HTerm f' b -> HTerm f' (a,b)
-> iPairP p x y = HTerm (hinjectP p $ hinj $ Pair x y)
+> iPairP :: (DistProd f p f', Value :<: f) => p -> Term f' a -> Term f' b -> Term f' (a,b)
+> iPairP p x y = Term (injectP p $ inj $ Pair x y)
>
-> iFstP :: (HDistProd f p f', Op :<<: f) => p -> HTerm f' (a,b) -> HTerm f' a
-> iFstP p x = HTerm (hinjectP p $ hinj $ Fst x)
+> iFstP :: (DistProd f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' a
+> iFstP p x = Term (injectP p $ inj $ Fst x)
>
-> iSndP :: (HDistProd f p f', Op :<<: f) => p -> HTerm f' (a,b) -> HTerm f' b
-> iSndP p x = HTerm (hinjectP p $ hinj $ Snd x)
+> iSndP :: (DistProd f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' b
+> iSndP p x = Term (injectP p $ inj $ Snd x)
>
> -- Example: desugPEx = iPairP (Pos 1 0)
> -- (iSndP (Pos 1 0) (iPairP (Pos 1 1)
@@ -374,7 +371,7 @@
> -- (iFstP (Pos 1 0) (iPairP (Pos 1 1)
> -- (iConstP (Pos 1 2) 1)
> -- (iConstP (Pos 1 3) 2)))
-> desugPEx :: HTerm SigP (Int,Int)
+> desugPEx :: Term SigP (Int,Int)
> desugPEx = desugP $ iSwapP (Pos 1 0) (iPairP (Pos 1 1) (iConstP (Pos 1 2) 1)
> (iConstP (Pos 1 3) 2))
-}
diff --git a/src/Data/Comp/Multi/Algebra.hs b/src/Data/Comp/Multi/Algebra.hs
--- a/src/Data/Comp/Multi/Algebra.hs
+++ b/src/Data/Comp/Multi/Algebra.hs
@@ -17,319 +17,311 @@
module Data.Comp.Multi.Algebra (
-- * Algebras & Catamorphisms
- HAlg,
- hfree,
- hcata,
- hcata',
- appHCxt,
+ Alg,
+ free,
+ cata,
+ cata',
+ appCxt,
-- * Monadic Algebras & Catamorphisms
- HAlgM,
+ AlgM,
-- halgM,
- hfreeM,
- hcataM,
- hcataM',
- liftMHAlg,
+ freeM,
+ cataM,
+ cataM',
+ liftMAlg,
-- * Term Homomorphisms
- HCxtFun,
- HSigFun,
- HTermHom,
- appHTermHom,
- compHTermHom,
- appHSigFun,
- compHSigFun,
- htermHom,
- compHAlg,
--- compHCoalg,
--- compHCVCoalg,
+ CxtFun,
+ SigFun,
+ TermHom,
+ appTermHom,
+ compTermHom,
+ appSigFun,
+ compSigFun,
+ termHom,
+ compAlg,
+-- compCoalg,
+-- compCVCoalg,
-- * Monadic Term Homomorphisms
- HCxtFunM,
- HSigFunM,
- HTermHomM,
--- HSigFunM',
--- HTermHomM',
- hsigFunM,
--- htermHom',
- appHTermHomM,
- htermHomM,
--- htermHomM',
- appHSigFunM,
--- appHSigFunM',
- compHTermHomM,
- compHSigFunM,
- compHAlgM,
- compHAlgM',
+ CxtFunM,
+ SigFunM,
+ TermHomM,
+-- SigFunM',
+-- TermHomM',
+ sigFunM,
+-- termHom',
+ appTermHomM,
+ termHomM,
+-- termHomM',
+ appSigFunM,
+-- appSigFunM',
+ compTermHomM,
+ compSigFunM,
+ compAlgM,
+ compAlgM',
-- * Coalgebras & Anamorphisms
- HCoalg,
- hana,
--- hana',
- HCoalgM,
- hanaM,
+ Coalg,
+ ana,
+-- ana',
+ CoalgM,
+ anaM,
-- * R-Algebras & Paramorphisms
- HRAlg,
- hpara,
- HRAlgM,
- hparaM,
+ RAlg,
+ para,
+ RAlgM,
+ paraM,
-- * R-Coalgebras & Apomorphisms
- HRCoalg,
- hapo,
- HRCoalgM,
- hapoM,
+ RCoalg,
+ apo,
+ RCoalgM,
+ apoM,
-- * CV-Algebras & Histomorphisms
-- $l1
--- HCVAlg,
--- hhisto,
--- HCVAlgM,
--- hhistoM,
+-- CVAlg,
+-- histo,
+-- CVAlgM,
+-- histoM,
-- * CV-Coalgebras & Futumorphisms
- HCVCoalg,
- hfutu,
--- HCVCoalg',
--- hfutu',
- HCVCoalgM,
- hfutuM,
-
- -- * Exponential Functors
- appHTermHomE,
- hcataE,
--- hanaE,
- appHCxtE
+ CVCoalg,
+ futu,
+-- CVCoalg',
+-- futu',
+ CVCoalgM,
+ futuM,
) where
import Data.Comp.Multi.Term
import Data.Comp.Multi.Functor
import Data.Comp.Multi.Traversable
-import Data.Comp.Multi.ExpFunctor
import Data.Comp.Ops
-
import Control.Monad
-type HAlg f e = f e :-> e
+type Alg f e = f e :-> e
-hfree :: forall f h a b . (HFunctor f) =>
- HAlg f b -> (a :-> b) -> HCxt h f a :-> b
-hfree f g = run
- where run :: HCxt h f a :-> b
- run (HHole v) = g v
- run (HTerm c) = f $ hfmap run c
+free :: forall f h a b . (HFunctor f) =>
+ Alg f b -> (a :-> b) -> Cxt h f a :-> b
+free f g = run
+ where run :: Cxt h f a :-> b
+ run (Hole v) = g v
+ run (Term c) = f $ hfmap run c
-hcata :: forall f a. (HFunctor f) => HAlg f a -> HTerm f :-> a
-hcata f = run
- where run :: HTerm f :-> a
- run (HTerm t) = f (hfmap run t)
+cata :: forall f a. HFunctor f => Alg f a -> Term f :-> a
+cata f = run
+ where run :: Term f :-> a
+ run (Term t) = f (hfmap run t)
-hcata' :: (HFunctor f) => HAlg f e -> HCxt h f e :-> e
-hcata' alg = hfree alg id
+cata' :: HFunctor f => Alg f e -> Cxt h f e :-> e
+cata' alg = free alg id
-- | This function applies a whole context into another context.
-appHCxt :: (HFunctor f) => HContext f (HCxt h f a) :-> HCxt h f a
-appHCxt = hcata' HTerm
+appCxt :: HFunctor f => Context f (Cxt h f a) :-> Cxt h f a
+appCxt = cata' Term
-- | This function lifts a many-sorted algebra to a monadic domain.
-liftMHAlg :: forall m f. (Monad m, HTraversable f) =>
- HAlg f I -> HAlg f m
-liftMHAlg alg = turn . liftM alg . hmapM run
+liftMAlg :: forall m f. (Monad m, HTraversable f) =>
+ Alg f I -> Alg f m
+liftMAlg alg = turn . liftM alg . hmapM run
where run :: m i -> m (I i)
run m = do x <- m
return $ I x
turn x = do I y <- x
return y
-type HAlgM m f e = NatM m (f e) e
+type AlgM m f e = NatM m (f e) e
-hfreeM :: forall f m h a b. (HTraversable f, Monad m) =>
- HAlgM m f b -> NatM m a b -> NatM m (HCxt h f a) b
-hfreeM algm var = run
- where run :: NatM m (HCxt h f a) b
- run (HHole x) = var x
- run (HTerm x) = hmapM run x >>= algm
+freeM :: forall f m h a b. (HTraversable f, Monad m) =>
+ AlgM m f b -> NatM m a b -> NatM m (Cxt h f a) b
+freeM algm var = run
+ where run :: NatM m (Cxt h f a) b
+ run (Hole x) = var x
+ run (Term x) = hmapM run x >>= algm
--- | This is a monadic version of 'hcata'.
+-- | This is a monadic version of 'cata'.
-hcataM :: forall f m a. (HTraversable f, Monad m) =>
- HAlgM m f a -> NatM m (HTerm f) a
--- hcataM alg h (HTerm t) = alg =<< hmapM (hcataM alg h) t
-hcataM alg = run
- where run :: NatM m (HTerm f) a
- run (HTerm x) = alg =<< hmapM run x
+cataM :: forall f m a. (HTraversable f, Monad m) =>
+ AlgM m f a -> NatM m (Term f) a
+-- cataM alg h (Term t) = alg =<< hmapM (cataM alg h) t
+cataM alg = run
+ where run :: NatM m (Term f) a
+ run (Term x) = alg =<< hmapM run x
-hcataM' :: forall m h a f. (Monad m, HTraversable f) => HAlgM m f a -> NatM m (HCxt h f a) a
--- hcataM' alg = hfreeM alg return
-hcataM' f = run
- where run :: NatM m (HCxt h f a) a
- run (HHole x) = return x
- run (HTerm x) = hmapM run x >>= f
+cataM' :: forall m h a f. (Monad m, HTraversable f) => AlgM m f a -> NatM m (Cxt h f a) a
+-- cataM' alg = freeM alg return
+cataM' f = run
+ where run :: NatM m (Cxt h f a) a
+ run (Hole x) = return x
+ run (Term x) = hmapM run x >>= f
-- | This type represents context function.
-type HCxtFun f g = forall a h. HCxt h f a :-> HCxt h g a
+type CxtFun f g = forall a h. Cxt h f a :-> Cxt h g a
-- | This type represents uniform signature function specification.
-type HSigFun f g = forall a. f a :-> g a
+type SigFun f g = forall a. f a :-> g a
-- | This type represents a term algebra.
-type HTermHom f g = HSigFun f (HContext g)
+type TermHom f g = SigFun f (Context g)
-- | This function applies the given term homomorphism to a
-- term/context.
-appHTermHom :: (HFunctor f, HFunctor g) => HTermHom f g -> HCxtFun f g
+appTermHom :: (HFunctor f, HFunctor g) => TermHom f g -> CxtFun f g
-- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type
--- (Functor f, Functor g) => (f (HCxt h g b) -> HContext g (HCxt h g b)) -> HCxt h f b -> HCxt h g b
+-- (Functor f, Functor g) => (f (Cxt h g b) -> Context g (Cxt h g b)) -> Cxt h f b -> Cxt h g b
-- would achieve the same. The given type is chosen for clarity.
-appHTermHom _ (HHole b) = HHole b
-appHTermHom f (HTerm t) = appHCxt . f . hfmap (appHTermHom f) $ t
+appTermHom _ (Hole b) = Hole b
+appTermHom f (Term t) = appCxt . f . hfmap (appTermHom f) $ t
-- | This function composes two term algebras.
-compHTermHom :: (HFunctor g, HFunctor h) => HTermHom g h -> HTermHom f g -> HTermHom f h
+compTermHom :: (HFunctor g, HFunctor h) => TermHom g h -> TermHom f g -> TermHom f h
-- Note: The rank 2 type polymorphism is not necessary. Alternatively, also the type
--- (Functor f, Functor g) => (f (HCxt h g b) -> HContext g (HCxt h g b))
--- -> (a -> HCxt h f b) -> a -> HCxt h g b
+-- (Functor f, Functor g) => (f (Cxt h g b) -> Context g (Cxt h g b))
+-- -> (a -> Cxt h f b) -> a -> Cxt h g b
-- would achieve the same. The given type is chosen for clarity.
-compHTermHom f g = appHTermHom f . g
+compTermHom f g = appTermHom f . g
-- | This function composes a term algebra with an algebra.
-compHAlg :: (HFunctor g) => HAlg g a -> HTermHom f g -> HAlg f a
-compHAlg alg talg = hcata' alg . talg
+compAlg :: (HFunctor g) => Alg g a -> TermHom f g -> Alg f a
+compAlg alg talg = cata' alg . talg
-- | This function applies a signature function to the given context.
-appHSigFun :: (HFunctor f, HFunctor g) => HSigFun f g -> HCxtFun f g
-appHSigFun f = appHTermHom $ htermHom f
+appSigFun :: (HFunctor f, HFunctor g) => SigFun f g -> CxtFun f g
+appSigFun f = appTermHom $ termHom f
-- | This function composes two signature functions.
-compHSigFun :: HSigFun g h -> HSigFun f g -> HSigFun f h
-compHSigFun f g = f . g
+compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
+compSigFun f g = f . g
-- | Lifts the given signature function to the canonical term homomorphism.
-htermHom :: (HFunctor g) => HSigFun f g -> HTermHom f g
-htermHom f = simpHCxt . f
+termHom :: (HFunctor g) => SigFun f g -> TermHom f g
+termHom f = simpCxt . f
-- | This type represents monadic context function.
-type HCxtFunM m f g = forall a h. NatM m (HCxt h f a) (HCxt h g a)
+type CxtFunM m f g = forall a h. NatM m (Cxt h f a) (Cxt h g a)
-- | This type represents monadic signature functions.
-type HSigFunM m f g = forall a. NatM m (f a) (g a)
+type SigFunM m f g = forall a. NatM m (f a) (g a)
-- | This type represents monadic term algebras.
-type HTermHomM m f g = HSigFunM m f (HContext g)
+type TermHomM m f g = SigFunM m f (Context g)
-- | This function lifts the given signature function to a monadic
-- signature function. Note that term algebras are instances of
-- signature functions. Hence this function also applies to term
-- algebras.
-hsigFunM :: (Monad m) => HSigFun f g -> HSigFunM m f g
-hsigFunM f = return . f
+sigFunM :: (Monad m) => SigFun f g -> SigFunM m f g
+sigFunM f = return . f
-- | This function lifts the give monadic signature function to a
-- monadic term algebra.
-htermHom' :: (HFunctor f, HFunctor g, Monad m) =>
- HSigFunM m f g -> HTermHomM m f g
-htermHom' f = liftM (HTerm . hfmap HHole) . f
+termHom' :: (HFunctor f, HFunctor g, Monad m) =>
+ SigFunM m f g -> TermHomM m f g
+termHom' f = liftM (Term . hfmap Hole) . f
-- | This function lifts the given signature function to a monadic
-- term algebra.
-htermHomM :: (HFunctor g, Monad m) => HSigFun f g -> HTermHomM m f g
-htermHomM f = hsigFunM $ htermHom f
+termHomM :: (HFunctor g, Monad m) => SigFun f g -> TermHomM m f g
+termHomM f = sigFunM $ termHom f
-- | This function applies the given monadic term homomorphism to the
-- given term/context.
-appHTermHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)
- => HTermHomM m f g -> HCxtFunM m f g
-appHTermHomM f = run
- where run :: NatM m (HCxt h f a) (HCxt h g a)
- run (HHole b) = return $ HHole b
- run (HTerm t) = liftM appHCxt . (>>= f) . hmapM run $ t
+appTermHomM :: forall f g m . (HTraversable f, HFunctor g, Monad m)
+ => TermHomM m f g -> CxtFunM m f g
+appTermHomM f = run
+ where run :: NatM m (Cxt h f a) (Cxt h g a)
+ run (Hole b) = return $ Hole b
+ run (Term t) = liftM appCxt . (>>= f) . hmapM run $ t
-- | This function applies the given monadic signature function to the
-- given context.
-appHSigFunM :: (HTraversable f, HFunctor g, Monad m) =>
- HSigFunM m f g -> HCxtFunM m f g
-appHSigFunM f = appHTermHomM $ htermHom' f
+appSigFunM :: (HTraversable f, HFunctor g, Monad m) =>
+ SigFunM m f g -> CxtFunM m f g
+appSigFunM f = appTermHomM $ termHom' f
-- | This function composes two monadic term algebras.
-compHTermHomM :: (HTraversable g, HFunctor h, Monad m)
- => HTermHomM m g h -> HTermHomM m f g -> HTermHomM m f h
-compHTermHomM f g a = g a >>= appHTermHomM f
+compTermHomM :: (HTraversable g, HFunctor h, Monad m)
+ => TermHomM m g h -> TermHomM m f g -> TermHomM m f h
+compTermHomM f g a = g a >>= appTermHomM f
{-| This function composes a monadic term algebra with a monadic algebra -}
-compHAlgM :: (HTraversable g, Monad m) => HAlgM m g a -> HTermHomM m f g -> HAlgM m f a
-compHAlgM alg talg c = hcataM' alg =<< talg c
+compAlgM :: (HTraversable g, Monad m) => AlgM m g a -> TermHomM m f g -> AlgM m f a
+compAlgM alg talg c = cataM' alg =<< talg c
-- | This function composes a monadic term algebra with a monadic
-- algebra.
-compHAlgM' :: (HTraversable g, Monad m) => HAlgM m g a -> HTermHom f g -> HAlgM m f a
-compHAlgM' alg talg = hcataM' alg . talg
+compAlgM' :: (HTraversable g, Monad m) => AlgM m g a -> TermHom f g -> AlgM m f a
+compAlgM' alg talg = cataM' alg . talg
{-| This function composes two monadic signature functions. -}
-compHSigFunM :: (Monad m) => HSigFunM m g h -> HSigFunM m f g -> HSigFunM m f h
-compHSigFunM f g a = g a >>= f
+compSigFunM :: (Monad m) => SigFunM m g h -> SigFunM m f g -> SigFunM m f h
+compSigFunM f g a = g a >>= f
----------------
-- Coalgebras --
----------------
-type HCoalg f a = a :-> f a
+type Coalg f a = a :-> f a
{-| This function unfolds the given value to a term using the given
-unravelling function. This is the unique homomorphism @a -> HTerm f@
+unravelling function. This is the unique homomorphism @a -> Term f@
from the given coalgebra of type @a -> f a@ to the final coalgebra
-@HTerm f@. -}
+@Term f@. -}
-hana :: forall f a. HFunctor f => HCoalg f a -> a :-> HTerm f
-hana f = run
- where run :: a :-> HTerm f
- run t = HTerm $ hfmap run (f t)
+ana :: forall f a. HFunctor f => Coalg f a -> a :-> Term f
+ana f = run
+ where run :: a :-> Term f
+ run t = Term $ hfmap run (f t)
-type HCoalgM m f a = NatM m a (f a)
+type CoalgM m f a = NatM m a (f a)
-- | This function unfolds the given value to a term using the given
-- monadic unravelling function. This is the unique homomorphism @a ->
--- HTerm f@ from the given coalgebra of type @a -> f a@ to the final
--- coalgebra @HTerm f@.
+-- Term f@ from the given coalgebra of type @a -> f a@ to the final
+-- coalgebra @Term f@.
-hanaM :: forall a m f. (HTraversable f, Monad m)
- => HCoalgM m f a -> NatM m a (HTerm f)
-hanaM f = run
- where run :: NatM m a (HTerm f)
- run t = liftM HTerm $ f t >>= hmapM run
+anaM :: forall a m f. (HTraversable f, Monad m)
+ => CoalgM m f a -> NatM m a (Term f)
+anaM f = run
+ where run :: NatM m a (Term f)
+ run t = liftM Term $ f t >>= hmapM run
--------------------------------
-- R-Algebras & Paramorphisms --
@@ -338,27 +330,27 @@
-- | This type represents r-algebras over functor @f@ and with domain
-- @a@.
-type HRAlg f a = f (HTerm f :*: a) :-> a
+type RAlg f a = f (Term f :*: a) :-> a
-- | This function constructs a paramorphism from the given r-algebra
-hpara :: forall f a. (HFunctor f) => HRAlg f a -> HTerm f :-> a
-hpara f = fsnd . hcata run
- where run :: HAlg f (HTerm f :*: a)
- run t = HTerm (hfmap ffst t) :*: f t
+para :: forall f a. (HFunctor f) => RAlg f a -> Term f :-> a
+para f = fsnd . cata run
+ where run :: Alg f (Term f :*: a)
+ run t = Term (hfmap ffst t) :*: f t
-- | This type represents monadic r-algebras over monad @m@ and
-- functor @f@ and with domain @a@.
-type HRAlgM m f a = NatM m (f (HTerm f :*: a)) a
+type RAlgM m f a = NatM m (f (Term f :*: a)) a
-- | This function constructs a monadic paramorphism from the given
-- monadic r-algebra
-hparaM :: forall f m a. (HTraversable f, Monad m) =>
- HRAlgM m f a -> NatM m(HTerm f) a
-hparaM f = liftM fsnd . hcataM run
- where run :: HAlgM m f (HTerm f :*: a)
+paraM :: forall f m a. (HTraversable f, Monad m) =>
+ RAlgM m f a -> NatM m(Term f) a
+paraM f = liftM fsnd . cataM run
+ where run :: AlgM m f (Term f :*: a)
run t = do
a <- f t
- return (HTerm (hfmap ffst t) :*: a)
+ return (Term (hfmap ffst t) :*: a)
--------------------------------
-- R-Coalgebras & Apomorphisms --
@@ -366,34 +358,34 @@
-- | This type represents r-coalgebras over functor @f@ and with
-- domain @a@.
-type HRCoalg f a = a :-> f (HTerm f :+: a)
+type RCoalg f a = a :-> f (Term f :+: a)
-- | This function constructs an apomorphism from the given
-- r-coalgebra.
-hapo :: forall f a . (HFunctor f) => HRCoalg f a -> a :-> HTerm f
-hapo f = run
- where run :: a :-> HTerm f
- run = HTerm . hfmap run' . f
- run' :: HTerm f :+: a :-> HTerm f
+apo :: forall f a . (HFunctor f) => RCoalg f a -> a :-> Term f
+apo f = run
+ where run :: a :-> Term f
+ run = Term . hfmap run' . f
+ run' :: Term f :+: a :-> Term f
run' (Inl t) = t
run' (Inr a) = run a
-- | This type represents monadic r-coalgebras over monad @m@ and
-- functor @f@ with domain @a@.
-type HRCoalgM m f a = NatM m a (f (HTerm f :+: a))
+type RCoalgM m f a = NatM m a (f (Term f :+: a))
-- | This function constructs a monadic apomorphism from the given
-- monadic r-coalgebra.
-hapoM :: forall f m a . (HTraversable f, Monad m) =>
- HRCoalgM m f a -> NatM m a (HTerm f)
-hapoM f = run
- where run :: NatM m a (HTerm f)
+apoM :: forall f m a . (HTraversable f, Monad m) =>
+ RCoalgM m f a -> NatM m a (Term f)
+apoM f = run
+ where run :: NatM m a (Term f)
run a = do
t <- f a
t' <- hmapM run' t
- return $ HTerm t'
- run' :: NatM m (HTerm f :+: a) (HTerm f)
+ return $ Term t'
+ run' :: NatM m (Term f :+: a) (Term f)
run' (Inl t) = return t
run' (Inr a) = run a
@@ -414,62 +406,29 @@
-- | This type represents cv-coalgebras over functor @f@ and with domain
-- @a@.
-type HCVCoalg f a = a :-> f (HContext f a)
+type CVCoalg f a = a :-> f (Context f a)
-- | This function constructs the unique futumorphism from the given
-- cv-coalgebra to the term algebra.
-hfutu :: forall f a . HFunctor f => HCVCoalg f a -> a :-> HTerm f
-hfutu coa = hana run . HHole
- where run :: HCoalg f (HContext f a)
- run (HHole a) = coa a
- run (HTerm v) = v
+futu :: forall f a . HFunctor f => CVCoalg f a -> a :-> Term f
+futu coa = ana run . Hole
+ where run :: Coalg f (Context f a)
+ run (Hole a) = coa a
+ run (Term v) = v
-- | This type represents monadic cv-coalgebras over monad @m@ and
-- functor @f@, and with domain @a@.
-type HCVCoalgM m f a = NatM m a (f (HContext f a))
+type CVCoalgM m f a = NatM m a (f (Context f a))
-- | This function constructs the unique monadic futumorphism from the
-- given monadic cv-coalgebra to the term algebra.
-hfutuM :: forall f a m . (HTraversable f, Monad m) =>
- HCVCoalgM m f a -> NatM m a (HTerm f)
-hfutuM coa = hanaM run . HHole
- where run :: HCoalgM m f (HContext f a)
- run (HHole a) = coa a
- run (HTerm v) = return v
-
-
---------------------------
--- Exponential Functors --
---------------------------
-
-{-| Catamorphism for higher-order exponential functors. -}
-hcataE :: forall f a . HExpFunctor f => HAlg f a -> HTerm f :-> a
-hcataE f = cataFS . toHCxt
- where cataFS :: HExpFunctor f => HContext f a :-> a
- cataFS (HHole x) = x
- cataFS (HTerm t) = f (hxmap cataFS HHole t)
-
-
-{-{-| Anamorphism for higher-order exponential functors. -}
-hanaE :: forall a f . HExpFunctor f => HCoalg f a -> a :-> HTerm (f :&: a)
-hanaE f = run
- where run :: a :-> HTerm (f :&: a)
- run t = HTerm $ hxmap run (snd . hprojectP . unHTerm) (f t) :&: t-}
-
--- | Variant of 'appHCxt' for contexts over 'HExpFunctor' signatures.
-appHCxtE :: (HExpFunctor f) => HContext f (HCxt h f a) :-> HCxt h f a
-appHCxtE (HHole x) = x
-appHCxtE (HTerm t) = HTerm (hxmap appHCxtE HHole t)
-
--- | Variant of 'appHTermHom' for term homomorphisms from and to
--- 'HExpFunctor' signatures.
-appHTermHomE :: forall f g . (HExpFunctor f, HExpFunctor g) => HTermHom f g
- -> HTerm f :-> HTerm g
-appHTermHomE f = cataFS . toHCxt
- where cataFS :: HContext f (HTerm g) :-> HTerm g
- cataFS (HHole x) = x
- cataFS (HTerm t) = appHCxtE (f (hxmap cataFS HHole t))
+futuM :: forall f a m . (HTraversable f, Monad m) =>
+ CVCoalgM m f a -> NatM m a (Term f)
+futuM coa = anaM run . Hole
+ where run :: CoalgM m f (Context f a)
+ run (Hole a) = coa a
+ run (Term v) = return v
diff --git a/src/Data/Comp/Multi/Equality.hs b/src/Data/Comp/Multi/Equality.hs
--- a/src/Data/Comp/Multi/Equality.hs
+++ b/src/Data/Comp/Multi/Equality.hs
@@ -31,25 +31,25 @@
'EqF' is propagated through sums.
-}
-instance (HEqF f, HEqF g) => HEqF (f :++: g) where
- heqF (HInl x) (HInl y) = heqF x y
- heqF (HInr x) (HInr y) = heqF x y
+instance (HEqF f, HEqF g) => HEqF (f :+: g) where
+ heqF (Inl x) (Inl y) = heqF x y
+ heqF (Inr x) (Inr y) = heqF x y
heqF _ _ = False
{-|
From an 'EqF' functor an 'Eq' instance of the corresponding
term type can be derived.
-}
-instance (HEqF f) => HEqF (HCxt h f) where
+instance (HEqF f) => HEqF (Cxt h f) where
- heqF (HTerm e1) (HTerm e2) = e1 `heqF` e2
- heqF (HHole h1) (HHole h2) = h1 `keq` h2
+ heqF (Term e1) (Term e2) = e1 `heqF` e2
+ heqF (Hole h1) (Hole h2) = h1 `keq` h2
heqF _ _ = False
-instance (HEqF f, KEq a) => KEq (HCxt h f a) where
+instance (HEqF f, KEq a) => KEq (Cxt h f a) where
keq = heqF
-instance KEq HNothing where
+instance KEq Nothing where
keq _ = undefined
diff --git a/src/Data/Comp/Multi/ExpFunctor.hs b/src/Data/Comp/Multi/ExpFunctor.hs
deleted file mode 100644
--- a/src/Data/Comp/Multi/ExpFunctor.hs
+++ /dev/null
@@ -1,24 +0,0 @@
-{-# LANGUAGE TypeOperators, RankNTypes #-}
---------------------------------------------------------------------------------
--- |
--- Module : Data.Comp.Multi.ExpFunctor
--- Copyright : (c) 2011 Tom Hvitved
--- License : BSD3
--- Maintainer : Tom Hvitved
--- Stability : experimental
--- Portability : non-portable (GHC Extensions)
---
--- This module defines higher-order exponential functors.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Multi.ExpFunctor
- (
- HExpFunctor(..)
- ) where
-
-import Data.Comp.Multi.Functor
-
-{-| Higher-order exponential functors are higher-order functors that may be both covariant (as ordinary higher-order functors) and contravariant. -}
-class HExpFunctor f where
- hxmap :: (a :-> b) -> (b :-> a) -> f a :-> f b
diff --git a/src/Data/Comp/Multi/Ops.hs b/src/Data/Comp/Multi/Ops.hs
--- a/src/Data/Comp/Multi/Ops.hs
+++ b/src/Data/Comp/Multi/Ops.hs
@@ -21,144 +21,139 @@
import Data.Comp.Multi.Functor
import Data.Comp.Multi.Foldable
import Data.Comp.Multi.Traversable
-import Data.Comp.Multi.ExpFunctor
-import Data.Comp.Ops
+import qualified Data.Comp.Ops as O
import Control.Monad
import Control.Applicative
-infixr 5 :++:
+infixr 5 :+:
-- |Data type defining coproducts.
-data (f :++: g) (h :: * -> *) e = HInl (f h e)
- | HInr (g h e)
-
-instance (HFunctor f, HFunctor g) => HFunctor (f :++: g) where
- hfmap f (HInl v) = HInl $ hfmap f v
- hfmap f (HInr v) = HInr $ hfmap f v
+data (f :+: g) (h :: * -> *) e = Inl (f h e)
+ | Inr (g h e)
-instance (HFoldable f, HFoldable g) => HFoldable (f :++: g) where
- hfold (HInl e) = hfold e
- hfold (HInr e) = hfold e
- hfoldMap f (HInl e) = hfoldMap f e
- hfoldMap f (HInr e) = hfoldMap f e
- hfoldr f b (HInl e) = hfoldr f b e
- hfoldr f b (HInr e) = hfoldr f b e
- hfoldl f b (HInl e) = hfoldl f b e
- hfoldl f b (HInr e) = hfoldl f b e
+instance (HFunctor f, HFunctor g) => HFunctor (f :+: g) where
+ hfmap f (Inl v) = Inl $ hfmap f v
+ hfmap f (Inr v) = Inr $ hfmap f v
- hfoldr1 f (HInl e) = hfoldr1 f e
- hfoldr1 f (HInr e) = hfoldr1 f e
- hfoldl1 f (HInl e) = hfoldl1 f e
- hfoldl1 f (HInr e) = hfoldl1 f e
+instance (HFoldable f, HFoldable g) => HFoldable (f :+: g) where
+ hfold (Inl e) = hfold e
+ hfold (Inr e) = hfold e
+ hfoldMap f (Inl e) = hfoldMap f e
+ hfoldMap f (Inr e) = hfoldMap f e
+ hfoldr f b (Inl e) = hfoldr f b e
+ hfoldr f b (Inr e) = hfoldr f b e
+ hfoldl f b (Inl e) = hfoldl f b e
+ hfoldl f b (Inr e) = hfoldl f b e
-instance (HTraversable f, HTraversable g) => HTraversable (f :++: g) where
- htraverse f (HInl e) = HInl <$> htraverse f e
- htraverse f (HInr e) = HInr <$> htraverse f e
- hmapM f (HInl e) = HInl `liftM` hmapM f e
- hmapM f (HInr e) = HInr `liftM` hmapM f e
+ hfoldr1 f (Inl e) = hfoldr1 f e
+ hfoldr1 f (Inr e) = hfoldr1 f e
+ hfoldl1 f (Inl e) = hfoldl1 f e
+ hfoldl1 f (Inr e) = hfoldl1 f e
-instance (HExpFunctor f, HExpFunctor g) => HExpFunctor (f :++: g) where
- hxmap f g (HInl v) = HInl $ hxmap f g v
- hxmap f g (HInr v) = HInr $ hxmap f g v
+instance (HTraversable f, HTraversable g) => HTraversable (f :+: g) where
+ htraverse f (Inl e) = Inl <$> htraverse f e
+ htraverse f (Inr e) = Inr <$> htraverse f e
+ hmapM f (Inl e) = Inl `liftM` hmapM f e
+ hmapM f (Inr e) = Inr `liftM` hmapM f e
-- |The subsumption relation.
-class (sub :: (* -> *) -> * -> *) :<<: sup where
- hinj :: sub a :-> sup a
- hproj :: NatM Maybe (sup a) (sub a)
+class (sub :: (* -> *) -> * -> *) :<: sup where
+ inj :: sub a :-> sup a
+ proj :: NatM Maybe (sup a) (sub a)
-instance (:<<:) f f where
- hinj = id
- hproj = Just
+instance (:<:) f f where
+ inj = id
+ proj = Just
-instance (:<<:) f (f :++: g) where
- hinj = HInl
- hproj (HInl x) = Just x
- hproj (HInr _) = Nothing
+instance (:<:) f (f :+: g) where
+ inj = Inl
+ proj (Inl x) = Just x
+ proj (Inr _) = Nothing
-instance (f :<<: g) => (:<<:) f (h :++: g) where
- hinj = HInr . hinj
- hproj (HInr x) = hproj x
- hproj (HInl _) = Nothing
+instance (f :<: g) => (:<:) f (h :+: g) where
+ inj = Inr . inj
+ proj (Inr x) = proj x
+ proj (Inl _) = Nothing
-- Products
-infixr 8 :**:
+infixr 8 :*:
-data (f :**: g) a = f a :**: g a
+data (f :*: g) a = f a :*: g a
-hfst :: (f :**: g) a -> f a
-hfst (x :**: _) = x
+fst :: (f :*: g) a -> f a
+fst (x :*: _) = x
-hsnd :: (f :**: g) a -> g a
-hsnd (_ :**: x) = x
+snd :: (f :*: g) a -> g a
+snd (_ :*: x) = x
-- Constant Products
-infixr 7 :&&:
+infixr 7 :&:
-- | This data type adds a constant product to a
-- signature. Alternatively, this could have also been defined as
--
--- @data (f :&&: a) (g :: * -> *) e = f g e :&&: a e@
+-- @data (f :&: a) (g :: * -> *) e = f g e :&: a e@
--
-- This is too general, however, for example for 'productHTermHom'.
-data (f :&&: a) (g :: * -> *) e = f g e :&&: a
+data (f :&: a) (g :: * -> *) e = f g e :&: a
-instance (HFunctor f) => HFunctor (f :&&: a) where
- hfmap f (v :&&: c) = hfmap f v :&&: c
+instance (HFunctor f) => HFunctor (f :&: a) where
+ hfmap f (v :&: c) = hfmap f v :&: c
-instance (HFoldable f) => HFoldable (f :&&: a) where
- hfold (v :&&: _) = hfold v
- hfoldMap f (v :&&: _) = hfoldMap f v
- hfoldr f e (v :&&: _) = hfoldr f e v
- hfoldl f e (v :&&: _) = hfoldl f e v
- hfoldr1 f (v :&&: _) = hfoldr1 f v
- hfoldl1 f (v :&&: _) = hfoldl1 f v
+instance (HFoldable f) => HFoldable (f :&: a) where
+ hfold (v :&: _) = hfold v
+ hfoldMap f (v :&: _) = hfoldMap f v
+ hfoldr f e (v :&: _) = hfoldr f e v
+ hfoldl f e (v :&: _) = hfoldl f e v
+ hfoldr1 f (v :&: _) = hfoldr1 f v
+ hfoldl1 f (v :&: _) = hfoldl1 f v
-instance (HTraversable f) => HTraversable (f :&&: a) where
- htraverse f (v :&&: c) = (:&&: c) <$> (htraverse f v)
- hmapM f (v :&&: c) = liftM (:&&: c) (hmapM f v)
+instance (HTraversable f) => HTraversable (f :&: a) where
+ htraverse f (v :&: c) = (:&: c) <$> (htraverse f v)
+ hmapM f (v :&: c) = liftM (:&: c) (hmapM f v)
-- | This class defines how to distribute a product over a sum of
-- signatures.
-class HDistProd (s :: (* -> *) -> * -> *) p s' | s' -> s, s' -> p where
+class DistProd (s :: (* -> *) -> * -> *) p s' | s' -> s, s' -> p where
-- | This function injects a product a value over a signature.
- hinjectP :: p -> s a :-> s' a
- hprojectP :: s' a :-> (s a :&: p)
+ injectP :: p -> s a :-> s' a
+ projectP :: s' a :-> (s a O.:&: p)
-class HRemoveP (s :: (* -> *) -> * -> *) s' | s -> s' where
- hremoveP :: s a :-> s' a
+class RemoveP (s :: (* -> *) -> * -> *) s' | s -> s' where
+ removeP :: s a :-> s' a
-instance (HRemoveP s s') => HRemoveP (f :&&: p :++: s) (f :++: s') where
- hremoveP (HInl (v :&&: _)) = HInl v
- hremoveP (HInr v) = HInr $ hremoveP v
+instance (RemoveP s s') => RemoveP (f :&: p :+: s) (f :+: s') where
+ removeP (Inl (v :&: _)) = Inl v
+ removeP (Inr v) = Inr $ removeP v
-instance HRemoveP (f :&&: p) f where
- hremoveP (v :&&: _) = v
+instance RemoveP (f :&: p) f where
+ removeP (v :&: _) = v
-instance HDistProd f p (f :&&: p) where
+instance DistProd f p (f :&: p) where
- hinjectP p v = v :&&: p
+ injectP p v = v :&: p
- hprojectP (v :&&: p) = v :&: p
+ projectP (v :&: p) = v O.:&: p
-instance (HDistProd s p s') => HDistProd (f :++: s) p ((f :&&: p) :++: s') where
- hinjectP p (HInl v) = HInl (v :&&: p)
- hinjectP p (HInr v) = HInr $ hinjectP p v
+instance (DistProd s p s') => DistProd (f :+: s) p ((f :&: p) :+: s') where
+ injectP p (Inl v) = Inl (v :&: p)
+ injectP p (Inr v) = Inr $ injectP p v
- hprojectP (HInl (v :&&: p)) = (HInl v :&: p)
- hprojectP (HInr v) = let (v' :&: p) = hprojectP v
- in (HInr v' :&: p)
+ projectP (Inl (v :&: p)) = (Inl v O.:&: p)
+ projectP (Inr v) = let (v' O.:&: p) = projectP v
+ in (Inr v' O.:&: p)
diff --git a/src/Data/Comp/Multi/Product.hs b/src/Data/Comp/Multi/Product.hs
--- a/src/Data/Comp/Multi/Product.hs
+++ b/src/Data/Comp/Multi/Product.hs
@@ -15,21 +15,21 @@
--------------------------------------------------------------------------------
module Data.Comp.Multi.Product
- ( (:&&:) (..),
- HDistProd (..),
- HRemoveP (..),
+ ( (:&:) (..),
+ DistProd (..),
+ RemoveP (..),
liftP,
constP,
liftP',
stripP,
- productHTermHom,
- hproject'
+ productTermHom,
+ project'
)where
import Data.Comp.Multi.Term
import Data.Comp.Multi.Sum
import Data.Comp.Multi.Ops
-import Data.Comp.Ops
+import qualified Data.Comp.Ops as O
import Data.Comp.Multi.Algebra
import Data.Comp.Multi.Functor
@@ -42,46 +42,46 @@
-- from a functor to a function with a domain constructed with the
-- same functor but with an additional product.
-liftP :: (HRemoveP s s') => (s' a :-> t) -> s a :-> t
-liftP f v = f (hremoveP v)
+liftP :: (RemoveP s s') => (s' a :-> t) -> s a :-> t
+liftP f v = f (removeP v)
-- | This function annotates each sub term of the given term with the
-- given value (of type a).
-constP :: (HDistProd f p g, HFunctor f, HFunctor g)
- => p -> HCxt h f a :-> HCxt h g a
-constP c = appHSigFun (hinjectP c)
+constP :: (DistProd f p g, HFunctor f, HFunctor g)
+ => p -> Cxt h f a :-> Cxt h g a
+constP c = appSigFun (injectP c)
-- | This function transforms a function with a domain constructed
-- from a functor to a function with a domain constructed with the
-- same functor but with an additional product.
-liftP' :: (HDistProd s' p s, HFunctor s, HFunctor s')
- => (s' a :-> HCxt h s' a) -> s a :-> HCxt h s a
-liftP' f v = let (v' :&: p) = hprojectP v
+liftP' :: (DistProd s' p s, HFunctor s, HFunctor s')
+ => (s' a :-> Cxt h s' a) -> s a :-> Cxt h s a
+liftP' f v = let (v' O.:&: p) = projectP v
in constP p (f v')
{-| This function strips the products from a term over a
functor whith products. -}
-stripP :: (HFunctor f, HRemoveP g f, HFunctor g)
- => HCxt h g a :-> HCxt h f a
-stripP = appHSigFun hremoveP
+stripP :: (HFunctor f, RemoveP g f, HFunctor g)
+ => Cxt h g a :-> Cxt h f a
+stripP = appSigFun removeP
-productHTermHom :: (HDistProd f p f', HDistProd g p g', HFunctor g, HFunctor g')
- => HTermHom f g -> HTermHom f' g'
-productHTermHom alg f' = constP p (alg f)
- where (f :&: p) = hprojectP f'
+productTermHom :: (DistProd f p f', DistProd g p g', HFunctor g, HFunctor g')
+ => TermHom f g -> TermHom f' g'
+productTermHom alg f' = constP p (alg f)
+ where (f O.:&: p) = projectP f'
--- | This function is similar to 'hproject' but applies to signatures
+-- | This function is similar to 'project' but applies to signatures
-- with a product which is then ignored.
--- hproject' :: (HRemoveP s s',s :<<: f) =>
--- NatM Maybe (HCxt h f a) (s' (HCxt h f a))
-hproject' v = liftM hremoveP $ hproject v
+-- project' :: (RemoveP s s',s :<: f) =>
+-- NatM Maybe (Cxt h f a) (s' (Cxt h f a))
+project' v = liftM removeP $ project v
diff --git a/src/Data/Comp/Multi/Show.hs b/src/Data/Comp/Multi/Show.hs
--- a/src/Data/Comp/Multi/Show.hs
+++ b/src/Data/Comp/Multi/Show.hs
@@ -26,24 +26,24 @@
import Data.Comp.Multi.Functor
import Data.Comp.Derive
-instance KShow HNothing where
+instance KShow Nothing where
kshow _ = undefined
instance KShow (K String) where
kshow = id
-instance (HShowF f, HFunctor f) => HShowF (HCxt h f) where
- hshowF (HHole s) = s
- hshowF (HTerm t) = hshowF $ hfmap hshowF t
+instance (HShowF f, HFunctor f) => HShowF (Cxt h f) where
+ hshowF (Hole s) = s
+ hshowF (Term t) = hshowF $ hfmap hshowF t
-instance (HShowF f, HFunctor f, KShow a) => KShow (HCxt h f a) where
- kshow = hfree hshowF kshow
+instance (HShowF f, HFunctor f, KShow a) => KShow (Cxt h f a) where
+ kshow = free hshowF kshow
instance (KShow f) => Show (f i) where
show = unK . kshow
-instance (HShowF f, Show p) => HShowF (f :&&: p) where
- hshowF (v :&&: p) = K $ unK (hshowF v) ++ " :&&: " ++ show p
+instance (HShowF f, Show p) => HShowF (f :&: p) where
+ hshowF (v :&: p) = K $ unK (hshowF v) ++ " :&: " ++ show p
-instance (HShowF f, HShowF g) => HShowF (f :++: g) where
- hshowF (HInl f) = hshowF f
- hshowF (HInr g) = hshowF g
+instance (HShowF f, HShowF g) => HShowF (f :+: g) where
+ hshowF (Inl f) = hshowF f
+ hshowF (Inr g) = hshowF g
diff --git a/src/Data/Comp/Multi/Sum.hs b/src/Data/Comp/Multi/Sum.hs
--- a/src/Data/Comp/Multi/Sum.hs
+++ b/src/Data/Comp/Multi/Sum.hs
@@ -16,184 +16,165 @@
module Data.Comp.Multi.Sum
(
- (:<<:)(..),
- (:++:)(..),
+ (:<:)(..),
+ (:+:)(..),
-- * Projections for Signatures and Terms
- hproj2,
- hproj3,
- hproject,
- hproject2,
- hproject3,
- deepHProject,
- deepHProject2,
- deepHProject3,
--- deepHProject',
--- deepHProject2',
--- deepHProject3',
+ proj2,
+ proj3,
+ project,
+ project2,
+ project3,
+ deepProject,
+ deepProject2,
+ deepProject3,
+-- deepProject',
+-- deepProject2',
+-- deepProject3',
-- * Injections for Signatures and Terms
- hinj2,
- hinj3,
- hinject,
- hinject2,
- hinject3,
- deepHInject,
- deepHInject2,
- deepHInject3,
- deepHInjectE,
- deepHInjectE2,
- deepHInjectE3,
+ inj2,
+ inj3,
+ inject,
+ inject2,
+ inject3,
+ deepInject,
+ deepInject2,
+ deepInject3,
-- * Injections and Projections for Constants
- hinjectHConst,
- hinjectHConst2,
- hinjectHConst3,
- hprojectHConst,
- hinjectHCxt,
- liftHCxt,
- substHHoles,
--- substHHoles'
+ injectConst,
+ injectConst2,
+ injectConst3,
+ projectConst,
+ injectCxt,
+ liftCxt,
+ substHoles,
+-- substHoles'
) where
import Data.Comp.Multi.Functor
import Data.Comp.Multi.Traversable
-import Data.Comp.Multi.ExpFunctor
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term
import Data.Comp.Multi.Algebra
import Control.Monad (liftM)
-{-| A variant of 'hproj' for binary sum signatures. -}
-hproj2 :: forall f g1 g2 a i. (g1 :<<: f, g2 :<<: f) =>
- f a i -> Maybe (((g1 :++: g2) a) i)
-hproj2 x = case hproj x of
- Just (y :: g1 a i) -> Just $ hinj y
- _ -> liftM hinj (hproj x :: Maybe (g2 a i))
+{-| A variant of 'proj' for binary sum signatures. -}
+proj2 :: forall f g1 g2 a i. (g1 :<: f, g2 :<: f) =>
+ f a i -> Maybe (((g1 :+: g2) a) i)
+proj2 x = case proj x of
+ Just (y :: g1 a i) -> Just $ inj y
+ _ -> liftM inj (proj x :: Maybe (g2 a i))
-{-| A variant of 'hproj' for ternary sum signatures. -}
-hproj3 :: forall f g1 g2 g3 a i. (g1 :<<: f, g2 :<<: f, g3 :<<: f) =>
- f a i -> Maybe (((g1 :++: g2 :++: g3) a) i)
-hproj3 x = case hproj x of
- Just (y :: g1 a i) -> Just $ hinj y
- _ -> case hproj x of
- Just (y :: g2 a i) -> Just $ hinj y
- _ -> liftM hinj (hproj x :: Maybe (g3 a i))
+{-| A variant of 'proj' for ternary sum signatures. -}
+proj3 :: forall f g1 g2 g3 a i. (g1 :<: f, g2 :<: f, g3 :<: f) =>
+ f a i -> Maybe (((g1 :+: g2 :+: g3) a) i)
+proj3 x = case proj x of
+ Just (y :: g1 a i) -> Just $ inj y
+ _ -> case proj x of
+ Just (y :: g2 a i) -> Just $ inj y
+ _ -> liftM inj (proj x :: Maybe (g3 a i))
-- |Project the outermost layer of a term to a sub signature.
-hproject :: (g :<<: f) => NatM Maybe (HCxt h f a) (g (HCxt h f a))
-hproject (HHole _) = Nothing
-hproject (HTerm t) = hproj t
+project :: (g :<: f) => NatM Maybe (Cxt h f a) (g (Cxt h f a))
+project (Hole _) = Nothing
+project (Term t) = proj t
-- |Project the outermost layer of a term to a binary sub signature.
-hproject2 :: (g1 :<<: f, g2 :<<: f) =>
- NatM Maybe (HCxt h f a) ((g1 :++: g2) (HCxt h f a))
-hproject2 (HHole _) = Nothing
-hproject2 (HTerm t) = hproj2 t
+project2 :: (g1 :<: f, g2 :<: f) =>
+ NatM Maybe (Cxt h f a) ((g1 :+: g2) (Cxt h f a))
+project2 (Hole _) = Nothing
+project2 (Term t) = proj2 t
-- |Project the outermost layer of a term to a ternary sub signature.
-hproject3 :: (g1 :<<: f, g2 :<<: f, g3 :<<: f) =>
- NatM Maybe (HCxt h f a) ((g1 :++: g2 :++: g3) (HCxt h f a))
-hproject3 (HHole _) = Nothing
-hproject3 (HTerm t) = hproj3 t
+project3 :: (g1 :<: f, g2 :<: f, g3 :<: f) =>
+ NatM Maybe (Cxt h f a) ((g1 :+: g2 :+: g3) (Cxt h f a))
+project3 (Hole _) = Nothing
+project3 (Term t) = proj3 t
-- |Project a term to a term over a sub signature.
-deepHProject :: (HTraversable f, HFunctor g, g :<<: f)
- => NatM Maybe (HCxt h f a) (HCxt h g a)
-deepHProject = appHSigFunM hproj
+deepProject :: (HTraversable f, HFunctor g, g :<: f)
+ => NatM Maybe (Cxt h f a) (Cxt h g a)
+deepProject = appSigFunM proj
-- |Project a term to a term over a binary sub signature.
-deepHProject2 :: (HTraversable f, HFunctor g1, HFunctor g2,
- g1 :<<: f, g2 :<<: f)
- => NatM Maybe (HCxt h f a) (HCxt h (g1 :++: g2) a)
-deepHProject2 = appHSigFunM hproj2
+deepProject2 :: (HTraversable f, HFunctor g1, HFunctor g2,
+ g1 :<: f, g2 :<: f)
+ => NatM Maybe (Cxt h f a) (Cxt h (g1 :+: g2) a)
+deepProject2 = appSigFunM proj2
-- |Project a term to a term over a ternary sub signature.
-deepHProject3 :: (HTraversable f, HFunctor g1, HFunctor g2, HFunctor g3,
- g1 :<<: f, g2 :<<: f, g3 :<<: f)
- => NatM Maybe (HCxt h f a) (HCxt h (g1 :++: g2 :++: g3) a)
-deepHProject3 = appHSigFunM hproj3
+deepProject3 :: (HTraversable f, HFunctor g1, HFunctor g2, HFunctor g3,
+ g1 :<: f, g2 :<: f, g3 :<: f)
+ => NatM Maybe (Cxt h f a) (Cxt h (g1 :+: g2 :+: g3) a)
+deepProject3 = appSigFunM proj3
-{-| A variant of 'hinj' for binary sum signatures. -}
-hinj2 :: (f1 :<<: g, f2 :<<: g) => (f1 :++: f2) a :-> g a
-hinj2 (HInl x) = hinj x
-hinj2 (HInr y) = hinj y
+{-| A variant of 'inj' for binary sum signatures. -}
+inj2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) a :-> g a
+inj2 (Inl x) = inj x
+inj2 (Inr y) = inj y
-{-| A variant of 'hinj' for ternary sum signatures. -}
-hinj3 :: (f1 :<<: g, f2 :<<: g, f3 :<<: g) => (f1 :++: f2 :++: f3) a :-> g a
-hinj3 (HInl x) = hinj x
-hinj3 (HInr y) = hinj2 y
+{-| A variant of 'inj' for ternary sum signatures. -}
+inj3 :: (f1 :<: g, f2 :<: g, f3 :<: g) => (f1 :+: f2 :+: f3) a :-> g a
+inj3 (Inl x) = inj x
+inj3 (Inr y) = inj2 y
-- |Inject a term where the outermost layer is a sub signature.
-hinject :: (g :<<: f) => g (HCxt h f a) :-> HCxt h f a
-hinject = HTerm . hinj
+inject :: (g :<: f) => g (Cxt h f a) :-> Cxt h f a
+inject = Term . inj
-- |Inject a term where the outermost layer is a binary sub signature.
-hinject2 :: (f1 :<<: g, f2 :<<: g) => (f1 :++: f2) (HCxt h g a) :-> HCxt h g a
-hinject2 = HTerm . hinj2
+inject2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) (Cxt h g a) :-> Cxt h g a
+inject2 = Term . inj2
-- |Inject a term where the outermost layer is a ternary sub signature.
-hinject3 :: (f1 :<<: g, f2 :<<: g, f3 :<<: g)
- => (f1 :++: f2 :++: f3) (HCxt h g a) :-> HCxt h g a
-hinject3 = HTerm . hinj3
+inject3 :: (f1 :<: g, f2 :<: g, f3 :<: g)
+ => (f1 :+: f2 :+: f3) (Cxt h g a) :-> Cxt h g a
+inject3 = Term . inj3
-- |Inject a term over a sub signature to a term over larger signature.
-deepHInject :: (HFunctor g, HFunctor f, g :<<: f) => HCxt h g a :-> HCxt h f a
-deepHInject = appHSigFun hinj
+deepInject :: (HFunctor g, HFunctor f, g :<: f) => Cxt h g a :-> Cxt h f a
+deepInject = appSigFun inj
-- |Inject a term over a binary sub signature to a term over larger signature.
-deepHInject2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<<: g, f2 :<<: g)
- => HCxt h (f1 :++: f2) a :-> HCxt h g a
-deepHInject2 = appHSigFun hinj2
+deepInject2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g)
+ => Cxt h (f1 :+: f2) a :-> Cxt h g a
+deepInject2 = appSigFun inj2
-- |Inject a term over a ternary sub signature to a term over larger signature.
-deepHInject3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,
- f1 :<<: g, f2 :<<: g, f3 :<<: g)
- => HCxt h (f1 :++: f2 :++: f3) a :-> HCxt h g a
-deepHInject3 = appHSigFun hinj3
-
-{-| A variant of 'deepHInject' for exponential signatures. -}
-deepHInjectE :: (HExpFunctor g, g :<<: f) => HTerm g :-> HTerm f
-deepHInjectE = hcataE hinject
-
-{-| A variant of 'deepHInject2' for exponential signatures. -}
-deepHInjectE2 :: (HExpFunctor g1, HExpFunctor g2, g1 :<<: f, g2 :<<: f) =>
- HTerm (g1 :++: g2) :-> HTerm f
-deepHInjectE2 = hcataE hinject2
-
-{-| A variant of 'deepHInject3' for exponential signatures. -}
-deepHInjectE3 :: (HExpFunctor g1, HExpFunctor g2, HExpFunctor g3,
- g1 :<<: f, g2 :<<: f, g3 :<<: f) =>
- HTerm (g1 :++: g2 :++: g3) :-> HTerm f
-deepHInjectE3 = hcataE hinject3
+deepInject3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,
+ f1 :<: g, f2 :<: g, f3 :<: g)
+ => Cxt h (f1 :+: f2 :+: f3) a :-> Cxt h g a
+deepInject3 = appSigFun inj3
-- | This function injects a whole context into another context.
-hinjectHCxt :: (HFunctor g, g :<<: f) => HCxt h' g (HCxt h f a) :-> HCxt h f a
-hinjectHCxt = hcata' hinject
+injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
+injectCxt = cata' inject
-- | This function lifts the given functor to a context.
-liftHCxt :: (HFunctor f, g :<<: f) => g a :-> HContext f a
-liftHCxt g = simpHCxt $ hinj g
+liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a
+liftCxt g = simpCxt $ inj g
-- | This function applies the given context with hole type @a@ to a
-- family @f@ of contexts (possibly terms) indexed by @a@. That is,
-- each hole @h@ is replaced by the context @f h@.
-substHHoles :: (HFunctor f, HFunctor g, f :<<: g)
- => (v :-> HCxt h g a) -> HCxt h' f v :-> HCxt h g a
-substHHoles f c = hinjectHCxt $ hfmap f c
+substHoles :: (HFunctor f, HFunctor g, f :<: g)
+ => (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
+substHoles f c = injectCxt $ hfmap f c
-hinjectHConst :: (HFunctor g, g :<<: f) => HConst g :-> HCxt h f a
-hinjectHConst = hinject . hfmap (const undefined)
+injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a
+injectConst = inject . hfmap (const undefined)
-hinjectHConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<<: g, f2 :<<: g)
- => HConst (f1 :++: f2) :-> HCxt h g a
-hinjectHConst2 = hinject2 . hfmap (const undefined)
+injectConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g)
+ => Const (f1 :+: f2) :-> Cxt h g a
+injectConst2 = inject2 . hfmap (const undefined)
-hinjectHConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,
- f1 :<<: g, f2 :<<: g, f3 :<<: g)
- => HConst (f1 :++: f2 :++: f3) :-> HCxt h g a
-hinjectHConst3 = hinject3 . hfmap (const undefined)
+injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,
+ f1 :<: g, f2 :<: g, f3 :<: g)
+ => Const (f1 :+: f2 :+: f3) :-> Cxt h g a
+injectConst3 = inject3 . hfmap (const undefined)
-hprojectHConst :: (HFunctor g, g :<<: f) => NatM Maybe (HCxt h f a) (HConst g)
-hprojectHConst = fmap (hfmap (const (K ()))) . hproject
+projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
+projectConst = fmap (hfmap (const (K ()))) . project
diff --git a/src/Data/Comp/Multi/Term.hs b/src/Data/Comp/Multi/Term.hs
--- a/src/Data/Comp/Multi/Term.hs
+++ b/src/Data/Comp/Multi/Term.hs
@@ -16,73 +16,74 @@
--------------------------------------------------------------------------------
module Data.Comp.Multi.Term
- (HCxt (..),
- HHole,
- HNoHole,
- HContext,
- HNothing,
- HTerm,
- HConst,
- constHTerm,
- unHTerm,
- toHCxt,
- simpHCxt
+ (Cxt (..),
+ Hole,
+ NoHole,
+ Context,
+ Nothing,
+ Term,
+ Const,
+ constTerm,
+ unTerm,
+ toCxt,
+ simpCxt
) where
import Data.Comp.Multi.Functor
import Unsafe.Coerce
-type HConst (f :: (* -> *) -> * -> *) = f (K ())
+type Const (f :: (* -> *) -> * -> *) = f (K ())
-- | This function converts a constant to a term. This assumes that
-- the argument is indeed a constant, i.e. does not have a value for
-- the argument type of the functor f.
-constHTerm :: (HFunctor f) => HConst f :-> HTerm f
-constHTerm = HTerm . hfmap (const undefined)
+constTerm :: (HFunctor f) => Const f :-> Term f
+constTerm = Term . hfmap (const undefined)
-- | This data type represents contexts over a signature. Contexts are
-- terms containing zero or more holes. The first type parameter is
--- supposed to be one of the phantom types 'HHole' and 'HNoHole'. The
+-- supposed to be one of the phantom types 'Hole' and 'NoHole'. The
-- second parameter is the signature of the context. The third
-- parameter is the type family of the holes. The last parameter is
-- the index/label.
-data HCxt h f a i where
- HTerm :: f (HCxt h f a) i -> HCxt h f a i
- HHole :: a i -> HCxt HHole f a i
+data Cxt h f a i where
+ Term :: f (Cxt h f a) i -> Cxt h f a i
+ Hole :: a i -> Cxt Hole f a i
--- | Phantom type that signals that a 'HCxt' might contain holes.
-data HHole
--- | Phantom type that signals that a 'HCxt' does not contain holes.
-data HNoHole
+-- | Phantom type that signals that a 'Cxt' might contain holes.
+data Hole
+-- | Phantom type that signals that a 'Cxt' does not contain holes.
+data NoHole
-- | A context might contain holes.
-type HContext = HCxt HHole
+type Context = Cxt Hole
-{-| Phantom type family used to define 'HTerm'. -}
-data HNothing :: * -> *
+{-| Phantom type family used to define 'Term'. -}
+data Nothing :: * -> *
-instance Show (HNothing i) where
-instance Eq (HNothing i) where
-instance Ord (HNothing i) where
+instance Show (Nothing i) where
+instance Eq (Nothing i) where
+instance Ord (Nothing i) where
-- | A (higher-order) term is a context with no holes.
-type HTerm f = HCxt HNoHole f HNothing
+type Term f = Cxt NoHole f Nothing
-- | This function unravels the given term at the topmost layer.
-unHTerm :: HTerm f t -> f (HTerm f) t
-unHTerm (HTerm t) = t
+unTerm :: Term f t -> f (Term f) t
+unTerm (Term t) = t
-instance (HFunctor f) => HFunctor (HCxt h f) where
- hfmap f (HHole x) = HHole (f x)
- hfmap f (HTerm t) = HTerm (hfmap (hfmap f) t)
+instance (HFunctor f) => HFunctor (Cxt h f) where
+ hfmap f (Hole x) = Hole (f x)
+ hfmap f (Term t) = Term (hfmap (hfmap f) t)
-simpHCxt :: (HFunctor f) => f a i -> HContext f a i
-simpHCxt = HTerm . hfmap HHole
+simpCxt :: (HFunctor f) => f a i -> Context f a i
+simpCxt = Term . hfmap Hole
-toHCxt :: HTerm f i -> HContext f a i
-toHCxt = unsafeCoerce
---toHCxt :: (HFunctor f) => HTerm f i -> HContext f a i
---toHCxt (HTerm t) = HTerm $ hfmap toHCxt t
+{-| Cast a term over a signature to a context over the same signature. -}
+toCxt :: (HFunctor f) => Term f :-> Context f a
+{-# INLINE toCxt #-}
+toCxt = unsafeCoerce
+-- equivalentto @Term . (hfmap toCxt) . unTerm@
diff --git a/src/Data/Comp/Multi/Variables.hs b/src/Data/Comp/Multi/Variables.hs
--- a/src/Data/Comp/Multi/Variables.hs
+++ b/src/Data/Comp/Multi/Variables.hs
@@ -10,142 +10,165 @@
-- Stability : experimental
-- Portability : non-portable (GHC Extensions)
--
--- This module defines an abstraction notion of a variable in a term. All
--- definitions are generalised versions of those in "Data.Comp.Variables".
+-- This module defines an abstract notion of (bound) variables in compositional
+-- data types, and capture-avoiding substitution. All definitions are
+-- generalised versions of those in "Data.Comp.Variables".
--
--------------------------------------------------------------------------------
-module Data.Comp.Multi.Variables where
+module Data.Comp.Multi.Variables
+ (
+ HasVars(..),
+ GSubst,
+ CxtSubst,
+ Subst,
+ varsToHoles,
+ containsVar,
+ variables,
+ variableList,
+ variables',
+ substVars,
+ appSubst,
+ compSubst
+ ) where
import Data.Comp.Multi.Term
import Data.Comp.Multi.Sum
import Data.Comp.Multi.Algebra
import Data.Comp.Multi.Functor
import Data.Comp.Multi.Foldable
-
import Data.Set (Set)
import qualified Data.Set as Set
-
import Data.Maybe
--- type HCxtSubst h a f v = [A (v :*: (HCxt h f a))]
+-- type CxtSubst h a f v = [A (v :*: (Cxt h f a))]
--- type Subst f v = HCxtSubst HNoHole HNothing f v
+-- type Subst f v = CxtSubst NoHole Nothing f v
type GSubst v a = NatM Maybe (K v) a
-type HCxtSubst h a f v = GSubst v (HCxt h f a)
-
-type Subst f v = HCxtSubst HNoHole HNothing f v
+type CxtSubst h a f v = GSubst v (Cxt h f a)
-{-| This multiparameter class defines functors with variables. An
-instance @HasVar f v@ denotes that values over @f@ might contain
-variables of type @v@. -}
+type Subst f v = CxtSubst NoHole Nothing f v
+{-| This multiparameter class defines functors with variables. An instance
+ @HasVar f v@ denotes that values over @f@ might contain and bind variables of
+ type @v@. -}
class HasVars (f :: (* -> *) -> * -> *) v where
isVar :: f a :=> Maybe v
isVar _ = Nothing
+ bindsVars :: f a :=> [v]
+ bindsVars _ = []
-instance (HasVars f v, HasVars g v) => HasVars (f :++: g) v where
- isVar (HInl v) = isVar v
- isVar (HInr v) = isVar v
+instance (HasVars f v, HasVars g v) => HasVars (f :+: g) v where
+ isVar (Inl v) = isVar v
+ isVar (Inr v) = isVar v
+ bindsVars (Inl v) = bindsVars v
+ bindsVars (Inr v) = bindsVars v
-instance HasVars f v => HasVars (HCxt h f) v where
- isVar (HTerm t) = isVar t
+instance HasVars f v => HasVars (Cxt h f) v where
+ isVar (Term t) = isVar t
isVar _ = Nothing
+ bindsVars (Term t) = bindsVars t
+ bindsVars _ = []
-varsToHHoles :: forall f v. (HFunctor f, HasVars f v) => HTerm f :-> HContext f (K v)
-varsToHHoles = hcata alg
- where alg :: HAlg f (HContext f (K v))
- alg t = case isVar t of
- Just v -> HHole $ K v
- Nothing -> HTerm t
+-- Auxiliary data type, used only to define varsToHoles
+data C a b i = C{ unC :: a -> b i }
-containsVarAlg :: (Eq v, HasVars f v, HFoldable f) => v -> HAlg f (K Bool)
-containsVarAlg v t = K $ local || kfoldl (||) False t
+varsToHoles :: forall f v. (HFunctor f, HasVars f v, Eq v) =>
+ Term f :-> Context f (K v)
+varsToHoles t = unC (cata alg t) []
+ where alg :: (HFunctor f, HasVars f v, Eq v) =>
+ Alg f (C [v] (Context f (K v)))
+ alg t = C $ \vars ->
+ let vars' = vars ++ bindsVars t in
+ case isVar t of
+ Just v ->
+ -- Check for capture-avoidance
+ if v `elem` vars' then
+ Term $ hfmap (\x -> unC x vars') t
+ else
+ Hole $ K v
+ Nothing ->
+ Term $ hfmap (\x -> unC x vars') t
+
+containsVarAlg :: (Eq v, HasVars f v, HFoldable f) => v -> Alg f (K Bool)
+containsVarAlg v t = K $ v `notElem` bindsVars t &&
+ (local || kfoldl (||) False t)
where local = case isVar t of
Just v' -> v == v'
Nothing -> False
-{-| This function checks whether a variable is contained in a
-context. -}
-
+{-| This function checks whether a variable is contained in a context. -}
containsVar :: (Eq v, HasVars f v, HFoldable f, HFunctor f)
- => v -> HCxt h f a :=> Bool
-containsVar v = unK . hfree (containsVarAlg v) (const $ K False)
-
+ => v -> Cxt h f a :=> Bool
+containsVar v = unK . free (containsVarAlg v) (const $ K False)
-variableListAlg :: (HasVars f v, HFoldable f)
- => HAlg f (K [v])
-variableListAlg t = K $ kfoldl (++) local t
+variableListAlg :: (HasVars f v, HFoldable f, Eq v) => Alg f (K [v])
+variableListAlg t = K $ filter (`notElem` bindsVars t) $ kfoldl (++) local t
where local = case isVar t of
Just v -> [v]
Nothing -> []
-{-| This function computes the list of variables occurring in a
-context. -}
-
-variableList :: (HasVars f v, HFoldable f, HFunctor f)
- => HCxt h f a :=> [v]
-variableList = unK . hfree variableListAlg (const $ K [])
-
-
+{-| This function computes the list of variables occurring in a context. -}
+variableList :: (HasVars f v, HFoldable f, HFunctor f, Eq v)
+ => Cxt h f a :=> [v]
+variableList = unK . free variableListAlg (const $ K [])
-variablesAlg :: (Ord v, HasVars f v, HFoldable f)
- => HAlg f (K (Set v))
-variablesAlg t = K $ kfoldl Set.union local t
+variablesAlg :: (Ord v, HasVars f v, HFoldable f) => Alg f (K (Set v))
+variablesAlg t = K $ Set.filter (`notElem` bindsVars t) $
+ kfoldl Set.union local t
where local = case isVar t of
Just v -> Set.singleton v
Nothing -> Set.empty
-{-| This function computes the set of variables occurring in a
-context. -}
-
+{-| This function computes the set of variables occurring in a context. -}
variables :: (Ord v, HasVars f v, HFoldable f, HFunctor f)
- => HCxt h f a :=> Set v
-variables = unK . hfree variablesAlg (const $ K Set.empty)
-
-{-| This function computes the set of variables occurring in a
-context. -}
+ => Cxt h f a :=> Set v
+variables = unK . free variablesAlg (const $ K Set.empty)
+{-| This function computes the set of variables occurring in a context. -}
variables' :: (Ord v, HasVars f v, HFoldable f, HFunctor f)
- => HConst f :=> Set v
+ => Const f :=> Set v
variables' c = case isVar c of
Nothing -> Set.empty
Just v -> Set.singleton v
-
-
-substAlg :: (HasVars f v) => HCxtSubst h a f v -> HAlg f (HCxt h f a)
-substAlg f t = fromMaybe (HTerm t) (isVar t >>= f . K)
-
{-| This function substitutes variables in a context according to a
partial mapping from variables to contexts.-}
-
class SubstVars v t a where
substVars :: GSubst v t -> a :-> a
-
appSubst :: SubstVars v t a => GSubst v t -> a :-> a
appSubst = substVars
-instance (Ord v, HasVars f v, HFunctor f) => SubstVars v (HCxt h f a) (HCxt h f a) where
- substVars f (HTerm v) = substAlg f $ hfmap (substVars f) v
- substVars _ (HHole a) = HHole a
--- have to use explicit GADT pattern matching!!
--- subst f = hfree (substAlg f) HHole
+instance (Ord v, HasVars f v, HFunctor f) => SubstVars v (Cxt h f a) (Cxt h f a) where
+ -- have to use explicit GADT pattern matching!!
+ -- subst f = free (substAlg f) Hole
+ substVars _ (Hole a) = Hole a
+ substVars f (Term v) = substAlg f v
+ where substAlg :: (HasVars f v) => CxtSubst h a f v
+ -> Alg f (Cxt h f a)
+ substAlg f t = fromMaybe (Term t) (isVar t >>= f . K)
+ -- The code below does not work with GHC 7
+ -- substVars _ (Hole a) = Hole a
+ -- substVars f (Term v) = let f' = res (bindsVars v) f in
+ -- substAlg f' $ hfmap (substVars f') v
+ -- where substAlg :: (HasVars f v) => CxtSubst h a f v
+ -- -> Alg f (Cxt h f a)
+ -- substAlg f t = fromMaybe (Term t) (isVar t >>= f . K)
+ -- res :: Eq v => [v] -> GSubst v t -> GSubst v t
+ -- res vars f x = if unK x `elem` vars then Nothing else f x
instance (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where
substVars f = hfmap (substVars f)
-
-
{-| This function composes two substitutions @s1@ and @s2@. That is,
applying the resulting substitution is equivalent to first applying
@s2@ and then @s1@. -}
compSubst :: (Ord v, HasVars f v, HFunctor f)
- => HCxtSubst h a f v -> HCxtSubst h a f v -> HCxtSubst h a f v
+ => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst s1 s2 v = case s2 v of
Nothing -> s1 v
Just t -> Just $ appSubst s1 t
diff --git a/src/Data/Comp/Ops.hs b/src/Data/Comp/Ops.hs
--- a/src/Data/Comp/Ops.hs
+++ b/src/Data/Comp/Ops.hs
@@ -23,8 +23,6 @@
import Control.Applicative
import Control.Monad hiding (sequence, mapM)
-import Data.Comp.ExpFunctor
-
import Prelude hiding (foldl, mapM, sequence, foldl1, foldr1, foldr)
@@ -65,10 +63,6 @@
sequence (Inl e) = Inl `liftM` sequence e
sequence (Inr e) = Inr `liftM` sequence e
-instance (ExpFunctor f, ExpFunctor g) => ExpFunctor (f :+: g) where
- xmap f g (Inl e) = Inl (xmap f g e)
- xmap f g (Inr e) = Inr (xmap f g e)
-
-- | Signature containment relation for automatic injections. The left-hand must
-- be an atomic signature, where as the right-hand side must have a list-like
-- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,
@@ -131,9 +125,6 @@
sequenceA (v :&: c) = liftA (:&: c)(sequenceA v)
mapM f (v :&: c) = liftM (:&: c) (mapM f v)
sequence (v :&: c) = liftM (:&: c) (sequence v)
-
-instance (ExpFunctor f) => ExpFunctor (f :&: a) where
- xmap f g (v :&: c) = xmap f g v :&: c
{-| This class defines how to distribute a product over a sum of
signatures. -}
diff --git a/src/Data/Comp/Sum.hs b/src/Data/Comp/Sum.hs
--- a/src/Data/Comp/Sum.hs
+++ b/src/Data/Comp/Sum.hs
@@ -42,9 +42,6 @@
deepInject,
deepInject2,
deepInject3,
- deepInjectE,
- deepInjectE2,
- deepInjectE3,
-- * Injections and Projections for Constants
injectConst,
@@ -60,7 +57,6 @@
import Data.Comp.Term
import Data.Comp.Algebra
import Data.Comp.Ops
-import Data.Comp.ExpFunctor
import Control.Monad hiding (sequence)
import Prelude hiding (sequence)
@@ -183,23 +179,6 @@
f1 :<: g, f2 :<: g, f3 :<: g)
=> Cxt h (f1 :+: f2 :+: f3) a -> Cxt h g a
deepInject3 = appSigFun inj3
-
-{-| A variant of 'deepInject' for exponential signatures. -}
-deepInjectE :: (ExpFunctor g, g :<: f) => Term g -> Term f
-deepInjectE = cataE inject
-
-{-| A variant of 'deepInject2' for exponential signatures. -}
-deepInjectE2 :: (ExpFunctor g1, ExpFunctor g2, g1 :<: f, g2 :<: f) =>
- Term (g1 :+: g2)
- -> Term f
-deepInjectE2 = cataE inject2
-
-{-| A variant of 'deepInject3' for exponential signatures. -}
-deepInjectE3 :: (ExpFunctor g1, ExpFunctor g2, ExpFunctor g3,
- g1 :<: f, g2 :<: f, g3 :<: f) =>
- Term (g1 :+: g2 :+: g3)
- -> Term f
-deepInjectE3 = cataE inject3
injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a
injectConst = inject . fmap (const undefined)
diff --git a/src/Data/Comp/Term.hs b/src/Data/Comp/Term.hs
--- a/src/Data/Comp/Term.hs
+++ b/src/Data/Comp/Term.hs
@@ -33,7 +33,6 @@
import Data.Traversable
import Data.Foldable
-
import Unsafe.Coerce
import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
@@ -72,15 +71,16 @@
type Context = Cxt Hole
{-| Convert a functorial value into a context. -}
-simpCxt :: (Functor f) => f a -> Context f a
+simpCxt :: Functor f => f a -> Context f a
{-# INLINE simpCxt #-}
simpCxt = Term . fmap Hole
{-| Cast a term over a signature to a context over the same signature. -}
-toCxt :: Term f -> Cxt h f a
+toCxt :: Functor f => Term f -> Cxt h f a
{-# INLINE toCxt #-}
toCxt = unsafeCoerce
+-- equivalent to @Term . (fmap toCxt) . unTerm@
{-| Phantom type used to define 'Term'. -}
diff --git a/src/Data/Comp/Variables.hs b/src/Data/Comp/Variables.hs
--- a/src/Data/Comp/Variables.hs
+++ b/src/Data/Comp/Variables.hs
@@ -5,150 +5,155 @@
-- Module : Data.Comp.Variables
-- Copyright : (c) 2010-2011 Patrick Bahr
-- License : BSD3
--- Maintainer : Patrick Bahr
+-- Maintainer : Patrick Bahr and Tom Hvitved
-- Stability : experimental
-- Portability : non-portable (GHC Extensions)
--
--- This module defines an abstraction notion of a variable in compositional
--- data type.
+-- This module defines an abstract notion of (bound) variables in compositional
+-- data types, and capture-avoiding substitution.
--
--------------------------------------------------------------------------------
-module Data.Comp.Variables (
- HasVars(..),
- Subst,
- CxtSubst,
- varsToHoles,
- containsVar,
- variables,
- variableList,
- variables',
- substVars,
- appSubst,
- compSubst) where
+module Data.Comp.Variables
+ (
+ HasVars(..),
+ Subst,
+ CxtSubst,
+ varsToHoles,
+ containsVar,
+ variables,
+ variableList,
+ variables',
+ substVars,
+ appSubst,
+ compSubst
+ ) where
import Data.Comp.Term
import Data.Comp.Sum
import Data.Comp.Algebra
-import Data.Foldable
-
+import Data.Foldable hiding (elem, notElem)
import Data.Maybe
-
import Data.Set (Set)
import qualified Data.Set as Set
-
import Data.Map (Map)
import qualified Data.Map as Map
-
import Prelude hiding (or, foldl)
type CxtSubst h a f v = Map v (Cxt h f a)
type Subst f v = CxtSubst NoHole Nothing f v
-{-| This multiparameter class defines functors with variables. An
-instance @HasVar f v@ denotes that values over @f@ might contain
-variables of type @v@. -}
-
+{-| This multiparameter class defines functors with variables. An instance
+ @HasVar f v@ denotes that values over @f@ might contain and bind variables of
+ type @v@. -}
class HasVars f v where
+ -- |Indicates whether the @f@ constructor is a variable.
isVar :: f a -> Maybe v
isVar _ = Nothing
+ -- |Indicates the set of variables bound by the @f@ constructor.
+ bindsVars :: f a -> [v]
+ bindsVars _ = []
instance (HasVars f v, HasVars g v) => HasVars (f :+: g) v where
isVar (Inl v) = isVar v
isVar (Inr v) = isVar v
+ bindsVars (Inl v) = bindsVars v
+ bindsVars (Inr v) = bindsVars v
instance HasVars f v => HasVars (Cxt h f) v where
isVar (Term t) = isVar t
isVar _ = Nothing
+ bindsVars (Term t) = bindsVars t
+ bindsVars _ = []
-varsToHoles :: (Functor f, HasVars f v) => Term f -> Context f v
-varsToHoles = cata alg
- where alg t = case isVar t of
- Just v -> Hole v
- Nothing -> Term t
+-- |Convert variables to holes, except those that are bound.
+varsToHoles :: (Functor f, HasVars f v, Eq v) => Term f -> Context f v
+varsToHoles t = cata alg t []
+ where alg :: (Functor f, HasVars f v, Eq v) => Alg f ([v] -> Context f v)
+ alg t vars =
+ let vars' = vars ++ bindsVars t in
+ case isVar t of
+ Just v ->
+ -- Check for capture-avoidance
+ if v `elem` vars' then
+ Term $ fmap (\x -> x vars') t
+ else
+ Hole v
+ Nothing ->
+ Term $ fmap (\x -> x vars') t
+-- |Algebra for checking whether a variable is contained in a term, except those
+-- that are bound.
containsVarAlg :: (Eq v, HasVars f v, Foldable f) => v -> Alg f Bool
-containsVarAlg v t = local || or t
+containsVarAlg v t = v `notElem` bindsVars t && (local || or t)
where local = case isVar t of
Just v' -> v == v'
Nothing -> False
-{-| This function checks whether a variable is contained in a
-context. -}
-
+{-| This function checks whether a variable is contained in a context. -}
containsVar :: (Eq v, HasVars f v, Foldable f, Functor f)
=> v -> Cxt h f a -> Bool
containsVar v = free (containsVarAlg v) (const False)
-variablesAlg :: (Ord v, HasVars f v, Foldable f)
- => Alg f (Set v)
-variablesAlg t = foldl Set.union local t
+-- |Algebra for generating a set of variables contained in a term, except those
+-- that are bound.
+variablesAlg :: (Ord v, HasVars f v, Foldable f) => Alg f (Set v)
+variablesAlg t = Set.filter (`notElem` bindsVars t) $ foldl Set.union local t
where local = case isVar t of
Just v -> Set.singleton v
Nothing -> Set.empty
-variableListAlg :: (Ord v, HasVars f v, Foldable f)
- => Alg f [v]
-variableListAlg t = foldl (++) local t
+-- |Algebra for generating a list of variables contained in a term, except those
+-- that are bound.
+variableListAlg :: (Ord v, HasVars f v, Foldable f) => Alg f [v]
+variableListAlg t = filter (`notElem` bindsVars t) $ foldl (++) local t
where local = case isVar t of
Just v -> [v]
Nothing -> []
-{-| This function computes the list of variables occurring in a
-context. -}
-
-variableList :: (Ord v, HasVars f v, Foldable f, Functor f)
- => Cxt h f a -> [v]
+{-| This function computes the list of variables occurring in a context. -}
+variableList :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> [v]
variableList = free variableListAlg (const [])
-{-| This function computes the set of variables occurring in a
-context. -}
-
-variables :: (Ord v, HasVars f v, Foldable f, Functor f)
- => Cxt h f a -> Set v
+{-| This function computes the set of variables occurring in a context. -}
+variables :: (Ord v, HasVars f v, Foldable f, Functor f) => Cxt h f a -> Set v
variables = free variablesAlg (const Set.empty)
-{-| This function computes the set of variables occurring in a
-context. -}
-
-variables' :: (Ord v, HasVars f v, Foldable f, Functor f)
- => Const f -> Set v
-variables' c = case isVar c of
- Nothing -> Set.empty
- Just v -> Set.singleton v
-
-
-substAlg :: (HasVars f v) => (v -> Maybe (Cxt h f a)) -> Alg f (Cxt h f a)
-substAlg f t = fromMaybe (Term t) (isVar t >>= f)
-
-{-| This function substitutes variables in a context according to a
-partial mapping from variables to contexts.-}
-
-
+{-| This function computes the set of variables occurring in a constant. -}
+variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v
+variables' c = case isVar c of
+ Nothing -> Set.empty
+ Just v -> Set.singleton v
+{-| This multiparameter class defines substitution of values of type @t@ for
+ variables of type @v@ in values of type @a@. -}
class SubstVars v t a where
substVars :: (v -> Maybe t) -> a -> a
-
+-- |Apply the given substitution.
appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a
appSubst subst = substVars f
where f v = Map.lookup v subst
-instance (Ord v, HasVars f v, Functor f) => SubstVars v (Cxt h f a) (Cxt h f a) where
- substVars f (Term v) = substAlg f $ fmap (substVars f) v
+instance (Ord v, HasVars f v, Functor f)
+ => SubstVars v (Cxt h f a) (Cxt h f a) where
+ -- have to use explicit GADT pattern matching!!
+ -- subst f = free (substAlg f) Hole
substVars _ (Hole a) = Hole a
--- have to use explicit GADT pattern matching!!
--- subst f = free (substAlg f) Hole
+ substVars f (Term v) = let f' = res (bindsVars v) f in
+ substAlg f' $ fmap (substVars f') v
+ where substAlg :: (HasVars f v) => (v -> Maybe (Cxt h f a))
+ -> Alg f (Cxt h f a)
+ substAlg f t = fromMaybe (Term t) (isVar t >>= f)
+ res :: Eq v => [v] -> (v -> Maybe t) -> (v -> Maybe t)
+ res vars f x = if x `elem` vars then Nothing else f x
instance (SubstVars v t a, Functor f) => SubstVars v t (f a) where
substVars f = fmap (substVars f)
-
-
{-| This function composes two substitutions @s1@ and @s2@. That is,
applying the resulting substitution is equivalent to first applying
@s2@ and then @s1@. -}
-
compSubst :: (Ord v, HasVars f v, Functor f)
=> CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst s1 s2 = fmap (appSubst s1) s2 `Map.union` s1