packages feed

syntactic 1.0.1 → 1.2

raw patch · 68 files changed

+4432/−3758 lines, 68 filesdep +QuickCheckdep +bytestringdep +syntacticdep −taggeddep ~base

Dependencies added: QuickCheck, bytestring, syntactic, test-framework, test-framework-golden, test-framework-quickcheck2, test-framework-th

Dependencies removed: tagged

Dependency ranges changed: base

Files

− Data/DynamicAlt.hs 
@@ -1,28 +0,0 @@--- | An alternative to "Data.Dynamic" with a different constraint on 'toDyn'--module Data.DynamicAlt where----import Data.Dynamic ()-import Data.Typeable-import GHC.Prim-import Unsafe.Coerce--import Data.Proxy----data Dynamic = Dynamic TypeRep Any--toDyn :: forall a b . Typeable (a -> b) => Proxy (a -> b) -> a -> Dynamic-toDyn _ a = case splitTyConApp $ typeOf (undefined :: a -> b) of-    (_,[ta,_]) -> Dynamic ta (unsafeCoerce a)--fromDyn :: Typeable a => Dynamic -> Maybe a-fromDyn (Dynamic t a)-    | b <- unsafeCoerce a-    , t == typeOf b-    = Just b-fromDyn _ = Nothing-
− Examples/NanoFeldspar/Core.hs 
@@ -1,261 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}---- | A minimal Feldspar core language implementation. The intention of this--- module is to demonstrate how to quickly make a language prototype using--- syntactic.------ A more realistic implementation would use custom contexts to restrict the--- types at which constructors operate. Currently, all general constructs (such--- as 'Literal' and 'Tuple') use a 'SimpleCtx' context, which means that the--- types are quite unrestricted. A real implementation would also probably use--- custom types for primitive functions, since 'Construct' is quite unsafe (uses--- only a 'String' to distinguish between functions).--module NanoFeldspar.Core where----import Data.Typeable--import Language.Syntactic-import Language.Syntactic.Constructs.Binding-import Language.Syntactic.Constructs.Binding.HigherOrder-import Language.Syntactic.Constructs.Condition-import Language.Syntactic.Constructs.Construct-import Language.Syntactic.Constructs.Literal-import Language.Syntactic.Constructs.Tuple-import Language.Syntactic.Sharing.SimpleCodeMotion--------------------------------------------------------------------------------------- * Types------------------------------------------------------------------------------------- | Convenient class alias-class    (Ord a, Show a, Typeable a) => Type a-instance (Ord a, Show a, Typeable a) => Type a-  -- TODO Use type synonym instead?--type Length = Int-type Index  = Int--------------------------------------------------------------------------------------- * Parallel arrays-----------------------------------------------------------------------------------data Parallel a-  where-    Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a])--instance Constrained Parallel-  where-    type Sat Parallel = Type-    exprDict Parallel = Dict--instance Semantic Parallel-  where-    semantics Parallel = Sem-        { semanticName = "parallel"-        , semanticEval = \len ixf -> map ixf [0 .. len-1]-        }--instance Equality Parallel where equal = equalDefault; exprHash = exprHashDefault-instance Render   Parallel where renderArgs = renderArgsDefault-instance Eval     Parallel where evaluate   = evaluateDefault-instance ToTree   Parallel-instance EvalBind Parallel where evalBindSym = evalBindSymDefault--instance AlphaEq dom dom dom env => AlphaEq Parallel Parallel dom env-  where-    alphaEqSym = alphaEqSymDefault--------------------------------------------------------------------------------------- * For loops-----------------------------------------------------------------------------------data ForLoop a-  where-    ForLoop :: Type st =>-        ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)--instance Constrained ForLoop-  where-    type Sat ForLoop = Type-    exprDict ForLoop = Dict--instance Semantic ForLoop-  where-    semantics ForLoop = Sem-        { semanticName = "forLoop"-        , semanticEval = \len init body -> foldl (flip body) init [0 .. len-1]-        }---instance Equality ForLoop where equal = equalDefault; exprHash = exprHashDefault-instance Render   ForLoop where renderArgs = renderArgsDefault-instance Eval     ForLoop where evaluate   = evaluateDefault-instance ToTree   ForLoop-instance EvalBind ForLoop where evalBindSym = evalBindSymDefault--instance AlphaEq dom dom dom env => AlphaEq ForLoop ForLoop dom env-  where-    alphaEqSym = alphaEqSymDefault--------------------------------------------------------------------------------------- * Feldspar domain------------------------------------------------------------------------------------- | The Feldspar domain-type FeldDomain-    =   Construct-    :+: Literal-    :+: Condition-    :+: Tuple-    :+: Select-    :+: Parallel-    :+: ForLoop--type FeldDomainAll = HODomain (Let :+: (FeldDomain :|| Eq :| Show)) Typeable--newtype Data a = Data { unData :: ASTF FeldDomainAll a }---- | Declaring 'Data' as syntactic sugar-instance Type a => Syntactic (Data a) FeldDomainAll-  where-    type Internal (Data a) = a-    desugar = unData-    sugar   = Data---- | Specialization of the 'Syntactic' class for the Feldspar domain-class    (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a-instance (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a----defaultBindDict2 ::-    BindDict ((Lambda :+: Variable :+: Let :+: (FeldDomain :|| Eq :| Show)) :|| Typeable)-defaultBindDict2 = BindDict-    { prjVariable = \a -> do-        Variable v <- prj a-        return v-    , prjLambda = \a -> do-        Lambda v <- prj a-        return v-    , injVariable = \ref v -> case exprDict ref of-        Dict -> injC (Variable v)-    , injLambda = \refa refb v -> case (exprDict refa, exprDict refb) of-        (Dict,Dict) -> injC (Lambda v)-    , injLet = \ref -> case exprDict ref of-        Dict -> injC Let  -- TODO Generalize the pattern of `Dict` matching-                          --      followed by `injC`-    }--------------------------------------------------------------------------------------- * Back ends------------------------------------------------------------------------------------- | Print the expression-printFeld :: Syntactic a FeldDomainAll => a -> IO ()-printFeld = printExpr . reifySmart defaultBindDict2 (const True)---- | Draw the syntax tree-drawFeld :: Syntactic a FeldDomainAll => a -> IO ()-drawFeld = drawAST . reifySmart defaultBindDict2 (const True)---- | Evaluation-eval :: Syntactic a FeldDomainAll => a -> Internal a-eval = evalBind . reifySmart defaultBindDict2 (const True)--------------------------------------------------------------------------------------- * Core library------------------------------------------------------------------------------------- | Literal-value :: Syntax a => Internal a -> a-value = sugarSymC . Literal--false :: Data Bool-false = value False--true :: Data Bool-true = value True---- | For types containing some kind of \"thunk\", this function can be used to--- force computation-force :: Syntax a => a -> a-force = resugar---- | Share a value using let binding-share :: (Syntax a, Syntax b) => a -> (a -> b) -> b-share = sugarSymC Let---- | Alpha equivalence-instance Type a => Eq (Data a)-  where-    Data a == Data b = alphaEq (reify a) (reify b)--instance Type a => Show (Data a)-  where-    show (Data a) = render $ reify a--instance (Type a, Num a) => Num (Data a)-  where-    fromInteger = value . fromInteger-    abs         = sugarSymC $ Construct "abs" abs-    signum      = sugarSymC $ Construct "signum" signum-    (+)         = sugarSymC $ Construct "(+)" (+)-    (-)         = sugarSymC $ Construct "(-)" (-)-    (*)         = sugarSymC $ Construct "(*)" (*)--(?) :: Syntax a => Data Bool -> (a,a) -> a-cond ? (t,e) = sugarSymC Condition cond t e---- | Parallel array-parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]-parallel = sugarSymC Parallel--forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st-forLoop = sugarSymC ForLoop--arrLength :: Type a => Data [a] -> Data Length-arrLength = sugarSymC $ Construct "arrLength" Prelude.length---- | Array indexing-getIx :: Type a => Data [a] -> Data Index -> Data a-getIx = sugarSymC $ Construct "getIx" eval-  where-    eval as i-        | i >= len || i < 0 = error "getIx: index out of bounds"-        | otherwise         = as !! i-      where-        len = Prelude.length as--not :: Data Bool -> Data Bool-not = sugarSymC $ Construct "not" Prelude.not--(==) :: Type a => Data a -> Data a -> Data Bool-(==) = sugarSymC $ Construct "(==)" (Prelude.==)--max :: Type a => Data a -> Data a -> Data a-max = sugarSymC $ Construct "max" Prelude.max--min :: Type a => Data a -> Data a -> Data a-min = sugarSymC $ Construct "min" Prelude.min-
− Examples/NanoFeldspar/Extra.hs 
@@ -1,81 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE ViewPatterns #-}--module NanoFeldspar.Extra where----import Data.Typeable--import Language.Syntactic-import Language.Syntactic.Constructs.Binding-import Language.Syntactic.Constructs.Binding.HigherOrder-import Language.Syntactic.Constructs.Binding.Optimize-import Language.Syntactic.Constructs.Construct-import Language.Syntactic.Constructs.Literal-import Language.Syntactic.Sharing.Graph-import Language.Syntactic.Sharing.ReifyHO--import NanoFeldspar.Core--------------------------------------------------------------------------------------- * Graph reification------------------------------------------------------------------------------------- | A predicate deciding which constructs can be shared. Literals and variables--- are not shared.-canShare :: ASTF FeldDomainAll a -> Bool-canShare (prj -> Just (Literal _))  = False-canShare (prj -> Just (Variable _)) = False-canShare a = True---- | Draw the syntax graph after common sub-expression elimination-drawFeldCSE :: Syntactic a FeldDomainAll => a -> IO ()-drawFeldCSE a = do-    (g,_) <- reifyGraph canShare a-    drawASG-      $ reindexNodesFrom0-      $ inlineSingle-      $ cse-      $ g---- | Draw the syntax graph after observing sharing-drawFeldObs :: Syntactic a FeldDomainAll => a -> IO ()-drawFeldObs a = do-    (g,_) <- reifyGraph canShare a-    drawASG-      $ reindexNodesFrom0-      $ inlineSingle-      $ g--------------------------------------------------------------------------------------- * Partial evaluation-----------------------------------------------------------------------------------instance Optimize ForLoop-  where-    optimizeSym = optimizeSymDefault--instance Optimize Parallel-  where-    optimizeSym = optimizeSymDefault--constFold :: forall a-    .  ASTF ((Lambda :+: Variable :+: Let :+: (FeldDomain :|| Eq :| Show)) :|| Typeable) a-    -> a-    -> ASTF ((Lambda :+: Variable :+: Let :+: (FeldDomain :|| Eq :| Show)) :|| Typeable) a-constFold expr a = match (\sym _ -> case sym of-      C' (InjR (InjR (InjR (C (C' _))))) -> injC (Literal a)-      _ -> expr-    ) expr--drawFeldPart :: Syntactic a FeldDomainAll => a -> IO ()-drawFeldPart = drawAST . optimize constFold . reify-
− Examples/NanoFeldspar/Test.hs 
@@ -1,91 +0,0 @@-import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith)--import NanoFeldspar.Core-import NanoFeldspar.Extra-import NanoFeldspar.Vector----prog1 :: Data Int -> Data Int -> Data Int-prog1 a b = min (max a (getIx (parallel b (\i -> min i b)) 3)) 2--test1_1 = drawFeld prog1-test1_2 = printFeld prog1-test1_3 = eval prog1 0 10--prog2 :: Data Int -> Data Int-prog2 a = let b = min a a in max b b--test2_1 = drawFeld prog2-test2_2 = printFeld prog2-test2_3 = eval prog2 34--prog3 :: Data Index-prog3 = sum $ reverse (10...45)--test3_1 = drawFeld prog3-test3_2 = printFeld prog3-test3_3 = eval prog3-test3_4 = eval (forLoop ((45 - 10) + 1) 0 (\var0 -> (\var1 -> ((((((45 - 10) + 1) - var0) - 1) + 10) + var1))))-  -- Pasted in the result of 'test3_2'--prog4 :: Vector (Data Index)-prog4 = map (uncurry (*)) $ zip (1...1000) (value [34,43,52,61])--test4_1 = drawFeld prog4-test4_2 = printFeld prog4-test4_3 = eval prog4--prog5 :: Vector (Data Index) -> Vector (Data Index)-prog5 = zipWith (*) (1...1000)--test5_1 = drawFeld prog5-test5_2 = printFeld prog5-test5_3 = eval prog5 [20..30]--prog6 :: Data Index -> Data Index-prog6 a = share (a*2,a*3) $ \(b,c) -> (b-c)*(c-b)--test6_1 = drawFeld prog6-test6_2 = printFeld prog6-test6_3 = eval prog6 20--------------------------------------------------------------------------------------- Demonstration of common sub-expression elimination and observable sharing-----------------------------------------------------------------------------------prog7 = index as 1 + sum as + sum as-  where-    as = map (*2) $ force (1...20)--test7_1 = drawFeld prog7-  -- Draws a tree with no duplication--test7_2 = drawFeldCSE prog7-  -- Draws a graph with no duplication--test7_3 = drawFeldObs prog7-  -- Draws a graph with some duplication. The 'forLoop' introduced by 'sum' is-  -- not shared, because 'sum as' is repeated twice in source code. But the-  -- 'parallel' introduced by 'force' is shared, because 'force' only appears-  -- once.--------------------------------------------------------------------------------------- Demonstration of partial evaluation-----------------------------------------------------------------------------------prog8 :: Data Int -> Data Int-prog8 a = (a==10) ? (max 5 (6+7), max 5 (6+7))--test8 = drawFeldPart prog8--prog9 a = expensiveCond ? (parallel a (+a), parallel a (+a))-  where-    expensiveCond = getIx (parallel (a*a*a*a) (+a)) 10 == 23--test9 = drawFeldPart prog9-
− Examples/NanoFeldspar/Vector.hs 
@@ -1,87 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeFamilies #-}---- | A simple vector library for NanoFeldspar. The intention of this module is--- to demonstrate how to add language features without extending the underlying--- core language. By declaring 'Vector' as syntactic sugar, vector operations--- can work seamlessly with the functions of the core language.------ An interesting aspect of the 'Vector' interface is that the only operation--- that produces a core language array (i.e. allocates memory) is 'freezeVector'--- (which uses 'parallel'). This means that expressions not involving--- 'freezeVector' are guaranteed to be fused. (Note, however, that--- 'freezeVector' is introduced by 'desugar', which in turn is used by many--- other functions.)--module NanoFeldspar.Vector where----import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith)--import Language.Syntactic (Syntactic (..), resugar)--import NanoFeldspar.Core----data Vector a-  where-    Indexed :: Data Length -> (Data Index -> a) -> Vector a--instance Syntax a => Syntactic (Vector a) FeldDomainAll-  where-    type Internal (Vector a) = [Internal a]-    desugar = desugar . freezeVector . map resugar-    sugar   = map resugar . unfreezeVector . sugar----length :: Vector a -> Data Length-length (Indexed len _) = len--indexed :: Data Length -> (Data Index -> a) -> Vector a-indexed = Indexed--index :: Vector a -> Data Index -> a-index (Indexed _ ixf) = ixf--freezeVector :: Type a => Vector (Data a) -> Data [a]-freezeVector vec = parallel (length vec) (index vec)--unfreezeVector :: Type a => Data [a] -> Vector (Data a)-unfreezeVector arr = Indexed (arrLength arr) (getIx arr)--zip :: Vector a -> Vector b -> Vector (a,b)-zip a b = indexed (length a `min` length b) (\i -> (index a i, index b i))--unzip :: Vector (a,b) -> (Vector a, Vector b)-unzip ab = (indexed len (fst . index ab), indexed len (snd . index ab))-  where-    len = length ab--permute :: (Data Length -> Data Index -> Data Index) -> (Vector a -> Vector a)-permute perm vec = indexed len (index vec . perm len)-  where-    len = length vec--reverse :: Vector a -> Vector a-reverse = permute $ \len i -> len-i-1--(...) :: Data Index -> Data Index -> Vector (Data Index)-l ... h = indexed (h-l+1) (+l)--map :: (a -> b) -> Vector a -> Vector b-map f (Indexed len ixf) = Indexed len (f . ixf)--zipWith :: (a -> b -> c) -> Vector a -> Vector b -> Vector c-zipWith f a b = map (uncurry f) $ zip a b--fold :: Syntax b => (a -> b -> b) -> b -> Vector a -> b-fold f b (Indexed len ixf) = forLoop len b (\i st -> f (ixf i) st)--sum :: (Type a, Num a) => Vector (Data a) -> Data a-sum = fold (+) 0-
− Language/Syntactic.hs 
@@ -1,27 +0,0 @@--- | The basic parts of the syntactic library--module Language.Syntactic-    ( module Language.Syntactic.Syntax-    , module Language.Syntactic.Traversal-    , module Language.Syntactic.Constraint-    , module Language.Syntactic.Sugar-    , module Language.Syntactic.Interpretation.Equality-    , module Language.Syntactic.Interpretation.Render-    , module Language.Syntactic.Interpretation.Evaluation-    , module Language.Syntactic.Interpretation.Semantics-    , module Data.Constraint-    ) where----import Language.Syntactic.Syntax-import Language.Syntactic.Traversal-import Language.Syntactic.Constraint-import Language.Syntactic.Sugar-import Language.Syntactic.Interpretation.Equality-import Language.Syntactic.Interpretation.Render-import Language.Syntactic.Interpretation.Evaluation-import Language.Syntactic.Interpretation.Semantics--import Data.Constraint (Dict (..))-
− Language/Syntactic/Constraint.hs 
@@ -1,262 +0,0 @@-{-# LANGUAGE OverlappingInstances #-}-{-# LANGUAGE UndecidableInstances #-}---- | Type constrained syntax trees--module Language.Syntactic.Constraint where----import Data.Constraint--import Language.Syntactic.Syntax-import Language.Syntactic.Interpretation.Equality-import Language.Syntactic.Interpretation.Render-import Language.Syntactic.Interpretation.Evaluation--------------------------------------------------------------------------------------- * Type predicates------------------------------------------------------------------------------------- | Intersection of type predicates-class    (c1 a, c2 a) => (c1 :/\: c2) a-instance (c1 a, c2 a) => (c1 :/\: c2) a--infixr 5 :/\:---- | Universal type predicate-class    Top a-instance Top a---- | Evidence that the predicate @sub@ is a subset of @sup@-type Sub sub sup = forall a . Dict (sub a) -> Dict (sup a)---- | Weaken an intersection-weakL :: Sub (c1 :/\: c2) c1-weakL Dict = Dict---- | Weaken an intersection-weakR :: Sub (c1 :/\: c2) c2-weakR Dict = Dict---- | Subset relation on type predicates-class sub :< sup-  where-    -- | Compute evidence that @sub@ is a subset of @sup@ (i.e. that @(sup a)@-    -- implies @(sub a)@)-    sub :: Sub sub sup--instance p :< p-  where-    sub = id--instance (p :/\: ps) :< p-  where-    sub = weakL--instance (ps :< q) => ((p :/\: ps) :< q)-  where-    sub = sub . weakR--------------------------------------------------------------------------------------- * Constrained syntax------------------------------------------------------------------------------------- | Constrain the result type of the expression by the given predicate-data (expr :| pred) sig-  where-    C :: pred (DenResult sig) => expr sig -> (expr :| pred) sig--infixl 4 :|--instance Project sub sup => Project sub (sup :| pred)-  where-    prj (C s) = prj s--instance Equality dom => Equality (dom :| pred)-  where-    equal (C a) (C b) = equal a b-    exprHash (C a)    = exprHash a--instance Render dom => Render (dom :| pred)-  where-    renderArgs args (C a) = renderArgs args a--instance Eval dom => Eval (dom :| pred)-  where-    evaluate (C a) = evaluate a--instance ToTree dom => ToTree (dom :| pred)-  where-    toTreeArgs args (C a) = toTreeArgs args a------ | Constrain the result type of the expression by the given predicate------ The difference between ':||' and ':|' is seen in the instances of the 'Sat'--- type:------ > type Sat (dom :|  pred) = pred :/\: Sat dom--- > type Sat (dom :|| pred) = pred-data (expr :|| pred) sig-  where-    C' :: pred (DenResult sig) => expr sig -> (expr :|| pred) sig--infixl 4 :||--instance Project sub sup => Project sub (sup :|| pred)-  where-    prj (C' s) = prj s--instance Equality dom => Equality (dom :|| pred)-  where-    equal (C' a) (C' b) = equal a b-    exprHash (C' a)     = exprHash a--instance Render dom => Render (dom :|| pred)-  where-    renderArgs args (C' a) = renderArgs args a--instance Eval dom => Eval (dom :|| pred)-  where-    evaluate (C' a) = evaluate a--instance ToTree dom => ToTree (dom :|| pred)-  where-    toTreeArgs args (C' a) = toTreeArgs args a------ | Expressions that constrain their result types-class Constrained expr-  where-    -- | Returns a predicate that is satisfied by the result type of all-    -- expressions of the given type (see 'exprDict').-    type Sat (expr :: * -> *) :: * -> Constraint--    -- | Compute a constraint on the result type of an expression-    exprDict :: expr a -> Dict (Sat expr (DenResult a))--instance Constrained dom => Constrained (AST dom)-  where-    type Sat (AST dom) = Sat dom-    exprDict (Sym s)  = exprDict s-    exprDict (s :$ _) = exprDict s--instance Constrained (sub1 :+: sub2)-  where-    -- | An over-approximation of the union of @Sat sub1@ and @Sat sub2@-    type Sat (sub1 :+: sub2) = Top-    exprDict (InjL s) = Dict-    exprDict (InjR s) = Dict--instance Constrained dom => Constrained (dom :| pred)-  where-    type Sat (dom :| pred) = pred :/\: Sat dom-    exprDict (C s) = case exprDict s of Dict -> Dict--instance Constrained (dom :|| pred)-  where-    type Sat (dom :|| pred) = pred-    exprDict (C' s) = Dict--type ConstrainedBy expr c = (Constrained expr, Sat expr :< c)---- | A version of 'exprDict' that returns a constraint for a particular--- predicate @p@ as long as @(p :< Sat dom)@ holds-exprDictSub :: ConstrainedBy expr p => expr a -> Dict (p (DenResult a))-exprDictSub = sub . exprDict---- | A version of 'exprDict' that works for domains of the form--- @(dom1 :+: dom2)@ as long as @(Sat dom1 ~ Sat dom2)@ holds-exprDictPlus :: (Constrained dom1, Constrained dom2, Sat dom1 ~ Sat dom2) =>-    AST (dom1 :+: dom2) a -> Dict (Sat dom1 (DenResult a))-exprDictPlus (s :$ _)       = exprDictPlus s-exprDictPlus (Sym (InjL a)) = exprDict a-exprDictPlus (Sym (InjR a)) = exprDict a------ | Symbol injection (like ':<:') with constrained result types-class (Project sub sup, Sat sup a) => InjectC sub sup a-  where-    injC :: (DenResult sig ~ a) => sub sig -> sup sig--instance InjectC sub sup sig => InjectC sub (AST sup) sig-  where-    injC = Sym . injC--instance (InjectC sub sup sig, pred sig) => InjectC sub (sup :| pred) sig-  where-    injC = C . injC--instance (InjectC sub sup sig, pred sig) => InjectC sub (sup :|| pred) sig-  where-    injC = C' . injC--instance Sat expr sig => InjectC expr expr sig-  where-    injC = id--instance InjectC expr1 (expr1 :+: expr2) sig-  where-    injC = InjL--instance InjectC expr1 expr3 sig => InjectC expr1 (expr2 :+: expr3) sig-  where-    injC = InjR . injC------ | Generic symbol application------ 'appSymC' has any type of the form:------ > appSymC :: InjectC expr (AST dom) x--- >     => expr (a :-> b :-> ... :-> Full x)--- >     -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)-appSymC :: (ApplySym sig f dom, InjectC sym (AST dom) (DenResult sig)) =>-    sym sig -> f-appSymC = appSym' . injC------ | 'AST' with existentially quantified result type-data ASTE dom-  where-    ASTE :: ASTF dom a -> ASTE dom--liftASTE-    :: (forall a . ASTF dom a -> b)-    -> ASTE dom-    -> b-liftASTE f (ASTE a) = f a--liftASTE2-    :: (forall a b . ASTF dom a -> ASTF dom b -> c)-    -> ASTE dom -> ASTE dom -> c-liftASTE2 f (ASTE a) (ASTE b) = f a b------ | 'AST' with bounded existentially quantified result type-data ASTB dom-  where-    ASTB :: Sat dom a => ASTF dom a -> ASTB dom--liftASTB-    :: (forall a . Sat dom a => ASTF dom a -> b)-    -> ASTB dom-    -> b-liftASTB f (ASTB a) = f a--liftASTB2-    :: (forall a b . (Sat dom a, Sat dom b) => ASTF dom a -> ASTF dom b -> c)-    -> ASTB dom -> ASTB dom -> c-liftASTB2 f (ASTB a) (ASTB b) = f a b-
− Language/Syntactic/Constructs/Binding.hs 
@@ -1,400 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | General binding constructs--module Language.Syntactic.Constructs.Binding where----import qualified Control.Monad.Identity as Monad-import Control.Monad.Reader-import Data.Ix-import Data.Tree-import Data.Typeable--import Data.Hash-import Data.Proxy--import Data.DynamicAlt-import Language.Syntactic-import Language.Syntactic.Constructs.Condition-import Language.Syntactic.Constructs.Construct-import Language.Syntactic.Constructs.Decoration-import Language.Syntactic.Constructs.Identity-import Language.Syntactic.Constructs.Literal-import Language.Syntactic.Constructs.Monad-import Language.Syntactic.Constructs.Tuple--------------------------------------------------------------------------------------- * Variables------------------------------------------------------------------------------------- | Variable identifier-newtype VarId = VarId { varInteger :: Integer }-  deriving (Eq, Ord, Num, Real, Integral, Enum, Ix)--instance Show VarId-  where-    show (VarId i) = show i--showVar :: VarId -> String-showVar v = "var" ++ show v------ | Variables-data Variable a-  where-    Variable :: VarId -> Variable (Full a)--instance Constrained Variable-  where-    type Sat Variable = Top-    exprDict _ = Dict---- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.------ 'exprHash' assigns the same hash to all variables. This is a valid--- over-approximation that enables the following property:------ @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@-instance Equality Variable-  where-    equal (Variable v1) (Variable v2) = v1==v2-    exprHash (Variable _)             = hashInt 0--instance Render Variable-  where-    render (Variable v) = showVar v--instance ToTree Variable-  where-    toTreeArgs [] (Variable v) = Node ("var:" ++ show v) []--------------------------------------------------------------------------------------- * Lambda binding------------------------------------------------------------------------------------- | Lambda binding-data Lambda a-  where-    Lambda :: VarId -> Lambda (b :-> Full (a -> b))--instance Constrained Lambda-  where-    type Sat Lambda = Top-    exprDict _ = Dict---- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.------ 'exprHash' assigns the same hash to all 'Lambda' bindings. This is a valid--- over-approximation that enables the following property:------ @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@-instance Equality Lambda-  where-    equal (Lambda v1) (Lambda v2) = v1==v2-    exprHash (Lambda _)           = hashInt 0--instance Render Lambda-  where-    renderArgs [body] (Lambda v) = "(\\" ++ showVar v ++ " -> "  ++ body ++ ")"--instance ToTree Lambda-  where-    toTreeArgs [body] (Lambda v) = Node ("Lambda " ++ show v) [body]--------------------------------------------------------------------------------------- * Let binding------------------------------------------------------------------------------------- | Let binding------ 'Let' is just an application operator with flipped argument order. The argument--- @(a -> b)@ is preferably constructed by 'Lambda'.-data Let a-  where-    Let :: Let (a :-> (a -> b) :-> Full b)--instance Constrained Let-  where-    type Sat Let = Top-    exprDict _ = Dict--instance Equality Let-  where-    equal Let Let = True-    exprHash Let  = hashInt 0--instance Render Let-  where-    renderArgs []    Let = "Let"-    renderArgs [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")"--instance ToTree Let-  where-    toTreeArgs [a,body] Let = case splitAt 7 node of-        ("Lambda ", var) -> Node ("Let " ++ var) [a,body']-        _                -> Node "Let" [a,body]-      where-        Node node ~[body'] = body-        var                = drop 7 node  -- Drop the "Lambda " prefix--instance Eval Let-  where-    evaluate Let = flip ($)--------------------------------------------------------------------------------------- * Interpretation------------------------------------------------------------------------------------- | Should be a capture-avoiding substitution, but it is currently not correct.------ Note: Variables with a different type than the new expression will be--- silently ignored.-subst :: forall constr dom a b-    .  ( ConstrainedBy dom Typeable-       , Project Lambda dom-       , Project Variable dom-       )-    => VarId       -- ^ Variable to be substituted-    -> ASTF dom a  -- ^ Expression to substitute for-    -> ASTF dom b  -- ^ Expression to substitute in-    -> ASTF dom b-subst v new a = go a-  where-    go :: AST dom c -> AST dom c-    go a@((prj -> Just (Lambda w)) :$ _)-        | v==w = a  -- Capture-    go (f :$ a) = go f :$ go a-    go var-        | Just (Variable w) <- prj var-        , v==w-        , Dict :: Dict (Typeable a) <- exprDictSub new-        , Dict :: Dict (Typeable x) <- exprDictSub var-        , Just new' <- gcast new-        = new'-    go a = a-  -- TODO Make it correct (may need to alpha-convert `new` before inserting it)-  -- TODO Should there be an error if `gcast` fails? (See note in Haddock-  --      comment.)---- | Beta-reduction of an expression. The expression to be reduced is assumed to--- be a `Lambda`.-betaReduce-    :: ( ConstrainedBy dom Typeable-       , Project Lambda dom-       , Project Variable dom-       )-    => ASTF dom a         -- ^ Argument-    -> ASTF dom (a -> b)  -- ^ Function to be reduced-    -> ASTF dom b-betaReduce new (lam :$ body)-    | Just (Lambda v) <- prj lam = subst v new body------ | Evaluation of expressions with variables-class EvalBind sub-  where-    evalBindSym-        :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig))-        => sub sig-        -> Args (AST dom) sig-        -> Reader [(VarId,Dynamic)] (DenResult sig)-  -- `(Typeable (DenResult sig))` is required because this dictionary cannot (in-  -- general) be obtained from `sub`. It can only be obtained from `dom`, and-  -- this is what `evalBindM` does.--instance (EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2)-  where-    evalBindSym (InjL a) = evalBindSym a-    evalBindSym (InjR a) = evalBindSym a---- | Evaluation of possibly open expressions-evalBindM :: (EvalBind dom, ConstrainedBy dom Typeable) =>-    ASTF dom a -> Reader [(VarId,Dynamic)] a-evalBindM a-    | Dict :: Dict (Typeable a) <- exprDictSub a-    = liftM result $ match (\s -> liftM Full . evalBindSym s) a---- | Evaluation of closed expressions-evalBind :: (EvalBind dom, ConstrainedBy dom Typeable) => ASTF dom a -> a-evalBind = flip runReader [] . evalBindM---- | Apply a symbol denotation to a list of arguments-appDen :: Denotation sig -> Args Monad.Identity sig -> DenResult sig-appDen a Nil       = a-appDen f (a :* as) = appDen (f $ result $ Monad.runIdentity a) as---- | Convenient default implementation of 'evalBindSym'-evalBindSymDefault-    :: (Eval sub, EvalBind dom, ConstrainedBy dom Typeable)-    => sub sig-    -> Args (AST dom) sig-    -> Reader [(VarId,Dynamic)] (DenResult sig)-evalBindSymDefault sym args = do-    args' <- mapArgsM (liftM (Monad.Identity . Full) . evalBindM) args-    return $ appDen (evaluate sym) args'--instance EvalBind dom => EvalBind (dom :| pred)-  where-    evalBindSym (C a) = evalBindSym a--instance EvalBind dom => EvalBind (dom :|| pred)-  where-    evalBindSym (C' a) = evalBindSym a--instance EvalBind dom => EvalBind (Decor info dom)-  where-    evalBindSym = evalBindSym . decorExpr--instance EvalBind Identity  where evalBindSym = evalBindSymDefault-instance EvalBind Construct where evalBindSym = evalBindSymDefault-instance EvalBind Literal   where evalBindSym = evalBindSymDefault-instance EvalBind Condition where evalBindSym = evalBindSymDefault-instance EvalBind Tuple     where evalBindSym = evalBindSymDefault-instance EvalBind Select    where evalBindSym = evalBindSymDefault-instance EvalBind Let       where evalBindSym = evalBindSymDefault--instance Monad m => EvalBind (MONAD m) where evalBindSym = evalBindSymDefault--instance EvalBind Variable-  where-    evalBindSym (Variable v) Nil = do-        env <- ask-        case lookup v env of-            Nothing -> return $ error "evalBind: evaluating free variable"-            Just a  -> case fromDyn a of-              Just a -> return a-              _      -> return $ error "evalBind: internal type error"--instance EvalBind Lambda-  where-    evalBindSym lam@(Lambda v) (body :* Nil) = do-        env <- ask-        return-            $ \a -> flip runReader ((v, toDyn (funType lam) a):env)-            $ evalBindM body-      where-        funType :: Lambda (b :-> Full (a -> b)) -> Proxy (a -> b)-        funType _ = Proxy--------------------------------------------------------------------------------------- * Alpha equivalence------------------------------------------------------------------------------------- | Environments containing a list of variable equivalences-class VarEqEnv a-  where-    prjVarEqEnv :: a -> [(VarId,VarId)]-    modVarEqEnv :: ([(VarId,VarId)] -> [(VarId,VarId)]) -> (a -> a)--instance VarEqEnv [(VarId,VarId)]-  where-    prjVarEqEnv = id-    modVarEqEnv = id---- | Alpha-equivalence-class AlphaEq sub1 sub2 dom env-  where-    alphaEqSym-        :: sub1 a-        -> Args (AST dom) a-        -> sub2 b-        -> Args (AST dom) b-        -> Reader env Bool--instance (AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) =>-    AlphaEq (subA1 :+: subA2) (subB1 :+: subB2) dom env-  where-    alphaEqSym (InjL a) aArgs (InjL b) bArgs = alphaEqSym a aArgs b bArgs-    alphaEqSym (InjR a) aArgs (InjR b) bArgs = alphaEqSym a aArgs b bArgs-    alphaEqSym _ _ _ _ = return False--alphaEqM :: AlphaEq dom dom dom env =>-    ASTF dom a -> ASTF dom b -> Reader env Bool-alphaEqM a b = simpleMatch (alphaEqM2 b) a--alphaEqM2 :: AlphaEq dom dom dom env =>-    ASTF dom b -> dom a -> Args (AST dom) a -> Reader env Bool-alphaEqM2 b a aArgs = simpleMatch (alphaEqSym a aArgs) b---- | Alpha-equivalence on lambda expressions. Free variables are taken to be--- equivalent if they have the same identifier.-alphaEq :: AlphaEq dom dom dom [(VarId,VarId)] =>-    ASTF dom a -> ASTF dom b -> Bool-alphaEq a b = flip runReader ([] :: [(VarId,VarId)]) $ alphaEqM a b--alphaEqSymDefault :: (Equality sub, AlphaEq dom dom dom env)-    => sub a-    -> Args (AST dom) a-    -> sub b-    -> Args (AST dom) b-    -> Reader env Bool-alphaEqSymDefault a aArgs b bArgs-    | equal a b = alphaEqChildren a' b'-    | otherwise = return False-  where-    a' = appArgs (Sym (undefined :: dom a)) aArgs-    b' = appArgs (Sym (undefined :: dom b)) bArgs--alphaEqChildren :: AlphaEq dom dom dom env =>-    AST dom a -> AST dom b -> Reader env Bool-alphaEqChildren (Sym _)  (Sym _)  = return True-alphaEqChildren (f :$ a) (g :$ b) = liftM2 (&&)-    (alphaEqChildren f g)-    (alphaEqM a b)-alphaEqChildren _ _ = return False--instance AlphaEq sub sub dom env => AlphaEq (sub :| pred) (sub :| pred) dom env-  where-    alphaEqSym (C a) aArgs (C b) bArgs = alphaEqSym a aArgs b bArgs--instance AlphaEq sub sub dom env => AlphaEq (sub :|| pred) (sub :|| pred) dom env-  where-    alphaEqSym (C' a) aArgs (C' b) bArgs = alphaEqSym a aArgs b bArgs--instance AlphaEq dom dom dom env => AlphaEq Condition Condition dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq Construct Construct dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq Identity  Identity  dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq Let       Let       dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq Literal   Literal   dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq Select    Select    dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq Tuple     Tuple     dom env where alphaEqSym = alphaEqSymDefault--instance AlphaEq sub sub dom env =>-    AlphaEq (Decor info sub) (Decor info sub) dom env-  where-    alphaEqSym a aArgs b bArgs =-        alphaEqSym (decorExpr a) aArgs (decorExpr b) bArgs--instance (AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env-  where-    alphaEqSym = alphaEqSymDefault--instance (AlphaEq dom dom dom env, VarEqEnv env) =>-    AlphaEq Variable Variable dom env-  where-    alphaEqSym (Variable v1) Nil (Variable v2) Nil = do-        env <- asks prjVarEqEnv-        case lookup v1 env of-          Nothing  -> return (v1==v2)   -- Free variables-          Just v2' -> return (v2==v2')--instance (AlphaEq dom dom dom env, VarEqEnv env) =>-    AlphaEq Lambda Lambda dom env-  where-    alphaEqSym (Lambda v1) (body1 :* Nil) (Lambda v2) (body2 :* Nil) =-        local (modVarEqEnv ((v1,v2):)) $ alphaEqM body1 body2-
− Language/Syntactic/Constructs/Binding/HigherOrder.hs 
@@ -1,90 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | This module provides binding constructs using higher-order syntax and a--- function ('reify') for translating to first-order syntax. Expressions--- constructed using the exported interface (specifically, not introducing--- 'Variable's explicitly) are guaranteed to have well-behaved translation.--module Language.Syntactic.Constructs.Binding.HigherOrder-    ( Variable-    , Let (..)-    , HOLambda (..)-    , HODomain-    , lambda-    , reifyM-    , reifyTop-    , reify-    ) where----import Control.Monad.State--import Language.Syntactic-import Language.Syntactic.Constructs.Binding------ | Higher-order lambda binding-data HOLambda dom p a-  where-    HOLambda-        :: p a-        => (ASTF (HODomain dom p) a -> ASTF (HODomain dom p) b)-        -> HOLambda dom p (Full (a -> b))--type HODomain dom p = (HOLambda dom p :+: Variable :+: dom) :|| p--instance Constrained (HOLambda dom p)-  where-    type Sat (HOLambda dom p) = Top-    exprDict _ = Dict------ | Lambda binding-lambda-    :: (p a, p (a -> b))-    => (ASTF (HODomain dom p) a -> ASTF (HODomain dom p) b)-    -> ASTF (HODomain dom p) (a -> b)-lambda = injC . HOLambda--instance-    ( Syntactic a (HODomain dom p)-    , Syntactic b (HODomain dom p)-    , p (Internal a)-    , p (Internal a -> Internal b)-    ) =>-      Syntactic (a -> b) (HODomain dom p)-  where-    type Internal (a -> b) = Internal a -> Internal b-    desugar f = lambda (desugar . f . sugar)-    sugar     = error "sugar not implemented for (a -> b)"-      -- TODO An implementation of sugar would require dom to have some kind of-      --      application. Perhaps use `Let` for this?----reifyM-    :: AST (HODomain dom p) a-    -> State VarId (AST ((Lambda :+: Variable :+: dom) :|| p) a)-reifyM (f :$ a)            = liftM2 (:$) (reifyM f) (reifyM a)-reifyM (Sym (C' (InjR a))) = return $ Sym $ C' $ InjR a-reifyM (Sym (C' (InjL (HOLambda f)))) = do-    v    <- get; put (v+1)-    body <- reifyM $ f $ injC (Variable v)-    return $ injC (Lambda v) :$ body---- | Translating expressions with higher-order binding to corresponding--- expressions using first-order binding-reifyTop ::-    AST (HODomain dom p) a -> AST ((Lambda :+: Variable :+: dom) :|| p) a-reifyTop = flip evalState 0 . reifyM-  -- It is assumed that there are no 'Variable' constructors (i.e. no free-  -- variables) in the argument. This is guaranteed by the exported interface.---- | Reify an n-ary syntactic function-reify :: Syntactic a (HODomain dom p) =>-    a -> ASTF ((Lambda :+: Variable :+: dom) :|| p) (Internal a)-reify = reifyTop . desugar-
− Language/Syntactic/Constructs/Binding/Optimize.hs 
@@ -1,130 +0,0 @@--- | Basic optimization-module Language.Syntactic.Constructs.Binding.Optimize where----import Control.Monad.Writer-import Data.Set as Set-import Data.Typeable--import Language.Syntactic-import Language.Syntactic.Constructs.Binding-import Language.Syntactic.Constructs.Condition-import Language.Syntactic.Constructs.Construct-import Language.Syntactic.Constructs.Identity-import Language.Syntactic.Constructs.Literal-import Language.Syntactic.Constructs.Tuple------ | Constant folder------ Given an expression and the statically known value of that expression,--- returns a (possibly) new expression with the same meaning as the original.--- Typically, the result will be a 'Literal', if the relevant type constraints--- are satisfied.-type ConstFolder dom = forall a . ASTF dom a -> a -> ASTF dom a---- | Basic optimization-class Optimize sym-  where-    -- | Bottom-up optimization of an expression. The optimization performed is-    -- up to each instance, but the intention is to provide a sensible set of-    -- \"always-appropriate\" optimizations. The default implementation-    -- 'optimizeSymDefault' does only constant folding. This constant folding-    -- uses the set of free variables to know when it's static evaluation is-    -- possible. Thus it is possible to help constant folding of other-    -- constructs by pruning away parts of the syntax tree that are known not to-    -- be needed. For example, by replacing (using ordinary Haskell as an-    -- example)-    ---    -- > if True then a else b-    ---    -- with @a@, we don't need to report the free variables in @b@. This, in-    -- turn, can lead to more constant folding higher up in the expression.-    optimizeSym-        :: Optimize' dom-        => ConstFolder dom-        -> (sym sig -> AST dom sig)-        -> sym sig-        -> Args (AST dom) sig-        -> Writer (Set VarId) (ASTF dom (DenResult sig))--  -- The reason for having @dom@ as a class parameter is that many instances-  -- need to put additional constraints on @dom@.--type Optimize' dom =-    ( Optimize dom-    , EvalBind dom-    , AlphaEq dom dom dom [(VarId,VarId)]-    , ConstrainedBy dom Typeable-    )--instance (Optimize sub1, Optimize sub2) => Optimize (sub1 :+: sub2)-  where-    optimizeSym constFold injecter (InjL a) = optimizeSym constFold (injecter . InjL) a-    optimizeSym constFold injecter (InjR a) = optimizeSym constFold (injecter . InjR) a--optimizeM :: Optimize' dom-    => ConstFolder dom-    -> ASTF dom a-    -> Writer (Set VarId) (ASTF dom a)-optimizeM constFold = matchTrans (optimizeSym constFold Sym)---- | Optimize an expression-optimize :: Optimize' dom => ConstFolder dom -> ASTF dom a -> ASTF dom a-optimize constFold = fst . runWriter . optimizeM constFold---- | Convenient default implementation of 'optimizeSym' (uses 'evalBind' to--- partially evaluate)-optimizeSymDefault :: Optimize' dom-    => ConstFolder dom-    -> (sym sig -> AST dom sig)-    -> sym sig-    -> Args (AST dom) sig-    -> Writer (Set VarId) (ASTF dom (DenResult sig))-optimizeSymDefault constFold injecter sym args = do-    (args',vars) <- listen $ mapArgsM (optimizeM constFold) args-    let result = appArgs (injecter sym) args'-        value  = evalBind result-    if Set.null vars-      then return $ constFold result value-      else return result--instance Optimize dom => Optimize (dom :| p)-   where-    optimizeSym cf i (C s) args = optimizeSym cf (i . C) s args--instance Optimize dom => Optimize (dom :|| p)-   where-    optimizeSym cf i (C' s) args = optimizeSym cf (i . C') s args--instance Optimize Identity  where optimizeSym = optimizeSymDefault-instance Optimize Construct where optimizeSym = optimizeSymDefault-instance Optimize Literal   where optimizeSym = optimizeSymDefault-instance Optimize Tuple     where optimizeSym = optimizeSymDefault-instance Optimize Select    where optimizeSym = optimizeSymDefault-instance Optimize Let       where optimizeSym = optimizeSymDefault--instance Optimize Condition-  where-    optimizeSym constFold injecter cond@Condition args@(c :* t :* e :* Nil)-        | Set.null cVars = optimizeM constFold t_or_e-        | alphaEq t e    = optimizeM constFold t-        | otherwise      = optimizeSymDefault constFold injecter cond args-      where-        (c',cVars) = runWriter $ optimizeM constFold c-        t_or_e     = if evalBind c' then t else e--instance Optimize Variable-  where-    optimizeSym _ injecter var@(Variable v) Nil = do-        tell (singleton v)-        return (injecter var)--instance Optimize Lambda-  where-    optimizeSym constFold injecter lam@(Lambda v) (body :* Nil) = do-        body' <- censor (delete v) $ optimizeM constFold body-        return $ injecter lam :$ body'-
− Language/Syntactic/Constructs/Condition.hs 
@@ -1,28 +0,0 @@--- | Conditional expressions--module Language.Syntactic.Constructs.Condition where----import Language.Syntactic----data Condition sig-  where-    Condition :: Condition (Bool :-> a :-> a :-> Full a)--instance Constrained Condition-  where-    type Sat Condition = Top-    exprDict _ = Dict--instance Semantic Condition-  where-    semantics Condition = Sem "condition" (\c t e -> if c then t else e)--instance Equality Condition where equal = equalDefault; exprHash = exprHashDefault-instance Render   Condition where renderArgs = renderArgsDefault-instance Eval     Condition where evaluate   = evaluateDefault-instance ToTree   Condition-
− Language/Syntactic/Constructs/Construct.hs 
@@ -1,31 +0,0 @@--- | Provides a simple way to make syntactic constructs for prototyping. Note--- that 'Construct' is quite unsafe as it only uses 'String' to distinguish--- between different constructs. Also, 'Construct' has a very free type that--- allows any number of arguments.--module Language.Syntactic.Constructs.Construct where----import Language.Syntactic----data Construct sig-  where-    Construct :: String -> Denotation sig -> Construct sig--instance Constrained Construct-  where-    type Sat Construct = Top-    exprDict _ = Dict--instance Semantic Construct-  where-    semantics (Construct name den) = Sem name den--instance Equality Construct where equal = equalDefault; exprHash = exprHashDefault-instance Render   Construct where renderArgs = renderArgsDefault-instance Eval     Construct where evaluate   = evaluateDefault-instance ToTree   Construct-
− Language/Syntactic/Constructs/Decoration.hs 
@@ -1,132 +0,0 @@--- | Construct for decorating expressions with additional information--module Language.Syntactic.Constructs.Decoration where----import Data.Tree--import Language.Syntactic--------------------------------------------------------------------------------------- * Decoration------------------------------------------------------------------------------------- | Decorating symbols with additional information------ One usage of 'Decor' is to decorate every node of a syntax tree. This is done--- simply by changing------ > AST dom sig------ to------ > AST (Decor info dom) sig------ Injection\/projection of an decorated tree is done using 'injDecor' \/--- 'prjDecor'.-data Decor info expr sig-  where-    Decor-        :: { decorInfo :: info (DenResult sig)-           , decorExpr :: expr sig-           }-        -> Decor info expr sig--instance Constrained expr => Constrained (Decor info expr)-  where-    type Sat (Decor info expr) = Sat expr-    exprDict (Decor _ a) = exprDict a--instance Project sub sup => Project sub (Decor info sup)-  where-    prj = prj . decorExpr--instance Equality expr => Equality (Decor info expr)-  where-    equal a b = decorExpr a `equal` decorExpr b-    exprHash  = exprHash . decorExpr--instance Render expr => Render (Decor info expr)-  where-    renderArgs args = renderArgs args . decorExpr-    render = render . decorExpr--instance ToTree expr => ToTree (Decor info expr)-  where-    toTreeArgs args = toTreeArgs args . decorExpr--instance Eval expr => Eval (Decor info expr)-  where-    evaluate = evaluate . decorExpr----injDecor :: (sub :<: sup) =>-    info (DenResult sig) -> sub sig -> AST (Decor info sup) sig-injDecor info = Sym . Decor info . inj--prjDecor :: (sub :<: sup) =>-    AST (Decor info sup) sig -> Maybe (info (DenResult sig), sub sig)-prjDecor a = do-    Sym (Decor info b) <- return a-    c                  <- prj b-    return (info, c)---- | Get the decoration of the top-level node-getInfo :: AST (Decor info dom) sig -> info (DenResult sig)-getInfo (Sym (Decor info _)) = info-getInfo (f :$ _)             = getInfo f---- | Update the decoration of the top-level node-updateDecor :: forall info dom a .-    (info a -> info a) -> ASTF (Decor info dom) a -> ASTF (Decor info dom) a-updateDecor f = match update-  where-    update-        :: (a ~ DenResult sig)-        => Decor info dom sig-        -> Args (AST (Decor info dom)) sig-        -> ASTF (Decor info dom) a-    update (Decor info a) args = appArgs (Sym sym) args-      where-        sym = Decor (f info) a---- | Lift a function that operates on expressions with associated information to--- operate on an 'Decor' expression. This function is convenient to use together--- with e.g. 'queryNodeSimple' when the domain has the form--- @(`Decor` info dom)@.-liftDecor :: (expr s -> info (DenResult s) -> b) -> (Decor info expr s -> b)-liftDecor f (Decor info a) = f a info---- | Collect the decorations of all nodes-collectInfo :: (forall sig . info sig -> b) -> AST (Decor info dom) sig -> [b]-collectInfo coll (Sym (Decor info _)) = [coll info]-collectInfo coll (f :$ a) = collectInfo coll f ++ collectInfo coll a---- | Rendering of decorated syntax trees-toTreeDecor :: forall info dom a . (Render info, ToTree dom) =>-    ASTF (Decor info dom) a -> Tree String-toTreeDecor a = mkTree [] a-  where-    mkTree :: [Tree String] -> AST (Decor info dom) sig -> Tree String-    mkTree args (Sym (Decor info expr)) = Node infoStr [toTreeArgs args expr]-      where-        infoStr = "<<" ++ render info ++ ">>"-    mkTree args (f :$ a) = mkTree (mkTree [] a : args) f---- | Show an decorated syntax tree using ASCII art-showDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> String-showDecor = drawTree . toTreeDecor---- | Print an decorated syntax tree using ASCII art-drawDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> IO ()-drawDecor = putStrLn . showDecor---- | Strip decorations from an 'AST'-stripDecor :: AST (Decor info dom) sig -> AST dom sig-stripDecor (Sym (Decor _ a)) = Sym a-stripDecor (f :$ a)          = stripDecor f :$ stripDecor a-
− Language/Syntactic/Constructs/Identity.hs 
@@ -1,29 +0,0 @@--- | Identity function--module Language.Syntactic.Constructs.Identity where----import Language.Syntactic------ | Identity function-data Identity sig-  where-    Id :: Identity (a :-> Full a)--instance Constrained Identity-  where-    type Sat Identity = Top-    exprDict _ = Dict--instance Semantic Identity-  where-    semantics Id = Sem "id" id--instance Equality Identity where equal = equalDefault; exprHash = exprHashDefault-instance Render   Identity where renderArgs = renderArgsDefault-instance Eval     Identity where evaluate   = evaluateDefault-instance ToTree   Identity-
− Language/Syntactic/Constructs/Literal.hs 
@@ -1,41 +0,0 @@--- | Literal expressions--module Language.Syntactic.Constructs.Literal where----import Data.Typeable--import Data.Hash--import Language.Syntactic----data Literal sig-  where-    Literal :: (Eq a, Show a, Typeable a) => a -> Literal (Full a)--instance Constrained Literal-  where-    type Sat Literal = Eq :/\: Show :/\: Typeable :/\: Top-    exprDict (Literal _) = Dict--instance Equality Literal-  where-    Literal a `equal` Literal b = case cast a of-        Just a' -> a'==b-        Nothing -> False--    exprHash (Literal a) = hash (show a)--instance Render Literal-  where-    render (Literal a) = show a--instance ToTree Literal--instance Eval Literal-  where-    evaluate (Literal a) = a-
− Language/Syntactic/Constructs/Monad.hs 
@@ -1,46 +0,0 @@--- | Monadic constructs------ This module is based on the paper--- /Generic Monadic Constructs for Embedded Languages/ (Persson et al., IFL 2011--- <http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf>).--module Language.Syntactic.Constructs.Monad where----import Control.Monad--import Language.Syntactic--import Data.Proxy----data MONAD m sig-  where-    Return :: MONAD m (a    :-> Full (m a))-    Bind   :: MONAD m (m a  :-> (a -> m b) :-> Full (m b))-    Then   :: MONAD m (m a  :-> m b        :-> Full (m b))-    When   :: MONAD m (Bool :-> m ()       :-> Full (m ()))--instance Constrained (MONAD m)-  where-    type Sat (MONAD m) = Top-    exprDict _ = Dict--instance Monad m => Semantic (MONAD m)-  where-    semantics Return = Sem "return" return-    semantics Bind   = Sem "bind"   (>>=)-    semantics Then   = Sem "then"   (>>)-    semantics When   = Sem "when"   when--instance Monad m => Equality (MONAD m) where equal = equalDefault; exprHash = exprHashDefault-instance Monad m => Render   (MONAD m) where renderArgs = renderArgsDefault-instance Monad m => Eval     (MONAD m) where evaluate   = evaluateDefault-instance Monad m => ToTree   (MONAD m)---- | Projection with explicit monad type-prjMonad :: (MONAD m :<: sup) => Proxy (m ()) -> sup sig -> Maybe (MONAD m sig)-prjMonad _ = prj-
− Language/Syntactic/Constructs/Tuple.hs 
@@ -1,362 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | Construction and elimination of tuples in the object language--module Language.Syntactic.Constructs.Tuple where----import Data.Tuple.Curry-import Data.Tuple.Select--import Language.Syntactic--------------------------------------------------------------------------------------- * Construction------------------------------------------------------------------------------------- | Expressions for constructing tuples-data Tuple sig-  where-    Tup2 :: Tuple (a :-> b :-> Full (a,b))-    Tup3 :: Tuple (a :-> b :-> c :-> Full (a,b,c))-    Tup4 :: Tuple (a :-> b :-> c :-> d :-> Full (a,b,c,d))-    Tup5 :: Tuple (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))-    Tup6 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))-    Tup7 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))--instance Constrained Tuple-  where-    type Sat Tuple = Top-    exprDict _ = Dict--instance Semantic Tuple-  where-    semantics Tup2 = Sem "tup2" (,)-    semantics Tup3 = Sem "tup3" (,,)-    semantics Tup4 = Sem "tup4" (,,,)-    semantics Tup5 = Sem "tup5" (,,,,)-    semantics Tup6 = Sem "tup6" (,,,,,)-    semantics Tup7 = Sem "tup7" (,,,,,,)--instance Equality Tuple where equal = equalDefault; exprHash = exprHashDefault-instance Render   Tuple where renderArgs = renderArgsDefault-instance Eval     Tuple where evaluate   = evaluateDefault-instance ToTree   Tuple--------------------------------------------------------------------------------------- * Projection------------------------------------------------------------------------------------- | These families ('Sel1'' - 'Sel7'') are needed because of the problem--- described in:------ <http://emil-fp.blogspot.com/2011/08/fundeps-weaker-than-type-families.html>-type family Sel1' a-type instance Sel1' (a,b)           = a-type instance Sel1' (a,b,c)         = a-type instance Sel1' (a,b,c,d)       = a-type instance Sel1' (a,b,c,d,e)     = a-type instance Sel1' (a,b,c,d,e,f)   = a-type instance Sel1' (a,b,c,d,e,f,g) = a--type family Sel2' a-type instance Sel2' (a,b)           = b-type instance Sel2' (a,b,c)         = b-type instance Sel2' (a,b,c,d)       = b-type instance Sel2' (a,b,c,d,e)     = b-type instance Sel2' (a,b,c,d,e,f)   = b-type instance Sel2' (a,b,c,d,e,f,g) = b--type family Sel3' a-type instance Sel3' (a,b,c)         = c-type instance Sel3' (a,b,c,d)       = c-type instance Sel3' (a,b,c,d,e)     = c-type instance Sel3' (a,b,c,d,e,f)   = c-type instance Sel3' (a,b,c,d,e,f,g) = c--type family Sel4' a-type instance Sel4' (a,b,c,d)       = d-type instance Sel4' (a,b,c,d,e)     = d-type instance Sel4' (a,b,c,d,e,f)   = d-type instance Sel4' (a,b,c,d,e,f,g) = d--type family Sel5' a-type instance Sel5' (a,b,c,d,e)     = e-type instance Sel5' (a,b,c,d,e,f)   = e-type instance Sel5' (a,b,c,d,e,f,g) = e--type family Sel6' a-type instance Sel6' (a,b,c,d,e,f)   = f-type instance Sel6' (a,b,c,d,e,f,g) = f--type family Sel7' a-type instance Sel7' (a,b,c,d,e,f,g) = g---- | Expressions for selecting elements of a tuple-data Select a-  where-    Sel1 :: (Sel1 a b, Sel1' a ~ b) => Select (a :-> Full b)-    Sel2 :: (Sel2 a b, Sel2' a ~ b) => Select (a :-> Full b)-    Sel3 :: (Sel3 a b, Sel3' a ~ b) => Select (a :-> Full b)-    Sel4 :: (Sel4 a b, Sel4' a ~ b) => Select (a :-> Full b)-    Sel5 :: (Sel5 a b, Sel5' a ~ b) => Select (a :-> Full b)-    Sel6 :: (Sel6 a b, Sel6' a ~ b) => Select (a :-> Full b)-    Sel7 :: (Sel7 a b, Sel7' a ~ b) => Select (a :-> Full b)--instance Constrained Select-  where-    type Sat Select = Top-    exprDict _ = Dict--instance Semantic Select-  where-    semantics Sel1 = Sem "sel1" sel1-    semantics Sel2 = Sem "sel2" sel2-    semantics Sel3 = Sem "sel3" sel3-    semantics Sel4 = Sem "sel4" sel4-    semantics Sel5 = Sem "sel5" sel5-    semantics Sel6 = Sem "sel6" sel6-    semantics Sel7 = Sem "sel7" sel7--instance Equality Select where equal = equalDefault; exprHash = exprHashDefault-instance Render   Select where renderArgs = renderArgsDefault-instance Eval     Select where evaluate   = evaluateDefault-instance ToTree   Select---- | Return the selected position, e.g.------ > selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3-selectPos :: Select a -> Int-selectPos Sel1 = 1-selectPos Sel2 = 2-selectPos Sel3 = 3-selectPos Sel4 = 4-selectPos Sel5 = 5-selectPos Sel6 = 6-selectPos Sel7 = 7------ TODO Move these instances to `Language.Syntactic.Frontend.Tuple` ?--instance-    ( Syntactic a dom-    , Syntactic b dom-    , InjectC Tuple dom-        ( Internal a-        , Internal b-        )-    , InjectC Select dom (Internal a)-    , InjectC Select dom (Internal b)-    ) =>-      Syntactic (a,b) dom-  where-    type Internal (a,b) =-        ( Internal a-        , Internal b-        )--    desugar = uncurryN $ sugarN $ appSymC Tup2--    sugar a =-        ( sugarSymC Sel1 a-        , sugarSymC Sel2 a-        )---instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , InjectC Tuple dom-        ( Internal a-        , Internal b-        , Internal c-        )-    , InjectC Select dom (Internal a)-    , InjectC Select dom (Internal b)-    , InjectC Select dom (Internal c)-    ) =>-      Syntactic (a,b,c) dom-  where-    type Internal (a,b,c) =-        ( Internal a-        , Internal b-        , Internal c-        )--    desugar = uncurryN $ sugarN $ appSymC Tup3-    sugar a =-        ( sugarSymC Sel1 a-        , sugarSymC Sel2 a-        , sugarSymC Sel3 a-        )--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , InjectC Tuple dom-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        )-    , InjectC Select dom (Internal a)-    , InjectC Select dom (Internal b)-    , InjectC Select dom (Internal c)-    , InjectC Select dom (Internal d)-    ) =>-      Syntactic (a,b,c,d) dom-  where-    type Internal (a,b,c,d) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        )--    desugar = uncurryN $ sugarN $ appSymC Tup4-    sugar a =-        ( sugarSymC Sel1 a-        , sugarSymC Sel2 a-        , sugarSymC Sel3 a-        , sugarSymC Sel4 a-        )---instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , Syntactic e dom-    , InjectC Tuple dom-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        )-    , InjectC Select dom (Internal a)-    , InjectC Select dom (Internal b)-    , InjectC Select dom (Internal c)-    , InjectC Select dom (Internal d)-    , InjectC Select dom (Internal e)-    ) =>-      Syntactic (a,b,c,d,e) dom-  where-    type Internal (a,b,c,d,e) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        )--    desugar = uncurryN $ sugarN $ appSymC Tup5-    sugar a =-        ( sugarSymC Sel1 a-        , sugarSymC Sel2 a-        , sugarSymC Sel3 a-        , sugarSymC Sel4 a-        , sugarSymC Sel5 a-        )--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , Syntactic e dom-    , Syntactic f dom-    , InjectC Tuple dom-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        )-    , InjectC Select dom (Internal a)-    , InjectC Select dom (Internal b)-    , InjectC Select dom (Internal c)-    , InjectC Select dom (Internal d)-    , InjectC Select dom (Internal e)-    , InjectC Select dom (Internal f)-    ) =>-      Syntactic (a,b,c,d,e,f) dom-  where-    type Internal (a,b,c,d,e,f) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        )--    desugar = uncurryN $ sugarN $ appSymC Tup6-    sugar a =-        ( sugarSymC Sel1 a-        , sugarSymC Sel2 a-        , sugarSymC Sel3 a-        , sugarSymC Sel4 a-        , sugarSymC Sel5 a-        , sugarSymC Sel6 a-        )--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , Syntactic e dom-    , Syntactic f dom-    , Syntactic g dom-    , InjectC Tuple dom-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        , Internal g-        )-    , InjectC Select dom (Internal a)-    , InjectC Select dom (Internal b)-    , InjectC Select dom (Internal c)-    , InjectC Select dom (Internal d)-    , InjectC Select dom (Internal e)-    , InjectC Select dom (Internal f)-    , InjectC Select dom (Internal g)-    ) =>-      Syntactic (a,b,c,d,e,f,g) dom-  where-    type Internal (a,b,c,d,e,f,g) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        , Internal g-        )--    desugar = uncurryN $ sugarN $ appSymC Tup7-    sugar a =-        ( sugarSymC Sel1 a-        , sugarSymC Sel2 a-        , sugarSymC Sel3 a-        , sugarSymC Sel4 a-        , sugarSymC Sel5 a-        , sugarSymC Sel6 a-        , sugarSymC Sel7 a-        )-
− Language/Syntactic/Frontend/Monad.hs 
@@ -1,78 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | Monadic constructs------ This module is based on the paper--- /Generic Monadic Constructs for Embedded Languages/ (Persson et al., IFL 2011--- <http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf>).--module Language.Syntactic.Frontend.Monad where----import Control.Monad.Cont-import Data.Typeable--import Language.Syntactic-import Language.Syntactic.Constructs.Binding.HigherOrder-import Language.Syntactic.Constructs.Monad------ TODO Unfortunately, this module hard-codes the use of `Typeable`. The problem---      is this: Say we replace `Typeable` in the definition of `Mon` by a---      parameter `p`. Then `sugarMonad` will get a constraint `p (a -> m r)`.---      But `r` existentially quantified and can only be constrained in the---      definition of `Mon`. With `Typeable` this works because---      `(Typeable1 m, Typeable a, Typeable r)` implies `Typeable (a -> m r)`.---- | User interface to embedded monadic programs-newtype Mon dom m a-  where-    Mon-        :: { unMon :: forall r-                   .  (Monad m, Typeable r, InjectC (MONAD m) dom (m r))-                   => Cont (ASTF (HODomain dom Typeable) (m r)) a-           }-        -> Mon dom m a--deriving instance Functor (Mon dom m)--instance (Monad m) => Monad (Mon dom m)-  where-    return a = Mon $ return a-    ma >>= f = Mon $ unMon ma >>= unMon . f---- | One-layer desugaring of monadic actions-desugarMonad-    :: ( InjectC (MONAD m) dom (m a)-       , Monad m-       , Typeable1 m-       , Typeable a-       )-    => Mon dom m (ASTF (HODomain dom Typeable) a)-    -> ASTF (HODomain dom Typeable) (m a)-desugarMonad = flip runCont (sugarSymC Return) . unMon---- | One-layer sugaring of monadic actions-sugarMonad-    :: ( Monad m-       , Typeable1 m-       , Typeable a-       )-    => ASTF (HODomain dom Typeable) (m a)-    -> Mon dom m (ASTF (HODomain dom Typeable) a)-sugarMonad ma = Mon $ cont $ sugarSymC Bind ma--instance ( Syntactic a (HODomain dom Typeable)-         , InjectC (MONAD m) dom (m (Internal a))-         , Monad m-         , Typeable1 m-         , Typeable (Internal a)-         ) =>-           Syntactic (Mon dom m a) (HODomain dom Typeable)-  where-    type Internal (Mon dom m a) = m (Internal a)-    desugar = desugarMonad . fmap desugar-    sugar   = fmap sugar   . sugarMonad-
− Language/Syntactic/Interpretation/Equality.hs 
@@ -1,52 +0,0 @@-module Language.Syntactic.Interpretation.Equality where----import Data.Hash--import Language.Syntactic.Syntax------ | Equality for expressions-class Equality expr-  where-    -- | Equality for expressions-    ---    -- Comparing expressions of different types is often needed when dealing-    -- with expressions with existentially quantified sub-terms.-    equal :: expr a -> expr b -> Bool--    -- | Computes a 'Hash' for an expression. Expressions that are equal-    -- according to 'equal' must result in the same hash:-    ---    -- @equal a b  ==>  exprHash a == exprHash b@-    exprHash :: expr a -> Hash---instance Equality dom => Equality (AST dom)-  where-    equal (Sym a)    (Sym b)    = equal a b-    equal (s1 :$ a1) (s2 :$ a2) = equal s1 s2 && equal a1 a2-    equal _ _                   = False--    exprHash (Sym a)  = hashInt 0 `combine` exprHash a-    exprHash (s :$ a) = hashInt 1 `combine` exprHash s `combine` exprHash a--instance Equality dom => Eq (AST dom a)-  where-    (==) = equal--instance (Equality expr1, Equality expr2) => Equality (expr1 :+: expr2)-  where-    equal (InjL a) (InjL b) = equal a b-    equal (InjR a) (InjR b) = equal a b-    equal _ _               = False--    exprHash (InjL a) = hashInt 0 `combine` exprHash a-    exprHash (InjR a) = hashInt 1 `combine` exprHash a--instance (Equality expr1, Equality expr2) => Eq ((expr1 :+: expr2) a)-  where-    (==) = equal-
− Language/Syntactic/Interpretation/Evaluation.hs 
@@ -1,28 +0,0 @@-module Language.Syntactic.Interpretation.Evaluation where----import Language.Syntactic.Syntax------ | The denotation of a symbol with the given signature-type family   Denotation sig-type instance Denotation (Full a)    = a-type instance Denotation (a :-> sig) = a -> Denotation sig--class Eval expr-  where-    -- | Evaluation of expressions-    evaluate :: expr a -> Denotation a--instance Eval dom => Eval (AST dom)-  where-    evaluate (Sym a)  = evaluate a-    evaluate (s :$ a) = evaluate s $ evaluate a--instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)-  where-    evaluate (InjL a) = evaluate a-    evaluate (InjR a) = evaluate a-
− Language/Syntactic/Interpretation/Render.hs 
@@ -1,83 +0,0 @@-module Language.Syntactic.Interpretation.Render-    ( Render (..)-    , printExpr-    , ToTree (..)-    , showAST-    , drawAST-    ) where----import Data.Tree--import Language.Syntactic.Syntax------ | Render an expression as concrete syntax. A complete instance must define--- either of the methods 'render' and 'renderArgs'.-class Render expr-  where-    -- | Render an expression as a 'String'-    render :: expr a -> String-    render = renderArgs []--    -- | Render a partially applied expression given a list of rendered missing-    -- arguments-    renderArgs :: [String] -> expr a -> String-    renderArgs []   a = render a-    renderArgs args a = "(" ++ unwords (render a : args) ++ ")"--instance Render dom => Render (AST dom)-  where-    renderArgs args (Sym a)  = renderArgs args a-    renderArgs args (s :$ a) = renderArgs (render a : args) s--instance Render dom => Show (AST dom a)-  where-    show = render--instance (Render expr1, Render expr2) => Render (expr1 :+: expr2)-  where-    renderArgs args (InjL a) = renderArgs args a-    renderArgs args (InjR a) = renderArgs args a--instance (Render expr1, Render expr2) => Show ((expr1 :+: expr2) a)-  where-    show = render---- | Print an expression-printExpr :: Render expr => expr a -> IO ()-printExpr = putStrLn . render----class Render expr => ToTree expr-  where-    -- | Convert a partially applied expression to a syntax tree given a list of-    -- rendered missing arguments-    toTreeArgs :: [Tree String] -> expr a -> Tree String-    toTreeArgs args a = Node (render a) args--instance ToTree dom => ToTree (AST dom)-  where-    toTreeArgs args (Sym a)  = toTreeArgs args a-    toTreeArgs args (s :$ a) = toTreeArgs (toTree a : args) s--instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2)-  where-    toTreeArgs args (InjL a) = toTreeArgs args a-    toTreeArgs args (InjR a) = toTreeArgs args a---- | Convert an expression to a syntax tree-toTree :: ToTree expr => expr a -> Tree String-toTree = toTreeArgs []---- | Show syntax tree using ASCII art-showAST :: ToTree dom => AST dom a -> String-showAST = drawTree . toTree---- | Print syntax tree using ASCII art-drawAST :: ToTree dom => AST dom a -> IO ()-drawAST = putStrLn . showAST-
− Language/Syntactic/Interpretation/Semantics.hs 
@@ -1,76 +0,0 @@--- | Default implementations of some interpretation functions--module Language.Syntactic.Interpretation.Semantics where----import Data.Hash--import Language.Syntactic.Syntax-import Language.Syntactic.Interpretation.Equality-import Language.Syntactic.Interpretation.Render-import Language.Syntactic.Interpretation.Evaluation------ | A representation of a syntactic construct as a 'String' and an evaluation--- function. It is not meant to be used as a syntactic symbol in an 'AST'. Its--- only purpose is to provide the default implementations of functions like--- `equal` via the `Semantic` class.-data Semantics a-  where-    Sem-        :: { semanticName :: String-           , semanticEval :: Denotation a-           }-        -> Semantics a----instance Equality Semantics-  where-    equal (Sem a _) (Sem b _) = a==b-    exprHash (Sem name _)     = hash name--instance Render Semantics-  where-    renderArgs [] (Sem name _) = name-    renderArgs args (Sem name _)-        | isInfix   = "(" ++ unwords [a,op,b] ++ ")"-        | otherwise = "(" ++ unwords (name : args) ++ ")"-      where-        [a,b] = args-        op    = init $ tail name-        isInfix-          =  not (null name)-          && head name == '('-          && last name == ')'-          && length args == 2--instance Eval Semantics-  where-    evaluate (Sem _ a) = a------ | Class of expressions that can be treated as constructs-class Semantic expr-  where-    semantics :: expr a -> Semantics a---- | Default implementation of 'equal'-equalDefault :: Semantic expr => expr a -> expr b -> Bool-equalDefault a b = equal (semantics a) (semantics b)---- | Default implementation of 'exprHash'-exprHashDefault :: Semantic expr => expr a -> Hash-exprHashDefault = exprHash . semantics---- | Default implementation of 'renderArgs'-renderArgsDefault :: Semantic expr => [String] -> expr a -> String-renderArgsDefault args = renderArgs args . semantics---- | Default implementation of 'evaluate'-evaluateDefault :: Semantic expr => expr a -> Denotation a-evaluateDefault = evaluate . semantics-
− Language/Syntactic/Sharing/Graph.hs 
@@ -1,336 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | Representation and manipulation of abstract syntax graphs--module Language.Syntactic.Sharing.Graph where----import Control.Arrow ((***))-import Control.Monad.Reader-import Data.Array-import Data.Function-import Data.List-import Data.Typeable--import Data.Hash--import Language.Syntactic-import Language.Syntactic.Constructs.Binding-import Language.Syntactic.Sharing.Utils--------------------------------------------------------------------------------------- * Representation------------------------------------------------------------------------------------- | Node identifier-newtype NodeId = NodeId { nodeInteger :: Integer }-  deriving (Eq, Ord, Num, Real, Integral, Enum, Ix)--instance Show NodeId-  where-    show (NodeId i) = show i--showNode :: NodeId -> String-showNode n = "node:" ++ show n------ | Placeholder for a syntax tree-data Node a-  where-    Node :: NodeId -> Node (Full a)--instance Constrained Node-  where-    type Sat Node = Top-    exprDict _ = Dict--instance Render Node-  where-    render (Node a) = showNode a--instance ToTree Node------ | Environment for alpha-equivalence-class NodeEqEnv dom a-  where-    prjNodeEqEnv :: a -> NodeEnv dom-    modNodeEqEnv :: (NodeEnv dom -> NodeEnv dom) -> (a -> a)--type EqEnv dom = ([(VarId,VarId)], NodeEnv dom)--type NodeEnv dom =-    ( Array NodeId Hash-    , Array NodeId (ASTB dom)-    )--instance NodeEqEnv dom (EqEnv dom)-  where-    prjNodeEqEnv   = snd-    modNodeEqEnv f = (id *** f)--instance VarEqEnv (EqEnv dom)-  where-    prjVarEqEnv   = fst-    modVarEqEnv f = (f *** id)--instance (AlphaEq dom dom dom env, NodeEqEnv dom env) =>-    AlphaEq Node Node dom env-  where-    alphaEqSym (Node n1) Nil (Node n2) Nil-        | n1 == n2  = return True-        | otherwise = do-            (hTab,nTab) :: NodeEnv dom <- asks prjNodeEqEnv-            if hTab!n1 /= hTab!n2-              then return False-              else case (nTab!n1, nTab!n2) of-                  (ASTB a, ASTB b) -> alphaEqM a b-                    -- TODO The result could be memoized in a-                    -- @Map (NodeId,NodeId) Bool@--  -- TODO With only this instance, the result will be 'False' when one argument-  --      is a 'Node' and the other one isn't. This is not really correct since-  --      'Node's are just meta-variables and shouldn't be part of the-  --      comparison. But as long as equivalent expressions always have 'Node's-  --      at the same position, it doesn't matter. This could probably be fixed-  --      by adding two overlapping instances.------ | \"Abstract Syntax Graph\"------ A representation of a syntax tree with explicit sharing. An 'ASG' is valid if--- and only if 'inlineAll' succeeds (and the 'numNodes' field is correct).-data ASG dom a = ASG-    { topExpression :: ASTF (NodeDomain dom) a            -- ^ Top-level expression-    , graphNodes    :: [(NodeId, ASTB (NodeDomain dom))]  -- ^ Mapping from node id to sub-expression-    , numNodes      :: NodeId                             -- ^ Total number of nodes-    }--type NodeDomain dom = (Node :+: dom) :|| Sat dom------ | Show syntax graph using ASCII art-showASG :: ToTree dom => ASG dom a -> String-showASG (ASG top nodes _) =-    unlines ((line "top" ++ showAST top) : map showNode nodes)-  where-    line str = "---- " ++ str ++ " " ++ rest ++ "\n"-      where-        rest = take (40 - length str) $ repeat '-'--    showNode (n, ASTB expr) = concat-      [ line ("node:" ++ show n)-      , showAST expr-      ]---- | Print syntax graph using ASCII art-drawASG :: ToTree dom => ASG dom a -> IO ()-drawASG = putStrLn . showASG---- | Update the node identifiers in an 'AST' using the supplied reindexing--- function-reindexNodesAST ::-    (NodeId -> NodeId) -> AST (NodeDomain dom) a -> AST (NodeDomain dom) a-reindexNodesAST reix (Sym (C' (InjL (Node n)))) = injC $ Node $ reix n-reindexNodesAST reix (s :$ a) = reindexNodesAST reix s :$ reindexNodesAST reix a-reindexNodesAST reix a = a---- | Reindex the nodes according to the given index mapping. The number of nodes--- is unchanged, so if the index mapping is not 1:1, the resulting graph will--- contain duplicates.-reindexNodes :: (NodeId -> NodeId) -> ASG dom a -> ASG dom a-reindexNodes reix (ASG top nodes n) = ASG top' nodes' n-  where-    top'   = reindexNodesAST reix top-    nodes' =-      [ (reix n, ASTB $ reindexNodesAST reix a)-        | (n, ASTB a) <- nodes-      ]---- | Reindex the nodes to be in the range @[0 .. l-1]@, where @l@ is the number--- of nodes in the graph-reindexNodesFrom0 :: ASG dom a -> ASG dom a-reindexNodesFrom0 graph = reindexNodes reix graph-  where-    reix = reindex $ map fst $ graphNodes graph---- | Remove duplicate nodes from a graph. The function only looks at the--- 'NodeId' of each node. The 'numNodes' field is updated accordingly.-nubNodes :: ASG dom a -> ASG dom a-nubNodes (ASG top nodes n) = ASG top nodes' n'-  where-    nodes' = nubBy ((==) `on` fst) nodes-    n'     = genericLength nodes'--------------------------------------------------------------------------------------- * Folding------------------------------------------------------------------------------------- | Pattern functor representation of an 'AST' with 'Node's-data SyntaxPF dom a-  where-    AppPF  :: a -> a -> SyntaxPF dom a-    NodePF :: NodeId -> a -> SyntaxPF dom a-    DomPF  :: dom b -> SyntaxPF dom a-  -- NOTE: The important constructor is 'NodePF', which makes a 'Node' appear as-  -- any other recursive constructor.--instance Functor (SyntaxPF dom)-  where-    fmap f (AppPF g a)  = AppPF  (f g) (f a)-    fmap f (NodePF n a) = NodePF n (f a)-    fmap f (DomPF a)    = DomPF a------ | Folding over a graph------ The user provides a function to fold a single constructor (an \"algebra\").--- The result contains the result of folding the whole graph as well as the--- result of each internal node, represented both as an array and an association--- list. Each node is processed exactly once.-foldGraph :: forall dom a b .-    (SyntaxPF dom b -> b) -> ASG dom a -> (b, (Array NodeId b, [(NodeId,b)]))-foldGraph alg (ASG top ns nn) = (g top, (arr,nodes))-  where-    nodes = [(n, g expr) | (n, ASTB expr) <- ns]-    arr   = array (0, nn-1) nodes--    g :: AST (NodeDomain dom) c -> b-    g (h :$ a)                   = alg $ AppPF (g h) (g a)-    g (Sym (C' (InjL (Node n)))) = alg $ NodePF n (arr!n)-    g (Sym (C' (InjR a)))        = alg $ DomPF a--------------------------------------------------------------------------------------- * Inlining------------------------------------------------------------------------------------- | Convert an 'ASG' to an 'AST' by inlining all nodes-inlineAll :: forall dom a . ConstrainedBy dom Typeable =>-    ASG dom a -> ASTF dom a-inlineAll (ASG top nodes n) = inline top-  where-    nodeMap = array (0, n-1) nodes--    inline :: AST (NodeDomain dom) b -> AST dom b-    inline (s :$ a) = inline s :$ inline a-    inline s@(Sym (C' (InjL (Node n)))) = case nodeMap ! n of-        ASTB a-          | Dict :: Dict (Typeable x) <- exprDictSub s-          , Dict :: Dict (Typeable y) <- exprDictSub a-          -> case gcast a of-               Nothing -> error "inlineAll: type mismatch"-               Just a  -> inline a-    inline (Sym (C' (InjR a))) = Sym a------ | Find the child nodes of each node in an expression. The child nodes of a--- node @n@ are the first nodes along all paths from @n@.-nodeChildren :: ASG dom a -> [(NodeId, [NodeId])]-nodeChildren = map (id *** fromDList) . snd . snd . foldGraph children-  where-    children :: SyntaxPF dom (DList NodeId) -> DList (NodeId)-    children (AppPF ns1 ns2) = ns1 . ns2-    children (NodePF n _)    = single n-    children _               = empty---- | Count the number of occurrences of each node in an expression-occurrences :: ASG dom a -> Array NodeId Int-occurrences graph-    = count (0, numNodes graph - 1)-    $ concatMap snd-    $ nodeChildren graph---- | Inline all nodes that are not shared-inlineSingle :: forall dom a . ConstrainedBy dom Typeable =>-    ASG dom a -> ASG dom a-inlineSingle graph@(ASG top nodes n) = ASG top' nodes' n'-  where-    nodeTab  = array (0, n-1) nodes-    occs     = occurrences graph--    top'   = inline top-    nodes' = [(n, ASTB (inline a)) | (n, ASTB a) <- nodes, occs!n > 1]-    n'     = genericLength nodes'--    inline :: AST (NodeDomain dom) b -> AST (NodeDomain dom) b-    inline (s :$ a) = inline s :$ inline a-    inline s@(Sym (C' (InjL (Node n))))-        | occs!n > 1 = injC $ Node n-        | otherwise = case nodeTab ! n of-            ASTB a-              | Dict :: Dict (Typeable x) <- exprDictSub s-              , Dict :: Dict (Typeable y) <- exprDictSub a-              -> case gcast a of-                   Nothing -> error "inlineSingle: type mismatch"-                   Just a  -> inline a-    inline (Sym (C' (InjR a))) = Sym $ C' $ InjR a--------------------------------------------------------------------------------------- * Sharing------------------------------------------------------------------------------------- | Compute a table (both array and list representation) of hash values for--- each node-hashNodes :: Equality dom => ASG dom a -> (Array NodeId Hash, [(NodeId, Hash)])-hashNodes = snd . foldGraph hashNode-  where-    hashNode (AppPF h1 h2) = hashInt 0 `combine` h1 `combine` h2-    hashNode (NodePF _ h)  = h-    hashNode (DomPF a)     = hashInt 1 `combine` exprHash a------ | Partitions the nodes such that two nodes are in the same sub-list if and--- only if they are alpha-equivalent.-partitionNodes :: forall dom a-    .  ( Equality dom-       , AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom))-       )-    => ASG dom a -> [[NodeId]]-partitionNodes graph = concatMap (fullPartition nodeEq) approxPartitioning-  where-    nTab          = array (0, numNodes graph - 1) (graphNodes graph)-    (hTab,hashes) = hashNodes graph--    -- | An approximate partitioning of the nodes: nodes in different partitions-    -- are guaranteed to be inequivalent, while nodes in the same partition-    -- might be equivalent.-    approxPartitioning-        = map (map fst)-        $ groupBy ((==) `on` snd)-        $ sortBy (compare `on` snd)-        $ hashes--    nodeEq :: NodeId -> NodeId -> Bool-    nodeEq n1 n2 = runReader-        (liftASTB2 alphaEqM (nTab!n1) (nTab!n2))-        (([],(hTab,nTab)) :: EqEnv (NodeDomain dom))------ | Common sub-expression elimination based on alpha-equivalence-cse-    :: ( Equality dom-       , AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom))-       )-    => ASG dom a -> ASG dom a-cse graph@(ASG top nodes n) = nubNodes $ reindexNodes (reixTab!) graph-  where-    parts   = partitionNodes graph-    reixTab = array (0,n-1) [(n,p) | (part,p) <- parts `zip` [0..], n <- part]-
− Language/Syntactic/Sharing/Reify.hs 
@@ -1,80 +0,0 @@--- | Reifying the sharing in an 'AST'------ This module is based on the paper /Type-Safe Observable Sharing in Haskell/--- (Andy Gill, 2009, <http://dx.doi.org/10.1145/1596638.1596653>).--module Language.Syntactic.Sharing.Reify-    ( reifyGraph-    ) where----import Control.Monad.Writer-import Data.IntMap as Map-import Data.IORef-import System.Mem.StableName--import Language.Syntactic-import Language.Syntactic.Sharing.Graph-import Language.Syntactic.Sharing.StableName------ | Shorthand used by 'reifyGraphM'------ Writes out a list of encountered nodes and returns the top expression.-type GraphMonad dom a = WriterT-      [(NodeId, ASTB (NodeDomain dom))]-      IO-      (AST (NodeDomain dom) a)----reifyGraphM :: forall dom a . Constrained dom-    => (forall a . ASTF dom a -> Bool)-    -> IORef NodeId-    -> IORef (History (AST dom))-    -> ASTF dom a-    -> GraphMonad dom (Full a)--reifyGraphM canShare nSupp history = reifyNode-  where-    reifyNode :: ASTF dom b -> GraphMonad dom (Full b)-    reifyNode a-      | Dict <- exprDict a = case canShare a of-          False               -> reifyRec a-          True | a `seq` True -> do-            st   <- liftIO $ makeStableName a-            hist <- liftIO $ readIORef history-            case lookHistory hist (StName st) of-              Just n -> return $ injC $ Node n-              _ -> do-                n  <- fresh nSupp-                liftIO $ modifyIORef history $ remember (StName st) n-                a' <- reifyRec a-                tell [(n, ASTB a')]-                return $ injC $ Node n--    reifyRec :: Sat dom (DenResult b) => AST dom b -> GraphMonad dom b-    reifyRec (f :$ a) = liftM2 (:$) (reifyRec f) (reifyNode a)-    reifyRec (Sym s)  = return $ Sym $ C' $ InjR s------ | Convert a syntax tree to a sharing-preserving graph------ This function is not referentially transparent (hence the 'IO'). However, it--- is well-behaved in the sense that the worst thing that could happen is that--- sharing is lost. It is not possible to get false sharing.-reifyGraph :: Constrained dom-    => (forall a . ASTF dom a -> Bool)-         -- ^ A function that decides whether a given node can be shared-    -> ASTF dom a-    -> IO (ASG dom a)-reifyGraph canShare a = do-    nSupp   <- newIORef 0-    history <- newIORef empty-    (a',ns) <- runWriterT $ reifyGraphM canShare nSupp history a-    n       <- readIORef nSupp-    return (ASG a' ns n)-
− Language/Syntactic/Sharing/ReifyHO.hs 
@@ -1,106 +0,0 @@--- | This module is similar to "Language.Syntactic.Sharing.Reify", but operates--- on @`AST` (`HODomain` dom p)@ rather than a general 'AST'. The reason for--- having this module is that when using 'HODomain', it is important to do--- simultaneous sharing analysis and 'HOLambda' reification. Obviously we cannot--- do sharing analysis first (using--- 'Language.Syntactic.Sharing.Reify.reifyGraph' from--- "Language.Syntactic.Sharing.Reify"), since it needs to be able to look inside--- 'HOLambda'. On the other hand, if we did 'HOLambda' reification first (using--- 'reify'), we would destroy the sharing.------ This module is based on the paper /Type-Safe Observable Sharing in Haskell/--- (Andy Gill, 2009, <http://dx.doi.org/10.1145/1596638.1596653>).--module Language.Syntactic.Sharing.ReifyHO-    ( reifyGraphTop-    , reifyGraph-    ) where----import Control.Monad.Writer-import Data.IntMap as Map-import Data.IORef-import System.Mem.StableName--import Language.Syntactic-import Language.Syntactic.Constructs.Binding-import Language.Syntactic.Constructs.Binding.HigherOrder-import Language.Syntactic.Sharing.Graph-import Language.Syntactic.Sharing.StableName-import qualified Language.Syntactic.Sharing.Reify  -- For Haddock------ | Shorthand used by 'reifyGraphM'------ Writes out a list of encountered nodes and returns the top expression.-type GraphMonad dom p a = WriterT-      [(NodeId, ASTB (NodeDomain ((Lambda :+: Variable :+: dom) :|| p)))]-      IO-      (AST (NodeDomain ((Lambda :+: Variable :+: dom) :|| p)) a)----reifyGraphM :: forall dom p a-    .  (forall a . ASTF (HODomain dom p) a -> Bool)-    -> IORef VarId-    -> IORef NodeId-    -> IORef (History (AST (HODomain dom p)))-    -> ASTF (HODomain dom p) a-    -> GraphMonad dom p (Full a)--reifyGraphM canShare vSupp nSupp history = reifyNode-  where-    reifyNode :: ASTF (HODomain dom p) b -> GraphMonad dom p (Full b)-    reifyNode a-      | Dict <- exprDict a = case canShare a of-          False               -> reifyRec a-          True | a `seq` True -> do-            st   <- liftIO $ makeStableName a-            hist <- liftIO $ readIORef history-            case lookHistory hist (StName st) of-              Just n -> return $ injC $ Node n-              _ -> do-                n  <- fresh nSupp-                liftIO $ modifyIORef history $ remember (StName st) n-                a' <- reifyRec a-                tell [(n, ASTB a')]-                return $ injC $ Node n--    reifyRec :: AST (HODomain dom p) b -> GraphMonad dom p b-    reifyRec (f :$ a)            = liftM2 (:$) (reifyRec f) (reifyNode a)-    reifyRec (Sym (C' (InjR a))) = return $ Sym $ C' $ InjR $ C' $ InjR a-    reifyRec (Sym (C' (InjL (HOLambda f)))) = do-        v    <- fresh vSupp-        body <- reifyNode $ f $ injC $ Variable v-        return $ injC (Lambda v) :$ body------ | Convert a syntax tree to a sharing-preserving graph-reifyGraphTop-    :: (forall a . ASTF (HODomain dom p) a -> Bool)-    -> ASTF (HODomain dom p) a-    -> IO (ASG ((Lambda :+: Variable :+: dom) :|| p) a, VarId)-reifyGraphTop canShare a = do-    vSupp   <- newIORef 0-    nSupp   <- newIORef 0-    history <- newIORef empty-    (a',ns) <- runWriterT $ reifyGraphM canShare vSupp nSupp history a-    v       <- readIORef vSupp-    n       <- readIORef nSupp-    return (ASG a' ns n, v)---- | Reifying an n-ary syntactic function to a sharing-preserving graph------ This function is not referentially transparent (hence the 'IO'). However, it--- is well-behaved in the sense that the worst thing that could happen is that--- sharing is lost. It is not possible to get false sharing.-reifyGraph :: Syntactic a (HODomain dom p)-    => (forall a . ASTF (HODomain dom p) a -> Bool)-         -- ^ A function that decides whether a given node can be shared-    -> a-    -> IO (ASG ((Lambda :+: Variable :+: dom) :|| p) (Internal a), VarId)-reifyGraph canShare = reifyGraphTop canShare . desugar-
− Language/Syntactic/Sharing/SimpleCodeMotion.hs 
@@ -1,214 +0,0 @@--- | Simple code motion transformation performing common sub-expression--- elimination and variable hoisting. Note that the implementation is very--- inefficient.------ The code is based on an implementation by Gergely Dévai.--module Language.Syntactic.Sharing.SimpleCodeMotion-    ( BindDict (..)-    , codeMotion-    , defaultBindDict-    , reifySmart-    , reifySmartDefault-    ) where----import Control.Monad.State-import Data.Set as Set-import Data.Typeable--import Language.Syntactic-import Language.Syntactic.Constructs.Binding-import Language.Syntactic.Constructs.Binding.HigherOrder------ | Interface for binding constructs-data BindDict dom = BindDict-    { prjVariable :: forall a   . dom a -> Maybe VarId-    , prjLambda   :: forall a   . dom a -> Maybe VarId-    , injVariable :: forall a   . ASTF dom a -> VarId -> dom (Full a)-    , injLambda   :: forall a b . ASTF dom a -> ASTF dom b -> VarId -> dom (b :-> Full (a -> b))-    , injLet      :: forall a b . ASTF dom b -> dom (a :-> (a -> b) :-> Full b)-    }---- | Substituting a sub-expression. Assumes no variable capturing in the--- expressions involved.-substitute :: forall dom a b-    .  (ConstrainedBy dom Typeable, AlphaEq dom dom dom [(VarId,VarId)])-    => ASTF dom a  -- ^ Sub-expression to be replaced-    -> ASTF dom a  -- ^ Replacing sub-expression-    -> ASTF dom b  -- ^ Whole expression-    -> ASTF dom b-substitute x y a-    | Dict :: Dict (Typeable a) <- exprDictSub y-    , Dict :: Dict (Typeable b) <- exprDictSub a-    , Just y' <- gcast y, alphaEq x a = y'-    | otherwise = subst a-  where-    subst :: AST dom c -> AST dom c-    subst (f :$ a) = subst f :$ substitute x y a-    subst a = a---- | Count the number of occurrences of a sub-expression-count :: forall dom a b-    .  AlphaEq dom dom dom [(VarId,VarId)]-    => ASTF dom a  -- ^ Expression to count-    -> ASTF dom b  -- ^ Expression to count in-    -> Int-count a b-    | alphaEq a b = 1-    | otherwise   = cnt b-  where-    cnt :: AST dom c -> Int-    cnt (f :$ b) = cnt f + count a b-    cnt _        = 0--nonTerminal :: AST dom a -> Bool-nonTerminal (_ :$ _) = True-nonTerminal _        = False---- | Environment for the expression in the 'choose' function-data Env dom = Env-    { inLambda :: Bool  -- ^ Whether the current expression is inside a lambda-    , canShare :: forall a . dom a -> Bool-        -- ^ Whether a given symbol can be shared-    , counter  :: ASTE dom -> Int-        -- ^ Counting the number of occurrences of an expression in the-        -- environment-    , dependencies :: Set VarId-        -- ^ The set of variables that are not allowed to occur in the chosen-        -- expression-    }--independent :: BindDict dom -> Env dom -> AST dom a -> Bool-independent bindDict env (Sym (prjVariable bindDict -> Just v)) =-    not (v `member` dependencies env)-independent bindDict env (f :$ a) =-    independent bindDict env f && independent bindDict env a-independent _ _ _ = True---- | Checks whether a sub-expression in a given environment can be lifted out-liftable :: BindDict dom -> Env dom -> ASTF dom a -> Bool-liftable bindDict env a = independent bindDict env a && heuristic-    -- Lifting dependent expressions is semantically incorrect-  where-    heuristic-        =  simpleMatch (const . canShare env) a-        && nonTerminal a-        && (inLambda env || (counter env (ASTE a) > 1))---- | Choose a sub-expression to share-choose-    :: AlphaEq dom dom dom [(VarId,VarId)]-    => BindDict dom-    -> (forall a . dom a -> Bool)-    -> ASTF dom a-    -> Maybe (ASTE dom)-choose bindDict canShr a = chooseEnv bindDict env a-  where-    env = Env-        { inLambda     = False-        , canShare     = canShr-        , counter      = \(ASTE b) -> count b a-        , dependencies = empty-        }---- | Choose a sub-expression to share in an 'Env' environment-chooseEnv :: BindDict dom -> Env dom -> ASTF dom a -> Maybe (ASTE dom)-chooseEnv bindDict env a-    | liftable bindDict env a = Just (ASTE a)-    | otherwise               = chooseEnvSub bindDict env a---- | Like 'chooseEnv', but does not consider the top expression for sharing-chooseEnvSub :: BindDict dom -> Env dom -> AST dom a -> Maybe (ASTE dom)-chooseEnvSub bindDict env (Sym (prjLambda bindDict -> Just v) :$ a) =-    chooseEnv bindDict env' a-  where-    env' = env-        { inLambda     = True-        , dependencies = insert v (dependencies env)-        }-chooseEnvSub bindDict env (f :$ a) =-    chooseEnvSub bindDict env f `mplus` chooseEnv bindDict env a-chooseEnvSub _ _ _ = Nothing------ | Perform common sub-expression elimination and variable hoisting-codeMotion :: forall dom a-    .  ( ConstrainedBy dom Typeable-       , AlphaEq dom dom dom [(VarId,VarId)]-       )-    => BindDict dom-    -> (forall a . dom a -> Bool)-    -> ASTF dom a-    -> State VarId (ASTF dom a)-codeMotion bindDict canShr a-    | Just b <- choose bindDict canShr a = share b-    | otherwise                          = descend a-  where-    share (ASTE b) = do-        b' <- codeMotion bindDict canShr b-        v  <- get; put (v+1)-        let x = Sym (injVariable bindDict b v)-        body <- codeMotion bindDict canShr $ substitute b x a-        return-            $  Sym (injLet bindDict body)-            :$ b'-            :$ (Sym (injLambda bindDict b' body v) :$ body)--    descend :: AST dom b -> State VarId (AST dom b)-    descend (f :$ a) = liftM2 (:$) (descend f) (codeMotion bindDict canShr a)-    descend a        = return a----defaultBindDict-    :: (Variable :<: dom, Lambda :<: dom, Let :<: dom, Constrained dom)-    => BindDict (dom :|| Typeable)-defaultBindDict = BindDict-    { prjVariable = \a -> do-        Variable v <- prj a-        return v--    , prjLambda = \a -> do-        Lambda v <- prj a-        return v--    , injVariable = \ref v -> case exprDict ref of-        Dict -> C' $ inj (Variable v)-    , injLambda = \refa refb v -> case (exprDict refa, exprDict refb) of-        (Dict, Dict) -> C' $ inj (Lambda v)-    , injLet = \ref -> case exprDict ref of-        Dict -> C' $ inj Let-    }------ TODO Abstract away from Typeable?---- | Like 'reify' but with common sub-expression elimination and variable--- hoisting-reifySmart-    :: ( AlphaEq dom dom ((Lambda :+: Variable :+: dom) :|| Typeable) [(VarId,VarId)]-       , Syntactic a (HODomain dom Typeable)-       )-    => BindDict ((Lambda :+: Variable :+: dom) :|| Typeable)-    -> (forall a . ((Lambda :+: Variable :+: dom) :|| Typeable) a -> Bool)-    -> a-    -> ASTF ((Lambda :+: Variable :+: dom) :|| Typeable) (Internal a)-reifySmart dict canShr = flip evalState 0 .-    (codeMotion dict canShr <=< reifyM . desugar)--reifySmartDefault-    :: ( Let :<: dom-       , AlphaEq dom dom ((Lambda :+: Variable :+: dom) :|| Typeable) [(VarId,VarId)]-       , Syntactic a (HODomain dom Typeable)-       )-    => (forall a . ((Lambda :+: Variable :+: dom) :|| Typeable) a -> Bool)-    -> a-    -> ASTF ((Lambda :+: Variable :+: dom) :|| Typeable) (Internal a)-reifySmartDefault = reifySmart defaultBindDict-
− Language/Syntactic/Sharing/StableName.hs 
@@ -1,53 +0,0 @@-module Language.Syntactic.Sharing.StableName where----import Control.Monad.IO.Class-import Data.IntMap as Map-import Data.IORef-import System.Mem.StableName-import Unsafe.Coerce--import Language.Syntactic-import Language.Syntactic.Sharing.Graph------ | 'StableName' of a @(c (Full a))@ with hidden result type-data StName c-  where-    StName :: StableName (c (Full a)) -> StName c--instance Eq (StName c)-  where-    StName a == StName b = a == unsafeCoerce b-      -- This is "probably" safe according to-      -- <http://www.haskell.org/pipermail/glasgow-haskell-users/2012-August/022758.html>--      -- TODO In future, use `eqStableName`. It should be in GHC 7.8.1.--hash :: StName c -> Int-hash (StName st) = hashStableName st---- | A hash table from 'StName' to 'NodeId' (with 'hash' as the hashing--- function). I.e. it is assumed that the 'StName's at each entry all have the--- same hash, and that this number is equal to the entry's key.-type History c = IntMap [(StName c, NodeId)]---- | Lookup a name in the history-lookHistory :: History c -> StName c -> Maybe NodeId-lookHistory hist st = case Map.lookup (hash st) hist of-    Nothing   -> Nothing-    Just list -> Prelude.lookup st list---- | Insert the name into the history-remember :: StName c -> NodeId -> History c -> History c-remember st n hist = insertWith (++) (hash st) [(st,n)] hist---- | Return a fresh identifier from the given supply-fresh :: (Enum a, MonadIO m) => IORef a -> m a-fresh aRef = do-    a <- liftIO $ readIORef aRef-    liftIO $ writeIORef aRef (succ a)-    return a-
− Language/Syntactic/Sharing/Utils.hs 
@@ -1,59 +0,0 @@--- | Some utility functions used by the other modules--module Language.Syntactic.Sharing.Utils where----import Data.Array-import Data.List--------------------------------------------------------------------------------------- * Difference lists------------------------------------------------------------------------------------- | Difference list-type DList a = [a] -> [a]---- | Empty list-empty :: DList a-empty = id---- | Singleton list-single :: a -> DList a-single = (:)--fromDList :: DList a -> [a]-fromDList = ($ [])--------------------------------------------------------------------------------------- * Misc.------------------------------------------------------------------------------------- | Given a list @is@ of unique natural numbers, returns a function that maps--- each number in @is@ to a unique number in the range @[0 .. length is-1]@. The--- complexity is O(@maximum is@).-reindex :: (Integral a, Ix a) => [a] -> a -> a-reindex is = (tab!)-  where-    tab = array (0, maximum is) $ zip is [0..]---- | Count the number of occurrences of each element in the list. The result is--- an array mapping each element to its number of occurrences.-count :: Ix a-    => (a,a)  -- ^ Upper and lower bound on the elements to be counted-    -> [a]    -- ^ Elements to be counted-    -> Array a Int-count bnds as = accumArray (+) 0 bnds [(n,1) | n <- as]---- | Partitions the list such that two elements are in the same sub-list if and--- only if they satisfy the equivalence check. The complexity is O(n^2).-fullPartition :: (a -> a -> Bool) -> [a] -> [[a]]-fullPartition eq []     = []-fullPartition eq (a:as) = (a:as1) : fullPartition eq as2-  where-    (as1,as2) = partition (eq a) as-
− Language/Syntactic/Sugar.hs 
@@ -1,111 +0,0 @@-{-# LANGUAGE OverlappingInstances #-}-{-# LANGUAGE UndecidableInstances #-}---- | \"Syntactic sugar\"--module Language.Syntactic.Sugar where----import Language.Syntactic.Syntax-import Language.Syntactic.Constraint------ | It is usually assumed that @(`desugar` (`sugar` a))@ has the same meaning--- as @a@.-class (Constrained dom, Sat dom (Internal a)) => Syntactic a dom | a -> dom-    -- Note: using a functional dependency rather than an associated type,-    -- because this makes it possible to make a class alias constraining dom.-    -- TODO Now that GHC allows equality super class constraints, this should be-    --      changed to an associated type.-  where-    type Internal a-    desugar :: a -> ASTF dom (Internal a)-    sugar   :: ASTF dom (Internal a) -> a--instance (Constrained dom, Sat dom a) => Syntactic (ASTF dom a) dom-  where-    type Internal (ASTF dom a) = a-    desugar = id-    sugar   = id---- | Syntactic type casting-resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b-resugar = sugar . desugar---- | N-ary syntactic functions------ 'desugarN' has any type of the form:------ > desugarN ::--- >     ( Syntactic a dom--- >     , Syntactic b dom--- >     , ...--- >     , Syntactic x dom--- >     ) => (a -> b -> ... -> x)--- >       -> (  ASTF dom (Internal a)--- >          -> ASTF dom (Internal b)--- >          -> ...--- >          -> ASTF dom (Internal x)--- >          )------ ...and vice versa for 'sugarN'.-class SyntacticN a internal | a -> internal-  where-    desugarN :: a -> internal-    sugarN   :: internal -> a--instance (Syntactic a dom, ia ~ AST dom (Full (Internal a))) => SyntacticN a ia-  where-    desugarN = desugar-    sugarN   = sugar--instance-    ( Syntactic a dom-    , ia ~ Internal a-    , SyntacticN b ib-    ) =>-      SyntacticN (a -> b) (AST dom (Full ia) -> ib)-  where-    desugarN f = desugarN . f . sugar-    sugarN f   = sugarN . f . desugar------ | \"Sugared\" symbol application------ 'sugarSym' has any type of the form:------ > sugarSym ::--- >     ( expr :<: AST dom--- >     , Syntactic a dom--- >     , Syntactic b dom--- >     , ...--- >     , Syntactic x dom--- >     ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))--- >       -> (a -> b -> ... -> x)-sugarSym :: (sym :<: AST dom, ApplySym sig b dom, SyntacticN c b) =>-    sym sig -> c-sugarSym = sugarN . appSym---- | \"Sugared\" symbol application------ 'sugarSymC' has any type of the form:------ > sugarSymC ::--- >     ( InjectC expr (AST dom) (Internal x)--- >     , Syntactic a dom--- >     , Syntactic b dom--- >     , ...--- >     , Syntactic x dom--- >     ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))--- >       -> (a -> b -> ... -> x)-sugarSymC-    :: ( InjectC sym (AST dom) (DenResult sig)-       , ApplySym sig b dom-       , SyntacticN c b-       )-    => sym sig -> c-sugarSymC = sugarN . appSymC-
− Language/Syntactic/Syntax.hs 
@@ -1,157 +0,0 @@-{-# LANGUAGE OverlappingInstances #-}-{-# LANGUAGE UndecidableInstances #-}---- | Generic representation of typed syntax trees------ For details, see: A Generic Abstract Syntax Model for Embedded Languages--- (ICFP 2012, <http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf>).--module Language.Syntactic.Syntax-    ( -- * Syntax trees-      AST (..)-    , ASTF-    , Full (..)-    , (:->) (..)-    , size-    , ApplySym (..)-    , DenResult-      -- * Symbol domains-    , (:+:) (..)-    , Project (..)-    , (:<:) (..)-    , appSym-    ) where----import Data.Typeable--------------------------------------------------------------------------------------- * Syntax trees------------------------------------------------------------------------------------- | Generic abstract syntax tree, parameterized by a symbol domain------ @(`AST` dom (a `:->` b))@ represents a partially applied (or unapplied)--- symbol, missing at least one argument, while @(`AST` dom (`Full` a))@--- represents a fully applied symbol, i.e. a complete syntax tree.-data AST dom sig-  where-    Sym  :: dom sig -> AST dom sig-    (:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig--infixl 1 :$---- | Fully applied abstract syntax tree-type ASTF dom a = AST dom (Full a)---- | Signature of a fully applied symbol-newtype Full a = Full { result :: a }-  deriving (Eq, Show, Typeable)---- | Signature of a partially applied (or unapplied) symbol-newtype a :-> sig = Partial (a -> sig)-  deriving (Typeable)--infixr :->---- | Count the number of symbols in an expression-size :: AST dom sig -> Int-size (Sym _)  = 1-size (s :$ a) = size s + size a---- | Class for the type-level recursion needed by 'appSym'-class ApplySym sig f dom | sig dom -> f, f -> sig dom-  where-    appSym' :: AST dom sig -> f--instance ApplySym (Full a) (ASTF dom a) dom-  where-    appSym' = id--instance ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom-  where-    appSym' sym a = appSym' (sym :$ a)---- | The result type of a symbol with the given signature-type family   DenResult sig-type instance DenResult (Full a)    = a-type instance DenResult (a :-> sig) = DenResult sig--------------------------------------------------------------------------------------- * Symbol domains------------------------------------------------------------------------------------- | Direct sum of two symbol domains-data (dom1 :+: dom2) a-  where-    InjL :: dom1 a -> (dom1 :+: dom2) a-    InjR :: dom2 a -> (dom1 :+: dom2) a--infixr :+:---- | Symbol projection-class Project sub sup-  where-    -- | Partial projection from @sup@ to @sub@-    prj :: sup a -> Maybe (sub a)--instance Project sub sup => Project sub (AST sup)-  where-    prj (Sym a) = prj a-    prj _       = Nothing--instance Project expr expr-  where-    prj = Just--instance Project expr1 (expr1 :+: expr2)-  where-    prj (InjL a) = Just a-    prj _        = Nothing--instance Project expr1 expr3 => Project expr1 (expr2 :+: expr3)-  where-    prj (InjR a) = prj a-    prj _        = Nothing---- | Symbol subsumption-class Project sub sup => sub :<: sup-  where-    -- | Injection from @sub@ to @sup@-    inj :: sub a -> sup a--instance (sub :<: sup) => (sub :<: AST sup)-  where-    inj = Sym . inj--instance (expr :<: expr)-  where-    inj = id--instance (expr1 :<: (expr1 :+: expr2))-  where-    inj = InjL--instance (expr1 :<: expr3) => (expr1 :<: (expr2 :+: expr3))-  where-    inj = InjR . inj---- The reason for separating the `Project` and `(:<:)` classes is that there are--- types that can be instances of the former but not the latter due to type--- constraints on the `a` type.---- | Generic symbol application------ 'appSym' has any type of the form:------ > appSym :: (expr :<: AST dom)--- >     => expr (a :-> b :-> ... :-> Full x)--- >     -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)-appSym :: (ApplySym sig f dom, sym :<: AST dom) => sym sig -> f-appSym = appSym' . inj-
− Language/Syntactic/Traversal.hs 
@@ -1,183 +0,0 @@--- | Generic traversals of 'AST' terms--module Language.Syntactic.Traversal-    ( gmapQ-    , gmapT-    , everywhereUp-    , everywhereDown-    , Args (..)-    , listArgs-    , mapArgs-    , mapArgsA-    , mapArgsM-    , appArgs-    , listFold-    , match-    , query-    , simpleMatch-    , fold-    , simpleFold-    , matchTrans-    , WrapFull (..)-    ) where----import Control.Applicative--import Language.Syntactic.Syntax------ | Map a function over all immediate sub-terms (corresponds to the function--- with the same name in Scrap Your Boilerplate)-gmapT :: forall dom-      .  (forall a . ASTF dom a -> ASTF dom a)-      -> (forall a . ASTF dom a -> ASTF dom a)-gmapT f a = go a-  where-    go :: forall a . AST dom a -> AST dom a-    go (s :$ a) = go s :$ f a-    go s        = s---- | Map a function over all immediate sub-terms, collecting the results in a--- list (corresponds to the function with the same name in Scrap Your--- Boilerplate)-gmapQ :: forall dom b-      .  (forall a . ASTF dom a -> b)-      -> (forall a . ASTF dom a -> [b])-gmapQ f a = go a-  where-    go :: forall a . AST dom a -> [b]-    go (s :$ a) = f a : go s-    go _        = []---- | Apply a transformation bottom-up over an expression (corresponds to--- @everywhere@ in Scrap Your Boilerplate)-everywhereUp-    :: (forall a . ASTF dom a -> ASTF dom a)-    -> (forall a . ASTF dom a -> ASTF dom a)-everywhereUp f = f . gmapT (everywhereUp f)---- | Apply a transformation top-down over an expression (corresponds to--- @everywhere'@ in Scrap Your Boilerplate)-everywhereDown-    :: (forall a . ASTF dom a -> ASTF dom a)-    -> (forall a . ASTF dom a -> ASTF dom a)-everywhereDown f = gmapT (everywhereDown f) . f---- | List of symbol arguments-data Args c sig-  where-    Nil  :: Args c (Full a)-    (:*) :: c (Full a) -> Args c sig -> Args c (a :-> sig)--infixr :*---- | Map a function over an 'Args' list and collect the results in an ordinary--- list-listArgs :: (forall a . c (Full a) -> b) -> Args c sig -> [b]-listArgs f Nil       = []-listArgs f (a :* as) = f a : listArgs f as---- | Map a function over an 'Args' list-mapArgs-    :: (forall a   . c1 (Full a) -> c2 (Full a))-    -> (forall sig . Args c1 sig -> Args c2 sig)-mapArgs f Nil       = Nil-mapArgs f (a :* as) = f a :* mapArgs f as---- | Map an applicative function over an 'Args' list-mapArgsA :: Applicative f-    => (forall a   . c1 (Full a) -> f (c2 (Full a)))-    -> (forall sig . Args c1 sig -> f (Args c2 sig))-mapArgsA f Nil       = pure Nil-mapArgsA f (a :* as) = (:*) <$> f a <*> mapArgsA f as---- | Map a monadic function over an 'Args' list-mapArgsM :: Monad m-    => (forall a   . c1 (Full a) -> m (c2 (Full a)))-    -> (forall sig . Args c1 sig -> m (Args c2 sig))-mapArgsM f = unwrapMonad . mapArgsA (WrapMonad . f)---- | Apply a (partially applied) symbol to a list of argument terms-appArgs :: AST dom sig -> Args (AST dom) sig -> ASTF dom (DenResult sig)-appArgs a Nil       = a-appArgs s (a :* as) = appArgs (s :$ a) as---- | \"Pattern match\" on an 'AST' using a function that gets direct access to--- the top-most symbol and its sub-trees-match :: forall dom a c-    .  ( forall sig . (a ~ DenResult sig) =>-           dom sig -> Args (AST dom) sig -> c (Full a)-       )-    -> ASTF dom a-    -> c (Full a)-match f a = go a Nil-  where-    go :: (a ~ DenResult sig) => AST dom sig -> Args (AST dom) sig -> c (Full a)-    go (Sym a)  as = f a as-    go (s :$ a) as = go s (a :* as)--query :: forall dom a c-    .  ( forall sig . (a ~ DenResult sig) =>-           dom sig -> Args (AST dom) sig -> c (Full a)-       )-    -> ASTF dom a-    -> c (Full a)-query = match-{-# DEPRECATED query "Please use `match` instead." #-}---- | A version of 'match' with a simpler result type-simpleMatch :: forall dom a b-    .  (forall sig . (a ~ DenResult sig) => dom sig -> Args (AST dom) sig -> b)-    -> ASTF dom a-    -> b-simpleMatch f = getConst . match (\s -> Const . f s)---- | Fold an 'AST' using an 'Args' list to hold the results of sub-terms-fold :: forall dom c-    .  (forall sig . dom sig -> Args c sig -> c (Full (DenResult sig)))-    -> (forall a   . ASTF dom a -> c (Full a))-fold f = match (\s -> f s . mapArgs (fold f))---- | Simplified version of 'fold' for situations where all intermediate results--- have the same type-simpleFold :: forall dom b-    .  (forall sig . dom sig -> Args (Const b) sig -> b)-    -> (forall a   . ASTF dom a                    -> b)-simpleFold f = getConst . fold (\s -> Const . f s)---- | Fold an 'AST' using a list to hold the results of sub-terms-listFold :: forall dom b-    .  (forall sig . dom sig -> [b] -> b)-    -> (forall a   . ASTF dom a     -> b)-listFold f = simpleFold (\s -> f s . listArgs getConst)--newtype WrapAST c dom sig = WrapAST { unWrapAST :: c (AST dom sig) }-  -- Only used in the definition of 'matchTrans'---- | A version of 'match' where the result is a transformed syntax tree,--- wrapped in a type constructor @c@-matchTrans :: forall dom dom' c a-    .  ( forall sig . (a ~ DenResult sig) =>-           dom sig -> Args (AST dom) sig -> c (ASTF dom' a)-       )-    -> ASTF dom a-    -> c (ASTF dom' a)-matchTrans f = unWrapAST . match (\s -> WrapAST . f s)---- | Can be used to make an arbitrary type constructor indexed by @(`Full` a)@.--- This is useful as the type constructor parameter of 'Args'. That is, use------ > Args (WrapFull c) ...------ instead of------ > Args c ...------ if @c@ is not indexed by @(`Full` a)@.-data WrapFull c a-  where-    WrapFull :: { unwrapFull :: c a } -> WrapFull c (Full a)-
+ examples/NanoFeldspar/Core.hs view
@@ -0,0 +1,262 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++-- | A minimal Feldspar core language implementation. The intention of this+-- module is to demonstrate how to quickly make a language prototype using+-- syntactic.+--+-- A more realistic implementation would use custom contexts to restrict the+-- types at which constructors operate. Currently, all general constructs (such+-- as 'Literal' and 'Tuple') use a 'SimpleCtx' context, which means that the+-- types are quite unrestricted. A real implementation would also probably use+-- custom types for primitive functions, since 'Construct' is quite unsafe (uses+-- only a 'String' to distinguish between functions).++module NanoFeldspar.Core where++++import Data.Typeable++import Language.Syntactic as Syntactic+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Construct+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Tuple+import Language.Syntactic.Frontend.Tuple+import Language.Syntactic.Sharing.SimpleCodeMotion++++--------------------------------------------------------------------------------+-- * Types+--------------------------------------------------------------------------------++-- | Convenient class alias+class    (Ord a, Show a, Typeable a) => Type a+instance (Ord a, Show a, Typeable a) => Type a++type Length = Int+type Index  = Int++++--------------------------------------------------------------------------------+-- * Parallel arrays+--------------------------------------------------------------------------------++data Parallel a+  where+    Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a])++instance Constrained Parallel+  where+    type Sat Parallel = Type+    exprDict Parallel = Dict++instance Semantic Parallel+  where+    semantics Parallel = Sem+        { semanticName = "parallel"+        , semanticEval = \len ixf -> map ixf [0 .. len-1]+        }++instance Equality Parallel where equal = equalDefault; exprHash = exprHashDefault+instance Render   Parallel where renderArgs = renderArgsDefault+instance Eval     Parallel where evaluate   = evaluateDefault+instance ToTree   Parallel+instance EvalBind Parallel where evalBindSym = evalBindSymDefault++instance AlphaEq dom dom dom env => AlphaEq Parallel Parallel dom env+  where+    alphaEqSym = alphaEqSymDefault++++--------------------------------------------------------------------------------+-- * For loops+--------------------------------------------------------------------------------++data ForLoop a+  where+    ForLoop :: Type st =>+        ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)++instance Constrained ForLoop+  where+    type Sat ForLoop = Type+    exprDict ForLoop = Dict++instance Semantic ForLoop+  where+    semantics ForLoop = Sem+        { semanticName = "forLoop"+        , semanticEval = \len init body -> foldl (flip body) init [0 .. len-1]+        }+++instance Equality ForLoop where equal = equalDefault; exprHash = exprHashDefault+instance Render   ForLoop where renderArgs = renderArgsDefault+instance Eval     ForLoop where evaluate   = evaluateDefault+instance ToTree   ForLoop+instance EvalBind ForLoop where evalBindSym = evalBindSymDefault++instance AlphaEq dom dom dom env => AlphaEq ForLoop ForLoop dom env+  where+    alphaEqSym = alphaEqSymDefault++++--------------------------------------------------------------------------------+-- * Feldspar domain+--------------------------------------------------------------------------------++-- | The Feldspar domain+type FeldDomain+    =   Construct+    :+: Literal+    :+: Condition+    :+: Tuple+    :+: Select+    :+: Parallel+    :+: ForLoop++type FeldSyms      = Let :+: (FeldDomain :|| Eq :| Show)+type FeldDomainAll = HODomain FeldSyms Typeable Top++newtype Data a = Data { unData :: ASTF FeldDomainAll a }++-- | Declaring 'Data' as syntactic sugar+instance Type a => Syntactic (Data a) FeldDomainAll+  where+    type Internal (Data a) = a+    desugar = unData+    sugar   = Data++-- | Specialization of the 'Syntactic' class for the Feldspar domain+class    (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a+instance (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a++-- | A predicate deciding which constructs can be shared. Variables, lambdas and literals are not+-- shared.+canShare :: ASTF (FODomain FeldSyms Typeable Top) a -> Maybe (Dict (Top a))+canShare (prjP (P::P (Variable :|| Top)) -> Just _) = Nothing+canShare (prjP (P::P (CLambda Top))      -> Just _) = Nothing+canShare (prj -> Just (Literal _)) = Nothing+canShare _  = Just Dict++canShareDict :: MkInjDict (FODomain FeldSyms Typeable Top)+canShareDict = mkInjDictFO canShare++++--------------------------------------------------------------------------------+-- * Back ends+--------------------------------------------------------------------------------++-- | Show the expression+showExpr :: Syntactic a FeldDomainAll => a -> String+showExpr = render . reifySmart canShareDict++-- | Print the expression+printExpr :: Syntactic a FeldDomainAll => a -> IO ()+printExpr = Syntactic.printExpr . reifySmart canShareDict++-- | Draw the syntax tree using ASCII+showAST :: Syntactic a FeldDomainAll => a -> String+showAST = Syntactic.showAST . reifySmart canShareDict++-- | Draw the syntax tree on the terminal using ASCII+drawAST :: Syntactic a FeldDomainAll => a -> IO ()+drawAST = Syntactic.drawAST . reifySmart canShareDict++-- | Evaluation+eval :: Syntactic a FeldDomainAll => a -> Internal a+eval = evalBind . reifySmart canShareDict++++--------------------------------------------------------------------------------+-- * Core library+--------------------------------------------------------------------------------++-- | Literal+value :: Syntax a => Internal a -> a+value = sugarSymC . Literal++false :: Data Bool+false = value False++true :: Data Bool+true = value True++-- | For types containing some kind of \"thunk\", this function can be used to+-- force computation+force :: Syntax a => a -> a+force = resugar++-- | Share a value using let binding+share :: (Syntax a, Syntax b) => a -> (a -> b) -> b+share = sugarSymC Let++-- | Alpha equivalence+instance Type a => Eq (Data a)+  where+    Data a == Data b = alphaEq (reify a) (reify b)++instance Type a => Show (Data a)+  where+    show (Data a) = render $ reify a++instance (Type a, Num a) => Num (Data a)+  where+    fromInteger = value . fromInteger+    abs         = sugarSymC $ Construct "abs" abs+    signum      = sugarSymC $ Construct "signum" signum+    (+)         = sugarSymC $ Construct "(+)" (+)+    (-)         = sugarSymC $ Construct "(-)" (-)+    (*)         = sugarSymC $ Construct "(*)" (*)++(?) :: Syntax a => Data Bool -> (a,a) -> a+cond ? (t,e) = sugarSymC Condition cond t e++-- | Parallel array+parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]+parallel = sugarSymC Parallel++forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st+forLoop = sugarSymC ForLoop++arrLength :: Type a => Data [a] -> Data Length+arrLength = sugarSymC $ Construct "arrLength" Prelude.length++-- | Array indexing+getIx :: Type a => Data [a] -> Data Index -> Data a+getIx = sugarSymC $ Construct "getIx" eval+  where+    eval as i+        | i >= len || i < 0 = error "getIx: index out of bounds"+        | otherwise         = as !! i+      where+        len = Prelude.length as++not :: Data Bool -> Data Bool+not = sugarSymC $ Construct "not" Prelude.not++(==) :: Type a => Data a -> Data a -> Data Bool+(==) = sugarSymC $ Construct "(==)" (Prelude.==)++max :: Type a => Data a -> Data a -> Data a+max = sugarSymC $ Construct "max" Prelude.max++min :: Type a => Data a -> Data a -> Data a+min = sugarSymC $ Construct "min" Prelude.min+
+ examples/NanoFeldspar/Extra.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++module NanoFeldspar.Extra where++++import Data.Typeable++import Language.Syntactic as Syntactic+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Constructs.Binding.Optimize+import Language.Syntactic.Constructs.Construct+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Sharing.Graph+import Language.Syntactic.Sharing.ReifyHO++import NanoFeldspar.Core++++--------------------------------------------------------------------------------+-- * Graph reification+--------------------------------------------------------------------------------++-- | A predicate deciding which constructs can be shared. Variables, lambdas and literals are not+-- shared.+canShare2 :: ASTF (HODomain FeldSyms Typeable Top) a -> Bool+canShare2 (prjP (P::P (Variable :|| Top))               -> Just _) = False+canShare2 (prjP (P::P (HOLambda FeldSyms Typeable Top)) -> Just _) = False+canShare2 (prj -> Just (Literal _)) = False+canShare2 _  = True++-- | Draw the syntax graph after common sub-expression elimination+drawCSE :: Syntactic a FeldDomainAll => a -> IO ()+drawCSE a = do+    (g,_) <- reifyGraph canShare2 a+    drawASG+      $ reindexNodesFrom0+      $ inlineSingle+      $ cse+      $ g++-- | Draw the syntax graph after observing sharing+drawObs :: Syntactic a FeldDomainAll => a -> IO ()+drawObs a = do+    (g,_) <- reifyGraph canShare2 a+    drawASG+      $ reindexNodesFrom0+      $ inlineSingle+      $ g++++--------------------------------------------------------------------------------+-- * Partial evaluation+--------------------------------------------------------------------------------++instance Optimize ForLoop+  where+    optimizeSym = optimizeSymDefault++instance Optimize Parallel+  where+    optimizeSym = optimizeSymDefault++constFold :: forall a+    .  ASTF ((FODomain (Let :+: (FeldDomain :|| Eq :| Show))) Typeable Top) a+    -> a+    -> ASTF ((FODomain (Let :+: (FeldDomain :|| Eq :| Show))) Typeable Top) a+constFold expr a = match (\sym _ -> case sym of+      C' (InjR (InjR (InjR (C (C' _))))) -> injC (Literal a)+      _ -> expr+    ) expr++drawPart :: Syntactic a FeldDomainAll => a -> IO ()+drawPart = Syntactic.drawAST . optimize constFold . reify+
+ examples/NanoFeldspar/Test.hs view
@@ -0,0 +1,85 @@+module NanoFeldspar.Test where++++import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith)++import NanoFeldspar.Core+import NanoFeldspar.Extra+import NanoFeldspar.Vector++++--------------------------------------------------------------------------------+-- Basic operations+--------------------------------------------------------------------------------++-- Parallel arrays+prog1 :: Data Int -> Data Int -> Data [Int]+prog1 a b = parallel a (\i -> min (i+3) b)++-- Evaluation+test1_1 = eval prog1 10 20++-- Print the expression+test1_2 = printExpr prog1++-- Render the syntax tree+test1_3 = drawAST prog1++-- Common sub-expressions+prog2 :: Data Int -> Data Int+prog2 a = max (min a a) (min a a)++-- Basic vector operations+prog3 :: Data Index -> Data Index -> Data Index+prog3 a b = sum $ reverse (l ... u)+  where+    l = min a b+    u = max a b++-- Explicit sharing+prog4 :: Data Index -> Data Index+prog4 a = share (a*2,a*3) $ \(b,c) -> (b-c)*(c-b)++++--------------------------------------------------------------------------------+-- Common sub-expression elimination and observable sharing+--------------------------------------------------------------------------------++prog5 = index as 1 + sum as + sum as+  where+    as = map (*2) $ force (1...20)++test5_1 = drawAST prog5+  -- Draws a tree with no duplication++test5_2 = drawCSE prog5+  -- Draws a graph with no duplication++test5_3 = drawObs prog5+  -- Draws a graph with some duplication. The 'forLoop' introduced by 'sum' is+  -- not shared, because 'sum as' is repeated twice in source code. But the+  -- 'parallel' introduced by 'force' is shared, because 'force' only appears+  -- once.++++--------------------------------------------------------------------------------+-- Optimizations+--------------------------------------------------------------------------------++prog6 :: Data Int -> Data Int+prog6 a = (a==10) ? (max 5 (6+7), max 5 (6+7))++test6 = drawPart prog6+  -- Reduced to the literal 13++prog7 a = c ? (parallel 10 (+a), parallel 10 (+a))+  where+    c = (a*a*a*a) == 23++test7 = drawPart prog7+  -- The condition gets pruned away+
+ examples/NanoFeldspar/Vector.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}++-- | A simple vector library for NanoFeldspar. The intention of this module is+-- to demonstrate how to add language features without extending the underlying+-- core language. By declaring 'Vector' as syntactic sugar, vector operations+-- can work seamlessly with the functions of the core language.+--+-- An interesting aspect of the 'Vector' interface is that the only operation+-- that produces a core language array (i.e. allocates memory) is 'freezeVector'+-- (which uses 'parallel'). This means that expressions not involving+-- 'freezeVector' are guaranteed to be fused. (Note, however, that+-- 'freezeVector' is introduced by 'desugar', which in turn is used by many+-- other functions.)++module NanoFeldspar.Vector where++++import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith)++import Language.Syntactic (Syntactic (..), resugar)++import NanoFeldspar.Core++++data Vector a+  where+    Indexed :: Data Length -> (Data Index -> a) -> Vector a++instance Syntax a => Syntactic (Vector a) FeldDomainAll+  where+    type Internal (Vector a) = [Internal a]+    desugar = desugar . freezeVector . map resugar+    sugar   = map resugar . unfreezeVector . sugar++++length :: Vector a -> Data Length+length (Indexed len _) = len++indexed :: Data Length -> (Data Index -> a) -> Vector a+indexed = Indexed++index :: Vector a -> Data Index -> a+index (Indexed _ ixf) = ixf++freezeVector :: Type a => Vector (Data a) -> Data [a]+freezeVector vec = parallel (length vec) (index vec)++unfreezeVector :: Type a => Data [a] -> Vector (Data a)+unfreezeVector arr = Indexed (arrLength arr) (getIx arr)++zip :: Vector a -> Vector b -> Vector (a,b)+zip a b = indexed (length a `min` length b) (\i -> (index a i, index b i))++unzip :: Vector (a,b) -> (Vector a, Vector b)+unzip ab = (indexed len (fst . index ab), indexed len (snd . index ab))+  where+    len = length ab++permute :: (Data Length -> Data Index -> Data Index) -> (Vector a -> Vector a)+permute perm vec = indexed len (index vec . perm len)+  where+    len = length vec++reverse :: Vector a -> Vector a+reverse = permute $ \len i -> len-i-1++(...) :: Data Index -> Data Index -> Vector (Data Index)+l ... h = indexed (h-l+1) (+l)++map :: (a -> b) -> Vector a -> Vector b+map f (Indexed len ixf) = Indexed len (f . ixf)++zipWith :: (a -> b -> c) -> Vector a -> Vector b -> Vector c+zipWith f a b = map (uncurry f) $ zip a b++fold :: Syntax b => (a -> b -> b) -> b -> Vector a -> b+fold f b (Indexed len ixf) = forLoop len b (\i st -> f (ixf i) st)++sum :: (Type a, Num a) => Vector (Data a) -> Data a+sum = fold (+) 0+
+ src/Data/DynamicAlt.hs view
@@ -0,0 +1,28 @@+-- | An alternative to "Data.Dynamic" with a different constraint on 'toDyn'++module Data.DynamicAlt where++++import Data.Dynamic ()+import Data.Typeable+import GHC.Prim+import Unsafe.Coerce++import Data.PolyProxy++++data Dynamic = Dynamic TypeRep Any++toDyn :: forall a b . Typeable (a -> b) => P (a -> b) -> a -> Dynamic+toDyn _ a = case splitTyConApp $ typeOf (undefined :: a -> b) of+    (_,[ta,_]) -> Dynamic ta (unsafeCoerce a)++fromDyn :: Typeable a => Dynamic -> Maybe a+fromDyn (Dynamic t a)+    | b <- unsafeCoerce a+    , t == typeOf b+    = Just b+fromDyn _ = Nothing+
+ src/Data/PolyProxy.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE PolyKinds #-}++-- TODO PolyKinds can be enabled globally in GHC 7.6. In 7.4, additional annotations are needed.++module Data.PolyProxy where++++-- | Kind-polymorphic proxy type+data P a where P :: P a+  -- Using one letter to remove line noise+
+ src/Language/Syntactic.hs view
@@ -0,0 +1,29 @@+-- | The basic parts of the syntactic library++module Language.Syntactic+    ( module Data.PolyProxy+    , module Language.Syntactic.Syntax+    , module Language.Syntactic.Traversal+    , module Language.Syntactic.Constraint+    , module Language.Syntactic.Sugar+    , module Language.Syntactic.Interpretation.Equality+    , module Language.Syntactic.Interpretation.Render+    , module Language.Syntactic.Interpretation.Evaluation+    , module Language.Syntactic.Interpretation.Semantics+    , module Data.Constraint+    ) where++++import Data.PolyProxy+import Language.Syntactic.Syntax+import Language.Syntactic.Traversal+import Language.Syntactic.Constraint+import Language.Syntactic.Sugar+import Language.Syntactic.Interpretation.Equality+import Language.Syntactic.Interpretation.Render+import Language.Syntactic.Interpretation.Evaluation+import Language.Syntactic.Interpretation.Semantics++import Data.Constraint (Constraint, Dict (..))+
+ src/Language/Syntactic/Constraint.hs view
@@ -0,0 +1,382 @@+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- TODO Only `InjectC` should be used overlapped. Move to separate module?++-- | Type-constrained syntax trees++module Language.Syntactic.Constraint where++++import Data.Typeable++import Data.Constraint++import Data.PolyProxy+import Language.Syntactic.Syntax+import Language.Syntactic.Interpretation.Equality+import Language.Syntactic.Interpretation.Render+import Language.Syntactic.Interpretation.Evaluation++++--------------------------------------------------------------------------------+-- * Type predicates+--------------------------------------------------------------------------------++-- | Intersection of type predicates+class    (c1 a, c2 a) => (c1 :/\: c2) a+instance (c1 a, c2 a) => (c1 :/\: c2) a++infixr 5 :/\:++-- | Universal type predicate+class    Top a+instance Top a++pTop :: P Top+pTop = P++pTypeable :: P Typeable+pTypeable = P++-- | Evidence that the predicate @sub@ is a subset of @sup@+type Sub sub sup = forall a . Dict (sub a) -> Dict (sup a)++-- | Weaken an intersection+weakL :: Sub (c1 :/\: c2) c1+weakL Dict = Dict++-- | Weaken an intersection+weakR :: Sub (c1 :/\: c2) c2+weakR Dict = Dict++-- | Subset relation on type predicates+class (sub :: * -> Constraint) :< (sup :: * -> Constraint)+  where+    -- | Compute evidence that @sub@ is a subset of @sup@ (i.e. that @(sup a)@+    -- implies @(sub a)@)+    sub :: Sub sub sup++instance p :< p+  where+    sub = id++instance (p :/\: ps) :< p+  where+    sub = weakL++instance (ps :< q) => ((p :/\: ps) :< q)+  where+    sub = sub . weakR++++--------------------------------------------------------------------------------+-- * Constrained syntax+--------------------------------------------------------------------------------++-- | Constrain the result type of the expression by the given predicate+data (:|) :: (* -> *) -> (* -> Constraint) -> (* -> *)+  where+    C :: pred (DenResult sig) => expr sig -> (expr :| pred) sig++infixl 4 :|++instance Project sub sup => Project sub (sup :| pred)+  where+    prj (C s) = prj s++instance Equality dom => Equality (dom :| pred)+  where+    equal (C a) (C b) = equal a b+    exprHash (C a)    = exprHash a++instance Render dom => Render (dom :| pred)+  where+    renderArgs args (C a) = renderArgs args a++instance Eval dom => Eval (dom :| pred)+  where+    evaluate (C a) = evaluate a++instance ToTree dom => ToTree (dom :| pred)+  where+    toTreeArgs args (C a) = toTreeArgs args a++++-- | Constrain the result type of the expression by the given predicate+--+-- The difference between ':||' and ':|' is seen in the instances of the 'Sat'+-- type:+--+-- > type Sat (dom :|  pred) = pred :/\: Sat dom+-- > type Sat (dom :|| pred) = pred+data (:||) :: (* -> *) -> (* -> Constraint) -> (* -> *)+  where+    C' :: pred (DenResult sig) => expr sig -> (expr :|| pred) sig++infixl 4 :||++instance Project sub sup => Project sub (sup :|| pred)+  where+    prj (C' s) = prj s++instance Equality dom => Equality (dom :|| pred)+  where+    equal (C' a) (C' b) = equal a b+    exprHash (C' a)     = exprHash a++instance Render dom => Render (dom :|| pred)+  where+    renderArgs args (C' a) = renderArgs args a++instance Eval dom => Eval (dom :|| pred)+  where+    evaluate (C' a) = evaluate a++instance ToTree dom => ToTree (dom :|| pred)+  where+    toTreeArgs args (C' a) = toTreeArgs args a++++-- | Expressions that constrain their result types+class Constrained expr+  where+    -- | Returns a predicate that is satisfied by the result type of all+    -- expressions of the given type (see 'exprDict').+    type Sat expr :: * -> Constraint++    -- | Compute a constraint on the result type of an expression+    exprDict :: expr a -> Dict (Sat expr (DenResult a))++instance Constrained dom => Constrained (AST dom)+  where+    type Sat (AST dom) = Sat dom+    exprDict (Sym s)  = exprDict s+    exprDict (s :$ _) = exprDict s++instance Constrained (sub1 :+: sub2)+  where+    -- | An over-approximation of the union of @Sat sub1@ and @Sat sub2@+    type Sat (sub1 :+: sub2) = Top+    exprDict (InjL s) = Dict+    exprDict (InjR s) = Dict++instance Constrained dom => Constrained (dom :| pred)+  where+    type Sat (dom :| pred) = pred :/\: Sat dom+    exprDict (C s) = case exprDict s of Dict -> Dict++instance Constrained (dom :|| pred)+  where+    type Sat (dom :|| pred) = pred+    exprDict (C' s) = Dict++type ConstrainedBy expr p = (Constrained expr, Sat expr :< p)++-- | A version of 'exprDict' that returns a constraint for a particular+-- predicate @p@ as long as @(p :< Sat dom)@ holds+exprDictSub :: ConstrainedBy expr p => P p -> expr a -> Dict (p (DenResult a))+exprDictSub _ = sub . exprDict++-- | A version of 'exprDict' that works for domains of the form+-- @(dom1 :+: dom2)@ as long as @(Sat dom1 ~ Sat dom2)@ holds+exprDictPlus :: (Constrained dom1, Constrained dom2, Sat dom1 ~ Sat dom2) =>+    AST (dom1 :+: dom2) a -> Dict (Sat dom1 (DenResult a))+exprDictPlus (s :$ _)       = exprDictPlus s+exprDictPlus (Sym (InjL a)) = exprDict a+exprDictPlus (Sym (InjR a)) = exprDict a++++-- | Symbol injection (like ':<:') with constrained result types+class (Project sub sup, Sat sup a) => InjectC sub sup a+  where+    injC :: (DenResult sig ~ a) => sub sig -> sup sig++instance InjectC sub sup a => InjectC sub (AST sup) a+  where+    injC = Sym . injC++instance (InjectC sub sup a, pred a) => InjectC sub (sup :| pred) a+  where+    injC = C . injC++instance (InjectC sub sup a, pred a) => InjectC sub (sup :|| pred) a+  where+    injC = C' . injC++instance Sat expr a => InjectC expr expr a+  where+    injC = id++instance InjectC expr1 (expr1 :+: expr2) a+  where+    injC = InjL++instance InjectC expr1 expr3 a => InjectC expr1 (expr2 :+: expr3) a+  where+    injC = InjR . injC++++-- | Generic symbol application+--+-- 'appSymC' has any type of the form:+--+-- > appSymC :: InjectC expr (AST dom) x+-- >     => expr (a :-> b :-> ... :-> Full x)+-- >     -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)+appSymC :: (ApplySym sig f dom, InjectC sym (AST dom) (DenResult sig)) => sym sig -> f+appSymC = appSym' . injC++++-- | Similar to ':||', but rather than constraining the whole result type, it assumes a result+-- type of the form @c a@ and constrains the @a@.+data SubConstr1 :: (* -> *) -> (* -> *) -> (* -> Constraint) -> (* -> *)+  where+    SubConstr1 :: (p a, DenResult sig ~ c a) => dom sig -> SubConstr1 c dom p sig++instance Constrained dom => Constrained (SubConstr1 c dom p)+  where+    type Sat (SubConstr1 c dom p) = Sat dom+    exprDict (SubConstr1 s) = exprDict s++instance Project sub sup => Project sub (SubConstr1 c sup p)+  where+    prj (SubConstr1 s) = prj s++instance Equality dom => Equality (SubConstr1 c dom p)+  where+    equal (SubConstr1 a) (SubConstr1 b) = equal a b+    exprHash (SubConstr1 s) = exprHash s++instance Render dom => Render (SubConstr1 c dom p)+  where+    renderArgs args (SubConstr1 s) = renderArgs args s++instance ToTree dom => ToTree (SubConstr1 c dom p)+  where+    toTreeArgs args (SubConstr1 a) = toTreeArgs args a++instance Eval dom => Eval (SubConstr1 c dom p)+  where+    evaluate (SubConstr1 a) = evaluate a++++-- | Similar to 'SubConstr1', but assumes a result type of the form @c a b@ and constrains both @a@+-- and @b@.+data SubConstr2 :: (* -> * -> *) -> (* -> *) -> (* -> Constraint) -> (* -> Constraint) -> (* -> *)+  where+    SubConstr2 :: (DenResult sig ~ c a b, pa a, pb b) => dom sig -> SubConstr2 c dom pa pb sig++instance Constrained dom => Constrained (SubConstr2 c dom pa pb)+  where+    type Sat (SubConstr2 c dom pa pb) = Sat dom+    exprDict (SubConstr2 s) = exprDict s++instance Project sub sup => Project sub (SubConstr2 c sup pa pb)+  where+    prj (SubConstr2 s) = prj s++instance Equality dom => Equality (SubConstr2 c dom pa pb)+  where+    equal (SubConstr2 a) (SubConstr2 b) = equal a b+    exprHash (SubConstr2 s) = exprHash s++instance Render dom => Render (SubConstr2 c dom pa pb)+  where+    renderArgs args (SubConstr2 s) = renderArgs args s++instance ToTree dom => ToTree (SubConstr2 c dom pa pb)+  where+    toTreeArgs args (SubConstr2 a) = toTreeArgs args a++instance Eval dom => Eval (SubConstr2 c dom pa pb)+  where+    evaluate (SubConstr2 a) = evaluate a++++--------------------------------------------------------------------------------+-- * Existential quantification+--------------------------------------------------------------------------------++-- | 'AST' with existentially quantified result type+data ASTE :: (* -> *) -> *+  where+    ASTE :: ASTF dom a -> ASTE dom++liftASTE+    :: (forall a . ASTF dom a -> b)+    -> ASTE dom+    -> b+liftASTE f (ASTE a) = f a++liftASTE2+    :: (forall a b . ASTF dom a -> ASTF dom b -> c)+    -> ASTE dom -> ASTE dom -> c+liftASTE2 f (ASTE a) (ASTE b) = f a b++++-- | 'AST' with bounded existentially quantified result type+data ASTB :: (* -> *) -> (* -> Constraint) -> *+  where+    ASTB :: p a => ASTF dom a -> ASTB dom p++liftASTB+    :: (forall a . p a => ASTF dom a -> b)+    -> ASTB dom p+    -> b+liftASTB f (ASTB a) = f a++liftASTB2+    :: (forall a b . (p a, p b) => ASTF dom a -> ASTF dom b -> c)+    -> ASTB dom p -> ASTB dom p -> c+liftASTB2 f (ASTB a) (ASTB b) = f a b++type ASTSAT dom = ASTB dom (Sat dom)++++--------------------------------------------------------------------------------+-- * Misc.+--------------------------------------------------------------------------------++-- | Empty symbol type+--+-- Use-case:+--+-- > data A a+-- > data B a+-- >+-- > test :: AST (A :+: (B:||Eq) :+: Empty) a+-- > test = injC (undefined :: (B :|| Eq) a)+--+-- Without 'Empty', this would lead to an overlapping instance error due to the instances+--+-- > InjectC (B :|| Eq) (B :|| Eq) (DenResult a)+--+-- and+--+-- > InjectC sub sup a, pred a) => InjectC sub (sup :|| pred) a+data Empty :: * -> *++instance Constrained Empty+  where+    type Sat Empty = Top+    exprDict = error "Not implemented: exprDict for Empty"++instance Equality Empty where equal      = error "Not implemented: equal for Empty"+                              exprHash   = error "Not implemented: exprHash for Empty"+instance Eval     Empty where evaluate   = error "Not implemented: equal for Empty"+instance Render   Empty where renderArgs = error "Not implemented: renderArgs for Empty"+instance ToTree   Empty+
+ src/Language/Syntactic/Constructs/Binding.hs view
@@ -0,0 +1,425 @@+{-# LANGUAGE UndecidableInstances #-}++-- | General binding constructs++module Language.Syntactic.Constructs.Binding where++++import qualified Control.Monad.Identity as Monad+import Control.Monad.Reader+import Data.Ix+import Data.Tree+import Data.Typeable++import Data.Hash++import Data.PolyProxy+import Data.DynamicAlt+import Language.Syntactic+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Construct+import Language.Syntactic.Constructs.Decoration+import Language.Syntactic.Constructs.Identity+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Monad+import Language.Syntactic.Constructs.Tuple++++--------------------------------------------------------------------------------+-- * Variables+--------------------------------------------------------------------------------++-- | Variable identifier+newtype VarId = VarId { varInteger :: Integer }+  deriving (Eq, Ord, Num, Real, Integral, Enum, Ix)++instance Show VarId+  where+    show (VarId i) = show i++showVar :: VarId -> String+showVar v = "var" ++ show v++++-- | Variables+data Variable a+  where+    Variable :: VarId -> Variable (Full a)++instance Constrained Variable+  where+    type Sat Variable = Top+    exprDict _ = Dict++-- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.+--+-- 'exprHash' assigns the same hash to all variables. This is a valid+-- over-approximation that enables the following property:+--+-- @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@+instance Equality Variable+  where+    equal (Variable v1) (Variable v2) = v1==v2+    exprHash (Variable _)             = hashInt 0++instance Render Variable+  where+    render (Variable v) = showVar v++instance ToTree Variable+  where+    toTreeArgs [] (Variable v) = Node ("var:" ++ show v) []++++--------------------------------------------------------------------------------+-- * Lambda binding+--------------------------------------------------------------------------------++-- | Lambda binding+data Lambda a+  where+    Lambda :: VarId -> Lambda (b :-> Full (a -> b))++instance Constrained Lambda+  where+    type Sat Lambda = Top+    exprDict _ = Dict++-- | 'equal' does strict identifier comparison; i.e. no alpha equivalence.+--+-- 'exprHash' assigns the same hash to all 'Lambda' bindings. This is a valid+-- over-approximation that enables the following property:+--+-- @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@+instance Equality Lambda+  where+    equal (Lambda v1) (Lambda v2) = v1==v2+    exprHash (Lambda _)           = hashInt 0++instance Render Lambda+  where+    renderArgs [body] (Lambda v) = "(\\" ++ showVar v ++ " -> "  ++ body ++ ")"++instance ToTree Lambda+  where+    toTreeArgs [body] (Lambda v) = Node ("Lambda " ++ show v) [body]++++--------------------------------------------------------------------------------+-- * Let binding+--------------------------------------------------------------------------------++-- | Let binding+--+-- 'Let' is just an application operator with flipped argument order. The argument+-- @(a -> b)@ is preferably constructed by 'Lambda'.+data Let a+  where+    Let :: Let (a :-> (a -> b) :-> Full b)++instance Constrained Let+  where+    type Sat Let = Top+    exprDict _ = Dict++instance Equality Let+  where+    equal Let Let = True+    exprHash Let  = hashInt 0++instance Render Let+  where+    renderArgs []    Let = "Let"+    renderArgs [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")"++instance ToTree Let+  where+    toTreeArgs [a,body] Let = case splitAt 7 node of+        ("Lambda ", var) -> Node ("Let " ++ var) [a,body']+        _                -> Node "Let" [a,body]+      where+        Node node ~[body'] = body+        var                = drop 7 node  -- Drop the "Lambda " prefix++instance Eval Let+  where+    evaluate Let = flip ($)++++--------------------------------------------------------------------------------+-- * Interpretation+--------------------------------------------------------------------------------++-- | Should be a capture-avoiding substitution, but it is currently not correct.+--+-- Note: Variables with a different type than the new expression will be+-- silently ignored.+subst :: forall constr dom a b+    .  ( ConstrainedBy dom Typeable+       , Project Lambda dom+       , Project Variable dom+       )+    => VarId       -- ^ Variable to be substituted+    -> ASTF dom a  -- ^ Expression to substitute for+    -> ASTF dom b  -- ^ Expression to substitute in+    -> ASTF dom b+subst v new a = go a+  where+    go :: AST dom c -> AST dom c+    go a@((prj -> Just (Lambda w)) :$ _)+        | v==w = a  -- Capture+    go (f :$ a) = go f :$ go a+    go var+        | Just (Variable w) <- prj var+        , v==w+        , Dict <- exprDictSub pTypeable new+        , Dict <- exprDictSub pTypeable var+        , Just new' <- gcast new+        = new'+    go a = a+  -- TODO Make it correct (may need to alpha-convert `new` before inserting it)+  -- TODO Should there be an error if `gcast` fails? (See note in Haddock+  --      comment.)++-- | Beta-reduction of an expression. The expression to be reduced is assumed to+-- be a `Lambda`.+betaReduce+    :: ( ConstrainedBy dom Typeable+       , Project Lambda dom+       , Project Variable dom+       )+    => ASTF dom a         -- ^ Argument+    -> ASTF dom (a -> b)  -- ^ Function to be reduced+    -> ASTF dom b+betaReduce new (lam :$ body)+    | Just (Lambda v) <- prj lam = subst v new body++++-- | Evaluation of expressions with variables+class EvalBind sub+  where+    evalBindSym+        :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig))+        => sub sig+        -> Args (AST dom) sig+        -> Reader [(VarId,Dynamic)] (DenResult sig)+  -- `(Typeable (DenResult sig))` is required because this dictionary cannot (in+  -- general) be obtained from `sub`. It can only be obtained from `dom`, and+  -- this is what `evalBindM` does.++instance (EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2)+  where+    evalBindSym (InjL a) = evalBindSym a+    evalBindSym (InjR a) = evalBindSym a++-- | Evaluation of possibly open expressions+evalBindM :: (EvalBind dom, ConstrainedBy dom Typeable) =>+    ASTF dom a -> Reader [(VarId,Dynamic)] a+evalBindM a+    | Dict <- exprDictSub pTypeable a+    = liftM result $ match (\s -> liftM Full . evalBindSym s) a++-- | Evaluation of closed expressions+evalBind :: (EvalBind dom, ConstrainedBy dom Typeable) => ASTF dom a -> a+evalBind = flip runReader [] . evalBindM++-- | Apply a symbol denotation to a list of arguments+appDen :: Denotation sig -> Args Monad.Identity sig -> DenResult sig+appDen a Nil       = a+appDen f (a :* as) = appDen (f $ result $ Monad.runIdentity a) as++-- | Convenient default implementation of 'evalBindSym'+evalBindSymDefault+    :: (Eval sub, EvalBind dom, ConstrainedBy dom Typeable)+    => sub sig+    -> Args (AST dom) sig+    -> Reader [(VarId,Dynamic)] (DenResult sig)+evalBindSymDefault sym args = do+    args' <- mapArgsM (liftM (Monad.Identity . Full) . evalBindM) args+    return $ appDen (evaluate sym) args'++instance EvalBind dom => EvalBind (dom :| pred)+  where+    evalBindSym (C a) = evalBindSym a++instance EvalBind dom => EvalBind (dom :|| pred)+  where+    evalBindSym (C' a) = evalBindSym a++instance EvalBind dom => EvalBind (SubConstr1 c dom p)+  where+    evalBindSym (SubConstr1 a) = evalBindSym a++instance EvalBind dom => EvalBind (SubConstr2 c dom pa pb)+  where+    evalBindSym (SubConstr2 a) = evalBindSym a++instance EvalBind Empty+  where+    evalBindSym = error "Not implemented: evalBindSym for Empty"++instance EvalBind dom => EvalBind (Decor info dom)+  where+    evalBindSym = evalBindSym . decorExpr++instance EvalBind Identity  where evalBindSym = evalBindSymDefault+instance EvalBind Construct where evalBindSym = evalBindSymDefault+instance EvalBind Literal   where evalBindSym = evalBindSymDefault+instance EvalBind Condition where evalBindSym = evalBindSymDefault+instance EvalBind Tuple     where evalBindSym = evalBindSymDefault+instance EvalBind Select    where evalBindSym = evalBindSymDefault+instance EvalBind Let       where evalBindSym = evalBindSymDefault++instance Monad m => EvalBind (MONAD m) where evalBindSym = evalBindSymDefault++instance EvalBind Variable+  where+    evalBindSym (Variable v) Nil = do+        env <- ask+        case lookup v env of+            Nothing -> return $ error "evalBind: evaluating free variable"+            Just a  -> case fromDyn a of+              Just a -> return a+              _      -> return $ error "evalBind: internal type error"++instance EvalBind Lambda+  where+    evalBindSym lam@(Lambda v) (body :* Nil) = do+        env <- ask+        return+            $ \a -> flip runReader ((v, toDyn (funType lam) a):env)+            $ evalBindM body+      where+        funType :: Lambda (b :-> Full (a -> b)) -> P (a -> b)+        funType _ = P++++--------------------------------------------------------------------------------+-- * Alpha equivalence+--------------------------------------------------------------------------------++-- | Environments containing a list of variable equivalences+class VarEqEnv a+  where+    prjVarEqEnv :: a -> [(VarId,VarId)]+    modVarEqEnv :: ([(VarId,VarId)] -> [(VarId,VarId)]) -> (a -> a)++instance VarEqEnv [(VarId,VarId)]+  where+    prjVarEqEnv = id+    modVarEqEnv = id++-- | Alpha-equivalence+class AlphaEq sub1 sub2 dom env+  where+    alphaEqSym+        :: sub1 a+        -> Args (AST dom) a+        -> sub2 b+        -> Args (AST dom) b+        -> Reader env Bool++instance (AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) =>+    AlphaEq (subA1 :+: subA2) (subB1 :+: subB2) dom env+  where+    alphaEqSym (InjL a) aArgs (InjL b) bArgs = alphaEqSym a aArgs b bArgs+    alphaEqSym (InjR a) aArgs (InjR b) bArgs = alphaEqSym a aArgs b bArgs+    alphaEqSym _ _ _ _ = return False++alphaEqM :: AlphaEq dom dom dom env =>+    ASTF dom a -> ASTF dom b -> Reader env Bool+alphaEqM a b = simpleMatch (alphaEqM2 b) a++alphaEqM2 :: AlphaEq dom dom dom env =>+    ASTF dom b -> dom a -> Args (AST dom) a -> Reader env Bool+alphaEqM2 b a aArgs = simpleMatch (alphaEqSym a aArgs) b++-- | Alpha-equivalence on lambda expressions. Free variables are taken to be+-- equivalent if they have the same identifier.+alphaEq :: AlphaEq dom dom dom [(VarId,VarId)] =>+    ASTF dom a -> ASTF dom b -> Bool+alphaEq a b = flip runReader ([] :: [(VarId,VarId)]) $ alphaEqM a b++alphaEqSymDefault :: (Equality sub, AlphaEq dom dom dom env)+    => sub a+    -> Args (AST dom) a+    -> sub b+    -> Args (AST dom) b+    -> Reader env Bool+alphaEqSymDefault a aArgs b bArgs+    | equal a b = alphaEqChildren a' b'+    | otherwise = return False+  where+    a' = appArgs (Sym (undefined :: dom a)) aArgs+    b' = appArgs (Sym (undefined :: dom b)) bArgs++alphaEqChildren :: AlphaEq dom dom dom env =>+    AST dom a -> AST dom b -> Reader env Bool+alphaEqChildren (Sym _)  (Sym _)  = return True+alphaEqChildren (f :$ a) (g :$ b) = liftM2 (&&)+    (alphaEqChildren f g)+    (alphaEqM a b)+alphaEqChildren _ _ = return False++instance AlphaEq sub sub dom env => AlphaEq (sub :| pred) (sub :| pred) dom env+  where+    alphaEqSym (C a) aArgs (C b) bArgs = alphaEqSym a aArgs b bArgs++instance AlphaEq sub sub dom env => AlphaEq (sub :|| pred) (sub :|| pred) dom env+  where+    alphaEqSym (C' a) aArgs (C' b) bArgs = alphaEqSym a aArgs b bArgs++instance AlphaEq sub sub dom env => AlphaEq (SubConstr1 c sub p) (SubConstr1 c sub p) dom env+  where+    alphaEqSym (SubConstr1 a) aArgs (SubConstr1 b) bArgs = alphaEqSym a aArgs b bArgs++instance AlphaEq sub sub dom env =>+    AlphaEq (SubConstr2 c sub pa pb) (SubConstr2 c sub pa pb) dom env+  where+    alphaEqSym (SubConstr2 a) aArgs (SubConstr2 b) bArgs = alphaEqSym a aArgs b bArgs++instance AlphaEq Empty Empty dom env+  where+    alphaEqSym = error "Not implemented: alphaEqSym for Empty"++instance AlphaEq dom dom dom env => AlphaEq Condition Condition dom env where alphaEqSym = alphaEqSymDefault+instance AlphaEq dom dom dom env => AlphaEq Construct Construct dom env where alphaEqSym = alphaEqSymDefault+instance AlphaEq dom dom dom env => AlphaEq Identity  Identity  dom env where alphaEqSym = alphaEqSymDefault+instance AlphaEq dom dom dom env => AlphaEq Let       Let       dom env where alphaEqSym = alphaEqSymDefault+instance AlphaEq dom dom dom env => AlphaEq Literal   Literal   dom env where alphaEqSym = alphaEqSymDefault+instance AlphaEq dom dom dom env => AlphaEq Select    Select    dom env where alphaEqSym = alphaEqSymDefault+instance AlphaEq dom dom dom env => AlphaEq Tuple     Tuple     dom env where alphaEqSym = alphaEqSymDefault++instance AlphaEq sub sub dom env =>+    AlphaEq (Decor info sub) (Decor info sub) dom env+  where+    alphaEqSym a aArgs b bArgs =+        alphaEqSym (decorExpr a) aArgs (decorExpr b) bArgs++instance (AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env+  where+    alphaEqSym = alphaEqSymDefault++instance (AlphaEq dom dom dom env, VarEqEnv env) =>+    AlphaEq Variable Variable dom env+  where+    alphaEqSym (Variable v1) Nil (Variable v2) Nil = do+        env <- asks prjVarEqEnv+        case lookup v1 env of+          Nothing  -> return (v1==v2)   -- Free variables+          Just v2' -> return (v2==v2')++instance (AlphaEq dom dom dom env, VarEqEnv env) =>+    AlphaEq Lambda Lambda dom env+  where+    alphaEqSym (Lambda v1) (body1 :* Nil) (Lambda v2) (body2 :* Nil) =+        local (modVarEqEnv ((v1,v2):)) $ alphaEqM body1 body2+
+ src/Language/Syntactic/Constructs/Binding/HigherOrder.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE UndecidableInstances #-}++-- | This module provides binding constructs using higher-order syntax and a+-- function ('reify') for translating to first-order syntax. Expressions+-- constructed using the exported interface (specifically, not introducing+-- 'Variable's explicitly) are guaranteed to have well-behaved translation.++module Language.Syntactic.Constructs.Binding.HigherOrder+    ( Variable+    , Let (..)+    , HOLambda (..)+    , HODomain+    , FODomain+    , CLambda+    , lambda+    , reifyM+    , reifyTop+    , reify+    ) where++++import Control.Monad.State++import Language.Syntactic+import Language.Syntactic.Constructs.Binding++++-- | Higher-order lambda binding+data HOLambda dom p pVar a+  where+    HOLambda+        :: (p a, pVar a)+        => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b)+        -> HOLambda dom p pVar (Full (a -> b))++-- | Adding support for higher-order abstract syntax to a domain+type HODomain dom p pVar = (HOLambda dom p pVar :+: (Variable :|| pVar) :+: dom) :|| p++-- | Equivalent to 'HODomain' (including type constraints), but using a first-order representation+-- of binding+type FODomain dom p pVar = (CLambda pVar :+: (Variable :|| pVar) :+: dom) :|| p++-- | 'Lambda' with a constraint on the bound variable type+type CLambda pVar = SubConstr2 (->) Lambda pVar Top++++-- | Lambda binding+lambda+    :: (p (a -> b), p a, pVar a)+    => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b)+    -> ASTF (HODomain dom p pVar) (a -> b)+lambda = injC . HOLambda++instance+    ( Syntactic a (HODomain dom p pVar)+    , Syntactic b (HODomain dom p pVar)+    , p (Internal a -> Internal b)+    , p (Internal a)+    , pVar (Internal a)+    ) =>+      Syntactic (a -> b) (HODomain dom p pVar)+  where+    type Internal (a -> b) = Internal a -> Internal b+    desugar f = lambda (desugar . f . sugar)+    sugar     = error "sugar not implemented for (a -> b)"+      -- TODO An implementation of sugar would require dom to have some kind of+      --      application. Perhaps use `Let` for this?++++reifyM :: forall dom p pVar a+    . AST (HODomain dom p pVar) a -> State VarId (AST (FODomain dom p pVar) a)+reifyM (f :$ a)            = liftM2 (:$) (reifyM f) (reifyM a)+reifyM (Sym (C' (InjR a))) = return $ Sym $ C' $ InjR a+reifyM (Sym (C' (InjL (HOLambda f)))) = do+    v    <- get; put (v+1)+    body <- reifyM $ f $ injC $ symType pVar $ C' (Variable v)+    return $ injC (symType pLam $ SubConstr2 (Lambda v)) :$ body+  where+    pVar = P::P (Variable :|| pVar)+    pLam = P::P (CLambda pVar)++-- | Translating expressions with higher-order binding to corresponding+-- expressions using first-order binding+reifyTop :: AST (HODomain dom p pVar) a -> AST (FODomain dom p pVar) a+reifyTop = flip evalState 0 . reifyM+  -- It is assumed that there are no 'Variable' constructors (i.e. no free+  -- variables) in the argument. This is guaranteed by the exported interface.++-- | Reify an n-ary syntactic function+reify :: Syntactic a (HODomain dom p pVar) => a -> ASTF (FODomain dom p pVar) (Internal a)+reify = reifyTop . desugar+
+ src/Language/Syntactic/Constructs/Binding/Optimize.hs view
@@ -0,0 +1,145 @@+-- | Basic optimization+module Language.Syntactic.Constructs.Binding.Optimize where++-- TODO This module should live somewhere else.++++import Control.Monad.Writer+import Data.Set as Set+import Data.Typeable++import Language.Syntactic+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Construct+import Language.Syntactic.Constructs.Identity+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Tuple++++-- | Constant folder+--+-- Given an expression and the statically known value of that expression,+-- returns a (possibly) new expression with the same meaning as the original.+-- Typically, the result will be a 'Literal', if the relevant type constraints+-- are satisfied.+type ConstFolder dom = forall a . ASTF dom a -> a -> ASTF dom a++-- | Basic optimization+class Optimize sym+  where+    -- | Bottom-up optimization of an expression. The optimization performed is+    -- up to each instance, but the intention is to provide a sensible set of+    -- \"always-appropriate\" optimizations. The default implementation+    -- 'optimizeSymDefault' does only constant folding. This constant folding+    -- uses the set of free variables to know when it's static evaluation is+    -- possible. Thus it is possible to help constant folding of other+    -- constructs by pruning away parts of the syntax tree that are known not to+    -- be needed. For example, by replacing (using ordinary Haskell as an+    -- example)+    --+    -- > if True then a else b+    --+    -- with @a@, we don't need to report the free variables in @b@. This, in+    -- turn, can lead to more constant folding higher up in the expression.+    optimizeSym+        :: Optimize' dom+        => ConstFolder dom+        -> (sym sig -> AST dom sig)+        -> sym sig+        -> Args (AST dom) sig+        -> Writer (Set VarId) (ASTF dom (DenResult sig))++  -- The reason for having @dom@ as a class parameter is that many instances+  -- need to put additional constraints on @dom@.++type Optimize' dom =+    ( Optimize dom+    , EvalBind dom+    , AlphaEq dom dom dom [(VarId,VarId)]+    , ConstrainedBy dom Typeable+    )++instance (Optimize sub1, Optimize sub2) => Optimize (sub1 :+: sub2)+  where+    optimizeSym constFold injecter (InjL a) = optimizeSym constFold (injecter . InjL) a+    optimizeSym constFold injecter (InjR a) = optimizeSym constFold (injecter . InjR) a++optimizeM :: Optimize' dom+    => ConstFolder dom+    -> ASTF dom a+    -> Writer (Set VarId) (ASTF dom a)+optimizeM constFold = matchTrans (optimizeSym constFold Sym)++-- | Optimize an expression+optimize :: Optimize' dom => ConstFolder dom -> ASTF dom a -> ASTF dom a+optimize constFold = fst . runWriter . optimizeM constFold++-- | Convenient default implementation of 'optimizeSym' (uses 'evalBind' to+-- partially evaluate)+optimizeSymDefault :: Optimize' dom+    => ConstFolder dom+    -> (sym sig -> AST dom sig)+    -> sym sig+    -> Args (AST dom) sig+    -> Writer (Set VarId) (ASTF dom (DenResult sig))+optimizeSymDefault constFold injecter sym args = do+    (args',vars) <- listen $ mapArgsM (optimizeM constFold) args+    let result = appArgs (injecter sym) args'+        value  = evalBind result+    if Set.null vars+      then return $ constFold result value+      else return result++instance Optimize dom => Optimize (dom :| p)+  where+    optimizeSym cf i (C s) args = optimizeSym cf (i . C) s args++instance Optimize dom => Optimize (dom :|| p)+  where+    optimizeSym cf i (C' s) args = optimizeSym cf (i . C') s args++instance Optimize Empty+  where+    optimizeSym = error "Not implemented: optimizeSym for Empty"++instance Optimize dom => Optimize (SubConstr1 c dom p)+  where+    optimizeSym cf i (SubConstr1 s) args = optimizeSym cf (i . SubConstr1) s args++instance Optimize dom => Optimize (SubConstr2 c dom pa pb)+  where+    optimizeSym cf i (SubConstr2 s) args = optimizeSym cf (i . SubConstr2) s args++instance Optimize Identity  where optimizeSym = optimizeSymDefault+instance Optimize Construct where optimizeSym = optimizeSymDefault+instance Optimize Literal   where optimizeSym = optimizeSymDefault+instance Optimize Tuple     where optimizeSym = optimizeSymDefault+instance Optimize Select    where optimizeSym = optimizeSymDefault+instance Optimize Let       where optimizeSym = optimizeSymDefault++instance Optimize Condition+  where+    optimizeSym constFold injecter cond@Condition args@(c :* t :* e :* Nil)+        | Set.null cVars = optimizeM constFold t_or_e+        | alphaEq t e    = optimizeM constFold t+        | otherwise      = optimizeSymDefault constFold injecter cond args+      where+        (c',cVars) = runWriter $ optimizeM constFold c+        t_or_e     = if evalBind c' then t else e++instance Optimize Variable+  where+    optimizeSym _ injecter var@(Variable v) Nil = do+        tell (singleton v)+        return (injecter var)++instance Optimize Lambda+  where+    optimizeSym constFold injecter lam@(Lambda v) (body :* Nil) = do+        body' <- censor (delete v) $ optimizeM constFold body+        return $ injecter lam :$ body'+
+ src/Language/Syntactic/Constructs/Condition.hs view
@@ -0,0 +1,28 @@+-- | Conditional expressions++module Language.Syntactic.Constructs.Condition where++++import Language.Syntactic++++data Condition sig+  where+    Condition :: Condition (Bool :-> a :-> a :-> Full a)++instance Constrained Condition+  where+    type Sat Condition = Top+    exprDict _ = Dict++instance Semantic Condition+  where+    semantics Condition = Sem "condition" (\c t e -> if c then t else e)++instance Equality Condition where equal = equalDefault; exprHash = exprHashDefault+instance Render   Condition where renderArgs = renderArgsDefault+instance Eval     Condition where evaluate   = evaluateDefault+instance ToTree   Condition+
+ src/Language/Syntactic/Constructs/Construct.hs view
@@ -0,0 +1,31 @@+-- | Provides a simple way to make syntactic constructs for prototyping. Note+-- that 'Construct' is quite unsafe as it only uses 'String' to distinguish+-- between different constructs. Also, 'Construct' has a very free type that+-- allows any number of arguments.++module Language.Syntactic.Constructs.Construct where++++import Language.Syntactic++++data Construct sig+  where+    Construct :: String -> Denotation sig -> Construct sig++instance Constrained Construct+  where+    type Sat Construct = Top+    exprDict _ = Dict++instance Semantic Construct+  where+    semantics (Construct name den) = Sem name den++instance Equality Construct where equal = equalDefault; exprHash = exprHashDefault+instance Render   Construct where renderArgs = renderArgsDefault+instance Eval     Construct where evaluate   = evaluateDefault+instance ToTree   Construct+
+ src/Language/Syntactic/Constructs/Decoration.hs view
@@ -0,0 +1,118 @@+-- | Construct for decorating expressions with additional information++module Language.Syntactic.Constructs.Decoration where++++import Data.Tree++import Language.Syntactic++++--------------------------------------------------------------------------------+-- * Decoration+--------------------------------------------------------------------------------++-- | Decorating symbols with additional information+--+-- One usage of 'Decor' is to decorate every node of a syntax tree. This is done+-- simply by changing+--+-- > AST dom sig+--+-- to+--+-- > AST (Decor info dom) sig+data Decor info expr sig+  where+    Decor+        :: { decorInfo :: info (DenResult sig)+           , decorExpr :: expr sig+           }+        -> Decor info expr sig++instance Constrained expr => Constrained (Decor info expr)+  where+    type Sat (Decor info expr) = Sat expr+    exprDict (Decor _ a) = exprDict a++instance Project sub sup => Project sub (Decor info sup)+  where+    prj = prj . decorExpr++instance Equality expr => Equality (Decor info expr)+  where+    equal a b = decorExpr a `equal` decorExpr b+    exprHash  = exprHash . decorExpr++instance Render expr => Render (Decor info expr)+  where+    renderArgs args = renderArgs args . decorExpr+    render = render . decorExpr++instance ToTree expr => ToTree (Decor info expr)+  where+    toTreeArgs args = toTreeArgs args . decorExpr++instance Eval expr => Eval (Decor info expr)+  where+    evaluate = evaluate . decorExpr++++-- | Get the decoration of the top-level node+getInfo :: AST (Decor info dom) sig -> info (DenResult sig)+getInfo (Sym (Decor info _)) = info+getInfo (f :$ _)             = getInfo f++-- | Update the decoration of the top-level node+updateDecor :: forall info dom a .+    (info a -> info a) -> ASTF (Decor info dom) a -> ASTF (Decor info dom) a+updateDecor f = match update+  where+    update+        :: (a ~ DenResult sig)+        => Decor info dom sig+        -> Args (AST (Decor info dom)) sig+        -> ASTF (Decor info dom) a+    update (Decor info a) args = appArgs (Sym sym) args+      where+        sym = Decor (f info) a++-- | Lift a function that operates on expressions with associated information to+-- operate on an 'Decor' expression. This function is convenient to use together+-- with e.g. 'queryNodeSimple' when the domain has the form+-- @(`Decor` info dom)@.+liftDecor :: (expr s -> info (DenResult s) -> b) -> (Decor info expr s -> b)+liftDecor f (Decor info a) = f a info++-- | Collect the decorations of all nodes+collectInfo :: (forall sig . info sig -> b) -> AST (Decor info dom) sig -> [b]+collectInfo coll (Sym (Decor info _)) = [coll info]+collectInfo coll (f :$ a) = collectInfo coll f ++ collectInfo coll a++-- | Rendering of decorated syntax trees+toTreeDecor :: forall info dom a . (Render info, ToTree dom) =>+    ASTF (Decor info dom) a -> Tree String+toTreeDecor a = mkTree [] a+  where+    mkTree :: [Tree String] -> AST (Decor info dom) sig -> Tree String+    mkTree args (Sym (Decor info expr)) = Node infoStr [toTreeArgs args expr]+      where+        infoStr = "<<" ++ render info ++ ">>"+    mkTree args (f :$ a) = mkTree (mkTree [] a : args) f++-- | Show an decorated syntax tree using ASCII art+showDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> String+showDecor = drawTree . toTreeDecor++-- | Print an decorated syntax tree using ASCII art+drawDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> IO ()+drawDecor = putStrLn . showDecor++-- | Strip decorations from an 'AST'+stripDecor :: AST (Decor info dom) sig -> AST dom sig+stripDecor (Sym (Decor _ a)) = Sym a+stripDecor (f :$ a)          = stripDecor f :$ stripDecor a+
+ src/Language/Syntactic/Constructs/Identity.hs view
@@ -0,0 +1,29 @@+-- | Identity function++module Language.Syntactic.Constructs.Identity where++++import Language.Syntactic++++-- | Identity function+data Identity sig+  where+    Id :: Identity (a :-> Full a)++instance Constrained Identity+  where+    type Sat Identity = Top+    exprDict _ = Dict++instance Semantic Identity+  where+    semantics Id = Sem "id" id++instance Equality Identity where equal = equalDefault; exprHash = exprHashDefault+instance Render   Identity where renderArgs = renderArgsDefault+instance Eval     Identity where evaluate   = evaluateDefault+instance ToTree   Identity+
+ src/Language/Syntactic/Constructs/Literal.hs view
@@ -0,0 +1,41 @@+-- | Literal expressions++module Language.Syntactic.Constructs.Literal where++++import Data.Typeable++import Data.Hash++import Language.Syntactic++++data Literal sig+  where+    Literal :: (Eq a, Show a, Typeable a) => a -> Literal (Full a)++instance Constrained Literal+  where+    type Sat Literal = Eq :/\: Show :/\: Typeable :/\: Top+    exprDict (Literal _) = Dict++instance Equality Literal+  where+    Literal a `equal` Literal b = case cast a of+        Just a' -> a'==b+        Nothing -> False++    exprHash (Literal a) = hash (show a)++instance Render Literal+  where+    render (Literal a) = show a++instance ToTree Literal++instance Eval Literal+  where+    evaluate (Literal a) = a+
+ src/Language/Syntactic/Constructs/Monad.hs view
@@ -0,0 +1,44 @@+-- | Monadic constructs+--+-- This module is based on the paper+-- /Generic Monadic Constructs for Embedded Languages/ (Persson et al., IFL 2011+-- <http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf>).++module Language.Syntactic.Constructs.Monad where++++import Control.Monad++import Language.Syntactic++++data MONAD m sig+  where+    Return :: MONAD m (a    :-> Full (m a))+    Bind   :: MONAD m (m a  :-> (a -> m b) :-> Full (m b))+    Then   :: MONAD m (m a  :-> m b        :-> Full (m b))+    When   :: MONAD m (Bool :-> m ()       :-> Full (m ()))++instance Constrained (MONAD m)+  where+    type Sat (MONAD m) = Top+    exprDict _ = Dict++instance Monad m => Semantic (MONAD m)+  where+    semantics Return = Sem "return" return+    semantics Bind   = Sem "bind"   (>>=)+    semantics Then   = Sem "then"   (>>)+    semantics When   = Sem "when"   when++instance Monad m => Equality (MONAD m) where equal = equalDefault; exprHash = exprHashDefault+instance Monad m => Render   (MONAD m) where renderArgs = renderArgsDefault+instance Monad m => Eval     (MONAD m) where evaluate   = evaluateDefault+instance Monad m => ToTree   (MONAD m)++-- | Projection with explicit monad type+prjMonad :: Project (MONAD m) sup => P m -> sup sig -> Maybe (MONAD m sig)+prjMonad _ = prj+
+ src/Language/Syntactic/Constructs/Tuple.hs view
@@ -0,0 +1,139 @@+-- | Construction and elimination of tuples in the object language++module Language.Syntactic.Constructs.Tuple where++++import Data.Tuple.Select++import Language.Syntactic++++--------------------------------------------------------------------------------+-- * Construction+--------------------------------------------------------------------------------++-- | Expressions for constructing tuples+data Tuple sig+  where+    Tup2 :: Tuple (a :-> b :-> Full (a,b))+    Tup3 :: Tuple (a :-> b :-> c :-> Full (a,b,c))+    Tup4 :: Tuple (a :-> b :-> c :-> d :-> Full (a,b,c,d))+    Tup5 :: Tuple (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))+    Tup6 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))+    Tup7 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))++instance Constrained Tuple+  where+    type Sat Tuple = Top+    exprDict _ = Dict++instance Semantic Tuple+  where+    semantics Tup2 = Sem "tup2" (,)+    semantics Tup3 = Sem "tup3" (,,)+    semantics Tup4 = Sem "tup4" (,,,)+    semantics Tup5 = Sem "tup5" (,,,,)+    semantics Tup6 = Sem "tup6" (,,,,,)+    semantics Tup7 = Sem "tup7" (,,,,,,)++instance Equality Tuple where equal = equalDefault; exprHash = exprHashDefault+instance Render   Tuple where renderArgs = renderArgsDefault+instance Eval     Tuple where evaluate   = evaluateDefault+instance ToTree   Tuple++++--------------------------------------------------------------------------------+-- * Projection+--------------------------------------------------------------------------------++-- | These families ('Sel1'' - 'Sel7'') are needed because of the problem+-- described in:+--+-- <http://emil-fp.blogspot.com/2011/08/fundeps-weaker-than-type-families.html>+type family Sel1' a+type instance Sel1' (a,b)           = a+type instance Sel1' (a,b,c)         = a+type instance Sel1' (a,b,c,d)       = a+type instance Sel1' (a,b,c,d,e)     = a+type instance Sel1' (a,b,c,d,e,f)   = a+type instance Sel1' (a,b,c,d,e,f,g) = a++type family Sel2' a+type instance Sel2' (a,b)           = b+type instance Sel2' (a,b,c)         = b+type instance Sel2' (a,b,c,d)       = b+type instance Sel2' (a,b,c,d,e)     = b+type instance Sel2' (a,b,c,d,e,f)   = b+type instance Sel2' (a,b,c,d,e,f,g) = b++type family Sel3' a+type instance Sel3' (a,b,c)         = c+type instance Sel3' (a,b,c,d)       = c+type instance Sel3' (a,b,c,d,e)     = c+type instance Sel3' (a,b,c,d,e,f)   = c+type instance Sel3' (a,b,c,d,e,f,g) = c++type family Sel4' a+type instance Sel4' (a,b,c,d)       = d+type instance Sel4' (a,b,c,d,e)     = d+type instance Sel4' (a,b,c,d,e,f)   = d+type instance Sel4' (a,b,c,d,e,f,g) = d++type family Sel5' a+type instance Sel5' (a,b,c,d,e)     = e+type instance Sel5' (a,b,c,d,e,f)   = e+type instance Sel5' (a,b,c,d,e,f,g) = e++type family Sel6' a+type instance Sel6' (a,b,c,d,e,f)   = f+type instance Sel6' (a,b,c,d,e,f,g) = f++type family Sel7' a+type instance Sel7' (a,b,c,d,e,f,g) = g++-- | Expressions for selecting elements of a tuple+data Select a+  where+    Sel1 :: (Sel1 a b, Sel1' a ~ b) => Select (a :-> Full b)+    Sel2 :: (Sel2 a b, Sel2' a ~ b) => Select (a :-> Full b)+    Sel3 :: (Sel3 a b, Sel3' a ~ b) => Select (a :-> Full b)+    Sel4 :: (Sel4 a b, Sel4' a ~ b) => Select (a :-> Full b)+    Sel5 :: (Sel5 a b, Sel5' a ~ b) => Select (a :-> Full b)+    Sel6 :: (Sel6 a b, Sel6' a ~ b) => Select (a :-> Full b)+    Sel7 :: (Sel7 a b, Sel7' a ~ b) => Select (a :-> Full b)++instance Constrained Select+  where+    type Sat Select = Top+    exprDict _ = Dict++instance Semantic Select+  where+    semantics Sel1 = Sem "sel1" sel1+    semantics Sel2 = Sem "sel2" sel2+    semantics Sel3 = Sem "sel3" sel3+    semantics Sel4 = Sem "sel4" sel4+    semantics Sel5 = Sem "sel5" sel5+    semantics Sel6 = Sem "sel6" sel6+    semantics Sel7 = Sem "sel7" sel7++instance Equality Select where equal = equalDefault; exprHash = exprHashDefault+instance Render   Select where renderArgs = renderArgsDefault+instance Eval     Select where evaluate   = evaluateDefault+instance ToTree   Select++-- | Return the selected position, e.g.+--+-- > selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3+selectPos :: Select a -> Int+selectPos Sel1 = 1+selectPos Sel2 = 2+selectPos Sel3 = 3+selectPos Sel4 = 4+selectPos Sel5 = 5+selectPos Sel6 = 6+selectPos Sel7 = 7+
+ src/Language/Syntactic/Frontend/Monad.hs view
@@ -0,0 +1,80 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Monadic constructs+--+-- This module is based on the paper+-- /Generic Monadic Constructs for Embedded Languages/ (Persson et al., IFL 2011+-- <http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf>).++module Language.Syntactic.Frontend.Monad where++++import Control.Monad.Cont+import Data.Typeable++import Language.Syntactic+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Constructs.Monad++++-- TODO Unfortunately, this module hard-codes the use of `Typeable`. The problem+--      is this: Say we replace `Typeable` in the definition of `Mon` by a+--      parameter `p`. Then `sugarMonad` will get a constraint `p (a -> m r)`.+--      But `r` existentially quantified and can only be constrained in the+--      definition of `Mon`. With `Typeable` this works because+--      `(Typeable1 m, Typeable a, Typeable r)` implies `Typeable (a -> m r)`.++-- | User interface to embedded monadic programs+newtype Mon dom pVar m a+  where+    Mon+        :: { unMon :: forall r+                   .  (Monad m, Typeable r, InjectC (MONAD m) dom (m r))+                   => Cont (ASTF (HODomain dom Typeable pVar) (m r)) a+           }+        -> Mon dom pVar m a++deriving instance Functor (Mon dom pVar m)++instance (Monad m) => Monad (Mon dom pVar m)+  where+    return a = Mon $ return a+    ma >>= f = Mon $ unMon ma >>= unMon . f++-- | One-layer desugaring of monadic actions+desugarMonad+    :: ( InjectC (MONAD m) dom (m a)+       , Monad m+       , Typeable1 m+       , Typeable a+       )+    => Mon dom pVar m (ASTF (HODomain dom Typeable pVar) a)+    -> ASTF (HODomain dom Typeable pVar) (m a)+desugarMonad = flip runCont (sugarSymC Return) . unMon++-- | One-layer sugaring of monadic actions+sugarMonad+    :: ( Monad m+       , Typeable1 m+       , Typeable a+       , pVar a+       )+    => ASTF (HODomain dom Typeable pVar) (m a)+    -> Mon dom pVar m (ASTF (HODomain dom Typeable pVar) a)+sugarMonad ma = Mon $ cont $ sugarSymC Bind ma++instance ( Syntactic a (HODomain dom Typeable pVar)+         , InjectC (MONAD m) dom (m (Internal a))+         , Monad m+         , Typeable1 m+         , Typeable (Internal a)+         , pVar (Internal a)+         ) =>+           Syntactic (Mon dom pVar m a) (HODomain dom Typeable pVar)+  where+    type Internal (Mon dom pVar m a) = m (Internal a)+    desugar = desugarMonad . fmap desugar+    sugar   = fmap sugar   . sugarMonad+
+ src/Language/Syntactic/Frontend/Tuple.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE UndecidableInstances #-}++-- | 'Syntactic' instances for Haskell tuples++module Language.Syntactic.Frontend.Tuple where++++import Language.Syntactic+import Language.Syntactic.Constructs.Tuple+import Data.Tuple.Curry++++instance+    ( Syntactic a dom+    , Syntactic b dom+    , InjectC Tuple dom+        ( Internal a+        , Internal b+        )+    , InjectC Select dom (Internal a)+    , InjectC Select dom (Internal b)+    ) =>+      Syntactic (a,b) dom+  where+    type Internal (a,b) =+        ( Internal a+        , Internal b+        )++    desugar = uncurryN $ sugarSymC Tup2+    sugar a =+        ( sugarSymC Sel1 a+        , sugarSymC Sel2 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , InjectC Tuple dom+        ( Internal a+        , Internal b+        , Internal c+        )+    , InjectC Select dom (Internal a)+    , InjectC Select dom (Internal b)+    , InjectC Select dom (Internal c)+    ) =>+      Syntactic (a,b,c) dom+  where+    type Internal (a,b,c) =+        ( Internal a+        , Internal b+        , Internal c+        )++    desugar = uncurryN $ sugarSymC Tup3+    sugar a =+        ( sugarSymC Sel1 a+        , sugarSymC Sel2 a+        , sugarSymC Sel3 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , InjectC Tuple dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        )+    , InjectC Select dom (Internal a)+    , InjectC Select dom (Internal b)+    , InjectC Select dom (Internal c)+    , InjectC Select dom (Internal d)+    ) =>+      Syntactic (a,b,c,d) dom+  where+    type Internal (a,b,c,d) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        )++    desugar = uncurryN $ sugarSymC Tup4+    sugar a =+        ( sugarSymC Sel1 a+        , sugarSymC Sel2 a+        , sugarSymC Sel3 a+        , sugarSymC Sel4 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , InjectC Tuple dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        )+    , InjectC Select dom (Internal a)+    , InjectC Select dom (Internal b)+    , InjectC Select dom (Internal c)+    , InjectC Select dom (Internal d)+    , InjectC Select dom (Internal e)+    ) =>+      Syntactic (a,b,c,d,e) dom+  where+    type Internal (a,b,c,d,e) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        )++    desugar = uncurryN $ sugarSymC Tup5+    sugar a =+        ( sugarSymC Sel1 a+        , sugarSymC Sel2 a+        , sugarSymC Sel3 a+        , sugarSymC Sel4 a+        , sugarSymC Sel5 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , Syntactic f dom+    , InjectC Tuple dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        )+    , InjectC Select dom (Internal a)+    , InjectC Select dom (Internal b)+    , InjectC Select dom (Internal c)+    , InjectC Select dom (Internal d)+    , InjectC Select dom (Internal e)+    , InjectC Select dom (Internal f)+    ) =>+      Syntactic (a,b,c,d,e,f) dom+  where+    type Internal (a,b,c,d,e,f) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        )++    desugar = uncurryN $ sugarSymC Tup6+    sugar a =+        ( sugarSymC Sel1 a+        , sugarSymC Sel2 a+        , sugarSymC Sel3 a+        , sugarSymC Sel4 a+        , sugarSymC Sel5 a+        , sugarSymC Sel6 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , Syntactic f dom+    , Syntactic g dom+    , InjectC Tuple dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        , Internal g+        )+    , InjectC Select dom (Internal a)+    , InjectC Select dom (Internal b)+    , InjectC Select dom (Internal c)+    , InjectC Select dom (Internal d)+    , InjectC Select dom (Internal e)+    , InjectC Select dom (Internal f)+    , InjectC Select dom (Internal g)+    ) =>+      Syntactic (a,b,c,d,e,f,g) dom+  where+    type Internal (a,b,c,d,e,f,g) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        , Internal g+        )++    desugar = uncurryN $ sugarSymC Tup7+    sugar a =+        ( sugarSymC Sel1 a+        , sugarSymC Sel2 a+        , sugarSymC Sel3 a+        , sugarSymC Sel4 a+        , sugarSymC Sel5 a+        , sugarSymC Sel6 a+        , sugarSymC Sel7 a+        )+
+ src/Language/Syntactic/Frontend/TupleConstrained.hs view
@@ -0,0 +1,324 @@+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Constrained 'Syntactic' instances for Haskell tuples++module Language.Syntactic.Frontend.TupleConstrained+    ( TupleSat+    ) where++++import Data.Constraint+import Data.Tuple.Curry++import Language.Syntactic+import Language.Syntactic.Constructs.Tuple++++-- | Type-level function computing the predicate attached to 'Tuple' or 'Select'+-- (whichever appears first) in a domain.+class TupleSat (dom :: * -> *) (p :: * -> Constraint) | dom -> p++instance TupleSat (Tuple :|| p) p+instance TupleSat ((Tuple :|| p) :+: dom2) p++instance TupleSat (Select :|| p) p+instance TupleSat ((Select :|| p) :+: dom2) p++instance TupleSat dom p => TupleSat (dom :| q) p+instance TupleSat dom p => TupleSat (dom :|| q) p+instance TupleSat dom2 p => TupleSat (dom1 :+: dom2) p++++sugarSymC' :: forall sym dom sig b c p+    .  ( TupleSat dom p+       , p (DenResult sig)+       , InjectC (sym :|| p) (AST dom) (DenResult sig)+       , ApplySym sig b dom+       , SyntacticN c b+       )+    => sym sig -> c+sugarSymC' s = sugarSymC (C' s :: (sym :|| p) sig)++++instance+    ( Syntactic a dom+    , Syntactic b dom+    , TupleSat dom p+    , p (Internal a, Internal b)+    , p (Internal a)+    , p (Internal b)+    , InjectC (Tuple :|| p) dom+        ( Internal a+        , Internal b+        )+    , InjectC (Select :|| p) dom (Internal a)+    , InjectC (Select :|| p) dom (Internal b)+    ) =>+      Syntactic (a,b) dom+  where+    type Internal (a,b) =+        ( Internal a+        , Internal b+        )++    desugar = uncurryN $ sugarSymC' Tup2+    sugar a =+        ( sugarSymC' Sel1 a+        , sugarSymC' Sel2 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , TupleSat dom p+    , p ( Internal a+        , Internal b+        , Internal c+        )+    , p (Internal a)+    , p (Internal b)+    , p (Internal c)+    , InjectC (Tuple :|| p) dom+        ( Internal a+        , Internal b+        , Internal c+        )+    , InjectC (Select :|| p) dom (Internal a)+    , InjectC (Select :|| p) dom (Internal b)+    , InjectC (Select :|| p) dom (Internal c)+    ) =>+      Syntactic (a,b,c) dom+  where+    type Internal (a,b,c) =+        ( Internal a+        , Internal b+        , Internal c+        )++    desugar = uncurryN $ sugarSymC' Tup3+    sugar a =+        ( sugarSymC' Sel1 a+        , sugarSymC' Sel2 a+        , sugarSymC' Sel3 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , TupleSat dom p+    , p ( Internal a+        , Internal b+        , Internal c+        , Internal d+        )+    , p (Internal a)+    , p (Internal b)+    , p (Internal c)+    , p (Internal d)+    , InjectC (Tuple :|| p) dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        )+    , InjectC (Select :|| p) dom (Internal a)+    , InjectC (Select :|| p) dom (Internal b)+    , InjectC (Select :|| p) dom (Internal c)+    , InjectC (Select :|| p) dom (Internal d)+    ) =>+      Syntactic (a,b,c,d) dom+  where+    type Internal (a,b,c,d) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        )++    desugar = uncurryN $ sugarSymC' Tup4+    sugar a =+        ( sugarSymC' Sel1 a+        , sugarSymC' Sel2 a+        , sugarSymC' Sel3 a+        , sugarSymC' Sel4 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , TupleSat dom p+    , p ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        )+    , p (Internal a)+    , p (Internal b)+    , p (Internal c)+    , p (Internal d)+    , p (Internal e)+    , InjectC (Tuple :|| p) dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        )+    , InjectC (Select :|| p) dom (Internal a)+    , InjectC (Select :|| p) dom (Internal b)+    , InjectC (Select :|| p) dom (Internal c)+    , InjectC (Select :|| p) dom (Internal d)+    , InjectC (Select :|| p) dom (Internal e)+    ) =>+      Syntactic (a,b,c,d,e) dom+  where+    type Internal (a,b,c,d,e) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        )++    desugar = uncurryN $ sugarSymC' Tup5+    sugar a =+        ( sugarSymC' Sel1 a+        , sugarSymC' Sel2 a+        , sugarSymC' Sel3 a+        , sugarSymC' Sel4 a+        , sugarSymC' Sel5 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , Syntactic f dom+    , TupleSat dom p+    , p ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        )+    , p (Internal a)+    , p (Internal b)+    , p (Internal c)+    , p (Internal d)+    , p (Internal e)+    , p (Internal f)+    , InjectC (Tuple :|| p) dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        )+    , InjectC (Select :|| p) dom (Internal a)+    , InjectC (Select :|| p) dom (Internal b)+    , InjectC (Select :|| p) dom (Internal c)+    , InjectC (Select :|| p) dom (Internal d)+    , InjectC (Select :|| p) dom (Internal e)+    , InjectC (Select :|| p) dom (Internal f)+    ) =>+      Syntactic (a,b,c,d,e,f) dom+  where+    type Internal (a,b,c,d,e,f) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        )++    desugar = uncurryN $ sugarSymC' Tup6+    sugar a =+        ( sugarSymC' Sel1 a+        , sugarSymC' Sel2 a+        , sugarSymC' Sel3 a+        , sugarSymC' Sel4 a+        , sugarSymC' Sel5 a+        , sugarSymC' Sel6 a+        )++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , Syntactic f dom+    , Syntactic g dom+    , TupleSat dom p+    , p ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        , Internal g+        )+    , p (Internal a)+    , p (Internal b)+    , p (Internal c)+    , p (Internal d)+    , p (Internal e)+    , p (Internal f)+    , p (Internal g)+    , InjectC (Tuple :|| p) dom+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        , Internal g+        )+    , InjectC (Select :|| p) dom (Internal a)+    , InjectC (Select :|| p) dom (Internal b)+    , InjectC (Select :|| p) dom (Internal c)+    , InjectC (Select :|| p) dom (Internal d)+    , InjectC (Select :|| p) dom (Internal e)+    , InjectC (Select :|| p) dom (Internal f)+    , InjectC (Select :|| p) dom (Internal g)+    ) =>+      Syntactic (a,b,c,d,e,f,g) dom+  where+    type Internal (a,b,c,d,e,f,g) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        , Internal g+        )++    desugar = uncurryN $ sugarSymC' Tup7+    sugar a =+        ( sugarSymC' Sel1 a+        , sugarSymC' Sel2 a+        , sugarSymC' Sel3 a+        , sugarSymC' Sel4 a+        , sugarSymC' Sel5 a+        , sugarSymC' Sel6 a+        , sugarSymC' Sel7 a+        )+
+ src/Language/Syntactic/Interpretation/Equality.hs view
@@ -0,0 +1,52 @@+module Language.Syntactic.Interpretation.Equality where++++import Data.Hash++import Language.Syntactic.Syntax++++-- | Equality for expressions+class Equality expr+  where+    -- | Equality for expressions+    --+    -- Comparing expressions of different types is often needed when dealing+    -- with expressions with existentially quantified sub-terms.+    equal :: expr a -> expr b -> Bool++    -- | Computes a 'Hash' for an expression. Expressions that are equal+    -- according to 'equal' must result in the same hash:+    --+    -- @equal a b  ==>  exprHash a == exprHash b@+    exprHash :: expr a -> Hash+++instance Equality dom => Equality (AST dom)+  where+    equal (Sym a)    (Sym b)    = equal a b+    equal (s1 :$ a1) (s2 :$ a2) = equal s1 s2 && equal a1 a2+    equal _ _                   = False++    exprHash (Sym a)  = hashInt 0 `combine` exprHash a+    exprHash (s :$ a) = hashInt 1 `combine` exprHash s `combine` exprHash a++instance Equality dom => Eq (AST dom a)+  where+    (==) = equal++instance (Equality expr1, Equality expr2) => Equality (expr1 :+: expr2)+  where+    equal (InjL a) (InjL b) = equal a b+    equal (InjR a) (InjR b) = equal a b+    equal _ _               = False++    exprHash (InjL a) = hashInt 0 `combine` exprHash a+    exprHash (InjR a) = hashInt 1 `combine` exprHash a++instance (Equality expr1, Equality expr2) => Eq ((expr1 :+: expr2) a)+  where+    (==) = equal+
+ src/Language/Syntactic/Interpretation/Evaluation.hs view
@@ -0,0 +1,28 @@+module Language.Syntactic.Interpretation.Evaluation where++++import Language.Syntactic.Syntax++++-- | The denotation of a symbol with the given signature+type family   Denotation sig+type instance Denotation (Full a)    = a+type instance Denotation (a :-> sig) = a -> Denotation sig++class Eval expr+  where+    -- | Evaluation of expressions+    evaluate :: expr a -> Denotation a++instance Eval dom => Eval (AST dom)+  where+    evaluate (Sym a)  = evaluate a+    evaluate (s :$ a) = evaluate s $ evaluate a++instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)+  where+    evaluate (InjL a) = evaluate a+    evaluate (InjR a) = evaluate a+
+ src/Language/Syntactic/Interpretation/Render.hs view
@@ -0,0 +1,83 @@+module Language.Syntactic.Interpretation.Render+    ( Render (..)+    , printExpr+    , ToTree (..)+    , showAST+    , drawAST+    ) where++++import Data.Tree++import Language.Syntactic.Syntax++++-- | Render an expression as concrete syntax. A complete instance must define+-- either of the methods 'render' and 'renderArgs'.+class Render expr+  where+    -- | Render an expression as a 'String'+    render :: expr a -> String+    render = renderArgs []++    -- | Render a partially applied expression given a list of rendered missing+    -- arguments+    renderArgs :: [String] -> expr a -> String+    renderArgs []   a = render a+    renderArgs args a = "(" ++ unwords (render a : args) ++ ")"++instance Render dom => Render (AST dom)+  where+    renderArgs args (Sym a)  = renderArgs args a+    renderArgs args (s :$ a) = renderArgs (render a : args) s++instance Render dom => Show (AST dom a)+  where+    show = render++instance (Render expr1, Render expr2) => Render (expr1 :+: expr2)+  where+    renderArgs args (InjL a) = renderArgs args a+    renderArgs args (InjR a) = renderArgs args a++instance (Render expr1, Render expr2) => Show ((expr1 :+: expr2) a)+  where+    show = render++-- | Print an expression+printExpr :: Render expr => expr a -> IO ()+printExpr = putStrLn . render++++class Render expr => ToTree expr+  where+    -- | Convert a partially applied expression to a syntax tree given a list of+    -- rendered missing arguments+    toTreeArgs :: [Tree String] -> expr a -> Tree String+    toTreeArgs args a = Node (render a) args++instance ToTree dom => ToTree (AST dom)+  where+    toTreeArgs args (Sym a)  = toTreeArgs args a+    toTreeArgs args (s :$ a) = toTreeArgs (toTree a : args) s++instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2)+  where+    toTreeArgs args (InjL a) = toTreeArgs args a+    toTreeArgs args (InjR a) = toTreeArgs args a++-- | Convert an expression to a syntax tree+toTree :: ToTree expr => expr a -> Tree String+toTree = toTreeArgs []++-- | Show syntax tree using ASCII art+showAST :: ToTree dom => AST dom a -> String+showAST = drawTree . toTree++-- | Print syntax tree using ASCII art+drawAST :: ToTree dom => AST dom a -> IO ()+drawAST = putStrLn . showAST+
+ src/Language/Syntactic/Interpretation/Semantics.hs view
@@ -0,0 +1,76 @@+-- | Default implementations of some interpretation functions++module Language.Syntactic.Interpretation.Semantics where++++import Data.Hash++import Language.Syntactic.Syntax+import Language.Syntactic.Interpretation.Equality+import Language.Syntactic.Interpretation.Render+import Language.Syntactic.Interpretation.Evaluation++++-- | A representation of a syntactic construct as a 'String' and an evaluation+-- function. It is not meant to be used as a syntactic symbol in an 'AST'. Its+-- only purpose is to provide the default implementations of functions like+-- `equal` via the `Semantic` class.+data Semantics a+  where+    Sem+        :: { semanticName :: String+           , semanticEval :: Denotation a+           }+        -> Semantics a++++instance Equality Semantics+  where+    equal (Sem a _) (Sem b _) = a==b+    exprHash (Sem name _)     = hash name++instance Render Semantics+  where+    renderArgs [] (Sem name _) = name+    renderArgs args (Sem name _)+        | isInfix   = "(" ++ unwords [a,op,b] ++ ")"+        | otherwise = "(" ++ unwords (name : args) ++ ")"+      where+        [a,b] = args+        op    = init $ tail name+        isInfix+          =  not (null name)+          && head name == '('+          && last name == ')'+          && length args == 2++instance Eval Semantics+  where+    evaluate (Sem _ a) = a++++-- | Class of expressions that can be treated as constructs+class Semantic expr+  where+    semantics :: expr a -> Semantics a++-- | Default implementation of 'equal'+equalDefault :: Semantic expr => expr a -> expr b -> Bool+equalDefault a b = equal (semantics a) (semantics b)++-- | Default implementation of 'exprHash'+exprHashDefault :: Semantic expr => expr a -> Hash+exprHashDefault = exprHash . semantics++-- | Default implementation of 'renderArgs'+renderArgsDefault :: Semantic expr => [String] -> expr a -> String+renderArgsDefault args = renderArgs args . semantics++-- | Default implementation of 'evaluate'+evaluateDefault :: Semantic expr => expr a -> Denotation a+evaluateDefault = evaluate . semantics+
+ src/Language/Syntactic/Sharing/Graph.hs view
@@ -0,0 +1,336 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Representation and manipulation of abstract syntax graphs++module Language.Syntactic.Sharing.Graph where++++import Control.Arrow ((***))+import Control.Monad.Reader+import Data.Array+import Data.Function+import Data.List+import Data.Typeable++import Data.Hash++import Language.Syntactic+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Sharing.Utils++++--------------------------------------------------------------------------------+-- * Representation+--------------------------------------------------------------------------------++-- | Node identifier+newtype NodeId = NodeId { nodeInteger :: Integer }+  deriving (Eq, Ord, Num, Real, Integral, Enum, Ix)++instance Show NodeId+  where+    show (NodeId i) = show i++showNode :: NodeId -> String+showNode n = "node:" ++ show n++++-- | Placeholder for a syntax tree+data Node a+  where+    Node :: NodeId -> Node (Full a)++instance Constrained Node+  where+    type Sat Node = Top+    exprDict _ = Dict++instance Render Node+  where+    render (Node a) = showNode a++instance ToTree Node++++-- | Environment for alpha-equivalence+class NodeEqEnv dom a+  where+    prjNodeEqEnv :: a -> NodeEnv dom (Sat dom)+    modNodeEqEnv :: (NodeEnv dom (Sat dom) -> NodeEnv dom (Sat dom)) -> (a -> a)++type EqEnv dom p = ([(VarId,VarId)], NodeEnv dom p)++type NodeEnv dom p =+    ( Array NodeId Hash+    , Array NodeId (ASTB dom p)+    )++instance (p ~ Sat dom) => NodeEqEnv dom (EqEnv dom p)+  where+    prjNodeEqEnv   = snd+    modNodeEqEnv f = (id *** f)++instance VarEqEnv (EqEnv dom p)+  where+    prjVarEqEnv   = fst+    modVarEqEnv f = (f *** id)++instance (AlphaEq dom dom dom env, NodeEqEnv dom env) =>+    AlphaEq Node Node dom env+  where+    alphaEqSym (Node n1) Nil (Node n2) Nil+        | n1 == n2  = return True+        | otherwise = do+            (hTab,nTab) :: NodeEnv dom p <- asks prjNodeEqEnv+            if hTab!n1 /= hTab!n2+              then return False+              else case (nTab!n1, nTab!n2) of+                  (ASTB a, ASTB b) -> alphaEqM a b+                    -- TODO The result could be memoized in a+                    -- @Map (NodeId,NodeId) Bool@++  -- TODO With only this instance, the result will be 'False' when one argument+  --      is a 'Node' and the other one isn't. This is not really correct since+  --      'Node's are just meta-variables and shouldn't be part of the+  --      comparison. But as long as equivalent expressions always have 'Node's+  --      at the same position, it doesn't matter. This could probably be fixed+  --      by adding two overlapping instances.++++-- | \"Abstract Syntax Graph\"+--+-- A representation of a syntax tree with explicit sharing. An 'ASG' is valid if+-- and only if 'inlineAll' succeeds (and the 'numNodes' field is correct).+data ASG dom a = ASG+    { topExpression :: ASTF (NodeDomain dom) a              -- ^ Top-level expression+    , graphNodes    :: [(NodeId, ASTSAT (NodeDomain dom))]  -- ^ Mapping from node id to sub-expression+    , numNodes      :: NodeId                               -- ^ Total number of nodes+    }++type NodeDomain dom = (Node :+: dom) :|| Sat dom++++-- | Show syntax graph using ASCII art+showASG :: ToTree dom => ASG dom a -> String+showASG (ASG top nodes _) =+    unlines ((line "top" ++ showAST top) : map showNode nodes)+  where+    line str = "---- " ++ str ++ " " ++ rest ++ "\n"+      where+        rest = take (40 - length str) $ repeat '-'++    showNode (n, ASTB expr) = concat+      [ line ("node:" ++ show n)+      , showAST expr+      ]++-- | Print syntax graph using ASCII art+drawASG :: ToTree dom => ASG dom a -> IO ()+drawASG = putStrLn . showASG++-- | Update the node identifiers in an 'AST' using the supplied reindexing+-- function+reindexNodesAST ::+    (NodeId -> NodeId) -> AST (NodeDomain dom) a -> AST (NodeDomain dom) a+reindexNodesAST reix (Sym (C' (InjL (Node n)))) = injC $ Node $ reix n+reindexNodesAST reix (s :$ a) = reindexNodesAST reix s :$ reindexNodesAST reix a+reindexNodesAST reix a = a++-- | Reindex the nodes according to the given index mapping. The number of nodes+-- is unchanged, so if the index mapping is not 1:1, the resulting graph will+-- contain duplicates.+reindexNodes :: (NodeId -> NodeId) -> ASG dom a -> ASG dom a+reindexNodes reix (ASG top nodes n) = ASG top' nodes' n+  where+    top'   = reindexNodesAST reix top+    nodes' =+      [ (reix n, ASTB $ reindexNodesAST reix a)+        | (n, ASTB a) <- nodes+      ]++-- | Reindex the nodes to be in the range @[0 .. l-1]@, where @l@ is the number+-- of nodes in the graph+reindexNodesFrom0 :: ASG dom a -> ASG dom a+reindexNodesFrom0 graph = reindexNodes reix graph+  where+    reix = reindex $ map fst $ graphNodes graph++-- | Remove duplicate nodes from a graph. The function only looks at the+-- 'NodeId' of each node. The 'numNodes' field is updated accordingly.+nubNodes :: ASG dom a -> ASG dom a+nubNodes (ASG top nodes n) = ASG top nodes' n'+  where+    nodes' = nubBy ((==) `on` fst) nodes+    n'     = genericLength nodes'++++--------------------------------------------------------------------------------+-- * Folding+--------------------------------------------------------------------------------++-- | Pattern functor representation of an 'AST' with 'Node's+data SyntaxPF dom a+  where+    AppPF  :: a -> a -> SyntaxPF dom a+    NodePF :: NodeId -> a -> SyntaxPF dom a+    DomPF  :: dom b -> SyntaxPF dom a+  -- NOTE: The important constructor is 'NodePF', which makes a 'Node' appear as+  -- any other recursive constructor.++instance Functor (SyntaxPF dom)+  where+    fmap f (AppPF g a)  = AppPF  (f g) (f a)+    fmap f (NodePF n a) = NodePF n (f a)+    fmap f (DomPF a)    = DomPF a++++-- | Folding over a graph+--+-- The user provides a function to fold a single constructor (an \"algebra\").+-- The result contains the result of folding the whole graph as well as the+-- result of each internal node, represented both as an array and an association+-- list. Each node is processed exactly once.+foldGraph :: forall dom a b .+    (SyntaxPF dom b -> b) -> ASG dom a -> (b, (Array NodeId b, [(NodeId,b)]))+foldGraph alg (ASG top ns nn) = (g top, (arr,nodes))+  where+    nodes = [(n, g expr) | (n, ASTB expr) <- ns]+    arr   = array (0, nn-1) nodes++    g :: AST (NodeDomain dom) c -> b+    g (h :$ a)                   = alg $ AppPF (g h) (g a)+    g (Sym (C' (InjL (Node n)))) = alg $ NodePF n (arr!n)+    g (Sym (C' (InjR a)))        = alg $ DomPF a++++--------------------------------------------------------------------------------+-- * Inlining+--------------------------------------------------------------------------------++-- | Convert an 'ASG' to an 'AST' by inlining all nodes+inlineAll :: forall dom a . ConstrainedBy dom Typeable =>+    ASG dom a -> ASTF dom a+inlineAll (ASG top nodes n) = inline top+  where+    nodeMap = array (0, n-1) nodes++    inline :: AST (NodeDomain dom) b -> AST dom b+    inline (s :$ a) = inline s :$ inline a+    inline s@(Sym (C' (InjL (Node n)))) = case nodeMap ! n of+        ASTB a+          | Dict <- exprDictSub pTypeable s+          , Dict <- exprDictSub pTypeable a+          -> case gcast a of+               Nothing -> error "inlineAll: type mismatch"+               Just a  -> inline a+    inline (Sym (C' (InjR a))) = Sym a++++-- | Find the child nodes of each node in an expression. The child nodes of a+-- node @n@ are the first nodes along all paths from @n@.+nodeChildren :: ASG dom a -> [(NodeId, [NodeId])]+nodeChildren = map (id *** fromDList) . snd . snd . foldGraph children+  where+    children :: SyntaxPF dom (DList NodeId) -> DList (NodeId)+    children (AppPF ns1 ns2) = ns1 . ns2+    children (NodePF n _)    = single n+    children _               = empty++-- | Count the number of occurrences of each node in an expression+occurrences :: ASG dom a -> Array NodeId Int+occurrences graph+    = count (0, numNodes graph - 1)+    $ concatMap snd+    $ nodeChildren graph++-- | Inline all nodes that are not shared+inlineSingle :: forall dom a . ConstrainedBy dom Typeable =>+    ASG dom a -> ASG dom a+inlineSingle graph@(ASG top nodes n) = ASG top' nodes' n'+  where+    nodeTab  = array (0, n-1) nodes+    occs     = occurrences graph++    top'   = inline top+    nodes' = [(n, ASTB (inline a)) | (n, ASTB a) <- nodes, occs!n > 1]+    n'     = genericLength nodes'++    inline :: AST (NodeDomain dom) b -> AST (NodeDomain dom) b+    inline (s :$ a) = inline s :$ inline a+    inline s@(Sym (C' (InjL (Node n))))+        | occs!n > 1 = injC $ Node n+        | otherwise = case nodeTab ! n of+            ASTB a+              | Dict <- exprDictSub pTypeable s+              , Dict <- exprDictSub pTypeable a+              -> case gcast a of+                   Nothing -> error "inlineSingle: type mismatch"+                   Just a  -> inline a+    inline (Sym (C' (InjR a))) = Sym $ C' $ InjR a++++--------------------------------------------------------------------------------+-- * Sharing+--------------------------------------------------------------------------------++-- | Compute a table (both array and list representation) of hash values for+-- each node+hashNodes :: Equality dom => ASG dom a -> (Array NodeId Hash, [(NodeId, Hash)])+hashNodes = snd . foldGraph hashNode+  where+    hashNode (AppPF h1 h2) = hashInt 0 `combine` h1 `combine` h2+    hashNode (NodePF _ h)  = h+    hashNode (DomPF a)     = hashInt 1 `combine` exprHash a++++-- | Partitions the nodes such that two nodes are in the same sub-list if and+-- only if they are alpha-equivalent.+partitionNodes :: forall dom a+    .  ( Equality dom+       , AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom) (Sat dom))+       )+    => ASG dom a -> [[NodeId]]+partitionNodes graph = concatMap (fullPartition nodeEq) approxPartitioning+  where+    nTab          = array (0, numNodes graph - 1) (graphNodes graph)+    (hTab,hashes) = hashNodes graph++    -- | An approximate partitioning of the nodes: nodes in different partitions+    -- are guaranteed to be inequivalent, while nodes in the same partition+    -- might be equivalent.+    approxPartitioning+        = map (map fst)+        $ groupBy ((==) `on` snd)+        $ sortBy (compare `on` snd)+        $ hashes++    nodeEq :: NodeId -> NodeId -> Bool+    nodeEq n1 n2 = runReader+        (liftASTB2 alphaEqM (nTab!n1) (nTab!n2))+        (([],(hTab,nTab)) :: EqEnv (NodeDomain dom) (Sat dom))++++-- | Common sub-expression elimination based on alpha-equivalence+cse+    :: ( Equality dom+       , AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom) (Sat dom))+       )+    => ASG dom a -> ASG dom a+cse graph@(ASG top nodes n) = nubNodes $ reindexNodes (reixTab!) graph+  where+    parts   = partitionNodes graph+    reixTab = array (0,n-1) [(n,p) | (part,p) <- parts `zip` [0..], n <- part]+
+ src/Language/Syntactic/Sharing/Reify.hs view
@@ -0,0 +1,80 @@+-- | Reifying the sharing in an 'AST'+--+-- This module is based on the paper /Type-Safe Observable Sharing in Haskell/+-- (Andy Gill, 2009, <http://dx.doi.org/10.1145/1596638.1596653>).++module Language.Syntactic.Sharing.Reify+    ( reifyGraph+    ) where++++import Control.Monad.Writer+import Data.IntMap as Map+import Data.IORef+import System.Mem.StableName++import Language.Syntactic+import Language.Syntactic.Sharing.Graph+import Language.Syntactic.Sharing.StableName++++-- | Shorthand used by 'reifyGraphM'+--+-- Writes out a list of encountered nodes and returns the top expression.+type GraphMonad dom a = WriterT+    [(NodeId, ASTB (NodeDomain dom) (Sat dom))]+    IO+    (AST (NodeDomain dom) a)++++reifyGraphM :: forall dom a . Constrained dom+    => (forall a . ASTF dom a -> Bool)+    -> IORef NodeId+    -> IORef (History (AST dom))+    -> ASTF dom a+    -> GraphMonad dom (Full a)++reifyGraphM canShare nSupp history = reifyNode+  where+    reifyNode :: ASTF dom b -> GraphMonad dom (Full b)+    reifyNode a+      | Dict <- exprDict a = case canShare a of+          False -> reifyRec a+          True | a `seq` True -> do+            st   <- liftIO $ makeStableName a+            hist <- liftIO $ readIORef history+            case lookHistory hist (StName st) of+              Just n -> return $ injC $ Node n+              _ -> do+                n  <- fresh nSupp+                liftIO $ modifyIORef history $ remember (StName st) n+                a' <- reifyRec a+                tell [(n, ASTB a')]+                return $ injC $ Node n++    reifyRec :: Sat dom (DenResult b) => AST dom b -> GraphMonad dom b+    reifyRec (f :$ a) = liftM2 (:$) (reifyRec f) (reifyNode a)+    reifyRec (Sym s)  = return $ Sym $ C' $ InjR s++++-- | Convert a syntax tree to a sharing-preserving graph+--+-- This function is not referentially transparent (hence the 'IO'). However, it+-- is well-behaved in the sense that the worst thing that could happen is that+-- sharing is lost. It is not possible to get false sharing.+reifyGraph :: Constrained dom+    => (forall a . ASTF dom a -> Bool)+         -- ^ A function that decides whether a given node can be shared+    -> ASTF dom a+    -> IO (ASG dom a)+reifyGraph canShare a = do+    nSupp   <- newIORef 0+    history <- newIORef empty+    (a',ns) <- runWriterT $ reifyGraphM canShare nSupp history a+    n       <- readIORef nSupp+    return (ASG a' ns n)+
+ src/Language/Syntactic/Sharing/ReifyHO.hs view
@@ -0,0 +1,109 @@+-- | This module is similar to "Language.Syntactic.Sharing.Reify", but operates+-- on @`AST` (`HODomain` dom p)@ rather than a general 'AST'. The reason for+-- having this module is that when using 'HODomain', it is important to do+-- simultaneous sharing analysis and 'HOLambda' reification. Obviously we cannot+-- do sharing analysis first (using+-- 'Language.Syntactic.Sharing.Reify.reifyGraph' from+-- "Language.Syntactic.Sharing.Reify"), since it needs to be able to look inside+-- 'HOLambda'. On the other hand, if we did 'HOLambda' reification first (using+-- 'reify'), we would destroy the sharing.+--+-- This module is based on the paper /Type-Safe Observable Sharing in Haskell/+-- (Andy Gill, 2009, <http://dx.doi.org/10.1145/1596638.1596653>).++module Language.Syntactic.Sharing.ReifyHO+    ( reifyGraphTop+    , reifyGraph+    ) where++++import Control.Monad.Writer+import Data.IntMap as Map+import Data.IORef+import System.Mem.StableName++import Language.Syntactic+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Sharing.Graph+import Language.Syntactic.Sharing.StableName+import qualified Language.Syntactic.Sharing.Reify  -- For Haddock++++-- | Shorthand used by 'reifyGraphM'+--+-- Writes out a list of encountered nodes and returns the top expression.+type GraphMonad dom p pVar a = WriterT+    [(NodeId, ASTB (NodeDomain (FODomain dom p pVar)) p)]+    IO+    (AST (NodeDomain (FODomain dom p pVar)) a)++++reifyGraphM :: forall dom p pVar a+    .  (forall a . ASTF (HODomain dom p pVar) a -> Bool)+    -> IORef VarId+    -> IORef NodeId+    -> IORef (History (AST (HODomain dom p pVar)))+    -> ASTF (HODomain dom p pVar) a+    -> GraphMonad dom p pVar (Full a)++reifyGraphM canShare vSupp nSupp history = reifyNode+  where+    reifyNode :: ASTF (HODomain dom p pVar) b -> GraphMonad dom p pVar (Full b)+    reifyNode a+      | Dict <- exprDict a = case canShare a of+          False -> reifyRec a+          True | a `seq` True -> do+            st   <- liftIO $ makeStableName a+            hist <- liftIO $ readIORef history+            case lookHistory hist (StName st) of+              Just n -> return $ injC $ Node n+              _ -> do+                n  <- fresh nSupp+                liftIO $ modifyIORef history $ remember (StName st) n+                a' <- reifyRec a+                tell [(n, ASTB a')]+                return $ injC $ Node n++    reifyRec :: AST (HODomain dom p pVar) b -> GraphMonad dom p pVar b+    reifyRec (f :$ a)            = liftM2 (:$) (reifyRec f) (reifyNode a)+    reifyRec (Sym (C' (InjR a))) = return $ Sym $ C' $ InjR $ C' $ InjR a+    reifyRec (Sym (C' (InjL (HOLambda f)))) = do+        v    <- fresh vSupp+        body <- reifyNode $ f $ injC $ symType pVar $ C' (Variable v)+        return $ injC (symType pLam $ SubConstr2 (Lambda v)) :$ body+      where+        pVar = P::P (Variable :|| pVar)+        pLam = P::P (CLambda pVar)++++-- | Convert a syntax tree to a sharing-preserving graph+reifyGraphTop+    :: (forall a . ASTF (HODomain dom p pVar) a -> Bool)+    -> ASTF (HODomain dom p pVar) a+    -> IO (ASG (FODomain dom p pVar) a, VarId)+reifyGraphTop canShare a = do+    vSupp   <- newIORef 0+    nSupp   <- newIORef 0+    history <- newIORef empty+    (a',ns) <- runWriterT $ reifyGraphM canShare vSupp nSupp history a+    v       <- readIORef vSupp+    n       <- readIORef nSupp+    return (ASG a' ns n, v)++-- | Reifying an n-ary syntactic function to a sharing-preserving graph+--+-- This function is not referentially transparent (hence the 'IO'). However, it+-- is well-behaved in the sense that the worst thing that could happen is that+-- sharing is lost. It is not possible to get false sharing.+reifyGraph :: Syntactic a (HODomain dom p pVar)+    => (forall a . ASTF (HODomain dom p pVar) a -> Bool)+         -- ^ A function that decides whether a given node can be shared+    -> a+    -> IO (ASG (FODomain dom p pVar) (Internal a), VarId)+reifyGraph canShare = reifyGraphTop canShare . desugar+
+ src/Language/Syntactic/Sharing/SimpleCodeMotion.hs view
@@ -0,0 +1,224 @@+-- | Simple code motion transformation performing common sub-expression elimination and variable+-- hoisting. Note that the implementation is very inefficient.+--+-- The code is based on an implementation by Gergely Dévai.++module Language.Syntactic.Sharing.SimpleCodeMotion+    ( PrjDict (..)+    , InjDict (..)+    , MkInjDict+    , codeMotion+    , prjDictFO+    , reifySmart+    , mkInjDictFO+    ) where++++import Control.Monad.State+import Data.Set as Set+import Data.Typeable++import Language.Syntactic+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder++++-- | Interface for projecting binding constructs+data PrjDict dom = PrjDict+    { prjVariable :: forall sig . dom sig -> Maybe VarId+    , prjLambda   :: forall sig . dom sig -> Maybe VarId+    }++-- | Interface for injecting binding constructs+data InjDict dom a b = InjDict+    { injVariable :: VarId -> dom (Full a)+    , injLambda   :: VarId -> dom (b :-> Full (a -> b))+    , injLet      :: dom (a :-> (a -> b) :-> Full b)+    }++-- | A function that, if possible, returns an 'InjDict' for sharing a specific sub-expression. The+-- first argument is the expression to be shared, and the second argument the expression in which it+-- will be shared.+--+-- This function makes the caller of 'codeMotion' responsible for making sure that the necessary+-- type constraints are fulfilled (otherwise 'Nothing' is returned). It also makes it possible to+-- transfer information, e.g. from the shared expression to the introduced variable.+type MkInjDict dom = forall a b . ASTF dom a -> ASTF dom b -> Maybe (InjDict dom a b)++++-- | Substituting a sub-expression. Assumes no variable capturing in the+-- expressions involved.+substitute :: forall dom a b+    .  (ConstrainedBy dom Typeable, AlphaEq dom dom dom [(VarId,VarId)])+    => ASTF dom a  -- ^ Sub-expression to be replaced+    -> ASTF dom a  -- ^ Replacing sub-expression+    -> ASTF dom b  -- ^ Whole expression+    -> ASTF dom b+substitute x y a+    | Dict <- exprDictSub pTypeable y+    , Dict <- exprDictSub pTypeable a+    , Just y' <- gcast y, alphaEq x a = y'+    | otherwise = subst a+  where+    subst :: AST dom c -> AST dom c+    subst (f :$ a) = subst f :$ substitute x y a+    subst a = a++-- | Count the number of occurrences of a sub-expression+count :: forall dom a b+    .  AlphaEq dom dom dom [(VarId,VarId)]+    => ASTF dom a  -- ^ Expression to count+    -> ASTF dom b  -- ^ Expression to count in+    -> Int+count a b+    | alphaEq a b = 1+    | otherwise   = cnt b+  where+    cnt :: AST dom c -> Int+    cnt (f :$ b) = cnt f + count a b+    cnt _        = 0++nonTerminal :: AST dom a -> Bool+nonTerminal (_ :$ _) = True+nonTerminal _        = False++-- | Environment for the expression in the 'choose' function+data Env dom = Env+    { inLambda :: Bool  -- ^ Whether the current expression is inside a lambda+    , counter  :: ASTE dom -> Int+        -- ^ Counting the number of occurrences of an expression in the+        -- environment+    , dependencies :: Set VarId+        -- ^ The set of variables that are not allowed to occur in the chosen+        -- expression+    }++independent :: PrjDict dom -> Env dom -> AST dom a -> Bool+independent pd env (Sym (prjVariable pd -> Just v)) = not (v `member` dependencies env)+independent pd env (f :$ a) = independent pd env f && independent pd env a+independent _ _ _ = True++-- | Checks whether a sub-expression in a given environment can be lifted out+liftable :: PrjDict dom -> Env dom -> ASTF dom a -> Bool+liftable pd env a = independent pd env a && heuristic+    -- Lifting dependent expressions is semantically incorrect+  where+    heuristic =  nonTerminal a && (inLambda env || (counter env (ASTE a) > 1))++-- | Choose a sub-expression to share+choose+    :: (AlphaEq dom dom dom [(VarId,VarId)])+    => PrjDict dom+    -> ASTF dom a+    -> Maybe (ASTE dom)+choose pd a = chooseEnv pd env a+  where+    env = Env+        { inLambda     = False+        , counter      = \(ASTE b) -> count b a+        , dependencies = empty+        }++-- | Choose a sub-expression to share in an 'Env' environment+chooseEnv :: forall dom a+    .  PrjDict dom+    -> Env dom+    -> ASTF dom a+    -> Maybe (ASTE dom)+chooseEnv pd env a+    | liftable pd env a = Just (ASTE a)+chooseEnv pd env a = chooseEnvSub pd env a++-- | Like 'chooseEnv', but does not consider the top expression for sharing+chooseEnvSub+    :: PrjDict dom+    -> Env dom+    -> AST dom a+    -> Maybe (ASTE dom)+chooseEnvSub pd env (Sym lam :$ a)+    | Just v <- prjLambda pd lam+    = chooseEnv pd (env' v) a+  where+    env' v = env+        { inLambda     = True+        , dependencies = insert v (dependencies env)+        }+chooseEnvSub pd env (f :$ a) = chooseEnvSub pd env f `mplus` chooseEnv pd env a+chooseEnvSub _ _ _ = Nothing++++-- | Perform common sub-expression elimination and variable hoisting+codeMotion :: forall dom a+    .  ( ConstrainedBy dom Typeable+       , AlphaEq dom dom dom [(VarId,VarId)]+       )+    => PrjDict dom+    -> MkInjDict dom+    -> ASTF dom a+    -> State VarId (ASTF dom a)+codeMotion pd mkId a+    | Just (ASTE b) <- choose pd a, Just id <- mkId b a = share id b+    | otherwise = descend a+  where+    share :: InjDict dom b a -> ASTF dom b -> State VarId (ASTF dom a)+    share id b = do+        b' <- codeMotion pd mkId b+        v  <- get; put (v+1)+        let x = Sym (injVariable id v)+        body <- codeMotion pd mkId $ substitute b x a+        return+            $  Sym (injLet id)+            :$ b'+            :$ (Sym (injLambda id v) :$ body)++    descend :: AST dom b -> State VarId (AST dom b)+    descend (f :$ a) = liftM2 (:$) (descend f) (codeMotion pd mkId a)+    descend a        = return a++++-- | A 'PrjDict' implementation for 'FODomain'+prjDictFO :: forall dom p pVar . PrjDict (FODomain dom p pVar)+prjDictFO = PrjDict+    { prjVariable = fmap (\(C' (Variable v)) -> v)       . prjP (P::P (Variable :|| pVar))+    , prjLambda   = fmap (\(SubConstr2 (Lambda v)) -> v) . prjP (P::P (CLambda pVar))+    }++-- | Like 'reify' but with common sub-expression elimination and variable hoisting+reifySmart :: forall dom p pVar a+    .  ( AlphaEq dom dom (FODomain dom p pVar) [(VarId,VarId)]+       , Syntactic a (HODomain dom p pVar)+       , p :< Typeable+       )+    => MkInjDict (FODomain dom p pVar)+    -> a+    -> ASTF (FODomain dom p pVar) (Internal a)+reifySmart mkId = flip evalState 0 . (codeMotion prjDictFO mkId <=< reifyM . desugar)++++-- | An 'MkInjDict' implementation for 'FODomain'+--+-- The supplied function determines whether or not an expression can be shared by returning a+-- witness that the type of the expression satisfies the predicate @pVar@.+mkInjDictFO :: forall dom pVar . (Let :<: dom)+    => (forall a . ASTF (FODomain dom Typeable pVar) a -> Maybe (Dict (pVar a)))+    -> MkInjDict (FODomain dom Typeable pVar)+mkInjDictFO canShare a b+    | Dict <- exprDict a+    , Dict <- exprDict b+    , Just Dict <- canShare a+    = Just $ InjDict+        { injVariable = \v -> injC (symType pVar $ C' (Variable v))+        , injLambda   = \v -> injC (symType pLam $ SubConstr2 (Lambda v))+        , injLet      = C' $ inj Let+        }+  where+    pVar = P::P (Variable :|| pVar)+    pLam = P::P (CLambda pVar)+mkInjDictFO _ _ _ = Nothing+
+ src/Language/Syntactic/Sharing/StableName.hs view
@@ -0,0 +1,53 @@+module Language.Syntactic.Sharing.StableName where++++import Control.Monad.IO.Class+import Data.IntMap as Map+import Data.IORef+import System.Mem.StableName+import Unsafe.Coerce++import Language.Syntactic+import Language.Syntactic.Sharing.Graph++++-- | 'StableName' of a @(c (Full a))@ with hidden result type+data StName c+  where+    StName :: StableName (c (Full a)) -> StName c++instance Eq (StName c)+  where+    StName a == StName b = a == unsafeCoerce b+      -- This is "probably" safe according to+      -- <http://www.haskell.org/pipermail/glasgow-haskell-users/2012-August/022758.html>++      -- TODO In future, use `eqStableName`. It should be in GHC 7.8.1.++hash :: StName c -> Int+hash (StName st) = hashStableName st++-- | A hash table from 'StName' to 'NodeId' (with 'hash' as the hashing+-- function). I.e. it is assumed that the 'StName's at each entry all have the+-- same hash, and that this number is equal to the entry's key.+type History c = IntMap [(StName c, NodeId)]++-- | Lookup a name in the history+lookHistory :: History c -> StName c -> Maybe NodeId+lookHistory hist st = case Map.lookup (hash st) hist of+    Nothing   -> Nothing+    Just list -> Prelude.lookup st list++-- | Insert the name into the history+remember :: StName c -> NodeId -> History c -> History c+remember st n hist = insertWith (++) (hash st) [(st,n)] hist++-- | Return a fresh identifier from the given supply+fresh :: (Enum a, MonadIO m) => IORef a -> m a+fresh aRef = do+    a <- liftIO $ readIORef aRef+    liftIO $ writeIORef aRef (succ a)+    return a+
+ src/Language/Syntactic/Sharing/Utils.hs view
@@ -0,0 +1,59 @@+-- | Some utility functions used by the other modules++module Language.Syntactic.Sharing.Utils where++++import Data.Array+import Data.List++++--------------------------------------------------------------------------------+-- * Difference lists+--------------------------------------------------------------------------------++-- | Difference list+type DList a = [a] -> [a]++-- | Empty list+empty :: DList a+empty = id++-- | Singleton list+single :: a -> DList a+single = (:)++fromDList :: DList a -> [a]+fromDList = ($ [])++++--------------------------------------------------------------------------------+-- * Misc.+--------------------------------------------------------------------------------++-- | Given a list @is@ of unique natural numbers, returns a function that maps+-- each number in @is@ to a unique number in the range @[0 .. length is-1]@. The+-- complexity is O(@maximum is@).+reindex :: (Integral a, Ix a) => [a] -> a -> a+reindex is = (tab!)+  where+    tab = array (0, maximum is) $ zip is [0..]++-- | Count the number of occurrences of each element in the list. The result is+-- an array mapping each element to its number of occurrences.+count :: Ix a+    => (a,a)  -- ^ Upper and lower bound on the elements to be counted+    -> [a]    -- ^ Elements to be counted+    -> Array a Int+count bnds as = accumArray (+) 0 bnds [(n,1) | n <- as]++-- | Partitions the list such that two elements are in the same sub-list if and+-- only if they satisfy the equivalence check. The complexity is O(n^2).+fullPartition :: (a -> a -> Bool) -> [a] -> [[a]]+fullPartition eq []     = []+fullPartition eq (a:as) = (a:as1) : fullPartition eq as2+  where+    (as1,as2) = partition (eq a) as+
+ src/Language/Syntactic/Sugar.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- | \"Syntactic sugar\"++module Language.Syntactic.Sugar where++++import Language.Syntactic.Syntax+import Language.Syntactic.Constraint++++-- | It is usually assumed that @(`desugar` (`sugar` a))@ has the same meaning+-- as @a@.+class Syntactic a dom | a -> dom+    -- Note: using a functional dependency rather than an associated type,+    -- because this makes it possible to make a class alias constraining dom.+    -- TODO Now that GHC allows equality super class constraints, this should be+    --      changed to an associated type.+  where+    type Internal a+    desugar :: a -> ASTF dom (Internal a)+    sugar   :: ASTF dom (Internal a) -> a++instance Syntactic (ASTF dom a) dom+  where+    type Internal (ASTF dom a) = a+    desugar = id+    sugar   = id++-- | Syntactic type casting+resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b+resugar = sugar . desugar++-- | N-ary syntactic functions+--+-- 'desugarN' has any type of the form:+--+-- > desugarN ::+-- >     ( Syntactic a dom+-- >     , Syntactic b dom+-- >     , ...+-- >     , Syntactic x dom+-- >     ) => (a -> b -> ... -> x)+-- >       -> (  ASTF dom (Internal a)+-- >          -> ASTF dom (Internal b)+-- >          -> ...+-- >          -> ASTF dom (Internal x)+-- >          )+--+-- ...and vice versa for 'sugarN'.+class SyntacticN a internal | a -> internal+  where+    desugarN :: a -> internal+    sugarN   :: internal -> a++instance (Syntactic a dom, ia ~ AST dom (Full (Internal a))) => SyntacticN a ia+  where+    desugarN = desugar+    sugarN   = sugar++instance+    ( Syntactic a dom+    , ia ~ Internal a+    , SyntacticN b ib+    ) =>+      SyntacticN (a -> b) (AST dom (Full ia) -> ib)+  where+    desugarN f = desugarN . f . sugar+    sugarN f   = sugarN . f . desugar++++-- | \"Sugared\" symbol application+--+-- 'sugarSym' has any type of the form:+--+-- > sugarSym ::+-- >     ( expr :<: AST dom+-- >     , Syntactic a dom+-- >     , Syntactic b dom+-- >     , ...+-- >     , Syntactic x dom+-- >     ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))+-- >       -> (a -> b -> ... -> x)+sugarSym :: (sym :<: AST dom, ApplySym sig b dom, SyntacticN c b) =>+    sym sig -> c+sugarSym = sugarN . appSym++-- | \"Sugared\" symbol application+--+-- 'sugarSymC' has any type of the form:+--+-- > sugarSymC ::+-- >     ( InjectC expr (AST dom) (Internal x)+-- >     , Syntactic a dom+-- >     , Syntactic b dom+-- >     , ...+-- >     , Syntactic x dom+-- >     ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))+-- >       -> (a -> b -> ... -> x)+sugarSymC+    :: ( InjectC sym (AST dom) (DenResult sig)+       , ApplySym sig b dom+       , SyntacticN c b+       )+    => sym sig -> c+sugarSymC = sugarN . appSymC+
+ src/Language/Syntactic/Syntax.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Generic representation of typed syntax trees+--+-- For details, see: A Generic Abstract Syntax Model for Embedded Languages+-- (ICFP 2012, <http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf>).++module Language.Syntactic.Syntax+    ( -- * Syntax trees+      AST (..)+    , ASTF+    , Full (..)+    , (:->) (..)+    , size+    , ApplySym (..)+    , DenResult+      -- * Symbol domains+    , (:+:) (..)+    , Project (..)+    , (:<:) (..)+    , appSym+      -- * Type inference+    , symType+    , prjP+    ) where++++import Data.Typeable++import Data.PolyProxy++++--------------------------------------------------------------------------------+-- * Syntax trees+--------------------------------------------------------------------------------++-- | Generic abstract syntax tree, parameterized by a symbol domain+--+-- @(`AST` dom (a `:->` b))@ represents a partially applied (or unapplied)+-- symbol, missing at least one argument, while @(`AST` dom (`Full` a))@+-- represents a fully applied symbol, i.e. a complete syntax tree.+data AST dom sig+  where+    Sym  :: dom sig -> AST dom sig+    (:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig++infixl 1 :$++-- | Fully applied abstract syntax tree+type ASTF dom a = AST dom (Full a)++-- | Signature of a fully applied symbol+newtype Full a = Full { result :: a }+  deriving (Eq, Show, Typeable)++-- | Signature of a partially applied (or unapplied) symbol+newtype a :-> sig = Partial (a -> sig)+  deriving (Typeable)++infixr :->++-- | Count the number of symbols in an expression+size :: AST dom sig -> Int+size (Sym _)  = 1+size (s :$ a) = size s + size a++-- | Class for the type-level recursion needed by 'appSym'+class ApplySym sig f dom | sig dom -> f, f -> sig dom+  where+    appSym' :: AST dom sig -> f++instance ApplySym (Full a) (ASTF dom a) dom+  where+    appSym' = id++instance ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom+  where+    appSym' sym a = appSym' (sym :$ a)++-- | The result type of a symbol with the given signature+type family   DenResult sig+type instance DenResult (Full a)    = a+type instance DenResult (a :-> sig) = DenResult sig++++--------------------------------------------------------------------------------+-- * Symbol domains+--------------------------------------------------------------------------------++-- | Direct sum of two symbol domains+data (dom1 :+: dom2) a+  where+    InjL :: dom1 a -> (dom1 :+: dom2) a+    InjR :: dom2 a -> (dom1 :+: dom2) a++infixr :+:++-- | Symbol projection+class Project sub sup+  where+    -- | Partial projection from @sup@ to @sub@+    prj :: sup a -> Maybe (sub a)++instance Project sub sup => Project sub (AST sup)+  where+    prj (Sym a) = prj a+    prj _       = Nothing++instance Project expr expr+  where+    prj = Just++instance Project expr1 (expr1 :+: expr2)+  where+    prj (InjL a) = Just a+    prj _        = Nothing++instance Project expr1 expr3 => Project expr1 (expr2 :+: expr3)+  where+    prj (InjR a) = prj a+    prj _        = Nothing++-- | Symbol subsumption+class Project sub sup => sub :<: sup+  where+    -- | Injection from @sub@ to @sup@+    inj :: sub a -> sup a++instance (sub :<: sup) => (sub :<: AST sup)+  where+    inj = Sym . inj++instance (expr :<: expr)+  where+    inj = id++instance (expr1 :<: (expr1 :+: expr2))+  where+    inj = InjL++instance (expr1 :<: expr3) => (expr1 :<: (expr2 :+: expr3))+  where+    inj = InjR . inj++-- The reason for separating the `Project` and `(:<:)` classes is that there are+-- types that can be instances of the former but not the latter due to type+-- constraints on the `a` type.++-- | Generic symbol application+--+-- 'appSym' has any type of the form:+--+-- > appSym :: (expr :<: AST dom)+-- >     => expr (a :-> b :-> ... :-> Full x)+-- >     -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)+appSym :: (ApplySym sig f dom, sym :<: AST dom) => sym sig -> f+appSym = appSym' . inj++++--------------------------------------------------------------------------------+-- * Type inference+--------------------------------------------------------------------------------++-- | Constrain a symbol to a specific type+symType :: P sym -> sym sig -> sym sig+symType _ = id++-- | Projection to a specific symbol type+prjP :: Project sub sup => P sub -> sup sig -> Maybe (sub sig)+prjP _ = prj+
+ src/Language/Syntactic/Traversal.hs view
@@ -0,0 +1,183 @@+-- | Generic traversals of 'AST' terms++module Language.Syntactic.Traversal+    ( gmapQ+    , gmapT+    , everywhereUp+    , everywhereDown+    , Args (..)+    , listArgs+    , mapArgs+    , mapArgsA+    , mapArgsM+    , appArgs+    , listFold+    , match+    , query+    , simpleMatch+    , fold+    , simpleFold+    , matchTrans+    , WrapFull (..)+    ) where++++import Control.Applicative++import Language.Syntactic.Syntax++++-- | Map a function over all immediate sub-terms (corresponds to the function+-- with the same name in Scrap Your Boilerplate)+gmapT :: forall dom+      .  (forall a . ASTF dom a -> ASTF dom a)+      -> (forall a . ASTF dom a -> ASTF dom a)+gmapT f a = go a+  where+    go :: forall a . AST dom a -> AST dom a+    go (s :$ a) = go s :$ f a+    go s        = s++-- | Map a function over all immediate sub-terms, collecting the results in a+-- list (corresponds to the function with the same name in Scrap Your+-- Boilerplate)+gmapQ :: forall dom b+      .  (forall a . ASTF dom a -> b)+      -> (forall a . ASTF dom a -> [b])+gmapQ f a = go a+  where+    go :: forall a . AST dom a -> [b]+    go (s :$ a) = f a : go s+    go _        = []++-- | Apply a transformation bottom-up over an expression (corresponds to+-- @everywhere@ in Scrap Your Boilerplate)+everywhereUp+    :: (forall a . ASTF dom a -> ASTF dom a)+    -> (forall a . ASTF dom a -> ASTF dom a)+everywhereUp f = f . gmapT (everywhereUp f)++-- | Apply a transformation top-down over an expression (corresponds to+-- @everywhere'@ in Scrap Your Boilerplate)+everywhereDown+    :: (forall a . ASTF dom a -> ASTF dom a)+    -> (forall a . ASTF dom a -> ASTF dom a)+everywhereDown f = gmapT (everywhereDown f) . f++-- | List of symbol arguments+data Args c sig+  where+    Nil  :: Args c (Full a)+    (:*) :: c (Full a) -> Args c sig -> Args c (a :-> sig)++infixr :*++-- | Map a function over an 'Args' list and collect the results in an ordinary+-- list+listArgs :: (forall a . c (Full a) -> b) -> Args c sig -> [b]+listArgs f Nil       = []+listArgs f (a :* as) = f a : listArgs f as++-- | Map a function over an 'Args' list+mapArgs+    :: (forall a   . c1 (Full a) -> c2 (Full a))+    -> (forall sig . Args c1 sig -> Args c2 sig)+mapArgs f Nil       = Nil+mapArgs f (a :* as) = f a :* mapArgs f as++-- | Map an applicative function over an 'Args' list+mapArgsA :: Applicative f+    => (forall a   . c1 (Full a) -> f (c2 (Full a)))+    -> (forall sig . Args c1 sig -> f (Args c2 sig))+mapArgsA f Nil       = pure Nil+mapArgsA f (a :* as) = (:*) <$> f a <*> mapArgsA f as++-- | Map a monadic function over an 'Args' list+mapArgsM :: Monad m+    => (forall a   . c1 (Full a) -> m (c2 (Full a)))+    -> (forall sig . Args c1 sig -> m (Args c2 sig))+mapArgsM f = unwrapMonad . mapArgsA (WrapMonad . f)++-- | Apply a (partially applied) symbol to a list of argument terms+appArgs :: AST dom sig -> Args (AST dom) sig -> ASTF dom (DenResult sig)+appArgs a Nil       = a+appArgs s (a :* as) = appArgs (s :$ a) as++-- | \"Pattern match\" on an 'AST' using a function that gets direct access to+-- the top-most symbol and its sub-trees+match :: forall dom a c+    .  ( forall sig . (a ~ DenResult sig) =>+           dom sig -> Args (AST dom) sig -> c (Full a)+       )+    -> ASTF dom a+    -> c (Full a)+match f a = go a Nil+  where+    go :: (a ~ DenResult sig) => AST dom sig -> Args (AST dom) sig -> c (Full a)+    go (Sym a)  as = f a as+    go (s :$ a) as = go s (a :* as)++query :: forall dom a c+    .  ( forall sig . (a ~ DenResult sig) =>+           dom sig -> Args (AST dom) sig -> c (Full a)+       )+    -> ASTF dom a+    -> c (Full a)+query = match+{-# DEPRECATED query "Please use `match` instead." #-}++-- | A version of 'match' with a simpler result type+simpleMatch :: forall dom a b+    .  (forall sig . (a ~ DenResult sig) => dom sig -> Args (AST dom) sig -> b)+    -> ASTF dom a+    -> b+simpleMatch f = getConst . match (\s -> Const . f s)++-- | Fold an 'AST' using an 'Args' list to hold the results of sub-terms+fold :: forall dom c+    .  (forall sig . dom sig -> Args c sig -> c (Full (DenResult sig)))+    -> (forall a   . ASTF dom a -> c (Full a))+fold f = match (\s -> f s . mapArgs (fold f))++-- | Simplified version of 'fold' for situations where all intermediate results+-- have the same type+simpleFold :: forall dom b+    .  (forall sig . dom sig -> Args (Const b) sig -> b)+    -> (forall a   . ASTF dom a                    -> b)+simpleFold f = getConst . fold (\s -> Const . f s)++-- | Fold an 'AST' using a list to hold the results of sub-terms+listFold :: forall dom b+    .  (forall sig . dom sig -> [b] -> b)+    -> (forall a   . ASTF dom a     -> b)+listFold f = simpleFold (\s -> f s . listArgs getConst)++newtype WrapAST c dom sig = WrapAST { unWrapAST :: c (AST dom sig) }+  -- Only used in the definition of 'matchTrans'++-- | A version of 'match' where the result is a transformed syntax tree,+-- wrapped in a type constructor @c@+matchTrans :: forall dom dom' c a+    .  ( forall sig . (a ~ DenResult sig) =>+           dom sig -> Args (AST dom) sig -> c (ASTF dom' a)+       )+    -> ASTF dom a+    -> c (ASTF dom' a)+matchTrans f = unWrapAST . match (\s -> WrapAST . f s)++-- | Can be used to make an arbitrary type constructor indexed by @(`Full` a)@.+-- This is useful as the type constructor parameter of 'Args'. That is, use+--+-- > Args (WrapFull c) ...+--+-- instead of+--+-- > Args c ...+--+-- if @c@ is not indexed by @(`Full` a)@.+data WrapFull c a+  where+    WrapFull :: { unwrapFull :: c a } -> WrapFull c (Full a)+
syntactic.cabal view
@@ -1,5 +1,5 @@ Name:           syntactic-Version:        1.0.1+Version:        1.2 Synopsis:       Generic abstract syntax, and utilities for embedded languages Description:    This library provides:                 .@@ -28,7 +28,7 @@                     <http://www.cse.chalmers.se/~emax/documents/axelsson2012generic-slides.pdf>                 .                 For a practical example of how to use the library, see the-                proof-of-concept implementation Feldspar EDSL in the @Examples@+                proof-of-concept implementation Feldspar EDSL in the @examples@                 directory. (The real Feldspar [2] is also implemented using                 Syntactic.)                 .@@ -49,20 +49,22 @@ Homepage:       http://projects.haskell.org/syntactic/ Category:       Language Build-type:     Simple-Cabal-version:  >=1.6+Cabal-version:  >=1.10+Tested-with:    GHC==7.6.1, GHC==7.4.2 -Extra-source-files:-  Examples/NanoFeldspar/Core.hs-  Examples/NanoFeldspar/Extra.hs-  Examples/NanoFeldspar/Vector.hs-  Examples/NanoFeldspar/Test.hs+extra-source-files:+  examples/NanoFeldspar/Core.hs+  examples/NanoFeldspar/Extra.hs+  examples/NanoFeldspar/Vector.hs+  examples/NanoFeldspar/Test.hs  source-repository head   type:     darcs   location: http://projects.haskell.org/syntactic/ -Library-  Exposed-modules:+library+  exposed-modules:+    Data.PolyProxy     Data.DynamicAlt     Language.Syntactic     Language.Syntactic.Syntax@@ -84,6 +86,8 @@     Language.Syntactic.Constructs.Monad     Language.Syntactic.Constructs.Tuple     Language.Syntactic.Frontend.Monad+    Language.Syntactic.Frontend.Tuple+    Language.Syntactic.Frontend.TupleConstrained     Language.Syntactic.Sharing.SimpleCodeMotion     Language.Syntactic.Sharing.Utils     Language.Syntactic.Sharing.Graph@@ -91,21 +95,24 @@     Language.Syntactic.Sharing.Reify     Language.Syntactic.Sharing.ReifyHO -  Other-modules:+  other-modules: -  Build-depends:+  build-depends:     array,-    base >= 4.0 && < 4.7,+    base >= 4 && < 4.7,     containers,     constraints,     data-hash,     ghc-prim,     mtl >= 2 && < 3,-    tagged,     transformers >= 0.2,     tuple >= 0.2 -  Extensions:+  hs-source-dirs: src++  default-language: Haskell2010++  default-extensions:     ConstraintKinds     DeriveDataTypeable     DeriveFunctor@@ -114,11 +121,80 @@     FunctionalDependencies     GADTs     GeneralizedNewtypeDeriving-    PatternGuards     Rank2Types     ScopedTypeVariables     StandaloneDeriving     TypeFamilies     TypeOperators     ViewPatterns++  other-extensions:+    -- Not understood by Cabal: PolyKinds+    OverlappingInstances+    UndecidableInstances++test-suite NanoFeldsparEval+  type: exitcode-stdio-1.0++  hs-source-dirs: tests examples++  main-is: NanoFeldsparEval.hs++  other-modules:++  default-language: Haskell2010++  default-extensions:+    FlexibleContexts+    FlexibleInstances+    GADTs+    MultiParamTypeClasses+    ScopedTypeVariables+    TypeFamilies+    TypeOperators+    UndecidableInstances+    ViewPatterns++  other-extensions:+    TemplateHaskell++  build-depends:+    syntactic,+    base >= 4 && < 4.7,+    QuickCheck >= 2.4 && < 3,+    test-framework >= 0.6,+    test-framework-th >= 0.2,+    test-framework-quickcheck2 >= 0.2++test-suite NanoFeldsparTree+  type: exitcode-stdio-1.0++  hs-source-dirs: tests examples++  main-is: NanoFeldsparTree.hs++  other-modules:++  default-language: Haskell2010++  default-extensions:+    FlexibleContexts+    FlexibleInstances+    GADTs+    MultiParamTypeClasses+    ScopedTypeVariables+    TypeFamilies+    TypeOperators+    UndecidableInstances+    ViewPatterns++  other-extensions:+    TemplateHaskell++  build-depends:+    syntactic,+    base >= 4 && < 4.7,+    bytestring,+    test-framework >= 0.6,+    test-framework-golden >= 1.1
+ tests/NanoFeldsparEval.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE TemplateHaskell #-}++import Test.Framework+import Test.Framework.TH+import Test.Framework.Providers.QuickCheck2++import NanoFeldspar.Core (eval)+import NanoFeldspar.Test++++prop_1 a b = eval prog1 a' b == ref a' b+  where+    a' = a `mod` 20+    ref a b = [min (i+3) b | i <- [0..a'-1]]++prop_2 a = eval prog2 a == ref a+  where+    ref a = max (min a a) (min a a)++prop_3 a b = eval prog3 a b' == ref a b'+  where+    b' = a - (b `mod` 20)+    ref a b = sum [l .. u]+      where+        l = min a b+        u = max a b++prop_4 a = eval prog4 a == ref a+  where+    ref a = let (b,c) = (a*2,a*3) in (b-c)*(c-b)++prop_5 = eval prog5 == ref+  where+    ref = as!!1 + sum as + sum as+      where+        as = map (*2) [1..20]++prop_7 a = eval prog7 a == ref a+  where+    ref a = [a .. a+9]++++main = $(defaultMainGenerator)+
+ tests/NanoFeldsparTree.hs view
@@ -0,0 +1,30 @@+import Test.Framework+import Test.Golden++import qualified Data.ByteString.Lazy.Char8 as B++import NanoFeldspar.Core (showAST)+import NanoFeldspar.Test++++mkGold1 = B.writeFile "tests/gold/prog1.txt" $ B.pack $ showAST prog1+mkGold2 = B.writeFile "tests/gold/prog2.txt" $ B.pack $ showAST prog2+mkGold3 = B.writeFile "tests/gold/prog3.txt" $ B.pack $ showAST prog3+mkGold4 = B.writeFile "tests/gold/prog4.txt" $ B.pack $ showAST prog4+mkGold5 = B.writeFile "tests/gold/prog5.txt" $ B.pack $ showAST prog5+mkGold6 = B.writeFile "tests/gold/prog6.txt" $ B.pack $ showAST prog6+mkGold7 = B.writeFile "tests/gold/prog7.txt" $ B.pack $ showAST prog7++tests = testGroup "TreeTests"+    [ goldenVsString "prog1" "tests/gold/prog1.txt" $ return $ B.pack $ showAST prog1+    , goldenVsString "prog2" "tests/gold/prog2.txt" $ return $ B.pack $ showAST prog2+    , goldenVsString "prog3" "tests/gold/prog3.txt" $ return $ B.pack $ showAST prog3+    , goldenVsString "prog4" "tests/gold/prog4.txt" $ return $ B.pack $ showAST prog4+    , goldenVsString "prog5" "tests/gold/prog5.txt" $ return $ B.pack $ showAST prog5+    , goldenVsString "prog6" "tests/gold/prog6.txt" $ return $ B.pack $ showAST prog6+    , goldenVsString "prog7" "tests/gold/prog7.txt" $ return $ B.pack $ showAST prog7+    ]++main = defaultMain [tests]+