Commit 1968e4f8 authored by POTTIER Francois's avatar POTTIER Francois

Preliminary work towards two expansion modes.

parent e10dee4c
......@@ -18,6 +18,14 @@ open Syntax
(* -------------------------------------------------------------------------- *)
(* Expansion modes. *)
type mode =
| ExpandHigherSort
| ExpandAll
(* -------------------------------------------------------------------------- *)
(* Expansion can be understood as traversing a graph where every vertex is
labeled with a pair of a nonterminal symbol [nt] and an instantiation of
the formal parameters of [nt]. *)
......@@ -124,6 +132,8 @@ and subst_parameters env params =
(* For syntactic convenience, the rest of this file is a functor. *)
module Run (G : sig
(* Expansion mode. *)
val mode: mode
(* Sort information. *)
val sorts: SortInference.sorts
(* The grammar [g] whose expansion is desired. *)
......@@ -262,6 +272,8 @@ let mangle : label -> nonterminal =
let recognize (param : parameter) : parameter =
(* [param] must have sort [star], in an appropriate sort environment. *)
match param with
| ParameterAnonymous _ ->
assert false
| ParameterVar _ ->
param
| ParameterApp (sym, ps) ->
......@@ -270,14 +282,21 @@ let recognize (param : parameter) : parameter =
(* This symbol is applied to at least one argument, so cannot be
a terminal symbol. It must be either a nonterminal symbol or
an (uninstantiated) formal parameter of the current rule. *)
(* Full specialization. *)
let label = (x, List.map (fun p -> Some p) ps)
and residuals = [] in
enqueue label;
let sym = mangle label in
Parameters.app (unknown sym) residuals
| ParameterAnonymous _ ->
assert false
(* Actually, in both modes, formal parameters of higher sort are
expanded away, so [sym] cannot be an uninstantiated parameter
of the current rule. It must be a nonterminal symbol. We can
therefore look up its sort in the toplevel environment [sorts]. *)
match mode with
| ExpandAll ->
(* Full specialization. *)
let label = (x, List.map (fun p -> Some p) ps)
and residuals = [] in
enqueue label;
let sym = mangle label in
Parameters.app (unknown sym) residuals
| ExpandHigherSort ->
(* Expansion of only the parameters of higher sort. *)
assert false
(* -------------------------------------------------------------------------- *)
......@@ -464,6 +483,10 @@ end (* of the functor *)
(* Re-package the above functor as a function. *)
let expand sorts g =
let module G = Run(struct let sorts = sorts let g = g end) in
let expand mode sorts g =
let module G = Run(struct
let mode = mode
let sorts = sorts
let g = g
end) in
G.g
......@@ -14,11 +14,25 @@
open Syntax
open SortInference
(* [expand sorts g] expands away some or all of the parameterized
nonterminal symbols in the grammar [g], producing a new grammar.
[sorts] is the sort environment produced by [SortInference]. *)
(* [expand sorts g] expands away some or all of the parameterized nonterminal
symbols in the grammar [g], producing a new grammar. [sorts] is the sort
environment produced by [SortInference]. *)
(* At this time, expansion is complete: all parameters are expanded
away. *)
(* The mode [ExpandHigherSort] causes a partial expansion: only the parameters
of higher sort (i.e., of sort other than [*]) are expanded away. This mode
is safe, in the sense that expansion always terminates. A proof sketch is
as follows: 1- an application always has sort [*]; 2- therefore, only a
variable can have higher sort; 3- therefore, only a finite number of terms
can appear during expansion. *)
val expand: sorts -> grammar -> grammar
(* The mode [ExpandAll] causes a complete expansion: all parameters are
expanded away. This process is potentially nonterminating. One must first
run the termination test in [CheckSafeParameterizedGrammar] (which itself
is applicable only after the parameters of higher sort have been expanded
away). *)
type mode =
| ExpandHigherSort
| ExpandAll
val expand: mode -> sorts -> grammar -> grammar
......@@ -17,7 +17,7 @@
(* Reading a grammar from a file. *)
let load_partial_grammar filename =
let load_partial_grammar filename : Syntax.partial_grammar =
let validExt = if Settings.coq then ".vy" else ".mly" in
if not (Filename.check_suffix filename validExt) then
Error.error []
......@@ -43,7 +43,7 @@ let load_partial_grammar filename =
(* Read all of the grammar files that are named on the command line. *)
let partial_grammars =
let grammars : Syntax.partial_grammar list =
List.map load_partial_grammar Settings.filenames
let () =
......@@ -53,31 +53,32 @@ let () =
(* Eliminate anonymous rules. *)
let partial_grammars =
List.map Anonymous.transform_partial_grammar partial_grammars
let grammars : Syntax.partial_grammar list =
List.map Anonymous.transform_partial_grammar grammars
(* ------------------------------------------------------------------------- *)
(* If several grammar files were specified, merge them. *)
let parameterized_grammar =
PartialGrammar.join_partial_grammars partial_grammars
let grammar : Syntax.grammar =
PartialGrammar.join_partial_grammars grammars
(* ------------------------------------------------------------------------- *)
(* Check that the grammar is well-sorted; infer the sort of every symbol. *)
let sorts =
SortInference.infer parameterized_grammar
SortInference.infer grammar
(* ------------------------------------------------------------------------- *)
(* Expand away all applications of parameterized nonterminal symbols, so as
to obtain a grammar without parameterized nonterminal symbols. *)
let grammar =
CheckSafeParameterizedGrammar.check parameterized_grammar;
Drop.drop (SelectiveExpansion.expand sorts parameterized_grammar)
let grammar : UnparameterizedSyntax.grammar =
(* TEMPORARY do selective expansion first *)
CheckSafeParameterizedGrammar.check grammar;
Drop.drop (SelectiveExpansion.expand SelectiveExpansion.ExpandAll sorts grammar)
let () =
Time.tick "Joining and expanding"
......
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