compdata 0.7.0.2 → 0.8
raw patch · 91 files changed
+1185/−6093 lines, 91 filesdep +compdatadep +tree-viewdep ~base
Dependencies added: compdata, tree-view
Dependency ranges changed: base
Files
- benchmark/Benchmark.hs +2/−1
- benchmark/DataTypes/Comp.hs +2/−1
- benchmark/Functions/Comp/Desugar.hs +2/−1
- benchmark/Functions/Comp/Eval.hs +6/−5
- benchmark/Functions/Comp/FreeVars.hs +2/−1
- benchmark/Functions/Comp/HOAS.hs +54/−0
- benchmark/Functions/Comp/Inference.hs +2/−1
- compdata.cabal +87/−177
- examples/Examples/Automata.hs +147/−0
- examples/Examples/Automata/MHom.hs +229/−0
- examples/Examples/Automata/SimpComp.hs +79/−0
- examples/Examples/Automata/SimpComp2.hs +153/−0
- examples/Examples/Desugar.hs +1/−1
- examples/Examples/Eval.hs +1/−1
- examples/Examples/EvalM.hs +1/−1
- examples/Examples/MultiParam/FOL.hs +0/−436
- examples/Examples/MultiParam/Lambda.hs +0/−106
- examples/Examples/Param/Graph.hs +0/−77
- examples/Examples/Param/Lambda.hs +0/−131
- examples/Examples/Param/Names.hs +0/−113
- examples/Examples/Thunk.hs +83/−0
- src/Data/Comp/Algebra.hs +2/−0
- src/Data/Comp/Annotation.hs +2/−1
- src/Data/Comp/Automata.hs +3/−3
- src/Data/Comp/Derive/DeepSeq.hs +5/−7
- src/Data/Comp/Derive/Equality.hs +0/−1
- src/Data/Comp/Derive/HaskellStrict.hs +3/−2
- src/Data/Comp/Derive/Injections.hs +0/−82
- src/Data/Comp/Derive/Projections.hs +1/−1
- src/Data/Comp/Derive/Show.hs +45/−7
- src/Data/Comp/Derive/SmartAConstructors.hs +5/−5
- src/Data/Comp/Derive/Traversable.hs +3/−3
- src/Data/Comp/Desugar.hs +1/−1
- src/Data/Comp/Generic.hs +1/−1
- src/Data/Comp/MultiParam.hs +0/−34
- src/Data/Comp/MultiParam/Algebra.hs +0/−346
- src/Data/Comp/MultiParam/Annotation.hs +0/−81
- src/Data/Comp/MultiParam/Derive.hs +0/−55
- src/Data/Comp/MultiParam/Derive/Equality.hs +0/−78
- src/Data/Comp/MultiParam/Derive/HDifunctor.hs +0/−85
- src/Data/Comp/MultiParam/Derive/Injections.hs +0/−91
- src/Data/Comp/MultiParam/Derive/Ordering.hs +0/−93
- src/Data/Comp/MultiParam/Derive/Projections.hs +0/−108
- src/Data/Comp/MultiParam/Derive/Show.hs +0/−87
- src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs +0/−48
- src/Data/Comp/MultiParam/Derive/SmartConstructors.hs +0/−72
- src/Data/Comp/MultiParam/Desugar.hs +0/−44
- src/Data/Comp/MultiParam/Equality.hs +0/−64
- src/Data/Comp/MultiParam/FreshM.hs +0/−54
- src/Data/Comp/MultiParam/HDifunctor.hs +0/−40
- src/Data/Comp/MultiParam/HDitraversable.hs +0/−29
- src/Data/Comp/MultiParam/Ops.hs +0/−126
- src/Data/Comp/MultiParam/Ordering.hs +0/−67
- src/Data/Comp/MultiParam/Show.hs +0/−42
- src/Data/Comp/MultiParam/Sum.hs +0/−180
- src/Data/Comp/MultiParam/Term.hs +0/−123
- src/Data/Comp/Ops.hs +158/−20
- src/Data/Comp/Param.hs +0/−32
- src/Data/Comp/Param/Algebra.hs +0/−962
- src/Data/Comp/Param/Annotation.hs +0/−79
- src/Data/Comp/Param/Derive.hs +0/−57
- src/Data/Comp/Param/Derive/Difunctor.hs +0/−96
- src/Data/Comp/Param/Derive/Ditraversable.hs +0/−88
- src/Data/Comp/Param/Derive/Equality.hs +0/−84
- src/Data/Comp/Param/Derive/Injections.hs +0/−86
- src/Data/Comp/Param/Derive/Ordering.hs +0/−93
- src/Data/Comp/Param/Derive/Projections.hs +0/−101
- src/Data/Comp/Param/Derive/Show.hs +0/−92
- src/Data/Comp/Param/Derive/SmartAConstructors.hs +0/−47
- src/Data/Comp/Param/Derive/SmartConstructors.hs +0/−62
- src/Data/Comp/Param/Desugar.hs +0/−45
- src/Data/Comp/Param/Difunctor.hs +0/−36
- src/Data/Comp/Param/Ditraversable.hs +0/−28
- src/Data/Comp/Param/Equality.hs +0/−67
- src/Data/Comp/Param/FreshM.hs +0/−49
- src/Data/Comp/Param/Ops.hs +0/−127
- src/Data/Comp/Param/Ordering.hs +0/−77
- src/Data/Comp/Param/Show.hs +0/−41
- src/Data/Comp/Param/Sum.hs +0/−186
- src/Data/Comp/Param/Term.hs +0/−109
- src/Data/Comp/Param/Thunk.hs +0/−127
- src/Data/Comp/Render.hs +33/−0
- src/Data/Comp/Show.hs +5/−0
- src/Data/Comp/Sum.hs +39/−99
- src/Data/Comp/Term.hs +11/−1
- src/Data/Comp/Thunk.hs +13/−8
- testsuite/tests/Data/Comp/Examples/MultiParam.hs +0/−34
- testsuite/tests/Data/Comp/Examples/Param.hs +0/−38
- testsuite/tests/Data/Comp/Examples_Test.hs +1/−5
- testsuite/tests/Data/Comp/Variables_Test.hs +2/−2
- testsuite/tests/Test/Utils.hs +1/−1
benchmark/Benchmark.hs view
@@ -11,6 +11,7 @@ import Control.DeepSeq import Test.QuickCheck.Arbitrary import Test.QuickCheck.Gen+import Test.QuickCheck.Random import System.Random aExpr :: SugarExpr@@ -138,7 +139,7 @@ randStdBenchmarks :: Int -> IO Benchmark randStdBenchmarks s = do- rand <- newStdGen+ rand <- newQCGen let ty = unGen arbitrary rand s putStr "size of the type term: " print $ size ty
benchmark/DataTypes/Comp.hs view
@@ -7,7 +7,8 @@ TypeOperators, ScopedTypeVariables, TypeSynonymInstances,- DeriveFunctor#-}+ DeriveFunctor,+ ConstraintKinds #-} module DataTypes.Comp ( module DataTypes.Comp,
benchmark/Functions/Comp/Desugar.hs view
@@ -6,7 +6,8 @@ UndecidableInstances, TypeOperators, ScopedTypeVariables,- TypeSynonymInstances #-}+ TypeSynonymInstances,+ ConstraintKinds #-} module Functions.Comp.Desugar where
benchmark/Functions/Comp/Eval.hs view
@@ -6,7 +6,8 @@ UndecidableInstances, TypeOperators, ScopedTypeVariables,- TypeSynonymInstances #-}+ TypeSynonymInstances,+ ConstraintKinds #-} module Functions.Comp.Eval where @@ -14,7 +15,7 @@ import Functions.Comp.Desugar import Data.Comp import Data.Comp.Ops-import Data.Comp.Thunk+import Data.Comp.Thunk hiding (eval, eval2) import Data.Comp.Derive import Control.Monad import Data.Traversable@@ -30,9 +31,9 @@ $(derive [liftSum] [''EvalT]) instance (Monad m, Traversable v, Value :<: v) => EvalT Value v m where- evalTAlg = inject+ evalTAlg = injectT -instance (Value :<: v, Traversable v, EqF v, Monad m) => EvalT Op v m where+instance (Value :<: (m :+: v), 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@@ -65,7 +66,7 @@ ProjLeft -> x ProjRight -> y -instance (Value :<: v, Traversable v, Monad m) => EvalT Sugar v m where+instance (Value :<: (m :+: v), Value :<: v, Traversable v, Monad m) => EvalT Sugar v m where evalTAlg (Neg x) = thunk $ do VInt i <- whnfPr x return $ iVInt (-i)
benchmark/Functions/Comp/FreeVars.hs view
@@ -6,7 +6,8 @@ UndecidableInstances, TypeOperators, ScopedTypeVariables,- TypeSynonymInstances #-}+ TypeSynonymInstances,+ ConstraintKinds #-} module Functions.Comp.FreeVars where
+ benchmark/Functions/Comp/HOAS.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE+ TemplateHaskell,+ MultiParamTypeClasses,+ FlexibleInstances,+ FlexibleContexts,+ UndecidableInstances,+ TypeOperators,+ ScopedTypeVariables,+ TypeSynonymInstances #-}++module Functions.Comp.Desugar where++import DataTypes.Comp+import Data.Comp.ExpFunctor+import Data.Comp+import Data.Foldable+import Prelude hiding (foldr)++ex1 :: HOASExpr+ex1 = iLam (\x -> case project x of+ Just (VInt _) -> x + _ -> x `iPlus` x)+ex2 :: HOASExpr+ex2 = iLam (\x -> case x of+ Term t -> case proj t of+ Just (VInt _) -> x + _ -> x `iPlus` x)+ ++class Vars f where+ varsAlg :: Alg f Int++instance (Vars f, Vars g) => Vars (g :+: f) where+ varsAlg (Inl v) = varsAlg v+ varsAlg (Inr v) = varsAlg v++instance Vars Lam where+ varsAlg (Lam f) = f 1++instance Vars App where+ varsAlg = foldr (+) 0++instance Vars Value where+ varsAlg = foldr (+) 0++instance Vars Op where+ varsAlg = foldr (+) 0+++instance Vars Sugar where+ varsAlg = foldr (+) 0++vars :: (ExpFunctor f, Vars f) => Term f -> Int+vars = cataE varsAlg
benchmark/Functions/Comp/Inference.hs view
@@ -6,7 +6,8 @@ UndecidableInstances, TypeOperators, ScopedTypeVariables,- TypeSynonymInstances #-}+ TypeSynonymInstances,+ ConstraintKinds#-} module Functions.Comp.Inference where
compdata.cabal view
@@ -1,5 +1,5 @@ Name: compdata-Version: 0.7.0.2+Version: 0.8 Synopsis: Compositional Data Types Description: @@ -69,18 +69,6 @@ to families of mutually recursive data types and (more generally) GADTs. This extension resides in the module "Data.Comp.Multi". .- * /Parametric compositional data types/ (Workshop on Mathematically- Structured Functional Programming, 3-24, 2012,- <http://dx.doi.org/10.4204/EPTCS.76.3>). All of the above is also- lifted to parametric data types, which enables support for- parametric higher-order abstract syntax (PHOAS). This extension- resides in the module "Data.Comp.Param".- .- * /Generalised parametric compositional data types/. All of the above is also- lifted to generalised parametric data types, which enables support for- typed parametric higher-order abstract syntax (PHOAS). This extension- resides in the module "Data.Comp.MultiParam".- . * Advanced recursion schemes derived from tree automata. These recursion schemes allow for a higher degree of modularity and make it possible to apply fusion. See /Modular Tree Automata/@@ -90,8 +78,8 @@ 2013, <http://dx.doi.org/10.1145/2502488.2502489>). . - Examples of using (generalised) (parametric) compositional data types are- bundled with the package in the libray @examples@.+ Examples of using (generalised) compositional data types are bundled+ with the package in the folder @examples@. Category: Generics License: BSD3@@ -103,178 +91,97 @@ extra-source-files: -- test files- testsuite/tests/Data_Test.hs,- testsuite/tests/Data/Comp_Test.hs,- testsuite/tests/Data/Comp/Equality_Test.hs,- testsuite/tests/Data/Comp/Variables_Test.hs,- testsuite/tests/Data/Comp/Multi_Test.hs,- testsuite/tests/Data/Comp/Multi/Variables_Test.hs,- testsuite/tests/Data/Comp/Examples_Test.hs,- testsuite/tests/Data/Comp/Examples/Comp.hs,- testsuite/tests/Data/Comp/Examples/Multi.hs,- testsuite/tests/Data/Comp/Examples/Param.hs,- testsuite/tests/Data/Comp/Examples/MultiParam.hs,+ testsuite/tests/*.hs+ testsuite/tests/Data/*.hs+ testsuite/tests/Data/Comp/*.hs+ testsuite/tests/Data/Comp/Multi/*.hs+ testsuite/tests/Data/Comp/Examples/*.hs testsuite/tests/Test/Utils.hs -- benchmark files- benchmark/Test.hs- benchmark/Benchmark.hs- benchmark/DataTypes.hs- benchmark/Functions.hs- benchmark/DataTypes/Comp.hs- benchmark/DataTypes/Transform.hs- benchmark/DataTypes/Standard.hs- benchmark/Multi/DataTypes/Comp.hs- benchmark/Multi/Functions/Comp/Eval.hs- benchmark/Multi/Functions/Comp/Desugar.hs- benchmark/Transformations.hs- benchmark/Functions/Comp.hs- benchmark/Functions/Comp/Eval.hs- benchmark/Functions/Comp/Desugar.hs- benchmark/Functions/Comp/FreeVars.hs- benchmark/Functions/Comp/Inference.hs- benchmark/Functions/Standard/Eval.hs- benchmark/Functions/Standard/Desugar.hs- benchmark/Functions/Standard/FreeVars.hs- benchmark/Functions/Standard/Inference.hs- benchmark/Functions/Standard.hs+ benchmark/*.hs+ benchmark/DataTypes/*.hs+ benchmark/Functions/*.hs+ benchmark/Functions/Comp/*.hs+ benchmark/Functions/Standard/*.hs+ benchmark/Multi/DataTypes/*.hs+ benchmark/Multi/Functions/Comp/*.hs -- example files- examples/Examples/Common.hs- examples/Examples/Eval.hs- examples/Examples/EvalM.hs- examples/Examples/Desugar.hs- examples/Examples/Automata/Compiler.hs,- examples/Examples/Multi/Common.hs- examples/Examples/Multi/Eval.hs- examples/Examples/Multi/EvalI.hs- examples/Examples/Multi/EvalM.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+ examples/Examples/*.hs+ examples/Examples/Automata/*.hs+ examples/Examples/Multi/*.hs library- Exposed-Modules: Data.Comp,- Data.Comp.Annotation,- Data.Comp.Sum,- Data.Comp.Term,- Data.Comp.Algebra,- Data.Comp.Equality,- Data.Comp.Ordering,- Data.Comp.DeepSeq,+ Exposed-Modules: Data.Comp+ Data.Comp.Annotation+ Data.Comp.Sum+ Data.Comp.Term+ Data.Comp.Algebra+ Data.Comp.Equality+ Data.Comp.Ordering+ Data.Comp.DeepSeq Data.Comp.Generic- Data.Comp.TermRewriting,- Data.Comp.Arbitrary,- Data.Comp.Show,- Data.Comp.Variables,- Data.Comp.Decompose,- Data.Comp.Unification,- Data.Comp.Derive,- Data.Comp.Matching,- Data.Comp.Desugar,- Data.Comp.Automata,- Data.Comp.MacroAutomata,- Data.Comp.Automata.Product,- Data.Comp.Number,- Data.Comp.Thunk,- Data.Comp.Ops,+ Data.Comp.TermRewriting+ Data.Comp.Arbitrary+ Data.Comp.Show+ Data.Comp.Render+ Data.Comp.Variables+ Data.Comp.Decompose+ Data.Comp.Unification+ Data.Comp.Derive+ Data.Comp.Derive.Utils+ Data.Comp.Matching+ Data.Comp.Desugar+ Data.Comp.Automata+ Data.Comp.MacroAutomata+ Data.Comp.Automata.Product+ Data.Comp.Number+ Data.Comp.Thunk+ Data.Comp.Ops - Data.Comp.Multi,- Data.Comp.Multi.Term,- Data.Comp.Multi.Sum,- 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.Multi.Number,+ Data.Comp.Multi+ Data.Comp.Multi.Term+ Data.Comp.Multi.Sum+ 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.Multi.Number Data.Comp.Multi.Derive- Data.Comp.Multi.Generic,- Data.Comp.Multi.Desugar,-- Data.Comp.Param,- Data.Comp.Param.Term,- Data.Comp.Param.FreshM,- Data.Comp.Param.Sum,- Data.Comp.Param.Difunctor,- Data.Comp.Param.Ditraversable,- Data.Comp.Param.Algebra,- Data.Comp.Param.Annotation,- Data.Comp.Param.Ops- Data.Comp.Param.Equality- Data.Comp.Param.Ordering- Data.Comp.Param.Show- Data.Comp.Param.Derive,- Data.Comp.Param.Desugar- Data.Comp.Param.Thunk-- Data.Comp.MultiParam,- Data.Comp.MultiParam.Term,- Data.Comp.MultiParam.FreshM,- Data.Comp.MultiParam.Sum,- Data.Comp.MultiParam.HDifunctor,- Data.Comp.MultiParam.HDitraversable,- Data.Comp.MultiParam.Algebra,- Data.Comp.MultiParam.Annotation,- Data.Comp.MultiParam.Ops- Data.Comp.MultiParam.Equality- Data.Comp.MultiParam.Ordering- Data.Comp.MultiParam.Show- Data.Comp.MultiParam.Derive,- Data.Comp.MultiParam.Desugar+ Data.Comp.Multi.Generic+ Data.Comp.Multi.Desugar - Other-Modules: Data.Comp.Derive.Utils,- Data.Comp.Derive.Equality,- Data.Comp.Derive.Ordering,- Data.Comp.Derive.Arbitrary,- Data.Comp.Derive.Show,- Data.Comp.Derive.DeepSeq,- Data.Comp.Derive.SmartConstructors,- Data.Comp.Derive.SmartAConstructors,- Data.Comp.Derive.Foldable,- Data.Comp.Derive.Traversable,- Data.Comp.Derive.Injections,- Data.Comp.Derive.Projections,- Data.Comp.Derive.HaskellStrict,- Data.Comp.Automata.Product.Derive,+ Other-Modules: Data.Comp.Derive.Equality+ Data.Comp.Derive.Ordering+ Data.Comp.Derive.Arbitrary+ Data.Comp.Derive.Show+ Data.Comp.Derive.DeepSeq+ Data.Comp.Derive.SmartConstructors+ Data.Comp.Derive.SmartAConstructors+ Data.Comp.Derive.Foldable+ Data.Comp.Derive.Traversable+ Data.Comp.Derive.Projections+ Data.Comp.Derive.HaskellStrict+ Data.Comp.Automata.Product.Derive - 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.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- Data.Comp.Multi.Derive.Injections,- Data.Comp.Multi.Derive.Projections,-- Data.Comp.Param.Derive.Difunctor,- Data.Comp.Param.Derive.Ditraversable,- Data.Comp.Param.Derive.Equality,- Data.Comp.Param.Derive.Ordering,- Data.Comp.Param.Derive.Show,- Data.Comp.Param.Derive.SmartConstructors,- Data.Comp.Param.Derive.SmartAConstructors,- Data.Comp.Param.Derive.Injections,- Data.Comp.Param.Derive.Projections,-- Data.Comp.MultiParam.Derive.HDifunctor,- Data.Comp.MultiParam.Derive.Equality,- Data.Comp.MultiParam.Derive.Ordering,- Data.Comp.MultiParam.Derive.Show,- Data.Comp.MultiParam.Derive.SmartConstructors,- Data.Comp.MultiParam.Derive.SmartAConstructors,- Data.Comp.MultiParam.Derive.Injections,- Data.Comp.MultiParam.Derive.Projections+ Data.Comp.Multi.Derive.Injections+ Data.Comp.Multi.Derive.Projections - Build-Depends: base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, th-expand-syns, transformers+ Build-Depends: base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive,+ deepseq, th-expand-syns, transformers, tree-view hs-source-dirs: src ghc-options: -W @@ -282,8 +189,10 @@ Test-Suite test Type: exitcode-stdio-1.0 Main-is: Data_Test.hs- hs-source-dirs: src testsuite/tests examples- Build-Depends: base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers+ hs-source-dirs: testsuite/tests examples+ Build-Depends: compdata, base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, + HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive,+ th-expand-syns, deepseq, transformers Benchmark algebra Type: exitcode-stdio-1.0@@ -301,7 +210,8 @@ ghc-options: -W -O2 -- Disable short-cut fusion rules in order to compare optimised and unoptimised code. cpp-options: -DNO_RULES- Build-Depends: base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers+ Build-Depends: base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, + deepseq, criterion, random, uniplate, th-expand-syns, transformers source-repository head
+ examples/Examples/Automata.hs view
@@ -0,0 +1,147 @@+{-# LANGUAGE RankNTypes #-}+--------------------------------------------------------------------------------+-- |+-- Module : Examples.Automata+-- Copyright : (c) 2010-2011 Patrick Bahr+-- License : BSD3+-- Maintainer : Patrick Bahr <paba@diku.dk>+-- Stability : experimental+-- Portability : non-portable (GHC Extensions)+--+-- This module defines tree automata based on compositional data types.+--+--------------------------------------------------------------------------------++module Examples.Automata where++import Data.Comp+import Data.Maybe+import Data.Traversable+import Control.Monad+++{-| This type represents transition functions of deterministic+bottom-up tree acceptors (DUTAs). -}++type DUTATrans f q = Alg f q++{-| This data type represents deterministic bottom-up tree acceptors (DUTAs).+-}+data DUTA f q = DUTA {+ dutaTrans :: DUTATrans f q,+ dutaAccept :: q -> Bool+ }++{-| This function runs the transition function of a DUTA on the given+term. -}++runDUTATrans :: Functor f => DUTATrans f q -> Term f -> q+runDUTATrans = cata++{-| This function checks whether a given DUTA accepts a term. -}++duta :: Functor f => DUTA f q -> Term f -> Bool+duta DUTA{dutaTrans = trans, dutaAccept = accept} = accept . runDUTATrans trans++++{-| This type represents transition functions of non-deterministic+bottom-up tree acceptors (NUTAs). -}++type NUTATrans f q = AlgM [] f q+++{-| This type represents non-deterministic bottom-up tree acceptors.+-}+data NUTA f q = NUTA {+ nutaTrans :: AlgM [] f q,+ nutaAccept :: q -> Bool+ }++{-| This function runs the given transition function of a NUTA on the+given term -}++runNUTATrans :: Traversable f => NUTATrans f q -> Term f -> [q]+runNUTATrans = cataM++{-| This function checks whether a given NUTA accepts a term. -}++nuta :: Traversable f => NUTA f q -> Term f -> Bool+nuta NUTA{nutaTrans = trans, nutaAccept = accept} = any accept . runNUTATrans trans+++{-| This function determinises the given NUTA. -}++determNUTA :: (Traversable f) => NUTA f q -> DUTA f [q]+determNUTA n = DUTA{+ dutaTrans = algM $ nutaTrans n,+ dutaAccept = any $ nutaAccept n}++{-| This function represents transition functions of+deterministic bottom-up tree transducers (DUTTs). -}++type DUTTTrans f g q = forall a. f (q,a) -> (q, Cxt Hole g a)++{-| This function transforms a DUTT transition function into an+algebra. -}++duttTransAlg :: (Functor f, Functor g) => DUTTTrans f g q -> Alg f (q, Term g)+duttTransAlg trans = fmap injectCxt . trans ++{-| This function runs the given DUTT transition function on the given+term. -}++runDUTTTrans :: (Functor f, Functor g) => DUTTTrans f g q -> Term f -> (q, Term g)+runDUTTTrans = cata . duttTransAlg++{-| This data type represents deterministic bottom-up tree+transducers. -}++data DUTT f g q = DUTT {+ duttTrans :: DUTTTrans f g q,+ duttAccept :: q -> Bool+ }++{-| This function transforms the given term according to the given+DUTT and returns the resulting term provided it is accepted by the+DUTT. -}++dutt :: (Functor f, Functor g) => DUTT f g q -> Term f -> Maybe (Term g)+dutt DUTT{duttTrans = trans, duttAccept = accept} = accept' . runDUTTTrans trans+ where accept' (q,res)+ | accept q = Just res+ | otherwise = Nothing++{-| This type represents transition functions of non-deterministic+bottom-up tree transducers (NUTTs). -}++type NUTTTrans f g q = forall a. f (q,a) -> [(q, Cxt Hole g a)]++{-| This function transforms a NUTT transition function into a monadic+algebra. -}++nuttTransAlg :: (Functor f, Functor g) => NUTTTrans f g q -> AlgM [] f (q, Term g)+nuttTransAlg trans = liftM (fmap injectCxt) . trans ++{-| This function runs the given NUTT transition function on the given+term. -}++runNUTTTrans :: (Traversable f, Functor g) => NUTTTrans f g q -> Term f -> [(q, Term g)]+runNUTTTrans = cataM . nuttTransAlg++{-| This data type represents non-deterministic bottom-up tree+transducers (NUTTs). -}++data NUTT f g q = NUTT {+ nuttTrans :: NUTTTrans f g q,+ nuttAccept :: q -> Bool+ }++{-| This function transforms the given term according to the given+NUTT and returns a list containing all accepted results. -}++nutt :: (Traversable f, Functor g) => NUTT f g q -> Term f -> [Term g]+nutt NUTT{nuttTrans = trans, nuttAccept = accept} = mapMaybe accept' . runNUTTTrans trans+ where accept' (q,res)+ | accept q = Just res+ | otherwise = Nothing
+ examples/Examples/Automata/MHom.hs view
@@ -0,0 +1,229 @@+{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances,+ FlexibleContexts, UndecidableInstances, TypeOperators,+ ImplicitParams, GADTs, IncoherentInstances, ScopedTypeVariables,+ TupleSections #-}+--------------------------------------------------------------------------------+-- |+-- Module : Examples.MHom+-- Copyright : (c) 2011 Patrick Bahr+-- License : BSD3+-- Maintainer : Patrick Bahr <paba@diku.dk>+-- Stability : experimental+-- Portability : non-portable (GHC Extensions)+--+--+--------------------------------------------------------------------------------++module Examples.Automata.MHom+ ( module Examples.Automata.MHom+ , module Data.Stream ) where++import Data.Comp.Zippable+import Data.Comp+import Data.Comp.Ops+import Data.Stream (Stream(..), (<:>))+import Data.Comp.Show ()+import Data.Map (Map)+import qualified Data.Map as Map+import Control.Monad+import Control.Arrow (first, (&&&))+import Data.Comp.Derive++-- | An instance @a :< b@ means that @a@ is a component of @b@. @a@+-- can be extracted from @b@ via the method 'ex'.+class p :< q where+ pr :: q a -> p a+ up :: p a -> q a -> q a++instance q :< q where+ pr = id+ up = const++instance p :< p :*: q where+ pr = ffst+ up x (_ :*: y) = x :*: y++instance (p :< q) => p :< (p' :*: q) where+ pr = pr . fsnd+ up y (x :*: y') = x :*: up y y'++-- | This function provides access to components of the states from+-- "below".+below :: (?below :: i -> q a, p :< q) => i -> p a+below = pr . ?below++-- | This function provides access to components of the state from+-- "above"+above :: (?above :: q a, p :< q) => p a+above = pr ?above++hole :: (?get :: i -> a) => i -> Context f a+hole = Hole . ?get++-- | Turns the explicit parameters @?above@ and @?below@ into explicit+-- ones.+explicit :: q a -> (i -> q a) -> (i -> a)+ -> ((?get :: i -> a, ?below :: i -> q a, ?above :: q a) => b) -> b+explicit ab bel get x = x+ where ?above = ab+ ?below = bel+ ?get = get+-- | This type represents generalised term homomorphisms. Generalised+-- term homomorphisms have access to a state that is provided+-- (separately) by a DUTA or a DDTA (or both).+type MHom q f g = forall a i . (?get :: i -> a, ?below :: i -> q a, ?above :: q a)+ => f i -> Context g a+++-- | This type represents transition functions of deterministic+-- bottom-up tree transducers (DUTTs).++type UpTrans q f g = forall a. f (q a,a) -> (q (Context g a), Context g a)++-- | This function transforms DUTT transition function into an+-- algebra.+upAlg :: (Functor g, Functor q) => UpTrans q f g -> Alg f (q (Term g), Term g)+upAlg trans t = let (q , c) = trans t+ in (fmap appCxt q, appCxt c)+++-- | This function runs the given DUTT on the given term.++runUpTrans :: (Functor f, Functor g, Functor q) => UpTrans q f g -> Term f -> (q (Term g), Term g)+runUpTrans = cata . upAlg++-- | This function generalises 'runUpTrans' to contexts. Therefore,+-- additionally, a transition function for the holes is needed.+runUpTrans' :: (Functor f, Functor g, Functor q)+ => UpTrans q f g -> Context f (q a,a) -> (q (Context g a), Context g a)+runUpTrans' trans = run where+ run (Hole (q,a)) = (fmap Hole q, Hole a)+ run (Term t) = let (q, c) = trans $ fmap run t+ in (fmap appCxt q, appCxt c)++-- | This function composes two DUTTs. (I'm not sure whether it is correct, yet.)+compUpTrans :: (Functor f, Functor g, Functor h, Functor q1, Functor q2)+ => UpTrans q2 g h -> UpTrans q1 f g -> UpTrans (q1 :*: q2) f h+compUpTrans t2 t1 x = (q1' :*: q2, c2) where+ (q1, c1) = t1 $ fmap shuffle x+ shuffle (q1 :*: q2,a) = (fmap (q2,) q1 ,(q2,a) )+ q1' = fmap (snd . runUpTrans' t2) q1+ (q2, c2) = runUpTrans' t2 c1++-- | This type represents transition functions of deterministic+-- bottom-up tree acceptors (DUTAs).+type UpState f q = forall a . f (q a, a) -> q a++-- | This combinator runs the given DUTA on a term returning the final+-- state of the run.+runUpState :: (Functor f) => UpState f q -> Term f -> q (Term f)+runUpState st = run where+ run (Term t) = st $ fmap (\ s -> (run s, s)) t+++-- | This function combines the product DUTA of the two given DUTAs.+prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p :*:q)+prodUpState sp sq t = p :*: q where+ p = sp $ fmap (first ffst) t+ q = sq $ fmap (first fsnd) t++-- | This function turns constructs a DUTT from a given macro term+-- homomorphism with the state propagated by the given DUTA.+toUpTrans :: (Functor f, Functor g, Functor q)+ => UpState f q -> MHom q f g -> UpTrans q f g+toUpTrans st f t = (fmap Hole q, c)+ where q = st t+ c = explicit q (pr . fst) snd f t++-- | This function applies a given generalised term homomorphism with+-- a state space propagated by the given DUTA to a term.+upHom :: (Functor f, Functor g, Functor q) => UpState f q -> MHom q f g -> Term f -> (q (Term g),Term g)+upHom alg h = runUpTrans (toUpTrans alg h)++-- | This type represents transition functions of generalised+-- deterministic bottom-up tree acceptors (GDUTAs) which have access+-- to an extended state space.+type GUpState f q p = forall a i . (?get :: i -> a, ?below :: i -> p a, ?above :: p a, q :< p) => f i -> q a++-- | This combinator turns an arbitrary DUTA into a GDUTA.+gUpState :: Functor f => UpState f q -> GUpState f q p+gUpState f = f . fmap (below &&& (?get))++-- | This combinator turns a GDUTA with the smallest possible state+-- space into a DUTA.+upState :: GUpState f q q -> UpState f q+upState f s = let res = explicit res fst snd f s in res++-- | This combinator runs a GDUTA on a term.+runGUpState :: Functor f => GUpState f q q -> Term f -> q (Term f)+runGUpState s = runUpState (upState s)++-- | This combinator constructs the product of two GDUTA.+prodGUpState :: (p :< pq, q :< pq)+ => GUpState f p pq -> GUpState f q pq -> GUpState f (p :*: q) pq+prodGUpState sp sq t = sp t :*: sq t++-- | This type represents transition functions of deterministic+-- top-down tree transducers (DDTTs).++type DownTrans q f g = forall a. (q a, f a) -> Context g (q (Context f a),a)++-- | This function runs the given DDTT on the given tree.+runDownTrans :: (Functor f, Functor g, Functor q) => DownTrans q f g -> q (Cxt h g a) -> Cxt h f a -> Cxt h g a+runDownTrans tr q t = run (q,t) where+ run (q,Term t) = appCxt $ fmap (\(q,a) -> run (fmap appCxt q,a)) $ tr (q, t)+ run (_,Hole a) = Hole a++-- | This function runs the given DDTT on the given tree.+runDownTrans' :: (Functor f, Functor g, Functor q) => DownTrans q f g -> q (Cxt h f a)+ -> Cxt h f a -> Cxt h g (q (Cxt h f a),a)+runDownTrans' tr q t = run (q,t) where+ run (q,Term t) = appCxt $ fmap (\(q,a) -> run (fmap appCxt q,a)) $ tr (q, t)+ run (q,Hole a) = Hole (q,a)++-- | This function composes two DDTTs. (not implemented yet)+compDownTrans :: (Functor f, Functor g, Functor h)+ => DownTrans p g h -> DownTrans q f g -> DownTrans (q :*:p) f h+compDownTrans = undefined++-- | This type represents transition functions of deterministic+-- top-down tree acceptors (DDTAs).+type DownState f q = forall a i. Ord i => (q a, f (i,a)) -> Map i (q a)++-- | This function constructs the product DDTA of the given two DDTAs.+prodDownState :: DownState f p -> DownState f q -> DownState f (p :*: q)+prodDownState sp sq (p :*: q,t) = prodMap p q (sp (p, t)) (sq (q, t))++++-- | This type is needed to construct the product of two DDTAs.+data ProdState p q = LState p+ | RState q+ | BState p q+-- | This function constructs the pointwise product of two maps each+-- with a default value.+prodMap :: (Ord i) => p a -> q a -> Map i (p a) -> Map i (q a) -> Map i ((p :*: q) a)+prodMap p q mp mq = Map.map final $ Map.unionWith combine ps qs+ where ps = Map.map LState mp+ qs = Map.map RState mq+ combine (LState p) (RState q) = BState p q+ combine (RState q) (LState p) = BState p q+ combine _ _ = error "unexpected merging"+ final (LState p) = p :*: q+ final (RState q) = p :*: q+ final (BState p q) = p :*: q++-- | Apply the given state mapping to the given functorial value by+-- adding the state to the corresponding index if it is in the map and+-- otherwise adding the provided default state.+appMap :: Zippable f => DownState f q -> q a -> f a -> f (q a,a)+appMap qmap q s = fmap qfun s'+ where s' = number' s+ mapping = qmap (q,s')+ qfun (k,a) = (Map.findWithDefault q k mapping ,a)++-- -- | This function constructs a DDTT from a given stateful term+-- -- homomorphism with the state propagated by the given DDTA.+-- toDownTrans :: (Zippable f, Functor q) => DownState f q -> MHom q f g -> DownTrans q f g+-- toDownTrans st f (q, s) = fmap mkQCxt $ explicit q fst id f (appMap st q s)+-- where mkQCxt (q,a) = (fmap Hole q, a)
+ examples/Examples/Automata/SimpComp.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses,+ TypeOperators, FlexibleInstances, UndecidableInstances,+ ScopedTypeVariables, TypeSynonymInstances, RankNTypes #-}++module Examples.Automata.Compiler where+++import Data.Comp.Automata hiding (DUpState, (<*>), runDUpState, dUpState)+import Data.Comp.Zippable+import Data.Comp.Derive+import Data.Comp.Ops+import Data.Comp hiding (height)+import Prelude hiding (foldl)++++type Var = String++data Sig a = Const Int | Plus a a+data Let a = Let Var a a+ | Var Var+++$(derive [makeFunctor, makeFoldable, smartConstructors, makeShowF] [''Sig, ''Let])++instance Zippable Sig where+ fzip _ (Const i) = Const i+ fzip (Cons a (Cons b _)) (Plus x y) = Plus (a,x) (b,y)++instance Zippable Let where+ fzip (Cons a (Cons b _)) (Let v x y) = Let v (a,x) (b,y)+ fzip _ (Var v) = Var v+++instance (Zippable f, Zippable g) => Zippable (f :+: g) where+ fzip x (Inl v) = Inl $ fzip x v+ fzip x (Inr v) = Inr $ fzip x v++evalSt :: UpState Sig Int+evalSt (Const i) = i+evalSt (Plus x y) = x + y++type Addr = Int++data Instr = Acc Int+ | Load Addr+ | Store Addr+ | Add Addr+ deriving (Show)++type Code = [Instr]++++type DUpState f q p = (q :< p) => f p -> q++dUpState :: Functor f => UpState f q -> DUpState f q p+dUpState st = st . fmap pr+++heightSt :: UpState Sig Int+heightSt (Const _) = 0+heightSt (Plus x y) = 1 + max x y++codeSt :: (Int :< q) => DUpState Sig Code q+codeSt (Const x) = [Acc x]+codeSt (Plus x y) = pr x ++ [Store a] ++ pr y ++ [Add a] where a = pr y++-- | This combinator constructs the product of two GDUTA.+(<*>) :: (p :< pq, q :< pq)+ => DUpState f p pq -> DUpState f q pq -> DUpState f (p,q) pq+(sp <*> sq) t = (sp t, sq t)+ +runDUpState :: Functor f => DUpState f q q -> Term f -> q+runDUpState = cata++code :: Term Sig -> Code+code = fst . runDUpState (codeSt <*> dUpState heightSt)+
+ examples/Examples/Automata/SimpComp2.hs view
@@ -0,0 +1,153 @@+{-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses,+ TypeOperators, FlexibleInstances, UndecidableInstances,+ ScopedTypeVariables, TypeSynonymInstances, RankNTypes, ImplicitParams, DeriveDataTypeable #-}++module Examples.Automata.Compiler where++import Data.Comp.Automata+import Data.Comp.Zippable+import Data.Comp.Derive+import Data.Comp.Ops+import Data.Comp hiding (height)+import Data.Foldable+import Prelude hiding (foldl)++import Data.Set (Set, union, singleton, delete, member)+import qualified Data.Set as Set++import Data.Map (Map)+import qualified Data.Map as Map+++++type Var = String++data Sig e = Const Int | Plus e e | LetIn Var e e | Var Var+++$(derive [makeFunctor, makeFoldable, smartConstructors, makeShowF] [''Sig])++instance Zippable Sig where+ fzip _ (Const i) = Const i+ fzip (Cons a (Cons b _)) (Plus x y) = Plus (a,x) (b,y)+ fzip (Cons a (Cons b _)) (LetIn v x y) = LetIn v (a,x) (b,y)+ fzip _ (Var v) = Var v+++instance (Zippable f, Zippable g) => Zippable (f :+: g) where+ fzip x (Inl v) = Inl $ fzip x v+ fzip x (Inr v) = Inr $ fzip x v++-- evalSt :: UpState Sig Int+-- evalSt (Const i) = i+-- evalSt (Plus x y) = x + y++type Addr = Int++data Instr = Acc Int+ | Load Addr+ | Store Addr+ | Add Addr+ deriving (Show)++type Code = [Instr]++++-- heightSt :: UpState Sig Int+-- heightSt (Const _) = 0+-- heightSt (Plus x y) = 1 + max x y+-- heightSt (LetIn _ e b) = 1 + max e b+-- heightSt (Var _) = 0++-- codeSt :: (Int :< q) => DUpState Sig q Code +-- codeSt (Const x) = [Acc x]+-- codeSt (Plus x y) = below x ++ [Store a] ++ below y ++ [Add a] where a = below y+++-- code :: Term Sig -> Code+-- code = fst . runDUpState (codeSt <*> dUpState heightSt)+++type Vars = Set Var++fvSt :: UpState Sig Vars+fvSt (Var v) = singleton v+fvSt (LetIn v e b) | v `member` b = e `union` delete v b+ | otherwise = delete v b+fvSt t = foldl union Set.empty t++-- | Stateful homomorphism that removes unnecessary let bindings.+remLetHom :: (Vars :< q) => QHom Sig q Sig+remLetHom (LetIn v _ y) | not (v `Set.member` below y) = Hole y+remLetHom t = simpCxt t++remLet :: Term Sig -> Term Sig+remLet = runUpHom fvSt remLetHom++ldepthSt :: DownState Sig Int+ldepthSt (d,LetIn _ _ b) = b |-> d + 1+ldepthSt _ = o++type Ren = Map Var Var+++newVar :: (?above :: q, Int :< q) => Var+newVar = show (above :: Int)++renSt :: (Int :< q) => DDownState Sig q Ren+renSt (LetIn v _ b) = b |-> (v |-> newVar & above)+renSt _ = o++renameHom :: (Ren :< q, Int :< q) => QHom Sig q Sig+renameHom (LetIn _ a b) = iLetIn newVar (Hole a) (Hole b)+renameHom (Var v) = case Map.lookup v above of+ Nothing -> iVar v+ Just v' -> iVar v'+renameHom t = simpCxt t++renameInit :: (Ren, Int)+renameInit = (o, 0)++rename :: Term Sig -> Term Sig+rename = runDownHom (downState (renSt >*< dDownState ldepthSt))+ renameHom renameInit+++heightSt :: Foldable f => UpState f Int+heightSt t = foldl max 0 t + 1++newtype Height = Height {height :: Int}++heightSt' :: (Functor f,Foldable f) => UpState f Height+heightSt' = tagUpState Height height heightSt+++newtype Depth = Depth {depth :: Int}++ldepthSt' :: DownState Sig Depth+ldepthSt' = tagDownState Depth depth ldepthSt++type Bind = Map Var Int++bindSt :: (Depth :< q) => DDownState Sig q Bind +bindSt (LetIn v _ e) = e |-> (v |-> 2 * depth above & above)+bindSt _ = o++codeSt :: (Height :< q, Depth :< q, Bind :< q) => DUpState Sig q Code +codeSt (Const x) = [Acc x]+codeSt (Plus x y) = below x ++ [Store a] ++ below y ++ [Add a] + where a = 2 * height (below y) + 1+codeSt (LetIn _ b e) = below b ++ [Store a] ++ below e+ where a = 2 * depth above+codeSt (Var v) = case Map.lookup v above of+ Nothing -> error $ "unbound variable " ++ v+ Just i -> [Load i]+++code :: Term Sig -> (Code, Height)+code = runDState + (codeSt <*> dUpState heightSt')+ (bindSt >*< dDownState ldepthSt')+ (o :: Bind, Depth 0)
examples/Examples/Desugar.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances,- OverlappingInstances #-}+ OverlappingInstances, ConstraintKinds #-} -------------------------------------------------------------------------------- -- | -- Module : Examples.Desugar
examples/Examples/Eval.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances,- OverlappingInstances #-}+ OverlappingInstances, ConstraintKinds #-} -------------------------------------------------------------------------------- -- | -- Module : Examples.Eval
examples/Examples/EvalM.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances,- OverlappingInstances #-}+ OverlappingInstances, ConstraintKinds #-} -------------------------------------------------------------------------------- -- | -- Module : Examples.EvalM
− examples/Examples/MultiParam/FOL.hs
@@ -1,436 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, FlexibleInstances,- FlexibleContexts, UndecidableInstances, GADTs, KindSignatures,- OverlappingInstances, TypeSynonymInstances, EmptyDataDecls #-}------------------------------------------------------------------------------------ |--- Module : Examples.MultiParam.FOL--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ First-Order Logic a la Carte------ This example illustrates how to implement First-Order Logic a la Carte--- (Knowles, The Monad.Reader Issue 11, '08) using Generalised Parametric--- Compositional Data Types.------ Rather than using a fixed domain 'Term' for binders as Knowles, our encoding--- uses a mutually recursive data structure for terms and formulae. This makes--- terms modular too, and hence we only introduce variables when they are--- actually needed in stage 5.--------------------------------------------------------------------------------------module Examples.MultiParam.FOL where--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 (Name, withName, evalFreshM)-import Data.List (intercalate)-import Data.Maybe-import Control.Monad.State-import Control.Monad.Reader---- Phantom types indicating whether a (recursive) term is a formula or a term-data TFormula-data TTerm---- Terms-data Const :: (* -> *) -> (* -> *) -> * -> * where- Const :: String -> [e TTerm] -> Const a e TTerm-data Var :: (* -> *) -> (* -> *) -> * -> * where- Var :: String -> Var a e TTerm---- Formulae-data TT :: (* -> *) -> (* -> *) -> * -> * where- TT :: TT a e TFormula-data FF :: (* -> *) -> (* -> *) -> * -> * where- FF :: FF a e TFormula-data Atom :: (* -> *) -> (* -> *) -> * -> * where- Atom :: String -> [e TTerm] -> Atom a e TFormula-data NAtom :: (* -> *) -> (* -> *) -> * -> * where- NAtom :: String -> [e TTerm] -> NAtom a e TFormula-data Not :: (* -> *) -> (* -> *) -> * -> * where- Not :: e TFormula -> Not a e TFormula-data Or :: (* -> *) -> (* -> *) -> * -> * where- Or :: e TFormula -> e TFormula -> Or a e TFormula-data And :: (* -> *) -> (* -> *) -> * -> * where- And :: e TFormula -> e TFormula -> And a e TFormula-data Impl :: (* -> *) -> (* -> *) -> * -> * where- Impl :: e TFormula -> e TFormula -> Impl a e TFormula-data Exists :: (* -> *) -> (* -> *) -> * -> * where- Exists :: (a TTerm -> e TFormula) -> Exists a e TFormula-data Forall :: (* -> *) -> (* -> *) -> * -> * where- Forall :: (a TTerm -> e TFormula) -> Forall a e TFormula--$(derive [makeHDifunctor, smartConstructors]- [''Const, ''Var, ''TT, ''FF, ''Atom, ''NAtom,- ''Not, ''Or, ''And, ''Impl, ''Exists, ''Forall])------------------------------------------------------------------------------------- (Custom) pretty printing of terms and formulae-----------------------------------------------------------------------------------instance ShowHD Const where- showHD (Const f t) = do ts <- mapM unK t- return $ f ++ "(" ++ intercalate ", " ts ++ ")"--instance ShowHD Var where- showHD (Var x) = return x--instance ShowHD TT where- showHD TT = return "true"--instance ShowHD FF where- showHD FF = return "false"--instance ShowHD Atom where- showHD (Atom p t) = do ts <- mapM unK t- return $ p ++ "(" ++ intercalate ", " ts ++ ")"--instance ShowHD NAtom where- showHD (NAtom p t) = do ts <- mapM unK t- return $ "not " ++ p ++ "(" ++ intercalate ", " ts ++ ")"--instance ShowHD Not where- showHD (Not (K f)) = liftM (\x -> "not (" ++ x ++ ")") f--instance ShowHD Or where- showHD (Or (K f1) (K f2)) =- liftM2 (\x y -> "(" ++ x ++ ") or (" ++ y ++ ")") f1 f2--instance ShowHD And where- showHD (And (K f1) (K f2)) =- liftM2 (\x y -> "(" ++ x ++ ") and (" ++ y ++ ")") f1 f2--instance ShowHD Impl where- showHD (Impl (K f1) (K f2)) =- liftM2 (\x y -> "(" ++ x ++ ") -> (" ++ y ++ ")") f1 f2--instance ShowHD Exists where- showHD (Exists f) =- withName (\x -> do b <- unK (f x)- return $ "exists " ++ show x ++ ". " ++ b)--instance ShowHD Forall where- showHD (Forall f) =- withName (\x -> do b <- unK (f x)- return $ "forall " ++ show x ++ ". " ++ b)------------------------------------------------------------------------------------- Stage 0-----------------------------------------------------------------------------------type Input = Const :+:- TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Impl :+:- Exists :+: Forall--foodFact :: Term Input TFormula-foodFact = Term $- iExists (\p -> iAtom "Person" [p] `iAnd`- iForall (\f -> iAtom "Food" [f] `iImpl`- iAtom "Eats" [p,f])) `iImpl`- iNot (iExists $ \f -> iAtom "Food" [f] `iAnd`- iNot (iExists $ \p -> iAtom "Person" [p] `iAnd`- iAtom "Eats" [p,f]))------------------------------------------------------------------------------------- Stage 1: Eliminate Implications-----------------------------------------------------------------------------------type Stage1 = Const :+:- TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Exists :+: Forall--class HDifunctor f => ElimImp f where- elimImpHom :: Hom f Stage1--$(derive [liftSum] [''ElimImp])--elimImp :: Term Input :-> Term Stage1-elimImp (Term t) = Term (appHom elimImpHom t)--instance (HDifunctor f, f :<: Stage1) => ElimImp f where- elimImpHom = simpCxt . inj--instance ElimImp Impl where- elimImpHom (Impl f1 f2) = iNot (Hole f1) `iOr` (Hole f2)--foodFact1 :: Term Stage1 TFormula-foodFact1 = elimImp foodFact------------------------------------------------------------------------------------- Stage 2: Move Negation Inwards-----------------------------------------------------------------------------------type Stage2 = Const :+:- TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Exists :+: Forall--class HDifunctor f => Dualize f where- dualizeHom :: f a (Cxt h Stage2 a b) :-> Cxt h Stage2 a b--$(derive [liftSum] [''Dualize])--dualize :: Trm Stage2 a :-> Trm Stage2 a-dualize = appHom (dualizeHom . hfmap Hole)--instance Dualize Const where- dualizeHom (Const f t) = iConst f t--instance Dualize TT where- dualizeHom TT = iFF--instance Dualize FF where- dualizeHom FF = iTT--instance Dualize Atom where- dualizeHom (Atom p t) = iNAtom p t--instance Dualize NAtom where- dualizeHom (NAtom p t) = iAtom p t--instance Dualize Or where- dualizeHom (Or f1 f2) = f1 `iAnd` f2--instance Dualize And where- dualizeHom (And f1 f2) = f1 `iOr` f2--instance Dualize Exists where- dualizeHom (Exists f) = inject $ Forall f--instance Dualize Forall where- dualizeHom (Forall f) = inject $ Exists f--class PushNot f where- pushNotAlg :: Alg f (Trm Stage2 a)--$(derive [liftSum] [''PushNot])--pushNotInwards :: Term Stage1 :-> Term Stage2-pushNotInwards t = Term (cata pushNotAlg t)--instance (HDifunctor f, f :<: Stage2) => PushNot f where- pushNotAlg = inject . hdimap MP.Var id -- default--instance PushNot Not where- pushNotAlg (Not f) = dualize f--foodFact2 :: Term Stage2 TFormula-foodFact2 = pushNotInwards foodFact1------------------------------------------------------------------------------------- Stage 4: Skolemization-----------------------------------------------------------------------------------type Stage4 = Const :+:- TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Forall--type Unique = Int-data UniqueSupply = UniqueSupply Unique UniqueSupply UniqueSupply--initialUniqueSupply :: UniqueSupply-initialUniqueSupply = genSupply 1- where genSupply n = UniqueSupply n (genSupply (2 * n))- (genSupply (2 * n + 1))--splitUniqueSupply :: UniqueSupply -> (UniqueSupply, UniqueSupply)-splitUniqueSupply (UniqueSupply _ l r) = (l,r)--getUnique :: UniqueSupply -> (Unique, UniqueSupply)-getUnique (UniqueSupply n l _) = (n,l)--type Supply = State UniqueSupply-type S a = ReaderT [Trm Stage4 a TTerm] Supply--evalS :: S a b -> [Trm Stage4 a TTerm] -> UniqueSupply -> b-evalS m env = evalState (runReaderT m env)--fresh :: S a Int-fresh = do supply <- get- let (uniq,rest) = getUnique supply- put rest- return uniq--freshes :: S a UniqueSupply-freshes = do supply <- get- let (l,r) = splitUniqueSupply supply- put r- return l--class Skolem f where- skolemAlg :: AlgM' (S a) f (Trm Stage4 a)--$(derive [liftSum] [''Skolem])--skolemize :: Term Stage2 :-> Term Stage4-skolemize f = Term (evalState (runReaderT (cataM' skolemAlg f) [])- initialUniqueSupply)--instance Skolem Const where- skolemAlg (Const f t) = liftM (iConst f) $ mapM getCompose t--instance Skolem TT where- skolemAlg TT = return iTT--instance Skolem FF where- skolemAlg FF = return iFF--instance Skolem Atom where- skolemAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t--instance Skolem NAtom where- skolemAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t--instance Skolem Or where- skolemAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2--instance Skolem And where- skolemAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2--instance Skolem Forall where- skolemAlg (Forall f) = do- supply <- freshes- xs <- ask- return $ iForall $ \x -> evalS (getCompose $ f x) (x : xs) supply--instance Skolem Exists where- skolemAlg (Exists f) = do- uniq <- fresh- xs <- ask- getCompose $ f (iConst ("Skol" ++ show uniq) xs)--foodFact4 :: Term Stage4 TFormula-foodFact4 = skolemize foodFact2------------------------------------------------------------------------------------- Stage 5: Prenex Normal Form-----------------------------------------------------------------------------------type Stage5 = Const :+: Var :+:- TT :+: FF :+: Atom :+: NAtom :+: Or :+: And--class Prenex f where- prenexAlg :: AlgM' (S a) f (Trm Stage5 a)--$(derive [liftSum] [''Prenex])--prenex :: Term Stage4 :-> Term Stage5-prenex f = Term (evalState (runReaderT (cataM' prenexAlg f) [])- initialUniqueSupply)--instance Prenex Const where- prenexAlg (Const f t) = liftM (iConst f) $ mapM getCompose t--instance Prenex TT where- prenexAlg TT = return iTT--instance Prenex FF where- prenexAlg FF = return iFF--instance Prenex Atom where- prenexAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t--instance Prenex NAtom where- prenexAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t--instance Prenex Or where- prenexAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2--instance Prenex And where- prenexAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2--instance Prenex Forall where- prenexAlg (Forall f) = do uniq <- fresh- getCompose $ f (iVar ('x' : show uniq))--foodFact5 :: Term Stage5 TFormula-foodFact5 = prenex foodFact4------------------------------------------------------------------------------------- Stage 6: Conjunctive Normal Form-----------------------------------------------------------------------------------type Literal a = Trm (Const :+: Var :+: Atom :+: NAtom) a-newtype Clause a i = Clause {unClause :: [Literal a i]} -- implicit disjunction-newtype CNF a i = CNF {unCNF :: [Clause a i]} -- implicit conjunction--instance (HDifunctor f, ShowHD f) => Show (Trm f Name i) where- show = evalFreshM . showHD . toCxt--instance Show (Clause Name i) where- show c = intercalate " or " $ map show $ unClause c--instance Show (CNF Name i) where- show c = intercalate "\n" $ map show $ unCNF c--class ToCNF f where- cnfAlg :: f (CNF a) (CNF a) i -> [Clause a i]--$(derive [liftSum] [''ToCNF])--cnf :: Term Stage5 :-> CNF a-cnf = cata (CNF . cnfAlg)--instance ToCNF Const where- cnfAlg (Const f t) =- [Clause [iConst f (map (head . unClause . head . unCNF) t)]]--instance ToCNF Var where- cnfAlg (Var x) = [Clause [iVar x]]--instance ToCNF TT where- cnfAlg TT = []--instance ToCNF FF where- cnfAlg FF = [Clause []]--instance ToCNF Atom where- cnfAlg (Atom p t) =- [Clause [iAtom p (map (head . unClause . head . unCNF) t)]]--instance ToCNF NAtom where- cnfAlg (NAtom p t) =- [Clause [iNAtom p (map (head . unClause . head . unCNF) t)]]--instance ToCNF And where- cnfAlg (And f1 f2) = unCNF f1 ++ unCNF f2--instance ToCNF Or where- cnfAlg (Or f1 f2) =- [Clause (x ++ y) | Clause x <- unCNF f1, Clause y <- unCNF f2]--foodFact6 :: CNF a TFormula-foodFact6 = cnf foodFact5------------------------------------------------------------------------------------- Stage 7: Implicative Normal Form-----------------------------------------------------------------------------------type T = Const :+: Var :+: Atom :+: NAtom-newtype IClause a i = IClause ([Trm T a i], -- implicit conjunction- [Trm T a i]) -- implicit disjunction-newtype INF a i = INF [IClause a i] -- implicit conjunction--instance Show (IClause Name i) where- show (IClause (cs,ds)) = let cs' = intercalate " and " $ map show cs- ds' = intercalate " or " $ map show ds- in "(" ++ cs' ++ ") -> (" ++ ds' ++ ")"--instance Show (INF Name i) where- show (INF fs) = intercalate "\n" $ map show fs--inf :: CNF a TFormula -> INF a TFormula-inf (CNF f) = INF $ map (toImpl . unClause) f- where toImpl :: [Literal a TFormula] -> IClause a TFormula- toImpl disj = IClause ([iAtom p t | NAtom p t <- mapMaybe proj1 disj],- [inject t | t <- mapMaybe proj2 disj])- proj1 :: NatM Maybe (Trm T a) (NAtom a (Trm T a))- proj1 = project- proj2 :: NatM Maybe (Trm T a) (Atom a (Trm T a))- proj2 = project--foodFact7 :: INF a TFormula-foodFact7 = inf foodFact6
− examples/Examples/MultiParam/Lambda.hs
@@ -1,106 +0,0 @@-{-# 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'
− examples/Examples/Param/Graph.hs
@@ -1,77 +0,0 @@-{-# 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
− examples/Examples/Param/Lambda.hs
@@ -1,131 +0,0 @@-{-# 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 Sem m = Fun (Sem m -> m (Sem m)) | Int Int--class Monad m => Eval f m where- evalAlg :: Alg f (m (Sem m))--$(derive [liftSum] [''Eval])--eval :: (Difunctor f, Eval f m) => Term f -> m (Sem m)-eval = cata evalAlg--instance Monad m => Eval Lam m where- evalAlg (Lam f) = return (Fun (f . return))--instance Monad m => Eval App m where- evalAlg (App mx my) = do x <- mx- case x of Fun f -> f =<< my; _ -> fail "stuck"--instance Monad m => Eval Const m where- evalAlg (Const n) = return (Int n)--instance Monad m => Eval Plus m where- evalAlg (Plus mx my) = do x <- mx- y <- my- case (x,y) of (Int n,Int m) -> return (Int (n + m))- _ -> fail "stuck"--instance Monad m => Eval Err m where- evalAlg Err = fail "error"--e :: Term Sig-e = Term (iLet (iConst 2) (\x -> (iLam (\y -> y `iPlus` x) `iApp` iConst 3)))--e' :: Term Sig'-e' = desugar e--evalEx :: Maybe (Sem Maybe)-evalEx = eval e'
− examples/Examples/Param/Names.hs
@@ -1,113 +0,0 @@-{-# 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))----- We make the lifting to sums explicit in order to make the N2PTrans--- work with the default instance declaration further below.-instance (N2PTrans f1 g, N2PTrans f2 g) => N2PTrans (f1 :+: f2) g where- n2pAlg = caseD n2pAlg n2pAlg--n2p :: (Difunctor f, N2PTrans f g) => Term f -> Term g-n2p t = Term $ runReader (cata n2pAlg t) Map.empty--instance (Lam :<: g) => N2PTrans NLam g where- n2pAlg (NLam x b) = do vars <- ask- return $ iLam $ \y -> runReader b (Map.insert x y vars)--instance (Ditraversable f, f :<: g) => N2PTrans f g where- n2pAlg = liftM inject . disequence . dimap (return . P.Var) id -- default--instance N2PTrans NVar g where- n2pAlg (NVar x) = liftM fromJust (asks (Map.lookup x))--en :: Term SigN-en = Term $ iNLam "x1" $ iNLam "x2" (iNLam "x3" $ iNVar "x2") `iApp` iNVar "x1"--ep :: Term SigP-ep = n2p en------------------------------------------------------------------------------------- PHOAS to names translation-----------------------------------------------------------------------------------type M' = Reader [Name]--class P2NTrans f g where- p2nAlg :: Alg f (M' (Trm g a))----- We make the lifting to sums explicit in order to make the P2NTrans--- work with the default instance declaration further below.-instance (P2NTrans f1 g, P2NTrans f2 g) => P2NTrans (f1 :+: f2) g where- p2nAlg = caseD p2nAlg p2nAlg---p2n :: (Difunctor f, P2NTrans f g) => Term f -> Term g-p2n t = Term $ runReader (cata p2nAlg t) ['x' : show n | n <- [1..]]--instance (Ditraversable f, f :<: g) => P2NTrans f g where- p2nAlg = liftM inject . disequence . dimap (return . P.Var) id -- default--instance (NLam :<: g, NVar :<: g) => P2NTrans Lam g where- p2nAlg (Lam f) = do n:names <- ask- return $ iNLam n (runReader (f (return $ iNVar n)) names)--ep' :: Term SigP-ep' = Term $ iLam $ \a -> iLam (\b -> (iLam $ \_ -> b)) `iApp` a--en' :: Term SigN-en' = p2n ep'
+ examples/Examples/Thunk.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,+ FlexibleInstances, FlexibleContexts, UndecidableInstances, OverlappingInstances #-}+--------------------------------------------------------------------------------+-- |+-- Module : Examples.Thunk+-- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved+-- License : BSD3+-- Maintainer : Tom Hvitved <hvitved@diku.dk>+-- Stability : experimental+-- Portability : non-portable (GHC Extensions)+--+-- This example illustrates how the ''Data.Comp.Thunk'' package can be+-- used to implement a non-strict language (or a partially non-strict+-- language).+--+--------------------------------------------------------------------------------++module Examples.Thunk where++import Data.Comp+import Data.Comp.Thunk+import Data.Comp.Derive+import Data.Comp.Show()+import Control.Monad+import Examples.Common hiding (Value(..), Sig)++-- Signature for values, strict pairs+data Value a = Const Int | Pair !a !a++-- Signature for the simple expression language+type Sig = Op :+: Value++-- Derive boilerplate code using Template Haskell+$(derive [makeFunctor, makeTraversable, makeFoldable,+ makeEqF, makeShowF, smartConstructors, makeHaskellStrict]+ [''Value])++-- Monadic term evaluation algebra+class EvalT f v where+ evalAlgT :: Monad m => AlgT m f v++$(derive [liftSum] [''EvalT])++-- Lift the monadic evaluation algebra to a monadic catamorphism+evalT :: (Traversable v, Functor f, EvalT f v, Monad m) => Term f -> m (Term v)+evalT = nf . cata evalAlgT++instance (Value :<: v) => EvalT Value v where+-- make pairs strict in both components+-- evalAlgT x@Pair{} = strict x+-- or explicitly:+-- evalAlgT (Pair x y) = thunk $ liftM2 iPair (dethunk' x) (dethunk' )y+-- evalAlgT x = inject x++-- or only partially strict+ evalAlgT = haskellStrict'++instance (Value :<: v) => EvalT Op v where+ evalAlgT (Add x y) = thunk $ do+ Const n1 <- whnfPr x+ Const n2 <- whnfPr y+ return $ iConst $ n1 + n2+ evalAlgT (Mult x y) = thunk $ do+ Const n1 <- whnfPr x+ Const n2 <- whnfPr y+ return $ iConst $ n1 * n2+ evalAlgT (Fst v) = thunk $ do + Pair x _ <- whnfPr v+ return x+ evalAlgT (Snd v) = thunk $ do + Pair _ y <- whnfPr v+ return y+++{-instance Monad (Either String) where+ Left msg >>= _ = Left msg+ Right x >>= f = f x+ + return = Right+ fail = Left-}++evalTEx :: Either String (Term Value)+evalTEx = evalT (iSnd (iFst (iConst 5) `iPair` iConst 4) :: Term Sig)
src/Data/Comp/Algebra.hs view
@@ -607,6 +607,7 @@ appAlgHom :: forall f g d . (Functor g) => Alg g d -> Hom f g -> Term f -> d+{-# NOINLINE [1] appAlgHom #-} appAlgHom alg hom = run where run :: Term f -> d run (Term t) = run' $ hom t@@ -632,6 +633,7 @@ -- requirements on the source signature @f@. appAlgHomM :: forall m f g a. (Traversable g, Monad m) => AlgM m g a -> HomM m f g -> Term f -> m a+{-# NOINLINE [1] appAlgHomM #-} appAlgHomM alg hom = run where run :: Term f -> m a run (Term t) = hom t >>= mapM run >>= run'
src/Data/Comp/Annotation.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,- UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables, FlexibleContexts #-}+ UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables, FlexibleContexts,+ ConstraintKinds #-} -------------------------------------------------------------------------------- -- | -- Module : Data.Comp.Annotation
src/Data/Comp/Automata.hs view
@@ -66,7 +66,7 @@ , upState , runDUpState , prodDUpState- , (<*>)+ , (|*|) -- * Deterministic Top-Down Tree Transducers , DownTrans , DownTrans'@@ -315,9 +315,9 @@ => DUpState f c p -> DUpState f c q -> DUpState f c (p,q) prodDUpState sp sq t = (sp t, sq t) -(<*>) :: (p :< c, q :< c)+(|*|) :: (p :< c, q :< c) => DUpState f c p -> DUpState f c q -> DUpState f c (p,q)-(<*>) = prodDUpState+(|*|) = prodDUpState
src/Data/Comp/Derive/DeepSeq.hs view
@@ -33,18 +33,16 @@ makeNFDataF :: Name -> Q [Dec] 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)+ let argNames = map (VarT . tyVarBndrName) (init args) complType = foldl AppT (ConT name) argNames preCond = map (ClassP ''NFData . (: [])) argNames classType = AppT (ConT ''NFDataF) complType constrs' <- mapM normalConExp constrs- rnfFDecl <- funD 'rnfF (rnfFClauses fArg constrs')+ rnfFDecl <- funD 'rnfF (rnfFClauses constrs') return [InstanceD preCond classType [rnfFDecl]]- where rnfFClauses fArg = map (genRnfFClause fArg)- genRnfFClause fArg (constr, args) = do - let isFargs = map (==fArg) args- n = length args+ where rnfFClauses = map genRnfFClause+ genRnfFClause (constr, args) = do + let n = length args varNs <- newNames n "x" let pat = ConP constr $ map VarP varNs allVars = map varE varNs
src/Data/Comp/Derive/Equality.hs view
@@ -40,7 +40,6 @@ return [InstanceD preCond classType [eqFDecl]] where eqFClauses constrs = map (genEqClause.abstractConType) constrs ++ defEqClause constrs- filterFarg fArg ty x = (fArg == ty, x) defEqClause constrs | length constrs < 2 = [] | otherwise = [clause [wildP,wildP] (normalB [|False|]) []]
src/Data/Comp/Derive/HaskellStrict.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, CPP #-}+{-# LANGUAGE TemplateHaskell, TypeOperators, CPP, FlexibleContexts, ConstraintKinds #-} -------------------------------------------------------------------------------- -- | -- Module : Data.Comp.Derive.HaskellStrict@@ -24,6 +24,7 @@ import Data.Maybe import Data.Comp.Thunk import Data.Comp.Sum+import Data.Comp.Ops import Data.Traversable import Data.Foldable hiding (any,or) import Control.Monad hiding (mapM, sequence)@@ -34,7 +35,7 @@ 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 t = thunk $ liftM (inject_ (Inr . inj)) $ thunkSequence t thunkSequenceInject' :: (Monad m, f :<: g) => f (TermT m g) -> TermT m g thunkSequenceInject' = thunkSequenceInject
− src/Data/Comp/Derive/Injections.hs
@@ -1,82 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Derive.Injections--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Derive functions for signature injections.--------------------------------------------------------------------------------------module Data.Comp.Derive.Injections- (- injn,- injectn,- deepInjectn- ) where--import Language.Haskell.TH hiding (Cxt)-import Data.Comp.Term-import Data.Comp.Algebra (CxtFun, appSigFun)-import Data.Comp.Ops ((:+:)(..), (:<:)(..))--injn :: Int -> Q [Dec]-injn n = do- let i = mkName $ "inj" ++ show n- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let avar = mkName "a"- let xvar = mkName "x"- let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]- 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)- (map varT fvars)- let tp' = arrowT `appT` (tp `appT` varT avar)- `appT` (varT gvar `appT` varT avar)- forallT (map PlainTV $ gvar : avar : fvars)- (sequence cxt) tp'- genDecl x n = [| case $(varE x) of- Inl x -> $(varE $ mkName "inj") x- Inr x -> $(varE $ mkName $ "inj" ++- if n > 2 then show (n - 1) else "") x |]-injectn :: Int -> Q [Dec]-injectn n = do- let i = mkName ("inject" ++ show n)- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let avar = mkName "a"- let d = [funD i [clause [] (normalB $ genDecl n) []]]- 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- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar- `appT` varT avar- let tp'' = arrowT `appT` (tp `appT` tp') `appT` tp'- forallT (map PlainTV $ hvar : gvar : avar : fvars)- (sequence cxt) tp''- genDecl n = [| Term . $(varE $ mkName $ "inj" ++ show n) |]--deepInjectn :: Int -> Q [Dec]-deepInjectn n = do- let i = mkName ("deepInject" ++ show n)- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let d = [funD i [clause [] (normalB $ genDecl n) []]]- sequence $ sigD i (genSig fvars gvar) : d- where genSig fvars gvar = do- let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let cxt' = classP ''Functor [tp]- let tp' = conT ''CxtFun `appT` tp `appT` varT gvar- forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'- genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
src/Data/Comp/Derive/Projections.hs view
@@ -24,7 +24,7 @@ import Data.Traversable (Traversable) import Data.Comp.Term import Data.Comp.Algebra (CxtFunM, appSigFunM')-import Data.Comp.Ops ((:+:)(..), (:<:)(..))+import Data.Comp.Ops ((:+:)(..), (:<:), proj, inj) projn :: Int -> Q [Dec] projn n = do
src/Data/Comp/Derive/Show.hs view
@@ -15,7 +15,9 @@ module Data.Comp.Derive.Show ( ShowF(..),- makeShowF+ makeShowF,+ ShowConstr(..),+ makeShowConstr ) where import Data.Comp.Derive.Utils@@ -25,11 +27,11 @@ @Show (Term f)@. -} class ShowF f where showF :: f String -> String- -showConstr :: String -> [String] -> String-showConstr con [] = con-showConstr con args = "(" ++ con ++ " " ++ unwords args ++ ")" +showCon :: String -> [String] -> String+showCon con [] = con+showCon con args = "(" ++ con ++ " " ++ unwords args ++ ")"+ {-| Derive an instance of 'ShowF' for a type constructor of any first-order kind taking at least one argument. -} makeShowF :: Name -> Q [Dec]@@ -49,12 +51,48 @@ mkShow (isFArg, var) | isFArg = var | otherwise = [| show $var |]- genShowFClause fArg (constr, args) = do + genShowFClause fArg (constr, args) = do let n = length args varNs <- newNames n "x" let pat = ConP constr $ map VarP varNs allVars = zipWith (filterFarg fArg) args varNs shows = listE $ map mkShow allVars conName = nameBase constr- body <- [|showConstr conName $shows|]+ body <- [|showCon conName $shows|]+ return $ Clause [pat] (NormalB body) []++{-| Constructor printing. -}+class ShowConstr f where+ showConstr :: f a -> String++showCon' :: String -> [String] -> String+showCon' con args = unwords $ con : filter (not.null) args++{-| Derive an instance of 'showConstr' for a type constructor of any first-order kind+ taking at least one argument. -}+makeShowConstr :: Name -> Q [Dec]+makeShowConstr 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+ preCond = map (ClassP ''Show . (: [])) argNames+ classType = AppT (ConT ''ShowConstr) complType+ constrs' <- mapM normalConExp constrs+ showConstrDecl <- funD 'showConstr (showConstrClauses fArg constrs')+ return [InstanceD preCond classType [showConstrDecl]]+ where showConstrClauses fArg = map (genShowConstrClause fArg)+ filterFarg fArg ty x = (fArg == ty, varE x)+ mkShow :: (Bool, ExpQ) -> ExpQ+ mkShow (isFArg, var)+ | isFArg = [| "" |]+ | otherwise = [| show $var |]+ genShowConstrClause fArg (constr, args) = do+ let n = length args+ varNs <- newNames n "x"+ let pat = ConP constr $ map VarP varNs+ allVars = zipWith (filterFarg fArg) args varNs+ shows = listE $ map mkShow allVars+ conName = nameBase constr+ body <- [|showCon' conName $shows|] return $ Clause [pat] (NormalB body) []
src/Data/Comp/Derive/SmartAConstructors.hs view
@@ -30,13 +30,13 @@ inserted. -} smartAConstructors :: Name -> Q [Dec] smartAConstructors fname = do- TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname+ TyConI (DataD _cxt _tname _targs constrs _deriving) <- abstractNewtypeQ $ reify fname let cons = map abstractConType constrs- liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons- where genSmartConstr targs tname (name, args) = do+ liftM concat $ mapM genSmartConstr cons+ where genSmartConstr (name, args) = do let bname = nameBase name- genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args- genSmartConstr' targs tname sname name args = do+ genSmartConstr' (mkName $ "iA" ++ bname) name args+ genSmartConstr' sname name args = do varNs <- newNames args "x" varPr <- newName "_p" let pats = map varP (varPr : varNs)
src/Data/Comp/Derive/Traversable.hs view
@@ -63,14 +63,14 @@ 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,_,_) =+ traverseClause (con, pat,vars',hasFargs,_allVars,_fVars) = 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) []- sequenceAClause (con, pat,vars',hasFargs,_,_) =+ sequenceAClause (con, pat,vars',_hasFargs,_,_) = do let vars = vars' (\d x -> iter' d [|sequenceA|] x) (\x -> [|pure $x|]) body <- P.foldl (\ x y -> [|$x <*> $y|]) [|pure $con|] vars return $ Clause [pat] (NormalB body) []@@ -85,7 +85,7 @@ 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) []- sequenceClause (con, pat,_,hasFargs,allVars, fvars) =+ sequenceClause (con, pat,_vars',_hasFargs,allVars, fvars) = do let conAp = P.foldl appE con allVars conBind (d, x) y = [| $(iter' d [|sequence|] (varE x)) >>= $(lamE [varP x] y)|] body <- P.foldr conBind [|return $conAp|] fvars
src/Data/Comp/Desugar.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,- UndecidableInstances, OverlappingInstances, TypeOperators #-}+ UndecidableInstances, OverlappingInstances, TypeOperators, ConstraintKinds #-} -------------------------------------------------------------------------------- -- | -- Module : Data.Comp.Desugar
src/Data/Comp/Generic.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE GADTs, ScopedTypeVariables, TypeOperators #-}+{-# LANGUAGE GADTs, ScopedTypeVariables, TypeOperators, ConstraintKinds, FlexibleContexts #-} -------------------------------------------------------------------------------- -- |
− src/Data/Comp/MultiParam.hs
@@ -1,34 +0,0 @@------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Patrick Bahr <paba@diku.dk>, Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines the infrastructure necessary to use--- /Generalised Parametric Compositional Data Types/. Generalised Parametric--- Compositional Data Types is an extension of Compositional Data Types with--- parametric higher-order abstract syntax (PHOAS) for usage with binders, and--- GADTs. Generalised Parametric Compositional Data Types combines Generalised--- Compositional Data Types ("Data.Comp.Multi") and Parametric Compositional--- Data Types ("Data.Comp.Param"). Examples of usage are bundled with the--- package in the library @examples\/Examples\/MultiParam@.-------------------------------------------------------------------------------------module Data.Comp.MultiParam (- module Data.Comp.MultiParam.Term- , module Data.Comp.MultiParam.Algebra- , module Data.Comp.MultiParam.HDifunctor- , module Data.Comp.MultiParam.Sum- , module Data.Comp.MultiParam.Annotation- , module Data.Comp.MultiParam.Equality- ) where--import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Algebra-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.Sum-import Data.Comp.MultiParam.Annotation-import Data.Comp.MultiParam.Equality
− src/Data/Comp/MultiParam/Algebra.hs
@@ -1,346 +0,0 @@-{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,- FlexibleContexts, CPP, KindSignatures #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Algebra--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines the notion of algebras and catamorphisms, and their--- generalizations to e.g. monadic versions and other (co)recursion schemes.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Algebra (- -- * Algebras & Catamorphisms- Alg,- free,- cata,- cata',- appCxt,- - -- * Monadic Algebras & Catamorphisms- AlgM,--- algM,- freeM,- cataM,- AlgM',- Compose(..),- freeM',- cataM',-- -- * Term Homomorphisms- CxtFun,- SigFun,- Hom,- appHom,- appHom',- compHom,- appSigFun,- appSigFun',- compSigFun,- hom,- compAlg,-- -- * Monadic Term Homomorphisms- CxtFunM,- SigFunM,- HomM,- sigFunM,- hom',- appHomM,- appTHomM,- appHomM',- appTHomM',- homM,- appSigFunM,- appTSigFunM,- appSigFunM',- appTSigFunM',- compHomM,- compSigFunM,- compAlgM,- compAlgM'- ) where--import Prelude hiding (sequence, mapM)-import Control.Monad hiding (sequence, mapM)-import Data.Functor.Compose -- Functor composition-import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.HDitraversable--{-| This type represents an algebra over a difunctor @f@ and carrier @a@. -}-type Alg f a = f a a :-> a--{-| Construct a catamorphism for contexts over @f@ with holes of type @b@, from- the given algebra. -}-free :: forall h f a b. HDifunctor f- => Alg f a -> (b :-> a) -> Cxt h f a b :-> a-free f g = run- where run :: Cxt h f a b :-> a- run (In t) = f (hfmap run t)- run (Hole x) = g x- run (Var p) = p--{-| Construct a catamorphism from the given algebra. -}-cata :: forall f a. HDifunctor f => Alg f a -> Term f :-> a -{-# NOINLINE [1] cata #-}-cata f (Term t) = run t- where run :: Trm f a :-> a- run (In t) = f (hfmap run t)- run (Var x) = x--{-| A generalisation of 'cata' from terms over @f@ to contexts over @f@, where- the holes have the type of the algebra carrier. -}-cata' :: HDifunctor f => Alg f a -> Cxt h f a a :-> a-{-# INLINE cata' #-}-cata' f = free f id--{-| This function applies a whole context into another context. -}-appCxt :: HDifunctor f => Cxt Hole f a (Cxt h f a b) :-> Cxt h f a b-appCxt (In t) = In (hfmap appCxt t)-appCxt (Hole x) = x-appCxt (Var p) = Var p--{-| This type represents a monadic algebra. It is similar to 'Alg' but- the return type is monadic. -}-type AlgM m f a = NatM m (f a a) a--{-| Construct a monadic catamorphism for contexts over @f@ with holes of type- @b@, from the given monadic algebra. -}-freeM :: forall m h f a b. (HDitraversable f, Monad m)- => AlgM m f a -> NatM m b a -> NatM m (Cxt h f a b) a-freeM f g = run- where run :: NatM m (Cxt h f a b) a- run (In t) = f =<< hdimapM run t- run (Hole x) = g x- run (Var p) = return p--{-| Construct a monadic catamorphism from the given monadic algebra. -}-cataM :: forall m f a. (HDitraversable f, Monad m)- => AlgM m f a -> NatM m (Term f) a-{-# NOINLINE [1] cataM #-}-cataM algm (Term t) = run t- where run :: NatM m (Trm f a) a- run (In t) = algm =<< hdimapM run t- run (Var x) = return x--{-| This type represents a monadic algebra, but where the covariant argument is- also a monadic computation. -}-type AlgM' m f a = NatM m (f a (Compose m a)) a--{-| Construct a monadic catamorphism for contexts over @f@ with holes of type- @b@, from the given monadic algebra. -}-freeM' :: forall m h f a b. (HDifunctor f, Monad m)- => AlgM' m f a -> NatM m b a -> NatM m (Cxt h f a b) a-freeM' f g = run- where run :: NatM m (Cxt h f a b) a- run (In t) = f $ hfmap (Compose . run) t- run (Hole x) = g x- run (Var p) = return p--{-| Construct a monadic catamorphism from the given monadic algebra. -}-cataM' :: forall m f a. (HDifunctor f, Monad m)- => AlgM' m f a -> NatM m (Term f) a-{-# NOINLINE [1] cataM' #-}-cataM' algm (Term t) = run t- where run :: NatM m (Trm f a) a- run (In t) = algm $ hfmap (Compose . run) t- run (Var x) = return x--{-| This type represents a signature function. -}-type SigFun f g = forall (a :: * -> *) (b :: * -> *) . f a b :-> g a b--{-| This type represents a context function. -}-type CxtFun f g = forall h. SigFun (Cxt h f) (Cxt h g)--{-| This type represents a term homomorphism. -}-type Hom f g = SigFun f (Context g)--{-| Apply a term homomorphism recursively to a term/context. -}-appHom :: forall f g. (HDifunctor f, HDifunctor g) => Hom f g -> CxtFun f g-{-# INLINE [1] appHom #-}-appHom f = run where- run :: CxtFun f g- run (In t) = appCxt (f (hfmap run t))- run (Hole x) = Hole x- run (Var p) = Var p---- | Apply a term homomorphism recursively to a term/context. This is--- a top-down variant of 'appHom'.-appHom' :: forall f g. (HDifunctor g)- => Hom f g -> CxtFun f g-{-# INLINE [1] appHom' #-}-appHom' f = run where- run :: CxtFun f g- run (In t) = appCxt (hfmapCxt run (f t))- run (Hole x) = Hole x- run (Var p) = Var p--{-| Compose two term homomorphisms. -}-compHom :: (HDifunctor g, HDifunctor h)- => Hom g h -> Hom f g -> Hom f h-compHom f g = appHom f . g--{-| Compose an algebra with a term homomorphism to get a new algebra. -}-compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> Hom f g -> Alg f a-compAlg alg talg = cata' alg . talg--{-| This function applies a signature function to the given context. -}-appSigFun :: forall f g. (HDifunctor f) => SigFun f g -> CxtFun f g-appSigFun f = run where- run :: CxtFun f g- run (In t) = In (f (hfmap run t))- run (Hole x) = Hole x- run (Var p) = Var p--{-| This function applies a signature function to the given context. -}-appSigFun' :: forall f g. (HDifunctor g) => SigFun f g -> CxtFun f g-appSigFun' f = run where- run :: CxtFun f g- run (In t) = In (hfmap run (f t))- run (Hole x) = Hole x- run (Var p) = Var p--{-| This function composes two signature functions. -}-compSigFun :: SigFun g h -> SigFun f g -> SigFun f h-compSigFun f g = f . g--{-| Lifts the given signature function to the canonical term homomorphism. -}-hom :: HDifunctor g => SigFun f g -> Hom f g-hom f = simpCxt . f--{-| This type represents a monadic signature function. -}-type SigFunM m f g = forall (a :: * -> *) (b :: * -> *) . NatM m (f a b) (g a b)--{-| This type represents a monadic context function. -}-type CxtFunM m f g = forall h . SigFunM m (Cxt h f) (Cxt h g)--{-| This type represents a monadic term homomorphism. -}-type HomM m f g = SigFunM m f (Cxt Hole g)---{-| Lift the given signature function to a monadic signature function. Note that- term homomorphisms are instances of signature functions. Hence this function- also applies to term homomorphisms. -}-sigFunM :: Monad m => SigFun f g -> SigFunM m f g-sigFunM f = return . f--{-| Lift the give monadic signature function to a monadic term homomorphism. -}-hom' :: (HDifunctor f, HDifunctor g, Monad m)- => SigFunM m f g -> HomM m f g-hom' f = liftM (In . hfmap Hole) . f--{-| Lift the given signature function to a monadic term homomorphism. -}-homM :: (HDifunctor g, Monad m) => SigFun f g -> HomM m f g-homM f = sigFunM $ hom f--{-| Apply a monadic term homomorphism recursively to a term/context. -}-appHomM :: forall f g m. (HDitraversable f, Monad m, HDifunctor g)- => HomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appHomM #-}-appHomM f = run- where run :: CxtFunM m f g- run (In t) = liftM appCxt (f =<< hdimapM run t)- run (Hole x) = return (Hole x)- run (Var p) = return (Var p)--{-| A restricted form of |appHomM| which only works for terms. -}-appTHomM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)- => HomM m f g -> Term f i -> m (Term g i)-appTHomM f (Term t) = termM (appHomM f t)---- | Apply a monadic term homomorphism recursively to a--- term/context. This is a top-down variant of 'appHomM'.-appHomM' :: forall f g m. (HDitraversable g, Monad m)- => HomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appHomM' #-}-appHomM' f = run- where run :: CxtFunM m f g- run (In t) = liftM appCxt (hdimapMCxt run =<< f t)- run (Hole x) = return (Hole x)- run (Var p) = return (Var p)--{-| A restricted form of |appHomM'| which only works for terms. -}-appTHomM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)- => HomM m f g -> Term f i -> m (Term g i)-appTHomM' f (Term t) = termM (appHomM' f t)--{-| This function applies a monadic signature function to the given context. -}-appSigFunM :: forall m f g. (HDitraversable f, Monad m)- => SigFunM m f g -> CxtFunM m f g-appSigFunM f = run- where run :: CxtFunM m f g- run (In t) = liftM In (f =<< hdimapM run t)- run (Hole x) = return (Hole x)- run (Var p) = return (Var p)--{-| A restricted form of |appSigFunM| which only works for terms. -}-appTSigFunM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)- => SigFunM m f g -> Term f i -> m (Term g i)-appTSigFunM f (Term t) = termM (appSigFunM f t)---- | This function applies a monadic signature function to the given--- context. This is a top-down variant of 'appSigFunM'.-appSigFunM' :: forall m f g. (HDitraversable g, Monad m)- => SigFunM m f g -> CxtFunM m f g-appSigFunM' f = run- where run :: CxtFunM m f g- run (In t) = liftM In (hdimapM run =<< f t)- run (Hole x) = return (Hole x)- run (Var p) = return (Var p)--{-| A restricted form of |appSigFunM'| which only works for terms. -}-appTSigFunM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)- => SigFunM m f g -> Term f i -> m (Term g i)-appTSigFunM' f (Term t) = termM (appSigFunM' f t)--{-| Compose two monadic term homomorphisms. -}-compHomM :: (HDitraversable g, HDifunctor h, Monad m)- => HomM m g h -> HomM m f g -> HomM m f h-compHomM f g = appHomM f <=< g--{-| Compose a monadic algebra with a monadic term homomorphism to get a new- monadic algebra. -}-compAlgM :: (HDitraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a-compAlgM alg talg = freeM alg return <=< talg--{-| Compose a monadic algebra with a term homomorphism to get a new monadic- algebra. -}-compAlgM' :: (HDitraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a-compAlgM' alg talg = freeM alg return . talg--{-| This function composes two monadic signature functions. -}-compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h-compSigFunM f g a = g a >>= f--{--#ifndef NO_RULES-{-# RULES- "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.- cata a (appHom h x) = cata (compAlg a h) x;-- "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.- appHom a (appHom h x) = appHom (compHom a h) x; #-}--{--{-# RULES - "cataM/appHomM" forall (a :: AlgM m g d) (h :: HomM m f g d) x.- appHomM h x >>= cataM a = cataM (compAlgM a h) x;-- "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.- cataM a (appHom h x) = cataM (compAlgM' a h) x;-- "appHomM/appHomM" forall (a :: HomM m g h b) (h :: HomM m f g b) x.- appHomM h x >>= appHomM a = appHomM (compHomM a h) x; #-}--{-# RULES- "cata/build" forall alg (g :: forall a . Alg f a -> a) .- cata alg (build g) = g alg #-}--}-#endif--}
− src/Data/Comp/MultiParam/Annotation.hs
@@ -1,81 +0,0 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,- UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Annotation--- Copyright : (c) 2010-2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines annotations on signatures.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Annotation- (- (:&:) (..),- (:*:) (..),- DistAnn (..),- RemA (..),- liftA,- liftA',- stripA,- propAnn,- propAnnM,- ann,- project'- ) where--import qualified Data.Comp.Ops as O-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Sum-import Data.Comp.MultiParam.Ops-import Data.Comp.MultiParam.Algebra--import Control.Monad--{-| Transform a function with a domain constructed from a higher-order difunctor- to a function with a domain constructed with the same higher-order difunctor,- but with an additional annotation. -}-liftA :: (RemA s s') => (s' a b :-> t) -> s a b :-> t-liftA f v = f (remA v)--{-| Transform a function with a domain constructed from a higher-order difunctor- to a function with a domain constructed with the same higher-order difunctor,- but with an additional annotation. -}-liftA' :: (DistAnn s' p s, HDifunctor s')- => (s' a b :-> Cxt h s' c d) -> s a b :-> Cxt h s c d-liftA' f v = let v' O.:&: p = projectA v- in ann p (f v')--{-| Strip the annotations from a term over a higher-order difunctor with- annotations. -}-stripA :: (RemA g f, HDifunctor g) => CxtFun g f-stripA = appSigFun remA--{-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism- over the same signatures, but extended with annotations. -}-propAnn :: (DistAnn f p f', DistAnn g p g', HDifunctor g) - => Hom f g -> Hom f' g'-propAnn hom f' = ann p (hom f)- where f O.:&: p = projectA f'--{-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic- term homomorphism over the same signatures, but extended with annotations. -}-propAnnM :: (DistAnn f p f', DistAnn g p g', HDifunctor g, Monad m)- => HomM m f g -> HomM m f' g'-propAnnM hom f' = liftM (ann p) (hom f)- where f O.:&: p = projectA f'--{-| Annotate each node of a term with a constant value. -}-ann :: (DistAnn f p g, HDifunctor f) => p -> CxtFun f g-ann c = appSigFun (injectA c)--{-| This function is similar to 'project' but applies to signatures- with an annotation which is then ignored. -}-project' :: (RemA f f', s :<: f') => Cxt h f a b i -> Maybe (s a (Cxt h f a b) i)-project' (In x) = proj $ remA x-project' _ = Nothing
− src/Data/Comp/MultiParam/Derive.hs
@@ -1,55 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module contains functionality for automatically deriving boilerplate--- code using Template Haskell. Examples include instances of 'HDifunctor',--- 'ShowHD', and 'EqHD'.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive- (- derive,- -- |Derive boilerplate instances for parametric signatures, i.e.- -- signatures for parametric compositional data types.-- -- ** EqHD- module Data.Comp.MultiParam.Derive.Equality,- -- ** OrdHD- module Data.Comp.MultiParam.Derive.Ordering,- -- ** ShowHD- module Data.Comp.MultiParam.Derive.Show,- -- ** HDifunctor- module Data.Comp.MultiParam.Derive.HDifunctor,- -- ** Smart Constructors- module Data.Comp.MultiParam.Derive.SmartConstructors,- -- ** Smart Constructors w/ Annotations- module Data.Comp.MultiParam.Derive.SmartAConstructors,- -- ** Lifting to Sums- liftSum- ) where--import Data.Comp.Derive.Utils (derive, liftSumGen)-import Data.Comp.MultiParam.Derive.Equality-import Data.Comp.MultiParam.Derive.Ordering-import Data.Comp.MultiParam.Derive.Show-import Data.Comp.MultiParam.Derive.HDifunctor-import Data.Comp.MultiParam.Derive.SmartConstructors-import Data.Comp.MultiParam.Derive.SmartAConstructors-import Data.Comp.MultiParam.Ops ((:+:), caseHD)--import Language.Haskell.TH--{-| Given the name of a type class, where the first parameter is a higher-order- difunctor, lift it to sums of higher-order difunctors. Example:- @class ShowHD f where ...@ is lifted as- @instance (ShowHD f, ShowHD g) => ShowHD (f :+: g) where ... @. -}-liftSum :: Name -> Q [Dec]-liftSum = liftSumGen 'caseHD ''(:+:)
− src/Data/Comp/MultiParam/Derive/Equality.hs
@@ -1,78 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,- ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.Equality--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @EqHD@.-------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.Equality- (- EqHD(..),- makeEqHD- ) where--import Data.Comp.Derive.Utils-import Data.Comp.MultiParam.FreshM hiding (Name)-import Data.Comp.MultiParam.Equality-import Control.Monad-import Language.Haskell.TH hiding (Cxt, match)--{-| Derive an instance of 'EqHD' for a type constructor of any parametric- kind taking at least three arguments. -}-makeEqHD :: Name -> Q [Dec]-makeEqHD fname = do- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- let args' = init args- -- covariant argument- let coArg :: Name = tyVarBndrName $ last args'- -- contravariant argument- let conArg :: Name = tyVarBndrName $ last $ init args'- let argNames = map (VarT . tyVarBndrName) (init $ init args')- let complType = foldl AppT (ConT name) argNames- let classType = AppT (ConT ''EqHD) complType- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- let defC = if length constrs < 2 then- []- else- [clause [wildP,wildP] (normalB [|return False|]) []]- eqHDDecl <- funD 'eqHD (map (eqHDClause conArg coArg) constrs' ++ defC)- let context = map (\arg -> ClassP ''Eq [arg]) argNames- return [InstanceD context classType [eqHDDecl]]- where eqHDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- eqHDClause conArg coArg (constr, args) = do- varXs <- newNames (length args) "x"- varYs <- newNames (length args) "y"- -- Patterns for the constructors- let patx = ConP constr $ map VarP varXs- let paty = ConP constr $ map VarP varYs- body <- eqHDBody conArg coArg (zip3 varXs varYs args)- return $ Clause [patx,paty] (NormalB body) []- eqHDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ- eqHDBody conArg coArg x =- [|liftM and (sequence $(listE $ map (eqHDB conArg coArg) x))|]- eqHDB :: Name -> Name -> (Name, Name, Type) -> ExpQ- eqHDB conArg coArg (x, y, tp)- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) =- [| return $ $(varE x) == $(varE y) |]- | otherwise =- case tp of- AppT (VarT a) _ - | a == coArg -> [| peq $(varE x) $(varE y) |]- AppT (AppT ArrowT (AppT (VarT a) _)) _- | a == conArg ->- [| withName (\v -> peq ($(varE x) $ nameCoerce v) ($(varE y) $ nameCoerce v)) |]- SigT tp' _ ->- eqHDB conArg coArg (x, y, tp')- _ ->- if containsType tp (VarT conArg) then- [| eqHD $(varE x) $(varE y) |]- else- [| peq $(varE x) $(varE y) |]
− src/Data/Comp/MultiParam/Derive/HDifunctor.hs
@@ -1,85 +0,0 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.HDifunctor--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @HDifunctor@.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.HDifunctor- (- HDifunctor,- makeHDifunctor- ) where--import Data.Comp.Derive.Utils-import Data.Comp.MultiParam.HDifunctor-import Language.Haskell.TH--{-| Derive an instance of 'HDifunctor' for a type constructor of any parametric- kind taking at least three arguments. -}-makeHDifunctor :: Name -> Q [Dec]-makeHDifunctor fname = do- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- let args' = init args- -- covariant argument- let coArg :: Name = tyVarBndrName $ last args'- -- contravariant argument- let conArg :: Name = tyVarBndrName $ last $ init args'- let argNames = map (VarT . tyVarBndrName) (init $ init args')- let complType = foldl AppT (ConT name) argNames- let classType = AppT (ConT ''HDifunctor) complType- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- hdimapDecl <- funD 'hdimap (map (hdimapClause conArg coArg) constrs')- return [InstanceD [] classType [hdimapDecl]]- where hdimapClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- hdimapClause conArg coArg (constr, args) = do- fn <- newName "_f"- gn <- newName "_g"- varNs <- newNames (length args) "x"- let f = varE fn- let g = varE gn- let fp = VarP fn- let gp = VarP gn- -- Pattern for the constructor- let pat = ConP constr $ map VarP varNs- body <- hdimapArgs conArg coArg f g (zip varNs args) (conE constr)- return $ Clause [fp, gp, pat] (NormalB body) []- hdimapArgs :: Name -> Name -> ExpQ -> ExpQ- -> [(Name, Type)] -> ExpQ -> ExpQ- hdimapArgs _ _ _ _ [] acc =- acc- hdimapArgs conArg coArg f g ((x,tp):tps) acc =- hdimapArgs conArg coArg f g tps- (acc `appE` (hdimapArg conArg coArg tp f g `appE` varE x))- hdimapArg :: Name -> Name -> Type -> ExpQ -> ExpQ -> ExpQ- hdimapArg conArg coArg tp f g- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) = [| id |]- | otherwise =- case tp of- AppT (VarT a) _ | a == conArg -> f- | a == coArg -> g- AppT (AppT ArrowT tp1) tp2 -> do- xn <- newName "x"- let ftp1 = hdimapArg conArg coArg tp1 f g- let ftp2 = hdimapArg conArg coArg tp2 f g- lamE [varP xn]- (infixE (Just ftp2)- [|(.)|]- (Just $ infixE (Just $ varE xn)- [|(.)|]- (Just ftp1)))- SigT tp' _ ->- hdimapArg conArg coArg tp' f g- _ ->- if containsType tp (VarT conArg) then- [| hdimap $f $g |]- else- [| fmap $g |]
− src/Data/Comp/MultiParam/Derive/Injections.hs
@@ -1,91 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.Injections--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Derive functions for signature injections.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.Injections- (- injn,- injectn,- deepInjectn- ) where--import Language.Haskell.TH hiding (Cxt)-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Algebra (CxtFun, appSigFun)-import Data.Comp.MultiParam.Ops ((:+:)(..), (:<:)(..))--injn :: Int -> Q [Dec]-injn n = do- let i = mkName $ "inj" ++ show n- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let avar = mkName "a"- let bvar = mkName "b"- let ivar = mkName "i"- let xvar = mkName "x"- let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]- sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d- where genSig fvars gvar avar bvar ivar = do- let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let tp' = arrowT `appT` (tp `appT` varT avar `appT`- varT bvar `appT` varT ivar)- `appT` (varT gvar `appT` varT avar `appT`- varT bvar `appT` varT ivar)- forallT (map PlainTV $ gvar : avar : bvar : ivar : fvars)- (sequence cxt) tp'- genDecl x n = [| case $(varE x) of- Inl x -> $(varE $ mkName "inj") x- Inr x -> $(varE $ mkName $ "inj" ++- if n > 2 then show (n - 1) else "") x |]-injectn :: Int -> Q [Dec]-injectn n = do- let i = mkName ("inject" ++ show n)- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let avar = mkName "a"- let bvar = mkName "b"- let ivar = mkName "i"- let d = [funD i [clause [] (normalB $ genDecl n) []]]- sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d- where genSig fvars gvar avar bvar ivar = do- let hvar = mkName "h"- let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar- `appT` varT avar `appT` varT bvar- let tp'' = arrowT `appT` (tp `appT` varT avar `appT`- tp' `appT` varT ivar)- `appT` (tp' `appT` varT ivar)- forallT (map PlainTV $ hvar : gvar : avar : bvar : ivar : fvars)- (sequence cxt) tp''- genDecl n = [| In . $(varE $ mkName $ "inj" ++ show n) |]--deepInjectn :: Int -> Q [Dec]-deepInjectn n = do- let i = mkName ("deepInject" ++ show n)- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let d = [funD i [clause [] (normalB $ genDecl n) []]]- sequence $ sigD i (genSig fvars gvar) : d- where genSig fvars gvar = do- let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let cxt' = classP ''HDifunctor [tp]- let tp' = conT ''CxtFun `appT` tp `appT` varT gvar- forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'- genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
− src/Data/Comp/MultiParam/Derive/Ordering.hs
@@ -1,93 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,- ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.Ordering--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @OrdHD@.-------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.Ordering- (- OrdHD(..),- makeOrdHD- ) where--import Data.Comp.MultiParam.FreshM hiding (Name)-import Data.Comp.MultiParam.Ordering-import Data.Comp.Derive.Utils-import Data.Maybe-import Data.List-import Language.Haskell.TH hiding (Cxt)-import Control.Monad (liftM)--compList :: [Ordering] -> Ordering-compList = fromMaybe EQ . find (/= EQ)--{-| Derive an instance of 'OrdHD' for a type constructor of any parametric- kind taking at least three arguments. -}-makeOrdHD :: Name -> Q [Dec]-makeOrdHD fname = do- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- let args' = init args- -- covariant argument- let coArg :: Name = tyVarBndrName $ last args'- -- contravariant argument- let conArg :: Name = tyVarBndrName $ last $ init args'- let argNames = map (VarT . tyVarBndrName) (init $ init args')- let complType = foldl AppT (ConT name) argNames- let classType = AppT (ConT ''OrdHD) complType- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- compareHDDecl <- funD 'compareHD (compareHDClauses conArg coArg constrs')- let context = map (\arg -> ClassP ''Ord [arg]) argNames- return [InstanceD context classType [compareHDDecl]]- where compareHDClauses :: Name -> Name -> [(Name,[Type])] -> [ClauseQ]- compareHDClauses _ _ [] = []- compareHDClauses conArg coArg constrs = - let constrs' = constrs `zip` [1..]- constPairs = [(x,y)| x<-constrs', y <- constrs']- in map (genClause conArg coArg) constPairs- genClause conArg coArg ((c,n),(d,m))- | n == m = genEqClause conArg coArg c- | n < m = genLtClause c d- | otherwise = genGtClause c d- genEqClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- genEqClause conArg coArg (constr, args) = do - varXs <- newNames (length args) "x"- varYs <- newNames (length args) "y"- let patX = ConP constr $ map VarP varXs- let patY = ConP constr $ map VarP varYs- body <- eqDBody conArg coArg (zip3 varXs varYs args)- return $ Clause [patX, patY] (NormalB body) []- eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ- eqDBody conArg coArg x =- [|liftM compList (sequence $(listE $ map (eqDB conArg coArg) x))|]- eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ- eqDB conArg coArg (x, y, tp)- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) =- [| return $ compare $(varE x) $(varE y) |]- | otherwise =- case tp of- AppT (VarT a) _ - | a == coArg -> [| pcompare $(varE x) $(varE y) |]- AppT (AppT ArrowT (AppT (VarT a) _)) _- | a == conArg ->- [| withName (\v -> pcompare ($(varE x) $ nameCoerce v)- ($(varE y) $ nameCoerce v)) |]- SigT tp' _ ->- eqDB conArg coArg (x, y, tp')- _ ->- if containsType tp (VarT conArg) then- [| compareHD $(varE x) $(varE y) |]- else- [| pcompare $(varE x) $(varE y) |]- genLtClause (c, _) (d, _) =- clause [recP c [], recP d []] (normalB [| return LT |]) []- genGtClause (c, _) (d, _) =- clause [recP c [], recP d []] (normalB [| return GT |]) []
− src/Data/Comp/MultiParam/Derive/Projections.hs
@@ -1,108 +0,0 @@-{-# LANGUAGE TemplateHaskell, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.Projections--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Derive functions for signature projections.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.Projections- (- projn,- projectn,- deepProjectn- ) where--import Language.Haskell.TH hiding (Cxt)-import Control.Monad (liftM)-import Data.Comp.MultiParam.HDitraversable (HDitraversable)-import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Algebra (appTSigFunM')-import Data.Comp.MultiParam.Ops ((:+:)(..), (:<:)(..))--projn :: Int -> Q [Dec]-projn n = do- let p = mkName $ "proj" ++ show n- let gvars = map (\n -> mkName $ 'g' : show n) [1..n]- let avar = mkName "a"- let bvar = mkName "b"- let ivar = mkName "i"- let xvar = mkName "x"- let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar bvar ivar) []]]- sequence $ (sigD p $ genSig gvars avar bvar ivar) : d- where genSig gvars avar bvar ivar = do- let fvar = mkName "f"- let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars- let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)- (map varT gvars)- let tp' = arrowT `appT` (varT fvar `appT` varT avar `appT`- varT bvar `appT` varT ivar)- `appT` (conT ''Maybe `appT`- (tp `appT` varT avar `appT`- varT bvar `appT` varT ivar))- forallT (map PlainTV $ fvar : avar : bvar : ivar : gvars)- (sequence cxt) tp'- genDecl x [g] a b i =- [| liftM inj (proj $(varE x)- :: Maybe ($(varT g `appT` varT a `appT`- varT b `appT` varT i))) |]- genDecl x (g:gs) a b i =- [| case (proj $(varE x)- :: Maybe ($(varT g `appT` varT a `appT`- varT b `appT` varT i))) of- Just y -> Just $ inj y- _ -> $(genDecl x gs a b i) |]- genDecl _ _ _ _ _ = error "genDecl called with empty list"--projectn :: Int -> Q [Dec]-projectn n = do- let p = mkName ("project" ++ show n)- let gvars = map (\n -> mkName $ 'g' : show n) [1..n]- let avar = mkName "a"- let bvar = mkName "b"- let ivar = mkName "i"- let xvar = mkName "x"- let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]- sequence $ (sigD p $ genSig gvars avar bvar ivar) : d- where genSig gvars avar bvar ivar = do- let fvar = mkName "f"- let hvar = mkName "h"- let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars- let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)- (map varT gvars)- let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar- `appT` varT avar `appT` varT bvar- let tp'' = arrowT `appT` (tp' `appT` varT ivar)- `appT` (conT ''Maybe `appT`- (tp `appT` varT avar `appT` tp' `appT`- varT ivar))- forallT (map PlainTV $ hvar : fvar : avar : bvar : ivar : gvars)- (sequence cxt) tp''- genDecl x n = [| case $(varE x) of- Hole _ -> Nothing- Var _ -> Nothing- In t -> $(varE $ mkName $ "proj" ++ show n) t |]--deepProjectn :: Int -> Q [Dec]-deepProjectn n = do- let p = mkName ("deepProject" ++ show n)- let gvars = map (\n -> mkName $ 'g' : show n) [1..n]- let d = [funD p [clause [] (normalB $ genDecl n) []]]- sequence $ (sigD p $ genSig gvars) : d- where genSig gvars = do- let fvar = mkName "f"- let ivar = mkName "i"- let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars- let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)- (map varT gvars)- let cxt' = classP ''HDitraversable [tp]- let tp' = arrowT `appT` (conT ''Term `appT` varT fvar `appT` varT ivar)- `appT` (conT ''Maybe `appT` (conT ''Term `appT` tp `appT` varT ivar))- forallT (map PlainTV $ fvar : ivar : gvars) (sequence $ cxt' : cxt) tp'- genDecl n = [| appTSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
− src/Data/Comp/MultiParam/Derive/Show.hs
@@ -1,87 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,- ScopedTypeVariables, UndecidableInstances, KindSignatures #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.Show--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @ShowHD@.-------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.Show- (- ShowHD(..),- makeShowHD- ) where--import Data.Comp.Derive.Utils-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)-import qualified Data.Traversable as T--{-| Signature printing. An instance @ShowHD f@ gives rise to an instance- @Show (Term f i)@. -}-class ShowHD f where- showHD :: f FreshM.Name (K (FreshM String)) i -> FreshM String--newtype Dummy = Dummy String--instance Show Dummy where- show (Dummy s) = s--{-| Derive an instance of 'ShowHD' for a type constructor of any parametric- kind taking at least three arguments. -}-makeShowHD :: Name -> Q [Dec]-makeShowHD fname = do- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- let args' = init args- -- covariant argument- let coArg :: Name = tyVarBndrName $ last args'- -- contravariant argument- let conArg :: Name = tyVarBndrName $ last $ init args'- let argNames = map (VarT . tyVarBndrName) (init $ init args')- let complType = foldl AppT (ConT name) argNames- let classType = AppT (ConT ''ShowHD) complType- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- showHDDecl <- funD 'showHD (map (showHDClause conArg coArg) constrs')- let context = map (\arg -> ClassP ''Show [arg]) argNames- return [InstanceD context classType [showHDDecl]]- where showHDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- showHDClause conArg coArg (constr, args) = do- varXs <- newNames (length args) "x"- -- Pattern for the constructor- let patx = ConP constr $ map VarP varXs- body <- showHDBody (nameBase constr) conArg coArg (zip varXs args)- return $ Clause [patx] (NormalB body) []- showHDBody :: String -> Name -> Name -> [(Name, Type)] -> ExpQ- showHDBody constr conArg coArg x =- [|liftM (unwords . (constr :) .- map (\x -> if elem ' ' x then "(" ++ x ++ ")" else x))- (sequence $(listE $ map (showHDB conArg coArg) x))|]- showHDB :: Name -> Name -> (Name, Type) -> ExpQ- showHDB conArg coArg (x, tp)- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) =- [| return $ show $(varE x) |]- | otherwise =- case tp of- AppT (VarT a) _ - | a == coArg -> [| unK $(varE x) |]- AppT (AppT ArrowT (AppT (VarT a) _)) _- | a == conArg ->- [| withName (\v -> do body <- (unK . $(varE x)) v- return $ "\\" ++ show v ++ " -> " ++ body) |]- SigT tp' _ ->- showHDB conArg coArg (x, tp')- _ ->- if containsType tp (VarT conArg) then- [| showHD $(varE x) |]- else- [| liftM show $ T.mapM (liftM Dummy . unK) $(varE x) |]
− src/Data/Comp/MultiParam/Derive/SmartAConstructors.hs
@@ -1,48 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.SmartAConstructors--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive smart constructors with annotations for higher-order--- difunctors.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.SmartAConstructors - (- smartAConstructors- ) where--import Language.Haskell.TH hiding (Cxt)-import Data.Comp.Derive.Utils-import Data.Comp.MultiParam.Ops-import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.HDifunctor--import Control.Monad--{-| Derive smart constructors with annotations for a higher-order difunctor. The- smart constructors are similar to the ordinary constructors, but a- 'injectA . hdimap Var id' is automatically inserted. -}-smartAConstructors :: Name -> Q [Dec]-smartAConstructors fname = do- TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname- let cons = map abstractConType constrs- liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons- where genSmartConstr targs tname (name, args) = do- let bname = nameBase name- genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args- genSmartConstr' targs tname sname name args = do- varNs <- newNames args "x"- varPr <- newName "_p"- let pats = map varP (varPr : varNs)- vars = map varE varNs- val = appE [|injectA $(varE varPr)|] $- appE [|inj . hdimap Var id|] $ foldl appE (conE name) vars- function = [funD sname [clause pats (normalB [|In $val|]) []]]- sequence function
− src/Data/Comp/MultiParam/Derive/SmartConstructors.hs
@@ -1,72 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Derive.SmartConstructors--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive smart constructors for higher-order difunctors.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Derive.SmartConstructors - (- smartConstructors- ) where--import Language.Haskell.TH hiding (Cxt)-import Data.Comp.Derive.Utils-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 Var id' is automatically inserted. -}-smartConstructors :: Name -> Q [Dec]-smartConstructors fname = do- TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname- let iVar = tyVarBndrName $ last targs- let cons = map (abstractConType &&& iTp iVar) constrs- liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons- where iTp iVar (ForallC _ cxt _) =- -- Check if the GADT phantom type is constrained- case [y | EqualP x y <- cxt, x == VarT iVar] of- [] -> Nothing- tp:_ -> Just tp- iTp _ _ = Nothing- genSmartConstr targs tname ((name, args), miTp) = do- let bname = nameBase name- genSmartConstr' targs tname (mkName $ 'i' : bname) name args miTp- genSmartConstr' targs tname sname name args miTp = do- varNs <- newNames args "x"- let pats = map varP varNs- vars = map varE varNs- val = foldl appE (conE name) vars- sig = genSig targs tname sname args miTp- function = [funD sname [clause pats (normalB [|inject (hdimap Var id $val)|]) []]]- sequence $ sig ++ function- genSig targs tname sname 0 miTp = (:[]) $ do- hvar <- newName "h"- fvar <- newName "f"- avar <- newName "a"- bvar <- newName "b"- ivar <- newName "i"- let targs' = init $ init $ init targs- vars = hvar:fvar:avar:bvar:maybe [ivar] (const []) miTp++targs'- h = varT hvar- f = varT fvar- a = varT avar- b = varT bvar- i = varT ivar- ftype = foldl appT (conT tname) (map varT targs')- constr = classP ''(:<:) [ftype, f]- typ = foldl appT (conT ''Cxt) [h, f, a, b,maybe i return miTp]- typeSig = forallT (map PlainTV vars) (sequence [constr]) typ- sigD sname typeSig- genSig _ _ _ _ _ = []
− src/Data/Comp/MultiParam/Desugar.hs
@@ -1,44 +0,0 @@-{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,- UndecidableInstances, OverlappingInstances, TypeOperators, Rank2Types #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Desugar--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This modules defines the 'Desugar' type class for desugaring of terms.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Desugar where--import Data.Comp.MultiParam---- |The desugaring term homomorphism.-class (HDifunctor f, HDifunctor g) => Desugar f g where- desugHom :: Hom f g- desugHom = desugHom' . hfmap Hole- desugHom' :: f a (Cxt h g a b) :-> Cxt h g a b- desugHom' x = appCxt (desugHom x)---- We make the lifting to sums explicit in order to make the Desugar--- class work with the default instance declaration further below.-instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where- desugHom = caseHD desugHom desugHom----- |Desugar a term.-desugar :: Desugar f g => Term f :-> Term g-desugar (Term t) = Term (appHom desugHom t)---- |Lift desugaring to annotated terms.-desugarA :: (HDifunctor f', HDifunctor g', DistAnn f p f', DistAnn g p g',- Desugar f g) => Term f' :-> Term g'-desugarA (Term t) = Term (appHom (propAnn desugHom) t)---- |Default desugaring instance.-instance (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g where- desugHom = simpCxt . inj
− src/Data/Comp/MultiParam/Equality.hs
@@ -1,64 +0,0 @@-{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,- UndecidableInstances, IncoherentInstances, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Equality--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines equality for signatures, which lifts to equality for--- terms.-------------------------------------------------------------------------------------module Data.Comp.MultiParam.Equality- (- PEq(..),- EqHD(..)- ) where--import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Sum-import Data.Comp.MultiParam.Ops-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.FreshM---- |Equality on parametric values. The equality test is performed inside the--- 'FreshM' monad for generating fresh identifiers.-class PEq a where- peq :: a i -> a j -> FreshM Bool--instance Eq a => PEq (K a) where- peq (K x) (K y) = return $ x == y--{-| Signature equality. An instance @EqHD f@ gives rise to an instance- @Eq (Term f i)@. The equality test is performed inside the 'FreshM' monad for- generating fresh identifiers. -}-class EqHD f where- eqHD :: PEq a => f Name a i -> f Name a j -> FreshM Bool--{-| 'EqHD' is propagated through sums. -}-instance (EqHD f, EqHD g) => EqHD (f :+: g) where- eqHD (Inl x) (Inl y) = eqHD x y- eqHD (Inr x) (Inr y) = eqHD x y- eqHD _ _ = return False--instance PEq Name where- peq x y = return $ nameCoerce x == y--{-| From an 'EqHD' difunctor an 'Eq' instance of the corresponding term type can- be derived. -}-instance EqHD f => EqHD (Cxt h f) where- eqHD (In e1) (In e2) = eqHD e1 e2- eqHD (Hole h1) (Hole h2) = peq h1 h2- eqHD (Var p1) (Var p2) = peq p1 p2- eqHD _ _ = return False--instance (EqHD f, PEq a) => PEq (Cxt h f Name a) where- peq = eqHD--{-| Equality on terms. -}-instance (HDifunctor f, EqHD f) => Eq (Term f i) where- (==) (Term x) (Term y) = evalFreshM $ eqHD x y
− src/Data/Comp/MultiParam/FreshM.hs
@@ -1,54 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.FreshM--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines a monad for generating fresh, abstract names, useful--- e.g. for defining equality on terms.-------------------------------------------------------------------------------------module Data.Comp.MultiParam.FreshM- (- FreshM,- Name,- withName,- nameCoerce,- evalFreshM- ) where--import Control.Monad.Reader---- |Monad for generating fresh (abstract) names.-newtype FreshM a = FreshM{unFreshM :: Reader Int a}- deriving Monad---- |Abstract notion of a name (the constructor is hidden).-newtype Name i = Name Int- deriving Eq--instance Show (Name i) where- show (Name x) = names !! x- where baseNames = ['a'..'z']- names = map (:[]) baseNames ++ names' 1- names' n = map (: show n) baseNames ++ names' (n + 1)--instance Ord (Name i) where- compare (Name x) (Name y) = compare x y---- |Change the type tag of a name.-nameCoerce :: Name i -> Name j-nameCoerce (Name x) = Name x---- |Run the given computation with the next available name.-withName :: (Name i -> FreshM a) -> FreshM a-withName m = do name <- FreshM (asks Name)- FreshM $ local ((+) 1) $ unFreshM $ m name---- |Evaluate a computation that uses fresh names.-evalFreshM :: FreshM a -> a-evalFreshM (FreshM m) = runReader m 0
− src/Data/Comp/MultiParam/HDifunctor.hs
@@ -1,40 +0,0 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, Rank2Types,- TypeOperators, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.HDifunctor--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines higher-order difunctors, a hybrid between higher-order--- functors (Johann, Ghani, POPL '08), and difunctors (Meijer, Hutton, FPCA--- '95). Higher-order difunctors are used to define signatures for--- compositional parametric generalised data types.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.HDifunctor- (- HDifunctor (..),- HFunctor (..),- I (..),- K (..),- E (..),- A (..),- (:->),- NatM- ) where--import Data.Comp.Multi.HFunctor---- | This class represents higher-order difunctors.-class HDifunctor f where- hdimap :: (a :-> b) -> (c :-> d) -> f b c :-> f a d---- |A higher-order difunctor gives rise to a higher-order functor when--- restricted to a particular contravariant argument.-instance HDifunctor f => HFunctor (f a) where- hfmap = hdimap id
− src/Data/Comp/MultiParam/HDitraversable.hs
@@ -1,29 +0,0 @@-{-# LANGUAGE Rank2Types, FlexibleInstances, MultiParamTypeClasses,- FlexibleContexts, OverlappingInstances, TypeOperators, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.HDitraversable--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines traversable higher-order difunctors.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.HDitraversable- (- HDitraversable (..),- HTraversable (..)- ) where--import Prelude hiding (mapM, sequence, foldr)-import Data.Comp.Multi.HTraversable-import Data.Comp.MultiParam.HDifunctor--{-| HDifunctors representing data structures that can be traversed from left to- right. -}-class HDifunctor f => HDitraversable f where- hdimapM :: Monad m => NatM m b c -> NatM m (f a b) (f a c)
− src/Data/Comp/MultiParam/Ops.hs
@@ -1,126 +0,0 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies,- FlexibleInstances, UndecidableInstances, IncoherentInstances,- KindSignatures, RankNTypes #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Ops--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module provides operators on higher-order difunctors.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Ops where--import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.HDitraversable-import qualified Data.Comp.Ops as O-import Control.Monad (liftM)----- Sums-infixr 6 :+:---- |Formal sum of signatures (difunctors).-data (f :+: g) (a :: * -> *) (b :: * -> *) i = Inl (f a b i)- | Inr (g a b i)--{-| Utility function to case on a higher-order difunctor sum, without exposing- the internal representation of sums. -}-caseHD :: (f a b i -> c) -> (g a b i -> c) -> (f :+: g) a b i -> c-caseHD f g x = case x of- Inl x -> f x- Inr x -> g x--instance (HDifunctor f, HDifunctor g) => HDifunctor (f :+: g) where- hdimap f g (Inl e) = Inl (hdimap f g e)- hdimap f g (Inr e) = Inr (hdimap f g e)--instance (HDitraversable f, HDitraversable g) => HDitraversable (f :+: g) where- hdimapM f (Inl e) = Inl `liftM` hdimapM f e- hdimapM f (Inr e) = Inr `liftM` hdimapM f e---- | Signature containment relation for automatic injections. The left-hand must--- be an atomic signature, where as the right-hand side must have a list-like--- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,--- non-examples include @f :+: g :<: f :+: (g :+: h)@ and--- @f :<: (f :+: g) :+: h@.-class (sub :: (* -> *) -> (* -> *) -> * -> *) :<: sup where- inj :: sub a b :-> sup a b- proj :: NatM Maybe (sup a b) (sub a b)--instance (:<:) f f where- inj = id- proj = Just--instance (:<:) f (f :+: g) where- inj = Inl- proj (Inl x) = Just x- proj (Inr _) = Nothing--instance (f :<: g) => (:<:) f (h :+: g) where- inj = Inr . inj- proj (Inr x) = proj x- proj (Inl _) = Nothing----- Products-infixr 8 :*:---- |Formal product of signatures (higher-order difunctors).-data (f :*: g) a b = f a b :*: g a b--ffst :: (f :*: g) a b -> f a b-ffst (x :*: _) = x--fsnd :: (f :*: g) a b -> g a b -fsnd (_ :*: x) = x----- Constant Products-infixr 7 :&:--{-| This data type adds a constant product to a signature. -}-data (f :&: p) (a :: * -> *) (b :: * -> *) i = f a b i :&: p--instance HDifunctor f => HDifunctor (f :&: p) where- hdimap f g (v :&: c) = hdimap f g v :&: c--instance HDitraversable f => HDitraversable (f :&: p) where- hdimapM f (v :&: c) = liftM (:&: c) (hdimapM f v)--{-| This class defines how to distribute an annotation over a sum of- signatures. -}-class DistAnn (s :: (* -> *) -> (* -> *) -> * -> *) p s' | s' -> s, s' -> p where- {-| Inject an annotation over a signature. -}- injectA :: p -> s a b :-> s' a b- {-| Project an annotation from a signature. -}- projectA :: s' a b :-> (s a b O.:&: p)--class RemA (s :: (* -> *) -> (* -> *) -> * -> *) s' | s -> s' where- {-| Remove annotations from a signature. -}- remA :: s a b :-> s' a b--instance (RemA s s') => RemA (f :&: p :+: s) (f :+: s') where- remA (Inl (v :&: _)) = Inl v- remA (Inr v) = Inr $ remA v--instance RemA (f :&: p) f where- remA (v :&: _) = v--instance DistAnn f p (f :&: p) where- injectA c v = v :&: c-- projectA (v :&: p) = v O.:&: p--instance (DistAnn s p s') => DistAnn (f :+: s) p ((f :&: p) :+: s') where- injectA c (Inl v) = Inl (v :&: c)- injectA c (Inr v) = Inr $ injectA c v-- projectA (Inl (v :&: p)) = Inl v O.:&: p- projectA (Inr v) = let (v' O.:&: p) = projectA v- in Inr v' O.:&: p
− src/Data/Comp/MultiParam/Ordering.hs
@@ -1,67 +0,0 @@-{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,- UndecidableInstances, IncoherentInstances, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.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.MultiParam.Ordering- (- POrd(..),- OrdHD(..)- ) where--import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Sum-import Data.Comp.MultiParam.Ops-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.FreshM-import Data.Comp.MultiParam.Equality---- |Ordering of parametric values.-class PEq a => POrd a where- pcompare :: a i -> a j -> FreshM Ordering--instance Ord a => POrd (K a) where- pcompare (K x) (K y) = return $ compare x y--{-| Signature ordering. An instance @OrdHD f@ gives rise to an instance- @Ord (Term f)@. -}-class EqHD f => OrdHD f where- compareHD :: POrd a => f Name a i -> f Name a j -> FreshM Ordering--{-| 'OrdHD' is propagated through sums. -}-instance (OrdHD f, OrdHD g) => OrdHD (f :+: g) where- compareHD (Inl x) (Inl y) = compareHD x y- compareHD (Inl _) (Inr _) = return LT- compareHD (Inr x) (Inr y) = compareHD x y- compareHD (Inr _) (Inl _) = return GT--{-| From an 'OrdHD' difunctor an 'Ord' instance of the corresponding term type- can be derived. -}-instance OrdHD f => OrdHD (Cxt h f) where- compareHD (In e1) (In e2) = compareHD e1 e2- compareHD (Hole h1) (Hole h2) = pcompare h1 h2- compareHD (Var p1) (Var p2) = pcompare p1 p2- compareHD (In _) _ = return LT- compareHD (Hole _) (In _) = return GT- compareHD (Hole _) (Var _) = return LT- compareHD (Var _) _ = return GT--instance POrd Name where- pcompare x y = return $ compare (nameCoerce x) y--instance (OrdHD f, POrd a) => POrd (Cxt h f Name a) where- pcompare = compareHD--{-| Ordering of terms. -}-instance (HDifunctor f, OrdHD f) => Ord (Term f i) where- compare (Term x) (Term y) = evalFreshM $ compareHD x y
− src/Data/Comp/MultiParam/Show.hs
@@ -1,42 +0,0 @@-{-# LANGUAGE TypeOperators, FlexibleInstances, TypeSynonymInstances,- IncoherentInstances, UndecidableInstances, TemplateHaskell, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Show--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines showing of signatures, which lifts to showing of terms.-------------------------------------------------------------------------------------module Data.Comp.MultiParam.Show- (- ShowHD(..)- ) where--import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.Ops-import Data.Comp.MultiParam.Derive-import Data.Comp.MultiParam.FreshM---- Lift ShowHD to sums-$(derive [liftSum] [''ShowHD])--{-| From an 'ShowHD' higher-order difunctor an 'ShowHD' instance of the- corresponding term type can be derived. -}-instance (HDifunctor f, ShowHD f) => ShowHD (Cxt h f) where- showHD (In t) = showHD $ hfmap (K . showHD) t- showHD (Hole h) = unK h- showHD (Var p) = return $ show p--{-| Printing of terms. -}-instance (HDifunctor f, ShowHD f) => Show (Term f i) where- show = evalFreshM . showHD . toCxt . unTerm--instance (ShowHD f, Show p) => ShowHD (f :&: p) where- showHD (x :&: p) = do sx <- showHD x- return $ sx ++ " :&: " ++ show p
− src/Data/Comp/MultiParam/Sum.hs
@@ -1,180 +0,0 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,- FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,- ScopedTypeVariables, TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Sum--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module provides the infrastructure to extend signatures.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Sum- (- (:<:),- (:+:),- caseHD,-- -- * Projections for Signatures and Terms- proj,- proj2,- proj3,- proj4,- proj5,- proj6,- proj7,- proj8,- proj9,- proj10,- project,- project2,- project3,- project4,- project5,- project6,- project7,- project8,- project9,- project10,- deepProject,- deepProject2,- deepProject3,- deepProject4,- deepProject5,- deepProject6,- deepProject7,- deepProject8,- deepProject9,- deepProject10,-- -- * Injections for Signatures and Terms- inj,- inj2,- inj3,- inj4,- inj5,- inj6,- inj7,- inj8,- inj9,- inj10,- inject,- inject2,- inject3,- inject4,- inject5,- inject6,- inject7,- inject8,- inject9,- inject10,- deepInject,- deepInject2,- deepInject3,- deepInject4,- deepInject5,- deepInject6,- deepInject7,- deepInject8,- deepInject9,- deepInject10,-- injectCxt,- liftCxt- ) where--import Prelude hiding (sequence)-import Control.Monad hiding (sequence)-import Data.Comp.MultiParam.Term-import Data.Comp.MultiParam.Algebra-import Data.Comp.MultiParam.Ops-import Data.Comp.MultiParam.Derive.Projections-import Data.Comp.MultiParam.Derive.Injections-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.HDitraversable--$(liftM concat $ mapM projn [2..10])---- |Project the outermost layer of a term to a sub signature. If the signature--- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.-project :: (g :<: f) => NatM Maybe (Cxt h f a b) (g a (Cxt h f a b))-project (In t) = proj t-project (Hole _) = Nothing-project (Var _) = Nothing--$(liftM concat $ mapM projectn [2..10])---- | Tries to coerce a term/context to a term/context over a sub-signature. If--- the signature @g@ is compound of /n/ atomic signatures, use--- @deepProject@/n/ instead.-deepProject :: (HDitraversable g, g :<: f) => Term f i -> Maybe (Term g i)-{-# INLINE deepProject #-}-deepProject = appTSigFunM' proj--$(liftM concat $ mapM deepProjectn [2..10])-{-# INLINE deepProject2 #-}-{-# INLINE deepProject3 #-}-{-# INLINE deepProject4 #-}-{-# INLINE deepProject5 #-}-{-# INLINE deepProject6 #-}-{-# INLINE deepProject7 #-}-{-# INLINE deepProject8 #-}-{-# INLINE deepProject9 #-}-{-# INLINE deepProject10 #-}--$(liftM concat $ mapM injn [2..10])---- |Inject a term where the outermost layer is a sub signature. If the signature--- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.-inject :: (g :<: f) => g a (Cxt h f a b) :-> Cxt h f a b-inject = In . inj--$(liftM concat $ mapM injectn [2..10])---- |Inject a term over a sub signature to a term over larger signature. If the--- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/--- instead.-deepInject :: (HDifunctor g, g :<: f) => CxtFun g f-{-# INLINE deepInject #-}-deepInject = appSigFun inj--$(liftM concat $ mapM deepInjectn [2..10])-{-# INLINE deepInject2 #-}-{-# INLINE deepInject3 #-}-{-# INLINE deepInject4 #-}-{-# INLINE deepInject5 #-}-{-# INLINE deepInject6 #-}-{-# INLINE deepInject7 #-}-{-# INLINE deepInject8 #-}-{-# INLINE deepInject9 #-}-{-# INLINE deepInject10 #-}--{-| This function injects a whole context into another context. -}-injectCxt :: (HDifunctor g, g :<: f) => Cxt h g a (Cxt h f a b) :-> Cxt h f a b-injectCxt (In t) = inject $ hfmap injectCxt t-injectCxt (Hole x) = x-injectCxt (Var p) = Var p--{-| This function lifts the given functor to a context. -}-liftCxt :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a b-liftCxt g = simpCxt $ inj g--instance (Show (f a b i), Show (g a b i)) => Show ((f :+: g) a b i) where- show (Inl v) = show v- show (Inr v) = show v--instance (Ord (f a b i), Ord (g a b i)) => Ord ((f :+: g) a b i) where- compare (Inl _) (Inr _) = LT- compare (Inr _) (Inl _) = GT- compare (Inl x) (Inl y) = compare x y- compare (Inr x) (Inr y) = compare x y--instance (Eq (f a b i), Eq (g a b i)) => Eq ((f :+: g) a b i) where- (Inl x) == (Inl y) = x == y- (Inr x) == (Inr y) = x == y - _ == _ = False
− src/Data/Comp/MultiParam/Term.hs
@@ -1,123 +0,0 @@-{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,- MultiParamTypeClasses, TypeOperators, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.MultiParam.Term--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines the central notion of /generalised parametrised terms/--- and their generalisation to generalised parametrised contexts.--------------------------------------------------------------------------------------module Data.Comp.MultiParam.Term- (- Cxt(..),- Hole,- NoHole,- Term(..),- Trm,- Context,- simpCxt,- toCxt,- hfmapCxt,- hdimapMCxt,- ParamFunctor (..)- ) where--import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)-import Data.Comp.MultiParam.HDifunctor-import Data.Comp.MultiParam.HDitraversable-import Control.Monad -import Unsafe.Coerce-import Data.Maybe (fromJust)--{-| This data type represents contexts over a signature. Contexts are terms- containing zero or more holes, and zero or more parameters. The first- parameter is a phantom type indicating whether the context has holes. The- second paramater is the signature of the context, in the form of a- "Data.Comp.MultiParam.HDifunctor". The third parameter is the type of- parameters, the fourth parameter is the type of holes, and the fifth- parameter is the GADT type. -}-data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> * where- In :: f a (Cxt h f a b) i -> Cxt h f a b i- Hole :: b i -> Cxt Hole f a b i- Var :: a i -> Cxt h f a b i--{-| Phantom type used to define 'Context'. -}-data Hole--{-| Phantom type used to define 'Term'. -}-data NoHole--{-| A context may contain holes. -}-type Context = Cxt Hole--{-| \"Preterms\" |-}-type Trm f a = Cxt NoHole f a (K ())--{-| A term is a context with no holes, where all occurrences of the- contravariant parameter is fully parametric. -}-newtype Term f i = Term{unTerm :: forall a. Trm f a i}--{-| Convert a difunctorial value into a context. -}-simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b-{-# INLINE simpCxt #-}-simpCxt = In . hfmap Hole--toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b-{-# INLINE toCxt #-}-toCxt = unsafeCoerce---- | This is an instance of 'hfmap' for 'Cxt'.-hfmapCxt :: forall h f a b b'. HDifunctor f- => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'-hfmapCxt f = run- where run :: Cxt h f a b :-> Cxt h f a b'- run (In t) = In $ hfmap run t- run (Var a) = Var a- run (Hole b) = Hole $ f b---- | This is an instance of 'hdimapM' for 'Cxt'.-hdimapMCxt :: forall h f a b b' m . (HDitraversable f, Monad m)- => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')-hdimapMCxt f = run- where run :: NatM m (Cxt h f a b) (Cxt h f a b')- run (In t) = liftM In $ hdimapM run t- run (Var a) = return $ Var a- run (Hole b) = liftM Hole (f b)- - - -{-| Monads for which embedded @Trm@ values, which are parametric at top level,- can be made into monadic @Term@ values, i.e. \"pushing the parametricity- inwards\". -}-class ParamFunctor m where- termM :: (forall a. m (Trm f a i)) -> m (Term f i)--coerceTermM :: ParamFunctor m => (forall a. m (Trm f a i)) -> m (Term f i)-{-# INLINE coerceTermM #-}-coerceTermM t = unsafeCoerce t--{-# RULES- "termM/coerce'" termM = coerceTermM- #-}--instance ParamFunctor Maybe where- termM Nothing = Nothing- termM x = Just (Term $ fromJust x)--instance ParamFunctor (Either a) where- termM (Left x) = Left x- termM x = Right (Term $ fromRight x)- where fromRight :: Either a b -> b- fromRight (Right x) = x- fromRight _ = error "fromRight: Left"--instance ParamFunctor [] where- termM [] = []- termM l = Term (head l) : termM (tail l)
src/Data/Comp/Ops.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances, FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,- ScopedTypeVariables, FunctionalDependencies, UndecidableInstances #-}+ ScopedTypeVariables, FunctionalDependencies, UndecidableInstances,+ TypeFamilies, DataKinds, ConstraintKinds #-} -------------------------------------------------------------------------------- -- |@@ -35,6 +36,12 @@ data (f :+: g) e = Inl (f e) | Inr (g e) +fromInl :: (f :+: g) e -> Maybe (f e)+fromInl = caseF Just (const Nothing)++fromInr :: (f :+: g) e -> Maybe (g e)+fromInr = caseF (const Nothing) Just + {-| 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@@ -71,28 +78,159 @@ sequence (Inl e) = Inl `liftM` sequence e sequence (Inr e) = Inr `liftM` sequence e --- | Signature containment relation for automatic injections. The left-hand must--- be an atomic signature, where as the right-hand side must have a list-like--- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,--- non-examples include @f :+: g :<: f :+: (g :+: h)@ and--- @f :<: (f :+: g) :+: h@.-class sub :<: sup where- inj :: sub a -> sup a- proj :: sup a -> Maybe (sub a)+infixl 5 :<:+infixl 5 :=: -instance (:<:) f f where- inj = id- proj = Just+data Pos = Here | GoLeft Pos | GoRight Pos | Sum Pos Pos+data Emb = NotFound | Ambiguous | Found Pos -instance (:<:) f (f :+: g) where- inj = Inl- proj (Inl x) = Just x- proj (Inr _) = Nothing -instance (f :<: g) => (:<:) f (h :+: g) where- inj = Inr . inj- proj (Inr x) = proj x- proj (Inl _) = Nothing+type family GetEmb (f :: * -> *) (g :: * -> *) :: Emb where+ GetEmb f f = Found Here+ GetEmb f (g1 :+: g2) = Pick f (g1 :+: g2) (GetEmb f g1) (GetEmb f g2)+ GetEmb f g = NotFound+++type family Pick f g (e1 :: Emb) (r :: Emb) :: Emb where+ Pick f g (Found x) (Found y) = Ambiguous+ Pick f g Ambiguous y = Ambiguous+ Pick f g x Ambiguous = Ambiguous+ Pick f g (Found x) y = Found (GoLeft x)+ Pick f g x (Found y) = Found (GoRight y)+ Pick f g x y = Split f g++type family Split (f :: * -> *) (g :: * -> *) :: Emb where+ Split (f1 :+: f2) g = Pick2 (GetEmb f1 g) (GetEmb f2 g) + Split f g = NotFound++type family Pick2 (e1 :: Emb) (r :: Emb) :: Emb where+ Pick2 (Found x) (Found y) = Found (Sum x y)+ Pick2 Ambiguous y = Ambiguous+ Pick2 x Ambiguous = Ambiguous+ Pick2 NotFound y = NotFound+ Pick2 x NotFound = NotFound++data EmbD (e :: Emb) (f :: * -> *) (g :: * -> *) where+ HereD :: EmbD (Found Here) f f+ GoLeftD :: EmbD (Found p) f g -> EmbD (Found (GoLeft p)) f (g :+: g')+ GoRightD :: EmbD (Found p) f g -> EmbD (Found (GoRight p)) f (g' :+: g)+ SumD :: EmbD (Found p1) f1 g -> EmbD (Found p2) f2 g -> EmbD (Found (Sum p1 p2)) (f1 :+: f2) g++class GetEmbD (e :: Emb) (f :: * -> *) (g :: * -> *) where+ getEmbD :: EmbD e f g++instance GetEmbD (Found Here) f f where+ getEmbD = HereD++instance GetEmbD (Found p) f g => GetEmbD (Found (GoLeft p)) f (g :+: g') where+ getEmbD = GoLeftD getEmbD++instance GetEmbD (Found p) f g => GetEmbD (Found (GoRight p)) f (g' :+: g) where+ getEmbD = GoRightD getEmbD++instance (GetEmbD (Found p1) f1 g, GetEmbD (Found p2) f2 g) + => GetEmbD (Found (Sum p1 p2)) (f1 :+: f2) g where+ getEmbD = SumD getEmbD getEmbD+++-- The following definitions are used to reject instances of :<: such+-- as @F :+: F :<: F@ or @F :+: (F :+: G) :<: F :+: G@.++data SimpPos = SimpHere | SimpLeft SimpPos | SimpRight SimpPos++data Res = CompPos SimpPos Pos | SingPos SimpPos+++type family DestrPos (e :: Pos) :: Res where+ DestrPos (GoLeft e) = ResLeft (DestrPos e)+ DestrPos (GoRight e) = ResRight (DestrPos e)+ DestrPos (Sum e1 e2) = ResSum (DestrPos e1) e2+ DestrPos Here = SingPos SimpHere++type family ResLeft (r :: Res) :: Res where+ ResLeft (CompPos p e) = CompPos (SimpLeft p) (GoLeft e)+ ResLeft (SingPos p) = SingPos (SimpLeft p)++type family ResRight (r :: Res) :: Res where+ ResRight (CompPos p e) = CompPos (SimpRight p) (GoRight e)+ ResRight (SingPos p) = SingPos (SimpRight p)++type family ResSum (r :: Res) (e :: Pos) :: Res where+ ResSum (CompPos p e1) e2 = CompPos p (Sum e1 e2)+ ResSum (SingPos p) e = CompPos p e++type family Or x y where+ Or x False = x+ Or False y = y+ Or x y = True++type family In (p :: SimpPos) (e :: Pos) :: Bool where+ In SimpHere e = True+ In p Here = True+ In (SimpLeft p) (GoLeft e) = In p e+ In (SimpRight p) (GoRight e) = In p e+ In p (Sum e1 e2) = Or (In p e1) (In p e2)+ In p e = False++type family Duplicates' (r :: Res) :: Bool where+ Duplicates' (SingPos p) = False+ Duplicates' (CompPos p e) = Or (In p e) (Duplicates' (DestrPos e))++type family Duplicates (e :: Emb) where+ Duplicates (Found p) = Duplicates' (DestrPos p)++-- This class is used to produce more informative error messages+class NoDup (b :: Bool) (f :: * -> *) (g :: * -> *)+instance NoDup False f g++inj_ :: EmbD e f g -> f a -> g a+inj_ HereD x = x+inj_ (GoLeftD e) x = Inl (inj_ e x)+inj_ (GoRightD e) x = Inr (inj_ e x)+inj_ (SumD e1 e2) x = case x of+ Inl y -> inj_ e1 y+ Inr y -> inj_ e2 y++-- | The :<: constraint is a conjunction of two constraints. The first+-- one is used to construct the evidence that is used to implement the+-- injection and projection functions. The first constraint alone+-- would allow instances such as @F :+: F :<: F@ or @F :+: (F :+: G)+-- :<: F :+: G@ which have multiple occurrences of the same+-- sub-signature on the left-hand side. Such instances are usually+-- unintended and yield injection functions that are not+-- injective. The second constraint excludes such instances.+type f :<: g = (GetEmbD (GetEmb f g) f g, NoDup (Duplicates (GetEmb f g)) f g)++inj :: forall f g a . (f :<: g) => f a -> g a+inj = inj_ (getEmbD :: EmbD (GetEmb f g) f g)++type f :=: g = (f :<: g, g :<: f) +++proj_ :: EmbD e f g -> g a -> Maybe (f a)+proj_ HereD x = Just x+proj_ (GoLeftD p) x = case x of + Inl y -> proj_ p y+ _ -> Nothing+proj_ (GoRightD p) x = case x of + Inr x -> proj_ p x+ _ -> Nothing+proj_ (SumD p1 p2) x = case proj_ p1 x of+ Just y -> Just (Inl y)+ _ -> case proj_ p2 x of+ Just y -> Just (Inr y)+ _ -> Nothing+++proj :: forall f g a . (f :<: g) => g a -> Maybe (f a)+proj = proj_ (getEmbD :: EmbD (GetEmb f g) f g)++spl :: (f :<: f1 :+: f2) => (f1 a -> b) -> (f2 a -> b) -> f a -> b+spl f1 f2 x = case inj x of + Inl y -> f1 y+ Inr y -> f2 y++ -- Products
− src/Data/Comp/Param.hs
@@ -1,32 +0,0 @@------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Patrick Bahr <paba@diku.dk>, Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines the infrastructure necessary to use--- /Parametric Compositional Data Types/. Parametric Compositional Data Types --- is an extension of Compositional Data Types with parametric--- higher-order abstract syntax (PHOAS) for usage with binders. Examples of--- usage are bundled with the package in the library--- @examples\/Examples\/Param@.-------------------------------------------------------------------------------------module Data.Comp.Param (- module Data.Comp.Param.Term- , module Data.Comp.Param.Algebra- , module Data.Comp.Param.Difunctor- , module Data.Comp.Param.Sum- , module Data.Comp.Param.Annotation- , module Data.Comp.Param.Equality- ) where--import Data.Comp.Param.Term-import Data.Comp.Param.Algebra-import Data.Comp.Param.Difunctor-import Data.Comp.Param.Sum-import Data.Comp.Param.Annotation-import Data.Comp.Param.Equality
− src/Data/Comp/Param/Algebra.hs
@@ -1,962 +0,0 @@-{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,- FlexibleContexts, CPP #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Algebra--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines the notion of algebras and catamorphisms, and their--- generalizations to e.g. monadic versions and other (co)recursion schemes.--------------------------------------------------------------------------------------module Data.Comp.Param.Algebra (- -- * Algebras & Catamorphisms- Alg,- free,- cata,- cata',- appCxt,- - -- * Monadic Algebras & Catamorphisms- AlgM,- algM,- freeM,- cataM,- cataM',-- -- * Term Homomorphisms- CxtFun,- SigFun,- Hom,- appHom,- appHom',- compHom,- appSigFun,- appSigFun',- compSigFun,- compHomSigFun,- compSigFunHom,- hom,- compAlg,- compAlgSigFun,-- -- * Monadic Term Homomorphisms- CxtFunM,- SigFunM,- HomM,- SigFunMD,- HomMD,- sigFunM,- appHomM,- appTHomM,- appHomM',- appTHomM',- homM,- homMD,- appSigFunM,- appTSigFunM,- appSigFunM',- appTSigFunM',- appSigFunMD,- appTSigFunMD,- compHomM,- compHomM',- compSigFunM,- compSigFunHomM,- compSigFunHomM',- compAlgSigFunM,- compAlgSigFunM',- compAlgM,- compAlgM',-- -- * Coalgebras & Anamorphisms- Coalg,- ana,- CoalgM,- anaM,-- -- * R-Algebras & Paramorphisms- RAlg,- para,- RAlgM,- paraM,-- -- * R-Coalgebras & Apomorphisms- RCoalg,- apo,- RCoalgM,- apoM,-- -- * CV-Algebras & Histomorphisms- CVAlg,- histo,- CVAlgM,- histoM,-- -- * CV-Coalgebras & Futumorphisms- CVCoalg,- futu,- CVCoalg',- futu',- CVCoalgM,- futuM- ) where--import Prelude hiding (sequence, mapM)-import Control.Monad hiding (sequence, mapM)-import Data.Comp.Param.Term-import Data.Comp.Param.Ops-import Data.Comp.Param.Difunctor-import Data.Comp.Param.Ditraversable--{-| This type represents an algebra over a difunctor @f@ and carrier @a@. -}-type Alg f a = f a a -> a---{-| Construct a catamorphism for contexts over @f@ with holes of type @b@, from- the given algebra. -}-free :: forall h f a b. Difunctor f- => Alg f a -> (b -> a) -> Cxt h f a b -> a-free f g = run- where run :: Cxt h f a b -> a- run (In t) = f (difmap run t)- run (Hole x) = g x- run (Var p) = p--{-| Construct a catamorphism from the given algebra. -}-cata :: forall f a. Difunctor f => Alg f a -> Term f -> a -{-# NOINLINE [1] cata #-}-cata f (Term t) = run t- where run :: Trm f a -> a- run (In t) = f (difmap run t)- run (Var x) = x--{-| A generalisation of 'cata' from terms over @f@ to contexts over @f@, where- the holes have the type of the algebra carrier. -}-cata' :: Difunctor f => Alg f a -> Cxt h f a a -> a-{-# INLINE cata' #-}-cata' f = free f id--{-| This function applies a whole context into another context. -}-appCxt :: Difunctor f => Context f a (Cxt h f a b) -> Cxt h f a b-appCxt (In t) = In (difmap appCxt t)-appCxt (Hole x) = x-appCxt (Var p) = Var p--{-| This type represents a monadic algebra. It is similar to 'Alg' but- the return type is monadic. -}-type AlgM m f a = f a a -> m a--{-| Convert a monadic algebra into an ordinary algebra with a monadic- carrier. -}-algM :: (Ditraversable f, Monad m) => AlgM m f a -> Alg f (m a)-algM f x = disequence (dimap return id x) >>= f--{-| Construct a monadic catamorphism for contexts over @f@ with holes of type- @b@, from the given monadic algebra. -}-freeM :: forall m h f a b. (Ditraversable f, Monad m)- => AlgM m f a -> (b -> m a) -> Cxt h f a b -> m a-freeM f g = run- where run :: Cxt h f a b -> m a- run (In t) = f =<< dimapM run t- run (Hole x) = g x- run (Var p) = return p--{-| Construct a monadic catamorphism from the given monadic algebra. -}-cataM :: forall m f a. (Ditraversable f, Monad m) => AlgM m f a -> Term f -> m a-{-# NOINLINE [1] cataM #-}-cataM algm (Term t) = run t- where run :: Trm f a -> m a- run (In t) = algm =<< dimapM run t- run (Var x) = return x--{-| A generalisation of 'cataM' from terms over @f@ to contexts over @f@, where- the holes have the type of the monadic algebra carrier. -}-cataM' :: forall m h f a. (Ditraversable f, Monad m)- => AlgM m f a -> Cxt h f a (m a) -> m a-{-# NOINLINE [1] cataM' #-}-cataM' f = freeM f id--{-| This type represents a context function. -}-type CxtFun f g = forall h a b. Cxt h f a b -> Cxt h g a b---{-| This type represents a signature function. -}-type SigFun f g = forall a b. f a b -> g a b--{-| This type represents a term homomorphism. -}-type Hom f g = SigFun f (Context g)--{-| Apply a term homomorphism recursively to a term/context. -}-appHom :: forall f g. (Difunctor f, Difunctor g) => Hom f g -> CxtFun f g-{-# NOINLINE [1] appHom #-}-appHom f = run where- run :: CxtFun f g- run (In t) = appCxt (f (difmap run t))- run (Hole x) = Hole x- run (Var p) = Var p--{-| Apply a term homomorphism recursively to a term/context. -}-appHom' :: forall f g. (Difunctor g) => Hom f g -> CxtFun f g-{-# NOINLINE [1] appHom' #-}-appHom' f = run where- run :: CxtFun f g- run (In t) = appCxt (fmapCxt run (f t))- run (Hole x) = Hole x- run (Var p) = Var p--fmapCxt :: Difunctor f => (b -> b') -> Cxt h f a b -> Cxt h f a b'-fmapCxt f = run- where run (In t) = In $ difmap run t- run (Var a) = Var a- run (Hole b) = Hole $ f b--{-| Compose two term homomorphisms. -}-compHom :: (Difunctor g, Difunctor h)- => Hom g h -> Hom f g -> Hom f h-compHom f g = appHom f . g---{-| Compose an algebra with a term homomorphism to get a new algebra. -}-compAlg :: (Difunctor f, Difunctor g) => Alg g a -> Hom f g -> Alg f a-compAlg alg talg = cata' alg . talg--compAlgSigFun :: Alg g a -> SigFun f g -> Alg f a-compAlgSigFun alg sig = alg . sig---{-| This function applies a signature function to the given context. -}-appSigFun :: forall f g. (Difunctor f) => SigFun f g -> CxtFun f g-{-# NOINLINE [1] appSigFun #-}-appSigFun f = run- where run (In t) = In $ f $ difmap run t- run (Var x) = Var x- run (Hole x) = Hole x--- implementation via term homomorphisms--- appSigFun f = appHom $ hom f----- | This function applies a signature function to the given--- context. This is a top-bottom variant of 'appSigFun'.-appSigFun' :: forall f g. (Difunctor g) => SigFun f g -> CxtFun f g-{-# NOINLINE [1] appSigFun' #-}-appSigFun' f = run- where run (In t) = In $ difmap run $ f t- run (Var x) = Var x- run (Hole x) = Hole x--{-| This function composes two signature functions. -}-compSigFun :: SigFun g h -> SigFun f g -> SigFun f h-compSigFun f g = f . g--{-| This function composes a term homomorphism and a signature function. -}-compHomSigFun :: Hom g h -> SigFun f g -> Hom f h-compHomSigFun f g = f . g--{-| This function composes a term homomorphism and a signature function. -}-compSigFunHom :: (Difunctor g) => SigFun g h -> Hom f g -> Hom f h-compSigFunHom f g = appSigFun f . g---{-| Lifts the given signature function to the canonical term homomorphism. -}-hom :: Difunctor g => SigFun f g -> Hom f g-hom f = simpCxt . f--{-| This type represents a monadic signature function. -}-type SigFunM m f g = forall a b. f a b -> m (g a b)--{-| This type represents a monadic context function. -}-type CxtFunM m f g = forall h . SigFunM m (Cxt h f) (Cxt h g)--{-| This type represents a monadic signature function. It is similar to- 'SigFunM' but has monadic values also in the domain. -}-type SigFunMD m f g = forall a b. f a (m b) -> m (g a b)--{-| This type represents a monadic term homomorphism. -}-type HomM m f g = SigFunM m f (Context g)--{-| This type represents a monadic term homomorphism. It is similar to- 'HomM' but has monadic values also in the domain. -}-type HomMD m f g = SigFunMD m f (Context g)--{-| Lift the given signature function to a monadic signature function. Note that- term homomorphisms are instances of signature functions. Hence this function- also applies to term homomorphisms. -}-sigFunM :: Monad m => SigFun f g -> SigFunM m f g-sigFunM f = return . f--{-| Lift the given signature function to a monadic term homomorphism. -}-homM :: (Difunctor g, Monad m) => SigFunM m f g -> HomM m f g-homM f = liftM simpCxt . f---- | Apply a monadic term homomorphism recursively to a--- term/context. The monad is sequenced bottom-up.-appHomM :: forall f g m. (Ditraversable f, Difunctor g, Monad m)- => HomM m f g -> CxtFunM m f g-{-# NOINLINE [1] appHomM #-}-appHomM f = run- where run :: CxtFunM m f g- run (In t) = liftM appCxt . f =<< dimapM run t- run (Hole x) = return (Hole x)- run (Var p) = return (Var p)--{-| A restricted form of |appHomM| which only works for terms. -}-appTHomM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)- => HomM m f g -> Term f -> m (Term g)-appTHomM f (Term t) = termM (appHomM f t)----- | Apply a monadic term homomorphism recursively to a--- term/context. The monad is sequence top-down.-appHomM' :: forall f g m. (Ditraversable g, Monad m)- => HomM m f g -> CxtFunM m f g-appHomM' f = run- where run :: CxtFunM m f g- run (In t) = liftM appCxt . dimapMCxt run =<< f t- run (Var p) = return (Var p)- run (Hole x) = return (Hole x)--dimapMCxt :: (Ditraversable f, Monad m)- => (b -> m b') -> Cxt h f a b -> m (Cxt h f a b')-dimapMCxt f = run- where run (In t) = liftM In $ dimapM run t- run (Var a) = return $ Var a- run (Hole b) = liftM Hole (f b)--{-| A restricted form of |appHomM'| which only works for terms. -}-appTHomM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g)- => HomM m f g -> Term f -> m (Term g)-appTHomM' f (Term t) = termM (appHomM' f t)- --{-| This function constructs the unique monadic homomorphism from the- initial term algebra to the given term algebra. -}-homMD :: forall f g m. (Difunctor f, Difunctor g, Monad m)- => HomMD m f g -> CxtFunM m f g-homMD f = run - where run :: CxtFunM m f g- run (In t) = liftM appCxt (f (difmap run t))- run (Hole x) = return (Hole x)- run (Var p) = return (Var p)--{-| This function applies a monadic signature function to the given context. -}-appSigFunM :: forall m f g. (Ditraversable f, Monad m)- => SigFunM m f g -> CxtFunM m f g-appSigFunM f = run- where run :: CxtFunM m f g- run (In t) = liftM In . f =<< dimapM run t- run (Var x) = return $ Var x- run (Hole x) = return $ Hole x--- implementation via term homomorphisms--- appSigFunM f = appHomM $ hom' f--{-| A restricted form of |appSigFunM| which only works for terms. -}-appTSigFunM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)- => SigFunM m f g -> Term f -> m (Term g)-appTSigFunM f (Term t) = termM (appSigFunM f t)---- | This function applies a monadic signature function to the given--- context. This is a 'top-down variant of 'appSigFunM'.-appSigFunM' :: forall m f g. (Ditraversable g, Monad m)- => SigFunM m f g -> CxtFunM m f g-appSigFunM' f = run- where run :: CxtFunM m f g- run (In t) = liftM In . dimapM run =<< f t- run (Var x) = return $ Var x- run (Hole x) = return $ Hole x--{-| A restricted form of |appSigFunM'| which only works for terms. -}-appTSigFunM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g)- => SigFunM m f g -> Term f -> m (Term g)-appTSigFunM' f (Term t) = termM (appSigFunM' f t)--{-| This function applies a signature function to the given context. -}-appSigFunMD :: forall f g m. (Ditraversable f, Difunctor g, Monad m)- => SigFunMD m f g -> CxtFunM m f g-appSigFunMD f = run - where run :: CxtFunM m f g- run (In t) = liftM In (f (difmap run t))- run (Hole x) = return (Hole x)- run (Var p) = return (Var p)--{-| A restricted form of |appSigFunMD| which only works for terms. -}-appTSigFunMD :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)- => SigFunMD m f g -> Term f -> m (Term g)-appTSigFunMD f (Term t) = termM (appSigFunMD f t)--{-| Compose two monadic term homomorphisms. -}-compHomM :: (Ditraversable g, Difunctor h, Monad m)- => HomM m g h -> HomM m f g -> HomM m f h-compHomM f g = appHomM f <=< g--{-| Compose two monadic term homomorphisms. -}-compHomM' :: (Ditraversable h, Monad m) => HomM m g h -> HomM m f g -> HomM m f h-compHomM' f g = appHomM' f <=< g--{-{-| Compose two monadic term homomorphisms. -}-compHomM_ :: (Difunctor h, Difunctor g, Monad m)- => Hom g h -> HomM m f g -> HomM m f h-compHomM_ f g = liftM (appHom f) . g--{-| Compose two monadic term homomorphisms. -}-compHomSigFunM :: Monad m => HomM m g h -> SigFunM m f g -> HomM m f h-compHomSigFunM f g = f <=< g-}--{-| Compose two monadic term homomorphisms. -}-compSigFunHomM :: (Ditraversable g, Monad m)- => SigFunM m g h -> HomM m f g -> HomM m f h-compSigFunHomM f g = appSigFunM f <=< g--{-| Compose two monadic term homomorphisms. -}-compSigFunHomM' :: (Ditraversable h, Monad m)- => SigFunM m g h -> HomM m f g -> HomM m f h-compSigFunHomM' f g = appSigFunM' f <=< g--{-| Compose a monadic algebra with a monadic term homomorphism to get a new- monadic algebra. -}-compAlgM :: (Ditraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a-compAlgM alg talg = freeM alg return <=< talg---{-| Compose a monadic algebra with a term homomorphism to get a new monadic- algebra. -}-compAlgM' :: (Ditraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a-compAlgM' alg talg = freeM alg return . talg--{-| Compose a monadic algebra with a monadic signature function to get a new- monadic algebra. -}-compAlgSigFunM :: Monad m => AlgM m g a -> SigFunM m f g -> AlgM m f a-compAlgSigFunM alg talg = alg <=< talg---{-| Compose a monadic algebra with a signature function to get a new monadic- algebra. -}-compAlgSigFunM' :: AlgM m g a -> SigFun f g -> AlgM m f a-compAlgSigFunM' alg talg = alg . talg--{-| This function composes two monadic signature functions. -}-compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h-compSigFunM f g = f <=< g---------------------- Coalgebras ---------------------{-| This type represents a coalgebra over a difunctor @f@ and carrier @a@. The- list of @(a,b)@s represent the parameters that may occur in the constructed- value. The first component represents the seed of the parameter,- and the second component is the (polymorphic) parameter itself. If @f@ is- itself a binder, then the parameters bound by @f@ can be passed to the- covariant argument, thereby making them available to sub terms. -}-type Coalg f a = forall b. a -> [(a,b)] -> Either b (f b (a,[(a,b)]))--{-| Construct an anamorphism from the given coalgebra. -}-ana :: Difunctor f => Coalg f a -> a -> Term f-ana f x = Term $ anaAux f x- where anaAux :: Difunctor f => Coalg f a -> a -> (forall a. Trm f a)- anaAux f x = run (x,[])- where run (a,bs) = case f a bs of- Left p -> Var p- Right t -> In $ difmap run t--{-| This type represents a monadic coalgebra over a difunctor @f@ and carrier- @a@. -}-type CoalgM m f a = forall b. a -> [(a,b)] -> m (Either b (f b (a,[(a,b)])))--{-| Construct a monadic anamorphism from the given monadic coalgebra. -}-anaM :: forall a m f. (Ditraversable f, Monad m)- => CoalgM m f a -> a -> forall a. m (Trm f a)-anaM f x = run (x,[])- where run (a,bs) = do c <- f a bs- case c of- Left p -> return $ Var p- Right t -> liftM In $ dimapM run t-------------------------------------- R-Algebras & Paramorphisms -------------------------------------{-| This type represents an r-algebra over a difunctor @f@ and carrier @a@. -}-type RAlg f a = f a (Trm f a, a) -> a--{-| Construct a paramorphism from the given r-algebra. -}-para :: forall f a. Difunctor f => RAlg f a -> Term f -> a-para f (Term t) = run t- where run :: Trm f a -> a- run (In t) = f $ difmap (\x -> (x, run x)) t- run (Var x) = x--{-| This type represents a monadic r-algebra over a difunctor @f@ and carrier- @a@. -}-type RAlgM m f a = f a (Trm f a, a) -> m a-{-| Construct a monadic paramorphism from the given monadic r-algebra. -}-paraM :: forall m f a. (Ditraversable f, Monad m) => RAlgM m f a -> Term f -> m a-paraM f (Term t) = run t- where run :: Trm f a -> m a- run (In t) = f =<< dimapM (\x -> run x >>= \y -> return (x, y)) t- run (Var x) = return x-------------------------------------- R-Coalgebras & Apomorphisms -------------------------------------{-| This type represents an r-coalgebra over a difunctor @f@ and carrier @a@. -}-type RCoalg f a = forall b. a -> [(a,b)] -> Either b (f b (Either (Trm f b) (a,[(a,b)])))--{-| Construct an apomorphism from the given r-coalgebra. -}-apo :: Difunctor f => RCoalg f a -> a -> Term f-apo f x = Term (apoAux f x)- where apoAux :: Difunctor f => RCoalg f a -> a -> (forall a. Trm f a)- apoAux coa x = run (x,[])- where -- run :: (a,[(a,b)]) -> Trm f b- run (a,bs) = case coa a bs of- Left x -> Var x- Right t -> In $ difmap run' t- -- run' :: Either (Trm f b) (a,[(a,b)]) -> Trm f b- run' (Left t) = t- run' (Right x) = run x----{-| This type represents a monadic r-coalgebra over a functor @f@ and carrier- @a@. -}-type RCoalgM m f a = forall b. a -> [(a,b)] -> m (Either b (f b (Either (Trm f b) (a,[(a,b)]))))--{-| Construct a monadic apomorphism from the given monadic r-coalgebra. -}-apoM :: forall f m a. (Ditraversable f, Monad m)- => RCoalgM m f a -> a -> forall a. m (Trm f a)-apoM coa x = run (x,[]) - where run (a,bs) = do- res <- coa a bs- case res of- Left x -> return $ Var x- Right t -> liftM In $ dimapM run' t- run' (Left t) = return t- run' (Right x) = run x---------------------------------------- CV-Algebras & Histomorphisms ---------------------------------------{-| This type represents a cv-algebra over a difunctor @f@ and carrier @a@. -}-type CVAlg f a f' = f a (Trm f' a) -> a---- | This function applies 'projectA' at the tip of the term.-projectTip :: DistAnn f a f' => Trm f' a -> a-projectTip (In v) = snd $ projectA v-projectTip (Var p) = p--{-| Construct a histomorphism from the given cv-algebra. -}-histo :: forall f f' a. (Difunctor f, DistAnn f a f')- => CVAlg f a f' -> Term f -> a-histo alg = projectTip . cata run- where run :: Alg f (Trm f' a)- run v = In $ injectA (alg v') v'- where v' = dimap Var id v--{-| This type represents a monadic cv-algebra over a functor @f@ and carrier- @a@. -}-type CVAlgM m f a f' = f a (Trm f' a) -> m a--{-| Construct a monadic histomorphism from the given monadic cv-algebra. -}-histoM :: forall f f' m a. (Ditraversable f, Monad m, DistAnn f a f')- => CVAlgM m f a f' -> Term f -> m a-histoM alg (Term t) = liftM projectTip (run t)- where run :: Trm f a -> m (Trm f' a)- run (In t) = do t' <- dimapM run t- r <- alg t'- return $ In $ injectA r t'- run (Var p) = return $ Var p----------------------------------------- CV-Coalgebras & Futumorphisms ----------------------------------------{-| This type represents a cv-coalgebra over a difunctor @f@ and carrier @a@.- The list of @(a,b)@s represent the parameters that may occur in the- constructed value. The first component represents the seed of the parameter,- and the second component is the (polymorphic) parameter itself. If @f@ is- itself a binder, then the parameters bound by @f@ can be passed to the- covariant argument, thereby making them available to sub terms. -}-type CVCoalg f a = forall b. a -> [(a,b)]- -> Either b (f b (Context f b (a,[(a,b)])))--{-| Construct a futumorphism from the given cv-coalgebra. -}-futu :: Difunctor f => CVCoalg f a -> a -> Term f-futu f x = Term (futuAux f x)- where futuAux :: Difunctor f => CVCoalg f a -> a -> (forall a. Trm f a)- futuAux coa x = run (x,[])- where run (a,bs) = case coa a bs of- Left p -> Var p- Right t -> In $ difmap run' t- run' (In t) = In $ difmap run' t- run' (Hole x) = run x- run' (Var p) = Var p--{-| This type represents a monadic cv-coalgebra over a difunctor @f@ and carrier- @a@. -}-type CVCoalgM m f a = forall b. a -> [(a,b)]- -> m (Either b (f b (Context f b (a,[(a,b)]))))--{-| Construct a monadic futumorphism from the given monadic cv-coalgebra. -}-futuM :: forall f a m. (Ditraversable f, Monad m) =>- CVCoalgM m f a -> a -> forall a. m (Trm f a)-futuM coa x = run (x,[])- where run (a,bs) = do c <- coa a bs- case c of - Left p -> return $ Var p- Right t -> liftM In $ dimapM run' t- run' (In t) = liftM In $ dimapM run' t- run' (Hole x) = run x- run' (Var p) = return $ Var p--{-| This type represents a generalised cv-coalgebra over a difunctor @f@ and- carrier @a@. -}-type CVCoalg' f a = forall b. a -> [(a,b)] -> Context f b (a,[(a,b)])--{-| Construct a futumorphism from the given generalised cv-coalgebra. -}-futu' :: Difunctor f => CVCoalg' f a -> a -> Term f-futu' f x = Term (futuAux' f x)- where futuAux' :: Difunctor f => CVCoalg' f a -> a -> (forall a. Trm f a)- futuAux' coa x = run (x,[])- where run (a,bs) = run' $ coa a bs- run' (In t) = In $ difmap run' t- run' (Hole x) = run x- run' (Var p) = Var p--{----------------------------------------------- functions only used for rewrite rules ------------------------------------------------appAlgHom :: forall f g d. Difunctor g => Alg g d -> Hom f g -> Term f -> d-{-# NOINLINE [1] appAlgHom #-}-appAlgHom alg hom (Term t) = run t where- run :: Trm f d -> d- run (In t) = run' $ hom t- run (Var a) = a- run' :: Context g d (Trm f d) -> d- run' (In t) = alg $ fmap run' t- run' (Var a) = a- run' (Hole x) = run x----- | This function applies a signature function after a term homomorphism.-appSigFunHom :: forall f g h. (Difunctor g)- => SigFun g h -> Hom f g -> CxtFun f h-{-# NOINLINE [1] appSigFunHom #-}-appSigFunHom f g = run where- run :: CxtFun f h- run (In t) = run' $ g t- run (Var a) = Var a- run (Hole h) = Hole h- run' :: Context g a (Cxt h' f a b) -> Cxt h' h a b- run' (In t) = In $ f $ fmap run' t- run' (Var a) = Var a- run' (Hole h) = run h--appAlgHomM :: forall m g f d. Ditraversable g- => AlgM m g d -> HomM m f g -> Term f -> m d-appAlgHomM alg hom (Term t) = run t where- run :: Trm f d -> m d- run (In t) = run' =<< hom t- run (Var a) = return a- run' :: Context g d (Trm f d) -> m d- run' (In t) = alg =<< dimapM run' t- run' (Var a) = return a- run' (Hole x) = run x--appHomHomM :: forall m f g h. (Ditraversable g, Difunctor h)- => HomM m g h -> HomM m f g -> CxtFunM m f h-appHomHomM f g = run where--- run :: CxtFunM m f h- run (In t) = run' =<< g t- run (Var a) = return $ Var a- run (Hole h) = return $ Hole h--- run' :: Context g Any (Cxt h' f Any b) -> m (Cxt h' h Any b)- run' (In t) = liftM appCxt $ f =<< dimapM run' t- run' (Var a) = return $ Var a- run' (Hole h) = run h--appSigFunHomM :: forall m f g h. Ditraversable g- => SigFunM m g h -> HomM m f g -> CxtFunM m f h-appSigFunHomM f g = run where--- run :: CxtFunM m f h- run (In t) = run' =<< g t- run (Var a) = return $ Var a- run (Hole h) = return $ Hole h--- run' :: Context g Any (Cxt h' f Any b) -> m (Cxt h' h Any b)- run' (In t) = liftM In $ f =<< dimapM run' t- run' (Var a) = return $ Var a- run' (Hole h) = run h------------------------- rewrite rules ------------------------#ifndef NO_RULES-{-# RULES- "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.- cata a (appHom h x) = cata (compAlg a h) x;-- "cata/appHom'" forall (a :: Alg g d) (h :: Hom f g) x.- cata a (appHom' h x) = appAlgHom a h x;-- "cata/appSigFun" forall (a :: Alg g d) (h :: SigFun f g) x.- cata a (appSigFun h x) = cata (compAlgSigFun a h) x;-- "cata/appSigFun'" forall (a :: Alg g d) (h :: SigFun f g) x.- cata a (appSigFun' h x) = appAlgHom a (hom h) x;-- "cata/appSigFunHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)- (h :: Hom f1 f2) x.- cata f (appSigFunHom g h x) = appAlgHom (compAlgSigFun f g) h x;-- "appAlgHom/appHom" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.- appAlgHom a h (appHom f x) = cata (compAlg a (compHom h f)) x;-- "appAlgHom/appHom'" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.- appAlgHom a h (appHom' f x) = appAlgHom a (compHom h f) x;-- "appAlgHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.- appAlgHom a h (appSigFun f x) = cata (compAlg a (compHomSigFun h f)) x;-- "appAlgHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.- appAlgHom a h (appSigFun' f x) = appAlgHom a (compHomSigFun h f) x;-- "appAlgHom/appSigFunHom" forall (a :: Alg i d) (f :: Hom f g) (g :: SigFun g h)- (h :: Hom h i) x.- appAlgHom a h (appSigFunHom g f x)- = appAlgHom a (compHom (compHomSigFun h g) f) x;-- "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.- appHom a (appHom h x) = appHom (compHom a h) x;-- "appHom'/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.- appHom' a (appHom' h x) = appHom' (compHom a h) x;-- "appHom'/appHom" forall (a :: Hom g h) (h :: Hom f g) x.- appHom' a (appHom h x) = appHom (compHom a h) x;-- "appHom/appHom'" forall (a :: Hom g h) (h :: Hom f g) x.- appHom a (appHom' h x) = appHom' (compHom a h) x;- - "appSigFun/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.- appSigFun f (appSigFun g x) = appSigFun (compSigFun f g) x;-- "appSigFun'/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.- appSigFun' f (appSigFun' g x) = appSigFun' (compSigFun f g) x;-- "appSigFun/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.- appSigFun f (appSigFun' g x) = appSigFunHom f (hom g) x;-- "appSigFun'/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.- appSigFun' f (appSigFun g x) = appSigFun (compSigFun f g) x;-- "appHom/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.- appHom f (appSigFun g x) = appHom (compHomSigFun f g) x;-- "appHom/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.- appHom f (appSigFun' g x) = appHom' (compHomSigFun f g) x;-- "appHom'/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.- appHom' f (appSigFun' g x) = appHom' (compHomSigFun f g) x;-- "appHom'/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.- appHom' f (appSigFun g x) = appHom (compHomSigFun f g) x;- - "appSigFun/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.- appSigFun f (appHom g x) = appSigFunHom f g x;-- "appSigFun'/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.- appSigFun' f (appHom' g x) = appHom' (compSigFunHom f g) x;-- "appSigFun/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.- appSigFun f (appHom' g x) = appSigFunHom f g x;-- "appSigFun'/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.- appSigFun' f (appHom g x) = appHom (compSigFunHom f g) x;- - "appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)- (h :: SigFun f1 f2) x.- appSigFunHom f g (appSigFun h x)- = appSigFunHom f (compHomSigFun g h) x;-- "appSigFunHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)- (h :: SigFun f1 f2) x.- appSigFunHom f g (appSigFun' h x)- = appSigFunHom f (compHomSigFun g h) x;-- "appSigFunHom/appHom" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)- (h :: Hom f1 f2) x.- appSigFunHom f g (appHom h x)- = appSigFunHom f (compHom g h) x;-- "appSigFunHom/appHom'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)- (h :: Hom f1 f2) x.- appSigFunHom f g (appHom' h x)- = appSigFunHom f (compHom g h) x;-- "appSigFun/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)- (h :: Hom f1 f2) x.- appSigFun f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;-- "appSigFun'/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)- (h :: Hom f1 f2) x.- appSigFun' f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;-- "appHom/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)- (h :: Hom f1 f2) x.- appHom f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;-- "appHom'/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)- (h :: Hom f1 f2) x.- appHom' f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;-- "appSigFunHom/appSigFunHom" forall (f1 :: SigFun f4 f5) (f2 :: Hom f3 f4)- (f3 :: SigFun f2 f3) (f4 :: Hom f1 f2) x.- appSigFunHom f1 f2 (appSigFunHom f3 f4 x)- = appSigFunHom f1 (compHom (compHomSigFun f2 f3) f4) x; #-}--{-# RULES - "cataM/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.- appHomM h x >>= cataM a = appAlgHomM a h x;-- "cataM/appHomM'" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.- appHomM' h x >>= cataM a = appAlgHomM a h x;-- "cataM/appSigFunM" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.- appSigFunM h x >>= cataM a = appAlgHomM a (homM h) x;-- "cataM/appSigFunM'" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.- appSigFunM' h x >>= cataM a = appAlgHomM a (homM h) x;-- "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.- cataM a (appHom h x) = appAlgHomM a (sigFunM h) x;-- "cataM/appHom'" forall (a :: AlgM m g d) (h :: Hom f g) x.- cataM a (appHom' h x) = appAlgHomM a (sigFunM h) x;-- "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.- cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;-- "cataM/appSigFun'" forall (a :: AlgM m g d) (h :: SigFun f g) x.- cataM a (appSigFun' h x) = appAlgHomM a (sigFunM $ hom h) x;-- "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.- cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;-- "cataM/appSigFunHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: Hom f g) x.- cataM a (appSigFunHom g f x) = appAlgHomM a (sigFunM $ compSigFunHom g f) x;-- "appHomM/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.- appHomM h x >>= appHomM a = appHomM (compHomM a h) x;-- "appHomM/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM h x >>= appHomM a = appHomM (compHomSigFunM a h) x;-- "appHomM/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.- appHomM' h x >>= appHomM a = appHomHomM a h x;-- "appHomM/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM' h x >>= appHomM a = appHomHomM a (homM h) x;-- "appHomM'/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.- appHomM h x >>= appHomM' a = appHomM' (compHomM' a h) x;-- "appHomM'/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;-- "appHomM'/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.- appHomM' h x >>= appHomM' a = appHomM' (compHomM' a h) x;-- "appHomM'/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM' h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;-- "appHomM/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.- appHomM a (appHom h x) = appHomHomM a (sigFunM h) x;-- "appHomM/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.- appHomM a (appSigFun h x) = appHomHomM a (sigFunM $ hom h) x;-- "appHomM'/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.- appHomM' a (appHom h x) = appHomM' (compHomM' a (sigFunM h)) x;-- "appHomM'/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.- appHomM' a (appSigFun h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;-- "appHomM/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.- appHomM a (appHom' h x) = appHomHomM a (sigFunM h) x;-- "appHomM/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.- appHomM a (appSigFun' h x) = appHomHomM a (sigFunM $ hom h) x;-- "appHomM'/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.- appHomM' a (appHom' h x) = appHomM' (compHomM' a (sigFunM h)) x;-- "appHomM'/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.- appHomM' a (appSigFun' h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;-- "appSigFunM/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.- appHomM h x >>= appSigFunM a = appSigFunHomM a h x;-- "appSigFunHomM/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM h x >>= appSigFunM a = appSigFunM (compSigFunM a h) x;-- "appSigFunM/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.- appHomM' h x >>= appSigFunM a = appSigFunHomM a h x;-- "appSigFunM/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM' h x >>= appSigFunM a = appSigFunHomM a (homM h) x;-- "appSigFunM'/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.- appHomM h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;-- "appSigFunM'/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;-- "appSigFunM'/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.- appHomM' h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;-- "appSigFunM'/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.- appSigFunM' h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;-- "appSigFunM/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.- appSigFunM a (appHom h x) = appSigFunHomM a (sigFunM h) x;-- "appSigFunM/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.- appSigFunM a (appSigFun h x) = appSigFunHomM a (sigFunM $ hom h) x;-- "appSigFunM'/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.- appSigFunM' a (appHom h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;-- "appSigFunM'/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.- appSigFunM' a (appSigFun h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;-- "appSigFunM/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.- appSigFunM a (appHom' h x) = appSigFunHomM a (sigFunM h) x;-- "appSigFunM/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.- appSigFunM a (appSigFun' h x) = appSigFunHomM a (sigFunM $ hom h) x;-- "appSigFunM'/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.- appSigFunM' a (appHom' h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;-- "appSigFunM'/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.- appSigFunM' a (appSigFun' h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;--- "appHom/appHomM" forall (a :: Hom g h) (h :: HomM m f g) x.- appHomM h x >>= (return . appHom a) = appHomM (compHomM_ a h) x; #-}-#endif--}
− src/Data/Comp/Param/Annotation.hs
@@ -1,79 +0,0 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,- UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Annotation--- Copyright : (c) 2010-2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines annotations on signatures.--------------------------------------------------------------------------------------module Data.Comp.Param.Annotation- (- (:&:) (..),- (:*:) (..),- DistAnn (..),- RemA (..),- liftA,- liftA',- stripA,- propAnn,- propAnnM,- ann,- project'- ) where--import Data.Comp.Param.Difunctor-import Data.Comp.Param.Term-import Data.Comp.Param.Sum-import Data.Comp.Param.Ops-import Data.Comp.Param.Algebra--import Control.Monad--{-| Transform a function with a domain constructed from a functor to a function- with a domain constructed with the same functor, but with an additional- annotation. -}-liftA :: (RemA s s') => (s' a b -> t) -> s a b -> t-liftA f v = f (remA v)--{-| Transform a function with a domain constructed from a functor to a function- with a domain constructed with the same functor, but with an additional- annotation. -}-liftA' :: (DistAnn s' p s, Difunctor s')- => (s' a b -> Cxt h s' c d) -> s a b -> Cxt h s c d-liftA' f v = let (v',p) = projectA v- in ann p (f v')--{-| Strip the annotations from a term over a functor with annotations. -}-stripA :: (RemA g f, Difunctor g) => CxtFun g f-stripA = appSigFun remA--{-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism- over the same signatures, but extended with annotations. -}-propAnn :: (DistAnn f p f', DistAnn g p g', Difunctor g) - => Hom f g -> Hom f' g'-propAnn hom f' = ann p (hom f)- where (f,p) = projectA f'--{-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic- term homomorphism over the same signatures, but extended with annotations. -}-propAnnM :: (DistAnn f p f', DistAnn g p g', Difunctor g, Monad m) - => HomM m f g -> HomM m f' g'-propAnnM hom f' = liftM (ann p) (hom f)- where (f,p) = projectA f'--{-| Annotate each node of a term with a constant value. -}-ann :: (DistAnn f p g, Difunctor f) => p -> CxtFun f g-ann c = appSigFun (injectA c)--{-| This function is similar to 'project' but applies to signatures-with an annotation which is then ignored. -}-project' :: (RemA f f', s :<: f') => Cxt h f a b -> Maybe (s a (Cxt h f a b))-project' (In x) = proj $ remA x-project' _ = Nothing
− src/Data/Comp/Param/Derive.hs
@@ -1,57 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module contains functionality for automatically deriving boilerplate--- code using Template Haskell. Examples include instances of 'Difunctor',--- 'Difoldable', and 'Ditraversable'.--------------------------------------------------------------------------------------module Data.Comp.Param.Derive- (- derive,- -- |Derive boilerplate instances for parametric signatures, i.e.- -- signatures for parametric compositional data types.-- -- ** EqD- module Data.Comp.Param.Derive.Equality,- -- ** OrdD- module Data.Comp.Param.Derive.Ordering,- -- ** ShowD- module Data.Comp.Param.Derive.Show,- -- ** Difunctor- module Data.Comp.Param.Derive.Difunctor,- -- ** Ditraversable- module Data.Comp.Param.Derive.Ditraversable,- -- ** Smart Constructors- module Data.Comp.Param.Derive.SmartConstructors,- -- ** Smart Constructors w/ Annotations- module Data.Comp.Param.Derive.SmartAConstructors,- -- ** Lifting to Sums- liftSum- ) where--import Data.Comp.Derive.Utils (derive, liftSumGen)-import Data.Comp.Param.Derive.Equality-import Data.Comp.Param.Derive.Ordering-import Data.Comp.Param.Derive.Show-import Data.Comp.Param.Derive.Difunctor-import Data.Comp.Param.Derive.Ditraversable-import Data.Comp.Param.Derive.SmartConstructors-import Data.Comp.Param.Derive.SmartAConstructors-import Data.Comp.Param.Ops ((:+:), caseD)--import Language.Haskell.TH--{-| Given the name of a type class, where the first parameter is a difunctor,- lift it to sums of difunctors. Example: @class ShowD f where ...@ is lifted- as @instance (ShowD f, ShowD g) => ShowD (f :+: g) where ... @. -}-liftSum :: Name -> Q [Dec]-liftSum = liftSumGen 'caseD ''(:+:)
− src/Data/Comp/Param/Derive/Difunctor.hs
@@ -1,96 +0,0 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.Functor--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @Difunctor@.--------------------------------------------------------------------------------------module Data.Comp.Param.Derive.Difunctor- (- Difunctor,- makeDifunctor- ) where--import Data.Comp.Derive.Utils-import Data.Comp.Param.Difunctor-import Language.Haskell.TH--{-| Derive an instance of 'Difunctor' for a type constructor of any parametric- kind taking at least two arguments. -}-makeDifunctor :: Name -> Q [Dec]-makeDifunctor fname = do- -- Comments below apply to the example where name = T, args = [a,b,c], and- -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type- -- declaration: T a b c = X c | Y a c | Z (b -> c)- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- -- coArg = c (covariant difunctor argument)- let coArg :: Name = tyVarBndrName $ last args- -- conArg = b (contravariant difunctor argument)- let conArg :: Name = tyVarBndrName $ last $ init args- -- argNames = [a]- let argNames = map (VarT . tyVarBndrName) (init $ init args)- -- compType = T a- let complType = foldl AppT (ConT name) argNames- -- classType = Difunctor (T a)- let classType = AppT (ConT ''Difunctor) complType- -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- dimapDecl <- funD 'dimap (map (dimapClause conArg coArg) constrs')- return [InstanceD [] classType [dimapDecl]]- where dimapClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- dimapClause conArg coArg (constr, args) = do- fn <- newName "_f"- gn <- newName "_g"- varNs <- newNames (length args) "x"- let f = varE fn- let g = varE gn- let fp = VarP fn- let gp = VarP gn- -- Pattern for the constructor- let pat = ConP constr $ map VarP varNs- body <- dimapArgs conArg coArg f g (zip varNs args) (conE constr)- return $ Clause [fp, gp, pat] (NormalB body) []- dimapArgs :: Name -> Name -> ExpQ -> ExpQ- -> [(Name, Type)] -> ExpQ -> ExpQ- dimapArgs _ _ _ _ [] acc =- acc- dimapArgs conArg coArg f g ((x,tp):tps) acc =- dimapArgs conArg coArg f g tps- (acc `appE` (dimapArg conArg coArg tp f g `appE` varE x))- -- Given the name of the difunctor variables, a type, and the two- -- arguments to dimap, return the expression that should be applied- -- to the parameter of the given type.- -- Example: dimapArg a b (a -> b) f g yields the expression- -- [|\x -> g . x . f|]- dimapArg :: Name -> Name -> Type -> ExpQ -> ExpQ -> ExpQ- dimapArg conArg coArg tp f g- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) = [| id |]- | otherwise =- case tp of- VarT a | a == conArg -> f- | a == coArg -> g- AppT (AppT ArrowT tp1) tp2 -> do- xn <- newName "x"- let ftp1 = dimapArg conArg coArg tp1 f g- let ftp2 = dimapArg conArg coArg tp2 f g- lamE [varP xn]- (infixE (Just ftp2)- [|(.)|]- (Just $ infixE (Just $ varE xn)- [|(.)|]- (Just ftp1)))- SigT tp' _ ->- dimapArg conArg coArg tp' f g- _ ->- if containsType tp (VarT conArg) then- [| dimap $f $g |]- else- [| fmap $g |]
− src/Data/Comp/Param/Derive/Ditraversable.hs
@@ -1,88 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.Ditraversable--- Copyright : (c) 2010-2011 Patrick Bahr--- License : BSD3--- Maintainer : Patrick Bahr <paba@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @Ditraversable@.--------------------------------------------------------------------------------------module Data.Comp.Param.Derive.Ditraversable- (- Ditraversable,- makeDitraversable- ) where--import Data.Comp.Derive.Utils-import Data.Comp.Param.Ditraversable-import Data.Traversable (mapM)-import Language.Haskell.TH-import Data.Maybe-import Control.Monad hiding (mapM)-import Prelude hiding (mapM)--iter 0 _ e = e-iter n f e = iter (n-1) f (f `appE` e)--iter' n f e = run n f e- where run 0 _ e = e- run m f e = let f' = iter (m-1) [|fmap|] f- in run (m-1) f (f' `appE` e)--{-| Derive an instance of 'Traversable' for a type constructor of any- first-order kind taking at least one argument. -}-makeDitraversable :: Name -> Q [Dec]-makeDitraversable fname = do- TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname- let fArg = VarT . tyVarBndrName $ last args- aArg = VarT . tyVarBndrName $ last (init args)- funTy = foldl AppT ArrowT [aArg,fArg]- argNames = map (VarT . tyVarBndrName) (init $ init args)- complType = foldl AppT (ConT name) argNames- classType = foldl1 AppT [ConT ''Ditraversable, complType]- normConstrs <- mapM normalConExp constrs- constrs' <- mapM (mkPatAndVars . isFarg fArg funTy) normConstrs- mapMDecl <- funD 'dimapM (map mapMClause constrs')- sequenceDecl <- funD 'disequence (map sequenceClause constrs')- return [InstanceD [] classType [mapMDecl,sequenceDecl]]- where isFarg fArg funTy (constr, args) =- (constr, map (\t -> (t `containsType'` fArg, t `containsType'` funTy)) args)- checksAarg aArg (_,args) = any (`containsType` aArg) args- filterVar _ _ nonFarg ([],[]) x = nonFarg x- filterVar farg _ _ ([depth],[]) x = farg depth x- filterVar _ aarg _ ([_],[depth]) x = aarg depth x- filterVar _ _ _ _ _ = error "functor variable occurring twice in argument type"- filterVars args varNs farg aarg nonFarg = zipWith (filterVar farg aarg nonFarg) args varNs- mkCPat constr varNs = ConP constr $ map mkPat varNs- mkPat = VarP- mkPatAndVars (constr, args) =- do varNs <- newNames (length args) "x"- return (conE constr, mkCPat constr varNs,- any (not . null . fst) args || any (not . null . snd) args, map varE varNs,- catMaybes $ filterVars args varNs (\x y -> Just (False,x,y)) (\x y -> Just (True, x, y)) (const Nothing))-- -- Note: the monadic versions are not defined- -- applicatively, as this results in a considerable- -- performance penalty (by factor 2)!- mapMClause (con, pat,hasFargs,allVars, fvars) =- do fn <- newName "f"- let f = varE fn- fp = if hasFargs then VarP fn else WildP- conAp = foldl appE con allVars- addDi False _ x = x- addDi True d x = [|dimapM $(f)|]- conBind (fun,d,x) y = [| $(iter d [|mapM|] (addDi fun d f)) $(varE x) >>= $(lamE [varP x] y)|]- body <- foldr conBind [|return $conAp|] fvars- return $ Clause [fp, pat] (NormalB body) []- sequenceClause (con, pat,hasFargs,allVars, fvars) =- do let conAp = foldl appE con allVars- varE' False _ x = varE x- varE' True d x = appE (iter d [|fmap|] [|disequence|]) (varE x)- conBind (fun,d, x) y = [| $(iter' d [|sequence|] (varE' fun d x)) >>= $(lamE [varP x] y)|]- body <- foldr conBind [|return $conAp|] fvars- return $ Clause [pat] (NormalB body) []
− src/Data/Comp/Param/Derive/Equality.hs
@@ -1,84 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,- ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.Equality--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @EqD@.-------------------------------------------------------------------------------------module Data.Comp.Param.Derive.Equality- (- EqD(..),- makeEqD- ) where--import Data.Comp.Derive.Utils-import Data.Comp.Param.FreshM hiding (Name)-import Data.Comp.Param.Equality-import Control.Monad-import Language.Haskell.TH hiding (Cxt, match)--{-| Derive an instance of 'EqD' for a type constructor of any parametric- kind taking at least two arguments. -}-makeEqD :: Name -> Q [Dec]-makeEqD fname = do- -- Comments below apply to the example where name = T, args = [a,b,c], and- -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type- -- declaration: T a b c = X c | Y a c | Z (b -> c)- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- -- coArg = c (covariant difunctor argument)- let coArg :: Name = tyVarBndrName $ last args- -- conArg = b (contravariant difunctor argument)- let conArg :: Name = tyVarBndrName $ last $ init args- -- argNames = [a]- let argNames = map (VarT . tyVarBndrName) (init $ init args)- -- compType = T a- let complType = foldl AppT (ConT name) argNames- -- classType = Difunctor (T a)- let classType = AppT (ConT ''EqD) complType- -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- let defC = if length constrs < 2 then- []- else- [clause [wildP,wildP] (normalB [|return False|]) []]- eqDDecl <- funD 'eqD (map (eqDClause conArg coArg) constrs' ++ defC)- let context = map (\arg -> ClassP ''Eq [arg]) argNames- return [InstanceD context classType [eqDDecl]]- where eqDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- eqDClause conArg coArg (constr, args) = do- varXs <- newNames (length args) "x"- varYs <- newNames (length args) "y"- -- Patterns for the constructors- let patx = ConP constr $ map VarP varXs- let paty = ConP constr $ map VarP varYs- body <- eqDBody conArg coArg (zip3 varXs varYs args)- return $ Clause [patx,paty] (NormalB body) []- eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ- eqDBody conArg coArg x =- [|liftM and (sequence $(listE $ map (eqDB conArg coArg) x))|]- eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ- eqDB conArg coArg (x, y, tp)- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) =- [| return $ $(varE x) == $(varE y) |]- | otherwise =- case tp of- VarT a- | a == coArg -> [| peq $(varE x) $(varE y) |]- AppT (AppT ArrowT (VarT a)) _- | a == conArg ->- [| withName (\v -> peq ($(varE x) v) ($(varE y) v)) |]- SigT tp' _ ->- eqDB conArg coArg (x, y, tp')- _ ->- if containsType tp (VarT conArg) then- [| eqD $(varE x) $(varE y) |]- else- [| peq $(varE x) $(varE y) |]
− src/Data/Comp/Param/Derive/Injections.hs
@@ -1,86 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.Injections--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Derive functions for signature injections.--------------------------------------------------------------------------------------module Data.Comp.Param.Derive.Injections- (- injn,- injectn,- deepInjectn- ) where--import Language.Haskell.TH hiding (Cxt)-import Data.Comp.Param.Difunctor-import Data.Comp.Param.Term-import Data.Comp.Param.Algebra (CxtFun, appSigFun)-import Data.Comp.Param.Ops ((:+:)(..), (:<:)(..))--injn :: Int -> Q [Dec]-injn n = do- let i = mkName $ "inj" ++ show n- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let avar = mkName "a"- let bvar = mkName "b"- let xvar = mkName "x"- let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]- sequence $ sigD i (genSig fvars gvar avar bvar) : d- where genSig fvars gvar avar bvar = do- let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let tp' = arrowT `appT` (tp `appT` varT avar `appT` varT bvar)- `appT` (varT gvar `appT` varT avar `appT`- varT bvar)- forallT (map PlainTV $ gvar : avar : bvar : fvars)- (sequence cxt) tp'- genDecl x n = [| case $(varE x) of- Inl x -> $(varE $ mkName "inj") x- Inr x -> $(varE $ mkName $ "inj" ++- if n > 2 then show (n - 1) else "") x |]-injectn :: Int -> Q [Dec]-injectn n = do- let i = mkName ("inject" ++ show n)- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let avar = mkName "a"- let bvar = mkName "b"- let d = [funD i [clause [] (normalB $ genDecl n) []]]- sequence $ sigD i (genSig fvars gvar avar bvar) : d- where genSig fvars gvar avar bvar = do- let hvar = mkName "h"- let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar- `appT` varT avar `appT` varT bvar- let tp'' = arrowT `appT` (tp `appT` varT avar `appT` tp') `appT` tp'- forallT (map PlainTV $ hvar : gvar : avar : bvar : fvars)- (sequence cxt) tp''- genDecl n = [| In . $(varE $ mkName $ "inj" ++ show n) |]--deepInjectn :: Int -> Q [Dec]-deepInjectn n = do- let i = mkName ("deepInject" ++ show n)- let fvars = map (\n -> mkName $ 'f' : show n) [1..n]- let gvar = mkName "g"- let d = [funD i [clause [] (normalB $ genDecl n) []]]- sequence $ sigD i (genSig fvars gvar) : d- where genSig fvars gvar = do- let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars- let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)- (map varT fvars)- let cxt' = classP ''Difunctor [tp]- let tp' = conT ''CxtFun `appT` tp `appT` varT gvar- forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'- genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
− src/Data/Comp/Param/Derive/Ordering.hs
@@ -1,93 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,- ScopedTypeVariables #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.Ordering--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @OrdD@.-------------------------------------------------------------------------------------module Data.Comp.Param.Derive.Ordering- (- OrdD(..),- makeOrdD- ) where--import Data.Comp.Param.FreshM hiding (Name)-import Data.Comp.Param.Ordering-import Data.Comp.Derive.Utils-import Language.Haskell.TH hiding (Cxt)-import Control.Monad (liftM)--{-| Derive an instance of 'OrdD' for a type constructor of any parametric- kind taking at least two arguments. -}-makeOrdD :: Name -> Q [Dec]-makeOrdD fname = do- -- Comments below apply to the example where name = T, args = [a,b,c], and- -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type- -- declaration: T a b c = X c | Y a c | Z (b -> c)- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- -- coArg = c (covariant difunctor argument)- let coArg :: Name = tyVarBndrName $ last args- -- conArg = b (contravariant difunctor argument)- let conArg :: Name = tyVarBndrName $ last $ init args- -- argNames = [a]- let argNames = map (VarT . tyVarBndrName) (init $ init args)- -- compType = T a- let complType = foldl AppT (ConT name) argNames- -- classType = Difunctor (T a)- let classType = AppT (ConT ''OrdD) complType- -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- compareDDecl <- funD 'compareD (compareDClauses conArg coArg constrs')- let context = map (\arg -> ClassP ''Ord [arg]) argNames- return [InstanceD context classType [compareDDecl]]- where compareDClauses :: Name -> Name -> [(Name,[Type])] -> [ClauseQ]- compareDClauses _ _ [] = []- compareDClauses conArg coArg constrs = - let constrs' = constrs `zip` [1..]- constPairs = [(x,y)| x<-constrs', y <- constrs']- in map (genClause conArg coArg) constPairs- genClause conArg coArg ((c,n),(d,m))- | n == m = genEqClause conArg coArg c- | n < m = genLtClause c d- | otherwise = genGtClause c d- genEqClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- genEqClause conArg coArg (constr, args) = do - varXs <- newNames (length args) "x"- varYs <- newNames (length args) "y"- let patX = ConP constr $ map VarP varXs- let patY = ConP constr $ map VarP varYs- body <- eqDBody conArg coArg (zip3 varXs varYs args)- return $ Clause [patX, patY] (NormalB body) []- eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ- eqDBody conArg coArg x =- [|liftM compList (sequence $(listE $ map (eqDB conArg coArg) x))|]- eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ- eqDB conArg coArg (x, y, tp)- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) =- [| return $ compare $(varE x) $(varE y) |]- | otherwise =- case tp of- VarT a- | a == coArg -> [| pcompare $(varE x) $(varE y) |]- AppT (AppT ArrowT (VarT a)) _- | a == conArg ->- [| withName (\v -> pcompare ($(varE x) v) ($(varE y) v)) |]- SigT tp' _ ->- eqDB conArg coArg (x, y, tp')- _ ->- if containsType tp (VarT conArg) then- [| compareD $(varE x) $(varE y) |]- else- [| pcompare $(varE x) $(varE y) |]- genLtClause (c, _) (d, _) =- clause [recP c [], recP d []] (normalB [| return LT |]) []- genGtClause (c, _) (d, _) =- clause [recP c [], recP d []] (normalB [| return GT |]) []
− src/Data/Comp/Param/Derive/Projections.hs
@@ -1,101 +0,0 @@-{-# LANGUAGE TemplateHaskell, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.Projections--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Derive functions for signature projections.--------------------------------------------------------------------------------------module Data.Comp.Param.Derive.Projections- (- projn,- projectn,- deepProjectn- ) where--import Language.Haskell.TH hiding (Cxt)-import Control.Monad (liftM)-import Data.Comp.Param.Ditraversable (Ditraversable)-import Data.Comp.Param.Term-import Data.Comp.Param.Algebra (appTSigFunM')-import Data.Comp.Param.Ops ((:+:)(..), (:<:)(..))--projn :: Int -> Q [Dec]-projn n = do- let p = mkName $ "proj" ++ show n- let gvars = map (\n -> mkName $ 'g' : show n) [1..n]- let avar = mkName "a"- let bvar = mkName "b"- let xvar = mkName "x"- let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar bvar) []]]- sequence $ (sigD p $ genSig gvars avar bvar) : d- where genSig gvars avar bvar = do- let fvar = mkName "f"- let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars- let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)- (map varT gvars)- let tp' = arrowT `appT` (varT fvar `appT` varT avar `appT`- varT bvar)- `appT` (conT ''Maybe `appT`- (tp `appT` varT avar `appT` varT bvar))- forallT (map PlainTV $ fvar : avar : bvar : gvars)- (sequence cxt) tp'- genDecl x [g] a b =- [| liftM inj (proj $(varE x)- :: Maybe ($(varT g `appT` varT a `appT` varT b))) |]- genDecl x (g:gs) a b =- [| case (proj $(varE x)- :: Maybe ($(varT g `appT` varT a `appT` varT b))) of- Just y -> Just $ inj y- _ -> $(genDecl x gs a b) |]- genDecl _ _ _ _ = error "genDecl called with empty list"--projectn :: Int -> Q [Dec]-projectn n = do- let p = mkName ("project" ++ show n)- let gvars = map (\n -> mkName $ 'g' : show n) [1..n]- let avar = mkName "a"- let bvar = mkName "b"- let xvar = mkName "x"- let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]- sequence $ (sigD p $ genSig gvars avar bvar) : d- where genSig gvars avar bvar = do- let fvar = mkName "f"- let hvar = mkName "h"- let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars- let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)- (map varT gvars)- let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar- `appT` varT avar `appT` varT bvar- let tp'' = arrowT `appT` tp'- `appT` (conT ''Maybe `appT`- (tp `appT` varT avar `appT` tp'))- forallT (map PlainTV $ hvar : fvar : avar : bvar : gvars)- (sequence cxt) tp''- genDecl x n = [| case $(varE x) of- Hole _ -> Nothing- Var _ -> Nothing- In t -> $(varE $ mkName $ "proj" ++ show n) t |]--deepProjectn :: Int -> Q [Dec]-deepProjectn n = do- let p = mkName ("deepProject" ++ show n)- let gvars = map (\n -> mkName $ 'g' : show n) [1..n]- let d = [funD p [clause [] (normalB $ genDecl n) []]]- sequence $ (sigD p $ genSig gvars) : d- where genSig gvars = do- let fvar = mkName "f"- let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars- let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)- (map varT gvars)- let cxt' = classP ''Ditraversable [tp]- let tp' = arrowT `appT` (conT ''Term `appT` varT fvar)- `appT` (conT ''Maybe `appT` (conT ''Term `appT` tp))- forallT (map PlainTV $ fvar : gvars) (sequence $ cxt' : cxt) tp'- genDecl n = [| appTSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
− src/Data/Comp/Param/Derive/Show.hs
@@ -1,92 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,- ScopedTypeVariables, UndecidableInstances #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.Show--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive instances of @ShowD@.-------------------------------------------------------------------------------------module Data.Comp.Param.Derive.Show- (- ShowD(..),- makeShowD- ) where--import Data.Comp.Derive.Utils-import Data.Comp.Param.FreshM hiding (Name)-import qualified Data.Comp.Param.FreshM as FreshM-import Control.Monad-import Language.Haskell.TH hiding (Cxt, match)-import qualified Data.Traversable as T--{-| Signature printing. An instance @ShowD f@ gives rise to an instance- @Show (Term f)@. -}-class ShowD f where- showD :: f FreshM.Name (FreshM String) -> FreshM String--newtype Dummy = Dummy String--instance Show Dummy where- show (Dummy s) = s--{-| Derive an instance of 'ShowD' for a type constructor of any parametric- kind taking at least two arguments. -}-makeShowD :: Name -> Q [Dec]-makeShowD fname = do- -- Comments below apply to the example where name = T, args = [a,b,c], and- -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type- -- declaration: T a b c = X c | Y a c | Z (b -> c)- TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname- -- coArg = c (covariant difunctor argument)- let coArg :: Name = tyVarBndrName $ last args- -- conArg = b (contravariant difunctor argument)- let conArg :: Name = tyVarBndrName $ last $ init args- -- argNames = [a]- let argNames = map (VarT . tyVarBndrName) (init $ init args)- -- compType = T a- let complType = foldl AppT (ConT name) argNames- -- classType = Difunctor (T a)- let classType = AppT (ConT ''ShowD) complType- -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]- constrs' :: [(Name,[Type])] <- mapM normalConExp constrs- showDDecl <- funD 'showD (map (showDClause conArg coArg) constrs')- let context = map (\arg -> ClassP ''Show [arg]) argNames- return [InstanceD context classType [showDDecl]]- where showDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ- showDClause conArg coArg (constr, args) = do- varXs <- newNames (length args) "x"- -- Pattern for the constructor- let patx = ConP constr $ map VarP varXs- body <- showDBody (nameBase constr) conArg coArg (zip varXs args)- return $ Clause [patx] (NormalB body) []- showDBody :: String -> Name -> Name -> [(Name, Type)] -> ExpQ- showDBody constr conArg coArg x =- [|liftM (unwords . (constr :) .- map (\x -> if elem ' ' x then "(" ++ x ++ ")" else x))- (sequence $(listE $ map (showDB conArg coArg) x))|]- showDB :: Name -> Name -> (Name, Type) -> ExpQ- showDB conArg coArg (x, tp)- | not (containsType tp (VarT conArg)) &&- not (containsType tp (VarT coArg)) =- [| return $ show $(varE x) |]- | otherwise =- case tp of- VarT a- | a == coArg -> [| $(varE x) |]- AppT (AppT ArrowT (VarT a)) _- | a == conArg ->- [| withName (\v -> do body <- $(varE x) v;- return $ "\\" ++ show v ++ " -> " ++ body) |]- SigT tp' _ ->- showDB conArg coArg (x, tp')- _ ->- if containsType tp (VarT conArg) then- [| showD $(varE x) |]- else- [| liftM show $ T.mapM (liftM Dummy) $(varE x) |]
− src/Data/Comp/Param/Derive/SmartAConstructors.hs
@@ -1,47 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.SmartAConstructors--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive smart constructors with annotations for difunctors.--------------------------------------------------------------------------------------module Data.Comp.Param.Derive.SmartAConstructors - (- smartAConstructors- ) where--import Language.Haskell.TH hiding (Cxt)-import Data.Comp.Derive.Utils-import Data.Comp.Param.Ops-import Data.Comp.Param.Term-import Data.Comp.Param.Difunctor--import Control.Monad--{-| Derive smart constructors with annotations for a difunctor. The smart- constructors are similar to the ordinary constructors, but a- 'injectA . dimap Var id' is automatically inserted. -}-smartAConstructors :: Name -> Q [Dec]-smartAConstructors fname = do- TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname- let cons = map abstractConType constrs- liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons- where genSmartConstr targs tname (name, args) = do- let bname = nameBase name- genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args- genSmartConstr' targs tname sname name args = do- varNs <- newNames args "x"- varPr <- newName "_p"- let pats = map varP (varPr : varNs)- vars = map varE varNs- val = appE [|injectA $(varE varPr)|] $- appE [|inj . dimap Var id|] $ foldl appE (conE name) vars- function = [funD sname [clause pats (normalB [|In $val|]) []]]- sequence function
− src/Data/Comp/Param/Derive/SmartConstructors.hs
@@ -1,62 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Derive.SmartConstructors--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ Automatically derive smart constructors for difunctors.--------------------------------------------------------------------------------------module Data.Comp.Param.Derive.SmartConstructors - (- smartConstructors- ) where--import Language.Haskell.TH hiding (Cxt)-import Data.Comp.Derive.Utils-import Data.Comp.Param.Sum-import Data.Comp.Param.Term-import Data.Comp.Param.Difunctor-import Control.Monad--{-| Derive smart constructors for a difunctor. The smart constructors are- similar to the ordinary constructors, but a 'inject . dimap Var id' is- automatically inserted. -}-smartConstructors :: Name -> Q [Dec]-smartConstructors fname = do- TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname- let cons = map abstractConType constrs- liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons- where genSmartConstr targs tname (name, args) = do- let bname = nameBase name- genSmartConstr' targs tname (mkName $ 'i' : bname) name args- genSmartConstr' targs tname sname name args = do- varNs <- newNames args "x"- let pats = map varP varNs- vars = map varE varNs- val = foldl appE (conE name) vars- sig = genSig targs tname sname args- function = [funD sname [clause pats (normalB [|inject (dimap Var id $val)|]) []]]- sequence $ sig ++ function- genSig targs tname sname 0 = (:[]) $ do- hvar <- newName "h"- fvar <- newName "f"- avar <- newName "a"- bvar <- newName "b"- let targs' = init $ init targs- vars = hvar:fvar:avar:bvar:targs'- h = varT hvar- f = varT fvar- a = varT avar- b = varT bvar- ftype = foldl appT (conT tname) (map varT targs')- constr = classP ''(:<:) [ftype, f]- typ = foldl appT (conT ''Cxt) [h, f, a, b]- typeSig = forallT (map PlainTV vars) (sequence [constr]) typ- sigD sname typeSig- genSig _ _ _ _ = []
− src/Data/Comp/Param/Desugar.hs
@@ -1,45 +0,0 @@-{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,- UndecidableInstances, OverlappingInstances, Rank2Types, TypeOperators #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Desugar--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This modules defines the 'Desugar' type class for desugaring of terms.--------------------------------------------------------------------------------------module Data.Comp.Param.Desugar where--import Data.Comp.Param----- |The desugaring term homomorphism.-class (Difunctor f, Difunctor g) => Desugar f g where- desugHom :: Hom f g- desugHom = desugHom' . fmap Hole- desugHom' :: f a (Cxt h g a b) -> Cxt h g a b- desugHom' x = appCxt (desugHom x)---- We make the lifting to sums explicit in order to make the Desugar--- class work with the default instance declaration further below.-instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where- desugHom = caseD desugHom desugHom---- |Desugar a term.-desugar :: Desugar f g => Term f -> Term g-{-# INLINE desugar #-}-desugar (Term t) = Term (appHom desugHom t)---- |Lift desugaring to annotated terms.-desugarA :: (Difunctor f', Difunctor g', DistAnn f p f', DistAnn g p g',- Desugar f g) => Term f' -> Term g'-desugarA (Term t) = Term (appHom (propAnn desugHom) t)---- |Default desugaring instance.-instance (Difunctor f, Difunctor g, f :<: g) => Desugar f g where- desugHom = simpCxt . inj
− src/Data/Comp/Param/Difunctor.hs
@@ -1,36 +0,0 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Difunctor--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines difunctors (Meijer, Hutton, FPCA '95), i.e. binary type--- constructors that are contravariant in the first argument and covariant in--- the second argument.--------------------------------------------------------------------------------------module Data.Comp.Param.Difunctor- (- difmap,- Difunctor(..)- ) where---- | This class represents difunctors, i.e. binary type constructors that are--- contravariant in the first argument and covariant in the second argument.-class Difunctor f where- dimap :: (a -> b) -> (c -> d) -> f b c -> f a d--{-| The canonical example of a difunctor. -}-instance Difunctor (->) where- dimap f g h = g . h . f--difmap :: Difunctor f => (a -> b) -> f c a -> f c b-difmap = dimap id--instance Difunctor f => Functor (f a) where- fmap = difmap
− src/Data/Comp/Param/Ditraversable.hs
@@ -1,28 +0,0 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Ditraversable--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines traversable difunctors.--------------------------------------------------------------------------------------module Data.Comp.Param.Ditraversable- (- Ditraversable(..)- ) where--import Data.Comp.Param.Difunctor--{-| Difunctors representing data structures that can be traversed from left to- right. -}-class Difunctor f => Ditraversable f where- dimapM :: Monad m => (b -> m c) -> f a b -> m (f a c)- dimapM f = disequence . fmap f- disequence :: Monad m => f a (m b) -> m (f a b)- disequence = dimapM id
− src/Data/Comp/Param/Equality.hs
@@ -1,67 +0,0 @@-{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,- UndecidableInstances, IncoherentInstances, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Equality--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines equality for signatures, which lifts to equality for--- terms.-------------------------------------------------------------------------------------module Data.Comp.Param.Equality- (- PEq(..),- EqD(..)- ) where--import Data.Comp.Param.Term-import Data.Comp.Param.Sum-import Data.Comp.Param.Ops-import Data.Comp.Param.Difunctor-import Data.Comp.Param.FreshM-import Control.Monad (liftM)---- |Equality on parametric values. The equality test is performed inside the--- 'FreshM' monad for generating fresh identifiers.-class PEq a where- peq :: a -> a -> FreshM Bool--instance PEq a => PEq [a] where- peq l1 l2- | length l1 /= length l2 = return False- | otherwise = liftM or $ mapM (uncurry peq) $ zip l1 l2--instance Eq a => PEq a where- peq x y = return $ x == y--{-| Signature equality. An instance @EqD f@ gives rise to an instance- @Eq (Term f)@. The equality test is performed inside the 'FreshM' monad for- generating fresh identifiers. -}-class EqD f where- eqD :: PEq a => f Name a -> f Name a -> FreshM Bool--{-| 'EqD' is propagated through sums. -}-instance (EqD f, EqD g) => EqD (f :+: g) where- eqD (Inl x) (Inl y) = eqD x y- eqD (Inr x) (Inr y) = eqD x y- eqD _ _ = return False--{-| From an 'EqD' difunctor an 'Eq' instance of the corresponding term type can- be derived. -}-instance EqD f => EqD (Cxt h f) where- eqD (In e1) (In e2) = eqD e1 e2- eqD (Hole h1) (Hole h2) = peq h1 h2- eqD (Var p1) (Var p2) = peq p1 p2- eqD _ _ = return False--instance (EqD f, PEq a) => PEq (Cxt h f Name a) where- peq = eqD--{-| Equality on terms. -}-instance (Difunctor f, EqD f) => Eq (Term f) where- (==) (Term x) (Term y) = evalFreshM $ eqD x y
− src/Data/Comp/Param/FreshM.hs
@@ -1,49 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.FreshM--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines a monad for generating fresh, abstract names, useful--- e.g. for defining equality on terms.-------------------------------------------------------------------------------------module Data.Comp.Param.FreshM- (- FreshM,- Name,- withName,- evalFreshM- ) where--import Control.Monad.Reader---- |Monad for generating fresh (abstract) names.-newtype FreshM a = FreshM{unFreshM :: Reader Int a}- deriving Monad---- |Abstract notion of a name (the constructor is hidden).-newtype Name = Name Int- deriving Eq--instance Show Name where- show (Name x) = names !! x- where baseNames = ['a'..'z']- names = map (:[]) baseNames ++ names' 1- names' n = map (: show n) baseNames ++ names' (n + 1)--instance Ord Name where- compare (Name x) (Name y) = compare x y---- |Run the given computation with the next available name.-withName :: (Name -> FreshM a) -> FreshM a-withName m = do name <- FreshM (asks Name)- FreshM $ local ((+) 1) $ unFreshM $ m name---- |Evaluate a computation that uses fresh names.-evalFreshM :: FreshM a -> a-evalFreshM (FreshM m) = runReader m 0
− src/Data/Comp/Param/Ops.hs
@@ -1,127 +0,0 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies,- FlexibleInstances, UndecidableInstances, IncoherentInstances #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Ops--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module provides operators on difunctors.--------------------------------------------------------------------------------------module Data.Comp.Param.Ops where--import Data.Comp.Param.Difunctor-import Data.Comp.Param.Ditraversable-import Control.Monad (liftM)----- Sums-infixr 6 :+:---- |Formal sum of signatures (difunctors).-data (f :+: g) a b = Inl (f a b)- | Inr (g a b)--{-| Utility function to case on a difunctor sum, without exposing the internal- representation of sums. -}-caseD :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c-caseD f g x = case x of- Inl x -> f x- Inr x -> g x--instance (Difunctor f, Difunctor g) => Difunctor (f :+: g) where- dimap f g (Inl e) = Inl (dimap f g e)- dimap f g (Inr e) = Inr (dimap f g e)--instance (Ditraversable f, Ditraversable g) => Ditraversable (f :+: g) where- dimapM f (Inl e) = Inl `liftM` dimapM f e- dimapM f (Inr e) = Inr `liftM` dimapM f e- disequence (Inl e) = Inl `liftM` disequence e- disequence (Inr e) = Inr `liftM` disequence e---- | Signature containment relation for automatic injections. The left-hand must--- be an atomic signature, where as the right-hand side must have a list-like--- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,--- non-examples include @f :+: g :<: f :+: (g :+: h)@ and--- @f :<: (f :+: g) :+: h@.-class sub :<: sup where- inj :: sub a b -> sup a b- proj :: sup a b -> Maybe (sub a b)--instance (:<:) f f where- inj = id- proj = Just--instance (:<:) f (f :+: g) where- inj = Inl- proj (Inl x) = Just x- proj (Inr _) = Nothing--instance (f :<: g) => (:<:) f (h :+: g) where- inj = Inr . inj- proj (Inr x) = proj x- proj (Inl _) = Nothing----- Products-infixr 8 :*:---- |Formal product of signatures (difunctors).-data (f :*: g) a b = f a b :*: g a b--ffst :: (f :*: g) a b -> f a b-ffst (x :*: _) = x--fsnd :: (f :*: g) a b -> g a b-fsnd (_ :*: x) = x----- Constant Products-infixr 7 :&:--{-| This data type adds a constant product to a signature. -}-data (f :&: p) a b = f a b :&: p--instance Difunctor f => Difunctor (f :&: p) where- dimap f g (v :&: c) = dimap f g v :&: c--instance Ditraversable f => Ditraversable (f :&: p) where- dimapM f (v :&: c) = liftM (:&: c) (dimapM f v)- disequence (v :&: c) = liftM (:&: c) (disequence v)--{-| This class defines how to distribute an annotation over a sum of- signatures. -}-class DistAnn s p s' | s' -> s, s' -> p where- {-| Inject an annotation over a signature. -}- injectA :: p -> s a b -> s' a b- {-| Project an annotation from a signature. -}- projectA :: s' a b -> (s a b, p)--class RemA s s' | s -> s' where- {-| Remove annotations from a signature. -}- remA :: s a b -> s' a b--instance (RemA s s') => RemA (f :&: p :+: s) (f :+: s') where- remA (Inl (v :&: _)) = Inl v- remA (Inr v) = Inr $ remA v--instance RemA (f :&: p) f where- remA (v :&: _) = v--instance DistAnn f p (f :&: p) where- injectA c v = v :&: c-- projectA (v :&: p) = (v,p)--instance (DistAnn s p s') => DistAnn (f :+: s) p ((f :&: p) :+: s') where- injectA c (Inl v) = Inl (v :&: c)- injectA c (Inr v) = Inr $ injectA c v-- projectA (Inl (v :&: p)) = (Inl v,p)- projectA (Inr v) = let (v',p) = projectA v- in (Inr v',p)
− src/Data/Comp/Param/Ordering.hs
@@ -1,77 +0,0 @@-{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,- UndecidableInstances, IncoherentInstances, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Ordering--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines ordering of signatures, which lifts to ordering of--- terms and contexts.-------------------------------------------------------------------------------------module Data.Comp.Param.Ordering- (- POrd(..),- OrdD(..),- compList- ) where--import Data.Comp.Param.Term-import Data.Comp.Param.Sum-import Data.Comp.Param.Ops-import Data.Comp.Param.Difunctor-import Data.Comp.Param.FreshM-import Data.Comp.Param.Equality-import Data.Maybe (fromMaybe)-import Data.List (find)-import Control.Monad (liftM)---- |Ordering of parametric values.-class PEq a => POrd a where- pcompare :: a -> a -> FreshM Ordering--instance POrd a => POrd [a] where- pcompare l1 l2- | length l1 < length l2 = return LT- | length l1 > length l2 = return GT- | otherwise = liftM compList $ mapM (uncurry pcompare) $ zip l1 l2--compList :: [Ordering] -> Ordering-compList = fromMaybe EQ . find (/= EQ)--instance Ord a => POrd a where- pcompare x y = return $ compare x y--{-| Signature ordering. An instance @OrdD f@ gives rise to an instance- @Ord (Term f)@. -}-class EqD f => OrdD f where- compareD :: POrd a => f Name a -> f Name a -> FreshM Ordering--{-| 'OrdD' is propagated through sums. -}-instance (OrdD f, OrdD g) => OrdD (f :+: g) where- compareD (Inl x) (Inl y) = compareD x y- compareD (Inl _) (Inr _) = return LT- compareD (Inr x) (Inr y) = compareD x y- compareD (Inr _) (Inl _) = return GT--{-| From an 'OrdD' difunctor an 'Ord' instance of the corresponding term type- can be derived. -}-instance OrdD f => OrdD (Cxt h f) where- compareD (In e1) (In e2) = compareD e1 e2- compareD (Hole h1) (Hole h2) = pcompare h1 h2- compareD (Var p1) (Var p2) = pcompare p1 p2- compareD (In _) _ = return LT- compareD (Hole _) (In _) = return GT- compareD (Hole _) (Var _) = return LT- compareD (Var _) _ = return GT--instance (OrdD f, POrd a) => POrd (Cxt h f Name a) where- pcompare = compareD--{-| Ordering of terms. -}-instance (Difunctor f, OrdD f) => Ord (Term f) where- compare (Term x) (Term y) = evalFreshM $ compareD x y
− src/Data/Comp/Param/Show.hs
@@ -1,41 +0,0 @@-{-# LANGUAGE TypeOperators, FlexibleInstances, TypeSynonymInstances,- IncoherentInstances, UndecidableInstances, TemplateHaskell, GADTs #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Show--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines showing of signatures, which lifts to showing of terms.-------------------------------------------------------------------------------------module Data.Comp.Param.Show- (- ShowD(..)- ) where--import Data.Comp.Param.Term-import Data.Comp.Param.Ops-import Data.Comp.Param.Derive-import Data.Comp.Param.FreshM---- Lift ShowD to sums-$(derive [liftSum] [''ShowD])--{-| From an 'ShowD' difunctor an 'ShowD' instance of the corresponding term type- can be derived. -}-instance (Difunctor f, ShowD f) => ShowD (Cxt h f) where- showD (In t) = showD $ fmap showD t- showD (Hole h) = h- showD (Var p) = return $ show p--{-| Printing of terms. -}-instance (Difunctor f, ShowD f) => Show (Term f) where- show = evalFreshM . showD . toCxt . unTerm--instance (ShowD f, Show p) => ShowD (f :&: p) where- showD (x :&: p) = do sx <- showD x- return $ sx ++ " :&: " ++ show p
− src/Data/Comp/Param/Sum.hs
@@ -1,186 +0,0 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,- FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,- ScopedTypeVariables, TemplateHaskell, Rank2Types #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Sum--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module provides the infrastructure to extend signatures.--------------------------------------------------------------------------------------module Data.Comp.Param.Sum- (- (:<:),- (:+:),- caseD,-- -- * Projections for Signatures and Terms- proj,- proj2,- proj3,- proj4,- proj5,- proj6,- proj7,- proj8,- proj9,- proj10,- project,- project2,- project3,- project4,- project5,- project6,- project7,- project8,- project9,- project10,- deepProject,- deepProject2,- deepProject3,- deepProject4,- deepProject5,- deepProject6,- deepProject7,- deepProject8,- deepProject9,- deepProject10,-- -- * Injections for Signatures and Terms- inj,- inj2,- inj3,- inj4,- inj5,- inj6,- inj7,- inj8,- inj9,- inj10,- inject,- inject',- inject2,- inject3,- inject4,- inject5,- inject6,- inject7,- inject8,- inject9,- inject10,- deepInject,- deepInject2,- deepInject3,- deepInject4,- deepInject5,- deepInject6,- deepInject7,- deepInject8,- deepInject9,- deepInject10,-- injectCxt,- liftCxt- ) where--import Prelude hiding (sequence)-import Control.Monad hiding (sequence)-import Data.Comp.Param.Term-import Data.Comp.Param.Algebra-import Data.Comp.Param.Ops-import Data.Comp.Param.Derive.Projections-import Data.Comp.Param.Derive.Injections-import Data.Comp.Param.Difunctor-import Data.Comp.Param.Ditraversable--$(liftM concat $ mapM projn [2..10])---- |Project the outermost layer of a term to a sub signature. If the signature--- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.-project :: (g :<: f) => Cxt h f a b -> Maybe (g a (Cxt h f a b))-project (In t) = proj t-project (Hole _) = Nothing-project (Var _) = Nothing--$(liftM concat $ mapM projectn [2..10])---- | Tries to coerce a term/context to a term/context over a sub-signature. If--- the signature @g@ is compound of /n/ atomic signatures, use--- @deepProject@/n/ instead.-deepProject :: (Ditraversable g, g :<: f) => Term f -> Maybe (Term g)-{-# INLINE deepProject #-}-deepProject = appTSigFunM' proj--$(liftM concat $ mapM deepProjectn [2..10])-{-# INLINE deepProject2 #-}-{-# INLINE deepProject3 #-}-{-# INLINE deepProject4 #-}-{-# INLINE deepProject5 #-}-{-# INLINE deepProject6 #-}-{-# INLINE deepProject7 #-}-{-# INLINE deepProject8 #-}-{-# INLINE deepProject9 #-}-{-# INLINE deepProject10 #-}--$(liftM concat $ mapM injn [2..10])---- |Inject a term where the outermost layer is a sub signature. If the signature--- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.-inject :: (g :<: f) => g a (Cxt h f a b) -> Cxt h f a b-inject = In . inj---- |Inject a term where the outermost layer is a sub signature. If the signature--- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.-inject' :: (Difunctor g, g :<: f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a b-inject' = inject . dimap Var id--$(liftM concat $ mapM injectn [2..10])---- |Inject a term over a sub signature to a term over larger signature. If the--- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/--- instead.-deepInject :: (Difunctor g, g :<: f) => Term g -> Term f-{-# INLINE deepInject #-}-deepInject (Term t) = Term (appSigFun inj t)--$(liftM concat $ mapM deepInjectn [2..10])-{-# INLINE deepInject2 #-}-{-# INLINE deepInject3 #-}-{-# INLINE deepInject4 #-}-{-# INLINE deepInject5 #-}-{-# INLINE deepInject6 #-}-{-# INLINE deepInject7 #-}-{-# INLINE deepInject8 #-}-{-# INLINE deepInject9 #-}-{-# INLINE deepInject10 #-}--{-| This function injects a whole context into another context. -}-injectCxt :: (Difunctor g, g :<: f) => Cxt h g a (Cxt h f a b) -> Cxt h f a b-injectCxt (In t) = inject $ difmap injectCxt t-injectCxt (Hole x) = x-injectCxt (Var p) = Var p--{-| This function lifts the given functor to a context. -}-liftCxt :: (Difunctor f, g :<: f) => g a b -> Cxt Hole f a b-liftCxt g = simpCxt $ inj g--instance (Show (f a b), Show (g a b)) => Show ((f :+: g) a b) where- show (Inl v) = show v- show (Inr v) = show v--instance (Ord (f a b), Ord (g a b)) => Ord ((f :+: g) a b) where- compare (Inl _) (Inr _) = LT- compare (Inr _) (Inl _) = GT- compare (Inl x) (Inl y) = compare x y- compare (Inr x) (Inr y) = compare x y--instance (Eq (f a b), Eq (g a b)) => Eq ((f :+: g) a b) where- (Inl x) == (Inl y) = x == y- (Inr x) == (Inr y) = x == y - _ == _ = False
− src/Data/Comp/Param/Term.hs
@@ -1,109 +0,0 @@-{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,- MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}------------------------------------------------------------------------------------ |--- Module : Data.Comp.Param.Term--- Copyright : (c) 2011 Patrick Bahr, Tom Hvitved--- License : BSD3--- Maintainer : Tom Hvitved <hvitved@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This module defines the central notion of /parametrised terms/ and their--- generalisation to parametrised contexts.--------------------------------------------------------------------------------------module Data.Comp.Param.Term- (- Cxt(..),- Hole,- NoHole,- Term(..),- Trm,- Context,- simpCxt,- toCxt,- cxtMap,- ParamFunctor(..)- ) where--import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)-import Data.Comp.Param.Difunctor-import Unsafe.Coerce (unsafeCoerce)--import Data.Maybe (fromJust)--{-| This data type represents contexts over a signature. Contexts are terms- containing zero or more holes, and zero or more parameters. The first- parameter is a phantom type indicating whether the context has holes. The- second paramater is the signature of the context, in the form of a- "Data.Comp.Param.Difunctor". The third parameter is the type of parameters,- and the fourth parameter is the type of holes. -}-data Cxt :: * -> (* -> * -> *) -> * -> * -> * where- In :: f a (Cxt h f a b) -> Cxt h f a b- Hole :: b -> Cxt Hole f a b- Var :: a -> Cxt h f a b--{-| Phantom type used to define 'Context'. -}-data Hole--{-| Phantom type used to define 'Term'. -}-data NoHole--{-| A context may contain holes. -}-type Context = Cxt Hole--{-| \"Preterms\" -}-type Trm f a = Cxt NoHole f a ()--{-| A term is a context with no holes, where all occurrences of the- contravariant parameter is fully parametric. -}-newtype Term f = Term{unTerm :: forall a. Trm f a}--{-| Convert a difunctorial value into a context. -}-simpCxt :: Difunctor f => f a b -> Cxt Hole f a b-{-# INLINE simpCxt #-}-simpCxt = In . difmap Hole--toCxt :: Difunctor f => Trm f a -> Cxt h f a b-{-# INLINE toCxt #-}-toCxt = unsafeCoerce---- | This combinator maps a function over a context by applying the--- function to each hole.-cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c-cxtMap f (Hole x) = Hole (f x)-cxtMap _ (Var x) = Var x-cxtMap f (In t) = In (dimap id (cxtMap f) t)---- Param Functor--{-| Monads for which embedded @Trm@ values, which are parametric at top level,- can be made into monadic @Term@ values, i.e. \"pushing the parametricity- inwards\". -}-class ParamFunctor m where- termM :: (forall a. m (Trm f a)) -> m (Term f)--coerceTermM :: ParamFunctor m => (forall a. m (Trm f a)) -> m (Term f)-{-# INLINE coerceTermM #-}-coerceTermM t = unsafeCoerce t--{-# RULES- "termM/coerce" termM = coerceTermM- #-}--instance ParamFunctor Maybe where- termM Nothing = Nothing- termM x = Just (Term $ fromJust x)--instance ParamFunctor (Either a) where- termM (Left x) = Left x- termM x = Right (Term $ fromRight x)- where fromRight :: Either a b -> b- fromRight (Right x) = x- fromRight _ = error "fromRight: Left"--instance ParamFunctor [] where- termM [] = []- termM l = Term (head l) : termM (tail l)
− src/Data/Comp/Param/Thunk.hs
@@ -1,127 +0,0 @@-{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, GADTs #-}------------------------------------------------------------------------------------- |--- Module : Data.Comp.Param.Thunk--- Copyright : (c) 2011 Patrick Bahr--- License : BSD3--- Maintainer : Patrick Bahr <paba@diku.dk>--- Stability : experimental--- Portability : non-portable (GHC Extensions)------ This modules defines terms & contexts with thunks, with deferred--- monadic computations.--------------------------------------------------------------------------------------module Data.Comp.Param.Thunk- (TermT- ,TrmT- ,CxtT- ,Thunk- ,thunk- ,whnf- ,whnf'- ,whnfPr- ,nf- ,nfT- ,nfPr- ,nfTPr- ,evalStrict- ,AlgT- ,strict- ,strict')- where--import Data.Comp.Param.Term-import Data.Comp.Param.Sum-import Data.Comp.Param.Ops-import Data.Comp.Param.Algebra-import Data.Comp.Param.Ditraversable-import Data.Comp.Param.Difunctor--import Control.Monad---- | This type represents terms with thunks.-type TermT m f = Term (Thunk m :+: f)---- | This type represents terms with thunks.-type TrmT m f a = Trm (Thunk m :+: f) a---- | This type represents contexts with thunks.-type CxtT h m f a = Cxt h (Thunk m :+: f) a--newtype Thunk m a b = Thunk (m b)---- | This function turns a monadic computation into a thunk.-thunk :: (Thunk m :<: f) => m (Cxt h f a b) -> Cxt h f a b-thunk = inject . Thunk---- | This function evaluates all thunks until a non-thunk node is--- found.-whnf :: Monad m => TrmT m f a -> m (Either a (f a (TrmT m f a)))-whnf (In (Inl (Thunk m))) = m >>= whnf-whnf (In (Inr t)) = return $ Right t-whnf (Var x) = return $ Left x--whnf' :: Monad m => TrmT m f a -> m (TrmT m f a)-whnf' = liftM (either Var inject) . whnf---- | This function first evaluates the argument term into whnf via--- 'whnf' and then projects the top-level signature to the desired--- subsignature. Failure to do the projection is signalled as a--- failure in the monad.-whnfPr :: (Monad m, g :<: f) => TrmT m f a -> m (g a (TrmT m f a))-whnfPr t = do res <- whnf t- case res of- Left _ -> fail "cannot project variable"- Right t ->- case proj t of- Just res' -> return res'- Nothing -> fail "projection failed"----- | This function evaluates all thunks.-nfT :: (ParamFunctor m, Monad m, Ditraversable f) => TermT m f -> m (Term f)-nfT t = termM $ nf $ unTerm t---- | This function evaluates all thunks.-nf :: (Monad m, Ditraversable f) => TrmT m f a -> m (Trm f a)-nf = either (return . Var) (liftM In . dimapM nf) <=< whnf---- | This function evaluates all thunks while simultaneously--- projecting the term to a smaller signature. Failure to do the--- projection is signalled as a failure in the monad as in 'whnfPr'.-nfTPr :: (ParamFunctor m, Monad m, Ditraversable g, g :<: f) => TermT m f -> m (Term g)-nfTPr t = termM $ nfPr $ unTerm t---- | This function evaluates all thunks while simultaneously--- projecting the term to a smaller signature. Failure to do the--- projection is signalled as a failure in the monad as in 'whnfPr'.-nfPr :: (Monad m, Ditraversable g, g :<: f) => TrmT m f a -> m (Trm g a)-nfPr = liftM In . dimapM nfPr <=< whnfPr---evalStrict :: (Ditraversable g, Monad m, g :<: f) => - (g (TrmT m f a) (f a (TrmT m f a)) -> TrmT m f a)- -> g (TrmT m f a) (TrmT m f a) -> TrmT m f a-evalStrict cont t = thunk $ do - t' <- dimapM (liftM (either (const Nothing) Just) . whnf) t- case disequence t' of- Nothing -> return $ inject' t- Just s -> return $ cont s- ---- | This type represents algebras which have terms with thunks as--- carrier.-type AlgT m f g = Alg f (TermT m g)---- | This combinator makes the evaluation of the given functor--- application strict by evaluating all thunks of immediate subterms.-strict :: (f :<: g, Ditraversable f, Monad m) => f a (TrmT m g a) -> TrmT m g a-strict x = thunk $ liftM inject $ dimapM whnf' x---- | This combinator makes the evaluation of the given functor--- application strict by evaluating all thunks of immediate subterms.-strict' :: (f :<: g, Ditraversable f, Monad m) => f (TrmT m g a) (TrmT m g a) -> TrmT m g a-strict' = strict . dimap Var id
+ src/Data/Comp/Render.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE TemplateHaskell, TypeSynonymInstances #-}+module Data.Comp.Render where++import Data.Foldable (toList)+import Data.Tree (Tree (..))+import Data.Tree.View+import Data.Comp+import Data.Comp.Derive+import Data.Comp.Show ()++-- | The 'stringTree' algebra of a functor. The default instance creates a tree+-- with the same structure as the term.+class (Functor f, Foldable f, ShowConstr f) => Render f where+ stringTreeAlg :: Alg f (Tree String)+ stringTreeAlg f = Node (showConstr f) $ toList f++-- | Convert a term to a 'Tree'+stringTree :: Render f => Term f -> Tree String+stringTree = cata stringTreeAlg++-- | Show a term using ASCII art+showTerm :: Render f => Term f -> String+showTerm = showTree . stringTree++-- | Print a term using ASCII art+drawTerm :: Render f => Term f -> IO ()+drawTerm = putStrLn . showTerm++-- | Write a term to an HTML file with foldable nodes+writeHtmlTerm :: Render f => FilePath -> Term f -> IO ()+writeHtmlTerm file = writeHtmlTree file . fmap (\n -> NodeInfo n "") . stringTree++$(derive [liftSum] [''Render])
src/Data/Comp/Show.hs view
@@ -36,3 +36,8 @@ $(derive [liftSum] [''ShowF]) $(derive [makeShowF] [''Maybe, ''[], ''(,)])++instance (ShowConstr f, Show p) => ShowConstr (f :&: p) where+ showConstr (v :&: p) = showConstr v ++ " :&: " ++ show p++$(derive [liftSum] [''ShowConstr])
src/Data/Comp/Sum.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances, FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,- ScopedTypeVariables, TemplateHaskell #-}+ ScopedTypeVariables, TemplateHaskell, ConstraintKinds, Rank2Types #-} -------------------------------------------------------------------------------- -- | -- Module : Data.Comp.Sum@@ -17,77 +17,28 @@ module Data.Comp.Sum ( (:<:),+ (:=:), (:+:), caseF, -- * Projections for Signatures and Terms proj,- proj2,- proj3,- proj4,- proj5,- proj6,- proj7,- proj8,- proj9,- proj10, project,- project2,- project3,- project4,- project5,- project6,- project7,- project8,- project9,- project10, deepProject,- deepProject2,- deepProject3,- deepProject4,- deepProject5,- deepProject6,- deepProject7,- deepProject8,- deepProject9,- deepProject10,+ project_,+ deepProject_, -- * Injections for Signatures and Terms inj,- inj2,- inj3,- inj4,- inj5,- inj6,- inj7,- inj8,- inj9,- inj10, inject,- inject2,- inject3,- inject4,- inject5,- inject6,- inject7,- inject8,- inject9,- inject10, deepInject,- deepInject2,- deepInject3,- deepInject4,- deepInject5,- deepInject6,- deepInject7,- deepInject8,- deepInject9,- deepInject10,+ inject_,+ deepInject_, + split,+ -- * Injections and Projections for Constants injectConst,- injectConst2,- injectConst3, projectConst, injectCxt, liftCxt,@@ -98,10 +49,9 @@ import Data.Comp.Term import Data.Comp.Algebra import Data.Comp.Ops-import Data.Comp.Derive.Projections-import Data.Comp.Derive.Injections import Control.Monad hiding (mapM,sequence)+import Control.Applicative (Applicative (..)) import Prelude hiding (mapM,sequence) import Data.Maybe@@ -110,16 +60,18 @@ import qualified Data.Map as Map -$(liftM concat $ mapM projn [2..10])- -- |Project the outermost layer of a term to a sub signature. If the signature -- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead. project :: (g :<: f) => Cxt h f a -> Maybe (g (Cxt h f a))-project (Hole _) = Nothing-project (Term t) = proj t+project = project_ proj -$(liftM concat $ mapM projectn [2..10])+-- |Project the outermost layer of a term to a sub signature. If the signature+-- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.+project_ :: (SigFunM Maybe f g) -> Cxt h f a -> Maybe (g (Cxt h f a))+project_ _ (Hole _) = Nothing+project_ f (Term t) = f t + -- | 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.@@ -127,55 +79,47 @@ {-# INLINE deepProject #-} deepProject = appSigFunM' proj -$(liftM concat $ mapM deepProjectn [2..10])-{-# INLINE deepProject2 #-}-{-# INLINE deepProject3 #-}-{-# INLINE deepProject4 #-}-{-# INLINE deepProject5 #-}-{-# INLINE deepProject6 #-}-{-# INLINE deepProject7 #-}-{-# INLINE deepProject8 #-}-{-# INLINE deepProject9 #-}-{-# INLINE deepProject10 #-}+-- | 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_ :: (Traversable g) => (SigFunM Maybe f g) -> CxtFunM Maybe f g+{-# INLINE deepProject_ #-}+deepProject_ f = appSigFunM' f -$(liftM concat $ mapM injn [2..10]) -- |Inject a term where the outermost layer is a sub signature. If the signature -- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead. inject :: (g :<: f) => g (Cxt h f a) -> Cxt h f a-inject = Term . inj+inject = inject_ inj -$(liftM concat $ mapM injectn [2..10])+-- |Inject a term where the outermost layer is a sub signature. If the signature+-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.+inject_ :: (SigFun g f) -> g (Cxt h f a) -> Cxt h f a+inject_ f = Term . f + -- |Inject a term over a sub signature to a term over larger signature. If the -- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/ -- instead. deepInject :: (Functor g, g :<: f) => CxtFun g f {-# INLINE deepInject #-}-deepInject = appSigFun inj+deepInject = deepInject_ inj -$(liftM concat $ mapM deepInjectn [2..10])-{-# INLINE deepInject2 #-}-{-# INLINE deepInject3 #-}-{-# INLINE deepInject4 #-}-{-# INLINE deepInject5 #-}-{-# INLINE deepInject6 #-}-{-# INLINE deepInject7 #-}-{-# INLINE deepInject8 #-}-{-# INLINE deepInject9 #-}-{-# INLINE deepInject10 #-}+-- |Inject a term over a sub signature to a term over larger signature. If the+-- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/+-- instead.+deepInject_ :: (Functor g) => SigFun g f -> CxtFun g f+{-# INLINE deepInject_ #-}+deepInject_ f = appSigFun f ++split :: (f :<: f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a+split f1 f2 (Term t) = spl f1 f2 t+ injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a injectConst = inject . fmap (const undefined) -injectConst2 :: (Functor f1, Functor f2, Functor g, f1 :<: g, f2 :<: g)- => Const (f1 :+: f2) -> Cxt h g a-injectConst2 = inject2 . fmap (const undefined) -injectConst3 :: (Functor f1, Functor f2, Functor f3, Functor g, f1 :<: g, f2 :<: g, f3 :<: g)- => Const (f1 :+: f2 :+: f3) -> Cxt h g a-injectConst3 = inject3 . fmap (const undefined)- projectConst :: (Functor g, g :<: f) => Cxt h f a -> Maybe (Const g) projectConst = fmap (fmap (const ())) . project @@ -196,10 +140,6 @@ substHoles' :: (Functor f, Functor g, f :<: g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a substHoles' c m = substHoles c (fromJust . (`Map.lookup` m))--instance (Functor f) => Monad (Context f) where- return = Hole- (>>=) = substHoles instance (Show (f a), Show (g a)) => Show ((f :+: g) a) where
src/Data/Comp/Term.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types #-}+{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types, TypeSynonymInstances, FlexibleInstances #-} -------------------------------------------------------------------------------- -- | -- Module : Data.Comp.Term@@ -92,6 +92,16 @@ instance Functor f => Functor (Cxt h f) where fmap f = run where run (Hole v) = Hole (f v)+ run (Term t) = Term (fmap run t)++instance Functor f => Applicative (Context f) where+ pure = Hole+ (<*>) = ap++instance (Functor f) => Monad (Context f) where+ return = Hole+ m >>= f = run m+ where run (Hole v) = f v run (Term t) = Term (fmap run t) instance (Foldable f) => Foldable (Cxt h f) where
src/Data/Comp/Thunk.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, ScopedTypeVariables, ConstraintKinds #-} -------------------------------------------------------------------------------- -- |@@ -18,6 +18,7 @@ (TermT ,CxtT ,thunk+ ,injectT ,whnf ,whnf' ,whnfPr@@ -39,7 +40,7 @@ import Data.Comp.Term import Data.Comp.Equality import Data.Comp.Algebra-import Data.Comp.Ops+import Data.Comp.Ops ((:+:)(..), fromInr) import Data.Comp.Sum import Data.Comp.Number import Data.Foldable hiding (and)@@ -60,9 +61,13 @@ -- | This function turns a monadic computation into a thunk.-thunk :: (m :<: f) => m (Cxt h f a) -> Cxt h f a-thunk = inject+thunk :: m (CxtT m h f a) -> CxtT m h f a+thunk = inject_ Inl +-- | Variant of 'inject' for the typex 'CxtT' and 'TermT'.+injectT :: (g :<: f) => g (CxtT m h f a) -> CxtT m h f a+injectT = inject_ (Inr . inj)+ -- | This function evaluates all thunks until a non-thunk node is -- found. whnf :: Monad m => TermT m f -> m (f (TermT m f))@@ -70,7 +75,7 @@ whnf (Term (Inr t)) = return t whnf' :: Monad m => TermT m f -> m (TermT m f)-whnf' = liftM inject . whnf+whnf' = liftM (inject_ Inr) . whnf -- | This function first evaluates the argument term into whnf via -- 'whnf' and then projects the top-level signature to the desired@@ -114,7 +119,7 @@ -- given function. deepEval :: (Traversable f, Monad m) => (Term f -> TermT m f) -> TermT m f -> TermT m f-deepEval cont v = case deepProject v of +deepEval cont v = case deepProject_ fromInr v of Just v' -> cont v' _ -> thunk $ liftM cont $ nf v @@ -150,7 +155,7 @@ -- | This combinator makes the evaluation of the given functor -- application strict by evaluating all thunks of immediate subterms. strict :: (f :<: g, Traversable f, Monad m) => f (TermT m g) -> TermT m g-strict x = thunk $ liftM inject $ mapM whnf' x+strict x = thunk $ liftM (inject_ (Inr . inj)) $ mapM whnf' x -- | This type represents position representations for a functor -- @f@. It is a function that extracts a number of components (of@@ -163,7 +168,7 @@ -- argument of this combinator specifies which positions are supposed -- to be strict. strictAt :: (f :<: g, Traversable f, Monad m) => Pos f -> f (TermT m g) -> TermT m g-strictAt p s = thunk $ liftM inject $ mapM run s'+strictAt p s = thunk $ liftM (inject_ (Inr . inj)) $ mapM run s' where s' = number s isStrict e = Set.member e $ Set.fromList $ p s' run e | isStrict e = whnf' $ unNumbered e
− testsuite/tests/Data/Comp/Examples/MultiParam.hs
@@ -1,34 +0,0 @@-{-# LANGUAGE TypeOperators #-}-module Data.Comp.Examples.MultiParam where--import Examples.MultiParam.FOL as FOL--import Data.Comp.MultiParam-import Data.Comp.MultiParam.FreshM (Name)--import Test.Framework-import Test.Framework.Providers.HUnit-import Test.HUnit-import Test.Utils----------------------------------------------------------------------------------------- Test Suits-----------------------------------------------------------------------------------tests = testGroup "Parametric Compositional Data Types" [- testCase "FOL" folTest- ]-------------------------------------------------------------------------------------- Properties-----------------------------------------------------------------------------------folTest = show (foodFact7 :: INF Name TFormula) @=? "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Person(Skol6(x2)))\n" ++- "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Eats(Skol6(x2), x2))\n" ++- "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Person(Skol6(x2)))\n" ++- "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Eats(Skol6(x2), x2))"
− testsuite/tests/Data/Comp/Examples/Param.hs
@@ -1,38 +0,0 @@-{-# LANGUAGE TypeOperators #-}-module Data.Comp.Examples.Param where--import Examples.Param.Names as Names-import Examples.Param.Graph as Graph--import Data.Comp.Param--import Test.Framework-import Test.Framework.Providers.HUnit-import Test.HUnit-import Test.Utils----------------------------------------------------------------------------------------- Test Suits-----------------------------------------------------------------------------------tests = testGroup "Parametric Compositional Data Types" [- testCase "names" namesTest,- testCase "graph" graphTest- ]-------------------------------------------------------------------------------------- Properties-----------------------------------------------------------------------------------instance (EqD f, PEq p) => EqD (f :&: p) where- eqD (v1 :&: p1) (v2 :&: p2) = do b1 <- peq p1 p2- b2 <- eqD v1 v2- return $ b1 && b2--namesTest = sequence_ [en @=? en', ep @=? ep']-graphTest = sequence_ [n @=? 5, f @=? [0,2,1,2]]
testsuite/tests/Data/Comp/Examples_Test.hs view
@@ -3,8 +3,6 @@ import qualified Data.Comp.Examples.Comp as C import qualified Data.Comp.Examples.Multi as M-import qualified Data.Comp.Examples.Param as P-import qualified Data.Comp.Examples.MultiParam as MP import Test.Framework import Test.Framework.Providers.QuickCheck2@@ -13,7 +11,5 @@ tests = testGroup "Examples" [ C.tests,- M.tests,- P.tests,- MP.tests+ M.tests ]
testsuite/tests/Data/Comp/Variables_Test.hs view
@@ -1,5 +1,5 @@-{-# LANGUAGE TemplateHaskell, TypeSynonymInstances,-FlexibleInstances, MultiParamTypeClasses, TypeOperators, FlexibleContexts#-}+{-# LANGUAGE TemplateHaskell, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, + TypeOperators, FlexibleContexts, ConstraintKinds #-} module Data.Comp.Variables_Test where
testsuite/tests/Test/Utils.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell, TypeOperators, FlexibleContexts, FlexibleInstances, ConstraintKinds #-} module Test.Utils where