diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 112 |
1 files changed, 81 insertions, 31 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index fdd84b25..f45b7be8 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -28,23 +28,63 @@ open Declarations - a set of universe constraints - a flag telling if Set is, can be, or cannot be set impredicative *) +type lazy_val +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option +val dummy_lazy_val : unit -> lazy_val +(** Linking information for the native compiler *) +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type key = int CEphemeron.key option ref + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals +(** globals = constants + projections + inductive types + modules + module-types *) + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type named_context_val = private { + env_named_ctx : Constr.named_context; + env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; +} + +type rel_context_val = private { + env_rel_ctx : Constr.rel_context; + env_rel_map : (Constr.rel_declaration * lazy_val) Range.t; +} + +type env = private { + env_globals : globals; + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} -type env -val pre_env : env -> Pre_env.env -val env_of_pre_env : Pre_env.env -> env val oracle : env -> Conv_oracle.oracle val set_oracle : env -> Conv_oracle.oracle -> env -type named_context_val val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t -val rel_context : env -> Context.Rel.t -val named_context : env -> Context.Named.t +val rel_context : env -> Constr.rel_context +val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val val opaque_tables : env -> Opaqueproof.opaquetab @@ -63,24 +103,26 @@ val empty_context : env -> bool (** {5 Context of de Bruijn variables ([rel_context]) } *) val nb_rel : env -> int -val push_rel : Context.Rel.Declaration.t -> env -> env -val push_rel_context : Context.Rel.t -> env -> env +val push_rel : Constr.rel_declaration -> env -> env +val push_rel_context : Constr.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 -> Context.Rel.Declaration.t +val lookup_rel : int -> env -> Constr.rel_declaration +val lookup_rel_val : int -> env -> lazy_val val evaluable_rel : int -> env -> bool +val env_of_rel : int -> env -> env (** {6 Recurrence on [rel_context] } *) val fold_rel_context : - (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Constr.rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a (** {5 Context of variables (section variables and goal assumptions) } *) -val named_context_of_val : named_context_val -> Context.Named.t -val val_of_named_context : Context.Named.t -> named_context_val +val named_context_of_val : named_context_val -> Constr.named_context +val val_of_named_context : Constr.named_context -> named_context_val val empty_named_context_val : named_context_val val ids_of_named_context_val : named_context_val -> Id.Set.t @@ -91,18 +133,19 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t val map_named_val : (constr -> constr) -> named_context_val -> named_context_val -val push_named : Context.Named.Declaration.t -> env -> env -val push_named_context : Context.Named.t -> env -> env +val push_named : Constr.named_declaration -> env -> env +val push_named_context : Constr.named_context -> env -> env val push_named_context_val : - Context.Named.Declaration.t -> named_context_val -> named_context_val + Constr.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 Id.t is not found *) -val lookup_named : variable -> env -> Context.Named.Declaration.t -val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t +val lookup_named : variable -> env -> Constr.named_declaration +val lookup_named_val : variable -> env -> lazy_val +val lookup_named_ctxt : variable -> named_context_val -> Constr.named_declaration val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option @@ -110,11 +153,13 @@ val named_body : variable -> env -> constr option (** {6 Recurrence on [named_context]: older declarations processed first } *) val fold_named_context : - (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + +val set_universes : env -> UGraph.t -> env (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : - ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a + ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a (** This forgets named and rel contexts *) val reset_context : env -> env @@ -125,12 +170,16 @@ val reset_with_named_context : named_context_val -> env -> env (** This removes the [n] last declarations from the rel context *) val pop_rel_context : int -> env -> env +(** Useful for printing *) +val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a + (** {5 Global constants } {6 Add entries to global environment } *) val add_constant : Constant.t -> constant_body -> env -> env -val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info -> +val add_constant_key : Constant.t -> constant_body -> link_info -> env -> env +val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) @@ -168,11 +217,15 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option (** {6 Primitive projections} *) -val lookup_projection : Names.Projection.t -> env -> projection_body -val is_projection : Constant.t -> env -> bool +(** Checks that the number of parameters is correct. *) +val lookup_projection : Names.Projection.t -> env -> types + +val get_projection : env -> inductive -> proj_arg:int -> Names.Projection.Repr.t option +val get_projections : env -> inductive -> Names.Projection.Repr.t array option (** {5 Inductive types } *) -val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env +val lookup_mind_key : MutInd.t -> env -> mind_key +val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names @@ -228,7 +281,7 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.Named.t +val keep_hyps : env -> Id.Set.t -> Constr.named_context (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is @@ -251,20 +304,16 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(** {6 Compilation of global declaration } *) - -val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option - 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 -> - (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> + (Constr.named_context -> Constr.named_declaration -> Constr.named_context -> Constr.named_declaration) -> named_context_val -val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val @@ -272,10 +321,11 @@ open Retroknowledge (** functions manipulating the retroknowledge @author spiwack *) val retroknowledge : (retroknowledge->'a) -> env -> 'a +[@@ocaml.deprecated "Use the record projection."] val registered : env -> field -> bool val register : env -> field -> Retroknowledge.entry -> env (** Native compiler *) -val no_link_info : Pre_env.link_info +val no_link_info : link_info |