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

9 files changed, 75 insertions, 47 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
diff --git a/printing/printer.ml b/printing/printer.ml
index fa9bfab992..70d1c9327d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -381,6 +381,8 @@ let rec pr_evars_int i = function
               str (string_of_existential ev)  ++ str " : " ++ pegl)) ++
       (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int (i+1) rest)
 
+let pr_evars_int i evs = pr_evars_int i (Evd.ExistentialMap.bindings evs)
+
 let default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
@@ -451,7 +453,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
 	       str ".")
 	| None ->
 	    let exl = Evarutil.non_instantiated sigma in
-	    if List.is_empty exl then
+	    if ExistentialMap.is_empty exl then
 	      (str"No more subgoals."
 	       ++ emacs_print_dependent_evars sigma seeds)
 	    else
diff --git a/printing/printer.mli b/printing/printer.mli
index 7c3a64b851..18ab975d5e 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -129,7 +129,7 @@ val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 val pr_open_subgoals       : unit -> std_ppcmds
 val pr_nth_open_subgoal    : int -> std_ppcmds
 val pr_evar                : (evar * evar_info) -> std_ppcmds
-val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
+val pr_evars_int           : int -> evar_info ExistentialMap.t -> std_ppcmds
 
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 8a2c7617c6..843af1373b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -483,10 +483,11 @@ module V82 = struct
 
   (* Main function in the implementation of Grab Existential Variables.*)
   let grab pv =
+    let undef = Evd.undefined_map pv.solution in
     let goals =
       List.map begin fun (e,_) ->
 	Goal.build e
-      end (Evd.undefined_list pv.solution)
+      end (Evd.ExistentialMap.bindings undef)
     in
     { pv with comb = goals }
       
@@ -508,9 +509,10 @@ module V82 = struct
     List.flatten (List.map evars_of_initial initial)
 
   let instantiate_evar n com pv =
-    let (evk,_) = 
+    let (evk,_) =
       let evl = Evarutil.non_instantiated pv.solution in
-     if (n <= 0) then
+      let evl = Evd.ExistentialMap.bindings evl in
+      if (n <= 0) then
 	Errors.error "incorrect existential variable index"
       else if List.length evl < n then
 	  Errors.error "not so many uninstantiated existential variables"
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 660bd4f3ee..1bb6f3bcf7 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -214,7 +214,7 @@ let evars () =
     if s <> "" then msg_info (str s);
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
-    let exl = Evarutil.non_instantiated sigma in
+    let exl = Evd.ExistentialMap.bindings (Evarutil.non_instantiated sigma) in
     let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar ev); } in
     let el = List.map map_evar exl in
     Some el
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d8f08cafd0..3d85d3fafa 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -35,8 +35,8 @@ let succfix (depth, fixrels) =
 let mkMetas n = List.init n (fun _ -> Evarutil.mk_new_meta ())
 
 let check_evars env evm =
-  List.iter
-  (fun (key, evi) ->
+  Evd.ExistentialMap.iter
+  (fun key evi ->
    let (loc,k) = evar_source key evm in
      match k with
      | Evar_kinds.QuestionMark _
@@ -44,7 +44,7 @@ let check_evars env evm =
      | _ ->
        Pretype_errors.error_unsolvable_implicit loc env
          evm (Evarutil.nf_evar_info evm evi) k None)
-  (Evd.undefined_list evm)
+  (Evd.undefined_map evm)
 
 type oblinfo =
   { ev_name: int * Id.t;
@@ -207,7 +207,8 @@ let eterm_obligations env name evm fs ?status t ty =
   let nc = Environ.named_context env in
   let nc_len = Context.named_context_length nc in
   let evm = Evarutil.nf_evar_map_undefined evm in
-  let evl = List.rev (Evarutil.non_instantiated evm) in
+  let evl = Evarutil.non_instantiated evm in
+  let evl = ExistentialMap.bindings evl 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