From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/environ.mli | 42 ++++++++++++++++++------------------------ 1 file changed, 18 insertions(+), 24 deletions(-) (limited to 'kernel/environ.mli') diff --git a/kernel/environ.mli b/kernel/environ.mli index b68123f6..667a0ed4 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: environ.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Names @@ -15,7 +15,7 @@ open Declarations open Sign (*i*) -(*s Unsafe environments. We define here a datatype for environments. +(*s Unsafe environments. We define here a datatype for environments. Since typing is not yet defined, it is not possible to check the informations added in environments, and that is why we speak here of ``unsafe'' environments. *) @@ -24,7 +24,7 @@ open Sign - a context for de Bruijn variables - a context for de Bruijn variables vm values - a context for section variables and goal assumptions - - a context for section variables and goal assumptions vm values + - a context for section variables and goal assumptions vm values - a context for global constants and axioms - a context for inductive definitions - a set of universe constraints @@ -55,7 +55,7 @@ val empty_context : env -> bool (************************************************************************) (*s Context of de Bruijn variables ([rel_context]) *) -val nb_rel : env -> int +val nb_rel : env -> int val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env val push_rec_types : rec_declaration -> env -> env @@ -80,12 +80,12 @@ val empty_named_context_val : named_context_val (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. - *** /!\ *** [f t] should be convertible with t *) -val map_named_val : + *** /!\ *** [f t] should be convertible with t *) +val map_named_val : (constr -> constr) -> named_context_val -> named_context_val val push_named : named_declaration -> env -> env -val push_named_context_val : +val push_named_context_val : named_declaration -> named_context_val -> named_context_val @@ -98,7 +98,7 @@ val lookup_named_val : variable -> named_context_val -> named_declaration val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option - + (*s Recurrence on [named_context]: older declarations processed first *) val fold_named_context : @@ -142,9 +142,6 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env (* raises [Not_found] if the required path is not found *) val lookup_mind : mutual_inductive -> env -> mutual_inductive_body -(* Find the ultimate inductive in the [mind_equiv] chain *) -val scrape_mind : env -> mutual_inductive -> mutual_inductive - (************************************************************************) (*s Modules *) val add_modtype : module_path -> module_type_body -> env -> env @@ -155,10 +152,6 @@ val shallow_add_module : module_path -> module_body -> env -> env val lookup_module : module_path -> env -> module_body val lookup_modtype : module_path -> env -> module_type_body -val register_alias : module_path -> module_path -> env -> env -val lookup_alias : module_path -> env -> module_path -val scrape_alias : module_path -> env -> module_path - (************************************************************************) (*s Universe constraints *) val set_universes : Univ.universes -> env -> env @@ -168,10 +161,11 @@ 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] *) +(* [global_vars_set env c] returns the list of [id]'s occurring either + directly as [Var id] in [c] or indirectly as a section variable + dependent in a global reference occurring in [c] *) val global_vars_set : env -> constr -> Idset.t -(* the constr must be an atomic construction *) +(* the constr must be a global reference *) val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context @@ -181,7 +175,7 @@ val keep_hyps : env -> Idset.t -> section_context actually only a datatype to store a term with its type and the type of its type. *) -type unsafe_judgment = { +type unsafe_judgment = { uj_val : constr; uj_type : types } @@ -189,14 +183,14 @@ val make_judge : constr -> types -> unsafe_judgment val j_val : unsafe_judgment -> constr val j_type : unsafe_judgment -> types -type unsafe_type_judgment = { +type unsafe_type_judgment = { utj_val : constr; utj_type : sorts } (*s Compilation of global declaration *) -val compile_constant_body : +val compile_constant_body : env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code (* opaque *) (* boxed *) @@ -206,7 +200,7 @@ exception Hyp_not_found return [tail::(f head (id,_,_) (rev tail))::head]. the value associated to id should not change *) -val apply_to_hyp : named_context_val -> variable -> +val apply_to_hyp : named_context_val -> variable -> (named_context -> named_declaration -> named_context -> named_declaration) -> named_context_val @@ -219,7 +213,7 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable -> named_context_val val insert_after_hyp : named_context_val -> variable -> - named_declaration -> + named_declaration -> (named_context -> unit) -> named_context_val val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val @@ -250,7 +244,7 @@ type context_object = module OrderedContextObject : Set.OrderedType with type t = context_object module ContextObjectMap : Map.S with type key = context_object -(* collects all the assumptions (optionally including opaque definitions) +(* collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type) *) val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t -- cgit v1.2.3