Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 65 insertions, 5 deletions

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