summaryrefslogtreecommitdiff
path: root/checker/environ.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /checker/environ.mli
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'checker/environ.mli')
-rw-r--r--checker/environ.mli67
1 files changed, 67 insertions, 0 deletions
diff --git a/checker/environ.mli b/checker/environ.mli
new file mode 100644
index 00000000..a3f531dd
--- /dev/null
+++ b/checker/environ.mli
@@ -0,0 +1,67 @@
+open Names
+open Term
+
+type globals = {
+ env_constants : Declarations.constant_body Cmap.t;
+ env_inductives : Declarations.mutual_inductive_body KNmap.t;
+ env_modules : Declarations.module_body MPmap.t;
+ env_modtypes : Declarations.module_type_body MPmap.t;
+ env_alias : module_path MPmap.t;
+}
+type stratification = {
+ env_universes : Univ.universes;
+ env_engagement : Declarations.engagement option;
+}
+type env = {
+ env_globals : globals;
+ env_named_context : named_context;
+ env_rel_context : rel_context;
+ env_stratification : stratification;
+ env_imports : Digest.t MPmap.t;
+}
+val empty_env : env
+val engagement : env -> Declarations.engagement option
+val universes : env -> Univ.universes
+val named_context : env -> named_context
+val rel_context : env -> rel_context
+val set_engagement : Declarations.engagement -> env -> env
+
+val add_digest : env -> dir_path -> Digest.t -> env
+val lookup_digest : env -> dir_path -> Digest.t
+
+val lookup_rel : int -> env -> rel_declaration
+val push_rel : rel_declaration -> env -> env
+val push_rel_context : rel_context -> env -> env
+val push_rec_types : name array * constr array * 'a -> env -> env
+
+val push_named : named_declaration -> env -> env
+val lookup_named : identifier -> env -> named_declaration
+val named_type : identifier -> env -> constr
+
+val add_constraints : Univ.constraints -> env -> env
+
+val lookup_constant : constant -> env -> Declarations.constant_body
+val add_constant : constant -> Declarations.constant_body -> env -> env
+val constant_type : env -> constant -> Declarations.constant_type
+type const_evaluation_result = NoBody | Opaque
+exception NotEvaluableConst of const_evaluation_result
+val constant_value : env -> constant -> constr
+val constant_opt_value : env -> constant -> constr option
+val evaluable_constant : constant -> env -> bool
+
+val lookup_mind :
+ mutual_inductive -> env -> Declarations.mutual_inductive_body
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+val add_mind :
+ mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
+val mind_equiv : env -> inductive -> inductive -> bool
+
+val add_modtype :
+ module_path -> Declarations.module_type_body -> env -> env
+val shallow_add_module :
+ module_path -> Declarations.module_body -> env -> env
+val register_alias : module_path -> module_path -> env -> env
+val scrape_alias : module_path -> env -> module_path
+val lookup_module : module_path -> env -> Declarations.module_body
+val lookup_modtype : module_path -> env -> Declarations.module_type_body
+val lookup_alias : module_path -> env -> module_path