Partly replacing list-based access functions in Evd. This is still

unsatisfactory as some functions implicitly require some ordering
on the evars, but this is already better.

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

4 files changed, 60 insertions, 37 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f52694edf0..84f7254b1b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -236,8 +236,8 @@ let evars_to_metas sigma (emap, c) =
 (* The list of non-instantiated existential declarations (order is important) *)
 
 let non_instantiated sigma =
-  let listev = Evd.undefined_list sigma in
-  List.map (fun (ev,evi) -> (ev,nf_evar_info sigma evi)) listev
+  let listev = Evd.undefined_map sigma in
+  ExistentialMap.map (fun evi -> nf_evar_info sigma evi) listev
 
 (************************)
 (* Manipulating filters *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 5f8a4bd375..7d917f15bd 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -64,7 +64,7 @@ val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
    returns the evar_map extended with dependent evars *)
 val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
 
-val non_instantiated : evar_map -> (evar * evar_info) list
+val non_instantiated : evar_map -> evar_info ExistentialMap.t
 
 (** {6 Unification utils} *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 35c0b73e3a..2c4ae94815 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -125,10 +125,8 @@ module EvarInfoMap = struct
     ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) undef;
     !l
 
-  let undefined_list (def,undef) =
-    (* Order is important: needs ocaml >= 3.08.4 from which "fold" is a
-       "fold_left" *)
-    ExistentialMap.fold (fun evk evi l -> (evk,evi)::l) undef []
+  let undefined_map (def, undef) = undef
+  let defined_map (def, undef) = def
 
   let undefined_evars (def,undef) = (ExistentialMap.empty,undef)
   let defined_evars (def,undef) = (def,ExistentialMap.empty)
@@ -219,7 +217,8 @@ module EvarMap = struct
   let remove (sigma,sm) k = (EvarInfoMap.remove sigma k, sm)
   let mem (sigma,_) = EvarInfoMap.mem sigma
   let to_list (sigma,_) = EvarInfoMap.to_list sigma
-  let undefined_list (sigma,_) = EvarInfoMap.undefined_list sigma
+  let undefined_map (sigma,_) = EvarInfoMap.undefined_map sigma
+  let defined_map (sigma,_) = EvarInfoMap.defined_map sigma
   let undefined_evars (sigma,sm) = (EvarInfoMap.undefined_evars sigma, sm)
   let defined_evars (sigma,sm) = (EvarInfoMap.defined_evars sigma, sm)
   let fold (sigma,_) = EvarInfoMap.fold sigma
@@ -346,7 +345,8 @@ let mem d e = EvarMap.mem d.evars e
 (* spiwack: this function loses information from the original evar_map
    it might be an idea not to export it. *)
 let to_list d = EvarMap.to_list d.evars
-let undefined_list d = EvarMap.undefined_list d.evars
+let undefined_map d = EvarMap.undefined_map d.evars
+let defined_map d = EvarMap.defined_map d.evars
 let undefined_evars d = { d with evars=EvarMap.undefined_evars d.evars }
 let defined_evars d = { d with evars=EvarMap.defined_evars d.evars }
 (* spiwack: not clear what folding over an evar_map, for now we shall
@@ -778,29 +778,48 @@ let pr_evar_info evi =
     (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]" ++
        candidates ++ spc() ++ src)
 
-let compute_evar_dependency_graph (sigma:evar_map) =
+let compute_evar_dependency_graph (sigma : evar_map) =
   (* Compute the map binding ev to the evars whose body depends on ev *)
-  fold (fun evk evi acc ->
-    let deps =
-      match evar_body evi with
-      | Evar_empty -> ExistentialSet.empty
-      | Evar_defined c -> collect_evars c in
-    ExistentialSet.fold (fun evk' acc ->
-      let tab = try ExistentialMap.find evk' acc with Not_found -> [] in
-      ExistentialMap.add evk' ((evk,evi)::tab) acc) deps acc)
-    sigma ExistentialMap.empty
+  let fold evk evi acc =
+    let fold_ev evk' acc =
+      let tab =
+        try ExistentialMap.find evk' acc
+        with Not_found -> ExistentialSet.empty
+      in
+      ExistentialMap.add evk' (ExistentialSet.add evk tab) acc
+    in
+    match evar_body evi with
+    | Evar_empty -> acc
+    | Evar_defined c -> ExistentialSet.fold fold_ev (collect_evars c) acc
+  in
+  EvarMap.fold sigma.evars fold ExistentialMap.empty
 
 let evar_dependency_closure n sigma =
+  (** Create the DAG of depth [n] representing the recursive dependencies of
+      undefined evars. *)
   let graph = compute_evar_dependency_graph sigma in
-  let order a b = fst a < fst b in
-  let rec aux n l =
-    if Int.equal n 0 then l
+  let rec aux n curr accu =
+    if Int.equal n 0 then ExistentialSet.union curr accu
     else
-      let l' =
-        List.map_append (fun (evk,_) ->
-          try ExistentialMap.find evk graph with Not_found -> []) l in
-      aux (n-1) (List.uniquize (Sort.list order (l@l'))) in
-  aux n (undefined_list sigma)
+      let fold evk accu =
+        try
+          let deps = ExistentialMap.find evk graph in
+          ExistentialSet.union deps accu
+        with Not_found -> accu
+      in
+      (** Consider only the newly added evars *)
+      let ncurr = ExistentialSet.fold fold curr ExistentialSet.empty in
+      (** Merge the others *)
+      let accu = ExistentialSet.union curr accu in
+      aux (n - 1) ncurr accu
+  in
+  let undef = ExistentialMap.domain (undefined_map sigma) in
+  aux n undef ExistentialSet.empty
+
+let evar_dependency_closure n sigma =
+  let deps = evar_dependency_closure n sigma in
+  let map = ExistentialMap.bind (fun ev -> find sigma ev) deps in
+  ExistentialMap.bindings map
 
 let pr_evar_map_t depth sigma =
   let (evars,(uvs,univs)) = sigma.evars in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 59e176543f..8dfc81fe8f 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -120,6 +120,10 @@ val evar_filtered_env :  evar_info -> env
 (*** Unification state ***)
 type evar_map
 
+module ExistentialSet : Set.S with type elt = existential_key
+module ExistentialMap : Map.ExtS
+  with type key = existential_key and module Set := ExistentialSet
+
 (** Unification state and existential variables *)
 
 (** Assuming that the second map extends the first one, this says if
@@ -140,10 +144,14 @@ val find : evar_map -> evar -> evar_info
 val find_undefined : evar_map -> evar -> evar_info
 val remove : evar_map -> evar -> evar_map
 val mem : evar_map -> evar -> bool
-val undefined_list : evar_map -> (evar * evar_info) list
 val to_list : evar_map -> (evar * evar_info) list
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+
 val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+(** [fold_undefined f m] iterates ("folds") function [f] over the undefined
+    evars (that is, whose value is [Evar_empty]) of map [m].
+    It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
+
 val define : evar -> constr -> evar_map -> evar_map
 
 val is_evar : evar_map -> evar -> bool
@@ -153,6 +161,9 @@ val is_undefined : evar_map -> evar -> bool
 
 val add_constraints : evar_map -> Univ.constraints -> evar_map
 
+val undefined_map : evar_map -> evar_info ExistentialMap.t
+val defined_map : evar_map -> evar_info ExistentialMap.t
+
 (** {6 ... } *)
 (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
     no body and [Not_found] if it does not exist in [sigma] *)
@@ -170,13 +181,10 @@ val subst_evar_defs_light : substitution -> evar_map -> evar_map
 (** spiwack: this function seems to somewhat break the abstraction. *)
 val evars_reset_evd  : ?with_conv_pbs:bool -> evar_map ->  evar_map -> evar_map
 
-
 val undefined_evars : evar_map -> evar_map
 val defined_evars : evar_map -> evar_map
-(* [fold_undefined f m] iterates ("folds") function [f] over the undefined
-    evars (that is, whose value is [Evar_empty]) of map [m].
-    It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
-val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+(** TODO: see where we can replace those functions by their [_map] variant. *)
+
 val evar_declare :
   named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
       ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
@@ -187,10 +195,6 @@ type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_map -> evar_map
 
-module ExistentialSet : Set.S with type elt = existential_key
-module ExistentialMap : Map.ExtS
-  with type key = existential_key and module Set := ExistentialSet
-
 val extract_changed_conv_pbs : evar_map ->
       (ExistentialSet.t -> evar_constraint -> bool) ->
       evar_map * evar_constraint list