diff options
| -rw-r--r-- | coqpp/coqpp_main.ml | 2 | ||||
| -rw-r--r-- | gramlib/grammar.ml | 85 | ||||
| -rw-r--r-- | gramlib/grammar.mli | 5 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 18 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 2 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 2 |
6 files changed, 51 insertions, 63 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 17f81c555c..0e0aefaaef 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -253,7 +253,7 @@ and print_symbol fmt tkn = match tkn with fprintf fmt "Pcoq.G.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body) in let pr fmt rules = print_list fmt pr rules in - fprintf fmt "(Pcoq.G.Symbol.rules ~warning:None %a)" pr (List.rev rules) + fprintf fmt "(Pcoq.G.Symbol.rules %a)" pr (List.rev rules) | SymbQuote c -> fprintf fmt "(%s)" c diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index ac6f752670..814844508b 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -63,7 +63,7 @@ module type S = sig val self : ('self, mayrec, 'self) t val next : ('self, mayrec, 'self) t val token : 'c pattern -> ('self, norec, 'c) t - val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t + val rules : 'a Rules.t list -> ('self, norec, 'a) t end and Rule : sig @@ -101,7 +101,7 @@ module type S = sig ; data : 'a single_extend_statement list } - val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit + val safe_extend : 'a Entry.t -> 'a extend_statement -> unit val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option @@ -348,7 +348,7 @@ let and_and_tree (type s tr' trt tr trn trs trb f) (ar : (tr', trt, tr) ty_and_r | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2 | NoRec2, NoRec3, NoRec -> NoRec2 -let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree = +let insert_tree (type s trs trt tr p k a) entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree = let rec insert : type trs trt tr p f k. (trs, trt, tr) ty_and_ex -> (s, trs, p) ty_symbols -> (p, k, f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree = fun ar symbols pf tree action -> match symbols, pf with @@ -362,15 +362,15 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t | NR10, Node (_, n) -> Node (MayRec3, node n) | NR11, Node (NoRec3, n) -> Node (NoRec3, node n) | NR11, LocAct (old_action, action_list) -> - begin match warning with - | None -> () - | Some warn_fn -> + (* What to do about this warning? For now it is disabled *) + if false then + begin let msg = "<W> Grammar extension: " ^ (if entry_name = "" then "" else "in ["^entry_name^"%s], ") ^ "some rule has been masked" in - warn_fn msg - end; + Feedback.msg_warning (Pp.str msg) + end; LocAct (action, old_action :: action_list) | NR11, DeadEnd -> LocAct (action, []) and insert_in_tree : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_ex -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree = @@ -429,14 +429,14 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t in insert ar gsymbols pf tree action -let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree = - insert_tree ~warning entry_name NR11 gsymbols pf action tree +let insert_tree_norec (type s p k a) entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree = + insert_tree entry_name NR11 gsymbols pf action tree -let insert_tree (type s trs trt p k a) ~warning entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree = +let insert_tree (type s trs trt p k a) entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree = let MayRecNR ar = and_symbols_tree gsymbols tree in - MayRecTree (insert_tree ~warning entry_name ar gsymbols pf action tree) + MayRecTree (insert_tree entry_name ar gsymbols pf action tree) -let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_symbol = +let srules (type self a) (rl : a ty_rules list) : (self, norec, a) ty_symbol = let rec retype_tree : type s a. (s, norec, a) ty_tree -> (self, norec, a) ty_tree = function | Node (NoRec3, {node = s; son = son; brother = bro}) -> @@ -463,7 +463,7 @@ let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_s (fun tree (TRules (symbols, action)) -> let symbols = retype_rule symbols in let AnyS (symbols, pf) = get_symbols symbols in - insert_tree_norec ~warning "" symbols pf action tree) + insert_tree_norec "" symbols pf action tree) DeadEnd rl in Stree t @@ -473,19 +473,19 @@ let is_level_labelled n (Level lev) = Some n1 -> n = n1 | None -> false -let insert_level (type s tr p k) ~warning entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level = +let insert_level (type s tr p k) entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level = match symbols with | TCns (_, Sself, symbols) -> let Level slev = slev in let RelS pf = pf in - let MayRecTree lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix in + let MayRecTree lsuffix = insert_tree entry_name symbols pf action slev.lsuffix in Level {assoc = slev.assoc; lname = slev.lname; lsuffix = lsuffix; lprefix = slev.lprefix} | _ -> let Level slev = slev in - let MayRecTree lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix in + let MayRecTree lprefix = insert_tree entry_name symbols pf action slev.lprefix in Level {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; lprefix = lprefix} @@ -499,34 +499,27 @@ let empty_lev lname assoc = Level {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} -let change_lev ~warning (Level lev) n lname assoc = +let change_lev (Level lev) n lname assoc = let a = match assoc with None -> lev.assoc | Some a -> if a <> lev.assoc then - begin - match warning with - | None -> () - | Some warn_fn -> - warn_fn ("<W> Changing associativity of level \""^n^"\"") - end; - a + Feedback.msg_warning (Pp.str ("<W> Changing associativity of level \""^n^"\"")); + a in - begin match lname with - Some n -> - if lname <> lev.lname then - begin match warning with - | None -> () - | Some warn_fn -> - warn_fn ("<W> Level label \""^n^"\" ignored") - end; - | None -> () + begin + match lname with + | Some n -> + (* warning disabled; it was in the past *) + if false && lname <> lev.lname then + Feedback.msg_warning (Pp.str ("<W> Level label \""^n^"\" ignored")) + | None -> () end; Level {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} -let get_level ~warning entry position levs = +let get_level entry position levs = match position with Some First -> [], empty_lev, levs | Some Last -> levs, empty_lev, [] @@ -539,7 +532,7 @@ let get_level ~warning entry position levs = flush stderr; failwith "Grammar.extend" | lev :: levs -> - if is_level_labelled n lev then [], change_lev ~warning lev n, levs + if is_level_labelled n lev then [], change_lev lev n, levs else let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 in @@ -574,7 +567,7 @@ let get_level ~warning entry position levs = get levs | None -> match levs with - lev :: levs -> [], change_lev ~warning lev "<top>", levs + lev :: levs -> [], change_lev lev "<top>", levs | [] -> [], empty_lev, [] let change_to_self0 (type s) (type trec) (type a) (entry : s ty_entry) : (s, trec, a) ty_symbol -> (s, a) ty_mayrec_symbol = @@ -624,7 +617,7 @@ let insert_tokens gram symbols = in linsert symbols -let levels_of_rules ~warning entry position rules = +let levels_of_rules entry position rules = let elev = match entry.edesc with Dlevels elev -> elev @@ -636,7 +629,7 @@ let levels_of_rules ~warning entry position rules = match rules with | [] -> elev | _ -> - let (levs1, make_lev, levs2) = get_level ~warning entry position elev in + let (levs1, make_lev, levs2) = get_level entry position elev in let (levs, _) = List.fold_left (fun (levs, make_lev) (lname, assoc, level) -> @@ -647,7 +640,7 @@ let levels_of_rules ~warning entry position rules = let MayRecRule symbols = change_to_self entry symbols in let AnyS (symbols, pf) = get_symbols symbols in insert_tokens egram symbols; - insert_level ~warning entry.ename symbols pf action lev) + insert_level entry.ename symbols pf action lev) lev level in lev :: levs, empty_lev) @@ -1503,8 +1496,8 @@ let init_entry_functions entry = let f = continue_parser_of_entry entry in entry.econtinue <- f; f lev bp a strm) -let extend_entry ~warning entry position rules = - let elev = levels_of_rules ~warning entry position rules in +let extend_entry entry position rules = + let elev = levels_of_rules entry position rules in entry.edesc <- Dlevels elev; init_entry_functions entry (* Deleting a rule *) @@ -1630,7 +1623,7 @@ module rec Symbol : sig val self : ('self, mayrec, 'self) t val next : ('self, mayrec, 'self) t val token : 'c pattern -> ('self, norec, 'c) t - val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t + val rules : 'a Rules.t list -> ('self, norec, 'a) t end = struct @@ -1645,7 +1638,7 @@ end = struct let self = Sself let next = Snext let token tok = Stoken tok - let rules ~warning (t : 'a Rules.t list) = srules ~warning t + let rules (t : 'a Rules.t list) = srules t end and Rule : sig @@ -1705,8 +1698,8 @@ type 'a extend_statement = ; data : 'a single_extend_statement list } -let safe_extend ~warning (e : 'a Entry.t) { pos; data } = - extend_entry ~warning e pos data +let safe_extend (e : 'a Entry.t) { pos; data } = + extend_entry e pos data let safe_delete_rule e (TProd (r,_act)) = let AnyS (symbols, _) = get_symbols r in diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 7738e32cab..16e147de3b 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -30,7 +30,6 @@ module type GLexerType = sig end end - type norec type mayrec @@ -73,7 +72,7 @@ module type S = sig val self : ('self, mayrec, 'self) t val next : ('self, mayrec, 'self) t val token : 'c pattern -> ('self, norec, 'c) t - val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t + val rules : 'a Rules.t list -> ('self, norec, 'a) t end and Rule : sig @@ -111,7 +110,7 @@ module type S = sig ; data : 'a single_extend_statement list } - val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit + val safe_extend : 'a Entry.t -> 'a extend_statement -> unit val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 59f92e7790..fe280c1f69 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -127,25 +127,24 @@ let grammar_delete_reinit e reinit ({ G.pos; data } as d)= | Some (Gramext.Level n) -> n | _ -> assert false in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in - G.safe_extend ~warning:(Some warning) e ext + G.safe_extend e ext (** Extension *) let grammar_extend e ext = let undo () = grammar_delete e ext in - let redo () = G.safe_extend ~warning:None e ext in + let redo () = G.safe_extend e ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e ext = camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state; - G.safe_extend ~warning:None e ext + G.safe_extend e ext let grammar_extend_sync_reinit e reinit ext = camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state; - G.safe_extend ~warning:None e ext + G.safe_extend e ext (** Remove extensions @@ -189,18 +188,16 @@ let eoi_entry en = let e = G.Entry.make ((G.Entry.name en) ^ "_eoi") in let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in let act = fun _ x loc -> x in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - G.safe_extend ~warning:(Some warning) e ext; + G.safe_extend e ext; e let map_entry f en = let e = G.Entry.make ((G.Entry.name en) ^ "_map") in let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in let act = fun x loc -> f x in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in - G.safe_extend ~warning:(Some warning) e ext; + G.safe_extend e ext; e (* Parse a string, does NOT check if the entire string was read @@ -348,9 +345,8 @@ module Module = let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) = let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in let entry = G.Entry.make "epsilon" in - let warning msg = Feedback.msg_warning Pp.(str msg) in let ext = { G.pos = None; data = [None, None, [r]] } in - let () = G.safe_extend ~warning:(Some warning) entry ext in + let () = G.safe_extend entry ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 920be6db5b..ab660b486e 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1614,7 +1614,7 @@ let rec make_seq_rule = function let () = add_scope "seq" begin fun toks -> let scope = let Seqrule (r, c) = make_seq_rule (List.rev toks) in - Pcoq.G.(Symbol.rules ~warning:None [Rules.make r (apply c [])]) + Pcoq.G.(Symbol.rules [Rules.make r (apply c [])]) in Tac2entries.ScopeRule (scope, (fun e -> e)) end diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 7a52f53dc0..c4f15a40ce 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -329,7 +329,7 @@ let make_sep_rules = function Pcoq.G.Symbol.token tk | tkl -> let r = Pcoq.G.mk_rule (List.rev tkl) in - Pcoq.G.Symbol.rules ~warning:None [r] + Pcoq.G.Symbol.rules [r] type ('s, 'a) mayrec_symbol = | MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol |