diff options
| -rw-r--r-- | intf/vernacexpr.mli | 14 | ||||
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 114 | ||||
| -rw-r--r-- | pretyping/arguments_renaming.ml | 8 | ||||
| -rw-r--r-- | pretyping/arguments_renaming.mli | 6 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 25 | ||||
| -rw-r--r-- | printing/prettyp.ml | 4 | ||||
| -rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
| -rw-r--r-- | test-suite/output/Arguments.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 32 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 385 |
12 files changed, 344 insertions, 254 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 857287040..1336c92b6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -416,10 +416,12 @@ type vernac_expr = | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * - (vernac_argument_status list) list * - int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | - `DefaultImplicits ] list + vernac_argument_status list (* Main arguments status list *) * + (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * + int option (* Number of args to trigger reduction *) * + [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | + `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | + `DefaultImplicits ] list | VernacArgumentsScope of reference or_by_notation * scope_name option list | VernacReserve of simple_binder list @@ -479,11 +481,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_implicit_status = Implicit | MaximallyImplicit | NotImplicit + and vernac_argument_status = { name : Name.t; recarg_like : bool; notation_scope : (Loc.t * string) option; - implicit_status : [ `Implicit | `MaximallyImplicit | `NotImplicit]; + implicit_status : vernac_implicit_status; } (* A vernac classifier has to tell if a command: diff --git a/library/impargs.ml b/library/impargs.ml index bce7a15cb..a709aedee 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -494,7 +494,7 @@ let implicits_of_global ref = let rename imp name = match imp, name with | Some (_, x,y), Name id -> Some (id, x,y) | _ -> imp in - List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l + List.map (fun (t, il) -> t, List.map2 rename il rename_l) l with Not_found -> l | Invalid_argument _ -> anomaly (Pp.str "renamings list and implicits list have different lenghts") diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index bc02a4621..e0d836df8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -651,58 +651,29 @@ GEXTEND Gram (* Arguments *) | IDENT "Arguments"; qid = smart_global; - impl = LIST1 [ l = LIST0 - [ item = argument_spec -> - 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 (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 (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 (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = `MaximallyImplicit}) items - ] -> l ] SEP ","; + args = LIST0 argument_spec_block; + more_implicits = OPT + [ ","; impl = LIST1 + [ impl = LIST0 more_implicits_block -> List.flatten impl] + SEP "," -> impl + ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> let mods = match mods with None -> [] | Some l -> List.flatten l in - let impl = List.map List.flatten impl in - let rec aux n (narg, impl) = function - | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl - | `Slash :: tl -> aux (n+1) (n, impl) tl - | [] -> narg, impl in - let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in - let nargs, rest = List.hd nargs, List.tl nargs in - if List.exists (fun arg -> not (Int.equal arg nargs)) rest then - error "All arguments lists must have the same length"; - let err_incompat x y = - error ("Options \""^x^"\" and \""^y^"\" are incompatible") in - if nargs > 0 && List.mem `ReductionNeverUnfold mods then - err_incompat "simpl never" "/"; - if List.mem `ReductionNeverUnfold mods && - List.mem `ReductionDontExposeCase mods then - err_incompat "simpl never" "simpl nomatch"; - VernacArguments (qid, impl, nargs, mods) - + let slash_position = ref None in + let rec parse_args i = function + | [] -> [] + | `Id x :: args -> x :: parse_args (i+1) args + | `Slash :: args -> + if Option.is_empty !slash_position then + (slash_position := Some i; parse_args i args) + else + error "The \"/\" modifier can occur only once" + in + let args = parse_args 0 (List.flatten args) in + let more_implicits = Option.default [] more_implicits in + VernacArguments (qid, args, more_implicits, !slash_position, mods) + + (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> @@ -759,6 +730,49 @@ GEXTEND Gram snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s ] ]; + (* List of arguments implicit status, scope, modifiers *) + argument_spec_block: [ + [ item = argument_spec -> + 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 (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 (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 (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = MaximallyImplicit}) items + ] + ]; + (* Same as [argument_spec_block], but with only implicit status and names *) + more_implicits_block: [ + [ name = name -> [(snd name, Vernacexpr.NotImplicit)] + | "["; items = LIST1 name; "]" -> + List.map (fun name -> (snd name, Vernacexpr.Implicit)) items + | "{"; items = LIST1 name; "}" -> + List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items + ] + ]; strategy_level: [ [ IDENT "expand" -> Conv_oracle.Expand | IDENT "opaque" -> Conv_oracle.Opaque diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ca1d0b7fb..e18aece09 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -16,12 +16,12 @@ open Libobject (*i*) let name_table = - Summary.ref (Refmap.empty : Name.t list list Refmap.t) + Summary.ref (Refmap.empty : Name.t list Refmap.t) ~name:"rename-arguments" type req = | ReqLocal - | ReqGlobal of global_reference * Name.t list list + | ReqGlobal of global_reference * Name.t list let load_rename_args _ (_, (_, (r, names))) = name_table := Refmap.add r names !name_table @@ -49,7 +49,7 @@ let discharge_rename_args = function let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fun (id, _,_,_) -> Name id) vars in - let names' = List.map (fun l -> var_names @ l) names in + let names' = var_names @ names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) | _ -> None @@ -83,7 +83,7 @@ let rec rename_prod c = function | _ -> c let rename_type ty ref = - try rename_prod ty (List.hd (arguments_names ref)) + try rename_prod ty (arguments_names ref) with Not_found -> ty let rename_type_of_constant env c = diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index a33405501..e123e7786 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -11,10 +11,10 @@ open Globnames open Environ open Term -val rename_arguments : bool -> global_reference -> Name.t list list -> unit +val rename_arguments : bool -> global_reference -> Name.t list -> unit -(** [Not_found] is raised is no names are defined for [r] *) -val arguments_names : global_reference -> Name.t list list +(** [Not_found] is raised if no names are defined for [r] *) +val arguments_names : global_reference -> Name.t list val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cfb4e79f0..5455ab891 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1023,7 +1023,7 @@ module Make str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") impls) ) - | VernacArguments (q, impl, nargs, mods) -> + | VernacArguments (q, args, more_implicits, nargs, mods) -> return ( hov 2 ( keyword "Arguments" ++ spc() ++ @@ -1031,19 +1031,28 @@ module Make 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 x = match imp with - | `Implicit -> str "[" ++ x ++ str "]" - | `MaximallyImplicit -> str "{" ++ x ++ str "}" - | `NotImplicit -> x in - let rec aux n l = + | Vernacexpr.Implicit -> str "[" ++ x ++ str "]" + | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}" + | Vernacexpr.NotImplicit -> x in + let rec print_arguments n l = match n, l with - | 0, l -> spc () ++ str"/" ++ aux ~-1 l + | Some 0, l -> spc () ++ str"/" ++ print_arguments None l | _, [] -> mt() | 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 ++ + print_arguments (Option.map pred n) tl + in + let rec print_implicits = function + | [] -> mt () + | (name, impl) :: rest -> + spc() ++ pr_br impl (pr_name name) ++ print_implicits rest + in + print_arguments nargs args ++ + if not (List.is_empty more_implicits) then + str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits + else (mt ()) ++ (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function | `ReductionDontExposeCase -> keyword "simpl nomatch" diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f71719cb9..b590a8c93 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -241,7 +241,7 @@ let print_name_infos ref = let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in let renames = - try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in + try Arguments_renaming.arguments_names ref with Not_found -> [] in let type_info_for_implicit = if need_expansion (select_impargs_size 0 impls) ref then (* Need to reduce since implicits are computed with products flattened *) @@ -281,7 +281,7 @@ let print_inductive_implicit_args = let print_inductive_renames = print_args_data_of_inductive_ids (fun r -> - try List.hd (Arguments_renaming.arguments_names r) with Not_found -> []) + try Arguments_renaming.arguments_names r with Not_found -> []) ((!=) Anonymous) print_renames_list diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b8c07512f..b99d80e95 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 2c7b04c62..a2ee2d4c8 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra argument _. +Error: Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1633ad976..8c5efcd89 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,20 +1,12 @@ -File "stdin", line 1, characters 0-36: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: To rename arguments the "rename" flag must be +specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: -Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] -File "stdin", 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 "stdin", line 4, characters 0-40: -Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Warning: This command is just asserting the 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] @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -112,18 +104,16 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: All arguments lists must declare the same names. +Error: Arguments lists should agree on names they provide. The command has indeed failed with message: -Error: The following arguments are not declared: x. +Error: Sequences of implicit arguments must be of different lengths The command has indeed failed with message: Error: Arguments names must be distinct. 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 "stdin", line 53, characters 0-26: -Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. -[arguments-ignore-rename-nonimpl,vernacular] +Error: Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +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 e42c98336..2d14c94ac 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. -Arguments identity T _ _. +Arguments identity A _ _. Arguments eq_refl A x : assert. Arguments eq_refl {B y}, [B] y : rename. @@ -46,9 +46,9 @@ About myplus. Check @myplus. Fail Arguments eq_refl {F g}, [H] k. -Fail Arguments eq_refl {F}, [F]. +Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F. -Fail Arguments eq {F} x [z]. +Fail Arguments eq {F} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index feec23b50..8a2caa446 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -973,182 +973,255 @@ let vernac_declare_implicits locality r l = let warn_arguments_assert = CWarnings.create ~name:"arguments-assert" ~category:"vernacular" (fun sr -> - strbrk "This command is just asserting the number and names of arguments of " ++ + strbrk "This command is just asserting the names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add " ++ strbrk "': assert' to silence the warning. If you want " ++ 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-ignore-rename-nonimpl" - ~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 { name } -> name)) l in - let names, rest = List.hd names, List.tl names 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)) - then error "Arguments names must be distinct."; - let sr = smart_global r in + +(* [nargs_for_red] is the number of arguments required to trigger reduction, + [args] is the main list of arguments statuses, + [more_implicits] is a list of extra lists of implicit statuses *) +let vernac_arguments locality reference args more_implicits nargs_for_red flags = + let assert_flag = List.mem `Assert flags in + let rename_flag = List.mem `Rename flags in + let clear_scopes_flag = List.mem `ClearScopes flags in + let extra_scopes_flag = List.mem `ExtraScopes flags in + let clear_implicits_flag = List.mem `ClearImplicits flags in + let default_implicits_flag = List.mem `DefaultImplicits flags in + let never_unfold_flag = List.mem `ReductionNeverUnfold flags in + + let err_incompat x y = + error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in + + if assert_flag && rename_flag then + err_incompat "assert" "rename"; + if Option.has_some nargs_for_red && never_unfold_flag then + err_incompat "simpl never" "/"; + if never_unfold_flag && List.mem `ReductionDontExposeCase flags then + err_incompat "simpl never" "simpl nomatch"; + if clear_scopes_flag && extra_scopes_flag then + err_incompat "clear scopes" "extra scopes"; + if clear_implicits_flag && default_implicits_flag then + err_incompat "clear implicits" "default implicits"; + + let sr = smart_global reference in let inf_names = let ty = Global.type_of_global_unsafe sr in - Impargs.compute_implicits_names (Global.env ()) ty in - let rec check li ld ls = match li, ld, ls with - | [], [], [] -> () - | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls - | [], _::_, (Some _)::ls when extra_scope_flag -> - error "Extra notation scopes can be set on anonymous arguments only" - | [], x::_, _ -> errorlabstrm "vernac_declare_arguments" - (str "Extra argument " ++ pr_name x ++ str ".") - | l, [], _ -> errorlabstrm "vernac_declare_arguments" - (str "The following arguments are not declared: " ++ - prlist_with_sep pr_comma pr_name l ++ str ".") - | _::li, _::ld, _::ls -> check li ld ls - | _ -> assert false in - let () = match l with - | [[]] when List.exists ((<>) `Assert) flags || - (* Arguments f /. used to be allowed by mistake *) - (Flags.version_less_or_equal Flags.V8_5 && nargs >= 0) -> () - | _ -> - List.iter2 (check inf_names) (names :: rest) scopes + Impargs.compute_implicits_names (Global.env ()) ty in - (* we take extra scopes apart, and we check they are consistent *) - let l, scopes = - let scopes, rest = List.hd scopes, List.tl scopes in - if List.exists (List.exists ((!=) None)) rest then - error "Notation scopes can be given only once"; - if not extra_scope_flag then l, scopes else - let l, _ = List.split (List.map (List.chop (List.length inf_names)) l) in - l, scopes in - (* we interpret _ as the inferred names *) - let l = match l with - | [[]] -> l - | _ -> - let name_anons = function - | { 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 { 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) + let prev_names = + try Arguments_renaming.arguments_names sr with Not_found -> inf_names in - let some_renaming_specified = - try - let names = Arguments_renaming.arguments_names sr in - not (List.equal (List.equal Name.equal) names names_decl) - with Not_found -> false in - let some_renaming_specified, implicits = - match l with - | [[]] -> false, [[]] + let num_args = List.length inf_names in + assert (Int.equal num_args (List.length prev_names)); + + let names_of args = List.map (fun a -> a.name) args in + + (* Checks *) + + let err_extra_args names = + errorlabstrm "vernac_declare_arguments" + (strbrk "Extra arguments: " ++ + prlist_with_sep pr_comma pr_name names ++ str ".") + in + let err_missing_args names = + errorlabstrm "vernac_declare_arguments" + (strbrk "The following arguments are not declared: " ++ + prlist_with_sep pr_comma pr_name names ++ str ".") + in + + let rec check_extra_args extra_args = + match extra_args with + | [] -> () + | { notation_scope = None } :: _ -> err_extra_args (names_of extra_args) + | { name = Anonymous; notation_scope = Some _ } :: args -> + check_extra_args args | _ -> - 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" - (str "To rename arguments the \"rename\" flag must be specified." ++ - match !renamed_arg with - | None -> mt () - | Some (o,n) -> - str "\nArgument " ++ pr_id o ++ - str " renamed to " ++ pr_id n ++ str ".") - else - Arguments_renaming.rename_arguments - (make_section_locality locality) sr names_decl; - (* All other infos are in the first item of l *) - let l = List.hd l in - let scopes = List.map (function - | None -> None - | Some (o, k) -> - try ignore (Notation.find_scope k); Some k - with UserError _ -> - Some (Notation.find_delimiters_scope o k)) scopes + error "Extra notation scopes can be set on anonymous and explicit arguments only." + in + + let args, scopes = + let scopes = List.map (fun { notation_scope = s } -> s) args in + if List.length args > num_args then + let args, extra_args = List.chop num_args args in + if extra_scopes_flag then + (check_extra_args extra_args; (args, scopes)) + else err_extra_args (names_of extra_args) + else args, scopes + in + + if Option.cata (fun n -> n > num_args) false nargs_for_red then + error "The \"/\" modifier should be put before any extra scope."; + + let scopes_specified = List.exists Option.has_some scopes in + + if scopes_specified && clear_scopes_flag then + error "The \"clear scopes\" flag is incompatible with scope annotations."; + + let names = List.map (fun { name } -> name) args in + let names = names :: List.map (List.map fst) more_implicits in + + let rename_flag_required = ref false in + let example_renaming = ref None in + let save_example_renaming renaming = + rename_flag_required := !rename_flag_required + || not (Name.equal (fst renaming) Anonymous); + if Option.is_empty !example_renaming then + example_renaming := Some renaming + in + + let rec names_union names1 names2 = + match names1, names2 with + | [], [] -> [] + | _ :: _, [] -> names1 + | [], _ :: _ -> names2 + | (Name _ as name) :: names1, Anonymous :: names2 + | Anonymous :: names1, (Name _ as name) :: names2 -> + name :: names_union names1 names2 + | name1 :: names1, name2 :: names2 -> + if Name.equal name1 name2 then + name1 :: names_union names1 names2 + else error "Arguments lists should agree on names they provide." + in + + let initial = List.make num_args Anonymous in + let names = List.fold_left names_union initial names in + + let rec rename prev_names names = + match prev_names, names with + | [], [] -> [] + | [], _ :: _ -> err_extra_args names + | _ :: _, [] when assert_flag -> + (* Error messages are expressed in terms of original names, not + renamed ones. *) + err_missing_args (List.lastn (List.length prev_names) inf_names) + | _ :: _, [] -> prev_names + | prev :: prev_names, Anonymous :: names -> + prev :: rename prev_names names + | prev :: prev_names, (Name id as name) :: names -> + if not (Name.equal prev name) then save_example_renaming (prev,name); + name :: rename prev_names names + in + + let names = rename prev_names names in + let renaming_specified = Option.has_some !example_renaming in + + if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names)) then + error "Arguments names must be distinct."; + + if !rename_flag_required && not rename_flag then + errorlabstrm "vernac_declare_arguments" + (strbrk "To rename arguments the \"rename\" flag must be specified." + ++ + match !example_renaming with + | None -> mt () + | Some (o,n) -> + str "\nArgument " ++ pr_name o ++ + str " renamed to " ++ pr_name n ++ str "."); + + + (* Parts of this code are overly complicated because the implicit arguments + API is completely crazy: positions (ExplByPos) are elaborated to + names. This is broken by design, since not all arguments have names. So + eventhough we eventually want to map only positions to implicit statuses, + we have to check whether the corresponding arguments have names, not to + trigger an error in the impargs code. Even better, the names we have to + check are not the current ones (after previous renamings), but the original + ones (inferred from the type). *) + + let implicits = + List.map (fun { name; implicit_status = i } -> (name,i)) args + in + let implicits = implicits :: more_implicits in + + let open Vernacexpr in + let rec build_implicits inf_names implicits = + match inf_names, implicits with + | _, [] -> [] + | _ :: inf_names, (_, NotImplicit) :: implicits -> + build_implicits inf_names implicits + + (* With the current impargs API, it is impossible to make an originally + anonymous argument implicit *) + | Anonymous :: _, (name, _) :: _ -> + errorlabstrm "vernac_declare_arguments" + (strbrk"Argument "++ pr_name name ++ + strbrk " cannot be declared implicit.") + + | Name id :: inf_names, (name, impl) :: implicits -> + let max = impl = MaximallyImplicit in + (ExplByName id,max,false) :: build_implicits inf_names implicits + + | _ -> assert false (* already checked in [names_union] *) in - let some_scopes_specified = List.exists ((!=) None) scopes in + + let implicits = List.map (build_implicits inf_names) implicits in + let implicits_specified = match implicits with [[]] -> false | _ -> true in + + if implicits_specified && clear_implicits_flag then + error "The \"clear implicits\" flag is incompatible with implicit annotations"; + + if implicits_specified && default_implicits_flag then + error "The \"default implicits\" flag is incompatible with implicit annotations"; + let rargs = Util.List.map_filter (function (n, true) -> Some n | _ -> None) - (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 - vernac_declare_implicits locality r [] - else if some_implicits_specified || List.mem `ClearImplicits flags then - vernac_declare_implicits locality r implicits; - if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then - error "The \"/\" option must be placed after the last \"!\"."; - let no_flags = List.is_empty flags in + (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) + in + let rec narrow = function | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl - | [] -> [] | _ :: tl -> narrow tl in - let flags = narrow flags in - let some_simpl_flags_specified = - not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) in - if some_simpl_flags_specified then begin + | [] -> [] | _ :: tl -> narrow tl + in + let red_flags = narrow flags in + let red_modifiers_specified = + not (List.is_empty rargs) || Option.has_some nargs_for_red + || not (List.is_empty red_flags) + in + + if not (List.is_empty rargs) && never_unfold_flag then + err_incompat "simpl never" "!"; + + + (* Actions *) + + if renaming_specified then begin + let local = make_section_locality locality in + Arguments_renaming.rename_arguments local sr names + end; + + if scopes_specified || clear_scopes_flag then begin + let scopes = List.map (Option.map (fun (o,k) -> + try ignore (Notation.find_scope k); k + with UserError _ -> + Notation.find_delimiters_scope o k)) scopes + in + vernac_arguments_scope locality reference scopes + end; + + if implicits_specified || clear_implicits_flag then + vernac_declare_implicits locality reference implicits; + + if default_implicits_flag then + vernac_declare_implicits locality reference []; + + if red_modifiers_specified then begin match sr with | ConstRef _ as c -> Reductionops.ReductionBehaviour.set - (make_section_locality locality) c (rargs, nargs, flags) + (make_section_locality locality) c + (rargs, Option.default ~-1 nargs_for_red, red_flags) | _ -> 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 || - some_scopes_specified || - some_simpl_flags_specified) && - no_flags then - warn_arguments_assert sr + if not (renaming_specified || + implicits_specified || + scopes_specified || + red_modifiers_specified) && (List.is_empty flags) then + warn_arguments_assert sr let default_env () = { Notation_term.ninterp_var_type = Id.Map.empty; @@ -1920,8 +1993,8 @@ let interp ?proof ~loc locality poly c = vernac_syntactic_definition locality id c local b | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits locality qid l - | VernacArguments (qid, l, narg, flags) -> - vernac_declare_arguments locality qid l narg flags + | VernacArguments (qid, args, more_implicits, nargs, flags) -> + vernac_arguments locality qid args more_implicits nargs flags | VernacReserve bl -> vernac_reserve bl | VernacGeneralizable gen -> vernac_generalizable locality gen | VernacSetOpacity qidl -> vernac_set_opacity locality qidl |