diff options
| -rw-r--r-- | interp/notation.ml | 28 | ||||
| -rw-r--r-- | interp/notation.mli | 5 | ||||
| -rw-r--r-- | intf/notation_term.mli | 15 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 27 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 23 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 8 |
6 files changed, 41 insertions, 65 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index b19fd9e1f..7ad104d03 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -967,23 +967,27 @@ let pr_visibility prglob = function type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list (* Concrete syntax for symbolic-extension table *) -let printing_rules = - ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t) +let notation_rules = + ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) -let declare_notation_printing_rule ntn ~extra unpl = - printing_rules := String.Map.add ntn (unpl,extra) !printing_rules +let declare_notation_rule ntn ~extra unpl gram = + notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules let find_notation_printing_rule ntn = - try fst (String.Map.find ntn !printing_rules) + try pi1 (String.Map.find ntn !notation_rules) with Not_found -> anomaly (str "No printing rule found for " ++ str ntn) let find_notation_extra_printing_rules ntn = - try snd (String.Map.find ntn !printing_rules) + try pi2 (String.Map.find ntn !notation_rules) with Not_found -> [] +let find_notation_parsing_rules ntn = + try pi3 (String.Map.find ntn !notation_rules) + with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn) + let add_notation_extra_printing_rule ntn k v = try - printing_rules := - let p, pp = String.Map.find ntn !printing_rules in - String.Map.add ntn (p, (k,v) :: pp) !printing_rules + notation_rules := + let p, pp, gr = String.Map.find ntn !notation_rules in + String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules with Not_found -> user_err_loc (Loc.ghost,"add_notation_extra_printing_rule", str "No such Notation.") @@ -993,7 +997,7 @@ let add_notation_extra_printing_rule ntn k v = let freeze _ = (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, - !delimiters_map, !notations_key_table, !printing_rules, + !delimiters_map, !notations_key_table, !notation_rules, !scope_class_map) let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = @@ -1003,7 +1007,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; - printing_rules := pprules; + notation_rules := pprules; scope_class_map := clsc let init () = @@ -1011,7 +1015,7 @@ let init () = notation_level_map := String.Map.empty; delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - printing_rules := String.Map.empty; + notation_rules := String.Map.empty; scope_class_map := initial_scope_class_map let _ = diff --git a/interp/notation.mli b/interp/notation.mli index 480979ccc..a85dc50f2 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -196,10 +196,11 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd (** Declare and look for the printing rule for symbolic notations *) type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list -val declare_notation_printing_rule : - notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val declare_notation_rule : + notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit val find_notation_printing_rule : notation -> unparsing_rule val find_notation_extra_printing_rules : notation -> extra_unparsing_rules +val find_notation_parsing_rules : notation -> notation_grammar val add_notation_extra_printing_rule : notation -> string -> string -> unit (** Rem: printing rules for primitive token are canonical *) diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 7c5d7657b..c7c301629 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -78,3 +78,18 @@ type notation_interp_env = { ninterp_rec_vars : Id.t Id.Map.t; mutable ninterp_only_parse : bool; } + +type grammar_constr_prod_item = + | GramConstrTerminal of Tok.t + | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option + | GramConstrListMark of int * bool + (* tells action rule to make a list of the n previous parsed items; + concat with last parsed list if true *) + +type notation_grammar = { + notgram_level : int; + notgram_assoc : Extend.gram_assoc option; + notgram_notation : Constrexpr.notation; + notgram_prods : grammar_constr_prod_item list list; + notgram_typs : notation_var_internalization_type list; +} diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 21a9afa29..ade31c1d3 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -9,9 +9,10 @@ open Errors open Util open Pcoq -open Extend open Constrexpr +open Notation open Notation_term +open Extend open Libnames open Names @@ -320,13 +321,6 @@ let cases_pattern_expr_of_name (loc,na) = match na with | Anonymous -> CPatAtom (loc,None) | Name id -> CPatAtom (loc,Some (Ident (loc,id))) -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - type 'r env = { constrs : 'r list; constrlists : 'r list list; @@ -444,14 +438,6 @@ let make_act : type r. r target -> _ -> r gen_eval = function let env = (env.constrs, env.constrlists) in CPatNotation (loc, notation, env, []) -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - let extend_constr state forpat ng = let n = ng.notgram_level in let assoc = ng.notgram_assoc in @@ -491,12 +477,3 @@ let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) - -let recover_constr_grammar ntn prec = - 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 (recover_grammar_command constr_grammar) with - | [x] -> x - | _ -> assert false diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 1fe06a29d..6dda3817a 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -19,28 +19,7 @@ open Egramml (** This is the part specific to Coq-level Notation and Tactic Notation. For the ML-level tactic and vernac extensions, see Egramml. *) -(** For constr notations *) - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> notation_grammar -> unit +val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit (** Add a term notation rule to the parsing system. *) - -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) *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 52117f13f..899bfaba9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -688,9 +688,9 @@ let cache_one_syntax_extension se = Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) Egramcoq.extend_constr_grammar prec se.synext_notgram; - (* Declare the printing rule *) - Notation.declare_notation_printing_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) + (* Declare the notation rule *) + Notation.declare_notation_rule ntn + ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram let cache_syntax_extension (_, (_, sy)) = List.iter cache_one_syntax_extension sy @@ -1063,7 +1063,7 @@ let recover_syntax ntn = let prec = Notation.level_of_notation ntn in let pp_rule,_ = Notation.find_notation_printing_rule ntn in let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in - let pa_rule = Egramcoq.recover_constr_grammar ntn prec in + let pa_rule = Notation.find_notation_parsing_rules ntn in { synext_level = prec; synext_notation = ntn; synext_notgram = pa_rule; |