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.
---
 interp/decls.mli | 100 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 100 insertions(+)
 create mode 100644 interp/decls.mli

(limited to 'interp/decls.mli')

diff --git a/interp/decls.mli b/interp/decls.mli
new file mode 100644
index 0000000000..570f03bbce
--- /dev/null
+++ b/interp/decls.mli
@@ -0,0 +1,100 @@
+(************************************************************************)
+(*         *   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
+
+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
+
+(** Operations *)
+val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
+
+(** 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
+
+(* Not used *)
+val variable_path : variable -> DirPath.t
+
+(* Only used in dumpglob *)
+val variable_secpath : variable -> qualid
+val variable_kind : variable -> logical_kind
+
+(* User in Lemma, Very dubious *)
+val variable_opacity : variable -> bool
+
+(* Used in declare, very dubious *)
+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 *)
+
+(* Only used in dumpglob *)
+val add_constant_kind : Constant.t -> logical_kind -> unit
+val constant_kind : Constant.t -> logical_kind
-- 
cgit v1.2.3