-- 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 functional
-- object 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.5
-- | Some utility functions used by the other modules
module Language.Syntactic.Sharing.Utils
-- | Difference list
type DList a = [a] -> [a]
-- | Empty list
empty :: DList a
-- | Singleton list
single :: a -> DList a
fromDList :: DList a -> [a]
-- | Given a list is of unique natural numbers, returns a function
-- that maps each number in is to a unique number in the range
-- [0 .. length is-1]. The complexity is O(maximum is).
reindex :: (Integral a, Ix a) => [a] -> a -> a
-- | Count the number of occurrences of each element in the list. The
-- result is an array mapping each element to its number of occurrences.
count :: Ix a => (a, a) -> [a] -> Array a Int
-- | Partitions the list such that two elements are in the same sub-list if
-- and only if they satisfy the equivalence check. The complexity is
-- O(n^2).
fullPartition :: (a -> a -> Bool) -> [a] -> [[a]]
-- | 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 (Wouter Swierstra, Journal of Functional Programming,
-- 2008). However, we do not need Swierstra's fixed-point machinery for
-- recursive data types. Instead we rely on AST being recursive.
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
-- | A witness of (ConsType a)
data ConsWit a
ConsWit :: ConsWit a
-- | Expressions in syntactic are supposed to have the form
-- (ConsType a => expr a). This class lets us witness
-- the ConsType constraint of an expression without examining the
-- expression.
class WitnessCons expr
witnessCons :: WitnessCons expr => expr a -> ConsWit 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 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a
-- | Apply the syntax tree to listed arguments
appHList :: ConsType a => AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult 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
-- | Like queryNode but with the result indexed by the constructor's
-- result type
queryNodeI :: (forall a. ConsType a => dom a -> HList (AST dom) a -> b (EvalResult a)) -> ASTF dom a -> b 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
-- | An abstract representation of a constraint on a. An instance
-- might look as follows:
--
--
-- instance MyClass a => Sat MyContext a
-- where
-- data Witness MyContext a = MyClass a => MyWitness
-- witness = MyWitness
--
--
-- This allows us to use (Sat MyContext a) instead of
-- (MyClass a). The point with this is that MyContext
-- can be provided as a parameter, so this effectively allows us to
-- parameterize on class constraints. Note that the existential context
-- in the data definition is important. This means that, given a
-- constraint (Sat MyContext a), we can always construct
-- the context (MyClass a) by calling the witness method
-- (the class instance only declares the reverse relationship).
--
-- This way of parameterizing over type classes was inspired by
-- Restricted Data Types in Haskell (John Hughes, Haskell
-- Workshop, 1999).
class Sat ctx a where { data family Witness ctx a; }
witness :: Sat ctx a => Witness ctx a
-- | Witness of a (Sat ctx a) constraint. This is different
-- from (Witness ctx a), which witnesses the class
-- encoded by ctx. Witness' has a single constructor for
-- all contexts, while Witness has different constructors for
-- different contexts.
data Witness' ctx a
Witness' :: Witness' ctx a
witness' :: Witness' ctx a -> Witness ctx a
-- | Symbols that act as witnesses of their result type
class WitnessSat sym where { type family Context sym; }
witnessSat :: WitnessSat sym => sym a -> Witness' (Context sym) (EvalResult a)
-- | Type application for constraining the ctx type of a
-- parameterized symbol
withContext :: sym ctx a -> Proxy ctx -> sym ctx a
-- | Representation of a fully polymorphic constraint -- i.e.
-- (Sat Poly a) is satisfied by all types
-- a.
data Poly
poly :: Proxy Poly
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] Sat Poly 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
exprHash :: ExprEq expr => expr a -> Hash
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
instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)
instance Eval dom => Eval (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)
-- | Get the annotation of the top-level node
getInfo :: AST (Ann info dom) a -> info (EvalResult a)
-- | Collect the annotations of all nodes
collectInfo :: (forall a. info a -> b) -> AST (Ann info dom) a -> [b]
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
-- | Simple symbols
--
-- Sym provides a simple way to make syntactic symbols for
-- prototyping. However, note that Sym is quite unsafe as it only
-- uses String to distinguish between different symbols. Also,
-- Sym has a very free type that allows any number of arguments.
module Language.Syntactic.Features.Symbol
data Sym a
Sym :: String -> ConsEval a -> Sym a
-- | A zero-argument symbol
sym0 :: (Typeable a, :<: Sym dom) => String -> a -> ASTF dom a
-- | A one-argument symbol
sym1 :: (Typeable a, :<: Sym dom) => String -> (a -> b) -> ASTF dom a -> ASTF dom b
-- | A two-argument symbol
sym2 :: (Typeable a, Typeable b, :<: Sym dom) => String -> (a -> b -> c) -> ASTF dom a -> ASTF dom b -> ASTF dom c
-- | A three-argument symbol
sym3 :: (Typeable a, Typeable b, Typeable c, :<: Sym dom) => String -> (a -> b -> c -> d) -> ASTF dom a -> ASTF dom b -> ASTF dom c -> ASTF dom d
-- | A four-argument symbol
sym4 :: (Typeable a, Typeable b, Typeable c, Typeable d, :<: Sym dom) => String -> (a -> b -> c -> d -> e) -> ASTF dom a -> ASTF dom b -> ASTF dom c -> ASTF dom d -> ASTF dom e
-- | Class of expressions that can be treated as symbols
class IsSymbol expr
toSym :: IsSymbol expr => expr a -> Sym a
-- | Default implementation of exprEq
exprEqFunc :: IsSymbol expr => expr a -> expr b -> Bool
-- | Default implementation of exprHash
exprHashFunc :: IsSymbol expr => expr a -> Hash
-- | Default implementation of renderPart
renderPartFunc :: IsSymbol expr => [String] -> expr a -> String
-- | Default implementation of evaluate
evaluateFunc :: IsSymbol expr => expr a -> a
instance Eval Sym
instance ToTree Sym
instance Render Sym
instance ExprEq Sym
instance WitnessCons Sym
-- | Literal expressions
module Language.Syntactic.Features.Literal
data Literal ctx a
Literal :: a -> Literal ctx (Full a)
-- | Literal with explicit context
litCtx :: (Eq a, Show a, Typeable a, Sat ctx a, :<: (Literal ctx) dom) => Proxy ctx -> a -> ASTF dom a
-- | Literal
lit :: (Eq a, Show a, Typeable a, :<: (Literal Poly) dom) => a -> ASTF dom a
-- | Partial literal projection with explicit context
prjLiteral :: :<: (Literal ctx) sup => Proxy ctx -> sup a -> Maybe (Literal ctx a)
instance Eval (Literal ctx)
instance ToTree (Literal ctx)
instance Render (Literal ctx)
instance ExprEq (Literal ctx)
instance WitnessSat (Literal ctx)
instance WitnessCons (Literal ctx)
-- | Conditional expressions
module Language.Syntactic.Features.Condition
data Condition ctx a
Condition :: Condition ctx (Bool :-> (a :-> (a :-> Full a)))
-- | Conditional expression with explicit context
conditionCtx :: (Sat ctx (Internal a), Syntactic a dom, :<: (Condition ctx) dom) => Proxy ctx -> ASTF dom Bool -> a -> a -> a
-- | Conditional expression
condition :: (:<: (Condition Poly) dom, Syntactic a dom) => ASTF dom Bool -> a -> a -> a
-- | Partial Condition projection with explicit context
prjCondition :: :<: (Condition ctx) sup => Proxy ctx -> sup a -> Maybe (Condition ctx a)
instance Eval (Condition ctx)
instance ToTree (Condition ctx)
instance Render (Condition ctx)
instance ExprEq (Condition ctx)
instance WitnessSat (Condition ctx)
instance WitnessCons (Condition ctx)
-- | Construction and projection of tuples in the object language
--
-- The function pairs desugarTupX/sugarTupX could be
-- used directly in Syntactic instances if it wasn't for the extra
-- (Proxy ctx) arguments. For this reason,
-- Syntactic instances have to be written manually for each
-- context. The module
-- Language.Syntactic.Features.TupleSyntacticPoly provides
-- instances for a Poly context. The exact same code can be used
-- to make instances for other contexts -- just copy/paste and replace
-- Poly and poly with the desired context (and probably add
-- an extra constraint in the class contexts).
module Language.Syntactic.Features.Tuple
-- | Expressions for constructing tuples
data Tuple ctx a
Tup2 :: Tuple ctx (a :-> (b :-> Full (a, b)))
Tup3 :: Tuple ctx (a :-> (b :-> (c :-> Full (a, b, c))))
Tup4 :: Tuple ctx (a :-> (b :-> (c :-> (d :-> Full (a, b, c, d)))))
Tup5 :: Tuple ctx (a :-> (b :-> (c :-> (d :-> (e :-> Full (a, b, c, d, e))))))
Tup6 :: Tuple ctx (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> Full (a, b, c, d, e, f)))))))
Tup7 :: Tuple ctx (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> Full (a, b, c, d, e, f, g))))))))
-- | Partial Tuple projection with explicit context
prjTuple :: :<: (Tuple ctx) sup => Proxy ctx -> sup a -> Maybe (Tuple ctx a)
desugarTup2 :: (Syntactic a dom, Syntactic b dom, Sat ctx (Internal a, Internal b), :<: (Tuple ctx) dom) => Proxy ctx -> (a, b) -> ASTF dom (Internal a, Internal b)
desugarTup3 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Sat ctx (Internal a, Internal b, Internal c), :<: (Tuple ctx) dom) => Proxy ctx -> (a, b, c) -> ASTF dom (Internal a, Internal b, Internal c)
desugarTup4 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Sat ctx (Internal a, Internal b, Internal c, Internal d), :<: (Tuple ctx) dom) => Proxy ctx -> (a, b, c, d) -> ASTF dom (Internal a, Internal b, Internal c, Internal d)
desugarTup5 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e), :<: (Tuple ctx) dom) => Proxy ctx -> (a, b, c, d, e) -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)
desugarTup6 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f), :<: (Tuple ctx) dom) => Proxy ctx -> (a, b, c, d, e, f) -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)
desugarTup7 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Syntactic g dom, Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g), :<: (Tuple ctx) dom) => Proxy ctx -> (a, b, c, d, e, f, g) -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)
-- | Expressions for selecting elements of a tuple
data Select ctx a
Sel1 :: Select ctx (a :-> Full b)
Sel2 :: Select ctx (a :-> Full b)
Sel3 :: Select ctx (a :-> Full b)
Sel4 :: Select ctx (a :-> Full b)
Sel5 :: Select ctx (a :-> Full b)
Sel6 :: Select ctx (a :-> Full b)
Sel7 :: Select ctx (a :-> Full b)
-- | Partial Select projection with explicit context
prjSelect :: :<: (Select ctx) sup => Proxy ctx -> sup a -> Maybe (Select ctx a)
-- | Return the selected position, e.g.
--
--
-- selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3
--
selectPos :: Select ctx a -> Int
sugarTup2 :: (Syntactic a dom, Syntactic b dom, Sat ctx (Internal a), Sat ctx (Internal b), :<: (Select ctx) dom) => Proxy ctx -> ASTF dom (Internal a, Internal b) -> (a, b)
sugarTup3 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), :<: (Select ctx) dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c) -> (a, b, c)
sugarTup4 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), :<: (Select ctx) dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d) -> (a, b, c, d)
sugarTup5 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), Sat ctx (Internal e), :<: (Select ctx) dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e) -> (a, b, c, d, e)
sugarTup6 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), Sat ctx (Internal e), Sat ctx (Internal f), :<: (Select ctx) dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) -> (a, b, c, d, e, f)
sugarTup7 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Syntactic g dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), Sat ctx (Internal e), Sat ctx (Internal f), Sat ctx (Internal g), :<: (Select ctx) dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) -> (a, b, c, d, e, f, g)
instance ToTree (Select ctx)
instance Eval (Select ctx)
instance Render (Select ctx)
instance ExprEq (Select ctx)
instance IsSymbol (Select ctx)
instance WitnessSat (Select ctx)
instance WitnessCons (Select ctx)
instance ToTree (Tuple ctx)
instance Eval (Tuple ctx)
instance Render (Tuple ctx)
instance ExprEq (Tuple ctx)
instance IsSymbol (Tuple ctx)
instance WitnessSat (Tuple ctx)
instance WitnessCons (Tuple ctx)
-- | Syntactic instances for tuples with Poly context
module Language.Syntactic.Features.TupleSyntacticPoly
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Syntactic g dom, Tuple Poly :<: dom, Select Poly :<: dom) => Syntactic (a, b, c, d, e, f, g) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Tuple Poly :<: dom, Select Poly :<: dom) => Syntactic (a, b, c, d, e, f) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Tuple Poly :<: dom, Select Poly :<: dom) => Syntactic (a, b, c, d, e) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Tuple Poly :<: dom, Select Poly :<: dom) => Syntactic (a, b, c, d) dom
instance (Syntactic a dom, Syntactic b dom, Syntactic c dom, Tuple Poly :<: dom, Select Poly :<: dom) => Syntactic (a, b, c) dom
instance (Syntactic a dom, Syntactic b dom, Tuple Poly :<: dom, Select Poly :<: 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 ctx a
Variable :: VarId -> Variable ctx (Full a)
-- | Partial Variable projection with explicit context
prjVariable :: :<: (Variable ctx) sup => Proxy ctx -> sup a -> Maybe (Variable ctx a)
-- | Lambda binding
data Lambda ctx a
Lambda :: VarId -> Lambda ctx (b :-> Full (a -> b))
-- | Partial Lambda projection with explicit context
prjLambda :: :<: (Lambda ctx) sup => Proxy ctx -> sup a -> Maybe (Lambda ctx a)
-- | Alpha equivalence in an environment of variable equivalences. The
-- supplied equivalence function gets called when the argument
-- expressions are not both Variables, both Lambdas or both
-- :$:.
alphaEqM :: (:<: (Lambda ctx) dom, :<: (Variable ctx) dom) => Proxy ctx -> (forall a b. AST dom a -> AST dom b -> Reader [(VarId, VarId)] Bool) -> (forall a b. AST dom a -> AST dom b -> Reader [(VarId, VarId)] Bool)
-- | Alpha-equivalence on lambda expressions. Free variables are taken to
-- be equivalent if they have the same identifier.
alphaEq :: (:<: (Lambda ctx) dom, :<: (Variable ctx) dom, ExprEq dom) => Proxy ctx -> AST dom a -> AST dom b -> Bool
-- | Evaluation of possibly open lambda expressions
evalLambdaM :: (Eval dom, MonadReader [(VarId, Dynamic)] m) => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> m a
-- | Evaluation of closed lambda expressions
evalLambda :: Eval dom => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> a
-- | The class of n-ary binding functions
class NAry ctx a dom | a -> dom where { type family NAryEval a; }
bindN :: NAry ctx a dom => Proxy ctx -> (forall b c. (Typeable b, Typeable c, Sat ctx b) => (ASTF dom b -> ASTF dom c) -> ASTF dom (b -> c)) -> a -> ASTF dom (NAryEval a)
-- | Let binding
--
-- A Let expression is really just an application of a lambda
-- binding (the argument (a -> b) is preferably constructed
-- by Lambda).
data Let ctxa ctxb a
Let :: Let ctxa ctxb (a :-> ((a -> b) :-> Full b))
-- | Partial Let projection with explicit context
prjLet :: :<: (Let ctxa ctxb) sup => Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)
instance Eq VarId
instance Ord VarId
instance Num VarId
instance Real VarId
instance Integral VarId
instance Enum VarId
instance Ix VarId
instance Eval (Let ctxa ctxb)
instance ToTree (Let ctxa ctxb)
instance Render (Let ctxa ctxb)
instance ExprEq (Let ctxa ctxb)
instance WitnessSat (Let ctxa ctxb)
instance WitnessCons (Let ctxa ctxb)
instance (Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) => NAry ctx (ASTF dom a -> b) dom
instance Sat ctx a => NAry ctx (ASTF dom a) dom
instance ToTree (Lambda ctx)
instance Render (Lambda ctx)
instance ExprEq (Lambda ctx)
instance WitnessCons (Lambda ctx)
instance ToTree (Variable ctx)
instance Render (Variable ctx)
instance ExprEq (Variable ctx)
instance WitnessSat (Variable ctx)
instance WitnessCons (Variable ctx)
instance Show VarId
-- | This module provides binding constructs using higher-order syntax and
-- a function for translating to first-order syntax. Expressions
-- constructed using the exported interface are guaranteed to have a
-- well-behaved translation.
module Language.Syntactic.Features.Binding.HigherOrder
-- | Variables
data Variable ctx a
-- | Evaluation of closed lambda expressions
evalLambda :: Eval dom => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> a
-- | Let binding
--
-- A Let expression is really just an application of a lambda
-- binding (the argument (a -> b) is preferably constructed
-- by Lambda).
data Let ctxa ctxb a
Let :: Let ctxa ctxb (a :-> ((a -> b) :-> Full b))
-- | Higher-order lambda binding
data HOLambda ctx dom a
HOLambda :: (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOLambda ctx dom (Full (a -> b))
type HOAST ctx dom = AST (HOLambda ctx dom :+: (Variable ctx :+: dom))
type HOASTF ctx dom a = HOAST ctx dom (Full a)
-- | Lambda binding
lambda :: (Typeable a, Typeable b, Sat ctx a) => (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOASTF ctx dom (a -> b)
-- | N-ary lambda binding
lambdaN :: NAry ctx a (HOLambda ctx dom :+: (Variable ctx :+: dom)) => a -> HOASTF ctx dom (NAryEval a)
-- | Let binding with explicit context
letBindCtx :: (Typeable a, Typeable b, :<: (Let ctxa ctxb) dom, Sat ctxa a, Sat ctxb b) => Proxy ctxb -> HOASTF ctxa dom a -> (HOASTF ctxa dom a -> HOASTF ctxa dom b) -> HOASTF ctxa dom b
-- | Let binding
letBind :: (Typeable a, Typeable b, :<: (Let Poly Poly) dom) => HOASTF Poly dom a -> (HOASTF Poly dom a -> HOASTF Poly dom b) -> HOASTF Poly dom b
reifyM :: Typeable a => HOAST ctx dom a -> State VarId (AST (Lambda ctx :+: (Variable ctx :+: dom)) a)
-- | Translating expressions with higher-order binding to corresponding
-- expressions using first-order binding
reifyTop :: Typeable a => HOAST ctx dom a -> AST (Lambda ctx :+: (Variable ctx :+: dom)) a
-- | Convenient class alias for n-ary syntactic functions
class (SyntacticN a internal, NAry ctx internal (HOLambda ctx dom :+: (Variable ctx :+: dom)), Typeable (NAryEval internal)) => Reifiable ctx a dom internal | a -> dom internal
-- | Reifying an n-ary syntactic function with explicit context
reifyCtx :: Reifiable ctx a dom internal => Proxy ctx -> a -> ASTF (Lambda ctx :+: (Variable ctx :+: dom)) (NAryEval internal)
-- | Reifying an n-ary syntactic function
reify :: Reifiable Poly a dom internal => a -> ASTF (Lambda Poly :+: (Variable Poly :+: dom)) (NAryEval internal)
instance (SyntacticN a internal, NAry ctx internal (HOLambda ctx dom :+: (Variable ctx :+: dom)), Typeable (NAryEval internal)) => Reifiable ctx a dom internal
instance WitnessCons (HOLambda ctx dom)
-- | Representation and manipulation of abstract syntax graphs
module Language.Syntactic.Sharing.Graph
-- | Node identifier
newtype NodeId
NodeId :: Integer -> NodeId
nodeInteger :: NodeId -> Integer
-- | Placeholder for a syntax tree
data Node ctx a
Node :: NodeId -> Node ctx (Full a)
showNode :: NodeId -> String
-- | Partial Node projection with explicit context
prjNode :: :<: (Node ctx) sup => Proxy ctx -> sup a -> Maybe (Node ctx a)
-- | An ASTF with hidden result type
data SomeAST dom
SomeAST :: ASTF dom a -> SomeAST dom
-- | "Abstract Syntax Graph"
--
-- A representation of a syntax tree with explicit sharing. An ASG
-- is valid if and only if inlineAll succeeds (and the
-- numNodes field is correct).
data ASG ctx dom a
ASG :: ASTF (Node ctx :+: dom) a -> [(NodeId, SomeAST (Node ctx :+: dom))] -> NodeId -> ASG ctx dom a
-- | Top-level expression
topExpression :: ASG ctx dom a -> ASTF (Node ctx :+: dom) a
-- | Mapping from node id to sub-expression
graphNodes :: ASG ctx dom a -> [(NodeId, SomeAST (Node ctx :+: dom))]
-- | Total number of nodes
numNodes :: ASG ctx dom a -> NodeId
-- | Show syntax graph using ASCII art
showASG :: ToTree dom => ASG ctx dom a -> String
-- | Print syntax graph using ASCII art
drawASG :: ToTree dom => ASG ctx dom a -> IO ()
-- | Update the node identifiers in an AST using the supplied
-- reindexing function
reindexNodesAST :: (NodeId -> NodeId) -> AST (Node ctx :+: dom) a -> AST (Node ctx :+: dom) a
-- | Reindex the nodes according to the given index mapping. The number of
-- nodes is unchanged, so if the index mapping is not 1:1, the resulting
-- graph will contain duplicates.
reindexNodes :: (NodeId -> NodeId) -> ASG ctx dom a -> ASG ctx dom a
-- | Reindex the nodes to be in the range [0 .. l-1], where
-- l is the number of nodes in the graph
reindexNodesFrom0 :: ASG ctx dom a -> ASG ctx dom a
-- | Remove duplicate nodes from a graph. The function only looks at the
-- NodeId of each node. The numNodes field is updated
-- accordingly.
nubNodes :: ASG ctx dom a -> ASG ctx dom a
liftSome2 :: (forall a b. ASTF (Node ctx :+: dom) a -> ASTF (Node ctx :+: dom) b -> c) -> SomeAST (Node ctx :+: dom) -> SomeAST (Node ctx :+: dom) -> c
-- | Pattern functor representation of an AST with Nodes
data SyntaxPF dom a
AppPF :: a -> a -> SyntaxPF dom a
NodePF :: NodeId -> a -> SyntaxPF dom a
DomPF :: dom b -> SyntaxPF dom a
-- | Folding over a graph
--
-- The user provides a function to fold a single constructor (an
-- "algebra"). The result contains the result of folding the whole graph
-- as well as the result of each internal node, represented both as an
-- array and an association list. Each node is processed exactly once.
foldGraph :: (SyntaxPF dom b -> b) -> ASG ctx dom a -> (b, (Array NodeId b, [(NodeId, b)]))
-- | Convert an ASG to an AST by inlining all nodes
inlineAll :: Typeable a => ASG ctx dom a -> ASTF dom a
-- | Find the child nodes of each node in an expression. The child nodes of
-- a node n are the first nodes along all paths from n.
nodeChildren :: ASG ctx dom a -> [(NodeId, [NodeId])]
-- | Count the number of occurrences of each node in an expression
occurrences :: ASG ctx dom a -> Array NodeId Int
-- | Inline all nodes that are not shared
inlineSingle :: Typeable a => ASG ctx dom a -> ASG ctx dom a
-- | Compute a table (both array and list representation) of hash values
-- for each node
hashNodes :: ExprEq dom => ASG ctx dom a -> (Array NodeId Hash, [(NodeId, Hash)])
-- | Partitions the nodes such that two nodes are in the same sub-list if
-- and only if they are alpha-equivalent.
partitionNodes :: (:<: (Lambda ctx) dom, :<: (Variable ctx) dom, ExprEq dom) => ASG ctx dom a -> [[NodeId]]
-- | Common sub-expression elimination based on alpha-equivalence
cse :: (:<: (Lambda ctx) dom, :<: (Variable ctx) dom, ExprEq dom) => ASG ctx dom a -> ASG ctx dom a
instance Eq NodeId
instance Ord NodeId
instance Num NodeId
instance Real NodeId
instance Integral NodeId
instance Enum NodeId
instance Ix NodeId
instance Functor (SyntaxPF dom)
instance ToTree (Node ctx)
instance Render (Node ctx)
instance WitnessCons (Node ctx)
instance Show NodeId
module Language.Syntactic.Sharing.StableName
-- | StableName of a (c (Full a)) with hidden result
-- type
data StName c
StName :: StableName (c (Full a)) -> StName c
stCast :: (Typeable a, Typeable b) => StableName (c (Full a)) -> Maybe (StableName (c (Full b)))
hash :: StName c -> Int
type History c = IntMap [(StName c, NodeId)]
lookHistory :: History c -> StName c -> Maybe NodeId
remember :: StName c -> NodeId -> History c -> History c
-- | Return a fresh identifier from the given supply
fresh :: (Enum a, MonadIO m) => IORef a -> m a
instance Eq (StName c)
-- | Reifying the sharing in an AST
--
-- This module is based on Type-Safe Observable Sharing in Haskell
-- (Andy Gill, Haskell Symposium, 2009).
module Language.Syntactic.Sharing.Reify
-- | Convert a syntax tree to a sharing-preserving graph
--
-- This function is not referentially transparent (hence the IO).
-- However, it is well-behaved in the sense that the worst thing that
-- could happen is that sharing is lost. It is not possible to get false
-- sharing.
reifyGraph :: Typeable a => (forall a. ASTF dom a -> Maybe (Witness' ctx a)) -> ASTF dom a -> IO (ASG ctx dom a)
-- | This module is similar to Language.Syntactic.Sharing.Reify, but
-- operates on HOAST rather than a general AST. The reason
-- for having this module is that when using HOAST, it is
-- important to do simultaneous sharing analysis and HOLambda
-- reification. Obviously we cannot do sharing analysis first (using
-- reifyGraph from Language.Syntactic.Sharing.Reify), since
-- it needs to be able to look inside HOLambda. On the other hand,
-- if we did HOLambda reification first (using reify), we
-- would destroy the sharing.
--
-- This module is based on Type-Safe Observable Sharing in Haskell
-- (Andy Gill, Haskell Symposium, 2009).
module Language.Syntactic.Sharing.ReifyHO
-- | Convert a syntax tree to a sharing-preserving graph
reifyGraphTop :: Typeable a => (forall a. HOASTF ctx dom a -> Maybe (Witness' ctx a)) -> HOASTF ctx dom a -> IO (ASG ctx (Lambda ctx :+: (Variable ctx :+: dom)) a, VarId)
-- | Reifying an n-ary syntactic function to a sharing-preserving graph
--
-- This function is not referentially transparent (hence the IO).
-- However, it is well-behaved in the sense that the worst thing that
-- could happen is that sharing is lost. It is not possible to get false
-- sharing.
reifyGraph :: Reifiable ctx a dom internal => (forall a. HOASTF ctx dom a -> Maybe (Witness' ctx a)) -> a -> IO (ASG ctx (Lambda ctx :+: (Variable ctx :+: dom)) (NAryEval internal), VarId)