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


-- | Generic representation and manipulation of abstract syntax
--   
--   The library provides a generic representation of type-indexed abstract
--   syntax trees (or indexed data types in general). It also permits the
--   definition of open syntax trees based on the technique in Data Types à
--   la Carte [1].
--   
--   For more information, 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>
--   
--   Example EDSL can be found in the <tt>examples</tt> folder.
--   
--   [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>.
@package syntactic
@version 2.0


-- | 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 Data.Syntactic.Syntax

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

-- | Fully applied abstract syntax tree
type ASTF sym a = AST sym (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 <a>AST</a>
size :: AST sym sig -> Int

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

-- | Witness of the arity of a symbol signature
data SigRep sig
SigFull :: SigRep (Full a)
SigMore :: SigRep sig -> SigRep (a :-> sig)

-- | Symbol signatures
class Signature sig
signature :: Signature sig => SigRep sig

-- | Maps a symbol signature to the type of the corresponding smart
--   constructor:
--   
--   <pre>
--   SmartFun sym (a :-&gt; b :-&gt; ... :-&gt; Full x) = ASTF sym a -&gt; ASTF sym b -&gt; ... -&gt; ASTF sym x
--   </pre>

-- | Maps a smart constructor type to the corresponding symbol signature:
--   
--   <pre>
--   SmartSig (ASTF sym a -&gt; ASTF sym b -&gt; ... -&gt; ASTF sym x) = a :-&gt; b :-&gt; ... :-&gt; Full x
--   </pre>

-- | Returns the symbol in the result of a smart constructor

-- | Make a smart constructor of a symbol. <a>smartSym</a> has any type of
--   the form:
--   
--   <pre>
--   smartSym
--       :: sym (a :-&gt; b :-&gt; ... :-&gt; Full x)
--       -&gt; (ASTF sym a -&gt; ASTF sym b -&gt; ... -&gt; ASTF sym x)
--   </pre>
smartSym' :: (Signature sig, f ~ SmartFun sym sig, sig ~ SmartSig f, sym ~ SmartSym f) => sym sig -> f

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

-- | Symbol projection
--   
--   The class is defined for <i>all pairs of types</i>, but <a>prj</a> can
--   only succeed if <tt>sup</tt> is of the form <tt>(... <a>:+:</a> sub
--   <a>:+:</a> ...)</tt>.
class Project sub sup
prj :: Project sub sup => sup a -> Maybe (sub a)

-- | Symbol injection
--   
--   The class includes types <tt>sub</tt> and <tt>sup</tt> where
--   <tt>sup</tt> is of the form <tt>(... <a>:+:</a> sub <a>:+:</a>
--   ...)</tt>.
class Project sub sup => (:<:) sub sup
inj :: :<: sub sup => sub a -> sup a

-- | Make a smart constructor of a symbol. <a>smartSym</a> has any type of
--   the form:
--   
--   <pre>
--   smartSym :: (sub :&lt;: AST sup)
--       =&gt; sub (a :-&gt; b :-&gt; ... :-&gt; Full x)
--       -&gt; (ASTF sup a -&gt; ASTF sup b -&gt; ... -&gt; ASTF sup x)
--   </pre>
smartSym :: (Signature sig, f ~ SmartFun sup sig, sig ~ SmartSig f, sup ~ SmartSym f, sub :<: sup) => sub sig -> f

-- | Empty symbol type
--   
--   Can be used to make uninhabited <a>AST</a> types. It can also be used
--   as a terminator in co-product lists (e.g. to avoid overlapping
--   instances):
--   
--   <pre>
--   (A :+: B :+: Empty)
--   </pre>
data Empty :: * -> *

-- | Existential quantification
data E e
E :: e a -> E e
liftE :: (forall a. e a -> b) -> E e -> b
liftE2 :: (forall a b. e a -> e b -> c) -> E e -> E e -> c

-- | Existential quantification of <a>Full</a>-indexed type
data EF e
EF :: e (Full a) -> EF e
liftEF :: (forall a. e (Full a) -> b) -> EF e -> b
liftEF2 :: (forall a b. e (Full a) -> e (Full b) -> c) -> EF e -> EF e -> c

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

-- | Projection to a specific symbol type
prjP :: Project sub sup => Proxy 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 sym1, Functor sym2) => Functor (sym1 :+: sym2)
instance [overlap ok] (Foldable sym1, Foldable sym2) => Foldable (sym1 :+: sym2)
instance [overlap ok] (Traversable sym1, Traversable sym2) => Traversable (sym1 :+: sym2)
instance [overlap ok] sym1 :<: sym3 => sym1 :<: (sym2 :+: sym3)
instance [overlap ok] sym1 :<: (sym1 :+: sym2)
instance [overlap ok] sym :<: sym
instance [overlap ok] sub :<: sup => sub :<: AST sup
instance [overlap ok] Project sub sup
instance [overlap ok] Project sym1 sym3 => Project sym1 (sym2 :+: sym3)
instance [overlap ok] Project sym1 (sym1 :+: sym2)
instance [overlap ok] Project sym sym
instance [overlap ok] Project sub sup => Project sub (AST sup)
instance [overlap ok] Signature sig => Signature (a :-> sig)
instance [overlap ok] Signature (Full a)
instance [overlap ok] Functor sym => Functor (AST sym)


-- | Generic traversals of <a>AST</a> terms
module Data.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 sym a -> b) -> (forall a. ASTF sym 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 sym a -> ASTF sym a) -> (forall a. ASTF sym a -> ASTF sym a)

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

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

-- | List all sub-terms (corresponds to <tt>universe</tt> in Uniplate)
universe :: ASTF sym a -> [EF (AST sym)]

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

-- | Right fold for an <a>Args</a> list
foldrArgs :: (forall a. c (Full a) -> b -> b) -> b -> (forall sig. Args c sig -> b)

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

-- | Fold an <a>AST</a> using a list to hold the results of sub-terms
listFold :: (forall sig. sym sig -> [b] -> b) -> (forall a. ASTF sym 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 => sym sig -> Args (AST sym) sig -> c (Full a)) -> ASTF sym a -> c (Full a)

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

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

-- | Simplified version of <a>fold</a> for situations where all
--   intermediate results have the same type
simpleFold :: (forall sig. sym sig -> Args (Const b) sig -> b) -> (forall a. ASTF sym 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 => sym sig -> Args (AST sym) sig -> c (ASTF sym' a)) -> ASTF sym a -> c (ASTF sym' a)

-- | Update the symbols in an AST
mapAST :: (forall sig'. sym1 sig' -> sym2 sig') -> AST sym1 sig -> AST sym2 sig

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


-- | Equality and rendering of <a>AST</a>s
module Data.Syntactic.Interpretation

-- | Higher-kinded equality
class Equality e
equal :: Equality e => e a -> e b -> Bool
hash :: Equality e => e a -> Hash

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

-- | Implementation of <a>renderArgs</a> that handles infix operators
renderArgsSmart :: Render sym => [String] -> sym a -> String

-- | Render an <a>AST</a> as concrete syntax
render :: Render sym => ASTF sym a -> String

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

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

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

-- | Print a syntax tree using ASCII art
drawAST :: StringTree sym => ASTF sym a -> IO ()

-- | Write a syntax tree to an HTML file with foldable nodes
writeHtmlAST :: StringTree sym => FilePath -> ASTF sym a -> IO ()

-- | Default implementation of <a>equal</a>
equalDefault :: Render sym => sym a -> sym b -> Bool

-- | Default implementation of <a>hash</a>
hashDefault :: Render sym => sym a -> Hash

-- | Derive instances for <a>Equality</a> and <a>StringTree</a>
interpretationInstances :: Name -> DecsQ
instance StringTree Empty
instance (StringTree sym1, StringTree sym2) => StringTree (sym1 :+: sym2)
instance Render sym => Show (ASTF sym a)
instance Render Empty
instance (Render sym1, Render sym2) => Render (sym1 :+: sym2)
instance Equality Empty
instance (Equality sym1, Equality sym2) => Eq ((:+:) sym1 sym2 a)
instance (Equality sym1, Equality sym2) => Equality (sym1 :+: sym2)
instance Equality sym => Eq (AST sym a)
instance Equality sym => Equality (AST sym)


-- | "Syntactic sugar"
--   
--   For details, see <a>Combining Deep and Shallow Embedding for EDSL</a>
--   (TFP 2013,
--   <a>http://www.cse.chalmers.se/~emax/documents/svenningsson2013combining.pdf</a>).
module Data.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 ~ sym
--       , Domain b ~ sym
--       , ...
--       , Domain x ~ sym
--       ) =&gt; (a -&gt; b -&gt; ... -&gt; x)
--         -&gt; (  ASTF sym (Internal a)
--            -&gt; ASTF sym (Internal b)
--            -&gt; ...
--            -&gt; ASTF sym (Internal x)
--            )
--   </pre>
--   
--   ...and vice versa for <a>sugarN</a>.
class SyntacticN f internal | f -> internal
desugarN :: SyntacticN f internal => f -> internal
sugarN :: SyntacticN f internal => internal -> f

-- | "Sugared" symbol application
--   
--   <a>sugarSym</a> has any type of the form:
--   
--   <pre>
--   sugarSym ::
--       ( sub :&lt;: AST sup
--       , Syntactic a
--       , Syntactic b
--       , ...
--       , Syntactic x
--       , Domain a ~ Domain b ~ ... ~ Domain x
--       ) =&gt; sub (Internal a :-&gt; Internal b :-&gt; ... :-&gt; Full (Internal x))
--         -&gt; (a -&gt; b -&gt; ... -&gt; x)
--   </pre>
sugarSym :: (Signature sig, fi ~ SmartFun sup sig, sig ~ SmartSig fi, sup ~ SmartSym fi, SyntacticN f fi, sub :<: sup) => sub sig -> f
instance [overlap ok] (Syntactic a, Domain a ~ sym, ia ~ Internal a, SyntacticN f fi) => SyntacticN (a -> f) (AST sym (Full ia) -> fi)
instance [overlap ok] (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi
instance [overlap ok] Syntactic (ASTF sym a)


-- | Construct for decorating symbols or expressions with additional
--   information
module Data.Syntactic.Decoration

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

-- | Map over a decoration
mapDecor :: (sym1 sig -> sym2 sig) -> (info1 (DenResult sig) -> info2 (DenResult sig)) -> ((sym1 :&: info1) sig -> (sym2 :&: info2) sig)

-- | Get the decoration of the top-level node
getDecor :: AST (sym :&: info) sig -> info (DenResult sig)

-- | Update the decoration of the top-level node
updateDecor :: (info a -> info a) -> ASTF (sym :&: info) a -> ASTF (sym :&: info) a

-- | Lift a function that operates on expressions with associated
--   information to operate on a <a>:&amp;:</a> expression. This function
--   is convenient to use together with e.g. <tt>queryNodeSimple</tt> when
--   the domain has the form <tt>(sym <a>:&amp;:</a> info)</tt>.
liftDecor :: (expr s -> info (DenResult s) -> b) -> ((expr :&: info) s -> b)

-- | Strip decorations from an <a>AST</a>
stripDecor :: AST (sym :&: info) sig -> AST sym sig

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

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

-- | Print an decorated syntax tree using ASCII art
drawDecorWith :: StringTree sym => (forall a. info a -> String) -> ASTF (sym :&: info) a -> IO ()
instance StringTree expr => StringTree (expr :&: info)
instance Render expr => Render (expr :&: info)
instance Equality expr => Equality (expr :&: info)
instance Project sub sup => Project sub (sup :&: info)


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


-- | Basics for implementing functional EDSLs
module Data.Syntactic.Functional

-- | Variable name
newtype Name
Name :: Integer -> Name

-- | Generic N-ary syntactic construct
--   
--   <a>Construct</a> gives a quick way to introduce a syntactic construct
--   by giving its name and semantic function.
data Construct a
Construct :: String -> Denotation sig -> Construct sig

-- | Variables and binders
data Binding a
Var :: Name -> Binding (Full a)
Lam :: Name -> Binding (b :-> Full (a -> b))

-- | Get the highest name bound by the first <a>Lam</a> binders at every
--   path from the root. If the term has <i>ordered binders</i> [1],
--   <a>maxLam</a> returns the highest name introduced in the whole term.
--   
--   [1] Ordered binders means that the names of <a>Lam</a> nodes are
--   decreasing along every path from the root.
maxLam :: Binding :<: s => AST s a -> Name

-- | Higher-order interface for variable binding
--   
--   Assumptions:
--   
--   <ul>
--   <li>The body <tt>f</tt> does not inspect its argument.</li>
--   <li>Applying <tt>f</tt> to a term with ordered binders results in a
--   term with <i>ordered binders</i> [1].</li>
--   </ul>
--   
--   [1] Ordered binders means that the names of <a>Lam</a> nodes are
--   decreasing along every path from the root.
--   
--   See "Using Circular Programs for Higher-Order Syntax" (ICFP 2013,
--   <a>http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf</a>).
lam :: Binding :<: s => (ASTF s a -> ASTF s b) -> ASTF s (a -> b)

-- | Convert from a term with De Bruijn indexes to one with explicit names
--   
--   In the argument term, variable <a>Name</a>s are treated as De Bruijn
--   indexes, and lambda <a>Name</a>s are ignored. (Ideally, one should use
--   a different type for De Bruijn terms.)
fromDeBruijn :: Binding :<: sym => ASTF sym a -> ASTF sym a

-- | Typed variables and binders
data BindingT a
VarT :: Name -> BindingT (Full a)
LamT :: Name -> BindingT (b :-> Full (a -> b))

-- | Get the highest name bound by the first <a>LamT</a> binders at every
--   path from the root. If the term has <i>ordered binders</i> [1],
--   <a>maxLamT</a> returns the highest name introduced in the whole term.
--   
--   [1] Ordered binders means that the names of <a>LamT</a> nodes are
--   decreasing along every path from the root.
maxLamT :: BindingT :<: s => AST s a -> Name

-- | Higher-order interface for typed variable binding
--   
--   Assumptions:
--   
--   <ul>
--   <li>The body <tt>f</tt> does not inspect its argument.</li>
--   <li>Applying <tt>f</tt> to a term with ordered binders results in a
--   term with <i>ordered binders</i> [1].</li>
--   </ul>
--   
--   [1] Ordered binders means that the names of <a>LamT</a> nodes are
--   decreasing along every path from the root.
--   
--   See "Using Circular Programs for Higher-Order Syntax" (ICFP 2013,
--   <a>http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf</a>).
lamT :: (BindingT :<: s, Typeable a) => (ASTF s a -> ASTF s b) -> ASTF s (a -> b)

-- | Domains that "might" include variables and binders
class BindingDomain sym
prVar :: BindingDomain sym => sym sig -> Maybe Name
prLam :: BindingDomain sym => sym sig -> Maybe Name

-- | Monadic constructs
--   
--   See "Generic Monadic Constructs for Embedded Languages" (Persson et
--   al., IFL 2011
--   <a>http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf</a>).
data MONAD m sig
Return :: MONAD m (a :-> Full (m a))
Bind :: MONAD m (m a :-> ((a -> m b) :-> Full (m b)))

-- | Reifiable monad
--   
--   See "Generic Monadic Constructs for Embedded Languages" (Persson et
--   al., IFL 2011
--   <a>http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf</a>).
--   
--   It is advised to convert to/from <tt>Mon</tt> using the
--   <a>Syntactic</a> instance provided in the modules
--   <tt>Data.Syntactic.Sugar.Monad</tt> or
--   <tt>Data.Syntactic.Sugar.MonadT</tt>.
newtype Remon sym m a
Remon :: (forall r. (Monad m, MONAD m :<: sym) => Cont (ASTF sym (m r)) a) -> Remon sym m a
unRemon :: Remon sym m a -> forall r. (Monad m, MONAD m :<: sym) => Cont (ASTF sym (m r)) a

-- | One-layer desugaring of monadic actions
desugarMonad :: (MONAD m :<: sym, Monad m) => Remon sym m (ASTF sym a) -> ASTF sym (m a)

-- | Environment used by <a>alphaEq'</a>
type AlphaEnv = [(Name, Name)]
alphaEq' :: (Equality sym, BindingDomain sym) => AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool

-- | Alpha-equivalence
alphaEq :: (Equality sym, BindingDomain sym) => ASTF sym a -> ASTF sym b -> Bool

-- | Semantic function type of the given symbol signature
class Eval s
evalSym :: Eval s => s sig -> Denotation sig

-- | Evaluation
evalDen :: Eval s => AST s sig -> Denotation sig

-- | Monadic denotation; mapping from a symbol signature
--   
--   <pre>
--   a :-&gt; b :-&gt; Full c
--   </pre>
--   
--   to
--   
--   <pre>
--   m a -&gt; m b -&gt; m c
--   </pre>

-- | Lift a <a>Denotation</a> to <a>DenotationM</a>
liftDenotationM :: (Monad m, Signature sig) => proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig

-- | Runtime environment
type RunEnv = [(Name, Dynamic)]

-- | Evaluation
class EvalEnv sym env
compileSym :: EvalEnv sym env => proxy env -> sym sig -> DenotationM (Reader env) sig

-- | Simple implementation of <a>compileSym</a> from a <a>Denotation</a>
compileSymDefault :: (Eval sym, Signature sig) => proxy env -> sym sig -> DenotationM (Reader env) sig

-- | Evaluation of open terms
evalOpen :: EvalEnv sym env => env -> ASTF sym a -> a

-- | Evaluation of closed terms where <a>RunEnv</a> is used as the internal
--   environment
--   
--   (Note that there is no guarantee that the term is actually closed.)
evalClosed :: EvalEnv sym RunEnv => ASTF sym a -> a

-- | Environment extension
class Ext ext orig
unext :: Ext ext orig => ext -> orig
diff :: (Ext ext orig, Num a) => Proxy ext -> Proxy orig -> a

-- | Lookup in an extended environment
lookEnv :: Ext env (a, e) => Proxy e -> Reader env a

-- | Well-scoped variable binding
--   
--   Well-scoped terms are introduced to be able to evaluate without type
--   casting. The implementation is inspired by "Typing Dynamic Typing"
--   (Baars and Swierstra, ICFP 2002,
--   <a>http://doi.acm.org/10.1145/581478.581494</a>) where expressions are
--   represented as (essentially) <tt><a>Reader</a> env a</tt> after
--   "compilation". However, a major difference is that "Typing Dynamic
--   Typing" starts from an untyped term, and thus needs (safe) dynamic
--   type casting during compilation. In contrast, the denotational
--   semantics of <a>BindingWS</a> (the <a>Eval</a> instance) uses no type
--   casting.
data BindingWS a
VarWS :: Proxy e -> BindingWS (Full (Reader env a))
LamWS :: BindingWS (Reader (a, e) b :-> Full (Reader e (a -> b)))

-- | Higher-order interface for well-scoped variable binding
--   
--   Inspired by Conor McBride's <a>I am not a number, I am a classy
--   hack</a> (<a>http://mazzo.li/epilogue/index.html%3Fp=773.html</a>).
lamWS :: BindingWS :<: sym => ((forall env. Ext env (a, e) => ASTF sym (Reader env a)) -> ASTF sym (Reader (a, e) b)) -> ASTF sym (Reader e (a -> b))

-- | Evaluation of open well-scoped terms
evalOpenWS :: Eval s => env -> ASTF s (Reader env a) -> a

-- | Evaluation of closed well-scoped terms
evalClosedWS :: Eval s => ASTF s (Reader () a) -> a

-- | Mapping from a symbol signature
--   
--   <pre>
--   a :-&gt; b :-&gt; Full c
--   </pre>
--   
--   to
--   
--   <pre>
--   Reader env a :-&gt; Reader env b :-&gt; Full (Reader env c)
--   </pre>

-- | Mapping from a symbol signature
--   
--   <pre>
--   Reader e a :-&gt; Reader e b :-&gt; Full (Reader e c)
--   </pre>
--   
--   to
--   
--   <pre>
--   a :-&gt; b :-&gt; Full c
--   </pre>

-- | Wrap a symbol to give it a <a>LiftReader</a> signature
data ReaderSym sym a
ReaderSym :: Proxy env -> sym sig -> ReaderSym sym (LiftReader env sig)

-- | Well-scoped <a>AST</a>
type WS sym env a = ASTF (BindingWS :+: ReaderSym sym) (Reader env a)

-- | Convert the representation of variables and binders from
--   <a>BindingWS</a> to <a>Binding</a>. The latter is easier to analyze,
--   has a <a>Render</a> instance, etc.
fromWS :: WS sym env a -> ASTF (Binding :+: sym) a

-- | Make a smart constructor for well-scoped terms. <a>smartWS</a> has any
--   type of the form:
--   
--   <pre>
--   smartWS :: (sub :&lt;: sup, bsym ~ (BindingWS :+: ReaderSym sup))
--       =&gt; sub (a :-&gt; b :-&gt; ... :-&gt; Full x)
--       -&gt; ASTF bsym (Reader env a) -&gt; ASTF bsym (Reader env b) -&gt; ... -&gt; ASTF bsym (Reader env x)
--   </pre>
smartWS :: (Signature sig, Signature sig', sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup), f ~ SmartFun bsym sig', sig' ~ SmartSig f, bsym ~ SmartSym f, sig' ~ LiftReader env sig, Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig, LowerReader (LiftReader env sig) ~ sig, Reader env a ~ DenResult sig') => sub sig -> f
instance [overlap ok] Eq Name
instance [overlap ok] Ord Name
instance [overlap ok] Num Name
instance [overlap ok] Enum Name
instance [overlap ok] Real Name
instance [overlap ok] Integral Name
instance [overlap ok] Functor (Remon sym m)
instance [overlap ok] Eval sym => Eval (ReaderSym sym)
instance [overlap ok] Eval BindingWS
instance [overlap ok] (Ext env e, ext ~ (a, env)) => Ext ext e
instance [overlap ok] Ext env env
instance [overlap ok] EvalEnv BindingT RunEnv
instance [overlap ok] Monad m => EvalEnv (MONAD m) env
instance [overlap ok] EvalEnv Construct env
instance [overlap ok] EvalEnv sym env => EvalEnv (sym :&: info) env
instance [overlap ok] EvalEnv Empty env
instance [overlap ok] (EvalEnv sym1 env, EvalEnv sym2 env) => EvalEnv (sym1 :+: sym2) env
instance [overlap ok] Monad m => Eval (MONAD m)
instance [overlap ok] Eval Construct
instance [overlap ok] Eval sym => Eval (sym :&: info)
instance [overlap ok] Eval Empty
instance [overlap ok] (Eval s, Eval t) => Eval (s :+: t)
instance [overlap ok] Monad m => Monad (Remon dom m)
instance [overlap ok] Applicative m => Applicative (Remon sym m)
instance [overlap ok] StringTree (MONAD m)
instance [overlap ok] Equality (MONAD m)
instance [overlap ok] Render (MONAD m)
instance [overlap ok] BindingDomain sym
instance [overlap ok] BindingDomain BindingT
instance [overlap ok] BindingDomain Binding
instance [overlap ok] BindingDomain sym => BindingDomain (AST sym)
instance [overlap ok] BindingDomain sym => BindingDomain (sym :&: i)
instance [overlap ok] (BindingDomain sym1, BindingDomain sym2) => BindingDomain (sym1 :+: sym2)
instance [overlap ok] StringTree BindingT
instance [overlap ok] Render BindingT
instance [overlap ok] Equality BindingT
instance [overlap ok] StringTree Binding
instance [overlap ok] Render Binding
instance [overlap ok] Equality Binding
instance [overlap ok] Show Name
instance [overlap ok] StringTree Construct
instance [overlap ok] Equality Construct
instance [overlap ok] Render Construct


-- | <a>Syntactic</a> instance for functions
--   
--   This module is based on having <a>Binding</a> in the domain. For
--   <a>BindingT</a> import module <a>Data.Syntactic.Sugar.BindingT</a>
--   instead
module Data.Syntactic.Sugar.Binding
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, Binding :<: dom) => Syntactic (a -> b)


-- | <a>Syntactic</a> instance for functions
--   
--   This module is based on having <a>BindingT</a> in the domain. For
--   <a>Binding</a> import module <a>Data.Syntactic.Sugar.Binding</a>
--   instead
module Data.Syntactic.Sugar.BindingT
instance (Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, BindingT :<: dom, Typeable (Internal a)) => Syntactic (a -> b)


-- | <a>Syntactic</a> instance for <a>Remon</a> using <a>Binding</a> to
--   handle variable binding
module Data.Syntactic.Sugar.Monad

-- | One-layer sugaring of monadic actions
sugarMonad :: Binding :<: sym => ASTF sym (m a) -> Remon sym m (ASTF sym a)
instance (Syntactic a, Domain a ~ sym, Binding :<: sym, MONAD m :<: sym, Monad m) => Syntactic (Remon sym m a)


-- | <a>Syntactic</a> instance for <a>Remon</a> using <a>BindingT</a> to
--   handle variable binding
module Data.Syntactic.Sugar.MonadT

-- | One-layer sugaring of monadic actions
sugarMonad :: (BindingT :<: sym, Typeable a) => ASTF sym (m a) -> Remon sym m (ASTF sym a)
instance (Syntactic a, Domain a ~ sym, BindingT :<: sym, MONAD m :<: sym, Monad m, Typeable (Internal a)) => Syntactic (Remon sym m a)