aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/environ.ml68
-rw-r--r--kernel/environ.mli13
-rw-r--r--kernel/nativeconv.ml5
-rw-r--r--kernel/nativelib.ml1
-rw-r--r--kernel/reduction.ml81
-rw-r--r--kernel/safe_typing.ml14
-rw-r--r--kernel/safe_typing.mli5
-rw-r--r--kernel/typeops.ml3
-rw-r--r--kernel/typeops.mli3
-rw-r--r--kernel/vconv.ml2
12 files changed, 125 insertions, 74 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 61fcb4832a..c1b38b4156 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -66,6 +66,8 @@ type typing_flags = {
check_universes : bool; (** If [false] universe constraints are not checked *)
conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
share_reduction : bool; (** Use by-need reduction algorithm *)
+ enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
+ enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d995786d97..3ed599c538 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -22,6 +22,8 @@ let safe_flags oracle = {
check_universes = true;
conv_oracle = oracle;
share_reduction = true;
+ enable_VM = true;
+ enable_native_compiler = true;
}
(** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 3b7e3ae544..f61dd0c101 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -350,9 +350,6 @@ let map_universes f env =
{ env with env_stratification =
{ s with env_universes = f s.env_universes } }
-let set_universes env u =
- { env with env_stratification = { env.env_stratification with env_universes = u } }
-
let add_constraints c env =
if Univ.Constraint.is_empty c then env
else map_universes (UGraph.merge_constraints c) env
@@ -405,19 +402,12 @@ let add_constant_key kn cb linkinfo env =
let add_constant kn cb env =
add_constant_key kn cb no_link_info env
-let constraints_of cb u =
- match cb.const_universes with
- | Monomorphic_const _ -> Univ.Constraint.empty
- | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
-
(* constant_type gives the type of a constant *)
let constant_type env (kn,u) =
let cb = lookup_constant kn env in
- match cb.const_universes with
- | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
- | Polymorphic_const _ctx ->
- let csts = constraints_of cb u in
- (subst_instance_constr u cb.const_type, csts)
+ let uctx = Declareops.constant_polymorphic_context cb in
+ let csts = Univ.AUContext.instantiate u uctx in
+ (subst_instance_constr u cb.const_type, csts)
type const_evaluation_result = NoBody | Opaque
@@ -425,20 +415,24 @@ exception NotEvaluableConst of const_evaluation_result
let constant_value_and_type env (kn, u) =
let cb = lookup_constant kn env in
- if Declareops.constant_is_polymorphic cb then
- let cst = constraints_of cb u in
- let b' = match cb.const_body with
- | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
- | OpaqueDef _ -> None
- | Undef _ -> None
- in
- b', subst_instance_constr u cb.const_type, cst
- else
- let b' = match cb.const_body with
- | Def l_body -> Some (Mod_subst.force_constr l_body)
- | OpaqueDef _ -> None
- | Undef _ -> None
- in b', cb.const_type, Univ.Constraint.empty
+ let uctx = Declareops.constant_polymorphic_context cb in
+ let cst = Univ.AUContext.instantiate u uctx in
+ let b' = match cb.const_body with
+ | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
+ | OpaqueDef _ -> None
+ | Undef _ -> None
+ in
+ b', subst_instance_constr u cb.const_type, cst
+
+let body_of_constant_body env cb =
+ let otab = opaque_tables env in
+ match cb.const_body with
+ | Undef _ ->
+ None
+ | Def c ->
+ Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+ | OpaqueDef o ->
+ Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
(* These functions should be called under the invariant that [env]
already contains the constraints corresponding to the constant
@@ -447,9 +441,7 @@ let constant_value_and_type env (kn, u) =
(* constant_type gives the type of a constant *)
let constant_type_in env (kn,u) =
let cb = lookup_constant kn env in
- if Declareops.constant_is_polymorphic cb then
- subst_instance_constr u cb.const_type
- else cb.const_type
+ subst_instance_constr u cb.const_type
let constant_value_in env (kn,u) =
let cb = lookup_constant kn env in
@@ -694,6 +686,22 @@ let is_polymorphic env r =
| IndRef ind -> polymorphic_ind ind env
| ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env
+let is_template_polymorphic env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef _id -> false
+ | ConstRef _c -> false
+ | IndRef ind -> template_polymorphic_ind ind env
+ | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
+
+let is_type_in_type env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef _id -> false
+ | ConstRef c -> type_in_type_constant c env
+ | IndRef ind -> type_in_type_ind ind env
+ | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env
+
(*spiwack: the following functions assemble the pieces of the retroknowledge
note that the "consistent" register function is available in the module
Safetyping, Environ only synchronizes the proactive and the reactive parts*)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 43bfe7c2fb..c285f907fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -155,11 +155,6 @@ val named_body : variable -> env -> constr option
val fold_named_context :
(env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
-val set_universes : env -> UGraph.t -> env
-(** This is used to update universes during a proof for the sake of
- evar map-unaware functions, eg [Typing] calling
- [Typeops.check_hyps_inclusion]. *)
-
(** Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse :
('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
@@ -211,6 +206,12 @@ val constant_value_and_type : env -> Constant.t puniverses ->
polymorphic *)
val constant_context : env -> Constant.t -> Univ.AUContext.t
+(** Returns the body of the constant if it has any, and the polymorphic context
+ it lives in. For monomorphic constant, the latter is empty, and for
+ polymorphic constants, the term contains De Bruijn universe variables that
+ need to be instantiated. *)
+val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option
+
(* These functions should be called under the invariant that [env]
already contains the constraints corresponding to the constant
application. *)
@@ -320,6 +321,8 @@ val apply_to_hyp : named_context_val -> variable ->
val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
val is_polymorphic : env -> Names.GlobRef.t -> bool
+val is_template_polymorphic : env -> GlobRef.t -> bool
+val is_type_in_type : env -> GlobRef.t -> bool
open Retroknowledge
(** functions manipulating the retroknowledge
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 054b6a2d17..f5d7ab3c9d 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -14,7 +14,8 @@ open Nativelib
open Reduction
open Util
open Nativevalues
-open Nativecode
+open Nativecode
+open Environ
(** This module implements the conversion test by compiling to OCaml code *)
@@ -142,7 +143,7 @@ let warn_no_native_compiler =
strbrk " falling back to VM conversion test.")
let native_conv_gen pb sigma env univs t1 t2 =
- if not Coq_config.native_compiler then begin
+ if not (typing_flags env).Declarations.enable_native_compiler then begin
warn_no_native_compiler ();
Vconv.vm_conv_gen pb env univs t1 t2
end
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index d294f2060e..833e4082f0 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -66,7 +66,6 @@ let warn_native_compiler_failed =
CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
let call_compiler ?profile:(profile=false) ml_filename =
- let () = assert Coq_config.native_compiler in
let load_path = !get_load_paths () in
let load_path = List.map (fun dn -> dn / output_dir) load_path in
let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 18697d07e5..5515ff9767 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -68,7 +68,7 @@ type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
| Zlproj of Projection.Repr.t * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
- | Zlcase of case_info * lift * fconstr * fconstr array
+ | Zlcase of case_info * lift * constr * constr array * fconstr subs
and lft_constr_stack = lft_constr_stack_elt list
let rec zlapp v = function
@@ -102,7 +102,7 @@ let pure_stack lfts stk =
let (lfx,pa) = pure_rec l a in
(l, Zlfix((lfx,fx),pa)::pstk)
| (ZcaseT(ci,p,br,e),(l,pstk)) ->
- (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk))
+ (l,Zlcase(ci,l,p,br,e)::pstk))
in
snd (pure_rec lfts stk)
@@ -288,31 +288,13 @@ let conv_table_key infos k1 k2 cuniv =
| RelKey n, RelKey n' when Int.equal n n' -> cuniv
| _ -> raise NotConvertible
-let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
- let rec cmp_rec pstk1 pstk2 cuniv =
- match (pstk1,pstk2) with
- | (z1::s1, z2::s2) ->
- let cu1 = cmp_rec s1 s2 cuniv in
- (match (z1,z2) with
- | (Zlapp a1,Zlapp a2) ->
- Array.fold_right2 f a1 a2 cu1
- | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
- if not (Projection.Repr.equal c1 c2) then
- raise NotConvertible
- else cu1
- | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
- let cu2 = f fx1 fx2 cu1 in
- cmp_rec a1 a2 cu2
- | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
- if not (fmind ci1.ci_ind ci2.ci_ind) then
- raise NotConvertible;
- let cu2 = f (l1,p1) (l2,p2) cu1 in
- Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2
- | _ -> assert false)
- | _ -> cuniv in
- if compare_stack_shape stk1 stk2 then
- cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
- else raise NotConvertible
+exception IrregularPatternShape
+
+let rec skip_pattern n c =
+ if Int.equal n 0 then c
+ else match kind c with
+ | Lambda (_, _, c) -> skip_pattern (pred n) c
+ | _ -> raise IrregularPatternShape
type conv_tab = {
cnv_inf : clos_infos;
@@ -611,10 +593,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| FProd _ | FEvar _), _ -> raise NotConvertible
and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
- compare_stacks
- (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
- (eq_ind)
- lft1 stk1 lft2 stk2 cuniv
+ let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in
+ let rec cmp_rec pstk1 pstk2 cuniv =
+ match (pstk1,pstk2) with
+ | (z1::s1, z2::s2) ->
+ let cu1 = cmp_rec s1 s2 cuniv in
+ (match (z1,z2) with
+ | (Zlapp a1,Zlapp a2) ->
+ Array.fold_right2 f a1 a2 cu1
+ | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
+ if not (Projection.Repr.equal c1 c2) then
+ raise NotConvertible
+ else cu1
+ | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
+ let cu2 = f fx1 fx2 cu1 in
+ cmp_rec a1 a2 cu2
+ | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
+ if not (eq_ind ci1.ci_ind ci2.ci_ind) then
+ raise NotConvertible;
+ let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
+ convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
+ | _ -> assert false)
+ | _ -> cuniv in
+ if compare_stack_shape stk1 stk2 then
+ cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
+ else raise NotConvertible
and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let lv1 = Array.length v1 in
@@ -629,6 +632,22 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
fold 0 cuniv
else raise NotConvertible
+and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
+ (** Skip comparison of the pattern types. We know that the two terms are
+ living in a common type, thus this check is useless. *)
+ let fold n c1 c2 cuniv = match skip_pattern n c1, skip_pattern n c2 with
+ | (c1, c2) ->
+ let lft1 = el_liftn n lft1 in
+ let lft2 = el_liftn n lft2 in
+ let e1 = subs_liftn n e1 in
+ let e2 = subs_liftn n e2 in
+ ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+ | exception IrregularPatternShape ->
+ (** Might happen due to a shape invariant that is not enforced *)
+ ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+ in
+ Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
+
let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
let infos = create_clos_infos ~evars reds env in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12f9592ab7..4b64cc6d11 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,18 @@ let set_engagement c senv =
let set_typing_flags c senv =
{ senv with env = Environ.set_typing_flags c senv.env }
+let set_share_reduction b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with share_reduction = b } senv
+
+let set_VM b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with enable_VM = b } senv
+
+let set_native_compiler b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with enable_native_compiler = b } senv
+
(** Check that the engagement [c] expected by a library matches
the current (initial) one *)
let check_engagement env expected_impredicative_set =
@@ -1190,7 +1202,7 @@ loaded by side-effect once and for all (like it is done in OCaml).
Would this be correct with respect to undo's and stuff ?
*)
-let set_strategy e k l = { e with env =
+let set_strategy k l e = { e with env =
(Environ.set_oracle e.env
(Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 26fa91adbd..8fb33b04d4 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -137,6 +137,9 @@ val add_constraints :
(** Setting the type theory flavor *)
val set_engagement : Declarations.engagement -> safe_transformer0
val set_typing_flags : Declarations.typing_flags -> safe_transformer0
+val set_share_reduction : bool -> safe_transformer0
+val set_VM : bool -> safe_transformer0
+val set_native_compiler : bool -> safe_transformer0
(** {6 Interactive module functions } *)
@@ -217,4 +220,4 @@ val register :
val register_inline : Constant.t -> safe_transformer0
val set_strategy :
- safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment
+ Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1bb2d3c79c..c8fd83c8a9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -91,7 +91,8 @@ let type_of_variable env id =
(* Checks if a context of variables can be instantiated by the
variables of the current env.
Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env f c sign =
+let check_hyps_inclusion env ?evars f c sign =
+ let conv env a b = conv env ?evars a b in
Context.Named.fold_outside
(fun d1 () ->
let open Context.Named.Declaration in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d24002065b..4193324136 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -116,4 +116,5 @@ val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit
+val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+ ('a -> constr) -> 'a -> Constr.named_context -> unit
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 5965853e1e..c1130e62c9 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -189,7 +189,7 @@ let warn_bytecode_compiler_failed =
strbrk "falling back to standard conversion")
let vm_conv_gen cv_pb env univs t1 t2 =
- if not Coq_config.bytecode_compiler then
+ if not (typing_flags env).Declarations.enable_VM then
Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
full_transparent_state env univs t1 t2
else
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 07:51:30 +0000