aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/closure.ml10
-rw-r--r--kernel/context.ml364
-rw-r--r--kernel/context.mli151
-rw-r--r--kernel/cooking.ml7
-rw-r--r--kernel/csymtable.ml10
-rw-r--r--kernel/declareops.ml35
-rw-r--r--kernel/environ.ml64
-rw-r--r--kernel/fast_typeops.ml17
-rw-r--r--kernel/indtypes.ml35
-rw-r--r--kernel/inductive.ml50
-rw-r--r--kernel/nativecode.ml17
-rw-r--r--kernel/nativelambda.ml3
-rw-r--r--kernel/pre_env.ml7
-rw-r--r--kernel/reduction.ml11
-rw-r--r--kernel/safe_typing.ml8
-rw-r--r--kernel/term.ml111
-rw-r--r--kernel/term_typing.ml24
-rw-r--r--kernel/typeops.ml39
-rw-r--r--kernel/vars.ml11
19 files changed, 638 insertions, 336 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 9bc67b5adb..dc98cc65d0 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -247,8 +247,8 @@ let info_env info = info.i_cache.i_env
let rec assoc_defined id = function
| [] -> raise Not_found
-| (_, None, _) :: ctxt -> assoc_defined id ctxt
-| (id', Some c, _) :: ctxt ->
+| Context.Named.Declaration.LocalAssum _ :: ctxt -> assoc_defined id ctxt
+| Context.Named.Declaration.LocalDef (id', c, _) :: ctxt ->
if Id.equal id id' then c else assoc_defined id ctxt
let ref_value_cache ({i_cache = cache} as infos) ref =
@@ -285,9 +285,9 @@ let defined_rels flags env =
let ctx = rel_context env in
let len = List.length ctx in
let ans = Array.make len None in
- let iter i (_, b, _) = match b with
- | None -> ()
- | Some _ -> Array.unsafe_set ans i b
+ let iter i = function
+ | Context.Rel.Declaration.LocalAssum _ -> ()
+ | Context.Rel.Declaration.LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b)
in
let () = List.iteri iter ctx in
ans
diff --git a/kernel/context.ml b/kernel/context.ml
index 3be1e83230..cc1e6f1762 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -33,33 +33,122 @@ open Names
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)].
- *)
+ (** Representation of {e local declarations}. *)
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)
+ (* local declaration *)
+ type t = LocalAssum of Name.t * Constr.t (* local assumption *)
+ | LocalDef of Name.t * Constr.t * Constr.t (* local definition *)
+
+ (** Return the name bound by a given declaration. *)
+ let get_name = function
+ | LocalAssum (na,_)
+ | LocalDef (na,_,_) -> na
+
+ (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+ let get_value = function
+ | LocalAssum _ -> None
+ | LocalDef (_,v,_) -> Some v
+
+ (** Return the type of the name bound by a given declaration. *)
+ let get_type = function
+ | LocalAssum (_,ty)
+ | LocalDef (_,_,ty) -> ty
+
+ (** Set the name that is bound by a given declaration. *)
+ let set_name na = function
+ | LocalAssum (_,ty) -> LocalAssum (na, ty)
+ | LocalDef (_,v,ty) -> LocalDef (na, v, ty)
+
+ (** Set the type of the bound variable in a given declaration. *)
+ let set_type ty = function
+ | LocalAssum (na,_) -> LocalAssum (na, ty)
+ | LocalDef (na,v,_) -> LocalDef (na, v, ty)
+
+ (** Return [true] iff a given declaration is a local assumption. *)
+ let is_local_assum = function
+ | LocalAssum _ -> true
+ | LocalDef _ -> false
+
+ (** Return [true] iff a given declaration is a local definition. *)
+ let is_local_def = function
+ | LocalAssum _ -> false
+ | LocalDef _ -> true
(** Check whether any term in a given declaration satisfies a given predicate. *)
- let exists f (_, v, ty) = Option.cata f false v || f ty
+ let exists f = function
+ | LocalAssum (_, ty) -> f ty
+ | LocalDef (_, v, ty) -> f 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
+ let for_all f = function
+ | LocalAssum (_, ty) -> f ty
+ | LocalDef (_, v, ty) -> f 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
+ let equal decl1 decl2 =
+ match decl1, decl2 with
+ | LocalAssum (n1,ty1), LocalAssum (n2, ty2) ->
+ Name.equal n1 n2 && Constr.equal ty1 ty2
+ | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) ->
+ Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+ | _ ->
+ false
+
+ (** Map the name bound by a given declaration. *)
+ let map_name f = function
+ | LocalAssum (na, ty) as decl ->
+ let na' = f na in
+ if na == na' then decl else LocalAssum (na', ty)
+ | LocalDef (na, v, ty) as decl ->
+ let na' = f na in
+ if na == na' then decl else LocalDef (na', v, ty)
+
+ (** For local assumptions, this function returns the original local assumptions.
+ For local definitions, this function maps the value in the local definition. *)
+ let map_value f = function
+ | LocalAssum _ as decl -> decl
+ | LocalDef (na, v, t) as decl ->
+ let v' = f v in
+ if v == v' then decl else LocalDef (na, v', t)
+
+ (** Map the type of the name bound by a given declaration. *)
+ let map_type f = function
+ | LocalAssum (na, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalAssum (na, ty')
+ | LocalDef (na, v, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalDef (na, v, ty')
+
+ (** Map all terms in a given declaration. *)
+ let map_constr f = function
+ | LocalAssum (na, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalAssum (na, ty')
+ | LocalDef (na, v, ty) as decl ->
+ let v' = f v in
+ let ty' = f ty in
+ if v == v' && ty == ty' then decl else LocalDef (na, v', ty')
+
+ (** Perform a given action on all terms in a given declaration. *)
+ let iter_constr f = function
+ | LocalAssum (_,ty) -> f ty
+ | LocalDef (_,v,ty) -> f v; f ty
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ let fold f decl acc =
+ match decl with
+ | LocalAssum (n,ty) -> f ty acc
+ | LocalDef (n,v,ty) -> f ty (f v acc)
+
+ let to_tuple = function
+ | LocalAssum (na, ty) -> na, None, ty
+ | LocalDef (na, v, ty) -> na, Some v, ty
+
+ let of_tuple = function
+ | n, None, ty -> LocalAssum (n,ty)
+ | n, Some v, ty -> LocalDef (n,v,ty)
end
(** Rel-context is represented as a list of declarations.
@@ -73,6 +162,21 @@ module Rel =
(** Return a new rel-context enriched by with a given inner-most declaration. *)
let add d ctx = d :: ctx
+ (** 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 open Declaration in
+ let rec nhyps acc = function
+ | [] -> acc
+ | LocalAssum _ :: hyps -> nhyps (succ acc) hyps
+ | LocalDef _ :: hyps -> nhyps acc hyps
+ in
+ nhyps 0
+
(** 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 =
@@ -81,15 +185,14 @@ module Rel =
| n, _ :: sign -> lookup (n-1) sign
| _, [] -> raise Not_found
+ (** Check whether given two rel-contexts are equal. *)
+ let equal = List.equal Declaration.equal
+
(** 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
+ let map f = List.smartmap (Declaration.map_constr f)
+
+ (** Perform a given action on every declaration in a given rel-context. *)
+ let iter f = List.iter (Declaration.iter_constr f)
(** Reduce all terms in a given rel-context to a single value.
Innermost declarations are processed first. *)
@@ -99,29 +202,13 @@ module Rel =
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
+ | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx
+ | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
in aux []
(** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
@@ -129,8 +216,8 @@ module Rel =
[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
+ | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+ | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps
| [] -> l
in
reln [] 1
@@ -143,38 +230,127 @@ module Rel =
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)].
- *)
+ (** Representation of {e local declarations}. *)
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)
+ (** local declaration *)
+ type t = LocalAssum of Id.t * Constr.t
+ | LocalDef of Id.t * Constr.t * Constr.t
+
+ (** Return the identifier bound by a given declaration. *)
+ let get_id = function
+ | LocalAssum (id,_) -> id
+ | LocalDef (id,_,_) -> id
+
+ (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+ let get_value = function
+ | LocalAssum _ -> None
+ | LocalDef (_,v,_) -> Some v
+
+ (** Return the type of the name bound by a given declaration. *)
+ let get_type = function
+ | LocalAssum (_,ty)
+ | LocalDef (_,_,ty) -> ty
+
+ (** Set the identifier that is bound by a given declaration. *)
+ let set_id id = function
+ | LocalAssum (_,ty) -> LocalAssum (id, ty)
+ | LocalDef (_, v, ty) -> LocalDef (id, v, ty)
+
+ (** Set the type of the bound variable in a given declaration. *)
+ let set_type ty = function
+ | LocalAssum (id,_) -> LocalAssum (id, ty)
+ | LocalDef (id,v,_) -> LocalDef (id, v, ty)
+
+ (** Return [true] iff a given declaration is a local assumption. *)
+ let is_local_assum = function
+ | LocalAssum _ -> true
+ | LocalDef _ -> false
+
+ (** Return [true] iff a given declaration is a local definition. *)
+ let is_local_def = function
+ | LocalDef _ -> true
+ | LocalAssum _ -> false
(** Check whether any term in a given declaration satisfies a given predicate. *)
- let exists f (_, v, ty) = Option.cata f false v || f ty
+ let exists f = function
+ | LocalAssum (_, ty) -> f ty
+ | LocalDef (_, v, ty) -> f 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
+ let for_all f = function
+ | LocalAssum (_, ty) -> f ty
+ | LocalDef (_, v, ty) -> f 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
+ let equal decl1 decl2 =
+ match decl1, decl2 with
+ | LocalAssum (id1, ty1), LocalAssum (id2, ty2) ->
+ Id.equal id1 id2 && Constr.equal ty1 ty2
+ | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) ->
+ Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+ | _ ->
+ false
+
+ (** Map the identifier bound by a given declaration. *)
+ let map_id f = function
+ | LocalAssum (id, ty) as decl ->
+ let id' = f id in
+ if id == id' then decl else LocalAssum (id', ty)
+ | LocalDef (id, v, ty) as decl ->
+ let id' = f id in
+ if id == id' then decl else LocalDef (id', v, ty)
+
+ (** For local assumptions, this function returns the original local assumptions.
+ For local definitions, this function maps the value in the local definition. *)
+ let map_value f = function
+ | LocalAssum _ as decl -> decl
+ | LocalDef (na, v, t) as decl ->
+ let v' = f v in
+ if v == v' then decl else LocalDef (na, v', t)
+
+ (** Map the type of the name bound by a given declaration. *)
+ let map_type f = function
+ | LocalAssum (id, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalAssum (id, ty')
+ | LocalDef (id, v, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalDef (id, v, ty')
+
+ (** Map all terms in a given declaration. *)
+ let map_constr f = function
+ | LocalAssum (id, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalAssum (id, ty')
+ | LocalDef (id, v, ty) as decl ->
+ let v' = f v in
+ let ty' = f ty in
+ if v == v' && ty == ty' then decl else LocalDef (id, v', ty')
+
+ (** Perform a given action on all terms in a given declaration. *)
+ let iter_constr f = function
+ | LocalAssum (_, ty) -> f ty
+ | LocalDef (_, v, ty) -> f v; f ty
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ let fold f decl a =
+ match decl with
+ | LocalAssum (_, ty) -> f ty a
+ | LocalDef (_, v, ty) -> a |> f v |> f ty
+
+ let to_tuple = function
+ | LocalAssum (id, ty) -> id, None, ty
+ | LocalDef (id, v, ty) -> id, Some v, ty
+
+ let of_tuple = function
+ | id, None, ty -> LocalAssum (id, ty)
+ | id, Some v, ty -> LocalDef (id, v, ty)
end
+ (** 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 = Declaration.t list
(** empty named-context *)
@@ -183,22 +359,23 @@ module Named =
(** empty named-context *)
let add d ctx = d :: ctx
+ (** Return the number of {e local declarations} in a given named-context. *)
+ let length = List.length
+
(** 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
+ @raise Not_found if the designated identifier is not present in the designated named-context. *) let rec lookup id = function
+ | decl :: _ when Id.equal id (Declaration.get_id decl) -> decl
+ | _ :: sign -> lookup id sign
+ | [] -> raise Not_found
+
+ (** Check whether given two named-contexts are equal. *)
+ let equal = List.equal Declaration.equal
(** 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
+ let map f = List.smartmap (Declaration.map_constr f)
+
+ (** Perform a given action on every declaration in a given named-context. *)
+ let iter f = List.iter (Declaration.iter_constr f)
(** Reduce all terms in a given named-context to a single value.
Innermost declarations are processed first. *)
@@ -208,18 +385,9 @@ module Named =
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
+ List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty
(** [instance_from_named_context Ω] builds an instance [args] such
that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
@@ -227,8 +395,8 @@ module Named =
gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
let to_instance =
let filter = function
- | (id, None, _) -> Some (Constr.mkVar id)
- | (_, Some _, _) -> None
+ | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id)
+ | _ -> None
in
List.map_filter filter
end
@@ -238,9 +406,15 @@ module NamedList =
module Declaration =
struct
type t = Id.t list * Constr.t option * Constr.t
- let map = Named.Declaration.map
+
+ let map_constr f (ids, copt, ty as decl) =
+ let copt' = Option.map f copt in
+ let ty' = f ty in
+ if copt == copt' && ty == ty' then decl else (ids, copt', ty')
end
+
type t = Declaration.t list
+
let fold f l ~init = List.fold_right f l init
end
diff --git a/kernel/context.mli b/kernel/context.mli
index 1976e46d33..a69754cc29 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -26,21 +26,32 @@ open Names
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
+ (* local declaration *)
+ type t = LocalAssum of Name.t * Constr.t (* local assumption *)
+ | LocalDef of Name.t * Constr.t * Constr.t (* local definition *)
- (** Map all terms in a given declaration. *)
- val map : (Constr.t -> Constr.t) -> t -> t
+ (** Return the name bound by a given declaration. *)
+ val get_name : t -> Name.t
- (** Reduce all terms in a given declaration to a single value. *)
- val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+ (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+ val get_value : t -> Constr.t option
+
+ (** Return the type of the name bound by a given declaration. *)
+ val get_type : t -> Constr.t
+
+ (** Set the name that is bound by a given declaration. *)
+ val set_name : Name.t -> t -> t
+
+ (** Set the type of the bound variable in a given declaration. *)
+ val set_type : Constr.t -> t -> t
+
+ (** Return [true] iff a given declaration is a local assumption. *)
+ val is_local_assum : t -> bool
+
+ (** Return [true] iff a given declaration is a local definition. *)
+ val is_local_def : t -> bool
(** Check whether any term in a given declaration satisfies a given predicate. *)
val exists : (Constr.t -> bool) -> t -> bool
@@ -50,6 +61,28 @@ sig
(** Check whether the two given declarations are equal. *)
val equal : t -> t -> bool
+
+ (** Map the name bound by a given declaration. *)
+ val map_name : (Name.t -> Name.t) -> t -> t
+
+ (** For local assumptions, this function returns the original local assumptions.
+ For local definitions, this function maps the value in the local definition. *)
+ val map_value : (Constr.t -> Constr.t) -> t -> t
+
+ (** Map the type of the name bound by a given declaration. *)
+ val map_type : (Constr.t -> Constr.t) -> t -> t
+
+ (** Map all terms in a given declaration. *)
+ val map_constr : (Constr.t -> Constr.t) -> t -> t
+
+ (** Perform a given action on all terms in a given declaration. *)
+ val iter_constr : (Constr.t -> unit) -> t -> unit
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+ val to_tuple : t -> Name.t * Constr.t option * Constr.t
+ val of_tuple : Name.t * Constr.t option * Constr.t -> t
end
(** Rel-context is represented as a list of declarations.
@@ -63,6 +96,15 @@ sig
(** Return a new rel-context enriched by with a given inner-most declaration. *)
val add : Declaration.t -> t -> t
+ (** Return the number of {e local declarations} in a given context. *)
+ val length : t -> int
+
+ (** Check whether given two rel-contexts are equal. *)
+ val equal : t -> t -> bool
+
+ (** Return the number of {e local assumptions} in a given rel-context. *)
+ val nhyps : t -> int
+
(** 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
@@ -70,6 +112,9 @@ sig
(** Map all terms in a given rel-context. *)
val map : (Constr.t -> Constr.t) -> t -> t
+ (** Perform a given action on every declaration in a given rel-context. *)
+ val iter : (Constr.t -> unit) -> t -> unit
+
(** 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
@@ -78,15 +123,6 @@ sig
Outermost declarations are processed first. *)
val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
- (** Perform a given action on every declaration in a given rel-context. *)
- val iter : (Constr.t -> unit) -> t -> unit
-
- (** Return the number of {e local declarations} in a given context. *)
- val length : t -> int
-
- (** Return the number of {e local assumptions} in a given rel-context. *)
- val nhyps : t -> int
-
(** 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
@@ -104,21 +140,32 @@ end
Individual declarations are then designated by the identifiers they bind. *)
module Named :
sig
- (** Representation of {e local declarations}.
-
- [(id, None, typ)] represents a {e local assumption}.
-
- [(id, Some value, typ)] represents a {e local definition}.
- *)
+ (** Representation of {e local declarations}. *)
module Declaration :
sig
- type t = Id.t * Constr.t option * Constr.t
+ type t = LocalAssum of Id.t * Constr.t
+ | LocalDef of Id.t * Constr.t * Constr.t
- (** Map all terms in a given declaration. *)
- val map : (Constr.t -> Constr.t) -> t -> t
+ (** Return the identifier bound by a given declaration. *)
+ val get_id : t -> Id.t
- (** Reduce all terms in a given declaration to a single value. *)
- val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+ (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+ val get_value : t -> Constr.t option
+
+ (** Return the type of the name bound by a given declaration. *)
+ val get_type : t -> Constr.t
+
+ (** Set the identifier that is bound by a given declaration. *)
+ val set_id : Id.t -> t -> t
+
+ (** Set the type of the bound variable in a given declaration. *)
+ val set_type : Constr.t -> t -> t
+
+ (** Return [true] iff a given declaration is a local assumption. *)
+ val is_local_assum : t -> bool
+
+ (** Return [true] iff a given declaration is a local definition. *)
+ val is_local_def : t -> bool
(** Check whether any term in a given declaration satisfies a given predicate. *)
val exists : (Constr.t -> bool) -> t -> bool
@@ -128,6 +175,28 @@ sig
(** Check whether the two given declarations are equal. *)
val equal : t -> t -> bool
+
+ (** Map the identifier bound by a given declaration. *)
+ val map_id : (Id.t -> Id.t) -> t -> t
+
+ (** For local assumptions, this function returns the original local assumptions.
+ For local definitions, this function maps the value in the local definition. *)
+ val map_value : (Constr.t -> Constr.t) -> t -> t
+
+ (** Map the type of the name bound by a given declaration. *)
+ val map_type : (Constr.t -> Constr.t) -> t -> t
+
+ (** Map all terms in a given declaration. *)
+ val map_constr : (Constr.t -> Constr.t) -> t -> t
+
+ (** Perform a given action on all terms in a given declaration. *)
+ val iter_constr : (Constr.t -> unit) -> t -> unit
+
+ (** Reduce all terms in a given declaration to a single value. *)
+ val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+ val to_tuple : t -> Id.t * Constr.t option * Constr.t
+ val of_tuple : Id.t * Constr.t option * Constr.t -> t
end
(** Rel-context is represented as a list of declarations.
@@ -141,13 +210,22 @@ sig
(** Return a new rel-context enriched by with a given inner-most declaration. *)
val add : Declaration.t -> t -> t
+ (** Return the number of {e local declarations} in a given named-context. *)
+ val length : t -> int
+
(** 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
+ (** Check whether given two rel-contexts are equal. *)
+ val equal : t -> t -> bool
+
(** Map all terms in a given named-context. *)
val map : (Constr.t -> Constr.t) -> t -> t
+ (** Perform a given action on every declaration in a given named-context. *)
+ val iter : (Constr.t -> unit) -> t -> unit
+
(** 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
@@ -156,15 +234,6 @@ sig
Outermost declarations are processed first. *)
val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
- (** Perform a given action on every declaration in a given named-context. *)
- val iter : (Constr.t -> unit) -> t -> unit
-
- (** Return the number of {e local declarations} in a given named-context. *)
- val length : t -> int
-
- (** Check whether given two named-contexts are equal. *)
- val equal : t -> t -> bool
-
(** Return the set of all identifiers bound in a given named-context. *)
val to_vars : t -> Id.Set.t
@@ -180,7 +249,7 @@ sig
module Declaration :
sig
type t = Id.t list * Constr.t option * Constr.t
- val map : (Constr.t -> Constr.t) -> t -> t
+ val map_constr : (Constr.t -> Constr.t) -> t -> t
end
type t = Declaration.t list
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3ab6983d8a..d2106f8609 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -201,8 +201,11 @@ let cook_constant env { from = cb; info } =
cb.const_body
in
let const_hyps =
- Context.Named.fold_outside (fun (h,_,_) hyps ->
- List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
+ Context.Named.fold_outside (fun decl hyps ->
+ let open Context.Named.Declaration in
+ let h = get_id decl in
+ List.filter (fun decl -> let id = get_id decl in
+ not (Id.equal id h)) hyps)
hyps ~init:cb.const_hyps in
let typ = match cb.const_type with
| RegularArity t ->
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8f60216afa..cfbb89f06c 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -189,16 +189,18 @@ 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.Named.lookup id env.env_named_context in
- fill_fv_cache nv id val_of_named idfun b
+ let open Context.Named in
+ let open Context.Named.Declaration in
+ fill_fv_cache nv id val_of_named idfun (lookup id env.env_named_context |> get_value)
| Some (v, _) -> v
end
| FVrel i ->
let rv = Pre_env.lookup_rel_val i env in
begin match force_lazy_val rv with
| None ->
- let _, b, _ = Context.Rel.lookup i env.env_rel_context in
- fill_fv_cache rv i val_of_rel env_of_rel b
+ let open Context.Rel in
+ let open Context.Rel.Declaration in
+ fill_fv_cache rv i val_of_rel env_of_rel (lookup i env.env_rel_context |> get_value)
| Some (v, _) -> v
end
| FVuniv_var idu ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f73eea030f..cb67135ad4 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -87,10 +87,18 @@ let is_opaque cb = match cb.const_body with
(** {7 Constant substitutions } *)
-let subst_rel_declaration sub (id,copt,t as x) =
- let copt' = Option.smartmap (subst_mps sub) copt in
- let t' = subst_mps sub t in
- if copt == copt' && t == t' then x else (id,copt',t')
+let subst_rel_declaration sub x =
+ let open Context.Rel.Declaration in
+ match x with
+ | LocalAssum (id,t) ->
+ let t' = subst_mps sub t in
+ if t == t' then x
+ else LocalAssum (id,t')
+ | LocalDef (id,v,t) ->
+ let v' = subst_mps sub v in
+ let t' = subst_mps sub t in
+ if v == v' && t == t' then x
+ else LocalDef (id,v',t')
let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
@@ -140,11 +148,20 @@ let subst_const_body sub cb =
share internal fields (e.g. constr), and not the records
themselves. But would it really bring substantial gains ? *)
-let hcons_rel_decl ((n,oc,t) as d) =
- let n' = Names.Name.hcons n
- and oc' = Option.smartmap Term.hcons_constr oc
- and t' = Term.hcons_types t
- in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
+let hcons_rel_decl d =
+ let open Context.Rel.Declaration in
+ match d with
+ | LocalAssum (n,t) ->
+ let n' = Names.Name.hcons n
+ and t' = Term.hcons_types t in
+ if n' == n && t' == t then d
+ else LocalAssum (n',t')
+ | LocalDef (n,v,t) ->
+ let n' = Names.Name.hcons n
+ and v' = Term.hcons_constr v
+ and t' = Term.hcons_types t in
+ if n' == n && v' == v && t' == t then d
+ else LocalDef (n',v',t')
let hcons_rel_context l = List.smartmap hcons_rel_decl l
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 847e1d08f9..1089dff92c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -72,9 +72,8 @@ let lookup_rel n env =
Context.Rel.lookup n env.env_rel_context
let evaluable_rel n env =
- match lookup_rel n env with
- | (_,Some _,_) -> true
- | _ -> false
+ let open Context.Rel.Declaration in
+ lookup_rel n env |> is_local_def
let nb_rel env = env.env_nb_rel
@@ -83,7 +82,8 @@ let push_rel = push_rel
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
+ let open Context.Rel.Declaration in
+ let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in
Array.fold_left (fun e assum -> push_rel assum e) env ctxt
let fold_rel_context f env ~init =
@@ -107,17 +107,8 @@ let named_vals_of_val = snd
(* [map_named_val f ctxt] apply [f] to the body and the type of
each declarations.
*** /!\ *** [f t] should be convertible with t *)
-let map_named_val f (ctxt,ctxtv) =
- let rec map ctx = match ctx with
- | [] -> []
- | (id, body, typ) :: rem ->
- let body' = Option.smartmap f body in
- let typ' = f typ in
- let rem' = map rem in
- if body' == body && typ' == typ && rem' == rem then ctx
- else (id, body', typ') :: rem'
- in
- (map ctxt, ctxtv)
+let map_named_val f =
+ on_fst (Context.Named.map f)
let empty_named_context = Context.Named.empty
@@ -138,10 +129,10 @@ let eq_named_context_val c1 c2 =
(* A local const is evaluable if it is defined *)
let named_type id env =
- let (_,_,t) = lookup_named id env in t
+ lookup_named id env |> Context.Named.Declaration.get_type
let named_body id env =
- let (_,b,_) = lookup_named id env in b
+ lookup_named id env |> Context.Named.Declaration.get_value
let evaluable_named id env =
match named_body id env with
@@ -426,15 +417,16 @@ let global_vars_set env constr =
contained in the types of the needed variables. *)
let really_needed env needed =
+ let open Context.Named.Declaration in
Context.Named.fold_inside
- (fun need (id,copt,t) ->
- if Id.Set.mem id need then
+ (fun need decl ->
+ if Id.Set.mem (get_id decl) need then
let globc =
- match copt with
- | None -> Id.Set.empty
- | Some c -> global_vars_set env c in
+ match decl with
+ | LocalAssum _ -> Id.Set.empty
+ | LocalDef (_,c,_) -> global_vars_set env c in
Id.Set.union
- (global_vars_set env t)
+ (global_vars_set env (get_type decl))
(Id.Set.union globc need)
else need)
~init:needed
@@ -443,8 +435,9 @@ let really_needed env needed =
let keep_hyps env needed =
let really_needed = really_needed env needed in
Context.Named.fold_outside
- (fun (id,_,_ as d) nsign ->
- if Id.Set.mem id really_needed then Context.Named.add d nsign
+ (fun d nsign ->
+ let open Context.Named.Declaration in
+ if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign
else nsign)
(named_context env)
~init:empty_named_context
@@ -494,11 +487,12 @@ let compile_constant_body = Cbytegen.compile_constant_body false
exception Hyp_not_found
let apply_to_hyp (ctxt,vals) id f =
+ let open Context.Named.Declaration in
let rec aux rtail ctxt vals =
match ctxt, vals with
- | (idc,c,ct as d)::ctxt, v::vals ->
- if Id.equal idc id then
- (f ctxt d rtail)::ctxt, v::vals
+ | d::ctxt, v::vals ->
+ if Id.equal (get_id d) id then
+ (f ctxt d rtail)::ctxt, v::vals
else
let ctxt',vals' = aux (d::rtail) ctxt vals in
d::ctxt', v::vals'
@@ -507,10 +501,11 @@ let apply_to_hyp (ctxt,vals) id f =
in aux [] ctxt vals
let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
+ let open Context.Named.Declaration in
let rec aux ctxt vals =
match ctxt,vals with
- | (idc,c,ct as d)::ctxt, v::vals ->
- if Id.equal idc id then
+ | d::ctxt, v::vals ->
+ if Id.equal (get_id d) id then
let sign = ctxt,vals in
push_named_context_val (f d sign) sign
else
@@ -521,10 +516,11 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
in aux ctxt vals
let insert_after_hyp (ctxt,vals) id d check =
+ let open Context.Named.Declaration in
let rec aux ctxt vals =
match ctxt, vals with
- | (idc,c,ct)::ctxt', v::vals' ->
- if Id.equal idc id then begin
+ | decl::ctxt', v::vals' ->
+ if Id.equal (get_id decl) id then begin
check ctxt;
push_named_context_val d (ctxt,vals)
end else
@@ -537,12 +533,12 @@ let insert_after_hyp (ctxt,vals) id d check =
(* To be used in Logic.clear_hyps *)
let remove_hyps ids check_context check_value (ctxt, vals) =
+ let open Context.Named.Declaration in
let rec remove_hyps ctxt vals = match ctxt, vals with
| [], [] -> [], []
| d :: rctxt, (nid, v) :: rvals ->
- let (id, _, _) = d in
let ans = remove_hyps rctxt rvals in
- if Id.Set.mem id ids then ans
+ if Id.Set.mem (get_id d) ids then ans
else
let (rctxt', rvals') = ans in
let d' = check_context d in
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index ebc1853d93..df95c93dc5 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -73,8 +73,9 @@ let judge_of_type u =
let judge_of_relative env n =
try
- let (_,_,typ) = lookup_rel n env in
- lift n typ
+ let open Context.Rel.Declaration in
+ let typ = get_type (lookup_rel n env) in
+ lift n typ
with Not_found ->
error_unbound_rel env n
@@ -91,7 +92,10 @@ let judge_of_variable env id =
(* TODO: check order? *)
let check_hyps_inclusion env f c sign =
Context.Named.fold_outside
- (fun (id,_,ty1) () ->
+ (fun decl () ->
+ let open Context.Named.Declaration in
+ let id = get_id decl in
+ let ty1 = get_type decl in
try
let ty2 = named_type id env in
if not (eq_constr ty2 ty1) then raise Exit
@@ -325,6 +329,7 @@ let type_fixpoint env lna lar vdef vdeft =
Ind et Constructsi un jour cela devient des constructions
arbitraires et non plus des variables *)
let rec execute env cstr =
+ let open Context.Rel.Declaration in
match kind_of_term cstr with
(* Atomic terms *)
| Sort (Prop c) ->
@@ -368,13 +373,13 @@ let rec execute env cstr =
| Lambda (name,c1,c2) ->
let _ = execute_is_type env c1 in
- let env1 = push_rel (name,None,c1) env in
+ let env1 = push_rel (LocalAssum (name,c1)) env in
let c2t = execute env1 c2 in
judge_of_abstraction env name c1 c2t
| Prod (name,c1,c2) ->
let vars = execute_is_type env c1 in
- let env1 = push_rel (name,None,c1) env in
+ let env1 = push_rel (LocalAssum (name,c1)) env in
let vars' = execute_is_type env1 c2 in
judge_of_product env name vars vars'
@@ -382,7 +387,7 @@ let rec execute env cstr =
let c1t = execute env c1 in
let _c2s = execute_is_type env c2 in
let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in
- let env1 = push_rel (name,Some c1,c2) env in
+ let env1 = push_rel (LocalDef (name,c1,c2)) env in
let c3t = execute env1 c3 in
subst1 c1 c3t
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a8625009ce..4834f95d15 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -20,6 +20,7 @@ open Reduction
open Typeops
open Entries
open Pp
+open Context.Rel.Declaration
(* Tell if indices (aka real arguments) contribute to size of inductive type *)
(* If yes, this is compatible with the univalent model *)
@@ -122,7 +123,7 @@ let infos_and_sort env t =
match kind_of_term t with
| Prod (name,c1,c2) ->
let varj = infer_type env c1 in
- let env1 = Environ.push_rel (name,None,varj.utj_val) env in
+ let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in
let max = Universe.sup max (univ_of_sort varj.utj_type) in
aux env1 c2 max
| _ when is_constructor_head t -> max
@@ -168,12 +169,14 @@ let infer_constructor_packet env_ar_par params lc =
(* If indices matter *)
let cumulate_arity_large_levels env sign =
fst (List.fold_right
- (fun (_,b,t as d) (lev,env) ->
- if Option.is_empty b then
+ (fun d (lev,env) ->
+ match d with
+ | LocalAssum (_,t) ->
let tj = infer_type env t in
let u = univ_of_sort tj.utj_type in
(Universe.sup u lev, push_rel d env)
- else lev, push_rel d env)
+ | LocalDef _ ->
+ lev, push_rel d env)
sign (Universe.type0m,env))
let is_impredicative env u =
@@ -184,12 +187,12 @@ let is_impredicative env u =
from the most recent and ignoring let-definitions) is not contributing
or is Some u_k if its level is u_k and is contributing. *)
let param_ccls params =
- let fold acc = function (_, None, p) ->
+ let fold acc = function (LocalAssum (_, p)) ->
(let c = strip_prod_assum p in
match kind_of_term c with
| Sort (Type u) -> Univ.Universe.level u
| _ -> None) :: acc
- | _ -> acc
+ | LocalDef _ -> acc
in
List.fold_left fold [] params
@@ -249,7 +252,7 @@ let typecheck_inductive env mie =
let full_arity = it_mkProd_or_LetIn arity params in
let id = ind.mind_entry_typename in
let env_ar' =
- push_rel (Name id, None, full_arity) env_ar in
+ push_rel (LocalAssum (Name id, full_arity)) env_ar in
(* (add_constraints cst2 env_ar) in *)
(env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l))
(env',[])
@@ -390,7 +393,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
let nhyps = List.length hyps in
let rec check k index = function
| [] -> ()
- | (_,Some _,_)::hyps -> check k (index+1) hyps
+ | LocalDef _ :: hyps -> check k (index+1) hyps
| _::hyps ->
match kind_of_term (whd_betadeltaiota env lpar.(k)) with
| Rel w when Int.equal w index -> check (k-1) (index+1) hyps
@@ -412,7 +415,7 @@ if Int.equal nmr 0 then 0 else
function
([],_) -> nmr
| (_,[]) -> assert false (* |hyps|>=nmr *)
- | (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps)
+ | (lp, LocalDef _ :: hyps) -> find k (index-1) (lp,hyps)
| (p::lp,_::hyps) ->
( match kind_of_term (whd_betadeltaiota env p) with
| Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps)
@@ -426,15 +429,15 @@ if Int.equal nmr 0 then 0 else
[lra] is the list of recursive tree of each variable
*)
let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
- (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+ (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
let auxntyp = 1 in
let specif = (lookup_mind_specif env mi, u) in
let ty = type_of_inductive env specif in
let env' =
- push_rel (Anonymous,None,
- hnf_prod_applist env ty lpar) env in
+ let decl = LocalAssum (Anonymous, hnf_prod_applist env ty lpar) in
+ push_rel decl env in
let ra_env' =
(Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -726,9 +729,9 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
in
- let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
- match b with
- | Some c ->
+ let projections decl (i, j, kns, pbs, subst, letsubst) =
+ match decl with
+ | LocalDef (na,c,t) ->
(* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
let c = liftn 1 j c in
@@ -746,7 +749,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
let letsubst = c2 :: letsubst in
(i, j+1, kns, pbs, subst, letsubst)
- | None ->
+ | LocalAssum (na,t) ->
match na with
| Name id ->
let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index dd49c4a1b7..ca29d83f6a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -17,6 +17,7 @@ open Declareops
open Environ
open Reduction
open Type_errors
+open Context.Rel.Declaration
type mind_specif = mutual_inductive_body * one_inductive_body
@@ -77,10 +78,10 @@ let instantiate_params full t u args sign =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
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)
- | (Some b,_,LetIn(_,_,_,t)) ->
+ (fun decl (largs,subs,ty) ->
+ match (decl, largs, kind_of_term ty) with
+ | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+ | (LocalDef (_,b,_), _, LetIn(_,_,_,t)) ->
(largs, (substl subs (subst_instance_constr u b))::subs, t)
| (_,[],_) -> if full then fail() else ([], subs, ty)
| _ -> fail ())
@@ -152,7 +153,7 @@ let remember_subst u subst =
(* Propagate the new levels in the signature *)
let make_subst env =
let rec make subst = function
- | (_,Some _,_)::sign, exp, args ->
+ | LocalDef _ :: sign, exp, args ->
make subst (sign, exp, args)
| d::sign, None::exp, args ->
let args = match args with _::args -> args | [] -> [] in
@@ -165,7 +166,7 @@ let make_subst env =
(* a useless extra constraint *)
let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
make (cons_subst u s subst) (sign, exp, args)
- | (na,None,t)::sign, Some u::exp, [] ->
+ | LocalAssum (na,t) :: sign, Some u::exp, [] ->
(* No more argument here: we add the remaining universes to the *)
(* substitution (when [u] is distinct from all other universes in the *)
(* template, it is identity substitution otherwise (ie. when u is *)
@@ -314,14 +315,14 @@ let is_correct_arity env c pj ind specif params =
let rec srec env pt ar =
let pt' = whd_betadeltaiota env pt in
match kind_of_term pt', ar with
- | Prod (na1,a1,t), (_,None,a1')::ar' ->
+ | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
let () =
try conv env a1 a1'
with NotConvertible -> raise (LocalArity None) in
- srec (push_rel (na1,None,a1) env) t ar'
+ srec (push_rel (LocalAssum (na1,a1)) env) t ar'
(* The last Prod domain is the type of the scrutinee *)
| Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
- let env' = push_rel (na1,None,a1) env in
+ let env' = push_rel (LocalAssum (na1,a1)) env in
let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
| Sort s -> family_of_sort s
| _ -> raise (LocalArity None) in
@@ -330,7 +331,7 @@ let is_correct_arity env c pj ind specif params =
try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None) in
check_allowed_sort ksort specif
- | _, (_,Some _,_ as d)::ar' ->
+ | _, (LocalDef _ as d)::ar' ->
srec (push_rel d env) (lift 1 pt') ar'
| _ ->
raise (LocalArity None)
@@ -482,7 +483,7 @@ let make_renv env recarg tree =
genv = [Lazy.lazy_from_val(Subterm(Large,tree))] }
let push_var renv (x,ty,spec) =
- { env = push_rel (x,None,ty) renv.env;
+ { env = push_rel (LocalAssum (x,ty)) renv.env;
rel_min = renv.rel_min+1;
genv = spec:: renv.genv }
@@ -568,14 +569,14 @@ let check_inductive_codomain env p =
(* The following functions are almost duplicated from indtypes.ml, except
that they carry here a poorer environment (containing less information). *)
let ienv_push_var (env, lra) (x,a,ra) =
- (push_rel (x,None,a) env, (Norec,ra)::lra)
+ (push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra)
let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
let mib = Environ.lookup_mind mind env in
let ntypes = mib.mind_ntypes in
let push_ind specif env =
- push_rel (Anonymous,None,
- hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env
+ let decl = LocalAssum (Anonymous, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+ push_rel decl env
in
let env = Array.fold_right push_ind mib.mind_packets env in
let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
@@ -848,7 +849,7 @@ let filter_stack_domain env ci p stack =
let t = whd_betadeltaiota env ar in
match stack, kind_of_term t with
| elt :: stack', Prod (n,a,c0) ->
- let d = (n,None,a) in
+ let d = LocalAssum (n,a) in
let ty, args = decompose_app (whd_betadeltaiota env a) in
let elt = match kind_of_term ty with
| Ind ind ->
@@ -905,10 +906,10 @@ let check_one_fix renv recpos trees def =
end
else
begin
- match pi2 (lookup_rel p renv.env) with
- | None ->
+ match lookup_rel p renv.env with
+ | LocalAssum _ ->
List.iter (check_rec_call renv []) l
- | Some c ->
+ | LocalDef (_,c,_) ->
try List.iter (check_rec_call renv []) l
with FixGuardError _ ->
check_rec_call renv stack (applist(lift p c,l))
@@ -983,10 +984,11 @@ let check_one_fix renv recpos trees def =
| Var id ->
begin
- match pi2 (lookup_named id renv.env) with
- | None ->
+ let open Context.Named.Declaration in
+ match lookup_named id renv.env with
+ | LocalAssum _ ->
List.iter (check_rec_call renv []) l
- | Some c ->
+ | LocalDef (_,c,_) ->
try List.iter (check_rec_call renv []) l
with (FixGuardError _) ->
check_rec_call renv stack (applist(c,l))
@@ -1040,7 +1042,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
match kind_of_term (whd_betadeltaiota env def) with
| Lambda (x,a,b) ->
if noccur_with_meta n nbfix a then
- let env' = push_rel (x, None, a) env in
+ let env' = push_rel (LocalAssum (x,a)) env in
if Int.equal n (k + 1) then
(* get the inductive type of the fixpoint *)
let (mind, _) =
@@ -1090,7 +1092,7 @@ let rec codomain_is_coind env c =
let b = whd_betadeltaiota env c in
match kind_of_term b with
| Prod (x,a,b) ->
- codomain_is_coind (push_rel (x, None, a) env) b
+ codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
| _ ->
(try find_coinductive env b
with Not_found ->
@@ -1131,7 +1133,7 @@ let check_one_cofix env nbfix def deftype =
| Lambda (x,a,b) ->
let () = assert (List.is_empty args) in
if noccur_with_meta n nbfix a then
- let env' = push_rel (x, None, a) env in
+ let env' = push_rel (LocalAssum (x,a)) env in
check_rec_call env' alreadygrd (n+1) tree vlra b
else
raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 711096b2b1..47274a5cd5 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1832,24 +1832,25 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
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,_) = Context.Rel.lookup n env.env_rel_context in
+ let decl = 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 open Context.Rel.Declaration in
+ match decl with
+ | LocalDef (_,t,_) ->
let code = lambda_of_constr env sigma t in
let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
Glet(Grel n, code)::auxdefs
- | None ->
+ | LocalAssum _ ->
Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
and compile_named env sigma univ auxdefs id =
- let (_,body,_) = Context.Named.lookup id env.env_named_context in
- match body with
- | Some t ->
+ let open Context.Named.Declaration in
+ match Context.Named.lookup id env.env_named_context with
+ | LocalDef (_,t,_) ->
let code = lambda_of_constr env sigma t in
let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
Glet(Gnamed id, code)::auxdefs
- | None ->
+ | LocalAssum _ ->
Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
let compile_constant env sigma prefix ~interactive con cb =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 01f59df15a..91b40be7e9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -727,7 +727,8 @@ let optimize lam =
let lambda_of_constr env sigma c =
set_global_env env;
let env = Renv.make () in
- let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in
+ let open Context.Rel.Declaration in
+ let ids = List.rev_map get_name !global_env.env_rel_context in
Renv.push_rels env (Array.of_list ids);
let lam = lambda_of_constr env sigma c in
(* if Flags.vm_draw_opt () then begin
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 4c1b2c5a64..99d99e6940 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -18,6 +18,7 @@ open Names
open Univ
open Term
open Declarations
+open Context.Named.Declaration
(* The type of environments. *)
@@ -124,18 +125,16 @@ let env_of_rel n env =
(* Named context *)
let push_named_context_val d (ctxt,vals) =
- let id,_,_ = d in
let rval = ref VKnone in
- Context.Named.add d ctxt, (id,rval)::vals
+ Context.Named.add d ctxt, (get_id d,rval)::vals
let push_named d env =
(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
assert (env.env_rel_context = []); *)
- let id,body,_ = d in
let rval = ref VKnone in
{ env_globals = env.env_globals;
env_named_context = Context.Named.add d env.env_named_context;
- env_named_vals = (id, rval) :: env.env_named_vals;
+ env_named_vals = (get_id d, rval) :: env.env_named_vals;
env_rel_context = env.env_rel_context;
env_rel_val = env.env_rel_val;
env_nb_rel = env.env_nb_rel;
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 40b80cc5e9..cfc286135d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -24,6 +24,7 @@ open Univ
open Environ
open Closure
open Esubst
+open Context.Rel.Declaration
let rec is_empty_stack = function
[] -> true
@@ -739,7 +740,7 @@ let dest_prod env =
let t = whd_betadeltaiota env c in
match kind_of_term t with
| Prod (n,a,c0) ->
- let d = (n,None,a) in
+ let d = LocalAssum (n,a) in
decrec (push_rel d env) (Context.Rel.add d m) c0
| _ -> m,t
in
@@ -751,10 +752,10 @@ let dest_prod_assum env =
let rty = whd_betadeltaiota_nolet env ty in
match kind_of_term rty with
| Prod (x,t,c) ->
- let d = (x,None,t) in
+ let d = LocalAssum (x,t) in
prodec_rec (push_rel d env) (Context.Rel.add d l) c
| LetIn (x,b,t,c) ->
- let d = (x,Some b,t) in
+ let d = LocalDef (x,b,t) in
prodec_rec (push_rel d env) (Context.Rel.add d l) c
| Cast (c,_,_) -> prodec_rec env l c
| _ ->
@@ -769,10 +770,10 @@ let dest_lam_assum env =
let rty = whd_betadeltaiota_nolet env ty in
match kind_of_term rty with
| Lambda (x,t,c) ->
- let d = (x,None,t) in
+ let d = LocalAssum (x,t) in
lamec_rec (push_rel d env) (Context.Rel.add d l) c
| LetIn (x,b,t,c) ->
- let d = (x,Some b,t) in
+ let d = LocalDef (x,b,t) in
lamec_rec (push_rel d env) (Context.Rel.add d l) c
| Cast (c,_,_) -> lamec_rec env l c
| _ -> l,rty
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e56a6e0999..8a402322f0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -60,6 +60,7 @@
open Util
open Names
open Declarations
+open Context.Named.Declaration
(** {6 Safe environments }
@@ -362,7 +363,8 @@ let check_required current_libs needed =
hypothesis many many times, and the check performed here would
cost too much. *)
-let safe_push_named (id,_,_ as d) env =
+let safe_push_named d env =
+ let id = get_id d in
let _ =
try
let _ = Environ.lookup_named id env in
@@ -383,13 +385,13 @@ let push_named_def (id,de) senv =
(Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
| _ -> assert false in
let senv' = push_context_set poly univs senv in
- let env'' = safe_push_named (id,Some c,typ) senv'.env in
+ let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
univs, {senv' with env=env''}
let push_named_assum ((id,t,poly),ctx) senv =
let senv' = push_context_set poly ctx senv in
let t = Term_typing.translate_local_assum senv'.env t in
- let env'' = safe_push_named (id,None,t) senv'.env in
+ let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in
{senv' with env=env''}
diff --git a/kernel/term.ml b/kernel/term.ml
index 9ba45f5403..4416770fe4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -383,40 +383,46 @@ let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c)
let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2)
(* Constructs either [(x:t)c] or [[x=b:t]c] *)
-let mkProd_or_LetIn (na,body,t) c =
- match body with
- | None -> mkProd (na, t, c)
- | Some b -> mkLetIn (na, b, t, c)
-
-let mkNamedProd_or_LetIn (id,body,t) c =
- match body with
- | None -> mkNamedProd id t c
- | Some b -> mkNamedLetIn id b t c
+let mkProd_or_LetIn decl c =
+ let open Context.Rel.Declaration in
+ match decl with
+ | LocalAssum (na,t) -> mkProd (na, t, c)
+ | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
+
+let mkNamedProd_or_LetIn decl c =
+ let open Context.Named.Declaration in
+ match decl with
+ | LocalAssum (id,t) -> mkNamedProd id t c
+ | LocalDef (id,b,t) -> mkNamedLetIn id b t c
(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
-let mkProd_wo_LetIn (na,body,t) c =
- match body with
- | None -> mkProd (na, t, c)
- | Some b -> subst1 b c
-
-let mkNamedProd_wo_LetIn (id,body,t) c =
- match body with
- | None -> mkNamedProd id t c
- | Some b -> subst1 b (subst_var id c)
+let mkProd_wo_LetIn decl c =
+ let open Context.Rel.Declaration in
+ match decl with
+ | LocalAssum (na,t) -> mkProd (na, t, c)
+ | LocalDef (na,b,t) -> subst1 b c
+
+let mkNamedProd_wo_LetIn decl c =
+ let open Context.Named.Declaration in
+ match decl with
+ | LocalAssum (id,t) -> mkNamedProd id t c
+ | LocalDef (id,b,t) -> subst1 b (subst_var id c)
(* non-dependent product t1 -> t2 *)
let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
(* Constructs either [[x:t]c] or [[x=b:t]c] *)
-let mkLambda_or_LetIn (na,body,t) c =
- match body with
- | None -> mkLambda (na, t, c)
- | Some b -> mkLetIn (na, b, t, c)
-
-let mkNamedLambda_or_LetIn (id,body,t) c =
- match body with
- | None -> mkNamedLambda id t c
- | Some b -> mkNamedLetIn id b t c
+let mkLambda_or_LetIn decl c =
+ let open Context.Rel.Declaration in
+ match decl with
+ | LocalAssum (na,t) -> mkLambda (na, t, c)
+ | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
+
+let mkNamedLambda_or_LetIn decl c =
+ let open Context.Named.Declaration in
+ match decl with
+ | LocalAssum (id,t) -> mkNamedLambda id t c
+ | LocalDef (id,b,t) -> mkNamedLetIn id b t c
(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
let prodn n env b =
@@ -576,10 +582,11 @@ let decompose_lam_n n =
(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
let decompose_prod_assum =
+ let open Context.Rel.Declaration in
let rec prodec_rec l c =
match kind_of_term c with
- | 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
+ | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+ | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
| Cast (c,_,_) -> prodec_rec l c
| _ -> l,c
in
@@ -589,9 +596,10 @@ let decompose_prod_assum =
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
let decompose_lam_assum =
let rec lamdec_rec l c =
+ let open Context.Rel.Declaration in
match kind_of_term c with
- | 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
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
| Cast (c,_,_) -> lamdec_rec l c
| _ -> l,c
in
@@ -606,11 +614,13 @@ let decompose_prod_n_assum n =
error "decompose_prod_n_assum: integer parameter must be positive";
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 (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"
+ else
+ let open Context.Rel.Declaration in
+ match kind_of_term c with
+ | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+ | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,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 Context.Rel.empty n
@@ -625,11 +635,13 @@ let decompose_lam_n_assum n =
error "decompose_lam_n_assum: integer parameter must be positive";
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 (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"
+ else
+ let open Context.Rel.Declaration in
+ match kind_of_term c with
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
+ | Cast (c,_,_) -> lamdec_rec l n c
+ | c -> error "decompose_lam_n_assum: not enough abstractions"
in
lamdec_rec Context.Rel.empty n
@@ -639,11 +651,13 @@ let decompose_lam_n_decls n =
error "decompose_lam_n_decls: integer parameter must be positive";
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 (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"
+ else
+ let open Context.Rel.Declaration in
+ match kind_of_term c with
+ | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,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 Context.Rel.empty n
@@ -669,10 +683,11 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
type arity = Context.Rel.t * sorts
let destArity =
+ let open Context.Rel.Declaration in
let rec prodec_rec l c =
match kind_of_term c with
- | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c
- | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+ | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c
+ | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
| Cast (c,_,_) -> prodec_rec l c
| Sort s -> l,s
| _ -> anomaly ~label:"destArity" (Pp.str "not an arity")
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 979165e49c..2a3ac957fb 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -138,16 +138,17 @@ let check_signatures curmb sl =
let skip_trusted_seff sl b e =
let rec aux sl b e acc =
+ let open Context.Rel.Declaration in
match sl, kind_of_term b with
| (None|Some 0), _ -> b, e, acc
| Some sl, LetIn (n,c,ty,bo) ->
aux (Some (sl-1)) bo
- (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc)
+ (Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc)
| Some sl, App(hd,arg) ->
begin match kind_of_term hd with
| Lambda (n,ty,bo) ->
aux (Some (sl-1)) bo
- (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc)
+ (Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc)
| _ -> assert false
end
| _ -> assert false
@@ -251,11 +252,13 @@ let global_vars_set_constant_type env = function
ctx ~init:Id.Set.empty
let record_aux env s_ty s_bo suggested_expr =
+ let open Context.Named.Declaration in
let in_ty = keep_hyps env s_ty in
let v =
String.concat " "
- (CList.map_filter (fun (id, _,_) ->
- if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+ (CList.map_filter (fun decl ->
+ let id = get_id decl in
+ if List.exists (Id.equal id % get_id) in_ty then None
else Some (Id.to_string id))
(keep_hyps env s_bo)) in
Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
@@ -264,8 +267,9 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
let set_suggest_proof_using f = suggest_proof_using := f
let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+ let open Context.Named.Declaration in
let check declared inferred =
- let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+ let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
let inferred_set, declared_set = mk_set inferred, mk_set declared in
if not (Id.Set.subset inferred_set declared_set) then
let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
@@ -276,12 +280,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
str " used but not declared:" ++
fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
let sort evn l =
- List.filter (fun (id,_,_) ->
- List.exists (fun (id',_,_) -> Names.Id.equal id id') l)
+ List.filter (fun decl ->
+ let id = get_id decl in
+ List.exists (Names.Id.equal id % get_id) l)
(named_context env) in
(* We try to postpone the computation of used section variables *)
let hyps, def =
- let context_ids = List.map pi1 (named_context env) in
+ let context_ids = List.map get_id (named_context env) in
match ctx with
| None when not (List.is_empty context_ids) ->
(* No declared section vars, and non-empty section context:
@@ -472,7 +477,8 @@ let translate_local_def mb env id centry =
| Undef _ -> ()
| Def _ -> ()
| OpaqueDef lc ->
- let context_ids = List.map pi1 (named_context env) in
+ let open Context.Named.Declaration in
+ let context_ids = List.map get_id (named_context env) in
let ids_typ = global_vars_set env typ in
let ids_def = global_vars_set env
(Opaqueproof.force_proof (opaque_tables env) lc) in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f31cba0a8a..eeb12a2b49 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -77,8 +77,9 @@ let judge_of_type u =
(*s Type of a de Bruijn index. *)
let judge_of_relative env n =
+ let open Context.Rel.Declaration in
try
- let (_,_,typ) = lookup_rel n env in
+ let typ = get_type (lookup_rel n env) in
{ uj_val = mkRel n;
uj_type = lift n typ }
with Not_found ->
@@ -98,18 +99,20 @@ 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 =
+ let open Context.Named.Declaration in
Context.Named.fold_outside
- (fun (id,b1,ty1) () ->
+ (fun d1 () ->
+ let id = get_id d1 in
try
- let (_,b2,ty2) = lookup_named id env in
- conv env ty2 ty1;
- (match b2,b1 with
- | None, None -> ()
- | None, Some _ ->
+ let d2 = lookup_named id env in
+ conv env (get_type d2) (get_type d1);
+ (match d2,d1 with
+ | LocalAssum _, LocalAssum _ -> ()
+ | LocalAssum _, LocalDef _ ->
(* This is wrong, because we don't know if the body is
needed or not for typechecking: *) ()
- | Some _, None -> raise NotConvertible
- | Some b2, Some b1 -> conv env b2 b1);
+ | LocalDef _, LocalAssum _ -> raise NotConvertible
+ | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1);
with Not_found | NotConvertible | Option.Heterogeneous ->
error_reference_variables env id c)
sign
@@ -124,9 +127,10 @@ let extract_level env p =
match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
let extract_context_levels env l =
- let fold l (_, b, p) = match b with
- | None -> extract_level env p :: l
- | _ -> l
+ let open Context.Rel.Declaration in
+ let fold l = function
+ | LocalAssum (_,p) -> extract_level env p :: l
+ | LocalDef _ -> l
in
List.fold_left fold [] l
@@ -416,6 +420,7 @@ let type_fixpoint env lna lar vdefj =
Ind et Constructsi un jour cela devient des constructions
arbitraires et non plus des variables *)
let rec execute env cstr =
+ let open Context.Rel.Declaration in
match kind_of_term cstr with
(* Atomic terms *)
| Sort (Prop c) ->
@@ -458,13 +463,13 @@ let rec execute env cstr =
| Lambda (name,c1,c2) ->
let varj = execute_type env c1 in
- let env1 = push_rel (name,None,varj.utj_val) env in
+ let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in
let j' = execute env1 c2 in
judge_of_abstraction env name varj j'
| Prod (name,c1,c2) ->
let varj = execute_type env c1 in
- let env1 = push_rel (name,None,varj.utj_val) env in
+ let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in
let varj' = execute_type env1 c2 in
judge_of_product env name varj varj'
@@ -472,7 +477,7 @@ let rec execute env cstr =
let j1 = execute env c1 in
let j2 = execute_type env c2 in
let _ = judge_of_cast env j1 DEFAULTcast j2 in
- let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
+ let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in
let j' = execute env1 c3 in
judge_of_letin env name j1 j2 j'
@@ -550,10 +555,10 @@ let infer_v env cv =
let infer_local_decl env id = function
| LocalDef c ->
let j = infer env c in
- (Name id, Some j.uj_val, j.uj_type)
+ Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type)
| LocalAssum c ->
let j = infer env c in
- (Name id, None, assumption_of_judgment env j)
+ Context.Rel.Declaration.LocalAssum (Name id, assumption_of_judgment env j)
let infer_local_decls env decls =
let rec inferec env = function
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4554c6be17..b935ab6b91 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -8,6 +8,7 @@
open Names
open Esubst
+open Context.Rel.Declaration
(*********************)
(* Occurring *)
@@ -159,17 +160,17 @@ 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 = 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
+let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r
+let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r
+let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r
(* Build a substitution from an instance, inserting missing let-ins *)
let subst_of_rel_context_instance sign l =
let rec aux subst sign l =
match sign, l with
- | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
- | (_,Some c,_)::sign', args' ->
+ | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args'
+ | LocalDef (_,c,_)::sign', args' ->
aux (substl subst c :: subst) sign' args'
| [], [] -> subst
| _ -> Errors.anomaly (Pp.str "Instance and signature do not match")
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:49:59 +0000