From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- kernel/environ.mli | 159 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 kernel/environ.mli (limited to 'kernel/environ.mli') diff --git a/kernel/environ.mli b/kernel/environ.mli new file mode 100644 index 00000000..4e54761b --- /dev/null +++ b/kernel/environ.mli @@ -0,0 +1,159 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Univ.universes +val rel_context : env -> rel_context +val named_context : env -> named_context + +type engagement = ImpredicativeSet + +val engagement : env -> engagement option + +(* is the local context empty *) +val empty_context : env -> bool + +(************************************************************************) +(*s Context of de Bruijn variables (rel_context) *) +val push_rel : rel_declaration -> env -> env +val push_rel_context : rel_context -> env -> env +val push_rec_types : rec_declaration -> env -> env + +(* Looks up in the context of local vars referred by indice ([rel_context]) *) +(* raises [Not_found] if the index points out of the context *) +val lookup_rel : int -> env -> rel_declaration +val evaluable_rel : int -> env -> bool + +(*s Recurrence on [rel_context] *) +val fold_rel_context : + (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + +(************************************************************************) +(* Context of variables (section variables and goal assumptions) *) +val push_named : named_declaration -> env -> env + +(* Looks up in the context of local vars referred by names ([named_context]) *) +(* raises [Not_found] if the identifier is not found *) +val lookup_named : variable -> env -> named_declaration +val evaluable_named : variable -> env -> bool + +(*s Recurrence on [named_context]: older declarations processed first *) +val fold_named_context : + (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + +(* Recurrence on [named_context] starting from younger decl *) +val fold_named_context_reverse : + ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a + +(* This forgets named and rel contexts *) +val reset_context : env -> env +(* This forgets rel context and sets a new named context *) +val reset_with_named_context : named_context -> env -> env + +(************************************************************************) +(*s Global constants *) +(*s Add entries to global environment *) +val add_constant : constant -> constant_body -> env -> env + +(* Looks up in the context of global constant names *) +(* raises [Not_found] if the required path is not found *) +val lookup_constant : constant -> env -> constant_body +val evaluable_constant : constant -> env -> bool + +(*s [constant_value env c] raises [NotEvaluableConst Opaque] if + [c] is opaque and [NotEvaluableConst NoBody] if it has no + body and [Not_found] if it does not exist in [env] *) +type const_evaluation_result = NoBody | Opaque +exception NotEvaluableConst of const_evaluation_result + +val constant_value : env -> constant -> constr +val constant_type : env -> constant -> types +val constant_opt_value : env -> constant -> constr option + +(************************************************************************) +(*s Inductive types *) +val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env + +(* Looks up in the context of global inductive names *) +(* raises [Not_found] if the required path is not found *) +val lookup_mind : mutual_inductive -> env -> mutual_inductive_body + +(************************************************************************) +(*s Modules *) +val add_modtype : kernel_name -> module_type_body -> env -> env + +(* [shallow_add_module] does not add module components *) +val shallow_add_module : module_path -> module_body -> env -> env + +val lookup_module : module_path -> env -> module_body +val lookup_modtype : kernel_name -> env -> module_type_body + +(************************************************************************) +(*s Universe constraints *) +val set_universes : Univ.universes -> env -> env +val add_constraints : Univ.constraints -> env -> env + +val set_engagement : engagement -> env -> env + +(************************************************************************) +(* Sets of referred section variables *) +(* [global_vars_set env c] returns the list of [id]'s occurring as + [VAR id] in [c] *) +val global_vars_set : env -> constr -> Idset.t +(* the constr must be an atomic construction *) +val vars_of_global : env -> constr -> identifier list + +val keep_hyps : env -> Idset.t -> section_context + +(************************************************************************) +(*s Unsafe judgments. We introduce here the pre-type of judgments, which is + actually only a datatype to store a term with its type and the type of its + type. *) + +type unsafe_judgment = { + uj_val : constr; + uj_type : types } + +val make_judge : constr -> types -> unsafe_judgment +val j_val : unsafe_judgment -> constr +val j_type : unsafe_judgment -> types + +type unsafe_type_judgment = { + utj_val : constr; + utj_type : sorts } + + + + + + -- cgit v1.2.3