-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Generic abstract syntax, and utilities for embedded languages
--
-- This library provides:
--
--
-- - Generic representation and manipulation of abstract syntax using a
-- practical encoding of open data types (based on Data Types à la Carte
-- [1])
-- - Utilities for analyzing and transforming generic syntax
-- - General variable binding constructs
-- - Utilities for building extensible embedded languages based on
-- generic syntax
-- - A small proof-of-concept implementation of the embedded language
-- Feldspar [2] (see the Examples directory)
--
--
-- Note: The library is probably mostly useful for data-flow languages,
-- such as Feldspar. Currently, it does not support cyclic programs.
--
-- [1] Data types à la carte, by Wouter Swierstra, in Journal
-- of Functional Programming, 2008
--
-- [2] http://hackage.haskell.org/package/feldspar-language
@package syntactic
@version 0.3
-- | Generic representation of typed syntax trees
--
-- As a simple demonstration, take the following simple language:
--
--
-- data Expr1 a
-- where
-- Num1 :: Int -> Expr1 Int
-- Add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
--
--
-- Using the present library, this can be rewritten as follows:
--
--
-- data Num2 a where Num2 :: Int -> Num2 (Full Int)
-- data Add2 a where Add2 :: Add2 (Int :-> Int :-> Full Int)
--
-- type Expr2 a = ASTF (Num2 :+: Add2) a
--
--
-- Note that Num2 and Add2 are non-recursive.
-- The only recursive data type here is AST, which is provided by
-- the library. Now, the important point is that Expr1 and
-- Expr2 are completely isomorphic! This is indicated by the
-- following conversions:
--
--
-- conv12 :: Expr1 a -> Expr2 a
-- conv12 (Num1 n) = inject (Num2 n)
-- conv12 (Add1 a b) = inject Add2 :$: conv12 a :$: conv12 b
--
-- conv21 :: Expr2 a -> Expr1 a
-- conv21 (project -> Just (Num2 n)) = Num1 n
-- conv21 ((project -> Just Add2) :$: a :$: b) = Add1 (conv21 a) (conv21 b)
--
--
-- A key property here is that the patterns in conv21 are
-- actually complete.
--
-- So, why should one use Expr2 instead of Expr1? The
-- answer is that Expr2 can be processed by generic algorithms
-- defined over AST, for example:
--
--
-- countNodes :: ASTF domain a -> Int
-- countNodes = count
-- where
-- count :: AST domain a -> Int
-- count (Symbol _) = 1
-- count (a :$: b) = count a + count b
--
--
-- Furthermore, although Expr2 was defined to use exactly the
-- constructors Num2 and Add2, it is possible to leave
-- the set of constructors open, leading to more modular and reusable
-- code. This can be seen by relaxing the types of conv12 and
-- conv21:
--
--
-- conv12 :: (Num2 :<: dom, Add2 :<: dom) => Expr1 a -> ASTF dom a
-- conv21 :: (Num2 :<: dom, Add2 :<: dom) => ASTF dom a -> Expr1 a
--
--
-- This way of encoding open data types is taken from Data types la
-- carte, by Wouter Swierstra, in Journal of Functional
-- Programming, 2008. However, we do not need Swierstra's fixed-point
-- machinery for recursive data types. Instead we rely on AST
-- being recursive.
module Language.Syntactic.Syntax
-- | The type of a fully applied constructor
newtype Full a
Full :: a -> Full a
result :: Full a -> a
-- | The type of a partially applied (or unapplied) constructor
newtype (:->) a b
Partial :: (a -> b) -> :-> a b
-- | Heterogeneous list, indexed by a container type and a ConsType
-- | Fully or partially applied constructor
--
-- This is a public alias for the hidden class ConsType'. The only
-- instances are:
--
--
-- instance ConsType' (Full a)
-- instance ConsType' b => ConsType' (a :-> b)
--
class ConsType' a => ConsType a
-- | Maps a ConsType to a simpler form where :-> has been
-- replaced by ->, and Full has been removed. This is
-- a public alias for the hidden type ConsEval'.
type ConsEval a = ConsEval' a
-- | Returns the result type (Full removed) of a ConsType.
-- This is a public alias for the hidden type EvalResult'.
type EvalResult a = EvalResult' a
-- | Make a constructor evaluation from a ConsEval representation
fromEval :: ConsType a => ConsEval a -> a
toEval :: ConsType a => a -> ConsEval a
-- | Convert a heterogeneous list to a normal list
listHList :: ConsType a => (forall a. c (Full a) -> b) -> HList c a -> [b]
-- | Convert a heterogeneous list to a normal list
listHListM :: (Monad m, ConsType a) => (forall a. c (Full a) -> m b) -> HList c a -> m [b]
-- | Change the container of each element in a heterogeneous list
mapHList :: ConsType a => (forall a. c1 a -> c2 a) -> HList c1 a -> HList c2 a
-- | Semantic constructor application
($:) :: (a :-> b) -> a -> b
-- | Generic abstract syntax tree, parameterized by a symbol domain
--
-- In general, (AST dom (a :-> b)) represents a
-- partially applied (or unapplied) constructor, missing at least one
-- argument, while (AST dom (Full a)) represents a
-- fully applied constructor, i.e. a complete syntax tree. It is not
-- possible to construct a total value of type (AST dom
-- a) that does not fulfill the constraint (ConsType
-- a).
--
-- Note that the hidden class ConsType' mentioned in the type of
-- Symbol is interchangeable with ConsType.
data AST dom a
Symbol :: dom a -> AST dom a
(:$:) :: AST dom (a :-> b) -> ASTF dom a -> AST dom b
-- | Fully applied abstract syntax tree
type ASTF dom a = AST dom (Full a)
-- | Co-product of two symbol domains
data (:+:) dom1 dom2 :: * -> *
InjectL :: dom1 a -> (dom1 :+: dom2) a
InjectR :: dom2 a -> (dom1 :+: dom2) a
class :<: sub sup
inject :: (:<: sub sup, ConsType a) => sub a -> sup a
project :: :<: sub sup => sup a -> Maybe (sub a)
-- | It is assumed that for all types A fulfilling
-- (Syntactic A dom):
--
--
-- eval a == eval (desugar $ (id :: A -> A) $ sugar a)
--
--
-- (using Language.Syntactic.Analysis.Evaluation.eval)
class Typeable (Internal a) => Syntactic a dom | a -> dom where { type family Internal a; }
desugar :: Syntactic a dom => a -> ASTF dom (Internal a)
sugar :: Syntactic a dom => ASTF dom (Internal a) -> a
-- | Syntactic type casting
resugar :: (Syntactic a dom, Syntactic b dom, (Internal a) ~ (Internal b)) => a -> b
-- | N-ary syntactic functions
--
-- desugarN has any type of the form:
--
--
-- desugarN ::
-- ( Syntactic a dom
-- , Syntactic b dom
-- , ...
-- , Syntactic x dom
-- ) => (a -> b -> ... -> x)
-- -> ( AST dom (Full (Internal a))
-- -> AST dom (Full (Internal b))
-- -> ...
-- -> AST dom (Full (Internal x))
-- )
--
--
-- ...and vice versa for sugarN.
class SyntacticN a internal | a -> internal
desugarN :: SyntacticN a internal => a -> internal
sugarN :: SyntacticN a internal => internal -> a
-- | Query an AST using a function that gets direct access to the
-- top-most constructor and its sub-trees
--
-- This function can be used to create AST traversal functions
-- indexed by the symbol types, for example:
--
--
-- class Count subDomain
-- where
-- count' :: Count domain => subDomain a -> HList (AST domain) a -> Int
--
-- instance (Count sub1, Count sub2) => Count (sub1 :+: sub2)
-- where
-- count' (InjectL a) args = count' a args
-- count' (InjectR a) args = count' a args
--
-- count :: Count dom => ASTF dom a -> Int
-- count = queryNode count'
--
--
-- Here, count represents some static analysis on an AST.
-- Each constructor in the tree will be queried by count'
-- indexed by the corresponding symbol type. That way, count'
-- can be seen as an open-ended function on an open data type. The
-- (Count domain) constraint on count' is to allow
-- recursion over sub-trees.
--
-- Let's say we have a symbol
--
--
-- data Add a
-- where
-- Add :: Add (Int :-> Int :-> Full Int)
--
--
-- Then the Count instance for Add might look as
-- follows:
--
--
-- instance Count Add
-- where
-- count' Add (a :*: b :*: Nil) = 1 + count a + count b
--
queryNode :: (forall a. ConsType a => dom a -> HList (AST dom) a -> b) -> ASTF dom a -> b
-- | Transform an AST using a function that gets direct access to
-- the top-most constructor and its sub-trees. This function is similar
-- to queryNode, but returns a transformed AST rather than
-- abstract interpretation.
transformNode :: (forall a. ConsType a => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a)) -> ASTF dom a -> ASTF dom' a
instance [overlap ok] Typeable1 Full
instance [overlap ok] Typeable2 :->
instance [overlap ok] Eq a => Eq (Full a)
instance [overlap ok] Show a => Show (Full a)
instance [overlap ok] (ia ~ Internal a, Syntactic a dom, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib)
instance [overlap ok] (ia ~ AST dom (Full (Internal a)), Syntactic a dom) => SyntacticN a ia
instance [overlap ok] Typeable a => Syntactic (ASTF dom a) dom
instance [overlap ok] expr1 :<: expr3 => expr1 :<: (expr2 :+: expr3)
instance [overlap ok] expr1 :<: (expr1 :+: expr2)
instance [overlap ok] expr :<: expr
instance [overlap ok] sub :<: sup => sub :<: AST sup
instance [overlap ok] ConsType' a => ConsType a
instance [overlap ok] ConsType' b => ConsType' (a :-> b)
instance [overlap ok] ConsType' (Full a)
module Language.Syntactic.Analysis.Equality
-- | Equality for expressions. The difference between Eq and
-- ExprEq is that ExprEq allows comparison of expressions
-- with different value types. It is assumed that when the types differ,
-- the expressions also differ. The reason for allowing comparison of
-- different types is that this is convenient when the types are
-- existentially quantified.
class ExprEq expr
exprEq :: ExprEq expr => expr a -> expr b -> Bool
eqSyn :: (Syntactic a dom, ExprEq dom) => a -> a -> Bool
instance (ExprEq expr1, ExprEq expr2) => Eq ((:+:) expr1 expr2 a)
instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2)
instance ExprEq dom => Eq (AST dom a)
instance ExprEq dom => ExprEq (AST dom)
module Language.Syntactic.Analysis.Render
-- | Render an expression as concrete syntax. A complete instance must
-- define either of the methods render and renderPart.
class Render expr
render :: Render expr => expr a -> String
renderPart :: Render expr => [String] -> expr a -> String
-- | Print an expression
printExpr :: Render expr => expr a -> IO ()
class Render expr => ToTree expr
toTreePart :: ToTree expr => [Tree String] -> expr a -> Tree String
-- | Show syntax tree using ASCII art
showAST :: ToTree dom => AST dom a -> String
-- | Print syntax tree using ASCII art
drawAST :: ToTree dom => AST dom a -> IO ()
instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2)
instance ToTree dom => ToTree (AST dom)
instance (Render expr1, Render expr2) => Show ((:+:) expr1 expr2 a)
instance (Render expr1, Render expr2) => Render (expr1 :+: expr2)
instance Render dom => Show (AST dom a)
instance Render dom => Render (AST dom)
module Language.Syntactic.Analysis.Evaluation
class Eval expr
evaluate :: Eval expr => expr a -> a
evalFull :: Eval dom => ASTF dom a -> a
evalSyn :: (Syntactic a dom, Eval dom) => a -> Internal a
instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)
instance Eval dom => Eval (AST dom)
module Language.Syntactic.Analysis.Hash
class ExprEq expr => ExprHash expr
exprHash :: ExprHash expr => expr a -> Hash
instance (ExprHash expr1, ExprHash expr2) => ExprHash (expr1 :+: expr2)
instance ExprHash dom => ExprHash (AST dom)
-- | Annotations for syntax trees
module Language.Syntactic.Features.Annotate
-- | Annotating an expression with arbitrary information.
--
-- This can be used to annotate every node of a syntax tree, which is
-- done by changing
--
--
-- AST dom a
--
--
-- to
--
--
-- AST (Ann info dom) a
--
--
-- Injection/projection of an annotated tree is done using
-- injectAnn / projectAnn.
data Ann info expr a
Ann :: info (EvalResult a) -> expr a -> Ann info expr a
annInfo :: Ann info expr a -> info (EvalResult a)
annExpr :: Ann info expr a -> expr a
type AnnSTF info dom a = ASTF (Ann info dom) a
injectAnn :: (:<: sub sup, ConsType a) => info (EvalResult a) -> sub a -> AST (Ann info sup) a
projectAnn :: :<: sub sup => AST (Ann info sup) a -> Maybe (info (EvalResult a), sub a)
getInfo :: AST (Ann info sup) a -> info (EvalResult a)
instance ExprHash expr => ExprHash (Ann info expr)
instance Eval expr => Eval (Ann info expr)
instance ToTree expr => ToTree (Ann info expr)
instance Render expr => Render (Ann info expr)
instance ExprEq expr => ExprEq (Ann info expr)
-- | The syntactic library
--
-- The basic functionality is provided by the module
-- Language.Syntactic.Syntax.
module Language.Syntactic
-- | Literal expressions
module Language.Syntactic.Features.Literal
data Literal a
Literal :: a -> Literal (Full a)
-- | Literal
lit :: (Eq a, Show a, Typeable a, :<: Literal dom) => a -> ASTF dom a
-- | Annotated literal
litAnn :: (Eq a, Show a, Typeable a, :<: Literal dom) => info a -> a -> AnnSTF info dom a
instance ExprHash Literal
instance Eval Literal
instance ToTree Literal
instance Render Literal
instance ExprEq Literal
-- | Primitive functions
module Language.Syntactic.Features.PrimFunc
data PrimFunc a
PrimFunc :: String -> (ConsEval (a :-> b)) -> PrimFunc (a :-> b)
primFunc1 :: (Typeable a, :<: PrimFunc dom) => String -> (a -> b) -> ASTF dom a -> ASTF dom b
primFunc2 :: (Typeable a, Typeable b, :<: PrimFunc dom) => String -> (a -> b -> c) -> ASTF dom a -> ASTF dom b -> ASTF dom c
primFunc3 :: (Typeable a, Typeable b, Typeable c, :<: PrimFunc dom) => String -> (a -> b -> c -> d) -> ASTF dom a -> ASTF dom b -> ASTF dom c -> ASTF dom d
primFunc4 :: (Typeable a, Typeable b, Typeable c, Typeable d, :<: PrimFunc dom) => String -> (a -> b -> c -> d -> e) -> ASTF dom a -> ASTF dom b -> ASTF dom c -> ASTF dom d -> ASTF dom e
primFuncAnn1 :: (Typeable a, :<: PrimFunc dom) => String -> (a -> b) -> info b -> AnnSTF info dom a -> AnnSTF info dom b
primFuncAnn2 :: (Typeable a, Typeable b, :<: PrimFunc dom) => String -> (a -> b -> c) -> info c -> AnnSTF info dom a -> AnnSTF info dom b -> AnnSTF info dom c
primFuncAnn3 :: (Typeable a, Typeable b, Typeable c, :<: PrimFunc dom) => String -> (a -> b -> c -> d) -> info d -> AnnSTF info dom a -> AnnSTF info dom b -> AnnSTF info dom c -> AnnSTF info dom d
primFuncAnn4 :: (Typeable a, Typeable b, Typeable c, Typeable d, :<: PrimFunc dom) => String -> (a -> b -> c -> d -> e) -> info e -> AnnSTF info dom a -> AnnSTF info dom b -> AnnSTF info dom c -> AnnSTF info dom d -> AnnSTF info dom e
-- | Class of expressions that can be treated as primitive functions
class IsFunction expr
toFunction :: IsFunction expr => expr a -> PrimFunc a
-- | Default implementation of exprEq
exprEqFunc :: IsFunction expr => expr a -> expr b -> Bool
-- | Default implementation of renderPart
renderPartFunc :: IsFunction expr => [String] -> expr a -> String
-- | Default implementation of evaluate
evaluateFunc :: IsFunction expr => expr a -> a
-- | Default implementation of exprHash
exprHashFunc :: IsFunction expr => expr a -> Hash
instance ExprHash PrimFunc
instance Eval PrimFunc
instance ToTree PrimFunc
instance Render PrimFunc
instance ExprEq PrimFunc
-- | Conditional expressions
module Language.Syntactic.Features.Condition
data Condition a
Condition :: Condition (Bool :-> (a :-> (a :-> Full a)))
-- | Conditional expression
condition :: (:<: Condition dom, Syntactic a dom) => ASTF dom Bool -> a -> a -> a
instance ExprHash Condition
instance Eval Condition
instance ToTree Condition
instance Render Condition
instance ExprEq Condition
-- | Construction and selection of tuples
module Language.Syntactic.Features.Tuple
-- | Expressions for constructing tuples
data Tuple a
Tup2 :: Tuple (a :-> (b :-> Full (a, b)))
Tup3 :: Tuple (a :-> (b :-> (c :-> Full (a, b, c))))
Tup4 :: Tuple (a :-> (b :-> (c :-> (d :-> Full (a, b, c, d)))))
Tup5 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> Full (a, b, c, d, e))))))
Tup6 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> Full (a, b, c, d, e, f)))))))
Tup7 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> Full (a, b, c, d, e, f, g))))))))
-- | Expressions for selecting elements of a tuple
data Select a
Sel1 :: Select (a :-> Full b)
Sel2 :: Select (a :-> Full b)
Sel3 :: Select (a :-> Full b)
Sel4 :: Select (a :-> Full b)
Sel5 :: Select (a :-> Full b)
Sel6 :: Select (a :-> Full b)
Sel7 :: Select (a :-> Full b)
-- | Return the selected position, e.g.
--
--
-- selectPos (Sel3 :: Select ((Int,Int,Int,Int) -> Int)) = 3
--
selectPos :: Select a -> Int
instance ToTree Select
instance ExprHash Select
instance Eval Select
instance Render Select
instance ExprEq Select
instance IsFunction Select
instance ToTree Tuple
instance ExprHash Tuple
instance Eval Tuple
instance Render Tuple
instance ExprEq Tuple
instance IsFunction Tuple
-- | Syntactic instances for tuples
module Language.Syntactic.Features.TupleSyntactic
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Syntactic g dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b, c, d, e, f, g) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b, c, d, e, f) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b, c, d, e) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b, c, d) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b, c) dom
instance (Syntactic a dom, Syntactic b dom, Tuple :<: dom, Select :<: dom) => Syntactic (a, b) dom
-- | General binding constructs
module Language.Syntactic.Features.Binding
-- | Variable identifier
newtype VarId
VarId :: Integer -> VarId
varInteger :: VarId -> Integer
showVar :: VarId -> String
-- | Variables
data Variable a
Variable :: VarId -> Variable (Full a)
-- | Lambda binding
data Lambda a
Lambda :: VarId -> Lambda (b :-> Full (a -> b))
-- | Alpha-equivalence on Lambda expressions. Free variables are
-- taken to be equvalent if they have the same identifier.
eqLambdaM :: ExprEq dom => AST (Lambda :+: (Variable :+: dom)) a -> AST (Lambda :+: (Variable :+: dom)) b -> Reader [(VarId, VarId)] Bool
eqLambda :: ExprEq dom => AST (Lambda :+: (Variable :+: dom)) a -> AST (Lambda :+: (Variable :+: dom)) b -> Bool
-- | Evaluation of possibly open LambdaAST expressions
evalLambdaM :: (Eval dom, MonadReader [(VarId, Dynamic)] m) => ASTF (Lambda :+: (Variable :+: dom)) a -> m a
-- | Evaluation of closed Lambda expressions
evalLambda :: Eval dom => ASTF (Lambda :+: (Variable :+: dom)) a -> a
-- | The class of n-ary binding functions
class NAry a dom | a -> dom where { type family NAryEval a; }
bindN :: NAry a dom => (forall b c. (Typeable b, Typeable c) => (ASTF dom b -> ASTF dom c) -> ASTF dom (b -> c)) -> a -> ASTF dom (NAryEval a)
-- | Let binding
data Let a
Let :: Let (a :-> ((a -> b) :-> Full b))
instance Eq VarId
instance Ord VarId
instance Num VarId
instance Enum VarId
instance Ix VarId
instance ExprHash Let
instance Eval Let
instance ToTree Let
instance Render Let
instance ExprEq Let
instance (Typeable a, NAry b dom, Typeable (NAryEval b)) => NAry (ASTF dom a -> b) dom
instance NAry (ASTF dom a) dom
instance ToTree Lambda
instance Render Lambda
instance ToTree Variable
instance Render Variable
instance Show VarId
-- | This module provides binding constructs using higher-order syntax and
-- a function for translating back to first-order syntax. Expressions
-- constructed using the exported interface are guaranteed to have a
-- well-behaved translation.
module Language.Syntactic.Features.Binding.HigherOrder
-- | Variables
data Variable a
-- | Evaluation of closed Lambda expressions
evalLambda :: Eval dom => ASTF (Lambda :+: (Variable :+: dom)) a -> a
-- | Let binding
data Let a
Let :: Let (a :-> ((a -> b) :-> Full b))
-- | Higher-order lambda binding
data HOLambda dom a
HOLambda :: (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOLambda dom (Full (a -> b))
type HOAST dom = AST (HOLambda dom :+: (Variable :+: dom))
-- | Lambda binding
lambda :: (Typeable a, Typeable b) => (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full (a -> b))
-- | N-ary lambda binding
lambdaN :: NAry a (HOLambda dom :+: (Variable :+: dom)) => a -> HOAST dom (Full (NAryEval a))
-- | Let binding
let_ :: (Typeable a, Typeable b, :<: Let dom) => HOAST dom (Full a) -> (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full b)
reifyM :: Typeable a => HOAST dom a -> State VarId (AST (Lambda :+: (Variable :+: dom)) a)
-- | Translating expressions with higher-order binding to corresponding
-- expressions using first-order binding
reifyHOAST :: Typeable a => HOAST dom a -> AST (Lambda :+: (Variable :+: dom)) a
-- | Convenient class alias for n-ary syntactic functions
class (SyntacticN a internal, NAry internal (HOLambda dom :+: (Variable :+: dom)), Typeable (NAryEval internal)) => Reifiable a dom internal | a -> dom internal
-- | Reifying an n-ary syntactic function
reify :: Reifiable a dom internal => a -> ASTF (Lambda :+: (Variable :+: dom)) (NAryEval internal)
instance (SyntacticN a internal, NAry internal (HOLambda dom :+: (Variable :+: dom)), Typeable (NAryEval internal)) => Reifiable a dom internal