%format rulerfront = "{\mbox{\scshape ruler-front}}" %format rulercore = "{\mbox{\scshape ruler-core}}" %format rulerback = "{\mbox{\scshape ruler-back}}" %format rulerfrontagda = "{\mbox{\scshape AG}_{\mbox{\scshape da}}}" %format rulercoreagda = "{\mbox{\scshape AG}^{\mbox{\scshape x}}_{\mbox{\scshape da}}}" %format Agda = "{\mbox{\scshape Agda}}" %format . = "." %format ^^ = "\;" %format ^^^ = "\;\;\;" %format ^^^^ = "\hspace{1em}" %format epsilon = "\epsilon" %format (sub (x) (y)) = "{" x "}_{" y "}" %format (sup (x) (y)) = "{" x "}^{" y "}" %format (many (x)) = "\overline{" x "}" %format forall = "\forall" %format Gamma = "\Gamma" %format Sigma = "\Sigma" %format Phi = "\Phi" %format :- = "\vdash" %format emptyset = "\emptyset" %format epsilon = "\epsilon" %format sep = "\:;\:" %format bar = "|" %format ::: = "\::\:" %format `union` = "\cup" %format union = "\cup" %format `intersection` = "\cap" %format intersection = "\cap" %format `subset` = " \subseteq " %format .== = "\doteq" %format `diam` = "\diamond" %format neg a = "\neg" a %format bottom = undefined %format Gamma0 %format Gamma1 %format Gamma2 %format Gamma3 %format Gamma4 %format Gamma' %format Gamma0 %format Gamma'' %format inGamma = "in" Gamma %format inGamma' %format Set1 %format Set2 %format _elem = "\_\in\_" %format _subseq = "\_\sqsubseteq\_" %format `subseq` = "\sqsubseteq" %format `mbElem` = "\in_?" %format _mbElem = "\_\in_?\_" %format `mbEqual` = "\equiv_?" %format `Either` = "\uplus" %format alpha = "\alpha" %format beta = "\beta" %format inj1 %format inj2 %format prv = "\phi" %format prv1 %format prv2 %format prv' %format tau = "\tau{}" %format tau' %format tau1 %format tau2 %format tau3 %format i1 %format i2 %format x1 %format x2 %format x3 %format x4 %format es1 %format es2 %format t1 %format t2 %format a1 %format a2 %format p1 %format p2 %format p3 %format p4 %format r1 %format r2 %format r3 %format r4 %format f1 %format f2 %format f3 %format f4 %format ty = "\tau" %format tail = "\kw{tail}" %format and = "\kw{and}" %format attr = "\kw{attr}" %format data = "\kw{data}" %format sem = "\kw{sem}" %format inh = "\kw{inh}" %format syn = "\kw{syn}" %format con = "\kw{con}" %format clause = "\kw{clause}" %format default = "\kw{default}" %format itf = "\kw{itf}" %format visit = "\kw{visit}" %format internal = "\kw{internal}" %format match = "\kw{match}" %format child = "\kw{child}" %format invoke = "\kw{invoke}" %format datasem = "\kw{datasem}" %format grammar = "\kw{grammar}" %format term = "\kw{term}" %format term0 = "\kw{term}^{?}" %format nonterm = "\kw{nonterm}" %format prod = "\kw{prod}" %format context = "\kw{context}" %format contexts = "\kw{contexts}" %format attach = "\kw{attach}" %format detach = "\kw{detach}" %format partition = "\kw{partition}" %format absurd = "\kw{absurd}" %format ?? = "^{?}" %format tau = "\tau" %format tau1 %format tau2 %format tau3 %format tau4 %format taus = "\overline{\tau}" %format taus1 %format taus2 %format taus3 %format taus4 %format adata = "\uw{data}" %format awhere = "\uw{where}" %format with = "\uw{with}" %format ainh = "\Varid{inh}" %format asyn = "\Varid{syn}" %format asem = "\Varid{sem}" %format xitf = "\Varid{itf}" %format nm = "\iota" %format nm1 %format nm2 %format nm3 %format nm4 %format terminator = "\Box" %format <+> = "\oplus{}" %format << = "\llbracket" %format >> = "\rrbracket" %format ~> = "\leadsto" %format (semb (z)) = << z >> %format (semiv (z) (i) (n) (t)) = "\llbracket_{\mathsf{iv\;}}" z >> "_{ " i "," t "}" "^{ " n "}" %format (sema (z)) = "\llbracket_{\mathsf{a\;}}" z >> %format (semat (z)) = "\llbracket_{\mathsf{at\;}}" z >> %format (seman (z)) = "\llbracket_{\mathsf{an\;}}" z >> %format (semev (z) (i) (n)) = "\llbracket_{\mathsf{ev }}" z >> "_{ " i "}" "^{ " n " }" %format (semr (z) (k)) = "\llbracket_{\mathsf{r\;}}" z >> "_{ " k "}" %format (semep (z) (i) (n)) = "\llbracket_{\mathsf{ep\;}}" z >> "_{ " i "}" "^{ " n " }" %format +++ = "{\_+\!\_}" %format Nat = "\ensuremath{{\mathbb{N}}}" %format (joinfun (x) (y)) = x "_" y %format (semfun (x)) = "sem_" x %format (catafun (x)) = "cata_" x %format (refi (c) (a)) = "{" c "_{" i "}" a "}" %format (refs (c) (a)) = "{" c "_{" s "}" a "}" %format (refc (k) (a)) = "{" k "_{" c "}" a "}" %format (refL (c) (a)) = "{" c "_{" l "}" a "}" %format (refa (c) (x)) = "{" c "_{" a "}" x "}" %format (refv (c) (x)) = "{" c "_{" v "}" x "}" %format (Tp (t)) = "{" T "''" t "}" %format (Tpv (t) (x)) = "{" T "''" t "''" x "}" %format (Tph (t) (x)) = "{" H "''" t "''" x "}" %format (Alg (t)) = "{" A "''" t "}" %format (ref (c) (a)) = "{" c "." a "}" %if not thesis \begin{abstract} %endif Attribute Grammars (AGs) are a domain-specific language for functional and composable descriptions of tree traversals. Given such a description, it is not immediately clear how to state and prove properties of AGs formally. To meet this challenge, we apply dependent types to AGs. In a dependently typed AG, the type of an attribute may refer to values of attributes. The type of an attribute is an invariant, the value of an attribute a proof for that invariant. Additionally, when an AG is cycle-free, the composition of the attributes is logically consistent. We present a lightweight approach using a preprocessor in combination with the dependently typed language Agda. %if not thesis \end{abstract} %endif \section{Introduction} Functional programming languages are known to be convenient languages for implementing %if thesis a compiler~\citep{DBLP:books/cu/Appel1998ml}. %else a compiler. %endif As part of the compilation process, a compiler computes properties of Abstract Syntax Trees (ASTs), such as environments, types, error messages, and code. In functional programming, these syntax-directed computations are typically written as \emph{catamorphisms}\footnote{ Catamorphisms are a generalization of folds to tree-like data structures. We consider catamorphisms from the perspective of algebraic data types in functional programming instead of the equivalent notion in terms of functors in category theory. A catamorphism |sub cata tau (f1, ..., sub f n)| replaces each occurrence of a constructor |sub c i| of |tau| in a data structure with |sub f i|. The product |(f1, ..., sub f n)| is called an \emph{algebra}. An element |sub f i| of the algebra is called a \emph{semantic function}. }. An \emph{algebra} defines an inductive property in terms of each constructor of the AST, and a catamorphism applies the algebra to the AST. Catamorphisms thus play an important role in a functional implementation of a compiler. Attribute Grammars (AGs)~\citep{DBLP:journals/mst/Knuth68} are a domain-specific language for \emph{composable} descriptions of catamorphisms. AGs facilitate the description of complex catamorphisms that typically occur in complex compiler implementations. %% Underlying an AG is a context-free grammar that describes the structure of the AST. An AG extends a context-free grammar by associating \emph{attributes} with nonterminals. Functional \emph{rules} are associated with productions, and define values for the attributes that occur in the nonterminals of associated productions. As AGs are typically embedded in a host language, the rules are terms in the host language, which may additionally refer to attributes. Attributes can easily be composed to form more complex properties. An AG can be compiled to an efficient functional algorithm that computes the synthesized attributes of the root of the AST, given the root's inherited attributes. It is not immediately clear how to formally specify and write proofs about programs implemented with AGs. %if thesis For example, it is common to prove that a type inferencer is a sound and complete implementation of a type system, and that the meaning of a well typed source program is preserved. %endif \emph{Dependent types}~\citep{bove09} provide a means to use \emph{types} to encode properties with the expressiveness of (higher-order) intuitionistic propositional logic, and \emph{terms} to encode proofs. Such programs are called correct by construction, because the program itself is a proof of its invariants. The goal of \thiswork{} is therefore to apply dependent types to AGs, in order to formally reason with AGs. Vice versa, AGs also offer benefits to dependently typed programming. Because of the Curry-Howard correspondence, dependently typed AGs are a domain-specific language to write structurally inductive proofs in a \emph{composable}, \emph{aspect-oriented} fashion; each attribute represents a separate aspect of the proof. Additionally, AGs alleviate the programmer from the tedious orchestration of multi-pass traversals over data structures, and ensure that the traversals are \emph{total}: totality is required for dependently typed programs for reasons of logical consistency and termination of type checking. Hence, the combination of dependent types and AGs is mutually beneficial. We make the following contributions in \thiswork{}: \begin{itemize} \item We present the language |rulerfrontagda| (Section~\ref{depend.section.example}), a light-weight approach to facilitate dependent types in AGs, and vice versa, AGs in the dependently typed language Agda. |rulerfrontagda| is an embedding in Agda via a preprocessor. In contrast to conventional AGs, we can encode invariants in terms of dependently typed attributes, and proofs as values for attributes. This expressiveness comes at a price: to be able to compile to a total Agda program, we restrict ourselves to the class of ordered AGs, and demand the definitions of attributes to be total. \item We define a desugared version of |rulerfrontagda| programs (Section~\ref{depend.sect.rulerfront.agda}) and show how to translate them to plain Agda programs (Section~\ref{depend.sect.translation.agda}). \item Our approach supports a conditional attribution of nonterminals, so that we can give total definitions of what would otherwise be partially defined attributes (Section~\ref{depend.sect.partial}). \end{itemize} In Section~\ref{depend.section.preliminaries}, we introduce the notation used in \thiswork{}. However, we assume that the reader is both familiar with AGs (see \citep{uuagc}) and dependently typed programming in Agda (see \citep{DBLP:conf/tldi/Norell09}). %if False %% Might have some nice sentences to use in the thesis introduction In the last years, we applied AGs in several large projects, including the Utrecht Haskell Compiler~\citep{uhc}, the Helium~\citep{Leijen:helium} compiler for learning Haskell, and the editor Proxima~\citep{Schrage04proxima}. The use of AGs in these projects is invaluable, for two reasons: rules for attributes can be written in isolation and combined automatically, and trivial rules can be inferred, saving the programmer from writing boilerplate code. Given a compiler such as the UHC, the question arises to what extend the compiler generates correct code (for some definition of correctness). In UHC, similar to any project that many people contribute to, we regularly encounter subtle bugs related to broken hidden invariants. Through the use of regression testing, we get a fair idea of how well the implementation is, however we never get sure about the number of erroneous cases that lurk in a dark corner. The holy grail in compiler implementation is to formally verify that a compiler exhibits certain properties of interest. For example, that a type inferencer is a sound and complete implementation of a type system, and that the meaning of a well typed source program is preserved. In practice, this formal verification is (still) infeasible for large projects with limited contributors. Given the complexity of compilers involved, it is already a struggle to implement and maintain a compiler that gives output that seems correct, let alone to attempt to prove this. When we implement our compilers in languages with advanced type systems, we can ensure that compilers have certain properties by construction. In mainstream strongly typed languages, it is possible to guarantee that (even for non-trivial inputs) the compiler produces output that conforms to a context-free grammar. It is enforceable that a compiler produces, for example, syntactically-correct HTML or C code. These are properties we get for free when we define our data structures properly in, for example, the strongly-typed programming language Haskell. Unfortunately, syntactic guarantees do not save us from hidden invariants. For that, we desire semantic guarantees. This is possible by using more complex types, but at a severe cost. It actually requires us to encode proofs by using the type system as a logic. In a dependently typed language such as Agda, we can impose arbitrary complex constraints on values via types, but as a consequence, proving that the program is well typed becomes considerably harder. To move from a compiler implementation in Haskell to Agda, for example, the least extra effort required---syntax and library issues aside---is to prove termination of the program (ensures that the program is a proof in a consistent logic). Compilers typically consist of primitive recursive functions, and those parts in a compiler that rely on iteration either compute fixpoints, or have iteration limits. Unification-based type inferencers may need to ensure that types in the substitution are finite, imposed via the `occurs check', which is a relatively easy property. The extra effort is substantial, but theoretically speaking, not a creative challenge. From there on, the programmer can make the types more specific, and prove stronger invariants. For a project the size of UHC, a verified compiler is still too much to ask for, as it makes implementation and maintenance more difficult and time consuming. Recent developments in dependently typed programming, however, make such approaches more and more feasible. Several success stories are known, which is promising for the future. Since we implement our compilers with Attribute Grammars, we present in \thiswork{} how these can be combined with dependently typed programming, using Agda in particular. AGs can be compiled to (a sequence of) functions that take a record of inherited attributes, have cases for each type of AST node, recursively visit the children of such a node, and produce a record of synthesized attributes. Such functions can be written in Agda. There are thus no theoretic limitations that prevent AGs to be embedded in a dependently typed programming language. However, dependently typed programming enforces structure to a program that is inconvenient when using plain Attribute Grammars. In short, to profit from programming with AGs, a fine granularity of attributes is beneficial, but may require partially defined attributes. In a dependently typed setting, all attributes must have a total definition, and to accomplish that, a coarser granularity of attributes may be required. The coarser the granularity of attributes, the less benefits an AG has over a conventional fold. We demonstrate this with an example in Section~\ref{depend.section.example}, and we show that we can keep the fine granularity of attributes when we extend attribute grammars with context-dependent attribution. In previous work, we implemented an AG preprocessor for Haskell, and some other languages (cite, cite). The language of this preprocessor is called RulerCore. In \thiswork{}, we introduce a variant called |rulerfrontagda|, which has additional syntax to support the more complex types for attributes, and to deal with dependently typed pattern matching in the left-hand sides of rules. In particular, dependent pattern matching against attributes may impose additional constraints on other attributes. For example, in the scope of a match against an equality proof, we get the additional information that two attributes are the same and Agda requires them to get a common name. The example in Section~\ref{depend.section.example} again demonstrates. As contributions, we extensively discuss an example in Section~\ref{depend.section.example}, then describe the AG-language |rulerfrontagda| in Section~\ref{depend.sect.rulerfront.agda}, and its translation to Agda in Section~\ref{depend.sect.translation.agda}. %endif \section{Preliminaries} \label{depend.section.preliminaries} In this warm-up section, we briefly touch upon the Agda and AG notation used throughout \thiswork{}. As an example, we implement the sum of a list of numbers with a catamorphism. We give two implementations: first one that uses plain Agda, then another using |rulerfrontagda|. This example does not yet use dependently typed attributes. These are introduced in the next section. In the following code snippet, the data type |List| represents a cons-list of natural numbers. The type |Tp List| is the type of the value we compute (a number), and |Alg List| is the type of an algebra for |List|. Such an algebra contains a \emph{semantic function} for each constructor of |List|, which transforms a value of that constructor into the desired value (of type |Tp List|), assuming that the transformation has been recursively applied to the fields of the constructor. The catamorphism |catafun List| performs the recursive application. \begin{code} adata List : Set awhere -- represents a cons-list of natural numbers nil : List -- constructor has no fields cons : Nat -> List -> List -- constructor has a number and tail list as fields Tp List = Nat -- defines a type alias |Tp List : Set|, Alg List = (Tp List , Nat -> Tp List -> Tp List) -- and |Alg List : Set| catafun List ^^ : Alg List -> List -> Tp List -- applies algebra to list catafun List ^^ (n , _) nil ^^^ = n -- in case of |nil|, replaces |nil| with |n| catafun List ^^ alg l ^^^ with ^^ alg ^^ | ^^ l -- otherwise, matches on |alg| and |l| catafun List ^^ alg l ^^^ | (_ , c) | cons x xs ^^^ with ^^ (catafun List) alg xs -- recurses on |xs| catafun List ^^ alg l ^^^ | (_ , c) | cons x xs ^^^ | r ^^^ = c x r -- replaces |cons| with |c| \end{code} %format bar = "\mid" %format e1 %format eN = e "_" n In Agda, a function is defined by one or more equations. A with-construct facilitates pattern matching against intermediate values. An equation that ends with |with e1 bar ... bar eN| parameterizes the equations that follow with the values of |e1, ..., eN| as additional arguments. Vertical bars separate the patterns intended for the additional parameters. %% In the above code snippet, |l| is scrutinized to %% match against a |cons|-value, and |alg| is scrutinized to get the semantic function %% |c| that is intended for |cons|-constructors. The with-construct can also be used to %% give names to intermediate values: the result of the %% expression |(catafun List) alg xs| is given the name |r|. The actual algebra itself simply takes |0| for the |nil| constructor, and |+++| for the |cons| constructor. The function |joinfun sum List| shows how the algebra and catamorphism can be used. \begin{code} semfun nil : Tp List -- semantic function for |nil| constructor semfun nil = 0 -- |Tp List = Nat| (defined above) semfun cons : Nat -> Tp List -> Tp List -- semantic function for |cons| constructor semfun cons = +++ -- |+++ : Nat -> Nat -> Nat| (defined in library) joinfun sum List : List -> Tp List -- transforms the |List| into the desired sum joinfun sum List = catafun List (semfun nil, semfun cons) -- algebra is semantic functions in a tuple \end{code} In the example, the sum is defined in a bottom-up fashion. By taking a function type for |Tp List|, values can also be passed top-down. Multiple types can be combined by using products. Such algebras quickly become tedious to write. Fortunately, we can use AGs as a domain-specific language for algebras. In the code below, we give an AG implementation: we specify a grammar that describes the structure of the AST, declare attributes on productions, and give rules that define attributes. We now give an implementation of the same example using |rulerfrontagda|. The code consists of blocks of plain Agda code, and blocks of AG code. To ease the distinction, Agda's keywords are underlined, and keywords of |rulerfrontagda| are typeset in bold. A grammar specification is a restricted form of a data declaration (for an AST): data constructors are called \emph{productions} and their fields are explicitly marked as \emph{terminal} or \emph{nonterminal}. A nonterminal field represents a \emph{child} in the AST and has attributes, whereas a terminal field only has a value. A plain Agda data-type declaration can be derived from a grammar specification. In such a specification, nonterminal types must have a fully saturated, outermost type constructor that is explicitly introduced by a grammar declaration. Terminal types may be arbitrary Agda types\footnote{ In general, although not needed in this example, nonterminal types may be parametrized, production types may refer to its field names, and field types may refer to preceding field names. }. \begin{code} grammar List : Set -- declares nonterminal |List| of type |Set| prod nil : List -- production |nil| of type |List| (no fields) prod cons : List -- production |cons| of type |List| (two fields) term ^^^ hd : Nat -- terminal field |hd| of type |Nat| nonterm ^^^ tl : List -- nonterminal field |tl| of type |List| \end{code} With an interface specification, we declare attributes for nonterminals. Attributes come in two fashions: \emph{inherited} attributes (used in a later example) must be defined by rules of the parent, and \emph{synthesized} attributes may be used by the parent. Names of inherited attributes are distinct from names of synthesized attributes; an attribute of the same name and fashion may only be declared once per nonterminal. We also partition the attributes in one or more \emph{visits}. These visits impose a partial order on attributes. Inherited attributes may not be defined in terms of a synthesized attributes of the same visit or later. We use this order in Section~\ref{depend.sect.rulerfront.agda} to derive semantic functions that are total. \begin{code} itf List -- interface for nonterminal |List|, visit compute -- with a single visit that is named |compute|, syn sum : Nat -- and a synthesized attribute named |sum| of type |Nat| \end{code} %format namechild = "\Varid{child}" %format nameattr = "\Varid{attr}" Finally, we define each of the production's attributes. We may refer to an attribute using |ref namechild nameattr| notation. For each production, we give rules that define the inherited attributes of the children and synthesized attributes of the production itself (with |lhs| as special name), using inherited attributes of the production and synthesized attributes of the children. The special name |loc| refers to the terminals, and to local attributes that we may associate with a production. \begin{code} datasem List -- defines attributes of |List| for constructors of |List| prod nil ^^^ lhs.sum = 0 -- rule for |sum| of production |nil| prod cons ^^^ lhs.sum = loc.hd + ref tl sum -- refers to terminal |hd| and attr |ref tl sum| \end{code} The left-hand side of a rule is a plain Agda pattern, and the right-hand side is either a plain Agda expression or with-construct (not shown in this example). Additionally, both the left and right-hand sides may contain attribute references. During attribute evaluation, visits are performed on children to obtain their associated synthesized attributes. We do not have to explicitly specify when to visit these children, neither is the order of appearance of rules relevant. However, an inherited attribute |ref c x| may not depend on a synthesized attribute |ref c y| of the same visit or later (in the interface). This guarantees that the attribute dependencies are acyclic, so that we can derive when children need to be visited and in what order. AGs are a domain-specific language to write algebras in terms of attributes. From the grammar, we generate the data type and catamorphism. From the interface, we generate the |Tp List| type. From the rules, we generate the semantic functions |semfun nil| and |semfun cons|. AGs pay off when an algebra has many inherited and synthesized attributes. Also, there are many AG extensions that offer abstractions over common usage patterns (not covered in \thiswork{}). In the next section we present AGs with dependent types, so that we can formulate properties of attributes (and their proofs). \section{Dependently Typed Example} \label{depend.section.example} In this section, we use |rulerfrontagda| to implement a mini-compiler that performs name checking of a simple language |Source|, and translates it to target language |Target| if all used identifiers are declared, or produces errors otherwise. A term in |Source| is a sequence of identifier definitions and identifier uses, for example: |def a `diam` use b `diam` use a|. In this case, |b| is not defined, thus the mini-compiler reports an error. Otherwise, it generates a |Target| term, which is a clone of the |Source| term that additionally carries evidence that the term is free of naming errors. Section~\ref{depend.sect.example.grammar} shows the definition of both |Source| and |Target|. We show how to prove that the mini-compiler produces only correctly named |Target| terms and errors messages that only mention undeclared identifiers. The proofs are part of the implementation's code. Name checking is only a minor task in a compiler. However, the example shows many aspects of a more realistic compiler. \subsection{Support Code Dealing With Environments} \label{depend.sect.utilcode} We need some Agda support code to deal with environments. We show the relevant data structures and type signatures for operations on them, but omit the actual implementation. %if thesis See Section~\ref{depend.sect.support} for more details about the actual implementation. %endif %if False \footnote{ We show only the signatures. The implementation can be found in %% TODO Section~\ref{depend.sect.support}. } %endif %% \footnote{ %% Section~\ref{depend.sect.support} shows the actual implementation of the support code. %%}. We represent the environment as a cons-list of identifiers. \begin{code} Ident = String -- |Ident : Set| Env = List Ident -- |Env : Set| \end{code} In intuitionistic type theory, a data type represents a relation, its data constructors deduction rules for such a relation, and values built using these constructors are proofs for instances of the relation. We use some data types to reason with environments. A value of type |nm `elem` Gamma| is a proof that an identifier |nm| is member of an environment |Gamma|. A value |here| indicates that identifier is at the front of the environment. A value |next| means that the identifier can be found in the tail of the environment, as described by the remainder of the proof. \begin{code} adata _elem : Ident -> Env -> Set awhere here : {nm : Ident} {Gamma : Env} -> nm `elem` (nm :: Gamma) next : {nm1 : Ident} {nm2 : Ident} {Gamma : Env} -> nm1 `elem` Gamma -> nm1 `elem` (nm2 :: Gamma) \end{code} The type |Gamma1 `subseq` Gamma2| represents a proof that an environment |Gamma1| is contained as a substring (with each mapping as a symbol) of an environment |Gamma2|. A value |subLeft| means that the environment |Gamma1| is a prefix of |Gamma2|, and |subRight| means that |Gamma1| is a suffix. With |trans|, we transitively compose two proofs. \begin{code} adata _subseq : Env -> Env -> Set awhere subLeft : {Gamma1 : Env} {Gamma2 : Env} -> Gamma1 `subseq` (Gamma1 ++ Gamma2) subRight : {Gamma1 : Env} {Gamma2 : Env} -> Gamma2 `subseq` (Gamma1 ++ Gamma2) trans : {Gamma1 : Env} {Gamma2 : Env} {Gamma3 : Env} -> Gamma1 `subseq` Gamma2 -> Gamma2 `subseq` Gamma3 -> Gamma1 `subseq` Gamma3 \end{code} The following functions operate on proofs. When an identifier occurs in an environment, function |inSubset| produces a proof that the identifier is also in the superset of the environment. Given an identifier and an environment, |nm `mbElem` Gamma| returns either a proof |nm `elem` Gamma| that the element is in the environment, or a proof that it is not. \begin{code} inSubset : {nm : Ident} {Gamma1 : Env} {Gamma2 : Env} -> Gamma1 `subseq` Gamma2 -> nm `elem` Gamma1 -> nm `elem` Gamma2 _mbElem : (nm : Ident) -> (Gamma : Env) -> neg (nm `elem` Gamma) `Either` (nm `elem` Gamma) \end{code} A value of the sum-type |alpha `Either` beta| either consists of an |alpha| wrapped in a constructor |inj1| or of a |beta| wrapped in |inj2|. \subsection{Grammar of the Source and Target Language} \label{depend.sect.example.grammar} Below, we give a grammar for both the |Source| and |Target| language, such that we can analyze their ASTs with AGs\footnote{ In our example, we could have defined the type |Target| using conventional Agda notation instead. However, the grammar for |Target| serves as an example of a parameterized nonterminal. }. The |Target| language is a clone of the |Source| language, except that terms that have identifiers carry a field |proof| that is evidence that the identifiers are properly introduced. \begin{code} grammar Root : Set -- start symbol of grammar and root of AST prod root : Root ^^^ nonterm top : Source -- top of the |Source| tree grammar Source : Set -- grammar for nonterminal |Source| prod use : Source -- 'result type' of production term nm : Ident -- terminals may have arbitrary Agda types prod def : Source -- 'result type' may be parametrized term nm : Ident prod _`diam`_ : Source -- represents sequencing of two |Source| terms nonterm left : Source -- nonterminal fields must have a nonterm as nonterm right : Source -- outermost type constructor. grammar Target : Env -> Set -- grammar for nonterminal |Target| prod def : Target Gamma -- production type may refer to any field, term0 Gamma : Env -- e.g. |Gamma|. Agda feature: implicit terminal term nm : Ident -- \hspace{4pt} (inferred when building a |def|) term prv : nm `elem` Gamma -- field type may refer to preceding fields prod use : Target Gamma term0 Gamma : Env -- a |Target| term carries evidence: a term nm : Ident -- proof that the identifier is in the term prv : nm `elem` Gamma -- environment _`diam`_ : Target Gamma term0 Gamma : Env nonterm left : Target Gamma -- nonterm fields introduce children that nonterm right : Target Gamma -- have attributes adata Err : Env -> Set where -- data type for errors in Agda notation scope : {Gamma : Env} (nm : Ident) -> neg (nm `elem` Gamma) -> Err Gamma Errs Gamma = List (Err Gamma) -- |Errs : Env -> Set| \end{code} As shown in Section~\ref{depend.section.preliminaries}, we generate Agda data-type definitions and catamorphisms from this specification. The concrete syntax of the source language |Source| and target language |Target| of the mini-compiler is out of scope for \thiswork{}; the grammar defines only the abstract syntax. Similarly, we omit a formal operational semantics for |Source| and |Target|: it evaluates to unit if there is an equally named |def| for every |use|, otherwise evaluation diverges. \subsection{Dependent Attributes} In this section, we define \emph{dependently typed} attributes for |Source|. Such a type may contain references to preceding\footnote{ We may refer to an attribute that is declared earlier (in order of appearance) in the same interface. There is one exception due to the translation to Agda (Section~\ref{depend.sect.translation.agda}): in the type of an inherited attribute, we may not refer to synthesized attributes of the same visit. } attributes using |ainh.attrNm| or |asyn.attrNm| notation, which explicitly distinguishes between inherited and synthesized attributes. The type specifies a property of the attributes it references; an attribute with such a type represents a proof of this property. In our mini-compiler, we compute bottom-up a synthesized attribute |gathEnv| that contains identifiers defined by the |Source| term. At the root, the |gathEnv| attribute contains all the defined identifiers. We output its value as the synthesized attribute |finEnv| (final environment) at the root. Also, we pass its value top-down as the inherited attribute |finEnv|, such that we can refer to this environment deeper down the AST. We also pass down an attribute |gathInFin| that represents a proof that the final environment is a superset of the gathered environment. When we know that an identifier is in the gathered environment, we can thus also find it in the final environment. We pass up the attribute |outcome|, which consists either of errors, or of a correct |Target| term. \begin{code} itf Root -- attributes for the root of the AST visit compile ^^^ syn finEnv : Env syn outcome : (Errs asyn.finEnv) `Either` (Target asyn.finEnv) itf Source -- attributes for |Source| visit analyze ^^^ syn gathEnv : Env -- attribute of first visit visit translate ^^^ inh finEnv : Env -- attributes of second visit inh gathInFin : asyn.gathEnv `subseq` ainh.finEnv syn outcome : (Errs ainh.finEnv) `Either` (Target ainh.finEnv) itf Target Gamma -- interface for |Target| (parameterized) is not used in the example. \end{code} As we show later, at the root, we need the value of |gathEnv| to define |finEnv|. This requires |gathEnv| to be placed in a strict earlier visit. Hence we define two visits, ordered by appearance. Attribute |gathInFin| has a dependent type: it specifies that |gathEnv| is a substring of |finEnv|. A value of this attribute is a proof that essentially states that we did not forget any identifiers. Similarly, in order to construct |Target| terms, we need to prove that |finEnv| defines the identifiers that occur in the term. In the next section, we construct such proofs by applying data constructors. We may use inherited attributes as \emph{assumptions} and pattern matches against values of attributes as \emph{case distinctions}. Thus, with a dependently typed AG we can formalize and prove correctness properties of our implementation. Agda's type checker validates such proofs using symbolic evaluation driven by unification. \subsection{Semantics of Attributes} For each production, we give definitions for the declared attributes via rules. At the root, we pass the gathered environment back down as final environment. Thus, these two attributes are equal, and we can trivially prove that the final environment is a substring using either |subRight| or |subLeft|. \begin{code} datasem Root prod root -- rules for production |root| of nonterm |Root| top.finEnv = top.gathEnv -- pass gathered environment down top.gathInFin = subRight {[]} -- substring proof, using: |[] ++ Gamma4 == Gamma4| lhs.finEnv = top.gathEnv -- pass |gathEnv| up lhs.outcome = top.outcome -- pass |outcome| up \end{code} For the |use|-production of |Source|, we check if the identifier (terminal |loc.nm|) is in the environment. If it is, we produce a |Target| term as value for the outcome attribute, otherwise we produce a |scope| error. For |def|, we introduce an identifier in the gathered environment. No errors can arise, hence we always produce a |Target| term. We prove (|loc.prv1|) that the identifier |loc.nm| is actually in the gathered environment, and prove (|loc.prv2|) using |inSubset| and attribute |lhs.gathInFin| that it must also be in the final environment. For |_`diam`_|, we pass |finEnv| down to both children, concatenate their |gathEnv|s, and combine their |outcome|s. \begin{code} datasem Source -- rules for productions of |Source| prod use lhs.gathEnv = [] -- no names introduced lhs.outcome with loc.nm `mbElem` lhs.finEnv -- tests presence of |nm| | inj1 notIn = inj1 [ scope loc.nm notIn ] -- when not in env | inj2 isIn = inj2 (use loc.nm isIn) -- when in env prod def lhs.gathEnv = [ loc.nm ] -- one name introduced loc.prv1 = here {loc.nm} {asyn.lhs.gathEnv} -- proof of |nm| in |gathEnv| loc.prv2 = inSubset lhs.gathInFin loc.prv1 -- proof of |nm| in |finEnv| lhs.outcome = inj2 (def loc.nm loc.prv2) -- never any errors prod _`diam`_ lhs.gathEnv = left.gathEnv ++ right.gathEnv -- pass names up left.finEnv = lhs.finEnv -- pass |finEnv| down right.finEnv = lhs.finEnv -- pass |finEnv| down left.gathInFin = trans subLeft lhs.gathInFin -- proof for |left| right.gathInFin = trans (subRight {asyn.lhs.gathEnv} {lhs.finEnv}) lhs.gathInFin -- proof for |right| lhs.outcome with left.outcome -- four alts. | inj1 es with right.outcome | inj1 es1 | inj1 es2 = inj1 (es1 ++ es2) -- 1: both in error | inj1 es1 | inj2 _ = inj1 es1 -- 2: only |left| | inj2 t1 with left.outcome | inj2 t1 | inj1 es2 = inj1 es2 -- 3: only |right| | inj2 t1 | inj2 t2 = inj2 (t1 `diam` t2) -- 4: none in error \end{code} Out of the above code, we generate each production's semantic function (and some wrapper code), such that these together with a catamorphism form a function that translates |Source| terms. The advantage of using AGs here is that we can easily add more attributes (and thus more properties and proofs) and refer to them. \section{AG Descriptions and their Core Representation} \label{depend.sect.rulerfront.agda} In the previous sections, we presented |rulerfrontagda| (by example). To describe the dependently-typed extension to AGs, we do so in terms of the core language |rulercoreagda| (a subset of |rulerfrontagda|). Implicit information in AG descriptions (notational conveniences, the order of rules, visits to children) is made explicit in |rulercoreagda|. We sketch the translation from |rulerfrontagda| to |rulercoreagda|. In previous work~\citep{Middelkoop10wgt,Middelkoop10gpce}, we described the process in more detail (albeit in a non-dependently typed setting). |rulercoreagda| contains interface declarations, but grammar declarations are absent and semantic blocks encoded differently. Each production in |rulerfrontagda| is mapped to a \emph{semantic function} in |rulercoreagda|: it is a domain-specific language for the contents of semantic functions. A terminal |x : tau| of the production is mapped to a parameter |(refL loc x) : tau|. Implicit terminals are mapped to implicit parameters. A nonterminal |x : N taus| is mapped to a parameter |refc loc x : Tp N taus|. The body of the production consists of the rules for the production given in the original |rulercoreagda| description, plus a number of additional rules that declare children and their visits explicitly. %format semprod_seq = asem "\!\diamond{}" \begin{code} semprod_seq : Tp Source -> Tp Source -> Tp Source -- derived from (non)terminal types semprod_seq (refc loc left) (refc loc right) = -- semantic function for |`diam`| sem : Source -- |rulercoreagda| semantics block child left : Source = (refc loc left) -- defines a child |left| child right : Source = (refc loc right) -- defines a child |right| invoke analyze of left -- rule requires visiting |analyze| on |left| invoke analyze of right -- rule requires visiting |analyze| on |right| invoke translate of left invoke translate of right lhs.gathEnv = left.gathEnv ++ right.gathEnv -- the |rulerfrontagda| rules ... -- etc. \end{code} A child rule introduces a child with explicit semantics (a value of the type |Tp Source|). Other rules may declare visits and refer to the attributes of the child. An invoke rule declares a visit to a child, and brings the attributes of that visit in scope. Conventional rules define attributes, and may refer to attributes. The dependencies between attributes induces a def-use (partial) order. \begin{figure}[tb] \begin{code} e ::= Agda [ many b ] -- embedded blocks |b| in |Agda| b ::= i | s | o -- |rulercoreagda| blocks o ::= ainh.c.x | asyn.c.x | loc.x -- embedded attribute reference i ::= itf I (many x) : tau v -- with first visit |v|, params |x|, and signature |tau| v ::= visit x inh (many a) syn (many a) v -- visit declaration | terminator -- terminator of visit decl. chain a ::= x : e -- attribute decl, with Agda type |e| s ::= sem : I (many e) t -- semantics expr, uses interface |I (many e)| t ::= visit x (many r) t -- visit definition, with next visit |t| | terminator -- terminator of visit def. chain r ::= p e' -- evaluation rule | invoke x of c -- invoke-rule, invokes |x| on child |c| | child c : I = e -- child-rule, defines a child |c|, with interface |I (many e)| p ::= o -- attribute def | .{e} -- Agda dot pattern | x (many p) -- constructor match e' ::= with e (many (p' e'??)) -- Agda |with| expression (|e'| absent when |p'| absurd) | = e -- Agda |=| expression p' -- Agda LHS x, I, c -- identifiers, interface names, children respectively tau -- plain Agda type \end{code} \caption{Syntax of |rulercore|} \label{depend.fig.sem.agda.rulercore} \end{figure} Actually, there is one more step to go to end up with a |rulercoreagda| description. A semantics block consists of one of more visit-blocks (in the order specified by the interface), and the rules are partitioned over the blocks. In a block, the |lhs| attributes of that and earlier visits are in scope, as well as those brought in scope by preceding rules. Also, the synthesized attributes of the visit must be defined in the block or in an earlier block. We assign rules to the earliest block that satisfies the def-use order. We convert this partial order into a total order by giving conventional rules precedence over child/invoke rules, and using the order of appearance otherwise: \begin{code} semprod_seq : Tp Source -> Tp Source -> Tp Source -- signature derived from itf semprod_seq (refc loc left) (refc loc right) = -- semantic function for |`diam`| sem : Source -- |rulercoreagda| block visit analyze -- first visit child left : Source = (refc loc left) -- defines a child |left| invoke analyze of left -- requires child to be defined child right : Source = (refc loc right) -- defines a child |right| invoke analyze of right -- requires child to be defined asyn.lhs.gathEnv = asyn.left.gathEnv ++ asyn.right.gathEnv visit translate -- second visit ainh.left.finEnv = ainh.lhs.finEnv -- needs |lhs.finEnv| ainh.right.finEnv = ainh.lhs.finEnv -- needs |lhs.finEnv| ainh.left.gathInFin = trans ... -- also needs |lhs.gathEnv| ainh.right.gathInFin = trans ... -- also needs|lhs.gathEnv| invoke translate of left -- needs def of inh attrs of |left| invoke translate of right -- needs def of inh attrs of |right| asyn.lhs.outcome ^^^ with ... -- needs |translate| attrs of children \end{code} It is a static error when such an order cannot be satisfied. Another interesting example is the semantic function for the root: it has a child with an interface different from its own, and has two invoke rules in the same visit. \begin{code} sem_root : Tp Source -> Tp Root -- semantic function for the root sem_root locStop = -- |Source|'s semantics as parameter sem : Root visit compile -- only one visit child top : Source = (refc loc top) -- defines a child |top| invoke analyze of top -- invokes first visit of |top| ainh.top.finEnv = asyn.top.gathEnv -- passes gathered environment back invoke translate of top -- invokes second visit of |top| asyn.lhs.output = asyn.top.gathEnv -- passes up the gathered env asyn.lhs.output = asyn.top.outcome -- passes up the result \end{code} Figure~\ref{depend.fig.sem.agda.rulercore} shows the syntax of |rulercoreagda|. In general, interfaces may be parametrized. The interface has a function type |tau| (equal to the type of the nonterminal declaration in |rulerfrontagda|) that specifies the type of each parameter, and the kind of the interface (an upper bound of the kinds of the parameters). For an evaluation rule, we either use a |with|-expression when the value of the attribute is conditionally defined, or use a simple equation as RHS. In the next section, we plug such an expression in a function defined via with-expressions; hence we need knowledge about the with-structure of the RHS. \section{Translation to Agda} \label{depend.sect.translation.agda} To explain the preprocessing of |rulercoreagda| to Agda, we give a translation scheme in Figure~\ref{depend.fig.sem.denot.agda} (explained via examples below). This translation scheme is a denotational semantics for |rulercoreagda|. Also, if the translation is correct Agda, then the original is correct |rulercoreagda|. %format inhAx = "\Varid{inh}_\Varid{a}" x %format synAx = "\Varid{syn}_\Varid{a}" x %format cVx = "\Varid{c}_\Varid{v}" x %format contv = "\varsigma" \begin{figure}[p] \begin{smallcode} \begin{code} (semb (itf I (many x) : (many (sub tau x))-> tau) v) ~> (semiv (v) (I) (many (x : (sub tau x) )) (tau)) ^^^ ; ^^^ (semb (sig I)) : (semb tau) ^^^ ; ^^^ (semb (sig I)) = (semb (sig I (name v))) (semiv (visit x inh (many a) syn (many b) v) (I) (many g) (tau)) ~> (semiv (v) (I) (many g ++ many a ++ many b) (tau)) -- interface type for later visits (semb (sig I x)) : (semat (sub g 1)) -> ... -> (semat (sub g n)) -> (semb (resultty tau)) (semb (sig I x)) (many (seman g)) = (sema (ainh.(sub a 1))) -> ... -> (sema (ainh.(sub a n))) -> (semb (typrod (many asyn.b) (sig I (name v)))) (semiv (terminator) (I) (many g) (tau)) ~> (semb (sig I terminator)) = terminator -- terminator (some unit-value) (sema (x : e)) ~> (semb (atname x)) : (semb e) -- extract attribute name and type (semat (x : e)) ~> (semb e) -- extract attribute type (seman (x : e)) ~> (semb (atname x)) -- extract attribute name (semb (sem x : I (many e) t)) ~> (semb (vis lhs (name t))) awhere (semev t I (many e, emptyset)) -- top of semfun (semev (visit x (many r) t) (I) (many e, many g)) ~> (semb (vis lhs x)) : (semb (sig I x)) (semb (many e)) (many (seman g)) -- type of visit fun (semb (vis lhs x)) (semb (inhs I x)) = (semr (many r) (semb contv)) -- chain of rules ^^^^ (semb contv) ~> = (semb (valprod (syns I x) (vis lhs (name t)))) awhere (semev t I (many g ++ many a ++ many b)) -- next visit (semev terminator (I) (many e, many g)) ~> (semb (vis lhs terminator)) : (semb (sig I terminator)) (semb (many e)) (many (seman g)) ^^^ ; ^^^ (semb (vis lhs terminator)) = terminator (semr (child c : I = e) k) ~> with (semb e) ^^^ ... | (semb (vis I (firstvisit I))) (semb k) -- |k|: remaining rules (semr (invoke x of c) k) ~> with (semb (vis (xitf c) x)) (semb (inhs (xitf c) x)) -- pass inh values ... | (valprod (syns (xitf c) x)) (semb k) -- match syn values (semr (p e') k) ~> (semep e' p k) -- translation for attr def rule (semep (with e (many (p e'))) p k) ~> with e ^^^ (many (... | (semb p) (semr (p e') k))) -- rule RHS is with-constr (semep (= e) p k) ~> with e ^^^ ... | (semb p) k -- rule RHS is expr atref ainh.c.x = refi c x ^^^^ atname ainh.x = inhAx -- naming conventions atref asyn.c.x = refs c x ^^^^ atname asyn.x = synAx -- |atref|: ref to attr value atref loc.x = refL loc x ^^^^ atname x = x -- |atname|: ref to attr in type vis I x = vis lhs x ^^^^ sig I = Tp I -- |vis|: name of visit function vis c x = refv c x ^^^^ sig I x = Tpv I x -- |sig|: itf types \end{code} \end{smallcode} \caption{Translation of |rulercoreagda| to Agda.} \label{depend.fig.sem.denot.agda} \end{figure} A semantics block in an |rulercoreagda| program is actually an algorithm that makes precise how to compute the attributes as specified by the interface: for each visit, the rules prescribe when to compute an attribute and when to visit a child. The idea is that we map such a block to an Agda function that takes values for its inherited attributes and delivers a dependent product\footnote{ A dependent product |Sigma tau f = (tau , f tau)| parameterizes the RHS |f| with the LHS |tau|. } of synthesized attributes. However, such a function would be cyclic: in the presented example, the result |gathEnv| would be needed for as input for |finEnv|. Fortunately, we can bypass this problem: we map to a |k|-visit \emph{coroutine} instead. A coroutine is a function that can be invoked |k| times. We associate each invocation with a visit of the interface. Values for the inherited attributes are inputs to the invocation. Values for the synthesized attributes are the result of the invocation. In a pure functional language (like Agda), we can encode coroutines as one-shot continuations (or \emph{visit functions}~\citep{Saraiva99}). We generate types for coroutines and for the individual visit functions that make up such a coroutine. These types are derived from the interface. For each visit (e.g. |translate| of |Source|), we generate a type that represents a function type from the attribute types of the inherited attributes for that visit, to a dependent product (|Sigma|) of the types of the synthesized attributes and the type of the next visit function. These types are parameterized with the attributes of earlier visits (e.g. |Tpv Source translate (refa asyn gathEnv)|). The type of the coroutine itself is the type of the first visit. %if thesis The type of the last visit is a terminator |terminator|. %endif \begin{smallcode} \begin{code} Tp Source ^^^ = ^^ Tpv Source analyze Tpv Source analyze ^^^ = ^^ Sigma ^^^ Env ^^^ (Tpv Source translate) Tpv Source translate ^^^ (refa asyn gathEnv) ^^ = ((refa ainh finEnv) ^^ : ^^ Env) ^^^ -> ^^^ ((refa ainh gathInFin) ^^ : ^^ (refa asyn gathEnv) `subseq` (refa ainh finEnv)) ^^ -> Sigma ^^ (Errs (refa ainh finEnv) `Either` Target (refa ainh finEnv)) ^^^ ((Tpv Source terminator) ^^^ (refa asyn gathEnv) (refa ainh finEnv) (refa ainh gathInFin)) Tpv Source terminator ^^^ (refa asyn gathEnv) ^^ (refa ainh finEnv) ^^ (refa ainh gathInFin) ^^ (refa asyn outcome) ^^ = terminator \end{code} \end{smallcode} %if False \begin{smallcode} \begin{code} Tp Source ^^^ = ^^^ Tpv Source analyze Tpv Source analyze ^^^ = ^^^ Sigma Env (\(refa asyn gathEnv) -> (Tpv Source translate) (refa asyn gathEnv)) Tpv Source translate ^^^ (refa asyn gathEnv) ^^^ = ((refa ainh finEnv) : Env) -> ((refa ainh gathInFin) : (refa asyn gathEnv) `subseq` (refa ainh finEnv)) -> Sigma (Errs (refa ainh finEnv) `Either` Target (refa ainh finEnv)) (\(refa asyn outcome) -> (Tpv Source terminator) (refa asyn gathEnv) (refa ainh finEnv) (refa ainh gathInFin) (refa asyn outcome)) Tpv Source terminator ^^^ (refa asyn gathEnv) ^^^ (refa ainh finEnv) ^^^ (refa ainh gathInFin) ^^^ (refa asyn outcome) ^^^ = terminator \end{code} \end{smallcode} %endif %if False \begin{smallcode} \begin{code} Tpv Source terminator (refa asyn gathEnv) (refa ainh finEnv) (refa ainh gathInFin) (refa asyn outcome) = terminator -- terminator Tpv Source translate (refa asyn gathEnv) = -- type for last visit ((refa ainh finEnv) : Env) -> ((refa ainh gathInFin) : (refa asyn gathEnv) `subseq` (refa ainh finEnv)) -> -- inh attrs Sigma (Errs (refa ainh finEnv) `Either` Target (refa ainh finEnv)) ((\(refa asyn outcome) -> -- syns prod (Tpv Source terminator) (refa asyn gathEnv) (refa ainh finEnv) (refa ainh gathInFin) (refa asyn outcome))) -- next vis Tpv Source analyze = Sigma Source (\(refa asyn gathEnv) -> (Tpv Source translate) (refa asyn gathEnv)) Tp Source = Tpv Source analyze -- type for coroutine: type of the first visit \end{code} \end{smallcode} %endif The restrictions on attribute order in the interface ensure that referenced attributes are in scope. %if thesis This representation can be optimized a bit by passing only on those attributes that are referenced in the remainder. %endif The scheme for |semiv v g I tau| formalizes this translation, where |g| is the list of preceding attribute declarations, and |tau| the type for |I|. The |typrod| function mentioned in the scheme constructs a right-nested dependent product. The coroutine itself consists of nested continuation functions (one for each visit). Each continuation takes the visit's inherited attributes as parameter, and consists of a tree of with-constructs that represent intermediate computations for computations of attributes and invocations of visits to children. Each leaf ends in a dependent product of the visit's synthesized attributes and the continuation function for the next visit\footnote{ As a technical detail, a leaf of the with-tree may also be an \emph{absurd pattern}. These are used in Agda to indicate an alternative that is never satisfiable. A body for such an alternative cannot be given. }. \begin{smallcode} \begin{code} semprod_seq : Tp Source -> Tp Source -> Tp Source -- example translation for |`diam`| semprod_seq (refc loc left) (refc loc right) = refv lhs analyze awhere -- delegates to first visit function (refv lhs analyze) : Tpv Source analyze -- signature of first visit function (refv lhs analyze) with ... -- computations for |analyze| here ... = (refs lhs gathEnv, refv lhs translate) ahwere -- result of first visit function (refv lhs translate) : Tpv Source translate (refs lhs gathEnv) -- last visit function (refv lhs translate) (refi lhs finEnv) (refi lhs gathInFin) with ... -- computations for |translate| here ... = (refs lhs outcome, refv lhs terminator) awhere -- result of second visit function (refv lhs terminator) : Tpv Source terminator (refs lhs gathEnv) (refi lhs finEnv) (refi lhs gathInFin) (refs lhs outcome) (refv lhs terminator) = terminator -- explicit terminator value \end{code} \end{smallcode} The scheme |(semev v (I) (many e, many g))| formalizes this translation for a visit |v| of interface |I|, where |many e| are type arguments to the interface (empty in the example), and |many g| are the attributes of previous visits. The with-tree for a visit-function consists of the translation of child-rules, invoke-rules and evaluation rules. Each rule plugs into this tree. For example, the translation for |(semb (child left : Source = (refs loc left)))| is: \begin{code} ... with (refs loc left) -- evaluate RHS to get first visit fun ... | (refv left analyze) with ... -- give it a name + proceed with remainder \end{code} For |(semb (invoke translate of left))| the translation is: \begin{code} ... with (refv left translate) (refi left finEnv) (refi left gathInFin) -- visit fun takes inh attrs ... | ((refs left outcome), (refv left sentinel)) with ... -- returns product of syn attrs \end{code} For |(semb (lhs.gathEnv = left.gathEnv ++ right.gathEnv))|: \begin{code} ... with (refs left gathEnv) ++ (refs right gathEnv) -- translation for RHS ... | (refs lhs gathEnv) with ... -- LHS + remainder \end{code} For |(semb (lhs.outcome with ...))| (where the RHS is a with-construct), we duplicate the remaining with-tree for each alternative of the RHS: \begin{code} ... with (refs left outcome) -- translation for RHS ... | inj1 es with (refs right outcome) ... | inj1 es1 | inj1 es2 with inj1 (es1 ++ es2) -- alternative one of four ... | inj1 es1 | inj1 es | (refs lhs outcome) with ... -- LHS + remainder ... | inj1 es1 | inj2 _ with inj1 es1 -- alternative two of four ... | inj1 es1 | inj2 _ | (refs lhs outcome) with ... -- LHS + remainder ... | inj2 ... -- remaining two alternatives \end{code} The scheme |(semr r k)| formalizes this translation, where |r| is a rule and |k| the translation of the rules that follow |r|. The size of the translated code may be exponential in the number of rules with with-constructs as RHS. %if False This is not bad, it may just encourage uses to break encapsulation. %endif It is not obvious how to treat such rules otherwise. Agda does not allow a with-construct as a subexpression. Neither can we easily factor out the RHS of a rule to a separate function, because the conclusions drawn from the evaluation of preceding rules are not in scope of this function. Fortunately, for rules that would otherwise cause a lot of needless duplication, the programmer can perform this process manually. When dependent pattern matching brings assumptions in scope that are needed \emph{across} rules, the code duplication is a necessity. To facilitate that pattern matching effects are visible across rules, we need to ensure that the rule that performs the match is ordered before a rule that needs the assumption. Chapter~\tref{chapt.side-effect} shows how such non-attribute dependencies can be captured. The translated code has attractive operational properties. Each attribute is only computed once, and each node is at most traversed |k| times. \section{Partially Defined Attributes} \label{depend.sect.partial} A fine granularity of attributes is important to use an AG effectively. In the mini-compiler of Section~\ref{depend.section.example}, we could replace the attribute |outcome| with an attribute |code| and a separate attribute |errors|. This would be more convenient, since it would not require a pattern match against the |output| attribute to collect errors. %if thesis This is convenient in general, as a finer granularity of attributes gives more opportunities to use default rules. %endif However, we cannot produce a target term in the presence of errors, thus |code| would not have a total definition. Therefore, we were forced to combine these two aspects into a single attribute |outcome|. It is common to use partially defined attributes in an AG. This holds especially when the attribute's value (e.g. |errors|) determines if another attribute is defined (e.g. |code|). We present a solution that uses the partitioning of attributes over visits. The idea is to make the availability of visits dependent on the value of a preceding attribute. We split up the |translate| visit in a visit |report| and a visit |generate|. The visit |report| has |errors| as synthesized attribute, and |generate| has |code|. Furthermore, we enforce that |generate| may only be invoked (by the parent in the AST) when the list of errors reported in the previous visit is empty. We accomplish this with an additional attribute |noErrors| on |generate| that gives evidence that the list of errors is empty. With this evidence, we can give a total definition for |code|. \begin{smallcode} \begin{code} itf Source -- |Root|'s visit needs to be split up in a similar way visit report ^^^ syn errors : Errs ainh.finEnv -- parent can inspect |errors| visit generate ^^^ inh noErrors : asyn.errors == [] -- enforces invariant syn code : Target ainh.finEnv -- only when |errors| is empty datasem Source prod use -- example for production |use| loc.testInEnv = loc.nm `mbElem` lhs.finEnv -- scheduled in visit |report| lhs.code with loc.testIn | lhs.noErrors -- scheduled in visit |generate| | inj1 _ | () -- cannot happen, hence an \emph{absurd pattern} | inj2 isIn | refl = use loc.nm isIn -- extract the evidence needed for the |code| term datasem Source prod `diam` -- |leftNil : (alpha : Env) -> (beta : Env) -> (alpha ++ beta == []) -> (alpha == [])| left.noErrors = leftNil left.errors right.errors lhs.noErrors -- |right.noErrors| similar lhs.code = left.code `diam` right.code -- scheduled in visit |generate| \end{code} \end{smallcode} For this approach to work, it is essential that visits are scheduled as late as possible, and only those that are needed. %if thesis Another application of the above idea is related to proofs for special cases, i.e. when we want to prove that with additional assumptions on inherited attributes, the synthesized attributes meet additional criteria. These assumptions are modeled as additional inherited attributes. However, since we are required to pass values for inherited attributes, our AG would only work for these special cases. For example, suppose that we want to prove that an AG for a type inferencer is complete. To do so, we give a typing derivation as input, and require a proof that the inferred type is more general than the type of the typing derivation. To infer a type, we do not want to provide a typing derivation, and in the proof, we do not want that the typing derivation would be defined in terms of the typing derivation. The typing derivation assumption is thus partially defined: only needed for the proof. Hence, we define the attributes for the proof in a separate visit. \begin{code} itf Expr visit infer ^^^ inh env : Env ^^^ syn self : Expr ^^^ syn errs : Errs visit typed ^^^ inh prv1 : asyn.errs == [] ^^^ syn tau : Ty visit proof -- special visit for proof inh tau' : Ty inh deriv : ainh.env :- asyn.self : ainh.tau' -- description of typing derivation. syn prv2 : asyn.tau <= ainh.tau' \end{code} %endif We can generalize the presented approach %if thesis (Section~\ref{depend.sect.depnontermattr}) %endif by defining a fixed number of alternative sets of attributes for a visit, and use the value of a preceding attribute to select one of these sets~\citep{middelkoop09wgt10}. \section{Related Work} Dependent types originate in Martin-L\"of's Type Theory. Several dependently-typed programming languages increasingly gain popularity, %if thesis including the languages Agda~\citep{DBLP:conf/tldi/Norell09}, Epigram~\citep{DBLP:conf/afp/McBride04}, and Coq~\citep{DBLP:conf/tphol/Bertot08}. %else including Agda~\citep{DBLP:conf/tldi/Norell09}, Epigram, and Coq. %endif We present the ideas in \thiswork{} with Agda as host language, because it has a concept of a dependent pattern match, to which we straightforwardly map the left-hand sides of AG rules. Also, in Coq and Epigram, a program is written via interactive theorem proving with tactics or commands. The preprocessor-based approach of \thiswork{}, however, suits a declarative approach more. Attribute grammars~\citep{DBLP:journals/mst/Knuth68} are considered to be a promising implementation for compiler construction. Recently, many Attribute Grammar systems arose for mainstream languages, such as the systems %if thesis {JastAdd}~\citep{DBLP:conf/oopsla/EkmanH07} and {Silver}~\citep{DBLP:journals/entcs/WykBGK08} %else JastAdd and Silver %endif for Java, and UUAG~\citep{uuagc} for Haskell. These approaches may benefit from the stronger type discipline as presented in \thiswork{}; however, it would require an encoding of dependent types in the host language. %if thesis In languages languages with meta-programming facilities, it is sometimes possible to implement AGs without the need of a preprocessor. \textualcite{Viera, et al.}{DBLP:conf/icfp/VieraSS09} show how to implement AGs into Haskell via type level programming. Each rule exposes in its type the attributes that it needs and the attributes that it defines. The rules can be composed via combinators. At one place in the program, the knit point, a proof is constructed that the set of used attributes equals the defined attributes. This proof is subsequently mapped to a semantic function. A combination of that paper with our work, would fit well in Agda, if Agda had a mechanism similar to Haskell's class system. Alternatively, it may be possible to embed first-class AGs in Agda, while using a preprocessor to generate boilerplate code. %endif AGs have a straightforward translation to cyclic functions in a lazy functional programming language~\citep{DBLP:conf/ifip2-4/SwierstraA98}. To prove that cyclic functions are total and terminating is a non-trivial exercise. Kastens~\citep{DBLP:journals/acta/Kastens80} presented Ordered Attribute Grammars (OAGs). In OAGs, the evaluation order of attribute computations as well as attribute lifetime can be determined statically. Saraiva~\citep{Saraiva99} described how to generate (noncyclic) functional coroutines from OAGs. The coroutines we generate are based on these ideas. %if False Boyland~\citep{DBLP:journals/toplas/Boyland96} introduced conditional attribute grammars. In such a grammar, semantic rules may be guarded. A rule may only be evaluated if its guard holds. Evaluation of guards can influence the evaluation order, which makes the evaluation less predictable. In comparison, in our clauses-in-visits model, we have to explicitly indicate in what visits guards are evaluated (the match-statements of a clause), which makes evaluation clear. Our approach has the additional benefit that children may be conditionally introduced and visited. %endif %if False The work for \thiswork{} is carried out for a research project to support the implementation of the type inference component of the Utrecht Haskell compiler. We presented an earlier version of RulerCore's clauses-per-visit model to allow attribute grammars with case distinction on more than a single AST, and express iteration and dynamic growing of trees~\citep{Middelkoop10vis,Middelkoop10wgt,Middelkoop10gpce}. %endif \section{Conclusion} \label{depend.sect.conclusion} We presented |rulerfrontagda|, a language for ordered AGs with dependently typed attributes: the type of an attribute may refer to the value of another attribute. This feature allows us to conveniently encode invariants in the type of attributes, and pass proofs of these invariants around as attributes. With a dependently typed AG, we write algebras for catamorphisms in a dependently typed language in a composable way. Each attribute describes a separate aspect of the catamorphism. %if thesis A particular advantage of composability is that attributes can easily be added and shared. Moreover, via \emph{local attributes} we can specify invariants and proofs at those places where the data is. We prove for the example in Section~\ref{depend.section.example} that the final environment must be equal to the gathered environment at the root of the tree: \begin{code} datasem Root prod root -- more rules for the root production loc.eqEnvs : inh.top.finEnv == syn.top.gathEnv -- signature for local attr loc.eqEnvs = refl -- proof of the equality \end{code} %endif The approach we presented is lightweight, which means that we encode AGs as an embedded language (via a preprocessor), such that type checking is deferred to the host language. To facilitate termination checking, we translate the AG to a coroutine (Section~\ref{depend.sect.translation.agda}) that encodes a terminating, multi-visit traversal, under the restriction that the AG is ordered and definitions for attributes are total. The preprocessor approach fits nicely with the interactive Emacs mode of Agda. Type errors in the generated program are traceable back to the source: in a statically checked |rulerfrontagda| program these can only occur in Agda blocks. These Agda blocks are literally preserved; due to unicode, even attribute references can stay the same. Also, the Emacs mode implements interactive features via markers, which are also preserved by the translation. The AG preprocessor is merely an additional preprocessing step. %if thesis Not all features integrate seamlessly, however. Syntactical errors in Agda blocks, such as an omitted closing parenthesis, may only be discovered during parsing of the generated code surrounding the block. This can be remedied by validating the syntax of Agda blocks during the preprocessing. A complication arises because the code of rules may occur multiple times in the generated code. Also, the case splitting feature causes the generated program to be transformed, such that it scrutinizes on a variable chosen by the programmer. The additional equations generated by case splitting need to be transformed back to rules with a with-construct. Fortunately, these are not fundamental problems. %endif With some generalizations, the work we have presented is a proposal for a more flexible termination checker for Agda that accepts |k|-orderable cyclic functions, if the function can be written as a non-cyclic |k|-visit coroutine. %% (i.e. at call sites, an input may depend on an output) %if thesis As future work, it may be possible to exploit patterns in AG descriptions to generate boilerplate for proofs. For example, we can generate boilerplate code to express termination and monotonicity properties of fixpoint iteration in AGs (Chapter~\tref{chapt.iterative}), and generate boilerplate code for standard environment lookup and extension patterns. Also, it may be possible to generate proof and AG templates from a type system specification~\citep{DBLP:conf/flops/DijkstraS06}. %endif %if thesis \begin{subappendices} \section{Implementation of the Support Code} \label{depend.sect.support} In this section, we give a definition of the support code mentioned briefly in Section~\ref{depend.section.example}. This section also serves to give a bit more background information about Agda's syntax. In a dependently typed language, the interpretation of an algebraic data type in an intuitionistic logic is a relation between the type parameters of the data type. A data constructor is an axiom for the relation. A type is a theorem; a value of that type is a proof that the theorem holds. We defined the following data types and data constructors to work with proofs for environments. We use the |_elem| data type to prove that an identifier is in the environment, and |_subseq| to prove that an environment occurs as substring in an environment. \begin{code} adata _elem : Ident -> Env -> Set awhere -- member of environment here : {nm : Ident} {Gamma : Env} -> nm `elem` (nm :: Gamma) next : {nm1 : Ident} {nm2 : Ident} {Gamma : Env} -> nm1 `elem` Gamma -> nm1 `elem` (nm2 :: Gamma) adata _subseq : Env -> Env -> Set awhere -- substring of environment subLeft : {Gamma1 : Env} {Gamma2 : Env} -> Gamma1 `subseq` (Gamma1 ++ Gamma2) subRight : {Gamma1 : Env} {Gamma2 : Env} -> Gamma2 `subseq` (Gamma1 ++ Gamma2) trans : {Gamma1 : Env} {Gamma2 : Env} {Gamma3 : Env} -> Gamma1 `subseq` Gamma2 -> Gamma2 `subseq` Gamma3 -> Gamma1 `subseq` Gamma3 \end{code} A membership proof for an identifier in the environment states that either the identifier is at the head of the environment, or there is a proof that it is in the tail of the environment. The substring-proof gives prefixes and suffixes to the encapsulated environment that together give the encapsulating environment. Note the use of curly braces here. These represent implicit parameters, which are denoted with similar syntax as implicit parameters for Haskell. An argument for an implicit parameter may be omitted if it can be derived from the context via unifications. The arrow type constructor can be interpreted as the logical implication. The parameters of a function are assumptions, and the return type is the conclusion. A function thus takes proofs for these assumption as parameter, and transforms these into a proof for the result. The following functions operate on proofs of the above types. When an identifier exists in an environment, then |append| proves that it also exists in a suffixed version of that environment. Similarly, |prefix| gives a prove for a prefixed environment. Function |inSubset| uses these two to prove that when an identifier occurs in a substring of an environment, it also occurs in the environment itself. \begin{code} append : {nm : Ident} {Gamma : Env} -> (nm `elem` Gamma) -> (Gamma' : Env) -> (nm `elem` (Gamma ++ Gamma')) append {nm} {.nm :: Gamma} (here) Gamma' = here {nm} {Gamma ++ Gamma'} append {nm} {nm' :: Gamma} (next inGamma) Gamma' = next (append {nm} {Gamma} inGamma Gamma') append {_} {[]} () _ prefix : {nm : Ident} {Gamma' : Env} -> (nm `elem` Gamma') -> (Gamma : Env) -> (nm `elem` (Gamma ++ Gamma')) prefix inGamma' [] = inGamma' prefix inGamma' (x :: Gamma) = next (prefix inGamma' Gamma) inSubset : {nm : Ident} {Gamma : Env} {Gamma' : Env} -> (Gamma' `subseq` Gamma) -> nm `elem` Gamma' -> nm `elem` Gamma inSubset (subLeft {_} {Gamma'}) inGamma' = append inGamma' Gamma' inSubset (subRight {Gamma}) inGamma' = prefix inGamma' Gamma inSubset (trans subL subR) inGamma' = inSubset subR (inSubset subL inGamma') \end{code} In case of |append|, the environment cannot be empty when we have a proof than an identifier occurs in it. However, to satisfy the totality checker, we are required to give a function definition for this case. Since a match against such a pattern cannot succeed, the match is called absurd, and no function body has to be given. The operator |`mbElem`| takes an identifier |nm| and an environment |Gamma|, and either gives a prove that the identifier is in the environment, or gives a proof that it is not in the environment. The sum type |_`Either`_| (named |Either| in Haskell) provides constructors |inj1| (|Left| in Haskell) and |inj2| (|Right| in Haskell) for this purpose. For the definition of |`mbElem`|, we use function |notFirst| to prove by contradiction that if an identifier does not occur in the tail of the environment, and is also not equal to the head of the environment, that it is neither in the whole environment. \begin{code} notFirst : {nm : Ident} {nm' : Ident} {Gamma : Env} -> neg (nm == nm') -> neg (nm' `elem` Gamma) -> neg (nm' `elem` (nm :: Gamma)) notFirst prv1 _ = \here -> prv2 refl notFirst _ prv1 = \(next prv2) -> prv1 prv2 \end{code} Negation of a type (neg tau) is defined as a function |tau -> bottom|. The type |bottom| (falsum) does not have any data constructors, so we cannot construct it explicitly, but can match against it with an absurd pattern. If we can derive its value, we proved a contradiction between the assumptions we made. \begin{code} _mbElem : (nm : Ident) -> (Gamma : Env) -> neg (nm `elem` Gamma) `Either` (nm `elem` Gamma) nm' `mbElem` [] = inj1 \() nm' `mbElem` (nm :: Gamma) with nm `mbEqual` nm' nm' `mbElem` (.nm' :: Gamma) | yes refl = inj2 here nm' `mbElem` (nm :: Gamma) | no prv' with nm' `mbElem` Gamma nm' `mbElem` (nm :: Gamma) | no prv' | inj2 prv = inj2 (next {nm'} {nm} prv) nm' `mbElem` (nm :: Gamma) | no prv' | inj1 prv = inj1 (notFirst prv' prv) \end{code} When the environment is empty, the identifier is not in the environment. We thus use |inj1| and need to construct a negation. This is a function, with an absurd pattern as first parameter, since none of the data constructors of |_elem| can be applied. The other cases apply when the environment is not empty. Also note that patterns in Agda must be strictly linear: there may only be one introduction of an identifier. If there are multiple locations, the identifier must be prefixed with a dot. In Section~\ref{depend.sect.partial}, we used the helper function |leftNil|. It is implemented by case distinction on its first argument. When |alpha| is empty, the requested property trivially holds. When |alpha| is not empty, normalization of |alpha ++ beta| gives another constructor than |[]|, hence the absurd pattern. \begin{code} leftNil : (alpha : Env) -> (beta : Env) -> (alpha ++ beta == []) -> (alpha == []) leftNil [] _ refl = refl leftNil (_ :: _) _ () \end{code} \subsection{Absurd Rules} \label{depend.sect.absurdrules} There may be productions for which no semantics for a given interface exists. For example, consider a grammar for a statically sized bit array. \begin{code} grammar BitArray : Nat -> Set -- statically sized bit array prod nil : BitArray 0 -- empty bit array prod cons : BitArray (suc n) -- non-empty bit array term0 n : Nat -- length of the tail term hd : Bool -- bit at the head of the array nonterm tl : BitArray n -- tail of the bit array \end{code} We declare a synthesized attribute |head| that stands for the head bit of the array. We can extract this bit when the array is not empty. Hence, we state this requirement as inherited attribute. \begin{code} itf BitArray n visit extract -- Interface to extract the head inh prf : n > 0 -- Proofs that the array is not empty syn head : Bool -- Must return the head bit \end{code} If the array is empty, then we cannot give a value for |lhs.head|. Fortunately, the proof helps us out. If the array would be empty, then we would not be able to give the proof. Indeed, we can match with an absurd pattern against the proof, so that we do not have to give a definition for |lhs.head|. \begin{code} datasem BitArray prod nil ^^^ lhs.head with lhs.prf -- would be proof of |suc 0 <= 0| ^^^ ^^^ | () -- not inhabited prod cons ^^^ lhs.head = loc.hd -- trivial \end{code} Under these conditions, a semantics for |nil| cannot be given. When the interface has multiple attributes, or even multiple visits, then the above code would have to be duplicated for each synthesized attribute of the production, and each inherited attribute of the children. To prevent such code duplication, we introduce an absurd-rule. Its LHS |p| must be an absurd pattern that matches against the outcome of the RHS |e|. \begin{code} r ::= ^^^ absurd ^^^ p = e -- absurd rule (with absurd |p|) \end{code} For example, we can use it to match against |lhs.prf| in the |nil| production. \begin{code} datasem BitArray prod nil absurd ^^^ () = lhs.prf -- would be proof of |suc 0 <= 0| \end{code} Attribute definitions and child declarations must be omitted if these would appear later than the absurd-rule in the rule order. The translation is relatively straight-forward. \begin{code} (semr (absurd p = e) k) ^^^^ ~> ^^^^ with e ^^^ ... | (semb p) -- ends the current with-branch \end{code} Since each with-branch ends in an absurd pattern, the continuation |k| is not needed. Since the follow-up rules on an absurd rule are not generated, we also demand that these are not specified in the first place. These absurd-rules have consequences for the rule scheduling algorithm. We want the absurd-rules to be scheduled early, such that we can omit the rules that would follow. Also, we want their scheduling to be predictable, such that we know which rules we can and must omit. The scheduling algorithm consists of a number of phases. \begin{itemize} \item In the first phase, attributes are scheduled to visits of the interface. We assume that this step is performed manually, although it can be automated to a large extend, as is implemented in UUAGC~\citep{uuagc}. \item In the remaining phases, we can deal with each productions independently. For each production we construct a DAG that captures the dependencies between rules (Chapter~\tref{chapt.side-effect}). In this DAG, we identify the (indirect) predecessors of absurd-rules. These predecessors, combined with the absurd-rules, we schedule as early as possible. The partial order imposed by the DAG is turned into a total order by giving precedence first to absurd-rules, then evaluation rules, invoke rules, and finally child rules. \item In the final phase, we schedule the remaining rules as late as possible. Superfluous rules end up in the terminator visit. \end{itemize} If the DAG is non-cyclic, this algorithm properly schedules the rules. The DAG models the def/use dependencies of the rules. Each subsequent pass preserves these dependencies. Thus, the algorithm is sound. Also, if an absurd-rule |r1| could be scheduled earlier than a non-absurd rule |r2|, then |r2| is not a predecessor of |r1|. However, then |r1| would have been scheduled earlier as absurd-rules take precedence. An absurd-rule thus forces the attributes its RHS refers to, to be scheduled as early as possible. It preferably does not have too complex dependencies (i.e. transitively speaking, only dependencies on inherited attributes and local attributes), so that it is clear when it is scheduled. \section{Dependent Nonterminal Attribution} \label{depend.sect.depnontermattr} In Section~\ref{depend.sect.partial}, we showed how to deal with an attribute |p| that is only defined when another attribute |q| has a particular value |v|. The trick is to move |p| to a later visit than |q|, and add the invariant to |p|'s visit that requires that it can only be invoked when |q| equals |v|. This invariant is expressed as additional attribute, which can then also be used in the definition of |p|. This is an example of a dependent attribution of nonterminals: depending on the value of |q|, the remaining attributes were either all present, or none were present. This approach can be generalized to allow a fixed number of different sets of attributes depending on the value of preceding attributes. The responsibility for choosing a set of attributes can be given to the caller or the callee. The callee is the node that is a child of the caller. We divide responsibilities as follows. The caller invokes a visit on the callee, and is responsible for selecting one of the alternative interfaces that are offered by the callee. The callee is required to produce results for that choice. The callee can encode restrictions on the available choices for the parent as inherited attributes. The caller must provide values for the inherited attributes of the alternative interface it chooses. With this choice, both the caller and callee can impose demands. The caller imposes these demands by choosing an interface of the callee, and the callee imposes these demands through inherited attributes. We change the syntax of interfaces to cater for \emph{contexts}. A visit consists of a set of explicitly named contexts |(many z)|. \begin{code} i ::= itf I (many x) : tau v -- with first visit |v|, params |x|, and signature |tau| v ::= visit x (many z) -- visit declaration with a set of contexts (many z) z ::= context x inh (many a) syn (many a) v -- context |x| for a visit \end{code} Notationally, layout becomes important. The contexts |many z| must have the same indentation, and visits and contexts occurring inside a context must have a deeper indentation. As syntactic sugar, we assume that the context-keyword and name may be omitted if there is only one context for a visit. The syntax for the \emph{terminator} visit is not needed anymore. It can be modeled as a visit with zero contexts. The names of contexts must be unique per interface. It allows us to distinguish contexts of different visits from each other, which is needed in |rulerfrontagda| because of its syntactical conveniences. For example, we define two contexts for the |generate| visit of the earlier example. The context |errorfree| contains the |code| attribute, but it may only be invoked when errors are absent. The context |haserrors| provides a |pretty| attribute with a pretty print of the program. It does not pose restrictions on the |errors| attribute. \begin{code} itf Source visit report ^^^ syn errors : Errs ainh.finEnv visit generate -- a visit may consist of one or more contexts context errorfree -- a context has a name inh noErrors : asyn.errors == [] syn code : Target ainh.finEnv context haserrors -- a context may also contain subsequent visits syn pretty : Doc \end{code} The callee must provide rules for each context. We split a semantics-block |t| for a visit up into a context |u| for each declared context of that visit in the corresponding interface. Such a context defines the next visit. For visits with more than one context, the caller must explicitly invoke them by means of an invoke rule. \begin{code} t ::= visit x (many u) -- visit definition, with next visit |t| u ::= context x (many r) t -- context with next visit |t| r ::= invoke x1 of c context x2 -- modified invoke rule \end{code} Similarly to the notational conveniences above, we allow the context-keyword and name to be omitted if there is only one context declared for a visit. For example, for production |`diam`|, we choose contexts of the children depending on the context the visit itself is in. In this example, the context for the child is the same as the context of the parent. This is not a requirement. \begin{code} datasem Source prod `diam` lhs.errors = left.errors ++ right.errors -- collect errors context errorfree -- rules exclusive for |errorfree| invoke generate of left context errorfree -- explicit invoke invoke generate of right context errorfree -- explicit invoke left.noErrors = leftNil left.errors right.errors lhs.noErrors left.noErrors = rightNil left.errors right.errors lhs.noErrors lhs.code = left.code `diam` right.code context haserrors -- rules exclusive for |haserrors| invoke generate of left context haserrors -- explicit invoke invoke generate of right context haserrors -- explicit invoke lhs.pretty = left.pretty <+> right.pretty -- collect pretty print \end{code} Ultimately, the choice for the context is made at the root. Either we make this choice external to the AG in terms of the generated coroutine, or use another AG extension~\citep{Middelkoop10gpce}: \emph{clauses}. A context may be split further into clauses. A clause may contain special match-rules, which may contain failing pattern matches. When a pattern match fails, execution backtracks to the next clause. The clauses are a means of case distinction on multiple rules at once. This is needed, in order to use different invoke-rules, depending on the values of an attribute. \begin{code} itf Root visit compile ^^^ syn outcome : (Errs asyn.finEnv) `Either` (Target asyn.finEnv) datasem Root prod root -- some rules omitted visit compile -- clauses of visit/context clause emptyerrors -- linear sequence of clauses match [] = top.errors -- possibly failing test top.noErrors = refl -- if match succeeds invoke generate of top context errorfree -- take |errorfree| visit lhs.outcome = inj2 top.code clause nonemptyerrors -- |neg ([] == top.errors)| invoke generate of top context haserrors -- take |haserrors| visit lhs.outcome = inj1 top.errors \end{code} Clauses and match rules are confined to the visit/context they are defined in. The clauses must be exhaustive. Within these constraints, match-rules can be scheduled as usual. Match-rules are also scheduled as early as possible, similarly to absurd-rules (Section~\ref{depend.sect.absurdrules}). There is a good reason to do so: we typically do not have explicit dependencies on a match rule, and its in general better to distinguish cases as soon as possible. In the |rulercoreagda| translation, the visit function that corresponds to a visit has a parameter for each attribute of that visit. For the translation of contexts we give an additional, initial parameter to such a visit function. The value is a \emph{handle}~\citep{Middelkoop10vis}: it describes what context we want, and what the type of that context is supposed to be. The handle can be considered a typed version of the control parameter in \citet{DBLP:conf/popl/KennedyW76}. For example, for visit |generate|, there are two contexts, |errorfree| and |haserrors| respectively. For each context, we generate a type that specifies the types of the attributes (as described earlier): \begin{code} Tpv Source errorfree ... Tpv Source haserrors ... \end{code} Each constructor of the handle-type is indexed by one of these context types: \begin{smallcode} \begin{code} data Tph Source generate : ((refs lhs gathEnv) : Env) -> ((refs lhs errors) : Errs (refs lhs gathEnv)) -> Set -> Set where errorfree : forall {(refs lhs gathEnv)} {(refs lhs errors)} -> (Tph Source translate) (refs lhs gathEnv) (refs lhs errors) ((Tpv Source errorfree (refs lhs gathEnv) (refs lhs errors))) haserrors : forall {(refs lhs gathEnv)} {(refs lhs errors)} -> (Tph Source translate) (refs lhs gathEnv) (refs lhs errors) ((Tpv Source haserrors (refs lhs gathEnv) (refs lhs errors))) \end{code} \end{smallcode} The visit function takes such a handle (|H'Generate beta|) and returns |beta|. The caller thus knows what |beta| is, and the callee can find this out by pattern matching against the data constructors. The actual type of the visit function, and its implementation becomes: \begin{smallcode} \begin{code} Tpv Source generate (refa asyn gathEnv) (refa asyn errors) = forall {beta} -> Tph Source (refa asyn gathEnv) (refa asyn errors) generate beta -> beta (refv lhs generate) : Tpv Source generate (refs lhs gathEnv) (refs lhs errors) (refv lhs generate) errorfree = ... -- translation for |errorfree| (refv lhs generate) haserrors = ... -- translation for |haserrors| \end{code} \end{smallcode} The types in question seem rather complex, although this is mainly plumbing to pass attributes around on the type level. Fortunately, AGs alleviate us from writing such code by hand. The presented mechanism opens up the possibility to have non-linear visit sequences. It also allows us to express interfaces for the ordered AGs as presented by \citet{DBLP:conf/popl/KennedyW76}. Each context can represent an operation or query to be performed on the AST. For example, we could define an interface on the AST of types, such that one context computes the free variables, and another one applies a substitution to the type. The presented approach only permits branching. However, it may be possible to generalize the approach further and allow branches to merge and loop. Merging of branches could be of use for proofs of special cases that span multiple visits (Section~\ref{depend.sect.partial}). Also, the interfaces can be seen as \emph{session types} for coroutines. %% Would like to cite the coroutine-package on Hackage here. \section{Ideas Transferrable to AG Systems for Haskell} Some of the above ideas carry over to AG systems for Haskell, such as UUAG~\citep{uuagc}. In a dependently typed AG, attributes can represent both values and types. In Haskell, there is a clear distinction between values and types. In an AG for Haskell, we can make an explicit distinction between attributes that represent types (and have a \emph{kind} as type), and attributes that represent values. The type of a type attribute may not refer to other attributes. The type of a value attribute, however, may refer to a type attribute. Type attributes correspond to quantification. An inherited type attribute corresponds to universal quantification, since the caller can choose its instantiation. A synthesized type attribute corresponds to existential quantification. The callee can choose its type, but the caller cannot make an assumption about it. This mechanism allows us to deal with polymorphism in interfaces. Currently, UUAG only supports kind star data types. We showed how to deal with parameterized data types, and GADT-style data constructors. These extensions allow AGs to be written for data types with a stronger typing discipline. Also, we can deal with class constraints in constructors by introducing explicit wrappers for dictionaries that we can store as additional fields, e.g.: \begin{code} data DictEq :: * -> * where DictEq :: Eq a => DictEq a \end{code} With such extensions, we can handle even non-regular data types, as long as nonterminals have an outermost type construct described by a grammar declaration. The handles of Appendix~\ref{depend.sect.depnontermattr} are conventional GADTs, hence the context-idea can be implemented in Haskell. %% What about dependent types themselves? %% Although dependent types can be emulated in Haskell, it is unlikely that dependent AGs %% are useful in this area, since the typing of dependent types is a host-language issue. %% Map compiler implementation (type rules?) to both Haskell code (without dependent types), and Agda %% code with many postulates. Problem: there is no good erasure to Haskell. Unless we describe type rules %% at a higher abstraction level. \end{subappendices} %endif