-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Generic abstract syntax, and utilities for embedded languages
--   
--   This library provides:
--   
--   <ul>
--   <li>Generic representation and manipulation of abstract syntax</li>
--   <li>Composable AST representations (partly based on Data Types à la
--   Carte [1])</li>
--   <li>A collection of common syntactic constructs, including variable
--   binding constructs</li>
--   <li>Utilities for analyzing and transforming generic abstract
--   syntax</li>
--   <li>Utilities for building extensible embedded languages based on
--   generic syntax</li>
--   </ul>
--   
--   For more information about the core functionality, see "A Generic
--   Abstract Syntax Model for Embedded Languages" (ICFP 2012):
--   
--   <ul>
--   <li>Paper:
--   <a>http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf</a></li>
--   <li>Slides:
--   <a>http://www.cse.chalmers.se/~emax/documents/axelsson2012generic-slides.pdf</a></li>
--   </ul>
--   
--   For a practical example of how to use the library, see the
--   proof-of-concept implementation Feldspar EDSL in the <tt>examples</tt>
--   directory. (The real Feldspar [2] is also implemented using
--   Syntactic.)
--   
--   The maturity of this library varies between different modules. The
--   core part (<a>Language.Syntactic</a>) is rather stable, but many of
--   the other modules are in a much more experimental state.
--   
--   [1] W. Swierstra. Data Types à la Carte. <i>Journal of Functional
--   Programming</i>, 18(4):423-436, 2008,
--   <a>http://dx.doi.org/10.1017/S0956796808006758</a>.
--   
--   [2] <a>http://hackage.haskell.org/package/feldspar-language</a>
@package syntactic
@version 1.13


-- | 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 <tt>is</tt> of unique natural numbers, returns a function
--   that maps each number in <tt>is</tt> to a unique number in the range
--   <tt>[0 .. length is-1]</tt>. The complexity is O(<tt>maximum is</tt>).
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]]

module Data.PolyProxy

-- | Kind-polymorphic proxy type
data P a
P :: P a


-- | An alternative to <a>Data.Dynamic</a> with a different constraint on
--   <a>toDyn</a>
module Data.DynamicAlt
data Dynamic
Dynamic :: TypeRep -> Any -> Dynamic
toDyn :: Typeable (a -> b) => P (a -> b) -> a -> Dynamic
fromDyn :: Typeable a => Dynamic -> Maybe a


-- | Generic representation of typed syntax trees
--   
--   For details, see: A Generic Abstract Syntax Model for Embedded
--   Languages (ICFP 2012,
--   <a>http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf</a>).
module Language.Syntactic.Syntax

-- | Generic abstract syntax tree, parameterized by a symbol domain
--   
--   <tt>(<a>AST</a> dom (a <a>:-&gt;</a> b))</tt> represents a partially
--   applied (or unapplied) symbol, missing at least one argument, while
--   <tt>(<a>AST</a> dom (<a>Full</a> a))</tt> represents a fully applied
--   symbol, i.e. a complete syntax tree.
data AST dom sig
Sym :: dom sig -> AST dom sig
(:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig

-- | Fully applied abstract syntax tree
type ASTF dom a = AST dom (Full a)

-- | Signature of a fully applied symbol
newtype Full a
Full :: a -> Full a
result :: Full a -> a

-- | Signature of a partially applied (or unapplied) symbol
newtype (:->) a sig
Partial :: (a -> sig) -> :-> a sig

-- | Count the number of symbols in an expression
size :: AST dom sig -> Int

-- | Class for the type-level recursion needed by <a>appSym</a>
class ApplySym sig f dom | sig dom -> f, f -> sig dom
appSym' :: ApplySym sig f dom => AST dom sig -> f

-- | The result type of a symbol with the given signature

-- | Direct sum of two symbol domains
data (:+:) dom1 dom2 a
InjL :: dom1 a -> (dom1 :+: dom2) a
InjR :: dom2 a -> (dom1 :+: dom2) a

-- | Symbol projection
class Project sub sup
prj :: Project sub sup => sup a -> Maybe (sub a)

-- | Symbol subsumption
class Project sub sup => (:<:) sub sup
inj :: :<: sub sup => sub a -> sup a

-- | Generic symbol application
--   
--   <a>appSym</a> has any type of the form:
--   
--   <pre>
--   appSym :: (expr :&lt;: AST dom)
--       =&gt; expr (a :-&gt; b :-&gt; ... :-&gt; Full x)
--       -&gt; (ASTF dom a -&gt; ASTF dom b -&gt; ... -&gt; ASTF dom x)
--   </pre>
appSym :: (ApplySym sig f dom, sym :<: AST dom) => sym sig -> f

-- | Constrain a symbol to a specific type
symType :: P sym -> sym sig -> sym sig

-- | Projection to a specific symbol type
prjP :: Project sub sup => P sub -> sup sig -> Maybe (sub sig)
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] Functor Full
instance [overlap ok] Functor ((:->) a)
instance [overlap ok] (Functor dom1, Functor dom2) => Functor (dom1 :+: dom2)
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] Project expr1 expr3 => Project expr1 (expr2 :+: expr3)
instance [overlap ok] Project expr1 (expr1 :+: expr2)
instance [overlap ok] Project expr expr
instance [overlap ok] Project sub sup => Project sub (AST sup)
instance [overlap ok] ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom
instance [overlap ok] ApplySym (Full a) (ASTF dom a) dom
instance [overlap ok] Functor dom => Functor (AST dom)


-- | Generic traversals of <a>AST</a> terms
module Language.Syntactic.Traversal

-- | Map a function over all immediate sub-terms, collecting the results in
--   a list (corresponds to the function with the same name in Scrap Your
--   Boilerplate)
gmapQ :: (forall a. ASTF dom a -> b) -> (forall a. ASTF dom a -> [b])

-- | Map a function over all immediate sub-terms (corresponds to the
--   function with the same name in Scrap Your Boilerplate)
gmapT :: (forall a. ASTF dom a -> ASTF dom a) -> (forall a. ASTF dom a -> ASTF dom a)

-- | Apply a transformation bottom-up over an expression (corresponds to
--   <tt>everywhere</tt> in Scrap Your Boilerplate)
everywhereUp :: (forall a. ASTF dom a -> ASTF dom a) -> (forall a. ASTF dom a -> ASTF dom a)

-- | Apply a transformation top-down over an expression (corresponds to
--   <tt>everywhere'</tt> in Scrap Your Boilerplate)
everywhereDown :: (forall a. ASTF dom a -> ASTF dom a) -> (forall a. ASTF dom a -> ASTF dom a)

-- | List of symbol arguments
data Args c sig
Nil :: Args c (Full a)
(:*) :: c (Full a) -> Args c sig -> Args c (a :-> sig)

-- | Map a function over an <a>Args</a> list and collect the results in an
--   ordinary list
listArgs :: (forall a. c (Full a) -> b) -> Args c sig -> [b]

-- | Map a function over an <a>Args</a> list
mapArgs :: (forall a. c1 (Full a) -> c2 (Full a)) -> (forall sig. Args c1 sig -> Args c2 sig)

-- | Map an applicative function over an <a>Args</a> list
mapArgsA :: Applicative f => (forall a. c1 (Full a) -> f (c2 (Full a))) -> (forall sig. Args c1 sig -> f (Args c2 sig))

-- | Map a monadic function over an <a>Args</a> list
mapArgsM :: Monad m => (forall a. c1 (Full a) -> m (c2 (Full a))) -> (forall sig. Args c1 sig -> m (Args c2 sig))

-- | Apply a (partially applied) symbol to a list of argument terms
appArgs :: AST dom sig -> Args (AST dom) sig -> ASTF dom (DenResult sig)

-- | Fold an <a>AST</a> using a list to hold the results of sub-terms
listFold :: (forall sig. dom sig -> [b] -> b) -> (forall a. ASTF dom a -> b)

-- | "Pattern match" on an <a>AST</a> using a function that gets direct
--   access to the top-most symbol and its sub-trees
match :: (forall sig. a ~ DenResult sig => dom sig -> Args (AST dom) sig -> c (Full a)) -> ASTF dom a -> c (Full a)

-- | <i>Deprecated: Please use <a>match</a> instead. </i>
query :: (forall sig. a ~ DenResult sig => dom sig -> Args (AST dom) sig -> c (Full a)) -> ASTF dom a -> c (Full a)

-- | A version of <a>match</a> with a simpler result type
simpleMatch :: (forall sig. a ~ DenResult sig => dom sig -> Args (AST dom) sig -> b) -> ASTF dom a -> b

-- | Fold an <a>AST</a> using an <a>Args</a> list to hold the results of
--   sub-terms
fold :: (forall sig. dom sig -> Args c sig -> c (Full (DenResult sig))) -> (forall a. ASTF dom a -> c (Full a))

-- | Simplified version of <a>fold</a> for situations where all
--   intermediate results have the same type
simpleFold :: (forall sig. dom sig -> Args (Const b) sig -> b) -> (forall a. ASTF dom a -> b)

-- | A version of <a>match</a> where the result is a transformed syntax
--   tree, wrapped in a type constructor <tt>c</tt>
matchTrans :: (forall sig. a ~ DenResult sig => dom sig -> Args (AST dom) sig -> c (ASTF dom' a)) -> ASTF dom a -> c (ASTF dom' a)

-- | Can be used to make an arbitrary type constructor indexed by
--   <tt>(<a>Full</a> a)</tt>. This is useful as the type constructor
--   parameter of <a>Args</a>. That is, use
--   
--   <pre>
--   Args (WrapFull c) ...
--   </pre>
--   
--   instead of
--   
--   <pre>
--   Args c ...
--   </pre>
--   
--   if <tt>c</tt> is not indexed by <tt>(<a>Full</a> a)</tt>.
data WrapFull c a
WrapFull :: c a -> WrapFull c (Full a)
unwrapFull :: WrapFull c (Full a) -> c a

-- | Convert an <a>AST</a> to a <a>Tree</a>
toTree :: (forall sig. dom sig -> b) -> ASTF dom a -> Tree b

module Language.Syntactic.Interpretation.Equality

-- | Equality for expressions
class Equality expr
equal :: Equality expr => expr a -> expr b -> Bool
exprHash :: Equality expr => expr a -> Hash
instance (Equality expr1, Equality expr2) => Eq ((:+:) expr1 expr2 a)
instance (Equality expr1, Equality expr2) => Equality (expr1 :+: expr2)
instance Equality dom => Eq (AST dom a)
instance Equality dom => Equality (AST dom)

module Language.Syntactic.Interpretation.Render

-- | Render a symbol as concrete syntax. A complete instance must define at
--   least the <a>renderSym</a> method.
class Render dom where renderArgs [] a = renderSym a renderArgs args a = "(" ++ unwords (renderSym a : args) ++ ")"
renderSym :: Render dom => dom sig -> String
renderArgs :: Render dom => [String] -> dom sig -> String

-- | Render an expression as concrete syntax
render :: Render dom => ASTF dom a -> String

-- | Convert a symbol to a <a>Tree</a> of strings
class Render dom => StringTree dom where stringTreeSym args a = Node (renderSym a) args
stringTreeSym :: StringTree dom => [Tree String] -> dom a -> Tree String

-- | Convert an expression to a <a>Tree</a> of strings
stringTree :: StringTree dom => ASTF dom a -> Tree String

-- | Show a syntax tree using ASCII art
showAST :: StringTree dom => ASTF dom a -> String

-- | Print a syntax tree using ASCII art
drawAST :: StringTree dom => ASTF dom a -> IO ()
writeHtmlAST :: StringTree sym => FilePath -> ASTF sym a -> IO ()
instance (StringTree dom1, StringTree dom2) => StringTree (dom1 :+: dom2)
instance Render dom => Show (ASTF dom a)
instance (Render expr1, Render expr2) => Render (expr1 :+: expr2)

module Language.Syntactic.Interpretation.Evaluation

-- | The denotation of a symbol with the given signature
class Eval expr
evaluate :: Eval expr => expr a -> Denotation a
instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)
instance Eval dom => Eval (AST dom)


-- | Default implementations of some interpretation functions
module Language.Syntactic.Interpretation.Semantics

-- | A representation of a syntactic construct as a <a>String</a> and an
--   evaluation function. It is not meant to be used as a syntactic symbol
--   in an <a>AST</a>. Its only purpose is to provide the default
--   implementations of functions like <a>equal</a> via the <a>Semantic</a>
--   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 <a>equal</a>
equalDefault :: Semantic expr => expr a -> expr b -> Bool

-- | Default implementation of <a>exprHash</a>
exprHashDefault :: Semantic expr => expr a -> Hash

-- | Default implementation of <a>renderSym</a>
renderSymDefault :: Semantic expr => expr a -> String

-- | Default implementation of <a>renderArgs</a>
renderArgsDefault :: Semantic expr => [String] -> expr a -> String

-- | Default implementation of <a>evaluate</a>
evaluateDefault :: Semantic expr => expr a -> Denotation a

-- | Derive instances for <a>Semantic</a> related classes (<a>Equality</a>,
--   <a>Render</a>, <a>StringTree</a>, <a>Eval</a>)
semanticInstances :: Name -> DecsQ
instance Eval Semantics
instance Render Semantics
instance Equality Semantics


-- | Type-constrained syntax trees
module Language.Syntactic.Constraint

-- | Intersection of type predicates
class (c1 a, c2 a) => (:/\:) c1 c2 a

-- | Universal type predicate
class Top a
pTop :: P Top
pTypeable :: P Typeable

-- | Evidence that the predicate <tt>sub</tt> is a subset of <tt>sup</tt>
type Sub sub sup = forall a. Dict (sub a) -> Dict (sup a)

-- | Weaken an intersection
weakL :: Sub (c1 :/\: c2) c1

-- | Weaken an intersection
weakR :: Sub (c1 :/\: c2) c2

-- | Subset relation on type predicates
class (:<) (sub :: * -> Constraint) (sup :: * -> Constraint)
sub :: :< sub sup => Sub sub sup

-- | Constrain the result type of the expression by the given predicate
data (:|) :: (* -> *) -> (* -> Constraint) -> (* -> *)
C :: expr sig -> (expr :| pred) sig

-- | Constrain the result type of the expression by the given predicate
--   
--   The difference between <a>:||</a> and <a>:|</a> is seen in the
--   instances of the <a>Sat</a> type:
--   
--   <pre>
--   type Sat (dom :|  pred) = pred :/\: Sat dom
--   type Sat (dom :|| pred) = pred
--   </pre>
data (:||) :: (* -> *) -> (* -> Constraint) -> (* -> *)
C' :: expr sig -> (expr :|| pred) sig

-- | Expressions that constrain their result types
class Constrained expr where type family Sat expr :: * -> Constraint
exprDict :: Constrained expr => expr a -> Dict (Sat expr (DenResult a))
type ConstrainedBy expr p = (Constrained expr, Sat expr :< p)

-- | A version of <a>exprDict</a> that returns a constraint for a
--   particular predicate <tt>p</tt> as long as <tt>(p :&lt; Sat dom)</tt>
--   holds
exprDictSub :: ConstrainedBy expr p => P p -> expr a -> Dict (p (DenResult a))

-- | A version of <a>exprDict</a> that works for domains of the form
--   <tt>(dom1 :+: dom2)</tt> as long as <tt>(Sat dom1 ~ Sat dom2)</tt>
--   holds
exprDictPlus :: (Constrained dom1, Constrained dom2, Sat dom1 ~ Sat dom2) => AST (dom1 :+: dom2) a -> Dict (Sat dom1 (DenResult a))

-- | Symbol injection (like <a>:&lt;:</a>) with constrained result types
class (Project sub sup, Sat sup a) => InjectC sub sup a
injC :: (InjectC sub sup a, DenResult sig ~ a) => sub sig -> sup sig

-- | Generic symbol application
--   
--   <a>appSymC</a> has any type of the form:
--   
--   <pre>
--   appSymC :: InjectC expr (AST dom) x
--       =&gt; expr (a :-&gt; b :-&gt; ... :-&gt; Full x)
--       -&gt; (ASTF dom a -&gt; ASTF dom b -&gt; ... -&gt; ASTF dom x)
--   </pre>
appSymC :: (ApplySym sig f dom, InjectC sym (AST dom) (DenResult sig)) => sym sig -> f

-- | Similar to <a>:||</a>, but rather than constraining the whole result
--   type, it assumes a result type of the form <tt>c a</tt> and constrains
--   the <tt>a</tt>.
data SubConstr1 :: (* -> *) -> (* -> *) -> (* -> Constraint) -> (* -> *)
SubConstr1 :: dom sig -> SubConstr1 c dom p sig

-- | Similar to <a>SubConstr1</a>, but assumes a result type of the form
--   <tt>c a b</tt> and constrains both <tt>a</tt> and <tt>b</tt>.
data SubConstr2 :: (* -> * -> *) -> (* -> *) -> (* -> Constraint) -> (* -> Constraint) -> (* -> *)
SubConstr2 :: dom sig -> SubConstr2 c dom pa pb sig

-- | <a>AST</a> with existentially quantified result type
data ASTE :: (* -> *) -> *
ASTE :: ASTF dom a -> ASTE dom
liftASTE :: (forall a. ASTF dom a -> b) -> ASTE dom -> b
liftASTE2 :: (forall a b. ASTF dom a -> ASTF dom b -> c) -> ASTE dom -> ASTE dom -> c

-- | <a>AST</a> with bounded existentially quantified result type
data ASTB :: (* -> *) -> (* -> Constraint) -> *
ASTB :: ASTF dom a -> ASTB dom p
liftASTB :: (forall a. p a => ASTF dom a -> b) -> ASTB dom p -> b
liftASTB2 :: (forall a b. (p a, p b) => ASTF dom a -> ASTF dom b -> c) -> ASTB dom p -> ASTB dom p -> c
type ASTSAT dom = ASTB dom (Sat dom)

-- | Empty symbol type
--   
--   Use-case:
--   
--   <pre>
--   data A a
--   data B a
--   
--   test :: AST (A :+: (B:||Eq) :+: Empty) a
--   test = injC (undefined :: (B :|| Eq) a)
--   </pre>
--   
--   Without <a>Empty</a>, this would lead to an overlapping instance error
--   due to the instances
--   
--   <pre>
--   InjectC (B :|| Eq) (B :|| Eq) (DenResult a)
--   </pre>
--   
--   and
--   
--   <pre>
--   InjectC sub sup a, pred a) =&gt; InjectC sub (sup :|| pred) a
--   </pre>
data Empty :: * -> *
universe :: ASTF dom a -> [ASTE dom]
instance [overlap ok] StringTree Empty
instance [overlap ok] Render Empty
instance [overlap ok] Eval Empty
instance [overlap ok] Equality Empty
instance [overlap ok] Constrained Empty
instance [overlap ok] Eval dom => Eval (SubConstr2 c dom pa pb)
instance [overlap ok] StringTree dom => StringTree (SubConstr2 c dom pa pb)
instance [overlap ok] Render dom => Render (SubConstr2 c dom pa pb)
instance [overlap ok] Equality dom => Equality (SubConstr2 c dom pa pb)
instance [overlap ok] Project sub sup => Project sub (SubConstr2 c sup pa pb)
instance [overlap ok] Constrained dom => Constrained (SubConstr2 c dom pa pb)
instance [overlap ok] Eval dom => Eval (SubConstr1 c dom p)
instance [overlap ok] StringTree dom => StringTree (SubConstr1 c dom p)
instance [overlap ok] Render dom => Render (SubConstr1 c dom p)
instance [overlap ok] Equality dom => Equality (SubConstr1 c dom p)
instance [overlap ok] Project sub sup => Project sub (SubConstr1 c sup p)
instance [overlap ok] Constrained dom => Constrained (SubConstr1 c dom p)
instance [overlap ok] InjectC expr1 expr3 a => InjectC expr1 (expr2 :+: expr3) a
instance [overlap ok] InjectC expr1 (expr1 :+: expr2) a
instance [overlap ok] (Sat expr a) => InjectC expr expr a
instance [overlap ok] (InjectC sub sup a, pred a) => InjectC sub (sup :|| pred) a
instance [overlap ok] (InjectC sub sup a, pred a) => InjectC sub (sup :| pred) a
instance [overlap ok] InjectC sub sup a => InjectC sub (AST sup) a
instance [overlap ok] Constrained (dom :|| pred)
instance [overlap ok] Constrained dom => Constrained (dom :| pred)
instance [overlap ok] Constrained (sub1 :+: sub2)
instance [overlap ok] Constrained dom => Constrained (AST dom)
instance [overlap ok] StringTree dom => StringTree (dom :|| pred)
instance [overlap ok] Eval dom => Eval (dom :|| pred)
instance [overlap ok] Render dom => Render (dom :|| pred)
instance [overlap ok] Equality dom => Equality (dom :|| pred)
instance [overlap ok] Project sub sup => Project sub (sup :|| pred)
instance [overlap ok] StringTree dom => StringTree (dom :| pred)
instance [overlap ok] Eval dom => Eval (dom :| pred)
instance [overlap ok] Render dom => Render (dom :| pred)
instance [overlap ok] Equality dom => Equality (dom :| pred)
instance [overlap ok] Project sub sup => Project sub (sup :| pred)
instance [overlap ok] ps :< q => (p :/\: ps) :< q
instance [overlap ok] (p :/\: ps) :< p
instance [overlap ok] p :< p
instance [overlap ok] Top a
instance [overlap ok] (c1 a, c2 a) => (:/\:) c1 c2 a


-- | "Syntactic sugar"
module Language.Syntactic.Sugar

-- | It is usually assumed that <tt>(<a>desugar</a> (<a>sugar</a> a))</tt>
--   has the same meaning as <tt>a</tt>.
class Syntactic a where type family Domain a :: * -> * type family Internal a
desugar :: Syntactic a => a -> ASTF (Domain a) (Internal a)
sugar :: Syntactic a => ASTF (Domain a) (Internal a) -> a

-- | Syntactic type casting
resugar :: (Syntactic a, Syntactic b, Domain a ~ Domain b, Internal a ~ Internal b) => a -> b

-- | N-ary syntactic functions
--   
--   <a>desugarN</a> has any type of the form:
--   
--   <pre>
--   desugarN ::
--       ( Syntactic a
--       , Syntactic b
--       , ...
--       , Syntactic x
--       , Domain a ~ dom
--       , Domain b ~ dom
--       , ...
--       , Domain x ~ dom
--       ) =&gt; (a -&gt; b -&gt; ... -&gt; x)
--         -&gt; (  ASTF dom (Internal a)
--            -&gt; ASTF dom (Internal b)
--            -&gt; ...
--            -&gt; ASTF dom (Internal x)
--            )
--   </pre>
--   
--   ...and vice versa for <a>sugarN</a>.
class SyntacticN a internal | a -> internal
desugarN :: SyntacticN a internal => a -> internal
sugarN :: SyntacticN a internal => internal -> a

-- | "Sugared" symbol application
--   
--   <a>sugarSym</a> has any type of the form:
--   
--   <pre>
--   sugarSym ::
--       ( expr :&lt;: AST dom
--       , Syntactic a dom
--       , Syntactic b dom
--       , ...
--       , Syntactic x dom
--       ) =&gt; expr (Internal a :-&gt; Internal b :-&gt; ... :-&gt; Full (Internal x))
--         -&gt; (a -&gt; b -&gt; ... -&gt; x)
--   </pre>
sugarSym :: (sym :<: AST dom, ApplySym sig b dom, SyntacticN c b) => sym sig -> c

-- | "Sugared" symbol application
--   
--   <a>sugarSymC</a> has any type of the form:
--   
--   <pre>
--   sugarSymC ::
--       ( InjectC expr (AST dom) (Internal x)
--       , Syntactic a dom
--       , Syntactic b dom
--       , ...
--       , Syntactic x dom
--       ) =&gt; expr (Internal a :-&gt; Internal b :-&gt; ... :-&gt; Full (Internal x))
--         -&gt; (a -&gt; b -&gt; ... -&gt; x)
--   </pre>
sugarSymC :: (InjectC sym (AST dom) (DenResult sig), ApplySym sig b dom, SyntacticN c b) => sym sig -> c
instance [overlap ok] (Syntactic a, Domain a ~ dom, ia ~ Internal a, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib)
instance [overlap ok] (Syntactic a, Domain a ~ dom, ia ~ AST dom (Full (Internal a))) => SyntacticN a ia
instance [overlap ok] Syntactic (ASTF dom a)


-- | The basic parts of the syntactic library
module Language.Syntactic


-- | Conditional expressions
module Language.Syntactic.Constructs.Condition
data Condition sig
Condition :: Condition (Bool :-> (a :-> (a :-> Full a)))
instance Eval Condition
instance StringTree Condition
instance Render Condition
instance Equality Condition
instance Semantic Condition
instance Constrained Condition


-- | Provides a simple way to make syntactic constructs for prototyping.
--   Note that <a>Construct</a> is quite unsafe as it only uses
--   <a>String</a> to distinguish between different constructs. Also,
--   <a>Construct</a> has a very free type that allows any number of
--   arguments.
module Language.Syntactic.Constructs.Construct
data Construct sig
Construct :: String -> Denotation sig -> Construct sig
instance Eval Construct
instance StringTree Construct
instance Render Construct
instance Equality Construct
instance Semantic Construct
instance Constrained Construct


-- | Construct for decorating expressions with additional information
module Language.Syntactic.Constructs.Decoration

-- | Decorating symbols with additional information
--   
--   One usage of <a>Decor</a> is to decorate every node of a syntax tree.
--   This is done simply by changing
--   
--   <pre>
--   AST dom sig
--   </pre>
--   
--   to
--   
--   <pre>
--   AST (Decor info dom) sig
--   </pre>
data Decor info expr sig
Decor :: info (DenResult sig) -> expr sig -> Decor info expr sig
decorInfo :: Decor info expr sig -> info (DenResult sig)
decorExpr :: Decor info expr sig -> expr sig

-- | Get the decoration of the top-level node
getInfo :: AST (Decor info dom) sig -> info (DenResult sig)

-- | 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 <a>Decor</a> expression. This function is
--   convenient to use together with e.g. <tt>queryNodeSimple</tt> when the
--   domain has the form <tt>(<a>Decor</a> info dom)</tt>.
liftDecor :: (expr s -> info (DenResult s) -> b) -> (Decor info expr s -> b)

-- | Collect the decorations of all nodes
collectInfo :: (forall sig. info sig -> b) -> AST (Decor info dom) sig -> [b]

-- | Rendering of decorated syntax trees
stringTreeDecor :: StringTree dom => (forall a. info a -> String) -> ASTF (Decor info dom) a -> Tree String

-- | Show an decorated syntax tree using ASCII art
showDecorWith :: StringTree dom => (forall a. info a -> String) -> ASTF (Decor info dom) a -> String

-- | Print an decorated syntax tree using ASCII art
drawDecorWith :: StringTree dom => (forall a. info a -> String) -> ASTF (Decor info dom) a -> IO ()

-- | Strip decorations from an <a>AST</a>
stripDecor :: AST (Decor info dom) sig -> AST dom sig
instance Eval expr => Eval (Decor info expr)
instance StringTree expr => StringTree (Decor info expr)
instance Render expr => Render (Decor info expr)
instance Equality expr => Equality (Decor info expr)
instance Project sub sup => Project sub (Decor info sup)
instance Constrained expr => Constrained (Decor info expr)


-- | Identity function
module Language.Syntactic.Constructs.Identity

-- | Identity function
data Identity sig
Id :: Identity (a :-> Full a)
instance Eval Identity
instance StringTree Identity
instance Render Identity
instance Equality Identity
instance Semantic Identity
instance Constrained Identity


-- | Literal expressions
module Language.Syntactic.Constructs.Literal
data Literal sig
Literal :: a -> Literal (Full a)
instance Eval Literal
instance StringTree Literal
instance Render Literal
instance Equality Literal
instance Constrained Literal


-- | Monadic constructs
--   
--   This module is based on the paper <i>Generic Monadic Constructs for
--   Embedded Languages</i> (Persson et al., IFL 2011
--   <a>http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf</a>).
module Language.Syntactic.Constructs.Monad
data MONAD m sig
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 :: Project (MONAD m) sup => P m -> sup sig -> Maybe (MONAD m sig)
instance Monad m => StringTree (MONAD m)
instance Monad m => Eval (MONAD m)
instance Monad m => Render (MONAD m)
instance Monad m => Equality (MONAD m)
instance Monad m => Semantic (MONAD m)
instance Constrained (MONAD m)


-- | Construction and elimination of tuples in the object language
module Language.Syntactic.Constructs.Tuple

-- | Expressions for constructing tuples
data Tuple sig
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))))))))
Tup8 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> Full (a, b, c, d, e, f, g, h)))))))))
Tup9 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> Full (a, b, c, d, e, f, g, h, i))))))))))
Tup10 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> Full (a, b, c, d, e, f, g, h, i, j)))))))))))
Tup11 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> Full (a, b, c, d, e, f, g, h, i, j, k))))))))))))
Tup12 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> Full (a, b, c, d, e, f, g, h, i, j, k, l)))))))))))))
Tup13 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> (m :-> Full (a, b, c, d, e, f, g, h, i, j, k, l, m))))))))))))))
Tup14 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> (m :-> (n :-> Full (a, b, c, d, e, f, g, h, i, j, k, l, m, n)))))))))))))))
Tup15 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> (m :-> (n :-> (o :-> Full (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o))))))))))))))))

-- | These families (<a>Sel1'</a> - <a>Sel15'</a>) are needed because of
--   the problem described in:
--   
--   
--   <a>http://emil-fp.blogspot.com/2011/08/fundeps-weaker-than-type-families.html</a>

-- | 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)
Sel8 :: Select (a :-> Full b)
Sel9 :: Select (a :-> Full b)
Sel10 :: Select (a :-> Full b)
Sel11 :: Select (a :-> Full b)
Sel12 :: Select (a :-> Full b)
Sel13 :: Select (a :-> Full b)
Sel14 :: Select (a :-> Full b)
Sel15 :: Select (a :-> Full b)

-- | Return the selected position, e.g.
--   
--   <pre>
--   selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-&gt; Full Int)) = 3
--   </pre>
selectPos :: Select a -> Int
instance Eval Select
instance StringTree Select
instance Render Select
instance Equality Select
instance Semantic Select
instance Constrained Select
instance Eval Tuple
instance StringTree Tuple
instance Render Tuple
instance Equality Tuple
instance Semantic Tuple
instance Constrained Tuple


-- | <a>Syntactic</a> instances for Haskell tuples
module Language.Syntactic.Frontend.Tuple
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, Syntactic m, Domain m ~ dom, Syntactic n, Domain n ~ dom, Syntactic o, Domain o ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m, Internal n, Internal o), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h), InjectC Select dom (Internal i), InjectC Select dom (Internal j), InjectC Select dom (Internal k), InjectC Select dom (Internal l), InjectC Select dom (Internal m), InjectC Select dom (Internal n), InjectC Select dom (Internal o)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, Syntactic m, Domain m ~ dom, Syntactic n, Domain n ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m, Internal n), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h), InjectC Select dom (Internal i), InjectC Select dom (Internal j), InjectC Select dom (Internal k), InjectC Select dom (Internal l), InjectC Select dom (Internal m), InjectC Select dom (Internal n)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l, m, n)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, Syntactic m, Domain m ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h), InjectC Select dom (Internal i), InjectC Select dom (Internal j), InjectC Select dom (Internal k), InjectC Select dom (Internal l), InjectC Select dom (Internal m)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l, m)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h), InjectC Select dom (Internal i), InjectC Select dom (Internal j), InjectC Select dom (Internal k), InjectC Select dom (Internal l)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h), InjectC Select dom (Internal i), InjectC Select dom (Internal j), InjectC Select dom (Internal k)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h), InjectC Select dom (Internal i), InjectC Select dom (Internal j)) => Syntactic (a, b, c, d, e, f, g, h, i, j)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h), InjectC Select dom (Internal i)) => Syntactic (a, b, c, d, e, f, g, h, i)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g), InjectC Select dom (Internal h)) => Syntactic (a, b, c, d, e, f, g, h)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f), InjectC Select dom (Internal g)) => Syntactic (a, b, c, d, e, f, g)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e), InjectC Select dom (Internal f)) => Syntactic (a, b, c, d, e, f)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d, Internal e), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d), InjectC Select dom (Internal e)) => Syntactic (a, b, c, d, e)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c, Internal d), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c), InjectC Select dom (Internal d)) => Syntactic (a, b, c, d)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, InjectC Tuple dom (Internal a, Internal b, Internal c), InjectC Select dom (Internal a), InjectC Select dom (Internal b), InjectC Select dom (Internal c)) => Syntactic (a, b, c)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, InjectC Tuple dom (Internal a, Internal b), InjectC Select dom (Internal a), InjectC Select dom (Internal b)) => Syntactic (a, b)


-- | Constrained <a>Syntactic</a> instances for Haskell tuples
module Language.Syntactic.Frontend.TupleConstrained

-- | Type-level function computing the predicate attached to <a>Tuple</a>
--   or <a>Select</a> (whichever appears first) in a domain.
class TupleSat (dom :: * -> *) (p :: * -> Constraint) | dom -> p
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, Syntactic m, Domain m ~ dom, Syntactic n, Domain n ~ dom, Syntactic o, Domain o ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m, Internal n, Internal o), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), p (Internal i), p (Internal j), p (Internal k), p (Internal l), p (Internal m), p (Internal n), p (Internal o), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m, Internal n, Internal o), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h), InjectC (Select :|| p) dom (Internal i), InjectC (Select :|| p) dom (Internal j), InjectC (Select :|| p) dom (Internal k), InjectC (Select :|| p) dom (Internal l), InjectC (Select :|| p) dom (Internal m), InjectC (Select :|| p) dom (Internal n), InjectC (Select :|| p) dom (Internal o)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, Syntactic m, Domain m ~ dom, Syntactic n, Domain n ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m, Internal n), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), p (Internal i), p (Internal j), p (Internal k), p (Internal l), p (Internal m), p (Internal n), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m, Internal n), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h), InjectC (Select :|| p) dom (Internal i), InjectC (Select :|| p) dom (Internal j), InjectC (Select :|| p) dom (Internal k), InjectC (Select :|| p) dom (Internal l), InjectC (Select :|| p) dom (Internal m), InjectC (Select :|| p) dom (Internal n)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l, m, n)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, Syntactic m, Domain m ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), p (Internal i), p (Internal j), p (Internal k), p (Internal l), p (Internal m), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l, Internal m), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h), InjectC (Select :|| p) dom (Internal i), InjectC (Select :|| p) dom (Internal j), InjectC (Select :|| p) dom (Internal k), InjectC (Select :|| p) dom (Internal l), InjectC (Select :|| p) dom (Internal m)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l, m)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, Syntactic l, Domain l ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), p (Internal i), p (Internal j), p (Internal k), p (Internal l), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k, Internal l), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h), InjectC (Select :|| p) dom (Internal i), InjectC (Select :|| p) dom (Internal j), InjectC (Select :|| p) dom (Internal k), InjectC (Select :|| p) dom (Internal l)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k, l)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, Syntactic k, Domain k ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), p (Internal i), p (Internal j), p (Internal k), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j, Internal k), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h), InjectC (Select :|| p) dom (Internal i), InjectC (Select :|| p) dom (Internal j), InjectC (Select :|| p) dom (Internal k)) => Syntactic (a, b, c, d, e, f, g, h, i, j, k)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, Syntactic j, Domain j ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), p (Internal i), p (Internal j), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i, Internal j), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h), InjectC (Select :|| p) dom (Internal i), InjectC (Select :|| p) dom (Internal j)) => Syntactic (a, b, c, d, e, f, g, h, i, j)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, Syntactic i, Domain i ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), p (Internal i), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h, Internal i), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h), InjectC (Select :|| p) dom (Internal i)) => Syntactic (a, b, c, d, e, f, g, h, i)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, Syntactic h, Domain h ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), p (Internal h), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g, Internal h), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g), InjectC (Select :|| p) dom (Internal h)) => Syntactic (a, b, c, d, e, f, g, h)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, Syntactic g, Domain g ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), p (Internal g), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f), InjectC (Select :|| p) dom (Internal g)) => Syntactic (a, b, c, d, e, f, g)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, Syntactic f, Domain f ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), p (Internal f), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e), InjectC (Select :|| p) dom (Internal f)) => Syntactic (a, b, c, d, e, f)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, Syntactic e, Domain e ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d, Internal e), p (Internal a), p (Internal b), p (Internal c), p (Internal d), p (Internal e), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d, Internal e), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d), InjectC (Select :|| p) dom (Internal e)) => Syntactic (a, b, c, d, e)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, Syntactic d, Domain d ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c, Internal d), p (Internal a), p (Internal b), p (Internal c), p (Internal d), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c, Internal d), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c), InjectC (Select :|| p) dom (Internal d)) => Syntactic (a, b, c, d)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Syntactic c, Domain c ~ dom, TupleSat dom p, p (Internal a, Internal b, Internal c), p (Internal a), p (Internal b), p (Internal c), InjectC (Tuple :|| p) dom (Internal a, Internal b, Internal c), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b), InjectC (Select :|| p) dom (Internal c)) => Syntactic (a, b, c)
instance [overlap ok] (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, TupleSat dom p, p (Internal a, Internal b), p (Internal a), p (Internal b), InjectC (Tuple :|| p) dom (Internal a, Internal b), InjectC (Select :|| p) dom (Internal a), InjectC (Select :|| p) dom (Internal b)) => Syntactic (a, b)
instance [overlap ok] TupleSat dom2 p => TupleSat (dom1 :+: dom2) p
instance [overlap ok] TupleSat dom p => TupleSat (dom :|| q) p
instance [overlap ok] TupleSat dom p => TupleSat (dom :| q) p
instance [overlap ok] TupleSat ((Select :|| p) :+: dom2) p
instance [overlap ok] TupleSat (Select :|| p) p
instance [overlap ok] TupleSat ((Tuple :|| p) :+: dom2) p
instance [overlap ok] TupleSat (Tuple :|| p) p


-- | General binding constructs
module Language.Syntactic.Constructs.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))

-- | Allow an existing binding to be used with a body of a different type
reuseLambda :: Lambda (b :-> Full (a -> b)) -> Lambda (c :-> Full (a -> c))

-- | Let binding
--   
--   <a>Let</a> is just an application operator with flipped argument
--   order. The argument <tt>(a -&gt; b)</tt> is preferably constructed by
--   <a>Lambda</a>.
data Let a
Let :: Let (a :-> ((a -> b) :-> Full b))

-- | Should be a capture-avoiding substitution, but it is currently not
--   correct.
--   
--   Note: Variables with a different type than the new expression will be
--   silently ignored.
subst :: (ConstrainedBy dom Typeable, Project Lambda dom, Project Variable dom) => 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 <a>Lambda</a>.
betaReduce :: (ConstrainedBy dom Typeable, Project Lambda dom, Project Variable dom) => ASTF dom a -> ASTF dom (a -> b) -> ASTF dom b

-- | Evaluation of expressions with variables
class EvalBind sub
evalBindSym :: (EvalBind sub, EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => sub sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

-- | Evaluation of possibly open expressions
evalBindM :: (EvalBind dom, ConstrainedBy dom Typeable) => ASTF dom a -> Reader [(VarId, Dynamic)] a

-- | Evaluation of closed expressions
evalBind :: (EvalBind dom, ConstrainedBy dom Typeable) => ASTF dom a -> a

-- | Apply a symbol denotation to a list of arguments
appDen :: Denotation sig -> Args Identity sig -> DenResult sig

-- | Convenient default implementation of <a>evalBindSym</a>
evalBindSymDefault :: (Eval sub, EvalBind dom, ConstrainedBy dom Typeable) => sub sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

-- | 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)

-- | Alpha-equivalence
class AlphaEq sub1 sub2 dom env
alphaEqSym :: AlphaEq sub1 sub2 dom env => 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 => 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 :: (Equality sub, AlphaEq dom dom dom env) => 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 Eq VarId
instance Ord VarId
instance Num VarId
instance Real VarId
instance Integral VarId
instance Enum VarId
instance Ix VarId
instance (AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Lambda Lambda dom env
instance (AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env
instance (AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env
instance AlphaEq sub sub dom env => AlphaEq (Decor info sub) (Decor info sub) dom env
instance AlphaEq dom dom dom env => AlphaEq Tuple Tuple dom env
instance AlphaEq dom dom dom env => AlphaEq Select Select dom env
instance AlphaEq dom dom dom env => AlphaEq Literal Literal dom env
instance AlphaEq dom dom dom env => AlphaEq Let Let dom env
instance AlphaEq dom dom dom env => AlphaEq Identity Identity dom env
instance AlphaEq dom dom dom env => AlphaEq Construct Construct dom env
instance AlphaEq dom dom dom env => AlphaEq Condition Condition dom env
instance AlphaEq Empty Empty dom env
instance AlphaEq sub sub dom env => AlphaEq (SubConstr2 c sub pa pb) (SubConstr2 c sub pa pb) dom env
instance AlphaEq sub sub dom env => AlphaEq (SubConstr1 c sub p) (SubConstr1 c sub p) dom env
instance AlphaEq sub sub dom env => AlphaEq (sub :|| pred) (sub :|| pred) dom env
instance AlphaEq sub sub dom env => AlphaEq (sub :| pred) (sub :| pred) dom env
instance (AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => AlphaEq (subA1 :+: subA2) (subB1 :+: subB2) dom env
instance VarEqEnv [(VarId, VarId)]
instance EvalBind Lambda
instance EvalBind Variable
instance Monad m => EvalBind (MONAD m)
instance EvalBind Let
instance EvalBind Select
instance EvalBind Tuple
instance EvalBind Condition
instance EvalBind Literal
instance EvalBind Construct
instance EvalBind Identity
instance EvalBind dom => EvalBind (Decor info dom)
instance EvalBind Empty
instance EvalBind dom => EvalBind (SubConstr2 c dom pa pb)
instance EvalBind dom => EvalBind (SubConstr1 c dom p)
instance EvalBind dom => EvalBind (dom :|| pred)
instance EvalBind dom => EvalBind (dom :| pred)
instance (EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2)
instance Eval Let
instance StringTree Let
instance Render Let
instance Equality Let
instance Constrained Let
instance StringTree Lambda
instance Render Lambda
instance Equality Lambda
instance Constrained Lambda
instance StringTree Variable
instance Render Variable
instance Equality Variable
instance Constrained Variable
instance Show VarId


-- | This module provides binding constructs using higher-order syntax and
--   a function (<a>reify</a>) for translating to first-order syntax.
--   Expressions constructed using the exported interface (specifically,
--   not introducing <a>Variable</a>s explicitly) are guaranteed to have
--   well-behaved translation.
module Language.Syntactic.Constructs.Binding.HigherOrder

-- | Variables
data Variable a

-- | Let binding
--   
--   <a>Let</a> is just an application operator with flipped argument
--   order. The argument <tt>(a -&gt; b)</tt> is preferably constructed by
--   <a>Lambda</a>.
data Let a
Let :: Let (a :-> ((a -> b) :-> Full b))

-- | Higher-order lambda binding
data HOLambda dom p pVar a
HOLambda :: (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b) -> HOLambda dom p pVar (Full (a -> b))

-- | Adding support for higher-order abstract syntax to a domain
type HODomain dom p pVar = (HOLambda dom p pVar :+: ((Variable :|| pVar) :+: dom)) :|| p

-- | Equivalent to <a>HODomain</a> (including type constraints), but using
--   a first-order representation of binding
type FODomain dom p pVar = (CLambda pVar :+: ((Variable :|| pVar) :+: dom)) :|| p

-- | <a>Lambda</a> with a constraint on the bound variable type
type CLambda pVar = SubConstr2 (->) Lambda pVar Top

-- | An abstraction of <a>HODomain</a>
class IsHODomain dom p pVar | dom -> p pVar
lambda :: (IsHODomain dom p pVar, p (a -> b), p a, pVar a) => (ASTF dom a -> ASTF dom b) -> ASTF dom (a -> b)
reifyM :: AST (HODomain dom p pVar) a -> State VarId (AST (FODomain dom p pVar) a)

-- | Translating expressions with higher-order binding to corresponding
--   expressions using first-order binding
reifyTop :: AST (HODomain dom p pVar) a -> AST (FODomain dom p pVar) a

-- | Reify an n-ary syntactic function
reify :: (Syntactic a, Domain a ~ HODomain dom p pVar) => a -> ASTF (FODomain dom p pVar) (Internal a)
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, IsHODomain dom p pVar, p (Internal a -> Internal b), p (Internal a), pVar (Internal a)) => Syntactic (a -> b)
instance IsHODomain (HODomain dom p pVar) p pVar


-- | Monadic constructs
--   
--   This module is based on the paper <i>Generic Monadic Constructs for
--   Embedded Languages</i> (Persson et al., IFL 2011
--   <a>http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf</a>).
module Language.Syntactic.Frontend.Monad

-- | User interface to embedded monadic programs
newtype Mon dom m a
Mon :: (forall r. (Monad m, Typeable r, InjectC (MONAD m) dom (m r)) => Cont (ASTF dom (m r)) a) -> Mon dom m a
unMon :: Mon dom m a -> forall r. (Monad m, Typeable r, InjectC (MONAD m) dom (m r)) => Cont (ASTF dom (m r)) a

-- | One-layer desugaring of monadic actions
desugarMonad :: (IsHODomain dom Typeable pVar, InjectC (MONAD m) dom (m a), Monad m, Typeable1 m, Typeable a) => Mon dom m (ASTF dom a) -> ASTF dom (m a)

-- | One-layer sugaring of monadic actions
sugarMonad :: (IsHODomain dom Typeable pVar, Monad m, Typeable1 m, Typeable a, pVar a) => ASTF dom (m a) -> Mon dom m (ASTF dom a)
instance Functor (Mon dom m)
instance (Syntactic a, Domain a ~ dom, IsHODomain dom Typeable pVar, InjectC (MONAD m) dom (m (Internal a)), Monad m, Typeable1 m, Typeable (Internal a), pVar (Internal a)) => Syntactic (Mon dom m a)
instance (Monad m, Applicative m) => Applicative (Mon dom m)
instance Monad m => Monad (Mon dom m)


-- | Basic optimization
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 <a>Literal</a>, if the
--   relevant type constraints are satisfied.
type ConstFolder dom = forall a. ASTF dom a -> a -> ASTF dom a

-- | Basic optimization
class Optimize sym
optimizeSym :: (Optimize sym, Optimize' dom) => ConstFolder dom -> (sym sig -> AST dom sig) -> sym sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig))
type Optimize' dom = (Optimize dom, EvalBind dom, AlphaEq dom dom dom [(VarId, VarId)], ConstrainedBy dom Typeable)
optimizeM :: Optimize' dom => ConstFolder dom -> ASTF dom a -> Writer (Set VarId) (ASTF dom a)

-- | Optimize an expression
optimize :: Optimize' dom => ConstFolder dom -> ASTF dom a -> ASTF dom a

-- | Convenient default implementation of <a>optimizeSym</a> (uses
--   <a>evalBind</a> to partially evaluate)
optimizeSymDefault :: Optimize' dom => ConstFolder dom -> (sym sig -> AST dom sig) -> sym sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig))
instance Optimize Lambda
instance Optimize Variable
instance Optimize Condition
instance Optimize Let
instance Optimize Select
instance Optimize Tuple
instance Optimize Literal
instance Optimize Construct
instance Optimize Identity
instance Optimize dom => Optimize (SubConstr2 c dom pa pb)
instance Optimize dom => Optimize (SubConstr1 c dom p)
instance Optimize Empty
instance Optimize dom => Optimize (dom :|| p)
instance Optimize dom => Optimize (dom :| p)
instance (Optimize sub1, Optimize sub2) => Optimize (sub1 :+: sub2)


-- | 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 projecting binding constructs
data PrjDict dom
PrjDict :: (forall sig. dom sig -> Maybe VarId) -> (forall sig. dom sig -> Maybe VarId) -> PrjDict dom
prjVariable :: PrjDict dom -> forall sig. dom sig -> Maybe VarId
prjLambda :: PrjDict dom -> forall sig. dom sig -> Maybe VarId

-- | Interface for injecting binding constructs
data InjDict dom a b
InjDict :: (VarId -> dom (Full a)) -> (VarId -> dom (b :-> Full (a -> b))) -> dom (a :-> ((a -> b) :-> Full b)) -> InjDict dom a b
injVariable :: InjDict dom a b -> VarId -> dom (Full a)
injLambda :: InjDict dom a b -> VarId -> dom (b :-> Full (a -> b))
injLet :: InjDict dom a b -> dom (a :-> ((a -> b) :-> Full b))

-- | A function that, if possible, returns an <a>InjDict</a> for sharing a
--   specific sub-expression. The first argument is the expression to be
--   shared, and the second argument the expression in which it will be
--   shared.
--   
--   This function makes the caller of <a>codeMotion</a> responsible for
--   making sure that the necessary type constraints are fulfilled
--   (otherwise <a>Nothing</a> is returned). It also makes it possible to
--   transfer information, e.g. from the shared expression to the
--   introduced variable.
type MkInjDict dom = forall a b. ASTF dom a -> ASTF dom b -> Maybe (InjDict dom a b)

-- | Perform common sub-expression elimination and variable hoisting
codeMotion :: (ConstrainedBy dom Typeable, AlphaEq dom dom dom [(VarId, VarId)]) => (forall c. ASTF dom c -> Bool) -> PrjDict dom -> MkInjDict dom -> ASTF dom a -> State VarId (ASTF dom a)

-- | A <a>PrjDict</a> implementation for <a>FODomain</a>
prjDictFO :: PrjDict (FODomain dom p pVar)

-- | Like <a>reify</a> but with common sub-expression elimination and
--   variable hoisting
reifySmart :: (AlphaEq dom dom (FODomain dom p pVar) [(VarId, VarId)], Syntactic a, Domain a ~ HODomain dom p pVar, p :< Typeable) => (forall c. ASTF (FODomain dom p pVar) c -> Bool) -> MkInjDict (FODomain dom p pVar) -> a -> ASTF (FODomain dom p pVar) (Internal a)

-- | An <a>MkInjDict</a> implementation for <a>FODomain</a>
--   
--   The supplied function determines whether or not an expression can be
--   shared by returning a witness that the type of the expression
--   satisfies the predicate <tt>pVar</tt>.
mkInjDictFO :: Let :<: dom => (forall a. ASTF (FODomain dom Typeable pVar) a -> Maybe (Dict (pVar a))) -> (forall b. ASTF (FODomain dom Typeable pVar) b -> Bool) -> MkInjDict (FODomain dom Typeable pVar)

module Language.Syntactic.Sharing.CodeMotion2
codeMotion2 :: (ConstrainedBy dom Typeable, AlphaEq dom dom dom [(VarId, VarId)], AlphaEq dom dom (NodeDomain dom) [(VarId, VarId)], Equality dom) => (forall c. ASTF dom c -> Bool) -> PrjDict dom -> MkInjDict dom -> ASTF dom a -> State VarId (ASTF dom a)

-- | Like <a>reify</a> but with common sub-expression elimination and
--   variable hoisting
reifySmart2 :: (AlphaEq dom dom (NodeDomain (FODomain dom p pVar)) [(VarId, VarId)], AlphaEq dom dom (FODomain dom p pVar) [(VarId, VarId)], Equality dom, Syntactic a, Domain a ~ HODomain dom p pVar, p :< Typeable) => (forall c. ASTF (FODomain dom p pVar) c -> Bool) -> MkInjDict (FODomain dom p pVar) -> a -> ASTF (FODomain dom p pVar) (Internal a)
instance Eq NodeId
instance Ord NodeId
instance Num NodeId
instance Real NodeId
instance Integral NodeId
instance Enum NodeId
instance Ix NodeId
instance Show GatherInfo
instance Equality Node
instance Constrained Node
instance AlphaEq dom dom dom env => AlphaEq Node Node dom env
instance Show NodeId


-- | Representation and manipulation of abstract syntax graphs
module Language.Syntactic.Sharing.Graph

-- | Node identifier
newtype NodeId
NodeId :: Integer -> NodeId
nodeInteger :: NodeId -> Integer
showNode :: NodeId -> String

-- | Placeholder for a syntax tree
data Node a
Node :: NodeId -> Node (Full a)

-- | Environment for alpha-equivalence
class NodeEqEnv dom a
prjNodeEqEnv :: NodeEqEnv dom a => a -> NodeEnv dom (Sat dom)
modNodeEqEnv :: NodeEqEnv dom a => (NodeEnv dom (Sat dom) -> NodeEnv dom (Sat dom)) -> (a -> a)
type EqEnv dom p = ([(VarId, VarId)], NodeEnv dom p)
type NodeEnv dom p = (Array NodeId Hash, Array NodeId (ASTB dom p))

-- | "Abstract Syntax Graph"
--   
--   A representation of a syntax tree with explicit sharing. An <a>ASG</a>
--   is valid if and only if <a>inlineAll</a> succeeds (and the
--   <a>numNodes</a> field is correct).
data ASG dom a
ASG :: ASTF (NodeDomain dom) a -> [(NodeId, ASTSAT (NodeDomain dom))] -> NodeId -> ASG dom a

-- | Top-level expression
topExpression :: ASG dom a -> ASTF (NodeDomain dom) a

-- | Mapping from node id to sub-expression
graphNodes :: ASG dom a -> [(NodeId, ASTSAT (NodeDomain dom))]

-- | Total number of nodes
numNodes :: ASG dom a -> NodeId
type NodeDomain dom = (Node :+: dom) :|| Sat dom

-- | Show syntax graph using ASCII art
showASG :: StringTree dom => ASG dom a -> String

-- | Print syntax graph using ASCII art
drawASG :: StringTree dom => ASG dom a -> IO ()

-- | Update the node identifiers in an <a>AST</a> using the supplied
--   reindexing function
reindexNodesAST :: (NodeId -> NodeId) -> AST (NodeDomain dom) a -> AST (NodeDomain 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 dom a -> ASG dom a

-- | Reindex the nodes to be in the range <tt>[0 .. l-1]</tt>, where
--   <tt>l</tt> is the number of nodes in the graph
reindexNodesFrom0 :: ASG dom a -> ASG dom a

-- | Remove duplicate nodes from a graph. The function only looks at the
--   <a>NodeId</a> of each node. The <a>numNodes</a> field is updated
--   accordingly.
nubNodes :: ASG dom a -> ASG dom a

-- | Pattern functor representation of an <a>AST</a> with <a>Node</a>s
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 dom a -> (b, (Array NodeId b, [(NodeId, b)]))

-- | Convert an <a>ASG</a> to an <a>AST</a> by inlining all nodes
inlineAll :: ConstrainedBy dom Typeable => ASG dom a -> ASTF dom a

-- | Find the child nodes of each node in an expression. The child nodes of
--   a node <tt>n</tt> are the first nodes along all paths from <tt>n</tt>.
nodeChildren :: ASG dom a -> [(NodeId, [NodeId])]

-- | Count the number of occurrences of each node in an expression
occurrences :: ASG dom a -> Array NodeId Int

-- | Inline all nodes that are not shared
inlineSingle :: ConstrainedBy dom Typeable => ASG dom a -> ASG dom a

-- | Compute a table (both array and list representation) of hash values
--   for each node
hashNodes :: Equality dom => ASG 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 :: (Equality dom, AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom) (Sat dom))) => ASG dom a -> [[NodeId]]

-- | Common sub-expression elimination based on alpha-equivalence
cse :: (Equality dom, AlphaEq dom dom (NodeDomain dom) (EqEnv (NodeDomain dom) (Sat dom))) => ASG dom a -> ASG 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 Node dom env
instance VarEqEnv (EqEnv dom p)
instance p ~ Sat dom => NodeEqEnv dom (EqEnv dom p)
instance StringTree Node
instance Render Node
instance Constrained Node
instance Show NodeId

module Language.Syntactic.Sharing.StableName

-- | <a>StableName</a> of a <tt>(c (Full a))</tt> with hidden result type
data StName c
StName :: StableName (c (Full a)) -> StName c
hash :: StName c -> Int

-- | A hash table from <a>StName</a> to <a>NodeId</a> (with <a>hash</a> as
--   the hashing function). I.e. it is assumed that the <a>StName</a>s at
--   each entry all have the same hash, and that this number is equal to
--   the entry's key.
type History c = IntMap [(StName c, NodeId)]

-- | Lookup a name in the history
lookHistory :: History c -> StName c -> Maybe NodeId

-- | Insert the name into the history
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 <a>AST</a>
--   
--   This module is based on the paper <i>Type-Safe Observable Sharing in
--   Haskell</i> (Andy Gill, 2009,
--   <a>http://dx.doi.org/10.1145/1596638.1596653</a>).
module Language.Syntactic.Sharing.Reify

-- | Convert a syntax tree to a sharing-preserving graph
--   
--   This function is not referentially transparent (hence the <a>IO</a>).
--   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 :: Constrained dom => (forall a. ASTF dom a -> Bool) -> ASTF dom a -> IO (ASG dom a)


-- | This module is similar to <a>Language.Syntactic.Sharing.Reify</a>, but
--   operates on <tt><a>AST</a> (<a>HODomain</a> dom p)</tt> rather than a
--   general <a>AST</a>. The reason for having this module is that when
--   using <a>HODomain</a>, it is important to do simultaneous sharing
--   analysis and <a>HOLambda</a> reification. Obviously we cannot do
--   sharing analysis first (using <a>reifyGraph</a> from
--   <a>Language.Syntactic.Sharing.Reify</a>), since it needs to be able to
--   look inside <a>HOLambda</a>. On the other hand, if we did
--   <a>HOLambda</a> reification first (using <a>reify</a>), we would
--   destroy the sharing.
--   
--   This module is based on the paper <i>Type-Safe Observable Sharing in
--   Haskell</i> (Andy Gill, 2009,
--   <a>http://dx.doi.org/10.1145/1596638.1596653</a>).
module Language.Syntactic.Sharing.ReifyHO

-- | Convert a syntax tree to a sharing-preserving graph
reifyGraphTop :: (forall a. ASTF (HODomain dom p pVar) a -> Bool) -> ASTF (HODomain dom p pVar) a -> IO (ASG (FODomain dom p pVar) a, VarId)

-- | Reifying an n-ary syntactic function to a sharing-preserving graph
--   
--   This function is not referentially transparent (hence the <a>IO</a>).
--   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, Domain a ~ HODomain dom p pVar) => (forall a. ASTF (HODomain dom p pVar) a -> Bool) -> a -> IO (ASG (FODomain dom p pVar) (Internal a), VarId)