diff options
-rw-r--r-- | ltac/tacentries.ml | 2 | ||||
-rw-r--r-- | parsing/egramcoq.ml | 81 | ||||
-rw-r--r-- | parsing/egramcoq.mli | 16 | ||||
-rw-r--r-- | parsing/pcoq.ml | 74 | ||||
-rw-r--r-- | parsing/pcoq.mli | 24 |
5 files changed, 100 insertions, 97 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index f829ae4f5..5c1e7c033 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) = let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry -let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn) +let extend_tactic_grammar kn ml ntn = extend_grammar_command tactic_grammar (kn, ml, ntn) (**********************************************************************) (* Tactic Notation *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 4c038db65..9cfd534b0 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -350,85 +350,16 @@ let extend_constr_notation (_, ng) = let nb' = extend_constr ForPattern ng in nb + nb' -module GrammarCommand = Dyn.Make(struct end) -module GrammarInterp = struct type 'a t = 'a -> int end -module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) - -let grammar_interp = ref GrammarInterpMap.empty - -let (grammar_state : (int * GrammarCommand.t) list ref) = ref [] - -type 'a grammar_command = 'a GrammarCommand.tag - -let create_grammar_command name interp : _ grammar_command = - let obj = GrammarCommand.create name in - let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in - obj - -let extend_grammar tag g = - let nb = GrammarInterpMap.find tag !grammar_interp g in - grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state - -let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g - -let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag = +let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn) +let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) let recover_constr_grammar ntn prec = - let filter (_, gram) : notation_grammar option = match gram with - | GrammarCommand.Dyn (tag, obj) -> - match GrammarCommand.eq tag constr_grammar with - | None -> None - | Some Refl -> - let (prec', ng) = obj in - if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng - else None + let filter (prec', ng) = + if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng + else None in - match List.map_filter filter !grammar_state with + match List.map_filter filter (recover_grammar_command constr_grammar) with | [x] -> x | _ -> assert false - -(* Summary functions: the state of the lexer is included in that of the parser. - Because the grammar affects the set of keywords when adding or removing - grammar rules. *) -type frozen_t = (int * GrammarCommand.t) list * CLexer.frozen_t - -let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) - -(* We compare the current state of the grammar and the state to unfreeze, - by computing the longest common suffixes *) -let factorize_grams l1 l2 = - if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 - -let number_of_entries gcl = - List.fold_left (fun n (p,_) -> n + p) 0 gcl - -let unfreeze (grams, lex) = - let (undo, redo, common) = factorize_grams !grammar_state grams in - let n = number_of_entries undo in - remove_grammars n; - remove_levels n; - grammar_state := common; - CLexer.unfreeze lex; - List.iter extend_dyn_grammar (List.rev_map snd redo) - -(** No need to provide an init function : the grammar state is - statically available, and already empty initially, while - the lexer state should not be resetted, since it contains - keywords declared in g_*.ml4 *) - -let _ = - Summary.declare_summary "GRAMMAR_LEXER" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = Summary.nop } - -let with_grammar_rule_protection f x = - let fs = freeze false in - try let a = f x in unfreeze fs; a - with reraise -> - let reraise = Errors.push reraise in - let () = unfreeze fs in - iraise reraise diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 6ec106626..1fe06a29d 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -36,20 +36,6 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -(** {5 Extending the parser with Summary-synchronized commands} *) - -type 'a grammar_command -(** Type of synchronized parsing extensions. The ['a] type should be - marshallable. *) - -val create_grammar_command : string -> ('a -> int) -> 'a grammar_command -(** Create a new grammar-modifying command with the given name. The function - should modify the parser state and return the number of grammar extensions - performed. *) - -val extend_grammar : 'a grammar_command -> 'a -> unit -(** Extend the grammar of Coq with the given data. *) - (** {5 Adding notations} *) val extend_constr_grammar : Notation.level -> notation_grammar -> unit @@ -58,5 +44,3 @@ val extend_constr_grammar : Notation.level -> notation_grammar -> unit val recover_constr_grammar : notation -> Notation.level -> notation_grammar (** For a declared grammar, returns the rule + the ordered entry types of variables in the rule (for use in the interpretation) *) - -val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 631c5325d..de57feb7f 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -546,6 +546,80 @@ let epsilon_value f e = let () = maybe_uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None +(** Synchronized grammar extensions *) + +module GrammarCommand = Dyn.Make(struct end) +module GrammarInterp = struct type 'a t = 'a -> int end +module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) + +let grammar_interp = ref GrammarInterpMap.empty + +let (grammar_state : (int * GrammarCommand.t) list ref) = ref [] + +type 'a grammar_command = 'a GrammarCommand.tag + +let create_grammar_command name interp : _ grammar_command = + let obj = GrammarCommand.create name in + let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in + obj + +let extend_grammar_command tag g = + let nb = GrammarInterpMap.find tag !grammar_interp g in + grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state + +let recover_grammar_command (type a) (tag : a grammar_command) : a list = + let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v)) -> + match GrammarCommand.eq tag tag' with + | None -> None + | Some Refl -> Some v + in + List.map_filter filter !grammar_state + +let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g + +(* Summary functions: the state of the lexer is included in that of the parser. + Because the grammar affects the set of keywords when adding or removing + grammar rules. *) +type frozen_t = (int * GrammarCommand.t) list * CLexer.frozen_t + +let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) + +(* We compare the current state of the grammar and the state to unfreeze, + by computing the longest common suffixes *) +let factorize_grams l1 l2 = + if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 + +let number_of_entries gcl = + List.fold_left (fun n (p,_) -> n + p) 0 gcl + +let unfreeze (grams, lex) = + let (undo, redo, common) = factorize_grams !grammar_state grams in + let n = number_of_entries undo in + remove_grammars n; + remove_levels n; + grammar_state := common; + CLexer.unfreeze lex; + List.iter extend_dyn_grammar (List.rev_map snd redo) + +(** No need to provide an init function : the grammar state is + statically available, and already empty initially, while + the lexer state should not be resetted, since it contains + keywords declared in g_*.ml4 *) + +let _ = + Summary.declare_summary "GRAMMAR_LEXER" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = Summary.nop } + +let with_grammar_rule_protection f x = + let fs = freeze false in + try let a = f x in unfreeze fs; a + with reraise -> + let reraise = Errors.push reraise in + let () = unfreeze fs in + iraise reraise + (** Registering grammar of generic arguments *) let () = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 72edab8f2..1021ef484 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -106,9 +106,6 @@ val grammar_extend : gram_reinit option (** for reinitialization if ever needed *) -> 'a Extend.extend_statment -> unit -(** Remove the last n extensions *) -val remove_grammars : int -> unit - (** Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -235,6 +232,25 @@ val set_command_entry : vernac_expr Gram.entry -> unit val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option +(** {5 Extending the parser with Summary-synchronized commands} *) + +type 'a grammar_command +(** Type of synchronized parsing extensions. The ['a] type should be + marshallable. *) + +val create_grammar_command : string -> ('a -> int) -> 'a grammar_command +(** Create a new grammar-modifying command with the given name. The function + should modify the parser state and return the number of grammar extensions + performed. *) + +val extend_grammar_command : 'a grammar_command -> 'a -> unit +(** Extend the grammar of Coq with the given data. *) + +val recover_grammar_command : 'a grammar_command -> 'a list +(** Recover the current stack of grammar extensions. *) + +val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b + (** Registering/resetting the level of a constr entry *) type gram_level = @@ -247,5 +263,3 @@ val find_position : val synchronize_level_positions : unit -> unit val register_empty_levels : bool -> int list -> gram_level list - -val remove_levels : int -> unit |