Commit 904c82cc authored by POTTIER Francois's avatar POTTIER Francois

Rename [Unparameterized] to [Basic].

parent 72155b19
...@@ -15,7 +15,7 @@ let value = Positions.value ...@@ -15,7 +15,7 @@ let value = Positions.value
(* The source. *) (* The source. *)
module S = Syntax module S = Syntax
(* The target. *) (* The target. *)
module T = UnparameterizedSyntax module T = BasicSyntax
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
......
...@@ -12,8 +12,8 @@ ...@@ -12,8 +12,8 @@
(******************************************************************************) (******************************************************************************)
(* This function translates a grammar from the [Syntax] format (* This function translates a grammar from the [Syntax] format
to the [UnparameterizedSyntax] format. Naturally, the grammar to the [BasicSyntax] format. Naturally, the grammar
must not have any parameterized symbols, since these are not must not have any parameterized symbols, since these are not
allowed by the latter format. *) allowed by the latter format. *)
val drop: Syntax.grammar -> UnparameterizedSyntax.grammar val drop: Syntax.grammar -> BasicSyntax.grammar
...@@ -25,7 +25,7 @@ ...@@ -25,7 +25,7 @@
(* 2016/08/25: in principle, the order in which file names appear on the (* 2016/08/25: in principle, the order in which file names appear on the
command line (when there are several of them) does not matter. It is command line (when there are several of them) does not matter. It is
however used in [UnparameterizedPrinter] (see the problem description however used in [BasicPrinter] (see the problem description
there). For this reason, we define a type [input_file] which includes there). For this reason, we define a type [input_file] which includes
the file's name as well as its index on the command line. *) the file's name as well as its index on the command line. *)
...@@ -52,7 +52,7 @@ let compare_input_files file1 file2 = ...@@ -52,7 +52,7 @@ let compare_input_files file1 file2 =
Pervasives.compare file1.input_file_index file2.input_file_index Pervasives.compare file1.input_file_index file2.input_file_index
(* Ideally, this function should NOT be used, as it reflects the (* Ideally, this function should NOT be used, as it reflects the
order of the input files on the command line. As of 2016/08/25, order of the input files on the command line. As of 2016/08/25,
it is used by [UnparameterizedPrinter], for lack of a better it is used by [BasicPrinter], for lack of a better
solution. *) solution. *)
let current_input_file = let current_input_file =
......
...@@ -15,7 +15,7 @@ open Printf ...@@ -15,7 +15,7 @@ open Printf
open Positions open Positions
open Syntax open Syntax
open Stretch open Stretch
open UnparameterizedSyntax open BasicSyntax
open Settings open Settings
(* When the original grammar is split over several files, it may be IMPOSSIBLE (* When the original grammar is split over several files, it may be IMPOSSIBLE
......
...@@ -22,5 +22,5 @@ ...@@ -22,5 +22,5 @@
If, furthermore, the [mode] parameter requests ``unit tokens'', then the If, furthermore, the [mode] parameter requests ``unit tokens'', then the
types carried by tokens are changed to unit. *) types carried by tokens are changed to unit. *)
val print: Settings.print_mode -> out_channel -> UnparameterizedSyntax.grammar -> unit val print: Settings.print_mode -> out_channel -> BasicSyntax.grammar -> unit
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
open Grammar open Grammar
open Cmly_format open Cmly_format
......
...@@ -1624,7 +1624,7 @@ let initenvdef = ...@@ -1624,7 +1624,7 @@ let initenvdef =
(* ------------------------------------------------------------------------ *) (* ------------------------------------------------------------------------ *)
(* Here is complete code for the parser. *) (* Here is complete code for the parser. *)
open UnparameterizedSyntax open BasicSyntax
let grammar = let grammar =
Front.grammar Front.grammar
......
...@@ -135,4 +135,4 @@ val errorval: expr ...@@ -135,4 +135,4 @@ val errorval: expr
val basics: string val basics: string
val mbasics: UnparameterizedSyntax.grammar -> structure val mbasics: BasicSyntax.grammar -> structure
...@@ -95,7 +95,7 @@ module Run (T: sig end) = struct ...@@ -95,7 +95,7 @@ module Run (T: sig end) = struct
| _ -> ()) | _ -> ())
(Production.rhs prod)); (Production.rhs prod));
if Front.grammar.UnparameterizedSyntax.parameters <> [] then if Front.grammar.BasicSyntax.parameters <> [] then
Error.error [] "the Coq back-end does not support %%parameter." Error.error [] "the Coq back-end does not support %%parameter."
(* Optimized because if we extract some constants to the right caml term, (* Optimized because if we extract some constants to the right caml term,
...@@ -509,7 +509,7 @@ module Run (T: sig end) = struct ...@@ -509,7 +509,7 @@ module Run (T: sig end) = struct
let write_all f = let write_all f =
if not Settings.coq_no_actions then if not Settings.coq_no_actions then
List.iter (fun s -> fprintf f "%s\n\n" s.Stretch.stretch_content) List.iter (fun s -> fprintf f "%s\n\n" s.Stretch.stretch_content)
Front.grammar.UnparameterizedSyntax.preludes; Front.grammar.BasicSyntax.preludes;
fprintf f "From Coq.Lists Require Import List.\n"; fprintf f "From Coq.Lists Require Import List.\n";
fprintf f "From Coq.Numbers.Cyclic.Int31 Require Import Int31.\n"; fprintf f "From Coq.Numbers.Cyclic.Int31 Require Import Int31.\n";
...@@ -525,5 +525,5 @@ module Run (T: sig end) = struct ...@@ -525,5 +525,5 @@ module Run (T: sig end) = struct
if not Settings.coq_no_actions then if not Settings.coq_no_actions then
List.iter (fun stretch -> fprintf f "\n\n%s" stretch.Stretch.stretch_raw_content) List.iter (fun stretch -> fprintf f "\n\n%s" stretch.Stretch.stretch_raw_content)
Front.grammar.UnparameterizedSyntax.postludes Front.grammar.BasicSyntax.postludes
end end
...@@ -75,7 +75,7 @@ let sorts = ...@@ -75,7 +75,7 @@ let sorts =
(* Expand away all applications of parameterized nonterminal symbols, so as (* Expand away all applications of parameterized nonterminal symbols, so as
to obtain a grammar without parameterized nonterminal symbols. *) to obtain a grammar without parameterized nonterminal symbols. *)
let grammar : UnparameterizedSyntax.grammar = let grammar : BasicSyntax.grammar =
let module S = SelectiveExpansion in let module S = SelectiveExpansion in
(* First, perform a selective expansion: expand away all parameters of (* First, perform a selective expansion: expand away all parameters of
higher sort, keeping the parameters of sort [*]. This process always higher sort, keeping the parameters of sort [*]. This process always
...@@ -190,7 +190,7 @@ let grammar = ...@@ -190,7 +190,7 @@ let grammar =
let () = let () =
match Settings.preprocess_mode with match Settings.preprocess_mode with
| Settings.PMOnlyPreprocess mode -> | Settings.PMOnlyPreprocess mode ->
UnparameterizedPrinter.print mode stdout grammar; BasicPrinter.print mode stdout grammar;
exit 0 exit 0
| Settings.PMNormal -> | Settings.PMNormal ->
() ()
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
inference. This yields the grammar that the back-end works with (often inference. This yields the grammar that the back-end works with (often
through the interface provided by module [Grammar]). *) through the interface provided by module [Grammar]). *)
val grammar: UnparameterizedSyntax.grammar val grammar: BasicSyntax.grammar
(* This flag tells whether the semantic actions have been type-checked. It is (* This flag tells whether the semantic actions have been type-checked. It is
set if and only if either [--infer] or [--infer-read-reply] is in use. Note set if and only if either [--infer] or [--infer-read-reply] is in use. Note
......
...@@ -11,14 +11,14 @@ ...@@ -11,14 +11,14 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
open Syntax open Syntax
open Positions open Positions
module Make (G : sig module Make (G : sig
(* An abstract syntax tree for the grammar. *) (* An abstract syntax tree for the grammar. *)
val grammar: UnparameterizedSyntax.grammar val grammar: BasicSyntax.grammar
(* This flag indicates whether it is OK to produce warnings, verbose (* This flag indicates whether it is OK to produce warnings, verbose
information, etc., when this functor is invoked. If it is set to information, etc., when this functor is invoked. If it is set to
......
...@@ -21,7 +21,7 @@ ...@@ -21,7 +21,7 @@
module Make (G : sig module Make (G : sig
(* An abstract syntax tree for the grammar. *) (* An abstract syntax tree for the grammar. *)
val grammar: UnparameterizedSyntax.grammar val grammar: BasicSyntax.grammar
(* This flag indicates whether it is OK to produce warnings, verbose (* This flag indicates whether it is OK to produce warnings, verbose
information, etc., when this functor is invoked. If it is set to information, etc., when this functor is invoked. If it is set to
......
...@@ -13,7 +13,7 @@ ...@@ -13,7 +13,7 @@
open Syntax open Syntax
open Stretch open Stretch
open UnparameterizedSyntax open BasicSyntax
open IL open IL
open CodeBits open CodeBits
open TokenType open TokenType
......
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
(* [ntvar symbol] is the name of the type variable associated with a (* [ntvar symbol] is the name of the type variable associated with a
nonterminal symbol. *) nonterminal symbol. *)
......
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
let position = Positions.position let position = Positions.position
open Keyword open Keyword
type sw = Action.sw type sw = Action.sw
open UnparameterizedSyntax open BasicSyntax
open ListMonad open ListMonad
let drop = MenhirLib.General.drop let drop = MenhirLib.General.drop
let take = MenhirLib.General.take let take = MenhirLib.General.take
......
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
(** [inline g] traverses the grammar [g] and inlines away the nonterminal (** [inline g] traverses the grammar [g] and inlines away the nonterminal
symbols whose definitions are marked [%inline]. The result is a grammar symbols whose definitions are marked [%inline]. The result is a grammar
......
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
open IL open IL
open CodeBits open CodeBits
......
...@@ -20,7 +20,7 @@ val excdef: IL.excdef ...@@ -20,7 +20,7 @@ val excdef: IL.excdef
(* The type of the entry point for the start symbol [nt]. *) (* The type of the entry point for the start symbol [nt]. *)
val entrytypescheme: UnparameterizedSyntax.grammar -> string -> IL.typescheme val entrytypescheme: BasicSyntax.grammar -> string -> IL.typescheme
(* The name of the interpreter sub-module, when the table back-end (* The name of the interpreter sub-module, when the table back-end
is used. *) is used. *)
...@@ -41,5 +41,5 @@ val inspection: string ...@@ -41,5 +41,5 @@ val inspection: string
(* This writes the interface of the generated parser to the [.mli] file. *) (* This writes the interface of the generated parser to the [.mli] file. *)
val write: UnparameterizedSyntax.grammar -> unit -> unit val write: BasicSyntax.grammar -> unit -> unit
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
open Keyword open Keyword
open IL open IL
open CodeBits open CodeBits
......
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
(* [expand_grammar] expands away the keywords [$startpos] and [$endpos], as well (* [expand_grammar] expands away the keywords [$startpos] and [$endpos], as well
the entire [ofs] family of keywords. Doing this early simplifies some aspects the entire [ofs] family of keywords. Doing this early simplifies some aspects
......
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
open IL open IL
(* This is the conventional name of the nonterminal GADT, which describes the (* This is the conventional name of the nonterminal GADT, which describes the
...@@ -41,7 +41,7 @@ let nonterminalgadtdef grammar = ...@@ -41,7 +41,7 @@ let nonterminalgadtdef grammar =
(* The ordering of this list matters. We want the data constructors (* The ordering of this list matters. We want the data constructors
to respect the internal ordering (as determined by [nonterminals] to respect the internal ordering (as determined by [nonterminals]
in [UnparameterizedSyntax]) of the nonterminal symbols. This may in [BasicSyntax]) of the nonterminal symbols. This may
be exploited in the table back-end to allow an unsafe conversion be exploited in the table back-end to allow an unsafe conversion
of a data constructor to an integer code. See [n2i] in of a data constructor to an integer code. See [n2i] in
[InspectionTableInterpreter]. *) [InspectionTableInterpreter]. *)
......
...@@ -33,7 +33,7 @@ val tnonterminalgadtdata: string -> string ...@@ -33,7 +33,7 @@ val tnonterminalgadtdata: string -> string
performed already. This definition is produced only in [--inspection] performed already. This definition is produced only in [--inspection]
mode. *) mode. *)
val nonterminalgadtdef: UnparameterizedSyntax.grammar -> IL.interface val nonterminalgadtdef: BasicSyntax.grammar -> IL.interface
(* When in [--(raw-)depend] mode, we are asked to produce a mock [.mli] file (* When in [--(raw-)depend] mode, we are asked to produce a mock [.mli] file
before [--infer] has run, which means that we are usually not able to before [--infer] has run, which means that we are usually not able to
......
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
(* *) (* *)
(******************************************************************************) (******************************************************************************)
open UnparameterizedSyntax open BasicSyntax
let rec visit grammar visited symbol = let rec visit grammar visited symbol =
try try
......
...@@ -15,5 +15,5 @@ ...@@ -15,5 +15,5 @@
of nonterminals that are reachable, via productions, from the of nonterminals that are reachable, via productions, from the
start nonterminals. *) start nonterminals. *)
val trim: UnparameterizedSyntax.grammar -> UnparameterizedSyntax.grammar val trim: BasicSyntax.grammar -> BasicSyntax.grammar
...@@ -49,7 +49,7 @@ rule lex = parse ...@@ -49,7 +49,7 @@ rule lex = parse
| (lowercase identchar *) as lid | (lowercase identchar *) as lid
{ try { try
let nt = Nonterminal.lookup lid in let nt = Nonterminal.lookup lid in
if StringSet.mem lid Front.grammar.UnparameterizedSyntax.start_symbols then if StringSet.mem lid Front.grammar.BasicSyntax.start_symbols then
NONTERMINAL (nt, lexbuf.lex_start_p, lexbuf.lex_curr_p) NONTERMINAL (nt, lexbuf.lex_start_p, lexbuf.lex_curr_p)
else else
error2 lexbuf "\"%s\" is not a start symbol." lid error2 lexbuf "\"%s\" is not a start symbol." lid
......
...@@ -969,7 +969,7 @@ let versiondef = { ...@@ -969,7 +969,7 @@ let versiondef = {
(* Let's put everything together. *) (* Let's put everything together. *)
open UnparameterizedSyntax open BasicSyntax
let grammar = let grammar =
Front.grammar Front.grammar
......
...@@ -15,7 +15,7 @@ ...@@ -15,7 +15,7 @@
the [token] type. In particular, if [--only-tokens] was specified, the [token] type. In particular, if [--only-tokens] was specified,
it emits the type definition and exits. *) it emits the type definition and exits. *)
open UnparameterizedSyntax open BasicSyntax
open IL open IL
open CodeBits open CodeBits
...@@ -111,7 +111,7 @@ let tokengadtdef grammar = ...@@ -111,7 +111,7 @@ let tokengadtdef grammar =
TDefSum ( TDefSum (
(* The ordering of this list matters. We want the data constructors (* The ordering of this list matters. We want the data constructors
to respect the internal ordering (as determined by [typed_tokens] to respect the internal ordering (as determined by [typed_tokens]
in [UnparameterizedSyntax]) of the terminal symbols. This may be in [BasicSyntax]) of the terminal symbols. This may be
exploited in the table back-end to allow an unsafe conversion exploited in the table back-end to allow an unsafe conversion
of a data constructor to an integer code. See [t2i] in of a data constructor to an integer code. See [t2i] in
[InspectionTableInterpreter]. *) [InspectionTableInterpreter]. *)
......
...@@ -54,12 +54,12 @@ val tokengadtdata: string -> string ...@@ -54,12 +54,12 @@ val tokengadtdata: string -> string
(* The definitions of the token type and of the token GADT, for use by the (* The definitions of the token type and of the token GADT, for use by the
code generators. Each of these lists defines zero or one type. *) code generators. Each of these lists defines zero or one type. *)
val tokentypedef: UnparameterizedSyntax.grammar -> IL.interface val tokentypedef: BasicSyntax.grammar -> IL.interface
val tokengadtdef: UnparameterizedSyntax.grammar -> IL.interface val tokengadtdef: BasicSyntax.grammar -> IL.interface
(* If [--only-tokens] is set, then [produce_tokentypes] writes the type (* If [--only-tokens] is set, then [produce_tokentypes] writes the type
definitions to the [.ml] and [.mli] files and stops Menhir. Otherwise, definitions to the [.ml] and [.mli] files and stops Menhir. Otherwise,
it does nothing. *) it does nothing. *)
val produce_tokentypes: UnparameterizedSyntax.grammar -> unit val produce_tokentypes: BasicSyntax.grammar -> unit
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