Cleaning and documenting Clenv.make_evar_clause

2 files changed, 46 insertions, 16 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fb5a76bd30..86d49cb2fe 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -563,13 +563,18 @@ type clause = {
   cl_concl : types;
 }
 
-let make_evar_clause env sigma bound t =
+let make_evar_clause env sigma ?len t =
+  let bound = match len with
+  | None -> -1
+  | Some n -> assert (0 <= n); n
+  in
   (** FIXME: do the renaming online *)
   let t = rename_bound_vars_as_displayed [] [] t in
-  let rec clrec (sigma, holes) n t = match n, kind_of_term t with
-  | (Some 0, _) -> (sigma, holes, t)
-  | (n, Cast (t, _, _)) -> clrec (sigma, holes) n t
-  | (n, Prod (na, t1, t2)) ->
+  let rec clrec (sigma, holes) n t =
+    if n = 0 then (sigma, holes, t)
+    else match kind_of_term t with
+    | Cast (t, _, _) -> clrec (sigma, holes) n t
+    | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
       let sigma, ev = new_evar ~store env sigma t1 in
       let dep = dependent (mkRel 1) t2 in
@@ -581,9 +586,9 @@ let make_evar_clause env sigma bound t =
         hole_name = na;
       } in
       let t2 = if dep then subst1 ev t2 else t2 in
-      clrec (sigma, hole :: holes) (Option.map ((+) (-1)) n) t2
-  | (n, LetIn (na, b, _, t)) -> clrec (sigma, holes) n (subst1 b t)
-  | (n, _) -> (sigma, holes, t)
+      clrec (sigma, hole :: holes) (pred n) t2
+    | LetIn (na, b, _, t) -> clrec (sigma, holes) n (subst1 b t)
+    | _ -> (sigma, holes, t)
   in
   let (sigma, holes, t) = clrec (sigma, []) bound t in
   let holes = List.rev holes in
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 5868f1e9bf..a302e64483 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -110,14 +110,38 @@ val clenv_push_prod : clausenv -> clausenv
 (** {6 Pretty-print (debug only) } *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
 
-(** {6 Evar version} *)
+(** {6 Evar-based clauses} *)
+
+(** The following code is an adaptation of the [make_clenv_*] functions above,
+    except that it uses evars instead of metas, and naturally fits in the new
+    refinement monad. It should eventually replace all uses of the
+    aforementioned functions.
+
+    A clause is constructed as follows: assume a type [t := forall (x1 : A1) ...
+    (xn : An), T], we instantiate all the [xi] with a fresh evar [ei] and
+    return [T(xi := ei)] together with the [ei] enriched with a bit of
+    additional data. This is the simple part done by [make_evar_clause].
+
+    The problem lies in the fact we want to solve such holes with some
+    [constr bindings]. This entails some subtleties, because the provided terms
+    may only be well-typed up to a coercion, which we can only infer if we have
+    enough typing information. The meta machinery could insert coercions through
+    tricky instantiation delays. The only solution we have now is to delay the
+    tentative resolution of clauses by providing the [solve_evar_clause]
+    function, to be called at a smart enough time.
+*)
 
 type hole = {
   hole_evar : constr;
+  (** The hole itself. Guaranteed to be an evar. *)
   hole_type : types;
+  (** Type of the hole in the current environment. *)
   hole_deps  : bool;
-  (** Dependent in hypotheses then in conclusion *)
+  (** Whether the remainder of the clause was dependent in the hole. Note that
+      because let binders are substituted, it does not mean that it actually
+      appears somewhere in the returned clause. *)
   hole_name : Name.t;
+  (** Name of the hole coming from its binder. *)
 }
 
 type clause = {
@@ -125,13 +149,13 @@ type clause = {
   cl_concl : types;
 }
 
-val make_evar_clause : env -> evar_map -> int option -> types ->
+val make_evar_clause : env -> evar_map -> ?len:int -> types ->
   (evar_map * clause)
 (** An evar version of {!make_clenv_binding}. Given a type [t],
-    [evar_environments env sigma n t bl] tries to eliminate at most [n] products
-    of the type [t] by filling it with evars. It returns the resulting type
-    together with the list of holes generated. Assumes that [t] is well-typed
-    in the environment. *)
+    [evar_environments env sigma ~len t bl] tries to eliminate at most [len]
+    products of the type [t] by filling it with evars. It returns the resulting
+    type together with the list of holes generated. Assumes that [t] is
+    well-typed in the environment. *)
 
 val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
   evar_map
@@ -139,4 +163,5 @@ val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
     in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
     the environment. The boolean [hyps] is a compatibility flag that allows to
     consider arguments to be dependent only when they appear in hypotheses and
-    not in the conclusion. *)
+    not in the conclusion. This boolean is only used when [bl] is of the form
+    [ImplicitBindings _]. *)