Module Parser.Grammar

Notation

Each rule in the grammar S returns a value of type S.t, which is a semantic action that will eventually build a Core Theory term of a corresponding to the rule type. This type is abstract and is totally co-inductive (i.e., it could also produced, there are no grammar rules (functions) that consume values of this type.

Since each grammar rule will eventually build a Core Theory term, we will describe rules using the Core Theory denotations. The parser generator will invoke recursively the top-level rules on each non-terminal. Those rules are referenced using the following names:

• bitv - parses the language of bitvectors;
• bool - parses the language of booleans;
• mem - parses the language of memories;
• stmt - parses the language of statements;
• float - parses the language of floats;
• rmode - parses the language of rounding modes.

The parsing rules occasionally need to refer to the sorts of therms, we use the following short-hand notation for sorts:

• bits m = Bitv.define m - a sort of bitvectors with m bits;
• Bool.t - the sort of booleans;
• mems k v = Mem.define k v - a sort of memories;

Finally, the width associated with the sort s is denoted with size s = Bitv.size s.

Example,

(** [add x y] is [add (bitv x) (bitv y)].  *)
val add : exp -> exp -> t

says that the grammar rule add interprets its arguments in the bitv context (recursively calls the bitv function) and have the denotation of the add p q term of the Core Theory, where p = bitv x and q = bitv y.

Contexts

To ensure the freshness of generated variables and to enable a higher-order abstract syntax style (a generalization of the De Bruijn notation) we wrap each semantic action in a context that holds the binding rules.

The var family of grammar rules rename the passed names if they are bound in the renaming context, which is denoted with context s which is a function that returns the name bound to s in the context or s if it is unbound.

The let_<T> n ... and tmp_<T> n ... take the old name n, create a fresh variable n' and append the n,n' binding to the context in which the grammar rule is invoked, denoted with rule [<non-term>|n->n'], e.g.,

[let_reg s x y] is [scoped @@ fun v -> (bitv x) (bitv [y|s->v])]

As a result of the let_reg rule applications any free occurrence of the variable s will be substituted with the freshly generated variable v. This will ensure alpha-equivalence of expressions that use the let_<T> forms.

The tmp_<T> rules are basically the same as let_<T> except that the scope of the freshly created variable is indefinite, so these forms could be used to create hygienic symbol generators.