From 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 27 Mar 2018 02:37:19 +0200 Subject: Swapping Context and Constr: defining declarations on constr in Constr. This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate). --- kernel/environ.mli | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) (limited to 'kernel/environ.mli') diff --git a/kernel/environ.mli b/kernel/environ.mli index 8928b32f1..deca8afde 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -60,13 +60,13 @@ type stratification = { } type named_context_val = private { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; + 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 : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; + env_rel_ctx : Constr.rel_context; + env_rel_map : (Constr.rel_declaration * lazy_val) Range.t; } type env = private { @@ -88,8 +88,8 @@ 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 @@ -108,13 +108,13 @@ 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 @@ -122,12 +122,12 @@ 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 @@ -138,19 +138,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 : variable -> env -> Constr.named_declaration val lookup_named_val : variable -> env -> lazy_val -val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t +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 @@ -158,13 +158,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 @@ -280,7 +280,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 @@ -309,10 +309,10 @@ 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 -> - (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) -> (lazy_val -> 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 -- cgit v1.2.3