diff options
| -rw-r--r-- | doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 12 | ||||
| -rw-r--r-- | interp/impargs.ml | 44 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.v | 3 | ||||
| -rw-r--r-- | test-suite/success/implicit.v | 13 |
6 files changed, 54 insertions, 30 deletions
diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst new file mode 100644 index 0000000000..32526babdb --- /dev/null +++ b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst @@ -0,0 +1,8 @@ +- **Added:** + :cmd:`Arguments <Arguments (implicits)>` now supports setting + implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`. + (`#11098 <https://github.com/coq/coq/pull/11098>`_, + by Hugo Herbelin, fixes `#4696 + <https://github.com/coq/coq/pull/4696>`_, `#5173 + <https://github.com/coq/coq/pull/5173>`_, `#9098 + <https://github.com/coq/coq/pull/9098>`_.). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 7b4b652a6a..f0bbaed8f3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1583,7 +1583,7 @@ An implicit argument is considered trailing when all following arguments are dec implicit. Trailing implicit arguments cannot be declared non maximally inserted, otherwise they would never be inserted. -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. +.. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance: @@ -1713,11 +1713,11 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmd:: Arguments @qualid {* {| [ @name ] | { @name } | @name } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, - where the list of possibly bracketed :token:`ident` is a prefix of the list of + where the list of possibly bracketed :token:`name` is a prefix of the list of arguments of :token:`qualid` where the ones to be declared implicit are surrounded by square brackets and the ones to be declared as maximally inserted implicits are surrounded by curly braces. @@ -1731,20 +1731,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Global Arguments @qualid {* {| [ @name ] | { @name } | @name } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Local Arguments @qualid {* {| [ @name ] | { @name } | @name } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @name ] | { @name } | @name } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of diff --git a/interp/impargs.ml b/interp/impargs.ml index 9b50d9ca71..78c4b21920 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -83,8 +83,12 @@ let with_implicit_protection f x = type on_trailing_implicit = Error | Info | Silent -let msg_trailing_implicit (fail : on_trailing_implicit) id = - let str1 = "Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, " in + +let msg_trailing_implicit (fail : on_trailing_implicit) na i = + let pos = match na with + | Anonymous -> "number " ^ string_of_int i + | Name id -> Names.Id.to_string id in + let str1 = "Argument " ^ pos ^ " is a trailing implicit, " in match fail with | Error -> user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ].")) @@ -92,12 +96,12 @@ let msg_trailing_implicit (fail : on_trailing_implicit) id = Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted.")) | Silent -> () -let set_maximality fail id imps b = +let set_maximality fail na i imps b = (* Force maximal insertion on ending implicits (compatibility) *) b || ( let is_set x = match x with None -> false | _ -> true in let b' = List.for_all is_set imps in - if b' then msg_trailing_implicit fail id; + if b' then msg_trailing_implicit fail na i; b') (*s Computation of implicit arguments *) @@ -355,13 +359,13 @@ let positions_of_implicits (_,impls) = (* Manage user-given implicit arguments *) -let rec prepare_implicits f = function +let rec prepare_implicits i f = function | [] -> [] | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") | (Name id, Some imp)::imps -> - let imps' = prepare_implicits f imps in - Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps' - | _::imps -> None :: prepare_implicits f imps + let imps' = prepare_implicits (i+1) f imps in + Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps' + | _::imps -> None :: prepare_implicits (i+1) f imps let set_manual_implicits silent flags enriching autoimps l = (* Compare with automatic implicits to recover printing data and names *) @@ -370,9 +374,9 @@ let set_manual_implicits silent flags enriching autoimps l = let imps' = merge (k+1) autoimps explimps in begin match autoimp, explimp.CAst.v with | (Name id,_), Some (_,max) -> - Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) id imps' max, true)) + Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) (Name id) k imps' max, true)) | (Name id,Some exp), None when enriching -> - Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) id imps' flags.maximal, true)) + Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) (Name id) k imps' flags.maximal, true)) | (Name _,_), None -> None | (Anonymous,_), Some (Name id,max) -> Some (ExplByName id,Manual,(max,true)) @@ -390,7 +394,7 @@ let set_manual_implicits silent flags enriching autoimps l = let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] else let l = compute_implicits_flags env sigma f false t in - [DefaultImpArgs, prepare_implicits f l] + [DefaultImpArgs, prepare_implicits 1 f l] (*s Constants. *) @@ -667,22 +671,22 @@ let maybe_declare_manual_implicits local ref ?enriching l = if List.exists (fun x -> x.CAst.v <> None) l then declare_manual_implicits local ref ?enriching l +let explicit_kind i = function + | Name id -> ExplByName id + | Anonymous -> ExplByPos (i,None) let compute_implicit_statuses autoimps l = let rec aux i = function | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, MaxImplicit :: manualimps -> - Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, NonMaxImplicit :: manualimps -> + | na :: autoimps, MaxImplicit :: manualimps -> + Some (explicit_kind i na, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) + | na :: autoimps, NonMaxImplicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in - let max = set_maximality Error id imps' false in - Some (ExplByName id, Manual, (max, true)) :: imps' - | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ -> - user_err ~hdr:"set_implicits" - (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit.")) + let max = set_maximality Error na i imps' false in + Some (explicit_kind i na, Manual, (max, true)) :: imps' | autoimps, [] -> List.map (fun _ -> None) autoimps | [], _::_ -> assert false - in aux 0 (autoimps, l) + in aux 1 (autoimps, l) let set_implicits local ref l = let flags = !implicit_args in diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5093e785de..26ebd8efc3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -86,8 +86,8 @@ Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Some argument names are duplicated: F The command has indeed failed with message: -Argument number 2 (anonymous in original definition) cannot be declared -implicit. +Argument number 3 is a trailing implicit, so it can't be declared non +maximal. Please use { } instead of [ ]. The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 9713a9dbbe..6ac09cf771 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -49,7 +49,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F : rename. -Fail Arguments eq {F} x [z] : rename. +Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. - diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 668d765d83..59650d6822 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -169,3 +169,16 @@ Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0. Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0. Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted. Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0. + +Module TestUnnamedImplicit. + +Axiom foo : forall A, A -> A. + +Arguments foo {A} {_}. +Check foo (arg_2:=true) : bool. +Check foo : bool. + +Arguments foo {A} {x}. +Check foo (x:=true) : bool. + +End TestUnnamedImplicit. |