Petit nettoyage de Evarutil et Evarconv

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

1 files changed, 31 insertions, 89 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 15151ca9b..fd52e0fa0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -13,37 +13,6 @@ open Classops
 open Recordops 
 open Evarutil
 
-(* Pb: Mach cannot type evar in the general case (all Const must be applied
- * to Vars). But evars may be applied to Rels or other terms! This is the
- * difference between type_of_const and type_of_const2.
- *)
-
-(* This code (i.e. try_solve_pb, solve_pb, etc.) takes a unification
- * problem, and tries to solve it. If it solves it, then it removes
- * all the conversion problems, and re-runs conversion on each one, in
- * the hopes that the new solution will aid in solving them.
- *
- * The kinds of problems it knows how to solve are those in which
- * the usable arguments of an existential var are all themselves
- * universal variables.
- * The solution to this problem is to do renaming for the Var's,
- * to make them match up with the Var's which are found in the
- * hyps of the existential, to do a "pop" for each Rel which is
- * not an argument of the existential, and a subst1 for each which
- * is, again, with the corresponding variable. This is done by
- * Tradevar.evar_define
- *
- * Thus, we take the arguments of the existential which we are about
- * to assign, and zip them with the identifiers in the hypotheses.
- * Then, we process all the Var's in the arguments, and sort the
- * Rel's into ascending order.  Then, we just march up, doing
- * subst1's and pop's.
- *
- * NOTE: We can do this more efficiently for the relative arguments,
- * by building a long substituend by hand, but this is a pain in the
- * ass.
- *)
-
 let evar_apprec env isevars stack c =
   let rec aux s =
     let (t,stack as s') = Reduction.apprec env !isevars s in
@@ -53,56 +22,31 @@ let evar_apprec env isevars stack c =
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 
-
-let conversion_problems = ref ([] : (conv_pb * constr * constr) list)
-
-let reset_problems () = conversion_problems := []
-
-let add_conv_pb pb = (conversion_problems := pb::!conversion_problems)
-
-let get_changed_pb lev =
-  let (pbs,pbs1) = 
-    List.fold_left
-      (fun (pbs,pbs1) pb ->
-    	 if status_changed lev pb then 
-	   (pb::pbs,pbs1)
-         else 
-	   (pbs,pb::pbs1))
-      ([],[])
-      !conversion_problems 
-  in
-  conversion_problems := pbs1;
-  pbs
-
 (* Precondition: one of the terms of the pb is an uninstanciated evar,
  * possibly applied to arguments. *)
 
-let rec solve_pb env isevars pb =
-  match solve_simple_eqn (evar_conv_x env isevars CONV) isevars pb with
-    | Some lsp ->
-	let pbs = get_changed_pb lsp in
-	List.for_all
- 	  (fun (pbty,t1,t2) -> evar_conv_x env isevars pbty t1 t2)
- 	  pbs
-    | None -> (add_conv_pb pb; true)
-
-and evar_conv_x env isevars pbty term1 term2 =
+let rec evar_conv_x env isevars pbty term1 term2 =
   let term1 = whd_ise1 !isevars term1 in
   let term2 = whd_ise1 !isevars term2 in
-  if eq_constr term1 term2 then 
+(*
+ if eq_constr term1 term2 then 
     true
   else if (not(has_undefined_isevars isevars term1)) &
     not(has_undefined_isevars isevars term2) 
   then 
     is_fconv pbty env !isevars term1 term2
-  else if ise_undefined isevars term1 or ise_undefined isevars term2
-  then 
-    solve_pb env isevars (pbty,term1,term2)
+  else
+*)
+  (is_fconv pbty env !isevars term1 term2) or
+  if ise_undefined isevars term1 then
+    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
+  else if ise_undefined isevars term2 then
+    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1)
   else 
     let (t1,l1) = evar_apprec env isevars [] term1 in
     let (t2,l2) = evar_apprec env isevars [] term2 in
-    if (head_is_embedded_exist isevars t1 & not(is_eliminator t2))
-      or (head_is_embedded_exist isevars t2 & not(is_eliminator t1))
+    if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
+      or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
     then 
       (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)); true)
     else 
@@ -111,15 +55,17 @@ and evar_conv_x env isevars pbty term1 term2 =
 and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
   match (kind_of_term term1, kind_of_term term2) with
-    | IsEvar (sp1,al1), IsEvar (sp2,al2) ->
+    | IsEvar (sp1,al1 as ev1), IsEvar (sp2,al2 as ev2) ->
 	let f1 () =
 	  if List.length l1 > List.length l2 then 
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-            solve_pb env isevars(pbty,applist(term1,deb1),term2)
+            solve_simple_eqn evar_conv_x env isevars 
+	      (pbty,ev2,applist(term1,deb1))
             & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 	  else
 	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	    solve_pb env isevars(pbty,term1,applist(term2,deb2))
+	    solve_simple_eqn evar_conv_x env isevars
+	      (pbty,ev1,applist(term2,deb2))
             & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 	and f2 () =
           (sp1 = sp2)
@@ -128,11 +74,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f2]
 
-    | IsEvar (sp1,al1), IsConst cst2 ->
+    | IsEvar ev1, IsConst cst2 ->
 	let f1 () =
 	  (List.length l1 <= List.length l2) &
 	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	  solve_pb env isevars(pbty,term1,applist(term2,deb2))
+	  solve_simple_eqn evar_conv_x env isevars
+	    (pbty,ev1,applist(term2,deb2))
           & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 	and f4 () =
 	  match constant_opt_value env cst2 with
@@ -143,11 +90,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst cst1, IsEvar (sp2,al2) ->
+    | IsConst cst1, IsEvar ev2 ->
 	let f1 () =
        	  (List.length l2 <= List.length l1) &
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-	  solve_pb env isevars(pbty,applist(term1,deb1),term2)
+	  solve_simple_eqn evar_conv_x env isevars
+	    (pbty,ev2,applist(term1,deb1))
           & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 	and f4 () =
 	  match constant_opt_value env cst1 with
@@ -182,16 +130,18 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f2; f3; f4]
 
-    | IsEvar (_,_), _ ->
+    | IsEvar ev1, _ ->
        	(List.length l1 <= List.length l2) &
        	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	solve_pb env isevars(pbty,term1,applist(term2,deb2))
+	solve_simple_eqn evar_conv_x env isevars
+	  (pbty,ev1,applist(term2,deb2))
         & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 
-    | _, IsEvar (_,_) ->
+    | _, IsEvar ev2 ->
        	(List.length l2 <= List.length l1) &
        	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-	solve_pb env isevars(pbty,applist(term1,deb1),term2)
+	solve_simple_eqn evar_conv_x env isevars
+	  (pbty,ev2,applist(term1,deb1))
         & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 
     | IsConst cst1, _ ->
@@ -342,14 +292,6 @@ and check_conv_record (t1,l1) (t2,l2) =
   with _ -> 
     raise Not_found
 
-let the_conv_x env isevars t1 t2 =
-  is_conv env !isevars t1 t2 or evar_conv_x env isevars CONV t1 t2
-
-(* Si conv_x_leq repond true, pourquoi diable est-ce qu'on repasse une couche
- * avec evar_conv_x! Si quelqu'un comprend pourquoi, qu'il remplace ce
- * commentaire. Sinon, il va y avoir un bon coup de balai. B.B.
- *)
-let the_conv_x_leq env isevars t1 t2 =
-  is_conv_leq env !isevars t1 t2
-  or evar_conv_x env isevars CONV_LEQ t1 t2     
+let the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV     t1 t2
+let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CONV_LEQ t1 t2