syntactic 0.4 → 0.5
raw patch · 28 files changed
+2141/−967 lines, 28 filesdep +taggeddep +transformers
Dependencies added: tagged, transformers
Files
- Examples/ALaCarte.hs +1/−1
- Examples/MuFeldspar/Core.hs +0/−211
- Examples/MuFeldspar/Test.hs +0/−44
- Examples/MuFeldspar/Vector.hs +0/−79
- Examples/NanoFeldspar/Core.hs +251/−0
- Examples/NanoFeldspar/Test.hs +78/−0
- Examples/NanoFeldspar/Vector.hs +89/−0
- Language/Syntactic.hs +0/−2
- Language/Syntactic/Analysis/Equality.hs +15/−5
- Language/Syntactic/Analysis/Evaluation.hs +0/−3
- Language/Syntactic/Analysis/Hash.hs +0/−27
- Language/Syntactic/Features/Annotate.hs +8/−6
- Language/Syntactic/Features/Binding.hs +131/−70
- Language/Syntactic/Features/Binding/HigherOrder.hs +67/−33
- Language/Syntactic/Features/Condition.hs +32/−14
- Language/Syntactic/Features/Literal.hs +29/−15
- Language/Syntactic/Features/PrimFunc.hs +0/−183
- Language/Syntactic/Features/Symbol.hs +144/−0
- Language/Syntactic/Features/Tuple.hs +357/−44
- Language/Syntactic/Features/TupleSyntactic.hs +0/−204
- Language/Syntactic/Features/TupleSyntacticPoly.hs +138/−0
- Language/Syntactic/Sharing/Graph.hs +324/−0
- Language/Syntactic/Sharing/Reify.hs +83/−0
- Language/Syntactic/Sharing/ReifyHO.hs +116/−0
- Language/Syntactic/Sharing/StableName.hs +61/−0
- Language/Syntactic/Sharing/Utils.hs +59/−0
- Language/Syntactic/Syntax.hs +140/−15
- syntactic.cabal +18/−11
Examples/ALaCarte.hs view
@@ -4,7 +4,7 @@ {-# LANGUAGE ViewPatterns #-} -- | Demonstration of the fact that "Language.Syntactic" has the same--- functionality as /Data types à la carte/ (Wouter Swierstra, in+-- functionality as /Data types à la carte/ (Wouter Swierstra, -- /Journal of Functional Programming/, 2008) module ALaCarte where
− Examples/MuFeldspar/Core.hs
@@ -1,211 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE UndecidableInstances #-}--module MuFeldspar.Core where----import Prelude hiding (max, min)-import qualified Prelude-import Data.Typeable--import Language.Syntactic-import Language.Syntactic.Features.Literal-import Language.Syntactic.Features.PrimFunc-import Language.Syntactic.Features.Condition-import Language.Syntactic.Features.Tuple-import Language.Syntactic.Features.TupleSyntactic-import Language.Syntactic.Features.Binding-import Language.Syntactic.Features.Binding.HigherOrder--------------------------------------------------------------------------------------- * Types------------------------------------------------------------------------------------- | Convenient class alias-class (Eq a, Show a, Typeable a) => Type a-instance (Eq a, Show a, Typeable a) => Type a--type Length = Int-type Index = Int--------------------------------------------------------------------------------------- * Parallel arrays-----------------------------------------------------------------------------------data Parallel a- where- Parallel :: Parallel (Length :-> (Index -> a) :-> Full [a])--instance Render Parallel- where- render Parallel = "parallel"--instance ToTree Parallel--instance ExprEq Parallel- where- Parallel `exprEq` Parallel = True--instance Eval Parallel- where- evaluate Parallel = fromEval $ \len ixf -> Prelude.map ixf [0 .. len-1]--------------------------------------------------------------------------------------- * For loops-----------------------------------------------------------------------------------data ForLoop a- where- ForLoop :: ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)--instance ExprEq ForLoop- where- ForLoop `exprEq` ForLoop = True--instance Render ForLoop- where- render ForLoop = "forLoop"--instance ToTree ForLoop--instance Eval ForLoop- where- evaluate ForLoop = fromEval $ \len init body -> foldr body init [0 .. len-1]--------------------------------------------------------------------------------------- * Feldspar domain-----------------------------------------------------------------------------------type FeldDomain- = Literal- :+: PrimFunc- :+: Condition- :+: Tuple- :+: Select- :+: Let- :+: Parallel- :+: ForLoop--data Data a = Type a => Data { unData :: HOAST FeldDomain (Full a) }--instance Type a =>- Syntactic (Data a) (HOLambda FeldDomain :+: Variable :+: FeldDomain)- where- type Internal (Data a) = a- desugar = unData- sugar = Data---- | Specialization of the 'Syntactic' class for the Feldspar domain-class- ( Syntactic a (HOLambda FeldDomain :+: Variable :+: FeldDomain)- , Type (Internal a)- , SyntacticN a- (ASTF (HOLambda FeldDomain :+: Variable :+: FeldDomain) (Internal a))- ) =>- Syntax a--instance- ( Syntactic a (HOLambda FeldDomain :+: Variable :+: FeldDomain)- , Type (Internal a)- , SyntacticN a- (ASTF (HOLambda FeldDomain :+: Variable :+: FeldDomain) (Internal a))- ) =>- Syntax a--------------------------------------------------------------------------------------- * Back ends-----------------------------------------------------------------------------------printFeld :: Reifiable a FeldDomain internal => a -> IO ()-printFeld = printExpr . reify--drawFeld :: Reifiable a FeldDomain internal => a -> IO ()-drawFeld = drawAST . reify--eval :: Reifiable a FeldDomain internal => a -> NAryEval internal-eval = evalLambda . reify--------------------------------------------------------------------------------------- * Core library-----------------------------------------------------------------------------------value :: Syntax a => Internal a -> a-value = sugar . lit---- | For types containing some kind of \"thunk\", this function can be used to--- force computation-force :: Syntax a => a -> a-force = resugar--share :: (Syntax a, Syntax b) => a -> (a -> b) -> b-share a f = sugar $ letBind (desugar a) (desugarN f)--instance Eq (Data a)- where- Data a == Data b = reify a `alphaEq` reify b--instance Show (Data a)- where- show (Data a) = render $ reify a--instance (Type a, Num a) => Num (Data a)- where- fromInteger = value . fromInteger- abs = sugarN $ primFunc1 "abs" abs- signum = sugarN $ primFunc1 "signum" signum- (+) = sugarN $ primFunc2 "(+)" (+)- (-) = sugarN $ primFunc2 "(-)" (-)- (*) = sugarN $ primFunc2 "(*)" (*)--parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]-parallel len ixf- = sugar- $ inject Parallel- :$: desugar len- :$: lambda (desugarN ixf)--forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st-forLoop len init body- = sugar- $ inject ForLoop- :$: desugar len- :$: desugar init- :$: lambdaN (desugarN body)--arrLength :: Type a => Data [a] -> Data Length-arrLength = sugarN $ primFunc1 "arrLength" Prelude.length--getIx :: Type a => Data [a] -> Data Index -> Data a-getIx = sugarN $ primFunc2 "getIx" eval- where- eval as i- | i >= len || i < 0 = error "getIx: index out of bounds"- | otherwise = as !! i- where- len = Prelude.length as--max :: (Type a, Ord a) => Data a -> Data a -> Data a-max = sugarN $ primFunc2 "max" Prelude.max--min :: (Type a, Ord a) => Data a -> Data a -> Data a-min = sugarN $ primFunc2 "min" Prelude.min-
− Examples/MuFeldspar/Test.hs
@@ -1,44 +0,0 @@-import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)--import MuFeldspar.Core-import MuFeldspar.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 = share (min a a) $ \b -> 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]-
− Examples/MuFeldspar/Vector.hs
@@ -1,79 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--module MuFeldspar.Vector where----import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)-import qualified Prelude--import Language.Syntactic-import Language.Syntactic.Features.Binding.HigherOrder--import MuFeldspar.Core----data Vector a- where- Indexed :: Data Length -> (Data Index -> a) -> Vector a--instance Syntax a =>- Syntactic (Vector a) (HOLambda FeldDomain :+: Variable :+: FeldDomain)- 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-
+ Examples/NanoFeldspar/Core.hs view
@@ -0,0 +1,251 @@+{-# 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 features (such as+-- 'Literal' and 'Tuple') use a 'Poly' context, which means that the types are+-- not restricted. A real implementation would also probably use custom types+-- for primitive functions, since the 'Sym' feature is quite unsafe (uses only+-- a 'String' to distinguish between functions).++module NanoFeldspar.Core where++++import Prelude hiding (max, min)+import qualified Prelude+import Data.Typeable++import Language.Syntactic+import Language.Syntactic.Features.Symbol+import Language.Syntactic.Features.Literal+import Language.Syntactic.Features.Condition+import Language.Syntactic.Features.Tuple+import Language.Syntactic.Features.Binding+import Language.Syntactic.Features.Binding.HigherOrder+import Language.Syntactic.Sharing.Graph+import Language.Syntactic.Sharing.ReifyHO++++--------------------------------------------------------------------------------+-- * 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 :: Parallel (Length :-> (Index -> a) :-> Full [a])++instance IsSymbol Parallel+ where+ toSym Parallel = Sym "parallel" parallel+ where+ parallel len ixf = map ixf [0 .. len-1]++instance ExprEq Parallel where exprEq = exprEqFunc; exprHash = exprHashFunc+instance Render Parallel where renderPart = renderPartFunc+instance Eval Parallel where evaluate = evaluateFunc+instance ToTree Parallel++++--------------------------------------------------------------------------------+-- * For loops+--------------------------------------------------------------------------------++data ForLoop a+ where+ ForLoop :: ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)++instance IsSymbol ForLoop+ where+ toSym ForLoop = Sym "forLoop" forLoop+ where+ forLoop len init body = foldl (flip body) init [0 .. len-1]++instance ExprEq ForLoop where exprEq = exprEqFunc; exprHash = exprHashFunc+instance Render ForLoop where renderPart = renderPartFunc+instance Eval ForLoop where evaluate = evaluateFunc+instance ToTree ForLoop++++--------------------------------------------------------------------------------+-- * Feldspar domain+--------------------------------------------------------------------------------++-- | The Feldspar domain+type FeldDomain+ = Literal Poly+ :+: Sym+ :+: Condition Poly+ :+: Tuple Poly+ :+: Select Poly+ :+: Let Poly Poly+ :+: Parallel+ :+: ForLoop++data Data a = Type a => Data { unData :: HOAST Poly FeldDomain (Full a) }++type FeldDomainAll = HOLambda Poly FeldDomain :+: Variable Poly :+: FeldDomain++-- | 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)+ , SyntacticN a (ASTF FeldDomainAll (Internal a))+ ) =>+ Syntax a++instance+ ( Syntactic a FeldDomainAll+ , Type (Internal a)+ , SyntacticN a (ASTF FeldDomainAll (Internal a))+ ) =>+ Syntax a++++--------------------------------------------------------------------------------+-- * Back ends+--------------------------------------------------------------------------------++-- | Print the expression+printFeld :: Reifiable Poly a FeldDomain internal => a -> IO ()+printFeld = printExpr . reify++-- | Draw the syntax tree+drawFeld :: Reifiable Poly a FeldDomain internal => a -> IO ()+drawFeld = drawAST . reify++-- | A predicate deciding which constructs can be shared. Variables and literals+-- are not shared.+canShare :: HOASTF Poly FeldDomain a -> Maybe (Witness' Poly a)+canShare (prjVariable poly -> Just _) = Nothing+canShare (prjLiteral poly -> Just _) = Nothing+canShare _ = Just Witness'++-- | Draw the syntax graph after common sub-expression elimination+drawFeldCSE :: Reifiable Poly a FeldDomain internal => a -> IO ()+drawFeldCSE a = do+ (g,_) <- reifyGraph canShare a+ drawASG+ $ reindexNodesFrom0+ $ inlineSingle+ $ cse+ $ g++-- | Draw the syntax graph after observing sharing+drawFeldObs :: Reifiable Poly a FeldDomain internal => a -> IO ()+drawFeldObs a = do+ (g,_) <- reifyGraph canShare a+ drawASG+ $ reindexNodesFrom0+ $ inlineSingle+ $ g++-- | Evaluation+eval :: Reifiable Poly a FeldDomain internal => a -> NAryEval internal+eval = evalLambda . reify++++--------------------------------------------------------------------------------+-- * Core library+--------------------------------------------------------------------------------++-- | Literal+value :: Syntax a => Internal a -> a+value = sugar . lit++-- | 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 a f = sugar $ letBind (desugar a) (desugarN f)++-- | Alpha equivalence+instance Eq (Data a)+ where+ Data a == Data b = alphaEq poly (reify a) (reify b)++instance Show (Data a)+ where+ show (Data a) = render $ reify a++instance (Type a, Num a) => Num (Data a)+ where+ fromInteger = value . fromInteger+ abs = sugarN $ sym1 "abs" abs+ signum = sugarN $ sym1 "signum" signum+ (+) = sugarN $ sym2 "(+)" (+)+ (-) = sugarN $ sym2 "(-)" (-)+ (*) = sugarN $ sym2 "(*)" (*)++-- | Parallel array+parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]+parallel len ixf+ = sugar+ $ inject Parallel+ :$: desugar len+ :$: lambda (desugarN ixf)++forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st+forLoop len init body+ = sugar+ $ inject ForLoop+ :$: desugar len+ :$: desugar init+ :$: lambdaN (desugarN body)++arrLength :: Type a => Data [a] -> Data Length+arrLength = sugarN $ sym1 "arrLength" Prelude.length++-- | Array indexing+getIx :: Type a => Data [a] -> Data Index -> Data a+getIx = sugarN $ sym2 "getIx" eval+ where+ eval as i+ | i >= len || i < 0 = error "getIx: index out of bounds"+ | otherwise = as !! i+ where+ len = Prelude.length as++max :: Type a => Data a -> Data a -> Data a+max = sugarN $ sym2 "max" Prelude.max++min :: Type a => Data a -> Data a -> Data a+min = sugarN $ sym2 "min" Prelude.min+
+ Examples/NanoFeldspar/Test.hs view
@@ -0,0 +1,78 @@+import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)++import Language.Syntactic.Features.TupleSyntacticPoly++import NanoFeldspar.Core+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 = share (min a a) $ \b -> 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 a lot of 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 of 'prog7'.+ -- But the 'parallel' introduced by 'force' is shared, because 'force' only+ -- appears once.++-- Note that we're still missing a way to rebuild an expression with let+-- bindings from the graph. This is ongoing work.+
+ Examples/NanoFeldspar/Vector.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++-- | 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+import Language.Syntactic.Features.Binding.HigherOrder++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 view
@@ -8,7 +8,6 @@ , module Language.Syntactic.Analysis.Equality , module Language.Syntactic.Analysis.Render , module Language.Syntactic.Analysis.Evaluation- , module Language.Syntactic.Analysis.Hash , module Language.Syntactic.Features.Annotate ) where @@ -18,6 +17,5 @@ import Language.Syntactic.Analysis.Equality import Language.Syntactic.Analysis.Render import Language.Syntactic.Analysis.Evaluation-import Language.Syntactic.Analysis.Hash import Language.Syntactic.Features.Annotate
Language/Syntactic/Analysis/Equality.hs view
@@ -2,6 +2,8 @@ +import Data.Hash+ import Language.Syntactic.Syntax @@ -15,12 +17,22 @@ where exprEq :: expr a -> expr b -> Bool + -- | Computes a 'Hash' for an expression. Expressions that are equal+ -- according to 'exprEq' must result in the same hash:+ --+ -- @`exprEq` a b ==> `exprHash` a == `exprHash` b@+ exprHash :: expr a -> Hash++ instance ExprEq dom => ExprEq (AST dom) where exprEq (Symbol a) (Symbol b) = exprEq a b exprEq (f1 :$: a1) (f2 :$: a2) = exprEq f1 f2 && exprEq a1 a2 exprEq _ _ = False + exprHash (Symbol a) = hashInt 0 `combine` exprHash a+ exprHash (f :$: a) = hashInt 1 `combine` exprHash f `combine` exprHash a+ instance ExprEq dom => Eq (AST dom a) where (==) = exprEq@@ -31,12 +43,10 @@ exprEq (InjectR a) (InjectR b) = exprEq a b exprEq _ _ = False + exprHash (InjectL a) = hashInt 0 `combine` exprHash a+ exprHash (InjectR a) = hashInt 1 `combine` exprHash a+ instance (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a) where (==) = exprEq----eqSyn :: (Syntactic a dom, ExprEq dom) => a -> a -> Bool-eqSyn a b = desugar a `exprEq` desugar b
Language/Syntactic/Analysis/Evaluation.hs view
@@ -24,6 +24,3 @@ evalFull :: Eval dom => ASTF dom a -> a evalFull = result . evaluate -evalSyn :: (Syntactic a dom, Eval dom) => a -> Internal a-evalSyn = evalFull . desugar-
− Language/Syntactic/Analysis/Hash.hs
@@ -1,27 +0,0 @@-module Language.Syntactic.Analysis.Hash where----import Data.Hash--import Language.Syntactic.Syntax-import Language.Syntactic.Analysis.Equality----class ExprEq expr => ExprHash expr- where- -- | Computes a 'Hash' for an expression. Expressions that are equal- -- according to 'exprEq' must result in the same hash.- exprHash :: expr a -> Hash--instance ExprHash dom => ExprHash (AST dom)- where- exprHash (Symbol a) = hashInt 0 `combine` exprHash a- exprHash (f :$: a) = hashInt 1 `combine` exprHash f `combine` exprHash a--instance (ExprHash expr1, ExprHash expr2) => ExprHash (expr1 :+: expr2)- where- exprHash (InjectL a) = hashInt 0 `combine` exprHash a- exprHash (InjectR a) = hashInt 1 `combine` exprHash a-
Language/Syntactic/Features/Annotate.hs view
@@ -8,7 +8,6 @@ import Language.Syntactic.Analysis.Equality import Language.Syntactic.Analysis.Render import Language.Syntactic.Analysis.Evaluation-import Language.Syntactic.Analysis.Hash @@ -40,6 +39,7 @@ instance ExprEq expr => ExprEq (Ann info expr) where exprEq a b = annExpr a `exprEq` annExpr b+ exprHash = exprHash . annExpr instance Render expr => Render (Ann info expr) where@@ -53,12 +53,8 @@ where evaluate = evaluate . annExpr -instance ExprHash expr => ExprHash (Ann info expr)- where- exprHash = exprHash . annExpr - injectAnn :: (sub :<: sup, ConsType a) => info (EvalResult a) -> sub a -> AST (Ann info sup) a injectAnn info = Symbol . Ann info . inject@@ -70,7 +66,13 @@ c <- project b return (info, c) -getInfo :: AST (Ann info sup) a -> info (EvalResult a)+-- | Get the annotation of the top-level node+getInfo :: AST (Ann info dom) a -> info (EvalResult a) getInfo (Symbol (Ann info _)) = info getInfo (f :$: _) = getInfo f++-- | Collect the annotations of all nodes+collectInfo :: (forall a . info a -> b) -> AST (Ann info dom) a -> [b]+collectInfo coll (Symbol (Ann info _)) = [coll info]+collectInfo coll (f :$: a) = collectInfo coll f ++ collectInfo coll a
Language/Syntactic/Features/Binding.hs view
@@ -10,14 +10,19 @@ import Data.Tree import Data.Hash+import Data.Proxy import Language.Syntactic +--------------------------------------------------------------------------------+-- * Variables+--------------------------------------------------------------------------------+ -- | Variable identifier newtype VarId = VarId { varInteger :: Integer }- deriving (Eq, Ord, Num, Enum, Ix)+ deriving (Eq, Ord, Num, Real, Integral, Enum, Ix) instance Show VarId where@@ -29,95 +34,132 @@ -- | Variables-data Variable a+data Variable ctx a where- Variable :: Typeable a => VarId -> Variable (Full a)+ Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a)+ -- 'Typeable' needed by the dynamic types in 'evalLambda'. --- | Strict identifier comparison; i.e. no alpha equivalence-instance ExprEq Variable+instance WitnessCons (Variable ctx) where+ witnessCons (Variable _) = ConsWit++instance WitnessSat (Variable ctx)+ where+ type Context (Variable ctx) = ctx+ witnessSat (Variable _) = Witness'++-- | 'exprEq' 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 ExprEq (Variable ctx)+ where exprEq (Variable v1) (Variable v2) = v1==v2+ exprHash (Variable _) = hashInt 0 -instance Render Variable+instance Render (Variable ctx) where render (Variable v) = showVar v -instance ToTree Variable+instance ToTree (Variable ctx) where toTreePart [] (Variable v) = Node ("var:" ++ show v) [] +-- | Partial `Variable` projection with explicit context+prjVariable :: (Variable ctx :<: sup) =>+ Proxy ctx -> sup a -> Maybe (Variable ctx a)+prjVariable _ = project ++--------------------------------------------------------------------------------+-- * Lambda binding+--------------------------------------------------------------------------------+ -- | Lambda binding-data Lambda a+data Lambda ctx a where- Lambda :: (Typeable a, Typeable b) => VarId -> Lambda (b :-> Full (a -> b))+ Lambda :: (Typeable a, Sat ctx a) =>+ VarId -> Lambda ctx (b :-> Full (a -> b))+ -- 'Typeable' needed by the dynamic types in 'evalLambda'. --- | Strict identifier comparison; i.e. no alpha equivalence-instance ExprEq Lambda+instance WitnessCons (Lambda ctx) where+ witnessCons (Lambda _) = ConsWit++-- | 'exprEq' 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 ExprEq (Lambda ctx)+ where exprEq (Lambda v1) (Lambda v2) = v1==v2+ exprHash (Lambda _) = hashInt 0 -instance Render Lambda+instance Render (Lambda ctx) where renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> " ++ body ++ ")" -instance ToTree Lambda+instance ToTree (Lambda ctx) where toTreePart [body] (Lambda v) = Node ("Lambda " ++ show v) [body] +-- | Partial `Lambda` projection with explicit context+prjLambda :: (Lambda ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Lambda ctx a)+prjLambda _ = project --- | Alpha-equivalence on 'Lambda' expressions. Free variables are taken to be--- equvalent if they have the same identifier.-alphaEqM :: ExprEq dom- => AST (Lambda :+: Variable :+: dom) a- -> AST (Lambda :+: Variable :+: dom) b- -> Reader [(VarId,VarId)] Bool+-- | Alpha equivalence in an environment of variable equivalences. The supplied+-- equivalence function gets called when the argument expressions are not both+-- 'Variable's, both 'Lambda's or both ':$:'.+alphaEqM :: (Lambda ctx :<: dom, Variable ctx :<: dom)+ => Proxy ctx+ -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)+ -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool) --- alphaEqM (project -> Just (Variable v1)) (project -> Just (Variable v2)) = do -- Not accepted by GHC-6.12-alphaEqM (Symbol (InjectR (InjectL (Variable v1)))) (Symbol (InjectR (InjectL (Variable v2)))) = do- env <- ask- case lookup v1 env of- Nothing -> return (v1==v2) -- Free variables- Just v2' -> return (v2==v2')+-- TODO This function is not ideal, since the type says nothing about which+-- cases have been handled when calling 'eq'. -alphaEqM--- ((project -> Just (Lambda v1)) :$: a1)--- ((project -> Just (Lambda v2)) :$: a2) -- Not accepted by GHC-6.12- (Symbol (InjectL (Lambda v1)) :$: a1)- (Symbol (InjectL (Lambda v2)) :$: a2)- = local ((v1,v2):) $ alphaEqM a1 a2+alphaEqM ctx eq+ ((prjLambda ctx -> Just (Lambda v1)) :$: a1)+ ((prjLambda ctx -> Just (Lambda v2)) :$: a2) =+ local ((v1,v2):) $ alphaEqM ctx eq a1 a2 -alphaEqM (f1 :$: a1) (f2 :$: a2) = do- e <- alphaEqM f1 f2- if e then alphaEqM a1 a2 else return False+alphaEqM ctx eq+ (prjVariable ctx -> Just (Variable v1))+ (prjVariable ctx -> Just (Variable v2)) = do+ env <- ask+ case lookup v1 env of+ Nothing -> return (v1==v2) -- Free variables+ Just v2' -> return (v2==v2') -alphaEqM- (Symbol (InjectR (InjectR a)))- (Symbol (InjectR (InjectR b)))- = return (exprEq a b)+alphaEqM ctx eq (f1 :$: a1) (f2 :$: a2) = do+ e <- alphaEqM ctx eq f1 f2+ if e then alphaEqM ctx eq a1 a2 else return False -alphaEqM _ _ = return False+alphaEqM _ eq a b = eq a b -alphaEq :: ExprEq dom- => AST (Lambda :+: Variable :+: dom) a- -> AST (Lambda :+: Variable :+: dom) b- -> Bool-alphaEq a b = runReader (alphaEqM a b) []+-- | Alpha-equivalence on lambda expressions. Free variables are taken to be+-- equivalent if they have the same identifier.+alphaEq :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) =>+ Proxy ctx -> AST dom a -> AST dom b -> Bool+alphaEq ctx a b = runReader (alphaEqM ctx (\a b -> return $ exprEq a b) a b) [] --- | Evaluation of possibly open 'LambdaAST' expressions+-- | Evaluation of possibly open lambda expressions evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>- ASTF (Lambda :+: Variable :+: dom) a -> m a+ ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> m a evalLambdaM = liftM result . eval where eval :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>- AST (Lambda :+: Variable :+: dom) a -> m a--- eval (project -> Just (Variable v)) = do -- Not accepted by GHC-6.12+ AST (Lambda ctx :+: Variable ctx :+: dom) a -> m a eval (Symbol (InjectR (InjectL (Variable v)))) = do env <- ask case lookup v env of@@ -126,7 +168,6 @@ Just a -> return (Full a) _ -> return $ error "eval: internal type error" --- eval ((project -> Just (Lambda v)) :$: body) = do -- Not accepted by GHC-6.12 eval (Symbol (InjectL (Lambda v)) :$: body) = do env <- ask return@@ -144,67 +185,87 @@ --- | Evaluation of closed 'Lambda' expressions-evalLambda :: Eval dom => ASTF (Lambda :+: Variable :+: dom) a -> a+-- | Evaluation of closed lambda expressions+evalLambda :: Eval dom => ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> a evalLambda = flip runReader [] . evalLambdaM -- | The class of n-ary binding functions-class NAry a dom | a -> dom- -- Note: using a two-parameter class rather than an associated type, because- -- this makes it possible to make a class alias constraining dom. GHC- -- doesn't yet handle equality super classes.+class NAry ctx 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.+ -- GHC doesn't yet handle equality super classes. where type NAryEval a -- | N-ary binding by nested use of the supplied binder bindN- :: ( forall b c . (Typeable b, Typeable c)+ :: Proxy ctx+ -> ( forall b c . (Typeable b, Typeable c, Sat ctx b) => (ASTF dom b -> ASTF dom c) -> ASTF dom (b -> c) ) -> a -> ASTF dom (NAryEval a) -instance NAry (ASTF dom a) dom+instance Sat ctx a => NAry ctx (ASTF dom a) dom where type NAryEval (ASTF dom a) = a- bindN _ = id+ bindN _ _ = id -instance (Typeable a, NAry b dom, Typeable (NAryEval b)) =>- NAry (ASTF dom a -> b) dom+instance (Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) =>+ NAry ctx (ASTF dom a -> b) dom where type NAryEval (ASTF dom a -> b) = a -> NAryEval b- bindN lambda = lambda . (bindN lambda .)+ bindN ctx lambda = lambda . (bindN ctx lambda .) +--------------------------------------------------------------------------------+-- * Let binding+--------------------------------------------------------------------------------+ -- | Let binding-data Let a+--+-- A 'Let' expression is really just an application of a lambda binding (the+-- argument @(a -> b)@ is preferably constructed by 'Lambda').+data Let ctxa ctxb a where- Let :: Let (a :-> (a -> b) :-> Full b)+ Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> (a -> b) :-> Full b) -instance ExprEq Let+instance WitnessCons (Let ctxa ctxb) where+ witnessCons Let = ConsWit++instance WitnessSat (Let ctxa ctxb)+ where+ type Context (Let ctxa ctxb) = ctxb+ witnessSat Let = Witness'++instance ExprEq (Let ctxa ctxb)+ where exprEq Let Let = True -instance Render Let+ exprHash Let = hashInt 0++instance Render (Let ctxa ctxb) where renderPart [] Let = "Let" renderPart [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")" -instance ToTree Let+instance ToTree (Let ctxa ctxb) where toTreePart [a,body] Let = Node ("Let " ++ var) [a,body'] where Node node [body'] = body var = drop 7 node -- Drop the "Lambda " prefix -instance Eval Let+instance Eval (Let ctxa ctxb) where evaluate Let = fromEval (flip ($)) -instance ExprHash Let- where- exprHash Let = hashInt 0+-- | Partial `Let` projection with explicit context+prjLet :: (Let ctxa ctxb :<: sup) =>+ Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)+prjLet _ _ = project
Language/Syntactic/Features/Binding/HigherOrder.hs view
@@ -1,9 +1,8 @@ {-# LANGUAGE UndecidableInstances #-} -- | This module provides binding constructs using higher-order syntax and a--- function for translating back to first-order syntax. Expressions constructed--- using the exported interface are guaranteed to have a well-behaved--- translation.+-- function for translating to first-order syntax. Expressions constructed using+-- the exported interface are guaranteed to have a well-behaved translation. module Language.Syntactic.Features.Binding.HigherOrder ( Variable@@ -11,12 +10,15 @@ , Let (..) , HOLambda (..) , HOAST+ , HOASTF , lambda , lambdaN+ , letBindCtx , letBind , reifyM- , reifyHOAST+ , reifyTop , Reifiable+ , reifyCtx , reify ) where @@ -25,54 +27,79 @@ import Control.Monad.State import Data.Typeable +import Data.Proxy+ import Language.Syntactic import Language.Syntactic.Features.Binding -- | Higher-order lambda binding-data HOLambda dom a+data HOLambda ctx dom a where- HOLambda :: (Typeable a, Typeable b)- => (HOAST dom (Full a) -> HOAST dom (Full b))- -> HOLambda dom (Full (a -> b))+ HOLambda :: (Typeable a, Typeable b, Sat ctx a)+ => (HOASTF ctx dom a -> HOASTF ctx dom b)+ -> HOLambda ctx dom (Full (a -> b)) -type HOAST dom = AST (HOLambda dom :+: Variable :+: dom)+type HOAST ctx dom = AST (HOLambda ctx dom :+: Variable ctx :+: dom)+type HOASTF ctx dom a = HOAST ctx dom (Full a) +instance WitnessCons (HOLambda ctx dom)+ where+ witnessCons (HOLambda _) = ConsWit + -- | Lambda binding-lambda :: (Typeable a, Typeable b) =>- (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full (a -> b))+lambda :: (Typeable a, Typeable b, Sat ctx a) =>+ (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOASTF ctx dom (a -> b) lambda = inject . HOLambda -- | N-ary lambda binding-lambdaN :: NAry a (HOLambda dom :+: Variable :+: dom) =>- a -> HOAST dom (Full (NAryEval a))-lambdaN = bindN lambda+lambdaN :: forall ctx dom a+ . NAry ctx a (HOLambda ctx dom :+: Variable ctx :+: dom)+ => a -> HOASTF ctx dom (NAryEval a)+lambdaN = bindN (Proxy :: Proxy ctx) lambda +-- | Let binding with explicit context+letBindCtx :: forall ctxa ctxb dom a b+ . (Typeable a, Typeable b, Let ctxa ctxb :<: dom, Sat ctxa a, Sat ctxb b)+ => Proxy ctxb+ -> HOASTF ctxa dom a+ -> (HOASTF ctxa dom a -> HOASTF ctxa dom b)+ -> HOASTF ctxa dom b+letBindCtx _ a f = inject let' :$: a :$: lambda f+ where+ let' :: Let ctxa ctxb (a :-> (a -> b) :-> Full b)+ let' = Let+ -- | Let binding-letBind :: (Typeable a, Typeable b, Let :<: dom)- => HOAST dom (Full a)- -> (HOAST dom (Full a) -> HOAST dom (Full b))- -> HOAST dom (Full b)-letBind a f = inject Let :$: a :$: lambda f+letBind :: (Typeable a, Typeable b, Let Poly Poly :<: dom)+ => HOASTF Poly dom a+ -> (HOASTF Poly dom a -> HOASTF Poly dom b)+ -> HOASTF Poly dom b+letBind = letBindCtx poly -reifyM :: Typeable a- => HOAST dom a- -> State VarId (AST (Lambda :+: Variable :+: dom) a)+reifyM :: forall ctx dom a . Typeable a+ => HOAST ctx dom a+ -> State VarId (AST (Lambda ctx :+: Variable ctx :+: dom) a) reifyM (f :$: a) = liftM2 (:$:) (reifyM f) (reifyM a) reifyM (Symbol (InjectR a)) = return $ Symbol $ InjectR a reifyM (Symbol (InjectL (HOLambda f))) = do- v <- get; put (v+1)- liftM (inject (Lambda v) :$:) $ reifyM $ f $ inject $ Variable v+ v <- get; put (v+1)+ body <- reifyM $ f $ inject $ (Variable v `withContext` ctx)+ return $ inject (Lambda v `withContext` ctx) :$: body+ where+ ctx = Proxy :: Proxy ctx + -- | Translating expressions with higher-order binding to corresponding -- expressions using first-order binding-reifyHOAST :: Typeable a => HOAST dom a -> AST (Lambda :+: Variable :+: dom) a-reifyHOAST = flip evalState 0 . reifyM+reifyTop :: Typeable a =>+ HOAST ctx dom a -> AST (Lambda ctx :+: Variable ctx :+: dom) 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. @@ -81,20 +108,27 @@ -- | Convenient class alias for n-ary syntactic functions class ( SyntacticN a internal- , NAry internal (HOLambda dom :+: Variable :+: dom)+ , NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom) , Typeable (NAryEval internal) ) =>- Reifiable a dom internal | a -> dom internal+ Reifiable ctx a dom internal | a -> dom internal instance ( SyntacticN a internal- , NAry internal (HOLambda dom :+: Variable :+: dom)+ , NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom) , Typeable (NAryEval internal) ) =>- Reifiable a dom internal+ Reifiable ctx a dom internal +-- | Reifying an n-ary syntactic function with explicit context+reifyCtx :: Reifiable ctx a dom internal+ => Proxy ctx+ -> a+ -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal)+reifyCtx _ = reifyTop . lambdaN . desugarN+ -- | Reifying an n-ary syntactic function-reify :: Reifiable a dom internal =>- a -> ASTF (Lambda :+: Variable :+: dom) (NAryEval internal)-reify = reifyHOAST . lambdaN . desugarN+reify :: Reifiable Poly a dom internal =>+ a -> ASTF (Lambda Poly :+: Variable Poly :+: dom) (NAryEval internal)+reify = reifyCtx poly
Language/Syntactic/Features/Condition.hs view
@@ -5,41 +5,59 @@ import Data.Hash+import Data.Proxy import Language.Syntactic -data Condition a+data Condition ctx a where- Condition :: Condition (Bool :-> a :-> a :-> Full a)+ Condition :: Sat ctx a => Condition ctx (Bool :-> a :-> a :-> Full a) -instance ExprEq Condition+instance WitnessCons (Condition ctx) where+ witnessCons Condition = ConsWit++instance WitnessSat (Condition ctx)+ where+ type Context (Condition ctx) = ctx+ witnessSat Condition = Witness'++instance ExprEq (Condition ctx)+ where exprEq Condition Condition = True+ exprHash Condition = hashInt 0 -instance Render Condition+instance Render (Condition ctx) where render Condition = "condition" -instance ToTree Condition+instance ToTree (Condition ctx) -instance Eval Condition+instance Eval (Condition ctx) where evaluate Condition = fromEval $ \cond tHEN eLSE -> if cond then tHEN else eLSE -instance ExprHash Condition- where- exprHash Condition = hashInt 0 ---- | Conditional expression-condition :: (Condition :<: dom, Syntactic a dom) =>- ASTF dom Bool -> a -> a -> a-condition cond tHEN eLSE = sugar $ inject Condition+-- | Conditional expression with explicit context+conditionCtx+ :: (Sat ctx (Internal a), Syntactic a dom, Condition ctx :<: dom)+ => Proxy ctx -> ASTF dom Bool -> a -> a -> a+conditionCtx ctx cond tHEN eLSE = sugar $ inject (Condition `withContext` ctx) :$: cond :$: desugar tHEN :$: desugar eLSE++-- | Conditional expression+condition :: (Condition Poly :<: dom, Syntactic a dom) =>+ ASTF dom Bool -> a -> a -> a+condition = conditionCtx poly++-- | Partial `Condition` projection with explicit context+prjCondition :: (Condition ctx :<: sup) =>+ Proxy ctx -> sup a -> Maybe (Condition ctx a)+prjCondition _ = project
Language/Syntactic/Features/Literal.hs view
@@ -7,43 +7,57 @@ import Data.Typeable import Data.Hash+import Data.Proxy import Language.Syntactic -data Literal a+data Literal ctx a where- Literal :: (Eq a, Show a, Typeable a) => a -> Literal (Full a)+ Literal :: (Eq a, Show a, Typeable a, Sat ctx a) =>+ a -> Literal ctx (Full a) -instance ExprEq Literal+instance WitnessCons (Literal ctx) where+ witnessCons (Literal _) = ConsWit++instance WitnessSat (Literal ctx)+ where+ type Context (Literal ctx) = ctx+ witnessSat (Literal _) = Witness'++instance ExprEq (Literal ctx)+ where Literal a `exprEq` Literal b = case cast a of Just a' -> a'==b Nothing -> False -instance Render Literal+ exprHash (Literal a) = hash (show a)++instance Render (Literal ctx) where render (Literal a) = show a -instance ToTree Literal+instance ToTree (Literal ctx) -instance Eval Literal+instance Eval (Literal ctx) where evaluate (Literal a) = fromEval a -instance ExprHash Literal- where- exprHash (Literal a) = hash (show a) +-- | Literal with explicit context+litCtx :: (Eq a, Show a, Typeable a, Sat ctx a, Literal ctx :<: dom) =>+ Proxy ctx -> a -> ASTF dom a+litCtx ctx = inject . (`withContext` ctx) . Literal -- | Literal-lit :: (Eq a, Show a, Typeable a, Literal :<: dom) => a -> ASTF dom a-lit = inject . Literal+lit :: (Eq a, Show a, Typeable a, Literal Poly :<: dom) => a -> ASTF dom a+lit = litCtx poly --- | Annotated literal-litAnn :: (Eq a, Show a, Typeable a, Literal :<: dom) =>- info a -> a -> AnnSTF info dom a-litAnn info = injectAnn info . Literal+-- | Partial literal projection with explicit context+prjLiteral :: (Literal ctx :<: sup) =>+ Proxy ctx -> sup a -> Maybe (Literal ctx a)+prjLiteral _ = project
− Language/Syntactic/Features/PrimFunc.hs
@@ -1,183 +0,0 @@--- | Primitive functions--module Language.Syntactic.Features.PrimFunc where----import Data.Typeable--import Data.Hash--import Language.Syntactic----data PrimFunc a- where- PrimFunc :: ConsType b =>- String -> (ConsEval (a :-> b)) -> PrimFunc (a :-> b)--instance ExprEq PrimFunc- where- PrimFunc f1 _ `exprEq` PrimFunc f2 _ = f1==f2--instance Render PrimFunc- where- renderPart [] (PrimFunc name _) = name- renderPart args (PrimFunc 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 ToTree PrimFunc--instance Eval PrimFunc- where- evaluate (PrimFunc _ f) = fromEval f--instance ExprHash PrimFunc- where- exprHash (PrimFunc name _) = hash name----primFunc1- :: ( Typeable a- , PrimFunc :<: dom- )- => String- -> (a -> b)- -> ASTF dom a- -> ASTF dom b-primFunc1 name f a = inject (PrimFunc name f) :$: a--primFunc2- :: ( Typeable a- , Typeable b- , PrimFunc :<: dom- )- => String- -> (a -> b -> c)- -> ASTF dom a- -> ASTF dom b- -> ASTF dom c-primFunc2 name f a b = inject (PrimFunc name f) :$: a :$: b--primFunc3- :: ( Typeable a- , Typeable b- , Typeable c- , PrimFunc :<: dom- )- => String- -> (a -> b -> c -> d)- -> ASTF dom a- -> ASTF dom b- -> ASTF dom c- -> ASTF dom d-primFunc3 name f a b c = inject (PrimFunc name f) :$: a :$: b :$: c--primFunc4- :: ( Typeable a- , Typeable b- , Typeable c- , Typeable d- , PrimFunc :<: dom- )- => String- -> (a -> b -> c -> d -> e)- -> ASTF dom a- -> ASTF dom b- -> ASTF dom c- -> ASTF dom d- -> ASTF dom e-primFunc4 name f a b c d = inject (PrimFunc name f) :$: a :$: b :$: c :$: d--primFuncAnn1- :: ( Typeable a- , PrimFunc :<: dom- )- => String- -> (a -> b)- -> info b- -> AnnSTF info dom a- -> AnnSTF info dom b-primFuncAnn1 name f ib a = injectAnn ib (PrimFunc name f) :$: a--primFuncAnn2- :: ( Typeable a- , Typeable b- , PrimFunc :<: dom- )- => String- -> (a -> b -> c)- -> info c- -> AnnSTF info dom a- -> AnnSTF info dom b- -> AnnSTF info dom c-primFuncAnn2 name f ic a b = injectAnn ic (PrimFunc name f) :$: a :$: b--primFuncAnn3- :: ( Typeable a- , Typeable b- , Typeable c- , PrimFunc :<: dom- )- => String- -> (a -> b -> c -> d)- -> info d- -> AnnSTF info dom a- -> AnnSTF info dom b- -> AnnSTF info dom c- -> AnnSTF info dom d-primFuncAnn3 name f id a b c =- injectAnn id (PrimFunc name f) :$: a :$: b :$: c--primFuncAnn4- :: ( Typeable a- , Typeable b- , Typeable c- , Typeable d- , PrimFunc :<: dom- )- => String- -> (a -> b -> c -> d -> e)- -> info e- -> AnnSTF info dom a- -> AnnSTF info dom b- -> AnnSTF info dom c- -> AnnSTF info dom d- -> AnnSTF info dom e-primFuncAnn4 name f ie a b c d =- injectAnn ie (PrimFunc name f) :$: a :$: b :$: c :$: d------ | Class of expressions that can be treated as primitive functions-class IsFunction expr- where- toFunction :: expr a -> PrimFunc a---- | Default implementation of 'exprEq'-exprEqFunc :: IsFunction expr => expr a -> expr b -> Bool-exprEqFunc a b = exprEq (toFunction a) (toFunction b)---- | Default implementation of 'renderPart'-renderPartFunc :: IsFunction expr => [String] -> expr a -> String-renderPartFunc args = renderPart args . toFunction---- | Default implementation of 'evaluate'-evaluateFunc :: IsFunction expr => expr a -> a-evaluateFunc = evaluate . toFunction---- | Default implementation of 'exprHash'-exprHashFunc :: IsFunction expr => expr a -> Hash-exprHashFunc = exprHash . toFunction-
+ Language/Syntactic/Features/Symbol.hs view
@@ -0,0 +1,144 @@+-- | Simple symbols+--+-- 'Sym' provides a simple way to make syntactic symbols for prototyping.+-- However, note that 'Sym' is quite unsafe as it only uses 'String' to+-- distinguish between different symbols. Also, 'Sym' has a very free type that+-- allows any number of arguments.++module Language.Syntactic.Features.Symbol where++++import Data.Typeable++import Data.Hash++import Language.Syntactic++++data Sym a+ where+ Sym :: ConsType a => String -> ConsEval a -> Sym a++instance WitnessCons Sym+ where+ witnessCons (Sym _ _) = ConsWit++instance ExprEq Sym+ where+ exprEq (Sym a _) (Sym b _) = a==b+ exprHash (Sym name _) = hash name++instance Render Sym+ where+ renderPart [] (Sym name _) = name+ renderPart args (Sym 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 ToTree Sym++instance Eval Sym+ where+ evaluate (Sym _ a) = fromEval a++++-- | A zero-argument symbol+sym0+ :: ( Typeable a+ , Sym :<: dom+ )+ => String+ -> a+ -> ASTF dom a+sym0 name a = inject (Sym name a)++-- | A one-argument symbol+sym1+ :: ( Typeable a+ , Sym :<: dom+ )+ => String+ -> (a -> b)+ -> ASTF dom a+ -> ASTF dom b+sym1 name f a = inject (Sym name f) :$: a++-- | A two-argument symbol+sym2+ :: ( Typeable a+ , Typeable b+ , Sym :<: dom+ )+ => String+ -> (a -> b -> c)+ -> ASTF dom a+ -> ASTF dom b+ -> ASTF dom c+sym2 name f a b = inject (Sym name f) :$: a :$: b++-- | A three-argument symbol+sym3+ :: ( Typeable a+ , Typeable b+ , Typeable c+ , Sym :<: dom+ )+ => String+ -> (a -> b -> c -> d)+ -> ASTF dom a+ -> ASTF dom b+ -> ASTF dom c+ -> ASTF dom d+sym3 name f a b c = inject (Sym name f) :$: a :$: b :$: c++-- | A four-argument symbol+sym4+ :: ( Typeable a+ , Typeable b+ , Typeable c+ , Typeable d+ , Sym :<: dom+ )+ => String+ -> (a -> b -> c -> d -> e)+ -> ASTF dom a+ -> ASTF dom b+ -> ASTF dom c+ -> ASTF dom d+ -> ASTF dom e+sym4 name f a b c d = inject (Sym name f) :$: a :$: b :$: c :$: d++++-- | Class of expressions that can be treated as symbols+class IsSymbol expr+ where+ toSym :: expr a -> Sym a++-- | Default implementation of 'exprEq'+exprEqFunc :: IsSymbol expr => expr a -> expr b -> Bool+exprEqFunc a b = exprEq (toSym a) (toSym b)++-- | Default implementation of 'exprHash'+exprHashFunc :: IsSymbol expr => expr a -> Hash+exprHashFunc = exprHash . toSym++-- | Default implementation of 'renderPart'+renderPartFunc :: IsSymbol expr => [String] -> expr a -> String+renderPartFunc args = renderPart args . toSym++-- | Default implementation of 'evaluate'+evaluateFunc :: IsSymbol expr => expr a -> a+evaluateFunc = evaluate . toSym+
Language/Syntactic/Features/Tuple.hs view
@@ -1,73 +1,249 @@--- | Construction and selection of tuples+-- | Construction and projection of tuples in the object language+--+-- The function pairs @desugarTupX@/@sugarTupX@ could be used directly in+-- 'Syntactic' instances if it wasn't for the extra @(`Proxy` ctx)@ arguments.+-- For this reason, 'Syntactic' instances have to be written manually for each+-- context. The module "Language.Syntactic.Features.TupleSyntacticPoly" provides+-- instances for a 'Poly' context. The exact same code can be used to make+-- instances for other contexts -- just copy/paste and replace 'Poly' and 'poly'+-- with the desired context (and probably add an extra constraint in the class+-- contexts). module Language.Syntactic.Features.Tuple where import Data.Hash+import Data.Proxy import Data.Tuple.Select import Language.Syntactic-import Language.Syntactic.Features.PrimFunc+import Language.Syntactic.Features.Symbol +--------------------------------------------------------------------------------+-- * Construction+--------------------------------------------------------------------------------+ -- | Expressions for constructing tuples-data Tuple a+data Tuple ctx a 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))+ Tup2 :: Sat ctx (a,b) => Tuple ctx (a :-> b :-> Full (a,b))+ Tup3 :: Sat ctx (a,b,c) => Tuple ctx (a :-> b :-> c :-> Full (a,b,c))+ Tup4 :: Sat ctx (a,b,c,d) => Tuple ctx (a :-> b :-> c :-> d :-> Full (a,b,c,d))+ Tup5 :: Sat ctx (a,b,c,d,e) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))+ Tup6 :: Sat ctx (a,b,c,d,e,f) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))+ Tup7 :: Sat ctx (a,b,c,d,e,f,g) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g)) -instance IsFunction Tuple+instance WitnessCons (Tuple ctx) where- toFunction Tup2 = PrimFunc "tup2" (,)- toFunction Tup3 = PrimFunc "tup3" (,,)- toFunction Tup4 = PrimFunc "tup4" (,,,)- toFunction Tup5 = PrimFunc "tup5" (,,,,)- toFunction Tup6 = PrimFunc "tup6" (,,,,,)- toFunction Tup7 = PrimFunc "tup7" (,,,,,,)+ witnessCons Tup2 = ConsWit+ witnessCons Tup3 = ConsWit+ witnessCons Tup4 = ConsWit+ witnessCons Tup5 = ConsWit+ witnessCons Tup6 = ConsWit+ witnessCons Tup7 = ConsWit -instance ExprEq Tuple where exprEq = exprEqFunc-instance Render Tuple where renderPart = renderPartFunc-instance Eval Tuple where evaluate = evaluateFunc-instance ExprHash Tuple where exprHash = exprHashFunc-instance ToTree Tuple+instance WitnessSat (Tuple ctx)+ where+ type Context (Tuple ctx) = ctx+ witnessSat Tup2 = Witness'+ witnessSat Tup3 = Witness'+ witnessSat Tup4 = Witness'+ witnessSat Tup5 = Witness'+ witnessSat Tup6 = Witness'+ witnessSat Tup7 = Witness' +instance IsSymbol (Tuple ctx)+ where+ toSym Tup2 = Sym "tup2" (,)+ toSym Tup3 = Sym "tup3" (,,)+ toSym Tup4 = Sym "tup4" (,,,)+ toSym Tup5 = Sym "tup5" (,,,,)+ toSym Tup6 = Sym "tup6" (,,,,,)+ toSym Tup7 = Sym "tup7" (,,,,,,)++instance ExprEq (Tuple ctx) where exprEq = exprEqFunc; exprHash = exprHashFunc+instance Render (Tuple ctx) where renderPart = renderPartFunc+instance Eval (Tuple ctx) where evaluate = evaluateFunc+instance ToTree (Tuple ctx)++-- | Partial `Tuple` projection with explicit context+prjTuple :: (Tuple ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Tuple ctx a)+prjTuple _ = project++++desugarTup2+ :: ( Syntactic a dom+ , Syntactic b dom+ , Sat ctx (Internal a, Internal b)+ , Tuple ctx :<: dom+ )+ => Proxy ctx+ -> (a,b)+ -> ASTF dom (Internal a, Internal b)+desugarTup2 ctx (a,b) = inject (Tup2 `withContext` ctx)+ :$: desugar a+ :$: desugar b++desugarTup3+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Sat ctx (Internal a, Internal b, Internal c)+ , Tuple ctx :<: dom+ )+ => Proxy ctx+ -> (a,b,c)+ -> ASTF dom (Internal a, Internal b, Internal c)+desugarTup3 ctx (a,b,c) = inject (Tup3 `withContext` ctx)+ :$: desugar a+ :$: desugar b+ :$: desugar c++desugarTup4+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Sat ctx (Internal a, Internal b, Internal c, Internal d)+ , Tuple ctx :<: dom+ )+ => Proxy ctx+ -> (a,b,c,d)+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d)+desugarTup4 ctx (a,b,c,d) = inject (Tup4 `withContext` ctx)+ :$: desugar a+ :$: desugar b+ :$: desugar c+ :$: desugar d++desugarTup5+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e)+ , Tuple ctx :<: dom+ )+ => Proxy ctx+ -> (a,b,c,d,e)+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)+desugarTup5 ctx (a,b,c,d,e) = inject (Tup5 `withContext` ctx)+ :$: desugar a+ :$: desugar b+ :$: desugar c+ :$: desugar d+ :$: desugar e++desugarTup6+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)+ , Tuple ctx :<: dom+ )+ => Proxy ctx+ -> (a,b,c,d,e,f)+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)+desugarTup6 ctx (a,b,c,d,e,f) = inject (Tup6 `withContext` ctx)+ :$: desugar a+ :$: desugar b+ :$: desugar c+ :$: desugar d+ :$: desugar e+ :$: desugar f++desugarTup7+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , Syntactic g dom+ , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)+ , Tuple ctx :<: dom+ )+ => Proxy ctx+ -> (a,b,c,d,e,f,g)+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)+desugarTup7 ctx (a,b,c,d,e,f,g) = inject (Tup7 `withContext` ctx)+ :$: desugar a+ :$: desugar b+ :$: desugar c+ :$: desugar d+ :$: desugar e+ :$: desugar f+ :$: desugar g++++--------------------------------------------------------------------------------+-- * Projection+--------------------------------------------------------------------------------+ -- | Expressions for selecting elements of a tuple-data Select a+data Select ctx a where- Sel1 :: Sel1 a b => Select (a :-> Full b)- Sel2 :: Sel2 a b => Select (a :-> Full b)- Sel3 :: Sel3 a b => Select (a :-> Full b)- Sel4 :: Sel4 a b => Select (a :-> Full b)- Sel5 :: Sel5 a b => Select (a :-> Full b)- Sel6 :: Sel6 a b => Select (a :-> Full b)- Sel7 :: Sel7 a b => Select (a :-> Full b)+ Sel1 :: (Sel1 a b, Sat ctx b) => Select ctx (a :-> Full b)+ Sel2 :: (Sel2 a b, Sat ctx b) => Select ctx (a :-> Full b)+ Sel3 :: (Sel3 a b, Sat ctx b) => Select ctx (a :-> Full b)+ Sel4 :: (Sel4 a b, Sat ctx b) => Select ctx (a :-> Full b)+ Sel5 :: (Sel5 a b, Sat ctx b) => Select ctx (a :-> Full b)+ Sel6 :: (Sel6 a b, Sat ctx b) => Select ctx (a :-> Full b)+ Sel7 :: (Sel7 a b, Sat ctx b) => Select ctx (a :-> Full b) -instance IsFunction Select+instance WitnessCons (Select ctx) where- toFunction Sel1 = PrimFunc "sel1" sel1- toFunction Sel2 = PrimFunc "sel2" sel2- toFunction Sel3 = PrimFunc "sel3" sel3- toFunction Sel4 = PrimFunc "sel4" sel4- toFunction Sel5 = PrimFunc "sel5" sel5- toFunction Sel6 = PrimFunc "sel6" sel6- toFunction Sel7 = PrimFunc "sel7" sel7+ witnessCons Sel1 = ConsWit+ witnessCons Sel2 = ConsWit+ witnessCons Sel3 = ConsWit+ witnessCons Sel4 = ConsWit+ witnessCons Sel5 = ConsWit+ witnessCons Sel6 = ConsWit+ witnessCons Sel7 = ConsWit -instance ExprEq Select where exprEq = exprEqFunc-instance Render Select where renderPart = renderPartFunc-instance Eval Select where evaluate = evaluateFunc-instance ExprHash Select where exprHash = exprHashFunc-instance ToTree Select+instance WitnessSat (Select ctx)+ where+ type Context (Select ctx) = ctx+ witnessSat Sel1 = Witness'+ witnessSat Sel2 = Witness'+ witnessSat Sel3 = Witness'+ witnessSat Sel4 = Witness'+ witnessSat Sel5 = Witness'+ witnessSat Sel6 = Witness'+ witnessSat Sel7 = Witness' +instance IsSymbol (Select ctx)+ where+ toSym Sel1 = Sym "sel1" sel1+ toSym Sel2 = Sym "sel2" sel2+ toSym Sel3 = Sym "sel3" sel3+ toSym Sel4 = Sym "sel4" sel4+ toSym Sel5 = Sym "sel5" sel5+ toSym Sel6 = Sym "sel6" sel6+ toSym Sel7 = Sym "sel7" sel7++instance ExprEq (Select ctx) where exprEq = exprEqFunc; exprHash = exprHashFunc+instance Render (Select ctx) where renderPart = renderPartFunc+instance Eval (Select ctx) where evaluate = evaluateFunc+instance ToTree (Select ctx)++-- | Partial `Select` projection with explicit context+prjSelect :: (Select ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Select ctx a)+prjSelect _ = project+ -- | Return the selected position, e.g. ----- > selectPos (Sel3 :: Select ((Int,Int,Int,Int) -> Int)) = 3-selectPos :: Select a -> Int+-- > selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3+selectPos :: Select ctx a -> Int selectPos Sel1 = 1 selectPos Sel2 = 2 selectPos Sel3 = 3@@ -75,4 +251,141 @@ selectPos Sel5 = 5 selectPos Sel6 = 6 selectPos Sel7 = 7++++sugarTup2+ :: ( Syntactic a dom+ , Syntactic b dom+ , Sat ctx (Internal a)+ , Sat ctx (Internal b)+ , Select ctx :<: dom+ )+ => Proxy ctx+ -> ASTF dom (Internal a, Internal b)+ -> (a,b)+sugarTup2 ctx a =+ ( sugar $ inject (Sel1 `withContext` ctx) :$: a+ , sugar $ inject (Sel2 `withContext` ctx) :$: a+ )++sugarTup3+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Sat ctx (Internal a)+ , Sat ctx (Internal b)+ , Sat ctx (Internal c)+ , Select ctx :<: dom+ )+ => Proxy ctx+ -> ASTF dom (Internal a, Internal b, Internal c)+ -> (a,b,c)+sugarTup3 ctx a =+ ( sugar $ inject (Sel1 `withContext` ctx) :$: a+ , sugar $ inject (Sel2 `withContext` ctx) :$: a+ , sugar $ inject (Sel3 `withContext` ctx) :$: a+ )++sugarTup4+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Sat ctx (Internal a)+ , Sat ctx (Internal b)+ , Sat ctx (Internal c)+ , Sat ctx (Internal d)+ , Select ctx :<: dom+ )+ => Proxy ctx+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d)+ -> (a,b,c,d)+sugarTup4 ctx a =+ ( sugar $ inject (Sel1 `withContext` ctx) :$: a+ , sugar $ inject (Sel2 `withContext` ctx) :$: a+ , sugar $ inject (Sel3 `withContext` ctx) :$: a+ , sugar $ inject (Sel4 `withContext` ctx) :$: a+ )++sugarTup5+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Sat ctx (Internal a)+ , Sat ctx (Internal b)+ , Sat ctx (Internal c)+ , Sat ctx (Internal d)+ , Sat ctx (Internal e)+ , Select ctx :<: dom+ )+ => Proxy ctx+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)+ -> (a,b,c,d,e)+sugarTup5 ctx a =+ ( sugar $ inject (Sel1 `withContext` ctx) :$: a+ , sugar $ inject (Sel2 `withContext` ctx) :$: a+ , sugar $ inject (Sel3 `withContext` ctx) :$: a+ , sugar $ inject (Sel4 `withContext` ctx) :$: a+ , sugar $ inject (Sel5 `withContext` ctx) :$: a+ )++sugarTup6+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , Sat ctx (Internal a)+ , Sat ctx (Internal b)+ , Sat ctx (Internal c)+ , Sat ctx (Internal d)+ , Sat ctx (Internal e)+ , Sat ctx (Internal f)+ , Select ctx :<: dom+ )+ => Proxy ctx+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)+ -> (a,b,c,d,e,f)+sugarTup6 ctx a =+ ( sugar $ inject (Sel1 `withContext` ctx) :$: a+ , sugar $ inject (Sel2 `withContext` ctx) :$: a+ , sugar $ inject (Sel3 `withContext` ctx) :$: a+ , sugar $ inject (Sel4 `withContext` ctx) :$: a+ , sugar $ inject (Sel5 `withContext` ctx) :$: a+ , sugar $ inject (Sel6 `withContext` ctx) :$: a+ )++sugarTup7+ :: ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , Syntactic g dom+ , Sat ctx (Internal a)+ , Sat ctx (Internal b)+ , Sat ctx (Internal c)+ , Sat ctx (Internal d)+ , Sat ctx (Internal e)+ , Sat ctx (Internal f)+ , Sat ctx (Internal g)+ , Select ctx :<: dom+ )+ => Proxy ctx+ -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)+ -> (a,b,c,d,e,f,g)+sugarTup7 ctx a =+ ( sugar $ inject (Sel1 `withContext` ctx) :$: a+ , sugar $ inject (Sel2 `withContext` ctx) :$: a+ , sugar $ inject (Sel3 `withContext` ctx) :$: a+ , sugar $ inject (Sel4 `withContext` ctx) :$: a+ , sugar $ inject (Sel5 `withContext` ctx) :$: a+ , sugar $ inject (Sel6 `withContext` ctx) :$: a+ , sugar $ inject (Sel7 `withContext` ctx) :$: a+ )
− Language/Syntactic/Features/TupleSyntactic.hs
@@ -1,204 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | 'Syntactic' instances for tuples-module Language.Syntactic.Features.TupleSyntactic where----import Language.Syntactic.Syntax-import Language.Syntactic.Features.Tuple----instance- ( Syntactic a dom- , Syntactic b dom- , Tuple :<: dom- , Select :<: dom- ) =>- Syntactic (a,b) dom- where- type Internal (a,b) =- ( Internal a- , Internal b- )-- desugar (a,b) = inject Tup2- :$: desugar a- :$: desugar b-- sugar a =- ( sugar $ inject Sel1 :$: a- , sugar $ inject Sel2 :$: a- )--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Tuple :<: dom- , Select :<: dom- ) =>- Syntactic (a,b,c) dom- where- type Internal (a,b,c) =- ( Internal a- , Internal b- , Internal c- )-- desugar (a,b,c) = inject Tup3- :$: desugar a- :$: desugar b- :$: desugar c-- sugar a =- ( sugar $ inject Sel1 :$: a- , sugar $ inject Sel2 :$: a- , sugar $ inject Sel3 :$: a- )--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Tuple :<: dom- , Select :<: dom- ) =>- Syntactic (a,b,c,d) dom- where- type Internal (a,b,c,d) =- ( Internal a- , Internal b- , Internal c- , Internal d- )-- desugar (a,b,c,d) = inject Tup4- :$: desugar a- :$: desugar b- :$: desugar c- :$: desugar d-- sugar a =- ( sugar $ inject Sel1 :$: a- , sugar $ inject Sel2 :$: a- , sugar $ inject Sel3 :$: a- , sugar $ inject Sel4 :$: a- )--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Tuple :<: dom- , Select :<: dom- ) =>- 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 (a,b,c,d,e) = inject Tup5- :$: desugar a- :$: desugar b- :$: desugar c- :$: desugar d- :$: desugar e-- sugar a =- ( sugar $ inject Sel1 :$: a- , sugar $ inject Sel2 :$: a- , sugar $ inject Sel3 :$: a- , sugar $ inject Sel4 :$: a- , sugar $ inject Sel5 :$: a- )--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Tuple :<: dom- , Select :<: dom- ) =>- 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 (a,b,c,d,e,f) = inject Tup6- :$: desugar a- :$: desugar b- :$: desugar c- :$: desugar d- :$: desugar e- :$: desugar f-- sugar a =- ( sugar $ inject Sel1 :$: a- , sugar $ inject Sel2 :$: a- , sugar $ inject Sel3 :$: a- , sugar $ inject Sel4 :$: a- , sugar $ inject Sel5 :$: a- , sugar $ inject Sel6 :$: a- )--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Syntactic g dom- , Tuple :<: dom- , Select :<: dom- ) =>- 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 (a,b,c,d,e,f,g) = inject Tup7- :$: desugar a- :$: desugar b- :$: desugar c- :$: desugar d- :$: desugar e- :$: desugar f- :$: desugar g-- sugar a =- ( sugar $ inject Sel1 :$: a- , sugar $ inject Sel2 :$: a- , sugar $ inject Sel3 :$: a- , sugar $ inject Sel4 :$: a- , sugar $ inject Sel5 :$: a- , sugar $ inject Sel6 :$: a- , sugar $ inject Sel7 :$: a- )-
+ Language/Syntactic/Features/TupleSyntacticPoly.hs view
@@ -0,0 +1,138 @@+{-# LANGUAGE UndecidableInstances #-}++-- | 'Syntactic' instances for tuples with 'Poly' context+module Language.Syntactic.Features.TupleSyntacticPoly where++++import Language.Syntactic.Syntax+import Language.Syntactic.Features.Tuple++++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Tuple Poly :<: dom+ , Select Poly :<: dom+ ) =>+ Syntactic (a,b) dom+ where+ type Internal (a,b) =+ ( Internal a+ , Internal b+ )++ desugar = desugarTup2 poly+ sugar = sugarTup2 poly++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Tuple Poly :<: dom+ , Select Poly :<: dom+ ) =>+ Syntactic (a,b,c) dom+ where+ type Internal (a,b,c) =+ ( Internal a+ , Internal b+ , Internal c+ )++ desugar = desugarTup3 poly+ sugar = sugarTup3 poly++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Tuple Poly :<: dom+ , Select Poly :<: dom+ ) =>+ Syntactic (a,b,c,d) dom+ where+ type Internal (a,b,c,d) =+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ )++ desugar = desugarTup4 poly+ sugar = sugarTup4 poly++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Tuple Poly :<: dom+ , Select Poly :<: dom+ ) =>+ 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 = desugarTup5 poly+ sugar = sugarTup5 poly++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , Tuple Poly :<: dom+ , Select Poly :<: dom+ ) =>+ 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 = desugarTup6 poly+ sugar = sugarTup6 poly++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , Syntactic g dom+ , Tuple Poly :<: dom+ , Select Poly :<: dom+ ) =>+ 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 = desugarTup7 poly+ sugar = sugarTup7 poly+
+ Language/Syntactic/Sharing/Graph.hs view
@@ -0,0 +1,324 @@+-- | 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 Data.Proxy++import Language.Syntactic+import Language.Syntactic.Features.Binding+import Language.Syntactic.Sharing.Utils++++--------------------------------------------------------------------------------+-- * Representation+--------------------------------------------------------------------------------++-- | Node identifier+newtype NodeId = NodeId { nodeInteger :: Integer }+ deriving (Eq, Ord, Num, Real, Integral, Enum, Ix)++++-- | Placeholder for a syntax tree+data Node ctx a+ where+ Node :: Sat ctx a => NodeId -> Node ctx (Full a)++instance Show NodeId+ where+ show (NodeId i) = show i++showNode :: NodeId -> String+showNode n = "node:" ++ show n++++instance WitnessCons (Node ctx)+ where+ witnessCons (Node _) = ConsWit++instance Render (Node ctx)+ where+ render (Node a) = showNode a++instance ToTree (Node ctx)++-- | Partial `Node` projection with explicit context+prjNode :: (Node ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Node ctx a)+prjNode _ = project++++-- | An 'ASTF' with hidden result type+data SomeAST dom+ where+ SomeAST :: Typeable a => ASTF dom a -> SomeAST dom++++-- | \"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 ctx dom a = ASG+ { topExpression :: ASTF (Node ctx :+: dom) a -- ^ Top-level expression+ , graphNodes :: [(NodeId, SomeAST (Node ctx :+: dom))] -- ^ Mapping from node id to sub-expression+ , numNodes :: NodeId -- ^ Total number of nodes+ }++++-- | Show syntax graph using ASCII art+showASG :: ToTree dom => ASG ctx 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, SomeAST expr) = concat+ [ line ("node:" ++ show n)+ , showAST expr+ ]++-- | Print syntax graph using ASCII art+drawASG :: ToTree dom => ASG ctx dom a -> IO ()+drawASG = putStrLn . showASG++-- | Update the node identifiers in an 'AST' using the supplied reindexing+-- function+reindexNodesAST ::+ (NodeId -> NodeId) -> AST (Node ctx :+: dom) a -> AST (Node ctx :+: dom) a+reindexNodesAST reix (Symbol (InjectL (Node n))) =+ Symbol (InjectL (Node $ reix n))+reindexNodesAST reix (f :$: a) =+ reindexNodesAST reix f :$: 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 ctx dom a -> ASG ctx dom a+reindexNodes reix (ASG top nodes n) = ASG top' nodes' n+ where+ top' = reindexNodesAST reix top+ nodes' =+ [ (reix n, SomeAST $ reindexNodesAST reix a)+ | (n, SomeAST 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 ctx dom a -> ASG ctx 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 ctx dom a -> ASG ctx dom a+nubNodes (ASG top nodes n) = ASG top nodes' n'+ where+ nodes' = nubBy ((==) `on` fst) nodes+ n' = genericLength nodes'++liftSome2+ :: (forall a b . ASTF (Node ctx :+: dom) a -> ASTF (Node ctx :+: dom) b -> c)+ -> SomeAST (Node ctx :+: dom)+ -> SomeAST (Node ctx :+: dom)+ -> c+liftSome2 f (SomeAST a) (SomeAST b) = f a b++++--------------------------------------------------------------------------------+-- * 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 ctx dom a b+ . (SyntaxPF dom b -> b)+ -> ASG ctx dom a+ -> (b, (Array NodeId b, [(NodeId,b)]))+foldGraph alg graph@(ASG top ns nn) = (g top, (arr,nodes))+ where+ nodes = [(n, g expr) | (n, SomeAST expr) <- ns]+ arr = array (0, nn-1) nodes++ g :: ConsType c => AST (Node ctx :+: dom) c -> b+ g (h :$: a) = alg $ AppPF (g h) (g a)+ g (Symbol (InjectL (Node n)) ) = alg $ NodePF n (arr!n)+ g (Symbol (InjectR a)) = alg $ DomPF a++++--------------------------------------------------------------------------------+-- * Inlining+--------------------------------------------------------------------------------++-- | Convert an 'ASG' to an 'AST' by inlining all nodes+inlineAll :: forall ctx dom a . Typeable a => ASG ctx dom a -> ASTF dom a+inlineAll (ASG top nodes n) = inline top+ where+ nodeMap = array (0, n-1) nodes++ inline :: forall b. (Typeable b, ConsType b) =>+ AST (Node ctx :+: dom) b -> AST dom b+ inline (f :$: a) = inline f :$: inline a+ inline (Symbol (InjectL (Node n))) = case nodeMap ! n of+ SomeAST a -> case gcast a of+ Nothing -> error "inlineAll: type mismatch"+ Just a -> inline a+ inline (Symbol (InjectR a)) = Symbol 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 ctx 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 ctx 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 ctx dom a . Typeable a => ASG ctx dom a -> ASG ctx 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, SomeAST (inline a)) | (n, SomeAST a) <- nodes, occs!n > 1]+ n' = genericLength nodes'++ inline :: forall b. (Typeable b, ConsType b) =>+ AST (Node ctx :+: dom) b -> AST (Node ctx :+: dom) b+ inline (f :$: a) = inline f :$: inline a+ inline (Symbol (InjectL (Node n)))+ | occs!n > 1 = Symbol (InjectL (Node n))+ | otherwise = case nodeTab ! n of+ SomeAST a -> case gcast a of+ Nothing -> error "inlineSingle: type mismatch"+ Just a -> inline a+ inline (Symbol (InjectR a)) = Symbol (InjectR a)++++--------------------------------------------------------------------------------+-- * Sharing+--------------------------------------------------------------------------------++-- | Compute a table (both array and list representation) of hash values for+-- each node+hashNodes :: ExprEq dom =>+ ASG ctx 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 ctx dom a+ . (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom)+ => ASG ctx 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++ eqNode :: forall a b . ExprEq dom+ => AST (Node ctx :+: dom) a+ -> AST (Node ctx :+: dom) b+ -> Reader [(VarId,VarId)] Bool+ eqNode (Symbol (InjectL (Node n1))) (Symbol (InjectL (Node n2)))+ | n1 == n2 = return True+ | hTab!n1 /= hTab!n2 = return False+ | otherwise = case (nTab!n1, nTab!n2) of+ (SomeAST a, SomeAST b) -> eqNodeAlpha a b+ -- TODO The result could be memoized in a+ -- @Map (NodeId,NodeId) Bool@+ eqNode (Symbol (InjectR a)) (Symbol (InjectR b)) = return (exprEq a b)+ eqNode _ _ = return False+ -- Returns '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 is just for simplicity; it would be easy to fix.++ -- | Alpha-equivalence for expressions with 'Node's+ eqNodeAlpha :: forall a b+ . AST (Node ctx :+: dom) a+ -> AST (Node ctx :+: dom) b+ -> Reader [(VarId,VarId)] Bool+ eqNodeAlpha a b = alphaEqM (Proxy::Proxy ctx) eqNode a b++ nodeEq :: NodeId -> NodeId -> Bool+ nodeEq n1 n2 = runReader (liftSome2 eqNodeAlpha (nTab!n1) (nTab!n2)) []++++-- | Common sub-expression elimination based on alpha-equivalence+cse :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) =>+ ASG ctx dom a -> ASG ctx 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 view
@@ -0,0 +1,83 @@+-- | Reifying the sharing in an 'AST'+--+-- This module is based on /Type-Safe Observable Sharing in Haskell/ (Andy Gill,+-- /Haskell Symposium/, 2009).++module Language.Syntactic.Sharing.Reify+ ( reifyGraph+ ) where++++import Control.Monad.Writer+import Data.IntMap as Map+import Data.IORef+import Data.Typeable+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 ctx dom a = WriterT+ [(NodeId, SomeAST (Node ctx :+: dom))]+ IO+ (AST (Node ctx :+: dom) a)++++reifyGraphM :: forall ctx dom a . Typeable a+ => (forall a . ASTF dom a -> Maybe (Witness' ctx a))+ -> IORef NodeId+ -> IORef (History (AST dom))+ -> ASTF dom a+ -> GraphMonad ctx dom (Full a)++reifyGraphM canShare nSupp history = reifyNode+ where+ reifyNode :: Typeable b => ASTF dom b -> GraphMonad ctx dom (Full b)+ reifyNode a = case canShare a of+ Nothing -> reifyRec a+ Just Witness' | a `seq` True -> do+ st <- liftIO $ makeStableName a+ hist <- liftIO $ readIORef history+ case lookHistory hist (StName st) of+ Just n -> return $ Symbol $ InjectL $ Node n+ _ -> do+ n <- fresh nSupp+ liftIO $ modifyIORef history $ remember (StName st) n+ a' <- reifyRec a+ tell [(n, SomeAST a')]+ return $ Symbol $ InjectL $ Node n++ reifyRec :: AST dom b -> GraphMonad ctx dom b+ reifyRec (f :$: a) = liftM2 (:$:) (reifyRec f) (reifyNode a)+ reifyRec (Symbol a) = return $ Symbol (InjectR a)++++-- | 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 :: Typeable a+ => (forall a . ASTF dom a -> Maybe (Witness' ctx a))+ -- ^ A function that decides whether a given node can be shared.+ -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose+ -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the+ -- function returns a 'Witness''.+ -> ASTF dom a+ -> IO (ASG ctx 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 view
@@ -0,0 +1,116 @@+-- | This module is similar to "Language.Syntactic.Sharing.Reify", but operates+-- on 'HOAST' rather than a general 'AST'. The reason for having this module is+-- that when using 'HOAST', 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 /Type-Safe Observable Sharing in Haskell/ (Andy Gill,+-- /Haskell Symposium/, 2009).+++module Language.Syntactic.Sharing.ReifyHO+ ( reifyGraphTop+ , reifyGraph+ ) where++++import Control.Monad.Writer+import Data.IntMap as Map+import Data.IORef+import Data.Typeable+import System.Mem.StableName++import Data.Proxy++import Language.Syntactic+import Language.Syntactic.Features.Binding+import Language.Syntactic.Features.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 ctx dom a = WriterT+ [(NodeId, SomeAST (Node ctx :+: Lambda ctx :+: Variable ctx :+: dom))]+ IO+ (AST (Node ctx :+: Lambda ctx :+: Variable ctx :+: dom) a)++++reifyGraphM :: forall ctx dom a . Typeable a+ => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))+ -> IORef VarId+ -> IORef NodeId+ -> IORef (History (HOAST ctx dom))+ -> HOASTF ctx dom a+ -> GraphMonad ctx dom (Full a)++reifyGraphM canShare vSupp nSupp history = reifyNode+ where+ reifyNode :: Typeable b => HOASTF ctx dom b -> GraphMonad ctx dom (Full b)+ reifyNode a = case canShare a of+ Nothing -> reifyRec a+ Just Witness' | a `seq` True -> do+ st <- liftIO $ makeStableName a+ hist <- liftIO $ readIORef history+ case lookHistory hist (StName st) of+ Just n -> return $ Symbol $ InjectL $ Node n+ _ -> do+ n <- fresh nSupp+ liftIO $ modifyIORef history $ remember (StName st) n+ a' <- reifyRec a+ tell [(n, SomeAST a')]+ return $ Symbol $ InjectL $ Node n++ reifyRec :: HOAST ctx dom b -> GraphMonad ctx dom b+ reifyRec (f :$: a) = liftM2 (:$:) (reifyRec f) (reifyNode a)+ reifyRec (Symbol (InjectR a)) = return $ Symbol (InjectR (InjectR a))+ reifyRec (Symbol (InjectL (HOLambda f))) = do+ v <- fresh vSupp+ body <- reifyNode $ f $ inject $ (Variable v `withContext` ctx)+ return $ inject (Lambda v `withContext` ctx) :$: body+ where+ ctx = Proxy :: Proxy ctx++++-- | Convert a syntax tree to a sharing-preserving graph+reifyGraphTop :: Typeable a+ => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))+ -> HOASTF ctx dom a+ -> IO (ASG ctx (Lambda ctx :+: Variable ctx :+: dom) 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 :: Reifiable ctx a dom internal+ => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))+ -- ^ A function that decides whether a given node can be shared.+ -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose+ -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the+ -- function returns a 'Witness''.+ -> a+ -> IO+ ( ASG ctx (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal)+ , VarId+ )+reifyGraph canShare = reifyGraphTop canShare . lambdaN . desugarN+
+ Language/Syntactic/Sharing/StableName.hs view
@@ -0,0 +1,61 @@+module Language.Syntactic.Sharing.StableName where++++import Control.Monad.IO.Class+import Data.IntMap as Map+import Data.IORef+import Data.Typeable+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 :: Typeable a => StableName (c (Full a)) -> StName c++stCast :: forall a b c . (Typeable a, Typeable b) =>+ StableName (c (Full a)) -> Maybe (StableName (c (Full b)))+stCast a+ | ta==tb = Just (unsafeCoerce a)+ | otherwise = Nothing+ where+ ta = typeOf (undefined :: a)+ tb = typeOf (undefined :: b)++instance Eq (StName c)+ where+ StName st1 == StName st2 = case stCast st1 of+ Just st1' -> st1'==st2+ _ -> False++hash :: StName c -> Int+hash (StName st) = hashStableName st++++-- 'History' implements 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)]++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++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 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+
Language/Syntactic/Syntax.hs view
@@ -50,10 +50,10 @@ -- > conv12 :: (Num2 :<: dom, Add2 :<: dom) => Expr1 a -> ASTF dom a -- > conv21 :: (Num2 :<: dom, Add2 :<: dom) => ASTF dom a -> Expr1 a ----- This way of encoding open data types is taken from /Data types à la carte/,--- by Wouter Swierstra, in /Journal of Functional Programming/, 2008. However,--- we do not need Swierstra's fixed-point machinery for recursive data types.--- Instead we rely on 'AST' being recursive.+-- This way of encoding open data types is taken from /Data types à la carte/+-- (Wouter Swierstra, /Journal of Functional Programming/, 2008). However, we do+-- not need Swierstra's fixed-point machinery for recursive data types. Instead+-- we rely on 'AST' being recursive. module Language.Syntactic.Syntax ( -- * Syntax trees@@ -63,11 +63,14 @@ , ConsType , ConsEval , EvalResult+ , ConsWit (..)+ , WitnessCons (..) , fromEval , toEval , listHList , listHListM , mapHList+ , appHList , ($:) , AST (..) , ASTF@@ -79,16 +82,31 @@ , resugar , SyntacticN (..) -- * AST processing+ , queryNodeI , queryNode , transformNode+ -- * Restricted syntax trees+ , Sat (..)+ , Witness' (..)+ , witness'+ , WitnessSat (..)+ , withContext+ , Poly+ , poly ) where import Data.Typeable +import Data.Proxy ++--------------------------------------------------------------------------------+-- * Syntax trees+--------------------------------------------------------------------------------+ -- | The type of a fully applied constructor newtype Full a = Full { result :: a } deriving (Eq, Show, Typeable)@@ -101,7 +119,9 @@ data family HList (c :: * -> *) a data instance HList c (Full a) = Nil-data instance HList c (a :-> b) = c (Full a) :*: HList c b+data instance HList c (a :-> b) = Typeable a => c (Full a) :*: HList c b+ -- The 'Typeable' constraint is needed in order to be able to rebuild an 'AST'+ -- from an 'HList' (since '(:$:)' has a `Typeable` constraint). infixr :->, :*: @@ -125,8 +145,10 @@ toEval' :: a -> ConsEval' a listHList' :: (forall a . c (Full a) -> b) -> HList c a -> [b] listHListM' :: Monad m => (forall a . c (Full a) -> m b) -> HList c a -> m [b]- mapHList' :: (forall a . c1 a -> c2 a) -> HList c1 a -> HList c2 a+ mapHList' :: (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a+ appHList' :: AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a) + instance ConsType' (Full a) where type ConsEval' (Full a) = a@@ -137,6 +159,7 @@ listHList' f Nil = [] listHListM' f Nil = return [] mapHList' f Nil = Nil+ appHList' a Nil = a instance ConsType' b => ConsType' (a :-> b) where@@ -148,6 +171,7 @@ listHList' f (a :*: as) = f a : listHList' f as listHListM' f (a :*: as) = sequence (f a : listHList' f as) mapHList' f (a :*: as) = f a :*: mapHList' f as+ appHList' c (a :*: as) = appHList' (c :$: a) as -- | Fully or partially applied constructor --@@ -168,6 +192,18 @@ -- alias for the hidden type 'EvalResult''. type EvalResult a = EvalResult' a +-- | A witness of @(`ConsType` a)@+data ConsWit a+ where+ ConsWit :: ConsType a => ConsWit a++-- | Expressions in syntactic are supposed to have the form+-- @(`ConsType` a => expr a)@. This class lets us witness the 'ConsType'+-- constraint of an expression without examining the expression.+class WitnessCons expr+ where+ witnessCons :: expr a -> ConsWit a+ -- | Make a constructor evaluation from a 'ConsEval' representation fromEval :: ConsType a => ConsEval a -> a fromEval = fromEval'@@ -187,9 +223,14 @@ -- | Change the container of each element in a heterogeneous list mapHList :: ConsType a =>- (forall a . c1 a -> c2 a) -> HList c1 a -> HList c2 a+ (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a mapHList = mapHList' +-- | Apply the syntax tree to listed arguments+appHList :: ConsType a =>+ AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)+appHList = appHList'+ -- | Semantic constructor application ($:) :: (a :-> b) -> a -> b Partial f $: a = f a@@ -226,6 +267,10 @@ +--------------------------------------------------------------------------------+-- * Subsumption+--------------------------------------------------------------------------------+ class sub :<: sup where -- | Injection from @sub@ to @sup@@@ -263,15 +308,19 @@ +--------------------------------------------------------------------------------+-- * Syntactic sugar+--------------------------------------------------------------------------------+ -- | It is assumed that for all types @A@ fulfilling @(`Syntactic` A dom)@: -- -- > eval a == eval (desugar $ (id :: A -> A) $ sugar a) -- -- (using 'Language.Syntactic.Analysis.Evaluation.eval') class Typeable (Internal a) => Syntactic a dom | a -> dom- -- Note: using a two-parameter class rather than an associated type, because- -- this makes it possible to make a class alias constraining dom. GHC- -- doesn't yet handle equality super classes.+ -- Note: using a functional dependency rather than an associated type,+ -- because this makes it possible to make a class alias constraining dom.+ -- GHC doesn't yet handle equality super classes. where type Internal a desugar :: a -> ASTF dom (Internal a)@@ -326,6 +375,24 @@ +--------------------------------------------------------------------------------+-- * AST processing+--------------------------------------------------------------------------------++-- | Like 'queryNode' but with the result indexed by the constructor's result+-- type+queryNodeI :: forall dom a b+ . (forall a . ConsType a => dom a -> HList (AST dom) a -> b (EvalResult a))+ -> ASTF dom a -> b a+queryNodeI f a = query a Nil+ where+ query :: AST dom c -> HList (AST dom) c -> b (EvalResult c)+ query (Symbol a) args = f a args+ query (c :$: a) args = query c (a :*: args)++newtype Wrap a b = Wrap {unWrap :: a}+ -- Only used in the definition of 'queryNode'+ -- | Query an 'AST' using a function that gets direct access to the top-most -- constructor and its sub-trees --@@ -364,11 +431,7 @@ queryNode :: forall dom a b . (forall a . ConsType a => dom a -> HList (AST dom) a -> b) -> ASTF dom a -> b-queryNode f a = query a Nil- where- query :: AST dom c -> HList (AST dom) c -> b- query (Symbol a) args = f a args- query (c :$: a) args = query c (a :*: args)+queryNode f a = unWrap $ queryNodeI (\c args -> Wrap $ f c args) a @@ -385,4 +448,66 @@ transform :: AST dom b -> HList (AST dom) b -> ASTF dom' (EvalResult b) transform (Symbol a) args = f a args transform (c :$: a) args = transform c (a :*: args)++++--------------------------------------------------------------------------------+-- * Restricted syntax trees+--------------------------------------------------------------------------------++-- | An abstract representation of a constraint on @a@. An instance might look+-- as follows:+--+-- > instance MyClass a => Sat MyContext a+-- > where+-- > data Witness MyContext a = MyClass a => MyWitness+-- > witness = MyWitness+--+-- This allows us to use @(`Sat` MyContext a)@ instead of @(MyClass a)@. The+-- point with this is that @MyContext@ can be provided as a parameter, so this+-- effectively allows us to parameterize on class constraints. Note that the+-- existential context in the data definition is important. This means that,+-- given a constraint @(`Sat` MyContext a)@, we can always construct the context+-- @(MyClass a)@ by calling the 'witness' method (the class instance only+-- declares the reverse relationship).+--+-- This way of parameterizing over type classes was inspired by+-- /Restricted Data Types in Haskell/ (John Hughes, /Haskell Workshop/, 1999).+class Sat ctx a+ where+ data Witness ctx a+ witness :: Witness ctx a++-- | Witness of a @(`Sat` ctx a)@ constraint. This is different from+-- @(`Witness` ctx a)@, which witnesses the class encoded by @ctx@. 'Witness''+-- has a single constructor for all contexts, while 'Witness' has different+-- constructors for different contexts.+data Witness' ctx a+ where+ Witness' :: Sat ctx a => Witness' ctx a++witness' :: Witness' ctx a -> Witness ctx a+witness' Witness' = witness++-- | Symbols that act as witnesses of their result type+class WitnessSat sym+ where+ type Context sym+ witnessSat :: sym a -> Witness' (Context sym) (EvalResult a)++-- | Type application for constraining the @ctx@ type of a parameterized symbol+withContext :: sym ctx a -> Proxy ctx -> sym ctx a+withContext = const++-- | Representation of a fully polymorphic constraint -- i.e. @(`Sat` `Poly` a)@+-- is satisfied by all types @a@.+data Poly++instance Sat Poly a+ where+ data Witness Poly a = PolyWit+ witness = PolyWit++poly :: Proxy Poly+poly = Proxy
syntactic.cabal view
@@ -1,5 +1,5 @@ Name: syntactic-Version: 0.4+Version: 0.5 Synopsis: Generic abstract syntax, and utilities for embedded languages Description: This library provides: .@@ -17,9 +17,9 @@ * A small proof-of-concept implementation of the embedded language Feldspar [2] (see the @Examples@ directory) .- Note: The library is probably mostly useful for data-flow- languages, such as Feldspar. Currently, it does not support- cyclic programs.+ Note: The library is probably mostly useful for /functional/+ object languages, such as Feldspar. Currently, it does not+ support cyclic programs. . \[1\] /Data types à la carte/, by Wouter Swierstra, in /Journal of Functional Programming/, 2008@@ -37,13 +37,13 @@ Extra-source-files: Examples/ALaCarte.hs- Examples/MuFeldspar/Core.hs- Examples/MuFeldspar/Vector.hs- Examples/MuFeldspar/Test.hs+ Examples/NanoFeldspar/Core.hs+ Examples/NanoFeldspar/Vector.hs+ Examples/NanoFeldspar/Test.hs source-repository head type: darcs- location: http://code.haskell.org/syntactic/+ location: http://projects.haskell.org/syntactic/ Library Exposed-modules:@@ -52,15 +52,20 @@ Language.Syntactic.Analysis.Equality Language.Syntactic.Analysis.Render Language.Syntactic.Analysis.Evaluation- Language.Syntactic.Analysis.Hash Language.Syntactic.Features.Annotate+ Language.Syntactic.Features.Symbol Language.Syntactic.Features.Literal- Language.Syntactic.Features.PrimFunc Language.Syntactic.Features.Condition Language.Syntactic.Features.Tuple- Language.Syntactic.Features.TupleSyntactic+ Language.Syntactic.Features.TupleSyntacticPoly Language.Syntactic.Features.Binding Language.Syntactic.Features.Binding.HigherOrder+ Language.Syntactic.Sharing.Utils+ Language.Syntactic.Sharing.Graph+ Language.Syntactic.Sharing.StableName+ Language.Syntactic.Sharing.Reify+ Language.Syntactic.Sharing.ReifyHO+ Other-modules: Build-depends:@@ -69,6 +74,8 @@ containers, data-hash, mtl >= 1.1 && < 3,+ tagged,+ transformers >= 0.2, tuple >= 0.2 Extensions: