syntactic 0.9 → 1.0
raw patch · 34 files changed
+1693/−2243 lines, 34 filesdep +constraintsdep +ghc-primdep ~base
Dependencies added: constraints, ghc-prim
Dependency ranges changed: base
Files
- Data/DynamicAlt.hs +28/−0
- Examples/ALaCarte.hs +0/−120
- Examples/NanoFeldspar/Core.hs +60/−60
- Examples/NanoFeldspar/Extra.hs +15/−19
- Examples/NanoFeldspar/Test.hs +0/−2
- Examples/NanoFeldspar/Vector.hs +2/−2
- Language/Syntactic.hs +10/−4
- Language/Syntactic/Constraint.hs +262/−0
- Language/Syntactic/Constructs/Binding.hs +162/−162
- Language/Syntactic/Constructs/Binding/HigherOrder.hs +36/−41
- Language/Syntactic/Constructs/Binding/Optimize.hs +64/−70
- Language/Syntactic/Constructs/Condition.hs +10/−28
- Language/Syntactic/Constructs/Construct.hs +11/−48
- Language/Syntactic/Constructs/Decoration.hs +33/−59
- Language/Syntactic/Constructs/Identity.hs +10/−28
- Language/Syntactic/Constructs/Literal.hs +11/−27
- Language/Syntactic/Constructs/Monad.hs +13/−16
- Language/Syntactic/Constructs/Tuple.hs +246/−305
- Language/Syntactic/Constructs/TupleSyntacticPoly.hs +0/−138
- Language/Syntactic/Constructs/TupleSyntacticSimple.hs +0/−138
- Language/Syntactic/Frontend/Monad.hs +37/−23
- Language/Syntactic/Interpretation/Equality.hs +22/−22
- Language/Syntactic/Interpretation/Evaluation.hs +7/−5
- Language/Syntactic/Interpretation/Render.hs +19/−19
- Language/Syntactic/Interpretation/Semantics.hs +19/−22
- Language/Syntactic/Sharing/Graph.hs +76/−87
- Language/Syntactic/Sharing/Reify.hs +29/−32
- Language/Syntactic/Sharing/ReifyHO.hs +40/−51
- Language/Syntactic/Sharing/SimpleCodeMotion.hs +65/−78
- Language/Syntactic/Sharing/StableName.hs +12/−20
- Language/Syntactic/Sugar.hs +111/−0
- Language/Syntactic/Syntax.hs +73/−596
- Language/Syntactic/Traversal.hs +183/−0
- syntactic.cabal +27/−21
+ Data/DynamicAlt.hs view
@@ -0,0 +1,28 @@+-- | An alternative to "Data.Dynamic" with a different constraint on 'toDyn'++module Data.DynamicAlt where++++import Data.Dynamic ()+import Data.Typeable+import GHC.Prim+import Unsafe.Coerce++import Data.Proxy++++data Dynamic = Dynamic TypeRep Any++toDyn :: forall a b . Typeable (a -> b) => Proxy (a -> b) -> a -> Dynamic+toDyn _ a = case splitTyConApp $ typeOf (undefined :: a -> b) of+ (_,[ta,_]) -> Dynamic ta (unsafeCoerce a)++fromDyn :: Typeable a => Dynamic -> Maybe a+fromDyn (Dynamic t a)+ | b <- unsafeCoerce a+ , t == typeOf b+ = Just b+fromDyn _ = Nothing+
− Examples/ALaCarte.hs
@@ -1,120 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE ViewPatterns #-}---- | Demonstration of the fact that "Language.Syntactic" has the same--- functionality as /Data types à la carte/ (Wouter Swierstra,--- /Journal of Functional Programming/, 2008)--module ALaCarte where----import Language.Syntactic----data Val a- where- Val :: Int -> Val (Full Int)--data Add a- where- Add :: Add (Int :-> Int :-> Full Int)--data Mul a- where- Mul :: Mul (Int :-> Int :-> Full Int)--instance Eval Val- where- evaluate (Val a) = Full a--instance Eval Add- where- evaluate Add = Partial $ \a -> Partial $ \b -> Full (a+b)--instance Eval Mul- where- evaluate Mul = Partial $ \a -> Partial $ \b -> Full (a*b)--instance Render Val- where- render (Val a) = show a--instance Render Add- where- render Add = "(+)"--instance Render Mul- where- render Mul = "(*)"------ Manual injection:--addExample :: ASTF (Val :+: Add) Int-addExample = Sym (InjR Add) :$ Sym (InjL (Val 118)) :$ Sym (InjL (Val 1219))------ Automatic injection:--val :: (Val :<: expr) => Int -> ASTF expr Int-val = inj . Val--(<+>) :: (Add :<: expr) => ASTF expr Int -> ASTF expr Int -> ASTF expr Int-a <+> b = inj Add :$ a :$ b--(<*>) :: (Mul :<: expr) => ASTF expr Int -> ASTF expr Int -> ASTF expr Int-a <*> b = inj Mul :$ a :$ b--infixl 6 <+>-infixl 7 <*>--example1 :: ASTF (Add :+: Val) Int-example1 = val 30000 <+> val 1330 <+> val 7--test1 = evaluate example1--example2 :: ASTF (Val :+: Add :+: Mul) Int-example2 = val 80 <*> val 5 <+> val 4--test2 = evaluate example2--example3 :: ASTF (Val :+: Mul) Int-example3 = val 6 <*> val 7--test3 = evaluate example3--example4 :: ASTF (Val :+: Add :+: Mul) Int-example4 = val 80 <*> val 5 <+> val 4--test4 = render example4------ Pattern matching:--distr :: (Add :<: expr, Mul :<: expr) => AST expr a -> AST expr a-distr ((prj -> Just Mul) :$ a :$ b) = case distr b of- (prj -> Just Add) :$ c :$ d -> a' <*> c <+> a' <*> d- b' -> a' <*> b'- where- a' = distr a-distr (f :$ a) = distr f :$ distr a-distr a = a- -- Note the use of direct recursion instead of a fold combinator--example5 :: ASTF (Val :+: Add :+: Mul) Int-example5 = val 80 <*> (val 5 <+> val 4) <+> val 543--test5 = render (distr example5)--example6 :: ASTF (Mul :+: Add :+: Val) Int-example6 = val 444 <*> (val 80 <*> (val 5 <+> val 3 <*> val 4))--test6 = render (distr example6)-
Examples/NanoFeldspar/Core.hs view
@@ -4,7 +4,6 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE UndecidableInstances #-} -- | A minimal Feldspar core language implementation. The intention of this@@ -25,7 +24,6 @@ import Data.Typeable import Language.Syntactic-import Language.Syntactic.Interpretation.Semantics import Language.Syntactic.Constructs.Binding import Language.Syntactic.Constructs.Binding.HigherOrder import Language.Syntactic.Constructs.Condition@@ -43,6 +41,7 @@ -- | 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@@ -57,18 +56,10 @@ where Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a]) -instance WitnessCons Parallel- where- witnessCons Parallel = ConsWit--instance WitnessSat Parallel- where- type SatContext Parallel = SimpleCtx- witnessSat Parallel = SatWit--instance MaybeWitnessSat SimpleCtx Parallel+instance Constrained Parallel where- maybeWitnessSat = maybeWitnessSatDefault+ type Sat Parallel = Type+ exprDict Parallel = Dict instance Semantic Parallel where@@ -77,14 +68,13 @@ , semanticEval = \len ixf -> map ixf [0 .. len-1] } -instance ExprEq Parallel where exprEq = exprEqSem; exprHash = exprHashSem-instance Render Parallel where renderPart = renderPartSem-instance Eval Parallel where evaluate = evaluateSem+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, Parallel :<: dom) =>- AlphaEq Parallel Parallel dom env+instance AlphaEq dom dom dom env => AlphaEq Parallel Parallel dom env where alphaEqSym = alphaEqSymDefault @@ -99,18 +89,10 @@ ForLoop :: Type st => ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st) -instance WitnessCons ForLoop- where- witnessCons ForLoop = ConsWit--instance WitnessSat ForLoop- where- type SatContext ForLoop = SimpleCtx- witnessSat ForLoop = SatWit--instance MaybeWitnessSat SimpleCtx ForLoop+instance Constrained ForLoop where- maybeWitnessSat = maybeWitnessSatDefault+ type Sat ForLoop = Type+ exprDict ForLoop = Dict instance Semantic ForLoop where@@ -120,14 +102,13 @@ } -instance ExprEq ForLoop where exprEq = exprEqSem; exprHash = exprHashSem-instance Render ForLoop where renderPart = renderPartSem-instance Eval ForLoop where evaluate = evaluateSem+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, ForLoop :<: dom) =>- AlphaEq ForLoop ForLoop dom env+instance AlphaEq dom dom dom env => AlphaEq ForLoop ForLoop dom env where alphaEqSym = alphaEqSymDefault @@ -139,16 +120,15 @@ -- | The Feldspar domain type FeldDomain- = Construct SimpleCtx- :+: Literal SimpleCtx- :+: Condition SimpleCtx- :+: Tuple SimpleCtx- :+: Select SimpleCtx- :+: Let SimpleCtx SimpleCtx+ = Construct+ :+: Literal+ :+: Condition+ :+: Tuple+ :+: Select :+: Parallel :+: ForLoop -type FeldDomainAll = HODomain SimpleCtx FeldDomain+type FeldDomainAll = HODomain (Let :+: (FeldDomain :|| Eq :| Show)) Typeable newtype Data a = Data { unData :: ASTF FeldDomainAll a } @@ -165,21 +145,41 @@ +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 (const True)+printFeld = printExpr . reifySmart defaultBindDict2 (const True) -- | Draw the syntax tree drawFeld :: Syntactic a FeldDomainAll => a -> IO ()-drawFeld = drawAST . reifySmart (const True)+drawFeld = drawAST . reifySmart defaultBindDict2 (const True) -- | Evaluation eval :: Syntactic a FeldDomainAll => a -> Internal a-eval = evalBind . reifySmart (const True)+eval = evalBind . reifySmart defaultBindDict2 (const True) @@ -189,7 +189,7 @@ -- | Literal value :: Syntax a => Internal a -> a-value = sugarSymCtx simpleCtx . Literal+value = sugarSymC . Literal false :: Data Bool false = value False@@ -204,7 +204,7 @@ -- | Share a value using let binding share :: (Syntax a, Syntax b) => a -> (a -> b) -> b-share = sugarSym (letBind simpleCtx)+share = sugarSymC Let -- | Alpha equivalence instance Type a => Eq (Data a)@@ -218,28 +218,28 @@ instance (Type a, Num a) => Num (Data a) where fromInteger = value . fromInteger- abs = sugarSymCtx simpleCtx $ Construct "abs" abs- signum = sugarSymCtx simpleCtx $ Construct "signum" signum- (+) = sugarSymCtx simpleCtx $ Construct "(+)" (+)- (-) = sugarSymCtx simpleCtx $ Construct "(-)" (-)- (*) = sugarSymCtx simpleCtx $ Construct "(*)" (*)+ 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) = sugarSymCtx simpleCtx Condition cond t e+cond ? (t,e) = sugarSymC Condition cond t e -- | Parallel array parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]-parallel = sugarSym Parallel+parallel = sugarSymC Parallel forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st-forLoop = sugarSym ForLoop+forLoop = sugarSymC ForLoop arrLength :: Type a => Data [a] -> Data Length-arrLength = sugarSymCtx simpleCtx $ Construct "arrLength" Prelude.length+arrLength = sugarSymC $ Construct "arrLength" Prelude.length -- | Array indexing getIx :: Type a => Data [a] -> Data Index -> Data a-getIx = sugarSymCtx simpleCtx $ Construct "getIx" eval+getIx = sugarSymC $ Construct "getIx" eval where eval as i | i >= len || i < 0 = error "getIx: index out of bounds"@@ -248,14 +248,14 @@ len = Prelude.length as not :: Data Bool -> Data Bool-not = sugarSymCtx simpleCtx $ Construct "not" Prelude.not+not = sugarSymC $ Construct "not" Prelude.not (==) :: Type a => Data a -> Data a -> Data Bool-(==) = sugarSymCtx simpleCtx $ Construct "(==)" (Prelude.==)+(==) = sugarSymC $ Construct "(==)" (Prelude.==) max :: Type a => Data a -> Data a -> Data a-max = sugarSymCtx simpleCtx $ Construct "max" Prelude.max+max = sugarSymC $ Construct "max" Prelude.max min :: Type a => Data a -> Data a -> Data a-min = sugarSymCtx simpleCtx $ Construct "min" Prelude.min+min = sugarSymC $ Construct "min" Prelude.min
Examples/NanoFeldspar/Extra.hs view
@@ -1,18 +1,15 @@-{-# OPTIONS_GHC -fcontext-stack=100 #-}- {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} module NanoFeldspar.Extra where +import Data.Typeable+ import Language.Syntactic import Language.Syntactic.Constructs.Binding import Language.Syntactic.Constructs.Binding.HigherOrder@@ -32,10 +29,10 @@ -- | A predicate deciding which constructs can be shared. Literals and variables -- are not shared.-canShare :: ASTF FeldDomainAll a -> Maybe (SatWit SimpleCtx a)-canShare (prjCtx simpleCtx -> Just (Literal _)) = Nothing-canShare (prjCtx simpleCtx -> Just (Variable _)) = Nothing-canShare a = maybeWitnessSat simpleCtx a+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 ()@@ -62,24 +59,23 @@ -- * Partial evaluation -------------------------------------------------------------------------------- -instance (ForLoop :<: dom, Optimize dom ctx dom) =>- Optimize ForLoop ctx dom+instance Optimize ForLoop where optimizeSym = optimizeSymDefault -instance (Parallel :<: dom, Optimize dom ctx dom) =>- Optimize Parallel ctx dom+instance Optimize Parallel where optimizeSym = optimizeSymDefault constFold :: forall a- . ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a+ . ASTF ((Lambda :+: Variable :+: Let :+: (FeldDomain :|| Eq :| Show)) :|| Typeable) a -> a- -> ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a-constFold expr a = case fmap fromSatWit (maybeWitnessSat simpleCtx expr) of- Just SimpleWit -> appSymCtx simpleCtx $ Literal a- _ -> expr+ -> 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 simpleCtx constFold . reify+drawFeldPart = drawAST . optimize constFold . reify
Examples/NanoFeldspar/Test.hs view
@@ -1,7 +1,5 @@ import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith) -import Language.Syntactic.Constructs.TupleSyntacticSimple- import NanoFeldspar.Core import NanoFeldspar.Extra import NanoFeldspar.Vector
Examples/NanoFeldspar/Vector.hs view
@@ -1,7 +1,7 @@+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeSynonymInstances #-} -- | A simple vector library for NanoFeldspar. The intention of this module is -- to demonstrate how to add language features without extending the underlying@@ -21,7 +21,7 @@ import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith) -import Language.Syntactic+import Language.Syntactic (Syntactic (..), resugar) import NanoFeldspar.Core
Language/Syntactic.hs view
@@ -1,21 +1,27 @@--- | The syntactic library------ The basic functionality is provided by the module--- "Language.Syntactic.Syntax".+-- | The basic parts of the syntactic library module Language.Syntactic ( module Language.Syntactic.Syntax+ , module Language.Syntactic.Traversal+ , module Language.Syntactic.Constraint+ , module Language.Syntactic.Sugar , module Language.Syntactic.Interpretation.Equality , module Language.Syntactic.Interpretation.Render , module Language.Syntactic.Interpretation.Evaluation , module Language.Syntactic.Interpretation.Semantics+ , module Data.Constraint ) where import Language.Syntactic.Syntax+import Language.Syntactic.Traversal+import Language.Syntactic.Constraint+import Language.Syntactic.Sugar import Language.Syntactic.Interpretation.Equality import Language.Syntactic.Interpretation.Render import Language.Syntactic.Interpretation.Evaluation import Language.Syntactic.Interpretation.Semantics++import Data.Constraint (Dict (..))
+ Language/Syntactic/Constraint.hs view
@@ -0,0 +1,262 @@+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Type constrained syntax trees++module Language.Syntactic.Constraint where++++import Data.Constraint++import Language.Syntactic.Syntax+import Language.Syntactic.Interpretation.Equality+import Language.Syntactic.Interpretation.Render+import Language.Syntactic.Interpretation.Evaluation++++--------------------------------------------------------------------------------+-- * Type predicates+--------------------------------------------------------------------------------++-- | Intersection of type predicates+class (c1 a, c2 a) => (c1 :/\: c2) a+instance (c1 a, c2 a) => (c1 :/\: c2) a++infixr 5 :/\:++-- | Universal type predicate+class Top a+instance Top a++-- | Evidence that the predicate @sub@ is a subset of @sup@+type Sub sub sup = forall a . Dict (sub a) -> Dict (sup a)++-- | Weaken an intersection+weakL :: Sub (c1 :/\: c2) c1+weakL Dict = Dict++-- | Weaken an intersection+weakR :: Sub (c1 :/\: c2) c2+weakR Dict = Dict++-- | Subset relation on type predicates+class sub :< sup+ where+ -- | Compute evidence that @sub@ is a subset of @sup@ (i.e. that @(sup a)@+ -- implies @(sub a)@)+ sub :: Sub sub sup++instance p :< p+ where+ sub = id++instance (p :/\: ps) :< p+ where+ sub = weakL++instance (ps :< q) => ((p :/\: ps) :< q)+ where+ sub = sub . weakR++++--------------------------------------------------------------------------------+-- * Constrained syntax+--------------------------------------------------------------------------------++-- | Constrain the result type of the expression by the given predicate+data (expr :| pred) sig+ where+ C :: pred (DenResult sig) => expr sig -> (expr :| pred) sig++infixl 4 :|++instance Project sub sup => Project sub (sup :| pred)+ where+ prj (C s) = prj s++instance Equality dom => Equality (dom :| pred)+ where+ equal (C a) (C b) = equal a b+ exprHash (C a) = exprHash a++instance Render dom => Render (dom :| pred)+ where+ renderArgs args (C a) = renderArgs args a++instance Eval dom => Eval (dom :| pred)+ where+ evaluate (C a) = evaluate a++instance ToTree dom => ToTree (dom :| pred)+ where+ toTreeArgs args (C a) = toTreeArgs args a++++-- | Constrain the result type of the expression by the given predicate+--+-- The difference between ':||' and ':|' is seen in the instances of the 'Sat'+-- type:+--+-- > type Sat (dom :| pred) = pred :/\: Sat dom+-- > type Sat (dom :|| pred) = pred+data (expr :|| pred) sig+ where+ C' :: pred (DenResult sig) => expr sig -> (expr :|| pred) sig++infixl 4 :||++instance Project sub sup => Project sub (sup :|| pred)+ where+ prj (C' s) = prj s++instance Equality dom => Equality (dom :|| pred)+ where+ equal (C' a) (C' b) = equal a b+ exprHash (C' a) = exprHash a++instance Render dom => Render (dom :|| pred)+ where+ renderArgs args (C' a) = renderArgs args a++instance Eval dom => Eval (dom :|| pred)+ where+ evaluate (C' a) = evaluate a++instance ToTree dom => ToTree (dom :|| pred)+ where+ toTreeArgs args (C' a) = toTreeArgs args a++++-- | Expressions that constrain their result types+class Constrained expr+ where+ -- | Returns a predicate that is satisfied by the result type of all+ -- expressions of the given type (see 'exprDict').+ type Sat (expr :: * -> *) :: * -> Constraint++ -- | Compute a constraint on the result type of an expression+ exprDict :: expr a -> Dict (Sat expr (DenResult a))++instance Constrained dom => Constrained (AST dom)+ where+ type Sat (AST dom) = Sat dom+ exprDict (Sym s) = exprDict s+ exprDict (s :$ _) = exprDict s++instance Constrained (sub1 :+: sub2)+ where+ -- | An over-approximation of the union of @Sat sub1@ and @Sat sub2@+ type Sat (sub1 :+: sub2) = Top+ exprDict (InjL s) = Dict+ exprDict (InjR s) = Dict++instance Constrained dom => Constrained (dom :| pred)+ where+ type Sat (dom :| pred) = pred :/\: Sat dom+ exprDict (C s) = case exprDict s of Dict -> Dict++instance Constrained (dom :|| pred)+ where+ type Sat (dom :|| pred) = pred+ exprDict (C' s) = Dict++type ConstrainedBy expr c = (Constrained expr, Sat expr :< c)++-- | A version of 'exprDict' that returns a constraint for a particular+-- predicate @p@ as long as @(p :< Sat dom)@ holds+exprDictSub :: ConstrainedBy expr p => expr a -> Dict (p (DenResult a))+exprDictSub = sub . exprDict++-- | A version of 'exprDict' that works for domains of the form+-- @(dom1 :+: dom2)@ as long as @(Sat dom1 ~ Sat dom2)@ holds+exprDictPlus :: (Constrained dom1, Constrained dom2, Sat dom1 ~ Sat dom2) =>+ AST (dom1 :+: dom2) a -> Dict (Sat dom1 (DenResult a))+exprDictPlus (s :$ _) = exprDictPlus s+exprDictPlus (Sym (InjL a)) = exprDict a+exprDictPlus (Sym (InjR a)) = exprDict a++++-- | Symbol injection (like ':<:') with constrained result types+class (Project sub sup, Sat sup a) => InjectC sub sup a+ where+ injC :: (DenResult sig ~ a) => sub sig -> sup sig++instance InjectC sub sup sig => InjectC sub (AST sup) sig+ where+ injC = Sym . injC++instance (InjectC sub sup sig, pred sig) => InjectC sub (sup :| pred) sig+ where+ injC = C . injC++instance (InjectC sub sup sig, pred sig) => InjectC sub (sup :|| pred) sig+ where+ injC = C' . injC++instance Sat expr sig => InjectC expr expr sig+ where+ injC = id++instance InjectC expr1 (expr1 :+: expr2) sig+ where+ injC = InjL++instance InjectC expr1 expr3 sig => InjectC expr1 (expr2 :+: expr3) sig+ where+ injC = InjR . injC++++-- | Generic symbol application+--+-- 'appSymC' has any type of the form:+--+-- > appSymC :: InjectC expr (AST dom) x+-- > => expr (a :-> b :-> ... :-> Full x)+-- > -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)+appSymC :: (ApplySym sig f dom, InjectC sym (AST dom) (DenResult sig)) =>+ sym sig -> f+appSymC = appSym' . injC++++-- | 'AST' with existentially quantified result type+data ASTE dom+ where+ ASTE :: ASTF dom a -> ASTE dom++liftASTE+ :: (forall a . ASTF dom a -> b)+ -> ASTE dom+ -> b+liftASTE f (ASTE a) = f a++liftASTE2+ :: (forall a b . ASTF dom a -> ASTF dom b -> c)+ -> ASTE dom -> ASTE dom -> c+liftASTE2 f (ASTE a) (ASTE b) = f a b++++-- | 'AST' with bounded existentially quantified result type+data ASTB dom+ where+ ASTB :: Sat dom a => ASTF dom a -> ASTB dom++liftASTB+ :: (forall a . Sat dom a => ASTF dom a -> b)+ -> ASTB dom+ -> b+liftASTB f (ASTB a) = f a++liftASTB2+ :: (forall a b . (Sat dom a, Sat dom b) => ASTF dom a -> ASTF dom b -> c)+ -> ASTB dom -> ASTB dom -> c+liftASTB2 f (ASTB a) (ASTB b) = f a b+
Language/Syntactic/Constructs/Binding.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE UndecidableInstances #-} -- | General binding constructs@@ -9,13 +8,14 @@ import qualified Control.Monad.Identity as Monad import Control.Monad.Reader-import Data.Dynamic 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@@ -45,46 +45,33 @@ -- | Variables-data Variable ctx a- where- Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a)- -- 'Typeable' needed by the dynamic types in 'evalBind'.--instance WitnessCons (Variable ctx)- where- witnessCons (Variable _) = ConsWit--instance WitnessSat (Variable ctx)- where- type SatContext (Variable ctx) = ctx- witnessSat (Variable _) = SatWit--instance MaybeWitnessSat ctx (Variable ctx)+data Variable a where- maybeWitnessSat = maybeWitnessSatDefault+ Variable :: VarId -> Variable (Full a) -instance MaybeWitnessSat ctx1 (Variable ctx2)+instance Constrained Variable where- maybeWitnessSat _ _ = Nothing+ type Sat Variable = Top+ exprDict _ = Dict --- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence.+-- | '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 ExprEq (Variable ctx)+instance Equality Variable where- exprEq (Variable v1) (Variable v2) = v1==v2- exprHash (Variable _) = hashInt 0+ equal (Variable v1) (Variable v2) = v1==v2+ exprHash (Variable _) = hashInt 0 -instance Render (Variable ctx)+instance Render Variable where render (Variable v) = showVar v -instance ToTree (Variable ctx)+instance ToTree Variable where- toTreePart [] (Variable v) = Node ("var:" ++ show v) []+ toTreeArgs [] (Variable v) = Node ("var:" ++ show v) [] @@ -93,38 +80,33 @@ -------------------------------------------------------------------------------- -- | Lambda binding-data Lambda ctx a- where- Lambda :: (Typeable a, Sat ctx a) =>- VarId -> Lambda ctx (b :-> Full (a -> b))- -- 'Typeable' needed by the dynamic types in 'evalBind'.--instance WitnessCons (Lambda ctx)+data Lambda a where- witnessCons (Lambda _) = ConsWit+ Lambda :: VarId -> Lambda (b :-> Full (a -> b)) -instance MaybeWitnessSat ctx1 (Lambda ctx2)+instance Constrained Lambda where- maybeWitnessSat _ _ = Nothing+ type Sat Lambda = Top+ exprDict _ = Dict --- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence.+-- | '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 ExprEq (Lambda ctx)+instance Equality Lambda where- exprEq (Lambda v1) (Lambda v2) = v1==v2- exprHash (Lambda _) = hashInt 0+ equal (Lambda v1) (Lambda v2) = v1==v2+ exprHash (Lambda _) = hashInt 0 -instance Render (Lambda ctx)+instance Render Lambda where- renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> " ++ body ++ ")"+ renderArgs [body] (Lambda v) = "(\\" ++ showVar v ++ " -> " ++ body ++ ")" -instance ToTree (Lambda ctx)+instance ToTree Lambda where- toTreePart [body] (Lambda v) = Node ("Lambda " ++ show v) [body]+ toTreeArgs [body] (Lambda v) = Node ("Lambda " ++ show v) [body] @@ -134,62 +116,39 @@ -- | Let binding ----- A 'Let' expression is really just an application of a lambda binding (the--- argument @(a -> b)@ is preferably constructed by 'Lambda').-data Let ctxa ctxb a- where- Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> (a -> b) :-> Full b)--instance WitnessCons (Let ctxa ctxb)- where- witnessCons Let = ConsWit--instance WitnessSat (Let ctxa ctxb)- where- type SatContext (Let ctxa ctxb) = ctxb- witnessSat Let = SatWit--instance MaybeWitnessSat ctxb (Let ctxa ctxb)+-- 'Let' is just an application operator with flipped argument order. The argument+-- @(a -> b)@ is preferably constructed by 'Lambda'.+data Let a where- maybeWitnessSat = maybeWitnessSatDefault+ Let :: Let (a :-> (a -> b) :-> Full b) -instance MaybeWitnessSat ctx (Let ctxa ctxb)+instance Constrained Let where- maybeWitnessSat _ _ = Nothing+ type Sat Let = Top+ exprDict _ = Dict -instance ExprEq (Let ctxa ctxb)+instance Equality Let where- exprEq Let Let = True-- exprHash Let = hashInt 0+ equal Let Let = True+ exprHash Let = hashInt 0 -instance Render (Let ctxa ctxb)+instance Render Let where- renderPart [] Let = "Let"- renderPart [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")"+ renderArgs [] Let = "Let"+ renderArgs [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")" -instance ToTree (Let ctxa ctxb)+instance ToTree Let where- toTreePart [a,body] Let = case splitAt 7 node of+ 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+ Node node ~[body'] = body+ var = drop 7 node -- Drop the "Lambda " prefix -instance Eval (Let ctxa ctxb)+instance Eval Let where- evaluate Let = fromEval (flip ($))---- | Let binding with explicit context-letBind :: (Sat ctx a, Sat ctx b) =>- Proxy ctx -> Let ctx ctx (a :-> (a -> b) :-> Full b)-letBind _ = Let---- | Partial `Let` projection with explicit context-prjLet :: (Let ctxa ctxb :<: sup) =>- Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)-prjLet _ _ = prj+ evaluate Let = flip ($) @@ -197,45 +156,63 @@ -- * Interpretation -------------------------------------------------------------------------------- --- | Capture-avoiding substitution-subst :: forall ctx dom a b- . (Lambda ctx :<: dom, Variable ctx :<: dom, Typeable a)- => Proxy ctx- -> VarId -- ^ Variable to be substituted+-- | 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 ctx v new a = go a+subst v new a = go a where go :: AST dom c -> AST dom c- go a@((prjCtx ctx -> Just (Lambda w)) :$ _)+ go a@((prj -> Just (Lambda w)) :$ _) | v==w = a -- Capture go (f :$ a) = go f :$ go a- go (prjCtx ctx -> Just (Variable w))- | v==w+ 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 :: forall ctx dom a b . (Lambda ctx :<: dom, Variable ctx :<: dom)- => Proxy ctx- -> ASTF dom a -- ^ Argument+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 ctx new ((prjCtx ctx -> Just (Lambda v)) :$ body) =- subst ctx v new body+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, Signature a)- => sub a- -> Args (AST dom) a- -> Reader [(VarId,Dynamic)] (DenResult a)+ :: (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@@ -243,55 +220,76 @@ evalBindSym (InjR a) = evalBindSym a -- | Evaluation of possibly open expressions-evalBindM :: EvalBind dom => ASTF dom a -> Reader [(VarId,Dynamic)] a-evalBindM = liftM result . queryNode (\a -> liftM Full . evalBindSym a)+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 => ASTF dom a -> a+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, Signature a, EvalBind dom)- => sub a- -> Args (AST dom) a- -> Reader [(VarId,Dynamic)] (DenResult a)+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 $ appEvalArgs (toEval $ evaluate sym) args'+ return $ appDen (evaluate sym) args' -instance EvalBind (Identity ctx) where evalBindSym = evalBindSymDefault-instance EvalBind (Construct ctx) where evalBindSym = evalBindSymDefault-instance EvalBind (Literal ctx) where evalBindSym = evalBindSymDefault-instance EvalBind (Condition ctx) where evalBindSym = evalBindSymDefault-instance EvalBind (Tuple ctx) where evalBindSym = evalBindSymDefault-instance EvalBind (Select ctx) where evalBindSym = evalBindSymDefault-instance EvalBind (Let ctxa ctxb) where evalBindSym = evalBindSymDefault-instance Monad m => EvalBind (MONAD m) where evalBindSym = evalBindSymDefault+instance EvalBind dom => EvalBind (dom :| pred)+ where+ evalBindSym (C a) = evalBindSym a -instance EvalBind dom => EvalBind (Decor info dom)+instance EvalBind dom => EvalBind (dom :|| pred) where- evalBindSym a args = evalBindSym (decorExpr a) args+ evalBindSym (C' a) = evalBindSym a -instance EvalBind (Lambda ctx)+instance EvalBind dom => EvalBind (Decor info dom) where- evalBindSym (Lambda v) (body :* Nil) = do- env <- ask- return- $ \a -> flip runReader ((v,toDyn a):env)- $ evalBindM body+ evalBindSym = evalBindSym . decorExpr -instance EvalBind (Variable ctx)+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 fromDynamic a of+ 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 --------------------------------------------------------------------------------@@ -307,11 +305,11 @@ prjVarEqEnv = id modVarEqEnv = id +-- | Alpha-equivalence class AlphaEq sub1 sub2 dom env where alphaEqSym- :: (Signature a, Signature b)- => sub1 a+ :: sub1 a -> Args (AST dom) a -> sub2 b -> Args (AST dom) b@@ -322,16 +320,15 @@ 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 (InjL a) aArgs (InjR b) bArgs = return False- alphaEqSym (InjR a) aArgs (InjL b) bArgs = return False+ alphaEqSym _ _ _ _ = return False alphaEqM :: AlphaEq dom dom dom env => ASTF dom a -> ASTF dom b -> Reader env Bool-alphaEqM a b = queryNodeSimple (alphaEqM2 b) a+alphaEqM a b = simpleMatch (alphaEqM2 b) a -alphaEqM2 :: (AlphaEq dom dom dom env, Signature a) =>+alphaEqM2 :: AlphaEq dom dom dom env => ASTF dom b -> dom a -> Args (AST dom) a -> Reader env Bool-alphaEqM2 b a aArgs = queryNodeSimple (alphaEqSym a aArgs) b+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.@@ -339,20 +336,15 @@ ASTF dom a -> ASTF dom b -> Bool alphaEq a b = flip runReader ([] :: [(VarId,VarId)]) $ alphaEqM a b -alphaEqSymDefault- :: ( ExprEq sub- , AlphaEq dom dom dom env- , Signature a- , Signature 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- | exprEq a b = alphaEqChildren a' b'- | otherwise = return False+ | equal a b = alphaEqChildren a' b'+ | otherwise = return False where a' = appArgs (Sym (undefined :: dom a)) aArgs b' = appArgs (Sym (undefined :: dom b)) bArgs@@ -365,36 +357,44 @@ (alphaEqM a b) alphaEqChildren _ _ = return False -instance AlphaEq dom dom dom env => AlphaEq (Identity ctx) (Identity ctx) dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq (Construct ctx) (Construct ctx) dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq (Literal ctx) (Literal ctx) dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq (Condition ctx) (Condition ctx) dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq (Tuple ctx) (Tuple ctx) dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq (Select ctx) (Select ctx) dom env where alphaEqSym = alphaEqSymDefault-instance AlphaEq dom dom dom env => AlphaEq (Let ctxa ctxb) (Let ctxa ctxb) dom env where alphaEqSym = alphaEqSymDefault+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, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env+instance AlphaEq sub sub dom env => AlphaEq (sub :|| pred) (sub :|| pred) dom env where- alphaEqSym = alphaEqSymDefault+ alphaEqSym (C' a) aArgs (C' b) bArgs = alphaEqSym a aArgs b bArgs -instance AlphaEq dom dom (Decor info dom) env =>- AlphaEq (Decor info dom) (Decor info dom) (Decor info dom) env+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, VarEqEnv env) =>- AlphaEq (Lambda ctx) (Lambda ctx) dom env+instance (AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env where- alphaEqSym (Lambda v1) (body1 :* Nil) (Lambda v2) (body2 :* Nil) =- local (modVarEqEnv ((v1,v2):)) $ alphaEqM body1 body2+ alphaEqSym = alphaEqSymDefault instance (AlphaEq dom dom dom env, VarEqEnv env) =>- AlphaEq (Variable ctx) (Variable ctx) dom env+ AlphaEq Variable Variable dom env where alphaEqSym (Variable v1) Nil (Variable v2) Nil = do env <- asks prjVarEqEnv case lookup v1 env of Nothing -> return (v1==v2) -- Free variables Just v2' -> return (v2==v2')++instance (AlphaEq dom dom dom env, VarEqEnv env) =>+ AlphaEq Lambda Lambda dom env+ where+ alphaEqSym (Lambda v1) (body1 :* Nil) (Lambda v2) (body2 :* Nil) =+ local (modVarEqEnv ((v1,v2):)) $ alphaEqM body1 body2
Language/Syntactic/Constructs/Binding/HigherOrder.hs view
@@ -1,8 +1,9 @@ {-# LANGUAGE UndecidableInstances #-} -- | This module provides binding constructs using higher-order syntax and a--- function for translating to first-order syntax. Expressions constructed using--- the exported interface are guaranteed to have a well-behaved translation.+-- 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@@ -18,78 +19,72 @@ import Control.Monad.State-import Data.Typeable -import Data.Proxy- import Language.Syntactic import Language.Syntactic.Constructs.Binding -- | Higher-order lambda binding-data HOLambda ctx dom a+data HOLambda dom p a where- HOLambda :: (Typeable a, Typeable b, Sat ctx a)- => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b)- -> HOLambda ctx dom (Full (a -> b))--type HODomain ctx dom = HOLambda ctx dom :+: Variable ctx :+: dom+ HOLambda+ :: p a+ => (ASTF (HODomain dom p) a -> ASTF (HODomain dom p) b)+ -> HOLambda dom p (Full (a -> b)) -instance WitnessCons (HOLambda ctx dom)- where- witnessCons (HOLambda _) = ConsWit+type HODomain dom p = (HOLambda dom p :+: Variable :+: dom) :|| p -instance MaybeWitnessSat ctx1 (HOLambda ctx2 dom)+instance Constrained (HOLambda dom p) where- maybeWitnessSat _ _ = Nothing+ type Sat (HOLambda dom p) = Top+ exprDict _ = Dict -- | Lambda binding-lambda :: (Typeable a, Typeable b, Sat ctx a)- => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b)- -> ASTF (HODomain ctx dom) (a -> b)-lambda = inj . HOLambda+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 ctx dom)- , Syntactic b (HODomain ctx dom)- , Sat ctx (Internal a)+ ( Syntactic a (HODomain dom p)+ , Syntactic b (HODomain dom p)+ , p (Internal a)+ , p (Internal a -> Internal b) ) =>- Syntactic (a -> b) (HODomain ctx dom)+ 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?+ -- application. Perhaps use `Let` for this? -reifyM :: forall ctx dom a . Typeable a- => AST (HODomain ctx dom) a- -> State VarId (AST (Lambda ctx :+: Variable ctx :+: dom) a)-reifyM (f :$ a) = liftM2 (:$) (reifyM f) (reifyM a)-reifyM (Sym (InjR a)) = return $ Sym $ InjR a-reifyM (Sym (InjL (HOLambda f))) = do+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 $ inj $ (Variable v `withContext` ctx)- return $ inj (Lambda v `withContext` ctx) :$ body- where- ctx = Proxy :: Proxy ctx+ 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 :: Typeable a =>- AST (HODomain ctx dom) a -> AST (Lambda ctx :+: Variable ctx :+: dom) a+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. --- | Reifying an n-ary syntactic function-reify :: Syntactic a (HODomain ctx dom)- => a- -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a)+-- | Reify an n-ary syntactic function+reify :: Syntactic a (HODomain dom p) =>+ a -> ASTF ((Lambda :+: Variable :+: dom) :|| p) (Internal a) reify = reifyTop . desugar
Language/Syntactic/Constructs/Binding/Optimize.hs view
@@ -1,14 +1,11 @@-{-# LANGUAGE UndecidableInstances #-}---- | Basic optimization of expressions+-- | Basic optimization module Language.Syntactic.Constructs.Binding.Optimize where import Control.Monad.Writer import Data.Set as Set--import Data.Proxy+import Data.Typeable import Language.Syntactic import Language.Syntactic.Constructs.Binding@@ -28,10 +25,10 @@ -- are satisfied. type ConstFolder dom = forall a . ASTF dom a -> a -> ASTF dom a --- | Basic optimization of a sub-domain-class EvalBind dom => Optimize sub ctx dom+-- | Basic optimization+class Optimize sym where- -- | Bottom-up optimization of a sub-domain. The optimization performed is+ -- | 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@@ -44,93 +41,90 @@ -- > 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 syntax tree.+ -- turn, can lead to more constant folding higher up in the expression. optimizeSym- :: Proxy ctx- -> ConstFolder dom- -> sub a- -> Args (AST dom) a- -> Writer (Set VarId) (ASTF dom (DenResult a))+ :: 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- -- require the constraint @(sub :<: dom)@. If @dom@ was forall-quantified in- -- 'optimizeSym', this constraint would not be allowed. On the other hand, it- -- is not possible to add the constraint @(sub :<: dom)@ to 'optimizeSym',- -- because the instance for '(:+:)' doesn't satisfy it.+ -- need to put additional constraints on @dom@. -instance (Optimize sub1 ctx dom, Optimize sub2 ctx dom) =>- Optimize (sub1 :+: sub2) ctx 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 ctx constFold (InjL a) = optimizeSym ctx constFold a- optimizeSym ctx constFold (InjR a) = optimizeSym ctx constFold a+ optimizeSym constFold injecter (InjL a) = optimizeSym constFold (injecter . InjL) a+ optimizeSym constFold injecter (InjR a) = optimizeSym constFold (injecter . InjR) a -optimizeM :: Optimize dom ctx dom- => Proxy ctx- -> ConstFolder dom+optimizeM :: Optimize' dom+ => ConstFolder dom -> ASTF dom a -> Writer (Set VarId) (ASTF dom a)-optimizeM ctx constFold = transformNode (optimizeSym ctx constFold)+optimizeM constFold = matchTrans (optimizeSym constFold Sym) -- | Optimize an expression-optimize :: Optimize dom ctx dom =>- Proxy ctx -> ConstFolder dom -> ASTF dom a -> ASTF dom a-optimize ctx constFold = fst . runWriter . optimizeM ctx constFold+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- :: ( sub :<: dom- , WitnessCons sub- , Optimize dom ctx dom- )- => Proxy ctx- -> ConstFolder dom- -> sub a- -> Args (AST dom) a- -> Writer (Set VarId) (ASTF dom (DenResult a))-optimizeSymDefault ctx constFold sym@(witnessCons -> ConsWit) args = do- (args',vars) <- listen $ mapArgsM (optimizeM ctx constFold) args- let result = appArgs (Sym $ inj sym) args'+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 (Identity ctx' :<: dom, Optimize dom ctx dom) => Optimize (Identity ctx') ctx dom where optimizeSym = optimizeSymDefault-instance (Construct ctx' :<: dom, Optimize dom ctx dom) => Optimize (Construct ctx') ctx dom where optimizeSym = optimizeSymDefault-instance (Literal ctx' :<: dom, Optimize dom ctx dom) => Optimize (Literal ctx') ctx dom where optimizeSym = optimizeSymDefault-instance (Tuple ctx' :<: dom, Optimize dom ctx dom) => Optimize (Tuple ctx') ctx dom where optimizeSym = optimizeSymDefault-instance (Select ctx' :<: dom, Optimize dom ctx dom) => Optimize (Select ctx') ctx dom where optimizeSym = optimizeSymDefault-instance (Let ctxa ctxb :<: dom, Optimize dom ctx dom) => Optimize (Let ctxa ctxb) ctx dom where optimizeSym = optimizeSymDefault+instance Optimize dom => Optimize (dom :| p)+ where+ optimizeSym cf i (C s) args = optimizeSym cf (i . C) s args -instance- ( Condition ctx' :<: dom- , Lambda ctx :<: dom- , Variable ctx :<: dom- , AlphaEq dom dom dom [(VarId,VarId)]- , Optimize dom ctx dom- ) =>- Optimize (Condition ctx') ctx dom+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 ctx constFold cond@Condition args@(c :* t :* e :* Nil)- | Set.null cVars = optimizeM ctx constFold t_or_e- | alphaEq t e = optimizeM ctx constFold t- | otherwise = optimizeSymDefault ctx constFold cond args+ 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 ctx constFold c+ (c',cVars) = runWriter $ optimizeM constFold c t_or_e = if evalBind c' then t else e -instance (Variable ctx :<: dom, Optimize dom ctx dom) =>- Optimize (Variable ctx) ctx dom+instance Optimize Variable where- optimizeSym _ _ var@(Variable v) Nil = do+ optimizeSym _ injecter var@(Variable v) Nil = do tell (singleton v)- return (inj var)+ return (injecter var) -instance (Lambda ctx :<: dom, Optimize dom ctx dom) =>- Optimize (Lambda ctx) ctx dom+instance Optimize Lambda where- optimizeSym ctx constFold lam@(Lambda v) (body :* Nil) = do- body' <- censor (delete v) $ optimizeM ctx constFold body- return $ inj lam :$ body'+ optimizeSym constFold injecter lam@(Lambda v) (body :* Nil) = do+ body' <- censor (delete v) $ optimizeM constFold body+ return $ injecter lam :$ body'
Language/Syntactic/Constructs/Condition.hs view
@@ -1,46 +1,28 @@-{-# LANGUAGE OverlappingInstances #-}- -- | Conditional expressions module Language.Syntactic.Constructs.Condition where -import Data.Proxy-import Data.Typeable- import Language.Syntactic-import Language.Syntactic.Interpretation.Semantics -data Condition ctx a- where- Condition :: Sat ctx a => Condition ctx (Bool :-> a :-> a :-> Full a)--instance WitnessCons (Condition ctx)- where- witnessCons Condition = ConsWit--instance WitnessSat (Condition ctx)- where- type SatContext (Condition ctx) = ctx- witnessSat Condition = SatWit--instance MaybeWitnessSat ctx (Condition ctx)+data Condition sig where- maybeWitnessSat = maybeWitnessSatDefault+ Condition :: Condition (Bool :-> a :-> a :-> Full a) -instance MaybeWitnessSat ctx1 (Condition ctx2)+instance Constrained Condition where- maybeWitnessSat _ _ = Nothing+ type Sat Condition = Top+ exprDict _ = Dict -instance Semantic (Condition ctx)+instance Semantic Condition where semantics Condition = Sem "condition" (\c t e -> if c then t else e) -instance ExprEq (Condition ctx) where exprEq = exprEqSem; exprHash = exprHashSem-instance Render (Condition ctx) where renderPart = renderPartSem-instance Eval (Condition ctx) where evaluate = evaluateSem-instance ToTree (Condition ctx)+instance Equality Condition where equal = equalDefault; exprHash = exprHashDefault+instance Render Condition where renderArgs = renderArgsDefault+instance Eval Condition where evaluate = evaluateDefault+instance ToTree Condition
Language/Syntactic/Constructs/Construct.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE OverlappingInstances #-}- -- | 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@@ -9,60 +7,25 @@ -import Data.Typeable--import Data.Hash-import Data.Proxy- import Language.Syntactic -data Construct ctx a- where- Construct :: (Signature a, Sat ctx (DenResult a)) =>- String -> Denotation a -> Construct ctx a--instance WitnessCons (Construct ctx)- where- witnessCons (Construct _ _) = ConsWit--instance WitnessSat (Construct ctx)- where- type SatContext (Construct ctx) = ctx- witnessSat (Construct _ _) = SatWit--instance MaybeWitnessSat ctx (Construct ctx)- where- maybeWitnessSat = maybeWitnessSatDefault--instance MaybeWitnessSat ctx1 (Construct ctx2)+data Construct sig where- maybeWitnessSat _ _ = Nothing+ Construct :: String -> Denotation sig -> Construct sig -instance ExprEq (Construct ctx)+instance Constrained Construct where- exprEq (Construct a _) (Construct b _) = a==b- exprHash (Construct name _) = hash name+ type Sat Construct = Top+ exprDict _ = Dict -instance Render (Construct ctx)+instance Semantic Construct where- renderPart [] (Construct name _) = name- renderPart args (Construct name _)- | isInfix = "(" ++ unwords [a,op,b] ++ ")"- | otherwise = "(" ++ unwords (name : args) ++ ")"- where- [a,b] = args- op = init $ tail name- isInfix- = not (null name)- && head name == '('- && last name == ')'- && length args == 2--instance ToTree (Construct ctx)+ semantics (Construct name den) = Sem name den -instance Eval (Construct ctx)- where- evaluate (Construct _ a) = fromEval a+instance Equality Construct where equal = equalDefault; exprHash = exprHashDefault+instance Render Construct where renderArgs = renderArgsDefault+instance Eval Construct where evaluate = evaluateDefault+instance ToTree Construct
Language/Syntactic/Constructs/Decoration.hs view
@@ -4,15 +4,9 @@ -import Control.Monad.Identity import Data.Tree -import Data.Proxy--import Language.Syntactic.Syntax-import Language.Syntactic.Interpretation.Equality-import Language.Syntactic.Interpretation.Evaluation-import Language.Syntactic.Interpretation.Render+import Language.Syntactic @@ -20,55 +14,49 @@ -- * Decoration -------------------------------------------------------------------------------- --- | Decorating an expression with additional information+-- | 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 a+-- > AST dom sig -- -- to ----- > AST (Decor info dom) a+-- > AST (Decor info dom) sig -- -- Injection\/projection of an decorated tree is done using 'injDecor' \/ -- 'prjDecor'.-data Decor info expr a+data Decor info expr sig where Decor- :: { decorInfo :: info (DenResult a)- , decorExpr :: expr a+ :: { decorInfo :: info (DenResult sig)+ , decorExpr :: expr sig }- -> Decor info expr a----instance WitnessCons dom => WitnessCons (Decor info dom)- where- witnessCons (Decor _ a) = witnessCons a+ -> Decor info expr sig -instance WitnessSat expr => WitnessSat (Decor info expr)+instance Constrained expr => Constrained (Decor info expr) where- type SatContext (Decor info expr) = SatContext expr- witnessSat (Decor _ a) = witnessSat a+ type Sat (Decor info expr) = Sat expr+ exprDict (Decor _ a) = exprDict a -instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (Decor info dom)+instance Project sub sup => Project sub (Decor info sup) where- maybeWitnessSat ctx (Decor _ a) = maybeWitnessSat ctx a+ prj = prj . decorExpr -instance ExprEq expr => ExprEq (Decor info expr)+instance Equality expr => Equality (Decor info expr) where- exprEq a b = decorExpr a `exprEq` decorExpr b- exprHash = exprHash . decorExpr+ equal a b = decorExpr a `equal` decorExpr b+ exprHash = exprHash . decorExpr instance Render expr => Render (Decor info expr) where- renderPart args = renderPart args . decorExpr+ renderArgs args = renderArgs args . decorExpr render = render . decorExpr instance ToTree expr => ToTree (Decor info expr) where- toTreePart args = toTreePart args . decorExpr+ toTreeArgs args = toTreeArgs args . decorExpr instance Eval expr => Eval (Decor info expr) where@@ -76,47 +64,33 @@ -injDecor :: (sub :<: sup, Signature a) =>- info (DenResult a) -> sub a -> AST (Decor info sup) a+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) a -> Maybe (info (DenResult a), sub a)+ 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) --- | 'injDecor' with explicit context-injDecorCtx :: (sub ctx :<: sup, Signature a) =>- Proxy ctx -> info (DenResult a) -> sub ctx a -> AST (Decor info sup) a-injDecorCtx ctx info = Sym . Decor info . injCtx ctx---- | 'prjDecor' with explicit context-prjDecorCtx :: (sub ctx :<: sup)- => Proxy ctx -> AST (Decor info sup) a- -> Maybe (info (DenResult a), sub ctx a)-prjDecorCtx ctx a = do- Sym (Decor info b) <- return a- c <- prjCtx ctx b- return (info, c)- -- | Get the decoration of the top-level node-getInfo :: AST (Decor info dom) a -> info (DenResult a)+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 = runIdentity . transformNode update+updateDecor f = match update where update- :: (Signature b, a ~ DenResult b)- => Decor info dom b- -> Args (AST (Decor info dom)) b- -> Identity (ASTF (Decor info dom) a)- update (Decor info a) args = Identity $ appArgs (Sym sym) args+ :: (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 @@ -124,11 +98,11 @@ -- 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 a -> info (DenResult a) -> b) -> (Decor info expr a -> b)+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 a . info a -> b) -> AST (Decor info dom) a -> [b]+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 @@ -137,8 +111,8 @@ ASTF (Decor info dom) a -> Tree String toTreeDecor a = mkTree [] a where- mkTree :: [Tree String] -> AST (Decor info dom) b -> Tree String- mkTree args (Sym (Decor info expr)) = Node infoStr [toTreePart args expr]+ 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@@ -152,7 +126,7 @@ drawDecor = putStrLn . showDecor -- | Strip decorations from an 'AST'-stripDecor :: AST (Decor info dom) a -> AST dom a+stripDecor :: AST (Decor info dom) sig -> AST dom sig stripDecor (Sym (Decor _ a)) = Sym a stripDecor (f :$ a) = stripDecor f :$ stripDecor a
Language/Syntactic/Constructs/Identity.hs view
@@ -1,47 +1,29 @@-{-# LANGUAGE OverlappingInstances #-}- -- | Identity function module Language.Syntactic.Constructs.Identity where -import Data.Proxy-import Data.Typeable- import Language.Syntactic-import Language.Syntactic.Interpretation.Semantics -- | Identity function-data Identity ctx a- where- Id :: Sat ctx a => Identity ctx (a :-> Full a)--instance WitnessCons (Identity ctx)- where- witnessCons Id = ConsWit--instance WitnessSat (Identity ctx)- where- type SatContext (Identity ctx) = ctx- witnessSat Id = SatWit--instance MaybeWitnessSat ctx (Identity ctx)+data Identity sig where- maybeWitnessSat = maybeWitnessSatDefault+ Id :: Identity (a :-> Full a) -instance MaybeWitnessSat ctx1 (Identity ctx2)+instance Constrained Identity where- maybeWitnessSat _ _ = Nothing+ type Sat Identity = Top+ exprDict _ = Dict -instance Semantic (Identity ctx)+instance Semantic Identity where semantics Id = Sem "id" id -instance ExprEq (Identity ctx) where exprEq = exprEqSem; exprHash = exprHashSem-instance Render (Identity ctx) where renderPart = renderPartSem-instance Eval (Identity ctx) where evaluate = evaluateSem-instance ToTree (Identity ctx)+instance Equality Identity where equal = equalDefault; exprHash = exprHashDefault+instance Render Identity where renderArgs = renderArgsDefault+instance Eval Identity where evaluate = evaluateDefault+instance ToTree Identity
Language/Syntactic/Constructs/Literal.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE OverlappingInstances #-}- -- | Literal expressions module Language.Syntactic.Constructs.Literal where@@ -9,49 +7,35 @@ import Data.Typeable import Data.Hash-import Data.Proxy import Language.Syntactic -data Literal ctx a- where- Literal :: (Eq a, Show a, Typeable a, Sat ctx a) =>- a -> Literal ctx (Full a)--instance WitnessCons (Literal ctx)- where- witnessCons (Literal _) = ConsWit--instance WitnessSat (Literal ctx)- where- type SatContext (Literal ctx) = ctx- witnessSat (Literal _) = SatWit--instance MaybeWitnessSat ctx (Literal ctx)+data Literal sig where- maybeWitnessSat = maybeWitnessSatDefault+ Literal :: (Eq a, Show a, Typeable a) => a -> Literal (Full a) -instance MaybeWitnessSat ctx1 (Literal ctx2)+instance Constrained Literal where- maybeWitnessSat _ _ = Nothing+ type Sat Literal = Eq :/\: Show :/\: Typeable :/\: Top+ exprDict (Literal _) = Dict -instance ExprEq (Literal ctx)+instance Equality Literal where- Literal a `exprEq` Literal b = case cast a of+ Literal a `equal` Literal b = case cast a of Just a' -> a'==b Nothing -> False exprHash (Literal a) = hash (show a) -instance Render (Literal ctx)+instance Render Literal where render (Literal a) = show a -instance ToTree (Literal ctx)+instance ToTree Literal -instance Eval (Literal ctx)+instance Eval Literal where- evaluate (Literal a) = fromEval a+ evaluate (Literal a) = a
Language/Syntactic/Constructs/Monad.hs view
@@ -1,4 +1,8 @@ -- | Monadic constructs+--+-- This module is based on the paper+-- /Generic Monadic Constructs for Embedded Languages/ (Persson et al., IFL 2011+-- <http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf>). module Language.Syntactic.Constructs.Monad where @@ -7,29 +11,22 @@ import Control.Monad import Language.Syntactic-import Language.Syntactic.Interpretation.Semantics import Data.Proxy -data MONAD m a+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 WitnessCons (MONAD m)- where- witnessCons Return = ConsWit- witnessCons Bind = ConsWit- witnessCons Then = ConsWit- witnessCons When = ConsWit--instance MaybeWitnessSat ctx (MONAD m)+instance Constrained (MONAD m) where- maybeWitnessSat _ _ = Nothing+ type Sat (MONAD m) = Top+ exprDict _ = Dict instance Monad m => Semantic (MONAD m) where@@ -38,12 +35,12 @@ semantics Then = Sem "then" (>>) semantics When = Sem "when" when -instance Monad m => ExprEq (MONAD m) where exprEq = exprEqSem; exprHash = exprHashSem-instance Monad m => Render (MONAD m) where renderPart = renderPartSem-instance Monad m => Eval (MONAD m) where evaluate = evaluateSem-instance Monad m => ToTree (MONAD m)+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 a -> Maybe (MONAD m a)+prjMonad :: (MONAD m :<: sup) => Proxy (m ()) -> sup sig -> Maybe (MONAD m sig) prjMonad _ = prj
Language/Syntactic/Constructs/Tuple.hs view
@@ -1,28 +1,15 @@-{-# OPTIONS_GHC -fcontext-stack=30 #-}--{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-} --- | Construction and projection of tuples in the object language------ The function pairs @desugarTupX@/@sugarTupX@ could be used directly in--- 'Syntactic' instances if it wasn't for the extra @(`Proxy` ctx)@ arguments.--- For this reason, 'Syntactic' instances have to be written manually for each--- context. The module "Language.Syntactic.Constructs.TupleSyntacticPoly"--- provides instances for a 'Poly' context. The exact same code can be used to--- make instances for other contexts -- just copy/paste and replace 'Poly' and--- 'poly' with the desired context (and probably add an extra constraint in the--- class contexts).+-- | Construction and elimination of tuples in the object language module Language.Syntactic.Constructs.Tuple where -import Data.Proxy import Data.Tuple.Curry import Data.Tuple.Select import Language.Syntactic-import Language.Syntactic.Interpretation.Semantics @@ -31,43 +18,21 @@ -------------------------------------------------------------------------------- -- | Expressions for constructing tuples-data Tuple ctx a- where- Tup2 :: Sat ctx (a,b) => Tuple ctx (a :-> b :-> Full (a,b))- Tup3 :: Sat ctx (a,b,c) => Tuple ctx (a :-> b :-> c :-> Full (a,b,c))- Tup4 :: Sat ctx (a,b,c,d) => Tuple ctx (a :-> b :-> c :-> d :-> Full (a,b,c,d))- Tup5 :: Sat ctx (a,b,c,d,e) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))- Tup6 :: Sat ctx (a,b,c,d,e,f) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))- Tup7 :: Sat ctx (a,b,c,d,e,f,g) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))--instance WitnessCons (Tuple ctx)- where- witnessCons Tup2 = ConsWit- witnessCons Tup3 = ConsWit- witnessCons Tup4 = ConsWit- witnessCons Tup5 = ConsWit- witnessCons Tup6 = ConsWit- witnessCons Tup7 = ConsWit--instance WitnessSat (Tuple ctx)- where- type SatContext (Tuple ctx) = ctx- witnessSat Tup2 = SatWit- witnessSat Tup3 = SatWit- witnessSat Tup4 = SatWit- witnessSat Tup5 = SatWit- witnessSat Tup6 = SatWit- witnessSat Tup7 = SatWit--instance MaybeWitnessSat ctx (Tuple ctx)+data Tuple sig where- maybeWitnessSat = maybeWitnessSatDefault+ 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 MaybeWitnessSat ctx1 (Tuple ctx2)+instance Constrained Tuple where- maybeWitnessSat _ _ = Nothing+ type Sat Tuple = Top+ exprDict _ = Dict -instance Semantic (Tuple ctx)+instance Semantic Tuple where semantics Tup2 = Sem "tup2" (,) semantics Tup3 = Sem "tup3" (,,)@@ -76,93 +41,10 @@ semantics Tup6 = Sem "tup6" (,,,,,) semantics Tup7 = Sem "tup7" (,,,,,,) -instance ExprEq (Tuple ctx) where exprEq = exprEqSem; exprHash = exprHashSem-instance Render (Tuple ctx) where renderPart = renderPartSem-instance Eval (Tuple ctx) where evaluate = evaluateSem-instance ToTree (Tuple ctx)----desugarTup2- :: ( Syntactic a dom- , Syntactic b dom- , Sat ctx (Internal a, Internal b)- , Tuple ctx :<: dom- )- => Proxy ctx- -> (a,b)- -> ASTF dom (Internal a, Internal b)-desugarTup2 ctx = uncurryN $ sugarSymCtx ctx Tup2--desugarTup3- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Sat ctx (Internal a, Internal b, Internal c)- , Tuple ctx :<: dom- )- => Proxy ctx- -> (a,b,c)- -> ASTF dom (Internal a, Internal b, Internal c)-desugarTup3 ctx = uncurryN $ sugarSymCtx ctx Tup3--desugarTup4- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Sat ctx (Internal a, Internal b, Internal c, Internal d)- , Tuple ctx :<: dom- )- => Proxy ctx- -> (a,b,c,d)- -> ASTF dom (Internal a, Internal b, Internal c, Internal d)-desugarTup4 ctx = uncurryN $ sugarSymCtx ctx Tup4--desugarTup5- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e)- , Tuple ctx :<: dom- )- => Proxy ctx- -> (a,b,c,d,e)- -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)-desugarTup5 ctx = uncurryN $ sugarSymCtx ctx Tup5--desugarTup6- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)- , Tuple ctx :<: dom- )- => Proxy ctx- -> (a,b,c,d,e,f)- -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)-desugarTup6 ctx = uncurryN $ sugarSymCtx ctx Tup6--desugarTup7- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Syntactic g dom- , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)- , Tuple ctx :<: dom- )- => Proxy ctx- -> (a,b,c,d,e,f,g)- -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)-desugarTup7 ctx = uncurryN $ sugarSymCtx ctx Tup7+instance Equality Tuple where equal = equalDefault; exprHash = exprHashDefault+instance Render Tuple where renderArgs = renderArgsDefault+instance Eval Tuple where evaluate = evaluateDefault+instance ToTree Tuple @@ -216,46 +98,22 @@ type instance Sel7' (a,b,c,d,e,f,g) = g -- | Expressions for selecting elements of a tuple-data Select ctx a- where- Sel1 :: (Sel1 a b, Sel1' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)- Sel2 :: (Sel2 a b, Sel2' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)- Sel3 :: (Sel3 a b, Sel3' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)- Sel4 :: (Sel4 a b, Sel4' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)- Sel5 :: (Sel5 a b, Sel5' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)- Sel6 :: (Sel6 a b, Sel6' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)- Sel7 :: (Sel7 a b, Sel7' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)--instance WitnessCons (Select ctx)- where- witnessCons Sel1 = ConsWit- witnessCons Sel2 = ConsWit- witnessCons Sel3 = ConsWit- witnessCons Sel4 = ConsWit- witnessCons Sel5 = ConsWit- witnessCons Sel6 = ConsWit- witnessCons Sel7 = ConsWit--instance WitnessSat (Select ctx)- where- type SatContext (Select ctx) = ctx- witnessSat Sel1 = SatWit- witnessSat Sel2 = SatWit- witnessSat Sel3 = SatWit- witnessSat Sel4 = SatWit- witnessSat Sel5 = SatWit- witnessSat Sel6 = SatWit- witnessSat Sel7 = SatWit--instance MaybeWitnessSat ctx (Select ctx)+data Select a where- maybeWitnessSat = maybeWitnessSatDefault+ 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 MaybeWitnessSat ctx1 (Select ctx2)+instance Constrained Select where- maybeWitnessSat _ _ = Nothing+ type Sat Select = Top+ exprDict _ = Dict -instance Semantic (Select ctx)+instance Semantic Select where semantics Sel1 = Sem "sel1" sel1 semantics Sel2 = Sem "sel2" sel2@@ -265,15 +123,15 @@ semantics Sel6 = Sem "sel6" sel6 semantics Sel7 = Sem "sel7" sel7 -instance ExprEq (Select ctx) where exprEq = exprEqSem; exprHash = exprHashSem-instance Render (Select ctx) where renderPart = renderPartSem-instance Eval (Select ctx) where evaluate = evaluateSem-instance ToTree (Select ctx)+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 ctx a -> Int+selectPos :: Select a -> Int selectPos Sel1 = 1 selectPos Sel2 = 2 selectPos Sel3 = 3@@ -284,138 +142,221 @@ -sugarTup2- :: ( Syntactic a dom- , Syntactic b dom- , Sat ctx (Internal a)- , Sat ctx (Internal b)- , Select ctx :<: dom- )- => Proxy ctx- -> ASTF dom (Internal a, Internal b)- -> (a,b)-sugarTup2 ctx a =- ( sugarSymCtx ctx Sel1 a- , sugarSymCtx ctx Sel2 a- )+-- TODO Move these instances to `Language.Syntactic.Frontend.Tuple` ? -sugarTup3- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Sat ctx (Internal a)- , Sat ctx (Internal b)- , Sat ctx (Internal c)- , Select ctx :<: dom- )- => Proxy ctx- -> ASTF dom (Internal a, Internal b, Internal c)- -> (a,b,c)-sugarTup3 ctx a =- ( sugarSymCtx ctx Sel1 a- , sugarSymCtx ctx Sel2 a- , sugarSymCtx ctx Sel3 a- )+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+ ) -sugarTup4- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Sat ctx (Internal a)- , Sat ctx (Internal b)- , Sat ctx (Internal c)- , Sat ctx (Internal d)- , Select ctx :<: dom- )- => Proxy ctx- -> ASTF dom (Internal a, Internal b, Internal c, Internal d)- -> (a,b,c,d)-sugarTup4 ctx a =- ( sugarSymCtx ctx Sel1 a- , sugarSymCtx ctx Sel2 a- , sugarSymCtx ctx Sel3 a- , sugarSymCtx ctx Sel4 a- )+ desugar = uncurryN $ sugarN $ appSymC Tup2 -sugarTup5- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Sat ctx (Internal a)- , Sat ctx (Internal b)- , Sat ctx (Internal c)- , Sat ctx (Internal d)- , Sat ctx (Internal e)- , Select ctx :<: dom- )- => Proxy ctx- -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)- -> (a,b,c,d,e)-sugarTup5 ctx a =- ( sugarSymCtx ctx Sel1 a- , sugarSymCtx ctx Sel2 a- , sugarSymCtx ctx Sel3 a- , sugarSymCtx ctx Sel4 a- , sugarSymCtx ctx Sel5 a- )+ sugar a =+ ( sugarSymC Sel1 a+ , sugarSymC Sel2 a+ ) -sugarTup6- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Sat ctx (Internal a)- , Sat ctx (Internal b)- , Sat ctx (Internal c)- , Sat ctx (Internal d)- , Sat ctx (Internal e)- , Sat ctx (Internal f)- , Select ctx :<: dom- )- => Proxy ctx- -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)- -> (a,b,c,d,e,f)-sugarTup6 ctx a =- ( sugarSymCtx ctx Sel1 a- , sugarSymCtx ctx Sel2 a- , sugarSymCtx ctx Sel3 a- , sugarSymCtx ctx Sel4 a- , sugarSymCtx ctx Sel5 a- , sugarSymCtx ctx Sel6 a- ) -sugarTup7- :: ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Syntactic g dom- , Sat ctx (Internal a)- , Sat ctx (Internal b)- , Sat ctx (Internal c)- , Sat ctx (Internal d)- , Sat ctx (Internal e)- , Sat ctx (Internal f)- , Sat ctx (Internal g)- , Select ctx :<: dom- )- => Proxy ctx- -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)- -> (a,b,c,d,e,f,g)-sugarTup7 ctx a =- ( sugarSymCtx ctx Sel1 a- , sugarSymCtx ctx Sel2 a- , sugarSymCtx ctx Sel3 a- , sugarSymCtx ctx Sel4 a- , sugarSymCtx ctx Sel5 a- , sugarSymCtx ctx Sel6 a- , sugarSymCtx ctx Sel7 a- )+instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , InjectC Tuple dom+ ( Internal a+ , Internal b+ , Internal c+ )+ , InjectC Select dom (Internal a)+ , InjectC Select dom (Internal b)+ , InjectC Select dom (Internal c)+ ) =>+ Syntactic (a,b,c) dom+ where+ type Internal (a,b,c) =+ ( Internal a+ , Internal b+ , Internal c+ )++ desugar = uncurryN $ sugarN $ appSymC Tup3+ sugar a =+ ( sugarSymC Sel1 a+ , sugarSymC Sel2 a+ , sugarSymC Sel3 a+ )++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , InjectC Tuple dom+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ )+ , InjectC Select dom (Internal a)+ , InjectC Select dom (Internal b)+ , InjectC Select dom (Internal c)+ , InjectC Select dom (Internal d)+ ) =>+ Syntactic (a,b,c,d) dom+ where+ type Internal (a,b,c,d) =+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ )++ desugar = uncurryN $ sugarN $ appSymC Tup4+ sugar a =+ ( sugarSymC Sel1 a+ , sugarSymC Sel2 a+ , sugarSymC Sel3 a+ , sugarSymC Sel4 a+ )+++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , InjectC Tuple dom+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ , Internal e+ )+ , InjectC Select dom (Internal a)+ , InjectC Select dom (Internal b)+ , InjectC Select dom (Internal c)+ , InjectC Select dom (Internal d)+ , InjectC Select dom (Internal e)+ ) =>+ Syntactic (a,b,c,d,e) dom+ where+ type Internal (a,b,c,d,e) =+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ , Internal e+ )++ desugar = uncurryN $ sugarN $ appSymC Tup5+ sugar a =+ ( sugarSymC Sel1 a+ , sugarSymC Sel2 a+ , sugarSymC Sel3 a+ , sugarSymC Sel4 a+ , sugarSymC Sel5 a+ )++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , InjectC Tuple dom+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ , Internal e+ , Internal f+ )+ , InjectC Select dom (Internal a)+ , InjectC Select dom (Internal b)+ , InjectC Select dom (Internal c)+ , InjectC Select dom (Internal d)+ , InjectC Select dom (Internal e)+ , InjectC Select dom (Internal f)+ ) =>+ Syntactic (a,b,c,d,e,f) dom+ where+ type Internal (a,b,c,d,e,f) =+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ , Internal e+ , Internal f+ )++ desugar = uncurryN $ sugarN $ appSymC Tup6+ sugar a =+ ( sugarSymC Sel1 a+ , sugarSymC Sel2 a+ , sugarSymC Sel3 a+ , sugarSymC Sel4 a+ , sugarSymC Sel5 a+ , sugarSymC Sel6 a+ )++instance+ ( Syntactic a dom+ , Syntactic b dom+ , Syntactic c dom+ , Syntactic d dom+ , Syntactic e dom+ , Syntactic f dom+ , Syntactic g dom+ , InjectC Tuple dom+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ , Internal e+ , Internal f+ , Internal g+ )+ , InjectC Select dom (Internal a)+ , InjectC Select dom (Internal b)+ , InjectC Select dom (Internal c)+ , InjectC Select dom (Internal d)+ , InjectC Select dom (Internal e)+ , InjectC Select dom (Internal f)+ , InjectC Select dom (Internal g)+ ) =>+ Syntactic (a,b,c,d,e,f,g) dom+ where+ type Internal (a,b,c,d,e,f,g) =+ ( Internal a+ , Internal b+ , Internal c+ , Internal d+ , Internal e+ , Internal f+ , Internal g+ )++ desugar = uncurryN $ sugarN $ appSymC Tup7+ sugar a =+ ( sugarSymC Sel1 a+ , sugarSymC Sel2 a+ , sugarSymC Sel3 a+ , sugarSymC Sel4 a+ , sugarSymC Sel5 a+ , sugarSymC Sel6 a+ , sugarSymC Sel7 a+ )
− Language/Syntactic/Constructs/TupleSyntacticPoly.hs
@@ -1,138 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | 'Syntactic' instances for tuples with 'Poly' context-module Language.Syntactic.Constructs.TupleSyntacticPoly where----import Language.Syntactic.Syntax-import Language.Syntactic.Constructs.Tuple----instance- ( Syntactic a dom- , Syntactic b dom- , Tuple Poly :<: dom- , Select Poly :<: dom- ) =>- Syntactic (a,b) dom- where- type Internal (a,b) =- ( Internal a- , Internal b- )-- desugar = desugarTup2 poly- sugar = sugarTup2 poly--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Tuple Poly :<: dom- , Select Poly :<: dom- ) =>- Syntactic (a,b,c) dom- where- type Internal (a,b,c) =- ( Internal a- , Internal b- , Internal c- )-- desugar = desugarTup3 poly- sugar = sugarTup3 poly--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Tuple Poly :<: dom- , Select Poly :<: dom- ) =>- Syntactic (a,b,c,d) dom- where- type Internal (a,b,c,d) =- ( Internal a- , Internal b- , Internal c- , Internal d- )-- desugar = desugarTup4 poly- sugar = sugarTup4 poly--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Tuple Poly :<: dom- , Select Poly :<: dom- ) =>- Syntactic (a,b,c,d,e) dom- where- type Internal (a,b,c,d,e) =- ( Internal a- , Internal b- , Internal c- , Internal d- , Internal e- )-- desugar = desugarTup5 poly- sugar = sugarTup5 poly--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Tuple Poly :<: dom- , Select Poly :<: dom- ) =>- Syntactic (a,b,c,d,e,f) dom- where- type Internal (a,b,c,d,e,f) =- ( Internal a- , Internal b- , Internal c- , Internal d- , Internal e- , Internal f- )-- desugar = desugarTup6 poly- sugar = sugarTup6 poly--instance- ( Syntactic a dom- , Syntactic b dom- , Syntactic c dom- , Syntactic d dom- , Syntactic e dom- , Syntactic f dom- , Syntactic g dom- , Tuple Poly :<: dom- , Select Poly :<: dom- ) =>- Syntactic (a,b,c,d,e,f,g) dom- where- type Internal (a,b,c,d,e,f,g) =- ( Internal a- , Internal b- , Internal c- , Internal d- , Internal e- , Internal f- , Internal g- )-- desugar = desugarTup7 poly- sugar = sugarTup7 poly-
− Language/Syntactic/Constructs/TupleSyntacticSimple.hs
@@ -1,138 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | 'Syntactic' instances for tuples with 'SimpleCtx' context-module Language.Syntactic.Constructs.TupleSyntacticSimple where----import Language.Syntactic.Syntax-import Language.Syntactic.Constructs.Tuple----instance- ( Syntactic a dom, Eq (Internal a), Show (Internal a)- , Syntactic b dom, Eq (Internal b), Show (Internal b)- , Tuple SimpleCtx :<: dom- , Select SimpleCtx :<: dom- ) =>- Syntactic (a,b) dom- where- type Internal (a,b) =- ( Internal a- , Internal b- )-- desugar = desugarTup2 simpleCtx- sugar = sugarTup2 simpleCtx--instance- ( Syntactic a dom, Eq (Internal a), Show (Internal a)- , Syntactic b dom, Eq (Internal b), Show (Internal b)- , Syntactic c dom, Eq (Internal c), Show (Internal c)- , Tuple SimpleCtx :<: dom- , Select SimpleCtx :<: dom- ) =>- Syntactic (a,b,c) dom- where- type Internal (a,b,c) =- ( Internal a- , Internal b- , Internal c- )-- desugar = desugarTup3 simpleCtx- sugar = sugarTup3 simpleCtx--instance- ( Syntactic a dom, Eq (Internal a), Show (Internal a)- , Syntactic b dom, Eq (Internal b), Show (Internal b)- , Syntactic c dom, Eq (Internal c), Show (Internal c)- , Syntactic d dom, Eq (Internal d), Show (Internal d)- , Tuple SimpleCtx :<: dom- , Select SimpleCtx :<: dom- ) =>- Syntactic (a,b,c,d) dom- where- type Internal (a,b,c,d) =- ( Internal a- , Internal b- , Internal c- , Internal d- )-- desugar = desugarTup4 simpleCtx- sugar = sugarTup4 simpleCtx--instance- ( Syntactic a dom, Eq (Internal a), Show (Internal a)- , Syntactic b dom, Eq (Internal b), Show (Internal b)- , Syntactic c dom, Eq (Internal c), Show (Internal c)- , Syntactic d dom, Eq (Internal d), Show (Internal d)- , Syntactic e dom, Eq (Internal e), Show (Internal e)- , Tuple SimpleCtx :<: dom- , Select SimpleCtx :<: dom- ) =>- Syntactic (a,b,c,d,e) dom- where- type Internal (a,b,c,d,e) =- ( Internal a- , Internal b- , Internal c- , Internal d- , Internal e- )-- desugar = desugarTup5 simpleCtx- sugar = sugarTup5 simpleCtx--instance- ( Syntactic a dom, Eq (Internal a), Show (Internal a)- , Syntactic b dom, Eq (Internal b), Show (Internal b)- , Syntactic c dom, Eq (Internal c), Show (Internal c)- , Syntactic d dom, Eq (Internal d), Show (Internal d)- , Syntactic e dom, Eq (Internal e), Show (Internal e)- , Syntactic f dom, Eq (Internal f), Show (Internal f)- , Tuple SimpleCtx :<: dom- , Select SimpleCtx :<: dom- ) =>- Syntactic (a,b,c,d,e,f) dom- where- type Internal (a,b,c,d,e,f) =- ( Internal a- , Internal b- , Internal c- , Internal d- , Internal e- , Internal f- )-- desugar = desugarTup6 simpleCtx- sugar = sugarTup6 simpleCtx--instance- ( Syntactic a dom, Eq (Internal a), Show (Internal a)- , Syntactic b dom, Eq (Internal b), Show (Internal b)- , Syntactic c dom, Eq (Internal c), Show (Internal c)- , Syntactic d dom, Eq (Internal d), Show (Internal d)- , Syntactic e dom, Eq (Internal e), Show (Internal e)- , Syntactic f dom, Eq (Internal f), Show (Internal f)- , Syntactic g dom, Eq (Internal g), Show (Internal g)- , Tuple SimpleCtx :<: dom- , Select SimpleCtx :<: dom- ) =>- Syntactic (a,b,c,d,e,f,g) dom- where- type Internal (a,b,c,d,e,f,g) =- ( Internal a- , Internal b- , Internal c- , Internal d- , Internal e- , Internal f- , Internal g- )-- desugar = desugarTup7 simpleCtx- sugar = sugarTup7 simpleCtx-
Language/Syntactic/Frontend/Monad.hs view
@@ -1,3 +1,11 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Monadic constructs+--+-- This module is based on the paper+-- /Generic Monadic Constructs for Embedded Languages/ (Persson et al., IFL 2011+-- <http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf>).+ module Language.Syntactic.Frontend.Monad where @@ -11,54 +19,60 @@ +-- 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 ctx dom m a+newtype Mon dom m a where Mon- :: { unMon :: forall r . (Monad m, Typeable r) =>- Cont (ASTF (HODomain ctx dom) (m r)) a+ :: { unMon :: forall r+ . (Monad m, Typeable r, InjectC (MONAD m) dom (m r))+ => Cont (ASTF (HODomain dom Typeable) (m r)) a }- -> Mon ctx dom m a+ -> Mon dom m a -deriving instance Functor (Mon ctx dom m)+deriving instance Functor (Mon dom m) -instance (Monad m) => Monad (Mon ctx 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- :: ( MONAD m :<: dom+ :: ( InjectC (MONAD m) dom (m a) , Monad m , Typeable1 m , Typeable a- , Sat ctx a )- => Mon ctx dom m (ASTF (HODomain ctx dom) a)- -> ASTF (HODomain ctx dom) (m a)-desugarMonad = flip runCont (sugarSym Return) . unMon+ => 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 :<: dom- , Monad m+ :: ( Monad m , Typeable1 m , Typeable a- , Sat ctx a )- => ASTF (HODomain ctx dom) (m a)- -> Mon ctx dom m (ASTF (HODomain ctx dom) a)-sugarMonad ma = Mon $ cont $ sugarSym Bind ma+ => ASTF (HODomain dom Typeable) (m a)+ -> Mon dom m (ASTF (HODomain dom Typeable) a)+sugarMonad ma = Mon $ cont $ sugarSymC Bind ma -instance ( MONAD m :<: dom- , Syntactic a (HODomain ctx dom)- , Monad m, Typeable1 m- , Sat ctx (Internal a)+instance ( Syntactic a (HODomain dom Typeable)+ , InjectC (MONAD m) dom (m (Internal a))+ , Monad m+ , Typeable1 m+ , Typeable (Internal a) ) =>- Syntactic (Mon ctx dom m a) (HODomain ctx dom)+ Syntactic (Mon dom m a) (HODomain dom Typeable) where- type Internal (Mon ctx dom m a) = m (Internal a)+ type Internal (Mon dom m a) = m (Internal a) desugar = desugarMonad . fmap desugar sugar = fmap sugar . sugarMonad
Language/Syntactic/Interpretation/Equality.hs view
@@ -8,45 +8,45 @@ --- | Equality for expressions. The difference between 'Eq' and 'ExprEq' is that--- 'ExprEq' allows comparison of expressions with different value types. It is--- assumed that when the types differ, the expressions also differ. The reason--- for allowing comparison of different types is that this is convenient when--- the types are existentially quantified.-class ExprEq expr+-- | Equality for expressions+class Equality expr where- exprEq :: expr a -> expr b -> Bool+ -- | 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 'exprEq' must result in the same hash:+ -- according to 'equal' must result in the same hash: --- -- @`exprEq` a b ==> `exprHash` a == `exprHash` b@+ -- @equal a b ==> exprHash a == exprHash b@ exprHash :: expr a -> Hash -instance ExprEq dom => ExprEq (AST dom)+instance Equality dom => Equality (AST dom) where- exprEq (Sym a) (Sym b) = exprEq a b- exprEq (f1 :$ a1) (f2 :$ a2) = exprEq f1 f2 && exprEq a1 a2- exprEq _ _ = False+ 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 (f :$ a) = hashInt 1 `combine` exprHash f `combine` exprHash a+ exprHash (s :$ a) = hashInt 1 `combine` exprHash s `combine` exprHash a -instance ExprEq dom => Eq (AST dom a)+instance Equality dom => Eq (AST dom a) where- (==) = exprEq+ (==) = equal -instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2)+instance (Equality expr1, Equality expr2) => Equality (expr1 :+: expr2) where- exprEq (InjL a) (InjL b) = exprEq a b- exprEq (InjR a) (InjR b) = exprEq a b- exprEq _ _ = False+ 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 (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a)+instance (Equality expr1, Equality expr2) => Eq ((expr1 :+: expr2) a) where- (==) = exprEq+ (==) = equal
Language/Syntactic/Interpretation/Evaluation.hs view
@@ -6,21 +6,23 @@ +-- | 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 -> a+ evaluate :: expr a -> Denotation a instance Eval dom => Eval (AST dom) where evaluate (Sym a) = evaluate a- evaluate (f :$ a) = evaluate f $: result (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--evalFull :: Eval dom => ASTF dom a -> a-evalFull = result . evaluate
Language/Syntactic/Interpretation/Render.hs view
@@ -15,23 +15,23 @@ -- | Render an expression as concrete syntax. A complete instance must define--- either of the methods 'render' and 'renderPart'.+-- either of the methods 'render' and 'renderArgs'. class Render expr where -- | Render an expression as a 'String' render :: expr a -> String- render = renderPart []+ render = renderArgs [] - -- | Render a partially applied constructor given a list of rendered missing+ -- | Render a partially applied expression given a list of rendered missing -- arguments- renderPart :: [String] -> expr a -> String- renderPart [] a = render a- renderPart args a = "(" ++ unwords (render a : args) ++ ")"+ renderArgs :: [String] -> expr a -> String+ renderArgs [] a = render a+ renderArgs args a = "(" ++ unwords (render a : args) ++ ")" instance Render dom => Render (AST dom) where- renderPart args (Sym a) = renderPart args a- renderPart args (f :$ a) = renderPart (render a : args) f+ renderArgs args (Sym a) = renderArgs args a+ renderArgs args (s :$ a) = renderArgs (render a : args) s instance Render dom => Show (AST dom a) where@@ -39,8 +39,8 @@ instance (Render expr1, Render expr2) => Render (expr1 :+: expr2) where- renderPart args (InjL a) = renderPart args a- renderPart args (InjR a) = renderPart args a+ renderArgs args (InjL a) = renderArgs args a+ renderArgs args (InjR a) = renderArgs args a instance (Render expr1, Render expr2) => Show ((expr1 :+: expr2) a) where@@ -54,24 +54,24 @@ class Render expr => ToTree expr where- -- | Convert a partially applied constructor to a syntax tree given a list- -- of rendered missing arguments- toTreePart :: [Tree String] -> expr a -> Tree String- toTreePart args a = Node (render a) args+ -- | 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- toTreePart args (Sym a) = toTreePart args a- toTreePart args (f :$ a) = toTreePart (toTree a : args) f+ 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- toTreePart args (InjL a) = toTreePart args a- toTreePart args (InjR a) = toTreePart args a+ 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 = toTreePart []+toTree = toTreeArgs [] -- | Show syntax tree using ASCII art showAST :: ToTree dom => AST dom a -> String
Language/Syntactic/Interpretation/Semantics.hs view
@@ -4,10 +4,7 @@ -import Data.Typeable- import Data.Hash-import Data.Proxy import Language.Syntactic.Syntax import Language.Syntactic.Interpretation.Equality@@ -19,26 +16,26 @@ -- | 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--- `exprEq` via the `Semantic` class.+-- `equal` via the `Semantic` class. data Semantics a where- Sem :: Signature a- => { semanticName :: String+ Sem+ :: { semanticName :: String , semanticEval :: Denotation a } -> Semantics a -instance ExprEq Semantics+instance Equality Semantics where- exprEq (Sem a _) (Sem b _) = a==b- exprHash (Sem name _) = hash name+ equal (Sem a _) (Sem b _) = a==b+ exprHash (Sem name _) = hash name instance Render Semantics where- renderPart [] (Sem name _) = name- renderPart args (Sem name _)+ renderArgs [] (Sem name _) = name+ renderArgs args (Sem name _) | isInfix = "(" ++ unwords [a,op,b] ++ ")" | otherwise = "(" ++ unwords (name : args) ++ ")" where@@ -52,7 +49,7 @@ instance Eval Semantics where- evaluate (Sem _ a) = fromEval a+ evaluate (Sem _ a) = a @@ -61,19 +58,19 @@ where semantics :: expr a -> Semantics a --- | Default implementation of 'exprEq'-exprEqSem :: Semantic expr => expr a -> expr b -> Bool-exprEqSem a b = exprEq (semantics a) (semantics b)+-- | Default implementation of 'equal'+equalDefault :: Semantic expr => expr a -> expr b -> Bool+equalDefault a b = equal (semantics a) (semantics b) -- | Default implementation of 'exprHash'-exprHashSem :: Semantic expr => expr a -> Hash-exprHashSem = exprHash . semantics+exprHashDefault :: Semantic expr => expr a -> Hash+exprHashDefault = exprHash . semantics --- | Default implementation of 'renderPart'-renderPartSem :: Semantic expr => [String] -> expr a -> String-renderPartSem args = renderPart args . semantics+-- | Default implementation of 'renderArgs'+renderArgsDefault :: Semantic expr => [String] -> expr a -> String+renderArgsDefault args = renderArgs args . semantics -- | Default implementation of 'evaluate'-evaluateSem :: Semantic expr => expr a -> a-evaluateSem = evaluate . semantics+evaluateDefault :: Semantic expr => expr a -> Denotation a+evaluateDefault = evaluate . semantics
Language/Syntactic/Sharing/Graph.hs view
@@ -14,7 +14,6 @@ import Data.Typeable import Data.Hash-import Data.Proxy import Language.Syntactic import Language.Syntactic.Constructs.Binding@@ -30,13 +29,6 @@ newtype NodeId = NodeId { nodeInteger :: Integer } deriving (Eq, Ord, Num, Real, Integral, Enum, Ix) ----- | Placeholder for a syntax tree-data Node ctx a- where- Node :: Sat ctx a => NodeId -> Node ctx (Full a)- instance Show NodeId where show (NodeId i) = show i@@ -46,25 +38,24 @@ -instance WitnessCons (Node ctx)+-- | Placeholder for a syntax tree+data Node a where- witnessCons (Node _) = ConsWit+ Node :: NodeId -> Node (Full a) -instance Render (Node ctx)+instance Constrained Node where- render (Node a) = showNode a--instance ToTree (Node ctx)--+ type Sat Node = Top+ exprDict _ = Dict --- | An 'ASTF' with hidden result type-data SomeAST dom+instance Render Node where- SomeAST :: Typeable a => ASTF dom a -> SomeAST dom+ render (Node a) = showNode a +instance ToTree Node + -- | Environment for alpha-equivalence class NodeEqEnv dom a where@@ -75,7 +66,7 @@ type NodeEnv dom = ( Array NodeId Hash- , Array NodeId (SomeAST dom)+ , Array NodeId (ASTB dom) ) instance NodeEqEnv dom (EqEnv dom)@@ -89,7 +80,7 @@ modVarEqEnv f = (f *** id) instance (AlphaEq dom dom dom env, NodeEqEnv dom env) =>- AlphaEq (Node ctx) (Node ctx) dom env+ AlphaEq Node Node dom env where alphaEqSym (Node n1) Nil (Node n2) Nil | n1 == n2 = return True@@ -98,7 +89,7 @@ if hTab!n1 /= hTab!n2 then return False else case (nTab!n1, nTab!n2) of- (SomeAST a, SomeAST b) -> alphaEqM a b+ (ASTB a, ASTB b) -> alphaEqM a b -- TODO The result could be memoized in a -- @Map (NodeId,NodeId) Bool@ @@ -115,16 +106,18 @@ -- -- A representation of a syntax tree with explicit sharing. An 'ASG' is valid if -- and only if 'inlineAll' succeeds (and the 'numNodes' field is correct).-data ASG ctx dom a = ASG- { topExpression :: ASTF (Node ctx :+: dom) a -- ^ Top-level expression- , graphNodes :: [(NodeId, SomeAST (Node ctx :+: dom))] -- ^ Mapping from node id to sub-expression- , numNodes :: NodeId -- ^ Total number of nodes+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 ctx dom a -> String+showASG :: ToTree dom => ASG dom a -> String showASG (ASG top nodes _) = unlines ((line "top" ++ showAST top) : map showNode nodes) where@@ -132,59 +125,52 @@ where rest = take (40 - length str) $ repeat '-' - showNode (n, SomeAST expr) = concat+ showNode (n, ASTB expr) = concat [ line ("node:" ++ show n) , showAST expr ] -- | Print syntax graph using ASCII art-drawASG :: ToTree dom => ASG ctx dom a -> IO ()+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 (Node ctx :+: dom) a -> AST (Node ctx :+: dom) a-reindexNodesAST reix (Sym (InjL (Node n))) = Sym (InjL (Node $ reix n))-reindexNodesAST reix (f :$ a) = reindexNodesAST reix f :$ reindexNodesAST reix a+ (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 ctx dom a -> ASG ctx dom a+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, SomeAST $ reindexNodesAST reix a)- | (n, SomeAST a) <- 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 ctx dom a -> ASG ctx dom a+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 ctx dom a -> ASG ctx dom a+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' -liftSome2- :: (forall a b . ASTF (Node ctx :+: dom) a -> ASTF (Node ctx :+: dom) b -> c)- -> SomeAST (Node ctx :+: dom)- -> SomeAST (Node ctx :+: dom)- -> c-liftSome2 f (SomeAST a) (SomeAST b) = f a b - -------------------------------------------------------------------------------- -- * Folding --------------------------------------------------------------------------------@@ -212,19 +198,17 @@ -- The result contains the result of folding the whole graph as well as the -- result of each internal node, represented both as an array and an association -- list. Each node is processed exactly once.-foldGraph :: forall ctx dom a b- . (SyntaxPF dom b -> b)- -> ASG ctx dom a- -> (b, (Array NodeId b, [(NodeId,b)]))-foldGraph alg graph@(ASG top ns nn) = (g top, (arr,nodes))+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, SomeAST expr) <- ns]+ nodes = [(n, g expr) | (n, ASTB expr) <- ns] arr = array (0, nn-1) nodes - g :: Signature c => AST (Node ctx :+: dom) c -> b- g (h :$ a) = alg $ AppPF (g h) (g a)- g (Sym (InjL (Node n)) ) = alg $ NodePF n (arr!n)- g (Sym (InjR a)) = alg $ DomPF a+ 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 @@ -233,25 +217,28 @@ -------------------------------------------------------------------------------- -- | Convert an 'ASG' to an 'AST' by inlining all nodes-inlineAll :: forall ctx dom a . Typeable a => ASG ctx dom a -> ASTF dom a+inlineAll :: 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 :: forall b. (Typeable b, Signature b) =>- AST (Node ctx :+: dom) b -> AST dom b- inline (f :$ a) = inline f :$ inline a- inline (Sym (InjL (Node n))) = case nodeMap ! n of- SomeAST a -> case gcast a of- Nothing -> error "inlineAll: type mismatch"- Just a -> inline a- inline (Sym (InjR a)) = Sym a+ 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 ctx dom a -> [(NodeId, [NodeId])]+nodeChildren :: ASG dom a -> [(NodeId, [NodeId])] nodeChildren = map (id *** fromDList) . snd . snd . foldGraph children where children :: SyntaxPF dom (DList NodeId) -> DList (NodeId)@@ -260,33 +247,36 @@ children _ = empty -- | Count the number of occurrences of each node in an expression-occurrences :: ASG ctx dom a -> Array NodeId Int+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 ctx dom a . Typeable a => ASG ctx dom a -> ASG ctx dom a+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, SomeAST (inline a)) | (n, SomeAST a) <- nodes, occs!n > 1]+ nodes' = [(n, ASTB (inline a)) | (n, ASTB a) <- nodes, occs!n > 1] n' = genericLength nodes' - inline :: forall b. (Typeable b, Signature b) =>- AST (Node ctx :+: dom) b -> AST (Node ctx :+: dom) b- inline (f :$ a) = inline f :$ inline a- inline (Sym (InjL (Node n)))- | occs!n > 1 = Sym (InjL (Node n))+ 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- SomeAST a -> case gcast a of- Nothing -> error "inlineSingle: type mismatch"- Just a -> inline a- inline (Sym (InjR a)) = Sym (InjR a)+ 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 @@ -296,8 +286,7 @@ -- | Compute a table (both array and list representation) of hash values for -- each node-hashNodes :: ExprEq dom =>- ASG ctx dom a -> (Array NodeId Hash, [(NodeId, Hash)])+hashNodes :: 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@@ -308,11 +297,11 @@ -- | Partitions the nodes such that two nodes are in the same sub-list if and -- only if they are alpha-equivalent.-partitionNodes :: forall ctx dom a- . ( ExprEq dom- , AlphaEq dom dom (Node ctx :+: dom) (EqEnv (Node ctx :+: dom))+partitionNodes :: forall dom a+ . ( Equality dom+ , AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom)) )- => ASG ctx dom a -> [[NodeId]]+ => ASG dom a -> [[NodeId]] partitionNodes graph = concatMap (fullPartition nodeEq) approxPartitioning where nTab = array (0, numNodes graph - 1) (graphNodes graph)@@ -329,17 +318,17 @@ nodeEq :: NodeId -> NodeId -> Bool nodeEq n1 n2 = runReader- (liftSome2 alphaEqM (nTab!n1) (nTab!n2))- (([],(hTab,nTab)) :: EqEnv (Node ctx :+: dom))+ (liftASTB2 alphaEqM (nTab!n1) (nTab!n2))+ (([],(hTab,nTab)) :: EqEnv (NodeDomain dom)) -- | Common sub-expression elimination based on alpha-equivalence cse- :: ( ExprEq dom- , AlphaEq dom dom (Node ctx :+: dom) (EqEnv (Node ctx :+: dom))+ :: ( Equality dom+ , AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom)) )- => ASG ctx dom a -> ASG ctx dom a+ => ASG dom a -> ASG dom a cse graph@(ASG top nodes n) = nubNodes $ reindexNodes (reixTab!) graph where parts = partitionNodes graph
Language/Syntactic/Sharing/Reify.hs view
@@ -1,7 +1,7 @@ -- | Reifying the sharing in an 'AST' ----- This module is based on /Type-Safe Observable Sharing in Haskell/ (Andy Gill,--- /Haskell Symposium/, 2009).+-- This module is based on the paper /Type-Safe Observable Sharing in Haskell/+-- (Andy Gill, 2009, <http://dx.doi.org/10.1145/1596638.1596653>). module Language.Syntactic.Sharing.Reify ( reifyGraph@@ -12,7 +12,6 @@ import Control.Monad.Writer import Data.IntMap as Map import Data.IORef-import Data.Typeable import System.Mem.StableName import Language.Syntactic@@ -24,40 +23,41 @@ -- | Shorthand used by 'reifyGraphM' -- -- Writes out a list of encountered nodes and returns the top expression.-type GraphMonad ctx dom a = WriterT- [(NodeId, SomeAST (Node ctx :+: dom))]+type GraphMonad dom a = WriterT+ [(NodeId, ASTB (NodeDomain dom))] IO- (AST (Node ctx :+: dom) a)+ (AST (NodeDomain dom) a) -reifyGraphM :: forall ctx dom a . Typeable a- => (forall a . ASTF dom a -> Maybe (SatWit ctx a))+reifyGraphM :: forall dom a . Constrained dom+ => (forall a . ASTF dom a -> Bool) -> IORef NodeId -> IORef (History (AST dom)) -> ASTF dom a- -> GraphMonad ctx dom (Full a)+ -> GraphMonad dom (Full a) reifyGraphM canShare nSupp history = reifyNode where- reifyNode :: Typeable b => ASTF dom b -> GraphMonad ctx dom (Full b)- reifyNode a = case canShare a of- Nothing -> reifyRec a- Just SatWit | a `seq` True -> do- st <- liftIO $ makeStableName a- hist <- liftIO $ readIORef history- case lookHistory hist (StName st) of- Just n -> return $ Sym $ InjL $ Node n- _ -> do- n <- fresh nSupp- liftIO $ modifyIORef history $ remember (StName st) n- a' <- reifyRec a- tell [(n, SomeAST a')]- return $ Sym $ InjL $ Node n+ 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 :: AST dom b -> GraphMonad ctx dom b+ reifyRec :: Sat dom (DenResult b) => AST dom b -> GraphMonad dom b reifyRec (f :$ a) = liftM2 (:$) (reifyRec f) (reifyNode a)- reifyRec (Sym a) = return $ Sym (InjR a)+ reifyRec (Sym s) = return $ Sym $ C' $ InjR s @@ -66,14 +66,11 @@ -- This function is not referentially transparent (hence the 'IO'). However, it -- is well-behaved in the sense that the worst thing that could happen is that -- sharing is lost. It is not possible to get false sharing.-reifyGraph :: Typeable a- => (forall a . ASTF dom a -> Maybe (SatWit ctx a))- -- ^ A function that decides whether a given node can be shared.- -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose- -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the- -- function returns a 'SatWit'.+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 ctx dom a)+ -> IO (ASG dom a) reifyGraph canShare a = do nSupp <- newIORef 0 history <- newIORef empty
Language/Syntactic/Sharing/ReifyHO.hs view
@@ -1,5 +1,5 @@ -- | This module is similar to "Language.Syntactic.Sharing.Reify", but operates--- on @`AST` (`HODomain` ctx dom)@ rather than a general 'AST'. The reason for+-- 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@@ -8,8 +8,8 @@ -- 'HOLambda'. On the other hand, if we did 'HOLambda' reification first (using -- 'reify'), we would destroy the sharing. ----- This module is based on /Type-Safe Observable Sharing in Haskell/ (Andy Gill,--- /Haskell Symposium/, 2009).+-- This module is based on the paper /Type-Safe Observable Sharing in Haskell/+-- (Andy Gill, 2009, <http://dx.doi.org/10.1145/1596638.1596653>). module Language.Syntactic.Sharing.ReifyHO ( reifyGraphTop@@ -21,11 +21,8 @@ import Control.Monad.Writer import Data.IntMap as Map import Data.IORef-import Data.Typeable import System.Mem.StableName -import Data.Proxy- import Language.Syntactic import Language.Syntactic.Constructs.Binding import Language.Syntactic.Constructs.Binding.HigherOrder@@ -38,56 +35,54 @@ -- | Shorthand used by 'reifyGraphM' -- -- Writes out a list of encountered nodes and returns the top expression.-type GraphMonad ctx dom a = WriterT- [(NodeId, SomeAST (Node ctx :+: Lambda ctx :+: Variable ctx :+: dom))]+type GraphMonad dom p a = WriterT+ [(NodeId, ASTB (NodeDomain ((Lambda :+: Variable :+: dom) :|| p)))] IO- (AST (Node ctx :+: Lambda ctx :+: Variable ctx :+: dom) a)+ (AST (NodeDomain ((Lambda :+: Variable :+: dom) :|| p)) a) -reifyGraphM :: forall ctx dom a . Typeable a- => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a))+reifyGraphM :: forall dom p a+ . (forall a . ASTF (HODomain dom p) a -> Bool) -> IORef VarId -> IORef NodeId- -> IORef (History (AST (HODomain ctx dom)))- -> ASTF (HODomain ctx dom) a- -> GraphMonad ctx dom (Full a)+ -> IORef (History (AST (HODomain dom p)))+ -> ASTF (HODomain dom p) a+ -> GraphMonad dom p (Full a) reifyGraphM canShare vSupp nSupp history = reifyNode where- reifyNode :: Typeable b =>- ASTF (HODomain ctx dom) b -> GraphMonad ctx dom (Full b)- reifyNode a = case canShare a of- Nothing -> reifyRec a- Just SatWit | a `seq` True -> do- st <- liftIO $ makeStableName a- hist <- liftIO $ readIORef history- case lookHistory hist (StName st) of- Just n -> return $ Sym $ InjL $ Node n- _ -> do- n <- fresh nSupp- liftIO $ modifyIORef history $ remember (StName st) n- a' <- reifyRec a- tell [(n, SomeAST a')]- return $ Sym $ InjL $ Node n+ 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 ctx dom) b -> GraphMonad ctx dom b- reifyRec (f :$ a) = liftM2 (:$) (reifyRec f) (reifyNode a)- reifyRec (Sym (InjR a)) = return $ Sym (InjR (InjR a))- reifyRec (Sym (InjL (HOLambda f))) = do+ 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 $ inj $ (Variable v `withContext` ctx)- return $ inj (Lambda v `withContext` ctx) :$ body- where- ctx = Proxy :: Proxy ctx+ body <- reifyNode $ f $ injC $ Variable v+ return $ injC (Lambda v) :$ body -- | Convert a syntax tree to a sharing-preserving graph-reifyGraphTop :: Typeable a- => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a))- -> ASTF (HODomain ctx dom) a- -> IO (ASG ctx (Lambda ctx :+: Variable ctx :+: dom) a, VarId)+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@@ -102,16 +97,10 @@ -- 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 ctx dom)- => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a))- -- ^ A function that decides whether a given node can be shared.- -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose- -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the- -- function returns a 'SatWit'.+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 ctx (Lambda ctx :+: Variable ctx :+: dom) (Internal a)- , VarId- )+ -> IO (ASG ((Lambda :+: Variable :+: dom) :|| p) (Internal a), VarId) reifyGraph canShare = reifyGraphTop canShare . desugar
Language/Syntactic/Sharing/SimpleCodeMotion.hs view
@@ -9,6 +9,7 @@ , codeMotion , defaultBindDict , reifySmart+ , reifySmartDefault ) where @@ -17,8 +18,6 @@ import Data.Set as Set import Data.Typeable -import Data.Proxy- import Language.Syntactic import Language.Syntactic.Constructs.Binding import Language.Syntactic.Constructs.Binding.HigherOrder@@ -26,36 +25,35 @@ -- | Interface for binding constructs-data BindDict ctx dom = BindDict+data BindDict dom = BindDict { prjVariable :: forall a . dom a -> Maybe VarId , prjLambda :: forall a . dom a -> Maybe VarId- , injVariable :: forall a . (Sat ctx a, Typeable a) => ASTF dom a -> VarId -> dom (Full a)- , injLambda :: forall a b . (Sat ctx a, Typeable a, Sat ctx b) => ASTF dom b -> VarId -> dom (b :-> Full (a -> b))- , injLet :: forall a b . (Sat ctx a, Sat ctx b) => ASTF dom b -> dom (a :-> (a -> b) :-> Full b)+ , 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) }- -- TODO `injLambda` has more constraints than the `Lambda` constructor. This- -- is demanded by the Feldspar implementation. One way to make things- -- more consistent would be to add an extra `ctx` parameter to `Lambda`- -- (like `Let`). -- | Substituting a sub-expression. Assumes no variable capturing in the -- expressions involved. substitute :: forall dom a b- . (Typeable a, Typeable b, AlphaEq dom dom dom [(VarId,VarId)])+ . (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- | Just y' <- gcast y, alphaEq x a = y'+ | 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 :: Typeable c => AST dom c -> AST dom c+ 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)]+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@@ -71,16 +69,12 @@ nonTerminal (_ :$ _) = True nonTerminal _ = False -data SomeAST ctx dom- where- SomeAST :: (Sat ctx a, Typeable a) => ASTF dom a -> SomeAST ctx dom- -- | Environment for the expression in the 'choose' function-data Env ctx dom = Env+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 :: SomeAST ctx dom -> Int+ , counter :: ASTE dom -> Int -- ^ Counting the number of occurrences of an expression in the -- environment , dependencies :: Set VarId@@ -88,7 +82,7 @@ -- expression } -independent :: BindDict ctx dom -> Env ctx dom -> AST dom a -> Bool+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) =@@ -96,47 +90,39 @@ independent _ _ _ = True -- | Checks whether a sub-expression in a given environment can be lifted out-liftable :: (Sat ctx a, Typeable a) =>- BindDict ctx dom -> Env ctx dom -> ASTF dom a -> Bool+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- = queryNodeSimple (const . canShare env) a+ = simpleMatch (const . canShare env) a && nonTerminal a- && (inLambda env || (counter env (SomeAST a) > 1))+ && (inLambda env || (counter env (ASTE a) > 1)) -- | Choose a sub-expression to share choose- :: ( AlphaEq dom dom dom [(VarId,VarId)]- , MaybeWitnessSat ctx dom- , Typeable a- )- => BindDict ctx dom+ :: AlphaEq dom dom dom [(VarId,VarId)]+ => BindDict dom -> (forall a . dom a -> Bool) -> ASTF dom a- -> Maybe (SomeAST ctx dom)+ -> Maybe (ASTE dom) choose bindDict canShr a = chooseEnv bindDict env a where env = Env { inLambda = False , canShare = canShr- , counter = \(SomeAST b) -> count b a+ , counter = \(ASTE b) -> count b a , dependencies = empty } -- | Choose a sub-expression to share in an 'Env' environment-chooseEnv :: forall ctx dom a . (MaybeWitnessSat ctx dom, Typeable a) =>- BindDict ctx dom -> Env ctx dom -> ASTF dom a -> Maybe (SomeAST ctx dom)+chooseEnv :: BindDict dom -> Env dom -> ASTF dom a -> Maybe (ASTE dom) chooseEnv bindDict env a- | Just SatWit <- maybeWitnessSat (Proxy :: Proxy ctx) a- , liftable bindDict env a- = Just (SomeAST a)- | otherwise = chooseEnvSub 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 :: MaybeWitnessSat ctx dom =>- BindDict ctx dom -> Env ctx dom -> AST dom a -> Maybe (SomeAST ctx dom)+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@@ -151,25 +137,19 @@ -- | Perform common sub-expression elimination and variable hoisting-codeMotion :: forall ctx dom a- . ( AlphaEq dom dom dom [(VarId,VarId)]- , MaybeWitnessSat ctx dom- , Typeable a+codeMotion :: forall dom a+ . ( ConstrainedBy dom Typeable+ , AlphaEq dom dom dom [(VarId,VarId)] )- => BindDict ctx dom+ => BindDict dom -> (forall a . dom a -> Bool) -> ASTF dom a -> State VarId (ASTF dom a) codeMotion bindDict canShr a- | Just SatWit <- maybeWitnessSat ctx a- , Just b <- choose bindDict canShr a- = share b- | otherwise = descend a+ | Just b <- choose bindDict canShr a = share b+ | otherwise = descend a where- ctx = Proxy :: Proxy ctx-- share :: Sat ctx a => SomeAST ctx dom -> State VarId (ASTF dom a)- share (SomeAST b) = do+ share (ASTE b) = do b' <- codeMotion bindDict canShr b v <- get; put (v+1) let x = Sym (injVariable bindDict b v)@@ -177,51 +157,58 @@ return $ Sym (injLet bindDict body) :$ b'- :$ (Sym (injLambda bindDict body v) :$ body)+ :$ (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+ descend a = return a -defaultBindDict :: forall ctx dom- . ( Variable ctx :<: dom- , Lambda ctx :<: dom- , Let ctx ctx :<: dom- )- => BindDict ctx dom+defaultBindDict+ :: (Variable :<: dom, Lambda :<: dom, Let :<: dom, Constrained dom)+ => BindDict (dom :|| Typeable) defaultBindDict = BindDict { prjVariable = \a -> do- Variable v <- prjCtx ctx a+ Variable v <- prj a return v , prjLambda = \a -> do- Lambda v <- prjCtx ctx a+ Lambda v <- prj a return v - , injVariable = \_ v -> inj (Variable v `withContext` ctx)- , injLambda = \_ v -> inj (Lambda v `withContext` ctx)- , injLet = \_ -> inj (letBind ctx)+ , 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 }- where- ctx = Proxy :: Proxy ctx +-- TODO Abstract away from Typeable?+ -- | Like 'reify' but with common sub-expression elimination and variable -- hoisting-reifySmart :: forall ctx dom a- . ( Let ctx ctx :<: dom- , AlphaEq dom dom (Lambda ctx :+: Variable ctx :+: dom) [(VarId,VarId)]- , MaybeWitnessSat ctx dom- , Syntactic a (HODomain ctx dom)+reifySmart+ :: ( AlphaEq dom dom ((Lambda :+: Variable :+: dom) :|| Typeable) [(VarId,VarId)]+ , Syntactic a (HODomain dom Typeable) )- => (forall a . (Lambda ctx :+: Variable ctx :+: dom) a -> Bool)+ => BindDict ((Lambda :+: Variable :+: dom) :|| Typeable)+ -> (forall a . ((Lambda :+: Variable :+: dom) :|| Typeable) a -> Bool) -> a- -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a)-reifySmart canShr = flip evalState 0 .+ -> ASTF ((Lambda :+: Variable :+: dom) :|| Typeable) (Internal a)+reifySmart dict canShr = flip evalState 0 . (codeMotion dict canShr <=< reifyM . desugar)- where- dict = defaultBindDict :: BindDict ctx (Lambda ctx :+: Variable ctx :+: dom)++reifySmartDefault+ :: ( Let :<: dom+ , AlphaEq dom dom ((Lambda :+: Variable :+: dom) :|| Typeable) [(VarId,VarId)]+ , Syntactic a (HODomain dom Typeable)+ )+ => (forall a . ((Lambda :+: Variable :+: dom) :|| Typeable) a -> Bool)+ -> a+ -> ASTF ((Lambda :+: Variable :+: dom) :|| Typeable) (Internal a)+reifySmartDefault = reifySmart defaultBindDict
Language/Syntactic/Sharing/StableName.hs view
@@ -5,7 +5,6 @@ import Control.Monad.IO.Class import Data.IntMap as Map import Data.IORef-import Data.Typeable import System.Mem.StableName import Unsafe.Coerce @@ -14,41 +13,34 @@ --- | 'StableName' of a (@c (`Full` a)@) with hidden result type+-- | 'StableName' of a @(c (Full a))@ with hidden result type data StName c where- StName :: Typeable a => StableName (c (Full a)) -> StName c--stCast :: forall a b c . (Typeable a, Typeable b) =>- StableName (c (Full a)) -> Maybe (StableName (c (Full b)))-stCast a- | ta==tb = Just (unsafeCoerce a)- | otherwise = Nothing- where- ta = typeOf (undefined :: a)- tb = typeOf (undefined :: b)+ StName :: StableName (c (Full a)) -> StName c instance Eq (StName c) where- StName st1 == StName st2 = case stCast st1 of- Just st1' -> st1'==st2- _ -> False+ StName a == StName b = a == unsafeCoerce b+ -- This is "probably" safe according to+ -- <http://www.haskell.org/pipermail/glasgow-haskell-users/2012-August/022758.html> + -- TODO In future, use `eqStableName`. It should be in GHC 7.8.1.+ hash :: StName c -> Int hash (StName st) = hashStableName st ----- 'History' implements a hash table from 'StName' to 'NodeId' (with 'hash' as--- the hashing function). I.e. it is assumed that the 'StName's at each entry--- all have the same 'hash', and that this number is equal to the entry's key.+-- | 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
+ Language/Syntactic/Sugar.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- | \"Syntactic sugar\"++module Language.Syntactic.Sugar where++++import Language.Syntactic.Syntax+import Language.Syntactic.Constraint++++-- | It is usually assumed that @(`desugar` (`sugar` a))@ has the same meaning+-- as @a@.+class Syntactic a dom | a -> dom+ -- Note: using a functional dependency rather than an associated type,+ -- because this makes it possible to make a class alias constraining dom.+ -- TODO Now that GHC allows equality super class constraints, this should be+ -- changed to an associated type.+ where+ type Internal a+ desugar :: a -> ASTF dom (Internal a)+ sugar :: ASTF dom (Internal a) -> a++instance Syntactic (ASTF dom a) dom+ where+ type Internal (ASTF dom a) = a+ desugar = id+ sugar = id++-- | Syntactic type casting+resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b+resugar = sugar . desugar++-- | N-ary syntactic functions+--+-- 'desugarN' has any type of the form:+--+-- > desugarN ::+-- > ( Syntactic a dom+-- > , Syntactic b dom+-- > , ...+-- > , Syntactic x dom+-- > ) => (a -> b -> ... -> x)+-- > -> ( ASTF dom (Internal a)+-- > -> ASTF dom (Internal b)+-- > -> ...+-- > -> ASTF dom (Internal x)+-- > )+--+-- ...and vice versa for 'sugarN'.+class SyntacticN a internal | a -> internal+ where+ desugarN :: a -> internal+ sugarN :: internal -> a++instance (Syntactic a dom, ia ~ AST dom (Full (Internal a))) => SyntacticN a ia+ where+ desugarN = desugar+ sugarN = sugar++instance+ ( Syntactic a dom+ , ia ~ Internal a+ , SyntacticN b ib+ ) =>+ SyntacticN (a -> b) (AST dom (Full ia) -> ib)+ where+ desugarN f = desugarN . f . sugar+ sugarN f = sugarN . f . desugar++++-- | \"Sugared\" symbol application+--+-- 'sugarSym' has any type of the form:+--+-- > sugarSym ::+-- > ( expr :<: AST dom+-- > , Syntactic a dom+-- > , Syntactic b dom+-- > , ...+-- > , Syntactic x dom+-- > ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))+-- > -> (a -> b -> ... -> x)+sugarSym :: (sym :<: AST dom, ApplySym sig b dom, SyntacticN c b) =>+ sym sig -> c+sugarSym = sugarN . appSym++-- | \"Sugared\" symbol application+--+-- 'sugarSymC' has any type of the form:+--+-- > sugarSymC ::+-- > ( InjectC expr (AST dom) (Internal x)+-- > , Syntactic a dom+-- > , Syntactic b dom+-- > , ...+-- > , Syntactic x dom+-- > ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))+-- > -> (a -> b -> ... -> x)+sugarSymC+ :: ( InjectC sym (AST dom) (DenResult sig)+ , ApplySym sig b dom+ , SyntacticN c b+ )+ => sym sig -> c+sugarSymC = sugarN . appSymC+
Language/Syntactic/Syntax.hs view
@@ -3,678 +3,155 @@ -- | Generic representation of typed syntax trees ----- As a simple demonstration, take the following simple language:------ > data Expr1 a--- > where--- > Num1 :: Int -> Expr1 Int--- > Add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int------ Using the present library, this can be rewritten as follows:------ > data Num2 a where Num2 :: Int -> Num2 (Full Int)--- > data Add2 a where Add2 :: Add2 (Int :-> Int :-> Full Int)--- >--- > type Expr2 a = ASTF (Num2 :+: Add2) a------ Note that @Num2@ and @Add2@ are /non-recursive/. The only recursive data type--- here is 'AST', which is provided by the library. Now, the important point is--- that @Expr1@ and @Expr2@ are completely isomorphic! This is indicated by the--- following conversions:------ > conv12 :: Expr1 a -> Expr2 a--- > conv12 (Num1 n) = inj (Num2 n)--- > conv12 (Add1 a b) = inj Add2 :$ conv12 a :$ conv12 b--- >--- > conv21 :: Expr2 a -> Expr1 a--- > conv21 (prj -> Just (Num2 n)) = Num1 n--- > conv21 ((prj -> Just Add2) :$ a :$ b) = Add1 (conv21 a) (conv21 b)------ A key property here is that the patterns in @conv21@ are actually complete.------ So, why should one use @Expr2@ instead of @Expr1@? The answer is that @Expr2@--- can be processed by generic algorithms defined over 'AST', for example:------ > countNodes :: ASTF domain a -> Int--- > countNodes = count--- > where--- > count :: AST domain a -> Int--- > count (Sym _) = 1--- > count (a :$ b) = count a + count b------ Furthermore, although @Expr2@ was defined to use exactly the constructors--- 'Num2' and 'Add2', it is possible to leave the set of constructors open,--- leading to more modular and reusable code. This can be seen by relaxing the--- types of @conv12@ and @conv21@:------ > conv12 :: (Num2 :<: dom, Add2 :<: dom) => Expr1 a -> ASTF dom a--- > conv21 :: (Num2 :<: dom, Add2 :<: dom) => ASTF dom a -> Expr1 a------ This way of encoding open data types is taken from /Data types à la carte/--- (Wouter Swierstra, /Journal of Functional Programming/, 2008). However, we do--- not need Swierstra's fixed-point machinery for recursive data types. Instead--- we rely on 'AST' being recursive.+-- For details, see: A Generic Abstract Syntax Model for Embedded Languages+-- (ICFP 2012, <http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf>). module Language.Syntactic.Syntax ( -- * Syntax trees- Full (..)+ AST (..)+ , ASTF+ , Full (..) , (:->) (..)- , Args (..)- , WrapFull (..)- , Signature- , Denotation+ , size+ , ApplySym (..) , DenResult- , ConsWit (..)- , WitnessCons (..)- , fromEval- , toEval- , listArgs- , mapArgs- , mapArgsM- , appArgs- , appEvalArgs- , ($:)- , AST (..)- , ASTF+ -- * Symbol domains , (:+:) (..)- , ApplySym- , appSym- , appSymCtx- -- * Subsumption+ , Project (..) , (:<:) (..)- , injCtx- , prjCtx- -- * Syntactic sugar- , Syntactic (..)- , resugar- , SyntacticN (..)- , sugarSym- , sugarSymCtx- -- * AST processing- , queryNode- , queryNodeSimple- , transformNode- -- * Restricted syntax trees- , Sat (..)- , Witness (PolyWit, SimpleWit)- -- TODO A warning reports that these are already exported by 'Sat (..)',- -- but that is actually not the case. This seems to have been fixed- -- recently:- --- -- http://hackage.haskell.org/trac/ghc/ticket/2436#comment:12- --- -- I don't know if the fix just removes the warning, or if it means- -- that 'Sat (..)' is enough.- , witnessByProxy- , SatWit (..)- , fromSatWit- , WitnessSat (..)- , MaybeWitnessSat (..)- , maybeWitnessSatDefault- , withContext- , Poly- , poly- , SimpleCtx- , simpleCtx+ , appSym ) where -import Control.Monad.Identity import Data.Typeable -import Data.Proxy - -------------------------------------------------------------------------------- -- * Syntax trees -------------------------------------------------------------------------------- --- | The type of a fully applied constructor-newtype Full a = Full { result :: a }- deriving (Eq, Show, Typeable)---- | The type of a partially applied (or unapplied) constructor-newtype a :-> b = Partial (a -> b)- deriving (Typeable)---- | Heterogeneous list, indexed by a container type and a 'Signature'-data family Args (c :: * -> *) a--data instance Args c (Full a) = Nil-data instance Args c (a :-> b) = Typeable a => c (Full a) :* Args c b- -- The 'Typeable' constraint is needed in order to be able to rebuild an 'AST'- -- from an 'Args' (since '(:$)' has a `Typeable` constraint).--infixr :->, :*---- | Can be used to turn a type constructor indexed by @a@ to a type constructor--- indexed by @(`Full` a)@. This is useful together with 'Args', which assumes--- its constructor to be indexed by @(`Full` a)@. 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)---- | Fully or partially applied constructor------ This class is private to the module to guarantee that all members of the--- class have the form:------ > Full a--- > a1 :-> Full a2--- > a1 :-> a2 :-> ... :-> Full an------ The closed class also has the property:--- @Signature' (a :-> b)@ iff. @Signature' b@.-class Signature' a- where- type Denotation' a- type DenResult' a-- fromEval' :: Denotation' a -> a- toEval' :: a -> Denotation' a- listArgs' :: (forall a . c (Full a) -> b) -> Args c a -> [b]- mapArgs' :: (forall a . c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 a- mapArgsM' :: Monad m => (forall a . c1 (Full a) -> m (c2 (Full a))) -> Args c1 a -> m (Args c2 a)- appArgs' :: AST dom a -> Args (AST dom) a -> ASTF dom (DenResult a)- appEvalArgs' :: Denotation a -> Args Identity a -> DenResult a--instance Signature' (Full a)- where- type Denotation' (Full a) = a- type DenResult' (Full a) = a-- fromEval' = Full- toEval' = result- listArgs' f Nil = []- mapArgs' f Nil = Nil- mapArgsM' f Nil = return Nil- appArgs' a Nil = a- appEvalArgs' a Nil = a--instance Signature' b => Signature' (a :-> b)- where- type Denotation' (a :-> b) = a -> Denotation' b- type DenResult' (a :-> b) = DenResult' b-- fromEval' = Partial . (fromEval' .)- toEval' (Partial f) = toEval' . f- listArgs' f (a :* as) = f a : listArgs' f as- mapArgs' f (a :* as) = f a :* mapArgs' f as- mapArgsM' f (a :* as) = liftM2 (:*) (f a) (mapArgsM' f as)- appArgs' c (a :* as) = appArgs' (c :$ a) as- appEvalArgs' f (a :* as) = appEvalArgs' (f $ result $ runIdentity a) as---- | Fully or partially applied constructor------ This is a public alias for the hidden class 'Signature''. The only instances--- are:------ > instance Signature' (Full a)--- > instance Signature' b => Signature' (a :-> b)-class Signature' a => Signature a-instance Signature' a => Signature a---- | Maps a 'Signature' to a simpler form where ':->' has been replaced by @->@,--- and 'Full' has been removed. This is a public alias for the hidden type--- 'Denotation''.-type Denotation a = Denotation' a---- | Returns the result type ('Full' removed) of a 'Signature'. This is a public--- alias for the hidden type 'DenResult''.-type DenResult a = DenResult' a---- | A witness of @(`Signature` a)@-data ConsWit a- where- ConsWit :: Signature a => ConsWit a---- | Expressions in syntactic are supposed to have the form--- @(`Signature` a => expr a)@. This class lets us witness the 'Signature'--- constraint of an expression without examining the expression.-class WitnessCons expr- where- witnessCons :: expr a -> ConsWit a--instance (WitnessCons sub1, WitnessCons sub2) => WitnessCons (sub1 :+: sub2)- where- witnessCons (InjL a) = witnessCons a- witnessCons (InjR a) = witnessCons a---- | Make a constructor evaluation from a 'Denotation' representation-fromEval :: Signature a => Denotation a -> a-fromEval = fromEval'--toEval :: Signature a => a -> Denotation a-toEval = toEval'---- | Convert a heterogeneous list to a normal list-listArgs :: Signature a => (forall a . c (Full a) -> b) -> Args c a -> [b]-listArgs = listArgs'---- | Change the container of each element in a heterogeneous list-mapArgs :: Signature a =>- (forall a . c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 a-mapArgs = mapArgs'---- | Change the container of each element in a heterogeneous list, monadic--- version-mapArgsM :: (Monad m, Signature a) =>- (forall a . c1 (Full a) -> m (c2 (Full a))) -> Args c1 a -> m (Args c2 a)-mapArgsM = mapArgsM'---- | Apply the syntax tree to the listed arguments-appArgs :: Signature a =>- AST dom a -> Args (AST dom) a -> ASTF dom (DenResult a)-appArgs = appArgs'---- | Apply the evaluation function to the listed arguments-appEvalArgs :: Signature a => Denotation a -> Args Identity a -> DenResult a-appEvalArgs = appEvalArgs'---- | Semantic constructor application-($:) :: (a :-> b) -> a -> b-Partial f $: a = f a--- -- | Generic abstract syntax tree, parameterized by a symbol domain ----- In general, @(`AST` dom (a `:->` b))@ represents a partially applied (or--- unapplied) constructor, missing at least one argument, while--- @(`AST` dom (`Full` a))@ represents a fully applied constructor, i.e. a--- complete syntax tree.--- It is not possible to construct a total value of type @(`AST` dom a)@ that--- does not fulfill the constraint @(`Signature` a)@.------ Note that the hidden class 'Signature'' mentioned in the type of 'Sym' is--- interchangeable with 'Signature'.-data AST dom a+-- @(`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 :: Signature' a => dom a -> AST dom a- (:$) :: Typeable a => AST dom (a :-> b) -> ASTF dom a -> AST dom b+ 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) --- | Co-product of two symbol domains-data dom1 :+: dom2 :: * -> *- where- InjL :: dom1 a -> (dom1 :+: dom2) a- InjR :: dom2 a -> (dom1 :+: dom2) a+-- | Signature of a fully applied symbol+newtype Full a = Full { result :: a }+ deriving (Eq, Show, Typeable) -infixl 1 :$-infixr :+:+-- | 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 that performs the type-level recursion needed by 'appSym'-class ApplySym a f dom | a dom -> f, f -> a dom+-- | Class for the type-level recursion needed by 'appSym'+class ApplySym sig f dom | sig dom -> f, f -> sig dom where- appSym' :: AST dom a -> f+ appSym' :: AST dom sig -> f instance ApplySym (Full a) (ASTF dom a) dom where appSym' = id -instance (Typeable a, ApplySym b f' dom) =>- ApplySym (a :-> b) (ASTF dom a -> f') dom+instance ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom where appSym' sym a = appSym' (sym :$ a) --- | Generic symbol application------ 'appSym' has any type of the form:------ > appSym :: (expr :<: AST dom, Typeable a, Typeable b, ..., Typeable x)--- > => expr (a :-> b :-> ... :-> Full x)--- > -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)-appSym :: (ApplySym a f dom, Signature a, sym :<: AST dom) => sym a -> f-appSym sym = appSym' (inj sym)---- | Generic symbol application with explicit context-appSymCtx :: (ApplySym a f dom, Signature a, sym ctx :<: dom) =>- Proxy ctx -> sym ctx a -> f-appSymCtx _ = appSym+-- | 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 ----------------------------------------------------------------------------------- * Subsumption+-- * Symbol domains -------------------------------------------------------------------------------- -class sub :<: sup+-- | Direct sum of two symbol domains+data (dom1 :+: dom2) a where- -- | Injection from @sub@ to @sup@- inj :: Signature a => sub a -> sup a+ 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 (sub :<: sup) => ((:<:) sub (AST sup))- -- GHC 6.12 requires prefix syntax here+instance Project sub sup => Project sub (AST sup) where- inj = Sym . inj- prj (Sym a) = prj a prj _ = Nothing -instance ((:<:) expr expr)+instance Project expr expr where- inj = id prj = Just -instance ((:<:) expr1 (expr1 :+: expr2))+instance Project expr1 (expr1 :+: expr2) where- inj = InjL- prj (InjL a) = Just a prj _ = Nothing -instance (expr1 :<: expr3) => ((:<:) expr1 (expr2 :+: expr3))+instance Project expr1 expr3 => Project expr1 (expr2 :+: expr3) where- inj = InjR . inj- prj (InjR a) = prj a prj _ = Nothing ----- | 'inj' with explicit context-injCtx :: (sub ctx :<: sup, Signature a) => Proxy ctx -> sub ctx a -> sup a-injCtx _ = inj---- | 'prj' with explicit context-prjCtx :: (sub ctx :<: sup) => Proxy ctx -> sup a -> Maybe (sub ctx a)-prjCtx _ = prj--------------------------------------------------------------------------------------- * Syntactic sugar------------------------------------------------------------------------------------- | It is assumed that for all types @A@ fulfilling @(`Syntactic` A dom)@:------ > eval a == eval (desugar $ (id :: A -> A) $ sugar a)------ (using 'Language.Syntactic.Interpretation.Evaluation.eval')-class Typeable (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.- -- GHC doesn't yet handle equality super classes.- where- type Internal a- desugar :: a -> ASTF dom (Internal a)- sugar :: ASTF dom (Internal a) -> a--instance Typeable a => Syntactic (ASTF dom a) dom+-- | Symbol subsumption+class Project sub sup => sub :<: sup 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+ -- | Injection from @sub@ to @sup@+ inj :: sub a -> sup a --- | N-ary syntactic functions------ 'desugarN' has any type of the form:------ > desugarN ::--- > ( Syntactic a dom--- > , Syntactic b dom--- > , ...--- > , Syntactic x dom--- > ) => (a -> b -> ... -> x)--- > -> ( AST dom (Full (Internal a))--- > -> AST dom (Full (Internal b))--- > -> ...--- > -> AST dom (Full (Internal x))--- > )------ ...and vice versa for 'sugarN'.-class SyntacticN a internal | a -> internal+instance (sub :<: sup) => (sub :<: AST sup) where- desugarN :: a -> internal- sugarN :: internal -> a+ inj = Sym . inj -instance (Syntactic a dom, ia ~ AST dom (Full (Internal a))) => SyntacticN a ia+instance (expr :<: expr) where- desugarN = desugar- sugarN = sugar+ inj = id -instance- ( Syntactic a dom- , ia ~ Internal a- , SyntacticN b ib- ) =>- SyntacticN (a -> b) (AST dom (Full ia) -> ib)+instance (expr1 :<: (expr1 :+: expr2)) 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- :: (Signature a, sym :<: AST dom, ApplySym a b dom, SyntacticN c b)- => sym a -> c-sugarSym = sugarN . appSym---- | \"Sugared\" symbol application with explicit context-sugarSymCtx- :: (Signature a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b)- => Proxy ctx -> sym ctx a -> c-sugarSymCtx _ = sugarSym--------------------------------------------------------------------------------------- * AST processing-----------------------------------------------------------------------------------newtype Const a b = Const {unConst :: a}- -- Only used in the definition of 'queryNodeSimple'--newtype WrapAST c dom a = WrapAST { unWrapAST :: c (AST dom a) }- -- Only used in the definition of 'transformNode'+ inj = InjL --- | Query an 'AST' using a function that gets direct access to the top-most--- constructor and its sub-trees------ Note that, by instantiating the type @c@ with @`AST` dom'@, we get the--- following type, which shows that 'queryNode' can be directly used to--- transform syntax trees (see also 'transformNode'):------ > (forall b . (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> ASTF dom' a)--- > -> ASTF dom a--- > -> ASTF dom' a-queryNode :: forall dom c a- . (forall b . (Signature b, a ~ DenResult b) =>- dom b -> Args (AST dom) b -> c (Full a))- -> ASTF dom a- -> c (Full a)-queryNode f a = query a Nil+instance (expr1 :<: expr3) => (expr1 :<: (expr2 :+: expr3)) where- query :: (a ~ DenResult b) => AST dom b -> Args (AST dom) b -> c (Full a)- query (Sym a) args = f a args- query (c :$ a) args = query c (a :* args)---- | A simpler version of 'queryNode'------ This function can be used to create 'AST' traversal functions indexed by the--- symbol types, for example:------ > class Count subDomain--- > where--- > count' :: Count domain => subDomain a -> Args (AST domain) a -> Int--- >--- > instance (Count sub1, Count sub2) => Count (sub1 :+: sub2)--- > where--- > count' (InjL a) args = count' a args--- > count' (InjR a) args = count' a args--- >--- > count :: Count dom => ASTF dom a -> Int--- > count = queryNodeSimple count'------ Here, @count@ represents some static analysis on an 'AST'. Each constructor--- in the tree will be queried by @count'@ indexed by the corresponding symbol--- type. That way, @count'@ can be seen as an open-ended function on an open--- data type. The @(Count domain)@ constraint on @count'@ is to allow recursion--- over sub-trees.------ Let's say we have a symbol------ > data Add a--- > where--- > Add :: Add (Int :-> Int :-> Full Int)------ Then the @Count@ instance for @Add@ might look as follows:------ > instance Count Add--- > where--- > count' Add (a :* b :* Nil) = 1 + count a + count b-queryNodeSimple :: forall dom a c- . (forall b . (Signature b, a ~ DenResult b) =>- dom b -> Args (AST dom) b -> c)- -> ASTF dom a- -> c-queryNodeSimple f a = unConst $ queryNode (\c -> Const . f c) a---- | A version of 'queryNode' where the result is a transformed syntax tree,--- wrapped in a type constructor @c@-transformNode :: forall dom dom' c a- . ( forall b . (Signature b, a ~ DenResult b)- => dom b -> Args (AST dom) b -> c (ASTF dom' a)- )- -> ASTF dom a- -> c (ASTF dom' a)-transformNode f a = unWrapAST $ queryNode (\a args -> WrapAST (f a args)) a--+ inj = InjR . inj ------------------------------------------------------------------------------------ * Restricted syntax trees---------------------------------------------------------------------------------+-- 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. --- | An abstract representation of a constraint on @a@. An instance might look--- as follows:------ > instance MyClass a => Sat MyContext a--- > where--- > data Witness MyContext a = MyClass a => MyWitness--- > witness = MyWitness+-- | Generic symbol application ----- This allows us to use @(`Sat` MyContext a)@ instead of @(MyClass a)@. The--- point with this is that @MyContext@ can be provided as a parameter, so this--- effectively allows us to parameterize on class constraints. Note that the--- existential context in the data definition is important. This means that,--- given a constraint @(`Sat` MyContext a)@, we can always construct the context--- @(MyClass a)@ by calling the 'witness' method (the class instance only--- declares the reverse relationship).+-- 'appSym' has any type of the form: ----- This way of parameterizing over type classes was inspired by--- /Restricted Data Types in Haskell/ (John Hughes, /Haskell Workshop/, 1999).-class Sat ctx a- where- data Witness ctx a- witness :: Witness ctx a- -- TODO Could probably use a one-parameter class instead, see- --- -- http://www.haskell.org/pipermail/glasgow-haskell-users/2011-December/021292.html- --- -- (but without the Super type family). Or even better, use ConstraintKinds.--witnessByProxy :: Sat ctx a => Proxy ctx -> Proxy a -> Witness ctx a-witnessByProxy _ _ = witness---- | Witness of a @(`Sat` ctx a)@ constraint. This is different from--- @(`Witness` ctx a)@, which witnesses the class encoded by @ctx@. 'Witness''--- has a single constructor for all contexts, while 'Witness' has different--- constructors for different contexts.-data SatWit ctx a- where- SatWit :: Sat ctx a => SatWit ctx a--fromSatWit :: SatWit ctx a -> Witness ctx a-fromSatWit SatWit = witness---- | Expressions that act as witnesses of their result type-class WitnessSat expr- where- type SatContext expr- witnessSat :: expr a -> SatWit (SatContext expr) (DenResult a)---- | Expressions that act as witnesses of their result type-class MaybeWitnessSat ctx expr- where- maybeWitnessSat :: Proxy ctx -> expr a -> Maybe (SatWit ctx (DenResult a))--instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (AST dom)- where- maybeWitnessSat ctx (Sym a) = maybeWitnessSat ctx a- maybeWitnessSat ctx (f :$ _) = maybeWitnessSat ctx f--instance (MaybeWitnessSat ctx sub1, MaybeWitnessSat ctx sub2) =>- MaybeWitnessSat ctx (sub1 :+: sub2)- where- maybeWitnessSat ctx (InjL a) = maybeWitnessSat ctx a- maybeWitnessSat ctx (InjR a) = maybeWitnessSat ctx a---- | Convenient default implementation of 'maybeWitnessSat'-maybeWitnessSatDefault :: WitnessSat expr- => Proxy (SatContext expr)- -> expr a- -> Maybe (SatWit (SatContext expr) (DenResult a))-maybeWitnessSatDefault _ = Just . witnessSat---- | Type application for constraining the @ctx@ type of a parameterized symbol-withContext :: sym ctx a -> Proxy ctx -> sym ctx a-withContext = const---- | Representation of a fully polymorphic constraint -- i.e. @(`Sat` `Poly` a)@--- is satisfied by all types @a@.-data Poly--instance Sat Poly a- where- data Witness Poly a = PolyWit- witness = PolyWit--poly :: Proxy Poly-poly = Proxy---- | Representation of \"simple\" types: types satisfying--- @(`Eq` a, `Show` a, `Typeable` a)@-data SimpleCtx--instance (Eq a, Show a, Typeable a) => Sat SimpleCtx a- where- data Witness SimpleCtx a = (Eq a, Show a, Typeable a) => SimpleWit- witness = SimpleWit--simpleCtx :: Proxy SimpleCtx-simpleCtx = Proxy+-- > appSym :: (expr :<: AST dom)+-- > => expr (a :-> b :-> ... :-> Full x)+-- > -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)+appSym :: (ApplySym sig f dom, sym :<: AST dom) => sym sig -> f+appSym = appSym' . inj
+ Language/Syntactic/Traversal.hs view
@@ -0,0 +1,183 @@+-- | Generic traversals of 'AST' terms++module Language.Syntactic.Traversal+ ( gmapQ+ , gmapT+ , everywhereUp+ , everywhereDown+ , Args (..)+ , listArgs+ , mapArgs+ , mapArgsA+ , mapArgsM+ , appArgs+ , listFold+ , match+ , query+ , simpleMatch+ , fold+ , simpleFold+ , matchTrans+ , WrapFull (..)+ ) where++++import Control.Applicative++import Language.Syntactic.Syntax++++-- | Map a function over all immediate sub-terms (corresponds to the function+-- with the same name in Scrap Your Boilerplate)+gmapT :: forall dom+ . (forall a . ASTF dom a -> ASTF dom a)+ -> (forall a . ASTF dom a -> ASTF dom a)+gmapT f a = go a+ where+ go :: forall a . AST dom a -> AST dom a+ go (s :$ a) = go s :$ f a+ go s = s++-- | Map a function over all immediate sub-terms, collecting the results in a+-- list (corresponds to the function with the same name in Scrap Your+-- Boilerplate)+gmapQ :: forall dom b+ . (forall a . ASTF dom a -> b)+ -> (forall a . ASTF dom a -> [b])+gmapQ f a = go a+ where+ go :: forall a . AST dom a -> [b]+ go (s :$ a) = f a : go s+ go _ = []++-- | Apply a transformation bottom-up over an expression (corresponds to+-- @everywhere@ in Scrap Your Boilerplate)+everywhereUp+ :: (forall a . ASTF dom a -> ASTF dom a)+ -> (forall a . ASTF dom a -> ASTF dom a)+everywhereUp f = f . gmapT (everywhereUp f)++-- | Apply a transformation top-down over an expression (corresponds to+-- @everywhere'@ in Scrap Your Boilerplate)+everywhereDown+ :: (forall a . ASTF dom a -> ASTF dom a)+ -> (forall a . ASTF dom a -> ASTF dom a)+everywhereDown f = gmapT (everywhereDown f) . f++-- | List of symbol arguments+data Args c sig+ where+ Nil :: Args c (Full a)+ (:*) :: c (Full a) -> Args c sig -> Args c (a :-> sig)++infixr :*++-- | Map a function over an 'Args' list and collect the results in an ordinary+-- list+listArgs :: (forall a . c (Full a) -> b) -> Args c sig -> [b]+listArgs f Nil = []+listArgs f (a :* as) = f a : listArgs f as++-- | Map a function over an 'Args' list+mapArgs+ :: (forall a . c1 (Full a) -> c2 (Full a))+ -> (forall sig . Args c1 sig -> Args c2 sig)+mapArgs f Nil = Nil+mapArgs f (a :* as) = f a :* mapArgs f as++-- | Map an applicative function over an 'Args' list+mapArgsA :: Applicative f+ => (forall a . c1 (Full a) -> f (c2 (Full a)))+ -> (forall sig . Args c1 sig -> f (Args c2 sig))+mapArgsA f Nil = pure Nil+mapArgsA f (a :* as) = (:*) <$> f a <*> mapArgsA f as++-- | Map a monadic function over an 'Args' list+mapArgsM :: Monad m+ => (forall a . c1 (Full a) -> m (c2 (Full a)))+ -> (forall sig . Args c1 sig -> m (Args c2 sig))+mapArgsM f = unwrapMonad . mapArgsA (WrapMonad . f)++-- | Apply a (partially applied) symbol to a list of argument terms+appArgs :: AST dom sig -> Args (AST dom) sig -> ASTF dom (DenResult sig)+appArgs a Nil = a+appArgs s (a :* as) = appArgs (s :$ a) as++-- | \"Pattern match\" on an 'AST' using a function that gets direct access to+-- the top-most symbol and its sub-trees+match :: forall dom a c+ . ( forall sig . (a ~ DenResult sig) =>+ dom sig -> Args (AST dom) sig -> c (Full a)+ )+ -> ASTF dom a+ -> c (Full a)+match f a = go a Nil+ where+ go :: (a ~ DenResult sig) => AST dom sig -> Args (AST dom) sig -> c (Full a)+ go (Sym a) as = f a as+ go (s :$ a) as = go s (a :* as)++query :: forall dom a c+ . ( forall sig . (a ~ DenResult sig) =>+ dom sig -> Args (AST dom) sig -> c (Full a)+ )+ -> ASTF dom a+ -> c (Full a)+query = match+{-# DEPRECATED query "Please use `match` instead." #-}++-- | A version of 'match' with a simpler result type+simpleMatch :: forall dom a b+ . (forall sig . (a ~ DenResult sig) => dom sig -> Args (AST dom) sig -> b)+ -> ASTF dom a+ -> b+simpleMatch f = getConst . match (\s -> Const . f s)++-- | Fold an 'AST' using an 'Args' list to hold the results of sub-terms+fold :: forall dom c+ . (forall sig . dom sig -> Args c sig -> c (Full (DenResult sig)))+ -> (forall a . ASTF dom a -> c (Full a))+fold f = match (\s -> f s . mapArgs (fold f))++-- | Simplified version of 'fold' for situations where all intermediate results+-- have the same type+simpleFold :: forall dom b+ . (forall sig . dom sig -> Args (Const b) sig -> b)+ -> (forall a . ASTF dom a -> b)+simpleFold f = getConst . fold (\s -> Const . f s)++-- | Fold an 'AST' using a list to hold the results of sub-terms+listFold :: forall dom b+ . (forall sig . dom sig -> [b] -> b)+ -> (forall a . ASTF dom a -> b)+listFold f = simpleFold (\s -> f s . listArgs getConst)++newtype WrapAST c dom sig = WrapAST { unWrapAST :: c (AST dom sig) }+ -- Only used in the definition of 'matchTrans'++-- | A version of 'match' where the result is a transformed syntax tree,+-- wrapped in a type constructor @c@+matchTrans :: forall dom dom' c a+ . ( forall sig . (a ~ DenResult sig) =>+ dom sig -> Args (AST dom) sig -> c (ASTF dom' a)+ )+ -> ASTF dom a+ -> c (ASTF dom' a)+matchTrans f = unWrapAST . match (\s -> WrapAST . f s)++-- | Can be used to make an arbitrary type constructor indexed by @(`Full` a)@.+-- This is useful as the type constructor parameter of 'Args'. That is, use+--+-- > Args (WrapFull c) ...+--+-- instead of+--+-- > Args c ...+--+-- if @c@ is not indexed by @(`Full` a)@.+data WrapFull c a+ where+ WrapFull :: { unwrapFull :: c a } -> WrapFull c (Full a)+
syntactic.cabal view
@@ -1,46 +1,50 @@ Name: syntactic-Version: 0.9+Version: 1.0 Synopsis: Generic abstract syntax, and utilities for embedded languages Description: This library provides: . * Generic representation and manipulation of abstract syntax- using a practical encoding of open data types (based on Data- Types à la Carte [1]) .- * Utilities for analyzing and transforming generic syntax+ * Composable AST representations (partly based on Data Types à+ la Carte [1]) .- * General variable binding constructs+ * A collection of common syntactic constructs, including+ variable binding constructs .+ * Utilities for analyzing and transforming generic abstract+ syntax+ . * Utilities for building extensible embedded languages based on generic syntax . * A small proof-of-concept implementation of the embedded language Feldspar [2] (see the @Examples@ directory) .- Note: The library is probably mostly useful for /functional/- object languages, such as Feldspar. Currently, it does not- support cyclic programs.- .- The following people have contributed to Syntactic:+ For details, see the paper+ \"A Generic Abstract Syntax Model for Embedded Languages\"+ (ICFP 2012,+ <http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf>). .- * Anders Persson+ The maturity of this library varies between different modules.+ The core part ("Language.Syntactic") is rather stable, but many+ of the other modules are in a much more experimental state. .- \[1\] /Data types à la carte/, by Wouter Swierstra, in- /Journal of Functional Programming/, 2008+ \[1\] W. Swierstra. Data Types à la Carte.+ /Journal of Functional Programming/, 18(4):423-436, 2008,+ <http://dx.doi.org/10.1017/S0956796808006758>. . \[2\] <http://hackage.haskell.org/package/feldspar-language> License: BSD3 License-file: LICENSE Author: Emil Axelsson Maintainer: emax@chalmers.se-Copyright: Copyright (c) 2011, Emil Axelsson+Copyright: Copyright (c) 2011-2012, Emil Axelsson Homepage: http://projects.haskell.org/syntactic/ Category: Language Build-type: Simple Cabal-version: >=1.6 Extra-source-files:- Examples/ALaCarte.hs Examples/NanoFeldspar/Core.hs Examples/NanoFeldspar/Extra.hs Examples/NanoFeldspar/Vector.hs@@ -52,8 +56,12 @@ Library Exposed-modules:+ Data.DynamicAlt Language.Syntactic Language.Syntactic.Syntax+ Language.Syntactic.Traversal+ Language.Syntactic.Constraint+ Language.Syntactic.Sugar Language.Syntactic.Interpretation.Equality Language.Syntactic.Interpretation.Evaluation Language.Syntactic.Interpretation.Render@@ -68,8 +76,6 @@ Language.Syntactic.Constructs.Literal Language.Syntactic.Constructs.Monad Language.Syntactic.Constructs.Tuple- Language.Syntactic.Constructs.TupleSyntacticPoly- Language.Syntactic.Constructs.TupleSyntacticSimple Language.Syntactic.Frontend.Monad Language.Syntactic.Sharing.SimpleCodeMotion Language.Syntactic.Sharing.Utils@@ -82,30 +88,30 @@ Build-depends: array,- base >= 4.0 && < 4.6,+ base >= 4.0 && < 4.7, containers,+ constraints, data-hash,+ ghc-prim, mtl >= 2 && < 3, tagged, transformers >= 0.2, tuple >= 0.2 Extensions:+ ConstraintKinds DeriveDataTypeable DeriveFunctor- EmptyDataDecls FlexibleContexts FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving- MultiParamTypeClasses PatternGuards Rank2Types ScopedTypeVariables StandaloneDeriving TypeFamilies TypeOperators- TypeSynonymInstances ViewPatterns