diff options
| -rw-r--r-- | ltac/tacentries.ml | 4 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 20 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 19 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 14 |
4 files changed, 33 insertions, 24 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 714bfa841..5720a6f37 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -184,8 +184,8 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - grammar_extend entry None (pos, [(None, None, List.rev [rules])]); - (1, state) + let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in + ([r], state) let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 8af324d71..21a9afa29 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -421,8 +421,8 @@ let target_to_bool : type r. r target -> bool = function let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = let empty = (pos, [(name, p4assoc, [])]) in - if forpat then grammar_extend Constr.pattern reinit empty - else grammar_extend Constr.operconstr reinit empty + if forpat then ExtendRule (Constr.pattern, reinit, empty) + else ExtendRule (Constr.operconstr, reinit, empty) let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with | Stop -> [] @@ -456,7 +456,7 @@ let extend_constr state forpat ng = let n = ng.notgram_level in let assoc = ng.notgram_assoc in let (entry, level) = interp_constr_entry_key forpat n in - let fold (nb, state) pt = + let fold (accu, state) pt = let AnyTyRule r = make_ty_rule assoc n forpat pt in let symbs = ty_erase r in let pure_sublevels = pure_sublevels level symbs in @@ -464,14 +464,14 @@ let extend_constr state forpat ng = let needed_levels, state = register_empty_levels state isforpat pure_sublevels in let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in let nb_decls = List.length needed_levels + 1 in - let () = List.iter (prepare_empty_levels isforpat) needed_levels in + let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in let empty = { constrs = []; constrlists = []; binders = [] } in let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = (name, p4assoc, [Rule (symbs, act)]) in - let () = grammar_extend entry reinit (pos, [rule]) in - (nb + nb_decls, state) + let r = ExtendRule (entry, reinit, (pos, [rule])) in + (accu @ empty_rules @ [r], state) in - List.fold_left fold (0, state) ng.notgram_prods + List.fold_left fold ([], state) ng.notgram_prods let constr_levels = GramState.field () @@ -481,11 +481,11 @@ let extend_constr_notation (_, ng) state = | Some lev -> lev in (* Add the notation in constr *) - let (nb, levels) = extend_constr levels ForConstr ng in + let (r, levels) = extend_constr levels ForConstr ng in (* Add the notation in cases_pattern *) - let (nb', levels) = extend_constr levels ForPattern ng in + let (r', levels) = extend_constr levels ForPattern ng in let state = GramState.set state constr_levels levels in - (nb + nb', state) + (r @ r', state) let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 1cc7b6c54..ae56c4723 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -98,11 +98,11 @@ let of_coq_extend_statement (pos, st) = (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position +type extend_rule = +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule + type ext_kind = - | ByGrammar : - 'a G.entry - * gram_reinit option (** for reinitialization if ever needed *) - * 'a Extend.extend_statment -> ext_kind + | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) (** The list of extensions *) @@ -110,7 +110,7 @@ type ext_kind = let camlp4_state = ref [] let grammar_extend e reinit ext = - camlp4_state := ByGrammar (e,reinit,ext) :: !camlp4_state; + camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; let ext = of_coq_extend_statement ext in camlp4_verbose (maybe_uncurry (G.extend e)) ext @@ -167,7 +167,7 @@ let rec remove_grammars n = if n>0 then (match !camlp4_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") - | ByGrammar(g,reinit,ext)::t -> + | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); camlp4_state := t; remove_grammars (n-1) @@ -405,7 +405,7 @@ let epsilon_value f e = module GramState = Store.Make(struct end) -type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t module GrammarCommand = Dyn.Make(struct end) module GrammarInterp = struct type 'a t = 'a grammar_extension end @@ -428,7 +428,10 @@ let extend_grammar_command tag g = | [] -> GramState.empty | (_, _, st) :: _ -> st in - let (nb, st) = modify g grammar_state in + let (rules, st) = modify g grammar_state in + let iter (ExtendRule (e, reinit, ext)) = grammar_extend e reinit ext in + let () = List.iter iter rules in + let nb = List.length rules in grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack let recover_grammar_command (type a) (tag : a grammar_command) : a list = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1d076e295..ed82607dd 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -241,12 +241,18 @@ type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be marshallable. *) -type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t +type extend_rule = +| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule + +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t +(** Grammar extension entry point. Given some ['a] and a current grammar state, + such a function must produce the list of grammar extensions that will be + applied in the same order and kept synchronized w.r.t. the summary, together + with a new state. It should be pure. *) val create_grammar_command : string -> 'a grammar_extension -> '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. *) +(** Create a new grammar-modifying command with the given name. The extension + function is called to generate the rules for a given data. *) val extend_grammar_command : 'a grammar_command -> 'a -> unit (** Extend the grammar of Coq with the given data. *) |