diff --git a/Data/DynamicAlt.hs b/Data/DynamicAlt.hs new file mode 100644 --- /dev/null +++ b/Data/DynamicAlt.hs @@ -0,0 +1,28 @@ +-- | An alternative to "Data.Dynamic" with a different constraint on 'toDyn' + +module Data.DynamicAlt where + + + +import Data.Dynamic () +import Data.Typeable +import GHC.Prim +import Unsafe.Coerce + +import Data.Proxy + + + +data Dynamic = Dynamic TypeRep Any + +toDyn :: forall a b . Typeable (a -> b) => Proxy (a -> b) -> a -> Dynamic +toDyn _ a = case splitTyConApp $ typeOf (undefined :: a -> b) of + (_,[ta,_]) -> Dynamic ta (unsafeCoerce a) + +fromDyn :: Typeable a => Dynamic -> Maybe a +fromDyn (Dynamic t a) + | b <- unsafeCoerce a + , t == typeOf b + = Just b +fromDyn _ = Nothing + diff --git a/Examples/ALaCarte.hs b/Examples/ALaCarte.hs deleted file mode 100644 --- a/Examples/ALaCarte.hs +++ /dev/null @@ -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) - diff --git a/Examples/NanoFeldspar/Core.hs b/Examples/NanoFeldspar/Core.hs --- a/Examples/NanoFeldspar/Core.hs +++ b/Examples/NanoFeldspar/Core.hs @@ -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 diff --git a/Examples/NanoFeldspar/Extra.hs b/Examples/NanoFeldspar/Extra.hs --- a/Examples/NanoFeldspar/Extra.hs +++ b/Examples/NanoFeldspar/Extra.hs @@ -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 diff --git a/Examples/NanoFeldspar/Test.hs b/Examples/NanoFeldspar/Test.hs --- a/Examples/NanoFeldspar/Test.hs +++ b/Examples/NanoFeldspar/Test.hs @@ -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 diff --git a/Examples/NanoFeldspar/Vector.hs b/Examples/NanoFeldspar/Vector.hs --- a/Examples/NanoFeldspar/Vector.hs +++ b/Examples/NanoFeldspar/Vector.hs @@ -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 diff --git a/Language/Syntactic.hs b/Language/Syntactic.hs --- a/Language/Syntactic.hs +++ b/Language/Syntactic.hs @@ -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 (..)) diff --git a/Language/Syntactic/Constraint.hs b/Language/Syntactic/Constraint.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constraint.hs @@ -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 + diff --git a/Language/Syntactic/Constructs/Binding.hs b/Language/Syntactic/Constructs/Binding.hs --- a/Language/Syntactic/Constructs/Binding.hs +++ b/Language/Syntactic/Constructs/Binding.hs @@ -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 diff --git a/Language/Syntactic/Constructs/Binding/HigherOrder.hs b/Language/Syntactic/Constructs/Binding/HigherOrder.hs --- a/Language/Syntactic/Constructs/Binding/HigherOrder.hs +++ b/Language/Syntactic/Constructs/Binding/HigherOrder.hs @@ -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 diff --git a/Language/Syntactic/Constructs/Binding/Optimize.hs b/Language/Syntactic/Constructs/Binding/Optimize.hs --- a/Language/Syntactic/Constructs/Binding/Optimize.hs +++ b/Language/Syntactic/Constructs/Binding/Optimize.hs @@ -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' diff --git a/Language/Syntactic/Constructs/Condition.hs b/Language/Syntactic/Constructs/Condition.hs --- a/Language/Syntactic/Constructs/Condition.hs +++ b/Language/Syntactic/Constructs/Condition.hs @@ -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 diff --git a/Language/Syntactic/Constructs/Construct.hs b/Language/Syntactic/Constructs/Construct.hs --- a/Language/Syntactic/Constructs/Construct.hs +++ b/Language/Syntactic/Constructs/Construct.hs @@ -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 diff --git a/Language/Syntactic/Constructs/Decoration.hs b/Language/Syntactic/Constructs/Decoration.hs --- a/Language/Syntactic/Constructs/Decoration.hs +++ b/Language/Syntactic/Constructs/Decoration.hs @@ -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 diff --git a/Language/Syntactic/Constructs/Identity.hs b/Language/Syntactic/Constructs/Identity.hs --- a/Language/Syntactic/Constructs/Identity.hs +++ b/Language/Syntactic/Constructs/Identity.hs @@ -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 diff --git a/Language/Syntactic/Constructs/Literal.hs b/Language/Syntactic/Constructs/Literal.hs --- a/Language/Syntactic/Constructs/Literal.hs +++ b/Language/Syntactic/Constructs/Literal.hs @@ -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 diff --git a/Language/Syntactic/Constructs/Monad.hs b/Language/Syntactic/Constructs/Monad.hs --- a/Language/Syntactic/Constructs/Monad.hs +++ b/Language/Syntactic/Constructs/Monad.hs @@ -1,4 +1,8 @@ -- | Monadic constructs +-- +-- This module is based on the paper +-- /Generic Monadic Constructs for Embedded Languages/ (Persson et al., IFL 2011 +-- ). module Language.Syntactic.Constructs.Monad where @@ -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 diff --git a/Language/Syntactic/Constructs/Tuple.hs b/Language/Syntactic/Constructs/Tuple.hs --- a/Language/Syntactic/Constructs/Tuple.hs +++ b/Language/Syntactic/Constructs/Tuple.hs @@ -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 + ) diff --git a/Language/Syntactic/Constructs/TupleSyntacticPoly.hs b/Language/Syntactic/Constructs/TupleSyntacticPoly.hs deleted file mode 100644 --- a/Language/Syntactic/Constructs/TupleSyntacticPoly.hs +++ /dev/null @@ -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 - diff --git a/Language/Syntactic/Constructs/TupleSyntacticSimple.hs b/Language/Syntactic/Constructs/TupleSyntacticSimple.hs deleted file mode 100644 --- a/Language/Syntactic/Constructs/TupleSyntacticSimple.hs +++ /dev/null @@ -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 - diff --git a/Language/Syntactic/Frontend/Monad.hs b/Language/Syntactic/Frontend/Monad.hs --- a/Language/Syntactic/Frontend/Monad.hs +++ b/Language/Syntactic/Frontend/Monad.hs @@ -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 +-- ). + 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 diff --git a/Language/Syntactic/Interpretation/Equality.hs b/Language/Syntactic/Interpretation/Equality.hs --- a/Language/Syntactic/Interpretation/Equality.hs +++ b/Language/Syntactic/Interpretation/Equality.hs @@ -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 diff --git a/Language/Syntactic/Interpretation/Evaluation.hs b/Language/Syntactic/Interpretation/Evaluation.hs --- a/Language/Syntactic/Interpretation/Evaluation.hs +++ b/Language/Syntactic/Interpretation/Evaluation.hs @@ -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 diff --git a/Language/Syntactic/Interpretation/Render.hs b/Language/Syntactic/Interpretation/Render.hs --- a/Language/Syntactic/Interpretation/Render.hs +++ b/Language/Syntactic/Interpretation/Render.hs @@ -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 diff --git a/Language/Syntactic/Interpretation/Semantics.hs b/Language/Syntactic/Interpretation/Semantics.hs --- a/Language/Syntactic/Interpretation/Semantics.hs +++ b/Language/Syntactic/Interpretation/Semantics.hs @@ -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 diff --git a/Language/Syntactic/Sharing/Graph.hs b/Language/Syntactic/Sharing/Graph.hs --- a/Language/Syntactic/Sharing/Graph.hs +++ b/Language/Syntactic/Sharing/Graph.hs @@ -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 diff --git a/Language/Syntactic/Sharing/Reify.hs b/Language/Syntactic/Sharing/Reify.hs --- a/Language/Syntactic/Sharing/Reify.hs +++ b/Language/Syntactic/Sharing/Reify.hs @@ -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, ). 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 diff --git a/Language/Syntactic/Sharing/ReifyHO.hs b/Language/Syntactic/Sharing/ReifyHO.hs --- a/Language/Syntactic/Sharing/ReifyHO.hs +++ b/Language/Syntactic/Sharing/ReifyHO.hs @@ -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, ). 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 diff --git a/Language/Syntactic/Sharing/SimpleCodeMotion.hs b/Language/Syntactic/Sharing/SimpleCodeMotion.hs --- a/Language/Syntactic/Sharing/SimpleCodeMotion.hs +++ b/Language/Syntactic/Sharing/SimpleCodeMotion.hs @@ -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 diff --git a/Language/Syntactic/Sharing/StableName.hs b/Language/Syntactic/Sharing/StableName.hs --- a/Language/Syntactic/Sharing/StableName.hs +++ b/Language/Syntactic/Sharing/StableName.hs @@ -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 + -- + -- 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 diff --git a/Language/Syntactic/Sugar.hs b/Language/Syntactic/Sugar.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Sugar.hs @@ -0,0 +1,111 @@ +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | \"Syntactic sugar\" + +module Language.Syntactic.Sugar where + + + +import Language.Syntactic.Syntax +import Language.Syntactic.Constraint + + + +-- | It is usually assumed that @(`desugar` (`sugar` a))@ has the same meaning +-- as @a@. +class Syntactic a dom | a -> dom + -- Note: using a functional dependency rather than an associated type, + -- because this makes it possible to make a class alias constraining dom. + -- TODO Now that GHC allows equality super class constraints, this should be + -- changed to an associated type. + where + type Internal a + desugar :: a -> ASTF dom (Internal a) + sugar :: ASTF dom (Internal a) -> a + +instance Syntactic (ASTF dom a) dom + where + type Internal (ASTF dom a) = a + desugar = id + sugar = id + +-- | Syntactic type casting +resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b +resugar = sugar . desugar + +-- | N-ary syntactic functions +-- +-- 'desugarN' has any type of the form: +-- +-- > desugarN :: +-- > ( Syntactic a dom +-- > , Syntactic b dom +-- > , ... +-- > , Syntactic x dom +-- > ) => (a -> b -> ... -> x) +-- > -> ( ASTF dom (Internal a) +-- > -> ASTF dom (Internal b) +-- > -> ... +-- > -> ASTF dom (Internal x) +-- > ) +-- +-- ...and vice versa for 'sugarN'. +class SyntacticN a internal | a -> internal + where + desugarN :: a -> internal + sugarN :: internal -> a + +instance (Syntactic a dom, ia ~ AST dom (Full (Internal a))) => SyntacticN a ia + where + desugarN = desugar + sugarN = sugar + +instance + ( Syntactic a dom + , ia ~ Internal a + , SyntacticN b ib + ) => + SyntacticN (a -> b) (AST dom (Full ia) -> ib) + where + desugarN f = desugarN . f . sugar + sugarN f = sugarN . f . desugar + + + +-- | \"Sugared\" symbol application +-- +-- 'sugarSym' has any type of the form: +-- +-- > sugarSym :: +-- > ( expr :<: AST dom +-- > , Syntactic a dom +-- > , Syntactic b dom +-- > , ... +-- > , Syntactic x dom +-- > ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x)) +-- > -> (a -> b -> ... -> x) +sugarSym :: (sym :<: AST dom, ApplySym sig b dom, SyntacticN c b) => + sym sig -> c +sugarSym = sugarN . appSym + +-- | \"Sugared\" symbol application +-- +-- 'sugarSymC' has any type of the form: +-- +-- > sugarSymC :: +-- > ( InjectC expr (AST dom) (Internal x) +-- > , Syntactic a dom +-- > , Syntactic b dom +-- > , ... +-- > , Syntactic x dom +-- > ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x)) +-- > -> (a -> b -> ... -> x) +sugarSymC + :: ( InjectC sym (AST dom) (DenResult sig) + , ApplySym sig b dom + , SyntacticN c b + ) + => sym sig -> c +sugarSymC = sugarN . appSymC + diff --git a/Language/Syntactic/Syntax.hs b/Language/Syntactic/Syntax.hs --- a/Language/Syntactic/Syntax.hs +++ b/Language/Syntactic/Syntax.hs @@ -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, ). 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 diff --git a/Language/Syntactic/Traversal.hs b/Language/Syntactic/Traversal.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Traversal.hs @@ -0,0 +1,183 @@ +-- | Generic traversals of 'AST' terms + +module Language.Syntactic.Traversal + ( gmapQ + , gmapT + , everywhereUp + , everywhereDown + , Args (..) + , listArgs + , mapArgs + , mapArgsA + , mapArgsM + , appArgs + , listFold + , match + , query + , simpleMatch + , fold + , simpleFold + , matchTrans + , WrapFull (..) + ) where + + + +import Control.Applicative + +import Language.Syntactic.Syntax + + + +-- | Map a function over all immediate sub-terms (corresponds to the function +-- with the same name in Scrap Your Boilerplate) +gmapT :: forall dom + . (forall a . ASTF dom a -> ASTF dom a) + -> (forall a . ASTF dom a -> ASTF dom a) +gmapT f a = go a + where + go :: forall a . AST dom a -> AST dom a + go (s :$ a) = go s :$ f a + go s = s + +-- | Map a function over all immediate sub-terms, collecting the results in a +-- list (corresponds to the function with the same name in Scrap Your +-- Boilerplate) +gmapQ :: forall dom b + . (forall a . ASTF dom a -> b) + -> (forall a . ASTF dom a -> [b]) +gmapQ f a = go a + where + go :: forall a . AST dom a -> [b] + go (s :$ a) = f a : go s + go _ = [] + +-- | Apply a transformation bottom-up over an expression (corresponds to +-- @everywhere@ in Scrap Your Boilerplate) +everywhereUp + :: (forall a . ASTF dom a -> ASTF dom a) + -> (forall a . ASTF dom a -> ASTF dom a) +everywhereUp f = f . gmapT (everywhereUp f) + +-- | Apply a transformation top-down over an expression (corresponds to +-- @everywhere'@ in Scrap Your Boilerplate) +everywhereDown + :: (forall a . ASTF dom a -> ASTF dom a) + -> (forall a . ASTF dom a -> ASTF dom a) +everywhereDown f = gmapT (everywhereDown f) . f + +-- | List of symbol arguments +data Args c sig + where + Nil :: Args c (Full a) + (:*) :: c (Full a) -> Args c sig -> Args c (a :-> sig) + +infixr :* + +-- | Map a function over an 'Args' list and collect the results in an ordinary +-- list +listArgs :: (forall a . c (Full a) -> b) -> Args c sig -> [b] +listArgs f Nil = [] +listArgs f (a :* as) = f a : listArgs f as + +-- | Map a function over an 'Args' list +mapArgs + :: (forall a . c1 (Full a) -> c2 (Full a)) + -> (forall sig . Args c1 sig -> Args c2 sig) +mapArgs f Nil = Nil +mapArgs f (a :* as) = f a :* mapArgs f as + +-- | Map an applicative function over an 'Args' list +mapArgsA :: Applicative f + => (forall a . c1 (Full a) -> f (c2 (Full a))) + -> (forall sig . Args c1 sig -> f (Args c2 sig)) +mapArgsA f Nil = pure Nil +mapArgsA f (a :* as) = (:*) <$> f a <*> mapArgsA f as + +-- | Map a monadic function over an 'Args' list +mapArgsM :: Monad m + => (forall a . c1 (Full a) -> m (c2 (Full a))) + -> (forall sig . Args c1 sig -> m (Args c2 sig)) +mapArgsM f = unwrapMonad . mapArgsA (WrapMonad . f) + +-- | Apply a (partially applied) symbol to a list of argument terms +appArgs :: AST dom sig -> Args (AST dom) sig -> ASTF dom (DenResult sig) +appArgs a Nil = a +appArgs s (a :* as) = appArgs (s :$ a) as + +-- | \"Pattern match\" on an 'AST' using a function that gets direct access to +-- the top-most symbol and its sub-trees +match :: forall dom a c + . ( forall sig . (a ~ DenResult sig) => + dom sig -> Args (AST dom) sig -> c (Full a) + ) + -> ASTF dom a + -> c (Full a) +match f a = go a Nil + where + go :: (a ~ DenResult sig) => AST dom sig -> Args (AST dom) sig -> c (Full a) + go (Sym a) as = f a as + go (s :$ a) as = go s (a :* as) + +query :: forall dom a c + . ( forall sig . (a ~ DenResult sig) => + dom sig -> Args (AST dom) sig -> c (Full a) + ) + -> ASTF dom a + -> c (Full a) +query = match +{-# DEPRECATED query "Please use `match` instead." #-} + +-- | A version of 'match' with a simpler result type +simpleMatch :: forall dom a b + . (forall sig . (a ~ DenResult sig) => dom sig -> Args (AST dom) sig -> b) + -> ASTF dom a + -> b +simpleMatch f = getConst . match (\s -> Const . f s) + +-- | Fold an 'AST' using an 'Args' list to hold the results of sub-terms +fold :: forall dom c + . (forall sig . dom sig -> Args c sig -> c (Full (DenResult sig))) + -> (forall a . ASTF dom a -> c (Full a)) +fold f = match (\s -> f s . mapArgs (fold f)) + +-- | Simplified version of 'fold' for situations where all intermediate results +-- have the same type +simpleFold :: forall dom b + . (forall sig . dom sig -> Args (Const b) sig -> b) + -> (forall a . ASTF dom a -> b) +simpleFold f = getConst . fold (\s -> Const . f s) + +-- | Fold an 'AST' using a list to hold the results of sub-terms +listFold :: forall dom b + . (forall sig . dom sig -> [b] -> b) + -> (forall a . ASTF dom a -> b) +listFold f = simpleFold (\s -> f s . listArgs getConst) + +newtype WrapAST c dom sig = WrapAST { unWrapAST :: c (AST dom sig) } + -- Only used in the definition of 'matchTrans' + +-- | A version of 'match' where the result is a transformed syntax tree, +-- wrapped in a type constructor @c@ +matchTrans :: forall dom dom' c a + . ( forall sig . (a ~ DenResult sig) => + dom sig -> Args (AST dom) sig -> c (ASTF dom' a) + ) + -> ASTF dom a + -> c (ASTF dom' a) +matchTrans f = unWrapAST . match (\s -> WrapAST . f s) + +-- | Can be used to make an arbitrary type constructor indexed by @(`Full` a)@. +-- This is useful as the type constructor parameter of 'Args'. That is, use +-- +-- > Args (WrapFull c) ... +-- +-- instead of +-- +-- > Args c ... +-- +-- if @c@ is not indexed by @(`Full` a)@. +data WrapFull c a + where + WrapFull :: { unwrapFull :: c a } -> WrapFull c (Full a) + diff --git a/syntactic.cabal b/syntactic.cabal --- a/syntactic.cabal +++ b/syntactic.cabal @@ -1,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, + ). . - * 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, + . . \[2\] 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