-- 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.
--
-- The following people have contributed to Syntactic:
--
--
--
-- [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.8
-- | 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) = inj (Num2 n)
-- conv12 (Add1 a b) = inj Add2 :$ conv12 a :$ conv12 b
--
-- conv21 :: Expr2 a -> Expr1 a
-- conv21 (prj -> Just (Num2 n)) = Num1 n
-- conv21 ((prj -> Just Add2) :$ a :$ b) = Add1 (conv21 a) (conv21 b)
--
--
-- A key property here is that the patterns in conv21 are
-- actually complete.
--
-- So, why should one use Expr2 instead of Expr1? The
-- answer is that Expr2 can be processed by generic algorithms
-- defined over AST, for example:
--
--
-- countNodes :: ASTF domain a -> Int
-- countNodes = count
-- where
-- count :: AST domain a -> Int
-- count (Sym _) = 1
-- count (a :$ b) = count a + count b
--
--
-- Furthermore, although Expr2 was defined to use exactly the
-- constructors Num2 and Add2, it is possible to leave
-- the set of constructors open, leading to more modular and reusable
-- code. This can be seen by relaxing the types of conv12 and
-- conv21:
--
--
-- conv12 :: (Num2 :<: dom, Add2 :<: dom) => Expr1 a -> ASTF dom a
-- conv21 :: (Num2 :<: dom, Add2 :<: dom) => ASTF dom a -> Expr1 a
--
--
-- This way of encoding open data types is taken from Data types à la
-- carte (Wouter Swierstra, Journal of Functional Programming,
-- 2008). However, we do not need Swierstra's fixed-point machinery for
-- recursive data types. Instead we rely on AST being recursive.
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 Signature
-- | Can be used to turn a type constructor indexed by a to a type
-- constructor indexed by (Full a). This is useful
-- together with Args, which assumes its constructor to be indexed
-- by (Full a). That is, use
--
--
-- Args (WrapFull c) ...
--
--
-- instead of
--
--
-- Args c ...
--
--
-- if c is not indexed by (Full a).
data WrapFull c a
WrapFull :: c a -> WrapFull c (Full a)
unwrapFull :: WrapFull c (Full a) -> c a
-- | Fully or partially applied constructor
--
-- This is a public alias for the hidden class Signature'. The
-- only instances are:
--
--
-- instance Signature' (Full a)
-- instance Signature' b => Signature' (a :-> b)
--
class Signature' a => Signature a
-- | Maps a Signature to a simpler form where :-> has been
-- replaced by ->, and Full has been removed. This is
-- a public alias for the hidden type Denotation'.
type Denotation a = Denotation' a
-- | Returns the result type (Full removed) of a Signature.
-- This is a public alias for the hidden type DenResult'.
type DenResult a = DenResult' a
-- | A witness of (Signature a)
data ConsWit a
ConsWit :: ConsWit a
-- | Expressions in syntactic are supposed to have the form
-- (Signature a => expr a). This class lets us witness
-- the Signature constraint of an expression without examining the
-- expression.
class WitnessCons expr
witnessCons :: WitnessCons expr => expr a -> ConsWit a
-- | Make a constructor evaluation from a Denotation representation
fromEval :: Signature a => Denotation a -> a
toEval :: Signature a => a -> Denotation a
-- | Convert a heterogeneous list to a normal list
listArgs :: Signature a => (forall a. c (Full a) -> b) -> Args c a -> [b]
-- | Change the container of each element in a heterogeneous list
mapArgs :: Signature a => (forall a. c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 a
-- | Change the container of each element in a heterogeneous list, monadic
-- version
mapArgsM :: (Monad m, Signature a) => (forall a. c1 (Full a) -> m (c2 (Full a))) -> Args c1 a -> m (Args c2 a)
-- | Apply the syntax tree to the listed arguments
appArgs :: Signature a => AST dom a -> Args (AST dom) a -> ASTF dom (DenResult a)
-- | Apply the evaluation function to the listed arguments
appEvalArgs :: Signature a => Denotation a -> Args Identity a -> DenResult 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 (Signature
-- a).
--
-- Note that the hidden class Signature' mentioned in the type of
-- Sym is interchangeable with Signature.
data AST dom a
Sym :: 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 :: * -> *
InjL :: dom1 a -> (dom1 :+: dom2) a
InjR :: dom2 a -> (dom1 :+: dom2) a
-- | Class that performs the type-level recursion needed by appSym
class ApplySym a f dom | a dom -> f, f -> a dom
-- | Generic symbol application
--
-- appSym has any type of the form:
--
--
-- appSym :: (expr :<: AST dom, Typeable a, Typeable b, ..., Typeable x)
-- => expr (a :-> b :-> ... :-> Full x)
-- -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)
--
appSym :: (ApplySym a f dom, Signature a, sym :<: AST dom) => sym a -> f
-- | Generic symbol application with explicit context
appSymCtx :: (ApplySym a f dom, Signature a, sym ctx :<: dom) => Proxy ctx -> sym ctx a -> f
class :<: sub sup
inj :: (:<: sub sup, Signature a) => sub a -> sup a
prj :: :<: sub sup => sup a -> Maybe (sub a)
-- | inj with explicit context
injCtx :: (sub ctx :<: sup, Signature a) => Proxy ctx -> sub ctx a -> sup a
-- | prj with explicit context
prjCtx :: sub ctx :<: sup => Proxy ctx -> sup a -> Maybe (sub ctx a)
-- | It is assumed that for all types A fulfilling
-- (Syntactic A dom):
--
--
-- eval a == eval (desugar $ (id :: A -> A) $ sugar a)
--
--
-- (using 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
-- | "Sugared" symbol application
--
-- sugarSym has any type of the form:
--
--
-- sugarSym ::
-- ( expr :<: AST dom
-- , Syntactic a dom
-- , Syntactic b dom
-- , ...
-- , Syntactic x dom
-- ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))
-- -> (a -> b -> ... -> x)
--
sugarSym :: (Signature a, sym :<: AST dom, ApplySym a b dom, SyntacticN c b) => sym a -> c
-- | "Sugared" symbol application with explicit context
sugarSymCtx :: (Signature a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b) => Proxy ctx -> sym ctx a -> c
-- | Query an AST using a function that gets direct access to the
-- top-most constructor and its sub-trees
--
-- Note that, by instantiating the type c with AST
-- dom', we get the following type, which shows that
-- queryNode can be directly used to transform syntax trees (see
-- also transformNode):
--
--
-- (forall b . (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> ASTF dom' a)
-- -> ASTF dom a
-- -> ASTF dom' a
--
queryNode :: (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c (Full a)) -> ASTF dom a -> c (Full a)
-- | A simpler version of queryNode
--
-- This function can be used to create AST traversal functions
-- indexed by the symbol types, for example:
--
--
-- class Count subDomain
-- where
-- count' :: Count domain => subDomain a -> Args (AST domain) a -> Int
--
-- instance (Count sub1, Count sub2) => Count (sub1 :+: sub2)
-- where
-- count' (InjL a) args = count' a args
-- count' (InjR a) args = count' a args
--
-- count :: Count dom => ASTF dom a -> Int
-- count = queryNodeSimple count'
--
--
-- Here, count represents some static analysis on an AST.
-- Each constructor in the tree will be queried by count'
-- indexed by the corresponding symbol type. That way, count'
-- can be seen as an open-ended function on an open data type. The
-- (Count domain) constraint on count' is to allow
-- recursion over sub-trees.
--
-- Let's say we have a symbol
--
--
-- data Add a
-- where
-- Add :: Add (Int :-> Int :-> Full Int)
--
--
-- Then the Count instance for Add might look as
-- follows:
--
--
-- instance Count Add
-- where
-- count' Add (a :* b :* Nil) = 1 + count a + count b
--
queryNodeSimple :: (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c) -> ASTF dom a -> c
-- | A version of queryNode where the result is a transformed syntax
-- tree, wrapped in a type constructor c
transformNode :: (forall b. (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> c (ASTF dom' a)) -> ASTF dom a -> c (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
witnessByProxy :: Sat ctx a => Proxy ctx -> Proxy 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 SatWit ctx a
SatWit :: SatWit ctx a
fromSatWit :: SatWit ctx a -> Witness ctx a
-- | Expressions that act as witnesses of their result type
class WitnessSat expr where type family SatContext expr
witnessSat :: WitnessSat expr => expr a -> SatWit (SatContext expr) (DenResult a)
-- | Expressions that act as witnesses of their result type
class MaybeWitnessSat ctx expr
maybeWitnessSat :: MaybeWitnessSat ctx expr => Proxy ctx -> expr a -> Maybe (SatWit ctx (DenResult a))
-- | Convenient default implementation of maybeWitnessSat
maybeWitnessSatDefault :: WitnessSat expr => Proxy (SatContext expr) -> expr a -> Maybe (SatWit (SatContext expr) (DenResult 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
-- | Representation of "simple" types: types satisfying (Eq a,
-- Show a, Typeable a)
data SimpleCtx
simpleCtx :: Proxy SimpleCtx
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] (Eq a, Show a, Typeable a) => Sat SimpleCtx a
instance [overlap ok] Sat Poly a
instance [overlap ok] (MaybeWitnessSat ctx sub1, MaybeWitnessSat ctx sub2) => MaybeWitnessSat ctx (sub1 :+: sub2)
instance [overlap ok] MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (AST dom)
instance [overlap ok] (Syntactic a dom, ia ~ Internal a, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib)
instance [overlap ok] (Syntactic a dom, ia ~ AST dom (Full (Internal a))) => 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] (Typeable a, ApplySym b f' dom) => ApplySym (a :-> b) (ASTF dom a -> f') dom
instance [overlap ok] ApplySym (Full a) (ASTF dom a) dom
instance [overlap ok] (WitnessCons sub1, WitnessCons sub2) => WitnessCons (sub1 :+: sub2)
instance [overlap ok] Signature' a => Signature a
instance [overlap ok] Signature' b => Signature' (a :-> b)
instance [overlap ok] Signature' (Full a)
module Language.Syntactic.Interpretation.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.Interpretation.Render
-- | Render an expression as concrete syntax. A complete instance must
-- define either of the methods render and renderPart.
class Render expr where render = renderPart [] renderPart [] a = render a renderPart args a = "(" ++ unwords (render a : args) ++ ")"
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 where toTreePart args a = Node (render a) args
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.Interpretation.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)
-- | Construct for decorating expressions with additional information
module Language.Syntactic.Constructs.Decoration
-- | Decorating an expression with additional information
--
-- One usage of Decor is to decorate every node of a syntax tree.
-- This is done simply by changing
--
--
-- AST dom a
--
--
-- to
--
--
-- AST (Decor info dom) a
--
--
-- Injection/projection of an decorated tree is done using
-- injDecor / prjDecor.
data Decor info expr a
Decor :: info (DenResult a) -> expr a -> Decor info expr a
decorInfo :: Decor info expr a -> info (DenResult a)
decorExpr :: Decor info expr a -> expr a
injDecor :: (sub :<: sup, Signature a) => info (DenResult a) -> sub a -> AST (Decor info sup) a
prjDecor :: sub :<: sup => AST (Decor info sup) a -> Maybe (info (DenResult a), sub a)
-- | injDecor with explicit context
injDecorCtx :: (sub ctx :<: sup, Signature a) => Proxy ctx -> info (DenResult a) -> sub ctx a -> AST (Decor info sup) a
-- | prjDecor with explicit context
prjDecorCtx :: sub ctx :<: sup => Proxy ctx -> AST (Decor info sup) a -> Maybe (info (DenResult a), sub ctx a)
-- | Get the decoration of the top-level node
getInfo :: AST (Decor info dom) a -> info (DenResult a)
-- | Update the decoration of the top-level node
updateDecor :: (info a -> info a) -> ASTF (Decor info dom) a -> ASTF (Decor info dom) a
-- | Lift a function that operates on expressions with associated
-- information to operate on an Decor expression. This function is
-- convenient to use together with e.g. queryNodeSimple when the
-- domain has the form (Decor info dom).
liftDecor :: (expr a -> info (DenResult a) -> b) -> (Decor info expr a -> b)
-- | Collect the decorations of all nodes
collectInfo :: (forall a. info a -> b) -> AST (Decor info dom) a -> [b]
-- | Rendering of decorated syntax trees
toTreeDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> Tree String
-- | Show an decorated syntax tree using ASCII art
showDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> String
-- | Print an decorated syntax tree using ASCII art
drawDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> IO ()
-- | Strip decorations from an AST
stripDecor :: AST (Decor info dom) a -> AST dom a
instance Eval expr => Eval (Decor info expr)
instance ToTree expr => ToTree (Decor info expr)
instance Render expr => Render (Decor info expr)
instance ExprEq expr => ExprEq (Decor info expr)
instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (Decor info dom)
instance WitnessSat expr => WitnessSat (Decor info expr)
instance WitnessCons dom => WitnessCons (Decor info dom)
-- | The syntactic library
--
-- The basic functionality is provided by the module
-- Language.Syntactic.Syntax.
module Language.Syntactic
-- | Default implementations of some interpretation functions
module Language.Syntactic.Interpretation.Semantics
-- | A representation of a syntactic construct as a String and an
-- evaluation function. It is not meant to be used as a syntactic symbol
-- in an AST. Its only purpose is to provide the default
-- implementations of functions like exprEq via the
-- Semantic class.
data Semantics a
Sem :: String -> Denotation a -> Semantics a
semanticName :: Semantics a -> String
semanticEval :: Semantics a -> Denotation a
-- | Class of expressions that can be treated as constructs
class Semantic expr
semantics :: Semantic expr => expr a -> Semantics a
-- | Default implementation of exprEq
exprEqSem :: Semantic expr => expr a -> expr b -> Bool
-- | Default implementation of exprHash
exprHashSem :: Semantic expr => expr a -> Hash
-- | Default implementation of renderPart
renderPartSem :: Semantic expr => [String] -> expr a -> String
-- | Default implementation of evaluate
evaluateSem :: Semantic expr => expr a -> a
instance Eval Semantics
instance Render Semantics
instance ExprEq Semantics
-- | Conditional expressions
module Language.Syntactic.Constructs.Condition
data Condition ctx a
Condition :: Condition ctx (Bool :-> (a :-> (a :-> Full a)))
instance [overlap ok] ToTree (Condition ctx)
instance [overlap ok] Eval (Condition ctx)
instance [overlap ok] Render (Condition ctx)
instance [overlap ok] ExprEq (Condition ctx)
instance [overlap ok] Semantic (Condition ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Condition ctx2)
instance [overlap ok] MaybeWitnessSat ctx (Condition ctx)
instance [overlap ok] WitnessSat (Condition ctx)
instance [overlap ok] WitnessCons (Condition ctx)
-- | Provides a simple way to make syntactic constructs for prototyping.
-- Note that Construct is quite unsafe as it only uses
-- String to distinguish between different constructs. Also,
-- Construct has a very free type that allows any number of
-- arguments.
module Language.Syntactic.Constructs.Construct
data Construct ctx a
Construct :: String -> Denotation a -> Construct ctx a
instance [overlap ok] Eval (Construct ctx)
instance [overlap ok] ToTree (Construct ctx)
instance [overlap ok] Render (Construct ctx)
instance [overlap ok] ExprEq (Construct ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Construct ctx2)
instance [overlap ok] MaybeWitnessSat ctx (Construct ctx)
instance [overlap ok] WitnessSat (Construct ctx)
instance [overlap ok] WitnessCons (Construct ctx)
-- | Identity function
module Language.Syntactic.Constructs.Identity
-- | Identity function
data Identity ctx a
Id :: Identity ctx (a :-> Full a)
instance [overlap ok] ToTree (Identity ctx)
instance [overlap ok] Eval (Identity ctx)
instance [overlap ok] Render (Identity ctx)
instance [overlap ok] ExprEq (Identity ctx)
instance [overlap ok] Semantic (Identity ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Identity ctx2)
instance [overlap ok] MaybeWitnessSat ctx (Identity ctx)
instance [overlap ok] WitnessSat (Identity ctx)
instance [overlap ok] WitnessCons (Identity ctx)
-- | Literal expressions
module Language.Syntactic.Constructs.Literal
data Literal ctx a
Literal :: a -> Literal ctx (Full a)
instance [overlap ok] Eval (Literal ctx)
instance [overlap ok] ToTree (Literal ctx)
instance [overlap ok] Render (Literal ctx)
instance [overlap ok] ExprEq (Literal ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Literal ctx2)
instance [overlap ok] MaybeWitnessSat ctx (Literal ctx)
instance [overlap ok] WitnessSat (Literal ctx)
instance [overlap ok] WitnessCons (Literal ctx)
-- | Monadic constructs
module Language.Syntactic.Constructs.Monad
data MONAD m a
Return :: MONAD m (a :-> Full (m a))
Bind :: MONAD m (m a :-> ((a -> m b) :-> Full (m b)))
Then :: MONAD m (m a :-> (m b :-> Full (m b)))
When :: MONAD m (Bool :-> (m () :-> Full (m ())))
-- | Projection with explicit monad type
prjMonad :: MONAD m :<: sup => Proxy (m ()) -> sup a -> Maybe (MONAD m a)
instance Monad m => ToTree (MONAD m)
instance Monad m => Eval (MONAD m)
instance Monad m => Render (MONAD m)
instance Monad m => ExprEq (MONAD m)
instance Monad m => Semantic (MONAD m)
instance MaybeWitnessSat ctx (MONAD m)
instance WitnessCons (MONAD m)
-- | Construction and projection of tuples in the object language
--
-- The function pairs desugarTupX/sugarTupX could be
-- used directly in Syntactic instances if it wasn't for the extra
-- (Proxy ctx) arguments. For this reason,
-- Syntactic instances have to be written manually for each
-- context. The module
-- Language.Syntactic.Constructs.TupleSyntacticPoly provides
-- instances for a Poly context. The exact same code can be used
-- to make instances for other contexts -- just copy/paste and replace
-- Poly and poly with the desired context (and probably add
-- an extra constraint in the class contexts).
module Language.Syntactic.Constructs.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))))))))
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)
-- | These families (Sel1' - Sel7') are needed because of the
-- problem described in:
--
--
-- http://emil-fp.blogspot.com/2011/08/fundeps-weaker-than-type-families.html
-- | 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)
-- | 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 [overlap ok] ToTree (Select ctx)
instance [overlap ok] Eval (Select ctx)
instance [overlap ok] Render (Select ctx)
instance [overlap ok] ExprEq (Select ctx)
instance [overlap ok] Semantic (Select ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Select ctx2)
instance [overlap ok] MaybeWitnessSat ctx (Select ctx)
instance [overlap ok] WitnessSat (Select ctx)
instance [overlap ok] WitnessCons (Select ctx)
instance [overlap ok] ToTree (Tuple ctx)
instance [overlap ok] Eval (Tuple ctx)
instance [overlap ok] Render (Tuple ctx)
instance [overlap ok] ExprEq (Tuple ctx)
instance [overlap ok] Semantic (Tuple ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Tuple ctx2)
instance [overlap ok] MaybeWitnessSat ctx (Tuple ctx)
instance [overlap ok] WitnessSat (Tuple ctx)
instance [overlap ok] WitnessCons (Tuple ctx)
-- | General binding constructs
module Language.Syntactic.Constructs.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)
-- | Lambda binding
data Lambda ctx a
Lambda :: VarId -> Lambda ctx (b :-> Full (a -> b))
-- | 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))
-- | Let binding with explicit context
letBind :: (Sat ctx a, Sat ctx b) => Proxy ctx -> Let ctx ctx (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)
-- | Capture-avoiding substitution
subst :: (Lambda ctx :<: dom, Variable ctx :<: dom, Typeable a) => Proxy ctx -> VarId -> ASTF dom a -> ASTF dom b -> ASTF dom b
-- | Beta-reduction of an expression. The expression to be reduced is
-- assumed to be a Lambda.
betaReduce :: (Lambda ctx :<: dom, Variable ctx :<: dom) => Proxy ctx -> ASTF dom a -> ASTF dom (a -> b) -> ASTF dom b
class EvalBind sub
evalBindSym :: (EvalBind sub, EvalBind dom, Signature a) => sub a -> Args (AST dom) a -> Reader [(VarId, Dynamic)] (DenResult a)
-- | Evaluation of possibly open expressions
evalBindM :: EvalBind dom => ASTF dom a -> Reader [(VarId, Dynamic)] a
-- | Evaluation of closed expressions
evalBind :: EvalBind dom => ASTF dom a -> a
-- | Convenient default implementation of evalBindSym
evalBindSymDefault :: (Eval sub, Signature a, EvalBind dom) => sub a -> Args (AST dom) a -> Reader [(VarId, Dynamic)] (DenResult a)
-- | Environments containing a list of variable equivalences
class VarEqEnv a
prjVarEqEnv :: VarEqEnv a => a -> [(VarId, VarId)]
modVarEqEnv :: VarEqEnv a => ([(VarId, VarId)] -> [(VarId, VarId)]) -> (a -> a)
class VarEqEnv env => AlphaEq sub1 sub2 dom env
alphaEqSym :: (AlphaEq sub1 sub2 dom env, Signature a, Signature b) => sub1 a -> Args (AST dom) a -> sub2 b -> Args (AST dom) b -> Reader env Bool
alphaEqM :: AlphaEq dom dom dom env => ASTF dom a -> ASTF dom b -> Reader env Bool
alphaEqM2 :: (AlphaEq dom dom dom env, Signature a) => ASTF dom b -> dom a -> Args (AST dom) a -> Reader env Bool
-- | Alpha-equivalence on lambda expressions. Free variables are taken to
-- be equivalent if they have the same identifier.
alphaEq :: AlphaEq dom dom dom [(VarId, VarId)] => ASTF dom a -> ASTF dom b -> Bool
alphaEqSymDefault :: (ExprEq sub, AlphaEq dom dom dom env, Signature a, Signature b) => sub a -> Args (AST dom) a -> sub b -> Args (AST dom) b -> Reader env Bool
alphaEqChildren :: AlphaEq dom dom dom env => AST dom a -> AST dom b -> Reader env Bool
instance [overlap ok] Eq VarId
instance [overlap ok] Ord VarId
instance [overlap ok] Num VarId
instance [overlap ok] Real VarId
instance [overlap ok] Integral VarId
instance [overlap ok] Enum VarId
instance [overlap ok] Ix VarId
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Variable ctx) (Variable ctx) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Lambda ctx) (Lambda ctx) dom env
instance [overlap ok] AlphaEq dom dom (Decor info dom) env => AlphaEq (Decor info dom) (Decor info dom) (Decor info dom) env
instance [overlap ok] (AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Let ctxa ctxb) (Let ctxa ctxb) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Select ctx) (Select ctx) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Tuple ctx) (Tuple ctx) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Condition ctx) (Condition ctx) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Literal ctx) (Literal ctx) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Construct ctx) (Construct ctx) dom env
instance [overlap ok] AlphaEq dom dom dom env => AlphaEq (Identity ctx) (Identity ctx) dom env
instance [overlap ok] (AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => AlphaEq (subA1 :+: subA2) (subB1 :+: subB2) dom env
instance [overlap ok] VarEqEnv [(VarId, VarId)]
instance [overlap ok] EvalBind (Variable ctx)
instance [overlap ok] EvalBind (Lambda ctx)
instance [overlap ok] EvalBind dom => EvalBind (Decor info dom)
instance [overlap ok] Monad m => EvalBind (MONAD m)
instance [overlap ok] EvalBind (Let ctxa ctxb)
instance [overlap ok] EvalBind (Select ctx)
instance [overlap ok] EvalBind (Tuple ctx)
instance [overlap ok] EvalBind (Condition ctx)
instance [overlap ok] EvalBind (Literal ctx)
instance [overlap ok] EvalBind (Construct ctx)
instance [overlap ok] EvalBind (Identity ctx)
instance [overlap ok] (EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2)
instance [overlap ok] Eval (Let ctxa ctxb)
instance [overlap ok] ToTree (Let ctxa ctxb)
instance [overlap ok] Render (Let ctxa ctxb)
instance [overlap ok] ExprEq (Let ctxa ctxb)
instance [overlap ok] MaybeWitnessSat ctx (Let ctxa ctxb)
instance [overlap ok] MaybeWitnessSat ctxb (Let ctxa ctxb)
instance [overlap ok] WitnessSat (Let ctxa ctxb)
instance [overlap ok] WitnessCons (Let ctxa ctxb)
instance [overlap ok] ToTree (Lambda ctx)
instance [overlap ok] Render (Lambda ctx)
instance [overlap ok] ExprEq (Lambda ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Lambda ctx2)
instance [overlap ok] WitnessCons (Lambda ctx)
instance [overlap ok] ToTree (Variable ctx)
instance [overlap ok] Render (Variable ctx)
instance [overlap ok] ExprEq (Variable ctx)
instance [overlap ok] MaybeWitnessSat ctx1 (Variable ctx2)
instance [overlap ok] MaybeWitnessSat ctx (Variable ctx)
instance [overlap ok] WitnessSat (Variable ctx)
instance [overlap ok] WitnessCons (Variable ctx)
instance [overlap ok] Show VarId
-- | Syntactic instances for tuples with Poly context
module Language.Syntactic.Constructs.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
-- | Syntactic instances for tuples with SimpleCtx context
module Language.Syntactic.Constructs.TupleSyntacticSimple
instance (Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), Syntactic e dom, Eq (Internal e), Show (Internal e), Syntactic f dom, Eq (Internal f), Show (Internal f), Syntactic g dom, Eq (Internal g), Show (Internal g), Tuple SimpleCtx :<: dom, Select SimpleCtx :<: dom) => Syntactic (a, b, c, d, e, f, g) dom
instance (Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), Syntactic e dom, Eq (Internal e), Show (Internal e), Syntactic f dom, Eq (Internal f), Show (Internal f), Tuple SimpleCtx :<: dom, Select SimpleCtx :<: dom) => Syntactic (a, b, c, d, e, f) dom
instance (Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), Syntactic e dom, Eq (Internal e), Show (Internal e), Tuple SimpleCtx :<: dom, Select SimpleCtx :<: dom) => Syntactic (a, b, c, d, e) dom
instance (Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Syntactic d dom, Eq (Internal d), Show (Internal d), Tuple SimpleCtx :<: dom, Select SimpleCtx :<: dom) => Syntactic (a, b, c, d) dom
instance (Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Syntactic c dom, Eq (Internal c), Show (Internal c), Tuple SimpleCtx :<: dom, Select SimpleCtx :<: dom) => Syntactic (a, b, c) dom
instance (Syntactic a dom, Eq (Internal a), Show (Internal a), Syntactic b dom, Eq (Internal b), Show (Internal b), Tuple SimpleCtx :<: dom, Select SimpleCtx :<: dom) => Syntactic (a, b) dom
-- | 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.Constructs.Binding.HigherOrder
-- | Variables
data Variable ctx 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 :: (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> HOLambda ctx dom (Full (a -> b))
type HODomain ctx dom = HOLambda ctx dom :+: (Variable ctx :+: dom)
-- | Lambda binding
lambda :: (Typeable a, Typeable b, Sat ctx a) => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> ASTF (HODomain ctx dom) (a -> b)
reifyM :: Typeable a => AST (HODomain 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 => AST (HODomain ctx dom) a -> AST (Lambda ctx :+: (Variable ctx :+: dom)) a
-- | Reifying an n-ary syntactic function
reify :: Syntactic a (HODomain ctx dom) => a -> ASTF (Lambda ctx :+: (Variable ctx :+: dom)) (Internal a)
instance (Syntactic a (HODomain ctx dom), Syntactic b (HODomain ctx dom), Sat ctx (Internal a)) => Syntactic (a -> b) (HODomain ctx dom)
instance MaybeWitnessSat ctx1 (HOLambda ctx2 dom)
instance WitnessCons (HOLambda ctx dom)
-- | Basic optimization of expressions
module Language.Syntactic.Constructs.Binding.Optimize
-- | Constant folder
--
-- Given an expression and the statically known value of that expression,
-- returns a (possibly) new expression with the same meaning as the
-- original. Typically, the result will be a Literal, if the
-- relevant type constraints are satisfied.
type ConstFolder dom = forall a. ASTF dom a -> a -> ASTF dom a
-- | Basic optimization of a sub-domain
class EvalBind dom => Optimize sub ctx dom
optimizeSym :: Optimize sub ctx dom => Proxy ctx -> ConstFolder dom -> sub a -> Args (AST dom) a -> Writer (Set VarId) (ASTF dom (DenResult a))
optimizeM :: Optimize dom ctx dom => Proxy ctx -> ConstFolder dom -> ASTF dom a -> Writer (Set VarId) (ASTF dom a)
-- | Optimize an expression
optimize :: Optimize dom ctx dom => Proxy ctx -> ConstFolder dom -> ASTF dom a -> ASTF dom a
-- | Convenient default implementation of optimizeSym (uses
-- evalBind to partially evaluate)
optimizeSymDefault :: (sub :<: dom, WitnessCons sub, Optimize dom ctx dom) => Proxy ctx -> ConstFolder dom -> sub a -> Args (AST dom) a -> Writer (Set VarId) (ASTF dom (DenResult a))
instance (Lambda ctx :<: dom, Optimize dom ctx dom) => Optimize (Lambda ctx) ctx dom
instance (Variable ctx :<: dom, Optimize dom ctx dom) => Optimize (Variable ctx) ctx dom
instance (Condition ctx' :<: dom, Lambda ctx :<: dom, Variable ctx :<: dom, AlphaEq dom dom dom [(VarId, VarId)], Optimize dom ctx dom) => Optimize (Condition ctx') ctx dom
instance (Let ctxa ctxb :<: dom, Optimize dom ctx dom) => Optimize (Let ctxa ctxb) ctx dom
instance (Select ctx' :<: dom, Optimize dom ctx dom) => Optimize (Select ctx') ctx dom
instance (Tuple ctx' :<: dom, Optimize dom ctx dom) => Optimize (Tuple ctx') ctx dom
instance (Literal ctx' :<: dom, Optimize dom ctx dom) => Optimize (Literal ctx') ctx dom
instance (Construct ctx' :<: dom, Optimize dom ctx dom) => Optimize (Construct ctx') ctx dom
instance (Identity ctx' :<: dom, Optimize dom ctx dom) => Optimize (Identity ctx') ctx dom
instance (Optimize sub1 ctx dom, Optimize sub2 ctx dom) => Optimize (sub1 :+: sub2) ctx dom
module Language.Syntactic.Frontend.Monad
-- | User interface to embedded monadic programs
newtype Mon ctx dom m a
Mon :: (forall r. (Monad m, Typeable r) => Cont (ASTF (HODomain ctx dom) (m r)) a) -> Mon ctx dom m a
unMon :: Mon ctx dom m a -> forall r. (Monad m, Typeable r) => Cont (ASTF (HODomain ctx dom) (m r)) a
-- | One-layer desugaring of monadic actions
desugarMonad :: (MONAD m :<: dom, Monad m, Typeable1 m, Typeable a, Sat ctx a) => Mon ctx dom m (ASTF (HODomain ctx dom) a) -> ASTF (HODomain ctx dom) (m a)
-- | One-layer sugaring of monadic actions
sugarMonad :: (MONAD m :<: dom, Monad m, Typeable1 m, Typeable a, Sat ctx a) => ASTF (HODomain ctx dom) (m a) -> Mon ctx dom m (ASTF (HODomain ctx dom) a)
instance Functor (Mon ctx dom m)
instance (MONAD m :<: dom, Syntactic a (HODomain ctx dom), Monad m, Typeable1 m, Sat ctx (Internal a)) => Syntactic (Mon ctx dom m a) (HODomain ctx dom)
instance Monad m => Monad (Mon ctx dom m)
-- | 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.Sharing.SimpleCodeMotion
-- | Interface for binding constructs
data BindDict ctx dom
BindDict :: (forall a. dom a -> Maybe VarId) -> (forall a. dom a -> Maybe VarId) -> (forall a. (Sat ctx a, Typeable a) => ASTF dom a -> VarId -> dom (Full a)) -> (forall a b. (Sat ctx a, Typeable a, Sat ctx b) => ASTF dom b -> VarId -> dom (b :-> Full (a -> b))) -> (forall a b. (Sat ctx a, Sat ctx b) => ASTF dom b -> dom (a :-> ((a -> b) :-> Full b))) -> BindDict ctx dom
prjVariable :: BindDict ctx dom -> forall a. dom a -> Maybe VarId
prjLambda :: BindDict ctx dom -> forall a. dom a -> Maybe VarId
injVariable :: BindDict ctx dom -> forall a. (Sat ctx a, Typeable a) => ASTF dom a -> VarId -> dom (Full a)
injLambda :: BindDict ctx dom -> forall a b. (Sat ctx a, Typeable a, Sat ctx b) => ASTF dom b -> VarId -> dom (b :-> Full (a -> b))
injLet :: BindDict ctx dom -> forall a b. (Sat ctx a, Sat ctx b) => ASTF dom b -> dom (a :-> ((a -> b) :-> Full b))
-- | Perform common sub-expression elimination and variable hoisting
codeMotion :: (AlphaEq dom dom dom [(VarId, VarId)], MaybeWitnessSat ctx dom, Typeable a) => BindDict ctx dom -> (forall a. dom a -> Bool) -> ASTF dom a -> State VarId (ASTF dom a)
defaultBindDict :: (Variable ctx :<: dom, Lambda ctx :<: dom, Let ctx ctx :<: dom) => BindDict ctx dom
-- | Like reify but with common sub-expression elimination and
-- variable hoisting
reifySmart :: (Let ctx ctx :<: dom, AlphaEq dom dom (Lambda ctx :+: (Variable ctx :+: dom)) [(VarId, VarId)], MaybeWitnessSat ctx dom, Syntactic a (HODomain ctx dom)) => (forall a. (Lambda ctx :+: (Variable ctx :+: dom)) a -> Bool) -> a -> ASTF (Lambda ctx :+: (Variable ctx :+: dom)) (Internal a)
-- | 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
-- | An ASTF with hidden result type
data SomeAST dom
SomeAST :: ASTF dom a -> SomeAST dom
-- | Environment for alpha-equivalence
class NodeEqEnv dom a
prjNodeEqEnv :: NodeEqEnv dom a => a -> NodeEnv dom
modNodeEqEnv :: NodeEqEnv dom a => (NodeEnv dom -> NodeEnv dom) -> (a -> a)
type EqEnv dom = ([(VarId, VarId)], NodeEnv dom)
type NodeEnv dom = (Array NodeId Hash, Array NodeId (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 :: (ExprEq dom, AlphaEq dom dom (Node ctx :+: dom) (EqEnv (Node ctx :+: dom))) => ASG ctx dom a -> [[NodeId]]
-- | Common sub-expression elimination based on alpha-equivalence
cse :: (ExprEq dom, AlphaEq dom dom (Node ctx :+: dom) (EqEnv (Node ctx :+: 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 (AlphaEq dom dom dom env, NodeEqEnv dom env) => AlphaEq (Node ctx) (Node ctx) dom env
instance VarEqEnv (EqEnv dom)
instance NodeEqEnv dom (EqEnv 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 (SatWit ctx a)) -> ASTF dom a -> IO (ASG ctx dom a)
-- | This module is similar to Language.Syntactic.Sharing.Reify, but
-- operates on AST (HODomain ctx dom) rather than
-- a general AST. The reason for having this module is that when
-- using HODomain, it is important to do simultaneous sharing
-- analysis and HOLambda reification. Obviously we cannot do
-- sharing analysis first (using 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. ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a)) -> ASTF (HODomain 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 :: Syntactic a (HODomain ctx dom) => (forall a. ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a)) -> a -> IO (ASG ctx (Lambda ctx :+: (Variable ctx :+: dom)) (Internal a), VarId)