Suppression de la dépendance en Map.fold de ocaml dont la sémantique a

changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre
d'application des Hints de auto)


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

10 files changed, 91 insertions, 83 deletions

diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index c1175a4d9c..fd5972fb74 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -278,7 +278,7 @@ let create_with_auto_hints l depth gl=
   let h dbname=
     let hdb=
       try
-	Util.Stringmap.find dbname !searchtable 
+	searchtable_map dbname
       with Not_found-> 
 	error ("Firstorder: "^dbname^" : No such Hint database") in
       Hint_db.iter g hdb in
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 0fcb0ec7b2..e3656b1e10 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -347,16 +347,16 @@ let eauto debug np dbnames =
   let db_list =
     List.map
       (fun x -> 
-	 try Stringmap.find x !searchtable
+	 try searchtable_map x
 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
   tclTRY (e_search_auto debug np db_list)
 
 let full_eauto debug n gl = 
-  let dbnames = stringmap_dom !searchtable in
+  let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
-  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
+  let db_list = List.map searchtable_map dbnames in
   let _local_db = make_local_hint_db gl in
   tclTRY (e_search_auto debug n db_list) gl
 
@@ -365,8 +365,6 @@ let my_full_eauto n gl = full_eauto false (n,0) gl
 (**********************************************************************
    copié de tactics/auto.ml on a juste modifié search_gen
 *)
-let searchtable_map name = 
-  Stringmap.find name !searchtable
 
 (* local_db is a Hint database containing the hypotheses of current goal *)
 (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
@@ -495,9 +493,9 @@ let search = search_gen 0
 let default_search_depth = ref 5
 			     
 let full_auto n gl = 
-  let dbnames = stringmap_dom !searchtable in
+  let dbnames = current_db_names () in
   let dbnames = list_subtract dbnames ["v62"] in
-  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  let db_list = List.map searchtable_map dbnames in
   let hyps = pf_hyps gl in
   tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
   
diff --git a/interp/notation.ml b/interp/notation.ml
index 27ba0fab67..ba997126e9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -45,18 +45,18 @@ type delimiters = string
 type notation_location = dir_path * string
 
 type scope = {
-  notations: (interpretation * notation_location) Stringmap.t;
+  notations: (string, interpretation * notation_location) Gmap.t;
   delimiters: delimiters option
 }
 
 (* Uninterpreted notation map: notation -> level * dir_path *)
-let notation_level_map = ref Stringmap.empty
+let notation_level_map = ref Gmap.empty
 
 (* Scopes table: scope_name -> symbol_interpretation *)
-let scope_map = ref Stringmap.empty
+let scope_map = ref Gmap.empty
 
 let empty_scope = {
-  notations = Stringmap.empty;
+  notations = Gmap.empty;
   delimiters = None
 }
 
@@ -64,20 +64,20 @@ let default_scope = "" (* empty name, not available from outside *)
 let type_scope = "type_scope" (* special scope used for interpreting types *)
 
 let init_scope_map () =
-  scope_map := Stringmap.add default_scope empty_scope !scope_map;
-  scope_map := Stringmap.add type_scope empty_scope !scope_map
+  scope_map := Gmap.add default_scope empty_scope !scope_map;
+  scope_map := Gmap.add type_scope empty_scope !scope_map
 
 (**********************************************************************)
 (* Operations on scopes *)
 
 let declare_scope scope =
-  try let _ = Stringmap.find scope !scope_map in ()
+  try let _ = Gmap.find scope !scope_map in ()
   with Not_found ->
 (*    Options.if_verbose message ("Creating scope "^scope);*)
-    scope_map := Stringmap.add scope empty_scope !scope_map
+    scope_map := Gmap.add scope empty_scope !scope_map
 
 let find_scope scope =
-  try Stringmap.find scope !scope_map
+  try Gmap.find scope !scope_map
   with Not_found -> error ("Scope "^scope^" is not declared")
 
 let check_scope sc = let _ = find_scope sc in ()
@@ -133,7 +133,7 @@ let push_scopes = List.fold_right push_scope
 (**********************************************************************)
 (* Delimiters *)
 
-let delimiters_map = ref Stringmap.empty
+let delimiters_map = ref Gmap.empty
 
 let declare_delimiters scope key =
   let sc = find_scope scope in
@@ -143,15 +143,15 @@ let declare_delimiters scope key =
       warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
   end;
   let sc = { sc with delimiters = Some key } in
-  scope_map := Stringmap.add scope sc !scope_map;
-  if Stringmap.mem key !delimiters_map then begin
-    let oldsc = Stringmap.find key !delimiters_map in
+  scope_map := Gmap.add scope sc !scope_map;
+  if Gmap.mem key !delimiters_map then begin
+    let oldsc = Gmap.find key !delimiters_map in
     Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
   end;
-  delimiters_map := Stringmap.add key scope !delimiters_map
+  delimiters_map := Gmap.add key scope !delimiters_map
 
 let find_delimiters_scope loc key = 
-  try Stringmap.find key !delimiters_map
+  try Gmap.find key !delimiters_map
   with Not_found -> 
     user_err_loc 
     (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
@@ -254,7 +254,7 @@ let check_required_module loc sc (ref,d) =
 let find_with_delimiters = function
   | None -> None
   | Some scope ->
-      match (Stringmap.find scope !scope_map).delimiters with
+      match (Gmap.find scope !scope_map).delimiters with
 	| Some key -> Some (Some scope, Some key)
 	| None -> None
 
@@ -282,23 +282,23 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 (* Uninterpreted notation levels *)
 
 let declare_notation_level ntn level =
-  if Stringmap.mem ntn !notation_level_map then
+  if Gmap.mem ntn !notation_level_map then
     error ("Notation "^ntn^" is already assigned a level");
-  notation_level_map := Stringmap.add ntn level !notation_level_map
+  notation_level_map := Gmap.add ntn level !notation_level_map
 
 let level_of_notation ntn =
-  Stringmap.find ntn !notation_level_map
+  Gmap.find ntn !notation_level_map
 
 (* The mapping between notations and their interpretation *)
 
 let declare_notation_interpretation ntn scopt pat df =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
-  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
+  if Gmap.mem ntn sc.notations && Options.is_verbose () then
     warning ("Notation "^ntn^" was already used"^
     (if scopt = None then "" else " in scope "^scope));
-  let sc = { sc with notations = Stringmap.add ntn (pat,df) sc.notations } in
-  scope_map := Stringmap.add scope sc !scope_map;
+  let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
+  scope_map := Gmap.add scope sc !scope_map;
   if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
 
 let declare_uninterpretation rule (metas,c as pat) =
@@ -318,7 +318,7 @@ let rec find_interpretation find = function
 	find_interpretation find scopes
 
 let find_notation ntn sc =
-  Stringmap.find ntn (find_scope sc).notations
+  Gmap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
   | Numeral n when is_pos_or_zero n -> to_string n
@@ -365,7 +365,7 @@ let uninterp_cases_pattern_notations c =
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
-    Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
+    Gmap.mem ntn (Gmap.find scope !scope_map).notations in
   find_without_delimiters f (ntn_scope,Some ntn) scopes
 
 let uninterp_prim_token c =
@@ -396,8 +396,8 @@ let availability_of_prim_token printer_scope scopes =
 let exists_notation_in_scope scopt ntn r =
   let scope = match scopt with Some s -> s | None -> default_scope in
   try
-    let sc = Stringmap.find scope !scope_map in
-    let (r',_) = Stringmap.find ntn sc.notations in
+    let sc = Gmap.find scope !scope_map in
+    let (r',_) = Gmap.find ntn sc.notations in
     r' = r
   with Not_found -> false
 
@@ -531,14 +531,14 @@ let pr_notation_info prraw ntn c =
 
 let pr_named_scope prraw scope sc =
  (if scope = default_scope then
-   match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
+   match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
      | 0 -> str "No lonely notation"
      | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
   else 
     str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
   ++ fnl ()
   ++ pr_scope_classes scope
-  ++ Stringmap.fold
+  ++ Gmap.fold
        (fun ntn ((_,r),(_,df)) strm ->
 	 pr_notation_info prraw df r ++ fnl () ++ strm)
        sc.notations (mt ())
@@ -546,12 +546,12 @@ let pr_named_scope prraw scope sc =
 let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
 
 let pr_scopes prraw =
- Stringmap.fold 
+ Gmap.fold 
    (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
    !scope_map (mt ())
 
 let rec find_default ntn = function
-  | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
+  | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations ->
       Some scope
   | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
   | _::scopes -> find_default ntn scopes
@@ -575,9 +575,9 @@ let browse_notation ntn map =
     if String.contains ntn ' ' then (=) ntn
     else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
   let l =
-    Stringmap.fold 
+    Gmap.fold 
       (fun scope_name sc ->
-	Stringmap.fold (fun ntn ((_,r),df) l ->
+	Gmap.fold (fun ntn ((_,r),df) l ->
 	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
       map [] in
   let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
@@ -604,7 +604,7 @@ let locate_notation prraw ntn =
 
 let collect_notation_in_scope scope sc known =
   assert (scope <> default_scope);
-  Stringmap.fold
+  Gmap.fold
     (fun ntn ((_,r),(_,df)) (l,known as acc) ->
       if List.mem ntn known then acc else ((df,r)::l,ntn::known))
     sc.notations ([],known)
@@ -622,7 +622,7 @@ let collect_notations stack =
 	  if List.mem ntn knownntn then (all,knownntn)
 	  else
 	    let ((_,r),(_,df)) =
-	      Stringmap.find ntn (find_scope default_scope).notations in
+	      Gmap.find ntn (find_scope default_scope).notations in
 	    let all' = match all with
 	      | (s,lonelyntn)::rest when s = default_scope ->
 		  (s,(df,r)::lonelyntn)::rest
@@ -658,13 +658,13 @@ type unparsing_rule = unparsing list * precedence
 
 (* Concrete syntax for symbolic-extension table *)
 let printing_rules = 
-  ref (Stringmap.empty : unparsing_rule Stringmap.t)
+  ref (Gmap.empty : (string,unparsing_rule) Gmap.t)
 
 let declare_notation_printing_rule ntn unpl =
-  printing_rules := Stringmap.add ntn unpl !printing_rules
+  printing_rules := Gmap.add ntn unpl !printing_rules
 
 let find_notation_printing_rule ntn =
-  try Stringmap.find ntn !printing_rules
+  try Gmap.find ntn !printing_rules
   with Not_found -> anomaly ("No printing rule found for "^ntn)
 
 (**********************************************************************)
@@ -688,13 +688,13 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
 let init () =
   init_scope_map ();
 (*
-  scope_stack := Stringmap.empty
+  scope_stack := Gmap.empty
   arguments_scope := Refmap.empty
 *)
-  notation_level_map := Stringmap.empty;
-  delimiters_map := Stringmap.empty;
+  notation_level_map := Gmap.empty;
+  delimiters_map := Gmap.empty;
   notations_key_table := Gmapl.empty;
-  printing_rules := Stringmap.empty;
+  printing_rules := Gmap.empty;
   class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
 
 let _ = 
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 4febb3ad1d..858cb40c8b 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -8,7 +8,7 @@
 (* $Id$ *)
 
 (* Maps using the generic comparison function of ocaml. Code borrowed from
-   the ocaml standard library. *)
+   the ocaml standard library (Copyright 1996, INRIA). *)
 
     type ('a,'b) t =
         Empty
@@ -81,12 +81,23 @@
           let c = Pervasives.compare x v in
           c = 0 || mem x (if c < 0 then l else r)
 
-    let rec merge t1 t2 =
+    let rec min_binding = function
+        Empty -> raise Not_found
+      | Node(Empty, x, d, r, _) -> (x, d)
+      | Node(l, x, d, r, _) -> min_binding l
+
+    let rec remove_min_binding = function
+        Empty -> invalid_arg "Map.remove_min_elt"
+      | Node(Empty, x, d, r, _) -> r
+      | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
+
+    let merge t1 t2 =
       match (t1, t2) with
         (Empty, t) -> t
       | (t, Empty) -> t
-      | (Node(l1, v1, d1, r1, h1), Node(l2, v2, d2, r2, h2)) ->
-          bal l1 v1 d1 (bal (merge r1 l2) v2 d2 r2)
+      | (_, _) ->
+          let (x, d) = min_binding t2 in
+          bal t1 x d (remove_min_binding t2)
 
     let rec remove x = function
         Empty ->
@@ -109,6 +120,9 @@
         Empty               -> Empty
       | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h)
 
+    (* Maintien de fold_right par compatibilité (changé en fold_left dans
+       ocaml-3.09.0) *)
+
     let rec fold f m accu =
       match m with
         Empty -> accu
diff --git a/lib/util.ml b/lib/util.ml
index df5be249d7..4f64b3a6e4 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -119,10 +119,6 @@ module Stringset = Set.Make(struct type t = string let compare = compare end)
 
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
-let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
-
-let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
-
 (* Lists *)
 
 let list_add_set x l = if List.mem x l then l else x::l
diff --git a/lib/util.mli b/lib/util.mli
index 3993fc8519..6fbe23c289 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -72,12 +72,8 @@ val string_string_contains : where:string -> what:string -> bool
 val parse_loadpath : string -> string list
 
 module Stringset : Set.S with type elt = string
-
 module Stringmap : Map.S with type key = string
 
-val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list 
-val stringmap_dom : 'a Stringmap.t -> string list
-
 (*s Lists. *)
 
 val list_add_set : 'a -> 'a list -> 'a list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index cc6dc33e62..9d3a5a2881 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -136,24 +136,28 @@ module Hint_db = struct
 
 end
 
-type frozen_hint_db_table = Hint_db.t Stringmap.t 
+module Hintdbmap = Gmap
 
-type hint_db_table = Hint_db.t Stringmap.t ref
+type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t 
+
+type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref
 
 type hint_db_name = string
 
-let searchtable = (ref Stringmap.empty : hint_db_table)
+let searchtable = (ref Hintdbmap.empty : hint_db_table)
 
 let searchtable_map name = 
-  Stringmap.find name !searchtable
+  Hintdbmap.find name !searchtable
 let searchtable_add (name,db) = 
-  searchtable := Stringmap.add name db !searchtable
+  searchtable := Hintdbmap.add name db !searchtable
+let current_db_names () =
+  Hintdbmap.dom !searchtable
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
 (**************************************************************************)
 
-let init     () = searchtable := Stringmap.empty
+let init     () = searchtable := Hintdbmap.empty
 let freeze   () = !searchtable
 let unfreeze fs = searchtable := fs
 
@@ -498,7 +502,7 @@ let fmt_hints_db (name,db,hintlist) =
 
 (* Print all hints associated to head c in any database *)
 let fmt_hint_list_for_head c = 
-  let dbs = stringmap_to_list !searchtable in
+  let dbs = Hintdbmap.to_list !searchtable in
   let valid_dbs = 
     map_succeed 
       (fun (name,db) -> (name,db,Hint_db.map_all c db)) 
@@ -523,7 +527,7 @@ let fmt_hint_term cl =
       | [] -> assert false 
     in
     let hd = head_of_constr_reference hdc in
-    let dbs = stringmap_to_list !searchtable in
+    let dbs = Hintdbmap.to_list !searchtable in
     let valid_dbs = 
       if occur_existential cl then 
 	map_succeed 
@@ -568,7 +572,7 @@ let print_hint_db_by_name dbname =
   
 (* displays all the hints of all databases *)
 let print_searchtable () =
-  Stringmap.iter
+  Hintdbmap.iter
     (fun name db ->
        msg (str "In the database " ++ str name ++ fnl ());
        print_hint_db db)
@@ -689,7 +693,7 @@ let trivial dbnames gl =
   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
     
 let full_trivial gl =
-  let dbnames = stringmap_dom !searchtable in
+  let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
@@ -791,7 +795,7 @@ let auto n dbnames gl =
 let default_auto = auto !default_search_depth []
 
 let full_auto n gl = 
-  let dbnames = stringmap_dom !searchtable in
+  let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
   let hyps = pf_hyps gl in
@@ -904,7 +908,7 @@ let search_superauto n to_add argl g =
       to_add empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
   let db = Hint_db.add_list db0 (make_local_hint_db g) in
-  super_search n [Stringmap.find "core" !searchtable] db argl g
+  super_search n [Hintdbmap.find "core" !searchtable] db argl g
 
 let superauto n to_add argl  = 
   tclTRY (tclCOMPLETE (search_superauto n to_add argl))
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 7442c34d32..6333e088b8 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -57,11 +57,11 @@ module Hint_db :
     val iter : (global_reference -> stored_data list -> unit) -> t -> unit
   end
 
-type frozen_hint_db_table = Hint_db.t Stringmap.t
+type hint_db_name = string
 
-type hint_db_table = Hint_db.t Stringmap.t ref
+val searchtable_map : hint_db_name -> Hint_db.t
 
-type hint_db_name = string
+val current_db_names : unit -> hint_db_name list
 
 val add_hints : locality_flag -> hint_db_name list -> hints -> unit
 
@@ -73,8 +73,6 @@ val print_hint_ref : global_reference -> unit
 
 val print_hint_db_by_name : hint_db_name -> unit
 
-val searchtable : hint_db_table
-
 (* [make_exact_entry hint_name (c, ctyp)]. 
    [hint_name] is the name of then hint;
    [c] is the term given as an exact proof to solve the goal;
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0a611e6552..d92c4f2ed2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -365,16 +365,16 @@ let eauto debug np dbnames =
   let db_list =
     List.map
       (fun x -> 
-	 try Stringmap.find x !searchtable
+	 try searchtable_map x
 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
   tclTRY (e_search_auto debug np db_list)
 
 let full_eauto debug n gl = 
-  let dbnames = stringmap_dom !searchtable in
+  let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
-  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
+  let db_list = List.map searchtable_map dbnames in
   let local_db = make_local_hint_db gl in
   tclTRY (e_search_auto debug n db_list) gl
 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index dbda5fd25d..57f6a4171f 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -10,9 +10,10 @@
 open Term
 open Proof_type
 open Tacexpr
+open Auto
 (*i*)
 
-val rawwit_hintbases : string list option raw_abstract_argument_type
+val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
 val e_assumption : tactic
 
@@ -24,4 +25,5 @@ val vernac_e_resolve_constr :  constr -> tactic
 
 val e_give_exact_constr : constr -> tactic
 
-val gen_eauto : bool -> bool * int -> Util.Stringmap.key list option -> tactic
+val gen_eauto : bool -> bool * int -> hint_db_name list option -> tactic
+