Add syntax for non maximally inserted implicit arguments

4 files changed, 62 insertions, 41 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f4ae5bf676..ab20f1b3ef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -330,15 +330,18 @@ let exists_name na l =
   | _ -> false
 
 let build_impls ?loc n bk na acc =
-  match bk with
-  | Implicit ->
+  let impl_status max =
     let na =
-       if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
-       else na in
+      if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
+      else na in
     let impl = match na with
-     | Name id -> Some (ExplByName id,Manual,(true,true))
-     | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
-     impl :: acc
+      | Name id -> Some (ExplByName id,Manual,(true,true))
+      | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
+    impl
+  in
+  match bk with
+  | NonMaxImplicit -> impl_status false :: acc
+  | MaxImplicit -> impl_status true :: acc
   | Explicit -> None :: acc
 
 let impls_binder_list =
@@ -426,7 +429,7 @@ let warn_unexpected_implicit_binder_declaration =
     Pp.(fun () -> str "Unexpected implicit binder declaration.")
 
 let check_implicit_meaningful ?loc k env =
-  if k = Implicit && env.impl_binder_index = None then
+  if k <> Explicit && env.impl_binder_index = None then
     warn_unexpected_implicit_binder_declaration ?loc ()
 
 let intern_generalized_binder intern_type ntnvars
@@ -444,7 +447,7 @@ let intern_generalized_binder intern_type ntnvars
   check_implicit_meaningful ?loc b' env;
   let bl = List.map
     CAst.(map (fun id ->
-      (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+      (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -2500,8 +2503,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
               let r = Retyping.relevance_of_type env sigma t in
               let d = LocalAssum (make_annot na r,t) in
               let impls =
-                if k == Implicit then CAst.make (Some (na,true)) :: impls
-                else CAst.make None :: impls
+                match k with
+                | NonMaxImplicit -> CAst.make (Some (na,false)) :: impls
+                | MaxImplicit -> CAst.make (Some (na,true)) :: impls
+                | Explicit -> CAst.make None :: impls
               in
                 (push_rel d env, sigma, d::params, succ n, impls)
           | Some b ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index e2c732809a..9b50d9ca71 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Constr
 open Globnames
+open Glob_term
 open Declarations
 open Lib
 open Libobject
@@ -80,10 +81,24 @@ let with_implicit_protection f x =
     let () = implicit_args := oflags in
     iraise reraise
 
-let set_maximality imps b =
+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
+  match fail with
+  | Error ->
+    user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ]."))
+  | Info ->
+    Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted."))
+  | Silent -> ()
+
+let set_maximality fail id imps b =
   (* Force maximal insertion on ending implicits (compatibility) *)
-  let is_set x = match x with None -> false | _ -> true in
-  b || List.for_all is_set imps
+  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;
+    b')
 
 (*s Computation of implicit arguments *)
 
@@ -302,6 +317,11 @@ let is_status_implicit = function
 
 let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
 
+let binding_kind_of_status = function
+  | Some (_, _, (false, _)) -> NonMaxImplicit
+  | Some (_, _, (true, _)) -> MaxImplicit
+  | None -> Explicit
+
 let name_of_implicit = function
   | None -> anomaly (Pp.str "Not an implicit argument.")
   | Some (ExplByName id,_,_) -> id
@@ -340,19 +360,19 @@ let rec prepare_implicits 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 imps' f.maximal,true)) :: imps'
+      Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
-let set_manual_implicits flags enriching autoimps l =
+let set_manual_implicits silent flags enriching autoimps l =
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k autoimps explimps = match autoimps, explimps with
     | autoimp::autoimps, explimp::explimps ->
        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 imps' max, true))
+          Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) id imps' max, true))
        | (Name id,Some exp), None when enriching ->
-          Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
+          Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) id imps' flags.maximal, true))
        | (Name _,_), None -> None
        | (Anonymous,_), Some (Name id,max) ->
           Some (ExplByName id,Manual,(max,true))
@@ -497,8 +517,9 @@ let impls_of_context ctx =
   let map decl =
     let id = NamedDecl.get_id decl in
     match Id.Map.get id !sec_implicits with
-    | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
-    | Glob_term.Explicit -> None
+    | NonMaxImplicit -> Some (ExplByName id, Manual, (false, true))
+    | MaxImplicit -> Some (ExplByName id, Manual, (true, true))
+    | Explicit -> None
   in
   List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
 
@@ -608,7 +629,7 @@ type manual_implicits = (Name.t * bool) option CAst.t list
 
 let compute_implicits_with_manual env sigma typ enriching l =
   let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
-  set_manual_implicits !implicit_args enriching autoimpls l
+  set_manual_implicits true !implicit_args enriching autoimpls l
 
 let check_inclusion l =
   (* Check strict inclusion *)
@@ -636,7 +657,7 @@ let declare_manual_implicits local ref ?enriching l =
   let t = of_constr t in
   let enriching = Option.default flags.auto enriching in
   let autoimpls = compute_auto_implicits env sigma flags enriching t in
-  let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in
+  let l = [DefaultImpArgs, set_manual_implicits false flags enriching autoimpls l] in
   let req =
     if is_local local ref then ImplLocal
     else ImplInteractive(flags,ImplManual (List.length autoimpls))
@@ -647,22 +668,16 @@ let maybe_declare_manual_implicits local ref ?enriching l =
     declare_manual_implicits local ref ?enriching l
 
 
-let msg_trailing_implicit id =
-  user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]."))
-
-type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
-
 let compute_implicit_statuses autoimps l =
   let rec aux i = function
-    | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
-    | Name id :: autoimps, MaximallyImplicit :: manualimps ->
+    | _ :: 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, Implicit :: manualimps ->
+    | Name id :: autoimps, NonMaxImplicit :: manualimps ->
        let imps' = aux (i+1) (autoimps, manualimps) in
-       let max = set_maximality imps' false in
-       if max then msg_trailing_implicit id;
+       let max = set_maximality Error id imps' false in
        Some (ExplByName id, Manual, (max, true)) :: imps'
-    | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
+    | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ ->
        user_err ~hdr:"set_implicits"
          (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))
     | autoimps, [] -> List.map (fun _ -> None) autoimps
@@ -684,7 +699,7 @@ let set_implicits local ref l =
        check_rigidity (is_rigid env sigma t);
        (* Sort by number of implicits, decreasing *)
        let is_implicit = function
-         | NotImplicit -> false
+         | Explicit -> false
          | _ -> true in
        let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in
        let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ef3c2496f4..65e7fd8aaf 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -77,6 +77,7 @@ type implicit_side_condition
 type implicits_list = implicit_side_condition * implicit_status list
 
 val is_status_implicit : implicit_status -> bool
+val binding_kind_of_status : implicit_status -> Glob_term.binding_kind
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> Id.t
 val maximal_insertion_of : implicit_status -> bool
@@ -113,12 +114,10 @@ val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
 val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
   manual_implicits -> unit
 
-type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
-
 (** [set_implicits local ref l]
    Manual declaration of implicit arguments.
   `l` is a list of possible sequences of implicit statuses. *)
-val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit
+val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit
 
 val implicits_of_global : GlobRef.t -> implicits_list list
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8b457ab37b..ffbb982ab7 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -203,8 +203,9 @@ let warn_ignoring_implicit_status =
 
 let implicits_of_glob_constr ?(with_products=true) l =
   let add_impl ?loc na bk l = match bk with
-  | Implicit -> CAst.make ?loc (Some (na,true)) :: l
-  | _ -> CAst.make ?loc None :: l
+  | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l
+  | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l
+  | Explicit -> CAst.make ?loc None :: l
   in
   let rec aux c =
     match DAst.get c with
@@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l =
       if with_products then add_impl na bk (aux b)
       else
         let () = match bk with
-          | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
-          | _ -> ()
+          | NonMaxImplicit
+          | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
+          | Explicit -> ()
         in []
     | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
     | GLetIn (na, b, t, c) -> aux c