diff --git a/Examples/ALaCarte.hs b/Examples/ALaCarte.hs --- a/Examples/ALaCarte.hs +++ b/Examples/ALaCarte.hs @@ -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 diff --git a/Examples/MuFeldspar/Core.hs b/Examples/MuFeldspar/Core.hs deleted file mode 100644 --- a/Examples/MuFeldspar/Core.hs +++ /dev/null @@ -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 - diff --git a/Examples/MuFeldspar/Test.hs b/Examples/MuFeldspar/Test.hs deleted file mode 100644 --- a/Examples/MuFeldspar/Test.hs +++ /dev/null @@ -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] - diff --git a/Examples/MuFeldspar/Vector.hs b/Examples/MuFeldspar/Vector.hs deleted file mode 100644 --- a/Examples/MuFeldspar/Vector.hs +++ /dev/null @@ -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 - diff --git a/Examples/NanoFeldspar/Core.hs b/Examples/NanoFeldspar/Core.hs new file mode 100644 --- /dev/null +++ b/Examples/NanoFeldspar/Core.hs @@ -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 + diff --git a/Examples/NanoFeldspar/Test.hs b/Examples/NanoFeldspar/Test.hs new file mode 100644 --- /dev/null +++ b/Examples/NanoFeldspar/Test.hs @@ -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. + diff --git a/Examples/NanoFeldspar/Vector.hs b/Examples/NanoFeldspar/Vector.hs new file mode 100644 --- /dev/null +++ b/Examples/NanoFeldspar/Vector.hs @@ -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 + diff --git a/Language/Syntactic.hs b/Language/Syntactic.hs --- a/Language/Syntactic.hs +++ b/Language/Syntactic.hs @@ -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 diff --git a/Language/Syntactic/Analysis/Equality.hs b/Language/Syntactic/Analysis/Equality.hs --- a/Language/Syntactic/Analysis/Equality.hs +++ b/Language/Syntactic/Analysis/Equality.hs @@ -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 diff --git a/Language/Syntactic/Analysis/Evaluation.hs b/Language/Syntactic/Analysis/Evaluation.hs --- a/Language/Syntactic/Analysis/Evaluation.hs +++ b/Language/Syntactic/Analysis/Evaluation.hs @@ -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 - diff --git a/Language/Syntactic/Analysis/Hash.hs b/Language/Syntactic/Analysis/Hash.hs deleted file mode 100644 --- a/Language/Syntactic/Analysis/Hash.hs +++ /dev/null @@ -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 - diff --git a/Language/Syntactic/Features/Annotate.hs b/Language/Syntactic/Features/Annotate.hs --- a/Language/Syntactic/Features/Annotate.hs +++ b/Language/Syntactic/Features/Annotate.hs @@ -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 diff --git a/Language/Syntactic/Features/Binding.hs b/Language/Syntactic/Features/Binding.hs --- a/Language/Syntactic/Features/Binding.hs +++ b/Language/Syntactic/Features/Binding.hs @@ -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 diff --git a/Language/Syntactic/Features/Binding/HigherOrder.hs b/Language/Syntactic/Features/Binding/HigherOrder.hs --- a/Language/Syntactic/Features/Binding/HigherOrder.hs +++ b/Language/Syntactic/Features/Binding/HigherOrder.hs @@ -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 diff --git a/Language/Syntactic/Features/Condition.hs b/Language/Syntactic/Features/Condition.hs --- a/Language/Syntactic/Features/Condition.hs +++ b/Language/Syntactic/Features/Condition.hs @@ -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 diff --git a/Language/Syntactic/Features/Literal.hs b/Language/Syntactic/Features/Literal.hs --- a/Language/Syntactic/Features/Literal.hs +++ b/Language/Syntactic/Features/Literal.hs @@ -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 diff --git a/Language/Syntactic/Features/PrimFunc.hs b/Language/Syntactic/Features/PrimFunc.hs deleted file mode 100644 --- a/Language/Syntactic/Features/PrimFunc.hs +++ /dev/null @@ -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 - diff --git a/Language/Syntactic/Features/Symbol.hs b/Language/Syntactic/Features/Symbol.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Features/Symbol.hs @@ -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 + diff --git a/Language/Syntactic/Features/Tuple.hs b/Language/Syntactic/Features/Tuple.hs --- a/Language/Syntactic/Features/Tuple.hs +++ b/Language/Syntactic/Features/Tuple.hs @@ -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 + ) diff --git a/Language/Syntactic/Features/TupleSyntactic.hs b/Language/Syntactic/Features/TupleSyntactic.hs deleted file mode 100644 --- a/Language/Syntactic/Features/TupleSyntactic.hs +++ /dev/null @@ -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 - ) - diff --git a/Language/Syntactic/Features/TupleSyntacticPoly.hs b/Language/Syntactic/Features/TupleSyntacticPoly.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Features/TupleSyntacticPoly.hs @@ -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 + diff --git a/Language/Syntactic/Sharing/Graph.hs b/Language/Syntactic/Sharing/Graph.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Sharing/Graph.hs @@ -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] + diff --git a/Language/Syntactic/Sharing/Reify.hs b/Language/Syntactic/Sharing/Reify.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Sharing/Reify.hs @@ -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) + diff --git a/Language/Syntactic/Sharing/ReifyHO.hs b/Language/Syntactic/Sharing/ReifyHO.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Sharing/ReifyHO.hs @@ -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 + diff --git a/Language/Syntactic/Sharing/StableName.hs b/Language/Syntactic/Sharing/StableName.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Sharing/StableName.hs @@ -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 + diff --git a/Language/Syntactic/Sharing/Utils.hs b/Language/Syntactic/Sharing/Utils.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Sharing/Utils.hs @@ -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 + diff --git a/Language/Syntactic/Syntax.hs b/Language/Syntactic/Syntax.hs --- a/Language/Syntactic/Syntax.hs +++ b/Language/Syntactic/Syntax.hs @@ -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 diff --git a/syntactic.cabal b/syntactic.cabal --- a/syntactic.cabal +++ b/syntactic.cabal @@ -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: