diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 90 |
1 files changed, 63 insertions, 27 deletions
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 || |