diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 90 |
1 files changed, 59 insertions, 31 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 20027d32ab..b8f565e45c 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -30,15 +30,20 @@ open Sign - 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 empty_env : env val universes : env -> Univ.universes val rel_context : env -> rel_context val named_context : env -> named_context - -type engagement = ImpredicativeSet +val named_context_val : env -> named_context_val val engagement : env -> engagement option @@ -47,6 +52,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 @@ -56,39 +62,41 @@ val push_rec_types : rec_declaration -> env -> env val lookup_rel : int -> env -> rel_declaration val evaluable_rel : int -> env -> bool -(* Abstract machine rel values *) -type 'a val_kind = - | VKvalue of values - | VKaxiom of 'a - | VKdef of constr * env - -type relval - -val kind_of_rel : relval -> inv_rel_key val_kind -val set_relval : relval -> values -> unit -val lookup_relval : int -> env -> relval -val nb_rel : env -> int (*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 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 -(* Abstract machine values of local vars referred by names *) -type namedval - -val kind_of_named : namedval -> identifier val_kind -val set_namedval : namedval -> values -> unit -val lookup_namedval : identifier -> env -> namedval +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 @@ -99,7 +107,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 *) @@ -108,15 +116,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 *) -type constant_key -exception NotEvaluated -exception AllReadyEvaluated -val constant_key_pos : constant_key -> int -val constant_key_body : constant_key -> constant_body -val set_pos_constant : constant_key -> int -> unit - -val lookup_constant_key : constant -> env -> constant_key val lookup_constant : constant -> env -> constant_body val evaluable_constant : constant -> env -> bool @@ -183,7 +183,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 |