Getting rid of module Gmapl.

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

2 files changed, 70 insertions, 14 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index b11a0f47ce..80e23ce6a7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -214,8 +214,37 @@ type key =
   | RefKey of global_reference
   | Oth
 
+let key_compare k1 k2 = match k1, k2 with
+| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2
+| RefKey _, Oth -> -1
+| Oth, RefKey _ -> 1
+| Oth, Oth -> 0
+
+module KeyOrd = struct type t = key let compare = key_compare end
+module KeyMap = Map.Make(KeyOrd)
+
+module InterpretationOrd =
+struct
+  type t = interp_rule * interpretation * int option
+  let compare = Pervasives.compare (* FIXME: to be explicitely written *)
+end
+
+module InterpretationSet = Set.Make (InterpretationOrd)
+(** ppedrot: We changed the semantics here. Before it was a FIFO stack, now it
+    is an ordered set with an badly defined comparison... *)
+
+let keymap_add key interp map =
+  let old = try KeyMap.find key map with Not_found -> InterpretationSet.empty in
+  KeyMap.add key (InterpretationSet.add interp old) map
+
+let keymap_find key map =
+  try
+    let set = KeyMap.find key map in
+    InterpretationSet.elements set
+  with Not_found -> []
+
 (* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref Gmapl.empty
+let notations_key_table = ref (KeyMap.empty : InterpretationSet.t KeyMap.t)
 let prim_token_key_table = Hashtbl.create 7
 
 let glob_prim_constr_key = function
@@ -364,7 +393,7 @@ let declare_notation_interpretation ntn scopt pat df =
 
 let declare_uninterpretation rule (metas,c as pat) =
   let (key,n) = notation_constr_key c in
-  notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
+  notations_key_table := keymap_add key (rule,pat,n) !notations_key_table
 
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
@@ -422,14 +451,14 @@ let interp_notation loc ntn local_scopes =
     (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
 
 let uninterp_notations c =
-  List.map_append (fun key -> Gmapl.find key !notations_key_table)
+  List.map_append (fun key -> keymap_find key !notations_key_table)
     (glob_constr_keys c)
 
 let uninterp_cases_pattern_notations c =
-  Gmapl.find (cases_pattern_key c) !notations_key_table
+  keymap_find (cases_pattern_key c) !notations_key_table
 
 let uninterp_ind_pattern_notations ind =
-  Gmapl.find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+  keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
@@ -932,7 +961,7 @@ let init () =
 *)
   notation_level_map := String.Map.empty;
   delimiters_map := String.Map.empty;
-  notations_key_table := Gmapl.empty;
+  notations_key_table := KeyMap.empty;
   printing_rules := String.Map.empty;
   scope_class_map := ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 0efcafcd23..0ab7ec6c7d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -16,14 +16,38 @@ open Nameops
 open Libobject
 open Lib
 open Notation_term
+open Notation_ops
 open Globnames
 
 type key =
   | RefKey of global_reference
   | Oth
 
+(** TODO: share code from Notation *)
+
+let key_compare k1 k2 = match k1, k2 with
+| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2
+| RefKey _, Oth -> -1
+| Oth, RefKey _ -> 1
+| Oth, Oth -> 0
+
+module KeyOrd = struct type t = key let compare = key_compare end
+module KeyMap = Map.Make(KeyOrd)
+
+module ReservedOrd =
+struct
+  type t = notation_constr * Id.t
+  let compare = Pervasives.compare (* FIXME *)
+end
+
+module ReservedSet = Set.Make(ReservedOrd)
+
+let keymap_add key data map =
+  let old = try KeyMap.find key map with Not_found -> ReservedSet.empty in
+  KeyMap.add key (ReservedSet.add data old) map
+
 let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type"
-let reserve_revtable = Summary.ref Gmapl.empty ~name:"reserved-type-rev"
+let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
@@ -35,7 +59,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 let cache_reserved_type (_,(id,t)) =
   let key = fst (notation_constr_key t) in
   reserve_table := Id.Map.add id t !reserve_table;
-  reserve_revtable := Gmapl.add key (t,id) !reserve_revtable
+  reserve_revtable := keymap_add key (t,id) !reserve_revtable
 
 let in_reserved : Id.t * notation_constr -> obj =
   declare_object {(default_object "RESERVED-TYPE") with
@@ -64,15 +88,18 @@ let constr_key c =
 
 let revert_reserved_type t =
   try
-    let l = Gmapl.find (constr_key t) !reserve_revtable in
+    let reserved = KeyMap.find (constr_key t) !reserve_revtable in
     let t = Detyping.detype false [] [] t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
-    let find (pat, id) =
-      try let _ = Notation_ops.match_notation_constr false t ([], pat) in true
-      with Notation_ops.No_match -> false
+    let filter (pat, id) =
+      try
+        let _ = match_notation_constr false t ([], pat) in
+        true
+      with No_match -> false
     in
-    let (_, id) = List.find find l in
+    let reserved = ReservedSet.filter filter reserved in
+    let (_, id) = ReservedSet.choose reserved in
     Name id
   with Not_found | Failure _ -> Anonymous
 
@@ -85,7 +112,7 @@ let anonymize_if_reserved na t = match na with
       (try
 	if not !Flags.raw_print &&
 	   (try
-            let ntn = Notation_ops.notation_constr_of_glob_constr [] [] t in
+            let ntn = notation_constr_of_glob_constr [] [] t in
             Pervasives.(=) ntn (find_reserved_type id) (** FIXME *)
             with UserError _ -> false)
 	then GHole (Loc.ghost,Evar_kinds.BinderType na)