aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli14
-rw-r--r--library/impargs.ml16
-rw-r--r--parsing/g_vernac.ml4114
-rw-r--r--pretyping/arguments_renaming.ml8
-rw-r--r--pretyping/arguments_renaming.mli6
-rw-r--r--printing/ppvernac.ml25
-rw-r--r--printing/prettyp.ml4
-rw-r--r--test-suite/.csdp.cachebin89077 -> 89077 bytes
-rw-r--r--test-suite/output/Arguments.out2
-rw-r--r--test-suite/output/Arguments_renaming.out32
-rw-r--r--test-suite/output/Arguments_renaming.v6
-rw-r--r--toplevel/vernacentries.ml385
12 files changed, 352 insertions, 260 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..828d652c8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -491,13 +491,15 @@ let implicits_of_global ref =
let l = Refmap.find ref !implicits_table in
try
let rename_l = Arguments_renaming.arguments_names ref in
- 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
+ let rec rename implicits names = match implicits, names with
+ | [], _ -> []
+ | _, [] -> implicits
+ | Some (_, x,y) :: implicits, Name id :: names ->
+ Some (id, x,y) :: rename implicits names
+ | imp :: implicits, _ :: names -> imp :: rename implicits names
+ in
+ List.map (fun (t, il) -> t, rename il rename_l) l
with Not_found -> l
- | Invalid_argument _ ->
- anomaly (Pp.str "renamings list and implicits list have different lenghts")
with Not_found -> [DefaultImpArgs,[]]
let cache_implicits_decl (ref,imps) =
@@ -657,7 +659,7 @@ let check_inclusion l =
let rec aux = function
| n1::(n2::_ as nl) ->
if n1 <= n2 then
- error "Sequences of implicit arguments must be of different lengths";
+ error "Sequences of implicit arguments must be of different lengths.";
aux nl
| _ -> () in
aux (List.map (fun (imps,_) -> List.length imps) l)
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
index b8c07512f..b99d80e95 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
Binary files differ
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..9d90de47c 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 f69bac437..4de1d9595 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;
@@ -1951,8 +2024,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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:30:47 +0000