Commit 4a1048f8 authored by POTTIER Francois's avatar POTTIER Francois

The generation of the inspection API is now subject to --inspection.

parent d4c8a4b4
...@@ -9,7 +9,7 @@ endif ...@@ -9,7 +9,7 @@ endif
# We assume that menhirLib has been installed in such a # We assume that menhirLib has been installed in such a
# way that ocamlfind knows about it. # way that ocamlfind knows about it.
MENHIRFLAGS := --infer --table MENHIRFLAGS := --infer --table --inspection
OCAMLBUILD := ocamlbuild -use-ocamlfind -use-menhir -menhir "$(MENHIR) $(MENHIRFLAGS)" -package menhirLib OCAMLBUILD := ocamlbuild -use-ocamlfind -use-menhir -menhir "$(MENHIR) $(MENHIRFLAGS)" -package menhirLib
......
...@@ -2,7 +2,9 @@ open UnparameterizedSyntax ...@@ -2,7 +2,9 @@ open UnparameterizedSyntax
open IL open IL
open CodeBits open CodeBits
(* This is the [Error] exception. *) (* -------------------------------------------------------------------------- *)
(* The [Error] exception. *)
let excname = let excname =
"Error" "Error"
...@@ -16,12 +18,16 @@ let excredef = { ...@@ -16,12 +18,16 @@ let excredef = {
excdef with exceq = Some excname excdef with exceq = Some excname
} }
(* -------------------------------------------------------------------------- *)
(* The type of the monolithic entry point for the start symbol [symbol]. *) (* The type of the monolithic entry point for the start symbol [symbol]. *)
let entrytypescheme grammar symbol = let entrytypescheme grammar symbol =
let typ = TypTextual (ocamltype_of_start_symbol grammar symbol) in let typ = TypTextual (ocamltype_of_start_symbol grammar symbol) in
type2scheme (marrow [ arrow tlexbuf TokenType.ttoken; tlexbuf ] typ) type2scheme (marrow [ arrow tlexbuf TokenType.ttoken; tlexbuf ] typ)
(* -------------------------------------------------------------------------- *)
(* When the table back-end is active, the generated parser contains, (* When the table back-end is active, the generated parser contains,
as a sub-module, an application of [Engine.Make]. This sub-module as a sub-module, an application of [Engine.Make]. This sub-module
is named as follows. *) is named as follows. *)
...@@ -32,6 +38,8 @@ let interpreter = ...@@ -32,6 +38,8 @@ let interpreter =
let result t = let result t =
TypApp (interpreter ^ ".result", [ t ]) TypApp (interpreter ^ ".result", [ t ])
(* -------------------------------------------------------------------------- *)
(* The name of the incremental entry point for the start symbol [symbol]. *) (* The name of the incremental entry point for the start symbol [symbol]. *)
let incremental symbol = let incremental symbol =
...@@ -46,67 +54,89 @@ let entrytypescheme_incremental grammar symbol = ...@@ -46,67 +54,89 @@ let entrytypescheme_incremental grammar symbol =
let t = TypTextual (ocamltype_of_start_symbol grammar symbol) in let t = TypTextual (ocamltype_of_start_symbol grammar symbol) in
type2scheme (marrow [ tunit ] (result t)) type2scheme (marrow [ tunit ] (result t))
(* This is the interface of the generated parser. *) (* -------------------------------------------------------------------------- *)
let interface grammar = [ (* The monolithic (traditional) API: the type [token], the exception [Error],
IIFunctor (grammar.parameters, and the parser's entry points. *)
let monolithic_api grammar =
TokenType.tokentypedef grammar @
IIComment "This exception is raised by the monolithic API functions." ::
IIExcDecls [ excdef ] ::
IIComment "The monolithic API." ::
IIValDecls (
StringSet.fold (fun symbol decls ->
(Misc.normalize symbol, entrytypescheme grammar symbol) :: decls
) grammar.start_symbols []
) ::
[]
(* -------------------------------------------------------------------------- *)
(* The incremental API. *)
let incremental_api grammar () =
(* The monolithic (traditional) API: the type [token], the exception IIComment "The incremental API." ::
[Error], and the parser's entry points. *) IIModule (
interpreter,
TokenType.tokentypedef grammar @ MTWithType (
MTNamedModuleType "MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE",
IIComment "This exception is raised by the monolithic API functions." :: "token", (* NOT [tctoken], which is qualified if [--external-tokens] is used *)
IIExcDecls [ excdef ] :: WKDestructive,
TokenType.ttoken
IIComment "The monolithic API." ::
IIValDecls (
StringSet.fold (fun symbol decls ->
(Misc.normalize symbol, entrytypescheme grammar symbol) :: decls
) grammar.start_symbols []
) ::
(* The incremental engine and API. *)
listiflazy Settings.table (fun () -> [
IIComment "The incremental API.";
IIModule (
interpreter,
MTWithType (
MTNamedModuleType "MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE",
"token", (* NOT [tctoken], which is qualified if [--external-tokens] is used *)
WKDestructive,
TokenType.ttoken
)
);
IIComment "The entry point(s) to the incremental API.";
IIValDecls (
StringSet.fold (fun symbol decls ->
(incremental symbol, entrytypescheme_incremental grammar symbol) :: decls
) grammar.start_symbols []
)
]) @
(* The inspection API. *)
listiflazy Settings.table (fun () ->
TokenType.tokengadtdef grammar @
NonterminalType.nonterminalgadtdef grammar @
SymbolType.symbolgadtdef grammar @
(* TEMPORARY emit a comment *)
IIValDecls [
let ty =
arrow (TypApp (interpreter ^ ".lr1state", [ TypVar "a" ]))
(TypApp ("symbol", [ TypVar "a" ]))
in
(* TEMPORARY code sharing with tableBackend *)
"symbol", type2scheme ty
] ::
[]
) )
) ::
IIComment "The entry point(s) to the incremental API." ::
IIValDecls (
StringSet.fold (fun symbol decls ->
(incremental symbol, entrytypescheme_incremental grammar symbol) :: decls
) grammar.start_symbols []
) ::
[]
(* -------------------------------------------------------------------------- *)
(* The inspection API. *)
let inspection_api grammar () =
TokenType.tokengadtdef grammar @
NonterminalType.nonterminalgadtdef grammar @
SymbolType.symbolgadtdef() @
(* TEMPORARY emit a comment *)
IIValDecls [
let ty =
arrow (TypApp (interpreter ^ ".lr1state", [ TypVar "a" ]))
(TypApp ("symbol", [ TypVar "a" ]))
in
(* TEMPORARY code sharing with tableBackend *)
"symbol", type2scheme ty
] ::
[]
(* -------------------------------------------------------------------------- *)
(* The complete interface of the generated parser. *)
let interface grammar = [
IIFunctor (grammar.parameters,
monolithic_api grammar @
listiflazy Settings.table (incremental_api grammar) @
listiflazy Settings.inspection (inspection_api grammar)
) )
] ]
(* -------------------------------------------------------------------------- *)
(* Writing the interface to a file. *) (* Writing the interface to a file. *)
let write grammar () = let write grammar () =
......
...@@ -22,9 +22,10 @@ let tnonterminalgadtdata nt = ...@@ -22,9 +22,10 @@ let tnonterminalgadtdata nt =
exception MissingOCamlType exception MissingOCamlType
let nonterminalgadtdef grammar = let nonterminalgadtdef grammar =
assert Settings.table; assert Settings.inspection;
try let comment, datadefs =
let datadefs = try
"The indexed type of nonterminal symbols.",
List.fold_left (fun defs nt -> List.fold_left (fun defs nt ->
let index = let index =
match ocamltype_of_symbol grammar nt with match ocamltype_of_symbol grammar nt with
...@@ -39,17 +40,21 @@ let nonterminalgadtdef grammar = ...@@ -39,17 +40,21 @@ let nonterminalgadtdef grammar =
datatypeparams = Some [ index ] datatypeparams = Some [ index ]
} :: defs } :: defs
) [] (nonterminals grammar) ) [] (nonterminals grammar)
in with MissingOCamlType ->
[ (* If the type of some nonterminal symbol is unknown, give up
IIComment "The indexed type of nonterminal symbols."; and define ['a nonterminal] as an abstract type. This is
IITypeDecls [{ useful when we are in [--(raw)-depend] mode and we do not
typename = tcnonterminalgadt; wish to fail. Instead, we produce a mock [.mli] file that
typeparams = [ "_" ]; is an approximation of the real [.mli] file. *)
typerhs = TDefSum datadefs; "The indexed type of nonterminal symbols (mock!).",
typeconstraint = None []
}] in
] [
with MissingOCamlType -> IIComment comment;
(* If the type of some nonterminal symbol is unknown, give up IITypeDecls [{
on the whole thing. *) typename = tcnonterminalgadt;
[] typeparams = [ "_" ];
typerhs = TDefSum datadefs;
typeconstraint = None
}]
]
...@@ -16,7 +16,8 @@ val tnonterminalgadtdata: string -> string ...@@ -16,7 +16,8 @@ val tnonterminalgadtdata: string -> string
generators. This definition can be constructed only if the type of every generators. This definition can be constructed only if the type of every
nonterminal symbol is known, either because the user has provided this nonterminal symbol is known, either because the user has provided this
information, or because [--infer] has been set and inference has been information, or because [--infer] has been set and inference has been
performed already. This definition is produced only in [--table] mode. *) performed already. This definition is produced only in [--inspection]
mode. *)
val nonterminalgadtdef: UnparameterizedSyntax.grammar -> IL.interface val nonterminalgadtdef: UnparameterizedSyntax.grammar -> IL.interface
......
...@@ -173,7 +173,7 @@ let options = Arg.align [ ...@@ -173,7 +173,7 @@ let options = Arg.align [
"--follow-construction", Arg.Set follow, " (undocumented)"; "--follow-construction", Arg.Set follow, " (undocumented)";
"--graph", Arg.Set graph, " Write grammar's dependency graph to <basename>.dot"; "--graph", Arg.Set graph, " Write grammar's dependency graph to <basename>.dot";
"--infer", Arg.Set infer, " Invoke ocamlc for ahead of time type inference"; "--infer", Arg.Set infer, " Invoke ocamlc for ahead of time type inference";
"--inspection", Arg.Set inspection, " Generate an inspection API (requires --table)"; "--inspection", Arg.Set inspection, " Generate the inspection API (requires --table)";
"--interpret", Arg.Set interpret, " Interpret the sentences provided on stdin"; "--interpret", Arg.Set interpret, " Interpret the sentences provided on stdin";
"--interpret-show-cst", Arg.Set interpret_show_cst, " Show a concrete syntax tree upon acceptance"; "--interpret-show-cst", Arg.Set interpret_show_cst, " Show a concrete syntax tree upon acceptance";
"--log-automaton", Arg.Set_int logA, "<level> Log information about the automaton"; "--log-automaton", Arg.Set_int logA, "<level> Log information about the automaton";
......
...@@ -131,6 +131,11 @@ val interpret_show_cst : bool ...@@ -131,6 +131,11 @@ val interpret_show_cst : bool
val table : bool val table : bool
(* Whether to generate the inspection API (which requires GADTs, and
requires producing more tables). *)
val inspection : bool
(* Whether to generate a coq description of the grammar and automaton. *) (* Whether to generate a coq description of the grammar and automaton. *)
val coq : bool val coq : bool
......
...@@ -20,33 +20,27 @@ let dataN = ...@@ -20,33 +20,27 @@ let dataN =
(* The definition of the symbol GADT. *) (* The definition of the symbol GADT. *)
let symbolgadtdef grammar = let symbolgadtdef () =
assert Settings.table; assert Settings.inspection;
(* This definition can be produced only if we are successfully able let a = "a" in
to construct the nonterminal GADT. *) let datadefs =
match NonterminalType.nonterminalgadtdef grammar with {
| [] -> dataname = dataT;
[] datavalparams = [ TokenType.ttokengadt (TypVar a) ];
| _ :: _ -> datatypeparams = Some [ TypVar a ]
let a = "a" in } ::
let datadefs = {
{ dataname = dataN;
dataname = dataT; datavalparams = [ NonterminalType.tnonterminalgadt (TypVar a) ];
datavalparams = [ TokenType.ttokengadt (TypVar a) ]; datatypeparams = Some [ TypVar a ]
datatypeparams = Some [ TypVar a ] } ::
} :: []
{ in
dataname = dataN; [ IIComment "The indexed type of terminal and nonterminal symbols.";
datavalparams = [ NonterminalType.tnonterminalgadt (TypVar a) ]; IITypeDecls [{
datatypeparams = Some [ TypVar a ] typename = tcsymbolgadt;
} :: typeparams = [ a ];
[] typerhs = TDefSum datadefs;
in typeconstraint = None
[ IIComment "The indexed type of terminal and nonterminal symbols."; }]
IITypeDecls [{ ]
typename = tcsymbolgadt;
typeparams = [ a ];
typerhs = TDefSum datadefs;
typeconstraint = None
}]
]
...@@ -10,5 +10,5 @@ val dataN: string ...@@ -10,5 +10,5 @@ val dataN: string
(* The definition of the symbol GADT. This definition can be produced only if (* The definition of the symbol GADT. This definition can be produced only if
we are successfully able to construct the nonterminal GADT first. *) we are successfully able to construct the nonterminal GADT first. *)
val symbolgadtdef: UnparameterizedSyntax.grammar -> IL.interface val symbolgadtdef: unit -> IL.interface
...@@ -778,8 +778,6 @@ let tlr1state a : typ = ...@@ -778,8 +778,6 @@ let tlr1state a : typ =
(* Produce a function [symbol] that maps a state of type ['a lr1state] (* Produce a function [symbol] that maps a state of type ['a lr1state]
(represented as an integer value) to a value of type ['a symbol]. *) (represented as an integer value) to a value of type ['a symbol]. *)
(* TEMPORARY maybe subject to a switch, so as to reduce table size *)
let incoming_symbol_def = { let incoming_symbol_def = {
valpublic = true; valpublic = true;
valpat = PVar "symbol"; valpat = PVar "symbol";
...@@ -858,13 +856,19 @@ let program = ...@@ -858,13 +856,19 @@ let program =
SIValDefs (false, api) :: SIValDefs (false, api) ::
interface_to_structure ( listiflazy Settings.inspection (fun () ->
tokengadtdef grammar @
nonterminalgadtdef grammar @ interface_to_structure (
symbolgadtdef grammar tokengadtdef grammar @
) @ nonterminalgadtdef grammar @
symbolgadtdef()
) @
SIValDefs (false, [incoming_symbol_def]) :: SIValDefs (false, [incoming_symbol_def]) ::
[]
) @
SIStretch grammar.postludes :: SIStretch grammar.postludes ::
......
...@@ -66,12 +66,12 @@ let tokentypedef grammar = ...@@ -66,12 +66,12 @@ let tokentypedef grammar =
(* This is the definition of the token GADT. Here, the data (* This is the definition of the token GADT. Here, the data
constructors have no value argument, but have a type index. *) constructors have no value argument, but have a type index. *)
(* The token GADT is produced only in [--table] mode. This ensures that, when (* The token GADT is produced only when [Settings.inspection] is true. Thus,
[--table] is off, we remain compatible with old versions of OCaml, without when [Settings.inspection] is false, we remain compatible with old versions
GADTs. *) of OCaml, without GADTs. *)
let tokengadtdef grammar = let tokengadtdef grammar =
assert Settings.table; assert Settings.inspection;
let datadefs = let datadefs =
StringMap.fold (fun token properties defs -> StringMap.fold (fun token properties defs ->
if properties.tk_is_declared then if properties.tk_is_declared then
...@@ -114,7 +114,7 @@ let produce_tokentypes grammar = ...@@ -114,7 +114,7 @@ let produce_tokentypes grammar =
let i = let i =
tokentypedef grammar @ tokentypedef grammar @
listiflazy Settings.table (fun () -> listiflazy Settings.inspection (fun () ->
tokengadtdef grammar tokengadtdef grammar
) )
in in
......
...@@ -5,9 +5,9 @@ ...@@ -5,9 +5,9 @@
which describes the tokens. A token contains a tag (a terminal symbol) which describes the tokens. A token contains a tag (a terminal symbol)
and possibly a semantic value. *) and possibly a semantic value. *)
(* In addition to that, in [--table] mode only, we produce a GADT which (* In addition to that, in [--inspection] mode only, we produce a GADT which
describes the terminal symbols. A terminal symbol is just a tag; it describes the terminal symbols. A terminal symbol is just a tag; it does
does not carry a semantic value. *) not carry a semantic value. *)
(* In this module, we also deal with [--only-tokens] and [--external-tokens]. (* In this module, we also deal with [--only-tokens] and [--external-tokens].
If [--only-tokens] is specified on the command line, [produce_tokentypes] If [--only-tokens] is specified on the command line, [produce_tokentypes]
...@@ -41,8 +41,8 @@ val tokengadtdata: string -> string ...@@ -41,8 +41,8 @@ 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 may define zero or one type. Indeed, code generators. Each of these lists may define zero or one type. Indeed,
both lists are empty when [--external-tokens] is set. Otherwise, only the both lists are empty when [--external-tokens] is set. Otherwise, only the
type [token] is defined when not in [--table] mode, and both [token] and type [token] is defined always, and the type [terminal] is defined only in
[terminal] are defined when in [--table] mode. *) [--inspection] mode. *)
val tokentypedef: UnparameterizedSyntax.grammar -> IL.interface val tokentypedef: UnparameterizedSyntax.grammar -> IL.interface
val tokengadtdef: UnparameterizedSyntax.grammar -> IL.interface val tokengadtdef: UnparameterizedSyntax.grammar -> IL.interface
......
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