From 9615c025a2a09b69f2001d44a66a1fddef74e680 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 29 Sep 2016 15:51:18 +0200 Subject: Fix bug #4869, allow Prop, Set, and level names in constraints. --- parsing/g_constr.ml4 | 6 +++--- parsing/g_vernac.ml4 | 4 ++-- parsing/pcoq.ml | 1 + parsing/pcoq.mli | 1 + 4 files changed, 7 insertions(+), 5 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 74994c5e3..7f3a3d10c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -127,7 +127,7 @@ let name_colon = let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr sort global + GLOBAL: binder_constr lconstr constr operconstr universe_level sort global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; @@ -298,10 +298,10 @@ GEXTEND Gram | -> [] ] ] ; instance: - [ [ "@{"; l = LIST1 level; "}" -> Some l + [ [ "@{"; l = LIST1 universe_level; "}" -> Some l | -> None ] ] ; - level: + universe_level: [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c09693b36..78176d934 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -226,8 +226,8 @@ GEXTEND Gram [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] ; univ_constraint: - [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; - r = identref -> (l, ord, r) ] ] + [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = universe_level -> (l, ord, r) ] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 714e25f85..4e069c9e3 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -304,6 +304,7 @@ module Constr = let binder_constr = gec_constr "binder_constr" let ident = make_gen_entry uconstr "ident" let global = make_gen_entry uconstr "global" + let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" let pattern = Gram.entry_create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 635b0170a..7f49c997f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -157,6 +157,7 @@ module Constr : val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry val global : reference Gram.entry + val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry -- cgit v1.2.3 From 601fd9343a241706c0a205aaf8e08255753c3780 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Sep 2016 15:23:07 +0200 Subject: Arguments: cleanup + detect discrepancy rename/implicit (#3753) It seems warnings are not taken into account in output/ tests. --- intf/vernacexpr.mli | 9 +++- parsing/g_vernac.ml4 | 20 +++++-- printing/ppvernac.ml | 14 ++--- test-suite/bugs/closed/3045.v | 2 +- test-suite/bugs/closed/3753.v | 4 ++ test-suite/bugs/opened/3753.v | 4 -- test-suite/output/Arguments_renaming.out | 20 +++++-- test-suite/output/Arguments_renaming.v | 2 +- toplevel/vernacentries.ml | 90 ++++++++++++++++++++++---------- 9 files changed, 118 insertions(+), 47 deletions(-) create mode 100644 test-suite/bugs/closed/3753.v delete mode 100644 test-suite/bugs/opened/3753.v (limited to 'parsing') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ed44704df..6df85f076 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -415,7 +415,7 @@ type vernac_expr = | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * - ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list * + (vernac_argument_status list) list * int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list @@ -477,6 +477,13 @@ and tacdef_body = | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) +and vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : (Loc.t * string) option; + implicit_status : [ `Implicit | `MaximallyImplicit | `NotImplicit]; +} + (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later vernac_type: if it is starts, ends, continues a proof or diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c09693b36..b0b656acf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -653,23 +653,35 @@ GEXTEND Gram | IDENT "Arguments"; qid = smart_global; impl = LIST1 [ l = LIST0 [ item = argument_spec -> - let id, r, s = item in [`Id (id,r,s,false,false)] + let name, recarg_like, notation_scope = item in + [`Id { name=name; recarg_like=recarg_like; + notation_scope=notation_scope; + implicit_status = `NotImplicit}] | "/" -> [`Slash] | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = `NotImplicit}) items | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = `Implicit}) items | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in - List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = `MaximallyImplicit}) items ] -> l ] SEP ","; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> let mods = match mods with None -> [] | Some l -> List.flatten l in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 40ce28dc0..1d8dcabcc 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1029,16 +1029,18 @@ module Make pr_smart_global q ++ let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in let pr_if b x = if b then x else str "" in - let pr_br imp max x = match imp, max with - | true, false -> str "[" ++ x ++ str "]" - | true, true -> str "{" ++ x ++ str "}" - | _ -> x in + let pr_br imp x = match imp with + | `Implicit -> str "[" ++ x ++ str "]" + | `MaximallyImplicit -> str "{" ++ x ++ str "}" + | `NotImplicit -> x in let rec aux n l = match n, l with | 0, l -> spc () ++ str"/" ++ aux ~-1 l | _, [] -> mt() - | n, (id,k,s,imp,max) :: tl -> - spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + | n, { name = id; recarg_like = k; + notation_scope = s; + implicit_status = imp } :: tl -> + spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ aux (n-1) tl in prlist_with_sep (fun () -> str", ") (aux nargs) impl ++ (if not (List.is_empty mods) then str" : " else str"") ++ diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v index ef110ad0d..5f80013df 100644 --- a/test-suite/bugs/closed/3045.v +++ b/test-suite/bugs/closed/3045.v @@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) := Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' }. -Arguments Compose {obj} [C s d d'] m1 m2 : rename. +Arguments Compose {obj} [C s d d'] _ _ : rename. Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. diff --git a/test-suite/bugs/closed/3753.v b/test-suite/bugs/closed/3753.v new file mode 100644 index 000000000..5bfbee949 --- /dev/null +++ b/test-suite/bugs/closed/3753.v @@ -0,0 +1,4 @@ +Axiom foo : Type -> Type. +Axiom bar : forall (T : Type), T -> foo T. +Arguments bar A x : rename. +About bar. \ No newline at end of file diff --git a/test-suite/bugs/opened/3753.v b/test-suite/bugs/opened/3753.v deleted file mode 100644 index 05d77c831..000000000 --- a/test-suite/bugs/opened/3753.v +++ /dev/null @@ -1,4 +0,0 @@ -Axiom foo : Type -> Type. -Axiom bar : forall (T : Type), T -> foo T. -Arguments bar A x : rename. -Fail About bar. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 3488cb305..815305581 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,9 +1,20 @@ +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 1, characters 0-36: +Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. +[arguments-assert,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to B. -The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. -Argument A renamed to T. +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. +[arguments-assert,vernacular] +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 2, characters 0-25: +Warning: This command is just asserting the number and names of arguments of +identity. If this is what you want add ': assert' to silence the warning. If +you want to clear implicit arguments add ': clear implicits'. If you want to +clear notation scopes add ': clear scopes' [arguments-assert,vernacular] +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 4, characters 0-40: +Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. +[arguments-assert,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -110,6 +121,9 @@ The command has indeed failed with message: Error: Argument z cannot be declared implicit. The command has indeed failed with message: Error: Extra argument y. +File "/home/gares/COQ/coq/test-suite/output/Arguments_renaming.v", line 53, characters 0-26: +Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. +[arguments-assert,vernacular] The command has indeed failed with message: Error: To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index b6fbeb6ec..e42c98336 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -1,5 +1,5 @@ Fail Arguments eq_refl {B y}, [B] y. -Fail Arguments identity T _ _. +Arguments identity T _ _. Arguments eq_refl A x : assert. Arguments eq_refl {B y}, [B] y : rename. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 25d16f91f..1d6278066 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -979,12 +979,17 @@ let warn_arguments_assert = strbrk "to clear implicit arguments add ': clear implicits'. " ++ strbrk "If you want to clear notation scopes add ': clear scopes'") +let warn_renaming_nonimplicit = + CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + (fun (oldn, newn) -> + strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++ + strbrk ". Only implicit arguments can be renamed.") let vernac_declare_arguments locality r l nargs flags = let extra_scope_flag = List.mem `ExtraScopes flags in - let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let names = List.map (List.map (fun { name } -> name)) l in let names, rest = List.hd names, List.tl names in - let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in + let scopes = List.map (List.map (fun { notation_scope = s } -> s)) l in if List.exists (fun na -> not (List.equal Name.equal na names)) rest then error "All arguments lists must declare the same names."; if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names)) @@ -1023,13 +1028,15 @@ let vernac_declare_arguments locality r l nargs flags = | [[]] -> l | _ -> let name_anons = function - | (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d + | { name = Anonymous } as x, Name id -> { x with name = Name id } | x, _ -> x in List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in - let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let names_decl = List.map (List.map (fun { name } -> name)) l in let renamed_arg = ref None in let set_renamed a b = - if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in + if Option.is_empty !renamed_arg && not (Id.equal a b) then + renamed_arg := Some(b,a) + in let some_renaming_specified = try let names = Arguments_renaming.arguments_names sr in @@ -1039,22 +1046,50 @@ let vernac_declare_arguments locality r l nargs flags = match l with | [[]] -> false, [[]] | _ -> - List.fold_map (fun sr il -> - let sr', impl = List.fold_map (fun b -> function - | (Anonymous, _,_, true, max), Name id -> assert false - | (Name x, _,_, true, _), Anonymous -> - errorlabstrm "vernac_declare_arguments" - (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.") - | (Name iid, _,_, true, max), Name id -> - set_renamed iid id; - b || not (Id.equal iid id), Some (ExplByName id, max, false) - | (Name iid, _,_, _, _), Name id -> - set_renamed iid id; - b || not (Id.equal iid id), None - | _ -> b, None) - sr (List.combine il inf_names) in - sr || sr', List.map_filter (fun x -> x) impl) - some_renaming_specified l in + let some_renaming = ref some_renaming_specified in + let rec aux il = + match il with + | [] -> [] + | il :: ils -> aux_single il inf_names :: aux ils + and aux_single impl inf_names = + match impl, inf_names with + | [], _ -> [] + | { name = Anonymous; + implicit_status = (`Implicit|`MaximallyImplicit)} :: _, + Name id :: _ -> + assert false + | { name = Name x; + implicit_status = (`Implicit|`MaximallyImplicit)} :: _, + Anonymous :: _ -> + errorlabstrm "vernac_declare_arguments" + (str"Argument "++ pr_id x ++str " cannot be declared implicit.") + | { name = Name iid; + implicit_status = (`Implicit|`MaximallyImplicit as i)} :: impl, + Name id :: inf_names -> + let max = i = `MaximallyImplicit in + set_renamed iid id; + some_renaming := !some_renaming || not (Id.equal iid id); + (ExplByName id,max,false) :: aux_single impl inf_names + | { name = Name iid } :: impl, + Name id :: inf_names when not (Id.equal iid id) -> + warn_renaming_nonimplicit (id, iid); + aux_single impl inf_names + | { name = Name iid } :: impl, Name id :: inf_names + when not (Id.equal iid id) -> + aux_single impl inf_names + | { name = Name iid } :: impl, Name id :: inf_names -> + set_renamed iid id; + some_renaming := !some_renaming || not (Id.equal iid id); + aux_single impl inf_names + | _ :: impl, _ :: inf_names -> + (* no rename, no implicit status *) aux_single impl inf_names + | _ :: _, [] -> assert false (* checked before in check() *) + in + !some_renaming, aux l in + (* We check if renamed arguments do match previously declared imp args, + * since the system has this invariant *) + let some_implicits_specified = + match implicits with [[]] -> false | _ -> true in if some_renaming_specified then if not (List.mem `Rename flags) then errorlabstrm "vernac_declare_arguments" @@ -1062,14 +1097,13 @@ let vernac_declare_arguments locality r l nargs flags = match !renamed_arg with | None -> mt () | Some (o,n) -> - str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".") + str "\nArgument " ++ pr_id o ++ + str " renamed to " ++ pr_id n ++ str ".") else Arguments_renaming.rename_arguments - (make_section_locality locality) sr names_decl; + (make_section_locality locality) sr names_decl; (* All other infos are in the first item of l *) let l = List.hd l in - let some_implicits_specified = match implicits with - | [[]] -> false | _ -> true in let scopes = List.map (function | None -> None | Some (o, k) -> @@ -1080,7 +1114,7 @@ let vernac_declare_arguments locality r l nargs flags = let some_scopes_specified = List.exists ((!=) None) scopes in let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) - (Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in + (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 l) in if some_scopes_specified || List.mem `ClearScopes flags then vernac_arguments_scope locality r scopes; if not some_implicits_specified && List.mem `DefaultImplicits flags then @@ -1101,7 +1135,9 @@ let vernac_declare_arguments locality r l nargs flags = | ConstRef _ as c -> Reductionops.ReductionBehaviour.set (make_section_locality locality) c (rargs, nargs, flags) - | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.") + | _ -> errorlabstrm "" + (strbrk "Modifiers of the behavior of the simpl tactic "++ + strbrk "are relevant for constants only.") end; if not (some_renaming_specified || some_implicits_specified || -- cgit v1.2.3 From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 27 Sep 2016 17:15:10 +0200 Subject: Fix bug #4798: compat notations should not modify the parser. This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data. --- ide/texmacspp.ml | 3 +- intf/vernacexpr.mli | 3 +- lib/flags.ml | 27 +++++++++------- lib/flags.mli | 1 + parsing/g_vernac.ml4 | 5 ++- printing/ppvernac.ml | 8 ++--- test-suite/bugs/closed/4798.v | 3 ++ toplevel/metasyntax.ml | 75 ++++++++++++++++++++++++++++--------------- 8 files changed, 80 insertions(+), 45 deletions(-) create mode 100644 test-suite/bugs/closed/4798.v (limited to 'parsing') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 53a29008a..9de1df9f1 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -189,7 +189,8 @@ match sm with end | SetEntryType (s, _) -> ["entrytype", s] | SetOnlyPrinting -> ["onlyprinting", ""] - | SetOnlyParsing v -> ["compat", Flags.pr_version v] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] | SetFormat (system, (loc, s)) -> let start, stop = unlock loc in ["format-"^system, s; "begin", start; "end", stop] diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 6df85f076..1063a74d9 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -211,8 +211,9 @@ type syntax_modifier = | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing of Flags.compat_version + | SetOnlyParsing | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version | SetFormat of string * string located type proof_end = diff --git a/lib/flags.ml b/lib/flags.ml index d29064c97..af55e9e2b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -112,17 +112,22 @@ type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current let compat_version = ref Current -let version_strictly_greater v = match !compat_version, v with -| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false -| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false -| V8_4, (V8_4 | V8_5 | Current) -> false -| V8_5, (V8_5 | Current) -> false -| Current, Current -> false -| V8_3, V8_2 -> true -| V8_4, (V8_2 | V8_3) -> true -| V8_5, (V8_2 | V8_3 | V8_4) -> true -| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true - +let version_compare v1 v2 = match v1, v2 with +| V8_2, V8_2 -> 0 +| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1 +| V8_3, V8_2 -> 1 +| V8_3, V8_3 -> 0 +| V8_3, (V8_4 | V8_5 | Current) -> -1 +| V8_4, (V8_2 | V8_3) -> 1 +| V8_4, V8_4 -> 0 +| V8_4, (V8_5 | Current) -> -1 +| V8_5, (V8_2 | V8_3 | V8_4) -> 1 +| V8_5, V8_5 -> 0 +| V8_5, Current -> -1 +| Current, Current -> 0 +| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1 + +let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function diff --git a/lib/flags.mli b/lib/flags.mli index 839c252cb..9dc0c9c04 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,6 +64,7 @@ val univ_print : bool ref type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current val compat_version : compat_version ref +val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b0b656acf..1a4012891 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1115,10 +1115,9 @@ GEXTEND Gram | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA | IDENT "only"; IDENT "printing" -> SetOnlyPrinting - | IDENT "only"; IDENT "parsing" -> - SetOnlyParsing Flags.Current + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> - SetOnlyParsing (Coqinit.get_compat_version s) + SetCompatVersion (Coqinit.get_compat_version s) | IDENT "format"; s1 = [s = STRING -> (!@loc,s)]; s2 = OPT [s = STRING -> (!@loc,s)] -> begin match s1, s2 with diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 1d8dcabcc..503b29aaf 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -367,8 +367,8 @@ module Make | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyPrinting -> keyword "only printing" - | SetOnlyParsing Flags.Current -> keyword "only parsing" - | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") + | SetOnlyParsing -> keyword "only parsing" + | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s @@ -1002,13 +1002,13 @@ module Make ) | VernacHints (_, dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> + | VernacSyntacticDefinition (id,(ids,c),_,compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) + (match compat with None -> [] | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v new file mode 100644 index 000000000..dbc3d46fc --- /dev/null +++ b/test-suite/bugs/closed/4798.v @@ -0,0 +1,3 @@ +Check match 2 with 0 => 0 | S n => n end. +Notation "|" := 1 (compat "8.4"). +Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a1edb7139..ce8798c71 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -673,8 +673,13 @@ type syntax_extension = { synext_notgram : notation_grammar; synext_unparsing : unparsing list; synext_extra : (string * string) list; + synext_compat : Flags.compat_version option; } +let is_active_compat = function +| None -> true +| Some v -> 0 <= Flags.version_compare v !Flags.compat_version + type syntax_extension_obj = locality_flag * syntax_extension list let cache_one_syntax_extension se = @@ -685,13 +690,15 @@ let cache_one_syntax_extension se = let oldprec = Notation.level_of_notation ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec with Not_found -> - (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; - (* Declare the parsing rule *) - if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; - (* Declare the notation rule *) - Notation.declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + if is_active_compat se.synext_compat then begin + (* Reserve the notation level *) + Notation.declare_notation_level ntn prec; + (* Declare the parsing rule *) + if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; + (* Declare the notation rule *) + Notation.declare_notation_rule ntn + ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + end let cache_syntax_extension (_, (_, sy)) = List.iter cache_one_syntax_extension sy @@ -725,9 +732,10 @@ let inSyntaxExtension : syntax_extension_obj -> obj = let interp_modifiers modl = let onlyparsing = ref false in let onlyprinting = ref false in + let compat = ref None in let rec interp assoc level etyps format extra = function | [] -> - (assoc,level,etyps,!onlyparsing,!onlyprinting,format,extra) + (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra) | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then @@ -749,12 +757,15 @@ let interp_modifiers modl = | SetAssoc a :: l -> if not (Option.is_empty assoc) then error"An associativity is given more than once."; interp (Some a) level etyps format extra l - | SetOnlyParsing _ :: l -> + | SetOnlyParsing :: l -> onlyparsing := true; interp assoc level etyps format extra l | SetOnlyPrinting :: l -> onlyprinting := true; interp assoc level etyps format extra l + | SetCompatVersion v :: l -> + compat := Some v; + interp assoc level etyps format extra l | SetFormat ("text",s) :: l -> if not (Option.is_empty format) then error "A format is given more than once."; interp assoc level etyps (Some s) extra l @@ -763,7 +774,7 @@ let interp_modifiers modl = in interp None None [] None [] modl let check_infix_modifiers modifiers = - let (_, _, t, _, _, _, _) = interp_modifiers modifiers in + let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in if not (List.is_empty t) then error "Explicit entry level or type unexpected in infix notation." @@ -775,20 +786,25 @@ let check_useless_entry_types recvars mainvars etyps = | _ -> () let not_a_syntax_modifier = function -| SetOnlyParsing _ -> true +| SetOnlyParsing -> true | SetOnlyPrinting -> true +| SetCompatVersion _ -> true | _ -> false let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods let is_only_parsing mods = - let test = function SetOnlyParsing _ -> true | _ -> false in + let test = function SetOnlyParsing -> true | _ -> false in List.exists test mods let is_only_printing mods = let test = function SetOnlyPrinting -> true | _ -> false in List.exists test mods +let get_compat_version mods = + let test = function SetCompatVersion v -> Some v | _ -> None in + try Some (List.find_map test mods) with Not_found -> None + (* Compute precedences from modifiers (or find default ones) *) let set_entry_type etyps (x,typ) = @@ -966,7 +982,7 @@ let remove_curly_brackets l = in aux true l let compute_syntax_data df modifiers = - let (assoc,n,etyps,onlyparse,onlyprint,fmt,extra) = interp_modifiers modifiers in + let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in let (recvars,mainvars,symbols) = analyze_notation_tokens toks in @@ -992,12 +1008,12 @@ let compute_syntax_data df modifiers = let sy_data = (n,sy_typs,symbols',fmt) in let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in - let i_data = (onlyparse,onlyprint,recvars,mainvars,(ntn_for_interp,df')) in + let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in (* Return relevant data for interpretation and for parsing/printing *) (msgs,i_data,i_typs,sy_fulldata,extra) let compute_pure_syntax_data df mods = - let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in + let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in let msgs = if onlyparse then (Feedback.msg_warning ?loc:None, @@ -1014,6 +1030,7 @@ type notation_obj = { notobj_interp : interpretation; notobj_onlyparse : bool; notobj_onlyprint : bool; + notobj_compat : Flags.compat_version option; notobj_notation : notation * notation_location; } @@ -1024,7 +1041,9 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin + let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in + let active = is_active_compat nobj.notobj_compat in + if Int.equal i 1 && fresh && active then begin (* Declare the interpretation *) let onlyprint = nobj.notobj_onlyprint in let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in @@ -1094,7 +1113,9 @@ let recover_syntax ntn = synext_notation = ntn; synext_notgram = pa_rule; synext_unparsing = pp_rule; - synext_extra = pp_extra_rules } + synext_extra = pp_extra_rules; + synext_compat = None; + } with Not_found -> raise NoSyntaxRule @@ -1128,7 +1149,7 @@ let make_pp_rule (n,typs,symbols,fmt) = | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) -let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint = +let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat = let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in let pp_rule = make_pp_rule sy_data in let sy = { @@ -1137,6 +1158,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint = synext_notgram = pa_rule; synext_unparsing = pp_rule; synext_extra = extra; + synext_compat = compat; } in (* By construction, the rule for "{ _ }" is declared, but we need to redeclare it because the file where it is declared needs not be open @@ -1153,9 +1175,9 @@ let to_map l = let add_notation_in_scope local df c mods scope = let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in (* Prepare the interpretation *) - let (onlyparse, onlyprint, recvars,mainvars, df') = i_data in + let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sy_data extra onlyprint in + let sy_rules = make_syntax_rules sy_data extra onlyprint compat in let i_vars = make_internalization_vars recvars mainvars i_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1173,6 +1195,7 @@ let add_notation_in_scope local df c mods scope = (** Order is important here! *) notobj_onlyparse = onlyparse; notobj_onlyprint = onlyprint; + notobj_compat = compat; notobj_notation = df'; } in (* Ready to change the global state *) @@ -1181,7 +1204,7 @@ let add_notation_in_scope local df c mods scope = Lib.add_anonymous_leaf (inNotation notation); df' -let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint = +let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) @@ -1212,6 +1235,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) (** Order is important here! *) notobj_onlyparse = onlyparse; notobj_onlyprint = onlyprint; + notobj_compat = compat; notobj_notation = df'; } in Lib.add_anonymous_leaf (inNotation notation); @@ -1221,19 +1245,19 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let add_syntax_extension local ((loc,df),mods) = let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in - let sy_rules = make_syntax_rules sy_data extra onlyprint in + let sy_rules = make_syntax_rules sy_data extra onlyprint None in Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) let add_notation_interpretation ((loc,df),c,sc) = - let df' = add_notation_interpretation_core false df c sc false false in + let df' = add_notation_interpretation_core false df c sc false false None in Dumpglob.dump_notation (loc,df') sc true let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore - (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false) ()); + (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> error "Parsing rule for this notation has to be previously declared."); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc @@ -1246,7 +1270,8 @@ let add_notation local c ((loc,df),modifiers) sc = (* No syntax data: try to rely on a previously declared rule *) let onlyparse = is_only_parsing modifiers in let onlyprint = is_only_printing modifiers in - try add_notation_interpretation_core local df c sc onlyparse onlyprint + let compat = get_compat_version modifiers in + try add_notation_interpretation_core local df c sc onlyparse onlyprint compat with NoSyntaxRule -> (* Try to determine a default syntax rule *) add_notation_in_scope local df c modifiers sc -- cgit v1.2.3 From 466b7e69e49a5f4bba36b834a2e046f120ece07c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 2 Oct 2016 12:02:53 +0200 Subject: Move bullet detection from lexer to parser (bug #5102). That way, bullet detection no longer depends on a global variable indicating whether a line is starting. This causes a small change in the recognized language. Before the commit, "--++" was recognized as a bullet "--" followed by a keyword "++" when at the start of a line; now it is always recognized as a keyword "--++". This also fixes a bug in Tok.to_string as a side-effect. --- parsing/cLexer.ml4 | 14 -------------- parsing/compat.ml4 | 1 - parsing/g_vernac.ml4 | 35 +++++++++++++++++++---------------- parsing/tok.ml | 7 ------- parsing/tok.mli | 1 - 5 files changed, 19 insertions(+), 39 deletions(-) (limited to 'parsing') diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index bec891f7f..fcdc37c08 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -479,14 +479,6 @@ let find_keyword loc id s = | None -> raise Not_found | Some c -> KEYWORD c -let process_sequence loc bp c cs = - let rec aux n cs = - match Stream.peek cs with - | Some c' when c == c' -> Stream.junk cs; aux (n+1) cs - | _ -> BULLET (String.make n c), set_loc_pos loc bp (Stream.count cs) - in - aux 1 cs - (* Must be a special token *) let process_chars loc bp c cs = let t = progress_from_byte loc None (-1) !token_tree cs c in @@ -552,12 +544,6 @@ let rec next_token loc = parser bp | _ -> () in (t, set_loc_pos loc bp ep) - | [< ' ('-'|'+'|'*' as c); s >] -> - let t,new_between_com = - if !between_com then process_sequence loc bp c s, true - else process_chars loc bp c s,false - in - comment_stop bp; between_com := new_between_com; t | [< ''?'; s >] ep -> let t = parse_after_qmark loc bp s in comment_stop bp; (t, set_loc_pos loc ep bp) diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 18bc8d664..5635eac7a 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -259,7 +259,6 @@ IFDEF CAMLP5 THEN | Tok.INT s -> "INT", s | Tok.STRING s -> "STRING", s | Tok.LEFTQMARK -> "LEFTQMARK", "" - | Tok.BULLET s -> "BULLET", s | Tok.EOI -> "EOI", "" in Gramext.Stoken pattern diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 50e469dd2..0f450ff9c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -33,8 +33,6 @@ let _ = List.iter CLexer.add_keyword vernac_kw let query_command = Gram.entry_create "vernac:query_command" -let subprf = Gram.entry_create "vernac:subprf" - let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" let thm_token = Gram.entry_create "vernac:thm_token" let def_body = Gram.entry_create "vernac:def_body" @@ -45,13 +43,25 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" -let make_bullet s = - let n = String.length s in - match s.[0] with - | '-' -> Dash n - | '+' -> Plus n - | '*' -> Star n - | _ -> assert false +let subprf = Gram.Entry.of_parser "vernac:subprf" (fun strm -> + match get_tok (Stream.peek strm) with + | Some (KEYWORD "{") -> Stream.junk strm; VernacSubproof None + | Some (KEYWORD "}") -> Stream.junk strm; VernacEndSubproof + | Some (KEYWORD k) -> + (match k.[0] with + | ('-'|'+'|'*') as c -> + let n = String.length k in + for i = 1 to n - 1 do + if k.[i] != c then raise Stream.Failure + done; + Stream.junk strm; + VernacBullet (match c with + | '-' -> Dash n + | '+' -> Plus n + | '*' -> Star n + | _ -> assert false) + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) GEXTEND Gram GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; @@ -102,13 +112,6 @@ GEXTEND Gram [ [ c = subgoal_command -> c None] ] ; - subprf: - [ [ s = BULLET -> VernacBullet (make_bullet s) - | "{" -> VernacSubproof None - | "}" -> VernacEndSubproof - ] ] - ; - subgoal_command: [ [ c = query_command; "." -> begin function diff --git a/parsing/tok.ml b/parsing/tok.ml index 8ae106512..99d5c972c 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -18,7 +18,6 @@ type t = | INT of string | STRING of string | LEFTQMARK - | BULLET of string | EOI let equal t1 t2 = match t1, t2 with @@ -30,7 +29,6 @@ let equal t1 t2 = match t1, t2 with | INT s1, INT s2 -> string_equal s1 s2 | STRING s1, STRING s2 -> string_equal s1 s2 | LEFTQMARK, LEFTQMARK -> true -| BULLET s1, BULLET s2 -> string_equal s1 s2 | EOI, EOI -> true | _ -> false @@ -42,7 +40,6 @@ let extract_string = function | FIELD s -> s | INT s -> s | LEFTQMARK -> "?" - | BULLET s -> s | EOI -> "" let to_string = function @@ -53,7 +50,6 @@ let to_string = function | INT s -> Format.sprintf "INT %s" s | STRING s -> Format.sprintf "STRING %S" s | LEFTQMARK -> "LEFTQMARK" - | BULLET s -> Format.sprintf "STRING %S" s | EOI -> "EOI" let match_keyword kwd = function @@ -75,7 +71,6 @@ let of_pattern = function | "INT", s -> INT s | "STRING", s -> STRING s | "LEFTQMARK", _ -> LEFTQMARK - | "BULLET", s -> BULLET s | "EOI", _ -> EOI | _ -> failwith "Tok.of_pattern: not a constructor" @@ -87,7 +82,6 @@ let to_pattern = function | INT s -> "INT", s | STRING s -> "STRING", s | LEFTQMARK -> "LEFTQMARK", "" - | BULLET s -> "BULLET", s | EOI -> "EOI", "" let match_pattern = @@ -100,7 +94,6 @@ let match_pattern = | "INT", "" -> (function INT s -> s | _ -> err ()) | "STRING", "" -> (function STRING s -> s | _ -> err ()) | "LEFTQMARK", "" -> (function LEFTQMARK -> "" | _ -> err ()) - | "BULLET", "" -> (function BULLET s -> s | _ -> err ()) | "EOI", "" -> (function EOI -> "" | _ -> err ()) | pat -> let tok = of_pattern pat in diff --git a/parsing/tok.mli b/parsing/tok.mli index b9286c53e..b1e79dc90 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -16,7 +16,6 @@ type t = | INT of string | STRING of string | LEFTQMARK - | BULLET of string | EOI val equal : t -> t -> bool -- cgit v1.2.3