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.ml     | 102 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 interp/decls.mli    | 100 +++++++++++++++++++++++++++++++++++++++++++++++++++
 interp/dumpglob.ml  |   2 +-
 interp/interp.mllib |   1 +
 4 files changed, 204 insertions(+), 1 deletion(-)
 create mode 100644 interp/decls.ml
 create mode 100644 interp/decls.mli

(limited to 'interp')

diff --git a/interp/decls.ml b/interp/decls.ml
new file mode 100644
index 0000000000..933aa774b4
--- /dev/null
+++ b/interp/decls.ml
@@ -0,0 +1,102 @@
+(************************************************************************)
+(*         *   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 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
+
+let logical_kind_of_goal_kind = function
+  | DefinitionBody d -> IsDefinition d
+  | Proof s -> IsProof s
+
+(** Data 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/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
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index e1269025a4..53baf137cf 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -69,7 +69,7 @@ let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
 let continue () = glob_output := !previous_state
 
-open Decl_kinds
+open Decls
 open Declarations
 
 let type_of_logical_kind = function
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 33573edcce..cb6c527c83 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -10,6 +10,7 @@ Notation
 Syntax_def
 Smartlocate
 Constrexpr_ops
+Decls
 Dumpglob
 Reserve
 Impargs
-- 
cgit v1.2.3