package menhirCST
Library
Module
Module type
Parameter
Class
Class type
The module DCST
offers an abstract data type dcst
of disjunctive concrete syntax trees. This definition is generic, that is, grammar-independent. This module offers an unsafe API: the smart constructors nonterminal
and choice
have preconditions whose validity is not tested at runtime. A safe, non-generic API can be constructed a posteriori on top of this unsafe, generic API.
A disjunctive concrete syntax tree (DCST) is a terminal node, a nonterminal node, or a disjunction node, also known as a choice node.
A disjunction node offers a choice between two subtrees. This is typically used to express a choice between two ways of displaying a piece of syntax: e.g., with or without enclosing parentheses. A DCST is typically a DAG: its subtrees can be shared.
Thanks to disjunction nodes, an (exponentially large) set of CSTs can be represented as a single DCST.
The type dcst
is presented as an abstract type equipped with three constructors, namely terminal
, nonterminal
, and choice
.
val nonterminal : A.production -> dcst array -> dcst
nonterminal prod dcsts
constructs a nonterminal node. It assumes (but does not check) that prod
is not a start production, that the number of subtrees is the length of the right-hand side of production prod
, and that the sequence of the head symbols of the subtrees forms the right-hand side of production prod
.
choice dcst1 dcst2
constructs a choice node. It assumes (but does not check) that the subtrees dcst1
and dcst2
have the same head symbol.
The head symbol of a DCST is defined as follows. The head symbol of terminal tok
is the terminal symbol associated with the token tok
. The head symbol of nonterminal prod dcsts
is the left-hand side of the production prod
. The head symbol of choice dcst1 dcst2
is the common head symbol of dcst1
and dcst2
.