From 70aecacb204bb4d86f9eb021540fe9322cabb0bf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Aug 2019 20:37:05 +0200 Subject: [api] Move `Keys` to pretyping This file is unrelated to library, but to pretyping/unification. This commit, along with others already submitted go towards the goal of `library` containing only the handling of library objects. --- library/keys.ml | 162 ---------------------------------------------- library/keys.mli | 23 ------- library/library.mllib | 1 - pretyping/keys.ml | 162 ++++++++++++++++++++++++++++++++++++++++++++++ pretyping/keys.mli | 23 +++++++ pretyping/pretyping.mllib | 1 + 6 files changed, 186 insertions(+), 186 deletions(-) delete mode 100644 library/keys.ml delete mode 100644 library/keys.mli create mode 100644 pretyping/keys.ml create mode 100644 pretyping/keys.mli diff --git a/library/keys.ml b/library/keys.ml deleted file mode 100644 index 9964992433..0000000000 --- a/library/keys.ml +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 9 + GlobRef.Ordered.hash gr - | KLam -> 0 - | KLet -> 1 - | KProd -> 2 - | KSort -> 3 - | KCase -> 4 - | KFix -> 5 - | KCoFix -> 6 - | KRel -> 7 - | KInt -> 8 - - let compare gr1 gr2 = - match gr1, gr2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.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 -> GlobRef.Ordered.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 *) - -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 (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None - | x -> Some x - -let discharge_keys (_,(k,k')) = - match discharge_key k, discharge_key k' with - | Some x, Some y -> Some (x, y) - | _ -> None - -type key_obj = key * key - -let inKeys : key_obj -> obj = - declare_object @@ superglobal_object "KEYS" - ~cache:cache_keys - ~subst:(Some subst_keys) - ~discharge:discharge_keys - -let declare_equiv_keys ref ref' = - Lib.add_anonymous_leaf (inKeys (ref,ref')) - -let constr_key kind c = - try - let rec aux k = - match kind k with - | Const (c, _) -> KGlob (GlobRef.ConstRef c) - | Ind (i, u) -> KGlob (GlobRef.IndRef i) - | Construct (c,u) -> KGlob (GlobRef.ConstructRef c) - | Var id -> KGlob (GlobRef.VarRef id) - | App (f, _) -> aux f - | Proj (p, _) -> KGlob (GlobRef.ConstRef (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 - | Int _ -> KInt - 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" - | KCase -> str"Case" - | KFix -> str"Fix" - | KCoFix -> str"CoFix" - | KRel -> str"Rel" - | KInt -> str"Int" - -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()) diff --git a/library/keys.mli b/library/keys.mli deleted file mode 100644 index a7adf7791b..0000000000 --- a/library/keys.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* key -> unit -(** Declare two keys as being equivalent. *) - -val equiv_keys : key -> key -> bool -(** Check equivalence of keys. *) - -val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option -(** Compute the head key of a term. *) - -val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t -(** Pretty-print the mapping *) diff --git a/library/library.mllib b/library/library.mllib index 35af5fa43b..84937ede93 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -11,5 +11,4 @@ Library States Kindops Goptions -Keys Coqlib diff --git a/pretyping/keys.ml b/pretyping/keys.ml new file mode 100644 index 0000000000..f8eecd80d4 --- /dev/null +++ b/pretyping/keys.ml @@ -0,0 +1,162 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* 9 + GlobRef.Ordered.hash gr + | KLam -> 0 + | KLet -> 1 + | KProd -> 2 + | KSort -> 3 + | KCase -> 4 + | KFix -> 5 + | KCoFix -> 6 + | KRel -> 7 + | KInt -> 8 + + let compare gr1 gr2 = + match gr1, gr2 with + | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.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 -> GlobRef.Ordered.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 *) + +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 (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None + | x -> Some x + +let discharge_keys (_,(k,k')) = + match discharge_key k, discharge_key k' with + | Some x, Some y -> Some (x, y) + | _ -> None + +type key_obj = key * key + +let inKeys : key_obj -> obj = + declare_object @@ superglobal_object "KEYS" + ~cache:cache_keys + ~subst:(Some subst_keys) + ~discharge:discharge_keys + +let declare_equiv_keys ref ref' = + Lib.add_anonymous_leaf (inKeys (ref,ref')) + +let constr_key kind c = + try + let rec aux k = + match kind k with + | Const (c, _) -> KGlob (GlobRef.ConstRef c) + | Ind (i, u) -> KGlob (GlobRef.IndRef i) + | Construct (c,u) -> KGlob (GlobRef.ConstructRef c) + | Var id -> KGlob (GlobRef.VarRef id) + | App (f, _) -> aux f + | Proj (p, _) -> KGlob (GlobRef.ConstRef (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 + | Int _ -> KInt + 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" + | KCase -> str"Case" + | KFix -> str"Fix" + | KCoFix -> str"CoFix" + | KRel -> str"Rel" + | KInt -> str"Int" + +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()) diff --git a/pretyping/keys.mli b/pretyping/keys.mli new file mode 100644 index 0000000000..a7adf7791b --- /dev/null +++ b/pretyping/keys.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* key -> unit +(** Declare two keys as being equivalent. *) + +val equiv_keys : key -> key -> bool +(** Check equivalence of keys. *) + +val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option +(** Compute the head key of a term. *) + +val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t +(** Pretty-print the mapping *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 34a6cecc95..0ca39f0404 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -35,4 +35,5 @@ Indrec GlobEnv Cases Pretyping +Keys Unification -- cgit v1.2.3