Fixing buggy abberant code for Evarutil.expand_evar

by the way renamed into materialize_evar.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14537 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 73 insertions, 73 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b9f09509c..0fa1111ff 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -391,77 +391,68 @@ let check_restricted_occur evd refine env filter constr =
   let res = aux 0 constr in
     Array.to_list filter, res
 
+(* We have a unification problem Σ; Γ |- ?e[u1..uq] = ty : s where ?e is not
+ * defined in Σ but yet known to be definable in some context x1:T1..xq:Tq.
+ * [declare_dangling_evar ... Γ Σ c ty (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)]
+ * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = ty holds.
+ *)
+
+let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env
+    inst_in_sign =
+  let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
+  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
+  let t_in_env = whd_evar evd t_in_env in
+  let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
+  let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
+  (evd,whd_evar evd evar_in_sign)
+
 (* We have x1..xq |- ?e1 : τ and had to solve something like
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
  * ?e2[v1..vn], hence flexible. We had to go through k binders and now
- * virtually have x1..xq, y1..yk | ?e1' : τ' and the equation
+ * virtually have x1..xq, y1'..yk' | ?e1' : τ' and the equation
  * Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
- * What we do is to formally introduce ?e1' in context x1..xq, Γ, y1..yk,
- * but forbidding it to use the variables of Γ (otherwise said,
- * Γ is here only for ensuring the correct typing of ?e1').
- *
- * In fact, we optimize a little and try to compute a maximum
- * common subpart of x1..xq and Γ. This is done by detecting the
- * longest subcontext x1..xp such that Γ = x1'..xp' z1..zm and
- * u1..up = x1'..xp'.
- *
- * At the end, we return ?e1'[x1..xn z1..zm y1..yk] so that ?e1 can be
- * instantiated by (...\y1 ... \yk ... ?e1'[x1..xn z1..zm y1..yk]) and the
- * new problem is Σ; Γ, y1..yk |- ?e1'[u1..un z1..zm y1..yk] = c,
- * making the z1..zm unavailable.
+ * [extend_evar Γ evd k (?e1[u1..uq]) c] extend Σ with the declaration of ?e1'
+ * and returns both its instance ?e1'[x1..xq y1..yk] in an extension of the
+ * context of e1 so that e1 can be instantiated by
+ * (...\y1' ... \yk' ... ?e1'[x1..xq y1'..yk']),
+ * and the instance ?e1'[u1..uq y1..yk] so that the remaining equation
+ * ?e1'[u1..uq y1..yk] = c can be registered
  *
- * This is what [extend_evar Γ evd k (?e1[u1..uq]) c] does.
+ * Note that, because invert_definition does not check types, we need to
+ * guess the types of y1'..yn' by inverting the types of y1..yn along the
+ * substitution u1..uq.
  *)
 
-let shrink_context env subst ty =
-  let rev_named_sign = List.rev (named_context env) in
-  let rel_sign = rel_context env in
-  (* We merge the contexts (optimization) *)
-  let rec shrink_rel i subst rel_subst rev_rel_sign =
-    match subst,rev_rel_sign with
-    | (id,c)::subst,_::rev_rel_sign when isRel c && destRel c = i ->
-	shrink_rel (i-1) subst (mkVar id::rel_subst) rev_rel_sign
-    | _ ->
-	substl_rel_context rel_subst (List.rev rev_rel_sign),
-	substl rel_subst ty
-  in
-  let rec shrink_named subst named_subst rev_named_sign =
-    match subst,rev_named_sign with
-    | (id,c)::subst,(id',b',t')::rev_named_sign when isVar c && destVar c = id' ->
-	shrink_named subst ((id',mkVar id)::named_subst) rev_named_sign
-    | _::_, [] ->
-	let nrel = List.length rel_sign in
-	let rel_sign, ty = shrink_rel nrel subst [] (List.rev rel_sign) in
-	[], map_rel_context (replace_vars named_subst) rel_sign,
-	replace_vars named_subst ty
-    | _ ->
-	map_named_context (replace_vars named_subst) (List.rev rev_named_sign),
-	rel_sign, ty
+let materialize_evar define_fun env evd k (evk1,args1) ty =
+  let evi1 = Evd.find_undefined evd evk1 in
+  let env1,rel_sign = env_rel_context_chop k env in
+  let sign1 = evar_hyps evi1 in
+  let ids1 = List.map pi1 (named_context_of_val sign1) in
+  let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
+    List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
+      match b with
+      | None ->
+          let id = next_name_away na avoid in
+          let evd,t_in_sign =
+            define_evar_from_virtual_equation define_fun env evd t_in_env
+              sign filter inst_in_env inst_in_sign in
+          (push_named_context_val (id,None,t_in_sign) sign,true::filter,
+           (mkRel 1)::(List.map (lift 1) inst_in_env),(mkVar id)::inst_in_sign,
+           push_rel d env,evd,id::avoid)
+      | Some b ->
+          (sign,filter,inst_in_env,inst_in_sign,
+           push_rel d env,evd,avoid))
+      rel_sign
+      (sign1,evar_filter evi1,Array.to_list args1,
+       List.map mkVar ids1,env1,evd,ids1)
   in
-  shrink_named subst [] rev_named_sign
-
-let extend_evar env evdref k (evk1,args1) ty =
-  let overwrite_first v1 v2 =
-    let v = Array.copy v1 in
-    let n = Array.length v - Array.length v2 in
-    for i = 0 to Array.length v2 - 1 do v.(n+i) <- v2.(i) done;
-    v in
-  let evi1 = Evd.find_undefined !evdref evk1 in
-  let named_sign',rel_sign',ty =
-    if k = 0 then [], [], ty
-    else shrink_context env (List.rev (make_pure_subst evi1 args1)) ty in
-  let extenv =
-    List.fold_right push_rel rel_sign'
-      (List.fold_right push_named named_sign' (evar_unfiltered_env evi1)) in
-  let nb_to_hide = rel_context_length rel_sign' - k in
-  let rel_filter = list_map_i (fun i _ -> i > nb_to_hide) 1 rel_sign' in
-  let named_filter1 = List.map (fun _ -> true) (evar_context evi1) in
-  let named_filter2 = List.map (fun _ -> false) named_sign' in
-  let filter = rel_filter@named_filter2@named_filter1 in
-  let evar1' = e_new_evar evdref extenv ~filter:filter ty in
-  let evk1',args1'_in_env = destEvar evar1' in
-  let args1'_in_extenv = Array.map (lift k) (overwrite_first args1'_in_env args1) in
-  (evar1',(evk1',args1'_in_extenv))
+  let evd,ev2ty_in_sign =
+    define_evar_from_virtual_equation define_fun env evd ty
+      sign2 filter2 inst2_in_env inst2_in_sign in
+  let evd,ev2_in_sign =
+    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
+  let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
+  (evd, ev2_in_sign, ev2_in_env)
 
 let subfilter env ccl filter newfilter args =
   let vars = collect_vars ccl in
@@ -1104,11 +1095,12 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 	   assert !progress;
 	   (* Make the virtual left evar real *)
 	   let ty = get_type_of env' !evdref t in
-	   let (evar'',ev'') = extend_evar env' evdref k ev ty in
-	     (try 
+	   let (evd,evar'',ev'') =
+             materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+	     (try
 		let evd =
 		  (* Try to project (a restriction of) the left evar ... *)
-		  try solve_evar_evar_l2r (evar_define conv_algo) env' !evdref ev'' ev'
+		  try solve_evar_evar_l2r (evar_define conv_algo) env' evd ev'' ev'
 		  with CannotProject projs'' ->
 		    (* ... or postpone the problem *)
 		    postpone_evar_evar env' evd projs'' ev'' projs' ev'
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 452b395dd..b28f8046f 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -623,7 +623,8 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
     | _ -> None
 
 (* Recognizing occurrences of a given subterm in a term: [subst_term c t]
-   substitutes [(Rel 1)] for all occurrences of term [c] in a term [t] *)
+   substitutes [(Rel 1)] for all occurrences of term [c] in a term [t];
+   works if [c] has rels *)
 
 let subst_term_gen eq_fun c t =
   let rec substrec (k,c as kc) t =
@@ -636,10 +637,11 @@ let subst_term_gen eq_fun c t =
   in
   substrec (1,c) t
 
+let subst_term = subst_term_gen eq_constr
+
 (* Recognizing occurrences of a given subterm in a term :
    [replace_term c1 c2 t] substitutes [c2] for all occurrences of
-   term [c1] in a term [t] *)
-(*i Meme remarque : a priori [c] n'est pas forcement clos i*)
+   term [c1] in a term [t]; works if [c1] and [c2] have rels *)
 
 let replace_term_gen eq_fun c by_c in_t =
   let rec substrec (k,c as kc) t =
@@ -652,8 +654,6 @@ let replace_term_gen eq_fun c by_c in_t =
   in
   substrec (0,c) in_t
 
-let subst_term = subst_term_gen eq_constr
-
 let replace_term = replace_term_gen eq_constr
 
 (* Substitute only at a list of locations or excluding a list of
@@ -1068,7 +1068,7 @@ let on_judgment_value f j = { j with uj_val = f j.uj_val }
 let on_judgment_type f j = { j with uj_type = f j.uj_type }
 
 (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
-     variables *)
+     variables; skips let-in's *)
 let context_chop k ctx =
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
@@ -1077,6 +1077,13 @@ let context_chop k ctx =
     | (_, []) -> anomaly "context_chop"
   in chop_aux [] (k,ctx)
 
+(* Do not skip let-in's *)
+let env_rel_context_chop k env =
+  let rels = rel_context env in
+  let ctx1,ctx2 = list_chop k rels in
+  push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
+  ctx1
+
 (*******************************************)
 (* Functions to deal with impossible cases *)
 (*******************************************)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 2028e5aca..d101d7d4f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -240,7 +240,8 @@ val ids_of_named_context : named_context -> identifier list
 val ids_of_context : env -> identifier list
 val names_of_rel_context : env -> names_context
 
-val context_chop : int -> rel_context -> (rel_context*rel_context)
+val context_chop : int -> rel_context -> rel_context * rel_context
+val env_rel_context_chop : int -> env -> env * rel_context
 
 (** Set of local names *)
 val vars_of_env: env -> Idset.t