diff options
author | 2015-01-25 14:42:51 +0100 | |
---|---|---|
committer | 2015-01-25 14:42:51 +0100 | |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /library/keys.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'library/keys.ml')
-rw-r--r-- | library/keys.ml | 170 |
1 files changed, 170 insertions, 0 deletions
diff --git a/library/keys.ml b/library/keys.ml new file mode 100644 index 00000000..3d277476 --- /dev/null +++ b/library/keys.ml @@ -0,0 +1,170 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +(** Keys for unification and indexing *) + +open Globnames +open Term +open Libobject + +type key = + | KGlob of global_reference + | KLam + | KLet + | KProd + | KSort + | KEvar + | KCase + | KFix + | KCoFix + | KRel + | KMeta + +module KeyOrdered = struct + type t = key + + let hash gr = + match gr with + | KGlob gr -> 10 + RefOrdered.hash gr + | KLam -> 0 + | KLet -> 1 + | KProd -> 2 + | KSort -> 3 + | KEvar -> 4 + | KCase -> 5 + | KFix -> 6 + | KCoFix -> 7 + | KRel -> 8 + | KMeta -> 9 + + let compare gr1 gr2 = + match gr1, gr2 with + | KGlob gr1, KGlob gr2 -> RefOrdered.compare gr1 gr2 + | _, KGlob _ -> -1 + | KGlob _, _ -> 1 + | k, k' -> Int.compare (hash k) (hash k') + + let equal k1 k2 = + match k1, k2 with + | KGlob gr1, KGlob gr2 -> RefOrdered.equal gr1 gr2 + | _, KGlob _ -> false + | KGlob _, _ -> false + | k, k' -> k == k' +end + +module Keymap = HMap.Make(KeyOrdered) +module Keyset = Keymap.Set + +(* Mapping structure for references to be considered equivalent *) + +type keys = Keyset.t Keymap.t + +let keys = Summary.ref Keymap.empty ~name:"Keys_decl" + +let add_kv k v m = + try Keymap.modify k (fun k' vs -> Keyset.add v vs) m + with Not_found -> Keymap.add k (Keyset.singleton v) m + +let add_keys k v = + keys := add_kv k v (add_kv v k !keys) + +let equiv_keys k k' = + k == k' || KeyOrdered.equal k k' || + try Keyset.mem k' (Keymap.find k !keys) + with Not_found -> false + +(** Registration of keys as an object *) + +let load_keys _ (_,(ref,ref')) = + add_keys ref ref' + +let cache_keys o = + load_keys 1 o + +let subst_key subst k = + match k with + | KGlob gr -> KGlob (subst_global_reference subst gr) + | _ -> k + +let subst_keys (subst,(k,k')) = + (subst_key subst k, subst_key subst k') + +let discharge_key = function + | KGlob g when Lib.is_in_section g -> + if isVarRef g then None else Some (KGlob (pop_global_reference g)) + | x -> Some x + +let discharge_keys (_,(k,k')) = + match discharge_key k, discharge_key k' with + | Some x, Some y -> Some (x, y) + | _ -> None + +let rebuild_keys (ref,ref') = (ref, ref') + +type key_obj = key * key + +let inKeys : key_obj -> obj = + declare_object {(default_object "KEYS") with + cache_function = cache_keys; + load_function = load_keys; + subst_function = subst_keys; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_keys; + rebuild_function = rebuild_keys } + +let declare_equiv_keys ref ref' = + Lib.add_anonymous_leaf (inKeys (ref,ref')) + +let constr_key c = + let open Globnames in + try + let rec aux k = + match kind_of_term k with + | Const (c, _) -> KGlob (ConstRef c) + | Ind (i, u) -> KGlob (IndRef i) + | Construct (c,u) -> KGlob (ConstructRef c) + | Var id -> KGlob (VarRef id) + | App (f, _) -> aux f + | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p)) + | Cast (p, _, _) -> aux p + | Lambda _ -> KLam + | Prod _ -> KProd + | Case _ -> KCase + | Fix _ -> KFix + | CoFix _ -> KCoFix + | Rel _ -> KRel + | Meta _ -> raise Not_found + | Evar _ -> raise Not_found + | Sort _ -> KSort + | LetIn _ -> KLet + in Some (aux c) + with Not_found -> None + +open Pp + +let pr_key pr_global = function + | KGlob gr -> pr_global gr + | KLam -> str"Lambda" + | KLet -> str"Let" + | KProd -> str"Product" + | KSort -> str"Sort" + | KEvar -> str"Evar" + | KCase -> str"Case" + | KFix -> str"Fix" + | KCoFix -> str"CoFix" + | KRel -> str"Rel" + | KMeta -> str"Meta" + +let pr_keyset pr_global v = + prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) + +let pr_mapping pr_global k v = + pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v + +let pr_keys pr_global = + Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt()) |