Cleaning and documenting Clenv.make_evar_clause

4 files changed, 48 insertions, 18 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fb5a76bd3..86d49cb2f 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 5868f1e9b..a302e6448 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 _]. *)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index eeb779448..a96bc5e42 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -487,7 +487,7 @@ let rec decompose_app_rel env evd t =
 let decompose_applied_relation env sigma orig (c,l) =
   let ctype = Retyping.get_type_of env sigma c in
   let find_rel ty =
-    let sigma, cl = Clenv.make_evar_clause env sigma None ty in
+    let sigma, cl = Clenv.make_evar_clause env sigma ty in
     let sigma = Clenv.solve_evar_clause env sigma true cl l in
     let { Clenv.cl_holes = holes; Clenv.cl_concl = t } = cl in
     let (equiv, c1, c2) = decompose_app_rel env sigma t in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0cff8a37e..cdf5cb717 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3825,7 +3825,7 @@ let check_expected_type env sigma (elimc,bl) =
   let sign,_ = splay_prod env sigma elimt in
   let n = List.length sign in
   if n == 0 then error "Scheme cannot be applied.";
-  let sigma,cl = make_evar_clause env sigma (Some (n-1)) elimt in
+  let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
   let sigma = solve_evar_clause env sigma true cl bl in
   let (_,u,_) = destProd cl.cl_concl in
   fun t -> Evarconv.e_cumul env (ref sigma) t u