Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 3f0f8bf4 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Added the generation of a table of the productions.

parent 702125eb
......@@ -131,6 +131,23 @@ let etrue : expr =
let eboolconst b =
if b then etrue else efalse
(* Option constructors. *)
let enone =
EData ("None", [])
let esome e =
EData ("Some", [e])
(* List constructors. *)
let rec elist xs =
match xs with
| [] ->
EData ("[]", [])
| x :: xs ->
EData ("::", [ x; elist xs ])
(* Integer constants as patterns. *)
let pint k : pattern =
......
......@@ -54,6 +54,15 @@ val etrue: expr
val efalse: expr
val eboolconst: bool -> expr
(* Option constructors. *)
val enone: expr
val esome: expr -> expr
(* List constructors. *)
val elist: expr list -> expr
(* Integer constants as patterns. *)
val pint: int -> pattern
......
......@@ -346,6 +346,9 @@ and exprk k f e =
var f d
| EData (d, [ arg ]) ->
fprintf f "%s %a" d atom arg
| EData ("::", [ arg1; arg2 ]) ->
(* Special case for infix cons. *)
fprintf f "%a :: %a" atom arg1 atom arg2
| EData (d, (_ :: _ :: _ as args)) ->
fprintf f "%s (%a)" d (seplist app comma) args
| EVar v ->
......
......@@ -15,6 +15,7 @@ val symbolgadtdef: unit -> IL.interface
(* The type [xsymbol] is an existentially quantified version of the symbol
GADT above. Thus, it is not parameterized. *)
val dataX: string
val txsymbol: IL.typ
val xsymboldef: unit -> IL.interface
......@@ -784,6 +784,13 @@ let esymbol (symbol : Symbol.t) : expr =
| Symbol.N nt ->
EData (dataN, [ enonterminal nt ])
(* [xsymbol symbol] is a value of type [xsymbol] that encodes the
symbol [symbol]. It is built by applying the injection [X] (an
existential quantifier) to [esymbol symbol]. *)
let xsymbol (symbol : Symbol.t) : expr =
EData (dataX, [ esymbol symbol ])
(* The type [MenhirInterpreter.lr1state] is known (to us) to be an
alias for [int], so we can pattern match on it. To the user,
though, it will be an abstract type. *)
......@@ -794,7 +801,7 @@ let tlr1state a : typ =
(* Produce a function [symbol] that maps a state of type ['a lr1state]
(represented as an integer value) to a value of type ['a symbol]. *)
let incoming_symbol_def = {
let incoming_symbol_def () = {
valpublic = true;
valpat = PVar "symbol";
valval =
......@@ -841,6 +848,34 @@ let incoming_symbol_def = {
(* ------------------------------------------------------------------------ *)
(* A table that maps a production (i.e., an integer index) to its definition
(i.e., its left-hand and right-hand sides). This table concerns ordinary
productions only, as opposed to the start productions, whose existence is
not exposed to the user. *)
let production_def prod =
if Production.is_start prod then
enone
else
esome (ETuple [
(* The production's left-hand side. This is always a nonterminal symbol,
of course. For simplicity, we encode it at type [xsymbol], even though
we could in principle use an existentially-quantified type of
nonterminal symbols. *)
xsymbol (Symbol.N (Production.nt prod));
(* The production's right-hand side. This is a list of symbols. *)
elist (List.map xsymbol (Array.to_list (Production.rhs prod)))
])
let production_defs () =
assert Settings.inspection;
define (
"production_defs",
EArray (Production.map production_def)
)
(* ------------------------------------------------------------------------ *)
(* Let's put everything together. *)
open UnparameterizedSyntax
......@@ -886,7 +921,10 @@ let program =
xsymboldef()
) @
SIValDefs (false, [incoming_symbol_def]) ::
SIValDefs (false, [
incoming_symbol_def();
production_defs()
]) ::
[]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment