diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/decls.ml | 85 | ||||
| -rw-r--r-- | interp/decls.mli | 86 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 11 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 3 | ||||
| -rw-r--r-- | interp/interp.mllib | 1 |
5 files changed, 184 insertions, 2 deletions
diff --git a/interp/decls.ml b/interp/decls.ml new file mode 100644 index 0000000000..b802dbe9c3 --- /dev/null +++ b/interp/decls.ml @@ -0,0 +1,85 @@ +(************************************************************************) +(* * 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 *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +(** 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 diff --git a/interp/decls.mli b/interp/decls.mli new file mode 100644 index 0000000000..05e4be0de6 --- /dev/null +++ b/interp/decls.mli @@ -0,0 +1,86 @@ +(************************************************************************) +(* * 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 library *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_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 diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index e1269025a4..482303d935 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 @@ -104,13 +104,20 @@ let type_of_logical_kind = function | Corollary -> "thm") | IsPrimitive -> "prim" + +(** Data associated to global parameters and constants *) + +let csttab = Summary.ref (Names.Cmap.empty : logical_kind Names.Cmap.t) ~name:"CONSTANT" +let add_constant_kind kn k = csttab := Names.Cmap.add kn k !csttab +let constant_kind kn = Names.Cmap.find kn !csttab + let type_of_global_ref gr = if Typeclasses.is_class gr then "class" else match gr with | Globnames.ConstRef cst -> - type_of_logical_kind (Decls.constant_kind cst) + type_of_logical_kind (constant_kind cst) | Globnames.VarRef v -> "var" ^ type_of_logical_kind (Decls.variable_kind v) | Globnames.IndRef ind -> diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 18955985a0..e0308b8afc 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -45,3 +45,6 @@ val dump_constraint : Names.lname -> bool -> string -> unit val dump_string : string -> unit val type_of_global_ref : Names.GlobRef.t -> string + +(** Registration of constant information *) +val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit 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 |