aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/constr.mli18
-rw-r--r--kernel/context.ml55
-rw-r--r--kernel/context.mli24
-rw-r--r--kernel/cooking.ml7
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/csymtable.ml10
-rw-r--r--kernel/declarations.mli11
-rw-r--r--kernel/declareops.ml7
-rw-r--r--kernel/entries.mli4
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/fast_typeops.ml11
-rw-r--r--kernel/names.ml11
-rw-r--r--kernel/names.mli9
-rw-r--r--kernel/nativecode.ml7
-rw-r--r--kernel/nativelambda.ml5
-rw-r--r--kernel/nativelib.ml2
-rw-r--r--kernel/pre_env.ml11
-rw-r--r--kernel/safe_typing.ml10
-rw-r--r--kernel/term.ml33
-rw-r--r--kernel/term.mli14
-rw-r--r--kernel/term_typing.ml24
-rw-r--r--kernel/typeops.ml7
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/vars.ml19
-rw-r--r--kernel/vars.mli4
27 files changed, 177 insertions, 136 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index b1fc0c85de..57b397e6f8 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -979,7 +979,7 @@ let compile fail_on_error ?universes:(universes=0) env c =
Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive tname ->
- let fn = if fail_on_error then CErrors.errorlabstrm "compile" else
+ let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else
(fun x -> Feedback.msg_warning x) in
(Pp.(fn
(str "Cannot compile code for virtual machine as it uses inductive " ++
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 42d298e3b9..7095dbe6f9 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -189,8 +189,12 @@ type ('constr, 'types) pcofixpoint =
int * ('constr, 'types) prec_declaration
type ('constr, 'types) kind_of_term =
- | Rel of int
- | Var of Id.t
+ | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
+
+ | Var of Id.t (** Gallina-variable that was introduced by Vernacular-command that extends
+ the local context of the currently open section
+ (i.e. [Variable] or [Let]). *)
+
| Meta of metavariable
| Evar of 'constr pexistential
| Sort of Sorts.t
@@ -199,12 +203,16 @@ type ('constr, 'types) kind_of_term =
| Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *)
| LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *)
| App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])].
+
The {!mkApp} constructor also enforces the following invariant:
- [F] itself is not {!App}
- and [[|P1;..;Pn|]] is not empty. *)
- | Const of constant puniverses
- | Ind of inductive puniverses
- | Construct of constructor puniverses
+
+ | Const of constant puniverses (** Gallina-variable that was introduced by Vernacular-command that extends the global environment
+ (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *)
+
+ | Ind of inductive puniverses (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
+ | Construct of constructor puniverses (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
diff --git a/kernel/context.ml b/kernel/context.ml
index 4e53b73a28..ae0388003d 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -138,7 +138,7 @@ struct
| LocalDef (_,v,ty) -> f v; f ty
(** Reduce all terms in a given declaration to a single value. *)
- let fold f decl acc =
+ let fold_constr f decl acc =
match decl with
| LocalAssum (n,ty) -> f ty acc
| LocalDef (n,v,ty) -> f ty (f v acc)
@@ -147,9 +147,6 @@ struct
| 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.
@@ -336,7 +333,7 @@ struct
| LocalDef (_, v, ty) -> f v; f ty
(** Reduce all terms in a given declaration to a single value. *)
- let fold f decl a =
+ let fold_constr f decl a =
match decl with
| LocalAssum (_, ty) -> f ty a
| LocalDef (_, v, ty) -> a |> f v |> f ty
@@ -348,6 +345,18 @@ struct
let of_tuple = function
| id, None, ty -> LocalAssum (id, ty)
| id, Some v, ty -> LocalDef (id, v, ty)
+
+ let of_rel_decl f = function
+ | Rel.Declaration.LocalAssum (na,t) ->
+ LocalAssum (f na, t)
+ | Rel.Declaration.LocalDef (na,v,t) ->
+ LocalDef (f na, v, t)
+
+ let to_rel_decl = function
+ | LocalAssum (id,t) ->
+ Rel.Declaration.LocalAssum (Name id, t)
+ | LocalDef (id,v,t) ->
+ Rel.Declaration.LocalDef (Name id,v,t)
end
(** Named-context is represented as a list of declarations.
@@ -401,23 +410,39 @@ struct
| _ -> None
in
List.map_filter filter
- end
+end
-module NamedList =
+module Compacted =
struct
module Declaration =
struct
- type t = Id.t list * Constr.t option * Constr.t
-
- 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')
+ type t =
+ | LocalAssum of Id.t list * Constr.t
+ | LocalDef of Id.t list * Constr.t * Constr.t
+
+ let map_constr f = function
+ | LocalAssum (ids, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalAssum (ids, ty')
+ | LocalDef (ids, c, ty) as decl ->
+ let ty' = f ty in
+ let c' = f c in
+ if c == c' && ty == ty' then decl else LocalDef (ids,c',ty')
+
+ let of_named_decl = function
+ | Named.Declaration.LocalAssum (id,t) ->
+ LocalAssum ([id],t)
+ | Named.Declaration.LocalDef (id,v,t) ->
+ LocalDef ([id],v,t)
+
+ let to_named_context = function
+ | LocalAssum (ids, t) ->
+ List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids
+ | LocalDef (ids, v, t) ->
+ List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids
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 b5f3904d22..955e214cb9 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -79,10 +79,9 @@ sig
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 fold_constr : (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.
@@ -193,10 +192,18 @@ sig
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 fold_constr : (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
+
+ (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value.
+ The function provided as the first parameter determines how to translate "names" to "ids". *)
+ val of_rel_decl : (Name.t -> Id.t) -> Rel.Declaration.t -> t
+
+ (** Convert [Named.Declaration.t] value to the corresponding [Rel.Declaration.t] value. *)
+ (* TODO: Move this function to [Rel.Declaration] module and rename it to [of_named]. *)
+ val to_rel_decl : t -> Rel.Declaration.t
end
(** Rel-context is represented as a list of declarations.
@@ -244,17 +251,20 @@ sig
val to_instance : t -> Constr.t list
end
-module NamedList :
+module Compacted :
sig
module Declaration :
sig
- type t = Id.t list * Constr.t option * Constr.t
+ type t =
+ | LocalAssum of Id.t list * Constr.t
+ | LocalDef of Id.t list * Constr.t * Constr.t
+
val map_constr : (Constr.t -> Constr.t) -> t -> t
+ val of_named_decl : Named.Declaration.t -> t
+ val to_named_context : t -> Named.t
end
type t = Declaration.t 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 1345991503..f5059cd750 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -21,6 +21,8 @@ open Declarations
open Environ
open Univ
+module NamedDecl = Context.Named.Declaration
+
(*s Cooking the constants. *)
let pop_dirpath p = match DirPath.repr p with
@@ -152,7 +154,7 @@ type inline = bool
type result =
constant_def * constant_type * projection_body option *
bool * constant_universes * inline
- * Context.section_context option
+ * Context.Named.t option
let on_body ml hy f = function
| Undef _ as x -> x
@@ -202,8 +204,7 @@ let cook_constant env { from = cb; info } =
in
let const_hyps =
Context.Named.fold_outside (fun decl hyps ->
- let open Context.Named.Declaration in
- List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl')))
+ List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
hyps)
hyps ~init:cb.const_hyps in
let typ = match cb.const_type with
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 327e697d23..eb40730969 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -19,7 +19,7 @@ type inline = bool
type result =
constant_def * constant_type * projection_body option *
bool * constant_universes * inline
- * Context.section_context option
+ * Context.Named.t option
val cook_constant : env -> recipe -> result
val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index c27cb04870..40595f944c 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -22,6 +22,8 @@ open Declarations
open Pre_env
open Cbytegen
+module NamedDecl = Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
@@ -189,18 +191,14 @@ 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 open Context.Named in
- let open Declaration in
- env |> Pre_env.lookup_named id |> get_value |> fill_fv_cache nv id val_of_named idfun
+ env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun
| 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 open Context.Rel in
- let open Declaration in
- env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel
+ env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
| Some (v, _) -> v
end
| FVuniv_var idu ->
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index f89773fcc5..7821ea20ff 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -58,10 +58,11 @@ type projection_body = {
proj_body : constr; (* For compatibility with VMs only, the match version *)
}
+(* Global declarations (i.e. constants) can be either: *)
type constant_def =
- | Undef of inline
- | Def of constr Mod_subst.substituted
- | OpaqueDef of Opaqueproof.opaque
+ | Undef of inline (** a global assumption *)
+ | Def of constr Mod_subst.substituted (** or a transparent global definition *)
+ | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *)
type constant_universes = Univ.universe_context
@@ -78,7 +79,7 @@ type typing_flags = {
(* some contraints are in constant_constraints, some other may be in
* the OpaueDef *)
type constant_body = {
- const_hyps : Context.section_context; (** New: younger hyp at top *)
+ const_hyps : Context.Named.t; (** New: younger hyp at top *)
const_body : constant_def;
const_type : constant_type;
const_body_code : Cemitcodes.to_patch_substituted option;
@@ -177,7 +178,7 @@ type mutual_inductive_body = {
mind_ntypes : int; (** Number of types in the block *)
- mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *)
+ mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *)
mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 211e5e062a..0a822d6fad 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -9,7 +9,8 @@
open Declarations
open Mod_subst
open Util
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
(** Operations concernings types in [Declarations] :
[constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -94,7 +95,7 @@ let is_opaque cb = match cb.const_body with
(** {7 Constant substitutions } *)
let subst_rel_declaration sub =
- map_constr (subst_mps sub)
+ RelDecl.map_constr (subst_mps sub)
let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
@@ -146,7 +147,7 @@ let subst_const_body sub cb =
themselves. But would it really bring substantial gains ? *)
let hcons_rel_decl =
- map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons
+ RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types
let hcons_rel_context l = List.smartmap hcons_rel_decl l
diff --git a/kernel/entries.mli b/kernel/entries.mli
index ea7c266bcd..77081947ec 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -61,7 +61,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
type 'a definition_entry = {
const_entry_body : 'a const_entry_body;
(* List of section variables *)
- const_entry_secctx : Context.section_context option;
+ const_entry_secctx : Context.Named.t option;
(* State id on which the completion of type checking is reported *)
const_entry_feedback : Stateid.t option;
const_entry_type : types option;
@@ -73,7 +73,7 @@ type 'a definition_entry = {
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
- Context.section_context option * bool * types Univ.in_universe_context * inline
+ Context.Named.t option * bool * types Univ.in_universe_context * inline
type projection_entry = {
proj_entry_ind : mutual_inductive;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 16ddfac64b..4a543f1957 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -413,7 +413,7 @@ let global_vars_set env constr =
Id.Set.union (vars_of_global env c) acc
| _ ->
acc in
- fold_constr filtrec acc c
+ Term.fold_constr filtrec acc c
in
filtrec Id.Set.empty constr
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6ac00088b3..ea570cb4a8 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -231,7 +231,7 @@ val vars_of_global : env -> constr -> Id.Set.t
val really_needed : env -> Id.Set.t -> Id.Set.t
(** like [really_needed] but computes a well ordered named context *)
-val keep_hyps : env -> Id.Set.t -> Context.section_context
+val keep_hyps : env -> Id.Set.t -> Context.Named.t
(** {5 Unsafe judgments. }
We introduce here the pre-type of judgments, which is
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index bd91c689d2..dce4e93076 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -18,6 +18,9 @@ open Reduction
open Inductive
open Type_errors
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
let conv_leq_vecti env v1 v2 =
@@ -73,8 +76,7 @@ let judge_of_type u =
let judge_of_relative env n =
try
- let open Context.Rel.Declaration in
- env |> lookup_rel n |> get_type |> lift n
+ env |> lookup_rel n |> RelDecl.get_type |> lift n
with Not_found ->
error_unbound_rel env n
@@ -92,9 +94,8 @@ let judge_of_variable env id =
let check_hyps_inclusion env f c sign =
Context.Named.fold_outside
(fun decl () ->
- let open Context.Named.Declaration in
- let id = get_id decl in
- let ty1 = get_type decl in
+ let id = NamedDecl.get_id decl in
+ let ty1 = NamedDecl.get_type decl in
try
let ty2 = named_type id env in
if not (eq_constr ty2 ty1) then raise Exit
diff --git a/kernel/names.ml b/kernel/names.ml
index 1eb9a31751..1f138581cc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -88,11 +88,14 @@ struct
type t = Anonymous (** anonymous identifier *)
| Name of Id.t (** non-anonymous identifier *)
+ let mk_name id =
+ Name id
+
let is_anonymous = function
| Anonymous -> true
| Name _ -> false
- let is_name = not % is_anonymous
+ let is_name = is_anonymous %> not
let compare n1 n2 = match n1, n2 with
| Anonymous, Anonymous -> 0
@@ -601,7 +604,13 @@ end
module Constant = KerPair
module Cmap = HMap.Make(Constant.CanOrd)
+(** A map whose keys are constants (values of the {!Constant.t} type).
+ Keys are ordered wrt. "cannonical form" of the constant. *)
+
module Cmap_env = HMap.Make(Constant.UserOrd)
+(** A map whose keys are constants (values of the {!Constant.t} type).
+ Keys are ordered wrt. "user form" of the constant. *)
+
module Cpred = Predicate.Make(Constant.CanOrd)
module Cset = Cmap.Set
module Cset_env = Cmap_env.Set
diff --git a/kernel/names.mli b/kernel/names.mli
index feaedc775c..6b0a80625b 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -82,6 +82,9 @@ sig
type t = Anonymous (** anonymous identifier *)
| Name of Id.t (** non-anonymous identifier *)
+ val mk_name : Id.t -> t
+ (** constructor *)
+
val is_anonymous : t -> bool
(** Return [true] iff a given name is [Anonymous]. *)
@@ -368,8 +371,14 @@ end
module Cpred : Predicate.S with type elt = Constant.t
module Cset : CSig.SetS with type elt = Constant.t
module Cset_env : CSig.SetS with type elt = Constant.t
+
module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset
+(** A map whose keys are constants (values of the {!Constant.t} type).
+ Keys are ordered wrt. "cannonical form" of the constant. *)
+
module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env
+(** A map whose keys are constants (values of the {!Constant.t} type).
+ Keys are ordered wrt. "user form" of the constant. *)
(** {6 Inductive names} *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index eaddace4b7..33bd7d8ddc 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1848,10 +1848,9 @@ 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 open Context.Rel in
- let n = length env.env_rel_context - n in
- let open Declaration in
- match lookup n env.env_rel_context with
+ let n = Context.Rel.length env.env_rel_context - n in
+ let open Context.Rel.Declaration in
+ match Context.Rel.lookup n env.env_rel_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
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 91b40be7e9..366f9a0a6d 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -14,6 +14,8 @@ open Pre_env
open Nativevalues
open Nativeinstr
+module RelDecl = Context.Rel.Declaration
+
(** This file defines the lambda code generation phase of the native compiler *)
exception NotClosed
@@ -727,8 +729,7 @@ let optimize lam =
let lambda_of_constr env sigma c =
set_global_env env;
let env = Renv.make () in
- let open Context.Rel.Declaration in
- let ids = List.rev_map get_name !global_env.env_rel_context in
+ let ids = List.rev_map RelDecl.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/nativelib.ml b/kernel/nativelib.ml
index 1c58c7445c..6bd82170e6 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -35,7 +35,7 @@ let ( / ) = Filename.concat
(* We have to delay evaluation of include_dirs because coqlib cannot be guessed
until flags have been properly initialized *)
let include_dirs () =
- [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"]
+ [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"]
(* Pointer to the function linking an ML object into coq's toplevel *)
let load_obj = ref (fun x -> () : string -> unit)
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index f211583e06..d14a254d32 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -17,7 +17,8 @@ open Util
open Names
open Term
open Declarations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(* The type of environments. *)
@@ -128,10 +129,10 @@ let env_of_rel n env =
(* Named context *)
let push_named_context_val_val d rval ctxt =
-(* assert (not (Id.Map.mem (get_id d) ctxt.env_named_map)); *)
+(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *)
{
env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
- env_named_map = Id.Map.add (get_id d) (d, rval) ctxt.env_named_map;
+ env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map;
}
let push_named_context_val d ctxt =
@@ -140,8 +141,8 @@ let push_named_context_val d ctxt =
let match_named_context_val c = match c.env_named_ctx with
| [] -> None
| decl :: ctx ->
- let (_, v) = Id.Map.find (get_id decl) c.env_named_map in
- let map = Id.Map.remove (get_id decl) c.env_named_map in
+ let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in
+ let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
let cval = { env_named_ctx = ctx; env_named_map = map } in
Some (decl, v, cval)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index bc1cb63d82..e4b3fcbf1a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -62,6 +62,8 @@ open Names
open Declarations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
(** {6 Safe environments }
Fields of [safe_environment] :
@@ -361,7 +363,7 @@ let check_required current_libs needed =
cost too much. *)
let safe_push_named d env =
- let id = get_id d in
+ let id = NamedDecl.get_id d in
let _ =
try
let _ = Environ.lookup_named id env in
@@ -795,7 +797,7 @@ type native_library = Nativecode.global list
let get_library_native_symbols senv dir =
try DPMap.find dir senv.native_symbols
- with Not_found -> CErrors.errorlabstrm "get_library_native_symbols"
+ with Not_found -> CErrors.user_err ~hdr:"get_library_native_symbols"
Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++
(str "This use case is not supported, but disabling the native compiler may help."))
@@ -819,7 +821,7 @@ let export ?except senv dir =
try join_safe_environment ?except senv
with e ->
let e = CErrors.push e in
- CErrors.errorlabstrm "export" (CErrors.iprint e)
+ CErrors.user_err ~hdr:"export" (CErrors.iprint e)
in
assert(senv.future_cst = []);
let () = check_current_library dir senv in
@@ -855,7 +857,7 @@ let import lib cst vodigest senv =
check_required senv.required lib.comp_deps;
check_engagement senv.env lib.comp_enga;
if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then
- CErrors.errorlabstrm "Safe_typing.import"
+ CErrors.user_err ~hdr:"Safe_typing.import"
(Pp.strbrk "Cannot load a library with the same name as the current one.");
let mp = MPfile lib.comp_name in
let mb = lib.comp_mod in
diff --git a/kernel/term.ml b/kernel/term.ml
index 15f187e5c4..62c161be4c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -328,38 +328,9 @@ let destCoFix c = match kind_of_term c with
let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false
(******************************************************************)
-(* Cast management *)
-(******************************************************************)
-
-let rec strip_outer_cast c = match kind_of_term c with
- | Cast (c,_,_) -> strip_outer_cast c
- | _ -> c
-
-(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *)
-
-let under_outer_cast f c = match kind_of_term c with
- | Cast (b,k,t) -> mkCast (f b, k, f t)
- | _ -> f c
-
-let rec under_casts f c = match kind_of_term c with
- | Cast (c,k,t) -> mkCast (under_casts f c, k, t)
- | _ -> f c
-
-(******************************************************************)
(* Flattening and unflattening of embedded applications and casts *)
(******************************************************************)
-(* flattens application lists throwing casts in-between *)
-let collapse_appl c = match kind_of_term c with
- | App (f,cl) ->
- let rec collapse_rec f cl2 =
- match kind_of_term (strip_outer_cast f) with
- | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
- | _ -> mkApp (f,cl2)
- in
- collapse_rec f cl
- | _ -> c
-
let decompose_app c =
match kind_of_term c with
| App (f,cl) -> (f, Array.to_list cl)
@@ -465,7 +436,7 @@ let rec to_lambda n prod =
match kind_of_term prod with
| Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
| Cast (c,_,_) -> to_lambda n c
- | _ -> errorlabstrm "to_lambda" (mt ())
+ | _ -> user_err ~hdr:"to_lambda" (mt ())
let rec to_prod n lam =
if Int.equal n 0 then
@@ -474,7 +445,7 @@ let rec to_prod n lam =
match kind_of_term lam with
| Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
| Cast (c,_,_) -> to_prod n c
- | _ -> errorlabstrm "to_prod" (mt ())
+ | _ -> user_err ~hdr:"to_prod" (mt ())
let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c)
let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
diff --git a/kernel/term.mli b/kernel/term.mli
index 60a3c77154..a8d9dfbfff 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr
val strip_prod_assum : types -> types
val strip_lam_assum : constr -> constr
-(** Flattens application lists *)
-val collapse_appl : constr -> constr
-
-
-(** Remove recursively the casts around a term i.e.
- [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : constr -> constr
-
-(** Apply a function letting Casted types in place *)
-val under_casts : (constr -> constr) -> constr -> constr
-
-(** Apply a function under components of Cast if any *)
-val under_outer_cast : (constr -> constr) -> constr -> constr
-
(** {5 ... } *)
(** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
Such a term can canonically be seen as the pair of a context of types
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 749b5dbafa..d8774944e4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,6 +22,9 @@ open Entries
open Typeops
open Fast_typeops
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
let constrain_type env j poly subst = function
| `None ->
if not poly then (* Old-style polymorphism *)
@@ -249,18 +252,17 @@ let global_vars_set_constant_type env = function
| RegularArity t -> global_vars_set env t
| TemplateArity (ctx,_) ->
Context.Rel.fold_outside
- (Context.Rel.Declaration.fold
+ (RelDecl.fold_constr
(fun t c -> Id.Set.union (global_vars_set env t) c))
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 decl ->
- let id = get_id decl in
- if List.exists (Id.equal id % get_id) in_ty then None
+ let id = NamedDecl.get_id decl in
+ if List.exists (NamedDecl.get_id %> Id.equal 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)
@@ -269,26 +271,25 @@ 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 get_id l) Id.Set.empty in
+ let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.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
let n = List.length l in
- errorlabstrm "" (Pp.(str "The following section " ++
+ user_err (Pp.(str "The following section " ++
str (String.plural n "variable") ++
str " " ++ str (String.conjugate_verb_to_be n) ++
str " used but not declared:" ++
fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
let sort evn l =
List.filter (fun decl ->
- let id = get_id decl in
- List.exists (Names.Id.equal id % get_id) l)
+ let id = NamedDecl.get_id decl in
+ List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
(named_context env) in
(* We try to postpone the computation of used section variables *)
let hyps, def =
- let context_ids = List.map get_id (named_context env) in
+ let context_ids = List.map NamedDecl.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:
@@ -482,8 +483,7 @@ let translate_local_def mb env id centry =
| Undef _ -> ()
| Def _ -> ()
| OpaqueDef lc ->
- let open Context.Named.Declaration in
- let context_ids = List.map get_id (named_context env) in
+ let context_ids = List.map NamedDecl.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 0059111c09..24018ab31a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -20,6 +20,9 @@ open Inductive
open Type_errors
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
let conv_leq_vecti env v1 v2 =
@@ -79,7 +82,7 @@ let judge_of_type u =
let judge_of_relative env n =
try
- let typ = get_type (lookup_rel n env) in
+ let typ = RelDecl.get_type (lookup_rel n env) in
{ uj_val = mkRel n;
uj_type = lift n typ }
with Not_found ->
@@ -102,7 +105,7 @@ let check_hyps_inclusion env c sign =
Context.Named.fold_outside
(fun d1 () ->
let open Context.Named.Declaration in
- let id = get_id d1 in
+ let id = NamedDecl.get_id d1 in
try
let d2 = lookup_named id env in
conv env (get_type d2) (get_type d1);
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 2112284ea6..81fd1427d0 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -127,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 -> Context.section_context -> unit
+val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 2ca749d505..4affb5f9fb 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -8,7 +8,8 @@
open Names
open Esubst
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
(*********************)
(* Occurring *)
@@ -160,14 +161,15 @@ 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_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
+let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r
+let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r
+let subst1_decl lam r = RelDecl.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 =
+ let open RelDecl in
match sign, l with
| LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args'
| LocalDef (_,c,_)::sign', args' ->
@@ -179,6 +181,15 @@ let subst_of_rel_context_instance sign l =
let adjust_subst_to_rel_context sign l =
List.rev (subst_of_rel_context_instance sign l)
+let adjust_rel_to_rel_context sign n =
+ let rec aux sign =
+ let open RelDecl in
+ match sign with
+ | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p)
+ | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p)
+ | [] -> (0,n)
+ in snd (aux sign)
+
(* (thin_val sigma) removes identity substitutions from sigma *)
let rec thin_val = function
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 574d50eccb..f7535e6d8f 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl
(** For compatibility: returns the substitution reversed *)
val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list
+(** Take an index in an instance of a context and returns its index wrt to
+ the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
+val adjust_rel_to_rel_context : Context.Rel.t -> int -> int
+
(** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an]
for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:51:20 +0000