diff options
| -rw-r--r-- | intf/vernacexpr.mli | 9 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 20 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 14 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3045.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3753.v (renamed from test-suite/bugs/opened/3753.v) | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 20 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 90 |
8 files changed, 115 insertions, 44 deletions
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/opened/3753.v b/test-suite/bugs/closed/3753.v index 05d77c831..5bfbee949 100644 --- a/test-suite/bugs/opened/3753.v +++ b/test-suite/bugs/closed/3753.v @@ -1,4 +1,4 @@ Axiom foo : Type -> Type. Axiom bar : forall (T : Type), T -> foo T. Arguments bar A x : rename. -Fail About bar. +About bar.
\ No newline at end of file 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 || |