Removing dubious use of evarmap manipulating functions in printing

related code.

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

4 files changed, 115 insertions, 98 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 84eba701ed..28ab4f1a5b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -809,39 +809,10 @@ let evar_dependency_closure n sigma =
 let has_no_evar sigma =
   EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
 
-let pr_evar_map_t depth sigma =
-  let { universes = uvs; univ_cstrs = univs; } = sigma in
-  let pr_evar_list l =
-    h 0 (prlist_with_sep fnl
-	   (fun (ev,evi) ->
-	     h 0 (str(string_of_existential ev) ++
-                    str"==" ++ pr_evar_info evi)) l) in
-  let evs =
-    if has_no_evar sigma then mt ()
-    else
-      match depth with
-      | None ->
-          (* Print all evars *)
-          str"EVARS:"++brk(0,1)++pr_evar_list (to_list sigma)++fnl()
-      | Some n ->
-          (* Print all evars *)
-          str"UNDEFINED EVARS"++
-          (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
-          brk(0,1)++
-          pr_evar_list (evar_dependency_closure n sigma)++fnl()
-  and svs =
-    if Univ.UniverseLSet.is_empty uvs then mt ()
-    else str"UNIVERSE VARIABLES:"++brk(0,1)++
-      h 0 (prlist_with_sep fnl
-	     (fun u -> Univ.pr_uni_level u) (Univ.UniverseLSet.elements uvs))++fnl()
-  and cs =
-    if Univ.is_initial_universes univs then mt ()
-    else str"UNIVERSES:"++brk(0,1)++
-      h 0 (Univ.pr_universes univs)++fnl()
-  in evs ++ svs ++ cs
-
 let print_env_short env =
-  let pr_body n = function None -> pr_name n | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
+  let pr_body n = function
+  | None -> pr_name n
+  | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
   let pr_named_decl (n, b, _) = pr_body (Name n) b in
   let pr_rel_decl (n, b, _) = pr_body n b in
   let nc = List.rev (named_context env) in
@@ -849,35 +820,79 @@ let print_env_short env =
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
     str "[" ++ pr_sequence pr_rel_decl rc ++ str "]"
 
-let pr_constraints pbs =
-  h 0
-    (prlist_with_sep fnl
-       (fun (pbty,env,t1,t2) ->
-	  print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-	    print_constr t1 ++ spc() ++
-	    str (match pbty with
-		 | Reduction.CONV -> "=="
-		 | Reduction.CUMUL -> "<=") ++
-	    spc() ++ print_constr t2) pbs)
-
-let pr_evar_map_constraints evd =
-  match evd.conv_pbs with
-  | [] -> mt ()
-  | _ -> pr_constraints evd.conv_pbs ++ fnl ()
-
-let pr_evar_map allevars evd =
-  let pp_evm =
-    if has_no_evar evd then mt() else
-      pr_evar_map_t allevars evd++fnl() in
-  let cstrs = match evd.conv_pbs with
-  | [] -> mt ()
-  | _ ->
-    str "CONSTRAINTS:" ++ brk(0,1) ++ pr_constraints evd.conv_pbs ++ fnl ()
+let pr_evar_constraints pbs =
+  let pr_evconstr (pbty, env, t1, t2) =
+    print_env_short env ++ spc () ++ str "|-" ++ spc () ++
+      print_constr t1 ++ spc () ++
+      str (match pbty with
+            | Reduction.CONV -> "=="
+            | Reduction.CUMUL -> "<=") ++
+      spc () ++ print_constr t2
   in
-  let pp_met =
-    if Metamap.is_empty evd.metas then mt() else
-      str"METAS:"++brk(0,1)++pr_meta_map evd.metas in
-  v 0 (pp_evm ++ cstrs ++ pp_met)
+  prlist_with_sep fnl pr_evconstr pbs
+
+let pr_evar_map_gen pr_evars sigma =
+  let { universes = uvs; univ_cstrs = univs; } = sigma in
+  let evs = if has_no_evar sigma then mt () else pr_evars sigma
+  and svs =
+    if Univ.UniverseLSet.is_empty uvs then mt ()
+    else str "UNIVERSE VARIABLES:" ++ brk (0, 1) ++
+      h 0 (prlist_with_sep fnl Univ.pr_uni_level
+        (Univ.UniverseLSet.elements uvs)) ++ fnl ()
+  and cs =
+    if Univ.is_initial_universes univs then mt ()
+    else str "UNIVERSES:" ++ brk (0, 1) ++
+      h 0 (Univ.pr_universes univs) ++ fnl ()
+  and cstrs =
+    if List.is_empty sigma.conv_pbs then mt ()
+    else
+    str "CONSTRAINTS:" ++ brk (0, 1) ++
+      pr_evar_constraints sigma.conv_pbs ++ fnl ()
+  and metas =
+    if Metamap.is_empty sigma.metas then mt ()
+    else
+      str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma.metas
+  in
+  evs ++ svs ++ cs ++ cstrs ++ metas
+
+let pr_evar_list l =
+  let pr (ev, evi) =
+    h 0 (str (string_of_existential ev) ++
+      str "==" ++ pr_evar_info evi)
+  in
+  h 0 (prlist_with_sep fnl pr l)
+
+let pr_evar_by_depth depth sigma = match depth with
+| None ->
+  (* Print all evars *)
+  str"EVARS:"++brk(0,1)++pr_evar_list (to_list sigma)++fnl()
+| Some n ->
+  (* Print all evars *)
+  str"UNDEFINED EVARS:"++
+  (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
+  brk(0,1)++
+  pr_evar_list (evar_dependency_closure n sigma)++fnl()
+
+let pr_evar_by_filter filter sigma =
+  let defined = Evar.Map.filter filter sigma.defn_evars in
+  let undefined = Evar.Map.filter filter sigma.undf_evars in
+  let prdef =
+    if Evar.Map.is_empty defined then mt ()
+    else str "DEFINED EVARS:" ++ brk (0, 1) ++
+      pr_evar_list (Evar.Map.bindings defined)
+  in
+  let prundef =
+    if Evar.Map.is_empty undefined then mt ()
+    else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
+      pr_evar_list (Evar.Map.bindings undefined)
+  in
+  prdef ++ prundef
+
+let pr_evar_map depth sigma =
+  pr_evar_map_gen (fun sigma -> pr_evar_by_depth depth sigma) sigma
+
+let pr_evar_map_filter filter sigma =
+  pr_evar_map_gen (fun sigma -> pr_evar_by_filter filter sigma) sigma
 
 let pr_metaset metas =
   str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]"
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 5ef243e136..554ce1bf2a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -112,9 +112,6 @@ val remove : evar_map -> evar -> evar_map
 val mem : evar_map -> evar -> bool
 (** Whether an evar is present in an evarmap. *)
 
-val to_list : evar_map -> (evar * evar_info) list
-(** Recover the evars as a list. This should not be used. *)
-
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 (** Apply a function to all evars and their associated info in an evarmap. *)
 
@@ -343,8 +340,10 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (** {5 Debug pretty-printers} *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_map_constraints : evar_map -> Pp.std_ppcmds
+val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
 val pr_evar_map : int option -> evar_map -> Pp.std_ppcmds
+val pr_evar_map_filter : (Evar.t -> evar_info -> bool) ->
+  evar_map -> Pp.std_ppcmds
 val pr_metaset : Metaset.t -> Pp.std_ppcmds
 
 (** {5 Deprecated functions} *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 0eacde8780..48cce3fa74 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -171,10 +171,7 @@ module Refinable = struct
   (* a pessimistic (i.e : there won't be many positive answers) filter
      over evar_maps, acting only on undefined evars *)
   let evar_map_filter_undefined f evm =
-    Evd.fold_undefined
-      (fun ev evi r -> if f ev evi then Evd.add r ev evi else r)
-      evm
-      Evd.empty
+    Evar.Map.filter f (Evd.undefined_map evm)
 
   (* Union, sorted in decreasing order, of two lists of evars in decreasing order. *)
   let rec fusion l1 l2 = match l1 , l2 with
@@ -193,7 +190,7 @@ module Refinable = struct
       post_defs
     in
     (* [delta_evars] in the shape of a list of [evar]-s*)
-    let delta_list = List.map fst (Evd.to_list delta_evars) in
+    let delta_list = List.map fst (Evar.Map.bindings delta_evars) in
     (* The variables in [myevars] are supposed to be stored
        in decreasing order. Breaking this invariant might cause
        many things to go wrong. *)
@@ -229,7 +226,7 @@ module Refinable = struct
 
   let constr_of_open_constr handle check_type (evars, c) env rdefs gl info =
     let delta = update_handle handle !rdefs evars in
-      rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
+      rdefs := Evar.Map.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
       if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
       else c
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index de77ee131c..e70d0a0e8b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -779,42 +779,48 @@ let explain_no_instance env (_,id) l =
 let is_goal_evar evi =
   match evi.evar_source with (_, Evar_kinds.GoalEvar) -> true | _ -> false
 
-let pr_constraints printenv env evm =
-  let l = Evd.to_list evm in
-  assert(not (List.is_empty l));
-  let (ev, evi) = List.hd l in
-    if List.for_all (fun (ev', evi') ->
-      eq_named_context_val evi.evar_hyps evi'.evar_hyps) l
+let pr_constraints printenv env evd evars cstrs =
+  let (ev, evi) = Evar.Map.choose evars in
+    if Evar.Map.for_all (fun ev' evi' ->
+      eq_named_context_val evi.evar_hyps evi'.evar_hyps) evars
     then
-      let pe = pr_ne_context_of (str "In environment:") (mt ())
-	(reset_with_named_context evi.evar_hyps env) in
-	(if printenv then pe ++ fnl () else mt ()) ++
-	  prlist_with_sep (fun () -> fnl ())
-	  (fun (ev, evi) -> str(string_of_existential ev) ++
-	     str " : " ++ pr_lconstr evi.evar_concl) l ++ fnl() ++
-	  pr_evar_map_constraints evm
+      let l = Evar.Map.bindings evars in
+      let pe =
+        if printenv then
+          pr_ne_context_of (str "In environment:") (mt ())
+            (reset_with_named_context evi.evar_hyps env) ++ fnl ()
+        else mt ()
+      in
+      let evs =
+        prlist_with_sep (fun () -> fnl ())
+        (fun (ev, evi) -> str(string_of_existential ev) ++
+            str " : " ++ pr_lconstr evi.evar_concl) l
+      in
+      pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs)
     else
-      pr_evar_map None evm
+      let filter evk _ = Evar.Map.mem evk evars in
+      pr_evar_map_filter filter evd
 
 let explain_unsatisfiable_constraints env evd constr =
-  let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in
+  let (_, constraints) = Evd.extract_all_conv_pbs evd in
+  let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined evd) in
   (* Remove evars that are not subject to resolution. *)
-  let undef = fold_undefined
-    (fun ev evi evm' ->
-       if not (Typeclasses.is_resolvable evi) then Evd.remove evm' ev else evm')
-    evm evm
-  in
+  let is_resolvable _ evi = Typeclasses.is_resolvable evi in
+  let undef = Evar.Map.filter is_resolvable undef in
   match constr with
   | None ->
-      str"Unable to satisfy the following constraints:" ++ fnl() ++
-	pr_constraints true env undef
+    str "Unable to satisfy the following constraints:" ++ fnl () ++
+    pr_constraints true env evd undef constraints
   | Some (ev, k) ->
-      explain_typeclass_resolution env (Evd.find evm ev) k ++ fnl () ++
-	(let remaining = Evd.remove undef ev in
-	   if Evd.has_undefined remaining then
-	     str"With the following constraints:" ++ fnl() ++
-	       pr_constraints false env remaining
-	   else mt ())
+    let cstr =
+      let remaining = Evar.Map.remove ev undef in
+      if not (Evar.Map.is_empty remaining) then
+        str "With the following constraints:" ++ fnl () ++
+          pr_constraints false env evd remaining constraints
+      else mt ()
+    in
+    let info = Evar.Map.find ev undef in
+    explain_typeclass_resolution env info k ++ fnl () ++ cstr
 
 let explain_mismatched_contexts env c i j =
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++