Impargs: Using ExplByPos/ExplByName rather than encoding index as an ident.

This moves the encoding of "n" as "arg_n" closer to the user interface level.

Note however that Constrintern.build_impl is not able yet to use ExplByPos.
See further commits.

5 files changed, 24 insertions, 17 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ff115a3e48..7bf7d5b683 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -319,8 +319,8 @@ let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
 (* Utilities for binders                                              *)
 let build_impls = function
   |Implicit -> (function
-                  |Name id ->  Some (id, Impargs.Manual, (true,true))
-                  |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
+                  |Name id ->  Some (ExplByName id, Impargs.Manual, (true,true))
+                  |Anonymous -> Some (ExplByName (Id.of_string "_"), Impargs.Manual, (true,true)))
   |Explicit -> fun _ -> None
 
 let impls_type_list ?(args = []) =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 2aa002ead1..df28b32f81 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,6 +20,7 @@ open Libobject
 open EConstr
 open Reductionops
 open Namegen
+open Constrexpr
 
 module NamedDecl = Context.Named.Declaration
 
@@ -289,7 +290,7 @@ type force_inference = bool (* true = always infer, never turn into evar/subgoal
 
 type implicit_status =
     (* None = Not implicit *)
-    (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option
+    (explicitation * implicit_explanation * (maximal_insertion * force_inference)) option
 
 type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
 
@@ -299,9 +300,12 @@ let is_status_implicit = function
   | None -> false
   | _ -> true
 
+let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
+
 let name_of_implicit = function
   | None -> anomaly (Pp.str "Not an implicit argument.")
-  | Some (id,_,_) -> id
+  | Some (ExplByName id,_,_) -> id
+  | Some (ExplByPos (k,_),_,_) -> name_of_pos k
 
 let maximal_insertion_of = function
   | Some (_,_,(b,_)) -> b
@@ -336,7 +340,7 @@ 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 (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
+      Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
 let set_manual_implicits flags enriching autoimps l =
@@ -346,15 +350,14 @@ let set_manual_implicits flags enriching autoimps l =
        let imps' = merge (k+1) autoimps explimps in
        begin match autoimp, explimp.CAst.v with
        | (Name id,_), Some (_,max) ->
-          Some (id, Manual, (set_maximality imps' max, true))
+          Some (ExplByName id, Manual, (set_maximality imps' max, true))
        | (Name id,Some exp), None when enriching ->
-          Some (id, exp, (set_maximality imps' flags.maximal, true))
+          Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
        | (Name _,_), None -> None
        | (Anonymous,_), Some (Name id,max) ->
-          Some (id,Manual,(max,true))
+          Some (ExplByName id,Manual,(max,true))
        | (Anonymous,_), Some (Anonymous,max) ->
-          let id = Id.of_string ("arg_" ^ string_of_int k) in
-          Some (id,Manual,(max,true))
+          Some (ExplByPos (k,None),Manual,(max,true))
        | (Anonymous,_), None -> None
        end :: imps'
     | [], [] -> []
@@ -464,7 +467,7 @@ let implicits_of_global ref =
         | [], _ -> []
         | _, [] -> implicits
         | Some (_, x,y) :: implicits, Name id :: names ->
-           Some (id, x,y) :: rename implicits names
+           Some (ExplByName 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
@@ -494,7 +497,7 @@ 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 (id, Manual, (true, true))
+    | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
     | Glob_term.Explicit -> None
   in
   List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
@@ -655,12 +658,12 @@ 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 ->
-       Some (id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
+       Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
     | Name id :: autoimps, Implicit :: manualimps ->
        let imps' = aux (i+1) (autoimps, manualimps) in
        let max = set_maximality imps' false in
        if max then warn_set_maximal_deprecated i;
-       Some (id, Manual, (max, true)) :: imps'
+       Some (ExplByName id, Manual, (max, true)) :: imps'
     | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
        user_err ~hdr:"set_implicits"
          (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 8fa69e818a..ef3c2496f4 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -68,7 +68,7 @@ type maximal_insertion = bool (** true = maximal contextual insertion *)
 
 type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
 
-type implicit_status = (Id.t * implicit_explanation *
+type implicit_status = (Constrexpr.explicitation * implicit_explanation *
                           (maximal_insertion * force_inference)) option
     (** [None] = Not implicit *)
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0e17f2b274..d48e2139d1 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -200,7 +200,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
         Constrintern.Recursive full_arity impls
     in
     let newimpls = Id.Map.singleton recname
-        (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+        (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
          scopes @ [None]) in
     interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
       ~impls:newimpls body (lift 1 top_arity)
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ea49cae9db..eb7b28f15b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -255,9 +255,13 @@ let needs_extra_scopes ref scopes =
   let ty, _ctx = Typeops.type_of_global_in_context env ref in
   aux env ty scopes
 
+let implicit_name_of_pos = function
+  | Constrexpr.ExplByName id -> Name id
+  | Constrexpr.ExplByPos (n,k) -> Anonymous
+
 let implicit_kind_of_status = function
   | None -> Anonymous, NotImplicit
-  | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
+  | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
 
 let dummy = {
   Vernacexpr.implicit_status = NotImplicit;