compdata 0.4.1 → 0.5

raw patch · 139 files changed

+3138/−3552 lines, 139 filessetup-changedPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Setup.hs +1/−35
• benchmark/Benchmark.hs +18/−1
• benchmark/Functions/Comp/Eval.hs +85/−0
• compdata.cabal +36/−42
• examples/Examples/Common.hs +32/−0
• examples/Examples/Desugar.hs +78/−0
• examples/Examples/DesugarEval.hs +0/−77
• examples/Examples/DesugarPos.hs +0/−72
• examples/Examples/Eval.hs +8/−17
• examples/Examples/EvalM.hs +6/−16
• examples/Examples/Multi/Common.hs +39/−0
• examples/Examples/Multi/Desugar.hs +75/−0
• examples/Examples/Multi/DesugarEval.hs +0/−88
• examples/Examples/Multi/DesugarPos.hs +0/−75
• examples/Examples/Multi/Eval.hs +7/−22
• examples/Examples/Multi/EvalI.hs +2/−18
• examples/Examples/Multi/EvalM.hs +7/−24
• examples/Examples/MultiParam/DesugarEval.hs +0/−107
• examples/Examples/MultiParam/DesugarPos.hs +0/−75
• examples/Examples/MultiParam/Eval.hs +0/−96
• examples/Examples/MultiParam/EvalAlgM.hs +0/−86
• examples/Examples/MultiParam/EvalI.hs +0/−75
• examples/Examples/MultiParam/EvalM.hs +0/−102
• examples/Examples/MultiParam/FOL.hs +179/−195
• examples/Examples/MultiParam/Lambda.hs +106/−0
• examples/Examples/Param/DesugarEval.hs +0/−109
• examples/Examples/Param/DesugarPos.hs +0/−69
• examples/Examples/Param/Eval.hs +0/−84
• examples/Examples/Param/EvalAlgM.hs +0/−78
• examples/Examples/Param/EvalM.hs +0/−99
• examples/Examples/Param/Graph.hs +77/−0
• examples/Examples/Param/Lambda.hs +131/−0
• examples/Examples/Param/Names.hs +104/−0
• examples/Examples/Param/Parsing.hs +0/−76
• src/Data/Comp.hs +10/−15
• src/Data/Comp/Algebra.hs +2/−2
• src/Data/Comp/Annotation.hs +30/−0
• src/Data/Comp/Automata.hs +164/−9
• src/Data/Comp/Automata/Product/Derive.hs +3/−3
• src/Data/Comp/DeepSeq.hs +0/−2
• src/Data/Comp/Derive.hs +3/−0
• src/Data/Comp/Derive/Arbitrary.hs +1/−1
• src/Data/Comp/Derive/DeepSeq.hs +1/−1
• src/Data/Comp/Derive/Equality.hs +1/−1
• src/Data/Comp/Derive/Foldable.hs +1/−1
• src/Data/Comp/Derive/HaskellStrict.hs +102/−0
• src/Data/Comp/Derive/Injections.hs +4/−4
• src/Data/Comp/Derive/LiftSum.hs +5/−18
• src/Data/Comp/Derive/Ordering.hs +1/−1
• src/Data/Comp/Derive/Show.hs +1/−1
• src/Data/Comp/Derive/Traversable.hs +1/−1
• src/Data/Comp/Derive/Utils.hs +76/−0
• src/Data/Comp/Equality.hs +12/−22
• src/Data/Comp/Multi.hs +2/−2
• src/Data/Comp/Multi/Algebra.hs +2/−2
• src/Data/Comp/Multi/Annotation.hs +1/−1
• src/Data/Comp/Multi/Derive.hs +10/−7
• src/Data/Comp/Multi/Derive/Equality.hs +10/−30
• src/Data/Comp/Multi/Derive/Foldable.hs +0/−119
• src/Data/Comp/Multi/Derive/Functor.hs +0/−63
• src/Data/Comp/Multi/Derive/HFoldable.hs +119/−0
• src/Data/Comp/Multi/Derive/HFunctor.hs +63/−0
• src/Data/Comp/Multi/Derive/HTraversable.hs +83/−0
• src/Data/Comp/Multi/Derive/Injections.hs +5/−5
• src/Data/Comp/Multi/Derive/LiftSum.hs +1/−18
• src/Data/Comp/Multi/Derive/Ordering.hs +74/−0
• src/Data/Comp/Multi/Derive/Projections.hs +1/−1
• src/Data/Comp/Multi/Derive/Show.hs +16/−16
• src/Data/Comp/Multi/Derive/SmartConstructors.hs +3/−3
• src/Data/Comp/Multi/Derive/Traversable.hs +0/−83
• src/Data/Comp/Multi/Equality.hs +31/−22
• src/Data/Comp/Multi/Foldable.hs +0/−67
• src/Data/Comp/Multi/Functor.hs +0/−85
• src/Data/Comp/Multi/Generic.hs +3/−3
• src/Data/Comp/Multi/HFoldable.hs +67/−0
• src/Data/Comp/Multi/HFunctor.hs +85/−0
• src/Data/Comp/Multi/HTraversable.hs +36/−0
• src/Data/Comp/Multi/Ops.hs +3/−3
• src/Data/Comp/Multi/Ordering.hs +62/−0
• src/Data/Comp/Multi/Show.hs +10/−12
• src/Data/Comp/Multi/Sum.hs +2/−2
• src/Data/Comp/Multi/Term.hs +4/−12
• src/Data/Comp/Multi/Traversable.hs +0/−36
• src/Data/Comp/Multi/Variables.hs +3/−3
• src/Data/Comp/MultiParam/Algebra.hs +79/−69
• src/Data/Comp/MultiParam/Any.hs +0/−23
• src/Data/Comp/MultiParam/Derive.hs +0/−6
• src/Data/Comp/MultiParam/Derive/Equality.hs +2/−4
• src/Data/Comp/MultiParam/Derive/Injections.hs +5/−5
• src/Data/Comp/MultiParam/Derive/LiftSum.hs +1/−18
• src/Data/Comp/MultiParam/Derive/Ordering.hs +5/−5
• src/Data/Comp/MultiParam/Derive/Projections.hs +9/−8
• src/Data/Comp/MultiParam/Derive/Show.hs +14/−12
• src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs +3/−3
• src/Data/Comp/MultiParam/Derive/SmartConstructors.hs +6/−5
• src/Data/Comp/MultiParam/Desugar.hs +3/−3
• src/Data/Comp/MultiParam/Equality.hs +7/−7
• src/Data/Comp/MultiParam/FreshM.hs +26/−36
• src/Data/Comp/MultiParam/HDifunctor.hs +1/−36
• src/Data/Comp/MultiParam/HDitraversable.hs +3/−36
• src/Data/Comp/MultiParam/Ops.hs +2/−3
• src/Data/Comp/MultiParam/Ordering.hs +11/−11
• src/Data/Comp/MultiParam/Show.hs +7/−16
• src/Data/Comp/MultiParam/Sum.hs +7/−119
• src/Data/Comp/MultiParam/Term.hs +52/−49
• src/Data/Comp/Ordering.hs +4/−5
• src/Data/Comp/Param/Algebra.hs +223/−189
• src/Data/Comp/Param/Any.hs +0/−23
• src/Data/Comp/Param/Derive/Ditraversable.hs +3/−10
• src/Data/Comp/Param/Derive/Equality.hs +2/−3
• src/Data/Comp/Param/Derive/Injections.hs +5/−5
• src/Data/Comp/Param/Derive/LiftSum.hs +1/−18
• src/Data/Comp/Param/Derive/Ordering.hs +4/−9
• src/Data/Comp/Param/Derive/Projections.hs +7/−7
• src/Data/Comp/Param/Derive/Show.hs +13/−12
• src/Data/Comp/Param/Derive/SmartAConstructors.hs +3/−3
• src/Data/Comp/Param/Derive/SmartConstructors.hs +2/−2
• src/Data/Comp/Param/Desugar.hs +3/−3
• src/Data/Comp/Param/Difunctor.hs +2/−2
• src/Data/Comp/Param/Ditraversable.hs +4/−103
• src/Data/Comp/Param/Equality.hs +11/−5
• src/Data/Comp/Param/FreshM.hs +22/−24
• src/Data/Comp/Param/Ops.hs +2/−3
• src/Data/Comp/Param/Ordering.hs +23/−10
• src/Data/Comp/Param/Show.hs +7/−15
• src/Data/Comp/Param/Sum.hs +16/−30
• src/Data/Comp/Param/Term.hs +40/−60
• src/Data/Comp/Param/Thunk.hs +127/−0
• src/Data/Comp/Show.hs +3/−1
• src/Data/Comp/Term.hs +1/−13
• src/Data/Comp/TermRewriting.hs +12/−0
• src/Data/Comp/Thunk.hs +179/−0
• src/Data/Comp/Unification.hs +13/−0
• src/Data/Comp/Variables.hs +6/−2
• src/Data/Comp/Zippable.hs +1/−1
• testsuite/tests/Data/Comp/Examples/Comp.hs +17/−23
• testsuite/tests/Data/Comp/Examples/Multi.hs +21/−31
• testsuite/tests/Data/Comp/Examples/MultiParam.hs +7/−25
• testsuite/tests/Data/Comp/Examples/Param.hs +6/−26

@@ -1,36 +1,2 @@ import Distribution.Simple-import Distribution.Simple.LocalBuildInfo-import Distribution.PackageDescription-import System.Cmd-import System.FilePath-import System.Directory-import Control.Exception-import System.IO.Error (isDoesNotExistError)---main = defaultMainWithHooks hooks-  where hooks = simpleUserHooks { runTests = runTests'}---hpcReportDir = "hpcreport"--runTests' :: Args -> Bool -> PackageDescription -> LocalBuildInfo -> IO ()-runTests' _ _ _ lbi = do-  res <- try (removeFile tixFile)-  case res of-    Left err-        | not (isDoesNotExistError err) -> putStrLn "tix file could not be removed"-    _ -> return ()-  putStrLn "running tests ..."-  system testprog-  putStrLn "computing code coverage ..."-  hpcReport-  putStrLn "generating code coverage reports ..."-  hpcMarkup-  return ()-    where testprog = (buildDir lbi) </> "test" </> "test"-          tixFile = "test.tix"-          hpcReport = system $ "hpc report test"++exclArgs-          hpcMarkup = system $ "hpc markup test --destdir="++hpcReportDir++exclArgs-          excludedModules = []-          exclArgs = concatMap (" --exclude="++) excludedModules+main = defaultMain

@@ -42,7 +42,24 @@  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 paperBenchmarks+    where getBench (sExpr, aExpr,n) = bgroup n evalBenchmarks+          -- these are the benchmarks for evaluation+          evalBenchmarks = [+                 bench "evalDesug" (nf A.desugEval2 aExpr),+                 bench "evalDesug (fusion)" (nf A.desugEval2' aExpr),+                 bench "evalDesug (comparison)" (nf S.desugEval2 sExpr),+                 bench "evalDesugM" (nf A.desugEval aExpr),+                 bench "evalDesugT" (nf A.desugEvalT aExpr),+                 bench "evalDesugM (fusion)" (nf A.desugEval' aExpr),+                 bench "evalDesugT (fusion)" (nf A.desugEvalT' aExpr),+                 bench "evalDesugM (comparison)" (nf S.desugEval sExpr),+                 bench "eval" (nf A.evalSugar2 aExpr),+                 bench "evalDirect" (nf A.evalDirectE2 aExpr),+                 bench "eval[Direct] (comparison)" (nf S.evalSugar2 sExpr),+                 bench "evalM" (nf A.evalSugar aExpr),+                 bench "evalT" (nf A.evalSugarT aExpr),+                 bench "evalDirectM" (nf A.evalDirectE aExpr),+                 bench "eval[Direct]M (comparison)" (nf S.evalSugar sExpr)]           -- these are the benchmarks from the WGP '11 paper           paperBenchmarks = [                  bench "desugHom" (nf A.desugExpr aExpr),

@@ -13,10 +13,82 @@ import DataTypes.Comp import Functions.Comp.Desugar import Data.Comp+import Data.Comp.Ops+import Data.Comp.Thunk import Data.Comp.Derive import Control.Monad import Data.Traversable +-- evaluation with thunks++class (Monad m, Traversable v) => EvalT e v m where+    evalTAlg :: AlgT m e v++evalT :: (EvalT e v m, Functor e) => Term e -> m (Term v)+evalT = nf . cata evalTAlg++$(derive [liftSum] [''EvalT])++instance (Monad m, Traversable v, Value :<: v) => EvalT Value v m where+    evalTAlg = inject++instance (Value :<: v, Traversable v, EqF v, Monad m) => EvalT Op v m where+    evalTAlg (Plus x y) = thunk $ do+                           VInt i <- whnfPr x+                           VInt j <- whnfPr y+                           return $ iVInt (i+j)+    evalTAlg (Mult x y) = thunk $ do+                           VInt i <- whnfPr x+                           VInt j <- whnfPr y+                           return $ iVInt (i*j)+    evalTAlg (If x y z) = thunk $ do +                            VBool b <- whnfPr x+                            return $ if b then y else z+    evalTAlg (Eq x y) = thunk $ liftM iVBool $ eqT x y+    evalTAlg (Lt x y) = thunk $ do+                          VInt i <- whnfPr x+                          VInt j <- whnfPr y+                          return $ iVBool (i < j)+    evalTAlg (And x y) = thunk $ do+                           VBool b1 <- whnfPr x+                           if b1 then do+                                   VBool b2 <- whnfPr y+                                   return $ iVBool b2+                                 else return $ iVBool False+    evalTAlg (Not x) = thunk $ do+                           VBool b <- whnfPr x+                           return $ iVBool (not b)+    evalTAlg (Proj p x) = thunk $ do+                            VPair a b <- whnfPr x+                            return $ select a b+         where select x y = case p of+                              ProjLeft -> x+                              ProjRight -> y++instance (Value :<: v, Traversable v, Monad m) => EvalT Sugar v m where+    evalTAlg (Neg x) = thunk $ do+                         VInt i <- whnfPr x+                         return $ iVInt (-i)+    evalTAlg (Minus x y) = thunk $ do+                           VInt i <- whnfPr x+                           VInt j <- whnfPr y+                           return $ iVInt (i-j)+    evalTAlg (Gt x y) = thunk $ do+                          VInt i <- whnfPr x+                          VInt j <- whnfPr y+                          return $ iVBool (i > j)+    evalTAlg (Or x y) = thunk $ do+                           VBool b1 <- whnfPr x+                           if b1 then return $ iVBool True+                                 else do+                                   VBool b2 <- whnfPr y+                                   return $ iVBool b2+    evalTAlg (Impl x y) = thunk $ do+                           VBool b1 <- whnfPr x+                           if b1 then do+                                   VBool b2 <- whnfPr y+                                   return $ iVBool b2+                                 else return $ iVBool True -- evaluation  class Monad m => Eval e v m where@@ -240,16 +312,29 @@ desugEval :: SugarExpr -> Err ValueExpr desugEval = eval . (desug :: SugarExpr -> Expr) +desugEvalT :: SugarExpr -> Err ValueExpr+desugEvalT = evalT . (desug :: SugarExpr -> Expr) + evalSugar :: SugarExpr -> Err ValueExpr evalSugar = eval +evalSugarT :: SugarExpr -> Err ValueExpr+evalSugarT = evalT+ desugEvalAlg  :: AlgM Err SugarSig ValueExpr desugEvalAlg = evalAlg  `compAlgM'` (desugAlg :: Hom SugarSig ExprSig)   desugEval' :: SugarExpr -> Err ValueExpr desugEval' = cataM desugEvalAlg++desugEvalAlgT  :: AlgT Err SugarSig Value+desugEvalAlgT = evalTAlg  `compAlg` (desugAlg :: Hom SugarSig ExprSig)++desugEvalT' :: SugarExpr -> Err ValueExpr+desugEvalT' = nf . cata desugEvalAlgT+  desugEval2 :: SugarExpr -> ValueExpr desugEval2 = eval2 . (desug :: SugarExpr -> Expr)

@@ -1,18 +1,21 @@ Name:			compdata-Version:		0.4.1+Version:		0.5 Synopsis:            	Compositional Data Types Description:    Based on Wouter Swierstra's Functional Pearl /Data types à la carte/-  (Journal of Functional Programming, 18(4):423-436, 2008),+  (Journal of Functional Programming, 18(4):423-436, 2008,+  <http://dx.doi.org/10.1017/S0956796808006758>),   this package provides a framework for defining recursive   data types in a compositional manner. The fundamental idea of-  compositional data types is to separate the signature of a data type+  /compositional data types/ (Workshop on Generic Programming, 83-94, 2011,+  <http://dx.doi.org/10.1145/2036918.2036930>) is to separate the+  signature of a data type   from the fixed point construction that produces its recursive   structure. By allowing to compose and decompose signatures,-  /compositional data types/ enable to combine data types in a flexible+  compositional data types enable to combine data types in a flexible   way. The key point of Wouter Swierstra's original work is to define-  functions on /compositional data types/ in a compositional manner as+  functions on compositional data types in a compositional manner as   well by leveraging Haskell's type class machinery.   .   Building on that foundation, this library provides additional@@ -85,8 +88,8 @@ License-file:		LICENSE Author:			Patrick Bahr, Tom Hvitved Maintainer:		paba@diku.dk-Build-Type:		Custom-Cabal-Version:          >=1.8.0.6+Build-Type:		Simple+Cabal-Version:          >=1.9.2  extra-source-files:   -- test files@@ -122,34 +125,22 @@   benchmark/Functions/Standard/Inference.hs   benchmark/Functions/Standard.hs   -- example files+  examples/Examples/Common.hs   examples/Examples/Eval.hs   examples/Examples/EvalM.hs-  examples/Examples/DesugarEval.hs-  examples/Examples/DesugarPos.hs+  examples/Examples/Desugar.hs   examples/Examples/Automata.hs,+  examples/Examples/Multi/Common.hs   examples/Examples/Multi/Eval.hs   examples/Examples/Multi/EvalI.hs   examples/Examples/Multi/EvalM.hs-  examples/Examples/Multi/DesugarEval.hs-  examples/Examples/Multi/DesugarPos.hs-  examples/Examples/Param/Eval.hs-  examples/Examples/Param/EvalM.hs-  examples/Examples/Param/EvalAlgM.hs-  examples/Examples/Param/DesugarEval.hs-  examples/Examples/Param/DesugarPos.hs-  examples/Examples/Param/Parsing.hs-  examples/Examples/MultiParam/Eval.hs-  examples/Examples/MultiParam/EvalI.hs-  examples/Examples/MultiParam/EvalM.hs-  examples/Examples/MultiParam/EvalAlgM.hs-  examples/Examples/MultiParam/DesugarEval.hs-  examples/Examples/MultiParam/DesugarPos.hs+  examples/Examples/Multi/Desugar.hs+  examples/Examples/Param/Lambda.hs+  examples/Examples/Param/Names.hs+  examples/Examples/Param/Graph.hs+  examples/Examples/MultiParam/Lambda.hs   examples/Examples/MultiParam/FOL.hs -flag test-  description: Build test executable.-  default:     False- flag benchmark   description: Build benchmark executable.   default:     False@@ -177,17 +168,19 @@                         Data.Comp.Automata,                         Data.Comp.Automata.Product,                         Data.Comp.Zippable,+                        Data.Comp.Thunk,                          Data.Comp.Multi,                         Data.Comp.Multi.Term,                         Data.Comp.Multi.Sum,-                        Data.Comp.Multi.Functor,-                        Data.Comp.Multi.Foldable,-                        Data.Comp.Multi.Traversable,+                        Data.Comp.Multi.HFunctor,+                        Data.Comp.Multi.HFoldable,+                        Data.Comp.Multi.HTraversable,                         Data.Comp.Multi.Algebra,                         Data.Comp.Multi.Annotation,                         Data.Comp.Multi.Show,                         Data.Comp.Multi.Equality,+                        Data.Comp.Multi.Ordering,                         Data.Comp.Multi.Variables,                         Data.Comp.Multi.Ops,                         Data.Comp.Ops,@@ -198,7 +191,6 @@                         Data.Comp.Param,                         Data.Comp.Param.Term,                         Data.Comp.Param.FreshM,-                        Data.Comp.Param.Any,                         Data.Comp.Param.Sum,                         Data.Comp.Param.Difunctor,                         Data.Comp.Param.Ditraversable,@@ -210,11 +202,11 @@                         Data.Comp.Param.Show                         Data.Comp.Param.Derive,                         Data.Comp.Param.Desugar+                        Data.Comp.Param.Thunk                          Data.Comp.MultiParam,                         Data.Comp.MultiParam.Term,                         Data.Comp.MultiParam.FreshM,-                        Data.Comp.MultiParam.Any,                         Data.Comp.MultiParam.Sum,                         Data.Comp.MultiParam.HDifunctor,                         Data.Comp.MultiParam.HDitraversable,@@ -240,12 +232,14 @@                         Data.Comp.Derive.Traversable,                         Data.Comp.Derive.Injections,                         Data.Comp.Derive.Projections,+                        Data.Comp.Derive.HaskellStrict,                         Data.Comp.Automata.Product.Derive, -                        Data.Comp.Multi.Derive.Functor,-                        Data.Comp.Multi.Derive.Foldable,-                        Data.Comp.Multi.Derive.Traversable,+                        Data.Comp.Multi.Derive.HFunctor,+                        Data.Comp.Multi.Derive.HFoldable,+                        Data.Comp.Multi.Derive.HTraversable,                         Data.Comp.Multi.Derive.Equality,+                        Data.Comp.Multi.Derive.Ordering,                         Data.Comp.Multi.Derive.Show,                         Data.Comp.Multi.Derive.SmartConstructors                         Data.Comp.Multi.Derive.SmartAConstructors@@ -280,20 +274,20 @@   if flag(benchmark)     buildable:     False -Executable test++Test-Suite test+  Type:                 exitcode-stdio-1.0   Main-is:		Data_Test.hs-  Build-Depends:	base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, test-framework, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers   hs-source-dirs:	src testsuite/tests examples-  ghc-options:          -fhpc-  if !flag(test)-    buildable:     False+  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, test-framework, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers  Executable benchmark   Main-is:		Benchmark.hs-  Build-Depends:	base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers   hs-source-dirs:	src benchmark   ghc-options:          -W -O2   -- Disable short-cut fusion rules in order to compare optimised and unoptimised code.   cpp-options:          -DNO_RULES   if !flag(benchmark)-    buildable:     False+    buildable:          False+  else+    Build-Depends:      base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers

@@ -0,0 +1,32 @@+{-# LANGUAGE TemplateHaskell, TypeOperators #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Common+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Common definitions used in examples.+--+--------------------------------------------------------------------------------++module Examples.Common where++import Data.Comp+import Data.Comp.Derive+import Data.Comp.Show ()+import Data.Comp.Equality ()++-- Signature for values and operators+data Value a = Const Int | Pair a a+data Op a    = Add a a | Mult a a | Fst a | Snd a++-- Signature for the simple expression language+type Sig = Op :+: Value++-- Derive boilerplate code using Template Haskell+$(derive [makeFunctor, makeTraversable, makeFoldable,+          makeEqF, makeShowF, smartConstructors, smartAConstructors]+         [''Value, ''Op])

@@ -0,0 +1,78 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Desugar+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Desugaring+--+-- The example illustrates how to compose a term homomorphism and an algebra,+-- exemplified via a desugaring term homomorphism and an evaluation algebra.+-- The example also illustrates how to lift a term homomorphism to annotations,+-- exemplified via a desugaring term homomorphism lifted to terms annotated with+-- source position information.+--+--------------------------------------------------------------------------------++module Examples.Desugar where++import Data.Comp+import Data.Comp.Show ()+import Data.Comp.Derive+import Data.Comp.Desugar+import Examples.Common+import Examples.Eval++-- Signature for syntactic sugar+data Sugar a = Neg a | Swap a++-- Source position information (line number, column number)+data Pos = Pos Int Int+           deriving (Show, Eq)++-- Signature for the simple expression language, extended with syntactic sugar+type Sig' = Sugar :+: Op :+: Value++-- Signature for the simple expression language with annotations+type SigP = Op :&: Pos :+: Value :&: Pos++-- Signature for the simple expression language, extended with syntactic sugar,+-- with annotations+type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos++-- Derive boilerplate code using Template Haskell+$(derive [makeFunctor, makeTraversable, makeFoldable,+          makeEqF, makeShowF, makeOrdF, smartConstructors, smartAConstructors]+         [''Sugar])++instance (Op :<: f, Value :<: f, Functor f) => Desugar Sugar f where+  desugHom' (Neg x)  = iConst (-1) `iMult` x+  desugHom' (Swap x) = iSnd x `iPair` iFst x++evalDesug :: Term Sig' -> Term Value+evalDesug = eval . (desugar :: Term Sig' -> Term Sig)++-- Example: evalEx = iPair (iConst 2) (iConst 1)+evalEx :: Term Value+evalEx = evalDesug $ iSwap $ iPair (iConst 1) (iConst 2)++-- Lift desugaring to terms annotated with source positions+desugP :: Term SigP' -> Term SigP+desugP = appHom (propAnn desugHom)++-- Example: desugPEx = iAPair (Pos 1 0)+--                            (iASnd (Pos 1 0) (iAPair (Pos 1 1)+--                                                     (iAConst (Pos 1 2) 1)+--                                                     (iAConst (Pos 1 3) 2)))+--                            (iAFst (Pos 1 0) (iAPair (Pos 1 1)+--                                                     (iAConst (Pos 1 2) 1)+--                                                     (iAConst (Pos 1 3) 2)))+desugPEx :: Term SigP+desugPEx = desugP $ iASwap (Pos 1 0) (iAPair (Pos 1 1) (iAConst (Pos 1 2) 1)+                                                       (iAConst (Pos 1 3) 2))

@@ -1,77 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances,-  OverlappingInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.DesugarEval--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Expression Evaluation------ The example illustrates how to compose a term homomorphism and an algebra,--- exemplified via a desugaring term homomorphism and an evaluation algebra.--------------------------------------------------------------------------------------module Examples.DesugarEval where--import Data.Comp-import Data.Comp.Show ()-import Data.Comp.Derive-import Data.Comp.Desugar---- Signature for values, operators, and syntactic sugar-data Value e = Const Int | Pair e e-data Op e = Add e e | Mult e e | Fst e | Snd e-data Sugar e = Neg e | Swap e---- Signature for the simple expression language-type Sig = Op :+: Value---- Signature for the simple expression language, extended with syntactic sugar-type Sig' = Sugar :+: Op :+: Value---- Derive boilerplate code using Template Haskell-$(derive [makeFunctor, makeTraversable, makeFoldable,-          makeEqF, makeShowF, smartConstructors]-         [''Value, ''Op, ''Sugar])--instance (Op :<: f, Value :<: f, Functor f) => Desugar Sugar f 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 :: Alg f (Term v)--$(derive [liftSum] [''Eval])--instance (Value :<: v) => Eval Value v where-  evalAlg = inject--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) => Term v -> Int-projC v = case project v of Just (Const n) -> n--projP :: (Value :<: v) => Term v -> (Term v, Term v)-projP v = case project v of Just (Pair x y) -> (x,y)---- Compose the evaluation algebra and the desugaring homomorphism to an algebra-eval :: Term Sig -> Term Value-eval = cata evalAlg--evalDesug :: Term Sig' -> Term Value-evalDesug = eval . desugar---- Example: evalEx = iPair (iConst 2) (iConst 1)-evalEx :: Term Value-evalEx = evalDesug $ iSwap $ iPair (iConst 1) (iConst 2)

@@ -1,72 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances,-  OverlappingInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.DesugarPos--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Propagation of Annotations------ The example illustrates how to lift a term homomorphism to products,--- exemplified via a desugaring term homomorphism lifted to terms annotated with--- source position information.--------------------------------------------------------------------------------------module Examples.DesugarPos where--import Data.Comp-import Data.Comp.Show ()-import Data.Comp.Equality ()-import Data.Comp.Derive-import Data.Comp.Desugar---- Signature for values, operators, and syntactic sugar-data Value e = Const Int | Pair e e-data Op e = Add e e | Mult e e | Fst e | Snd e-data Sugar e = Neg e | Swap e---- Source position information (line number, column number)-data Pos = Pos Int Int-           deriving (Show, Eq)---- Signature for the simple expression language-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---- Derive boilerplate code using Template Haskell-$(derive [makeFunctor, makeTraversable, makeFoldable,-          makeEqF, makeShowF, smartConstructors, smartAConstructors]-         [''Value, ''Op, ''Sugar])--instance (Op :<: f, Value :<: f, Functor f) => Desugar Sugar f where-  desugHom' (Neg x)  = iConst (-1) `iMult` x-  desugHom' (Swap x) = iSnd x `iPair` iFst x---- Example: desugEx = iPair (iConst 2) (iConst 1)-desugEx :: Term Sig-desugEx = desugar (iSwap $ iPair (iConst 1) (iConst 2) :: Term Sig')---- Lift desugaring to terms annotated with source positions-desugP :: Term SigP' -> Term SigP-desugP = appHom (propAnn desugHom)---- Example: desugPEx = iAPair (Pos 1 0)---                            (iASnd (Pos 1 0) (iAPair (Pos 1 1)---                                                     (iAConst (Pos 1 2) 1)---                                                     (iAConst (Pos 1 3) 2)))---                            (iAFst (Pos 1 0) (iAPair (Pos 1 1)---                                                     (iAConst (Pos 1 2) 1)---                                                     (iAConst (Pos 1 3) 2)))-desugPEx :: Term SigP-desugPEx = desugP $ iASwap (Pos 1 0) (iAPair (Pos 1 1) (iAConst (Pos 1 2) 1)-                                                       (iAConst (Pos 1 3) 2))

@@ -1,5 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances #-}+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances #-} -------------------------------------------------------------------------------- -- | -- Module      :  Examples.Eval@@ -22,17 +23,7 @@ import Data.Comp import Data.Comp.Show () import Data.Comp.Derive---- Signature for values and operators-data Value e = Const Int | Pair e e-data Op e = Add e e | Mult e e | Fst e | Snd e---- Signature for the simple expression language-type Sig = Op :+: Value---- Derive boilerplate code using Template Haskell-$(derive [makeFunctor, makeShowF,-          makeEqF, smartConstructors] [''Value, ''Op])+import Examples.Common  -- Term evaluation algebra class Eval f v where@@ -44,12 +35,12 @@ eval :: (Functor f, Eval f v) => Term f -> Term v eval = cata evalAlg -instance (Value :<: v) => Eval Value v where-  evalAlg = inject+instance (f :<: v) => Eval f v where+  evalAlg = inject -- default instance  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 (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 @@ -61,4 +52,4 @@  -- Example: evalEx = iConst 5 evalEx :: Term Value-evalEx = eval ((iConst 1) `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)+evalEx = eval (iConst 1 `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)

@@ -1,5 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances #-}+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances #-} -------------------------------------------------------------------------------- -- | -- Module      :  Examples.EvalM@@ -22,18 +23,7 @@ import Data.Comp import Data.Comp.Derive import Control.Monad (liftM)---- Signature for values and operators-data Value e = Const Int | Pair e e-data Op e = Add e e | Mult e e | Fst e | Snd e---- Signature for the simple expression language-type Sig = Op :+: Value---- Derive boilerplate code using Template Haskell-$(derive [makeFunctor, makeTraversable, makeFoldable,-          makeEqF, makeShowF, smartConstructors]-         [''Value, ''Op])+import Examples.Common  -- Monadic term evaluation algebra class EvalM f v where@@ -45,8 +35,8 @@ evalM :: (Traversable f, EvalM f v) => Term f -> Maybe (Term v) evalM = cataM evalAlgM -instance (Value :<: v) => EvalM Value v where-  evalAlgM = return . inject+instance (f :<: v) => EvalM f v where+  evalAlgM = return . inject -- default instance  instance (Value :<: v) => EvalM Op v where   evalAlgM (Add x y)  = do n1 <- projC x@@ -70,4 +60,4 @@  -- Example: evalMEx = Just (iConst 5) evalMEx :: Maybe (Term Value)-evalMEx = evalM ((iConst 1) `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)+evalMEx = evalM (iConst 1 `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)

@@ -0,0 +1,39 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Multi.Common+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Common example files.+--+--------------------------------------------------------------------------------++module Examples.Multi.Common where++import Data.Comp.Multi+import Data.Comp.Multi.Show ()+import Data.Comp.Multi.Equality ()+import Data.Comp.Multi.Ordering ()+import Data.Comp.Multi.Derive++-- Signature for values and operators+data Value a i where+  Const ::        Int -> Value a Int+  Pair  :: a i -> a j -> Value a (i,j)+data Op a i where+  Add, Mult :: a Int -> a Int   -> Op a Int+  Fst       ::          a (i,j) -> Op a i+  Snd       ::          a (i,j) -> Op a j++-- Signature for the simple expression language+type Sig = Op :+: Value++-- Derive boilerplate code using Template Haskell (GHC 7 needed)+$(derive [makeHFunctor, makeHFoldable, makeHTraversable, makeShowHF, makeEqHF,+          makeOrdHF, smartConstructors, smartAConstructors] +         [''Value, ''Op])

@@ -0,0 +1,75 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,+  OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Multi.Desugar+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Desugaring+--+-- The example illustrates how to compose a term homomorphism and an algebra,+-- exemplified via a desugaring term homomorphism and an evaluation algebra.+-- The example also illustrates how to lift a term homomorphism to products,+-- exemplified via a desugaring term homomorphism lifted to terms annotated with+-- source position information.+--+--------------------------------------------------------------------------------++module Examples.Multi.Desugar where++import Data.Comp.Multi+import Data.Comp.Multi.Derive+import Data.Comp.Multi.Desugar+import Examples.Multi.Common+import Examples.Multi.Eval++-- Signature for syntactic sugar+data Sugar a i where+  Neg  :: a Int   -> Sugar a Int+  Swap :: a (i,j) -> Sugar a (j,i)++-- Source position information (line number, column number)+data Pos = Pos Int Int+           deriving (Eq, Show)++-- Signature for the simple expression language+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++-- Derive boilerplate code using Template Haskell (GHC 7 needed)+$(derive [makeHFunctor, makeHTraversable, makeHFoldable, makeEqHF, makeShowHF,+          makeOrdHF, smartConstructors, smartAConstructors]+         [''Sugar])++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++-- Compose the evaluation algebra and the desugaring homomorphism to an+-- algebra+evalDesug :: Term Sig' :-> Term Value+evalDesug = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))++-- Example: evalEx = iPair (iConst 2) (iConst 1)+evalEx :: Term Value (Int,Int)+evalEx = evalDesug $ iSwap $ iPair (iConst 1) (iConst 2)++-- Example: desugPEx = iAPair (Pos 1 0)+--                            (iASnd (Pos 1 0) (iAPair (Pos 1 1)+--                                                     (iAConst (Pos 1 2) 1)+--                                                     (iAConst (Pos 1 3) 2)))+--                            (iAFst (Pos 1 0) (iAPair (Pos 1 1)+--                                                     (iAConst (Pos 1 2) 1)+--                                                     (iAConst (Pos 1 3) 2)))+desugPEx :: Term SigP (Int,Int)+desugPEx = desugarA (iASwap (Pos 1 0) (iAPair (Pos 1 1) (iAConst (Pos 1 2) 1)+                                                        (iAConst (Pos 1 3) 2))+                     :: Term SigP' (Int,Int))

@@ -1,88 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,-  OverlappingInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Multi.DesugarEval--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Expression Evaluation------ The example illustrates how to compose a term homomorphism and an algebra,--- exemplified via a desugaring term homomorphism and an evaluation algebra.--------------------------------------------------------------------------------------module Examples.Multi.DesugarEval where--import Data.Comp.Multi-import Data.Comp.Multi.Show ()-import Data.Comp.Multi.Derive-import Data.Comp.Multi.Desugar---- Signature for values, operators, and syntactic sugar-data Value e l where-  Const  ::        Int -> Value e Int-  Pair   :: e s -> e t -> Value e (s,t)-data Op e l where-  Add, Mult  :: e Int -> e Int   -> Op e Int-  Fst        ::          e (s,t) -> Op e s-  Snd        ::          e (s,t) -> Op e t-data Sugar e l where-  Neg   :: e Int   -> Sugar e Int-  Swap  :: e (s,t) -> Sugar e (t,s)---- Source position information (line number, column number)-data Pos = Pos Int Int-           deriving Show---- Signature for the simple expression language-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---- Derive boilerplate code using Template Haskell (GHC 7 needed)-$(derive [makeHFunctor, makeHTraversable, makeHFoldable,-          makeHEqF, makeHShowF, smartConstructors]-         [''Value, ''Op, ''Sugar])--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 :: Alg f (Term v)--$(derive [liftSum] [''Eval])--instance (Value :<: v) => Eval Value v where-  evalAlg = inject--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) => Term v Int -> Int-projC v = case project v of Just (Const n) -> n--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)---- Compose the evaluation algebra and the desugaring homomorphism to an--- algebra-eval :: Term Sig' :-> Term Value-eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))---- Example: evalEx = iPair (iConst 2) (iConst 1)-evalEx :: Term Value (Int,Int)-evalEx = eval $ iSwap $ iPair (iConst 1) (iConst 2)

@@ -1,75 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,-  OverlappingInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Multi.DesugarPos--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Propagation of Annotations------ The example illustrates how to lift a term homomorphism to products,--- exemplified via a desugaring term homomorphism lifted to terms annotated with--- source position information.--------------------------------------------------------------------------------------module Examples.Multi.DesugarPos where--import Data.Comp.Multi-import Data.Comp.Multi.Show ()-import Data.Comp.Multi.Derive-import Data.Comp.Multi.Desugar---- Signature for values, operators, and syntactic sugar-data Value e l where-  Const  ::        Int -> Value e Int-  Pair   :: e s -> e t -> Value e (s,t)-data Op e l where-  Add, Mult  :: e Int -> e Int   -> Op e Int-  Fst        ::          e (s,t) -> Op e s-  Snd        ::          e (s,t) -> Op e t-data Sugar e l where-  Neg   :: e Int   -> Sugar e Int-  Swap  :: e (s,t) -> Sugar e (t,s)---- Source position information (line number, column number)-data Pos = Pos Int Int-           deriving (Show, Eq)---- Signature for the simple expression language-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---- Derive boilerplate code using Template Haskell (GHC 7 needed)-$(derive [makeHFunctor, makeHTraversable, makeHFoldable,-          makeHEqF, makeHShowF, smartConstructors, smartAConstructors]-         [''Value, ''Op, ''Sugar])--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---- Example: desugEx = iPair (iConst 2) (iConst 1)-desugEx :: Term Sig (Int,Int)-desugEx = desugar (iSwap $ iPair (iConst 1) (iConst 2) :: Term Sig' (Int,Int))---- Example: desugPEx = iAPair (Pos 1 0)---                            (iASnd (Pos 1 0) (iAPair (Pos 1 1)---                                                     (iAConst (Pos 1 2) 1)---                                                     (iAConst (Pos 1 3) 2)))---                            (iAFst (Pos 1 0) (iAPair (Pos 1 1)---                                                     (iAConst (Pos 1 2) 1)---                                                     (iAConst (Pos 1 3) 2)))-desugPEx :: Term SigP (Int,Int)-desugPEx = desugarA (iASwap (Pos 1 0) (iAPair (Pos 1 1) (iAConst (Pos 1 2) 1)-                                                        (iAConst (Pos 1 3) 2))-                     :: Term SigP' (Int,Int))

@@ -1,5 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs #-}+  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,+  OverlappingInstances #-} -------------------------------------------------------------------------------- -- | -- Module      :  Examples.Multi.Eval@@ -20,24 +21,8 @@ module Examples.Multi.Eval where  import Data.Comp.Multi-import Data.Comp.Multi.Show () import Data.Comp.Multi.Derive---- Signature for values and operators-data Value e l where-  Const  ::        Int -> Value e Int-  Pair   :: e s -> e t -> Value e (s,t)-data Op e l where-  Add, Mult  :: e Int -> e Int   -> Op e Int-  Fst        ::          e (s,t) -> Op e s-  Snd        ::          e (s,t) -> Op e t---- Signature for the simple expression language-type Sig = Op :+: Value---- Derive boilerplate code using Template Haskell (GHC 7 needed)-$(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors] -         [''Value, ''Op])+import Examples.Multi.Common  -- Term evaluation algebra class Eval f v where@@ -49,12 +34,12 @@ eval :: (HFunctor f, Eval f v) => Term f :-> Term v eval = cata evalAlg -instance (Value :<: v) => Eval Value v where-  evalAlg = inject+instance (f :<: v) => Eval f v where+  evalAlg = inject -- default instance  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 (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 

@@ -9,7 +9,7 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- Intrinsic Expression Evaluation+-- Intrinsic, Tag-less Expression Evaluation -- -- The example illustrates how to use generalised compositional data types  -- to implement a small expression language, and  an evaluation function mapping@@ -20,24 +20,8 @@ module Examples.Multi.EvalI where  import Data.Comp.Multi-import Data.Comp.Multi.Show () import Data.Comp.Multi.Derive---- Signature for values and operators-data Value e l where-  Const  ::        Int -> Value e Int-  Pair   :: e s -> e t -> Value e (s,t)-data Op e l where-  Add, Mult  :: e Int -> e Int   -> Op e Int-  Fst        ::          e (s,t) -> Op e s-  Snd        ::          e (s,t) -> Op e t---- Signature for the simple expression language-type Sig = Op :+: Value---- Derive boilerplate code using Template Haskell (GHC 7 needed)-$(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors] -         [''Value, ''Op])+import Examples.Multi.Common  -- Term evaluation algebra class EvalI f where

@@ -1,5 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs #-}+  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,+  OverlappingInstances #-} -------------------------------------------------------------------------------- -- | -- Module      :  Examples.Multi.EvalM@@ -20,26 +21,9 @@ module Examples.Multi.EvalM where  import Data.Comp.Multi-import Data.Comp.Multi.Show () import Data.Comp.Multi.Derive import Control.Monad (liftM)---- Signature for values and operators-data Value e l where-  Const  ::        Int -> Value e Int-  Pair   :: e s -> e t -> Value e (s,t)-data Op e l where-  Add, Mult  :: e Int -> e Int   -> Op e Int-  Fst        ::          e (s,t) -> Op e s-  Snd        ::          e (s,t) -> Op e t---- Signature for the simple expression language-type Sig = Op :+: Value---- Derive boilerplate code using Template Haskell (GHC 7 needed)-$(derive [makeHFunctor, makeHTraversable, makeHFoldable,-          makeHEqF, makeHShowF, smartConstructors]-         [''Value, ''Op])+import Examples.Multi.Common  -- Monadic term evaluation algebra class EvalM f v where@@ -47,11 +31,11 @@  $(derive [liftSum] [''EvalM]) -evalM :: (HTraversable f, EvalM f v) => Term f l -> Maybe (Term v l)+evalM :: (HTraversable f, EvalM f v) => Term f i -> Maybe (Term v i) evalM = cataM evalAlgM -instance (Value :<: v) => EvalM Value v where-  evalAlgM = return . inject+instance (f :<: v) => EvalM f v where+  evalAlgM = return . inject -- default instance  instance (Value :<: v) => EvalM Op v where   evalAlgM (Add x y)  = do n1 <- projC x@@ -73,5 +57,4 @@  -- Example: evalMEx = Just (iConst 5) evalMEx :: Maybe (Term Value Int)-evalMEx = evalM ((iConst 1) `iAdd`-                 (iConst 2 `iMult` iConst 2) :: Term Sig Int)+evalMEx = evalM (iConst 1 `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig Int)

@@ -1,107 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances,-  TypeSynonymInstances, OverlappingInstances, GADTs, KindSignatures #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.MultiParam.DesugarEval--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Expression Evaluation------ The example illustrates how to compose a term homomorphism and an algebra,--- exemplified via a desugaring term homomorphism and an evaluation algebra.------ The example extends the example from 'Examples.MultiParam.Eval'.--------------------------------------------------------------------------------------module Examples.MultiParam.DesugarEval where--import Data.Comp.MultiParam hiding (Const)-import Data.Comp.MultiParam.Show ()-import Data.Comp.MultiParam.Derive-import Data.Comp.MultiParam.Desugar---- Signatures for values and operators-data Const :: (* -> *) -> (* -> *) -> * -> * where-    Const :: Int -> Const a e Int-data Lam :: (* -> *) -> (* -> *) -> * -> * where-    Lam :: (a i -> e j) -> Lam a e (i -> j)-data App :: (* -> *) -> (* -> *) -> * -> * where-    App :: e (i -> j) -> e i -> App a e j-data Op :: (* -> *) -> (* -> *) -> * -> * where-    Add :: e Int -> e Int -> Op a e Int-    Mult :: e Int -> e Int -> Op a e Int-data Fun :: (* -> *) -> (* -> *) -> * -> * where-    Fun :: (e i -> e j) -> Fun a e (i -> j)-data IfThenElse :: (* -> *) -> (* -> *) -> * -> * where-                   IfThenElse :: (e Int) -> (e i) -> (e i) -> IfThenElse a e i---- Signature for syntactic sugar (negation, let expressions)-data Sug :: (* -> *) -> (* -> *) -> * -> * where-            Neg :: e Int -> Sug a e Int-            Let :: e i -> (a i -> e j) -> Sug a e j---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op :+: IfThenElse--- Signature for the simple expression language with syntactic sugar-type Sig' = Sug :+: Sig--- Signature for values. Note the use of 'Fun' rather than 'Lam' (!)-type Value = Const :+: Fun--- Signature for ground values.-type GValue = Const---- Derive boilerplate code using Template Haskell-$(derive [makeHDifunctor, makeEqHD, makeShowHD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op, ''IfThenElse, ''Sug])-$(derive [makeHFoldable, makeHTraversable]-         [''Const, ''App, ''Op])--instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, HDifunctor f)-  => Desugar Sug f where-  desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = inject (Lam y) `iApp` x---- Term evaluation algebra-class Eval f v where-  evalAlg :: Alg f (Term v)--$(derive [liftSum] [''Eval])---- Compose the evaluation algebra and the desugaring homomorphism to an algebra-eval :: Term Sig' :-> Term Value-eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))--instance (Const :<: v) => Eval Const v where-  evalAlg (Const n) = iConst n--instance (Const :<: v) => Eval Op v where-  evalAlg (Add x y)  = iConst $ (projC x) + (projC y)-  evalAlg (Mult x y) = iConst $ (projC x) * (projC y)--instance (Fun :<: v) => Eval App v where-  evalAlg (App x y) = (projF x) y--instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = inject $ Fun f--instance (Const :<: v) => Eval IfThenElse v where-  evalAlg (IfThenElse c v1 v2) = if projC c /= 0 then v1 else v2--projC :: (Const :<: v) => Term v Int -> Int-projC v = case project v of Just (Const n) -> n--projF :: (Fun :<: v) => Term v (i -> j) -> Term v i -> Term v j-projF v = case project v of Just (Fun f) -> f---- |Evaluation of expressions to ground values.-evalG :: Term Sig' i -> Maybe (Term GValue i)-evalG = deepProject . (eval :: Term Sig' :-> Term Value)---- Example: evalEx = Just (iConst -6)-evalEx :: Maybe (Term GValue Int)-evalEx = evalG $ iLet (iConst 6) $ \x -> iNeg x

@@ -1,75 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances,-  TypeSynonymInstances, OverlappingInstances, GADTs, KindSignatures #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.MultiParam.DesugarPos--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Propagation of Annotations.------ The example illustrates how to compose a term homomorphism and an algebra,--- exemplified via a desugaring term homomorphism and an evaluation algebra.--------------------------------------------------------------------------------------module Examples.MultiParam.DesugarPos where--import Data.Comp.MultiParam hiding (Const)-import Data.Comp.MultiParam.Show ()-import Data.Comp.MultiParam.Derive-import Data.Comp.MultiParam.Desugar---- Signatures for values and operators-data Const :: (* -> *) -> (* -> *) -> * -> * where-    Const :: Int -> Const a e Int-data Lam :: (* -> *) -> (* -> *) -> * -> * where-    Lam :: (a i -> e j) -> Lam a e (i -> j)-data App :: (* -> *) -> (* -> *) -> * -> * where-    App :: e (i -> j) -> e i -> App a e j-data Op :: (* -> *) -> (* -> *) -> * -> * where-    Add :: e Int -> e Int -> Op a e Int-    Mult :: e Int -> e Int -> Op a e Int-data Fun :: (* -> *) -> (* -> *) -> * -> * where-    Fun :: (e i -> e j) -> Fun a e (i -> j)-data IfThenElse :: (* -> *) -> (* -> *) -> * -> * where-                   IfThenElse :: (e Int) -> (e i) -> (e i) -> IfThenElse a e i---- Signature for syntactic sugar (negation, let expressions)-data Sug :: (* -> *) -> (* -> *) -> * -> * where-            Neg :: e Int -> Sug a e Int-            Let :: e i -> (a i -> e j) -> Sug a e j---- Source position information (line number, column number)-data Pos = Pos Int Int-           deriving (Show, Eq)---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op-type SigP = Const :&: Pos :+: Lam :&: Pos :+: App :&: Pos :+: Op :&: Pos---- Signature for the simple expression language, extended with syntactic sugar-type Sig' = Sug :+: Sug-type SigP' = Sug :&: Pos :+: SigP---- Derive boilerplate code using Template Haskell-$(derive [makeHDifunctor, makeEqHD, makeShowHD,-          smartConstructors, smartAConstructors]-         [''Const, ''Lam, ''App, ''Op, ''Sug])--instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, HDifunctor f)-  => Desugar Sug f where-  desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = inject (Lam y) `iApp` x---- Example: desugPEx == iAApp (Pos 1 0)--- (iALam (Pos 1 0) $ \x -> iAMult (Pos 1 2) (iAConst (Pos 1 2) (-1)) x)--- (iAConst (Pos 1 1) 6)-desugPEx :: Term SigP Int-desugPEx = desugarA (iALet (Pos 1 0)-                           (iAConst (Pos 1 1) 6)-                           (\x -> iANeg (Pos 1 2) x :: Term SigP' Int))

@@ -1,96 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,-  KindSignatures #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.MultiParam.Eval--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Expression Evaluation------ The example illustrates how to use generalised parametric compositional data--- types to implement a small expression language, with a language of values,--- and an evaluation function mapping typed expressions to typed values. The--- example demonstrates how (parametric) abstractions are mapped to general--- functions, from values to values, and how it is possible to project a general--- value (with functions) back into ground values, that can again be analysed.------ The following language extensions are needed in order to run the example:--- @TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,--- @FlexibleInstances@, @FlexibleContexts@, @UndecidableInstances@, @GADTs@,--- and @KindSignatures@.--------------------------------------------------------------------------------------module Examples.MultiParam.Eval where--import Data.Comp.MultiParam hiding (Const)-import Data.Comp.MultiParam.Show ()-import Data.Comp.MultiParam.Derive---- Signatures for values and operators-data Const :: (* -> *) -> (* -> *) -> * -> * where-    Const :: Int -> Const a e Int-data Lam :: (* -> *) -> (* -> *) -> * -> * where-    Lam :: (a i -> e j) -> Lam a e (i -> j)-data App :: (* -> *) -> (* -> *) -> * -> * where-    App :: e (i -> j) -> e i -> App a e j-data Op :: (* -> *) -> (* -> *) -> * -> * where-    Add :: e Int -> e Int -> Op a e Int-    Mult :: e Int -> e Int -> Op a e Int-data Fun :: (* -> *) -> (* -> *) -> * -> * where-    Fun :: (e i -> e j) -> Fun a e (i -> j)---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op--- Signature for values. Note the use of 'Fun' rather than 'Lam' (!)-type Value = Const :+: Fun--- Signature for ground values.-type GValue = Const---- Derive boilerplate code using Template Haskell-$(derive [makeHDifunctor, makeEqHD, makeShowHD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op])-$(derive [makeHFoldable, makeHTraversable]-         [''Const, ''App, ''Op])---- Term evaluation algebra-class Eval f v where-  evalAlg :: Alg f (Term v)--$(derive [liftSum] [''Eval])---- Lift the evaluation algebra to a catamorphism-eval :: (HDifunctor f, Eval f v) => Term f :-> Term v-eval = cata evalAlg--instance (Const :<: v) => Eval Const v where-  evalAlg (Const n) = iConst n--instance (Const :<: v) => Eval Op v where-  evalAlg (Add x y)  = iConst $ (projC x) + (projC y)-  evalAlg (Mult x y) = iConst $ (projC x) * (projC y)--instance (Fun :<: v) => Eval App v where-  evalAlg (App x y) = (projF x) y--instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = inject $ Fun f--projC :: (Const :<: v) => Term v Int -> Int-projC v = case project v of Just (Const n) -> n--projF :: (Fun :<: v) => Term v (i -> j) -> Term v i -> Term v j-projF v = case project v of Just (Fun f) -> f---- |Evaluation of expressions to ground values.-evalG :: Term Sig i -> Maybe (Term GValue i)-evalG = deepProject . (eval :: Term Sig :-> Term Value)---- Example: evalEx = Just (iConst 4)-evalEx :: Maybe (Term GValue Int)-evalEx = evalG $ (iLam $ \x -> x `iAdd` x) `iApp` iConst 2

@@ -1,86 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,-  KindSignatures #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.MultiParam.EvalAlgM--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Monadic Expression Evaluation without PHOAS------ The example illustrates how to use generalised parametric compositional--- data types to implement a small expression language, with a sub language of--- values, and a monadic evaluation function mapping expressions to values.--- The lack of PHOAS means that -- unlike the example in--- 'Examples.MultiParam.EvalM' -- a monadic algebra can be used.--------------------------------------------------------------------------------------module Examples.MultiParam.EvalAlgM where--import Data.Comp.MultiParam-import Data.Comp.MultiParam.Show ()-import Data.Comp.MultiParam.HDitraversable-import Data.Comp.MultiParam.Derive-import Control.Monad (liftM)---- Signature for values and operators-data Value :: (* -> *) -> (* -> *) -> * -> * where-              Const :: Int -> Value a e Int-              Pair :: e i -> e j -> Value a e (i,j)-data Op :: (* -> *) -> (* -> *) -> * -> * where-           Add :: e Int -> e Int -> Op a e Int-           Mult :: e Int -> e Int -> Op a e Int-           Fst :: e (i,j) -> Op a e i-           Snd :: e (i,j) -> Op a e j---- Signature for the simple expression language-type Sig = Op :+: Value---- Derive boilerplate code using Template Haskell-$(derive [makeHDifunctor, makeHTraversable, makeHFoldable,-          makeEqHD, makeShowHD, smartConstructors]-         [''Value, ''Op])---- Monadic term evaluation algebra-class EvalM f v where-  evalAlgM :: AlgM Maybe f (Term v)--$(derive [liftSum] [''EvalM])---- Lift the monadic evaluation algebra to a monadic catamorphism-evalM :: (HDitraversable f Maybe (Term v), EvalM f v)-         => Term f i -> Maybe (Term v i)-evalM = cataM evalAlgM--instance (Value :<: v) => EvalM Value v where-  evalAlgM (Const n) = return $ iConst n-  evalAlgM (Pair x y) = return $ iPair x y--instance (Value :<: v) => EvalM Op v where-  evalAlgM (Add x y)  = do n1 <- projC x-                           n2 <- projC y-                           return $ iConst $ n1 + n2-  evalAlgM (Mult x y) = do n1 <- projC x-                           n2 <- projC y-                           return $ iConst $ n1 * n2-  evalAlgM (Fst v)    = liftM fst $ projP v-  evalAlgM (Snd v)    = liftM snd $ projP v--projC :: (Value :<: v) => Term v Int -> Maybe Int-projC v = case project v of-            Just (Const n) -> return n-            _ -> Nothing--projP :: (Value :<: v) => Term v (i,j) -> Maybe (Term v i, Term v j)-projP v = case project v of-            Just (Pair x y) -> return (x,y)-            _ -> Nothing---- Example: evalMEx = Just (iConst 5)-evalMEx :: Maybe (Term Value Int)-evalMEx = evalM ((iConst 1) `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig Int)

@@ -1,75 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,-  KindSignatures #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.MultiParam.EvalI--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Intrinsic Expression Evaluation------ The example illustrates how to use generalised parametric compositional data--- types to implement a small expression language, and an evaluation function--- mapping typed expressions to values.--------------------------------------------------------------------------------------module Examples.MultiParam.EvalI where--import Data.Comp.MultiParam hiding (Const)-import Data.Comp.MultiParam.Show ()-import Data.Comp.MultiParam.Derive---- Signatures for values and operators-data Const :: (* -> *) -> (* -> *) -> * -> * where-    Const :: Int -> Const a e Int-data Lam :: (* -> *) -> (* -> *) -> * -> * where-    Lam :: (a i -> e j) -> Lam a e (i -> j)-data App :: (* -> *) -> (* -> *) -> * -> * where-    App :: e (i -> j) -> e i -> App a e j-data Op :: (* -> *) -> (* -> *) -> * -> * where-    Add :: e Int -> e Int -> Op a e Int-    Mult :: e Int -> e Int -> Op a e Int---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op---- Derive boilerplate code using Template Haskell-$(derive [makeHDifunctor, makeEqHD, makeShowHD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op])-$(derive [makeHFoldable, makeHTraversable]-         [''Const, ''App, ''Op])---- Term evaluation algebra-class Eval f where-  evalAlg :: Alg f I-  evalAlg = I . evalAlg'-  evalAlg' :: f I I i -> i-  evalAlg' = unI . evalAlg--$(derive [liftSum] [''Eval])---- Lift the evaluation algebra to a catamorphism-eval :: (HDifunctor f, Eval f) => Term f i -> i-eval = unI . cata evalAlg--instance Eval Const where-  evalAlg' (Const n) = n--instance Eval Op where-  evalAlg' (Add (I x) (I y))  = x + y-  evalAlg' (Mult (I x) (I y)) = x * y--instance Eval App where-  evalAlg' (App (I f) (I x)) = f x--instance Eval Lam where-  evalAlg' (Lam f) = unI . f . I---- Example: evalEx = 4-evalEx :: Int-evalEx = eval $ ((iLam $ \x -> x `iAdd` x) `iApp` iConst 2 :: Term Sig Int)

@@ -1,102 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,-  KindSignatures, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.MultiParam.EvalM--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Monadic Expression Evaluation------ The example illustrates how to use generalised parametric compositional data--- types to implement a small expression language, with a language of values,--- and a monadic evaluation function mapping expressions to values. The example--- demonstrates how (parametric) abstractions are mapped to general functions,--- from values to /monadic/ values, and how it is possible to project a general--- value (with functions) back into ground values, that can again be analysed.--------------------------------------------------------------------------------------module Examples.MultiParam.EvalM where--import Data.Comp.MultiParam hiding (Const)-import Data.Comp.MultiParam.Show ()-import Data.Comp.MultiParam.Derive-import Control.Monad ((<=<))---- Signatures for values and operators-data Const :: (* -> *) -> (* -> *) -> * -> * where-    Const :: Int -> Const a e Int-data Lam :: (* -> *) -> (* -> *) -> * -> * where-    Lam :: (a i -> e j) -> Lam a e (i -> j)-data App :: (* -> *) -> (* -> *) -> * -> * where-    App :: e (i -> j) -> e i -> App a e j-data Op :: (* -> *) -> (* -> *) -> * -> * where-    Add :: e Int -> e Int -> Op a e Int-    Mult :: e Int -> e Int -> Op a e Int-data FunM :: (* -> *) -> (* -> *) -> (* -> *) -> * -> * where-    FunM :: (e i -> Compose m e j) -> FunM m a e (i -> j)---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op--- Signature for values. Note the use of 'FunM' rather than 'Lam' (!)-type Value = Const :+: FunM Maybe--- Signature for ground values.-type GValue = Const---- Derive boilerplate code using Template Haskell-$(derive [makeHDifunctor, makeEqHD, makeShowHD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op])-$(derive [makeHFoldable, makeHTraversable]-         [''Const, ''App, ''Op])---- Term evaluation algebra.-class EvalM f v where-  evalAlgM :: AlgM' Maybe f (Term v)--$(derive [liftSum] [''EvalM])---- Lift the evaluation algebra to a catamorphism-evalM :: (HDifunctor f, EvalM f v) => Term f i -> Maybe (Term v i)-evalM = cataM' evalAlgM--instance (Const :<: v) => EvalM Const v where-  evalAlgM (Const n) = return $ iConst n--instance (Const :<: v) => EvalM Op v where-  evalAlgM (Add mx my) = do x <- projC =<< getCompose mx-                            y <- projC =<< getCompose my-                            return $ iConst $ x + y-  evalAlgM (Mult mx my) = do x <- projC =<< getCompose mx-                             y <- projC =<< getCompose my-                             return $ iConst $ x * y--instance (FunM Maybe :<: v) => EvalM App v where-  evalAlgM (App mx my) = do f <- projF =<< getCompose mx-                            (getCompose . f) =<< getCompose my--instance (FunM Maybe :<: v) => EvalM Lam v where-  evalAlgM (Lam f) = return $ inject $ FunM f--projC :: (Const :<: v) => Term v Int -> Maybe Int-projC v = case project v of-            Just (Const n) -> return n; _ -> Nothing--projF :: (FunM Maybe :<: v)-         => Term v (i -> j) -> Maybe (Term v i -> Compose Maybe (Term v) j)-projF v = case project v of-            Just (FunM f :: FunM Maybe Any (Term v) (i -> j)) -> return f-            _ -> Nothing---- |Evaluation of expressions to ground values.-evalMG :: Term Sig i -> Maybe (Term GValue i)-evalMG = deepProject <=< (evalM :: Term Sig i -> Maybe (Term Value i))---- Example: evalEx = Just (iConst 12) (3 * (2 + 2) = 12)-evalMEx :: Maybe (Term GValue Int)-evalMEx = evalMG $ (iLam $ \x -> iLam $ \y -> y `iMult` (x `iAdd` x))-                   `iApp` iConst 2 `iApp` iConst 3

@@ -1,6 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, FlexibleInstances,   FlexibleContexts, UndecidableInstances, GADTs, KindSignatures,-  OverlappingInstances, TypeSynonymInstances #-}+  OverlappingInstances, TypeSynonymInstances, EmptyDataDecls #-} -------------------------------------------------------------------------------- -- | -- Module      :  Examples.MultiParam.FOL@@ -10,26 +10,27 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- First-Order Logic à la Carte+-- First-Order Logic a la Carte ----- This example illustrates how to implement First-Order Logic à la Carte+-- This example illustrates how to implement First-Order Logic a la Carte -- (Knowles, The Monad.Reader Issue 11, '08) using Generalised Parametric -- Compositional Data Types. ----- Rather than having a fixed domain @Term@ for binders, a la Knowles, our--- encoding uses a mutually recursive data structure for terms and formulae.--- This enables variables to be introduced only when they are actually needed--- in the term language, i.e. in stage 5.+-- Rather than using a fixed domain 'Term' for binders as Knowles, our encoding+-- uses a mutually recursive data structure for terms and formulae. This makes+-- terms modular too, and hence we only introduce variables when they are+-- actually needed in stage 5. -- --------------------------------------------------------------------------------  module Examples.MultiParam.FOL where -import Data.Comp.MultiParam hiding (Const)+import Data.Comp.MultiParam hiding (Var)+import qualified Data.Comp.MultiParam as MP import Data.Comp.MultiParam.Show () import Data.Comp.MultiParam.Derive-import Data.Comp.MultiParam.FreshM (genVar)-import Data.List (intersperse)+import Data.Comp.MultiParam.FreshM (Name, withName, evalFreshM)+import Data.List (intercalate) import Data.Maybe import Control.Monad.State import Control.Monad.Reader@@ -40,217 +41,192 @@  -- Terms data Const :: (* -> *) -> (* -> *) -> * -> * where-              Const :: String -> [e TTerm] -> Const a e TTerm+    Const :: String -> [e TTerm] -> Const a e TTerm data Var :: (* -> *) -> (* -> *) -> * -> * where-            Var :: String -> Var a e TTerm+    Var :: String -> Var a e TTerm  -- Formulae data TT :: (* -> *) -> (* -> *) -> * -> * where-           TT :: TT a e TFormula+    TT :: TT a e TFormula data FF :: (* -> *) -> (* -> *) -> * -> * where-           FF :: FF a e TFormula+    FF :: FF a e TFormula data Atom :: (* -> *) -> (* -> *) -> * -> * where-             Atom :: String -> [e TTerm] -> Atom a e TFormula+    Atom :: String -> [e TTerm] -> Atom a e TFormula data NAtom :: (* -> *) -> (* -> *) -> * -> * where-              NAtom :: String -> [e TTerm] -> NAtom a e TFormula+    NAtom :: String -> [e TTerm] -> NAtom a e TFormula data Not :: (* -> *) -> (* -> *) -> * -> * where-            Not :: e TFormula -> Not a e TFormula+    Not :: e TFormula -> Not a e TFormula data Or :: (* -> *) -> (* -> *) -> * -> * where-           Or :: e TFormula -> e TFormula -> Or a e TFormula+    Or :: e TFormula -> e TFormula -> Or a e TFormula data And :: (* -> *) -> (* -> *) -> * -> * where-            And :: e TFormula -> e TFormula -> And a e TFormula+    And :: e TFormula -> e TFormula -> And a e TFormula data Impl :: (* -> *) -> (* -> *) -> * -> * where-             Impl :: e TFormula -> e TFormula -> Impl a e TFormula+    Impl :: e TFormula -> e TFormula -> Impl a e TFormula data Exists :: (* -> *) -> (* -> *) -> * -> * where-               Exists :: (a TTerm -> e TFormula) -> Exists a e TFormula+    Exists :: (a TTerm -> e TFormula) -> Exists a e TFormula data Forall :: (* -> *) -> (* -> *) -> * -> * where-               Forall :: (a TTerm -> e TFormula) -> Forall a e TFormula+    Forall :: (a TTerm -> e TFormula) -> Forall a e TFormula --- Derive boilerplate code using Template Haskell $(derive [makeHDifunctor, smartConstructors]          [''Const, ''Var, ''TT, ''FF, ''Atom, ''NAtom,           ''Not, ''Or, ''And, ''Impl, ''Exists, ''Forall])  ----------------------------------------------------------------------------------- Pretty printing of terms and formulae+-- (Custom) pretty printing of terms and formulae --------------------------------------------------------------------------------  instance ShowHD Const where-    showHD (Const f t) = do-      ts <- mapM pshow t-      return $ f ++ "(" ++ concat (intersperse ", " ts) ++ ")"+  showHD (Const f t) = do ts <- mapM unK t+                          return $ f ++ "(" ++ intercalate ", " ts ++ ")"  instance ShowHD Var where-    showHD (Var x) = return x+  showHD (Var x) = return x  instance ShowHD TT where-    showHD TT = return "true"+  showHD TT = return "true"  instance ShowHD FF where-    showHD FF = return "false"+  showHD FF = return "false"  instance ShowHD Atom where-    showHD (Atom p t) = do-      ts <- mapM pshow t-      return $ p ++ "(" ++ concat (intersperse ", " ts) ++ ")"+  showHD (Atom p t) = do ts <- mapM unK t+                         return $ p ++ "(" ++ intercalate ", " ts ++ ")"  instance ShowHD NAtom where-    showHD (NAtom p t) = do-      ts <- mapM pshow t-      return $ "not " ++ p ++ "(" ++ concat (intersperse ", " ts) ++ ")"+  showHD (NAtom p t) = do ts <- mapM unK t+                          return $ "not " ++ p ++ "(" ++ intercalate ", " ts ++ ")"  instance ShowHD Not where-    showHD (Not f) = liftM (\x -> "not (" ++ x ++ ")") (pshow f)+  showHD (Not (K f)) = liftM (\x -> "not (" ++ x ++ ")") f  instance ShowHD Or where-    showHD (Or f1 f2) =-        liftM2 (\x y -> "(" ++ x ++ ") or (" ++ y ++ ")") (pshow f1) (pshow f2)+  showHD (Or (K f1) (K f2)) =+      liftM2 (\x y -> "(" ++ x ++ ") or (" ++ y ++ ")") f1 f2  instance ShowHD And where-    showHD (And f1 f2) =-        liftM2 (\x y -> "(" ++ x ++ ") and (" ++ y ++ ")") (pshow f1) (pshow f2)+  showHD (And (K f1) (K f2)) =+      liftM2 (\x y -> "(" ++ x ++ ") and (" ++ y ++ ")") f1 f2  instance ShowHD Impl where-    showHD (Impl f1 f2) =-        liftM2 (\x y -> "(" ++ x ++ ") -> (" ++ y ++ ")") (pshow f1) (pshow f2)+  showHD (Impl (K f1) (K f2)) =+      liftM2 (\x y -> "(" ++ x ++ ") -> (" ++ y ++ ")") f1 f2  instance ShowHD Exists where-    showHD (Exists f) = do x <- genVar-                           x' <- pshow x-                           b <- pshow $ f x-                           return $ "exists " ++ x' ++ ". " ++ b+  showHD (Exists f) =+      withName (\x -> do b <- unK (f x)+                         return $ "exists " ++ show x ++ ". " ++ b)  instance ShowHD Forall where-    showHD (Forall f) = do x <- genVar-                           x' <- pshow x-                           b <- pshow $ f x-                           return $ "forall " ++ x' ++ ". " ++ b+  showHD (Forall f) =+      withName (\x -> do b <- unK (f x)+                         return $ "forall " ++ show x ++ ". " ++ b)  -------------------------------------------------------------------------------- -- Stage 0 -------------------------------------------------------------------------------- -type Input = Const :+: TT :+: FF :+: Atom :+: Not :+: Or :+: And :+:-             Impl :+: Exists :+: Forall+type Input = Const :+:+             TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Impl :+:+             Exists :+: Forall  foodFact :: Term Input TFormula-foodFact =-    (iExists $ \p -> iAtom "Person" [Place p] `iAnd`-                     (iForall $ \f -> iAtom "Food" [Place f] `iImpl`-                                      iAtom "Eats" [Place p,Place f])) `iImpl`-    iNot (iExists $ \f -> iAtom "Food" [Place f] `iAnd`-                          iNot (iExists $ \p -> iAtom "Person" [Place p] `iAnd`-                                                iAtom "Eats" [Place p,Place f]))+foodFact = Term $+  iExists (\p -> iAtom "Person" [p] `iAnd`+                 iForall (\f -> iAtom "Food" [f] `iImpl`+                                iAtom "Eats" [p,f])) `iImpl`+  iNot (iExists $ \f -> iAtom "Food" [f] `iAnd`+                        iNot (iExists $ \p -> iAtom "Person" [p] `iAnd`+                                              iAtom "Eats" [p,f]))  ----------------------------------------------------------------------------------- Stage 1+-- Stage 1: Eliminate Implications -------------------------------------------------------------------------------- -type Stage1 = Const :+: TT :+: FF :+: Atom :+: Not :+: Or :+: And :+:-              Exists :+: Forall+type Stage1 = Const :+:+              TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Exists :+: Forall -class ElimImp f where-    elimImpHom :: Hom f Stage1+class HDifunctor f => ElimImp f where+  elimImpHom :: Hom f Stage1  $(derive [liftSum] [''ElimImp]) -instance (f :<: Stage1) => ElimImp f where-    elimImpHom = simpCxt . inj+elimImp :: Term Input :-> Term Stage1+elimImp (Term t) = Term (appHom elimImpHom t) -instance ElimImp Impl where-    elimImpHom (Impl f1 f2) = iNot (Hole f1) `iOr` (Hole f2)+instance (HDifunctor f, f :<: Stage1) => ElimImp f where+  elimImpHom = simpCxt . inj -elimImp :: Term Input :-> Term Stage1-elimImp = appHom elimImpHom+instance ElimImp Impl where+  elimImpHom (Impl f1 f2) = iNot (Hole f1) `iOr` (Hole f2)  foodFact1 :: Term Stage1 TFormula foodFact1 = elimImp foodFact  ----------------------------------------------------------------------------------- Stage 2+-- Stage 2: Move Negation Inwards -------------------------------------------------------------------------------- -type Stage2 = Const :+: TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+:-              Exists :+: Forall+type Stage2 = Const :+:+              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Exists :+: Forall -class Dualize f where-    dualizeHom :: Hom f Stage2+class HDifunctor f => Dualize f where+  dualizeHom :: f a (Cxt h Stage2 a b) :-> Cxt h Stage2 a b  $(derive [liftSum] [''Dualize]) +dualize :: Trm Stage2 a :-> Trm Stage2 a+dualize = appHom (dualizeHom . hfmap Hole)+ instance Dualize Const where-    dualizeHom (Const f t) = iConst f $ map Hole t+  dualizeHom (Const f t) = iConst f t  instance Dualize TT where-    dualizeHom TT = iFF+  dualizeHom TT = iFF  instance Dualize FF where-    dualizeHom FF = iTT+  dualizeHom FF = iTT  instance Dualize Atom where-    dualizeHom (Atom p t) = iNAtom p $ map Hole t+  dualizeHom (Atom p t) = iNAtom p t  instance Dualize NAtom where-    dualizeHom (NAtom p t) = iAtom p $ map Hole t+  dualizeHom (NAtom p t) = iAtom p t  instance Dualize Or where-    dualizeHom (Or f1 f2) = Hole f1 `iAnd` Hole f2+  dualizeHom (Or f1 f2) = f1 `iAnd` f2  instance Dualize And where-    dualizeHom (And f1 f2) = Hole f1 `iOr` Hole f2+  dualizeHom (And f1 f2) = f1 `iOr` f2  instance Dualize Exists where-    dualizeHom (Exists f) = iForall (Hole . f)+  dualizeHom (Exists f) = inject $ Forall f  instance Dualize Forall where-    dualizeHom (Forall f) = iExists (Hole . f)--dualize :: Term Stage2 :-> Term Stage2-dualize = appHom dualizeHom+  dualizeHom (Forall f) = inject $ Exists f  class PushNot f where-    pushNotAlg :: Alg f (Term Stage2)+  pushNotAlg :: Alg f (Trm Stage2 a)  $(derive [liftSum] [''PushNot]) -instance PushNot Const where-    pushNotAlg (Const f t) = iConst f t--instance PushNot TT where-    pushNotAlg TT = iTT--instance PushNot FF where-    pushNotAlg FF = iFF+pushNotInwards :: Term Stage1 :-> Term Stage2+pushNotInwards t = Term (cata pushNotAlg t) -instance PushNot Atom where-    pushNotAlg (Atom p t) = iAtom p t+instance (HDifunctor f, f :<: Stage2) => PushNot f where+  pushNotAlg = inject . hdimap MP.Var id -- default  instance PushNot Not where-    pushNotAlg (Not f) = dualize f--instance PushNot Or where-    pushNotAlg (Or f1 f2) = f1 `iOr` f2--instance PushNot And where-    pushNotAlg (And f1 f2) = f1 `iAnd` f2--instance PushNot Exists where-    pushNotAlg (Exists f) = iExists (f . Place)--instance PushNot Forall where-    pushNotAlg (Forall f) = iForall (f . Place)--pushNotInwards :: Term Stage1 :-> Term Stage2-pushNotInwards = cata pushNotAlg+  pushNotAlg (Not f) = dualize f  foodFact2 :: Term Stage2 TFormula foodFact2 = pushNotInwards foodFact1  ----------------------------------------------------------------------------------- Stage 4+-- Stage 4: Skolemization -------------------------------------------------------------------------------- -type Stage4 = Const :+: TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Forall+type Stage4 = Const :+:+              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Forall  type Unique = Int data UniqueSupply = UniqueSupply Unique UniqueSupply UniqueSupply@@ -267,186 +243,194 @@ getUnique (UniqueSupply n l _) = (n,l)  type Supply = State UniqueSupply-type S = ReaderT [Term Stage4 TTerm] Supply+type S a = ReaderT [Trm Stage4 a TTerm] Supply -evalS :: S a -> [Term Stage4 TTerm] -> UniqueSupply -> a-evalS m env s = evalState (runReaderT m env) s+evalS :: S a b -> [Trm Stage4 a TTerm] -> UniqueSupply -> b+evalS m env = evalState (runReaderT m env) -fresh :: S Int+fresh :: S a Int fresh = do supply <- get            let (uniq,rest) = getUnique supply            put rest            return uniq -freshes :: S UniqueSupply+freshes :: S a UniqueSupply freshes = do supply <- get              let (l,r) = splitUniqueSupply supply              put r              return l  class Skolem f where-    skolemAlg :: AlgM' S f (Term Stage4)+  skolemAlg :: AlgM' (S a) f (Trm Stage4 a)  $(derive [liftSum] [''Skolem]) +skolemize :: Term Stage2 :-> Term Stage4+skolemize f = Term (evalState (runReaderT (cataM' skolemAlg f) [])+                              initialUniqueSupply)+ instance Skolem Const where-    skolemAlg (Const f t) = liftM (iConst f) $ mapM getCompose t+  skolemAlg (Const f t) = liftM (iConst f) $ mapM getCompose t  instance Skolem TT where-    skolemAlg TT = return iTT+  skolemAlg TT = return iTT  instance Skolem FF where-    skolemAlg FF = return iFF+  skolemAlg FF = return iFF  instance Skolem Atom where-    skolemAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t+  skolemAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t  instance Skolem NAtom where-    skolemAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t+  skolemAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t  instance Skolem Or where-    skolemAlg (Or f1 f2) = liftM2 iOr (getCompose f1) (getCompose f2)+  skolemAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2  instance Skolem And where-    skolemAlg (And f1 f2) = liftM2 iAnd (getCompose f1) (getCompose f2)+  skolemAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2  instance Skolem Forall where-    skolemAlg (Forall f) = do-      supply <- freshes-      xs <- ask-      return $ iForall $ \x -> evalS (getCompose $ f (Place x))-                                     (Place x : xs)-                                     supply+  skolemAlg (Forall f) = do+    supply <- freshes+    xs <- ask+    return $ iForall $ \x -> evalS (getCompose $ f x) (x : xs) supply  instance Skolem Exists where-    skolemAlg (Exists f) = do uniq <- fresh-                              xs <- ask-                              getCompose $ f (iConst ("Skol" ++ show uniq) xs)--skolemize :: Term Stage2 :-> Term Stage4-skolemize f = evalState (runReaderT (cataM' skolemAlg f) []) initialUniqueSupply+  skolemAlg (Exists f) = do+    uniq <- fresh+    xs <- ask+    getCompose $ f (iConst ("Skol" ++ show uniq) xs)  foodFact4 :: Term Stage4 TFormula foodFact4 = skolemize foodFact2  ----------------------------------------------------------------------------------- Stage 5+-- Stage 5: Prenex Normal Form -------------------------------------------------------------------------------- -type Stage5 = Const :+: Var :+: TT :+: FF :+: Atom :+: NAtom :+: Or :+: And+type Stage5 = Const :+: Var :+:+              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And  class Prenex f where-    prenexAlg :: AlgM' S f (Term Stage5)+  prenexAlg :: AlgM' (S a) f (Trm Stage5 a)  $(derive [liftSum] [''Prenex]) +prenex :: Term Stage4 :-> Term Stage5+prenex f = Term (evalState (runReaderT (cataM' prenexAlg f) [])+                           initialUniqueSupply)+ instance Prenex Const where-    prenexAlg (Const f t) = liftM (iConst f) $ mapM getCompose t+  prenexAlg (Const f t) = liftM (iConst f) $ mapM getCompose t  instance Prenex TT where-    prenexAlg TT = return iTT+  prenexAlg TT = return iTT  instance Prenex FF where-    prenexAlg FF = return iFF+  prenexAlg FF = return iFF  instance Prenex Atom where-    prenexAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t+  prenexAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t  instance Prenex NAtom where-    prenexAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t+  prenexAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t  instance Prenex Or where-    prenexAlg (Or f1 f2) = liftM2 iOr (getCompose f1) (getCompose f2)+  prenexAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2  instance Prenex And where-    prenexAlg (And f1 f2) = liftM2 iAnd (getCompose f1) (getCompose f2)+  prenexAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2  instance Prenex Forall where-    prenexAlg (Forall f) = do uniq <- fresh-                              getCompose $ f (iVar ("x" ++ show uniq))--prenex :: Term Stage4 :-> Term Stage5-prenex f = evalState (runReaderT (cataM' prenexAlg f) []) initialUniqueSupply+  prenexAlg (Forall f) = do uniq <- fresh+                            getCompose $ f (iVar ('x' : show uniq))  foodFact5 :: Term Stage5 TFormula foodFact5 = prenex foodFact4  ----------------------------------------------------------------------------------- Stage 6+-- Stage 6: Conjunctive Normal Form -------------------------------------------------------------------------------- -type Literal = Term (Const :+: Var :+: Atom :+: NAtom)-newtype Clause i = Clause {unClause :: [Literal i]} -- implicit disjunction-newtype CNF i = CNF {unCNF :: [Clause i]} -- implicit conjunction+type Literal a     = Trm (Const :+: Var :+: Atom :+: NAtom) a+newtype Clause a i = Clause {unClause :: [Literal a i]} -- implicit disjunction+newtype CNF a i    = CNF {unCNF :: [Clause a i]}        -- implicit conjunction -instance Show (Clause i) where-    show c = concat $ intersperse " or " $ map show $ unClause c+instance (HDifunctor f, ShowHD f) => Show (Trm f Name i) where+  show = evalFreshM . showHD . toCxt -instance Show (CNF i) where-    show c = concat $ intersperse "\n" $ map show $ unCNF c+instance Show (Clause Name i) where+  show c = intercalate " or " $ map show $ unClause c +instance Show (CNF Name i) where+  show c = intercalate "\n" $ map show $ unCNF c+ class ToCNF f where-    cnfAlg :: Alg f CNF+  cnfAlg :: f (CNF a) (CNF a) i -> [Clause a i]  $(derive [liftSum] [''ToCNF]) +cnf :: Term Stage5 :-> CNF a+cnf = cata (CNF . cnfAlg)+ instance ToCNF Const where-    cnfAlg (Const f t) = CNF [Clause [iConst f (map (head . unClause . head . unCNF) t)]]+  cnfAlg (Const f t) =+      [Clause [iConst f (map (head . unClause . head . unCNF) t)]]  instance ToCNF Var where-    cnfAlg (Var x) = CNF [Clause [iVar x]]+  cnfAlg (Var x) = [Clause [iVar x]]  instance ToCNF TT where-    cnfAlg TT = CNF []+  cnfAlg TT = []  instance ToCNF FF where-    cnfAlg FF = CNF [Clause []]+  cnfAlg FF = [Clause []]  instance ToCNF Atom where-    cnfAlg (Atom p t) = CNF [Clause [iAtom p (map (head . unClause . head . unCNF) t)]]+  cnfAlg (Atom p t) =+      [Clause [iAtom p (map (head . unClause . head . unCNF) t)]]  instance ToCNF NAtom where-    cnfAlg (NAtom p t) = CNF [Clause [iNAtom p (map (head . unClause . head . unCNF) t)]]+  cnfAlg (NAtom p t) =+      [Clause [iNAtom p (map (head . unClause . head . unCNF) t)]]  instance ToCNF And where-    cnfAlg (And f1 f2) = CNF $ unCNF f1 ++ unCNF f2+  cnfAlg (And f1 f2) = unCNF f1 ++ unCNF f2  instance ToCNF Or where-    cnfAlg (Or f1 f2) = CNF [Clause (x ++ y) | Clause x <- unCNF f1, Clause y <- unCNF f2]--cnf :: Term Stage5 :-> CNF-cnf = cata cnfAlg+  cnfAlg (Or f1 f2) =+      [Clause (x ++ y) | Clause x <- unCNF f1, Clause y <- unCNF f2] -foodFact6 :: CNF TFormula+foodFact6 :: CNF a TFormula foodFact6 = cnf foodFact5  ----------------------------------------------------------------------------------- Stage 7+-- Stage 7: Implicative Normal Form -------------------------------------------------------------------------------- -type T = Const :+: Var :+: Atom :+: NAtom-newtype IClause i = IClause ([Term T i], -- implicit conjunction-                             [Term T i]) -- implicit disjunction-newtype INF i = INF [IClause i] -- implicit conjunction+type T              = Const :+: Var :+: Atom :+: NAtom+newtype IClause a i = IClause ([Trm T a i], -- implicit conjunction+                               [Trm T a i]) -- implicit disjunction+newtype INF a i     = INF [IClause a i]     -- implicit conjunction -instance Show (IClause i) where-    show (IClause (cs,ds)) =-        let cs' = concat $ intersperse " and " $ map show cs-            ds' = concat $ intersperse " or " $ map show ds-        in "(" ++ cs' ++ ") -> (" ++ ds' ++ ")"+instance Show (IClause Name i) where+  show (IClause (cs,ds)) = let cs' = intercalate " and " $ map show cs+                               ds' = intercalate " or " $ map show ds+                           in "(" ++ cs' ++ ") -> (" ++ ds' ++ ")" -instance Show (INF i) where-    show (INF fs) = concat $ intersperse "\n" $ map show fs+instance Show (INF Name i) where+  show (INF fs) = intercalate "\n" $ map show fs -inf :: CNF TFormula -> INF TFormula+inf :: CNF a TFormula -> INF a TFormula inf (CNF f) = INF $ map (toImpl . unClause) f-    where toImpl :: [Literal TFormula] -> IClause TFormula+    where toImpl :: [Literal a TFormula] -> IClause a TFormula           toImpl disj = IClause ([iAtom p t | NAtom p t <- mapMaybe proj1 disj],                                  [inject t | t <- mapMaybe proj2 disj])-          proj1 :: NatM Maybe (Term T) (NAtom Any (Term T))+          proj1 :: NatM Maybe (Trm T a) (NAtom a (Trm T a))           proj1 = project-          proj2 :: NatM Maybe (Term T) (Atom Any (Term T))+          proj2 :: NatM Maybe (Trm T a) (Atom a (Trm T a))           proj2 = project -foodFact7 :: INF TFormula+foodFact7 :: INF a TFormula foodFact7 = inf foodFact6

@@ -0,0 +1,106 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances, Rank2Types, GADTs, KindSignatures,+  ScopedTypeVariables, TypeFamilies #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.MultiParam.Lambda+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Tagless (monadic) interpretation of extended lambda calculus+--+--------------------------------------------------------------------------------++module Examples.MultiParam.Lambda where++import Data.Comp.MultiParam+import Data.Comp.MultiParam.Show ()+import Data.Comp.MultiParam.Equality ()+import Data.Comp.MultiParam.Derive+import Control.Monad (liftM2)+import Control.Monad.Error (MonadError, throwError)++data Lam :: (* -> *) -> (* -> *) -> * -> * where+  Lam :: (a i -> b j) -> Lam a b (i -> j)+data App :: (* -> *) -> (* -> *) -> * -> * where+  App :: b (i -> j) -> b i -> App a b j+data Const :: (* -> *) -> (* -> *) -> * -> * where+  Const :: Int -> Const a b Int+data Plus :: (* -> *) -> (* -> *) -> * -> * where+  Plus :: b Int -> b Int -> Plus a b Int+data Err :: (* -> *) -> (* -> *) -> * -> * where+  Err :: Err a b i+type Sig = Lam :+: App :+: Const :+: Plus :+: Err++$(derive [smartConstructors, makeHDifunctor, makeShowHD, makeEqHD]+         [''Lam, ''App, ''Const, ''Plus, ''Err])++-- * Tagless interpretation+class Eval f where+  evalAlg :: f I I i -> i -- I . evalAlg :: Alg f I is the actual algebra++$(derive [liftSum] [''Eval])++eval :: (HDifunctor f, Eval f) => Term f i -> i+eval = unI . cata (I . evalAlg)++instance Eval Lam where+  evalAlg (Lam f) = unI . f . I++instance Eval App where+  evalAlg (App (I f) (I x)) = f x++instance Eval Const where+  evalAlg (Const n) = n++instance Eval Plus where+  evalAlg (Plus (I x) (I y)) = x + y++instance Eval Err where+  evalAlg Err = error "error"++-- * Tagless monadic interpretation+type family Sem (m :: * -> *) i+type instance Sem m (i -> j) = Sem m i -> m (Sem m j)+type instance Sem m Int = Int++newtype M m i = M {unM :: m (Sem m i)}++class Monad m => EvalM m f where+  evalMAlg :: f (M m) (M m) i -> m (Sem m i) -- M . evalMAlg :: Alg f (M m)++$(derive [liftSum] [''EvalM])++evalM :: (Monad m, HDifunctor f, EvalM m f) => Term f i -> m (Sem m i)+evalM = unM . cata (M . evalMAlg)++instance Monad m => EvalM m Lam where+  evalMAlg (Lam f) = return $ unM . f . M . return++instance Monad m => EvalM m App where+  evalMAlg (App (M mf) (M mx)) = do f <- mf; f =<< mx+  +instance Monad m => EvalM m Const where+  evalMAlg (Const n) = return n++instance Monad m => EvalM m Plus where+  evalMAlg (Plus (M mx) (M my)) = liftM2 (+) mx my++instance MonadError String m => EvalM m Err where+  evalMAlg Err = throwError "error" -- 'throwError' rather than 'error'++e :: Term Sig Int+e = Term ((iLam $ \x -> (iLam (\y -> y `iPlus` x) `iApp` iConst 3)) `iApp` iConst 2)++v :: Either String Int+v = evalM e++e' :: Term Sig (Int -> Int)+e' = Term iErr --(iLam id)++v' :: Either String (Int -> Either String Int)+v' = evalM e'

@@ -1,109 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances,-  TypeSynonymInstances, OverlappingInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Param.DesugarEval--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Expression Evaluation------ The example illustrates how to compose a term homomorphism and an algebra,--- exemplified via a desugaring term homomorphism and an evaluation algebra.------ The example extends the example from 'Examples.Param.Eval'.--------------------------------------------------------------------------------------module Examples.Param.DesugarEval where--import Data.Comp.Param hiding (Const)-import Data.Comp.Param.Show ()-import Data.Comp.Param.Derive-import Data.Comp.Param.Desugar---- Signatures for values and operators-data Const a e = Const Int-data Lam a e = Lam (a -> e) -- Note: not e -> e-data App a e = App e e-data Op a e = Add e e | Mult e e-data Fun a e = Fun (e -> e) -- Note: not a -> e-data IfThenElse a e = IfThenElse e e e---- Signature for syntactic sugar (negation, let expressions, Y combinator)-data Sug a e = Neg e | Let e (a -> e) | Fix---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op :+: IfThenElse--- Signature for the simple expression language with syntactic sugar-type Sig' = Sug :+: Sig--- Signature for values. Note the use of 'Fun' rather than 'Lam' (!)-type Value = Const :+: Fun--- Signature for ground values.-type GValue = Const---- Derive boilerplate code using Template Haskell-$(derive [makeDifunctor, makeEqD, makeShowD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op, ''IfThenElse, ''Sug])-$(derive [makeDitraversable]-         [''Const, ''App, ''Op])--instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, Difunctor f)-  => Desugar Sug f where-  desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = inject (Lam y) `iApp` x-  desugHom' Fix       = iLam $ \f -> (iLam $ \x -> f `iApp` (x `iApp` x)) `iApp`-                                     (iLam $ \x -> f `iApp` (x `iApp` x))---- Term evaluation algebra-class Eval f v where-  evalAlg :: Alg f (Term v)--$(derive [liftSum] [''Eval])---- Compose the evaluation algebra and the desugaring homomorphism to an algebra-eval :: Term Sig -> Term Value-eval = cata evalAlg--evalDesug :: Term Sig' -> Term Value-evalDesug = eval . desugar--instance (Const :<: v) => Eval Const v where-  evalAlg (Const n) = iConst n--instance (Const :<: v) => Eval Op v where-  evalAlg (Add x y)  = iConst $ (projC x) + (projC y)-  evalAlg (Mult x y) = iConst $ (projC x) * (projC y)--instance (Fun :<: v) => Eval App v where-  evalAlg (App x y) = (projF x) y--instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = inject $ Fun f--instance (Const :<: v) => Eval IfThenElse v where-  evalAlg (IfThenElse c v1 v2) = if projC c /= 0 then v1 else v2--projC :: (Const :<: v) => Term v -> Int-projC v = case project v of Just (Const n) -> n--projF :: (Fun :<: v) => Term v -> Term v -> Term v-projF v = case project v of Just (Fun f) -> f---- |Evaluation of expressions to ground values.-evalG :: Term Sig' -> Maybe (Term GValue)-evalG = deepProject . evalDesug---- Example: evalEx = Just (iConst 720)-evalEx :: Maybe (Term GValue)-evalEx = evalG $ fact `iApp` iConst 6--fact :: Term Sig'-fact = iFix `iApp`-       (iLam $ \f ->-          iLam $ \n ->-              iIfThenElse n  (n `iMult` (f `iApp` (n `iAdd` iConst (-1)))) (iConst 1))

@@ -1,69 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances,-  TypeSynonymInstances, OverlappingInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Param.DesugarPos--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Desugaring + Propagation of Annotations------ The example illustrates how to compose a term homomorphism and an algebra,--- exemplified via a desugaring term homomorphism and an evaluation algebra.--------------------------------------------------------------------------------------module Examples.Param.DesugarPos where--import Data.Comp.Param hiding (Const)-import Data.Comp.Param.Show ()-import Data.Comp.Param.Derive-import Data.Comp.Param.Desugar---- Signatures for values and operators-data Const a e = Const Int-data Lam a e = Lam (a -> e) -- Note: not e -> e-data App a e = App e e-data Op a e = Add e e | Mult e e---- Signature for syntactic sugar (negation, let expressions, Y combinator)-data Sug a e = Neg e | Let e (a -> e) | Fix---- Source position information (line number, column number)-data Pos = Pos Int Int-           deriving (Show, Eq)---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op-type SigP = Const :&: Pos :+: Lam :&: Pos :+: App :&: Pos :+: Op :&: Pos---- Signature for the simple expression language, extended with syntactic sugar-type Sig' = Sug :+: Sug-type SigP' = Sug :&: Pos :+: SigP---- Derive boilerplate code using Template Haskell-$(derive [makeDifunctor, makeEqD, makeShowD,-          smartConstructors, smartAConstructors]-         [''Const, ''Lam, ''App, ''Op, ''Sug])--instance (Op :<: f, Const :<: f, Lam :<: f, App :<: f, Difunctor f)-  => Desugar Sug f where-  desugHom' (Neg x)   = iConst (-1) `iMult` x-  desugHom' (Let x y) = inject (Lam y) `iApp` x-  desugHom' Fix       = iLam $ \f -> (iLam $ \x -> f `iApp` (x `iApp` x)) `iApp`-                                     (iLam $ \x -> f `iApp` (x `iApp` x))---- Example: desugPEx == iAApp (Pos 1 0)---          (iALam (Pos 1 0) id)---          (iALam (Pos 1 1) $ \f ->---               iAApp (Pos 1 1)---                     (iALam (Pos 1 1) $ \x ->---                          iAApp (Pos 1 1) f (iAApp (Pos 1 1) x x))---                     (iALam (Pos 1 1) $ \x ->---                          iAApp (Pos 1 1) f (iAApp (Pos 1 1) x  x)))-desugPEx :: Term SigP-desugPEx = desugarA (iALet (Pos 1 0) (iAFix (Pos 1 1)) id :: Term SigP')

@@ -1,84 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Param.Eval--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Expression Evaluation------ The example illustrates how to use parametric compositional data types to--- implement a small expression language, with a language of values, and--- an evaluation function mapping expressions to values. The example--- demonstrates how (parametric) abstractions are mapped to general functions,--- from values to values, and how it is possible to project a general value--- (with functions) back into ground values, that can again be analysed.--------------------------------------------------------------------------------------module Examples.Param.Eval where--import Data.Comp.Param hiding (Const)-import Data.Comp.Param.Show ()-import Data.Comp.Param.Derive---- Signatures for values and operators-data Const a e = Const Int-data Lam a e = Lam (a -> e) -- Note: not e -> e-data App a e = App e e-data Op a e = Add e e | Mult e e-data Fun a e = Fun (e -> e) -- Note: not a -> e---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op--- Signature for values. Note the use of 'Fun' rather than 'Lam' (!)-type Value = Const :+: Fun--- Signature for ground values.-type GValue = Const---- Derive boilerplate code using Template Haskell-$(derive [makeDifunctor, makeEqD, makeShowD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op])-$(derive [makeDitraversable]-         [''Const, ''App, ''Op])---- Term evaluation algebra-class Eval f v where-  evalAlg :: Alg f (Term v)--$(derive [liftSum] [''Eval])---- Lift the evaluation algebra to a catamorphism-eval :: (Difunctor f, Eval f v) => Term f -> Term v-eval = cata evalAlg--instance (Const :<: v) => Eval Const v where-  evalAlg (Const n) = iConst n--instance (Const :<: v) => Eval Op v where-  evalAlg (Add x y)  = iConst $ (projC x) + (projC y)-  evalAlg (Mult x y) = iConst $ (projC x) * (projC y)--instance (Fun :<: v) => Eval App v where-  evalAlg (App x y) = (projF x) y--instance (Fun :<: v) => Eval Lam v where-  evalAlg (Lam f) = inject $ Fun f--projC :: (Const :<: v) => Term v -> Int-projC v = case project v of Just (Const n) -> n--projF :: (Fun :<: v) => Term v -> Term v -> Term v-projF v = case project v of Just (Fun f) -> f---- |Evaluation of expressions to ground values.-evalG :: Term Sig -> Maybe (Term GValue)-evalG = deepProject . (eval :: Term Sig -> Term Value)---- Example: evalEx = Just (iConst 4)-evalEx :: Maybe (Term GValue)-evalEx = evalG $ (iLam $ \x -> x `iAdd` x) `iApp` iConst 2

@@ -1,78 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Param.EvalAlgM--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Monadic Expression Evaluation without PHOAS------ The example illustrates how to use parametric compositional data types to--- implement a small expression language, with a sub language of values, and a--- monadic evaluation function mapping expressions to values. The lack for PHOAS--- means that -- unlike the example in 'Examples.Param.EvalM' -- a monadic--- algebra can be used.--------------------------------------------------------------------------------------module Examples.Param.EvalAlgM where--import Data.Comp.Param-import Data.Comp.Param.Show ()-import Data.Comp.Param.Ditraversable-import Data.Comp.Param.Derive-import Control.Monad (liftM)---- Signature for values and operators-data Value a e = Const Int | Pair e e-data Op a e = Add e e | Mult e e | Fst e | Snd e---- Signature for the simple expression language-type Sig = Op :+: Value---- Derive boilerplate code using Template Haskell-$(derive [makeDifunctor, makeDitraversable,-          makeEqD, makeShowD, smartConstructors]-         [''Value, ''Op])---- Monadic term evaluation algebra-class EvalM f v where-  evalAlgM :: AlgM Maybe f (Term v)--$(derive [liftSum] [''EvalM])---- Lift the monadic evaluation algebra to a monadic catamorphism-evalM :: (Ditraversable f Maybe (Term v), EvalM f v) => Term f -> Maybe (Term v)-evalM = cataM evalAlgM--instance (Value :<: v) => EvalM Value v where-  evalAlgM (Const n) = return $ iConst n-  evalAlgM (Pair x y) = return $ iPair x y--instance (Value :<: v) => EvalM Op v where-  evalAlgM (Add x y)  = do n1 <- projC x-                           n2 <- projC y-                           return $ iConst $ n1 + n2-  evalAlgM (Mult x y) = do n1 <- projC x-                           n2 <- projC y-                           return $ iConst $ n1 * n2-  evalAlgM (Fst v)    = liftM fst $ projP v-  evalAlgM (Snd v)    = liftM snd $ projP v--projC :: (Value :<: v) => Term v -> Maybe Int-projC v = case project v of-            Just (Const n) -> return n-            _ -> Nothing--projP :: (Value :<: v) => Term v -> Maybe (Term v, Term v)-projP v = case project v of-            Just (Pair x y) -> return (x,y)-            _ -> Nothing---- Example: evalMEx = Just (iConst 5)-evalMEx :: Maybe (Term Value)-evalMEx = evalM ((iConst 1) `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)

@@ -1,99 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Param.EvalM--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Monadic Expression Evaluation------ The example illustrates how to use parametric compositional data types to--- implement a small expression language, with a language of values, and--- a monadic evaluation function mapping expressions to values. The example--- demonstrates how (parametric) abstractions are mapped to general functions,--- from values to /monadic/ values, and how it is possible to project a general--- value (with functions) back into ground values, that can again be analysed.--------------------------------------------------------------------------------------module Examples.Param.EvalM where--import Data.Comp.Param hiding (Const)-import Data.Comp.Param.Show ()-import Data.Comp.Param.Derive-import Control.Monad ((<=<))---- Signatures for values and operators-data Const a e = Const Int-data Lam a e = Lam (a -> e) -- Note: not e -> e-data App a e = App e e-data Op a e = Add e e | Mult e e-data FunM m a e = FunM (e -> m e) -- Note: not a -> m e---- Signature for the simple expression language-type Sig = Const :+: Lam :+: App :+: Op--- Signature for values. Note the use of 'FunM' rather than 'Lam' (!)-type Value = Const :+: FunM Maybe--- Signature for ground values.-type GValue = Const---- Derive boilerplate code using Template Haskell-$(derive [makeDifunctor, makeEqD, makeShowD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op])-$(derive [makeDitraversable]-         [''Const, ''App, ''Op])---- Term evaluation algebra. Note that we cannot use @AlgM Maybe f (Term v)@--- because that would force @FunM@ to have the type @e -> e@ rather than--- @e -> m e@. The latter is needed because the input to a @Lam@ (which is--- evaluated to a @Fun@) will determine whether or not an error should be--- returned. Example: @(\x -> x x) 42@ will produce an error because the--- abstraction is applied to a non-functional, whereas @(\x -> x x)(\y -> y)@--- will not.-class EvalM f v where-  evalAlgM :: Alg f (Maybe (Term v))--$(derive [liftSum] [''EvalM])---- Lift the evaluation algebra to a catamorphism-evalM :: (Difunctor f, EvalM f v) => Term f -> Maybe (Term v)-evalM = cata evalAlgM--instance (Const :<: v) => EvalM Const v where-  evalAlgM (Const n) = return $ iConst n--instance (Const :<: v) => EvalM Op v where-  evalAlgM (Add mx my)  = do x <- projC =<< mx-                             y <- projC =<< my-                             return $ iConst $ x + y-  evalAlgM (Mult mx my) = do x <- projC =<< mx-                             y <- projC =<< my-                             return $ iConst $ x * y--instance (FunM Maybe :<: v) => EvalM App v where-  evalAlgM (App mx my) = do f <- projF =<< mx-                            f =<< my--instance (FunM Maybe :<: v) => EvalM Lam v where-  evalAlgM (Lam f) = return $ inject $ FunM $ f . return--projC :: (Const :<: v) => Term v -> Maybe Int-projC v = do Const n <- project v-             return n--projF :: (FunM Maybe :<: v) => Term v -> Maybe (Term v -> Maybe (Term v))-projF v = do FunM f <- project v-             return f---- |Evaluation of expressions to ground values.-evalMG :: Term Sig -> Maybe (Term GValue)-evalMG = deepProject <=< (evalM :: Term Sig -> Maybe (Term Value))---- Example: evalEx = Just (iConst 12) (3 * (2 + 2) = 12)-evalMEx :: Maybe (Term GValue)-evalMEx = evalMG $ (iLam $ \x -> iLam $ \y -> y `iMult` (x `iAdd` x))-                   `iApp` iConst 2 `iApp` iConst 3

@@ -0,0 +1,77 @@+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, TemplateHaskell,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Param.Graph+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Graph representation. The example is taken from (Fegaras and Sheard,+-- Revisiting Catamorphisms over Datatypes with Embedded Functions, '96).+--+--------------------------------------------------------------------------------++module Examples.Param.Graph where++import Data.Comp.Param+import Data.Comp.Param.Derive+import Data.Comp.Param.Show ()+import Data.Comp.Param.Equality ()++data N p a b = N p [b] -- Node+data R a b = R (a -> b) -- Recursion+data S a b = S (a -> b) b -- Sharing++$(derive [makeDifunctor, makeShowD, makeEqD, makeOrdD, smartConstructors]+         [''N, ''R, ''S])+$(derive [makeDitraversable] [''N])++type Graph p = Term (N p :+: R :+: S)++class FlatG f p where+  flatGAlg :: Alg f [p]++$(derive [liftSum] [''FlatG])++flatG :: (Difunctor f, FlatG f p) => Term f -> [p]+flatG = cata flatGAlg++instance FlatG (N p) p where+  flatGAlg (N p ps) = p : concat ps++instance FlatG R p where+  flatGAlg (R f) = f []++instance FlatG S p where+  flatGAlg (S f g) = f g++class SumG f where+  sumGAlg :: Alg f Int++$(derive [liftSum] [''SumG])++sumG :: (Difunctor f, SumG f) => Term f -> Int+sumG = cata sumGAlg++instance SumG (N Int) where+  sumGAlg (N p ps) = p + sum ps++instance SumG R where+  sumGAlg (R f) = f 0++instance SumG S where+  sumGAlg (S f g) = f g++g :: Graph Int+g = Term $ iR (\x -> iS (\z -> iN (0 :: Int) [z,iR $ \y -> iN (1 :: Int) [y,z]])+                        (iN (2 :: Int) [x]))++f :: [Int]+f = flatG g++n :: Int+n = sumG g

@@ -0,0 +1,131 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances, Rank2Types, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Param.Lambda+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Lambda calculus examples+--+-- We define a pretty printer, a desugaring transformation, constant folding,+-- and call-by-value interpreter for an extended variant of the simply typed+-- lambda calculus.+--+--------------------------------------------------------------------------------++module Examples.Param.Lambda where++import Data.Comp.Param+import Data.Comp.Param.Show ()+import Data.Comp.Param.Equality ()+import Data.Comp.Param.Ordering ()+import Data.Comp.Param.Derive+import Data.Comp.Param.Desugar++data Lam a b   = Lam (a -> b)+data App a b   = App b b+data Const a b = Const Int+data Plus a b  = Plus b b+data Let a b   = Let b (a -> b)+data Err a b   = Err++type Sig       = Lam :+: App :+: Const :+: Plus :+: Let :+: Err+type Sig'      = Lam :+: App :+: Const :+: Plus :+: Err++$(derive [smartConstructors, makeDifunctor, makeShowD, makeEqD, makeOrdD]+         [''Lam, ''App, ''Const, ''Plus, ''Let, ''Err])++-- * Pretty printing+data Stream a = Cons a (Stream a)++class Pretty f where+  prettyAlg :: Alg f (Stream String -> String)++$(derive [liftSum] [''Pretty])++pretty :: (Difunctor f, Pretty f) => Term f -> String+pretty t = cata prettyAlg t (nominals 1)+    where nominals n = Cons ('x' : show n) (nominals (n + 1))++instance Pretty Lam where+  prettyAlg (Lam f) (Cons x xs) = "(\\" ++ x ++ ". " ++ f (const x) xs ++ ")"++instance Pretty App where+  prettyAlg (App e1 e2) xs = "(" ++ e1 xs ++ " " ++ e2 xs ++ ")"++instance Pretty Const where+  prettyAlg (Const n) _ = show n++instance Pretty Plus where+  prettyAlg (Plus e1 e2) xs = "(" ++ e1 xs ++ " + " ++ e2 xs ++ ")"++instance Pretty Err where+  prettyAlg Err _ = "error"++instance Pretty Let where+  prettyAlg (Let e1 e2) (Cons x xs) = "let " ++ x ++ " = " ++ e1 xs ++ " in " ++ e2 (const x) xs++-- * Desugaring+instance (Difunctor f, App :<: f, Lam :<: f) => Desugar Let f where+  desugHom' (Let e1 e2) = inject (Lam e2) `iApp` e1++-- * Constant folding+class Constf f g where+  constfAlg :: forall a. Alg f (Trm g a)++$(derive [liftSum] [''Constf])++constf :: (Difunctor f, Constf f g) => Term f -> Term g+constf t = Term (cata constfAlg t)++instance (Difunctor f, f :<: g) => Constf f g where+  constfAlg = inject . dimap Var id -- default instance++instance (Plus :<: f, Const :<: f) => Constf Plus f where+  constfAlg (Plus e1 e2) = case (project e1, project e2) of+                             (Just (Const n),Just (Const m)) -> iConst (n + m)+                             _                               -> e1 `iPlus` e2++-- * Call-by-value evaluation+data Monad m => Sem m = Fun (Sem m -> m (Sem m)) | Int Int++class Monad m => Eval f m where+  evalAlg :: Alg f (m (Sem m))++$(derive [liftSum] [''Eval])++eval :: (Difunctor f, Eval f m) => Term f -> m (Sem m)+eval = cata evalAlg++instance Monad m => Eval Lam m where+  evalAlg (Lam f) = return (Fun (f . return))++instance Monad m => Eval App m where+  evalAlg (App mx my) = do x <- mx+                           case x of Fun f -> f =<< my; _ -> fail "stuck"++instance Monad m => Eval Const m where+  evalAlg (Const n) = return (Int n)++instance Monad m => Eval Plus m where+  evalAlg (Plus mx my) = do x <- mx+                            y <- my+                            case (x,y) of (Int n,Int m) -> return (Int (n + m))+                                          _             -> fail "stuck"++instance Monad m => Eval Err m where+  evalAlg Err = fail "error"++e :: Term Sig+e = Term (iLet (iConst 2) (\x -> (iLam (\y -> y `iPlus` x) `iApp` iConst 3)))++e' :: Term Sig'+e' = desugar e++evalEx :: Maybe (Sem Maybe)+evalEx = eval e'

@@ -0,0 +1,104 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+  FlexibleInstances, FlexibleContexts, UndecidableInstances,+  OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Examples.Param.Names+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- From names to parametric higher-order abstract syntax and back+--+-- The example illustrates how to convert a parse tree with explicit names into+-- an AST that uses parametric higher-order abstract syntax, and back again. The+-- example shows how we can easily convert object language binders to Haskell+-- binders, without having to worry about capture avoidance.+--+--------------------------------------------------------------------------------++module Examples.Param.Names where++import Data.Comp.Param hiding (Var)+import qualified Data.Comp.Param as P+import Data.Comp.Param.Derive+import Data.Comp.Param.Ditraversable+import Data.Comp.Param.Show ()+import Data.Maybe+import qualified Data.Map as Map+import Control.Monad.Reader++data Lam a b  = Lam (a -> b)+data App a b  = App b b+data Lit a b  = Lit Int+data Plus a b = Plus b b+type Name     = String                 -- The type of names+data NLam a b = NLam Name b+data NVar a b = NVar Name+type SigB     = App :+: Lit :+: Plus+type SigN     = NLam :+: NVar :+: SigB -- The name signature+type SigP     = Lam :+: SigB           -- The PHOAS signature++$(derive [makeDifunctor, makeShowD, makeEqD, smartConstructors]+         [''Lam, ''App, ''Lit, ''Plus, ''NLam, ''NVar])+$(derive [makeDitraversable]+         [''App, ''Lit, ''Plus, ''NLam, ''NVar])++--------------------------------------------------------------------------------+-- Names to PHOAS translation+--------------------------------------------------------------------------------++type M f a = Reader (Map.Map Name (Trm f a))++class N2PTrans f g where+  n2pAlg :: Alg f (M g a (Trm g a))++$(derive [liftSum] [''N2PTrans])++n2p :: (Difunctor f, N2PTrans f g) => Term f -> Term g+n2p t = Term $ runReader (cata n2pAlg t) Map.empty++instance (Lam :<: g) => N2PTrans NLam g where+  n2pAlg (NLam x b) = do vars <- ask+                         return $ iLam $ \y -> runReader b (Map.insert x y vars)++instance (Ditraversable f, f :<: g) => N2PTrans f g where+  n2pAlg = liftM inject . disequence . dimap (return . P.Var) id -- default++instance N2PTrans NVar g where+  n2pAlg (NVar x) = liftM fromJust (asks (Map.lookup x))++en :: Term SigN+en = Term $ iNLam "x1" $ iNLam "x2" (iNLam "x3" $ iNVar "x2") `iApp` iNVar "x1"++ep :: Term SigP+ep = n2p en++--------------------------------------------------------------------------------+-- PHOAS to names translation+--------------------------------------------------------------------------------++type M' = Reader [Name]++class P2NTrans f g where+  p2nAlg :: Alg f (M' (Trm g a))++$(derive [liftSum] [''P2NTrans])++p2n :: (Difunctor f, P2NTrans f g) => Term f -> Term g+p2n t = Term $ runReader (cata p2nAlg t) ['x' : show n | n <- [1..]]++instance (Ditraversable f, f :<: g) => P2NTrans f g where+  p2nAlg = liftM inject . disequence . dimap (return . P.Var) id -- default++instance (NLam :<: g, NVar :<: g) => P2NTrans Lam g where+  p2nAlg (Lam f) = do n:names <- ask+                      return $ iNLam n (runReader (f (return $ iNVar n)) names)++ep' :: Term SigP+ep' = Term $ iLam $ \a -> iLam (\b -> (iLam $ \a -> b)) `iApp` a++en' :: Term SigN+en' = p2n ep'

@@ -1,76 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,-  FlexibleInstances, FlexibleContexts, UndecidableInstances,-  OverlappingInstances #-}------------------------------------------------------------------------------------ |--- Module      :  Examples.Param.Parsing--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ From Parse Tree to Parametric Higher-Order Abstract Syntax------ The example illustrates how to convert a parse tree with explicit variables--- into an AST which uses parametric higher-order abstract syntax instead. The--- example shows how we can easily convert object language binders to Haskell--- binders, without having to worry about capture avoidance.--------------------------------------------------------------------------------------module Examples.Param.Parsing where--import Data.Comp.Param hiding (Const)-import Data.Comp.Param.Show ()-import Data.Comp.Param.Derive-import Data.Comp.Param.Ditraversable--import Data.Map (Map)-import qualified Data.Map as Map-import Data.Maybe (fromJust)-import Control.Monad.Reader--type VarId = String---- Signatures for values and operators-data Const a e = Const Int-data Abs a e = Abs VarId e-data Var a e = Var VarId-data Lam a e = Lam (a -> e) -- Note: not e -> e-data App a e = App e e-data Op a e = Add e e | Mult e e---- Signature for the simple expression language, parse tree-type Sig = Const :+: Abs :+: Var :+: App :+: Op--- Signature for the simple expression language, PHOAS (Lam replaces Abs + Var)-type Sig' = Const :+: Lam :+: App :+: Op---- Derive boilerplate code using Template Haskell-$(derive [makeDifunctor, makeDitraversable, makeEqD, makeShowD, smartConstructors]-         [''Const, ''Lam, ''App, ''Op, ''Abs, ''Var])--type TransM f = Reader (Map VarId (Term f))--class PHOASTrans f g where-  transAlg :: Alg f (TransM g (Term g))--$(derive [liftSum] [''PHOASTrans])---- default translation-instance (f :<: g, Ditraversable f (TransM g) Any) => PHOASTrans f g where-  transAlg x = liftM inject $ disequence $ dimap (return . Place) id x--instance (Lam :<: g) => PHOASTrans Abs g where-  transAlg (Abs x b) = do env <- ask-                          return $ iLam $ \y -> runReader b (Map.insert x y env)--instance PHOASTrans Var g where-  transAlg (Var x) = liftM fromJust $ asks $ Map.lookup x--trans :: Term Sig -> Term Sig'-trans x = runReader (cata transAlg x) Map.empty---- Example: evalEx = iLam $ \a -> iApp (iLam $ \b -> iLam $ \c -> b) a-transEx :: Term Sig'-transEx = trans $ iAbs "y" $ (iAbs "x" $ iAbs "y" $ iVar "x") `iApp` (iVar "y")

@@ -13,20 +13,15 @@ -- usage are bundled with the package in the library @examples\/Examples@. -- ---------------------------------------------------------------------------------module Data.Comp(-    module Data.Comp.Term-  , module Data.Comp.Algebra-  , module Data.Comp.Sum-  , module Data.Comp.Annotation-  , module Data.Comp.Equality-  , module Data.Comp.Ordering-  , module Data.Comp.Generic+module Data.Comp+    (+     module X     ) where -import Data.Comp.Term-import Data.Comp.Algebra-import Data.Comp.Sum-import Data.Comp.Annotation-import Data.Comp.Equality-import Data.Comp.Ordering-import Data.Comp.Generic+import Data.Comp.Term as X+import Data.Comp.Algebra as X+import Data.Comp.Sum as X+import Data.Comp.Annotation as X+import Data.Comp.Equality as X+import Data.Comp.Ordering as X+import Data.Comp.Generic as X

@@ -621,7 +621,7 @@ {-# NOINLINE [1] appSigFunHom #-} appSigFunHom f g = run where     run :: CxtFun f h-    run (Term t) = run' $ g $ t+    run (Term t) = run' $ g t     run (Hole h) = Hole h     run' :: Context g (Cxt h' f b) -> Cxt h' h b     run' (Term t) = Term $ f $ fmap run' t@@ -635,7 +635,7 @@ appAlgHomM alg hom = run     where run :: Term f -> m a           run (Term t) = hom t >>= mapM run >>= run'-          run' :: (Context g a) -> m a+          run' :: Context g a -> m a           run' (Term t) = mapM run' t >>= alg           run' (Hole x) = return x 

@@ -23,6 +23,9 @@      liftA',      stripA,      propAnn,+     propAnnQ,+     propAnnUp,+     propAnnDown,      propAnnM,      ann,      project'@@ -32,6 +35,7 @@ import Data.Comp.Sum import Data.Comp.Ops import Data.Comp.Algebra+import Data.Comp.Automata import Control.Monad  {-| Transform a function with a domain constructed from a functor to a function@@ -57,6 +61,32 @@ propAnn :: (DistAnn f p f', DistAnn g p g', Functor g)          => Hom f g -> Hom f' g' propAnn hom f' = ann p (hom f)+    where (f,p) = projectA f'+++-- | Lift a stateful term homomorphism over signatures @f@ and @g@ to+-- a stateful term homomorphism over the same signatures, but extended with+-- annotations.+propAnnQ :: (DistAnn f p f', DistAnn g p g', Functor g) +        => QHom f q g -> QHom f' q g'+propAnnQ hom f' = ann p (hom f)+    where (f,p) = projectA f'++-- | Lift a bottom-up tree transducer over signatures @f@ and @g@ to a+-- bottom-up tree transducer over the same signatures, but extended+-- with annotations.+propAnnUp :: (DistAnn f p f', DistAnn g p g', Functor g) +        => UpTrans f q g -> UpTrans f' q g'+propAnnUp trans f' = (q, ann p t)+    where (f,p) = projectA f'+          (q,t) = trans f++-- | Lift a top-down tree transducer over signatures @f@ and @g@ to a+-- top-down tree transducer over the same signatures, but extended+-- with annotations.+propAnnDown :: (DistAnn f p f', DistAnn g p g', Functor g) +        => DownTrans f q g -> DownTrans f' q g'+propAnnDown trans (q, f') = ann p (trans (q, f))     where (f,p) = projectA f'  {-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic

@@ -1,4 +1,4 @@-{-# LANGUAGE RankNTypes, FlexibleContexts, ImplicitParams, GADTs, ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes, FlexibleContexts, ImplicitParams, GADTs #-} -------------------------------------------------------------------------------- -- | -- Module      :  Data.Comp.Automata@@ -16,27 +16,92 @@ --------------------------------------------------------------------------------  module Data.Comp.Automata-    ( module Data.Comp.Automata,-      module Data.Comp.Automata.Product+    ( module Data.Comp.Automata.Product+    -- * Stateful Term Homomorphisms+    , QHom+    , below+    , above+    -- ** Bottom-Up State Propagation+    , upTrans+    , runUpHom+    , runUpHomSt+    -- ** Top-Down State Propagation+    , downTrans+    , runDownHom+    -- ** Bidirectional State Propagation+    , runQHom+    -- * Deterministic Bottom-Up Tree Transducers+    , UpTrans+    , runUpTrans+    , compUpTrans+    , compUpTransHom+    , compHomUpTrans+    , compUpTransSig+    , compSigUpTrans+    , compAlgUpTrans+    -- * Deterministic Bottom-Up Tree State Transformations+    -- ** Monolithic State+    , UpState+    , tagUpState+    , runUpState+    , prodUpState+    -- ** Modular State+    , DUpState+    , dUpState+    , upState+    , runDUpState+    , prodDUpState+    , (<*>)+    -- * Deterministic Top-Down Tree Transducers+    , DownTrans+    , runDownTrans+    , compDownTrans+    , compDownTransSig+    , compSigDownTrans+    , compDownTransHom+    , compHomDownTrans+    -- * Deterministic Top-Down Tree State Transformations+    -- ** Monolithic State+    , DownState+    , tagDownState+    , prodDownState+    -- ** Modular State+    , DDownState+    , dDownState+    , downState+    , prodDDownState+    , (>*<)+    -- * Bidirectional Tree State Transformations+    , runDState+    -- * Operators for Finite Mappings+    , (&)+    , (|->)+    , o     ) where  import Data.Comp.Zippable import Data.Comp.Automata.Product import Data.Comp.Term import Data.Comp.Algebra-import Data.Comp.Show () import Data.Map (Map) import qualified Data.Map as Map ++-- The following are operators to specify finite mappings.++ infix 1 |-> infixr 0 & +-- | left-biased union of two mappings. (&) :: Ord k => Map k v -> Map k v -> Map k v (&) = Map.union +-- | This operator constructs a singleton mapping. (|->) :: k -> a -> Map k a (|->) = Map.singleton +-- | This is the empty mapping. o :: Map k a o = Map.empty @@ -61,7 +126,18 @@ -- by a DUTA or a DDTA (or both). type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a +-- -- | This type represents (pure, i.e. stateless) homomorphism by+-- -- universally quantifying over the state type.+-- type PHom f g = forall q . QHom f q g +-- -- | This combinator runs a stateless homomorphism. (use+-- -- 'Data.Comp.Algebra.appHom' instead).+-- runPHom :: forall f g . (Functor f, Functor g) => PHom f g -> CxtFun f g+-- runPHom hom = run where+--     run :: CxtFun f g+--     run (Hole x) = Hole x+--     run (Term t) = appCxt (explicit () (const ()) hom (fmap run t))+ -- | This type represents transition functions of deterministic -- bottom-up tree transducers (DUTTs). @@ -75,9 +151,15 @@  -- | This function runs the given DUTT on the given term. -runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> (q, Term g)-runUpTrans = cata . upAlg+runUpTrans :: (Functor f, Functor g) => UpTrans f q g -> Term f -> Term g+runUpTrans trans = snd . runUpTransSt trans +-- | This function is a variant of 'runUpTrans' that additionally+-- returns the final state of the run.++runUpTransSt :: (Functor f, Functor g) => UpTrans f q g -> Term f -> (q, Term g)+runUpTransSt = cata . upAlg+ -- | This function generalises 'runUpTrans' to contexts. Therefore, -- additionally, a transition function for the holes is needed. runUpTrans' :: (Functor f, Functor g) => UpTrans f q g -> Context f (q,a) -> (q, Context g a)@@ -92,6 +174,31 @@     (q1, c1) = t1 $ fmap (\((q1,q2),a) -> (q1,(q2,a))) x     (q2, c2) = runUpTrans' t2 c1 ++-- | This function composes a DUTT with an algebra.+compAlgUpTrans :: (Functor g)+               => Alg g a -> UpTrans f q g -> Alg f (q,a)+compAlgUpTrans alg trans = fmap (cata' alg) . trans+++-- | This combinator composes a DUTT followed by a signature function.+compSigUpTrans :: (Functor g) => SigFun g h -> UpTrans f q g -> UpTrans f q h+compSigUpTrans sig trans x = (q, appSigFun sig x') where+    (q, x') = trans x++-- | This combinator composes a signature function followed by a DUTT.+compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h+compUpTransSig trans sig = trans . sig++-- | This combinator composes a DUTT followed by a homomorphism.+compHomUpTrans :: (Functor g, Functor h) => Hom g h -> UpTrans f q g -> UpTrans f q h+compHomUpTrans hom trans x = (q, appHom hom x') where+    (q, x') = trans x++-- | This combinator composes a homomorphism followed by a DUTT.+compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h+compUpTransHom trans hom x  = runUpTrans' trans . hom $ x+ -- | This type represents transition functions of deterministic -- bottom-up tree acceptors (DUTAs). type UpState f q = Alg f q@@ -121,10 +228,15 @@  -- | This function applies a given stateful term homomorphism with -- a state space propagated by the given DUTA to a term.-runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q,Term g)-runUpHom alg h = runUpTrans (upTrans alg h)+runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g+runUpHom st hom = snd . runUpHomSt st hom +-- | This is a variant of 'runUpHom' that also returns the final state+-- of the run.+runUpHomSt :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q,Term g)+runUpHomSt alg h = runUpTransSt (upTrans alg h) + -- | This type represents transition functions of generalised -- deterministic bottom-up tree acceptors (GDUTAs) which have access -- to an extended state space.@@ -178,6 +290,26 @@ compDownTrans t2 t1 ((q,p), t) = fmap (\(p, (q, a)) -> ((q,p),a)) $ runDownTrans' t2 p (t1 (q, t))  +-- | This function composes a signature function after a DDTT.+compSigDownTrans :: (Functor g) => SigFun g h -> DownTrans f q g -> DownTrans f q h+compSigDownTrans sig trans = appSigFun sig . trans++-- | This function composes a DDTT after a function.+compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h+compDownTransSig trans hom (q,t) = trans (q, hom t)+++-- | This function composes a homomorphism after a DDTT.+compHomDownTrans :: (Functor g, Functor h)+              => Hom g h -> DownTrans f q g -> DownTrans f q h+compHomDownTrans hom trans = appHom hom . trans++-- | This function composes a DDTT after a homomorphism.+compDownTransHom :: (Functor g, Functor h)+              => DownTrans g q h -> Hom f g -> DownTrans f q h+compDownTransHom trans hom (q,t) = runDownTrans' trans q (hom t)++ -- | This type represents transition functions of deterministic -- top-down tree acceptors (DDTAs). type DownState f q = forall a. Ord a => (q, f a) -> Map a q@@ -247,15 +379,21 @@           bel k = Map.findWithDefault q k res  --- | This combinator constructs the product of two GDDTA.+-- | This combinator constructs the product of two dependant top-down+-- state transformations. prodDDownState :: (p :< c, q :< c)                => DDownState f c p -> DDownState f c q -> DDownState f c (p,q) prodDDownState sp sq t = prodMap above above (sp t) (sq t) +-- | This is a synonym for 'prodDDownState'. (>*<) :: (p :< c, q :< c, Functor f)          => DDownState f c p -> DDownState f c q -> DDownState f c (p,q) (>*<) = prodDDownState ++-- | This combinator combines a bottom-up and a top-down state+-- transformations. Both state transformations can depend mutually+-- recursive on each other. runDState :: Zippable f => DUpState f (u,d) u -> DDownState f (u,d) d -> d -> Term f -> u runDState up down d (Term t) = u where         t' = fmap bel $ number t@@ -264,3 +402,20 @@             in Numbered (i, (runDState up down d' s, d'))         m = explicit (u,d) unNumbered down t'         u = explicit (u,d) unNumbered up t'++-- | This combinator runs a stateful term homomorphisms with a state+-- space produced both on a bottom-up and a top-down state+-- transformation.+runQHom :: (Zippable f, Functor g) =>+           DUpState f (u,d) u -> DDownState f (u,d) d -> +           QHom f (u,d) g ->+           d -> Term f -> (u, Term g)+runQHom up down trans d (Term t) = (u,t'') where+        t' = fmap bel $ number t+        bel (Numbered (i,s)) = +            let d' = Map.findWithDefault d (Numbered (i,undefined)) m+                (u', s') = runQHom up down trans d' s+            in Numbered (i, ((u', d'),s'))+        m = explicit (u,d) (fst . unNumbered) down t'+        u = explicit (u,d) (fst . unNumbered) up t'+        t'' = appCxt $ fmap (snd . unNumbered) $  explicit (u,d) (fst . unNumbered) trans t'

@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, IncoherentInstances, TemplateHaskell #-}+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, IncoherentInstances #-} -------------------------------------------------------------------------------- -- | -- Module      :  Data.Comp.Automata.Product.Derive@@ -39,7 +39,7 @@   ty <- genType n dir   ex <- genEx dir   up <- genUp dir-  return $ InstanceD [] (ConT (mkName ":<") `AppT` (VarT n) `AppT` ty) [ex,up]+  return $ InstanceD [] (ConT (mkName ":<") `AppT` VarT n `AppT` ty) [ex,up]  genType :: Name -> [Dir] -> Q Type genType n = gen@@ -78,4 +78,4 @@   pairT :: TypeQ -> TypeQ -> TypeQ-pairT x y = appT (appT (tupleT 2) x) y+pairT x = appT (appT (tupleT 2) x)

@@ -35,7 +35,5 @@     rnf (Hole x) = rnf x     rnf (Term x) = rnfF x -instance NFData Nothing where- $(derive [liftSum] [''NFDataF]) $(derive [makeNFDataF] [''Maybe, ''[], ''(,)])

@@ -31,6 +31,8 @@      module Data.Comp.Derive.Foldable,      -- ** Traversable      module Data.Comp.Derive.Traversable,+     -- ** HaskellStrict+     module Data.Comp.Derive.HaskellStrict,      -- ** Arbitrary      module Data.Comp.Derive.Arbitrary,      NFData(..),@@ -47,6 +49,7 @@  import Control.DeepSeq (NFData(..)) import Data.Comp.Derive.Utils (derive)+import Data.Comp.Derive.HaskellStrict import Data.Comp.Derive.Foldable import Data.Comp.Derive.Traversable import Data.Comp.Derive.DeepSeq

@@ -46,7 +46,7 @@ makeArbitraryF :: Name -> Q [Dec] makeArbitraryF dt = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify dt-  let argNames = (map (VarT . tyVarBndrName) (tail args))+  let argNames = map (VarT . tyVarBndrName) (tail args)       complType = foldl AppT (ConT name) argNames       preCond = map (ClassP ''Arbitrary . (: [])) argNames       classType = AppT (ConT ''ArbitraryF) complType

@@ -35,7 +35,7 @@ makeNFDataF fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let fArg = VarT . tyVarBndrName $ last args-      argNames = (map (VarT . tyVarBndrName) (init args))+      argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames       preCond = map (ClassP ''NFData . (: [])) argNames       classType = AppT (ConT ''NFDataF) complType

@@ -32,7 +32,7 @@ makeEqF :: Name -> Q [Dec] makeEqF fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname-  let argNames = (map (VarT . tyVarBndrName) (init args))+  let argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames       preCond = map (ClassP ''Eq . (: [])) argNames       classType = AppT (ConT ''EqF) complType

@@ -42,7 +42,7 @@ makeFoldable fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let fArg = VarT . tyVarBndrName $ last args-      argNames = (map (VarT . tyVarBndrName) (init args))+      argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames       classType = AppT (ConT ''Foldable) complType   constrs' <- mapM (mkPatAndVars  . isFarg fArg <=< normalConExp) constrs

@@ -0,0 +1,102 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Derive.HaskellStrict+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @HaskellStrict@.+--+--------------------------------------------------------------------------------++module Data.Comp.Derive.HaskellStrict+    (+     makeHaskellStrict+     , haskellStrict+     , haskellStrict'+    ) where++import Data.Comp.Derive.Utils+import Language.Haskell.TH+import Data.Maybe+import Data.Comp.Thunk+import Data.Comp.Sum+import Data.Traversable+import Data.Foldable hiding (any,or)+import Control.Monad hiding (mapM, sequence)+import qualified Prelude as P (foldl, foldr, mapM, all)+import Prelude hiding  (foldl, foldr,mapM, sequence)+++class HaskellStrict f where+    thunkSequence :: (Monad m) => f (TermT m g) -> m (f (TermT m g))+    thunkSequenceInject :: (Monad m, f :<: g) => f (TermT m g) -> TermT m g+    thunkSequenceInject t = thunk $ liftM inject $ thunkSequence t+    thunkSequenceInject' :: (Monad m, f :<: g) => f (TermT m g) -> TermT m g+    thunkSequenceInject' = thunkSequenceInject++haskellStrict :: (Monad m, HaskellStrict f, f :<: g) => f (TermT m g) -> TermT m g+haskellStrict = thunkSequenceInject++haskellStrict' :: (Monad m, HaskellStrict f, f :<: g) => f (TermT m g) -> TermT m g+haskellStrict' = thunkSequenceInject'++deepThunk d = iter d [|thunkSequence|]+    where iter 0 _ = [|whnf'|]+          iter 1 e = e+          iter n e = iter (n-1) ([|mapM|] `appE` e)++{-| Derive an instance of 'HaskellStrict' for a type constructor of any+  first-order kind taking at least one argument. -}+makeHaskellStrict :: Name -> Q [Dec]+makeHaskellStrict fname = do+  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname+  let fArg = VarT . tyVarBndrName $ last args+      argNames = map (VarT . tyVarBndrName) (init args)+      complType = foldl AppT (ConT name) argNames+      classType = AppT (ConT ''HaskellStrict) complType+  constrs_ <- P.mapM (liftM (isFarg fArg) . normalConStrExp) constrs+  if foldr (\ y x -> x && P.all null (snd y)) True constrs_+   then do+     sequenceDecl <- valD (varP 'thunkSequence) (normalB [|return|]) []+     injectDecl <- valD (varP 'thunkSequenceInject) (normalB [|inject|]) []+     injectDecl' <- valD (varP 'thunkSequenceInject') (normalB [|inject|]) []+     return [InstanceD [] classType [sequenceDecl, injectDecl, injectDecl']]+   else do+     (sc',matchPat,ic') <- liftM unzip3 $ P.mapM mkClauses constrs_+     xn <- newName "x"+     doThunk <- [|thunk|]+     let sequenceDecl = FunD 'thunkSequence sc'+         injectDecl = FunD 'thunkSequenceInject [Clause [VarP xn] (NormalB (doThunk `AppE` CaseE (VarE xn) matchPat)) []] +         injectDecl' = FunD 'thunkSequenceInject' ic'+     return [InstanceD [] classType [sequenceDecl, injectDecl, injectDecl']]+      where isFarg fArg (constr, args) = (constr, map (containsStr fArg) args)+            containsStr _ (NotStrict,_) = []+            containsStr fArg (IsStrict,ty) = ty `containsType'` fArg+            filterVar _ nonFarg [] x  = nonFarg x+            filterVar farg _ [depth] x = farg depth x+            filterVar _ _ _ _ = error "functor variable occurring twice in argument type"+            filterVars args varNs farg nonFarg = zipWith (filterVar farg nonFarg) args varNs+            mkCPat constr varNs = ConP constr $ map mkPat varNs+            mkPat = VarP+            mkClauses (constr, args) =+                do varNs <- newNames (length args) "x"+                   let pat = mkCPat constr varNs+                       fvars = catMaybes $ filterVars args varNs (curry Just) (const Nothing)+                       allVars = map varE varNs+                       conAp = P.foldl appE (conE constr) allVars+                       conBind (d, x) y = [| $(deepThunk d `appE` (varE x))  >>= $(lamE [varP x] y)|]+                   bodySC' <- P.foldr conBind [|return $conAp|] fvars+                   let sc' = Clause [pat] (NormalB bodySC') []+                   bodyMatch <- case fvars of+                             [] -> [|return (inject $conAp)|]+                             _ -> P.foldr conBind [|return (inject $conAp)|] fvars+                   let matchPat = Match pat (NormalB bodyMatch) []+                   bodyIC' <- case fvars of+                             [] -> [|inject $conAp|]+                             _ -> [| thunk |] `appE` P.foldr conBind [|return (inject $conAp)|] fvars+                   let ic' = Clause [pat] (NormalB bodyIC') []+                   return (sc', matchPat, ic')

@@ -32,7 +32,7 @@   let avar = mkName "a"   let xvar = mkName "x"   let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]-  sequence $ (sigD i $ genSig fvars gvar avar) : d+  sequence $ sigD i (genSig fvars gvar avar) : d     where genSig fvars gvar avar = do             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars             let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)@@ -42,7 +42,7 @@             forallT (map PlainTV $ gvar : avar : fvars)                     (sequence cxt) tp'           genDecl x n = [| case $(varE x) of-                             Inl x -> $(varE $ mkName $ "inj") x+                             Inl x -> $(varE $ mkName "inj") x                              Inr x -> $(varE $ mkName $ "inj" ++                                         if n > 2 then show (n - 1) else "") x |] injectn :: Int -> Q [Dec]@@ -52,7 +52,7 @@   let gvar = mkName "g"   let avar = mkName "a"   let d = [funD i [clause [] (normalB $ genDecl n) []]]-  sequence $ (sigD i $ genSig fvars gvar avar) : d+  sequence $ sigD i (genSig fvars gvar avar) : d     where genSig fvars gvar avar = do             let hvar = mkName "h"             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars@@ -71,7 +71,7 @@   let fvars = map (\n -> mkName $ 'f' : show n) [1..n]   let gvar = mkName "g"   let d = [funD i [clause [] (normalB $ genDecl n) []]]-  sequence $ (sigD i $ genSig fvars gvar) : d+  sequence $ sigD i (genSig fvars gvar) : d     where genSig fvars gvar = do             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars             let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)

@@ -23,32 +23,19 @@ import Data.Comp.Sum import Data.Comp.Ops ((:+:)(..)) + {-| Given the name of a type class, where the first parameter is a functor,   lift it to sums of functors. Example: @class ShowF f where ...@ is lifted   as @instance (ShowF f, ShowF g) => ShowF (f :+: g) where ... @. -} liftSum :: Name -> Q [Dec]-liftSum fname = do-  ClassI (ClassD _ name targs _ decs) _ <- abstractNewtypeQ $ reify fname-  let targs' = map tyVarBndrName $ tail targs-  let f = mkName "f"-  let g = mkName "g"-  let cxt = [ClassP name (map VarT $ f : targs'),-             ClassP name (map VarT $ g : targs')]-  let tp = ConT name `AppT` ((ConT ''(:+:) `AppT` VarT f) `AppT` VarT g)-  let complType = foldl (\a x -> a `AppT` VarT x) tp targs'-  decs' <- sequence $ concatMap decl decs-  return [InstanceD cxt complType decs']-      where decl :: Dec -> [DecQ]-            decl (SigD f _) = [funD f [clause f]]-            decl _ = []-            clause :: Name -> ClauseQ-            clause f = do x <- newName "x"-                          b <- normalB [|caseF $(varE f) $(varE f) $(varE x)|]-                          return $ Clause [VarP x] b []+liftSum = liftSumGen 'caseF ''(:+:)+                          + {-| Utility function to case on a functor sum, without exposing the internal   representation of sums. -} caseF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b+{-# INLINE caseF #-} caseF f g x = case x of                 Inl x -> f x                 Inr x -> g x

@@ -38,7 +38,7 @@ makeOrdF :: Name -> Q [Dec] makeOrdF fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname-  let argNames = (map (VarT . tyVarBndrName) (init args))+  let argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames       preCond = map (ClassP ''Ord . (: [])) argNames       classType = AppT (ConT ''OrdF) complType

@@ -36,7 +36,7 @@ makeShowF fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let fArg = VarT . tyVarBndrName $ last args-      argNames = (map (VarT . tyVarBndrName) (init args))+      argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames       preCond = map (ClassP ''Show . (: [])) argNames       classType = AppT (ConT ''ShowF) complType

@@ -42,7 +42,7 @@ makeTraversable fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let fArg = VarT . tyVarBndrName $ last args-      argNames = (map (VarT . tyVarBndrName) (init args))+      argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames       classType = AppT (ConT ''Traversable) complType   constrs' <- P.mapM (mkPatAndVars . isFarg fArg <=< normalConExp) constrs

@@ -54,6 +54,15 @@   ts' <- mapM expandSyns ts   return (n, ts') ++-- | Same as normalConExp' but retains strictness annotations.+normalConStrExp :: Con -> Q (Name,[StrictType])+normalConStrExp c = do +  let (n,ts) = normalCon c+  ts' <- mapM (\ (st,ty) -> do ty' <- expandSyns ty; return (st,ty')) ts+  return (n, ts')++ {-|   This function provides the name and the arity of the given data constructor. -}@@ -108,3 +117,70 @@  -} derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec] derive ders names = liftM concat $ sequence [der name | der <- ders, name <- names]++-- | This function lifts type class instances over sums+-- ofsignatures. To this end it assumes that it contains only methods+-- with types of the form @f t1 .. tn -> t@ where @f@ is the signature+-- that is used to construct sums. Since this function is generic it+-- assumes as its first argument the name of the function that is+-- used to lift methods over sums i.e. a function of type+--+-- @+-- (f t1 .. tn -> t) -> (g t1 .. tn -> t) -> ((f :+: g) t1 .. tn -> t)+-- @+--+-- where @:+:@ is the sum type constructor. The second argument to+-- this function is expected to be the name of that constructor. The+-- last argument is the name of the class whose instances should be+-- lifted over sums.++liftSumGen :: Name -> Name -> Name -> Q [Dec]+liftSumGen caseName sumName fname = do+  ClassI (ClassD _ name targs_ _ decs) _ <- reify fname+  let targs = map tyVarBndrName targs_+  splitM <- findSig targs decs+  case splitM of +    Nothing -> do report True $ "Class " ++ show name ++ " cannot be lifted to sums!"+                  return []+    Just (ts1_, ts2_) -> do+      let f = VarT $ mkName "f"+      let g = VarT $ mkName "g"+      let ts1 = map VarT ts1_+      let ts2 = map VarT ts2_+      let cxt = [ClassP name (ts1 ++ f : ts2),+                 ClassP name (ts1 ++ g : ts2)]+      let tp = ((ConT sumName `AppT` f) `AppT` g)+      let complType = foldl AppT (foldl AppT (ConT name) ts1 `AppT` tp) ts2+      decs' <- sequence $ concatMap decl decs+      return [InstanceD cxt complType decs']+        where decl :: Dec -> [DecQ]+              decl (SigD f _) = [funD f [clause f]]+              decl _ = []+              clause :: Name -> ClauseQ+              clause f = do x <- newName "x"+                            let b = NormalB (VarE caseName `AppE` VarE f `AppE` VarE f `AppE` VarE x)+                            return $ Clause [VarP x] b []+                          +                          +findSig :: [Name] -> [Dec] -> Q (Maybe ([Name],[Name]))+findSig targs decs = case map run decs of+                       []  -> return Nothing+                       mx:_ -> do x <- mx+                                  case x of+                                    Nothing -> return Nothing+                                    Just n -> return $ splitNames n targs+  where run :: Dec -> Q (Maybe Name)+        run (SigD _ ty) = do +          ty' <- expandSyns ty+          return $ getSig False ty'+        run _ = return Nothing+        getSig t (ForallT _ _ ty) = getSig t ty+        getSig False (AppT (AppT ArrowT ty) _) = getSig True ty+        getSig True (AppT ty _) = getSig True ty+        getSig True (VarT n) = Just n+        getSig _ _ = Nothing+        splitNames y (x:xs) +          | y == x = Just ([],xs)+          | otherwise = do (xs1,xs2) <- splitNames y xs+                           return (x:xs1,xs2)+        splitNames _ [] = Nothing

@@ -21,50 +21,40 @@ import Data.Comp.Term import Data.Comp.Sum import Data.Comp.Ops-import Data.Comp.Derive+import Data.Comp.Derive.Equality import Data.Comp.Derive.Utils- import Data.Foldable- import Control.Monad hiding (mapM_) import Prelude hiding (mapM_, all) -- -- instance (EqF f, Eq p) => EqF (f :*: p) where --    eqF (v1 :*: p1) (v2 :*: p2) = p1 == p2 && v1 `eqF` v2  {-|-  'EqF' is propagated through sums.--}--instance (EqF f, EqF g) => EqF (f :+: g) where-    eqF (Inl x) (Inl y) = eqF x y-    eqF (Inr x) (Inr y) = eqF x y-    eqF _ _ = False--{-|   From an 'EqF' functor an 'Eq' instance of the corresponding   term type can be derived. -}-instance (EqF f) => EqF (Cxt h f) where+instance (EqF f, Eq a) => Eq (Cxt h f a) where+    (==) = eqF +instance (EqF f) => EqF (Cxt h f) where     eqF (Term e1) (Term e2) = e1 `eqF` e2     eqF (Hole h1) (Hole h2) = h1 == h2     eqF _ _ = False -instance (EqF f, Eq a)  => Eq (Cxt h f a) where-    (==) = eqF--instance EqF [] where-    eqF = (==)+{-|+  'EqF' is propagated through sums.+-}+instance (EqF f, EqF g) => EqF (f :+: g) where+    eqF (Inl x) (Inl y) = eqF x y+    eqF (Inr x) (Inr y) = eqF x y+    eqF _ _ = False  {-| This function implements equality of values of type @f a@ modulo the equality of @a@ itself. If two functorial values are equal in this sense, 'eqMod' returns a 'Just' value containing a list of pairs consisting of corresponding components of the two functorial values. -}- eqMod :: (EqF f, Functor f, Foldable f) => f a -> f b -> Maybe [(a,b)] eqMod s t     | unit s `eqF` unit' t = Just args@@ -73,4 +63,4 @@           unit' = fmap (const ())           args = toList s `zip` toList t -$(derive [makeEqF] $ (''Maybe) : tupleTypes 2 10)+$(derive [makeEqF] $ [''Maybe, ''[]] ++ tupleTypes 2 10)

@@ -16,7 +16,7 @@ -------------------------------------------------------------------------------- module Data.Comp.Multi (     module Data.Comp.Multi.Term-  , module Data.Comp.Multi.Functor+  , module Data.Comp.Multi.HFunctor   , module Data.Comp.Multi.Algebra   , module Data.Comp.Multi.Sum   , module Data.Comp.Multi.Annotation@@ -24,7 +24,7 @@   , module Data.Comp.Multi.Generic     ) where -import Data.Comp.Multi.Functor+import Data.Comp.Multi.HFunctor import Data.Comp.Multi.Term import Data.Comp.Multi.Algebra import Data.Comp.Multi.Sum

@@ -87,8 +87,8 @@   import Data.Comp.Multi.Term-import Data.Comp.Multi.Functor-import Data.Comp.Multi.Traversable+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HTraversable import Data.Comp.Ops import Control.Monad 

@@ -32,7 +32,7 @@ import Data.Comp.Multi.Ops import qualified Data.Comp.Ops as O import Data.Comp.Multi.Algebra-import Data.Comp.Multi.Functor+import Data.Comp.Multi.HFunctor  import Control.Monad 

@@ -21,14 +21,16 @@       -- ** HShowF      module Data.Comp.Multi.Derive.Show,-     -- ** HEqF+     -- ** EqHF      module Data.Comp.Multi.Derive.Equality,+     -- ** OrdHF+     module Data.Comp.Multi.Derive.Ordering,      -- ** HFunctor-     module Data.Comp.Multi.Derive.Functor,+     module Data.Comp.Multi.Derive.HFunctor,      -- ** HFoldable-     module Data.Comp.Multi.Derive.Foldable,+     module Data.Comp.Multi.Derive.HFoldable,      -- ** HTraversable-     module Data.Comp.Multi.Derive.Traversable,+     module Data.Comp.Multi.Derive.HTraversable,      -- ** Smart Constructors      module Data.Comp.Multi.Derive.SmartConstructors,      -- ** Smart Constructors w/ Annotations@@ -39,10 +41,11 @@  import Data.Comp.Derive.Utils (derive) import Data.Comp.Multi.Derive.Equality+import Data.Comp.Multi.Derive.Ordering import Data.Comp.Multi.Derive.Show-import Data.Comp.Multi.Derive.Functor-import Data.Comp.Multi.Derive.Foldable-import Data.Comp.Multi.Derive.Traversable+import Data.Comp.Multi.Derive.HFunctor+import Data.Comp.Multi.Derive.HFoldable+import Data.Comp.Multi.Derive.HTraversable import Data.Comp.Multi.Derive.SmartConstructors import Data.Comp.Multi.Derive.SmartAConstructors import Data.Comp.Multi.Derive.LiftSum

@@ -8,53 +8,33 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- Automatically derive instances of @HEqF@.+-- Automatically derive instances of @EqHF@. -- -------------------------------------------------------------------------------- module Data.Comp.Multi.Derive.Equality     (-     HEqF(..),+     EqHF(..),      KEq(..),-     makeHEqF+     makeEqHF     ) where  import Data.Comp.Derive.Utils-import Data.Comp.Multi.Functor+import Data.Comp.Multi.Equality import Language.Haskell.TH hiding (Cxt, match) --class KEq f where-    keq :: f i -> f j -> Bool--{-| Signature equality. An instance @HEqF f@ gives rise to an instance-  @KEq (HTerm f)@. -}-class HEqF f where--    heqF :: KEq g => f g i -> f g j -> Bool---instance KEq f => Eq (f i) where-    (==) = keq--instance Eq a => KEq (K a) where-    keq (K x) (K y) = x == y--instance KEq a => Eq (A a) where-     A x == A y = x `keq`  y--{-| Derive an instance of 'HEqF' for a type constructor of any higher-order+{-| Derive an instance of 'EqHF' for a type constructor of any higher-order   kind taking at least two arguments. -}-makeHEqF :: Name -> Q [Dec]-makeHEqF fname = do+makeEqHF :: Name -> Q [Dec]+makeEqHF fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let args' = init args-      argNames = (map (VarT . tyVarBndrName) (init args'))+      argNames = map (VarT . tyVarBndrName) (init args')       ftyp = VarT . tyVarBndrName $ last args'       complType = foldl AppT (ConT name) argNames       preCond = map (ClassP ''Eq . (: [])) argNames-      classType = AppT (ConT ''HEqF) complType+      classType = AppT (ConT ''EqHF) complType   constrs' <- mapM normalConExp constrs-  eqFDecl <- funD 'heqF  (eqFClauses ftyp constrs constrs')+  eqFDecl <- funD 'eqHF  (eqFClauses ftyp constrs constrs')   return [InstanceD preCond classType [eqFDecl]]       where eqFClauses ftyp constrs constrs' = map (genEqClause ftyp) constrs'                                    ++ defEqClause constrs

@@ -1,119 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Comp.Multi.Derive.Foldable--- Copyright   :  (c) 2011 Patrick Bahr--- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Automatically derive instances of @HFoldable@.--------------------------------------------------------------------------------------module Data.Comp.Multi.Derive.Foldable-    (-     HFoldable,-     makeHFoldable-    )where--import Data.Comp.Derive.Utils-import Data.Comp.Multi.Functor-import Data.Comp.Multi.Foldable-import Data.Foldable-import Language.Haskell.TH-import Data.Monoid-import Data.Maybe-import qualified Prelude as P (foldl,foldr,foldl1)-import Prelude hiding  (foldl,foldr,foldl1)-import Control.Monad---iter 0 _ e = e-iter n f e = iter (n-1) f (f `appE` e)--iter' n f e = run n f e-    where run 0 _ e = e-          run m f e = let f' = iter (m-1) [|fmap|] f-                      in run (m-1) f (f' `appE` e)--iterSp n f g e = run n e-    where run 0 e = e-          run m e = let f' = iter (m-1) [|fmap|] (if n == m then g else f)-                    in run (m-1) (f' `appE` e)--{-| Derive an instance of 'HFoldable' for a type constructor of any higher-order-  kind taking at least two arguments. -}-makeHFoldable :: Name -> Q [Dec]-makeHFoldable fname = do-  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname-  let args' = init args-      fArg = VarT . tyVarBndrName $ last args'-      argNames = (map (VarT . tyVarBndrName) (init args'))-      complType = P.foldl AppT (ConT name) argNames-      classType = AppT (ConT ''HFoldable) complType-  constrs' <- mapM (mkPatAndVars . isFarg fArg <=< normalConExp) constrs-  foldDecl <- funD 'hfold (map foldClause constrs')-  foldMapDecl <- funD 'hfoldMap (map foldMapClause constrs')-  foldlDecl <- funD 'hfoldl (map foldlClause constrs')-  foldrDecl <- funD 'hfoldr (map foldrClause constrs')-  return [InstanceD [] classType [foldDecl,foldMapDecl,foldlDecl,foldrDecl]]-      where isFarg fArg (constr, args) = (constr, map (`containsType'` fArg) args)-            filterVar [] _ = Nothing-            filterVar [d] x =Just (d, varE x)-            filterVar _ _ =  error "functor variable occurring twice in argument type"-            filterVars args varNs = catMaybes $ zipWith filterVar args varNs-            mkCPat constr args varNs = ConP constr $ zipWith mkPat args varNs-            mkPat [] _ = WildP-            mkPat _ x = VarP x-            mkPatAndVars (constr, args) =-                do varNs <- newNames (length args) "x"-                   return (mkCPat constr args varNs, filterVars args varNs)-            foldClause (pat,vars) =-                do let conApp (0,x) = [|unK $x|]-                       conApp (d,x) = iterSp d [|fold|] [| foldMap unK |] x-                   body <- if null vars-                           then [|mempty|]-                           else P.foldl1 (\ x y -> [|$x `mappend` $y|])-                                    $ map conApp vars-                   return $ Clause [pat] (NormalB body) []-            foldMapClause (pat,vars) =-                do fn <- newName "y"-                   let f = varE fn-                       f' 0 = f-                       f' n = iter (n-1) [|fmap|] [| foldMap $f |]-                       fp = if null vars then WildP else VarP fn-                   body <- case vars of-                             [] -> [|mempty|]-                             (_:_) -> P.foldl1 (\ x y -> [|$x `mappend` $y|]) $ -                                      map (\ (d,z) -> iter' (max (d-1) 0) [|fold|] (f' d `appE` z)) vars-                   return $ Clause [fp, pat] (NormalB body) []-            foldlClause (pat,vars) =-                do fn <- newName "f"-                   en <- newName "e"-                   let f = varE fn-                       e = varE en-                       fp = if null vars then WildP else VarP fn-                       ep = VarP en-                       conApp x (0,y) = [|$f $x $y|]-                       conApp x (1,y) = [|foldl $f $x $y|]-                       conApp x (d,y) = let hidEndo = iter (d-1) [|fmap|] [|Endo . flip (foldl $f)|] `appE` y-                                            endo = iter' (d-1) [|fold|] hidEndo-                                        in [| appEndo $endo $x|]-                   body <- P.foldl conApp e vars-                   return $ Clause [fp, ep, pat] (NormalB body) []-            foldrClause (pat,vars) =-                do fn <- newName "f"-                   en <- newName "e"-                   let f = varE fn-                       e = varE en-                       fp = if null vars then WildP else VarP fn-                       ep = VarP en-                       conApp (0,x) y = [|$f $x $y|]-                       conApp (1,x) y = [|foldr $f $y $x |]-                       conApp (d,x) y = let hidEndo = iter (d-1) [|fmap|] [|Endo . flip (foldr $f)|] `appE` x-                                            endo = iter' (d-1) [|fold|] hidEndo-                                        in [| appEndo $endo $y|]-                   body <- P.foldr conApp e vars-                   return $ Clause [fp, ep, pat] (NormalB body) []

@@ -1,63 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Comp.Multi.Derive.Functor--- Copyright   :  (c) 2011 Patrick Bahr--- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Automatically derive instances of @HFunctor@.--------------------------------------------------------------------------------------module Data.Comp.Multi.Derive.Functor-    (-     HFunctor,-     makeHFunctor-    ) where--import Data.Comp.Derive.Utils-import Data.Comp.Multi.Functor-import Language.Haskell.TH-import qualified Prelude as P (mapM)-import Prelude hiding (mapM)-import Data.Maybe-import Control.Monad--iter 0 _ e = e-iter n f e = iter (n-1) f (f `appE` e)--{-| Derive an instance of 'HFunctor' for a type constructor of any higher-order-  kind taking at least two arguments. -}-makeHFunctor :: Name -> Q [Dec]-makeHFunctor fname = do-  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname-  let args' = init args-      fArg = VarT . tyVarBndrName $ last args'-      argNames = (map (VarT . tyVarBndrName) (init args'))-      complType = foldl AppT (ConT name) argNames-      classType = AppT (ConT ''HFunctor) complType-  constrs' <- P.mapM (mkPatAndVars . isFarg fArg <=< normalConExp) constrs-  hfmapDecl <- funD 'hfmap (map hfmapClause constrs')-  return [InstanceD [] classType [hfmapDecl]]-      where isFarg fArg (constr, args) = (constr, map (`containsType'` fArg) args)-            filterVar _ nonFarg [] x  = nonFarg x-            filterVar farg _ [depth] x = farg depth x-            filterVar _ _ _ _ = error "functor variable occurring twice in argument type"-            filterVars args varNs farg nonFarg = zipWith (filterVar farg nonFarg) args varNs-            mkCPat constr varNs = ConP constr $ map mkPat varNs-            mkPat = VarP-            mkPatAndVars (constr, args) =-                do varNs <- newNames (length args) "x"-                   return (conE constr, mkCPat constr varNs,-                           \ f g -> filterVars args varNs (\ d x -> f d (varE x)) (g . varE),-                           any (not . null) args, map varE varNs, catMaybes $ filterVars args varNs (curry Just) (const Nothing))-            hfmapClause (con, pat,vars',hasFargs,_,_) =-                do fn <- newName "f"-                   let f = varE fn-                       fp = if hasFargs then VarP fn else WildP-                       vars = vars' (\d x -> iter d [|fmap|] f `appE` x) id-                   body <- foldl appE con vars-                   return $ Clause [fp, pat] (NormalB body) []

@@ -0,0 +1,119 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.Derive.HFoldable+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @HFoldable@.+--+--------------------------------------------------------------------------------++module Data.Comp.Multi.Derive.HFoldable+    (+     HFoldable,+     makeHFoldable+    )where++import Data.Comp.Derive.Utils+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HFoldable+import Data.Foldable+import Language.Haskell.TH+import Data.Monoid+import Data.Maybe+import qualified Prelude as P (foldl,foldr,foldl1)+import Prelude hiding  (foldl,foldr,foldl1)+import Control.Monad+++iter 0 _ e = e+iter n f e = iter (n-1) f (f `appE` e)++iter' n f e = run n f e+    where run 0 _ e = e+          run m f e = let f' = iter (m-1) [|fmap|] f+                      in run (m-1) f (f' `appE` e)++iterSp n f g e = run n e+    where run 0 e = e+          run m e = let f' = iter (m-1) [|fmap|] (if n == m then g else f)+                    in run (m-1) (f' `appE` e)++{-| Derive an instance of 'HFoldable' for a type constructor of any higher-order+  kind taking at least two arguments. -}+makeHFoldable :: Name -> Q [Dec]+makeHFoldable fname = do+  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname+  let args' = init args+      fArg = VarT . tyVarBndrName $ last args'+      argNames = map (VarT . tyVarBndrName) (init args')+      complType = P.foldl AppT (ConT name) argNames+      classType = AppT (ConT ''HFoldable) complType+  constrs' <- mapM (mkPatAndVars . isFarg fArg <=< normalConExp) constrs+  foldDecl <- funD 'hfold (map foldClause constrs')+  foldMapDecl <- funD 'hfoldMap (map foldMapClause constrs')+  foldlDecl <- funD 'hfoldl (map foldlClause constrs')+  foldrDecl <- funD 'hfoldr (map foldrClause constrs')+  return [InstanceD [] classType [foldDecl,foldMapDecl,foldlDecl,foldrDecl]]+      where isFarg fArg (constr, args) = (constr, map (`containsType'` fArg) args)+            filterVar [] _ = Nothing+            filterVar [d] x =Just (d, varE x)+            filterVar _ _ =  error "functor variable occurring twice in argument type"+            filterVars args varNs = catMaybes $ zipWith filterVar args varNs+            mkCPat constr args varNs = ConP constr $ zipWith mkPat args varNs+            mkPat [] _ = WildP+            mkPat _ x = VarP x+            mkPatAndVars (constr, args) =+                do varNs <- newNames (length args) "x"+                   return (mkCPat constr args varNs, filterVars args varNs)+            foldClause (pat,vars) =+                do let conApp (0,x) = [|unK $x|]+                       conApp (d,x) = iterSp d [|fold|] [| foldMap unK |] x+                   body <- if null vars+                           then [|mempty|]+                           else P.foldl1 (\ x y -> [|$x `mappend` $y|])+                                    $ map conApp vars+                   return $ Clause [pat] (NormalB body) []+            foldMapClause (pat,vars) =+                do fn <- newName "y"+                   let f = varE fn+                       f' 0 = f+                       f' n = iter (n-1) [|fmap|] [| foldMap $f |]+                       fp = if null vars then WildP else VarP fn+                   body <- case vars of+                             [] -> [|mempty|]+                             (_:_) -> P.foldl1 (\ x y -> [|$x `mappend` $y|]) $ +                                      map (\ (d,z) -> iter' (max (d-1) 0) [|fold|] (f' d `appE` z)) vars+                   return $ Clause [fp, pat] (NormalB body) []+            foldlClause (pat,vars) =+                do fn <- newName "f"+                   en <- newName "e"+                   let f = varE fn+                       e = varE en+                       fp = if null vars then WildP else VarP fn+                       ep = VarP en+                       conApp x (0,y) = [|$f $x $y|]+                       conApp x (1,y) = [|foldl $f $x $y|]+                       conApp x (d,y) = let hidEndo = iter (d-1) [|fmap|] [|Endo . flip (foldl $f)|] `appE` y+                                            endo = iter' (d-1) [|fold|] hidEndo+                                        in [| appEndo $endo $x|]+                   body <- P.foldl conApp e vars+                   return $ Clause [fp, ep, pat] (NormalB body) []+            foldrClause (pat,vars) =+                do fn <- newName "f"+                   en <- newName "e"+                   let f = varE fn+                       e = varE en+                       fp = if null vars then WildP else VarP fn+                       ep = VarP en+                       conApp (0,x) y = [|$f $x $y|]+                       conApp (1,x) y = [|foldr $f $y $x |]+                       conApp (d,x) y = let hidEndo = iter (d-1) [|fmap|] [|Endo . flip (foldr $f)|] `appE` x+                                            endo = iter' (d-1) [|fold|] hidEndo+                                        in [| appEndo $endo $y|]+                   body <- P.foldr conApp e vars+                   return $ Clause [fp, ep, pat] (NormalB body) []

@@ -0,0 +1,63 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.Derive.HFunctor+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @HFunctor@.+--+--------------------------------------------------------------------------------++module Data.Comp.Multi.Derive.HFunctor+    (+     HFunctor,+     makeHFunctor+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Multi.HFunctor+import Language.Haskell.TH+import qualified Prelude as P (mapM)+import Prelude hiding (mapM)+import Data.Maybe+import Control.Monad++iter 0 _ e = e+iter n f e = iter (n-1) f (f `appE` e)++{-| Derive an instance of 'HFunctor' for a type constructor of any higher-order+  kind taking at least two arguments. -}+makeHFunctor :: Name -> Q [Dec]+makeHFunctor fname = do+  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname+  let args' = init args+      fArg = VarT . tyVarBndrName $ last args'+      argNames = map (VarT . tyVarBndrName) (init args')+      complType = foldl AppT (ConT name) argNames+      classType = AppT (ConT ''HFunctor) complType+  constrs' <- P.mapM (mkPatAndVars . isFarg fArg <=< normalConExp) constrs+  hfmapDecl <- funD 'hfmap (map hfmapClause constrs')+  return [InstanceD [] classType [hfmapDecl]]+      where isFarg fArg (constr, args) = (constr, map (`containsType'` fArg) args)+            filterVar _ nonFarg [] x  = nonFarg x+            filterVar farg _ [depth] x = farg depth x+            filterVar _ _ _ _ = error "functor variable occurring twice in argument type"+            filterVars args varNs farg nonFarg = zipWith (filterVar farg nonFarg) args varNs+            mkCPat constr varNs = ConP constr $ map mkPat varNs+            mkPat = VarP+            mkPatAndVars (constr, args) =+                do varNs <- newNames (length args) "x"+                   return (conE constr, mkCPat constr varNs,+                           \ f g -> filterVars args varNs (\ d x -> f d (varE x)) (g . varE),+                           any (not . null) args, map varE varNs, catMaybes $ filterVars args varNs (curry Just) (const Nothing))+            hfmapClause (con, pat,vars',hasFargs,_,_) =+                do fn <- newName "f"+                   let f = varE fn+                       fp = if hasFargs then VarP fn else WildP+                       vars = vars' (\d x -> iter d [|fmap|] f `appE` x) id+                   body <- foldl appE con vars+                   return $ Clause [fp, pat] (NormalB body) []

@@ -0,0 +1,83 @@+{-# LANGUAGE TemplateHaskell #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.Derive.HTraversable+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @HTraversable@.+--+--------------------------------------------------------------------------------++module Data.Comp.Multi.Derive.HTraversable+    (+     HTraversable,+     makeHTraversable+    ) where++import Data.Comp.Derive.Utils+import Data.Comp.Multi.HTraversable+import Language.Haskell.TH+import Data.Maybe+import Data.Traversable+import Data.Foldable hiding (any,or)+import Control.Applicative+import Control.Monad hiding (mapM, sequence)+import qualified Prelude as P (foldl, foldr, mapM)+import Prelude hiding  (foldl, foldr,mapM, sequence)++iter 0 _ e = e+iter n f e = iter (n-1) f (f `appE` e)++iter' n f e = run n f e+    where run 0 _ e = e+          run m f e = let f' = iter (m-1) [|fmap|] f+                        in run (m-1) f (f' `appE` e)++{-| Derive an instance of 'HTraversable' for a type constructor of any+  higher-order kind taking at least two arguments. -}+makeHTraversable :: Name -> Q [Dec]+makeHTraversable fname = do+  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname+  let args' = init args+      fArg = VarT . tyVarBndrName $ last args'+      argNames = map (VarT . tyVarBndrName) (init args')+      complType = foldl AppT (ConT name) argNames+      classType = AppT (ConT ''HTraversable) complType+  constrs' <- P.mapM (mkPatAndVars . isFarg fArg <=< normalConExp) constrs+  traverseDecl <- funD 'htraverse (map traverseClause constrs')+  mapMDecl <- funD 'hmapM (map mapMClause constrs')+  return [InstanceD [] classType [traverseDecl, mapMDecl]]+      where isFarg fArg (constr, args) = (constr, map (`containsType'` fArg) args)+            filterVar _ nonFarg [] x  = nonFarg x+            filterVar farg _ [depth] x = farg depth x+            filterVar _ _ _ _ = error "functor variable occurring twice in argument type"+            filterVars args varNs farg nonFarg = zipWith (filterVar farg nonFarg) args varNs+            mkCPat constr varNs = ConP constr $ map mkPat varNs+            mkPat = VarP+            mkPatAndVars (constr, args) =+                do varNs <- newNames (length args) "x"+                   return (conE constr, mkCPat constr varNs,+                           \f g -> filterVars args varNs (\ d x -> f d (varE x)) (g . varE),+                           any (not . null) args, map varE varNs, catMaybes $ filterVars args varNs (curry Just) (const Nothing))+            traverseClause (con, pat,vars',hasFargs,_,_) =+                do fn <- newName "f"+                   let f = varE fn+                       fp = if hasFargs then VarP fn else WildP+                       vars = vars' (\d x -> iter d [|traverse|] f `appE` x) (\x -> [|pure $x|])+                   body <- P.foldl (\ x y -> [|$x <*> $y|]) [|pure $con|] vars+                   return $ Clause [fp, pat] (NormalB body) []+            -- Note: the monadic versions are not defined+            -- applicatively, as this results in a considerable+            -- performance penalty (by factor 2)!+            mapMClause (con, pat,_,hasFargs,allVars, fvars) =+                do fn <- newName "f"+                   let f = varE fn+                       fp = if hasFargs then VarP fn else WildP+                       conAp = P.foldl appE con allVars+                       conBind (d,x) y = [| $(iter d [|mapM|] f) $(varE x)  >>= $(lamE [varP x] y)|]+                   body <- P.foldr conBind [|return $conAp|] fvars+                   return $ Clause [fp, pat] (NormalB body) []

@@ -20,7 +20,7 @@     ) where  import Language.Haskell.TH hiding (Cxt)-import Data.Comp.Multi.Functor+import Data.Comp.Multi.HFunctor import Data.Comp.Multi.Term import Data.Comp.Multi.Algebra (CxtFun, appSigFun) import Data.Comp.Multi.Ops ((:+:)(..), (:<:)(..))@@ -34,7 +34,7 @@   let ivar = mkName "i"   let xvar = mkName "x"   let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]-  sequence $ (sigD i $ genSig fvars gvar avar ivar) : d+  sequence $ sigD i (genSig fvars gvar avar ivar) : d     where genSig fvars gvar avar ivar = do             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars             let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)@@ -45,7 +45,7 @@             forallT (map PlainTV $ gvar : avar : ivar : fvars)                     (sequence cxt) tp'           genDecl x n = [| case $(varE x) of-                             Inl x -> $(varE $ mkName $ "inj") x+                             Inl x -> $(varE $ mkName "inj") x                              Inr x -> $(varE $ mkName $ "inj" ++                                         if n > 2 then show (n - 1) else "") x |] injectn :: Int -> Q [Dec]@@ -56,7 +56,7 @@   let avar = mkName "a"   let ivar = mkName "i"   let d = [funD i [clause [] (normalB $ genDecl n) []]]-  sequence $ (sigD i $ genSig fvars gvar avar ivar) : d+  sequence $ sigD i (genSig fvars gvar avar ivar) : d     where genSig fvars gvar avar ivar = do             let hvar = mkName "h"             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars@@ -76,7 +76,7 @@   let fvars = map (\n -> mkName $ 'f' : show n) [1..n]   let gvar = mkName "g"   let d = [funD i [clause [] (normalB $ genDecl n) []]]-  sequence $ (sigD i $ genSig fvars gvar) : d+  sequence $ sigD i (genSig fvars gvar) : d     where genSig fvars gvar = do             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars             let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)

@@ -29,24 +29,7 @@   is lifted as @instance (HShowF f, HShowF g) => HShowF (f :+: g) where ... @.  -} liftSum :: Name -> Q [Dec]-liftSum fname = do-  ClassI (ClassD _ name targs _ decs) _ <- abstractNewtypeQ $ reify fname-  let targs' = map tyVarBndrName $ tail targs-  let f = mkName "f"-  let g = mkName "g"-  let cxt = [ClassP name (map VarT $ f : targs'),-             ClassP name (map VarT $ g : targs')]-  let tp = ConT name `AppT` ((ConT ''(:+:) `AppT` VarT f) `AppT` VarT g)-  let complType = foldl (\a x -> a `AppT` VarT x) tp targs'-  decs' <- sequence $ concatMap decl decs-  return [InstanceD cxt complType decs']-      where decl :: Dec -> [DecQ]-            decl (SigD f _) = [funD f [clause f]]-            decl _ = []-            clause :: Name -> ClauseQ-            clause f = do x <- newName "x"-                          b <- normalB [|caseH $(varE f) $(varE f) $(varE x)|]-                          return $ Clause [VarP x] b []+liftSum = liftSumGen 'caseH ''(:+:)  {-| Utility function to case on a higher-order functor sum, without exposing the   internal representation of sums. -}

@@ -0,0 +1,74 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,+  ScopedTypeVariables #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.Derive.Ordering+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Automatically derive instances of @OrdHF@.+--+--------------------------------------------------------------------------------+module Data.Comp.Multi.Derive.Ordering+    (+     OrdHF(..),+     makeOrdHF+    ) where++import Data.Comp.Multi.Ordering+import Data.Comp.Derive.Utils+import Data.Maybe+import Data.List+import Language.Haskell.TH hiding (Cxt)++compList :: [Ordering] -> Ordering+compList = fromMaybe EQ . find (/= EQ)++{-| Derive an instance of 'OrdHF' for a type constructor of any parametric+  kind taking at least three arguments. -}+makeOrdHF :: Name -> Q [Dec]+makeOrdHF fname = do+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname+  let args' = init args+  -- covariant argument+  let coArg :: Name = tyVarBndrName $ last args'+  let argNames = map (VarT . tyVarBndrName) (init args')+  let complType = foldl AppT (ConT name) argNames+  let classType = AppT (ConT ''OrdHF) complType+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs+  compareHFDecl <- funD 'compareHF (compareHFClauses coArg constrs')+  return [InstanceD [] classType [compareHFDecl]]+      where compareHFClauses :: Name -> [(Name,[Type])] -> [ClauseQ]+            compareHFClauses _ [] = []+            compareHFClauses coArg constrs = +                let constrs' = constrs `zip` [1..]+                    constPairs = [(x,y)| x<-constrs', y <- constrs']+                in map (genClause coArg) constPairs+            genClause coArg ((c,n),(d,m))+                | n == m = genEqClause coArg c+                | n < m = genLtClause c d+                | otherwise = genGtClause c d+            genEqClause :: Name -> (Name,[Type]) -> ClauseQ+            genEqClause coArg (constr, args) = do +              varXs <- newNames (length args) "x"+              varYs <- newNames (length args) "y"+              let patX = ConP constr $ map VarP varXs+              let patY = ConP constr $ map VarP varYs+              body <- eqDBody coArg (zip3 varXs varYs args)+              return $ Clause [patX, patY] (NormalB body) []+            eqDBody :: Name -> [(Name, Name, Type)] -> ExpQ+            eqDBody coArg x =+                [|compList $(listE $ map (eqDB coArg) x)|]+            eqDB :: Name -> (Name, Name, Type) -> ExpQ+            eqDB coArg (x, y, tp)+                | not (containsType tp (VarT coArg)) =+                    [| compare $(varE x) $(varE y) |]+                | otherwise =+                    [| kcompare $(varE x) $(varE y) |]+            genLtClause (c, _) (d, _) =+                clause [recP c [], recP d []] (normalB [| LT |]) []+            genGtClause (c, _) (d, _) =+                clause [recP c [], recP d []] (normalB [| GT |]) []

@@ -21,7 +21,7 @@  import Language.Haskell.TH hiding (Cxt) import Control.Monad (liftM)-import Data.Comp.Multi.Traversable (HTraversable)+import Data.Comp.Multi.HTraversable (HTraversable) import Data.Comp.Multi.Term import Data.Comp.Multi.Algebra (CxtFunM, appSigFunM') import Data.Comp.Multi.Ops ((:+:)(..), (:<:)(..))

@@ -8,29 +8,29 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- Automatically derive instances of @HShowF@.+-- Automatically derive instances of @ShowHF@. -- --------------------------------------------------------------------------------  module Data.Comp.Multi.Derive.Show     (-     HShowF(..),+     ShowHF(..),      KShow(..),-     makeHShowF+     makeShowHF     ) where  import Data.Comp.Derive.Utils-import Data.Comp.Multi.Functor+import Data.Comp.Multi.HFunctor import Data.Comp.Multi.Algebra import Language.Haskell.TH -{-| Signature printing. An instance @HShowF f@ gives rise to an instance+{-| Signature printing. An instance @ShowHF f@ gives rise to an instance   @KShow (HTerm f)@. -}-class HShowF f where-    hshowF :: Alg f (K String)-    hshowF = K . hshowF'-    hshowF' :: f (K String) :=> String-    hshowF' = unK . hshowF+class ShowHF f where+    showHF :: Alg f (K String)+    showHF = K . showHF'+    showHF' :: f (K String) :=> String+    showHF' = unK . showHF  class KShow a where     kshow :: a i -> K String i@@ -39,19 +39,19 @@ showConstr con [] = con showConstr con args = "(" ++ con ++ " " ++ unwords args ++ ")" -{-| Derive an instance of 'HShowF' for a type constructor of any higher-order+{-| Derive an instance of 'ShowHF' for a type constructor of any higher-order   kind taking at least two arguments. -}-makeHShowF :: Name -> Q [Dec]-makeHShowF fname = do+makeShowHF :: Name -> Q [Dec]+makeShowHF fname = do   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let args' = init args       fArg = VarT . tyVarBndrName $ last args'-      argNames = (map (VarT . tyVarBndrName) (init args'))+      argNames = map (VarT . tyVarBndrName) (init args')       complType = foldl AppT (ConT name) argNames       preCond = map (ClassP ''Show . (: [])) argNames-      classType = AppT (ConT ''HShowF) complType+      classType = AppT (ConT ''ShowHF) complType   constrs' <- mapM normalConExp constrs-  showFDecl <- funD 'hshowF (showFClauses fArg constrs')+  showFDecl <- funD 'showHF (showFClauses fArg constrs')   return [InstanceD preCond classType [showFDecl]]       where showFClauses fArg = map (genShowFClause fArg)             filterFarg fArg ty x = (containsType ty fArg, varE x)

@@ -21,7 +21,7 @@ import Data.Comp.Derive.Utils import Data.Comp.Multi.Sum import Data.Comp.Multi.Term-+import Control.Arrow ((&&&)) import Control.Monad  {-| Derive smart constructors for a type constructor of any higher-order kind@@ -31,7 +31,7 @@ smartConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname     let iVar = tyVarBndrName $ last targs-    let cons = map (\con -> (abstractConType con, iTp iVar con)) constrs+    let cons = map (abstractConType &&& iTp iVar) constrs     liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons         where iTp iVar (ForallC _ cxt _) =                   -- Check if the GADT phantom type is constrained@@ -56,7 +56,7 @@                 avar <- newName "a"                 ivar <- newName "i"                 let targs' = init $ init targs-                    vars = hvar:fvar:avar:(maybe [ivar] (const []) miTp)++targs'+                    vars = hvar:fvar:avar:maybe [ivar] (const []) miTp++targs'                     f = varT fvar                     h = varT hvar                     a = varT avar

@@ -1,83 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Comp.Multi.Derive.Traversable--- Copyright   :  (c) 2011 Patrick Bahr--- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ Automatically derive instances of @HTraversable@.--------------------------------------------------------------------------------------module Data.Comp.Multi.Derive.Traversable-    (-     HTraversable,-     makeHTraversable-    ) where--import Data.Comp.Derive.Utils-import Data.Comp.Multi.Traversable-import Language.Haskell.TH-import Data.Maybe-import Data.Traversable-import Data.Foldable hiding (any,or)-import Control.Applicative-import Control.Monad hiding (mapM, sequence)-import qualified Prelude as P (foldl, foldr, mapM)-import Prelude hiding  (foldl, foldr,mapM, sequence)--iter 0 _ e = e-iter n f e = iter (n-1) f (f `appE` e)--iter' n f e = run n f e-    where run 0 _ e = e-          run m f e = let f' = iter (m-1) [|fmap|] f-                        in run (m-1) f (f' `appE` e)--{-| Derive an instance of 'HTraversable' for a type constructor of any-  higher-order kind taking at least two arguments. -}-makeHTraversable :: Name -> Q [Dec]-makeHTraversable fname = do-  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname-  let args' = init args-      fArg = VarT . tyVarBndrName $ last args'-      argNames = (map (VarT . tyVarBndrName) (init args'))-      complType = foldl AppT (ConT name) argNames-      classType = AppT (ConT ''HTraversable) complType-  constrs' <- P.mapM (mkPatAndVars . isFarg fArg <=< normalConExp) constrs-  traverseDecl <- funD 'htraverse (map traverseClause constrs')-  mapMDecl <- funD 'hmapM (map mapMClause constrs')-  return [InstanceD [] classType [traverseDecl, mapMDecl]]-      where isFarg fArg (constr, args) = (constr, map (`containsType'` fArg) args)-            filterVar _ nonFarg [] x  = nonFarg x-            filterVar farg _ [depth] x = farg depth x-            filterVar _ _ _ _ = error "functor variable occurring twice in argument type"-            filterVars args varNs farg nonFarg = zipWith (filterVar farg nonFarg) args varNs-            mkCPat constr varNs = ConP constr $ map mkPat varNs-            mkPat = VarP-            mkPatAndVars (constr, args) =-                do varNs <- newNames (length args) "x"-                   return (conE constr, mkCPat constr varNs,-                           \f g -> filterVars args varNs (\ d x -> f d (varE x)) (g . varE),-                           any (not . null) args, map varE varNs, catMaybes $ filterVars args varNs (curry Just) (const Nothing))-            traverseClause (con, pat,vars',hasFargs,_,_) =-                do fn <- newName "f"-                   let f = varE fn-                       fp = if hasFargs then VarP fn else WildP-                       vars = vars' (\d x -> iter d [|traverse|] f `appE` x) (\x -> [|pure $x|])-                   body <- P.foldl (\ x y -> [|$x <*> $y|]) [|pure $con|] vars-                   return $ Clause [fp, pat] (NormalB body) []-            -- Note: the monadic versions are not defined-            -- applicatively, as this results in a considerable-            -- performance penalty (by factor 2)!-            mapMClause (con, pat,_,hasFargs,allVars, fvars) =-                do fn <- newName "f"-                   let f = varE fn-                       fp = if hasFargs then VarP fn else WildP-                       conAp = P.foldl appE con allVars-                       conBind (d,x) y = [| $(iter d [|mapM|] f) $(varE x)  >>= $(lamE [varP x] y)|]-                   body <- P.foldr conBind [|return $conAp|] fvars-                   return $ Clause [fp, pat] (NormalB body) []

@@ -15,7 +15,7 @@ -------------------------------------------------------------------------------- module Data.Comp.Multi.Equality     (-     HEqF(..),+     EqHF(..),      KEq(..),      heqMod     ) where@@ -23,36 +23,45 @@ import Data.Comp.Multi.Term import Data.Comp.Multi.Sum import Data.Comp.Multi.Ops-import Data.Comp.Multi.Derive+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HFoldable -import Data.Comp.Multi.Functor-import Data.Comp.Multi.Foldable+class KEq f where+    keq :: f i -> f j -> Bool +{-| Signature equality. An instance @EqHF f@ gives rise to an instance+  @KEq (HTerm f)@. -}+class EqHF f where+    eqHF :: KEq g => f g i -> f g j -> Bool++instance Eq a => KEq (K a) where+    keq (K x) (K y) = x == y++instance KEq a => Eq (A a) where+     A x == A y = x `keq`  y+ {-|   'EqF' is propagated through sums. -}+instance (EqHF f, EqHF g) => EqHF (f :+: g) where+    eqHF (Inl x) (Inl y) = eqHF x y+    eqHF (Inr x) (Inr y) = eqHF x y+    eqHF _ _ = False -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+instance EqHF f => EqHF (Cxt h f) where+    eqHF (Term e1) (Term e2) = e1 `eqHF` e2+    eqHF (Hole h1) (Hole h2) = h1 `keq` h2+    eqHF _ _ = False +instance (EqHF f, KEq a) => KEq (Cxt h f a) where+    keq = eqHF+ {-|   From an 'EqF' functor an 'Eq' instance of the corresponding   term type can be derived. -}-instance (HEqF f) => HEqF (Cxt h f) where--    heqF (Term e1) (Term e2) = e1 `heqF` e2-    heqF (Hole h1) (Hole h2) = h1 `keq` h2-    heqF _ _ = False--instance (HEqF f, KEq a)  => KEq (Cxt h f a) where-    keq = heqF--instance KEq Nothing where-    keq _ = undefined-+instance (EqHF f, KEq a) => Eq (Cxt h f a i) where+    (==) = keq  {-| This function implements equality of values of type @f a@ modulo the equality of @a@ itself. If two functorial values are equal in this@@ -60,9 +69,9 @@ consisting of corresponding components of the two functorial values. -} -heqMod :: (HEqF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)]+heqMod :: (EqHF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)] heqMod s t-    | unit s `heqF` unit' t = Just args+    | unit s `eqHF` unit' t = Just args     | otherwise = Nothing     where unit = hfmap (const $ K ())           unit' = hfmap (const $ K ())

@@ -1,67 +0,0 @@-{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}------------------------------------------------------------------------------------- |--- Module      :  Data.Comp.Multi.Foldable--- Copyright   :  (c) 2011 Patrick Bahr--- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ This module defines higher-order foldable functors.--------------------------------------------------------------------------------------module Data.Comp.Multi.Foldable-    (-     HFoldable (..),-     kfoldr,-     kfoldl,-     htoList-     ) where--import Data.Monoid-import Data.Maybe-import Data.Comp.Multi.Functor---- | Higher-order functors that can be folded.------ Minimal complete definition: 'hfoldMap' or 'hfoldr'.-class HFunctor h => HFoldable h where-    hfold :: Monoid m => h (K m) :=> m-    hfold = hfoldMap unK--    hfoldMap :: Monoid m => (a :=> m) -> h a :=> m-    hfoldMap f = hfoldr (mappend . f) mempty--    hfoldr :: (a :=> b -> b) -> b -> h a :=> b-    hfoldr f z t = appEndo (hfoldMap (Endo . f) t) z--    hfoldl :: (b -> a :=> b) -> b -> h a :=> b-    hfoldl f z t = appEndo (getDual (hfoldMap (Dual . Endo . flip f) t)) z---    hfoldr1 :: forall a. (a -> a -> a) -> h (K a) :=> a-    hfoldr1 f xs = fromMaybe (error "hfoldr1: empty structure")-                   (hfoldr mf Nothing xs)-          where mf :: K a :=> Maybe a -> Maybe a-                mf (K x) Nothing = Just x-                mf (K x) (Just y) = Just (f x y)--    hfoldl1 :: forall a . (a -> a -> a) -> h (K a) :=> a-    hfoldl1 f xs = fromMaybe (error "hfoldl1: empty structure")-                   (hfoldl mf Nothing xs)-          where mf :: Maybe a -> K a :=> Maybe a-                mf Nothing (K y) = Just y-                mf (Just x) (K y) = Just (f x y)--htoList :: (HFoldable f) => f a :=> [A a]-htoList = hfoldr (\ n l ->  A n : l) []-    -kfoldr :: (HFoldable f) => (a -> b -> b) -> b -> f (K a) :=> b-kfoldr f = hfoldr (\ (K x) y -> f x y)---kfoldl :: (HFoldable f) => (b -> a -> b) -> b -> f (K a) :=> b-kfoldl f = hfoldl (\ x (K y) -> f x y)

@@ -1,85 +0,0 @@-{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}------------------------------------------------------------------------------------- |--- Module      :  Data.Comp.Multi.Functor--- Copyright   :  (c) 2011 Patrick Bahr--- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ This module defines higher-order functors (Johann, Ghani, POPL--- '08), i.e. endofunctors on the category of endofunctors.--------------------------------------------------------------------------------------module Data.Comp.Multi.Functor-    (-     HFunctor (..),-     (:->),-     (:=>),-     NatM,-     I (..),-     K (..),-     A (..),-     (:.:)(..)-     ) where---- | The identity Functor.-newtype I a = I {unI :: a}---- | The parametrised constant functor.-newtype K a i = K {unK :: a}--instance Functor (K a) where-    fmap _ (K x) = K x--data A f = forall i. A {unA :: f i}--instance Eq a => Eq (K a i) where-    K x == K y = x == y-    K x /= K y = x /= y--instance Ord a => Ord (K a i) where-    K x < K y = x < y-    K x > K y = x > y-    K x <= K y = x <= y-    K x >= K y = x >= y-    min (K x) (K y) = K $ min x y-    max (K x) (K y) = K $ max x y-    compare (K x) (K y) = compare x y---infixr 0 :-> -- same precedence as function space operator ->-infixr 0 :=> -- same precedence as function space operator ->---- | This type represents natural transformations.-type f :-> g = forall i . f i -> g i---- | This type represents co-cones from @f@ to @a@. @f :=> a@ is--- isomorphic to f :-> K a-type f :=> a = forall i . f i -> a---type NatM m f g = forall i. f i -> m (g i)---- | This class represents higher-order functors (Johann, Ghani, POPL--- '08) which are endofunctors on the category of endofunctors.-class HFunctor h where-    -- A higher-order functor @f@ maps every functor @g@ to a-    -- functor @f g@.-    ---    -- @ffmap :: (Functor g) => (a -> b) -> f g a -> f g b@-    -- -    -- We omit this, as it does not work for GADTs (see Johand and-    -- Ghani 2008).--    -- | A higher-order functor @f@ also maps a natural transformation-    -- @g :-> h@ to a natural transformation @f g :-> f h@-    hfmap :: (f :-> g) -> h f :-> h g--infixl 5 :.:---- | This data type denotes the composition of two functor families.-data (f :.: g) e t = Comp f (g e) t

@@ -19,9 +19,9 @@  import Data.Comp.Multi.Term import Data.Comp.Multi.Sum-import Data.Comp.Multi.Functor-import Data.Comp.Multi.Foldable-import Data.Comp.Multi.Traversable+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HFoldable+import Data.Comp.Multi.HTraversable import GHC.Exts import Control.Monad import Prelude

@@ -0,0 +1,67 @@+{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.HFoldable+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines higher-order foldable functors.+--+--------------------------------------------------------------------------------++module Data.Comp.Multi.HFoldable+    (+     HFoldable (..),+     kfoldr,+     kfoldl,+     htoList+     ) where++import Data.Monoid+import Data.Maybe+import Data.Comp.Multi.HFunctor++-- | Higher-order functors that can be folded.+--+-- Minimal complete definition: 'hfoldMap' or 'hfoldr'.+class HFunctor h => HFoldable h where+    hfold :: Monoid m => h (K m) :=> m+    hfold = hfoldMap unK++    hfoldMap :: Monoid m => (a :=> m) -> h a :=> m+    hfoldMap f = hfoldr (mappend . f) mempty++    hfoldr :: (a :=> b -> b) -> b -> h a :=> b+    hfoldr f z t = appEndo (hfoldMap (Endo . f) t) z++    hfoldl :: (b -> a :=> b) -> b -> h a :=> b+    hfoldl f z t = appEndo (getDual (hfoldMap (Dual . Endo . flip f) t)) z+++    hfoldr1 :: forall a. (a -> a -> a) -> h (K a) :=> a+    hfoldr1 f xs = fromMaybe (error "hfoldr1: empty structure")+                   (hfoldr mf Nothing xs)+          where mf :: K a :=> Maybe a -> Maybe a+                mf (K x) Nothing = Just x+                mf (K x) (Just y) = Just (f x y)++    hfoldl1 :: forall a . (a -> a -> a) -> h (K a) :=> a+    hfoldl1 f xs = fromMaybe (error "hfoldl1: empty structure")+                   (hfoldl mf Nothing xs)+          where mf :: Maybe a -> K a :=> Maybe a+                mf Nothing (K y) = Just y+                mf (Just x) (K y) = Just (f x y)++htoList :: (HFoldable f) => f a :=> [A a]+htoList = hfoldr (\ n l ->  A n : l) []+    +kfoldr :: (HFoldable f) => (a -> b -> b) -> b -> f (K a) :=> b+kfoldr f = hfoldr (\ (K x) y -> f x y)+++kfoldl :: (HFoldable f) => (b -> a -> b) -> b -> f (K a) :=> b+kfoldl f = hfoldl (\ x (K y) -> f x y)

@@ -0,0 +1,85 @@+{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.HFunctor+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines higher-order functors (Johann, Ghani, POPL+-- '08), i.e. endofunctors on the category of endofunctors.+--+--------------------------------------------------------------------------------++module Data.Comp.Multi.HFunctor+    (+     HFunctor (..),+     (:->),+     (:=>),+     NatM,+     I (..),+     K (..),+     A (..),+     (:.:)(..)+     ) where++-- | The identity Functor.+newtype I a = I {unI :: a}++-- | The parametrised constant functor.+newtype K a i = K {unK :: a}++instance Functor (K a) where+    fmap _ (K x) = K x++data A f = forall i. A {unA :: f i}++instance Eq a => Eq (K a i) where+    K x == K y = x == y+    K x /= K y = x /= y++instance Ord a => Ord (K a i) where+    K x < K y = x < y+    K x > K y = x > y+    K x <= K y = x <= y+    K x >= K y = x >= y+    min (K x) (K y) = K $ min x y+    max (K x) (K y) = K $ max x y+    compare (K x) (K y) = compare x y+++infixr 0 :-> -- same precedence as function space operator ->+infixr 0 :=> -- same precedence as function space operator ->++-- | This type represents natural transformations.+type f :-> g = forall i . f i -> g i++-- | This type represents co-cones from @f@ to @a@. @f :=> a@ is+-- isomorphic to f :-> K a+type f :=> a = forall i . f i -> a+++type NatM m f g = forall i. f i -> m (g i)++-- | This class represents higher-order functors (Johann, Ghani, POPL+-- '08) which are endofunctors on the category of endofunctors.+class HFunctor h where+    -- A higher-order functor @f@ maps every functor @g@ to a+    -- functor @f g@.+    --+    -- @ffmap :: (Functor g) => (a -> b) -> f g a -> f g b@+    -- +    -- We omit this, as it does not work for GADTs (see Johand and+    -- Ghani 2008).++    -- | A higher-order functor @f@ also maps a natural transformation+    -- @g :-> h@ to a natural transformation @f g :-> f h@+    hfmap :: (f :-> g) -> h f :-> h g++infixl 5 :.:++-- | This data type denotes the composition of two functor families.+data (f :.: g) e t = Comp f (g e) t

@@ -0,0 +1,36 @@+{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.HTraversable+-- Copyright   :  (c) 2011 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines higher-order traversable functors.+--+--------------------------------------------------------------------------------++module Data.Comp.Multi.HTraversable+    (+     HTraversable (..)+    ) where++import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HFoldable+import Control.Applicative++class HFoldable t => HTraversable t where++    -- | Map each element of a structure to a monadic action, evaluate+    -- these actions from left to right, and collect the results.+    --+    -- Alternative type in terms of natural transformations using+    -- functor composition @:.:@:+    --+    -- @hmapM :: Monad m => (a :-> m :.: b) -> t a :-> m :.: (t b)@+    hmapM :: (Monad m) => NatM m a b -> NatM m (t a) (t b)++    htraverse :: (Applicative f) => NatM f a b -> NatM f (t a) (t b)

@@ -18,9 +18,9 @@  module Data.Comp.Multi.Ops where -import Data.Comp.Multi.Functor-import Data.Comp.Multi.Foldable-import Data.Comp.Multi.Traversable+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HFoldable+import Data.Comp.Multi.HTraversable import qualified Data.Comp.Ops as O import Control.Monad import Control.Applicative

@@ -0,0 +1,62 @@+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,+  UndecidableInstances, IncoherentInstances, GADTs #-}+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.Ordering+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved+-- License     :  BSD3+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module defines ordering of signatures, which lifts to ordering of+-- terms and contexts.+--+--------------------------------------------------------------------------------+module Data.Comp.Multi.Ordering+    (+     KOrd(..),+     OrdHF(..)+    ) where++import Data.Comp.Multi.Term+import Data.Comp.Multi.Sum+import Data.Comp.Multi.Ops+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.Equality++class KEq f => KOrd f where+    kcompare :: f i -> f j -> Ordering++{-| Signature ordering. An instance @OrdHF f@ gives rise to an instance+  @Ord (Term f)@. -}+class EqHF f => OrdHF f where+    compareHF :: KOrd a => f a i -> f a j -> Ordering++--instance KOrd f => Ord (f i) where+--    compare = kcompare++instance Ord a => KOrd (K a) where+    kcompare (K x) (K y) = compare x y++{-| 'OrdHF' is propagated through sums. -}+instance (OrdHF f, OrdHF g) => OrdHF (f :+: g) where+    compareHF (Inl x) (Inl y) = compareHF x y+    compareHF (Inl _) (Inr _) = LT+    compareHF (Inr x) (Inr y) = compareHF x y+    compareHF (Inr _) (Inl _) = GT++{-| From an 'OrdHF' difunctor an 'Ord' instance of the corresponding term type+  can be derived. -}+instance (HFunctor f, OrdHF f) => OrdHF (Cxt h f) where+    compareHF (Term e1) (Term e2) = compareHF e1 e2+    compareHF (Hole h1) (Hole h2) = kcompare h1 h2+    compareHF (Term _) _ = LT+    compareHF (Hole _) (Term _) = GT++instance (HFunctor f, OrdHF f, KOrd a) => KOrd (Cxt h f a) where+    kcompare = compareHF++{-| Ordering of terms. -}+instance (HFunctor f, OrdHF f, KOrd a) => Ord (Cxt h f a i) where+    compare = kcompare

@@ -17,31 +17,29 @@ --------------------------------------------------------------------------------  module Data.Comp.Multi.Show-    ( HShowF(..)+    ( ShowHF(..)     ) where  import Data.Comp.Multi.Term import Data.Comp.Multi.Annotation import Data.Comp.Multi.Algebra-import Data.Comp.Multi.Functor+import Data.Comp.Multi.HFunctor import Data.Comp.Multi.Derive -instance KShow Nothing where-    kshow _ = undefined instance KShow (K String) where     kshow = id -instance (HShowF f, HFunctor f) => HShowF (Cxt h f) where-    hshowF (Hole s) = s-    hshowF (Term t) = hshowF $ hfmap hshowF t+instance (ShowHF f, HFunctor f) => ShowHF (Cxt h f) where+    showHF (Hole s) = s+    showHF (Term t) = showHF $ hfmap showHF t -instance (HShowF f, HFunctor f, KShow a) => KShow (Cxt h f a) where-    kshow = free hshowF kshow+instance (ShowHF f, HFunctor f, KShow a) => KShow (Cxt h f a) where+    kshow = free showHF 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 (ShowHF f, Show p) => ShowHF (f :&: p) where+    showHF (v :&: p) =  K $ unK (showHF v) ++ " :&: " ++ show p -$(derive [liftSum] [''HShowF])+$(derive [liftSum] [''ShowHF])

@@ -94,8 +94,8 @@ --     substHoles'     ) where -import Data.Comp.Multi.Functor-import Data.Comp.Multi.Traversable+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HTraversable import Data.Comp.Multi.Ops import Data.Comp.Multi.Term import Data.Comp.Multi.Algebra

@@ -20,7 +20,6 @@      Hole,      NoHole,      Context,-     Nothing,      Term,      Const,      constTerm,@@ -29,9 +28,9 @@      simpCxt      ) where -import Data.Comp.Multi.Functor-import Data.Comp.Multi.Foldable-import Data.Comp.Multi.Traversable+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HFoldable+import Data.Comp.Multi.HTraversable import Data.Monoid  import Control.Monad@@ -67,15 +66,8 @@ -- | A context might contain holes. type Context = Cxt Hole -{-| Phantom type family used to define 'Term'.  -}-data Nothing :: * -> *--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 Term f = Cxt NoHole f Nothing+type Term f = Cxt NoHole f (K ())  -- | This function unravels the given term at the topmost layer. unTerm :: Term f t -> f (Term f) t

@@ -1,36 +0,0 @@-{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}------------------------------------------------------------------------------------- |--- Module      :  Data.Comp.Multi.Traversable--- Copyright   :  (c) 2011 Patrick Bahr--- License     :  BSD3--- Maintainer  :  Patrick Bahr <paba@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ This module defines higher-order traversable functors.--------------------------------------------------------------------------------------module Data.Comp.Multi.Traversable-    (-     HTraversable (..)-    ) where--import Data.Comp.Multi.Functor-import Data.Comp.Multi.Foldable-import Control.Applicative--class HFoldable t => HTraversable t where--    -- | Map each element of a structure to a monadic action, evaluate-    -- these actions from left to right, and collect the results.-    ---    -- Alternative type in terms of natural transformations using-    -- functor composition @:.:@:-    ---    -- @hmapM :: Monad m => (a :-> m :.: b) -> t a :-> m :.: (t b)@-    hmapM :: (Monad m) => NatM m a b -> NatM m (t a) (t b)--    htraverse :: (Applicative f) => NatM f a b -> NatM f (t a) (t b)

@@ -34,8 +34,8 @@ import Data.Comp.Multi.Term import Data.Comp.Multi.Algebra import Data.Comp.Multi.Derive-import Data.Comp.Multi.Functor-import Data.Comp.Multi.Foldable+import Data.Comp.Multi.HFunctor+import Data.Comp.Multi.HFoldable import Data.Set (Set) import qualified Data.Set as Set import Data.Maybe@@ -49,7 +49,7 @@  type CxtSubst h a f v =  GSubst v (Cxt h f a) -type Subst f v = CxtSubst NoHole Nothing f v+type Subst f v = CxtSubst NoHole (K ()) 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

@@ -2,7 +2,7 @@   FlexibleContexts, CPP #-} -------------------------------------------------------------------------------- -- |--- Module      :  Data.Comp.Algebra+-- Module      :  Data.Comp.MultiParam.Algebra -- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved -- License     :  BSD3 -- Maintainer  :  Tom Hvitved <hvitved@diku.dk>@@ -52,10 +52,14 @@       sigFunM,       hom',       appHomM,+      appTHomM,       appHomM',+      appTHomM',       homM,       appSigFunM,+      appTSigFunM,       appSigFunM',+      appTSigFunM',       compHomM,       compSigFunM,       compAlgM,@@ -69,8 +73,6 @@ import Data.Comp.MultiParam.HDifunctor import Data.Comp.MultiParam.HDitraversable -import Unsafe.Coerce (unsafeCoerce)- {-| This type represents an algebra over a difunctor @f@ and carrier @a@. -} type Alg f a = f a a :-> a @@ -80,17 +82,17 @@         => Alg f a -> (b :-> a) -> Cxt h f a b :-> a free f g = run     where run :: Cxt h f a b :-> a-          run (Term t) = f (hfmap run t)+          run (In t) = f (hfmap run t)           run (Hole x) = g x-          run (Place p) = p+          run (Var p) = p  {-| Construct a catamorphism from the given algebra. -} cata :: forall f a. HDifunctor f => Alg f a -> Term f :-> a  {-# NOINLINE [1] cata #-}-cata f = run . coerceCxt+cata f (Term t) = run t     where run :: Trm f a :-> a-          run (Term t) = f (hfmap run t)-          run (Place x) = x+          run (In t) = f (hfmap run t)+          run (Var x) = x  {-| A generalisation of 'cata' from terms over @f@ to contexts over @f@, where   the holes have the type of the algebra carrier. -}@@ -100,9 +102,9 @@  {-| This function applies a whole context into another context. -} appCxt :: HDifunctor f => Cxt Hole f a (Cxt h f a b) :-> Cxt h f a b-appCxt (Term t) = Term (hfmap appCxt t)+appCxt (In t) = In (hfmap appCxt t) appCxt (Hole x) = x-appCxt (Place p) = Place p+appCxt (Var p) = Var p  {-| This type represents a monadic algebra. It is similar to 'Alg' but   the return type is monadic. -}@@ -110,22 +112,22 @@  {-| Construct a monadic catamorphism for contexts over @f@ with holes of type   @b@, from the given monadic algebra. -}-freeM :: forall m h f a b. (HDitraversable f m a, Monad m)+freeM :: forall m h f a b. (HDitraversable f, Monad m)          => AlgM m f a -> NatM m b a -> NatM m (Cxt h f a b) a freeM f g = run     where run :: NatM m (Cxt h f a b) a-          run (Term t) = f =<< hdimapM run t+          run (In t) = f =<< hdimapM run t           run (Hole x) = g x-          run (Place p) = return p+          run (Var p) = return p  {-| Construct a monadic catamorphism from the given monadic algebra. -}-cataM :: forall m f a. (HDitraversable f m a, Monad m)+cataM :: forall m f a. (HDitraversable f, Monad m)          => AlgM m f a -> NatM m (Term f) a {-# NOINLINE [1] cataM #-}-cataM algm = run . coerceCxt+cataM algm (Term t) = run t     where run :: NatM m (Trm f a) a-          run (Term t) = algm =<< hdimapM run t-          run (Place x) = return x+          run (In t) = algm =<< hdimapM run t+          run (Var x) = return x  {-| This type represents a monadic algebra, but where the covariant argument is   also a monadic computation. -}@@ -137,18 +139,18 @@           => AlgM' m f a -> NatM m b a -> NatM m (Cxt h f a b) a freeM' f g = run     where run :: NatM m (Cxt h f a b) a-          run (Term t) = f $ hfmap (Compose . run) t+          run (In t) = f $ hfmap (Compose . run) t           run (Hole x) = g x-          run (Place p) = return p+          run (Var p) = return p  {-| Construct a monadic catamorphism from the given monadic algebra. -} cataM' :: forall m f a. (HDifunctor f, Monad m)           => AlgM' m f a -> NatM m (Term f) a {-# NOINLINE [1] cataM' #-}-cataM' algm = run . coerceCxt+cataM' algm (Term t) = run t     where run :: NatM m (Trm f a) a-          run (Term t) = algm $ hfmap (Compose . run) t-          run (Place x) = return x+          run (In t) = algm $ hfmap (Compose . run) t+          run (Var x) = return x  {-| This type represents a signature function. -} type SigFun f g = forall a b. f a b :-> g a b@@ -160,14 +162,13 @@ type Hom f g = SigFun f (Context g)  {-| Apply a term homomorphism recursively to a term/context. -}-appHom :: forall f g. (HDifunctor f, HDifunctor g)-              => Hom f g -> CxtFun f g+appHom :: forall f g. (HDifunctor f, HDifunctor g) => Hom f g -> CxtFun f g {-# INLINE [1] appHom #-} appHom f = run where     run :: CxtFun f g-    run (Term t) = appCxt (f (hfmap run t))+    run (In t) = appCxt (f (hfmap run t))     run (Hole x) = Hole x-    run (Place p) = Place p+    run (Var p) = Var p  -- | Apply a term homomorphism recursively to a term/context. This is -- a top-down variant of 'appHom'.@@ -176,9 +177,9 @@ {-# INLINE [1] appHom' #-} appHom' f = run where     run :: CxtFun f g-    run (Term t) = appCxt (hfmapCxt run (f t))+    run (In t) = appCxt (hfmapCxt run (f t))     run (Hole x) = Hole x-    run (Place p) = Place p+    run (Var p) = Var p  {-| Compose two term homomorphisms. -} compHom :: (HDifunctor g, HDifunctor h)@@ -193,17 +194,17 @@ appSigFun :: forall f g. (HDifunctor f) => SigFun f g -> CxtFun f g appSigFun f = run where     run :: CxtFun f g-    run (Term t) = Term (f (hfmap run t))+    run (In t) = In (f (hfmap run t))     run (Hole x) = Hole x-    run (Place p) = Place p+    run (Var p) = Var p  {-| This function applies a signature function to the given context. -} appSigFun' :: forall f g. (HDifunctor g) => SigFun f g -> CxtFun f g appSigFun' f = run where     run :: CxtFun f g-    run (Term t) = Term (hfmap run (f t))+    run (In t) = In (hfmap run (f t))     run (Hole x) = Hole x-    run (Place p) = Place p+    run (Var p) = Var p  {-| This function composes two signature functions. -} compSigFun :: SigFun g h -> SigFun f g -> SigFun f h@@ -219,14 +220,6 @@ {-| This type represents a monadic context function. -} type CxtFunM m f g = forall h . SigFunM m (Cxt h f) (Cxt h g) -{-| This type represents a monadic context function. -}-type CxtFunM' m f g = forall h b . NatM m (Cxt h f Any b) (Cxt h g Any b)---coerceCxtFunM :: CxtFunM' m f g -> CxtFunM m f g-coerceCxtFunM = unsafeCoerce-- {-| This type represents a monadic term homomorphism. -} type HomM m f g = SigFunM m f (Cxt Hole g) @@ -240,76 +233,92 @@ {-| Lift the give monadic signature function to a monadic term homomorphism. -} hom' :: (HDifunctor f, HDifunctor g, Monad m)             => SigFunM m f g -> HomM m f g-hom' f = liftM  (Term . hfmap Hole) . f+hom' f = liftM  (In . hfmap Hole) . f  {-| Lift the given signature function to a monadic term homomorphism. -} homM :: (HDifunctor g, Monad m) => SigFun f g -> HomM m f g homM f = sigFunM $ hom f  {-| Apply a monadic term homomorphism recursively to a term/context. -}-appHomM :: forall f g m. (HDitraversable f m Any, HDifunctor g, Monad m)+appHomM :: forall f g m. (HDitraversable f, Monad m, HDifunctor g)                => HomM m f g -> CxtFunM m f g {-# NOINLINE [1] appHomM #-}-appHomM f = coerceCxtFunM run-    where run :: CxtFunM' m f g-          run (Term t) = liftM appCxt (f =<< hdimapM run t)+appHomM f = run+    where run :: CxtFunM m f g+          run (In t) = liftM appCxt (f =<< hdimapM run t)           run (Hole x) = return (Hole x)-          run (Place p) = return (Place p)+          run (Var p) = return (Var p) +{-| A restricted form of |appHomM| which only works for terms. -}+appTHomM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)+            => HomM m f g -> Term f i -> m (Term g i)+appTHomM f (Term t) = termM (appHomM f t)+ -- | Apply a monadic term homomorphism recursively to a -- term/context. This is a top-down variant of 'appHomM'.-appHomM' :: forall f g m. (HDitraversable g m Any, Monad m)-               => HomM m f g -> CxtFunM m f g+appHomM' :: forall f g m. (HDitraversable g, Monad m)+            => HomM m f g -> CxtFunM m f g {-# NOINLINE [1] appHomM' #-}-appHomM' f = coerceCxtFunM run-    where run :: CxtFunM' m f g-          run (Term t) = liftM appCxt (hdimapMCxt run =<<  f t)+appHomM' f = run+    where run :: CxtFunM m f g+          run (In t) = liftM appCxt (hdimapMCxt run =<<  f t)           run (Hole x) = return (Hole x)-          run (Place p) = return (Place p)+          run (Var p) = return (Var p) +{-| A restricted form of |appHomM'| which only works for terms. -}+appTHomM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)+             => HomM m f g -> Term f i -> m (Term g i)+appTHomM' f (Term t) = termM (appHomM' f t)  {-| This function applies a monadic signature function to the given context. -}-appSigFunM :: forall m f g. (HDitraversable f m Any, Monad m)+appSigFunM :: forall m f g. (HDitraversable f, Monad m)               => SigFunM m f g -> CxtFunM m f g-appSigFunM f = coerceCxtFunM run-    where run :: CxtFunM' m f g-          run (Term t) = liftM Term (f =<< hdimapM run t)+appSigFunM f = run+    where run :: CxtFunM m f g+          run (In t)   = liftM In (f =<< hdimapM run t)           run (Hole x) = return (Hole x)-          run (Place p) = return (Place p)+          run (Var p)  = return (Var p) +{-| A restricted form of |appSigFunM| which only works for terms. -}+appTSigFunM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)+               => SigFunM m f g -> Term f i -> m (Term g i)+appTSigFunM f (Term t) = termM (appSigFunM f t)+ -- | This function applies a monadic signature function to the given -- context. This is a top-down variant of 'appSigFunM'.-appSigFunM' :: forall m f g. (HDitraversable g m Any, Monad m)-              => SigFunM m f g -> CxtFunM m f g-appSigFunM' f = coerceCxtFunM run-    where run :: CxtFunM' m f g-          run (Term t) = liftM Term (hdimapM run =<< f t)+appSigFunM' :: forall m f g. (HDitraversable g, Monad m)+               => SigFunM m f g -> CxtFunM m f g+appSigFunM' f = run+    where run :: CxtFunM m f g+          run (In t)   = liftM In (hdimapM run =<< f t)           run (Hole x) = return (Hole x)-          run (Place p) = return (Place p)+          run (Var p)  = return (Var p) +{-| A restricted form of |appSigFunM'| which only works for terms. -}+appTSigFunM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)+                => SigFunM m f g -> Term f i -> m (Term g i)+appTSigFunM' f (Term t) = termM (appSigFunM' f t)  {-| Compose two monadic term homomorphisms. -}-compHomM :: (HDitraversable g m Any, HDifunctor h, Monad m)+compHomM :: (HDitraversable g, HDifunctor h, Monad m)                 => HomM m g h -> HomM m f g -> HomM m f h compHomM f g = appHomM f <=< g  {-| Compose a monadic algebra with a monadic term homomorphism to get a new   monadic algebra. -}-compAlgM :: (HDitraversable g m a, Monad m)-            => AlgM m g a -> HomM m f g -> AlgM m f a+compAlgM :: (HDitraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a compAlgM alg talg = freeM alg return <=< talg  {-| Compose a monadic algebra with a term homomorphism to get a new monadic   algebra. -}-compAlgM' :: (HDitraversable g m a, Monad m) => AlgM m g a-          -> Hom f g -> AlgM m f a+compAlgM' :: (HDitraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a compAlgM' alg talg = freeM alg return . talg  {-| This function composes two monadic signature functions. -} compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h compSigFunM f g a = g a >>= f -+{- #ifndef NO_RULES {-# RULES   "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.@@ -337,3 +346,4 @@  #-} -} #endif+-}

@@ -1,23 +0,0 @@-{-# LANGUAGE EmptyDataDecls, KindSignatures #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Comp.MultiParam.Any--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved--- License     :  BSD3--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>--- Stability   :  experimental--- Portability :  non-portable (GHC Extensions)------ This module defines the empty data type 'Any', which is used to emulate--- parametricity (\"poor mans parametricity\").--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Any-    (-     Any-    ) where---- |The empty data type 'Any' is used to emulate parametricity--- (\"poor mans parametricity\").-data Any :: * -> *

@@ -27,10 +27,6 @@      module Data.Comp.MultiParam.Derive.Show,      -- ** HDifunctor      module Data.Comp.MultiParam.Derive.HDifunctor,-     -- ** HFoldable-     module Data.Comp.Multi.Derive.Foldable,-     -- ** HTraversable-     module Data.Comp.Multi.Derive.Traversable,      -- ** Smart Constructors      module Data.Comp.MultiParam.Derive.SmartConstructors,      -- ** Smart Constructors w/ Annotations@@ -44,8 +40,6 @@ import Data.Comp.MultiParam.Derive.Ordering import Data.Comp.MultiParam.Derive.Show import Data.Comp.MultiParam.Derive.HDifunctor-import Data.Comp.Multi.Derive.Foldable-import Data.Comp.Multi.Derive.Traversable import Data.Comp.MultiParam.Derive.SmartConstructors import Data.Comp.MultiParam.Derive.SmartAConstructors import Data.Comp.MultiParam.Derive.LiftSum

@@ -19,7 +19,7 @@     ) where  import Data.Comp.Derive.Utils-import Data.Comp.MultiParam.FreshM+import Data.Comp.MultiParam.FreshM hiding (Name) import Data.Comp.MultiParam.Equality import Control.Monad import Language.Haskell.TH hiding (Cxt, match)@@ -68,9 +68,7 @@                           | a == coArg -> [| peq $(varE x) $(varE y) |]                       AppT (AppT ArrowT (AppT (VarT a) _)) _                           | a == conArg ->-                              [| do {v <- genVar;-                                     peq ($(varE x) $ varCoerce v) -                                         ($(varE y) $ varCoerce v)} |]+                              [| withName (\v -> peq ($(varE x) $ nameCoerce v)                                                      ($(varE y) $ nameCoerce v)) |]                       SigT tp' _ ->                           eqHDB conArg coArg (x, y, tp')                       _ ->

@@ -35,7 +35,7 @@   let ivar = mkName "i"   let xvar = mkName "x"   let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]-  sequence $ (sigD i $ genSig fvars gvar avar bvar ivar) : d+  sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d     where genSig fvars gvar avar bvar ivar = do             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars             let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)@@ -47,7 +47,7 @@             forallT (map PlainTV $ gvar : avar : bvar : ivar : fvars)                     (sequence cxt) tp'           genDecl x n = [| case $(varE x) of-                             Inl x -> $(varE $ mkName $ "inj") x+                             Inl x -> $(varE $ mkName "inj") x                              Inr x -> $(varE $ mkName $ "inj" ++                                         if n > 2 then show (n - 1) else "") x |] injectn :: Int -> Q [Dec]@@ -59,7 +59,7 @@   let bvar = mkName "b"   let ivar = mkName "i"   let d = [funD i [clause [] (normalB $ genDecl n) []]]-  sequence $ (sigD i $ genSig fvars gvar avar bvar ivar) : d+  sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d     where genSig fvars gvar avar bvar ivar = do             let hvar = mkName "h"             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars@@ -72,7 +72,7 @@                               `appT` (tp' `appT` varT ivar)             forallT (map PlainTV $ hvar : gvar : avar : bvar : ivar : fvars)                     (sequence cxt) tp''-          genDecl n = [| Term . $(varE $ mkName $ "inj" ++ show n) |]+          genDecl n = [| In . $(varE $ mkName $ "inj" ++ show n) |]  deepInjectn :: Int -> Q [Dec] deepInjectn n = do@@ -80,7 +80,7 @@   let fvars = map (\n -> mkName $ 'f' : show n) [1..n]   let gvar = mkName "g"   let d = [funD i [clause [] (normalB $ genDecl n) []]]-  sequence $ (sigD i $ genSig fvars gvar) : d+  sequence $ sigD i (genSig fvars gvar) : d     where genSig fvars gvar = do             let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars             let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)

@@ -29,24 +29,7 @@   @class ShowHD f where ...@ is lifted as   @instance (ShowHD f, ShowHD g) => ShowHD (f :+: g) where ... @. -} liftSum :: Name -> Q [Dec]-liftSum fname = do-  ClassI (ClassD _ name targs _ decs) _ <- abstractNewtypeQ $ reify fname-  let targs' = map tyVarBndrName $ tail targs-  let f = mkName "f"-  let g = mkName "g"-  let cxt = [ClassP name (map VarT $ f : targs'),-             ClassP name (map VarT $ g : targs')]-  let tp = ConT name `AppT` ((ConT ''(:+:) `AppT` VarT f) `AppT` VarT g)-  let complType = foldl (\a x -> a `AppT` VarT x) tp targs'-  decs' <- sequence $ concatMap decl decs-  return [InstanceD cxt complType decs']-      where decl :: Dec -> [DecQ]-            decl (SigD f _) = [funD f [clause f]]-            decl _ = []-            clause :: Name -> ClauseQ-            clause f = do x <- newName "x"-                          b <- normalB [|caseHD $(varE f) $(varE f) $(varE x)|]-                          return $ Clause [VarP x] b []+liftSum = liftSumGen 'caseHD ''(:+:)  {-| Utility function to case on a higher-order difunctor sum, without exposing   the internal representation of sums. -}

@@ -18,7 +18,7 @@      makeOrdHD     ) where -import Data.Comp.MultiParam.FreshM+import Data.Comp.MultiParam.FreshM hiding (Name) import Data.Comp.MultiParam.Ordering import Data.Comp.Derive.Utils import Data.Maybe@@ -44,7 +44,8 @@   let classType = AppT (ConT ''OrdHD) complType   constrs' :: [(Name,[Type])] <- mapM normalConExp constrs   compareHDDecl <- funD 'compareHD (compareHDClauses conArg coArg constrs')-  return [InstanceD [] classType [compareHDDecl]]+  let context = map (\arg -> ClassP ''Ord [arg]) argNames+  return [InstanceD context classType [compareHDDecl]]       where compareHDClauses :: Name -> Name -> [(Name,[Type])] -> [ClauseQ]             compareHDClauses _ _ [] = []             compareHDClauses conArg coArg constrs = @@ -77,9 +78,8 @@                           | a == coArg -> [| pcompare $(varE x) $(varE y) |]                       AppT (AppT ArrowT (AppT (VarT a) _)) _                           | a == conArg ->-                              [| do {v <- genVar;-                                     pcompare ($(varE x) $ varCoerce v)-                                              ($(varE y) $ varCoerce v)} |]+                              [| withName (\v -> pcompare ($(varE x) $ nameCoerce v)+                                                          ($(varE y) $ nameCoerce v)) |]                       SigT tp' _ ->                           eqDB conArg coArg (x, y, tp')                       _ ->

@@ -23,7 +23,7 @@ import Control.Monad (liftM) import Data.Comp.MultiParam.HDitraversable (HDitraversable) import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Algebra (CxtFunM, appSigFunM')+import Data.Comp.MultiParam.Algebra (appTSigFunM') import Data.Comp.MultiParam.Ops ((:+:)(..), (:<:)(..))  projn :: Int -> Q [Dec]@@ -86,8 +86,8 @@                     (sequence cxt) tp''           genDecl x n = [| case $(varE x) of                              Hole _ -> Nothing-                             Place _ -> Nothing-                             Term t -> $(varE $ mkName $ "proj" ++ show n) t |]+                             Var _ -> Nothing+                             In t -> $(varE $ mkName $ "proj" ++ show n) t |]  deepProjectn :: Int -> Q [Dec] deepProjectn n = do@@ -97,11 +97,12 @@   sequence $ (sigD p $ genSig gvars) : d     where genSig gvars = do             let fvar = mkName "f"+            let ivar = mkName "i"             let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars             let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)                             (map varT gvars)-            let cxt' = classP ''HDitraversable [tp, conT ''Maybe, conT ''Any]-            let tp' = conT ''CxtFunM `appT` conT ''Maybe-                                     `appT` varT fvar `appT` tp-            forallT (map PlainTV $ fvar : gvars) (sequence $ cxt' : cxt) tp'-          genDecl n = [| appSigFunM' $(varE $ mkName $ "proj" ++ show n) |]+            let cxt' = classP ''HDitraversable [tp]+            let tp' = arrowT `appT` (conT ''Term `appT` varT fvar `appT` varT ivar)+                             `appT` (conT ''Maybe `appT` (conT ''Term `appT` tp `appT` varT ivar))+            forallT (map PlainTV $ fvar : ivar : gvars) (sequence $ cxt' : cxt) tp'+          genDecl n = [| appTSigFunM' $(varE $ mkName $ "proj" ++ show n) |]

@@ -14,25 +14,28 @@ -------------------------------------------------------------------------------- module Data.Comp.MultiParam.Derive.Show     (-     PShow(..),      ShowHD(..),      makeShowHD     ) where  import Data.Comp.Derive.Utils-import Data.Comp.MultiParam.FreshM+import Data.Comp.MultiParam.FreshM hiding (Name)+import qualified Data.Comp.MultiParam.FreshM as FreshM+import Data.Comp.MultiParam.HDifunctor import Control.Monad import Language.Haskell.TH hiding (Cxt, match)---- |Printing of parametric values.-class PShow a where-    pshow :: a i -> FreshM String+import qualified Data.Traversable as T  {-| Signature printing. An instance @ShowHD f@ gives rise to an instance   @Show (Term f i)@. -} class ShowHD f where-    showHD :: PShow a => f Var a i -> FreshM String+    showHD :: f FreshM.Name (K (FreshM String)) i -> FreshM String +newtype Dummy = Dummy String++instance Show Dummy where+  show (Dummy s) = s+ {-| Derive an instance of 'ShowHD' for a type constructor of any parametric   kind taking at least three arguments. -} makeShowHD :: Name -> Q [Dec]@@ -70,16 +73,15 @@                 | otherwise =                     case tp of                       AppT (VarT a) _ -                          | a == coArg -> [| pshow $(varE x) |]+                          | a == coArg -> [| unK $(varE x) |]                       AppT (AppT ArrowT (AppT (VarT a) _)) _                           | a == conArg ->-                              [| do {v <- genVar;-                                     body <- pshow $ $(varE x) v;-                                     return $ "\\" ++ varShow v ++ " -> " ++ body} |]+                              [| withName (\v -> do body <- (unK . $(varE x)) v+                                                    return $ "\\" ++ show v ++ " -> " ++ body) |]                       SigT tp' _ ->                           showHDB conArg coArg (x, tp')                       _ ->                           if containsType tp (VarT conArg) then                               [| showHD $(varE x) |]                           else-                              [| pshow $(varE x) |]+                              [| liftM show $ T.mapM (liftM Dummy . unK) $(varE x) |]

@@ -28,7 +28,7 @@  {-| Derive smart constructors with annotations for a higher-order difunctor. The  smart constructors are similar to the ordinary constructors, but a- 'injectA . hdimap Place id' is automatically inserted. -}+ 'injectA . hdimap Var id' is automatically inserted. -} smartAConstructors :: Name -> Q [Dec] smartAConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname@@ -43,6 +43,6 @@                 let pats = map varP (varPr : varNs)                     vars = map varE varNs                     val = appE [|injectA $(varE varPr)|] $-                          appE [|inj . hdimap Place id|] $ foldl appE (conE name) vars-                    function = [funD sname [clause pats (normalB [|Term $val|]) []]]+                          appE [|inj . hdimap Var id|] $ foldl appE (conE name) vars+                    function = [funD sname [clause pats (normalB [|In $val|]) []]]                 sequence function

@@ -22,16 +22,17 @@ import Data.Comp.MultiParam.Sum import Data.Comp.MultiParam.Term import Data.Comp.MultiParam.HDifunctor+import Control.Arrow ((&&&)) import Control.Monad  {-| Derive smart constructors for a higher-order difunctor. The smart  constructors are similar to the ordinary constructors, but a- 'inject . hdimap Place id' is automatically inserted. -}+ 'inject . hdimap Var id' is automatically inserted. -} smartConstructors :: Name -> Q [Dec] smartConstructors fname = do     TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname     let iVar = tyVarBndrName $ last targs-    let cons = map (\con -> (abstractConType con, iTp iVar con)) constrs+    let cons = map (abstractConType &&& iTp iVar) constrs     liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons         where iTp iVar (ForallC _ cxt _) =                   -- Check if the GADT phantom type is constrained@@ -48,7 +49,7 @@                     vars = map varE varNs                     val = foldl appE (conE name) vars                     sig = genSig targs tname sname args miTp-                    function = [funD sname [clause pats (normalB [|inject (hdimap Place id $val)|]) []]]+                    function = [funD sname [clause pats (normalB [|inject (hdimap Var id $val)|]) []]]                 sequence $ sig ++ function               genSig targs tname sname 0 miTp = (:[]) $ do                 hvar <- newName "h"@@ -56,8 +57,8 @@                 avar <- newName "a"                 bvar <- newName "b"                 ivar <- newName "i"-                let targs' = init $ init $ init $ targs-                    vars = hvar:fvar:avar:bvar:(maybe [ivar] (const []) miTp)++targs'+                let targs' = init $ init $ init targs+                    vars = hvar:fvar:avar:bvar:maybe [ivar] (const []) miTp++targs'                     h = varT hvar                     f = varT fvar                     a = varT avar

@@ -1,5 +1,5 @@ {-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,-  UndecidableInstances, OverlappingInstances, TypeOperators #-}+  UndecidableInstances, OverlappingInstances, TypeOperators, Rank2Types #-} -------------------------------------------------------------------------------- -- | -- Module      :  Data.Comp.MultiParam.Desugar@@ -29,12 +29,12 @@  -- |Desugar a term. desugar :: Desugar f g => Term f :-> Term g-desugar = appHom desugHom+desugar (Term t) = Term (appHom desugHom t)  -- |Lift desugaring to annotated terms. desugarA :: (HDifunctor f', HDifunctor g', DistAnn f p f', DistAnn g p g',              Desugar f g) => Term f' :-> Term g'-desugarA = appHom (propAnn desugHom)+desugarA (Term t) = Term (appHom (propAnn desugHom) t)  -- |Default desugaring instance. instance (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g where

@@ -37,7 +37,7 @@   @Eq (Term f i)@. The equality test is performed inside the 'FreshM' monad for   generating fresh identifiers. -} class EqHD f where-    eqHD :: PEq a => f Var a i -> f Var a j -> FreshM Bool+    eqHD :: PEq a => f Name a i -> f Name a j -> FreshM Bool  {-| 'EqHD' is propagated through sums. -} instance (EqHD f, EqHD g) => EqHD (f :+: g) where@@ -45,20 +45,20 @@     eqHD (Inr x) (Inr y) = eqHD x y     eqHD _ _ = return False -instance PEq Var where-   peq x y = return $ varEq x y+instance PEq Name where+   peq x y = return $ nameCoerce x == y  {-| From an 'EqHD' difunctor an 'Eq' instance of the corresponding term type can   be derived. -} instance EqHD f => EqHD (Cxt h f) where-    eqHD (Term e1) (Term e2) = eqHD e1 e2+    eqHD (In e1) (In e2) = eqHD e1 e2     eqHD (Hole h1) (Hole h2) = peq h1 h2-    eqHD (Place p1) (Place p2) = peq p1 p2+    eqHD (Var p1) (Var p2) = peq p1 p2     eqHD _ _ = return False -instance (EqHD f, PEq a) => PEq (Cxt h f Var a) where+instance (EqHD f, PEq a) => PEq (Cxt h f Name a) where     peq = eqHD  {-| Equality on terms. -} instance (HDifunctor f, EqHD f) => Eq (Term f i) where-    (==) x y = evalFreshM $ eqHD (coerceCxt x) (coerceCxt y)+    (==) (Term x) (Term y) = evalFreshM $ eqHD x y

@@ -8,57 +8,47 @@ -- Stability   :  experimental -- Portability :  non-portable (GHC Extensions) ----- This module defines a monad for generating fresh, abstract variables, useful+-- This module defines a monad for generating fresh, abstract names, useful -- e.g. for defining equality on terms. -- -------------------------------------------------------------------------------- module Data.Comp.MultiParam.FreshM     (      FreshM,-     Var,-     varEq,-     varCompare,-     varShow,-     genVar,-     varCoerce,+     Name,+     withName,+     nameCoerce,      evalFreshM     ) where -import Control.Monad.State+import Control.Monad.Reader --- |Monad for generating fresh (abstract) variables.-newtype FreshM a = FreshM (State [String] a)+-- |Monad for generating fresh (abstract) names.+newtype FreshM a = FreshM{unFreshM :: Reader Int a}     deriving Monad --- |Abstract notion of a variable (the constructor is hidden).-data Var i = Var String---- |Equality on variables.-varEq :: Var i -> Var j -> Bool-varEq (Var x) (Var y) = x == y+-- |Abstract notion of a name (the constructor is hidden).+newtype Name i = Name Int+    deriving Eq --- |Ordering of variables.-varCompare :: Var i -> Var j -> Ordering-varCompare (Var x) (Var y) = compare x y+instance Show (Name i) where+    show (Name x) = names !! x+        where baseNames = ['a'..'z']+              names = map (:[]) baseNames ++ names' 1+              names' n = map (: show n) baseNames ++ names' (n + 1) --- |Printing of variables.-varShow :: Var i -> String-varShow (Var x) = x+instance Ord (Name i) where+    compare (Name x) (Name y) = compare x y --- |Change the type of a variable.-varCoerce :: Var i -> Var j-varCoerce (Var x) = Var x+-- |Change the type tag of a name.+nameCoerce :: Name i -> Name j+nameCoerce (Name x) = Name x --- |Generate a fresh variable.-genVar :: FreshM (Var i)-genVar = FreshM $ do xs <- get-                     case xs of-                       (x : xs') -> do {put xs'; return $ Var x}-                       _ -> fail "Unexpected empty list"+-- |Run the given computation with the next available name.+withName :: (Name i -> FreshM a) -> FreshM a+withName m = do name <- FreshM (asks Name)+                FreshM $ local ((+) 1) $ unFreshM $ m name --- |Evaluate a computation that uses fresh variables.+-- |Evaluate a computation that uses fresh names. evalFreshM :: FreshM a -> a-evalFreshM (FreshM m) = evalState m vars-    where baseVars = ['a'..'z']-          vars = map (:[]) baseVars ++ vars' 1-          vars' n = map (: show n) baseVars ++ vars' (n + 1)+evalFreshM (FreshM m) = runReader m 0

@@ -27,42 +27,7 @@      NatM     ) where -import Data.Comp.Multi.Functor (HFunctor (..))---- | The identity functor.-newtype I a = I {unI :: a}---- | The parametrised constant functor.-newtype K a i = K {unK :: a}--instance Functor I where-    fmap f (I x) = I (f x)--instance Functor (K a) where-    fmap _ (K x) = K x--data A f = forall i. A {unA :: f i}--instance Eq a => Eq (K a i) where-    K x == K y = x == y-    K x /= K y = x /= y--instance Ord a => Ord (K a i) where-    K x < K y = x < y-    K x > K y = x > y-    K x <= K y = x <= y-    K x >= K y = x >= y-    min (K x) (K y) = K $ min x y-    max (K x) (K y) = K $ max x y-    compare (K x) (K y) = compare x y--infixr 0 :-> -- same precedence as function space operator ->---- |This type represents natural transformations.-type f :-> g = forall i . f i -> g i---- |This type represents monadic natural transformations.-type NatM m f g = forall i. f i -> m (g i)+import Data.Comp.Multi.HFunctor  -- | This class represents higher-order difunctors. class HDifunctor f where

@@ -20,43 +20,10 @@     ) where  import Prelude hiding (mapM, sequence, foldr)-import Data.Comp.Multi.Traversable+import Data.Comp.Multi.HTraversable import Data.Comp.MultiParam.HDifunctor-{-import Data.Traversable-import Test.QuickCheck.Gen-import Data.Functor.Identity-import Control.Monad.Reader hiding (mapM, sequence)-}  {-| HDifunctors representing data structures that can be traversed from left to   right. -}-class (HDifunctor f, Monad m) => HDitraversable f m a where-    hdimapM :: NatM m b c -> NatM m (f a b) (f a c)--{-| If a higher-order difunctor is 'HTraversable' for a given contravariant-  argument @a@, then it is 'HDitraversable' for all 'Monad's @m@ with the same-  @a@. -}-instance (HDifunctor f, Monad m, HTraversable (f a)) => HDitraversable f m a where-    hdimapM = hmapM--{-instance HDitraversable (:~>) Gen a where-    hdimapM f ((:~>) s) = MkGen run-        where run stdGen seed a = unGen (f (s a)) stdGen seed--instance HDitraversable (->) Identity a where-    dimapM f s = Identity run-        where run a = runIdentity (f (s a))-    disequence s = Identity run-        where run a = runIdentity (s a)--instance HDitraversable (->) m a =>  HDitraversable (->) (ReaderT r m) a where-    dimapM f s = ReaderT (disequence . run)-        where run r a = runReaderT (f (s a)) r-    disequence s = ReaderT (disequence . run)-        where run r a = runReaderT (s a) r--{-| Functions of the type @Any -> Maybe a@ can be turned into functions of- type @Maybe (Any -> a)@. The empty type @Any@ ensures that the function- is parametric in the input, and hence the @Maybe@ monad can be pulled out. -}-instance HDitraversable (->) Maybe Any where-    disequence f = do _ <- f undefined-                      return $ \x -> fromJust $ f x-}+class HDifunctor f => HDitraversable f where+    hdimapM :: Monad m => NatM m b c -> NatM m (f a b) (f a c)

@@ -33,8 +33,7 @@     hdimap f g (Inl e) = Inl (hdimap f g e)     hdimap f g (Inr e) = Inr (hdimap f g e) -instance (HDitraversable f m a, HDitraversable g m a)-    => HDitraversable (f :+: g) m a where+instance (HDitraversable f, HDitraversable g) => HDitraversable (f :+: g) where     hdimapM f (Inl e) = Inl `liftM` hdimapM f e     hdimapM f (Inr e) = Inr `liftM` hdimapM f e @@ -84,7 +83,7 @@ instance HDifunctor f => HDifunctor (f :&: p) where     hdimap f g (v :&: c) = hdimap f g v :&: c -instance HDitraversable f m a => HDitraversable (f :&: p) m a where+instance HDitraversable f => HDitraversable (f :&: p) where     hdimapM f (v :&: c) = liftM (:&: c) (hdimapM f v)  {-| This class defines how to distribute an annotation over a sum of

@@ -36,7 +36,7 @@ {-| Signature ordering. An instance @OrdHD f@ gives rise to an instance   @Ord (Term f)@. -} class EqHD f => OrdHD f where-    compareHD :: POrd a => f Var a i -> f Var a j -> FreshM Ordering+    compareHD :: POrd a => f Name a i -> f Name a j -> FreshM Ordering  {-| 'OrdHD' is propagated through sums. -} instance (OrdHD f, OrdHD g) => OrdHD (f :+: g) where@@ -48,20 +48,20 @@ {-| From an 'OrdHD' difunctor an 'Ord' instance of the corresponding term type   can be derived. -} instance OrdHD f => OrdHD (Cxt h f) where-    compareHD (Term e1) (Term e2) = compareHD e1 e2+    compareHD (In e1) (In e2) = compareHD e1 e2     compareHD (Hole h1) (Hole h2) = pcompare h1 h2-    compareHD (Place p1) (Place p2) = pcompare p1 p2-    compareHD (Term _) _ = return LT-    compareHD (Hole _) (Term _) = return GT-    compareHD (Hole _) (Place _) = return LT-    compareHD (Place _) _ = return GT+    compareHD (Var p1) (Var p2) = pcompare p1 p2+    compareHD (In _) _ = return LT+    compareHD (Hole _) (In _) = return GT+    compareHD (Hole _) (Var _) = return LT+    compareHD (Var _) _ = return GT -instance POrd Var where-    pcompare x y = return $ varCompare x y+instance POrd Name where+    pcompare x y = return $ compare (nameCoerce x) y -instance (OrdHD f, POrd a) => POrd (Cxt h f Var a) where+instance (OrdHD f, POrd a) => POrd (Cxt h f Name a) where     pcompare = compareHD  {-| Ordering of terms. -} instance (HDifunctor f, OrdHD f) => Ord (Term f i) where-    compare x y = evalFreshM $ compareHD (coerceCxt x) (coerceCxt y)+    compare (Term x) (Term y) = evalFreshM $ compareHD x y

@@ -14,7 +14,6 @@ -------------------------------------------------------------------------------- module Data.Comp.MultiParam.Show     (-     PShow(..),      ShowHD(..)     ) where @@ -24,28 +23,20 @@ import Data.Comp.MultiParam.Derive import Data.Comp.MultiParam.FreshM -instance Show a => PShow (K a) where-    pshow = return . show . unK- -- Lift ShowHD to sums $(derive [liftSum] [''ShowHD]) -instance PShow Var where-    pshow = return . varShow- {-| From an 'ShowHD' higher-order difunctor an 'ShowHD' instance of the   corresponding term type can be derived. -}-instance (ShowHD f, PShow a) => PShow (Cxt h f Var a) where-    pshow (Term t) = showHD t-    pshow (Hole h) = pshow h-    pshow (Place p) = pshow p+instance (HDifunctor f, ShowHD f) => ShowHD (Cxt h f) where+    showHD (In t) = showHD $ hfmap (K . showHD) t+    showHD (Hole h) = unK h+    showHD (Var p) = return $ show p  {-| Printing of terms. -} instance (HDifunctor f, ShowHD f) => Show (Term f i) where-    show = evalFreshM . pshow .-           (coerceCxt :: Term f i -> Trm f Var i)+    show = evalFreshM . showHD . toCxt . unTerm -instance (ShowHD f, PShow (K p)) => ShowHD (f :&: p) where+instance (ShowHD f, Show p) => ShowHD (f :&: p) where     showHD (x :&: p) = do sx <- showHD x-                          sp <- pshow $ K p-                          return $ sx ++ " :&: " ++ sp+                          return $ sx ++ " :&: " ++ show p

@@ -83,11 +83,6 @@      deepInject9,      deepInject10, -     -- * Injections and Projections for Constants-     injectConst,-     injectConst2,-     injectConst3,-     projectConst,      injectCxt,      liftCxt     ) where@@ -107,18 +102,18 @@ -- |Project the outermost layer of a term to a sub signature. If the signature -- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead. project :: (g :<: f) => NatM Maybe (Cxt h f a b) (g a (Cxt h f a b))-project (Term t) = proj t+project (In t)   = proj t project (Hole _) = Nothing-project (Place _) = Nothing+project (Var _)  = Nothing  $(liftM concat $ mapM projectn [2..10])  -- | Tries to coerce a term/context to a term/context over a sub-signature. If -- the signature @g@ is compound of /n/ atomic signatures, use -- @deepProject@/n/ instead.-deepProject :: (HDitraversable g Maybe Any, g :<: f) => CxtFunM Maybe f g+deepProject :: (HDitraversable g, g :<: f) => Term f i -> Maybe (Term g i) {-# INLINE deepProject #-}-deepProject = appSigFunM' proj+deepProject = appTSigFunM' proj  $(liftM concat $ mapM deepProjectn [2..10]) {-# INLINE deepProject2 #-}@@ -136,7 +131,7 @@ -- |Inject a term where the outermost layer is a sub signature. If the signature -- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead. inject :: (g :<: f) => g a (Cxt h f a b) :-> Cxt h f a b-inject = Term . inj+inject = In . inj  $(liftM concat $ mapM injectn [2..10]) @@ -158,118 +153,11 @@ {-# INLINE deepInject9 #-} {-# INLINE deepInject10 #-} -{-{-| A variant of 'proj' for binary sum signatures.  -}-proj2 :: forall f g1 g2 a b i. (g1 :<: f, g2 :<: f) => f a b i-      -> Maybe ((g1 :+: g2) a b i)-proj2 x = case proj x of-            Just (y :: g1 a b i) -> Just $ inj y-            _ -> liftM inj (proj x :: Maybe (g2 a b i))--{-| A variant of 'proj' for ternary sum signatures.  -}-proj3 :: forall f g1 g2 g3 a b i. (g1 :<: f, g2 :<: f, g3 :<: f) => f a b i-      -> Maybe ((g1 :+: g2 :+: g3) a b i)-proj3 x = case proj x of-            Just (y :: g1 a b i) -> Just $ inj y-            _ -> case proj x of-                   Just (y :: g2 a b i) -> Just $ inj y-                   _ -> liftM inj (proj x :: Maybe (g3 a b i))---- |Project the outermost layer of a term to a sub signature.-project :: (g :<: f) => NatM Maybe (Cxt h f a b) (g a (Cxt h f a b))-project (Term t) = proj t-project (Hole _) = Nothing-project (Place _) = Nothing---- |Project the outermost layer of a term to a binary sub signature.-project2 :: (g1 :<: f, g2 :<: f)-            => NatM Maybe (Cxt h f a b) ((g1 :+: g2) a (Cxt h f a b))-project2 (Term t) = proj2 t-project2 (Hole _) = Nothing-project2 (Place _) = Nothing---- |Project the outermost layer of a term to a ternary sub signature.-project3 :: (g1 :<: f, g2 :<: f, g3 :<: f)-            => NatM Maybe (Cxt h f a b) ((g1 :+: g2 :+: g3) a (Cxt h f a b))-project3 (Term t) = proj3 t-project3 (Hole _) = Nothing-project3 (Place _) = Nothing---- | Tries to coerce a term/context to a term/context over a--- sub-signature.-deepProject :: (HDitraversable g Maybe Any, g :<: f)-             => CxtFunM Maybe f g-deepProject = appSigFunM' proj---- | This is a variant of 'deepProject' that can be used if the target--- signature cannot be derived as being a sub-signature of the source--- signature directly but its decomposition into two summands can.-deepProject2 :: (HDitraversable (g1 :+: g2) Maybe Any, g1 :<: f, g2 :<: f)-              => CxtFunM Maybe f (g1 :+: g2)-deepProject2 = appSigFunM' proj2---- | This is a variant of 'deepProject' that can be used if the target--- signature cannot be derived as being a sub-signature of the source--- signature directly but its decomposition into three summands can.-deepProject3 ::(HDitraversable (g1 :+: g2 :+: g3) Maybe Any, g1 :<: f, g2 :<: f, g3 :<: f)-                 => CxtFunM Maybe f (g1 :+: g2 :+: g3)-deepProject3 = appSigFunM' proj3--{-| A variant of 'inj' for binary sum signatures.  -}-inj2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) a b :-> g a b-inj2 (Inl x) = inj x-inj2 (Inr y) = inj y--{-| A variant of 'inj' for ternary sum signatures.  -}-inj3 :: (f1 :<: g, f2 :<: g, f3 :<: g) => (f1 :+: f2 :+: f3) a b :-> g a b-inj3 (Inl x) = inj x-inj3 (Inr y) = inj2 y---- |Inject a term where the outermost layer is a sub signature.-inject :: (g :<: f) => g a (Cxt h f a b) :-> Cxt h f a b-inject = Term . inj---- |Inject a term where the outermost layer is a binary sub signature.-inject2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) a (Cxt h g a b) :-> Cxt h g a b-inject2 = Term . inj2---- |Inject a term where the outermost layer is a ternary sub signature.-inject3 :: (f1 :<: g, f2 :<: g, f3 :<: g) => (f1 :+: f2 :+: f3) a (Cxt h g a b)-        :-> Cxt h g a b-inject3 = Term . inj3---- |Inject a term over a sub signature to a term over larger signature.-deepInject :: (HDifunctor g, g :<: f) => CxtFun g f-deepInject = appSigFun inj---- |Inject a term over a binary sub signature to a term over larger signature.-deepInject2 :: (HDifunctor (f1 :+: f2), f1 :<: g, f2 :<: g)  => CxtFun (f1 :+: f2) g-deepInject2 = appSigFun inj2---- |Inject a term over a ternary signature to a term over larger signature.-deepInject3 :: (HDifunctor (f1 :+: f2 :+: f3), f1 :<: g, f2 :<: g, f3 :<: g)-               => CxtFun (f1 :+: f2 :+: f3) g-deepInject3 =  appSigFun inj3-}--injectConst :: (HDifunctor g, g :<: f) => Const g :-> Cxt h f Any a-injectConst = inject . hfmap (const undefined)--injectConst2 :: (HDifunctor f1, HDifunctor f2, HDifunctor g, f1 :<: g, f2 :<: g)-                => Const (f1 :+: f2) :-> Cxt h g Any a-injectConst2 = inject2 . hfmap (const undefined)--injectConst3 :: (HDifunctor f1, HDifunctor f2, HDifunctor f3, HDifunctor g,-                 f1 :<: g, f2 :<: g, f3 :<: g)-                => Const (f1 :+: f2 :+: f3) :-> Cxt h g Any a-injectConst3 = inject3 . hfmap (const undefined)--projectConst :: (HDifunctor g, g :<: f) => NatM Maybe (Cxt h f Any a) (Const g)-projectConst = fmap (hfmap (const (K ()))) . project- {-| This function injects a whole context into another context. -} injectCxt :: (HDifunctor g, g :<: f) => Cxt h g a (Cxt h f a b) :-> Cxt h f a b-injectCxt (Term t) = inject $ hfmap injectCxt t+injectCxt (In t) = inject $ hfmap injectCxt t injectCxt (Hole x) = x-injectCxt (Place p) = Place p+injectCxt (Var p) = Var p  {-| This function lifts the given functor to a context. -} liftCxt :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a b