diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2011-2014, Emil Axelsson +Copyright (c) 2011-2015, Emil Axelsson All rights reserved. diff --git a/benchmarks/JoiningTypes.hs b/benchmarks/JoiningTypes.hs --- a/benchmarks/JoiningTypes.hs +++ b/benchmarks/JoiningTypes.hs @@ -4,8 +4,8 @@ import Criterion.Main import Criterion.Types -import Data.Syntactic -import Data.Syntactic.Functional +import Language.Syntactic +import Language.Syntactic.Functional -- Normal DSL, not joined types. data Expr1 t where diff --git a/benchmarks/Normal.hs b/benchmarks/Normal.hs --- a/benchmarks/Normal.hs +++ b/benchmarks/Normal.hs @@ -4,8 +4,8 @@ import Criterion.Main import Criterion.Types -import Data.Syntactic -import Data.Syntactic.Functional +import Language.Syntactic +import Language.Syntactic.Functional main :: IO () main = defaultMainWith (defaultConfig {csvFile = Just "bench-results/normal.csv"}) diff --git a/benchmarks/WithArity.hs b/benchmarks/WithArity.hs --- a/benchmarks/WithArity.hs +++ b/benchmarks/WithArity.hs @@ -4,8 +4,8 @@ import Criterion.Main import Criterion.Types -import Data.Syntactic hiding (E) -import Data.Syntactic.Functional +import Language.Syntactic hiding (E) +import Language.Syntactic.Functional main :: IO () main = defaultMainWith (defaultConfig {csvFile = Just "bench-results/withArity.csv"}) diff --git a/examples/Monad.hs b/examples/Monad.hs --- a/examples/Monad.hs +++ b/examples/Monad.hs @@ -17,43 +17,43 @@ import Data.Char (isDigit) import Data.Typeable (Typeable) -import Data.Syntactic -import Data.Syntactic.Functional -import Data.Syntactic.Sugar.MonadT () +import Language.Syntactic +import Language.Syntactic.Functional +import Language.Syntactic.Sugar.MonadT () import NanoFeldspar (Type, Arithmetic (..)) -type Dom = BindingT :+: MONAD IO :+: Construct :+: Arithmetic +type Dom = Typed (BindingT :+: MONAD IO :+: Construct :+: Arithmetic) type Exp a = ASTF Dom a type IO' a = Remon Dom IO (Exp a) getDigit :: IO' Int -getDigit = sugarSym $ Construct "getDigit" get +getDigit = sugarSymT $ Construct "getDigit" get where get = do c <- getChar if isDigit c then return (fromEnum c - fromEnum '0') else get putDigit :: Exp Int -> IO' () -putDigit = sugarSym $ Construct "putDigit" print +putDigit = sugarSymT $ Construct "putDigit" print iter :: Typeable a => Exp Int -> IO' a -> IO' () -iter = sugarSym $ Construct "iter" replicateM_ +iter = sugarSymT $ Construct "iter" replicateM_ -- | Literal -value :: Show a => a -> Exp a -value a = sugar $ inj $ Construct (show a) a +value :: (Show a, Typeable a) => a -> Exp a +value a = sugarSymT $ Construct (show a) a instance (Num a, Type a) => Num (Exp a) where fromInteger = value . fromInteger - (+) = sugarSym Add - (-) = sugarSym Sub - (*) = sugarSym Mul + (+) = sugarSymT Add + (-) = sugarSymT Sub + (*) = sugarSymT Mul ex1 :: Exp Int -> IO' () ex1 n = iter n $ do diff --git a/examples/NanoFeldspar.hs b/examples/NanoFeldspar.hs --- a/examples/NanoFeldspar.hs +++ b/examples/NanoFeldspar.hs @@ -20,13 +20,15 @@ import Prelude hiding (max, min, not, (==), length, map, sum, zip, zipWith) import qualified Prelude -import Data.Tree import Data.Typeable -import Data.Syntactic hiding (fold, printExpr, showAST, drawAST, writeHtmlAST) -import qualified Data.Syntactic as Syntactic -import Data.Syntactic.Functional -import Data.Syntactic.Sugar.BindingT () +import Language.Syntactic hiding (fold, printExpr, showAST, drawAST, writeHtmlAST) +import qualified Language.Syntactic as Syntactic +import Language.Syntactic.Functional +import Language.Syntactic.Functional.Sharing +import Language.Syntactic.Functional.Tuple +import Language.Syntactic.Sugar.BindingT () +import Language.Syntactic.Sugar.TupleT () @@ -76,35 +78,6 @@ instance EvalEnv Arithmetic env -data Let sig - where - Let :: Let (a :-> (a -> b) :-> Full b) - -instance Symbol Let - where - symSig Let = signature - -instance Equality Let - where - equal = equalDefault - hash = hashDefault - -instance Render Let - where - renderSym Let = "letBind" - -instance StringTree Let - where - stringTreeSym [a, Node lam [body]] Let - | ("Lam",v) <- splitAt 3 lam = Node ("Let" ++ v) [a,body] - stringTreeSym [a,f] Let = Node "Let" [a,f] - -instance Eval Let - where - evalSym Let = flip ($) - -instance EvalEnv Let env - data Parallel sig where Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a]) @@ -145,13 +118,20 @@ instance EvalEnv ForLoop env -type FeldDomain - = Arithmetic - :+: BindingT +type FeldDomain = Typed + ( BindingT :+: Let + :+: Tuple + :+: Arithmetic :+: Parallel :+: ForLoop :+: Construct + ) + -- `Construct` can be used to create arbitrary symbols from a name and an + -- evaluation function. We could have used `Construct` for all symbols, but + -- the problem with `Construct` is that it does not know about the arity or + -- type of the construct it represents, so it's easy to make mistakes, e.g. + -- when transforming expressions with `Construct` symbols. newtype Data a = Data { unData :: ASTF FeldDomain a } @@ -169,7 +149,7 @@ instance Type a => Show (Data a) where - show = render . unData + show = showExpr @@ -177,9 +157,37 @@ -- * "Backends" -------------------------------------------------------------------------------- +cmInterface :: CodeMotionInterface FeldDomain +cmInterface = defaultInterfaceT sharable (const True) + where + sharable :: ASTF FeldDomain a -> ASTF FeldDomain b -> Bool + sharable (Sym _) _ = False + -- Simple expressions not shared + sharable (lam :$ _) _ + | Just _ <- prLam lam = False + -- Lambdas not shared + sharable _ (lam :$ _) + | Just _ <- prLam lam = False + -- Don't place let bindings over lambdas. This ensures that function + -- arguments of higher-order constructs such as `Parallel` are always + -- lambdas. + sharable (sel :$ _) _ + | Just Sel1 <- prj sel = False + | Just Sel2 <- prj sel = False + | Just Sel3 <- prj sel = False + | Just Sel4 <- prj sel = False + -- Tuple selection not shared + sharable (arrl :$ _ ) _ + | Just (Construct "arrLen" _) <- prj arrl = False + -- Array length not shared + sharable (gix :$ _ :$ _) _ + | Just (Construct "arrIx" _) <- prj gix = False + -- Array indexing not shared + sharable _ _ = True + -- | Show the expression showExpr :: (Syntactic a, Domain a ~ FeldDomain) => a -> String -showExpr = render . desugar +showExpr = render . codeMotion cmInterface . desugar -- | Print the expression printExpr :: (Syntactic a, Domain a ~ FeldDomain) => a -> IO () @@ -187,7 +195,7 @@ -- | Show the syntax tree using unicode art showAST :: (Syntactic a, Domain a ~ FeldDomain) => a -> String -showAST = Syntactic.showAST . desugar +showAST = Syntactic.showAST . codeMotion cmInterface . desugar -- | Draw the syntax tree on the terminal using unicode art drawAST :: (Syntactic a, Domain a ~ FeldDomain) => a -> IO () @@ -195,8 +203,10 @@ -- | Write the syntax tree to an HTML file with foldable nodes writeHtmlAST :: (Syntactic a, Domain a ~ FeldDomain) => a -> IO () -writeHtmlAST = Syntactic.writeHtmlAST "tree.html" . desugar +writeHtmlAST = + Syntactic.writeHtmlAST "tree.html" . codeMotion cmInterface . desugar +-- | Evaluate an expression eval :: (Syntactic a, Domain a ~ FeldDomain) => a -> Internal a eval = evalClosed . desugar @@ -208,7 +218,7 @@ -- | Literal value :: Syntax a => Internal a -> a -value a = sugar $ inj $ Construct (show a) a +value a = sugar $ injT $ Construct (show a) a false :: Data Bool false = value False @@ -216,59 +226,61 @@ true :: Data Bool true = value True --- | For types containing some kind of \"thunk\", this function can be used to --- force computation +-- | Force computation force :: Syntax a => a -> a force = resugar instance (Type a, Num a) => Num (Data a) where fromInteger = value . fromInteger - (+) = sugarSym Add - (-) = sugarSym Sub - (*) = sugarSym Mul + (+) = sugarSymT Add + (-) = sugarSymT Sub + (*) = sugarSymT Mul -share :: (Syntax a, Syntactic b, Domain b ~ FeldDomain) => a -> (a -> b) -> b -share = sugarSym Let +-- | Explicit sharing +share :: (Syntax a, Syntax b) => a -> (a -> b) -> b +share = sugarSymT Let -- | Parallel array parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a] -parallel = sugarSym Parallel +parallel = sugarSymT Parallel -- | For loop forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st -forLoop = sugarSym ForLoop +forLoop = sugarSymT ForLoop +-- | Conditional expression (?) :: forall a . Syntax a => Data Bool -> (a,a) -> a -c ? (t,f) = sugarSym sym c t f +c ? (t,f) = sugarSymT sym c t f where sym :: Construct (Bool :-> Internal a :-> Internal a :-> Full (Internal a)) sym = Construct "cond" (\c t f -> if c then t else f) -arrLength :: Type a => Data [a] -> Data Length -arrLength = sugarSym $ Construct "arrLength" Prelude.length +-- | Get the length of an array +arrLen :: Type a => Data [a] -> Data Length +arrLen = sugarSymT $ Construct "arrLen" Prelude.length --- | Array indexing -getIx :: Type a => Data [a] -> Data Index -> Data a -getIx = sugarSym $ Construct "getIx" eval +-- | Index into an array +arrIx :: Type a => Data [a] -> Data Index -> Data a +arrIx = sugarSymT $ Construct "arrIx" eval where eval as i - | i >= len || i < 0 = error "getIx: index out of bounds" + | i >= len || i < 0 = error "arrIx: index out of bounds" | otherwise = as !! i where len = Prelude.length as not :: Data Bool -> Data Bool -not = sugarSym $ Construct "not" Prelude.not +not = sugarSymT $ Construct "not" Prelude.not (==) :: Type a => Data a -> Data a -> Data Bool -(==) = sugarSym $ Construct "(==)" (Prelude.==) +(==) = sugarSymT $ Construct "(==)" (Prelude.==) max :: Type a => Data a -> Data a -> Data a -max = sugarSym $ Construct "max" Prelude.max +max = sugarSymT $ Construct "max" Prelude.max min :: Type a => Data a -> Data a -> Data a -min = sugarSym $ Construct "min" Prelude.min +min = sugarSymT $ Construct "min" Prelude.min @@ -305,7 +317,7 @@ freezeVector vec = parallel (length vec) (index vec) thawVector :: Type a => Data [a] -> Vector (Data a) -thawVector arr = Indexed (arrLength arr) (getIx arr) +thawVector arr = Indexed (arrLen arr) (arrIx arr) zip :: Vector a -> Vector b -> Vector (a,b) zip a b = indexed (length a `min` length b) (\i -> (index a i, index b i)) @@ -335,6 +347,9 @@ fold :: Syntax b => (a -> b -> b) -> b -> Vector a -> b fold f b (Indexed len ixf) = forLoop len b (\i st -> f (ixf i) st) +fold1 :: Syntax a => (a -> a -> a) -> Vector a -> a +fold1 f (Indexed len ixf) = forLoop len (ixf 0) (\i st -> f (ixf i) st) + sum :: (Num a, Syntax a) => Vector a -> a sum = fold (+) 0 @@ -349,6 +364,19 @@ -------------------------------------------------------------------------------- -- * Examples -------------------------------------------------------------------------------- + +-- | Fibonacci function +fib :: Data Int -> Data Int +fib n = fst $ forLoop n (0,1) $ \_ (a,b) -> (b,a+b) + +-- | The span of a vector (difference between greatest and smallest element) +spanVec :: Vector (Data Int) -> Data Int +spanVec vec = hi-lo + where + (lo,hi) = fold (\a (l,h) -> (min a l, max a h)) (vec!0,vec!0) vec + -- This demonstrates how tuples interplay with sharing. Tuples are essentially + -- useless without sharing. This function would get two identical for loops if + -- it wasn't for sharing. -- | Scalar product scProd :: Vector (Data Float) -> Vector (Data Float) -> Data Float diff --git a/examples/WellScoped.hs b/examples/WellScoped.hs --- a/examples/WellScoped.hs +++ b/examples/WellScoped.hs @@ -16,10 +16,9 @@ -import Data.Syntactic -import Data.Syntactic.Functional - -import NanoFeldspar (Let (..)) +import Language.Syntactic +import Language.Syntactic.Functional +import Language.Syntactic.Functional.WellScoped diff --git a/src/Data/Syntactic.hs b/src/Data/Syntactic.hs deleted file mode 100644 --- a/src/Data/Syntactic.hs +++ /dev/null @@ -1,18 +0,0 @@ --- | The basic parts of the syntactic library - -module Data.Syntactic - ( module Data.Syntactic.Syntax - , module Data.Syntactic.Traversal - , module Data.Syntactic.Interpretation - , module Data.Syntactic.Sugar - , module Data.Syntactic.Decoration - ) where - - - -import Data.Syntactic.Syntax -import Data.Syntactic.Traversal -import Data.Syntactic.Interpretation -import Data.Syntactic.Sugar -import Data.Syntactic.Decoration - diff --git a/src/Data/Syntactic/Decoration.hs b/src/Data/Syntactic/Decoration.hs deleted file mode 100644 --- a/src/Data/Syntactic/Decoration.hs +++ /dev/null @@ -1,115 +0,0 @@ --- | Construct for decorating symbols or expressions with additional information - -module Data.Syntactic.Decoration where - - - -import Data.Tree (Tree (..)) - -import Data.Tree.View - -import Data.Syntactic.Syntax -import Data.Syntactic.Traversal -import Data.Syntactic.Interpretation - - - --- | Decorating symbols or expressions with additional information --- --- One usage of ':&:' is to decorate every node of a syntax tree. This is done --- simply by changing --- --- > AST sym sig --- --- to --- --- > AST (sym :&: info) sig -data (expr :&: info) sig - where - (:&:) - :: { decorExpr :: expr sig - , decorInfo :: info (DenResult sig) - } - -> (expr :&: info) sig - -instance Symbol sym => Symbol (sym :&: info) - where - rnfSym = rnfSym . decorExpr - symSig = symSig . decorExpr - -instance Project sub sup => Project sub (sup :&: info) - where - prj = prj . decorExpr - -instance Equality expr => Equality (expr :&: info) - where - equal a b = decorExpr a `equal` decorExpr b - hash = hash . decorExpr - -instance Render expr => Render (expr :&: info) - where - renderSym = renderSym . decorExpr - renderArgs args = renderArgs args . decorExpr - -instance StringTree expr => StringTree (expr :&: info) - where - stringTreeSym args = stringTreeSym args . decorExpr - - - --- | Map over a decoration -mapDecor - :: (sym1 sig -> sym2 sig) - -> (info1 (DenResult sig) -> info2 (DenResult sig)) - -> ((sym1 :&: info1) sig -> (sym2 :&: info2) sig) -mapDecor fs fi (s :&: i) = fs s :&: fi i - --- | Get the decoration of the top-level node -getDecor :: AST (sym :&: info) sig -> info (DenResult sig) -getDecor (Sym (_ :&: info)) = info -getDecor (f :$ _) = getDecor f - --- | Update the decoration of the top-level node -updateDecor :: forall info sym a . - (info a -> info a) -> ASTF (sym :&: info) a -> ASTF (sym :&: info) a -updateDecor f = match update - where - update - :: (a ~ DenResult sig) - => (sym :&: info) sig - -> Args (AST (sym :&: info)) sig - -> ASTF (sym :&: info) a - update (a :&: info) args = appArgs (Sym sym) args - where - sym = a :&: (f info) - --- | Lift a function that operates on expressions with associated information to --- operate on a ':&:' expression. This function is convenient to use together --- with e.g. 'queryNodeSimple' when the domain has the form @(sym `:&:` info)@. -liftDecor :: (expr s -> info (DenResult s) -> b) -> ((expr :&: info) s -> b) -liftDecor f (a :&: info) = f a info - --- | Strip decorations from an 'AST' -stripDecor :: AST (sym :&: info) sig -> AST sym sig -stripDecor (Sym (a :&: _)) = Sym a -stripDecor (f :$ a) = stripDecor f :$ stripDecor a - --- | Rendering of decorated syntax trees -stringTreeDecor :: forall info sym a . StringTree sym => - (forall a . info a -> String) -> ASTF (sym :&: info) a -> Tree String -stringTreeDecor showInfo a = mkTree [] a - where - mkTree :: [Tree String] -> AST (sym :&: info) sig -> Tree String - mkTree args (Sym (expr :&: info)) = Node infoStr [stringTreeSym args expr] - where - infoStr = "<<" ++ showInfo info ++ ">>" - mkTree args (f :$ a) = mkTree (mkTree [] a : args) f - --- | Show an decorated syntax tree using ASCII art -showDecorWith :: StringTree sym => (forall a . info a -> String) -> ASTF (sym :&: info) a -> String -showDecorWith showInfo = showTree . stringTreeDecor showInfo - --- | Print an decorated syntax tree using ASCII art -drawDecorWith :: StringTree sym => (forall a . info a -> String) -> ASTF (sym :&: info) a -> IO () -drawDecorWith showInfo = putStrLn . showDecorWith showInfo - diff --git a/src/Data/Syntactic/Functional.hs b/src/Data/Syntactic/Functional.hs deleted file mode 100644 --- a/src/Data/Syntactic/Functional.hs +++ /dev/null @@ -1,709 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE UndecidableInstances #-} - -#ifndef MIN_VERSION_GLASGOW_HASKELL -#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0 -#endif - -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10 - -#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) -#else -{-# LANGUAGE OverlappingInstances #-} -#endif - --- | Basics for implementing functional EDSLs - -module Data.Syntactic.Functional - ( -- * Syntactic constructs - Name (..) - , Construct (..) - , Binding (..) - , maxLam - , lam - , fromDeBruijn - , BindingT (..) - , maxLamT - , lamT - , BindingDomain (..) - , MONAD (..) - , Remon (..) - , desugarMonad - -- * Alpha-equivalence - , AlphaEnv - , alphaEq' - , alphaEq - -- * Evaluation - , Denotation - , Eval (..) - , evalDen - , DenotationM - , liftDenotationM - , RunEnv - , EvalEnv (..) - , compileSymDefault - , evalOpen - , evalClosed - -- * Well-scoped terms - , Ext (..) - , lookEnv - , BindingWS (..) - , lamWS - , evalOpenWS - , evalClosedWS - , LiftReader - , UnReader - , LowerReader - , ReaderSym (..) - , WS - , fromWS - , smartWS - ) where - - - -import Control.Applicative -- Needed by GHC < 7.10 -import Control.DeepSeq -import Control.Monad.Cont -import Control.Monad.Reader -import Data.Dynamic -import Data.List (genericIndex) -import Data.Proxy -- Needed by GHC < 7.8 -import Data.Tree - -import Data.Hash (hashInt) -import Safe - -import Data.Syntactic - - - ----------------------------------------------------------------------------------------------------- --- * Syntactic constructs ----------------------------------------------------------------------------------------------------- - --- | Generic N-ary syntactic construct --- --- 'Construct' gives a quick way to introduce a syntactic construct by giving its name and semantic --- function. -data Construct sig - where - Construct :: Signature sig => String -> Denotation sig -> Construct sig - -instance Symbol Construct - where - rnfSym (Construct name den) = rnf name `seq` den `seq` () - symSig (Construct _ _) = signature - -instance Render Construct - where - renderSym (Construct name _) = name - renderArgs = renderArgsSmart - -instance Equality Construct - where - equal = equalDefault - hash = hashDefault - -instance StringTree Construct - --- | Variable name -newtype Name = Name Integer - deriving (Eq, Ord, Num, Enum, Real, Integral, NFData) - -instance Show Name - where - show (Name n) = show n - --- | Variables and binders -data Binding sig - where - Var :: Name -> Binding (Full a) - Lam :: Name -> Binding (b :-> Full (a -> b)) - -instance Symbol Binding - where - rnfSym (Var v) = rnf v - rnfSym (Lam v) = rnf v - symSig (Var _) = signature - symSig (Lam _) = signature - --- | 'equal' does strict identifier comparison; i.e. no alpha equivalence. --- --- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation --- that enables the following property: --- --- @`alphaEq` a b ==> `hash` a == `hash` b@ -instance Equality Binding - where - equal (Var v1) (Var v2) = v1==v2 - equal (Lam v1) (Lam v2) = v1==v2 - equal _ _ = False - - hash (Var _) = hashInt 0 - hash (Lam _) = hashInt 0 - -instance Render Binding - where - renderSym (Var v) = 'v' : show v - renderSym (Lam v) = "Lam v" ++ show v - renderArgs [] (Var v) = 'v' : show v - renderArgs [body] (Lam v) = "(\\" ++ ('v':show v) ++ " -> " ++ body ++ ")" - -instance StringTree Binding - where - stringTreeSym [] (Var v) = Node ('v' : show v) [] - stringTreeSym [body] (Lam v) = Node ("Lam " ++ 'v' : show v) [body] - --- | Get the highest name bound by the first 'Lam' binders at every path from the root. If the term --- has /ordered binders/ \[1\], 'maxLam' returns the highest name introduced in the whole term. --- --- \[1\] Ordered binders means that the names of 'Lam' nodes are decreasing along every path from --- the root. -maxLam :: (Binding :<: s) => AST s a -> Name -maxLam (Sym lam :$ _) | Just (Lam v) <- prj lam = v -maxLam (s :$ a) = maxLam s `Prelude.max` maxLam a -maxLam _ = 0 - --- | Higher-order interface for variable binding --- --- Assumptions: --- --- * The body @f@ does not inspect its argument. --- --- * Applying @f@ to a term with ordered binders results in a term with /ordered binders/ \[1\]. --- --- \[1\] Ordered binders means that the names of 'Lam' nodes are decreasing along every path from --- the root. --- --- See \"Using Circular Programs for Higher-Order Syntax\" --- (ICFP 2013, ). -lam :: (Binding :<: s) => (ASTF s a -> ASTF s b) -> ASTF s (a -> b) -lam f = smartSym (Lam v) body - where - body = f (smartSym (Var v)) - v = succ $ maxLam body - --- | Convert from a term with De Bruijn indexes to one with explicit names --- --- In the argument term, variable 'Name's are treated as De Bruijn indexes, and lambda 'Name's are --- ignored. (Ideally, one should use a different type for De Bruijn terms.) -fromDeBruijn :: (Binding :<: sym) => ASTF sym a -> ASTF sym a -fromDeBruijn = go [] - where - go :: (Binding :<: sym) => [Name] -> ASTF sym a -> (ASTF sym a) - go vs var | Just (Var i) <- prj var = inj $ Var $ genericIndex vs i - go vs (lam :$ body) | Just (Lam _) <- prj lam = inj (Lam v) :$ body' - where - body' = go (v:vs) body - v = succ $ maxLam body' - -- Same trick as in `lam` - go vs a = gmapT (go vs) a - --- | Typed variables and binders -data BindingT sig - where - VarT :: Typeable a => Name -> BindingT (Full a) - LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b)) - -instance Symbol BindingT - where - rnfSym (VarT v) = rnf v - rnfSym (LamT v) = rnf v - symSig (VarT _) = signature - symSig (LamT _) = signature - --- | 'equal' does strict identifier comparison; i.e. no alpha equivalence. --- --- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation --- that enables the following property: --- --- @`alphaEq` a b ==> `hash` a == `hash` b@ -instance Equality BindingT - where - equal (VarT v1) (VarT v2) = v1==v2 - equal (LamT v1) (LamT v2) = v1==v2 - equal _ _ = False - - hash (VarT _) = hashInt 0 - hash (LamT _) = hashInt 0 - -instance Render BindingT - where - renderSym (VarT v) = renderSym (Var v) - renderSym (LamT v) = renderSym (Lam v) - renderArgs args (VarT v) = renderArgs args (Var v) - renderArgs args (LamT v) = renderArgs args (Lam v) - -instance StringTree BindingT - where - stringTreeSym args (VarT v) = stringTreeSym args (Var v) - stringTreeSym args (LamT v) = stringTreeSym args (Lam v) - --- | Get the highest name bound by the first 'LamT' binders at every path from the root. If the term --- has /ordered binders/ \[1\], 'maxLamT' returns the highest name introduced in the whole term. --- --- \[1\] Ordered binders means that the names of 'LamT' nodes are decreasing along every path from --- the root. -maxLamT :: (BindingT :<: s) => AST s a -> Name -maxLamT (Sym lam :$ _) | Just (LamT n :: BindingT (b :-> a)) <- prj lam = n -maxLamT (s :$ a) = maxLamT s `Prelude.max` maxLamT a -maxLamT _ = 0 - --- | Higher-order interface for typed variable binding --- --- Assumptions: --- --- * The body @f@ does not inspect its argument. --- --- * Applying @f@ to a term with ordered binders results in a term with /ordered binders/ \[1\]. --- --- \[1\] Ordered binders means that the names of 'LamT' nodes are decreasing along every path from --- the root. --- --- See \"Using Circular Programs for Higher-Order Syntax\" --- (ICFP 2013, ). -lamT :: forall s a b . (BindingT :<: s, Typeable a) => (ASTF s a -> ASTF s b) -> ASTF s (a -> b) -lamT f = smartSym (LamT v :: BindingT (b :-> Full (a -> b))) body - where - body = f (smartSym (VarT v)) - v = succ $ maxLamT body - --- | Domains that \"might\" include variables and binders -class BindingDomain sym - where - prVar :: sym sig -> Maybe Name - prLam :: sym sig -> Maybe Name - -- It is in principle possible to replace a constraint `BindingDomain s` by - -- `(Project Binding s, Project BindingT s)`. However, the problem is that one then has to - -- specify the type `t` through a `Proxy`. The `BindingDomain` class gets around this problem. - -instance {-# OVERLAPPING #-} - (BindingDomain sym1, BindingDomain sym2) => BindingDomain (sym1 :+: sym2) - where - prVar (InjL s) = prVar s - prVar (InjR s) = prVar s - prLam (InjL s) = prLam s - prLam (InjR s) = prLam s - -instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (sym :&: i) - where - prVar = prVar . decorExpr - prLam = prLam . decorExpr - -instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (AST sym) - where - prVar (Sym s) = prVar s - prVar _ = Nothing - prLam (Sym s) = prLam s - prLam _ = Nothing - -instance {-# OVERLAPPING #-} BindingDomain Binding - where - prVar (Var v) = Just v - prVar _ = Nothing - prLam (Lam v) = Just v - prLam _ = Nothing - -instance {-# OVERLAPPING #-} BindingDomain BindingT - where - prVar (VarT v) = Just v - prVar _ = Nothing - prLam (LamT v) = Just v - prLam _ = Nothing - -instance {-# OVERLAPPING #-} BindingDomain sym - where - prVar _ = Nothing - prLam _ = Nothing - --- | Monadic constructs --- --- See \"Generic Monadic Constructs for Embedded Languages\" (Persson et al., IFL 2011 --- ). -data MONAD m sig - where - Return :: MONAD m (a :-> Full (m a)) - Bind :: MONAD m (m a :-> (a -> m b) :-> Full (m b)) - -instance Symbol (MONAD m) - where - symSig Return = signature - symSig Bind = signature - -instance Render (MONAD m) - where - renderSym Return = "return" - renderSym Bind = "(>>=)" - renderArgs = renderArgsSmart - -instance Equality (MONAD m) - where - equal = equalDefault - hash = hashDefault - -instance StringTree (MONAD m) - --- | Reifiable monad --- --- See \"Generic Monadic Constructs for Embedded Languages\" (Persson et al., IFL 2011 --- ). --- --- It is advised to convert to/from 'Mon' using the 'Syntactic' instance provided in the modules --- @Data.Syntactic.Sugar.Monad@ or @Data.Syntactic.Sugar.MonadT@. -newtype Remon sym m a - where - Remon - :: { unRemon :: forall r . (Monad m, MONAD m :<: sym) => Cont (ASTF sym (m r)) a } - -> Remon sym m a - deriving (Functor) - -instance (Applicative m) => Applicative (Remon sym m) - where - pure a = Remon $ pure a - f <*> a = Remon $ unRemon f <*> unRemon a - -instance (Monad m) => Monad (Remon dom m) - where - return a = Remon $ return a - ma >>= f = Remon $ unRemon ma >>= unRemon . f - --- | One-layer desugaring of monadic actions -desugarMonad :: (MONAD m :<: sym, Monad m) => Remon sym m (ASTF sym a) -> ASTF sym (m a) -desugarMonad = flip runCont (sugarSym Return) . unRemon - - - ----------------------------------------------------------------------------------------------------- --- * Alpha-equivalence ----------------------------------------------------------------------------------------------------- - --- | Environment used by 'alphaEq'' -type AlphaEnv = [(Name,Name)] - -alphaEq' :: (Equality sym, BindingDomain sym) => AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool -alphaEq' env var1 var2 - | Just v1 <- prVar var1 - , Just v2 <- prVar var2 - = case (lookup v1 env, lookup v2 env') of - (Nothing, Nothing) -> v1==v2 -- Free variables - (Just v2', Just v1') -> v1==v1' && v2==v2' - _ -> False - where - env' = [(v2,v1) | (v1,v2) <- env] -alphaEq' env (lam1 :$ body1) (lam2 :$ body2) - | Just v1 <- prLam lam1 - , Just v2 <- prLam lam2 - = alphaEq' ((v1,v2):env) body1 body2 -alphaEq' env a b = simpleMatch (alphaEq'' env b) a - -alphaEq'' :: (Equality sym, BindingDomain sym) => - AlphaEnv -> ASTF sym b -> sym a -> Args (AST sym) a -> Bool -alphaEq'' env b a aArgs = simpleMatch (alphaEq''' env a aArgs) b - -alphaEq''' :: (Equality sym, BindingDomain sym) => - AlphaEnv -> sym a -> Args (AST sym) a -> sym b -> Args (AST sym) b -> Bool -alphaEq''' env a aArgs b bArgs - | equal a b = alphaEqChildren env a' b' - | otherwise = False - where - a' = appArgs (Sym undefined) aArgs - b' = appArgs (Sym undefined) bArgs - -alphaEqChildren :: (Equality sym, BindingDomain sym) => AlphaEnv -> AST sym a -> AST sym b -> Bool -alphaEqChildren _ (Sym _) (Sym _) = True -alphaEqChildren env (s :$ a) (t :$ b) = alphaEqChildren env s t && alphaEq' env a b -alphaEqChildren _ _ _ = False - --- | Alpha-equivalence -alphaEq :: (Equality sym, BindingDomain sym) => ASTF sym a -> ASTF sym b -> Bool -alphaEq = alphaEq' [] - - - ----------------------------------------------------------------------------------------------------- --- * Evaluation ----------------------------------------------------------------------------------------------------- - --- | Semantic function type of the given symbol signature -type family Denotation sig -type instance Denotation (Full a) = a -type instance Denotation (a :-> sig) = a -> Denotation sig - -class Eval s - where - evalSym :: s sig -> Denotation sig - -instance (Eval s, Eval t) => Eval (s :+: t) - where - evalSym (InjL s) = evalSym s - evalSym (InjR s) = evalSym s - -instance Eval Empty - where - evalSym = error "evalSym: Empty" - -instance Eval sym => Eval (sym :&: info) - where - evalSym = evalSym . decorExpr - -instance Eval Construct - where - evalSym (Construct _ d) = d - -instance Monad m => Eval (MONAD m) - where - evalSym Return = return - evalSym Bind = (>>=) - --- | Evaluation -evalDen :: Eval s => AST s sig -> Denotation sig -evalDen = go - where - go :: Eval s => AST s sig -> Denotation sig - go (Sym s) = evalSym s - go (s :$ a) = go s $ go a - --- | Monadic denotation; mapping from a symbol signature --- --- > a :-> b :-> Full c --- --- to --- --- > m a -> m b -> m c -type family DenotationM (m :: * -> *) sig -type instance DenotationM m (Full a) = m a -type instance DenotationM m (a :-> sig) = m a -> DenotationM m sig - --- | Lift a 'Denotation' to 'DenotationM' -liftDenotationM :: forall m sig proxy1 proxy2 . Monad m => - SigRep sig -> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig -liftDenotationM sig _ _ = help2 sig . help1 sig - where - help1 :: Monad m => - SigRep sig' -> Denotation sig' -> Args (WrapFull m) sig' -> m (DenResult sig') - help1 SigFull f _ = return f - help1 (SigMore sig) f (WrapFull ma :* as) = do - a <- ma - help1 sig (f a) as - - help2 :: SigRep sig' -> (Args (WrapFull m) sig' -> m (DenResult sig')) -> DenotationM m sig' - help2 SigFull f = f Nil - help2 (SigMore sig) f = \a -> help2 sig (\as -> f (WrapFull a :* as)) - --- | Runtime environment -type RunEnv = [(Name, Dynamic)] - -- TODO Use a more efficient data structure? - --- | Evaluation -class EvalEnv sym env - where - default compileSym :: (Symbol sym, Eval sym) => - proxy env -> sym sig -> DenotationM (Reader env) sig - - compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig - compileSym p s = compileSymDefault (symSig s) p s - --- | Simple implementation of `compileSym` from a 'Denotation' -compileSymDefault :: forall proxy env sym sig . Eval sym => - SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig -compileSymDefault sig p s = liftDenotationM sig (Proxy :: Proxy (Reader env)) s (evalSym s) - -instance (EvalEnv sym1 env, EvalEnv sym2 env) => EvalEnv (sym1 :+: sym2) env - where - compileSym p (InjL s) = compileSym p s - compileSym p (InjR s) = compileSym p s - -instance EvalEnv Empty env - where - compileSym = error "compileSym: Empty" - -instance EvalEnv sym env => EvalEnv (sym :&: info) env - where - compileSym p = compileSym p . decorExpr - -instance EvalEnv Construct env - where - compileSym _ s@(Construct _ d) = liftDenotationM signature p s d - where - p = Proxy :: Proxy (Reader env) - -instance Monad m => EvalEnv (MONAD m) env - -instance EvalEnv BindingT RunEnv - where - compileSym _ (VarT v) = reader $ \env -> case fromJustNote (msgVar v) $ lookup v env of - d -> fromJustNote msgType $ fromDynamic d - where - msgVar v = "compileSym: Variable " ++ show v ++ " not in scope" - msgType = "compileSym: type error" -- TODO Print types - compileSym _ (LamT v) = \body -> reader $ \env a -> runReader body ((v, toDyn a) : env) - --- | \"Compile\" a term to a Haskell function -compile :: EvalEnv sym env => proxy env -> AST sym sig -> DenotationM (Reader env) sig -compile p (Sym s) = compileSym p s -compile p (s :$ a) = compile p s $ compile p a - -- This use of the term \"compile\" comes from \"Typing Dynamic Typing\" (Baars and Swierstra, - -- ICFP 2002, ) - --- | Evaluation of open terms -evalOpen :: EvalEnv sym env => env -> ASTF sym a -> a -evalOpen env a = runReader (compile Proxy a) env - --- | Evaluation of closed terms where 'RunEnv' is used as the internal environment --- --- (Note that there is no guarantee that the term is actually closed.) -evalClosed :: EvalEnv sym RunEnv => ASTF sym a -> a -evalClosed a = runReader (compile (Proxy :: Proxy RunEnv) a) [] - - - ----------------------------------------------------------------------------------------------------- --- * Well-scoped terms ----------------------------------------------------------------------------------------------------- - --- | Environment extension -class Ext ext orig - where - -- | Remove the extension of an environment - unext :: ext -> orig - -- | Return the amount by which an environment has been extended - diff :: Num a => Proxy ext -> Proxy orig -> a - -instance {-# OVERLAPPING #-} Ext env env - where - unext = id - diff _ _ = 0 - -instance {-# OVERLAPPING #-} (Ext env e, ext ~ (a,env)) => Ext ext e - where - unext = unext . snd - diff m n = diff (fmap snd m) n + 1 - --- | Lookup in an extended environment -lookEnv :: forall env a e . Ext env (a,e) => Proxy e -> Reader env a -lookEnv _ = reader $ \env -> let (a, _ :: e) = unext env in a - --- | Well-scoped variable binding --- --- Well-scoped terms are introduced to be able to evaluate without type casting. The implementation --- is inspired by \"Typing Dynamic Typing\" (Baars and Swierstra, ICFP 2002, --- ) where expressions are represented as (essentially) --- @`Reader` env a@ after \"compilation\". However, a major difference is that --- \"Typing Dynamic Typing\" starts from an untyped term, and thus needs (safe) dynamic type casting --- during compilation. In contrast, the denotational semantics of 'BindingWS' (the 'Eval' instance) --- uses no type casting. -data BindingWS sig - where - VarWS :: Ext env (a,e) => Proxy e -> BindingWS (Full (Reader env a)) - LamWS :: BindingWS (Reader (a,e) b :-> Full (Reader e (a -> b))) - -instance Symbol BindingWS - where - rnfSym (VarWS Proxy) = () - rnfSym LamWS = () - symSig (VarWS _) = signature - symSig LamWS = signature - -instance Eval BindingWS - where - evalSym (VarWS p) = lookEnv p - evalSym LamWS = \f -> reader $ \e -> \a -> runReader f (a,e) - --- | Higher-order interface for well-scoped variable binding --- --- Inspired by Conor McBride's "I am not a number, I am a classy hack" --- (). -lamWS :: forall a e sym b . (BindingWS :<: sym) - => ((forall env . (Ext env (a,e)) => ASTF sym (Reader env a)) -> ASTF sym (Reader (a,e) b)) - -> ASTF sym (Reader e (a -> b)) -lamWS f = smartSym LamWS $ f $ smartSym (VarWS (Proxy :: Proxy e)) - --- | Evaluation of open well-scoped terms -evalOpenWS :: Eval s => env -> ASTF s (Reader env a) -> a -evalOpenWS e = ($ e) . runReader . evalDen - --- | Evaluation of closed well-scoped terms -evalClosedWS :: Eval s => ASTF s (Reader () a) -> a -evalClosedWS = evalOpenWS () - --- | Mapping from a symbol signature --- --- > a :-> b :-> Full c --- --- to --- --- > Reader env a :-> Reader env b :-> Full (Reader env c) -type family LiftReader env sig -type instance LiftReader env (Full a) = Full (Reader env a) -type instance LiftReader env (a :-> sig) = Reader env a :-> LiftReader env sig - -type family UnReader a -type instance UnReader (Reader e a) = a - --- | Mapping from a symbol signature --- --- > Reader e a :-> Reader e b :-> Full (Reader e c) --- --- to --- --- > a :-> b :-> Full c -type family LowerReader sig -type instance LowerReader (Full a) = Full (UnReader a) -type instance LowerReader (a :-> sig) = UnReader a :-> LowerReader sig - --- | Wrap a symbol to give it a 'LiftReader' signature -data ReaderSym sym sig - where - ReaderSym - :: ( Signature sig - , Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig - , LowerReader (LiftReader env sig) ~ sig - ) - => Proxy env - -> sym sig - -> ReaderSym sym (LiftReader env sig) - -instance Eval sym => Eval (ReaderSym sym) - where - evalSym (ReaderSym (_ :: Proxy env) s) = liftDenotationM signature p s $ evalSym s - where - p = Proxy :: Proxy (Reader env) - --- | Well-scoped 'AST' -type WS sym env a = ASTF (BindingWS :+: ReaderSym sym) (Reader env a) - --- | Convert the representation of variables and binders from 'BindingWS' to 'Binding'. The latter --- is easier to analyze, has a 'Render' instance, etc. -fromWS :: WS sym env a -> ASTF (Binding :+: sym) a -fromWS = fromDeBruijn . go - where - go :: AST (BindingWS :+: ReaderSym sym) sig -> AST (Binding :+: sym) (LowerReader sig) - go (Sym (InjL s@(VarWS p))) = Sym (InjL (Var (diff (mkProxy2 s) (mkProxy1 s p)))) - where - mkProxy1 = (\_ _ -> Proxy) :: BindingWS (Full (Reader e' a)) -> Proxy e -> Proxy (a,e) - mkProxy2 = (\_ -> Proxy) :: BindingWS (Full (Reader e' a)) -> Proxy e' - go (Sym (InjL LamWS)) = Sym $ InjL $ Lam (-1) -- -1 since we're using De Bruijn - go (s :$ a) = go s :$ go a - go (Sym (InjR (ReaderSym _ s))) = Sym $ InjR s - --- | Make a smart constructor for well-scoped terms. 'smartWS' has any type of the form: --- --- > smartWS :: (sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup)) --- > => sub (a :-> b :-> ... :-> Full x) --- > -> ASTF bsym (Reader env a) -> ASTF bsym (Reader env b) -> ... -> ASTF bsym (Reader env x) -smartWS :: forall sig sig' bsym f sub sup env a - . ( Signature sig - , Signature sig' - , sub :<: sup - , bsym ~ (BindingWS :+: ReaderSym sup) - , f ~ SmartFun bsym sig' - , sig' ~ SmartSig f - , bsym ~ SmartSym f - , sig' ~ LiftReader env sig - , Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig - , LowerReader (LiftReader env sig) ~ sig - , Reader env a ~ DenResult sig' - ) - => sub sig -> f -smartWS s = smartSym' $ InjR $ ReaderSym (Proxy :: Proxy env) $ inj s - diff --git a/src/Data/Syntactic/Interpretation.hs b/src/Data/Syntactic/Interpretation.hs deleted file mode 100644 --- a/src/Data/Syntactic/Interpretation.hs +++ /dev/null @@ -1,205 +0,0 @@ -{-# LANGUAGE TemplateHaskell #-} - --- | Equality and rendering of 'AST's - -module Data.Syntactic.Interpretation - ( -- * Equality - Equality (..) - -- * Rendering - , Render (..) - , renderArgsSmart - , render - , StringTree (..) - , stringTree - , showAST - , drawAST - , writeHtmlAST - -- * Default interpretation - , equalDefault - , hashDefault - , interpretationInstances - ) where - - - -import Data.Tree (Tree (..)) -import Language.Haskell.TH - -import Data.Hash (Hash, combine, hashInt) -import qualified Data.Hash as Hash -import Data.Tree.View - -import Data.Syntactic.Syntax - - - ----------------------------------------------------------------------------------------------------- --- * Equality ----------------------------------------------------------------------------------------------------- - --- | Higher-kinded equality -class Equality e - where - -- | Higher-kinded equality - -- - -- Comparing elements of different types is often needed when dealing with expressions with - -- existentially quantified sub-terms. - equal :: e a -> e b -> Bool - - -- | Higher-kinded hashing. Elements that are equal according to 'equal' must result in the same - -- hash: - -- - -- @equal a b ==> hash a == hash b@ - hash :: e a -> Hash - -instance Equality sym => Equality (AST sym) - where - equal (Sym s1) (Sym s2) = equal s1 s2 - equal (s1 :$ a1) (s2 :$ a2) = equal s1 s2 && equal a1 a2 - equal _ _ = False - - hash (Sym s) = hashInt 0 `combine` hash s - hash (s :$ a) = hashInt 1 `combine` hash s `combine` hash a - -instance Equality sym => Eq (AST sym a) - where - (==) = equal - -instance (Equality sym1, Equality sym2) => Equality (sym1 :+: sym2) - where - equal (InjL a) (InjL b) = equal a b - equal (InjR a) (InjR b) = equal a b - equal _ _ = False - - hash (InjL a) = hashInt 0 `combine` hash a - hash (InjR a) = hashInt 1 `combine` hash a - -instance (Equality sym1, Equality sym2) => Eq ((sym1 :+: sym2) a) - where - (==) = equal - -instance Equality Empty - where - equal = error "equal: Empty" - hash = error "hash: Empty" - - - ----------------------------------------------------------------------------------------------------- --- * Rendering ----------------------------------------------------------------------------------------------------- - --- | Render a symbol as concrete syntax. A complete instance must define at least the 'renderSym' --- method. -class Render sym - where - -- | Show a symbol as a 'String' - renderSym :: sym sig -> String - - -- | Render a symbol given a list of rendered arguments - renderArgs :: [String] -> sym sig -> String - renderArgs [] s = renderSym s - renderArgs args s = "(" ++ unwords (renderSym s : args) ++ ")" - -instance (Render sym1, Render sym2) => Render (sym1 :+: sym2) - where - renderSym (InjL s) = renderSym s - renderSym (InjR s) = renderSym s - renderArgs args (InjL s) = renderArgs args s - renderArgs args (InjR s) = renderArgs args s - --- | Implementation of 'renderArgs' that handles infix operators -renderArgsSmart :: Render sym => [String] -> sym a -> String -renderArgsSmart [] sym = renderSym sym -renderArgsSmart args sym - | isInfix = "(" ++ unwords [a,op,b] ++ ")" - | otherwise = "(" ++ unwords (name : args) ++ ")" - where - name = renderSym sym - [a,b] = args - op = init $ tail name - isInfix - = not (null name) - && head name == '(' - && last name == ')' - && length args == 2 - --- | Render an 'AST' as concrete syntax -render :: forall sym a. Render sym => ASTF sym a -> String -render = go [] - where - go :: [String] -> AST sym sig -> String - go args (Sym s) = renderArgs args s - go args (s :$ a) = go (render a : args) s - -instance Render Empty - where - renderSym = error "renderSym: Empty" - renderArgs = error "renderArgs: Empty" - -instance Render sym => Show (ASTF sym a) - where - show = render - - - --- | Convert a symbol to a 'Tree' of strings -class Render sym => StringTree sym - where - -- | Convert a symbol to a 'Tree' given a list of argument trees - stringTreeSym :: [Tree String] -> sym a -> Tree String - stringTreeSym args s = Node (renderSym s) args - -instance (StringTree sym1, StringTree sym2) => StringTree (sym1 :+: sym2) - where - stringTreeSym args (InjL s) = stringTreeSym args s - stringTreeSym args (InjR s) = stringTreeSym args s - -instance StringTree Empty - --- | Convert an 'AST' to a 'Tree' of strings -stringTree :: forall sym a . StringTree sym => ASTF sym a -> Tree String -stringTree = go [] - where - go :: [Tree String] -> AST sym sig -> Tree String - go args (Sym s) = stringTreeSym args s - go args (s :$ a) = go (stringTree a : args) s - --- | Show a syntax tree using ASCII art -showAST :: StringTree sym => ASTF sym a -> String -showAST = showTree . stringTree - --- | Print a syntax tree using ASCII art -drawAST :: StringTree sym => ASTF sym a -> IO () -drawAST = putStrLn . showAST - --- | Write a syntax tree to an HTML file with foldable nodes -writeHtmlAST :: StringTree sym => FilePath -> ASTF sym a -> IO () -writeHtmlAST file = writeHtmlTree file . fmap (\n -> NodeInfo n "") . stringTree - - - ----------------------------------------------------------------------------------------------------- --- * Default interpretation ----------------------------------------------------------------------------------------------------- - --- | Default implementation of 'equal' -equalDefault :: Render sym => sym a -> sym b -> Bool -equalDefault a b = renderSym a == renderSym b - --- | Default implementation of 'hash' -hashDefault :: Render sym => sym a -> Hash -hashDefault = Hash.hash . renderSym - --- | Derive instances for 'Equality' and 'StringTree' -interpretationInstances :: Name -> DecsQ -interpretationInstances n = - [d| - instance Equality $(typ) where - equal = equalDefault - hash = hashDefault - instance StringTree $(typ) - |] - where - typ = conT n - diff --git a/src/Data/Syntactic/Sugar.hs b/src/Data/Syntactic/Sugar.hs deleted file mode 100644 --- a/src/Data/Syntactic/Sugar.hs +++ /dev/null @@ -1,113 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE UndecidableInstances #-} - -#ifndef MIN_VERSION_GLASGOW_HASKELL -#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0 -#endif - -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10 - -#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) -#else -{-# LANGUAGE OverlappingInstances #-} -#endif - --- | \"Syntactic sugar\" --- --- For details, see "Combining Deep and Shallow Embedding for EDSL" --- (TFP 2013, ). - -module Data.Syntactic.Sugar where - - - -import Data.Syntactic.Syntax - - - --- | It is usually assumed that @(`desugar` (`sugar` a))@ has the same meaning --- as @a@. -class Syntactic a - where - type Domain a :: * -> * - type Internal a - desugar :: a -> ASTF (Domain a) (Internal a) - sugar :: ASTF (Domain a) (Internal a) -> a - -instance Syntactic (ASTF sym a) - where - type Domain (ASTF sym a) = sym - type Internal (ASTF sym a) = a - desugar = id - sugar = id - --- | Syntactic type casting -resugar :: (Syntactic a, Syntactic b, Domain a ~ Domain b, Internal a ~ Internal b) => a -> b -resugar = sugar . desugar - --- | N-ary syntactic functions --- --- 'desugarN' has any type of the form: --- --- > desugarN :: --- > ( Syntactic a --- > , Syntactic b --- > , ... --- > , Syntactic x --- > , Domain a ~ sym --- > , Domain b ~ sym --- > , ... --- > , Domain x ~ sym --- > ) => (a -> b -> ... -> x) --- > -> ( ASTF sym (Internal a) --- > -> ASTF sym (Internal b) --- > -> ... --- > -> ASTF sym (Internal x) --- > ) --- --- ...and vice versa for 'sugarN'. -class SyntacticN f internal | f -> internal - where - desugarN :: f -> internal - sugarN :: internal -> f - -instance {-# OVERLAPPING #-} - (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi - where - desugarN = desugar - sugarN = sugar - -instance {-# OVERLAPPING #-} - ( Syntactic a - , Domain a ~ sym - , ia ~ Internal a - , SyntacticN f fi - ) => - SyntacticN (a -> f) (AST sym (Full ia) -> fi) - where - desugarN f = desugarN . f . sugar - sugarN f = sugarN . f . desugar - --- | \"Sugared\" symbol application --- --- 'sugarSym' has any type of the form: --- --- > sugarSym :: --- > ( sub :<: AST sup --- > , Syntactic a --- > , Syntactic b --- > , ... --- > , Syntactic x --- > , Domain a ~ Domain b ~ ... ~ Domain x --- > ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x)) --- > -> (a -> b -> ... -> x) -sugarSym - :: ( Signature sig - , fi ~ SmartFun sup sig - , sig ~ SmartSig fi - , sup ~ SmartSym fi - , SyntacticN f fi - , sub :<: sup - ) - => sub sig -> f -sugarSym = sugarN . smartSym - diff --git a/src/Data/Syntactic/Sugar/Binding.hs b/src/Data/Syntactic/Sugar/Binding.hs deleted file mode 100644 --- a/src/Data/Syntactic/Sugar/Binding.hs +++ /dev/null @@ -1,28 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | 'Syntactic' instance for functions --- --- This module is based on having 'Binding' in the domain. For 'BindingT' import module --- "Data.Syntactic.Sugar.BindingT" instead - -module Data.Syntactic.Sugar.Binding where - - - -import Data.Syntactic -import Data.Syntactic.Functional - - - -instance - ( Syntactic a, Domain a ~ dom - , Syntactic b, Domain b ~ dom - , Binding :<: dom - ) => - Syntactic (a -> b) - where - type Domain (a -> b) = Domain a - type Internal (a -> b) = Internal a -> Internal b - desugar f = lam (desugar . f . sugar) - sugar = error "sugar not implemented for (a -> b)" - diff --git a/src/Data/Syntactic/Sugar/BindingT.hs b/src/Data/Syntactic/Sugar/BindingT.hs deleted file mode 100644 --- a/src/Data/Syntactic/Sugar/BindingT.hs +++ /dev/null @@ -1,31 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | 'Syntactic' instance for functions --- --- This module is based on having 'BindingT' in the domain. For 'Binding' import module --- "Data.Syntactic.Sugar.Binding" instead - -module Data.Syntactic.Sugar.BindingT where - - - -import Data.Typeable - -import Data.Syntactic -import Data.Syntactic.Functional - - - -instance - ( Syntactic a, Domain a ~ dom - , Syntactic b, Domain b ~ dom - , BindingT :<: dom - , Typeable (Internal a) - ) => - Syntactic (a -> b) - where - type Domain (a -> b) = Domain a - type Internal (a -> b) = Internal a -> Internal b - desugar f = lamT (desugar . f . sugar) - sugar = error "sugar not implemented for (a -> b)" - diff --git a/src/Data/Syntactic/Sugar/Monad.hs b/src/Data/Syntactic/Sugar/Monad.hs deleted file mode 100644 --- a/src/Data/Syntactic/Sugar/Monad.hs +++ /dev/null @@ -1,34 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | 'Syntactic' instance for 'Remon' using 'Binding' to handle variable binding - -module Data.Syntactic.Sugar.Monad where - - - -import Control.Monad.Cont - -import Data.Syntactic -import Data.Syntactic.Functional -import Data.Syntactic.Sugar.Binding - - - --- | One-layer sugaring of monadic actions -sugarMonad :: (Binding :<: sym) => ASTF sym (m a) -> Remon sym m (ASTF sym a) -sugarMonad ma = Remon $ cont $ sugarSym Bind ma - -instance - ( Syntactic a - , Domain a ~ sym - , Binding :<: sym - , MONAD m :<: sym - , Monad m - ) => - Syntactic (Remon sym m a) - where - type Domain (Remon sym m a) = sym - type Internal (Remon sym m a) = m (Internal a) - desugar = desugarMonad . fmap desugar - sugar = fmap sugar . sugarMonad - diff --git a/src/Data/Syntactic/Sugar/MonadT.hs b/src/Data/Syntactic/Sugar/MonadT.hs deleted file mode 100644 --- a/src/Data/Syntactic/Sugar/MonadT.hs +++ /dev/null @@ -1,36 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | 'Syntactic' instance for 'Remon' using 'BindingT' to handle variable binding - -module Data.Syntactic.Sugar.MonadT where - - - -import Control.Monad.Cont -import Data.Typeable - -import Data.Syntactic -import Data.Syntactic.Functional -import Data.Syntactic.Sugar.BindingT - - - --- | One-layer sugaring of monadic actions -sugarMonad :: (BindingT :<: sym, Typeable a) => ASTF sym (m a) -> Remon sym m (ASTF sym a) -sugarMonad ma = Remon $ cont $ sugarSym Bind ma - -instance - ( Syntactic a - , Domain a ~ sym - , BindingT :<: sym - , MONAD m :<: sym - , Monad m - , Typeable (Internal a) - ) => - Syntactic (Remon sym m a) - where - type Domain (Remon sym m a) = sym - type Internal (Remon sym m a) = m (Internal a) - desugar = desugarMonad . fmap desugar - sugar = fmap sugar . sugarMonad - diff --git a/src/Data/Syntactic/Syntax.hs b/src/Data/Syntactic/Syntax.hs deleted file mode 100644 --- a/src/Data/Syntactic/Syntax.hs +++ /dev/null @@ -1,332 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE UndecidableInstances #-} - -#ifndef MIN_VERSION_GLASGOW_HASKELL -#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0 -#endif - -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10 - -#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) -#else -{-# LANGUAGE OverlappingInstances #-} -#endif - --- | Generic representation of typed syntax trees --- --- For details, see: A Generic Abstract Syntax Model for Embedded Languages --- (ICFP 2012, ). - -module Data.Syntactic.Syntax - ( -- * Syntax trees - AST (..) - , ASTF - , Full (..) - , (:->) (..) - , SigRep (..) - , Signature (..) - , DenResult - , Symbol (..) - , size - -- Smart constructors - , SmartFun - , SmartSig - , SmartSym - , smartSym' - -- * Open symbol domains - , (:+:) (..) - , Project (..) - , (:<:) (..) - , smartSym - , Empty - -- * Existential quantification - , E (..) - , liftE - , liftE2 - , EF (..) - , liftEF - , liftEF2 - -- * Type inference - , symType - , prjP - ) where - - - -import Control.DeepSeq -import Data.Typeable -import Data.Foldable (Foldable) -- Needed by GHC < 7.10 -import Data.Proxy -- Needed by GHC < 7.8 -import Data.Traversable (Traversable) -- Needed by GHC < 7.10 - - - - --------------------------------------------------------------------------------- --- * Syntax trees --------------------------------------------------------------------------------- - --- | Generic abstract syntax tree, parameterized by a symbol domain --- --- @(`AST` sym (a `:->` b))@ represents a partially applied (or unapplied) --- symbol, missing at least one argument, while @(`AST` sym (`Full` a))@ --- represents a fully applied symbol, i.e. a complete syntax tree. -data AST sym sig - where - Sym :: sym sig -> AST sym sig - (:$) :: AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig - -infixl 1 :$ - --- | Fully applied abstract syntax tree -type ASTF sym a = AST sym (Full a) - -instance Functor sym => Functor (AST sym) - where - fmap f (Sym s) = Sym (fmap f s) - fmap f (s :$ a) = fmap (fmap f) s :$ a - --- | Signature of a fully applied symbol -newtype Full a = Full { result :: a } - deriving (Eq, Show, Typeable, Functor) - --- | Signature of a partially applied (or unapplied) symbol -newtype a :-> sig = Partial (a -> sig) - deriving (Typeable, Functor) - -infixr :-> - --- | Witness of the arity of a symbol signature -data SigRep sig - where - SigFull :: SigRep (Full a) - SigMore :: SigRep sig -> SigRep (a :-> sig) - --- | Valid symbol signatures -class Signature sig - where - signature :: SigRep sig - -instance Signature (Full a) - where - signature = SigFull - -instance Signature sig => Signature (a :-> sig) - where - signature = SigMore signature - --- | 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 - --- | Valid symbols to use in an 'AST' -class Symbol sym - where - -- | Force a symbol to normal form - rnfSym :: sym sig -> () - rnfSym s = s `seq` () - - -- | Reify the signature of a symbol - symSig :: sym sig -> SigRep sig - -instance Symbol sym => NFData (AST sym sig) - where - rnf (Sym s) = rnfSym s - rnf (s :$ a) = rnf s `seq` rnf a - --- | Count the number of symbols in an 'AST' -size :: AST sym sig -> Int -size (Sym _) = 1 -size (s :$ a) = size s + size a - - - --------------------------------------------------------------------------------- --- * Smart constructors --------------------------------------------------------------------------------- - --- | Maps a symbol signature to the type of the corresponding smart constructor: --- --- > SmartFun sym (a :-> b :-> ... :-> Full x) = ASTF sym a -> ASTF sym b -> ... -> ASTF sym x -type family SmartFun (sym :: * -> *) sig -type instance SmartFun sym (Full a) = ASTF sym a -type instance SmartFun sym (a :-> sig) = ASTF sym a -> SmartFun sym sig - --- | Maps a smart constructor type to the corresponding symbol signature: --- --- > SmartSig (ASTF sym a -> ASTF sym b -> ... -> ASTF sym x) = a :-> b :-> ... :-> Full x -type family SmartSig f -type instance SmartSig (AST sym sig) = sig -type instance SmartSig (ASTF sym a -> f) = a :-> SmartSig f - --- | Returns the symbol in the result of a smart constructor -type family SmartSym f :: * -> * -type instance SmartSym (AST sym sig) = sym -type instance SmartSym (a -> f) = SmartSym f - --- | Make a smart constructor of a symbol. 'smartSym' has any type of the form: --- --- > smartSym --- > :: sym (a :-> b :-> ... :-> Full x) --- > -> (ASTF sym a -> ASTF sym b -> ... -> ASTF sym x) -smartSym' :: forall sig f sym - . ( Signature sig - , f ~ SmartFun sym sig - , sig ~ SmartSig f - , sym ~ SmartSym f - ) - => sym sig -> f -smartSym' s = go (signature :: SigRep sig) (Sym s) - where - go :: forall sig . SigRep sig -> AST sym sig -> SmartFun sym sig - go SigFull s = s - go (SigMore sig) s = \a -> go sig (s :$ a) - - - --------------------------------------------------------------------------------- --- * Open symbol domains --------------------------------------------------------------------------------- - --- | Direct sum of two symbol domains -data (sym1 :+: sym2) sig - where - InjL :: sym1 a -> (sym1 :+: sym2) a - InjR :: sym2 a -> (sym1 :+: sym2) a - deriving (Functor, Foldable, Traversable) - -infixr :+: - -instance (Symbol sym1, Symbol sym2) => Symbol (sym1 :+: sym2) - where - rnfSym (InjL s) = rnfSym s - rnfSym (InjR s) = rnfSym s - symSig (InjL s) = symSig s - symSig (InjR s) = symSig s - --- | Symbol projection --- --- The class is defined for /all pairs of types/, but 'prj' can only succeed if @sup@ is of the form --- @(... `:+:` sub `:+:` ...)@. -class Project sub sup - where - -- | Partial projection from @sup@ to @sub@ - prj :: sup a -> Maybe (sub a) - -instance {-# OVERLAPPING #-} Project sub sup => Project sub (AST sup) - where - prj (Sym s) = prj s - prj _ = Nothing - -instance {-# OVERLAPPING #-} Project sym sym - where - prj = Just - -instance {-# OVERLAPPING #-} Project sym1 (sym1 :+: sym2) - where - prj (InjL a) = Just a - prj _ = Nothing - -instance {-# OVERLAPPING #-} Project sym1 sym3 => Project sym1 (sym2 :+: sym3) - where - prj (InjR a) = prj a - prj _ = Nothing - --- | If @sub@ is not in @sup@, 'prj' always returns 'Nothing'. -instance Project sub sup - where - prj _ = Nothing - --- | Symbol injection --- --- The class includes types @sub@ and @sup@ where @sup@ is of the form @(... `:+:` sub `:+:` ...)@. -class Project sub sup => sub :<: sup - where - -- | Injection from @sub@ to @sup@ - inj :: sub a -> sup a - -instance {-# OVERLAPPING #-} (sub :<: sup) => (sub :<: AST sup) - where - inj = Sym . inj - -instance {-# OVERLAPPING #-} (sym :<: sym) - where - inj = id - -instance {-# OVERLAPPING #-} (sym1 :<: (sym1 :+: sym2)) - where - inj = InjL - -instance {-# OVERLAPPING #-} (sym1 :<: sym3) => (sym1 :<: (sym2 :+: sym3)) - where - inj = InjR . inj - --- The reason for separating the `Project` and `(:<:)` classes is that there are --- types that can be instances of the former but not the latter due to type --- constraints on the `a` type. - --- | Make a smart constructor of a symbol. 'smartSym' has any type of the form: --- --- > smartSym :: (sub :<: AST sup) --- > => sub (a :-> b :-> ... :-> Full x) --- > -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x) -smartSym - :: ( Signature sig - , f ~ SmartFun sup sig - , sig ~ SmartSig f - , sup ~ SmartSym f - , sub :<: sup - ) - => sub sig -> f -smartSym = smartSym' . inj - --- | Empty symbol type --- --- Can be used to make uninhabited 'AST' types. It can also be used as a terminator in co-product --- lists (e.g. to avoid overlapping instances): --- --- > (A :+: B :+: Empty) -data Empty :: * -> * - - - --------------------------------------------------------------------------------- --- * Existential quantification --------------------------------------------------------------------------------- - --- | Existential quantification -data E e - where - E :: e a -> E e - -liftE :: (forall a . e a -> b) -> E e -> b -liftE f (E a) = f a - -liftE2 :: (forall a b . e a -> e b -> c) -> E e -> E e -> c -liftE2 f (E a) (E b) = f a b - --- | Existential quantification of 'Full'-indexed type -data EF e - where - EF :: e (Full a) -> EF e - -liftEF :: (forall a . e (Full a) -> b) -> EF e -> b -liftEF f (EF a) = f a - -liftEF2 :: (forall a b . e (Full a) -> e (Full b) -> c) -> EF e -> EF e -> c -liftEF2 f (EF a) (EF b) = f a b - - - --------------------------------------------------------------------------------- --- * Type inference --------------------------------------------------------------------------------- - --- | Constrain a symbol to a specific type -symType :: Proxy sym -> sym sig -> sym sig -symType _ = id - --- | Projection to a specific symbol type -prjP :: Project sub sup => Proxy sub -> sup sig -> Maybe (sub sig) -prjP _ = prj - diff --git a/src/Data/Syntactic/Traversal.hs b/src/Data/Syntactic/Traversal.hs deleted file mode 100644 --- a/src/Data/Syntactic/Traversal.hs +++ /dev/null @@ -1,202 +0,0 @@ --- | Generic traversals of 'AST' terms - -module Data.Syntactic.Traversal - ( gmapQ - , gmapT - , everywhereUp - , everywhereDown - , universe - , Args (..) - , listArgs - , mapArgs - , mapArgsA - , mapArgsM - , foldrArgs - , appArgs - , listFold - , match - , simpleMatch - , fold - , simpleFold - , matchTrans - , mapAST - , WrapFull (..) - , toTree - ) where - - - -import Control.Applicative -import Data.Tree - -import Data.Syntactic.Syntax - - - --- | Map a function over all immediate sub-terms (corresponds to the function --- with the same name in Scrap Your Boilerplate) -gmapT :: forall sym - . (forall a . ASTF sym a -> ASTF sym a) - -> (forall a . ASTF sym a -> ASTF sym a) -gmapT f a = go a - where - go :: AST sym a -> AST sym 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 sym b - . (forall a . ASTF sym a -> b) - -> (forall a . ASTF sym a -> [b]) -gmapQ f a = go a - where - go :: AST sym a -> [b] - go (s :$ a) = f a : go s - go _ = [] - --- | Apply a transformation bottom-up over an 'AST' (corresponds to @everywhere@ in Scrap Your --- Boilerplate) -everywhereUp - :: (forall a . ASTF sym a -> ASTF sym a) - -> (forall a . ASTF sym a -> ASTF sym a) -everywhereUp f = f . gmapT (everywhereUp f) - --- | Apply a transformation top-down over an 'AST' (corresponds to @everywhere'@ in Scrap Your --- Boilerplate) -everywhereDown - :: (forall a . ASTF sym a -> ASTF sym a) - -> (forall a . ASTF sym a -> ASTF sym a) -everywhereDown f = gmapT (everywhereDown f) . f - --- | List all sub-terms (corresponds to @universe@ in Uniplate) -universe :: ASTF sym a -> [EF (AST sym)] -universe a = EF a : go a - where - go :: AST sym a -> [EF (AST sym)] - go (Sym s) = [] - go (s :$ a) = go s ++ universe a - --- | 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) - --- | Right fold for an 'Args' list -foldrArgs - :: (forall a . c (Full a) -> b -> b) - -> b - -> (forall sig . Args c sig -> b) -foldrArgs f b Nil = b -foldrArgs f b (a :* as) = f a (foldrArgs f b as) - --- | Apply a (partially applied) symbol to a list of argument terms -appArgs :: AST sym sig -> Args (AST sym) sig -> ASTF sym (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 sym a c - . ( forall sig . (a ~ DenResult sig) => - sym sig -> Args (AST sym) sig -> c (Full a) - ) - -> ASTF sym a - -> c (Full a) -match f a = go a Nil - where - go :: (a ~ DenResult sig) => AST sym sig -> Args (AST sym) sig -> c (Full a) - go (Sym a) as = f a as - go (s :$ a) as = go s (a :* as) - --- | A version of 'match' with a simpler result type -simpleMatch :: forall sym a b - . (forall sig . (a ~ DenResult sig) => sym sig -> Args (AST sym) sig -> b) - -> ASTF sym 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 sym c - . (forall sig . sym sig -> Args c sig -> c (Full (DenResult sig))) - -> (forall a . ASTF sym 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 sym b - . (forall sig . sym sig -> Args (Const b) sig -> b) - -> (forall a . ASTF sym 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 sym b - . (forall sig . sym sig -> [b] -> b) - -> (forall a . ASTF sym a -> b) -listFold f = simpleFold (\s -> f s . listArgs getConst) - -newtype WrapAST c sym sig = WrapAST { unWrapAST :: c (AST sym 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 sym sym' c a - . ( forall sig . (a ~ DenResult sig) => - sym sig -> Args (AST sym) sig -> c (ASTF sym' a) - ) - -> ASTF sym a - -> c (ASTF sym' a) -matchTrans f = unWrapAST . match (\s -> WrapAST . f s) - --- | Update the symbols in an AST -mapAST :: (forall sig' . sym1 sig' -> sym2 sig') -> AST sym1 sig -> AST sym2 sig -mapAST f (Sym s) = Sym (f s) -mapAST f (s :$ a) = mapAST f s :$ mapAST f a - --- | 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) - --- | Convert an 'AST' to a 'Tree' -toTree :: forall dom a b . (forall sig . dom sig -> b) -> ASTF dom a -> Tree b -toTree f = listFold (Node . f) - diff --git a/src/Language/Syntactic.hs b/src/Language/Syntactic.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic.hs @@ -0,0 +1,18 @@ +-- | The basic parts of the syntactic library + +module Language.Syntactic + ( module Language.Syntactic.Syntax + , module Language.Syntactic.Traversal + , module Language.Syntactic.Interpretation + , module Language.Syntactic.Sugar + , module Language.Syntactic.Decoration + ) where + + + +import Language.Syntactic.Syntax +import Language.Syntactic.Traversal +import Language.Syntactic.Interpretation +import Language.Syntactic.Sugar +import Language.Syntactic.Decoration + diff --git a/src/Language/Syntactic/Decoration.hs b/src/Language/Syntactic/Decoration.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Decoration.hs @@ -0,0 +1,123 @@ +-- | Construct for decorating symbols or expressions with additional information + +module Language.Syntactic.Decoration where + + + +import Data.Tree (Tree (..)) + +import Data.Tree.View + +import Language.Syntactic.Syntax +import Language.Syntactic.Traversal +import Language.Syntactic.Interpretation + + + +-- | Decorating symbols or expressions with additional information +-- +-- One usage of ':&:' is to decorate every node of a syntax tree. This is done +-- simply by changing +-- +-- > AST sym sig +-- +-- to +-- +-- > AST (sym :&: info) sig +data (expr :&: info) sig + where + (:&:) + :: { decorExpr :: expr sig + , decorInfo :: info (DenResult sig) + } + -> (expr :&: info) sig + +instance Symbol sym => Symbol (sym :&: info) + where + rnfSym = rnfSym . decorExpr + symSig = symSig . decorExpr + +instance Project sub sup => Project sub (sup :&: info) + where + prj = prj . decorExpr + +instance Equality expr => Equality (expr :&: info) + where + equal a b = decorExpr a `equal` decorExpr b + hash = hash . decorExpr + +instance Render expr => Render (expr :&: info) + where + renderSym = renderSym . decorExpr + renderArgs args = renderArgs args . decorExpr + +instance StringTree expr => StringTree (expr :&: info) + where + stringTreeSym args = stringTreeSym args . decorExpr + + + +-- | Map over a decoration +mapDecor + :: (sym1 sig -> sym2 sig) + -> (info1 (DenResult sig) -> info2 (DenResult sig)) + -> ((sym1 :&: info1) sig -> (sym2 :&: info2) sig) +mapDecor fs fi (s :&: i) = fs s :&: fi i + +-- | Get the decoration of the top-level node +getDecor :: AST (sym :&: info) sig -> info (DenResult sig) +getDecor (Sym (_ :&: info)) = info +getDecor (f :$ _) = getDecor f + +-- | Update the decoration of the top-level node +updateDecor :: forall info sym a . + (info a -> info a) -> ASTF (sym :&: info) a -> ASTF (sym :&: info) a +updateDecor f = match update + where + update + :: (a ~ DenResult sig) + => (sym :&: info) sig + -> Args (AST (sym :&: info)) sig + -> ASTF (sym :&: info) a + update (a :&: info) args = appArgs (Sym sym) args + where + sym = a :&: (f info) + +-- | Lift a function that operates on expressions with associated information to +-- operate on a ':&:' expression. This function is convenient to use together +-- with e.g. 'queryNodeSimple' when the domain has the form @(sym `:&:` info)@. +liftDecor :: (expr s -> info (DenResult s) -> b) -> ((expr :&: info) s -> b) +liftDecor f (a :&: info) = f a info + +-- | Strip decorations from an 'AST' +stripDecor :: AST (sym :&: info) sig -> AST sym sig +stripDecor (Sym (a :&: _)) = Sym a +stripDecor (f :$ a) = stripDecor f :$ stripDecor a + +-- | Rendering of decorated syntax trees +stringTreeDecor :: forall info sym a . StringTree sym => + (forall a . info a -> String) -> ASTF (sym :&: info) a -> Tree String +stringTreeDecor showInfo a = mkTree [] a + where + mkTree :: [Tree String] -> AST (sym :&: info) sig -> Tree String + mkTree args (Sym (expr :&: info)) = Node infoStr [stringTreeSym args expr] + where + infoStr = "<<" ++ showInfo info ++ ">>" + mkTree args (f :$ a) = mkTree (mkTree [] a : args) f + +-- | Show an decorated syntax tree using ASCII art +showDecorWith :: StringTree sym => (forall a . info a -> String) -> ASTF (sym :&: info) a -> String +showDecorWith showInfo = showTree . stringTreeDecor showInfo + +-- | Print an decorated syntax tree using ASCII art +drawDecorWith :: StringTree sym => (forall a . info a -> String) -> ASTF (sym :&: info) a -> IO () +drawDecorWith showInfo = putStrLn . showDecorWith showInfo + +writeHtmlDecorWith :: forall info sym a. (StringTree sym) + => (forall b. info b -> String) -> FilePath -> ASTF (sym :&: info) a -> IO () +writeHtmlDecorWith showInfo file a = writeHtmlTree file $ mkTree [] a + where + mkTree :: [Tree NodeInfo] -> AST (sym :&: info) sig -> Tree NodeInfo + mkTree args (f :$ a) = mkTree (mkTree [] a : args) f + mkTree args (Sym (expr :&: info)) = Node (NodeInfo (renderSym expr) (showInfo info)) args + diff --git a/src/Language/Syntactic/Functional.hs b/src/Language/Syntactic/Functional.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Functional.hs @@ -0,0 +1,646 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} + +#ifndef MIN_VERSION_GLASGOW_HASKELL +#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0 +#endif + -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10 + +#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) +#else +{-# LANGUAGE OverlappingInstances #-} +#endif + +#if __GLASGOW_HASKELL__ < 708 +#define TYPEABLE Typeable1 +#else +#define TYPEABLE Typeable +#endif + +-- | Basics for implementing functional EDSLs + +module Language.Syntactic.Functional + ( -- * Syntactic constructs + Name (..) + , Construct (..) + , Binding (..) + , maxLam + , lam + , fromDeBruijn + , BindingT (..) + , maxLamT + , lamT + , BindingDomain (..) + , Let (..) + , MONAD (..) + , Remon (..) + , desugarMonad + , desugarMonadT + -- * Free and bound variables + , freeVars + , allVars + -- * Alpha-equivalence + , AlphaEnv + , alphaEq' + , alphaEq + -- * Evaluation + , Denotation + , Eval (..) + , evalDen + , DenotationM + , liftDenotationM + , RunEnv + , EvalEnv (..) + , compileSymDefault + , evalOpen + , evalClosed + ) where + + + +#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) +#else +import Control.Applicative +#endif +import Control.DeepSeq +import Control.Monad.Cont +import Control.Monad.Reader +import Data.Dynamic +import Data.List (genericIndex) +#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) +#else +import Data.Proxy -- Needed by GHC < 7.8 +#endif +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Tree + +import Data.Hash (hashInt) + +import Language.Syntactic + + + +---------------------------------------------------------------------------------------------------- +-- * Syntactic constructs +---------------------------------------------------------------------------------------------------- + +-- | Generic N-ary syntactic construct +-- +-- 'Construct' gives a quick way to introduce a syntactic construct by giving its name and semantic +-- function. +data Construct sig + where + Construct :: Signature sig => String -> Denotation sig -> Construct sig + +instance Symbol Construct + where + rnfSym (Construct name den) = rnf name `seq` den `seq` () + symSig (Construct _ _) = signature + +instance Render Construct + where + renderSym (Construct name _) = name + renderArgs = renderArgsSmart + +instance Equality Construct + where + equal = equalDefault + hash = hashDefault + +instance StringTree Construct + +-- | Variable name +newtype Name = Name Integer + deriving (Eq, Ord, Num, Enum, Real, Integral, NFData) + +instance Show Name + where + show (Name n) = show n + +-- | Variables and binders +data Binding sig + where + Var :: Name -> Binding (Full a) + Lam :: Name -> Binding (b :-> Full (a -> b)) + +instance Symbol Binding + where + rnfSym (Var v) = rnf v + rnfSym (Lam v) = rnf v + symSig (Var _) = signature + symSig (Lam _) = signature + +-- | 'equal' does strict identifier comparison; i.e. no alpha equivalence. +-- +-- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation +-- that enables the following property: +-- +-- @`alphaEq` a b ==> `hash` a == `hash` b@ +instance Equality Binding + where + equal (Var v1) (Var v2) = v1==v2 + equal (Lam v1) (Lam v2) = v1==v2 + equal _ _ = False + + hash (Var _) = hashInt 0 + hash (Lam _) = hashInt 0 + +instance Render Binding + where + renderSym (Var v) = 'v' : show v + renderSym (Lam v) = "Lam v" ++ show v + renderArgs [] (Var v) = 'v' : show v + renderArgs [body] (Lam v) = "(\\" ++ ('v':show v) ++ " -> " ++ body ++ ")" + +instance StringTree Binding + where + stringTreeSym [] (Var v) = Node ('v' : show v) [] + stringTreeSym [body] (Lam v) = Node ("Lam " ++ 'v' : show v) [body] + +-- | Get the highest name bound by the first 'Lam' binders at every path from the root. If the term +-- has /ordered binders/ \[1\], 'maxLam' returns the highest name introduced in the whole term. +-- +-- \[1\] Ordered binders means that the names of 'Lam' nodes are decreasing along every path from +-- the root. +maxLam :: (Binding :<: s) => AST s a -> Name +maxLam (Sym lam :$ _) | Just (Lam v) <- prj lam = v +maxLam (s :$ a) = maxLam s `Prelude.max` maxLam a +maxLam _ = 0 + +-- | Higher-order interface for variable binding +-- +-- Assumptions: +-- +-- * The body @f@ does not inspect its argument. +-- +-- * Applying @f@ to a term with ordered binders results in a term with /ordered binders/ \[1\]. +-- +-- \[1\] Ordered binders means that the names of 'Lam' nodes are decreasing along every path from +-- the root. +-- +-- See \"Using Circular Programs for Higher-Order Syntax\" +-- (ICFP 2013, ). +lam :: (Binding :<: s) => (ASTF s a -> ASTF s b) -> ASTF s (a -> b) +lam f = smartSym (Lam v) body + where + body = f (smartSym (Var v)) + v = succ $ maxLam body + +-- | Convert from a term with De Bruijn indexes to one with explicit names +-- +-- In the argument term, variable 'Name's are treated as De Bruijn indexes, and lambda 'Name's are +-- ignored. (Ideally, one should use a different type for De Bruijn terms.) +fromDeBruijn :: (Binding :<: sym) => ASTF sym a -> ASTF sym a +fromDeBruijn = go [] + where + go :: (Binding :<: sym) => [Name] -> ASTF sym a -> (ASTF sym a) + go vs var | Just (Var i) <- prj var = inj $ Var $ genericIndex vs i + go vs (lam :$ body) | Just (Lam _) <- prj lam = inj (Lam v) :$ body' + where + body' = go (v:vs) body + v = succ $ maxLam body' + -- Same trick as in `lam` + go vs a = gmapT (go vs) a + +-- | Typed variables and binders +data BindingT sig + where + VarT :: Typeable a => Name -> BindingT (Full a) + LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b)) + +instance Symbol BindingT + where + rnfSym (VarT v) = rnf v + rnfSym (LamT v) = rnf v + symSig (VarT _) = signature + symSig (LamT _) = signature + +-- | 'equal' does strict identifier comparison; i.e. no alpha equivalence. +-- +-- 'hash' assigns the same hash to all variables and binders. This is a valid over-approximation +-- that enables the following property: +-- +-- @`alphaEq` a b ==> `hash` a == `hash` b@ +instance Equality BindingT + where + equal (VarT v1) (VarT v2) = v1==v2 + equal (LamT v1) (LamT v2) = v1==v2 + equal _ _ = False + + hash (VarT _) = hashInt 0 + hash (LamT _) = hashInt 0 + +instance Render BindingT + where + renderSym (VarT v) = renderSym (Var v) + renderSym (LamT v) = renderSym (Lam v) + renderArgs args (VarT v) = renderArgs args (Var v) + renderArgs args (LamT v) = renderArgs args (Lam v) + +instance StringTree BindingT + where + stringTreeSym args (VarT v) = stringTreeSym args (Var v) + stringTreeSym args (LamT v) = stringTreeSym args (Lam v) + +-- | Get the highest name bound by the first 'LamT' binders at every path from the root. If the term +-- has /ordered binders/ \[1\], 'maxLamT' returns the highest name introduced in the whole term. +-- +-- \[1\] Ordered binders means that the names of 'LamT' nodes are decreasing along every path from +-- the root. +maxLamT :: Project BindingT sym => AST sym a -> Name +maxLamT (Sym lam :$ _) | Just (LamT n :: BindingT (b :-> a)) <- prj lam = n +maxLamT (s :$ a) = maxLamT s `Prelude.max` maxLamT a +maxLamT _ = 0 + +-- | Higher-order interface for typed variable binding +-- +-- Assumptions: +-- +-- * The body @f@ does not inspect its argument. +-- +-- * Applying @f@ to a term with ordered binders results in a term with /ordered binders/ \[1\]. +-- +-- \[1\] Ordered binders means that the names of 'LamT' nodes are decreasing along every path from +-- the root. +-- +-- See \"Using Circular Programs for Higher-Order Syntax\" +-- (ICFP 2013, ). +lamT :: forall sym symT a b + . ( BindingT :<: sym + , symT ~ Typed sym + , Typeable a + , Typeable b + ) + => (ASTF symT a -> ASTF symT b) -> ASTF symT (a -> b) +lamT f = smartSymT (LamT v) body + where + body = f (smartSymT (VarT v)) + v = succ $ maxLamT body + +-- | Domains that \"might\" include variables and binders +class BindingDomain sym + where + prVar :: sym sig -> Maybe Name + prLam :: sym sig -> Maybe Name + -- It is in principle possible to replace a constraint `BindingDomain s` by + -- `(Project Binding s, Project BindingT s)`. However, the problem is that one then has to + -- specify the type `t` through a `Proxy`. The `BindingDomain` class gets around this problem. + +instance {-# OVERLAPPING #-} + (BindingDomain sym1, BindingDomain sym2) => BindingDomain (sym1 :+: sym2) + where + prVar (InjL s) = prVar s + prVar (InjR s) = prVar s + prLam (InjL s) = prLam s + prLam (InjR s) = prLam s + +instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (Typed sym) + where + prVar (Typed s) = prVar s + prLam (Typed s) = prLam s + +instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (sym :&: i) + where + prVar = prVar . decorExpr + prLam = prLam . decorExpr + +instance {-# OVERLAPPING #-} BindingDomain sym => BindingDomain (AST sym) + where + prVar (Sym s) = prVar s + prVar _ = Nothing + prLam (Sym s) = prLam s + prLam _ = Nothing + +instance {-# OVERLAPPING #-} BindingDomain Binding + where + prVar (Var v) = Just v + prVar _ = Nothing + prLam (Lam v) = Just v + prLam _ = Nothing + +instance {-# OVERLAPPING #-} BindingDomain BindingT + where + prVar (VarT v) = Just v + prVar _ = Nothing + prLam (LamT v) = Just v + prLam _ = Nothing + +instance {-# OVERLAPPING #-} BindingDomain sym + where + prVar _ = Nothing + prLam _ = Nothing + +-- | A symbol for let bindings +-- +-- This symbol is just an application operator. The actual binding has to be +-- done by a lambda that constructs the second argument. +data Let sig + where + Let :: Let (a :-> (a -> b) :-> Full b) + +instance Symbol Let where symSig Let = signature +instance Render Let where renderSym Let = "letBind" +instance Eval Let where evalSym Let = flip ($) +instance EvalEnv Let env + +instance Equality Let + where + equal = equalDefault + hash = hashDefault + +instance StringTree Let + where + stringTreeSym [a, Node lam [body]] Let + | ("Lam",v) <- splitAt 3 lam = Node ("Let" ++ v) [a,body] + stringTreeSym [a,f] Let = Node "Let" [a,f] + +-- | Monadic constructs +-- +-- See \"Generic Monadic Constructs for Embedded Languages\" (Persson et al., IFL 2011 +-- ). +data MONAD m sig + where + Return :: MONAD m (a :-> Full (m a)) + Bind :: MONAD m (m a :-> (a -> m b) :-> Full (m b)) + +instance Symbol (MONAD m) + where + symSig Return = signature + symSig Bind = signature + +instance Render (MONAD m) + where + renderSym Return = "return" + renderSym Bind = "(>>=)" + renderArgs = renderArgsSmart + +instance Equality (MONAD m) + where + equal = equalDefault + hash = hashDefault + +instance StringTree (MONAD m) + +-- | Reifiable monad +-- +-- See \"Generic Monadic Constructs for Embedded Languages\" (Persson et al., +-- IFL 2011 ). +-- +-- It is advised to convert to/from 'Remon' using the 'Syntactic' instance +-- provided in the modules "Language.Syntactic.Sugar.Monad" or +-- "Language.Syntactic.Sugar.MonadT". +newtype Remon sym m a + where + Remon + :: { unRemon :: forall r . Typeable r => Cont (ASTF sym (m r)) a } + -> Remon sym m a + deriving (Functor) + -- The `Typeable` constraint is a bit unfortunate. It's only needed when using + -- a `Typed` domain. Since this is probably the most common case I decided to + -- bake in `Typeable` here. A more flexible solution would be to parameterize + -- `Remon` on the constraint. + +instance Applicative (Remon sym m) + where + pure a = Remon $ pure a + f <*> a = Remon $ unRemon f <*> unRemon a + +instance Monad (Remon dom m) + where + return a = Remon $ return a + ma >>= f = Remon $ unRemon ma >>= unRemon . f + +-- | One-layer desugaring of monadic actions +desugarMonad + :: ( MONAD m :<: sym + , Typeable a + , TYPEABLE m + ) + => Remon sym m (ASTF sym a) -> ASTF sym (m a) +desugarMonad = flip runCont (sugarSym Return) . unRemon + +-- | One-layer desugaring of monadic actions +desugarMonadT + :: ( MONAD m :<: sym + , symT ~ Typed sym + , Typeable a + , TYPEABLE m + ) + => Remon symT m (ASTF symT a) -> ASTF symT (m a) +desugarMonadT = flip runCont (sugarSymT Return) . unRemon + + + +---------------------------------------------------------------------------------------------------- +-- * Free variables +---------------------------------------------------------------------------------------------------- + +-- | Get the set of free variables in an expression +freeVars :: BindingDomain sym => AST sym sig -> Set Name +freeVars var + | Just v <- prVar var = Set.singleton v +freeVars (lam :$ body) + | Just v <- prLam lam = Set.delete v (freeVars body) +freeVars (s :$ a) = Set.union (freeVars s) (freeVars a) +freeVars _ = Set.empty + +-- | Get the set of variables (free, bound and introduced by lambdas) in an +-- expression +allVars :: BindingDomain sym => AST sym sig -> Set Name +allVars var + | Just v <- prVar var = Set.singleton v +allVars (lam :$ body) + | Just v <- prLam lam = Set.insert v (allVars body) +allVars (s :$ a) = Set.union (allVars s) (allVars a) +allVars _ = Set.empty + + + +---------------------------------------------------------------------------------------------------- +-- * Alpha-equivalence +---------------------------------------------------------------------------------------------------- + +-- | Environment used by 'alphaEq'' +type AlphaEnv = [(Name,Name)] + +alphaEq' :: (Equality sym, BindingDomain sym) => AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool +alphaEq' env var1 var2 + | Just v1 <- prVar var1 + , Just v2 <- prVar var2 + = case (lookup v1 env, lookup v2 env') of + (Nothing, Nothing) -> v1==v2 -- Free variables + (Just v2', Just v1') -> v1==v1' && v2==v2' + _ -> False + where + env' = [(v2,v1) | (v1,v2) <- env] +alphaEq' env (lam1 :$ body1) (lam2 :$ body2) + | Just v1 <- prLam lam1 + , Just v2 <- prLam lam2 + = alphaEq' ((v1,v2):env) body1 body2 +alphaEq' env a b = simpleMatch (alphaEq'' env b) a + +alphaEq'' :: (Equality sym, BindingDomain sym) => + AlphaEnv -> ASTF sym b -> sym a -> Args (AST sym) a -> Bool +alphaEq'' env b a aArgs = simpleMatch (alphaEq''' env a aArgs) b + +alphaEq''' :: (Equality sym, BindingDomain sym) => + AlphaEnv -> sym a -> Args (AST sym) a -> sym b -> Args (AST sym) b -> Bool +alphaEq''' env a aArgs b bArgs + | equal a b = alphaEqChildren env a' b' + | otherwise = False + where + a' = appArgs (Sym undefined) aArgs + b' = appArgs (Sym undefined) bArgs + +alphaEqChildren :: (Equality sym, BindingDomain sym) => AlphaEnv -> AST sym a -> AST sym b -> Bool +alphaEqChildren _ (Sym _) (Sym _) = True +alphaEqChildren env (s :$ a) (t :$ b) = alphaEqChildren env s t && alphaEq' env a b +alphaEqChildren _ _ _ = False + +-- | Alpha-equivalence +alphaEq :: (Equality sym, BindingDomain sym) => ASTF sym a -> ASTF sym b -> Bool +alphaEq = alphaEq' [] + + + +---------------------------------------------------------------------------------------------------- +-- * Evaluation +---------------------------------------------------------------------------------------------------- + +-- | Semantic function type of the given symbol signature +type family Denotation sig +type instance Denotation (Full a) = a +type instance Denotation (a :-> sig) = a -> Denotation sig + +class Eval s + where + evalSym :: s sig -> Denotation sig + +instance (Eval s, Eval t) => Eval (s :+: t) + where + evalSym (InjL s) = evalSym s + evalSym (InjR s) = evalSym s + +instance Eval Empty + where + evalSym = error "evalSym: Empty" + +instance Eval sym => Eval (sym :&: info) + where + evalSym = evalSym . decorExpr + +instance Eval Construct + where + evalSym (Construct _ d) = d + +instance Monad m => Eval (MONAD m) + where + evalSym Return = return + evalSym Bind = (>>=) + +-- | Evaluation +evalDen :: Eval s => AST s sig -> Denotation sig +evalDen = go + where + go :: Eval s => AST s sig -> Denotation sig + go (Sym s) = evalSym s + go (s :$ a) = go s $ go a + +-- | Monadic denotation; mapping from a symbol signature +-- +-- > a :-> b :-> Full c +-- +-- to +-- +-- > m a -> m b -> m c +type family DenotationM (m :: * -> *) sig +type instance DenotationM m (Full a) = m a +type instance DenotationM m (a :-> sig) = m a -> DenotationM m sig + +-- | Lift a 'Denotation' to 'DenotationM' +liftDenotationM :: forall m sig proxy1 proxy2 . Monad m => + SigRep sig -> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig +liftDenotationM sig _ _ = help2 sig . help1 sig + where + help1 :: Monad m => + SigRep sig' -> Denotation sig' -> Args (WrapFull m) sig' -> m (DenResult sig') + help1 SigFull f _ = return f + help1 (SigMore sig) f (WrapFull ma :* as) = do + a <- ma + help1 sig (f a) as + + help2 :: SigRep sig' -> (Args (WrapFull m) sig' -> m (DenResult sig')) -> DenotationM m sig' + help2 SigFull f = f Nil + help2 (SigMore sig) f = \a -> help2 sig (\as -> f (WrapFull a :* as)) + +-- | Runtime environment +type RunEnv = [(Name, Dynamic)] + -- TODO Use a more efficient data structure? + +-- | Evaluation +class EvalEnv sym env + where + default compileSym :: (Symbol sym, Eval sym) => + proxy env -> sym sig -> DenotationM (Reader env) sig + + compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig + compileSym p s = compileSymDefault (symSig s) p s + +-- | Simple implementation of `compileSym` from a 'Denotation' +compileSymDefault :: forall proxy env sym sig . Eval sym => + SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig +compileSymDefault sig p s = liftDenotationM sig (Proxy :: Proxy (Reader env)) s (evalSym s) + +instance (EvalEnv sym1 env, EvalEnv sym2 env) => EvalEnv (sym1 :+: sym2) env + where + compileSym p (InjL s) = compileSym p s + compileSym p (InjR s) = compileSym p s + +instance EvalEnv Empty env + where + compileSym = error "compileSym: Empty" + +instance EvalEnv sym env => EvalEnv (Typed sym) env + where + compileSym p (Typed s) = compileSym p s + +instance EvalEnv sym env => EvalEnv (sym :&: info) env + where + compileSym p = compileSym p . decorExpr + +instance EvalEnv Construct env + where + compileSym _ s@(Construct _ d) = liftDenotationM signature p s d + where + p = Proxy :: Proxy (Reader env) + +instance Monad m => EvalEnv (MONAD m) env + +instance EvalEnv BindingT RunEnv + where + compileSym _ (VarT v) = reader $ \env -> + case lookup v env of + Nothing -> error $ "compileSym: Variable " ++ show v ++ " not in scope" + Just d -> case fromDynamic d of + Nothing -> error "compileSym: type error" -- TODO Print types + Just a -> a + compileSym _ (LamT v) = \body -> reader $ \env a -> runReader body ((v, toDyn a) : env) + +-- | \"Compile\" a term to a Haskell function +compile :: EvalEnv sym env => proxy env -> AST sym sig -> DenotationM (Reader env) sig +compile p (Sym s) = compileSym p s +compile p (s :$ a) = compile p s $ compile p a + -- This use of the term \"compile\" comes from \"Typing Dynamic Typing\" (Baars and Swierstra, + -- ICFP 2002, ) + +-- | Evaluation of open terms +evalOpen :: EvalEnv sym env => env -> ASTF sym a -> a +evalOpen env a = runReader (compile Proxy a) env + +-- | Evaluation of closed terms where 'RunEnv' is used as the internal environment +-- +-- (Note that there is no guarantee that the term is actually closed.) +evalClosed :: EvalEnv sym RunEnv => ASTF sym a -> a +evalClosed a = runReader (compile (Proxy :: Proxy RunEnv) a) [] + diff --git a/src/Language/Syntactic/Functional/Sharing.hs b/src/Language/Syntactic/Functional/Sharing.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Functional/Sharing.hs @@ -0,0 +1,259 @@ +{-# LANGUAGE RecordWildCards #-} + +-- | Simple code motion transformation performing common sub-expression +-- elimination and variable hoisting. Note that the implementation is very +-- inefficient. +-- +-- The code is based on an implementation by Gergely Dévai. + +module Language.Syntactic.Functional.Sharing + ( -- * Interface + InjDict (..) + , CodeMotionInterface (..) + , defaultInterface + , defaultInterfaceT + -- * Code motion + , codeMotion + ) where + + + +import Control.Monad.State +import Data.Maybe (isNothing) +import Data.Set (Set) +import qualified Data.Set as Set + +import Language.Syntactic +import Language.Syntactic.Functional + + + +-------------------------------------------------------------------------------- +-- * Interface +-------------------------------------------------------------------------------- + +-- | Interface for injecting binding constructs +data InjDict sym a b = InjDict + { injVariable :: Name -> sym (Full a) + -- ^ Inject a variable + , injLambda :: Name -> sym (b :-> Full (a -> b)) + -- ^ Inject a lambda + , injLet :: sym (a :-> (a -> b) :-> Full b) + -- ^ Inject a "let" symbol + } + +-- | Code motion interface +data CodeMotionInterface sym = Interface + { mkInjDict :: forall a b . ASTF sym a -> ASTF sym b -> Maybe (InjDict sym a b) + -- ^ Try to construct an 'InjDict'. The first argument is the expression + -- to be shared, and the second argument the expression in which it will + -- be shared. This function can be used to transfer information (e.g. + -- from static analysis) from the shared expression to the introduced + -- variable. + , castExprCM :: forall a b . ASTF sym a -> ASTF sym b -> Maybe (ASTF sym b) + -- ^ Try to type cast an expression. The first argument is the + -- expression to cast. The second argument can be used to construct a + -- witness to support the casting. The resulting expression (if any) + -- should be equal to the first argument. + , hoistOver :: forall c. ASTF sym c -> Bool + -- ^ Whether a sub-expression can be hoisted over the given expression + } + +-- | Default 'CodeMotionInterface' for domains of the form +-- @`Typed` (... `:+:` `Binding` `:+:` ...)@. +defaultInterface :: forall sym symT + . ( Binding :<: sym + , Let :<: sym + , symT ~ Typed sym + ) + => (forall a b . ASTF symT a -> ASTF symT b -> Bool) + -- ^ Can the expression represented by the first argument be shared in + -- the second argument? + -> (forall a . ASTF symT a -> Bool) -- ^ Can we hoist over this expression? + -> CodeMotionInterface symT +defaultInterface sharable hoistOver = Interface {..} + where + mkInjDict :: ASTF symT a -> ASTF symT b -> Maybe (InjDict symT a b) + mkInjDict a b | not (sharable a b) = Nothing + mkInjDict a b = + simpleMatch + (\(Typed _) _ -> simpleMatch + (\(Typed _) _ -> + let injVariable = Typed . inj . Var + injLambda = Typed . inj . Lam + injLet = Typed $ inj Let + in Just InjDict {..} + ) b + ) a + + castExprCM = castExpr + +-- | Default 'CodeMotionInterface' for domains of the form +-- @`Typed` (... `:+:` `BindingT` `:+:` ...)@. +defaultInterfaceT :: forall sym symT + . ( BindingT :<: sym + , Let :<: sym + , symT ~ Typed sym + ) + => (forall a b . ASTF symT a -> ASTF symT b -> Bool) + -- ^ Can the expression represented by the first argument be shared in + -- the second argument? + -> (forall a . ASTF symT a -> Bool) -- ^ Can we hoist over this expression? + -> CodeMotionInterface symT +defaultInterfaceT sharable hoistOver = Interface {..} + where + mkInjDict :: ASTF symT a -> ASTF symT b -> Maybe (InjDict symT a b) + mkInjDict a b | not (sharable a b) = Nothing + mkInjDict a b = + simpleMatch + (\(Typed _) _ -> simpleMatch + (\(Typed _) _ -> + let injVariable = Typed . inj . VarT + injLambda = Typed . inj . LamT + injLet = Typed $ inj Let + in Just InjDict {..} + ) b + ) a + + castExprCM = castExpr + + + +-------------------------------------------------------------------------------- +-- * Code motion +-------------------------------------------------------------------------------- + +-- | Substituting a sub-expression. Assumes no variable capturing in the +-- expressions involved. +substitute :: forall sym a b + . (Equality sym, BindingDomain sym) + => CodeMotionInterface sym + -> ASTF sym a -- ^ Sub-expression to be replaced + -> ASTF sym a -- ^ Replacing sub-expression + -> ASTF sym b -- ^ Whole expression + -> ASTF sym b +substitute iface x y a + | Just y' <- castExprCM iface y a, alphaEq x a = y' + | otherwise = subst a + where + subst :: AST sym c -> AST sym c + subst (f :$ a) = subst f :$ substitute iface x y a + subst a = a + -- Note: Since `codeMotion` only uses `substitute` to replace sub-expressions + -- with fresh variables, there's no risk of capturing. + +-- | Count the number of occurrences of a sub-expression +count :: forall sym a b + . (Equality sym, BindingDomain sym) + => ASTF sym a -- ^ Expression to count + -> ASTF sym b -- ^ Expression to count in + -> Int +count a b + | alphaEq a b = 1 + | otherwise = cnt b + where + cnt :: AST sym c -> Int + cnt (f :$ b) = cnt f + count a b + cnt _ = 0 + +-- | Environment for the expression in the 'choose' function +data Env sym = Env + { inLambda :: Bool -- ^ Whether the current expression is inside a lambda + , counter :: EF (AST sym) -> Int + -- ^ Counting the number of occurrences of an expression in the + -- environment + , dependencies :: Set Name + -- ^ The set of variables that are not allowed to occur in the chosen + -- expression + } + +-- | Checks whether a sub-expression in a given environment can be lifted out +liftable :: BindingDomain sym => Env sym -> ASTF sym a -> Bool +liftable env a = independent && isNothing (prVar a) && heuristic + -- Lifting dependent expressions is semantically incorrect. Lifting + -- variables would cause `codeMotion` to loop. + where + independent = Set.null $ Set.intersection (freeVars a) (dependencies env) + heuristic = inLambda env || (counter env (EF a) > 1) + +-- | A sub-expression chosen to be shared together with an evidence that it can +-- actually be shared in the whole expression under consideration +data Chosen sym a + where + Chosen :: InjDict sym b a -> ASTF sym b -> Chosen sym a + +-- | Choose a sub-expression to share +choose :: forall sym a + . (Equality sym, BindingDomain sym) + => CodeMotionInterface sym + -> ASTF sym a + -> Maybe (Chosen sym a) +choose iface a = chooseEnvSub initEnv a + where + initEnv = Env + { inLambda = False + , counter = \(EF b) -> count b a + , dependencies = Set.empty + } + + chooseEnv :: Env sym -> ASTF sym b -> Maybe (Chosen sym a) + chooseEnv env b + | liftable env b + , Just id <- mkInjDict iface b a + = Just $ Chosen id b + chooseEnv env b + | hoistOver iface b = chooseEnvSub env b + | otherwise = Nothing + + -- | Like 'chooseEnv', but does not consider the top expression for sharing + chooseEnvSub :: Env sym -> AST sym b -> Maybe (Chosen sym a) + chooseEnvSub env (Sym lam :$ b) + | Just v <- prLam lam + = chooseEnv (env' v) b + where + env' v = env + { inLambda = True + , dependencies = Set.insert v (dependencies env) + } + chooseEnvSub env (s :$ b) = chooseEnvSub env s `mplus` chooseEnv env b + chooseEnvSub _ _ = Nothing + +codeMotionM :: forall sym m a + . ( Equality sym + , BindingDomain sym + , MonadState Name m + ) + => CodeMotionInterface sym + -> ASTF sym a + -> m (ASTF sym a) +codeMotionM iface a + | Just (Chosen id b) <- choose iface a = share id b + | otherwise = descend a + where + share :: InjDict sym b a -> ASTF sym b -> m (ASTF sym a) + share id b = do + b' <- codeMotionM iface b + v <- get; put (v+1) + let x = Sym (injVariable id v) + body <- codeMotionM iface $ substitute iface b x a + return + $ Sym (injLet id) + :$ b' + :$ (Sym (injLambda id v) :$ body) + + descend :: AST sym b -> m (AST sym b) + descend (f :$ a) = liftM2 (:$) (descend f) (codeMotionM iface a) + descend a = return a + +-- | Perform common sub-expression elimination and variable hoisting +codeMotion :: forall sym m a + . ( Equality sym + , BindingDomain sym + ) + => CodeMotionInterface sym + -> ASTF sym a + -> ASTF sym a +codeMotion iface a = flip evalState maxVar $ codeMotionM iface a + where + maxVar = succ $ Set.findMax $ allVars a + diff --git a/src/Language/Syntactic/Functional/Tuple.hs b/src/Language/Syntactic/Functional/Tuple.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Functional/Tuple.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE TemplateHaskell #-} + +-- | Construction and elimination of tuples + +module Language.Syntactic.Functional.Tuple where + + + +import Language.Syntactic +import Language.Syntactic.Functional + + + +-------------------------------------------------------------------------------- +-- * Generic tuple projection +-------------------------------------------------------------------------------- + +class Select1 tup + where + type Sel1 tup + select1 :: tup -> Sel1 tup + +class Select2 tup + where + type Sel2 tup + select2 :: tup -> Sel2 tup + +class Select3 tup + where + type Sel3 tup + select3 :: tup -> Sel3 tup + +class Select4 tup + where + type Sel4 tup + select4 :: tup -> Sel4 tup + +instance Select1 (a,b) + where + type Sel1 (a,b) = a + select1 (a,b) = a + +instance Select2 (a,b) + where + type Sel2 (a,b) = b + select2 (a,b) = b + +instance Select1 (a,b,c) + where + type Sel1 (a,b,c) = a + select1 (a,b,c) = a + +instance Select2 (a,b,c) + where + type Sel2 (a,b,c) = b + select2 (a,b,c) = b + +instance Select3 (a,b,c) + where + type Sel3 (a,b,c) = c + select3 (a,b,c) = c + +instance Select1 (a,b,c,d) + where + type Sel1 (a,b,c,d) = a + select1 (a,b,c,d) = a + +instance Select2 (a,b,c,d) + where + type Sel2 (a,b,c,d) = b + select2 (a,b,c,d) = b + +instance Select3 (a,b,c,d) + where + type Sel3 (a,b,c,d) = c + select3 (a,b,c,d) = c + +instance Select4 (a,b,c,d) + where + type Sel4 (a,b,c,d) = d + select4 (a,b,c,d) = d + + + +-------------------------------------------------------------------------------- +-- * Symbols +-------------------------------------------------------------------------------- + +-- | Construction and elimination of tuples +data Tuple sig + where + Tup2 :: Tuple (a :-> b :-> Full (a,b)) + Tup3 :: Tuple (a :-> b :-> c :-> Full (a,b,c)) + Tup4 :: Tuple (a :-> b :-> c :-> d :-> Full (a,b,c,d)) + Sel1 :: Select1 tup => Tuple (tup :-> Full (Sel1 tup)) + Sel2 :: Select2 tup => Tuple (tup :-> Full (Sel2 tup)) + Sel3 :: Select3 tup => Tuple (tup :-> Full (Sel3 tup)) + Sel4 :: Select4 tup => Tuple (tup :-> Full (Sel4 tup)) + +instance Symbol Tuple + where + symSig Tup2 = signature + symSig Tup3 = signature + symSig Tup4 = signature + symSig Sel1 = signature + symSig Sel2 = signature + symSig Sel3 = signature + symSig Sel4 = signature + +instance Render Tuple + where + renderSym Tup2 = "tup2" + renderSym Tup3 = "tup3" + renderSym Tup4 = "tup4" + renderSym Sel1 = "sel1" + renderSym Sel2 = "sel2" + renderSym Sel3 = "sel3" + renderSym Sel4 = "sel4" + renderArgs = renderArgsSmart + +interpretationInstances ''Tuple + +instance Eval Tuple + where + evalSym Tup2 = (,) + evalSym Tup3 = (,,) + evalSym Tup4 = (,,,) + evalSym Sel1 = select1 + evalSym Sel2 = select2 + evalSym Sel3 = select3 + evalSym Sel4 = select4 + +instance EvalEnv Tuple env + diff --git a/src/Language/Syntactic/Functional/WellScoped.hs b/src/Language/Syntactic/Functional/WellScoped.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Functional/WellScoped.hs @@ -0,0 +1,173 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} + +#ifndef MIN_VERSION_GLASGOW_HASKELL +#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0 +#endif + -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10 + +#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) +#else +{-# LANGUAGE OverlappingInstances #-} +#endif + +-- | Well-scoped terms + +module Language.Syntactic.Functional.WellScoped where + + + +import Control.Monad.Reader +import Data.Proxy + +import Language.Syntactic +import Language.Syntactic.Functional + + + +-- | Environment extension +class Ext ext orig + where + -- | Remove the extension of an environment + unext :: ext -> orig + -- | Return the amount by which an environment has been extended + diff :: Num a => Proxy ext -> Proxy orig -> a + +instance {-# OVERLAPPING #-} Ext env env + where + unext = id + diff _ _ = 0 + +instance {-# OVERLAPPING #-} (Ext env e, ext ~ (a,env)) => Ext ext e + where + unext = unext . snd + diff m n = diff (fmap snd m) n + 1 + +-- | Lookup in an extended environment +lookEnv :: forall env a e . Ext env (a,e) => Proxy e -> Reader env a +lookEnv _ = reader $ \env -> let (a, _ :: e) = unext env in a + +-- | Well-scoped variable binding +-- +-- Well-scoped terms are introduced to be able to evaluate without type casting. The implementation +-- is inspired by \"Typing Dynamic Typing\" (Baars and Swierstra, ICFP 2002, +-- ) where expressions are represented as (essentially) +-- @`Reader` env a@ after \"compilation\". However, a major difference is that +-- \"Typing Dynamic Typing\" starts from an untyped term, and thus needs (safe) dynamic type casting +-- during compilation. In contrast, the denotational semantics of 'BindingWS' (the 'Eval' instance) +-- uses no type casting. +data BindingWS sig + where + VarWS :: Ext env (a,e) => Proxy e -> BindingWS (Full (Reader env a)) + LamWS :: BindingWS (Reader (a,e) b :-> Full (Reader e (a -> b))) + +instance Symbol BindingWS + where + rnfSym (VarWS Proxy) = () + rnfSym LamWS = () + symSig (VarWS _) = signature + symSig LamWS = signature + +instance Eval BindingWS + where + evalSym (VarWS p) = lookEnv p + evalSym LamWS = \f -> reader $ \e -> \a -> runReader f (a,e) + +-- | Higher-order interface for well-scoped variable binding +-- +-- Inspired by Conor McBride's "I am not a number, I am a classy hack" +-- (). +lamWS :: forall a e sym b . (BindingWS :<: sym) + => ((forall env . (Ext env (a,e)) => ASTF sym (Reader env a)) -> ASTF sym (Reader (a,e) b)) + -> ASTF sym (Reader e (a -> b)) +lamWS f = smartSym LamWS $ f $ smartSym (VarWS (Proxy :: Proxy e)) + +-- | Evaluation of open well-scoped terms +evalOpenWS :: Eval s => env -> ASTF s (Reader env a) -> a +evalOpenWS e = ($ e) . runReader . evalDen + +-- | Evaluation of closed well-scoped terms +evalClosedWS :: Eval s => ASTF s (Reader () a) -> a +evalClosedWS = evalOpenWS () + +-- | Mapping from a symbol signature +-- +-- > a :-> b :-> Full c +-- +-- to +-- +-- > Reader env a :-> Reader env b :-> Full (Reader env c) +type family LiftReader env sig +type instance LiftReader env (Full a) = Full (Reader env a) +type instance LiftReader env (a :-> sig) = Reader env a :-> LiftReader env sig + +type family UnReader a +type instance UnReader (Reader e a) = a + +-- | Mapping from a symbol signature +-- +-- > Reader e a :-> Reader e b :-> Full (Reader e c) +-- +-- to +-- +-- > a :-> b :-> Full c +type family LowerReader sig +type instance LowerReader (Full a) = Full (UnReader a) +type instance LowerReader (a :-> sig) = UnReader a :-> LowerReader sig + +-- | Wrap a symbol to give it a 'LiftReader' signature +data ReaderSym sym sig + where + ReaderSym + :: ( Signature sig + , Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig + , LowerReader (LiftReader env sig) ~ sig + ) + => Proxy env + -> sym sig + -> ReaderSym sym (LiftReader env sig) + +instance Eval sym => Eval (ReaderSym sym) + where + evalSym (ReaderSym (_ :: Proxy env) s) = liftDenotationM signature p s $ evalSym s + where + p = Proxy :: Proxy (Reader env) + +-- | Well-scoped 'AST' +type WS sym env a = ASTF (BindingWS :+: ReaderSym sym) (Reader env a) + +-- | Convert the representation of variables and binders from 'BindingWS' to 'Binding'. The latter +-- is easier to analyze, has a 'Render' instance, etc. +fromWS :: WS sym env a -> ASTF (Binding :+: sym) a +fromWS = fromDeBruijn . go + where + go :: AST (BindingWS :+: ReaderSym sym) sig -> AST (Binding :+: sym) (LowerReader sig) + go (Sym (InjL s@(VarWS p))) = Sym (InjL (Var (diff (mkProxy2 s) (mkProxy1 s p)))) + where + mkProxy1 = (\_ _ -> Proxy) :: BindingWS (Full (Reader e' a)) -> Proxy e -> Proxy (a,e) + mkProxy2 = (\_ -> Proxy) :: BindingWS (Full (Reader e' a)) -> Proxy e' + go (Sym (InjL LamWS)) = Sym $ InjL $ Lam (-1) -- -1 since we're using De Bruijn + go (s :$ a) = go s :$ go a + go (Sym (InjR (ReaderSym _ s))) = Sym $ InjR s + +-- | Make a smart constructor for well-scoped terms. 'smartWS' has any type of the form: +-- +-- > smartWS :: (sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup)) +-- > => sub (a :-> b :-> ... :-> Full x) +-- > -> ASTF bsym (Reader env a) -> ASTF bsym (Reader env b) -> ... -> ASTF bsym (Reader env x) +smartWS :: forall sig sig' bsym f sub sup env a + . ( Signature sig + , Signature sig' + , sub :<: sup + , bsym ~ (BindingWS :+: ReaderSym sup) + , f ~ SmartFun bsym sig' + , sig' ~ SmartSig f + , bsym ~ SmartSym f + , sig' ~ LiftReader env sig + , Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig + , LowerReader (LiftReader env sig) ~ sig + , Reader env a ~ DenResult sig' + ) + => sub sig -> f +smartWS s = smartSym' $ InjR $ ReaderSym (Proxy :: Proxy env) $ inj s + diff --git a/src/Language/Syntactic/Interpretation.hs b/src/Language/Syntactic/Interpretation.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Interpretation.hs @@ -0,0 +1,219 @@ +{-# LANGUAGE TemplateHaskell #-} + +-- | Equality and rendering of 'AST's + +module Language.Syntactic.Interpretation + ( -- * Equality + Equality (..) + -- * Rendering + , Render (..) + , renderArgsSmart + , render + , StringTree (..) + , stringTree + , showAST + , drawAST + , writeHtmlAST + -- * Default interpretation + , equalDefault + , hashDefault + , interpretationInstances + ) where + + + +import Data.Tree (Tree (..)) +import Language.Haskell.TH + +import Data.Hash (Hash, combine, hashInt) +import qualified Data.Hash as Hash +import Data.Tree.View + +import Language.Syntactic.Syntax + + + +---------------------------------------------------------------------------------------------------- +-- * Equality +---------------------------------------------------------------------------------------------------- + +-- | Higher-kinded equality +class Equality e + where + -- | Higher-kinded equality + -- + -- Comparing elements of different types is often needed when dealing with expressions with + -- existentially quantified sub-terms. + equal :: e a -> e b -> Bool + + -- | Higher-kinded hashing. Elements that are equal according to 'equal' must result in the same + -- hash: + -- + -- @equal a b ==> hash a == hash b@ + hash :: e a -> Hash + +instance Equality sym => Equality (AST sym) + where + equal (Sym s1) (Sym s2) = equal s1 s2 + equal (s1 :$ a1) (s2 :$ a2) = equal s1 s2 && equal a1 a2 + equal _ _ = False + + hash (Sym s) = hashInt 0 `combine` hash s + hash (s :$ a) = hashInt 1 `combine` hash s `combine` hash a + +instance Equality sym => Eq (AST sym a) + where + (==) = equal + +instance (Equality sym1, Equality sym2) => Equality (sym1 :+: sym2) + where + equal (InjL a) (InjL b) = equal a b + equal (InjR a) (InjR b) = equal a b + equal _ _ = False + + hash (InjL a) = hashInt 0 `combine` hash a + hash (InjR a) = hashInt 1 `combine` hash a + +instance (Equality sym1, Equality sym2) => Eq ((sym1 :+: sym2) a) + where + (==) = equal + +instance Equality Empty + where + equal = error "equal: Empty" + hash = error "hash: Empty" + +instance Equality sym => Equality (Typed sym) + where + equal (Typed s1) (Typed s2) = equal s1 s2 + hash (Typed s) = hash s + + + +---------------------------------------------------------------------------------------------------- +-- * Rendering +---------------------------------------------------------------------------------------------------- + +-- | Render a symbol as concrete syntax. A complete instance must define at least the 'renderSym' +-- method. +class Render sym + where + -- | Show a symbol as a 'String' + renderSym :: sym sig -> String + + -- | Render a symbol given a list of rendered arguments + renderArgs :: [String] -> sym sig -> String + renderArgs [] s = renderSym s + renderArgs args s = "(" ++ unwords (renderSym s : args) ++ ")" + +instance (Render sym1, Render sym2) => Render (sym1 :+: sym2) + where + renderSym (InjL s) = renderSym s + renderSym (InjR s) = renderSym s + renderArgs args (InjL s) = renderArgs args s + renderArgs args (InjR s) = renderArgs args s + +-- | Implementation of 'renderArgs' that handles infix operators +renderArgsSmart :: Render sym => [String] -> sym a -> String +renderArgsSmart [] sym = renderSym sym +renderArgsSmart args sym + | isInfix = "(" ++ unwords [a,op,b] ++ ")" + | otherwise = "(" ++ unwords (name : args) ++ ")" + where + name = renderSym sym + [a,b] = args + op = init $ tail name + isInfix + = not (null name) + && head name == '(' + && last name == ')' + && length args == 2 + +-- | Render an 'AST' as concrete syntax +render :: forall sym a. Render sym => ASTF sym a -> String +render = go [] + where + go :: [String] -> AST sym sig -> String + go args (Sym s) = renderArgs args s + go args (s :$ a) = go (render a : args) s + +instance Render Empty + where + renderSym = error "renderSym: Empty" + renderArgs = error "renderArgs: Empty" + +instance Render sym => Render (Typed sym) + where + renderSym (Typed s) = renderSym s + renderArgs args (Typed s) = renderArgs args s + +instance Render sym => Show (ASTF sym a) + where + show = render + + + +-- | Convert a symbol to a 'Tree' of strings +class Render sym => StringTree sym + where + -- | Convert a symbol to a 'Tree' given a list of argument trees + stringTreeSym :: [Tree String] -> sym a -> Tree String + stringTreeSym args s = Node (renderSym s) args + +instance (StringTree sym1, StringTree sym2) => StringTree (sym1 :+: sym2) + where + stringTreeSym args (InjL s) = stringTreeSym args s + stringTreeSym args (InjR s) = stringTreeSym args s + +instance StringTree Empty + +instance StringTree sym => StringTree (Typed sym) + where + stringTreeSym args (Typed s) = stringTreeSym args s + +-- | Convert an 'AST' to a 'Tree' of strings +stringTree :: forall sym a . StringTree sym => ASTF sym a -> Tree String +stringTree = go [] + where + go :: [Tree String] -> AST sym sig -> Tree String + go args (Sym s) = stringTreeSym args s + go args (s :$ a) = go (stringTree a : args) s + +-- | Show a syntax tree using ASCII art +showAST :: StringTree sym => ASTF sym a -> String +showAST = showTree . stringTree + +-- | Print a syntax tree using ASCII art +drawAST :: StringTree sym => ASTF sym a -> IO () +drawAST = putStrLn . showAST + +-- | Write a syntax tree to an HTML file with foldable nodes +writeHtmlAST :: StringTree sym => FilePath -> ASTF sym a -> IO () +writeHtmlAST file = writeHtmlTree file . fmap (\n -> NodeInfo n "") . stringTree + + + +---------------------------------------------------------------------------------------------------- +-- * Default interpretation +---------------------------------------------------------------------------------------------------- + +-- | Default implementation of 'equal' +equalDefault :: Render sym => sym a -> sym b -> Bool +equalDefault a b = renderSym a == renderSym b + +-- | Default implementation of 'hash' +hashDefault :: Render sym => sym a -> Hash +hashDefault = Hash.hash . renderSym + +-- | Derive instances for 'Equality' and 'StringTree' +interpretationInstances :: Name -> DecsQ +interpretationInstances n = + [d| + instance Equality $(typ) where + equal = equalDefault + hash = hashDefault + instance StringTree $(typ) + |] + where + typ = conT n + diff --git a/src/Language/Syntactic/Sugar.hs b/src/Language/Syntactic/Sugar.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sugar.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} + +#ifndef MIN_VERSION_GLASGOW_HASKELL +#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0 +#endif + -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10 + +#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) +#else +{-# LANGUAGE OverlappingInstances #-} +#endif + +-- | \"Syntactic sugar\" +-- +-- For details, see "Combining Deep and Shallow Embedding for EDSL" +-- (TFP 2013, ). + +module Language.Syntactic.Sugar where + + + +import Data.Typeable + +import Language.Syntactic.Syntax + + + +-- | It is usually assumed that @(`desugar` (`sugar` a))@ has the same meaning +-- as @a@. +class Syntactic a + where + type Domain a :: * -> * + type Internal a + desugar :: a -> ASTF (Domain a) (Internal a) + sugar :: ASTF (Domain a) (Internal a) -> a + +instance Syntactic (ASTF sym a) + where + type Domain (ASTF sym a) = sym + type Internal (ASTF sym a) = a + desugar = id + sugar = id + +-- | Syntactic type casting +resugar :: (Syntactic a, Syntactic b, Domain a ~ Domain b, Internal a ~ Internal b) => a -> b +resugar = sugar . desugar + +-- | N-ary syntactic functions +-- +-- 'desugarN' has any type of the form: +-- +-- > desugarN :: +-- > ( Syntactic a +-- > , Syntactic b +-- > , ... +-- > , Syntactic x +-- > , Domain a ~ sym +-- > , Domain b ~ sym +-- > , ... +-- > , Domain x ~ sym +-- > ) => (a -> b -> ... -> x) +-- > -> ( ASTF sym (Internal a) +-- > -> ASTF sym (Internal b) +-- > -> ... +-- > -> ASTF sym (Internal x) +-- > ) +-- +-- ...and vice versa for 'sugarN'. +class SyntacticN f internal | f -> internal + where + desugarN :: f -> internal + sugarN :: internal -> f + +instance {-# OVERLAPPING #-} + (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi + where + desugarN = desugar + sugarN = sugar + +instance {-# OVERLAPPING #-} + ( Syntactic a + , Domain a ~ sym + , ia ~ Internal a + , SyntacticN f fi + ) => + SyntacticN (a -> f) (AST sym (Full ia) -> fi) + where + desugarN f = desugarN . f . sugar + sugarN f = sugarN . f . desugar + +-- | \"Sugared\" symbol application +-- +-- 'sugarSym' has any type of the form: +-- +-- > sugarSym :: +-- > ( sub :<: AST sup +-- > , Syntactic a +-- > , Syntactic b +-- > , ... +-- > , Syntactic x +-- > , Domain a ~ Domain b ~ ... ~ Domain x +-- > ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x)) +-- > -> (a -> b -> ... -> x) +sugarSym + :: ( Signature sig + , fi ~ SmartFun sup sig + , sig ~ SmartSig fi + , sup ~ SmartSym fi + , SyntacticN f fi + , sub :<: sup + ) + => sub sig -> f +sugarSym = sugarN . smartSym + +-- | \"Sugared\" symbol application +-- +-- 'sugarSym' has any type of the form: +-- +-- > sugarSym :: +-- > ( sub :<: AST (Typed sup) +-- > , Syntactic a +-- > , Syntactic b +-- > , ... +-- > , Syntactic x +-- > , Domain a ~ Domain b ~ ... ~ Domain x +-- > , Typeable (Internal x) +-- > ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x)) +-- > -> (a -> b -> ... -> x) +sugarSymT + :: ( Signature sig + , fi ~ SmartFun (Typed sup) sig + , sig ~ SmartSig fi + , Typed sup ~ SmartSym fi + , SyntacticN f fi + , sub :<: sup + , Typeable (DenResult sig) + ) + => sub sig -> f +sugarSymT = sugarN . smartSymT + diff --git a/src/Language/Syntactic/Sugar/Binding.hs b/src/Language/Syntactic/Sugar/Binding.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sugar/Binding.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | 'Syntactic' instance for functions +-- +-- This module is based on having 'Binding' in the domain. For 'BindingT' import +-- module "Language.Syntactic.Sugar.BindingT" instead. + +module Language.Syntactic.Sugar.Binding where + + + +import Language.Syntactic +import Language.Syntactic.Functional + + + +instance + ( Syntactic a, Domain a ~ dom + , Syntactic b, Domain b ~ dom + , Binding :<: dom + ) => + Syntactic (a -> b) + where + type Domain (a -> b) = Domain a + type Internal (a -> b) = Internal a -> Internal b + desugar f = lam (desugar . f . sugar) + sugar = error "sugar not implemented for (a -> b)" + diff --git a/src/Language/Syntactic/Sugar/BindingT.hs b/src/Language/Syntactic/Sugar/BindingT.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sugar/BindingT.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | 'Syntactic' instance for functions +-- +-- This module is based on having 'BindingT' in the domain. For 'Binding' import +-- module "Language.Syntactic.Sugar.Binding" instead. + +module Language.Syntactic.Sugar.BindingT where + + + +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Functional + + + +instance + ( Syntactic a, Domain a ~ Typed dom + , Syntactic b, Domain b ~ Typed dom + , BindingT :<: dom + , Typeable (Internal a) + , Typeable (Internal b) + ) => + Syntactic (a -> b) + where + type Domain (a -> b) = Domain a + type Internal (a -> b) = Internal a -> Internal b + desugar f = lamT (desugar . f . sugar) + sugar = error "sugar not implemented for (a -> b)" + diff --git a/src/Language/Syntactic/Sugar/Monad.hs b/src/Language/Syntactic/Sugar/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sugar/Monad.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} + +#if __GLASGOW_HASKELL__ < 708 +#define TYPEABLE Typeable1 +#else +#define TYPEABLE Typeable +#endif + +-- | 'Syntactic' instance for 'Remon' using 'Binding' to handle variable binding + +module Language.Syntactic.Sugar.Monad where + + + +import Control.Monad.Cont +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Functional +import Language.Syntactic.Sugar.Binding () + + + +-- | One-layer sugaring of monadic actions +sugarMonad :: (Binding :<: sym, MONAD m :<: sym) => + ASTF sym (m a) -> Remon sym m (ASTF sym a) +sugarMonad ma = Remon $ cont $ sugarSym Bind ma + +instance + ( Syntactic a + , Domain a ~ sym + , Binding :<: sym + , MONAD m :<: sym + , TYPEABLE m + , Typeable (Internal a) + -- The `Typeable` constraints are only needed due to the `Typeable` + -- constraint in `Remon`. That constraint, in turn, is only needed by + -- the module "Language.Syntactic.Sugar.MonadT". + ) => + Syntactic (Remon sym m a) + where + type Domain (Remon sym m a) = sym + type Internal (Remon sym m a) = m (Internal a) + desugar = desugarMonad . fmap desugar + sugar = fmap sugar . sugarMonad + diff --git a/src/Language/Syntactic/Sugar/MonadT.hs b/src/Language/Syntactic/Sugar/MonadT.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sugar/MonadT.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} + +#if __GLASGOW_HASKELL__ < 708 +#define TYPEABLE Typeable1 +#else +#define TYPEABLE Typeable +#endif + +-- | 'Syntactic' instance for 'Remon' using 'BindingT' to handle variable binding + +module Language.Syntactic.Sugar.MonadT where + + + +import Control.Monad.Cont +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Functional +import Language.Syntactic.Sugar.BindingT () + + + +-- | One-layer sugaring of monadic actions +sugarMonad + :: ( BindingT :<: sym + , MONAD m :<: sym + , symT ~ Typed sym + , TYPEABLE m + , Typeable a + ) + => ASTF symT (m a) -> Remon symT m (ASTF symT a) +sugarMonad ma = Remon $ cont $ sugarSymT Bind ma + +instance + ( Syntactic a + , Domain a ~ symT + , symT ~ Typed sym + , BindingT :<: sym + , MONAD m :<: sym + , TYPEABLE m + , Typeable (Internal a) + ) => + Syntactic (Remon symT m a) + where + type Domain (Remon symT m a) = symT + type Internal (Remon symT m a) = m (Internal a) + desugar = desugarMonadT . fmap desugar + sugar = fmap sugar . sugarMonad + diff --git a/src/Language/Syntactic/Sugar/Tuple.hs b/src/Language/Syntactic/Sugar/Tuple.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sugar/Tuple.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | 'Syntactic' instances for tuples + +module Language.Syntactic.Sugar.Tuple where + + + +import Language.Syntactic +import Language.Syntactic.Functional.Tuple + + + +instance + ( Syntactic a + , Syntactic b + , Domain a ~ Domain b + , Tuple :<: Domain a + ) => + Syntactic (a,b) + where + type Domain (a,b) = Domain a + type Internal (a,b) = (Internal a, Internal b) + desugar (a,b) = sugarSym Tup2 a b + sugar ab = (sugarSym Sel1 ab, sugarSym Sel2 ab) + +instance + ( Syntactic a + , Syntactic b + , Syntactic c + , Domain a ~ Domain b + , Domain a ~ Domain c + , Tuple :<: Domain a + ) => + Syntactic (a,b,c) + where + type Domain (a,b,c) = Domain a + type Internal (a,b,c) = (Internal a, Internal b, Internal c) + desugar (a,b,c) = sugarSym Tup3 a b c + sugar abc = (sugarSym Sel1 abc, sugarSym Sel2 abc, sugarSym Sel3 abc) + +instance + ( Syntactic a + , Syntactic b + , Syntactic c + , Syntactic d + , Domain a ~ Domain b + , Domain a ~ Domain c + , Domain a ~ Domain d + , Tuple :<: Domain a + ) => + Syntactic (a,b,c,d) + where + type Domain (a,b,c,d) = Domain a + type Internal (a,b,c,d) = (Internal a, Internal b, Internal c, Internal d) + desugar (a,b,c,d) = sugarSym Tup4 a b c d + sugar abcd = (sugarSym Sel1 abcd, sugarSym Sel2 abcd, sugarSym Sel3 abcd, sugarSym Sel4 abcd) + diff --git a/src/Language/Syntactic/Sugar/TupleT.hs b/src/Language/Syntactic/Sugar/TupleT.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Sugar/TupleT.hs @@ -0,0 +1,72 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | 'Syntactic' instances for tuples and 'Typed' symbol domains + +module Language.Syntactic.Sugar.TupleT where + + + +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Functional.Tuple + + + +instance + ( Syntactic a + , Syntactic b + , Typeable (Internal a) + , Typeable (Internal b) + , Domain a ~ Typed sym + , Domain a ~ Domain b + , Tuple :<: sym + ) => + Syntactic (a,b) + where + type Domain (a,b) = Domain a + type Internal (a,b) = (Internal a, Internal b) + desugar (a,b) = sugarSymT Tup2 a b + sugar ab = (sugarSymT Sel1 ab, sugarSymT Sel2 ab) + +instance + ( Syntactic a + , Syntactic b + , Syntactic c + , Typeable (Internal a) + , Typeable (Internal b) + , Typeable (Internal c) + , Domain a ~ Typed sym + , Domain a ~ Domain b + , Domain a ~ Domain c + , Tuple :<: sym + ) => + Syntactic (a,b,c) + where + type Domain (a,b,c) = Domain a + type Internal (a,b,c) = (Internal a, Internal b, Internal c) + desugar (a,b,c) = sugarSymT Tup3 a b c + sugar abc = (sugarSymT Sel1 abc, sugarSymT Sel2 abc, sugarSymT Sel3 abc) + +instance + ( Syntactic a + , Syntactic b + , Syntactic c + , Syntactic d + , Typeable (Internal a) + , Typeable (Internal b) + , Typeable (Internal c) + , Typeable (Internal d) + , Domain a ~ Typed sym + , Domain a ~ Domain b + , Domain a ~ Domain c + , Domain a ~ Domain d + , Tuple :<: sym + ) => + Syntactic (a,b,c,d) + where + type Domain (a,b,c,d) = Domain a + type Internal (a,b,c,d) = (Internal a, Internal b, Internal c, Internal d) + desugar (a,b,c,d) = sugarSymT Tup4 a b c d + sugar abcd = (sugarSymT Sel1 abcd, sugarSymT Sel2 abcd, sugarSymT Sel3 abcd, sugarSymT Sel4 abcd) + diff --git a/src/Language/Syntactic/Syntax.hs b/src/Language/Syntactic/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Syntax.hs @@ -0,0 +1,400 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE UndecidableInstances #-} + +#ifndef MIN_VERSION_GLASGOW_HASKELL +#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0 +#endif + -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10 + +#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) +#else +{-# LANGUAGE OverlappingInstances #-} +#endif + +-- | Generic representation of typed syntax trees +-- +-- For details, see: A Generic Abstract Syntax Model for Embedded Languages +-- (ICFP 2012, ). + +module Language.Syntactic.Syntax + ( -- * Syntax trees + AST (..) + , ASTF + , Full (..) + , (:->) (..) + , SigRep (..) + , Signature (..) + , DenResult + , Symbol (..) + , size + -- * Smart constructors + , SmartFun + , SmartSig + , SmartSym + , smartSym' + -- * Open symbol domains + , (:+:) (..) + , Project (..) + , (:<:) (..) + , smartSym + , smartSymT + , Empty + -- * Existential quantification + , E (..) + , liftE + , liftE2 + , EF (..) + , liftEF + , liftEF2 + -- * Type casting expressions + , Typed (..) + , injT + , castExpr + -- * Type inference + , symType + , prjP + ) where + + + +import Control.DeepSeq +import Data.Typeable +#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0) +#else +import Data.Foldable (Foldable) +import Data.Proxy -- Needed by GHC < 7.8 +import Data.Traversable (Traversable) +#endif + + + +-------------------------------------------------------------------------------- +-- * Syntax trees +-------------------------------------------------------------------------------- + +-- | Generic abstract syntax tree, parameterized by a symbol domain +-- +-- @(`AST` sym (a `:->` b))@ represents a partially applied (or unapplied) +-- symbol, missing at least one argument, while @(`AST` sym (`Full` a))@ +-- represents a fully applied symbol, i.e. a complete syntax tree. +data AST sym sig + where + Sym :: sym sig -> AST sym sig + (:$) :: AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig + +infixl 1 :$ + +-- | Fully applied abstract syntax tree +type ASTF sym a = AST sym (Full a) + +instance Functor sym => Functor (AST sym) + where + fmap f (Sym s) = Sym (fmap f s) + fmap f (s :$ a) = fmap (fmap f) s :$ a + +-- | Signature of a fully applied symbol +newtype Full a = Full { result :: a } + deriving (Eq, Show, Typeable, Functor) + +-- | Signature of a partially applied (or unapplied) symbol +newtype a :-> sig = Partial (a -> sig) + deriving (Typeable, Functor) + +infixr :-> + +-- | Witness of the arity of a symbol signature +data SigRep sig + where + SigFull :: SigRep (Full a) + SigMore :: SigRep sig -> SigRep (a :-> sig) + +-- | Valid symbol signatures +class Signature sig + where + signature :: SigRep sig + +instance Signature (Full a) + where + signature = SigFull + +instance Signature sig => Signature (a :-> sig) + where + signature = SigMore signature + +-- | 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 + +-- | Valid symbols to use in an 'AST' +class Symbol sym + where + -- | Force a symbol to normal form + rnfSym :: sym sig -> () + rnfSym s = s `seq` () + + -- | Reify the signature of a symbol + symSig :: sym sig -> SigRep sig + +instance Symbol sym => NFData (AST sym sig) + where + rnf (Sym s) = rnfSym s + rnf (s :$ a) = rnf s `seq` rnf a + +-- | Count the number of symbols in an 'AST' +size :: AST sym sig -> Int +size (Sym _) = 1 +size (s :$ a) = size s + size a + + + +-------------------------------------------------------------------------------- +-- * Smart constructors +-------------------------------------------------------------------------------- + +-- | Maps a symbol signature to the type of the corresponding smart constructor: +-- +-- > SmartFun sym (a :-> b :-> ... :-> Full x) = ASTF sym a -> ASTF sym b -> ... -> ASTF sym x +type family SmartFun (sym :: * -> *) sig +type instance SmartFun sym (Full a) = ASTF sym a +type instance SmartFun sym (a :-> sig) = ASTF sym a -> SmartFun sym sig + +-- | Maps a smart constructor type to the corresponding symbol signature: +-- +-- > SmartSig (ASTF sym a -> ASTF sym b -> ... -> ASTF sym x) = a :-> b :-> ... :-> Full x +type family SmartSig f +type instance SmartSig (AST sym sig) = sig +type instance SmartSig (ASTF sym a -> f) = a :-> SmartSig f + +-- | Returns the symbol in the result of a smart constructor +type family SmartSym f :: * -> * +type instance SmartSym (AST sym sig) = sym +type instance SmartSym (a -> f) = SmartSym f + +-- | Make a smart constructor of a symbol. 'smartSym' has any type of the form: +-- +-- > smartSym +-- > :: sym (a :-> b :-> ... :-> Full x) +-- > -> (ASTF sym a -> ASTF sym b -> ... -> ASTF sym x) +smartSym' :: forall sig f sym + . ( Signature sig + , f ~ SmartFun sym sig + , sig ~ SmartSig f + , sym ~ SmartSym f + ) + => sym sig -> f +smartSym' s = go (signature :: SigRep sig) (Sym s) + where + go :: forall sig . SigRep sig -> AST sym sig -> SmartFun sym sig + go SigFull s = s + go (SigMore sig) s = \a -> go sig (s :$ a) + + + +-------------------------------------------------------------------------------- +-- * Open symbol domains +-------------------------------------------------------------------------------- + +-- | Direct sum of two symbol domains +data (sym1 :+: sym2) sig + where + InjL :: sym1 a -> (sym1 :+: sym2) a + InjR :: sym2 a -> (sym1 :+: sym2) a + deriving (Functor, Foldable, Traversable) + +infixr :+: + +instance (Symbol sym1, Symbol sym2) => Symbol (sym1 :+: sym2) + where + rnfSym (InjL s) = rnfSym s + rnfSym (InjR s) = rnfSym s + symSig (InjL s) = symSig s + symSig (InjR s) = symSig s + +-- | Symbol projection +-- +-- The class is defined for /all pairs of types/, but 'prj' can only succeed if @sup@ is of the form +-- @(... `:+:` sub `:+:` ...)@. +class Project sub sup + where + -- | Partial projection from @sup@ to @sub@ + prj :: sup a -> Maybe (sub a) + +instance {-# OVERLAPPING #-} Project sub sup => Project sub (AST sup) + where + prj (Sym s) = prj s + prj _ = Nothing + +instance {-# OVERLAPPING #-} Project sym sym + where + prj = Just + +instance {-# OVERLAPPING #-} Project sym1 (sym1 :+: sym2) + where + prj (InjL a) = Just a + prj _ = Nothing + +instance {-# OVERLAPPING #-} Project sym1 sym3 => Project sym1 (sym2 :+: sym3) + where + prj (InjR a) = prj a + prj _ = Nothing + +-- | If @sub@ is not in @sup@, 'prj' always returns 'Nothing'. +instance Project sub sup + where + prj _ = Nothing + +-- | Symbol injection +-- +-- The class includes types @sub@ and @sup@ where @sup@ is of the form @(... `:+:` sub `:+:` ...)@. +class Project sub sup => sub :<: sup + where + -- | Injection from @sub@ to @sup@ + inj :: sub a -> sup a + +instance {-# OVERLAPPING #-} (sub :<: sup) => (sub :<: AST sup) + where + inj = Sym . inj + +instance {-# OVERLAPPING #-} (sym :<: sym) + where + inj = id + +instance {-# OVERLAPPING #-} (sym1 :<: (sym1 :+: sym2)) + where + inj = InjL + +instance {-# OVERLAPPING #-} (sym1 :<: sym3) => (sym1 :<: (sym2 :+: sym3)) + where + inj = InjR . inj + +-- The reason for separating the `Project` and `(:<:)` classes is that there are +-- types that can be instances of the former but not the latter due to type +-- constraints on the `a` type. + +-- | Make a smart constructor of a symbol. 'smartSym' has any type of the form: +-- +-- > smartSym :: (sub :<: AST sup) +-- > => sub (a :-> b :-> ... :-> Full x) +-- > -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x) +smartSym + :: ( Signature sig + , f ~ SmartFun sup sig + , sig ~ SmartSig f + , sup ~ SmartSym f + , sub :<: sup + ) + => sub sig -> f +smartSym = smartSym' . inj + +-- | Make a smart constructor of a symbol. 'smartSymT' has any type of the form: +-- +-- > smartSym :: (sub :<: AST (Typed sup), Typeable x) +-- > => sub (a :-> b :-> ... :-> Full x) +-- > -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x) +smartSymT + :: ( Signature sig + , f ~ SmartFun (Typed sup) sig + , sig ~ SmartSig f + , Typed sup ~ SmartSym f + , sub :<: sup + , Typeable (DenResult sig) + ) + => sub sig -> f +smartSymT = smartSym' . Typed . inj + +-- | Empty symbol type +-- +-- Can be used to make uninhabited 'AST' types. It can also be used as a terminator in co-product +-- lists (e.g. to avoid overlapping instances): +-- +-- > (A :+: B :+: Empty) +data Empty :: * -> * + + + +-------------------------------------------------------------------------------- +-- * Existential quantification +-------------------------------------------------------------------------------- + +-- | Existential quantification +data E e + where + E :: e a -> E e + +liftE :: (forall a . e a -> b) -> E e -> b +liftE f (E a) = f a + +liftE2 :: (forall a b . e a -> e b -> c) -> E e -> E e -> c +liftE2 f (E a) (E b) = f a b + +-- | Existential quantification of 'Full'-indexed type +data EF e + where + EF :: e (Full a) -> EF e + +liftEF :: (forall a . e (Full a) -> b) -> EF e -> b +liftEF f (EF a) = f a + +liftEF2 :: (forall a b . e (Full a) -> e (Full b) -> c) -> EF e -> EF e -> c +liftEF2 f (EF a) (EF b) = f a b + + + +-------------------------------------------------------------------------------- +-- * Type casting expressions +-------------------------------------------------------------------------------- + +-- | \"Typed\" symbol. Using @`Typed` sym@ instead of @sym@ gives access to the +-- function 'castExpr' for casting expressions. +data Typed sym sig + where + Typed :: Typeable (DenResult sig) => sym sig -> Typed sym sig + +instance {-# OVERLAPPING #-} Project sub sup => Project sub (Typed sup) + where + prj (Typed s) = prj s + +-- | Inject a symbol in an 'AST' with a 'Typed' domain +injT :: (sub :<: sup, Typeable (DenResult sig)) => + sub sig -> AST (Typed sup) sig +injT = Sym . Typed . inj + +-- | Type cast an expression +castExpr :: forall sym a b + . ASTF (Typed sym) a -- ^ Expression to cast + -> ASTF (Typed sym) b -- ^ Witness for typeability of result + -> Maybe (ASTF (Typed sym) b) +castExpr a b = cast1 a + where + cast1 :: (DenResult sig ~ a) => AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b) + cast1 (s :$ _) = cast1 s + cast1 (Sym (Typed _)) = cast2 b + where + cast2 :: (DenResult sig ~ b) => AST (Typed sym) sig -> Maybe (ASTF (Typed sym) b) + cast2 (s :$ _) = cast2 s + cast2 (Sym (Typed _)) = gcast a + -- Could be simplified using `simpleMatch`, but that would give an import + -- cycle. + -- + -- castExpr a b = + -- simpleMatch + -- (\(Typed _) _ -> simpleMatch + -- (\(Typed _) _ -> gcast a + -- ) b + -- ) a + + + +-------------------------------------------------------------------------------- +-- * Type inference +-------------------------------------------------------------------------------- + +-- | Constrain a symbol to a specific type +symType :: Proxy sym -> sym sig -> sym sig +symType _ = id + +-- | Projection to a specific symbol type +prjP :: Project sub sup => Proxy sub -> sup sig -> Maybe (sub sig) +prjP _ = prj + diff --git a/src/Language/Syntactic/Traversal.hs b/src/Language/Syntactic/Traversal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Syntactic/Traversal.hs @@ -0,0 +1,202 @@ +-- | Generic traversals of 'AST' terms + +module Language.Syntactic.Traversal + ( gmapQ + , gmapT + , everywhereUp + , everywhereDown + , universe + , Args (..) + , listArgs + , mapArgs + , mapArgsA + , mapArgsM + , foldrArgs + , appArgs + , listFold + , match + , simpleMatch + , fold + , simpleFold + , matchTrans + , mapAST + , WrapFull (..) + , toTree + ) where + + + +import Control.Applicative +import Data.Tree + +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 sym + . (forall a . ASTF sym a -> ASTF sym a) + -> (forall a . ASTF sym a -> ASTF sym a) +gmapT f a = go a + where + go :: AST sym a -> AST sym 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 sym b + . (forall a . ASTF sym a -> b) + -> (forall a . ASTF sym a -> [b]) +gmapQ f a = go a + where + go :: AST sym a -> [b] + go (s :$ a) = f a : go s + go _ = [] + +-- | Apply a transformation bottom-up over an 'AST' (corresponds to @everywhere@ in Scrap Your +-- Boilerplate) +everywhereUp + :: (forall a . ASTF sym a -> ASTF sym a) + -> (forall a . ASTF sym a -> ASTF sym a) +everywhereUp f = f . gmapT (everywhereUp f) + +-- | Apply a transformation top-down over an 'AST' (corresponds to @everywhere'@ in Scrap Your +-- Boilerplate) +everywhereDown + :: (forall a . ASTF sym a -> ASTF sym a) + -> (forall a . ASTF sym a -> ASTF sym a) +everywhereDown f = gmapT (everywhereDown f) . f + +-- | List all sub-terms (corresponds to @universe@ in Uniplate) +universe :: ASTF sym a -> [EF (AST sym)] +universe a = EF a : go a + where + go :: AST sym a -> [EF (AST sym)] + go (Sym s) = [] + go (s :$ a) = go s ++ universe a + +-- | 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) + +-- | Right fold for an 'Args' list +foldrArgs + :: (forall a . c (Full a) -> b -> b) + -> b + -> (forall sig . Args c sig -> b) +foldrArgs f b Nil = b +foldrArgs f b (a :* as) = f a (foldrArgs f b as) + +-- | Apply a (partially applied) symbol to a list of argument terms +appArgs :: AST sym sig -> Args (AST sym) sig -> ASTF sym (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 sym a c + . ( forall sig . (a ~ DenResult sig) => + sym sig -> Args (AST sym) sig -> c (Full a) + ) + -> ASTF sym a + -> c (Full a) +match f a = go a Nil + where + go :: (a ~ DenResult sig) => AST sym sig -> Args (AST sym) sig -> c (Full a) + go (Sym a) as = f a as + go (s :$ a) as = go s (a :* as) + +-- | A version of 'match' with a simpler result type +simpleMatch :: forall sym a b + . (forall sig . (a ~ DenResult sig) => sym sig -> Args (AST sym) sig -> b) + -> ASTF sym 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 sym c + . (forall sig . sym sig -> Args c sig -> c (Full (DenResult sig))) + -> (forall a . ASTF sym 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 sym b + . (forall sig . sym sig -> Args (Const b) sig -> b) + -> (forall a . ASTF sym 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 sym b + . (forall sig . sym sig -> [b] -> b) + -> (forall a . ASTF sym a -> b) +listFold f = simpleFold (\s -> f s . listArgs getConst) + +newtype WrapAST c sym sig = WrapAST { unWrapAST :: c (AST sym 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 sym sym' c a + . ( forall sig . (a ~ DenResult sig) => + sym sig -> Args (AST sym) sig -> c (ASTF sym' a) + ) + -> ASTF sym a + -> c (ASTF sym' a) +matchTrans f = unWrapAST . match (\s -> WrapAST . f s) + +-- | Update the symbols in an AST +mapAST :: (forall sig' . sym1 sig' -> sym2 sig') -> AST sym1 sig -> AST sym2 sig +mapAST f (Sym s) = Sym (f s) +mapAST f (s :$ a) = mapAST f s :$ mapAST f a + +-- | 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) + +-- | Convert an 'AST' to a 'Tree' +toTree :: forall dom a b . (forall sig . dom sig -> b) -> ASTF dom a -> Tree b +toTree f = listFold (Node . f) + diff --git a/syntactic.cabal b/syntactic.cabal --- a/syntactic.cabal +++ b/syntactic.cabal @@ -1,10 +1,13 @@ Name: syntactic -Version: 2.1 +Version: 3.0 Synopsis: Generic representation and manipulation of abstract syntax Description: The library provides a generic representation of type-indexed abstract syntax trees (or indexed data types in general). It also permits the definition of open syntax trees based on the technique in Data Types à la Carte [1]. . + (Note that the difference between version 2.x and 3.0 is not that big. The bump to + 3.0 was done because the modules changed namespace.) + . For more information, see \"A Generic Abstract Syntax Model for Embedded Languages\" (ICFP 2012): @@ -24,7 +27,7 @@ License-file: LICENSE Author: Emil Axelsson Maintainer: emax@chalmers.se -Copyright: Copyright (c) 2011-2014, Emil Axelsson +Copyright: Copyright (c) 2011-2015, Emil Axelsson Homepage: https://github.com/emilaxelsson/syntactic Bug-reports: https://github.com/emilaxelsson/syntactic/issues Stability: experimental @@ -45,26 +48,29 @@ library exposed-modules: - Data.Syntactic - Data.Syntactic.Syntax - Data.Syntactic.Traversal - Data.Syntactic.Interpretation - Data.Syntactic.Sugar - Data.Syntactic.Decoration - Data.Syntactic.Functional - Data.Syntactic.Sugar.Binding - Data.Syntactic.Sugar.BindingT - Data.Syntactic.Sugar.Monad - Data.Syntactic.Sugar.MonadT + Language.Syntactic + Language.Syntactic.Syntax + Language.Syntactic.Traversal + Language.Syntactic.Interpretation + Language.Syntactic.Sugar + Language.Syntactic.Decoration + Language.Syntactic.Functional + Language.Syntactic.Functional.Sharing + Language.Syntactic.Functional.Tuple + Language.Syntactic.Functional.WellScoped + Language.Syntactic.Sugar.Binding + Language.Syntactic.Sugar.BindingT + Language.Syntactic.Sugar.Monad + Language.Syntactic.Sugar.MonadT + Language.Syntactic.Sugar.Tuple + Language.Syntactic.Sugar.TupleT build-depends: base >= 4 && < 5, containers, - constraints, data-hash, deepseq, mtl >= 2 && < 3, - safe, tagged, template-haskell, tree-view diff --git a/tests/MonadTests.hs b/tests/MonadTests.hs --- a/tests/MonadTests.hs +++ b/tests/MonadTests.hs @@ -11,7 +11,7 @@ import Data.ByteString.Lazy.UTF8 (fromString) -import Data.Syntactic +import Language.Syntactic import qualified Monad diff --git a/tests/NanoFeldsparTests.hs b/tests/NanoFeldsparTests.hs --- a/tests/NanoFeldsparTests.hs +++ b/tests/NanoFeldsparTests.hs @@ -15,16 +15,37 @@ import Data.ByteString.Lazy.UTF8 (fromString) -import Data.Syntactic -import Data.Syntactic.Functional +import Language.Syntactic +import Language.Syntactic.Functional +import Language.Syntactic.Functional.Sharing import qualified NanoFeldspar as Nano +-- | Evaluate after code motion. Used to test that 'codeMotion' doesn't change +-- semantics. +evalCM :: (Syntactic a, Domain a ~ Nano.FeldDomain) => a -> Internal a +evalCM = evalClosed . codeMotion Nano.cmInterface . desugar + +fib :: Int -> Int +fib n = fibs !! n + where + fibs = 0 : 1 : zipWith (+) fibs (tail fibs) + +prop_fib (NonNegative (Small n)) = fib n == Nano.eval Nano.fib n +prop_fibCM (NonNegative (Small n)) = fib n == evalCM Nano.fib n + +spanVec :: [Int] -> Int +spanVec as = maximum as - minimum as + +prop_spanVec (NonEmpty as) = spanVec as == Nano.eval Nano.spanVec as +prop_spanVecCM (NonEmpty as) = spanVec as == evalCM Nano.spanVec as + scProd :: [Float] -> [Float] -> Float scProd as bs = sum $ zipWith (*) as bs -prop_scProd as bs = scProd as bs == Nano.eval Nano.scProd as bs +prop_scProd as bs = scProd as bs == Nano.eval Nano.scProd as bs +prop_scProdCM as bs = scProd as bs == evalCM Nano.scProd as bs genMat :: Gen [[Float]] genMat = sized $ \s -> do @@ -44,6 +65,11 @@ forAll genMat $ \b -> matMul a b == Nano.eval Nano.matMul a b +prop_matMulCM = + forAll genMat $ \a -> + forAll genMat $ \b -> + matMul a b == evalCM Nano.matMul a b + mkGold_scProd = writeFile "tests/gold/scProd.txt" $ Nano.showAST Nano.scProd mkGold_matMul = writeFile "tests/gold/matMul.txt" $ Nano.showAST Nano.matMul @@ -51,30 +77,38 @@ alphaRename = mapAST rename where rename :: Nano.FeldDomain a -> Nano.FeldDomain a - rename s - | Just (VarT v) <- prj s = inj (VarT (v+1)) - | Just (LamT v) <- prj s = inj (LamT (v+1)) - | otherwise = s + rename (Typed s) + | Just (VarT v) <- prj s = Typed $ inj (VarT (v+1)) + | Just (LamT v) <- prj s = Typed $ inj (LamT (v+1)) + | otherwise = Typed s badRename :: ASTF Nano.FeldDomain a -> ASTF Nano.FeldDomain a badRename = mapAST rename where rename :: Nano.FeldDomain a -> Nano.FeldDomain a - rename s - | Just (VarT v) <- prj s = inj (VarT (v+1)) - | Just (LamT v) <- prj s = inj (LamT (v-1)) - | otherwise = s + rename (Typed s) + | Just (VarT v) <- prj s = Typed $ inj (VarT (v+1)) + | Just (LamT v) <- prj s = Typed $ inj (LamT (v-1)) + | otherwise = Typed s prop_alphaEq a = alphaEq a (alphaRename a) prop_alphaEqBad a = alphaEq a (badRename a) tests = testGroup "NanoFeldsparTests" - [ goldenVsString "scProd tree" "tests/gold/scProd.txt" $ return $ fromString $ Nano.showAST Nano.scProd - , goldenVsString "matMul tree" "tests/gold/matMul.txt" $ return $ fromString $ Nano.showAST Nano.matMul + [ goldenVsString "fib tree" "tests/gold/fib.txt" $ return $ fromString $ Nano.showAST Nano.fib + , goldenVsString "spanVec tree" "tests/gold/spanVec.txt" $ return $ fromString $ Nano.showAST Nano.spanVec + , goldenVsString "scProd tree" "tests/gold/scProd.txt" $ return $ fromString $ Nano.showAST Nano.scProd + , goldenVsString "matMul tree" "tests/gold/matMul.txt" $ return $ fromString $ Nano.showAST Nano.matMul - , testProperty "scProd eval" prop_scProd - , testProperty "matMul eval" prop_matMul + , testProperty "fib eval" prop_fib + , testProperty "spanVec eval" prop_spanVec + , testProperty "scProd eval" prop_scProd + , testProperty "matMul eval" prop_matMul + + , testProperty "fib evalCM" prop_fibCM + , testProperty "scProd evalCM" prop_scProdCM + , testProperty "matMul evalCM" prop_matMulCM , testProperty "alphaEq scProd" (prop_alphaEq (desugar Nano.scProd)) , testProperty "alphaEq matMul" (prop_alphaEq (desugar Nano.matMul)) diff --git a/tests/WellScopedTests.hs b/tests/WellScopedTests.hs --- a/tests/WellScopedTests.hs +++ b/tests/WellScopedTests.hs @@ -12,8 +12,8 @@ import Data.ByteString.Lazy.UTF8 (fromString) -import Data.Syntactic -import Data.Syntactic.Functional +import Language.Syntactic +import Language.Syntactic.Functional.WellScoped import qualified WellScoped as WS diff --git a/tests/gold/fib.txt b/tests/gold/fib.txt new file mode 100644 --- /dev/null +++ b/tests/gold/fib.txt @@ -0,0 +1,17 @@ +Lam v3 + └╴sel1 + └╴forLoop + ├╴v3 + ├╴tup2 + │ ├╴0 + │ └╴1 + └╴Lam v2 + └╴Lam v1 + └╴tup2 + ├╴sel2 + │ └╴v1 + └╴(+) + ├╴sel1 + │ └╴v1 + └╴sel2 + └╴v1 diff --git a/tests/gold/matMul.txt b/tests/gold/matMul.txt --- a/tests/gold/matMul.txt +++ b/tests/gold/matMul.txt @@ -1,36 +1,38 @@ Lam v6 └╴Lam v5 └╴parallel - ├╴arrLength + ├╴arrLen │ └╴v6 └╴Lam v4 - └╴parallel - ├╴arrLength - │ └╴getIx - │ ├╴v5 - │ └╴0 - └╴Lam v3 - └╴forLoop - ├╴min - │ ├╴arrLength - │ │ └╴getIx - │ │ ├╴v6 - │ │ └╴v4 - │ └╴arrLength - │ └╴v5 - ├╴0.0 - └╴Lam v2 - └╴Lam v1 - └╴(+) - ├╴(*) - │ ├╴getIx - │ │ ├╴getIx - │ │ │ ├╴v6 - │ │ │ └╴v4 - │ │ └╴v2 - │ └╴getIx - │ ├╴getIx - │ │ ├╴v5 - │ │ └╴v2 - │ └╴v3 - └╴v1 + └╴Let v7 + ├╴min + │ ├╴arrLen + │ │ └╴arrIx + │ │ ├╴v6 + │ │ └╴v4 + │ └╴arrLen + │ └╴v5 + └╴parallel + ├╴arrLen + │ └╴arrIx + │ ├╴v5 + │ └╴0 + └╴Lam v3 + └╴forLoop + ├╴v7 + ├╴0.0 + └╴Lam v2 + └╴Lam v1 + └╴(+) + ├╴(*) + │ ├╴arrIx + │ │ ├╴arrIx + │ │ │ ├╴v6 + │ │ │ └╴v4 + │ │ └╴v2 + │ └╴arrIx + │ ├╴arrIx + │ │ ├╴v5 + │ │ └╴v2 + │ └╴v3 + └╴v1 diff --git a/tests/gold/scProd.txt b/tests/gold/scProd.txt --- a/tests/gold/scProd.txt +++ b/tests/gold/scProd.txt @@ -2,19 +2,19 @@ └╴Lam v3 └╴forLoop ├╴min - │ ├╴arrLength + │ ├╴arrLen │ │ └╴v4 - │ └╴arrLength + │ └╴arrLen │ └╴v3 ├╴0.0 └╴Lam v2 └╴Lam v1 └╴(+) ├╴(*) - │ ├╴getIx + │ ├╴arrIx │ │ ├╴v4 │ │ └╴v2 - │ └╴getIx + │ └╴arrIx │ ├╴v3 │ └╴v2 └╴v1 diff --git a/tests/gold/spanVec.txt b/tests/gold/spanVec.txt new file mode 100644 --- /dev/null +++ b/tests/gold/spanVec.txt @@ -0,0 +1,32 @@ +Lam v3 + └╴Let v4 + ├╴forLoop + │ ├╴arrLen + │ │ └╴v3 + │ ├╴tup2 + │ │ ├╴arrIx + │ │ │ ├╴v3 + │ │ │ └╴0 + │ │ └╴arrIx + │ │ ├╴v3 + │ │ └╴0 + │ └╴Lam v2 + │ └╴Lam v1 + │ └╴tup2 + │ ├╴min + │ │ ├╴arrIx + │ │ │ ├╴v3 + │ │ │ └╴v2 + │ │ └╴sel1 + │ │ └╴v1 + │ └╴max + │ ├╴arrIx + │ │ ├╴v3 + │ │ └╴v2 + │ └╴sel2 + │ └╴v1 + └╴(-) + ├╴sel2 + │ └╴v4 + └╴sel1 + └╴v4