%%% !!!!
%%% NOTE: moved this file to ../ariem-thesis/warren/warren.lhs
%%% !!!!
%%% EDIT IT THERE




%format ph = "\rho{}"
%format (sub (x) (y)) = "{" x "}_{" y "}"
%format (ann (x) (y) (z)) = "{" x "}_{" y "}^{" z "}"
%format pc = "\phi{}"
%format pc1
%format ~< = "\preceq{}"
%format >~ = "\succeq{}"
%format tau = "\tau{}"
%format (many (m)) = "\overline{" m "}"
%format q1
%format Phi = "\Phi{}"
%format <+> = "\cup{}"
%format ~> = "\leadsto{}"
%format :-> = "\mapsto{}"
%format :- = "\vdash{}"
%format . = "."
%format \/ = "\cup{}"
%format \+/ = "\uplus{}"
%format emptyset = "\emptyset{}"
%format (semb(x)(y)) = "\llbracket{}{" x "}\rrbracket{}_{" y "}"
%format `bar` = "|"
%format `pre` = "\prec{}"
%format Gamma = "\Gamma{}"
%format `compose` = "\circ{}"
%format initial = "\mathsf{initial}"
%format ^^ = "\;"
%format ^^^ = "\hspace{1em}"
%format Heap = H
%format unit = "\imath{}"
%format ---> = "\longrightarrow{}"
%format Ktx = "\mathcal{K}"
%format vinkje = "\!\!\!{\surd{}}"
%format `subseteq` = "\subseteq{}"
%format atom = "\nu{}"

%format grammar = "\mathbf{grammar}"
%format nonterm = "\mathbf{nonterm}"
%format term = "\mathbf{term}"
%format itf = "\mathbf{itf}"
%format inh = "\mathbf{inh}"
%format syn = "\mathbf{syn}"
%format phase = "\mathbf{phase}"
%format sem = "\mathbf{sem}"
%format child = "\mathbf{child}"
%format order = "\mathbf{order}"
%format attr = "\mathbf{attr}"
%format rule = "\mathbf{rule}"
%format begin = "\mathbf{begin}"
%format end = "\mathbf{end}"

%format d1
%format d2
%format o1
%format o2
%format Heap0
%format Heap1
%format Heap2
%format Heap3
%format Gamma0
%format Gamma1
%format Gamma2
%format f1
%format f2
%format f3
%format f4
%format f5
%format ph0
%format ph1


\section{Introduction}

Compositionality is an important property of attribute grammars.
In fact, AGs are so easily composed that compositions may accidentally
become inconsistent, i.e. have attributes are cyclicly defined.
Knuth proves that an AG is well-defined if and only if the dependency graphs
of productions according to his refined algorithm (Knuth-2) are cycle-free.
When the depedency graphs according to Knuth's original algorithm (Knuth-1) are cycle-free
then the AG is well-defined, but not necessairely the other way around.
These are static properties of AGs that allow us to statically guarantee that
the evaluation of an AG terminates.

Knuth-2 uses a dependency graph per production/child production combination, in contrast
to a single dependency graph per production as Knuth-1 approaches use.
Knuth-2 leads to an approximate number of dependency graphs per production in the order
$(|p|^|b|)$, where |p| is the number of productions of the child nonterminals, and |b| is the
number of children. In practice, e.g. for the let-production of a lambda calculus,
|p| is rather large (|p > 10|), but |b| is typically small (|b <= 2|).
However, we usually define a fine granularity of nonterminals so that
distinct dependency graphs per production/child production combination does not offer an
advantage over a single graph per production.

In our experience, our AGs are either necessarily cyclic, or are cycle-free in both fashions
of the dependency graph as mentioned above. In the first case, on-demand evaluation may still yield
results for attributes, although it is the responsibility of the programmer to ensure this.
In the second case, we know that an evaluation order exists, and can use an eager evaluation
algorithm. An eager evaluation algorithm is likely to exhibit better time and space behavior, and
actually allows us to make minor assumptions about the evaluation order.

Unfortunately, when using the Kastens approach, we often
encounter cycles that are induced by the scheduling as resulting from Kastens' scheduling algorithm.
These induced cycles hamper compositionality as we typically need to add artificial dependencies between attributes
to the AG to control the scheduling.
Therefore, we wish to apply the Kennedy-Warren approach, which does not have this problem.
Unfortunately, it is not immediately clear how schedules according to Kennedy-Warren's algorithm
can be mapped to effecient, well-typed, and pure functions. Also, the Kennedy-Warren approach
may result in a large number execution plans for a production, which we may need to control to
prevent code blowup.

\paragraph{Goal.}
We apply Kennedy-Warren's algorithm to produce execution plans for productions, then define
a mapping that translates these plans to Haskell functions in the form of coroutines.

\paragraph{Extensions.}
We make the notion of a phase explicit. Phases are partitions of the inherited
and synthesized attributes of nonterminals.
For a nonterminal |N|, we define a total order of one or more phases |ph1, ..., (sub ph n)|.
A phase |(sub ph i)|
declaratively represents one or more actual and distinct visits to the coroutine. The amount of visits
per phase, and the attributes scheduled to a visit depends on the context the nonterminal appears in
(courtesy of Kennedy-Warren).

An attribute declaration of
attribute |x| takes zero or more phase constraints |pc1, ..., (sub pc m)| of the
form |x >~ (sub ph j)| or |x ~< (sub ph j)|.
When  |x ~< (sub ph k)| and |y >~ (sub ph l)| for an attribute |x| and |y| with |k < l|, then
|x| is scheduled to an earlier visit than |y|.
In a similar way, we allow rules and the beginning and end of phases on children to be restrained.

Scheduling restrictions are imposed with this mechanism, which can limit the number of possible parent
contexts, and is thus a mechanism to limit a potential code explosion.
In particular, we may manually schedule attributes to fixed phases, and thus obtain a
Kastens-like scheduling.
In addition, the ability to specify the relative order on rules and invocations of phases on children,
allows us to incorporate simple forms of side effect that may be tedious to encode via explicit attribute
threading.

\section{Example of a Multi-visit AG}

The following example is a variation on the typical rep-min example that requires more than one visit
with an eager evaluation strategy. We replace a leaf-child with the minimum value of its sibling.
\begin{code}
grammar Tree                                -- grammar for nonterm |Tree|
  | Leaf  x :: Int                          -- production |Leaf|
  | Bin   l,r : Tree                        -- production |Bin| with two nonterms

attr Tree  ^^^  syn gath :: Int             -- attributes for nonterm |Tree|
                inh min  :: Int
                syn repl :: Tree

sem Tree                                    -- semantics for nonterm |Tree|
  | Leaf  lhs.gath  = loc.x
          lhs.repl  = Leaf lhs.min          -- replacement tree
  | Bin   lhs.gath  = min l.gath r.gath     -- global minimum gathering
          l.min     = r.gath                -- crossover between |r| and |l|
          r.min     = l.gath 
          lhs.repl  = Bin l.repl r.repl     -- replacement tree
\end{code}
In order to get the |min| attribute of |l|, the |gath| attribute of |r| is needed and
vice versa. With eager evaluation, this can be accomplished
by first computing the |gath| attribute as a first
visit, then compute |min| and |repl| in a second visit.

Optionally, we can explicitly specify that |min| and |repl| belong in different visits
by introducing two phases.
\begin{code}
attr Tree                  -- attributes and phases for nonterm |Tree|
  syn repl :: Tree         -- attribute unassociated with a phase
  phase gather             -- phase 1: gathering
    syn gath :: Int        -- attribute tied to gather-phase
  phase distr              -- phase 2: distribution
    syn repl :: Tree       -- attribute tied to distr-phase
\end{code}
Also, we can enforce that for the |Bin|-production, the phases of the right child are performed
before the corresponding phases of the left child.
\begin{code}
sem Tree | Bin
  order  end l.gather  `pre` begin r.gather
  order  end l.distr   `pre` begin r.distr
\end{code}
We define the semantics of these ordering instructions for a desugared subset of this AG language.

\begin{figure}[t]
\begin{code}
g  ::=  grammar N (many (| P (many u)))  -- productions |P| of nonterminal |N| with symbols |u|
u  ::=  nonterm x : N                    -- nonterminal symbol |N| with name |x|
   |    term x :: tau                    -- terminal symbol with name |x| of type |tau|

n  ::=  attr N (many q)                  -- attr decls for nonterminal |N|
q  ::=  a                                -- attr decl
   |    begin ph                         -- begin phase marker
   |    end ph                           -- end phase marker
a ::=   t x :: tau                       -- attribute |x| of type |tau|
t ::=   inh | syn                        -- attribute form

s  ::=  (sub sem Gamma) N | P (many r)   -- semantics of nonterminal |N| and production |P|
r  ::=  child x : N = f((many o))        -- (higher order) child declaration
   |    x : p((many o1)) = f((many o2))  -- evaluation rule named |x| with LHS |p| and RHS |f|
   |    order d1 `pre` d2                -- order declaration

d  ::=  begin c ph                       -- designates begin of phase |ph| of child |c|
   |    end c ph                         -- designates end of phase |ph| of child |c|
   |    child x                          -- designates child |x|
   |    o                                -- designates an attribute occurrence
   |    rule x                           -- designates a rule named x

o  ::=  t c x                            -- occurrence attr |x| of |c|

c  ::=  lhs | loc | x                    -- child designators
\end{code}
\caption{AG core representation.}
\label{warren.fig.agcore}
\end{figure}

\section{Syntax of the Core Language}

Figure~\ref{warren.fig.agcore} shows a representation of AGs after preprocessing.
Thus, the representation we end up with
after static checks, desugaring, item grouping, and copy rule insertion have been performed.
This core representation serves two purposes: it allows us to formally reason with AGs, as
well as specify the derivation of dependency graphs, and the construction of execution plans.
We explain this core representation in the remainder of this section.

The following example is the desugared version of the example of the previous section.
Again, we explain the syntax in the remainder of this section.
\begin{code}
sem'Tree (Leaf x)   = sem'Tree'Leaf x
sem'Tree (Bin l r)  = sem'Tree'Bin (sem'Tree l) (sem'Tree r)

attr Tree  ^^^  syn gath  :: Int
                inh min   :: Int
                syn repl  :: Tree

sem'Tree'Leaf field'x =
  sem { f1 = field'x, f2 = Leaf } Tree | Leaf
    id (syn lhs gath)  = f1
    id (syn lhs repl)  = f2 (inh lhs min)

sem'Tree'Bin field'l field'r =
  sem { f1 = field'l, f2 = field'r, f3=min, f4=Bin } Tree | Bin
    child l : Tree     = f1
    child r : Tree     = f2
  
    id (syn lhs gath)  = f3 (syn l gath) (syn r gath)
    id (inh l min)     = id (syn r gath)
    id (inh r min)     = id (syn l gath)
    id (syn lhs repl)  = f4 (syn l repl) (syn r repl)

ast = sem'Tree'Bin (sem'Tree'Leaf 1) (sem'Tree'Leaf 2)
\end{code}

The additional phase annotations on attributes can be written as:
\begin{code}
attr Tree  ^^^  syn repl    :: Tree    -- unassociated attr
                begin gather           -- begin marker for |gather|
                  inh min   :: Int     -- tied to |gather| phase
                end gather             -- end marker for |gather|
                begin distr            -- begin marker for |distr|
                  syn repl  :: Tree    -- tied to |distr| phase
                end distr              -- end marker for |distr|
\end{code}
The attributes of a nonterminal are specified as a sequence |q1, ..., (sub q n)|, where |sub q i| is either an
inherited or synthesized attribute declaration, or a marker that designates the beginning or end of
a phase. An attribute declared before the first
phase marker is not associated with a particular phase. Otherwise, an attribute is associated with the phase
of the last preceeding marker in the sequence. We assume that there are no phase markers in the sequence
between |begin ph| and |end ph|.

More formally, the phase |Phi ((sub q i))| of |sub q i|
is partially defined as:
\begin{code}
Phi ((sub a i))             = Phi (sub a (i-1))
Phi ((sub ((begin ph)) i))  = ph
Phi ((sub ((end ph)) i))    = ph
\end{code}
For unassociated attributes, the phase of an attribute is |undefined|.
Phases are totally ordered.

We desugared the abstract grammar to terms in the host language, and eliminated the need for the
structure of the grammar in the semantics of a production.
We derive a catamorphism |sem'N| in the host language from the grammar
specification, and treat the semantics as components of the catamorphism's algebra
in the form of semantic functions |sem'N'P|.
%format cata = "\mathsf{cata}"
%format pattern = "\mathsf{pat}"
%format recurse = "\mathsf{rec}"
\begin{code}
semb (grammar N (many (| P (many u)))) (cata)  =  ^^^ many (semb ((many u)) (cata(N,P)))
semb (many u) (cata(N,P))                      =      sem'N (P (many ( semb (u) pattern ))) = sem'N'P (many ( semb (u) recurse ))

semb (nonterm x : N) pattern                   = ^^^  x
semb (term x :: tau) pattern                   =      x

semb (nonterm x : N) recurse                   =      sem'N x
semb (term x :: tau) recurse                   =      x
\end{code}
The core language has a notion of higher-order children. Thus, the information about the
children that is captured by the grammar specification can be encoded as rules.
We desugar each field |u| of some production |P| of nonterminal |M| to a rule |semb u desugar|.
\begin{code}
semb (nonterm x : N) desugar  =  ^^^  child x : N  = id field'x
semb (term x : N) desugar     =       (loc.x)      = id field'x
\end{code}
When the field is a nonterminal, we introduce it explicitly as a child. When the field is
a terminal, we provide the field as local attribute. In this internal representation, all children
are thus explicitly declared via a rule. The notion of conventional children and higher-order
children is unified in this representation.
As a consequence, the semantic functions are target-language terms that take values of terminals
and nonterminals as |field'x| parameter, and consist of an embedded
semantics-block |sub s (N,P)|:
%format declfield = "\mathsf{field}"
\begin{code}
semb (grammar N (many (| P (many u)))) (desugar)  = ^^^  many (semb ((many u)) (desugar(N,P)))
semb (many u) (desugar(N,P))                      =      sem'N'P (many ( semb u (declfield) )) = sub s (N,P)

semb (nonterm x : N) declfield                    =      field'x
semb (term x :: tau) declfield                    =      field'x
\end{code}
With this desugaring-step we factored out the modelling of semantic trees and focus in the semantics
on children, rules and attributes of productions.
In a similar way, we can generate a data type for nonterminal |N| and data constructors for productions |P|.

An evaluation rule consists of an LHS |p((many o1))| and RHS |f((many o2))| such that
|p `compose` f :: ((many ( sub(tau)(o2) ))) -> ((many ( sub(tau)(o1) )))|, where |p| and |f|
are bound in global environment |sub Gamma initial| or in |Gamma|.
Also, evaluation rules have an explicit unique name. Ordering constraints can be imposed on rules via
their name. However, we do not expect that programmers give names to rules. Instead, the names
are mainly used internally to make rules explicitly visible in the operational semantics,
dependency graphs, and execution plans that we define later.
As part of the desugaring process, rules that do not have a name become a fresh name.

The occurrences of attributes in patterns and expressions may refer to inherited or synthesized
attributes. Since a nonterminal may have both an inherited and synthesized attribute with the
name |x|, we make this distinction explicit in the attribute occurrence.

\section{Operational Semantics of the Core Language}

Ultimately, we generate target-language code for the core language term. However, to facilitate reasoning
with terms in the core language, we first define an operational semantics\footnote{
  This operational semantics is also implemented as part of the @ruler-interpreter@:
  \url{https://subversion.cs.uu.nl/repos/project.ruler.systems/ruler-interpreter/}.
} in Figure~\ref{warren.fig.nodeeval}.
The semantics refers to rules in Figure~\ref{warren.fig.readyrules}, which can be interpreted as a dynamic version of
the dependency analysis that we define in the next section.

Since we deal with higher-order AGs, the operational semantics describes both the construction and decoration
of the AST.

\begin{figure}[htbp]
\begin{small}
\begin{mathpar}
  \fbox{|Gamma :- v ---> v|}\\
  
  \inferrule*[right=e.descent]
    { |H(child x) = v| \\
      |Gamma0 :- v ---> v'|
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{child x :-> v'} \/ H)|}
  
  \inferrule*[right=e.down.inh]
    {|H(inh x y) = v| \\
     |H(child x) = (N',P',Gamma2,H')|\\
     |N';P';H' (sub (:-) vinkje) inh lhs y|
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{child x :-> (N',P',Gamma2,{inh lhs y :-> v} \+/ H')} \/ H)|}
  
  \inferrule*[right=e.lift.begin]
    {|H(child x) = (N',P',Gamma2,H')|\\
     |H'(begin lhs ph) = unit|\\
     |N;P;H (sub (:-) vinkje) begin x ph|\\
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{begin x ph :-> unit} \+/ H) |}

  \inferrule*[right=e.lift.end]
    {|H(child x) = (N',P',Gamma2,H')|\\
     |H'(end lhs ph) = unit|\\
     |N;P;H (sub (:-) vinkje) end x ph|\\
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{end x ph :-> unit} \+/ H) |}

  \inferrule*[right=e.lift.syn]
    {|H(child x) = (N',P',Gamma2,H')|\\
     |H'(syn lhs y) = v|\\
     |N;P;H (sub (:-) vinkje) syn x y|\\
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{syn x y :-> v} \+/ H) |}
  
  \inferrule*[right=e.intro.begin]
    { |N;P;H (sub (:-) vinkje) begin lhs ph|\\
      |ph `elem` phases(N)| \\
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{begin lhs ph :-> unit} \+/ H) |}

  \inferrule*[right=e.intro.end]
    { |N;P;H (sub (:-) vinkje) end lhs ph|\\
      |ph `elem` phases(N)|\\
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{end lhs ph :-> unit} \+/ H) |}

  \inferrule*[right=e.intro.child]
    {
      |( child x : N' = f((many o)) ) `elem` rules(N,P)|\\
      |N;P;H (sub (:-) vinkje) child x|\\
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,{child x :-> (Gamma0 Gamma1 f) ((many (H(o))))} \+/ H) |}

  \inferrule*[right=e.intro.rule]
    {
      |( x : p((many o1)) = f((many o2)) ) `elem` rules(N,P)|\\
      |N;P;H (sub (:-) vinkje) rule x|\\
      |sub(H)(attr) = {(many o1) :-> ((Gamma0 Gamma1 p) `compose` (Gamma0 Gamma1 f)) ((many (H(o1))))}|\\
    }
    {|Gamma0 :- (N,P,Gamma1,H) ---> (N,P,Gamma1,(sub H attr) \+/ {rule x} \+/ H) |}
\end{mathpar}
\end{small}
\caption{Small-step evaluation rules for a node.}
\label{warren.fig.nodeeval}
\end{figure}

The first question is how we represent the AST. In essence, a node of a tree contains a reference to the
rules of the node, and contains state that keeps track of the attributes and children of the node that are present
so far. We represent a node as the tuple |(N,P,Gamma,Heap)|, where |N| is the associated nonterminal, |P| is
the associated production, |Gamma| is an environment that contains
bindings for the functions that are mentioned the rules of |P|, and the heap |Heap| contains values for
attributes and nodes that form the children of |P|.

\begin{figure}[htbp]
\begin{small}
\begin{mathpar}
  \fbox{|N;P;H (sub (:-) vinkje) d|}\\
  
  \inferrule*[right=d.expl]
    {|N;P;H (ann (:-) vinkje dep) d| \\
     |(order d' `pre` d) `elem` rules(N,P)|\\
     |d' `elem` dom(H)| \\
    }
    {|N;P;H (sub (:-) vinkje) d|}
  
  \inferrule*[right=d.attr]
    { |c == lhs && t == inh ^^ => ^^ { begin lhs ph ^^ `bar` ^^ ph = phaseOf(t x,N) } `subseteq` dom(H)|
    }
    {|N;P;H (ann (:-) vinkje dep) t c x|}
  
  \inferrule*[right=d.child]
    { |( child x : N' = f((many o)) ) `elem` rules(N,P)|\\\\
       |(many o) `subseteq` dom(H)| \\
    }
    {|N;P;H (ann (:-) vinkje dep) child x|}
  
  \inferrule*[right=d.rule]
    { |( x : p((many o1)) = f((many o2)) ) `elem` rules(N,P)|\\\\
      |(many o2) `subseteq` dom(H)| \\
      |N;P;H (sub (:-) vinkje) (many o1)| \\
    }
    {|N;P;H (ann (:-) vinkje dep) rule x|}
  
  \inferrule*[right=d.begin.lhs]
    { |{ end lhs ph0 ^^ `bar` ^^ ph0 = pred(ph,N) } `subseteq` dom(H)|
    }
    {|N;P;H (ann (:-) vinkje dep) begin lhs ph|}
  
  \inferrule*[right=d.begin.x]
    {}
    {|N;P;H (ann (:-) vinkje dep) begin x ph|}

  \inferrule*[right=d.end.lhs]
    { |(begin lhs ph) `elem` dom(H)| \\\\
      |{t lhs x ^^ `bar` ^^ phaseOf(t x,N) = ph } `subseteq` dom(H)| \\
    }
    {|N;P;H (ann (:-) vinkje dep) end lhs ph|}

  \inferrule*[right=d.end.x]
    {}
    {|N;P;H (ann (:-) vinkje dep) end x ph|}
\end{mathpar}
\end{small}
\caption{Designator dependency rules.}
\label{warren.fig.readyrules}
\end{figure}

More specificially, a heap |H| is a partial map between descriptors |d| and a value |v|.
A descriptor is either an identifier for an attribute, child, or a phase.
\begin{code}
v     ::=  atom | unit | n          -- atomic value |atom|, or unit value |unit|, or node |n|
n     ::=  (N,P,Gamma,Heap)         -- node associated to |N| and |P|, with env |Gamma|, and heap |Heap|
\end{code}
A value of an attribute is either an atomic value |atom| in the domain of the attribute, or a tree in
case of a higher-order attribute.
Furthermore, we track the phases initiated and performed on nodes.

A tree |n| is in normal form when all the nodes of |n| consist of heaps that contain bindings for all the
node's descriptors. A tree in normal form essentially has all its attributes computed.
The small-step relation |Gamma0 :- v ---> v'| describes how we
evaluate a tree |v| one step further to |v'| in a global environment |Gamma0|.
We start with an initial tree and gradually grow the tree by modifying the heaps.
In the initial tree |v0 = (N,P,Gamma,emptyset)|, |N| is the nonterminal of the
root, |P| is the production of the root, and |Gamma| contains bindings for functions as mentioned in the
rules of |P|. In particular, for each child-rule in |P|, there is a binding for a function in |Gamma| that
provides the semantics for that child.
When the AG is well-formed, the resulting tree is in normal form when the rules are applied exhaustively.

We use the following notation in the rules.
The operator |\/| represents the left-biassed union of its two operands heaps, and operator |\+/|
takes the union of two heaps with disjoined keys. The domain |dom(H)| of a heap |H| is the set of
the heap's keys. A heap |H| applied to a designator |d|, written |H(d)|, returns the binding for
|d| in |H|. Similarly, |Gamma0 Gamma1 f| returns the function binding for |f| in the
right-biassed union of |Gamma0| and |Gamma1|.
The |phaseOf| function returns the phase of
an attribute, or |undefined| if the attribute is not constrained to a particular phase.
The |pred| function returns the preceding phase, or |undefined| if there is no such phase.

The idea incorporated in the rules of Figure~\ref{warren.fig.nodeeval} is that we can nondeterministically
select a node that we constructed so far (rule \TirName{e.decent}) and reduce it a bit further. Each node
has its own heap that explicitly tracks which attributes have been computed, which children have been
constructed, and what rules have been applied. A test to check if a rule can be applied then boils down
to verifying that the dependencies of the rule are part of the heap (Figure~\ref{warren.fig.readyrules}).

The lift-rules take the synthesized attributes and phase markers of the children and copy these to the heap
of the parent under the name of that child. Similarly, the \TirName{e.down.inh} copies bindings for the
inherited attribute of a child to the heap of that child, when that child is ready to receive these bindings.
For example, inherited attributes for a child can be computed even before the child is introduced.

The actual computations are performed by the intro-rules. Evaluation of the RHS of a child-rule gives
us the initial tree to use for that child in the heap. Evaluation of an attribute rule results in bindings
for one or more attributes. Note the careful use of disjoined unions that rules out duplicate evaluations
for attributes and rules.

The main dependency rule of Figure~\ref{warren.fig.readyrules} is \TirName{d.expl}, which factors out
the dependency handling regarding explicit order-rules. The remaining rules deal with the implicit
conditions under which we may construct a certain attribute, child or phase marker.
Attributes are not restricted, with one exception: lhs-inherited attributes that are tied to a particular
phase may only be introduced for a node when that node is in that phase.
Children can be introduced if the dependencies of the RHS are part of the heap. Similarly for evaluation
rules, except that we then also need to verify that potential constraints on the attributes of the LHS
imposed by explicit-order rules have been met.
A begin marker for a phase for a node itself can be introduced if it is the first phase, or the previous
phase is finished. And end marker for a phase of a node can be introduced if that phase was started,
and all attributes for that phase have been computed. The markers for children of a node are copied
from the node. Since the responsibility of introducing these markers in the correct order lies with
the evaluation of such a child, we do not impose additional constraints on them in the parent.

\section{Static Dependency Graphs of Nonterminals and Productions}

We construct the dependency graphs according to Knuth-1, which involves
a dependency graph per production (|pdg(N,P)|) and a dependency graph per nonterminal (|ndg(N)|).
We first define the initial graphs, then specify the actual graphs as the fixpoints of the
functions:
%format initial = "\mathsf{init}"
\begin{code}
pdg(N,P)  = sub(pdg(N,P))(initial)  <+> { instantiate (ndg( (sub N c) ))  | c `elem` children P }
ndg(N)    = sub(ndg(N))(initial)    <+> { abstract (pdg(N,P))             | P `elem` prods N }
\end{code}
The function |instantiate| translates the edges between declarations of |sub N c| in the NDG as edges
between the attributes of child |c| in the PDG. Similarly, when there is a path between two attributes of
|lhs| in the PDg, then |absract| translates these as edges between the same attributes in |N|'s NDG.

\paragraph{Initial production dependency graph.}

%format vert1 = "\mathsf{vert}"
Per production |C| of nonterminal |N|, we construct a production dependency graph |pdg(N,P)|. The vertices
|semb (sem N `bar` C (many r)) (vert1)| of |pdg(N,P)| consist of designators |d|.
\begin{code}
semb (sem N | P (many r)) (vert1)  = {child lhs} <+> semb (sub (many q) N) (vert1(lhs)) <+> semb (many r) (vert1)

semb (inh y :: tau) (vert1(x))     = {inh x y}
semb (syn y :: tau) (vert1(x))     = {syn x y}
semb (begin ph) (vert1(x))         = {begin x ph}
semb (end ph) (vert1(x))           = {end x ph}

semb (child x : N = e) vert1       = {child x} <+> semb (sub (many q) N) (vert1(x))
semb (x : p = e) vert1             = {rule x}
semb (order d1 `pre` d2) vert1     = emptyset
\end{code}
%format edge1 = "\mathsf{edge}"
%format pre1  = "\mathsf{pre}"
%format suc1  = "\mathsf{succ}"
The directed edges |semb (sem N `bar` C (many r)) (edge1)| of |pdg(N,P)| relate designators.
When there is an edge from |d1| to |d2|, then |d2| must be scheduled before |d1|.
\begin{code}
semb (sem (sub N Gamma) `bar` P (many r)) (edge1)  = semb (many r) (edge1)

semb (child x : N = f((many o))) edge1             = semb ((many o)) (pre1(child x))
semb (x : p((many o2)) = f((many o1))) edge1       = semb ((many o1)) (pre1(rule x)) <+> semb ((many o2)) (suc1(rule x))
semb (order d1 `pre` d2)                           = {d2 -> d1}

semb (o) (pre1(d))                                 = {d -> o}
semb (o) (suc1(d))                                 = {o -> d}
\end{code}
This graph lacks the dependencies imposed by the semantics of each child. We obtain the
actual production dependency graph by augmenting it with the edges taken from the
nonterminal dependency graphs of the children.

\paragraph{Initial nonterminal dependency graph.}
The vertices of the nondeterminal dependency graph |ndg(N)| are the
declarations |q| of |N|.
\begin{code}
semb (attr N (many q)) (vert1) = semb ((many q)) (vert1)
semb (q) (vert1) = {q}
\end{code}
The initial edges are derived from the order in the sequence. Attributes that are
declared inside a particular phase are constrained between the begin and end marker
of that phase.
\begin{code}
semb (attr N (many q)) (edge1)  = semb ((many q)) (edge1(N))
semb (a) (edge1(N))             = {a -> begin Phi(a), end Phi(a) -> a | Phi(a) /= undefined}
semb (begin ph) (edge1(N))      = {begin ph -> end (pred (ph,N)) | pred (ph,N) /= undefined}
semb (end ph) (edge1(N))        = {end ph -> begin ph}
\end{code}
The actual edges are obtained by taking the union over.

Proofs. Sound with respect to operational semantics. Complete when all attributes are associated with a
singleton phase.

\section{Scheduling}

Algorithm.
Execution plan.


\section{Translation of Execution Plans}

Translation to coroutines.