diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 121 |
1 files changed, 73 insertions, 48 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 88d3546f..3100298e 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,57 +8,89 @@ (* Reserved names *) +open Errors open Util open Pp open Names open Nameops -open Summary open Libobject open Lib -open Topconstr -open Libnames +open Notation_term +open Notation_ops +open Globnames type key = | RefKey of global_reference | Oth -let reserve_table = ref Idmap.empty -let reserve_revtable = ref Gmapl.empty +(** TODO: share code from Notation *) -let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) - | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) - | AList (_,_,AApp (ARef ref,args),_,_) - | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) - | ARef ref -> RefKey(canonical_gr ref), None +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 ReservedSet : +sig + type t + val empty : t + val add : (Id.t * notation_constr) -> t -> t + val find : (Id.t -> notation_constr -> bool) -> t -> Id.t * notation_constr +end = +struct + type t = (Id.t * notation_constr) list + + let empty = [] + + let rec mem id c = function + | [] -> false + | (id', c') :: l -> + if c == c' && Id.equal id id' then true else mem id c l + + let add p l = + let (id, c) = p in + if mem id c l then l else p :: l + + let rec find f = function + | [] -> raise Not_found + | (id, c) as p :: l -> if f id c then p else find f l +end + + +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 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) + | NList (_,_,NApp (NRef ref,args),_,_) + | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | NRef ref -> RefKey(canonical_gr ref), None | _ -> Oth, None let cache_reserved_type (_,(id,t)) = - let key = fst (aconstr_key t) in - reserve_table := Idmap.add id t !reserve_table; - reserve_revtable := Gmapl.add key (t,id) !reserve_revtable + let key = fst (notation_constr_key t) in + reserve_table := Id.Map.add id t !reserve_table; + reserve_revtable := keymap_add key (id, t) !reserve_revtable -let in_reserved : identifier * aconstr -> obj = +let in_reserved : Id.t * notation_constr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } -let freeze_reserved () = (!reserve_table,!reserve_revtable) -let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr -let init_reserved () = - reserve_table := Idmap.empty; reserve_revtable := Gmapl.empty - -let _ = - Summary.declare_summary "reserved-type" - { Summary.freeze_function = freeze_reserved; - Summary.unfreeze_function = unfreeze_reserved; - Summary.init_function = init_reserved } - let declare_reserved_type_binding (loc,id) t = - if id <> root_of_id id then + if not (Id.equal id (root_of_id id)) then user_err_loc(loc,"declare_reserved_type", (pr_id id ++ str " is not reservable: it must have no trailing digits, quote, or _")); begin try - let _ = Idmap.find id !reserve_table in + let _ = Id.Map.find id !reserve_table in user_err_loc(loc,"declare_reserved_type", (pr_id id++str" is already bound to a type")) with Not_found -> () end; @@ -67,7 +99,7 @@ let declare_reserved_type_binding (loc,id) t = let declare_reserved_type idl t = List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl) -let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table +let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table let constr_key c = try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c)))) @@ -75,25 +107,18 @@ let constr_key c = let revert_reserved_type t = try - let l = Gmapl.find (constr_key t) !reserve_revtable in - let t = Detyping.detype false [] [] t in - list_try_find - (fun (pat,id) -> - try let _ = match_aconstr false t ([],pat) in Name id - with No_match -> failwith "") l + let reserved = KeyMap.find (constr_key t) !reserve_revtable in + let t = Detyping.detype false [] (Global.env()) Evd.empty t in + (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] + then I've introduced a bug... *) + let filter _ pat = + try + let _ = match_notation_constr false t ([], pat) in + true + with No_match -> false + in + let (id, _) = ReservedSet.find filter reserved in + Name id with Not_found | Failure _ -> Anonymous let _ = Namegen.set_reserved_typed_name revert_reserved_type - -open Glob_term - -let anonymize_if_reserved na t = match na with - | Name id as na -> - (try - if not !Flags.raw_print & - (try aconstr_of_glob_constr [] [] t = find_reserved_type id - with UserError _ -> false) - then GHole (dummy_loc,Evd.BinderType na) - else t - with Not_found -> t) - | Anonymous -> t |