Partial fix for bug #1948: recompute order of dependencies between

evars at the end of unification as later evars can refer to
previous ones. This removes the assumption that evars are already
ordered in eterm's code.


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

5 files changed, 57 insertions, 14 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index c2d7a59f1b..6e522d499a 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 (**
    - Get types of existentials ;
    - Flatten dependency tree (prefix order) ;
@@ -129,12 +130,34 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
+let evar_dependencies evm ev =
+  let one_step deps = 
+    Intset.fold (fun ev s -> 
+      let evi = Evd.find evm ev in
+	Intset.union (Evarutil.evars_of_evar_info evi) s)
+      deps deps
+  in 
+  let rec aux deps =
+    let deps' = one_step deps in
+      if Intset.equal deps deps' then deps
+      else aux deps'
+  in aux (Intset.singleton ev)
+
+let sort_dependencies evl =
+  List.sort (fun (_, _, deps) (_, _, deps') -> 
+    if Intset.subset deps deps' then (* deps' depends on deps *) -1
+    else if Intset.subset deps' deps then 1
+    else Intset.compare deps deps')
+    evl
+    
 let eterm_obligations env name isevars evm fs ?status t ty = 
-  (* 'Serialize' the evars, we assume that the types of the existentials
-     refer to previous existentials in the list only *)
+  (* 'Serialize' the evars *)
   let nc = Environ.named_context env in
   let nc_len = Sign.named_context_length nc in
   let evl = List.rev (to_list evm) in
+  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
+  let sevl = sort_dependencies evl in
+  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
   let evn = 
     let i = ref (-1) in
       List.rev_map (fun (id, ev) -> incr i; 
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index e197024ff4..a2010c9016 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -16,6 +16,9 @@ open Util
 
 val mkMetas : int -> constr list
 
+val evar_dependencies : evar_map -> int -> Intset.t
+val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list
+
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 63a56f0d13..5491607153 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1054,7 +1054,28 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
   with e when precatchable_exception e ->
     (evd,false)
 
-
+let evars_of_term c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) -> Intset.add n acc
+    | _ -> fold_constr evrec acc c
+  in 
+    evrec Intset.empty c
+
+let evars_of_named_context nc =
+  List.fold_right (fun (_, b, t) s ->
+    Option.fold_left (fun s t -> 
+      Intset.union s (evars_of_term t))
+      s b) nc Intset.empty
+
+let evars_of_evar_info evi =
+  Intset.union (evars_of_term evi.evar_concl)
+    (Intset.union 
+	(match evi.evar_body with 
+	| Evar_empty -> Intset.empty
+	| Evar_defined b -> evars_of_term b)
+	(evars_of_named_context (named_context_of_val evi.evar_hyps)))
+    
 (* [check_evars] fails if some unresolved evar remains *)
 (* it assumes that the defined existentials have already been substituted *)
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d11e1fa2a5..ab9f8bebb1 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -94,6 +94,10 @@ val is_unification_pattern_evar : env -> existential -> constr list -> bool
 val is_unification_pattern : env -> constr -> constr array -> bool
 val solve_pattern_eqn : env -> constr list -> constr -> constr
 
+val evars_of_term : constr -> Intset.t
+val evars_of_named_context : named_context -> Intset.t
+val evars_of_evar_info : evar_info -> Intset.t
+
 (***********************************************************)
 (* Value/Type constraints *)
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 115e47ae18..e9bd15b119 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -61,14 +61,6 @@ let init_setoid () =
 
 (** Typeclasses instance search tactic / eauto *)
 
-let evars_of_term init c = 
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) -> Intset.add n acc
-    | _ -> fold_constr evrec acc c
-  in 
-    evrec init c
-
 let intersects s t =
   Intset.exists (fun el -> Intset.mem el t) s
 
@@ -183,14 +175,14 @@ let rec catchable = function
   | e -> Logic.catchable_exception e
 
 let is_dep gl gls =
-  let evs = evars_of_term Intset.empty gl.evar_concl in
+  let evs = Evarutil.evars_of_term gl.evar_concl in
     if evs = Intset.empty then false
     else
       List.fold_left
 	(fun b gl -> 
 	  if b then b 
 	  else
-	    let evs' = evars_of_term Intset.empty gl.evar_concl in
+	    let evs' = Evarutil.evars_of_term gl.evar_concl in
 	      intersects evs evs')
 	false gls
 	
@@ -455,7 +447,7 @@ let rec merge_deps deps = function
 	
 let split_evars evm =
   Evd.fold (fun ev evi acc ->
-    let deps = evars_of_term (Intset.singleton ev) evi.evar_concl in
+    let deps = Intset.union (Intset.singleton ev) (Evarutil.evars_of_term evi.evar_concl) in
       merge_deps deps acc)
     evm []