aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/context.ml356
-rw-r--r--kernel/context.mli243
-rw-r--r--kernel/cooking.ml6
-rw-r--r--kernel/csymtable.ml5
-rw-r--r--kernel/declarations.mli7
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/environ.ml27
-rw-r--r--kernel/environ.mli45
-rw-r--r--kernel/fast_typeops.ml2
-rw-r--r--kernel/indtypes.ml33
-rw-r--r--kernel/indtypes.mli4
-rw-r--r--kernel/inductive.ml15
-rw-r--r--kernel/inductive.mli9
-rw-r--r--kernel/nativecode.ml9
-rw-r--r--kernel/opaqueproof.ml2
-rw-r--r--kernel/opaqueproof.mli2
-rw-r--r--kernel/pre_env.ml17
-rw-r--r--kernel/pre_env.mli13
-rw-r--r--kernel/reduction.ml17
-rw-r--r--kernel/reduction.mli7
-rw-r--r--kernel/term.ml33
-rw-r--r--kernel/term.mli37
-rw-r--r--kernel/term_typing.ml5
-rw-r--r--kernel/typeops.ml7
-rw-r--r--kernel/typeops.mli5
-rw-r--r--kernel/vars.ml11
-rw-r--r--kernel/vars.mli15
27 files changed, 533 insertions, 401 deletions
diff --git a/kernel/context.ml b/kernel/context.ml
index 5923048fa..372f16a8d 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -15,137 +15,233 @@
(* This file defines types and combinators regarding indexes-based and
names-based contexts *)
-open Util
-open Names
-
-(***************************************************************************)
-(* Type of assumptions *)
-(***************************************************************************)
-
-type named_declaration = Id.t * Constr.t option * Constr.t
-type named_list_declaration = Id.t list * Constr.t option * Constr.t
-type rel_declaration = Name.t * Constr.t option * Constr.t
-
-let map_named_declaration_skel f (id, (v : Constr.t option), ty) =
- (id, Option.map f v, f ty)
-let map_named_list_declaration = map_named_declaration_skel
-let map_named_declaration = map_named_declaration_skel
-
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty
-let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
-
-let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
-let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
-
-let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
- Id.equal i1 i2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
- Name.equal n1 n2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-(***************************************************************************)
-(* Type of local contexts (telescopes) *)
-(***************************************************************************)
-
-(*s Signatures of ordered optionally named variables, intended to be
- accessed by de Bruijn indices (to represent bound variables) *)
-
-type rel_context = rel_declaration list
-
-let empty_rel_context = []
-
-let add_rel_decl d ctxt = d::ctxt
-
-let rec lookup_rel n sign =
- match n, sign with
- | 1, decl :: _ -> decl
- | n, _ :: sign -> lookup_rel (n-1) sign
- | _, [] -> raise Not_found
-
-let rel_context_length = List.length
+(** The modules defined below represent a {e local context}
+ as defined by Chapter 4 in the Reference Manual:
-let rel_context_nhyps hyps =
- let rec nhyps acc = function
- | [] -> acc
- | (_,None,_)::hyps -> nhyps (1+acc) hyps
- | (_,Some _,_)::hyps -> nhyps acc hyps in
- nhyps 0 hyps
+ A {e local context} is an ordered list of of {e local declarations}
+ of names that we call {e variables}.
-let rel_context_tags ctx =
- let rec aux l = function
- | [] -> l
- | (_,Some _,_)::ctx -> aux (true::l) ctx
- | (_,None,_)::ctx -> aux (false::l) ctx
- in aux [] ctx
+ A {e local declaration} of some variable can be either:
+ - a {e local assumption}, or
+ - a {e local definition}.
+*)
-(*s Signatures of named hypotheses. Used for section variables and
- goal assumptions. *)
-
-type named_context = named_declaration list
-type named_list_context = named_list_declaration list
-
-let empty_named_context = []
-
-let add_named_decl d sign = d::sign
-
-let rec lookup_named id = function
- | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
- | _ :: sign -> lookup_named id sign
- | [] -> raise Not_found
-
-let named_context_length = List.length
-let named_context_equal = List.equal eq_named_declaration
-
-let vars_of_named_context ctx =
- List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx
-
-let instance_from_named_context sign =
- let filter = function
- | (id, None, _) -> Some (Constr.mkVar id)
- | (_, Some _, _) -> None
- in
- List.map_filter filter sign
-
-(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
- with n = |Δ| and with the local definitions of [Γ] skipped in
- [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-
-let extended_rel_list n hyps =
- let rec reln l p = function
- | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
- | (_, Some _, _) :: hyps -> reln l (p+1) hyps
- | [] -> l
- in
- reln [] 1 hyps
-
-let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
-
-let fold_named_context f l ~init = List.fold_right f l init
-let fold_named_list_context f l ~init = List.fold_right f l init
-let fold_named_context_reverse f ~init l = List.fold_left f init l
-
-(*s Signatures of ordered section variables *)
-type section_context = named_context
-
-let fold_rel_context f l ~init:x = List.fold_right f l x
-let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
-
-let map_context f l =
- let map_decl (n, body_o, typ as decl) =
- let body_o' = Option.smartmap f body_o in
- let typ' = f typ in
- if body_o' == body_o && typ' == typ then decl else
- (n, body_o', typ')
- in
- List.smartmap map_decl l
-
-let map_rel_context = map_context
-let map_named_context = map_context
+open Util
+open Names
-let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
+ Individual declarations are then designated by de Bruijn indexes. *)
+module Rel =
+ struct
+ (** Representation of {e local declarations}.
+
+ [(name, None, typ)] represents a {e local assumption}.
+ In the Reference Manual we denote them as [(name:typ)].
+
+ [(name, Some value, typ)] represents a {e local definition}.
+ In the Reference Manual we denote them as [(name := value : typ)].
+ *)
+ module Declaration =
+ struct
+ type t = Name.t * Constr.t option * Constr.t
+
+ (** Map all terms in a given declaration. *)
+ let map f (n, v, ty) = (n, Option.map f v, f ty)
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
+
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ let exists f (_, v, ty) = Option.cata f false v || f ty
+
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ let for_all f (_, v, ty) = Option.cata f true v && f ty
+
+ (** Check whether the two given declarations are equal. *)
+ let equal (n1, v1, ty1) (n2, v2, ty2) =
+ Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+ end
+
+ (** Rel-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Declaration.t list
+
+ (** empty rel-context *)
+ let empty = []
+
+ (** Return a new rel-context enriched by with a given inner-most declaration. *)
+ let add d ctx = d :: ctx
+
+ (** Return a declaration designated by a given de Bruijn index.
+ @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
+ let rec lookup n ctx =
+ match n, ctx with
+ | 1, decl :: _ -> decl
+ | n, _ :: sign -> lookup (n-1) sign
+ | _, [] -> raise Not_found
+
+ (** Map all terms in a given rel-context. *)
+ let map f =
+ let map_decl (n, body_o, typ as decl) =
+ let body_o' = Option.smartmap f body_o in
+ let typ' = f typ in
+ if body_o' == body_o && typ' == typ then decl else
+ (n, body_o', typ')
+ in
+ List.smartmap map_decl
+
+ (** Reduce all terms in a given rel-context to a single value.
+ Innermost declarations are processed first. *)
+ let fold_inside f ~init = List.fold_left f init
+
+ (** Reduce all terms in a given rel-context to a single value.
+ Outermost declarations are processed first. *)
+ let fold_outside f l ~init = List.fold_right f l init
+
+ (** Perform a given action on every declaration in a given rel-context. *)
+ let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+
+ (** Return the number of {e local declarations} in a given context. *)
+ let length = List.length
+
+ (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+ with n = |Δ| and with the local definitions of [Γ] skipped in
+ [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ let nhyps =
+ let rec nhyps acc = function
+ | [] -> acc
+ | (_,None,_)::hyps -> nhyps (1+acc) hyps
+ | (_,Some _,_)::hyps -> nhyps acc hyps in
+ nhyps 0
+
+ (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
+ and each {e local definition} is mapped to [false]. *)
+ let to_tags =
+ let rec aux l = function
+ | [] -> l
+ | (_,Some _,_)::ctx -> aux (true::l) ctx
+ | (_,None,_)::ctx -> aux (false::l) ctx
+ in aux []
+
+ (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+ with n = |Δ| and with the {e local definitions} of [Γ] skipped in
+ [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ let to_extended_list n =
+ let rec reln l p = function
+ | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+ | (_, Some _, _) :: hyps -> reln l (p+1) hyps
+ | [] -> l
+ in
+ reln [] 1
+
+ (** [extended_vect n Γ] does the same, returning instead an array. *)
+ let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+ end
+
+(** This module represents contexts that can capture non-anonymous variables.
+ Individual declarations are then designated by the identifiers they bind. *)
+module Named =
+ struct
+ (** Representation of {e local declarations}.
+
+ [(id, None, typ)] represents a {e local assumption}.
+ In the Reference Manual we denote them as [(name:typ)].
+
+ [(id, Some value, typ)] represents a {e local definition}.
+ In the Reference Manual we denote them as [(name := value : typ)].
+ *)
+ module Declaration =
+ struct
+ (** Named-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Id.t * Constr.t option * Constr.t
+
+ (** Map all terms in a given declaration. *)
+ let map = Rel.Declaration.map
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
+
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ let exists f (_, v, ty) = Option.cata f false v || f ty
+
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ let for_all f (_, v, ty) = Option.cata f true v && f ty
+
+ (** Check whether the two given declarations are equal. *)
+ let equal (i1, v1, ty1) (i2, v2, ty2) =
+ Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+ end
+
+ type t = Declaration.t list
+
+ (** empty named-context *)
+ let empty = []
+
+ (** empty named-context *)
+ let add d ctx = d :: ctx
+
+ (** Return a declaration designated by a given de Bruijn index.
+ @raise Not_found if the designated identifier is not present in the designated named-context. *)
+ let rec lookup id = function
+ | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
+ | _ :: sign -> lookup id sign
+ | [] -> raise Not_found
+
+ (** Map all terms in a given named-context. *)
+ let map f =
+ let map_decl (n, body_o, typ as decl) =
+ let body_o' = Option.smartmap f body_o in
+ let typ' = f typ in
+ if body_o' == body_o && typ' == typ then decl else
+ (n, body_o', typ')
+ in
+ List.smartmap map_decl
+
+ (** Reduce all terms in a given named-context to a single value.
+ Innermost declarations are processed first. *)
+ let fold_inside f ~init = List.fold_left f init
+
+ (** Reduce all terms in a given named-context to a single value.
+ Outermost declarations are processed first. *)
+ let fold_outside f l ~init = List.fold_right f l init
+
+ (** Perform a given action on every declaration in a given named-context. *)
+ let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+
+ (** Return the number of {e local declarations} in a given named-context. *)
+ let length = List.length
+
+ (** Check whether given two named-contexts are equal. *)
+ let equal = List.equal Declaration.equal
+
+ (** Return the set of all identifiers bound in a given named-context. *)
+ let to_vars =
+ List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty
+
+ (** [instance_from_named_context Ω] builds an instance [args] such
+ that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+ definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+ gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
+ let to_instance =
+ let filter = function
+ | (id, None, _) -> Some (Constr.mkVar id)
+ | (_, Some _, _) -> None
+ in
+ List.map_filter filter
+ end
+
+module NamedList =
+ struct
+ module Declaration =
+ struct
+ type t = Id.t list * Constr.t option * Constr.t
+ let map = Named.Declaration.map
+ end
+ type t = Declaration.t list
+ let fold f l ~init = List.fold_right f l init
+ end
+
+type section_context = Named.t
diff --git a/kernel/context.mli b/kernel/context.mli
index 735467747..0db82beb5 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -6,131 +6,186 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** The modules defined below represent a {e local context}
+ as defined by Chapter 4 in the Reference Manual:
+
+ A {e local context} is an ordered list of of {e local declarations}
+ of names that we call {e variables}.
+
+ A {e local declaration} of some variable can be either:
+ - a {e local assumption}, or
+ - a {e local definition}.
+
+ {e Local assumptions} are denoted in the Reference Manual as [(name : typ)] and
+ {e local definitions} are there denoted as [(name := value : typ)].
+*)
+
open Names
-(** TODO: cleanup *)
+(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
+ Individual declarations are then designated by de Bruijn indexes. *)
+module Rel :
+sig
+ (** Representation of {e local declarations}.
+
+ [(name, None, typ)] represents a {e local assumption}.
+
+ [(name, Some value, typ)] represents a {e local definition}.
+ *)
+ module Declaration :
+ sig
+ type t = Name.t * Constr.t option * Constr.t
+
+ (** Map all terms in a given declaration. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ val exists : (Constr.t -> bool) -> t -> bool
+
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ val for_all : (Constr.t -> bool) -> t -> bool
+
+ (** Check whether the two given declarations are equal. *)
+ val equal : t -> t -> bool
+ end
+
+ (** Rel-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Declaration.t list
+
+ (** empty rel-context *)
+ val empty : t
+
+ (** Return a new rel-context enriched by with a given inner-most declaration. *)
+ val add : Declaration.t -> t -> t
+
+ (** Return a declaration designated by a given de Bruijn index.
+ @raise Not_found if the designated de Bruijn index outside the range. *)
+ val lookup : int -> t -> Declaration.t
+
+ (** Map all terms in a given rel-context. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
-(** {6 Declarations} *)
-(** A {e declaration} has the form [(name,body,type)]. It is either an
- {e assumption} if [body=None] or a {e definition} if
- [body=Some actualbody]. It is referred by {e name} if [na] is an
- identifier or by {e relative index} if [na] is not an identifier
- (in the latter case, [na] is of type [name] but just for printing
- purpose) *)
+ (** Reduce all terms in a given rel-context to a single value.
+ Innermost declarations are processed first. *)
+ val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
-type named_declaration = Id.t * Constr.t option * Constr.t
-type named_list_declaration = Id.t list * Constr.t option * Constr.t
-type rel_declaration = Name.t * Constr.t option * Constr.t
+ (** Reduce all terms in a given rel-context to a single value.
+ Outermost declarations are processed first. *)
+ val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
-val map_named_declaration :
- (Constr.t -> Constr.t) -> named_declaration -> named_declaration
-val map_named_list_declaration :
- (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration
-val map_rel_declaration :
- (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration
+ (** Perform a given action on every declaration in a given rel-context. *)
+ val iter : (Constr.t -> unit) -> t -> unit
-val fold_named_declaration :
- (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
- (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+ (** Return the number of {e local declarations} in a given context. *)
+ val length : t -> int
-val exists_named_declaration :
- (Constr.t -> bool) -> named_declaration -> bool
-val exists_rel_declaration :
- (Constr.t -> bool) -> rel_declaration -> bool
+ (** Return the number of {e local assumptions} in a given rel-context. *)
+ val nhyps : t -> int
-val for_all_named_declaration :
- (Constr.t -> bool) -> named_declaration -> bool
-val for_all_rel_declaration :
- (Constr.t -> bool) -> rel_declaration -> bool
+ (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
+ and each {e local definition} is mapped to [false]. *)
+ val to_tags : t -> bool list
-val eq_named_declaration :
- named_declaration -> named_declaration -> bool
+ (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+ with n = |Δ| and with the {e local definitions} of [Γ] skipped in
+ [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ val to_extended_list : int -> t -> Constr.t list
-val eq_rel_declaration :
- rel_declaration -> rel_declaration -> bool
+ (** [extended_vect n Γ] does the same, returning instead an array. *)
+ val to_extended_vect : int -> t -> Constr.t array
+end
-(** {6 Signatures of ordered named declarations } *)
+(** This module represents contexts that can capture non-anonymous variables.
+ Individual declarations are then designated by the identifiers they bind. *)
+module Named :
+sig
+ (** Representation of {e local declarations}.
-type named_context = named_declaration list
-type section_context = named_context
-type named_list_context = named_list_declaration list
-type rel_context = rel_declaration list
-(** In [rel_context], more recent declaration is on top *)
+ [(id, None, typ)] represents a {e local assumption}.
-val empty_named_context : named_context
-val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.Set.t
+ [(id, Some value, typ)] represents a {e local definition}.
+ *)
+ module Declaration :
+ sig
+ type t = Id.t * Constr.t option * Constr.t
-val lookup_named : Id.t -> named_context -> named_declaration
+ (** Map all terms in a given declaration. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
-(** number of declarations *)
-val named_context_length : named_context -> int
+ (** Reduce all terms in a given declaration to a single value. *)
+ val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
-(** named context equality *)
-val named_context_equal : named_context -> named_context -> bool
+ (** Check whether any term in a given declaration satisfies a given predicate. *)
+ val exists : (Constr.t -> bool) -> t -> bool
-(** {6 Recurrence on [named_context]: older declarations processed first } *)
-val fold_named_context :
- (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+ (** Check whether all terms in a given declaration satisfy a given predicate. *)
+ val for_all : (Constr.t -> bool) -> t -> bool
-val fold_named_list_context :
- (named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a
+ (** Check whether the two given declarations are equal. *)
+ val equal : t -> t -> bool
+ end
-(** newer declarations first *)
-val fold_named_context_reverse :
- ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
+ (** Rel-context is represented as a list of declarations.
+ Inner-most declarations are at the beginning of the list.
+ Outer-most declarations are at the end of the list. *)
+ type t = Declaration.t list
-(** {6 Section-related auxiliary functions } *)
+ (** empty named-context *)
+ val empty : t
-(** [instance_from_named_context Ω] builds an instance [args] such
- that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
- definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
- gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
-val instance_from_named_context : named_context -> Constr.t list
+ (** Return a new rel-context enriched by with a given inner-most declaration. *)
+ val add : Declaration.t -> t -> t
-(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
- with n = |Δ| and with the local definitions of [Γ] skipped in
- [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-val extended_rel_list : int -> rel_context -> Constr.t list
+ (** Return a declaration designated by an identifier of the variable bound in that declaration.
+ @raise Not_found if the designated identifier is not bound in a given named-context. *)
+ val lookup : Id.t -> t -> Declaration.t
-(** [extended_rel_vect n Γ] does the same, returning instead an array. *)
-val extended_rel_vect : int -> rel_context -> Constr.t array
+ (** Map all terms in a given named-context. *)
+ val map : (Constr.t -> Constr.t) -> t -> t
-(** {6 ... } *)
-(** Signatures of ordered optionally named variables, intended to be
- accessed by de Bruijn indices *)
+ (** Reduce all terms in a given named-context to a single value.
+ Innermost declarations are processed first. *)
+ val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
-(** {6 Recurrence on [rel_context]: older declarations processed first } *)
-val fold_rel_context :
- (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+ (** Reduce all terms in a given named-context to a single value.
+ Outermost declarations are processed first. *)
+ val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
-(** newer declarations first *)
-val fold_rel_context_reverse :
- ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
+ (** Perform a given action on every declaration in a given named-context. *)
+ val iter : (Constr.t -> unit) -> t -> unit
-(** {6 Map function of [rel_context] } *)
-val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context
+ (** Return the number of {e local declarations} in a given named-context. *)
+ val length : t -> int
-(** {6 Map function of [named_context] } *)
-val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context
+ (** Check whether given two named-contexts are equal. *)
+ val equal : t -> t -> bool
-(** {6 Map function of [rel_context] } *)
-val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit
+ (** Return the set of all identifiers bound in a given named-context. *)
+ val to_vars : t -> Id.Set.t
-(** {6 Map function of [named_context] } *)
-val iter_named_context : (Constr.t -> unit) -> named_context -> unit
+ (** [instance_from_named_context Ω] builds an instance [args] such
+ that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+ definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+ gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
+ val to_instance : t -> Constr.t list
+end
-(** {6 Contexts of declarations referred to by de Bruijn indices } *)
+module NamedList :
+sig
+ module Declaration :
+ sig
+ type t = Id.t list * Constr.t option * Constr.t
+ val map : (Constr.t -> Constr.t) -> t -> t
+ end
-val empty_rel_context : rel_context
-val add_rel_decl : rel_declaration -> rel_context -> rel_context
+ type t = Declaration.t list
-val lookup_rel : int -> rel_context -> rel_declaration
-(** Size of the [rel_context] including LetIns *)
-val rel_context_length : rel_context -> int
-(** Size of the [rel_context] without LetIns *)
-val rel_context_nhyps : rel_context -> int
-(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
-val rel_context_tags : rel_context -> bool list
+ val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
+end
+type section_context = Named.t
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index be71bd7b4..1302e71c9 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -173,7 +173,7 @@ let expmod_constr_subst cache modlist subst c =
let cook_constr { Opaqueproof.modlist ; abstract } c =
let cache = RefTable.create 13 in
let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
- let hyps = Context.map_named_context expmod (pi1 abstract) in
+ let hyps = Context.Named.map expmod (pi1 abstract) in
abstract_constant_body (expmod c) hyps
let lift_univs cb subst =
@@ -195,13 +195,13 @@ let cook_constant env { from = cb; info } =
let abstract, usubst, abs_ctx = abstract in
let usubst, univs = lift_univs cb usubst in
let expmod = expmod_constr_subst cache modlist usubst in
- let hyps = Context.map_named_context expmod abstract in
+ let hyps = Context.Named.map expmod abstract in
let body = on_body modlist (hyps, usubst, abs_ctx)
(fun c -> abstract_constant_body (expmod c) hyps)
cb.const_body
in
let const_hyps =
- Context.fold_named_context (fun (h,_,_) hyps ->
+ Context.Named.fold_outside (fun (h,_,_) hyps ->
List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
hyps ~init:cb.const_hyps in
let typ = match cb.const_type with
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index aa9ef66fe..2067eb899 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -15,7 +15,6 @@
open Util
open Names
open Term
-open Context
open Vm
open Cemitcodes
open Cbytecodes
@@ -190,7 +189,7 @@ and slot_for_fv env fv =
let nv = Pre_env.lookup_named_val id env in
begin match force_lazy_val nv with
| None ->
- let _, b, _ = Context.lookup_named id env.env_named_context in
+ let _, b, _ = Context.Named.lookup id env.env_named_context in
fill_fv_cache nv id val_of_named idfun b
| Some (v, _) -> v
end
@@ -198,7 +197,7 @@ and slot_for_fv env fv =
let rv = Pre_env.lookup_rel_val i env in
begin match force_lazy_val rv with
| None ->
- let _, b, _ = lookup_rel i env.env_rel_context in
+ let _, b, _ = Context.Rel.lookup i env.env_rel_context in
fill_fv_cache rv i val_of_rel env_of_rel b
| Some (v, _) -> v
end
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index dc5c17a75..981dfe05e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
(** This module defines the internal representation of global
declarations. This includes global constants/axioms, mutual
@@ -38,7 +37,7 @@ type ('a, 'b) declaration_arity =
| RegularArity of 'a
| TemplateArity of 'b
-type constant_type = (types, rel_context * template_arity) declaration_arity
+type constant_type = (types, Context.Rel.t * template_arity) declaration_arity
(** Inlining level of parameters at functor applications.
None means no inlining *)
@@ -117,7 +116,7 @@ type one_inductive_body = {
mind_typename : Id.t; (** Name of the type: [Ii] *)
- mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
+ mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
mind_arity : inductive_arity; (** Arity sort and original user arity *)
@@ -171,7 +170,7 @@ type mutual_inductive_body = {
mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *)
- mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *)
+ mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *)
mind_polymorphic : bool; (** Is it polymorphic or not *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 73cfd0122..6239d3c8d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -254,7 +254,7 @@ let subst_mind_body sub mib =
mind_nparams = mib.mind_nparams;
mind_nparams_rec = mib.mind_nparams_rec;
mind_params_ctxt =
- Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
+ Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_polymorphic = mib.mind_polymorphic;
mind_universes = mib.mind_universes;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 09fe64d77..da540bb05 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -24,7 +24,6 @@ open Errors
open Util
open Names
open Term
-open Context
open Vars
open Declarations
open Pre_env
@@ -70,7 +69,7 @@ let empty_context env =
(* Rel context *)
let lookup_rel n env =
- lookup_rel n env.env_rel_context
+ Context.Rel.lookup n env.env_rel_context
let evaluable_rel n env =
match lookup_rel n env with
@@ -81,7 +80,7 @@ let nb_rel env = env.env_nb_rel
let push_rel = push_rel
-let push_rel_context ctxt x = Context.fold_rel_context push_rel ctxt ~init:x
+let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x
let push_rec_types (lna,typarray,_) env =
let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
@@ -120,7 +119,7 @@ let map_named_val f (ctxt,ctxtv) =
in
(map ctxt, ctxtv)
-let empty_named_context = empty_named_context
+let empty_named_context = Context.Named.empty
let push_named = push_named
let push_named_context = List.fold_right push_named
@@ -130,11 +129,11 @@ let val_of_named_context ctxt =
List.fold_right push_named_context_val ctxt empty_named_context_val
-let lookup_named id env = Context.lookup_named id env.env_named_context
-let lookup_named_val id (ctxt,_) = Context.lookup_named id ctxt
+let lookup_named id env = Context.Named.lookup id env.env_named_context
+let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt
let eq_named_context_val c1 c2 =
- c1 == c2 || named_context_equal (named_context_of_val c1) (named_context_of_val c2)
+ c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2)
(* A local const is evaluable if it is defined *)
@@ -153,7 +152,7 @@ let reset_with_named_context (ctxt,ctxtv) env =
{ env with
env_named_context = ctxt;
env_named_vals = ctxtv;
- env_rel_context = empty_rel_context;
+ env_rel_context = Context.Rel.empty;
env_rel_val = [];
env_nb_rel = 0 }
@@ -176,7 +175,7 @@ let fold_named_context f env ~init =
in fold_right env
let fold_named_context_reverse f ~init env =
- Context.fold_named_context_reverse f ~init:init (named_context env)
+ Context.Named.fold_inside f ~init:init (named_context env)
(* Universe constraints *)
@@ -389,11 +388,11 @@ let add_mind kn mib env =
let lookup_constant_variables c env =
let cmap = lookup_constant c env in
- Context.vars_of_named_context cmap.const_hyps
+ Context.Named.to_vars cmap.const_hyps
let lookup_inductive_variables (kn,i) env =
let mis = lookup_mind kn env in
- Context.vars_of_named_context mis.mind_hyps
+ Context.Named.to_vars mis.mind_hyps
let lookup_constructor_variables (ind,_) env =
lookup_inductive_variables ind env
@@ -427,7 +426,7 @@ let global_vars_set env constr =
contained in the types of the needed variables. *)
let really_needed env needed =
- Context.fold_named_context_reverse
+ Context.Named.fold_inside
(fun need (id,copt,t) ->
if Id.Set.mem id need then
let globc =
@@ -443,9 +442,9 @@ let really_needed env needed =
let keep_hyps env needed =
let really_needed = really_needed env needed in
- Context.fold_named_context
+ Context.Named.fold_outside
(fun (id,_,_ as d) nsign ->
- if Id.Set.mem id really_needed then add_named_decl d nsign
+ if Id.Set.mem id really_needed then Context.Named.add d nsign
else nsign)
(named_context env)
~init:empty_named_context
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2eab32e72..f3fe4d6ae 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Declarations
open Univ
@@ -42,8 +41,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 -> rel_context
-val named_context : env -> named_context
+val rel_context : env -> Context.Rel.t
+val named_context : env -> Context.Named.t
val named_context_val : env -> named_context_val
val opaque_tables : env -> Opaqueproof.opaquetab
@@ -60,25 +59,25 @@ val empty_context : env -> bool
(** {5 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_rel : Context.Rel.Declaration.t -> env -> env
+val push_rel_context : Context.Rel.t -> 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 -> rel_declaration
+val lookup_rel : int -> env -> Context.Rel.Declaration.t
val evaluable_rel : int -> env -> bool
(** {6 Recurrence on [rel_context] } *)
val fold_rel_context :
- (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+ (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
(** {5 Context of variables (section variables and goal assumptions) } *)
-val named_context_of_val : named_context_val -> named_context
+val named_context_of_val : named_context_val -> Context.Named.t
val named_vals_of_val : named_context_val -> Pre_env.named_vals
-val val_of_named_context : named_context -> named_context_val
+val val_of_named_context : Context.Named.t -> named_context_val
val empty_named_context_val : named_context_val
@@ -88,18 +87,18 @@ val empty_named_context_val : named_context_val
val map_named_val :
(constr -> constr) -> named_context_val -> named_context_val
-val push_named : named_declaration -> env -> env
-val push_named_context : named_context -> env -> env
+val push_named : Context.Named.Declaration.t -> env -> env
+val push_named_context : Context.Named.t -> env -> env
val push_named_context_val :
- named_declaration -> named_context_val -> named_context_val
+ Context.Named.Declaration.t -> 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 -> named_declaration
-val lookup_named_val : variable -> named_context_val -> named_declaration
+val lookup_named : variable -> env -> Context.Named.Declaration.t
+val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t
val evaluable_named : variable -> env -> bool
val named_type : variable -> env -> types
val named_body : variable -> env -> constr option
@@ -107,11 +106,11 @@ val named_body : variable -> env -> constr option
(** {6 Recurrence on [named_context]: older declarations processed first } *)
val fold_named_context :
- (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+ (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
(** Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse :
- ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
+ ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
(** This forgets named and rel contexts *)
val reset_context : env -> env
@@ -228,7 +227,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 -> section_context
+val keep_hyps : env -> Id.Set.t -> Context.section_context
(** {5 Unsafe judgments. }
We introduce here the pre-type of judgments, which is
@@ -258,22 +257,22 @@ 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 ->
- (named_context -> named_declaration -> named_context -> named_declaration) ->
+ (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) ->
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) ->
+ (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
+ (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
named_context_val
val insert_after_hyp : named_context_val -> variable ->
- named_declaration ->
- (named_context -> unit) -> named_context_val
+ Context.Named.Declaration.t ->
+ (Context.Named.t -> unit) -> named_context_val
-val remove_hyps : Id.Set.t -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> 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
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index b625478f2..85c74534e 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -90,7 +90,7 @@ let judge_of_variable env id =
variables of the current env *)
(* TODO: check order? *)
let check_hyps_inclusion env f c sign =
- Context.fold_named_context
+ Context.Named.fold_outside
(fun (id,_,ty1) () ->
try
let ty2 = named_type id env in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 11df40caf..da2d213ff 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -12,7 +12,6 @@ open Names
open Univ
open Term
open Vars
-open Context
open Declarations
open Declareops
open Inductive
@@ -341,7 +340,7 @@ let typecheck_inductive env mie =
type ill_formed_ind =
| LocalNonPos of int
| LocalNotEnoughArgs of int
- | LocalNotConstructor of rel_context * constr list
+ | LocalNotConstructor of Context.Rel.t * constr list
| LocalNonPar of int * int * int
exception IllFormedInd of ill_formed_ind
@@ -361,7 +360,7 @@ let explain_ind_err id ntyp env nbpar c err =
raise (InductiveError
(NotEnoughArgs (env,c',mkRel (kt+nbpar))))
| LocalNotConstructor (paramsctxt,args)->
- let nparams = rel_context_nhyps paramsctxt in
+ let nparams = Context.Rel.nhyps paramsctxt in
raise (InductiveError
(NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,
List.length args - nparams)))
@@ -384,7 +383,7 @@ let failwith_non_pos_list n ntypes l =
(* Check the inductive type is called with the expected parameters *)
let check_correct_par (env,n,ntypes,_) hyps l largs =
- let nparams = rel_context_nhyps hyps in
+ let nparams = Context.Rel.nhyps hyps in
let largs = Array.of_list largs in
if Array.length largs < nparams then
raise (IllFormedInd (LocalNotEnoughArgs l));
@@ -465,8 +464,8 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
arguments (used to generate induction schemes, so a priori less
relevant to the kernel). *)
let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
- let lparams = rel_context_length hyps in
- let nmr = rel_context_nhyps hyps in
+ let lparams = Context.Rel.length hyps in
+ let nmr = Context.Rel.nhyps hyps in
(** Positivity of one argument [c] of a constructor (i.e. the
constructor [cn] has a type of the shape [… -> c … -> P], where,
more generally, the arrows may be dependent). *)
@@ -617,13 +616,13 @@ let check_positivity kn env_ar params inds =
let ntypes = Array.length inds in
let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
let lra_ind = Array.rev_to_list rc in
- let lparams = rel_context_length params in
- let nmr = rel_context_nhyps params in
+ let lparams = Context.Rel.length params in
+ let nmr = Context.Rel.nhyps params in
let check_one i (_,lcnames,lc,(sign,_)) =
let ra_env =
List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
- let nargs = rel_context_nhyps sign - nmr in
+ let nargs = Context.Rel.nhyps sign - nmr in
check_positivity_one ienv params (kn,i) nargs lcnames lc
in
let irecargs_nmr = Array.mapi check_one inds in
@@ -697,7 +696,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
matching with a parameter context. *)
let indty, paramsletsubst =
(* [ty] = [Ind inst] is typed in context [params] *)
- let inst = extended_rel_vect 0 paramslet in
+ let inst = Context.Rel.to_extended_vect 0 paramslet in
let ty = mkApp (mkIndU indu, inst) in
(* [Ind inst] is typed in context [params-wo-let] *)
let inst' = rel_list 0 nparamargs in
@@ -710,7 +709,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
in
let ci =
let print_info =
- { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
+ { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
{ ci_ind = ind;
ci_npar = nparamargs;
ci_cstr_ndecls = mind_consnrealdecls;
@@ -783,8 +782,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let hyps = used_section_variables env inds in
- let nparamargs = rel_context_nhyps params in
- let nparamdecls = rel_context_length params in
+ let nparamargs = Context.Rel.nhyps params in
+ let nparamdecls = Context.Rel.length params in
let subst, ctx = Univ.abstract_universes p ctx in
let params = Vars.subst_univs_level_context subst params in
let env_ar =
@@ -799,10 +798,10 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
let consnrealdecls =
- Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
+ Array.map (fun (d,_) -> Context.Rel.length d - Context.Rel.length params)
splayed_lc in
let consnrealargs =
- Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+ Array.map (fun (d,_) -> Context.Rel.nhyps d - Context.Rel.nhyps params)
splayed_lc in
(* Elimination sorts *)
let arkind,kelim =
@@ -835,8 +834,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
{ mind_typename = id;
mind_arity = arkind;
mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
- mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
- mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
+ mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
+ mind_nrealdecls = Context.Rel.length ar_sign - nparamdecls;
mind_kelim = kelim;
mind_consnames = Array.of_list cnames;
mind_consnrealdecls = consnrealdecls;
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 01acdce5c..1fe47b1a5 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -42,6 +42,6 @@ val enforce_indices_matter : unit -> unit
val is_indices_matter : unit -> bool
val compute_projections : pinductive -> Id.t -> Id.t ->
- int -> Context.rel_context -> int array -> int array ->
- Context.rel_context -> Context.rel_context ->
+ int -> Context.Rel.t -> int array -> int array ->
+ Context.Rel.t -> Context.Rel.t ->
(constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 632b4daea..f9a6e04c1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -12,7 +12,6 @@ open Names
open Univ
open Term
open Vars
-open Context
open Declarations
open Declareops
open Environ
@@ -77,7 +76,7 @@ let instantiate_params full t u args sign =
let fail () =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
- Context.fold_rel_context
+ Context.Rel.fold_outside
(fun (_,copt,_) (largs,subs,ty) ->
match (copt, largs, kind_of_term ty) with
| (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
@@ -297,7 +296,7 @@ let build_dependent_inductive ind (_,mip) params =
applist
(mkIndU ind,
List.map (lift mip.mind_nrealdecls) params
- @ extended_rel_list 0 realargs)
+ @ Context.Rel.to_extended_list 0 realargs)
(* This exception is local *)
exception LocalArity of (sorts_family * sorts_family * arity_error) option
@@ -350,12 +349,12 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
let build_one_branch i cty =
let typi = full_constructor_instantiate (ind,u,specif,params) cty in
let (cstrsign,ccl) = decompose_prod_assum typi in
- let nargs = rel_context_length cstrsign in
+ let nargs = Context.Rel.length cstrsign in
let (_,allargs) = decompose_app ccl in
let (lparams,vargs) = List.chop (inductive_params specif) allargs in
let cargs =
let cstr = ith_constructor_of_inductive ind (i+1) in
- let dep_cstr = applist (mkConstructU (cstr,u),lparams@(extended_rel_list 0 cstrsign)) in
+ let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in
vargs @ [dep_cstr] in
let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
it_mkProd_or_LetIn base cstrsign in
@@ -499,7 +498,7 @@ let subterm_var p renv =
with Failure _ | Invalid_argument _ -> Not_subterm
let push_ctxt_renv renv ctxt =
- let n = rel_context_length ctxt in
+ let n = Context.Rel.length ctxt in
{ env = push_rel_context ctxt renv.env;
rel_min = renv.rel_min+n;
genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv }
@@ -701,7 +700,7 @@ let restrict_spec env spec p =
else let absctx, ar = dest_lam_assum env p in
(* Optimization: if the predicate is not dependent, no restriction is needed
and we avoid building the recargs tree. *)
- if noccur_with_meta 1 (rel_context_length absctx) ar then spec
+ if noccur_with_meta 1 (Context.Rel.length absctx) ar then spec
else
let env = push_rel_context absctx env in
let arctx, s = dest_prod_assum env ar in
@@ -843,7 +842,7 @@ let filter_stack_domain env ci p stack =
let absctx, ar = dest_lam_assum env p in
(* Optimization: if the predicate is not dependent, no restriction is needed
and we avoid building the recargs tree. *)
- if noccur_with_meta 1 (rel_context_length absctx) ar then stack
+ if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack
else let env = push_rel_context absctx env in
let rec filter_stack env ar stack =
let t = whd_betadeltaiota env ar in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 5847d25f6..541fb8282 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Univ
open Declarations
open Environ
@@ -35,7 +34,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif
(** {6 Functions to build standard types related to inductive } *)
val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
-val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
+val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
val instantiate_inductive_constraints :
mutual_inductive_body -> universe_instance -> constraints
@@ -86,7 +85,7 @@ val build_branches_type :
constr list -> constr -> types array
(** Return the arity of an inductive type *)
-val mind_arity : one_inductive_body -> rel_context * sorts_family
+val mind_arity : one_inductive_body -> Context.Rel.t * sorts_family
val inductive_sort_family : one_inductive_body -> sorts_family
@@ -111,8 +110,8 @@ exception SingletonInductiveBecomesProp of Id.t
val max_inductive_sort : sorts array -> universe
-val instantiate_universes : env -> rel_context ->
- template_arity -> constr Lazy.t array -> rel_context * sorts
+val instantiate_universes : env -> Context.Rel.t ->
+ template_arity -> constr Lazy.t array -> Context.Rel.t * sorts
(** {6 Debug} *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 98b2d6d2e..dd6ef1c66 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -8,7 +8,6 @@
open Errors
open Names
open Term
-open Context
open Declarations
open Util
open Nativevalues
@@ -1826,15 +1825,15 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
in
let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
let auxdefs = List.fold_right get_named_val fv_named auxdefs in
- let lvl = rel_context_length env.env_rel_context in
+ let lvl = Context.Rel.length env.env_rel_context in
let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in
let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in
let aux_name = fresh_lname Anonymous in
auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
and compile_rel env sigma univ auxdefs n =
- let (_,body,_) = lookup_rel n env.env_rel_context in
- let n = rel_context_length env.env_rel_context - n in
+ let (_,body,_) = Context.Rel.lookup n env.env_rel_context in
+ let n = Context.Rel.length env.env_rel_context - n in
match body with
| Some t ->
let code = lambda_of_constr env sigma t in
@@ -1844,7 +1843,7 @@ and compile_rel env sigma univ auxdefs n =
Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
and compile_named env sigma univ auxdefs id =
- let (_,body,_) = lookup_named id env.env_named_context in
+ let (_,body,_) = Context.Named.lookup id env.env_named_context in
match body with
| Some t ->
let code = lambda_of_constr env sigma t in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index badb15b56..bfddf8286 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
type proofterm = (constr * Univ.universe_context_set) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 009ff82ff..5b743a4c7 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -48,7 +48,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
(* The type has two caveats:
1) cook_constr is defined after
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 615b9d49b..9fcec1114 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,7 +15,6 @@
open Util
open Names
-open Context
open Univ
open Term
open Declarations
@@ -66,9 +65,9 @@ type named_vals = (Id.t * lazy_val) list
type env = {
env_globals : globals;
- env_named_context : named_context;
+ env_named_context : Context.Named.t;
env_named_vals : named_vals;
- env_rel_context : rel_context;
+ env_rel_context : Context.Rel.t;
env_rel_val : lazy_val list;
env_nb_rel : int;
env_stratification : stratification;
@@ -77,7 +76,7 @@ type env = {
indirect_pterms : Opaqueproof.opaquetab;
}
-type named_context_val = named_context * named_vals
+type named_context_val = Context.Named.t * named_vals
let empty_named_context_val = [],[]
@@ -87,9 +86,9 @@ let empty_env = {
env_inductives = Mindmap_env.empty;
env_modules = MPmap.empty;
env_modtypes = MPmap.empty};
- env_named_context = empty_named_context;
+ env_named_context = Context.Named.empty;
env_named_vals = [];
- env_rel_context = empty_rel_context;
+ env_rel_context = Context.Rel.empty;
env_rel_val = [];
env_nb_rel = 0;
env_stratification = {
@@ -107,7 +106,7 @@ let nb_rel env = env.env_nb_rel
let push_rel d env =
let rval = ref VKnone in
{ env with
- env_rel_context = add_rel_decl d env.env_rel_context;
+ env_rel_context = Context.Rel.add d env.env_rel_context;
env_rel_val = rval :: env.env_rel_val;
env_nb_rel = env.env_nb_rel + 1 }
@@ -127,7 +126,7 @@ let env_of_rel n env =
let push_named_context_val d (ctxt,vals) =
let id,_,_ = d in
let rval = ref VKnone in
- add_named_decl d ctxt, (id,rval)::vals
+ Context.Named.add d ctxt, (id,rval)::vals
let push_named d env =
(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
@@ -135,7 +134,7 @@ let push_named d env =
let id,body,_ = d in
let rval = ref VKnone in
{ env_globals = env.env_globals;
- env_named_context = Context.add_named_decl d env.env_named_context;
+ env_named_context = Context.Named.add d env.env_named_context;
env_named_vals = (id, rval) :: env.env_named_vals;
env_rel_context = env.env_rel_context;
env_rel_val = env.env_rel_val;
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index b499ac0c5..9cd940a88 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Declarations
open Univ
@@ -46,9 +45,9 @@ type named_vals = (Id.t * lazy_val) list
type env = {
env_globals : globals;
- env_named_context : named_context;
+ env_named_context : Context.Named.t;
env_named_vals : named_vals;
- env_rel_context : rel_context;
+ env_rel_context : Context.Rel.t;
env_rel_val : lazy_val list;
env_nb_rel : int;
env_stratification : stratification;
@@ -57,7 +56,7 @@ type env = {
indirect_pterms : Opaqueproof.opaquetab;
}
-type named_context_val = named_context * named_vals
+type named_context_val = Context.Named.t * named_vals
val empty_named_context_val : named_context_val
@@ -66,15 +65,15 @@ val empty_env : env
(** Rel context *)
val nb_rel : env -> int
-val push_rel : rel_declaration -> env -> env
+val push_rel : Context.Rel.Declaration.t -> env -> env
val lookup_rel_val : int -> env -> lazy_val
val env_of_rel : int -> env -> env
(** Named context *)
val push_named_context_val :
- named_declaration -> named_context_val -> named_context_val
-val push_named : named_declaration -> env -> env
+ Context.Named.Declaration.t -> named_context_val -> named_context_val
+val push_named : Context.Named.Declaration.t -> env -> env
val lookup_named_val : Id.t -> env -> lazy_val
val env_of_named : Id.t -> env -> env
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bf2ee2707..78222c6b6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -20,7 +20,6 @@ open Util
open Names
open Term
open Vars
-open Context
open Univ
open Environ
open Closure
@@ -741,10 +740,10 @@ let dest_prod env =
match kind_of_term t with
| Prod (n,a,c0) ->
let d = (n,None,a) in
- decrec (push_rel d env) (add_rel_decl d m) c0
+ decrec (push_rel d env) (Context.Rel.add d m) c0
| _ -> m,t
in
- decrec env empty_rel_context
+ decrec env Context.Rel.empty
(* The same but preserving lets in the context, not internal ones. *)
let dest_prod_assum env =
@@ -753,17 +752,17 @@ let dest_prod_assum env =
match kind_of_term rty with
| Prod (x,t,c) ->
let d = (x,None,t) in
- prodec_rec (push_rel d env) (add_rel_decl d l) c
+ prodec_rec (push_rel d env) (Context.Rel.add d l) c
| LetIn (x,b,t,c) ->
let d = (x,Some b,t) in
- prodec_rec (push_rel d env) (add_rel_decl d l) c
+ prodec_rec (push_rel d env) (Context.Rel.add d l) c
| Cast (c,_,_) -> prodec_rec env l c
| _ ->
let rty' = whd_betadeltaiota env rty in
if Term.eq_constr rty' rty then l, rty
else prodec_rec env l rty'
in
- prodec_rec env empty_rel_context
+ prodec_rec env Context.Rel.empty
let dest_lam_assum env =
let rec lamec_rec env l ty =
@@ -771,14 +770,14 @@ let dest_lam_assum env =
match kind_of_term rty with
| Lambda (x,t,c) ->
let d = (x,None,t) in
- lamec_rec (push_rel d env) (add_rel_decl d l) c
+ lamec_rec (push_rel d env) (Context.Rel.add d l) c
| LetIn (x,b,t,c) ->
let d = (x,Some b,t) in
- lamec_rec (push_rel d env) (add_rel_decl d l) c
+ lamec_rec (push_rel d env) (Context.Rel.add d l) c
| Cast (c,_,_) -> lamec_rec env l c
| _ -> l,rty
in
- lamec_rec env empty_rel_context
+ lamec_rec env Context.Rel.empty
exception NotArity
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index f7a8d88c2..35daff7b5 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Term
-open Context
open Environ
(***********************************************************************
@@ -99,9 +98,9 @@ val betazeta_appvect : int -> constr -> constr array -> constr
(***********************************************************************
s Recognizing products and arities modulo reduction *)
-val dest_prod : env -> types -> rel_context * types
-val dest_prod_assum : env -> types -> rel_context * types
-val dest_lam_assum : env -> types -> rel_context * types
+val dest_prod : env -> types -> Context.Rel.t * types
+val dest_prod_assum : env -> types -> Context.Rel.t * types
+val dest_lam_assum : env -> types -> Context.Rel.t * types
exception NotArity
diff --git a/kernel/term.ml b/kernel/term.ml
index 455248dd5..19f4b7a23 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -10,7 +10,6 @@ open Util
open Pp
open Errors
open Names
-open Context
open Vars
(**********************************************************************)
@@ -590,24 +589,24 @@ let decompose_lam_n n =
let decompose_prod_assum =
let rec prodec_rec l c =
match kind_of_term c with
- | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) c
- | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c
+ | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) c
+ | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) c
| Cast (c,_,_) -> prodec_rec l c
| _ -> l,c
in
- prodec_rec empty_rel_context
+ prodec_rec Context.Rel.empty
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
let decompose_lam_assum =
let rec lamdec_rec l c =
match kind_of_term c with
- | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) c
- | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) c
| Cast (c,_,_) -> lamdec_rec l c
| _ -> l,c
in
- lamdec_rec empty_rel_context
+ lamdec_rec Context.Rel.empty
(* Given a positive integer n, decompose a product or let-in term
of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair
@@ -619,12 +618,12 @@ let decompose_prod_n_assum n =
let rec prodec_rec l n c =
if Int.equal n 0 then l,c
else match kind_of_term c with
- | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
- | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+ | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) (n-1) c
+ | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c
| Cast (c,_,_) -> prodec_rec l n c
| c -> error "decompose_prod_n_assum: not enough assumptions"
in
- prodec_rec empty_rel_context n
+ prodec_rec Context.Rel.empty n
(* Given a positive integer n, decompose a lambda or let-in term [fun
(x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted
@@ -638,12 +637,12 @@ let decompose_lam_n_assum n =
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else match kind_of_term c with
- | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
- | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) n c
| Cast (c,_,_) -> lamdec_rec l n c
| c -> error "decompose_lam_n_assum: not enough abstractions"
in
- lamdec_rec empty_rel_context n
+ lamdec_rec Context.Rel.empty n
(* Same, counting let-in *)
let decompose_lam_n_decls n =
@@ -652,12 +651,12 @@ let decompose_lam_n_decls n =
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else match kind_of_term c with
- | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
- | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c
| Cast (c,_,_) -> lamdec_rec l n c
| c -> error "decompose_lam_n_decls: not enough abstractions"
in
- lamdec_rec empty_rel_context n
+ lamdec_rec Context.Rel.empty n
let prod_assum t = fst (decompose_prod_assum t)
let prod_n_assum n t = fst (decompose_prod_n_assum n t)
@@ -678,7 +677,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
Such a term can canonically be seen as the pair of a context of types
and of a sort *)
-type arity = rel_context * sorts
+type arity = Context.Rel.t * sorts
let destArity =
let rec prodec_rec l c =
diff --git a/kernel/term.mli b/kernel/term.mli
index 972a67ebe..c45e04338 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Context
(** {5 Redeclaration of types from module Constr and Sorts}
@@ -213,14 +212,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
val mkNamedProd : Id.t -> types -> types -> types
(** Constructs either [(x:t)c] or [[x=b:t]c] *)
-val mkProd_or_LetIn : rel_declaration -> types -> types
-val mkProd_wo_LetIn : rel_declaration -> types -> types
-val mkNamedProd_or_LetIn : named_declaration -> types -> types
-val mkNamedProd_wo_LetIn : named_declaration -> types -> types
+val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types
+val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types
(** Constructs either [[x:t]c] or [[x=b:t]c] *)
-val mkLambda_or_LetIn : rel_declaration -> constr -> constr
-val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
+val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr
+val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr
(** {5 Other term constructors. } *)
@@ -262,8 +261,8 @@ val to_lambda : int -> constr -> constr
where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
val to_prod : int -> constr -> constr
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
+val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
(** In [lambda_applist c args], [c] is supposed to have the form
[λΓ.c] with [Γ] without let-in; it returns [c] with the variables
@@ -314,29 +313,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
(** Extract the premisses and the conclusion of a term of the form
"(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
-val decompose_prod_assum : types -> rel_context * types
+val decompose_prod_assum : types -> Context.Rel.t * types
(** Idem with lambda's *)
-val decompose_lam_assum : constr -> rel_context * constr
+val decompose_lam_assum : constr -> Context.Rel.t * constr
(** Idem but extract the first [n] premisses, counting let-ins. *)
-val decompose_prod_n_assum : int -> types -> rel_context * types
+val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
(** Idem for lambdas, _not_ counting let-ins *)
-val decompose_lam_n_assum : int -> constr -> rel_context * constr
+val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr
(** Idem, counting let-ins *)
-val decompose_lam_n_decls : int -> constr -> rel_context * constr
+val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr
(** Return the premisses/parameters of a type/term (let-in included) *)
-val prod_assum : types -> rel_context
-val lam_assum : constr -> rel_context
+val prod_assum : types -> Context.Rel.t
+val lam_assum : constr -> Context.Rel.t
(** Return the first n-th premisses/parameters of a type (let included and counted) *)
-val prod_n_assum : int -> types -> rel_context
+val prod_n_assum : int -> types -> Context.Rel.t
(** Return the first n-th premisses/parameters of a term (let included but not counted) *)
-val lam_n_assum : int -> constr -> rel_context
+val lam_n_assum : int -> constr -> Context.Rel.t
(** Remove the premisses/parameters of a type/term *)
val strip_prod : types -> types
@@ -369,7 +368,7 @@ val under_outer_cast : (constr -> constr) -> constr -> constr
Such a term can canonically be seen as the pair of a context of types
and of a sort *)
-type arity = rel_context * sorts
+type arity = Context.Rel.t * sorts
(** Build an "arity" from its canonical form *)
val mkArity : arity -> types
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a566028d4..db50a393b 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -16,7 +16,6 @@ open Errors
open Util
open Names
open Term
-open Context
open Declarations
open Environ
open Entries
@@ -246,8 +245,8 @@ let infer_declaration ~trust env kn dcl =
let global_vars_set_constant_type env = function
| RegularArity t -> global_vars_set env t
| TemplateArity (ctx,_) ->
- Context.fold_rel_context
- (fold_rel_declaration
+ Context.Rel.fold_outside
+ (Context.Rel.Declaration.fold
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4f32fdce8..35f53b7e7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -12,7 +12,6 @@ open Names
open Univ
open Term
open Vars
-open Context
open Declarations
open Environ
open Entries
@@ -99,7 +98,7 @@ let judge_of_variable env id =
variables of the current env.
Order does not have to be checked assuming that all names are distinct *)
let check_hyps_inclusion env c sign =
- Context.fold_named_context
+ Context.Named.fold_outside
(fun (id,b1,ty1) () ->
try
let (_,b2,ty2) = lookup_named id env in
@@ -561,6 +560,6 @@ let infer_local_decls env decls =
| (id, d) :: l ->
let (env, l) = inferec env l in
let d = infer_local_decl env id d in
- (push_rel d env, add_rel_decl d l)
- | [] -> (env, empty_rel_context) in
+ (push_rel d env, Context.Rel.add d l)
+ | [] -> (env, Context.Rel.empty) in
inferec env decls
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 010b2b6f0..bcaa6b63e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -9,7 +9,6 @@
open Names
open Univ
open Term
-open Context
open Environ
open Entries
open Declarations
@@ -28,7 +27,7 @@ val infer_v : env -> constr array -> unsafe_judgment array
val infer_type : env -> types -> unsafe_type_judgment
val infer_local_decls :
- env -> (Id.t * local_entry) list -> (env * rel_context)
+ env -> (Id.t * local_entry) list -> (env * Context.Rel.t)
(** {6 Basic operations of the typing machine. } *)
@@ -128,4 +127,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
constant_type
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> constr -> section_context -> unit
+val check_hyps_inclusion : env -> constr -> Context.section_context -> unit
diff --git a/kernel/vars.ml b/kernel/vars.ml
index a00c7036f..53543e043 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -8,7 +8,6 @@
open Names
open Esubst
-open Context
(*********************)
(* Occurring *)
@@ -160,9 +159,9 @@ let substnl laml n c = substn_many (make_subst laml) n c
let substl laml c = substn_many (make_subst laml) 0 c
let subst1 lam c = substn_many [|make_substituend lam|] 0 c
-let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r
-let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r
-let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r
+let substnl_decl laml k r = Context.Rel.Declaration.map (fun c -> substnl laml k c) r
+let substl_decl laml r = Context.Rel.Declaration.map (fun c -> substnl laml 0 c) r
+let subst1_decl lam r = Context.Rel.Declaration.map (fun c -> subst1 lam c) r
(* Build a substitution from an instance, inserting missing let-ins *)
@@ -302,7 +301,7 @@ let subst_univs_level_constr subst c =
if !changed then c' else c
let subst_univs_level_context s =
- map_rel_context (subst_univs_level_constr s)
+ Context.Rel.map (subst_univs_level_constr s)
let subst_instance_constr subst c =
if Univ.Instance.is_empty subst then c
@@ -343,7 +342,7 @@ let subst_instance_constr subst c =
let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
- else map_rel_context (fun x -> subst_instance_constr s x) ctx
+ else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
type id_key = constant tableKey
let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index a84cf0114..659990806 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -8,7 +8,6 @@
open Names
open Constr
-open Context
(** {6 Occur checks } *)
@@ -69,10 +68,10 @@ type substl = constr list
as if usable in [applist] while the substitution is
represented the other way round, i.e. ending with either [u₁] or
[c₁], as if usable for [substl]. *)
-val subst_of_rel_context_instance : rel_context -> constr list -> substl
+val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
(** For compatibility: returns the substitution reversed *)
-val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
+val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
(** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
@@ -92,13 +91,13 @@ val subst1 : constr -> constr -> constr
accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if
Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then
Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *)
-val substnl_decl : substl -> int -> rel_declaration -> rel_declaration
+val substnl_decl : substl -> int -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
(** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *)
-val substl_decl : substl -> rel_declaration -> rel_declaration
+val substl_decl : substl -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
(** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *)
-val subst1_decl : constr -> rel_declaration -> rel_declaration
+val subst1_decl : constr -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
(** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by
[cj] in [t]. *)
@@ -136,11 +135,11 @@ val subst_univs_constr : universe_subst -> constr -> constr
(** Level substitutions for polymorphism. *)
val subst_univs_level_constr : universe_level_subst -> constr -> constr
-val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
+val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t
(** Instance substitution for polymorphism. *)
val subst_instance_constr : universe_instance -> constr -> constr
-val subst_instance_context : universe_instance -> rel_context -> rel_context
+val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t
type id_key = constant tableKey
val eq_id_key : id_key -> id_key -> bool
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 11:31:03 +0000