From 66e52c88076ba830c8c8b3cf8e4bb77959fb7843 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 20:14:46 +0200
Subject: [api] Refactor most of `Decl_kinds`

We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.

The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.

Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.

IMO this needs more work, but this should be a good start.
---
 library/decl_kinds.ml | 48 ------------------------------------------------
 library/decls.ml      | 51 ---------------------------------------------------
 library/decls.mli     | 41 -----------------------------------------
 library/kindops.ml    | 37 -------------------------------------
 library/kindops.mli   | 17 -----------------
 library/library.mllib |  3 +--
 6 files changed, 1 insertion(+), 196 deletions(-)
 delete mode 100644 library/decls.ml
 delete mode 100644 library/decls.mli
 delete mode 100644 library/kindops.ml
 delete mode 100644 library/kindops.mli

(limited to 'library')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 6eb582baef..5c479255df 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -15,51 +15,3 @@ type binding_kind = Explicit | Implicit
 type private_flag = bool
 
 type cumulative_inductive_flag = bool
-
-type theorem_kind =
-  | Theorem
-  | Lemma
-  | Fact
-  | Remark
-  | Property
-  | Proposition
-  | Corollary
-
-type definition_object_kind =
-  | Definition
-  | Coercion
-  | SubClass
-  | CanonicalStructure
-  | Example
-  | Fixpoint
-  | CoFixpoint
-  | Scheme
-  | StructureComponent
-  | IdentityCoercion
-  | Instance
-  | Method
-  | Let
-
-type assumption_object_kind = Definitional | Logical | Conjectural | Context
-
-(* [assumption_kind]
-
-                |  Local      | Global
-   ------------------------------------
-   Definitional |  Variable   | Parameter
-   Logical      |  Hypothesis | Axiom
-
-*)
-(** Kinds used in proofs *)
-
-type goal_object_kind =
-  | DefinitionBody of definition_object_kind
-  | Proof of theorem_kind
-
-(** Kinds used in library *)
-
-type logical_kind =
-  | IsPrimitive
-  | IsAssumption of assumption_object_kind
-  | IsDefinition of definition_object_kind
-  | IsProof of theorem_kind
diff --git a/library/decls.ml b/library/decls.ml
deleted file mode 100644
index 5cb35323dd..0000000000
--- a/library/decls.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** This module registers tables for some non-logical informations
-     associated declarations *)
-
-open Names
-open Decl_kinds
-open Libnames
-
-(** Datas associated to section variables and local definitions *)
-
-type variable_data = {
-  path:DirPath.t;
-  opaque:bool;
-  univs:Univ.ContextSet.t;
-  poly:bool;
-  kind:logical_kind;
-}
-
-let vartab =
-  Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
-
-let add_variable_data id o = vartab := Id.Map.add id o !vartab
-
-let variable_path id = let {path} = Id.Map.find id !vartab in path
-let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque
-let variable_kind id = let {kind} = Id.Map.find id !vartab in kind
-let variable_context id = let {univs} = Id.Map.find id !vartab in univs
-let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly
-
-let variable_secpath id =
-  let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
-  make_qualid dir id
-
-let variable_exists id = Id.Map.mem id !vartab
-
-(** Datas associated to global parameters and constants *)
-
-let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
-
-let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
-
-let constant_kind kn = Cmap.find kn !csttab
diff --git a/library/decls.mli b/library/decls.mli
deleted file mode 100644
index f88958bb04..0000000000
--- a/library/decls.mli
+++ /dev/null
@@ -1,41 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Libnames
-open Decl_kinds
-
-(** This module manages non-kernel informations about declarations. It
-    is either non-logical informations or logical informations that
-    have no place to be (yet) in the kernel *)
-
-(** Registration and access to the table of variable *)
-
-type variable_data = {
-  path:DirPath.t;
-  opaque:bool;
-  univs:Univ.ContextSet.t;
-  poly:bool;
-  kind:logical_kind;
-}
-
-val add_variable_data : variable -> variable_data -> unit
-val variable_path : variable -> DirPath.t
-val variable_secpath : variable -> qualid
-val variable_kind : variable -> logical_kind
-val variable_opacity : variable -> bool
-val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> bool
-val variable_exists : variable -> bool
-
-(** Registration and access to the table of constants *)
-
-val add_constant_kind : Constant.t -> logical_kind -> unit
-val constant_kind : Constant.t -> logical_kind
diff --git a/library/kindops.ml b/library/kindops.ml
deleted file mode 100644
index 0bf55c62a9..0000000000
--- a/library/kindops.ml
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Decl_kinds
-
-(** Operations about types defined in [Decl_kinds] *)
-
-let logical_kind_of_goal_kind = function
-  | DefinitionBody d -> IsDefinition d
-  | Proof s -> IsProof s
-
-let string_of_theorem_kind = function
-  | Theorem -> "Theorem"
-  | Lemma -> "Lemma"
-  | Fact -> "Fact"
-  | Remark -> "Remark"
-  | Property -> "Property"
-  | Proposition -> "Proposition"
-  | Corollary -> "Corollary"
-
-let string_of_definition_object_kind = function
-  | Definition -> "Definition"
-  | Example -> "Example"
-  | Coercion -> "Coercion"
-  | SubClass -> "SubClass"
-  | CanonicalStructure -> "Canonical Structure"
-  | Instance -> "Instance"
-  | Let -> "Let"
-  | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
-    CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/kindops.mli b/library/kindops.mli
deleted file mode 100644
index 3c9f2bb7c3..0000000000
--- a/library/kindops.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Decl_kinds
-
-(** Operations about types defined in [Decl_kinds] *)
-
-val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
-val string_of_theorem_kind : theorem_kind -> string
-val string_of_definition_object_kind : definition_object_kind -> string
diff --git a/library/library.mllib b/library/library.mllib
index ef53471377..35af5fa43b 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,16 +1,15 @@
+Decl_kinds
 Libnames
 Globnames
 Libobject
 Summary
 Nametab
 Global
-Decl_kinds
 Lib
 Declaremods
 Library
 States
 Kindops
 Goptions
-Decls
 Keys
 Coqlib
-- 
cgit v1.2.3