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