From e43c35ba795520fe111ac39a834f334753491b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Apr 2017 10:31:29 +0200 Subject: [STM] explicit handling of parsing states DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès Co-authored-by: Emilio Jesus Gallego Arias --- parsing/pcoq.ml | 1 - parsing/pcoq.mli | 14 ++++++++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) (limited to 'parsing') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 19ae97da77..759e60fbca 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -439,7 +439,6 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end - let epsilon_value f e = let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in let ext = [None, None, [r]] in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 352857d4cd..3203a25b46 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -41,6 +41,16 @@ end - static rules explicitly defined in files g_*.ml4 - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and VERNAC EXTEND (see e.g. file extratactics.ml4) + + Note that parsing a Coq document is in essence stateful: the parser + needs to recognize commands that start proofs and use a different + parsing entry point for them. + + We thus provide two different interfaces: the "raw" parsing + interface, in the style of camlp5, which provides more flexibility, + and a more specialize "parse_vernac" one, which will indeed adjust + the state as needed. + *) (** Dynamic extension of rules @@ -269,3 +279,7 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry val register_grammars_by_name : string -> any_entry list -> unit val find_grammars_by_name : string -> any_entry list + +(** Parsing state handling *) +val freeze : marshallable:bool -> frozen_t +val unfreeze : frozen_t -> unit -- cgit v1.2.3