Turning "manual_implicits" into a list of position in impargs.ml.

11 files changed, 53 insertions, 141 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 622a9aee3d..e55f66e856 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2435,10 +2435,8 @@ 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
-		  let na = match na with Name n -> Some n | Anonymous -> None in
-                    CAst.make (ExplByPos (n, na), (true, true, true)) :: impls
-		else impls
+                if k == Implicit then CAst.make (Some (na,true)) :: impls
+                else CAst.make None :: impls
 	      in
                 (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
@@ -2447,7 +2445,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
               let d = LocalDef (make_annot na r, c, t) in
                 (push_rel d env, sigma, d::params, n, impls))
       (env,sigma,[],k+1,[]) (List.rev bl)
-  in sigma, ((env, par), impls)
+  in sigma, ((env, par), List.rev impls)
 
 let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
   let int_env,bl = intern_context global_level env impl_env params in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 81fe3e22b3..112862da18 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
 open Libobject
 open EConstr
 open Reductionops
-open Constrexpr
 open Namegen
 
 module NamedDecl = Context.Named.Declaration
@@ -341,78 +340,30 @@ let rec prepare_implicits f = function
       Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
-(*
-If found, returns Some (x,(b,fi,fo)) and l with the entry removed,
-otherwise returns None and l unchanged.
- *)
-let assoc_by_pos k l =
-  let rec aux = function
-      (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl
-    | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl
-    | [] -> raise Not_found
-  in try aux l with Not_found -> None, l
-
-let check_correct_manual_implicits autoimps l =
-  List.iter (function
-    | ExplByName id,(b,fi,forced) ->
-	if not forced then
-	  user_err 
-            (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".")
-    | ExplByPos (i,_id),_t ->
-	if i<1 || i>List.length autoimps then
-	  user_err 
-            (str "Bad implicit argument number: " ++ int i ++ str ".")
-	else
-	  user_err 
-	    (str "Cannot set implicit argument number " ++ int i ++
-	      str ": it has no name.")) l
-
-(* Take a list l of explicitations, and map them to positions. *)
-let flatten_explicitations l autoimps =
-  let l = List.map (fun c -> c.CAst.v) l in
-  let rec aux k l = function
-    | (Name id,_)::imps ->
-       let value, l' =
-         try
-           let eq = Constrexpr_ops.explicitation_eq in
-           let flags = List.assoc_f eq (ExplByName id) l in
-           Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l
-         with Not_found -> assoc_by_pos k l
-       in value :: aux (k+1) l' imps
-    | (Anonymous,_)::imps ->
-       let value, l' = assoc_by_pos k l
-       in value :: aux (k+1) l' imps
-    | [] when List.is_empty l -> []
-    | [] ->
-       check_correct_manual_implicits autoimps l;
-       []
-  in aux 1 l autoimps
-
 let set_manual_implicits flags enriching autoimps l =
-  if not (List.distinct l) then
-    user_err Pp.(str "Some parameters are referred more than once.");
   (* 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 with
-       | (Name id,_), Some (_, (b, fi, _)) ->
-          Some (id, Manual, (set_maximality imps' b, fi))
+       begin match autoimp, explimp.CAst.v with
+       | (Name id,_), Some (_,max) ->
+          Some (id, Manual, (set_maximality imps' max, true))
        | (Name id,Some exp), None when enriching ->
           Some (id, exp, (set_maximality imps' flags.maximal, true))
        | (Name _,_), None -> None
-       | (Anonymous,_), Some (Some id, (b, fi, true)) ->
-          Some (id,Manual,(b,fi))
-       | (Anonymous,_), Some (None, (b, fi, true)) ->
+       | (Anonymous,_), Some (Name id,max) ->
+          Some (id,Manual,(max,true))
+       | (Anonymous,_), Some (Anonymous,max) ->
           let id = Id.of_string ("arg_" ^ string_of_int k) in
-          Some (id,Manual,(b,fi))
-       | (Anonymous,_), Some (_, (_, _, false)) -> None
+          Some (id,Manual,(max,true))
        | (Anonymous,_), None -> None
        end :: imps'
     | [], [] -> []
-    (* flatten_explicitations returns a list of the same length as autoimps *)
-    | _ -> assert false
-  in merge 1 autoimps (flatten_explicitations l autoimps)
+    | [], _ -> assert false
+    (* possibly more automatic than manual implicit arguments n
+       when the conclusion is an unfoldable constant *)
+    | autoimps, [] -> merge k autoimps [CAst.make None]
+  in merge 1 autoimps l
 
 let compute_semi_auto_implicits env sigma f t =
   if not f.auto then [DefaultImpArgs, []]
@@ -643,9 +594,7 @@ let declare_mib_implicits kn =
       (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
 
 (* Declare manual implicits *)
-type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
-
-type manual_implicits = manual_explicitation CAst.t list
+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
@@ -670,8 +619,6 @@ let projection_implicits env p impls =
   CList.skipn_at_least npars impls
 
 let declare_manual_implicits local ref ?enriching l =
-  assert (List.for_all (fun {CAst.v=(_, (max, fi, fu))} -> fi && fu) l);
-  assert (List.for_all (fun {CAst.v=(ex, _)} -> match ex with ExplByPos (_,_) -> true | _ -> false) l);
   let flags = !implicit_args in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -686,9 +633,8 @@ let declare_manual_implicits local ref ?enriching l =
   in add_anonymous_leaf (inImplicits (req,[ref,l]))
 
 let maybe_declare_manual_implicits local ref ?enriching l =
-  match l with
-  | [] -> ()
-  | _ -> 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
 
 (* TODO: either turn these warnings on and document them, or handle these cases sensibly *)
 
@@ -751,12 +697,6 @@ let extract_impargs_data impls =
     | [] -> [] in
   aux 0 impls
 
-let lift_implicits n =
-  List.map (CAst.map (fun x ->
-    match fst x with
-	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
-      | _ -> x))
-
 let make_implicits_list l = [DefaultImpArgs, l]
 
 let rec drop_first_implicits p l =
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 07f015d319..92b6bdd406 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -84,13 +84,7 @@ val force_inference_of : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
-(** A [manual_explicitation] is a tuple of a positional or named explicitation with
-   maximal insertion, force inference and force usage flags. Forcing usage makes
-   the argument implicit even if the automatic inference considers it not inferable. *)
-type manual_explicitation = Constrexpr.explicitation *
-    (maximal_insertion * force_inference * bool)
-
-type manual_implicits = manual_explicitation CAst.t list
+type manual_implicits = (Name.t * bool) option CAst.t list
 
 val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool ->
   manual_implicits -> implicit_status list
@@ -131,8 +125,6 @@ val implicits_of_global : GlobRef.t -> implicits_list list
 val extract_impargs_data :
   implicits_list list -> ((int * int) option * implicit_status list) list
 
-val lift_implicits : int -> manual_implicits -> manual_implicits
-
 val make_implicits_list : implicit_status list -> implicits_list list
 
 val drop_first_implicits : int -> implicits_list -> implicits_list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 34674fb102..bab9024415 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -257,32 +257,23 @@ let warn_ignoring_implicit_status =
        Name.print na ++ strbrk " and following binders")
 
 let implicits_of_glob_constr ?(with_products=true) l =
-  let add_impl ?loc i na bk l = match bk with
-  | Implicit ->
-    let name =
-      match na with
-      | Name id -> Some id
-      | Anonymous -> None
-    in
-    CAst.make ?loc (ExplByPos (i, name), (true, true, true)) :: l
-  | _ -> l
+  let add_impl ?loc na bk l = match bk with
+  | Implicit -> CAst.make ?loc (Some (na,true)) :: l
+  | _ -> CAst.make ?loc None :: l
   in
-  let rec aux i c =
-    let abs ?loc na bk b =
-      add_impl ?loc i na bk (aux (succ i) b)
-    in
+  let rec aux c =
     match DAst.get c with
     | GProd (na, bk, t, b) ->
-      if with_products then abs na bk b
+      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
           | _ -> ()
         in []
-    | GLambda (na, bk, t, b) -> abs ?loc:t.CAst.loc na bk b
-    | GLetIn (na, b, t, c) -> aux i c
+    | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
+    | GLetIn (na, b, t, c) -> aux c
     | GRec (fix_kind, nas, args, tys, bds) ->
       let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
-      List.fold_left_i (fun i l (na,bk,t,_) -> add_impl ?loc:c.CAst.loc i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
+      List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb))
     | _ -> []
-  in aux 1 l
+  in aux l
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b64af52b6e..bd5a211f1d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -537,8 +537,7 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   in
   let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
   let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in
-  let len = Context.Rel.nhyps ctx in
-  let imps = imps @ Impargs.lift_implicits len imps' in
+  let imps = imps @ imps' in
   let ctx', c = decompose_prod_assum sigma c' in
   let ctx'' = ctx' @ ctx in
   let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index c1f676b043..a27c08d176 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -283,8 +283,8 @@ let context poly l =
       Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
       status
     else
-      let test {CAst.v = (x, _)} = match x with
-      | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
+      let test x = match x.CAst.v with
+      | Some (Name id',_) -> Id.equal id id'
       | _ -> false
       in
       let impl = List.exists test impls in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 01274e2568..ae1f55acda 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -30,16 +30,16 @@ let warn_implicits_in_term =
             strbrk "Discarding incompatible declaration in term.")
 
 let check_imps ~impsty ~impsbody =
-  let impsty = List.map (fun x -> x.CAst.v) impsty in
-  List.iter (fun {CAst.v = (key, (va:bool*bool*bool)); CAst.loc} ->
-      let b =
-        try
-          (* Pervasives.(=) is OK for this type *)
-          Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va
-        with Not_found -> false
-      in
-      if not b then warn_implicits_in_term ?loc ())
-    impsbody
+  let rec aux impsty impsbody =
+  match impsty, impsbody with
+  | a1 :: impsty, a2 :: impsbody ->
+    (match a1.CAst.v, a2.CAst.v with
+    | None , None -> aux impsty impsbody
+    | Some _ , Some _ -> aux impsty impsbody
+    | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ())
+  | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
+  | [], [] -> () in
+  aux impsty impsbody
 
 let interp_definition ~program_mode pl bl poly red_option c ctypopt =
   let env = Global.env() in
@@ -57,11 +57,11 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt =
     match tyopt with
     | None ->
       let evd, (c, impsbody) = interp_constr_evars_impls ~program_mode ~impls env_bl evd c in
-      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
+      evd, c, imps1@impsbody, None
     | Some (ty, impsty) ->
       let evd, (c, impsbody) = interp_casted_constr_evars_impls ~program_mode ~impls env_bl evd c ty in
       check_imps ~impsty ~impsbody;
-      evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
+      evd, c, imps1@impsty, Some ty
   in
   (* Do the reduction *)
   let evd, c = red_constant_body red_option env_bl evd c in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 6068cd90f1..0d7ba69955 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -197,7 +197,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
   let fiximps = List.map3
-    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
+    (fun ctximps cclimps (_,ctx) -> ctximps@cclimps)
     fixctximps fixcclimps fixctxs in
   let sigma, rec_sign =
     List.fold_left2
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index e0f2f05fe3..2f8b12f4c5 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -375,8 +375,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
-  let indimpls = List.map (fun impls -> userimpls @
-    lift_implicits (Context.Rel.nhyps ctx_params) impls) indimpls in
+  let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
   let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
   let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -402,8 +401,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
                        constructors
   in
   let ctx_params = ctx_params @ ctx_uparams in
-  let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in
-  let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in
+  let userimpls = useruimpls @ userimpls in
+  let indimpls = List.map (fun iimpl -> useruimpls @ iimpl) indimpls in
   let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
   let env_ar = push_types env0 indnames relevances fullarities in
   let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
@@ -450,10 +449,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
       indl arities arityconcl constructors
   in
   let impls =
-    let len = Context.Rel.nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
         indimpls, List.map (fun impls ->
-          userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
+          userimpls @ impls) cimpls) indimpls constructors
   in
   let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in
   (* Build the mutual inductive entry *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a7366b2c56..7aba64fb93 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -469,7 +469,7 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
     (* XXX: The nf_evar is critical !! *)
     evd, (id.CAst.v,
           (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
-           (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
+           (ids, imps @ imps'))))
       evd thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
diff --git a/vernac/record.ml b/vernac/record.ml
index e555c6d154..48cde133a8 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -476,21 +476,15 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
   List.mapi map record_data
 
 let implicits_of_context ctx =
-  List.map_i (fun i name ->
-    let explname =
-      match name with
-      | Name n -> Some n
-      | Anonymous -> None
-    in CAst.make (ExplByPos (i, explname), (true, true, true)))
-    1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
+  List.map (fun name -> CAst.make (Some (name,true)))
+    (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
 let declare_class def cum ubinders univs id idbuild paramimpls params arity
     template fieldimpls fields ?(kind=StructureComponent) coers priorities =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
-    let len = List.length params in
     let impls = implicits_of_context params in
-      List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
+      List.map (fun x -> impls @ x) fieldimpls
   in
   let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
   let data =
@@ -704,7 +698,7 @@ let definition_structure udecl kind ~template cum poly finite records =
     declare_class def cum ubinders univs id.CAst.v idbuild
       implpars params arity template implfs fields coers priorities
   | _ ->
-    let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
+    let map impls = implpars @ [CAst.make None] @ impls in
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
     let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
       let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->