%format <|> = "<\!\!|\!\!>"
%format <#> = "<\!\!|\!\!>"
%format <*> = "<\!\!\!*\!\!\!>"
%format <$> = "<\!\!\$\!\!>"
%format <=> = "\Longleftrightarrow"
%format . = "."

%format ~> = "\leadsto"
%format << = "\llbracket"
%format >> = "\rrbracket"
%format (semb (z)) = << z >>

%format (many (i)) = "\overline{" i "}"

%format attr       = "\mathbf{attr}"
%format data       = "\mathbf{data}"
%format sem        = "\mathbf{sem}"
%format inh        = "\mathbf{inh}"
%format syn        = "\mathbf{syn}"
%format con        = "\mathbf{con}"
%format clause     = "\mathbf{clause}"
%format default    = "\mathbf{default}"
%format itf        = "\mathbf{itf}"
%format visit      = "\mathbf{visit}"
%format internal   = "\mathbf{internal}"
%format match      = "\mathbf{match}"
%format child      = "\mathbf{child}"
%format invoke     = "\mathbf{invoke}"
%format datasem    = "\mathbf{datasem}"
%format tail       = "\mathbf{tail}"
%format prod       = "\mathbf{prod}"
%format resume     = "\mathbf{resume}"
%format assert     = "\mathbf{assert}"
%format grammar    = "\mathbf{grammar}"
%format as         = "\mathbf{as}"

% AG keywords occurring in Haskell
%format hinh = "inh"
%format hsyn = "syn"
%format happ x y = x "(" y ")"

%format ruler = "{\mbox{\scshape ruler}}"

  The Universiteit Utrecht Parser Combinators are an embedded domain-specific language in Haskell
  for 1-S-Attributed Grammars (non left-recursive, context-free and monadic).
  The operational semantics of such a grammar is a fast, deterministic, error-correcting
  parser that produces its result in an online fashion. Due to the consise and flexible
  interface, and its efficient implementation, it is useful for both simple and complex
  parsing tasks.

  According to Swierstra (cite), the implementation of this library is conceptually based
  on Attribute Grammars (AGs), and manually translated to Haskell functions. In this paper, we
  formally express the library as an AG (using various AG extensions), and consequently
  obtain the translation automatically.
  The idea is that the parser combinators form a tree, and we show that parsing can be seen
  as a decoration of this tree with the input as attribute with AGs.

  The parser combinators offer a BNF-syntax (using Haskell's |Applicative| and |Alternative|
  interface), such that each combinator-expression
  represents an (anonymous) nonterminal. With mutual-recursive bindings, names can
  be given to such nonterminals.
  The grammar is the lambda graph (cite) represented by these definitions.
  
  This graph is analyzed to compute several properties of this
  graph, in the form of attributes for each nonterminal.
  For example, these attributes consists of a parser and information about nonterminals.
  In the latter case, the firsts-set of a nonterminal, or whether the nonterminal may expand
  to the empty string, for example.
  These attributes are mutually dependent: to compute the firsts set, information about
  emptyness is needed. Also, the parsers rely on these attributes.
  The graph may be cyclic, and the attributes are hence cyclicly defined.
  Despite that, when the grammar is not left-recursive, lazy evaluation of these definitions
  results in values for the attributes.

  Implementing these analyses, unfortunately, is a tedious job. To retain sharing, these
  analyses must be implemented as one monolothic traversal over the graph.
  We tend to see these attributes as
  separate aspects of the grammar that we idealy describe separately.
  However, we are forced to scatter this code all over the program.
  Consequently, the implementation is difficult to extend and maintain.
  
  Furthermore, parsing itself is search procedure over the tree consisting of the
  union of all paths of this graph, directed by the input.
  Productions in the grammar correspond to alternative paths. A breadth-first search
  technique allows dead alternatives to be pruned from the tree. In a purely functional
  language, however, breadth-first search complicates the implementation (cite).

  Attribute grammars offer us the separate and isolated description of attributes
  of nodes, and overcome the engeneering problem as mentioned above.
  However, AGs operate on a tree, not on a graph.
  We can represent the graph as an (infinite) tree (Section~\ref{sect.graphastree}).
  The traversal over the graph that computes the attributes corresponds to a finite
  traversal over this tree. 
  In this paper, we show how to encode this traversal with a purely-functional,
  breadth-first demand-driven, multi-visit, ordered Attribute Grammar.
  We encode two visits to the graph: the first visit as a shallow depth-first traversal to
  compute attributes of nonterminals, and as second visit a deep breadth-first traversal to
  represent the actual parsing process.
  With a breadth-first AG, we eliminate most of the implementation complexity related to
  breadth-first search.
  
  The description of parsers with AGs poses several challenges that we solve with
  various AG techniques.
  (todo: formulate this in a nicer way)
  Retain sharing or partial evaluation: we partition the evaluation of a node in a visit
  with only synthesized-attributes such that we retain sharing, and in a subsequent visits
  that take inherited attributes and are not shared.
  The tree and attributes have complex types: we use value-attributes and type-attributes.
  The tree may be infinite: we use demand-driven visits to nodes in the tree.
  
  Although this paper focusses on parser combinators, it actually shows an example of
  flexible breath-first search on a proof tree with an attribute grammar.

\section{Introduction to Attribute Grammars}
\label{sect.attributegrammars}

  In this paper, we build on previous work on |ruler|, a domain-specific language for
  AGs, with many extensions. We extend this previous work with breadth-first
  evaluation in a later section. In this section, we shortly introduce the notation.
  See (cite) for an explanation of the core language, (cite) for several notational
  extensions that make the use of AGs profitable, and (cite) explaining types as attributes.
  
  In this paper, we describe the semantics of grammars (in the form of a parser) with an
  attribute grammar. The former is the language we are processing, the latter is the language
  in which the processor is written. It is important to keep these two formalisms apart,
  because they share the same terminology.
  
  An attribute grammar is an extension of a context-free grammar, where nonterminals are annotated
  with attributes, and each production defines relations between attributes via semantic rules.
  The semantic rules are functions between attributes.
  A tree node |C|, with |data N = C (many x) (many Y)|, matches the grammar, if there is
  a production |happ p C : happ n N -> (many (happ t x)) (many (happ n Y))|.
  Given such a tree, attribute evaluation is the process of decorating each node with attributes,
  by applying the semantic rules. There are two types of attributes: inherited attributes are
  defined by the parent node, whereas synthesized attributes are defined by the node itself.
  More precisely, an attribute grammar is compiled to an algebra (indexed by N), consisting
  of smart constructor |happ c C| for each |C|, such that |happ c C :: (many x) -> (many (happ T Y)) -> happ T N|,
  where |happ T N| represents a decorated tree.
  The type |happ T N|, we call the interface of |happ n N|.
  The smart constructor gets decorated trees for the children as parameter, and uses the rules to produce
  values for their inherited attributes, as well as its own synthesized attributes. It may use the values of
  inherited attributes of itself, as well as the synthesized attributes of the children.
  
  The representation of a decorated tree depends on the implementation of the attribute grammar evaluator.
  A possibly representation for a decorated tree is a function with the type |happ T N = happ I N -> happ S N| that takes
  values for the inherited attributes |happ I N| of |happ n N| as parameter and produces a tuple of values for the synthesized
  attributes |happ S N|.
  The body of the smart constructor is merely a multually recursive let-block, with bindings for attributes for each rule, and
  function calls to the children. These values are well-defined if the attributes are not cyclicly defined.
  
  With |ruler|, we use a more complicated representation. Instead of producing all synthesized attributes in a single
  function call, we represent the decorated tree as a coroutine that is invoked multiple times. Each invocation, it takes
  values for some inherited attributes and produces values for some of the synthesized attributes.
  Each invocation is called a visit. The notion of these visits play an important role in the remainder of this paper.
  
  A |ruler| description consists of Haskell extended with attribute grammar code. 
  
  \begin{code}
  itf Parser
    inh a ::: *
    visit analyze
      syn containsAlt  :: Bool
  \end{code}

  \begin{code}
  itf Parser_Pure
    inh a ::: *
    visit construct
      inh f :: hinh.a
    tail t : Parser
      t.a = hinh.a
  
  itf Parser_Seq
    inh a, b ::: *
    visit construct
      inh p, q : Parser
      p.a = hinh.a -> hinh.b
      q.a = hinh.a
    tail t : Parser
      t.a = hinh.b
  
  itf Parser_Alt
    inh a ::: *
    visit construct
      inh p, q : Parser
      p.a = hinh.a
      q.a = hinh.a
    tail t : Parser
      t.a = hinh.a
  \end{code}
  
  \begin{code}
  instance Applicative Parser where
    pure   = prod prodPure  : Parser_Pure
    (<*>)  = prod prodSeq   : Parser_Seq

  instance Alternative Parser where
    (<|>)  = prod prodAlt : Parser_Alt
  \end{code}

  \begin{code}
  sem prodPure   lhs.containsAlt  = False
  sem prodSeq    lhs.containsAlt  = p.containsAlt || q.containsAlt
  sem prodAlt    lhs.containsAlt  = True
  \end{code}


\section{Sketch}
\label{sect.graphastree}

  In this section, we sketch how to encode a grammar as a tree, and use an attribute grammar
  to analyze this tree, as well as perform the actual parsing. In subsequent sections, we
  make the individual steps precise.
  
  \subsection{Grammar Graph}
  
  With parser combinators, a grammar is encoded. This grammar is represented as
  a graph.
  As an example, consider the following parser |mana|, which parses a
  sequence of |a|'s using some parser |pA|:
  \begin{code}
  mana   =       const [] <$> pEof
            <|>  (:) <$> pA <*> mana
  \end{code}
  In the above code, |pEof| matches the end of the input, and |pA| matches
  a single |a| token. As semantic values, these matched |a| tokens are
  collected in a list. In this section, the semantic value of a parser is
  irrelevant. Hence, for simplicity, we omit these:
  \begin{code}
  mana   =       pEof
            <|>  pA <*> mana
  \end{code}
  
  The above parser is an encoding of a grammar.
  Named nonterminals of this grammar, such as |mana|, are encoded as recursive
  let-bound values, with a definition that
  consists of a combinator-expression that may refer to such let-bound values.
  A grammar described with these combinators forms a directed, cylic graph without
  direct cycles.
  Figure~\ref{fig.grammartree} shows the grammar graph denoted by the above parser.
  Each node represents a nonterminal, either in the form of a combinator or an
  explicitly named nonterminal. 
  The edges represent a dependency of a nonterminal upon the combinators that form its definition,
  from a combinator to its combinator-subexpressions, and from a combinator to the
  nonterminal it refers to.
  Recursion in the grammar, encoded as conventional recursion in Haskell, is thus
  represented as a cycle in this graph.
  
  \subsection{Grammar Tree}
  
  To optimize the parsing process later, we analyze the graph, and compute a number
  of attributes for each node. These attributes represent static properties of the
  grammar.
  For example, to determine if a node represents a parser
  that accepts the empty string, or the set of symbols that this parser expects as
  first symbol. The small blocks in Figure~ref{fig.grammartree}
  to the right of a node are a visualisation of these attributes.
  The value of such an attribute is defined as a function of the values of the attributes
  of the successors of a node. This value is computed by visiting the successors of the
  node to compute their attributes, and then applying the function on these.
  Such an attribute is well-defined if it does not depend indirectly on itself.
  For example, in Figure~\ref{fig.grammartree}, the computation for the attributes
  of |mana| must not require a visit to itself (the dotted node).

  An nonterminal can be empty when in case of |l <#> r|, at least
  one of |l| and |r| can be empty, and in case of |l <*> r| when |l| can be empty.
  The black arrows between the attributes in the figure illustrate this.
  Similarly, the first set of a nonterminal in case of |l <#> r| is the union of
  the first sets of |l| and |r|, and in case of |l <*> r| is that of |l|, plus
  that of |r| when |l| can be empty. Note that the emptyness-attribute is needed
  in order to compute the firsts set.
  
  \begin{figure}[htp]
    \centering
    \subfigure[Grammar graph and tree.] {
      \begin{tikzpicture}
        [ nd/.style={circle, minimum size=10.3mm, thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\scriptsize}
        , arr/.style={->, black, thick}
        , virtual/.style={dotted}
        , s1/.style={rectangle, minimum size=2mm, draw=black, top color=black!50, bottom color=black!20,font=\scriptsize,xshift=-3mm,yshift=-3mm}
        , s2/.style={rectangle, minimum size=2mm, draw=black, top color=black!50, bottom color=black!20,font=\scriptsize,xshift=0.3mm,yshift=-3mm}
        ]
    
      \node[nd] (many1) {|mana|}
        [sibling distance=30mm,level distance=20mm]
        child[arr] {
          node[nd] (or) {|<#>|}
            child[arr] {
              node[nd] (empty) {|pEof|}
            }
            child[arr] {
              node[nd] (seq) {|<*>|}
                child[arr] {
                  node[nd] (pa) {|pA|}
                }
                child[arr] {
                  node[nd, virtual] (many2) {|mana|}
                }
            }
        };
    
        \draw[arr, virtual] (many2) [out=90,in=0] to (many1);
    
        \foreach \x in {many1, or, empty, seq, pa} {
          \node[s1, right of=\x] (s1\x) {};
          \node[s2, right of=\x] (s2\x) {};
        }
        
        \draw[->, very thick] (s1empty) [out=90,in=-90] to (s1or);
        \draw[->, very thick] (s1seq) [out=90,in=-90] to (s1or);
        \draw[->, very thick] (s1pa) to (s1seq);
      \end{tikzpicture}
      \label{fig.grammartree}
    }
    \subfigure[Parse tree.] {
      \begin{tikzpicture}
        [ nd/.style={circle, minimum size=10.3mm, thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\scriptsize}
        , arr/.style={->, black, thick}
        , virtual/.style={dotted}
        , s1/.style={rectangle, minimum size=2mm, draw=black, top color=black!50, bottom color=black!20,font=\scriptsize,xshift=-3mm,yshift=-3mm}
        , s2/.style={rectangle, minimum size=2mm, draw=black, top color=black!50, bottom color=black!20,font=\scriptsize,xshift=0.3mm,yshift=-3mm}
        , s3/.style={rectangle, minimum size=2mm, draw=black, top color=black!50, bottom color=black!20,font=\scriptsize,xshift=4.3mm,yshift=-3mm}
        , i1/.style={rectangle, minimum size=2mm, draw=black, top color=black!50, bottom color=black!20,font=\scriptsize,xshift=2.3mm,yshift=-3mm}
        , err/.style={red!100!blue!80!green!80}
        , ann/.style={font=\scriptsize, xshift=2.3mm, yshift=-6mm}
        , ann2/.style={font=\scriptsize, xshift=4.3mm, yshift=-6mm}
        ]

      \node[nd] (many1) {|mana|}
        [sibling distance=30mm,level distance=19mm]
        child[arr] {
          node[nd] (or1) {|<#>|}
            child[arr, virtual, err] {
              node[nd, virtual] (empty1) {|pEof|}
            }
            child[arr] {
              node[nd] (seq1) {|<*>|}
                child[arr] {
                  node[nd] (pa1) {|pA|}
                }
                child[arr] {
                  node[nd] (many2) {|mana|}
                    child[arr] {
                      node[nd] (or2) {|<#>|}
                        child[arr] {
                          node[nd] (empty2) {|pEof|}
                        }
                        child[arr, virtual, err] {
                          node[nd, virtual] (seq2) {|<*>|}
                        }
                    }
                }
            }
        };
        
        %%% \draw[arr, virtual] (seq2) [out=90,in=0] to (seq1);
    
        \foreach \x in {many1, or1, seq1, pa1, many2, or2, empty2} {
          \node[s1, right of=\x] (s1\x) {};
          \node[s2, right of=\x] (s2\x) {};
          \node[s3, right of=\x] (s3\x) {};
          \node[i1, left of=\x]  (i1\x) {};
        }
        
        \foreach \x in {empty1,seq2} {
          \node[i1, left of=\x] (i1\x) {};
        }
        
        \node[ann,left of=many1]{|"a"|};
        \node[ann,left of=pa1]{|"a"|};
        \node[ann2,right of=pa1]{|""|};
        \node[ann,left of=many2]{|""|};
        
        \draw[->, very thick] (s3pa1) [out=90,in=90] to (i1many2);
        \draw[->, very thick] (i1or1) [out=-90,in=90] to (i1empty1);
        \draw[->, very thick] (i1or1) [out=-90,in=90] to (i1seq1);
        \draw[->, very thick] (s3seq1) to (s3or1);
        \draw[->, very thick] (s3empty2) to (s3or2);
      \end{tikzpicture}
      \label{fig.parsetree}
    }
  \caption{Tree representations of the grammar graph.}
  \label{fig.graphtrees}
  \end{figure}
  
  A complication with the implementation of these analyses is that
  the cycles in the graph cannot be observed, because the nodes in the graph have no
  identity (in Haskell). If nodes had an identity, a node cannot simply be replaced
  by its combinator-body, which violates referential transparency.
  When the grammar is not left recursive, however, a cyclic path through this graph
  always contains a terminal symbol on each cycle. Analyses that never look beyond
  this symbol can thus produce a result wihtout getting trapped on such a cycle.
  Hence, attributes of interest such as emptyness and the first-set can be computed.

  If we ignore all the back edges in the grammar graph (the dotted edge in
  Figure~\ref{fig.grammartree}) we get a grammar tree. The attributes of the nodes
  of this tree, we can describe with an attribute grammar that visits the nodes
  on-demand.
  
  \subsection{Parse Tree}
  \label{sect.parsetree}
  
  There is another interpretation of the graph as a tree, constructed by
  expanding a nonterminal by its definition, repeatedly.
  Due to referential transparency, there is no distinction between this tree
  and the graph.
  Alternatively formulated, given a certain start node (corresponding to the
  start symbol of the grammar), we can see the graph as a (potentially infinite)
  tree that is formed by merging all paths (including non-simple paths) that
  start at this node.

  Parsing corresponds to a finite exploration of the above tree, directed by the
  input. Assume for now that we decorate the nodes with two additional attributes:
  an inherited attribute (to the left of a node) that contains the input, and
  a synthesized attribute (to the right of a node) that contains the remaining
  input if parsing succeeded for that node.
  Figure~\ref{fig.parsetree} demonstrates this exploration for the input
  |"a"|.

  For a |<#>|-node, the input is passed to both children. The remaining input is
  taken from the child that successfully parses. For this approach to work, we
  need to ensure that the tree has a certain shape, which we discuss in Section~\ref{sect.rewritegrammar}.
  For a |<*>|-node, the input remaining from the left subtree is fed as input
  to the right subtree.
  The fat arrows illustrate in the figure. The children for which parsing
  fails are marked with a dotted border in the figure.
  Exploration of this tree is finite if the input schrinks for each repeated
  occurrence of a graph-node in this tree. This is the case when the grammar
  is not left-recursive.

  With the attribute that contains the firsts set, the parsing process can be
  optimized. If the nonterminal does not accept the empty string, we may
  exclude parsing of those alternatives that do not have the next token in
  their firsts set.

  Given a recursive occurrence of the node of the graph in the tree, if its
  synthesized attributes do not depend on its inherited attributes,
  these attributes have the same value for each occurrence of the
  node. We describe the parser combinators with a multi-visit AG. With a multi-visit
  AG, the synthesized attributes are partitioned, and computed one partition at a time.
  
  In the first visit, we only compute synthesized attributes related to the analysis. The
  values of the synthesized attributes are a function of the inherited
  attributes. By absence of inherited attributes, as is the case with the analysis,
  the synthesized attributes are thus the same for each recursive occurrence.
  Via Haskell's sharing, we get the the representation as in
  Figure~\ref{fig.grammartree}.
  
  In the second visit, we add
  inherited attributes (e.g. to represent the input), and some
  additional synthesized attributes. These attributes are fresh
  for each recursive occurrence.
  This gives us the representation of Figure~\ref{fig.parsetree}.
  However, the attributes of the previous visit
  are still shared for each occurrence (and thus only computed once).
  Sharing combined with multiple visits is
  thus important to ensure that the analysis is only done once.
  
  \subsection{Tree Transformation}
  \label{sect.rewritegrammar}
  
  The parsing algorithm as roughly sketched in Section~\ref{sect.parsetree}
  may not work if the tree has an undesirable shape.
  When there is an alternative-combinator to the left of a
  sequential-combinator, for example |(p <#> q) <*> r|, it may only be possible to
  choose between |p| or |q| after parsing with |r|. This
  situation arises when |p| and |q| consume different amounts of input and both
  succeed. To choose between |p <#> q|, we cannot consider only the
  outcome of parsing |p| and |q|, unless we transform the grammar such that the
  remaining parsing steps are pushed inside the choice, as is allowed by the
  distributivity of |<#>| over |<*>|.
  
  The following transformation rules lift the alternative-combinator to
  top-level. For simplicity, we express the |<$>|, and |<*>| combinator
  as the monadic combinators (dedicated rules for these combinators are
  more efficient). The |rewrite|-rules represent simplification steps,
  and the |rewrite'| rules the lifting steps. In the latter case,
  a sequence of binds is made right-skewed to ensure sharing of |p|
  for alternatives in |f|. After these preparations, we lift an
  |<#>| combinator by pushing |r| inwards (using distributivity).
  
%format rewrite (x) = << x >>
%format rewrite' (x) = << x >> "^\circ"
  \begin{code}
  rewrite (f <$> p)  = rewrite (return f <*> p)
  rewrite (p <*> q)  = rewrite (p >>= (\f . q >>= (return . f)))
  rewrite (p <|> q)  = rewrite p <|> rewrite q
  rewrite (p >>= r)  = rewrite' (rewrite p >>= r)
  rewrite p = p  -- otherwise
  \end{code}

  \begin{code}
  rewrite' ((p >>= f) >>= r)   = rewrite (p >>= (\x . (f x) >>= r))
  rewrite' ((p <|> q)  >>= r)  = rewrite ((p >>= r) <|> (q >>= r))
  rewrite' (p >>= r)           = p >>= (\x . rewrite (r x))  -- otherwise
  \end{code}
  
  As postcondition, to the left of a |>>=|, there is no occurrence of |<#>|.
  Rewrite steps are applied on the left spine until an atomic combinator is
  encountered, or an |<#>|-combinator. In the latter case, this combinator
  is lifted up. Due to lazy evaluation, a rewrite of the children of an |<#>|
  only continues if the respective parser is needed. For a
  recursive grammar, we always encounter an |<#>|-combinator (otherwise
  the grammar is infinite).
  
  In Figure~\ref{fig.transformtree}, we express the above rewrite
  procedure in terms of the combinators directly to retain sharing,
  as we explain below.
  The combinators (of the type |Grammar|) are defined in terms of more basic combinators
  (of the type |TransformedGrammar|). The grammar described by the latter combinators
  has the desired shape.

  \begin{figure}[htp]
  \begin{code}
  newtype Grammar a = G (Reify a, TransformedGrammar a)

  data Reify a where
    Node_Alt    :: Grammar a -> Grammar a -> Reify a
    Node_Bind   :: Grammar b -> (b -> Grammar a) -> Reify a
    Node_Other  :: Grammar a -> Reify a

  n2g :: Reify a -> Grammar a
  n2g (Node_Alt l r)   = l <|> r
  n2g (Node_Bind l r)  = l >>= r
  n2g (Node_Other g)   = g

  finalG :: Grammar a -> TransformedGrammar a
  finalG (G (_, g)) = g

  instance Functor Grammar where
    f <$> p  = return f <*> p

  instance Applicative Grammar where
    pure x   = return x
    p <*> q  = p >>= (\f -> q >>= (return . f))

  instance Alternative Grammar where
    empty                    = G (Node_Other empty, sem_Empty)
    (G (a,b)) <|> (G (c,d))  = G (Node_Alt (n2g a) (n2g c), b <|> d)

  instance Monad Grammar where
    return x            = G (Node_Other (return x), return x)
    l@(G (n,l')) >>= f  = case n of
      Node_Other _   -> G (Node_Bind l f, l' >>= finalG . f)
      Node_Alt p q   -> (p >>= f) <|> (q >>= f)
      Node_Bind p g  -> G  ( Node_Bind p (\x -> (g x) >>= f)
                           , finalG p >>= (\x -> finalG (g x) >>= finalG . f))
  \end{code}
  \caption{Transform the Grammar Tree.}
  \label{fig.transformtree}
  \end{figure}
  
  We represent the former grammar as a tuple of a value that describes
  the node itself (of the type |Reify a|), and the transformed value for
  this node. This |Reify|-value also witnesses to what extend rewriting is
  completed for a node. In that case, we may take the transformed value.
  
  After the above restructuring of the tree, the tree described by the
  |TransformedGrammar| combinators has the appropriate structure, and
  is suitable for a description with AGs.

\section{Higher-Order Ordered Attribute Grammar}
  
  \begin{figure}[htb]
  \begin{code}
    e  ::=  H [ many b ]                                  -- embedded |rulercore| blocks |b| in |H|
    b  ::=  i | s | o | g                                 -- |rulercore| blocks

    i  ::=  itf I (many a) visit (many a)                 -- interface decl
    a  ::=  syn x z                                       -- syn attr decl
       |    inh x z                                       -- inh attr decl
       |    p = e                                         -- attr def (interface level)
    z  ::=  ::: e                                         -- type of a type attribute
       |    :: e                                          -- type of a value attribute
       |    : x                                           -- type of a child attribute
       
    g  ::=  grammar I (many q)                            -- grammar declaration
    q  ::=  prod x : I                                    -- production declaration

    s  ::=  sem : I t                                     -- semantics expr, defines nonterm |x|
    t  ::=  (many r) t                                    -- execution of rules
       |    invoke (many k) as k resume t                 -- construct and invoke children
       |    (many c)                                      -- clause selection
       |    ()                                            -- terminator

    c  ::=  clause t                                      -- clause definition

    k  ::=  child x : I = e                               -- child definition
    r  ::=  assert  p = e                                 -- assert-rule, evaluates |e|, bind to pattern |p|
       |    match   p = e                                 -- match-rule, backtracking variant

    o  ::=  c.x                                           -- attribute reference in embedded code
    
    p  ::=  c.x                                           -- attribute reference in pattern
       |    C (many p)                                    -- constructor match
    
    x, I                                                  -- identifiers
  \end{code}
  \caption{Syntax of |rulercore|}
  \label{fig.syntax.rulercore}
  \end{figure}
  
  Steps:
  Generate all intermediate representations for a rulercore program.
  Generate eval funciton.
  Generate step function.
  
  Closure data type generation for each sem
  \begin{code}
  kkk
  \end{code}

%if False
  \subsection{Tree Rewriting}
  
  Attribute evaluation can be seen as a rewriting process. A node
  decorated with inherited attributes is rewritten to its synthesized
  attributes.
  
  The parse-tree representation as shown above is a tree that keeps
  growing during the parse process.
  There will be many |<#>| and |<*>| nodes in the tree that after
  some point in the parsing process become redundant, because
  their attributes are fully defined by one of the children.
  Referential transparency allows us to replace a node in the graph with
  a node that produces equivalent values for the synthesized attributes.
  Hence, we eliminate redundant nodes via tree rewriting to
  lower the memory usage.
  
  There are a number of general equivalence-laws for the |<*>| and
  |<#>|-nodes.
  We rewrite the tree after we observe that a child succeeds
  or fails to parse. For a node |l <#> r|, we rewrite the node to
  |l| or |r| when their sibling fails to parse.
  We replace a node |l <*> r| with |r| substituted with some
  results of |l|, as soon as |l| succeeded to parse.
  
  The traversal strategy for attribute evaluation
  influences the effectiveness of rewriting. 
  With a depth-first strategy, a node may only be rewritten after visiting the
  children fully. This means, for example, that all |<*>|-nodes (and their
  attributes) of the parse tree are only rewritten until the input is fully
  parsed.
  Since their children represent the parsed tokens of the input,
  it effectively means that the entire input resides in memory until
  the end of parsing.
  In contrast, when the grammar is LL(1), for example, only one token is
  present in memory at a time.

  With a breath-first strategy, however, nodes can already rewritten
  when children fail to parse, or are guarenteed to succeed.
  This is the strategy of preference. We obtain this strategy via
  demand-driven visits.
  
  In a multi-visit AG, we can see each visit as a rewrite of the node.
  We rewrite a node to an intermediate node that upon evaluation
  (perhaps leading to further rewrites) leads to the
  values for the desired synthesized attributes.
  The node we rewrite to, is a synthesized attribute of the previous
  visit.
  Formally, a node in an AG-tree is a function |f|,
  such that |(many s) = f (many i)|, where |many s| are the node's synthesized
  attributes and |many i| the inherited attributes. Rewriting entails the
  decomposition of |f| into a function |g| and |h|, such that
  |(many s) = h (many i) (g (many i))|.
  In practice, |g| and |h| may not need all of |many i|, and |g| may already
  result in some of |many s|.
  
  \subsection{Online results}
  
  The above tree representations are not suitable to produce online results.
  For a |<*>|-node: replace node with lhs partially parameterized with rhs.
  A.k.a. beta reduction.
%endif