From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/environ.mli | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 65 insertions(+), 5 deletions(-) (limited to 'kernel/environ.mli') diff --git a/kernel/environ.mli b/kernel/environ.mli index a2a66cb7..701159da 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,v 1.66.2.2 2005/01/21 16:41:49 herbelin Exp $ i*) +(*i $Id: environ.mli 7640 2005-12-05 10:16:24Z gregoire $ i*) (*i*) open Names @@ -22,21 +22,30 @@ open Sign (* Environments have the following components: - 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 global constants and axioms - a context for inductive definitions - a set of universe constraints - a flag telling if Set is, can be, or cannot be set impredicative *) + + + type env +val pre_env : env -> Pre_env.env + +type named_context_val +val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> Univ.universes val rel_context : env -> rel_context val named_context : env -> named_context +val named_context_val : env -> named_context_val -type engagement = ImpredicativeSet val engagement : env -> engagement option @@ -45,6 +54,7 @@ val empty_context : env -> bool (************************************************************************) (*s Context of de Bruijn variables ([rel_context]) *) +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 @@ -60,14 +70,35 @@ val fold_rel_context : (************************************************************************) (* Context of variables (section variables and goal assumptions) *) + +val named_context_of_val : named_context_val -> named_context +val val_of_named_context : named_context -> named_context_val +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 : + (constr -> constr) -> named_context_val -> named_context_val + val push_named : named_declaration -> env -> env +val push_named_context_val : + named_declaration -> named_context_val -> named_context_val + + (* 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 +val lookup_named : variable -> env -> named_declaration +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 : (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a @@ -78,7 +109,7 @@ val fold_named_context_reverse : (* 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 +val reset_with_named_context : named_context_val -> env -> env (************************************************************************) (*s Global constants *) @@ -87,6 +118,7 @@ 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 @@ -153,7 +185,35 @@ type unsafe_type_judgment = { utj_type : sorts } +(*s Compilation of global declaration *) + +val compile_constant_body : + env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code + (* opaque *) (* boxed *) + +(*s Functions for proofs/logic.ml *) +val clear_hyps : + variable list -> (variable list -> named_declaration -> unit) -> + named_context_val -> named_context_val * variable list + +exception Hyp_not_found +(* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and + return [tail::(f head (id,_,_) (rev tail))::head]. + the value associated to id should not change *) +val apply_to_hyp : named_context_val -> variable -> + (named_context -> named_declaration -> named_context -> named_declaration) -> + named_context_val +(* [apply_to_hyp_and_dependent_on sign id f g] split [sign] into + [tail::(id,_,_)::head] and + return [(g tail)::(f (id,_,_))::head]. *) +val apply_to_hyp_and_dependent_on : named_context_val -> variable -> + (named_declaration -> named_context_val -> named_declaration) -> + (named_declaration -> named_context_val -> named_declaration) -> + named_context_val +val insert_after_hyp : named_context_val -> variable -> + named_declaration -> + (named_context -> unit) -> named_context_val -- cgit v1.2.3