To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
An untyped grammar for a subset of Core Theory languages.
This module defines grammars for six sub-languages for each sort of Core Theory terms.
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
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.
(** [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.
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.
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.
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
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.
type ieee754 = IEEE754.parameters
module type Bitv = sig ... end
module type Bool = sig ... end
module type Mem = sig ... end
module type Stmt = sig ... end
module type Float = sig ... end
Floating point expressions.
module type Rmode = sig ... end