diff options
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | interp/notation.ml | 41 | ||||
| -rw-r--r-- | interp/reserve.ml | 43 | ||||
| -rw-r--r-- | lib/gmapl.ml | 33 | ||||
| -rw-r--r-- | lib/gmapl.mli | 21 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 | ||||
| -rw-r--r-- | toplevel/autoinstance.ml | 26 |
7 files changed, 91 insertions, 75 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index e7e342204..01b44f148 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -29,7 +29,6 @@ Envars Gmap Fset Fmap -Gmapl Profile Explore Predicate diff --git a/interp/notation.ml b/interp/notation.ml index b11a0f47c..80e23ce6a 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 0efcafcd2..0ab7ec6c7 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) diff --git a/lib/gmapl.ml b/lib/gmapl.ml deleted file mode 100644 index 4be8f4baf..000000000 --- a/lib/gmapl.ml +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util - -type ('a,'b) t = ('a,'b list) Gmap.t - -let empty = Gmap.empty -let mem = Gmap.mem -let iter = Gmap.iter -let map = Gmap.map -let fold = Gmap.fold - -let add x y m = - try - let l = Gmap.find x m in - Gmap.add x (y::List.except y l) m - with Not_found -> - Gmap.add x [y] m - -let find x m = - try Gmap.find x m with Not_found -> [] - -let remove x y m = - let l = Gmap.find x m in - Gmap.add x (if List.mem y l then List.subtract l [y] else l) m - - diff --git a/lib/gmapl.mli b/lib/gmapl.mli deleted file mode 100644 index 5e7720886..000000000 --- a/lib/gmapl.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Maps from ['a] to lists of ['b]. *) - -type ('a,'b) t - -val empty : ('a,'b) t -val mem : 'a -> ('a,'b) t -> bool -val iter : ('a -> 'b list -> unit) -> ('a,'b) t -> unit -val map : ('b list -> 'c list) -> ('a,'b) t -> ('a,'c) t -val fold : ('a -> 'b list -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c - -val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t -val find : 'a -> ('a,'b) t -> 'b list -val remove : 'a -> 'b -> ('a,'b) t -> ('a,'b) t diff --git a/lib/lib.mllib b/lib/lib.mllib index 0ff2d97e9..088bbf010 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -12,7 +12,6 @@ Gmap Fset Fmap Tries -Gmapl Profile Explore Predicate diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index f8a76f874..049d631bf 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -223,22 +223,38 @@ let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ct | Prod (n,t,c) -> iter_under_prod f ((n,None,t)::ctx) c | _ -> () +module GREMOrd = +struct + type t = Globnames.global_reference * Evd.evar_map + let compare (gr1, _) (gr2, _) = Globnames.RefOrdered.compare gr1 gr2 + (** ppedrot: this code was actually already broken before this modification, + and used polymorphic equality over evar maps, which is just bad. Now we + simply ignore it, which looks more sensible. *) +end + +module GREM = Map.Make(GREMOrd) + +let grem_add key data map = + try + let l = GREM.find key map in + GREM.add key (data :: l) map + with Not_found -> + GREM.add key [data] map + (* main search function: search for total instances containing gr, and apply k to each of them *) let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature -> unit) : unit = let gr_c = Globnames.constr_of_global gr in - let (smap:(Globnames.global_reference * Evd.evar_map, - ('a * 'b * Term.constr) list * Evd.evar) - Gmapl.t ref) = ref Gmapl.empty in + let smap = ref GREM.empty in iter_under_prod ( fun ctx typ -> List.iter (fun ((cl,ev,evm),_,_) -> (* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Pp.int ev++str " dans "++pr_evar_map evm);*) - smap := Gmapl.add (cl,evm) (ctx,ev) !smap) + smap := grem_add (cl,evm) (ctx,ev) !smap) (Recordops.methods_matching typ) ) [] deftyp; - Gmapl.iter + GREM.iter ( fun (cl,evm) evl -> let f = if Typeclasses.is_class cl then declare_class_instance else declare_record_instance in |