aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c11
-rw-r--r--kernel/byterun/coq_float64.c (renamed from kernel/byterun/coq_float64.h)52
-rw-r--r--kernel/byterun/coq_interp.c139
-rw-r--r--kernel/byterun/coq_memory.c3
-rw-r--r--kernel/byterun/coq_values.h3
-rw-r--r--kernel/byterun/dune2
-rw-r--r--kernel/context.ml9
-rw-r--r--kernel/context.mli3
-rw-r--r--kernel/entries.ml9
-rw-r--r--kernel/genOpcodeFiles.ml18
-rw-r--r--kernel/indTyping.ml11
-rw-r--r--kernel/inferCumulativity.ml109
-rw-r--r--kernel/inferCumulativity.mli4
-rw-r--r--kernel/type_errors.ml5
-rw-r--r--kernel/type_errors.mli3
-rw-r--r--kernel/vmbytecodes.ml13
-rw-r--r--kernel/vmbytecodes.mli5
-rw-r--r--kernel/vmbytegen.ml37
-rw-r--r--kernel/vmemitcodes.ml45
-rw-r--r--kernel/vmlambda.ml55
-rw-r--r--kernel/vmlambda.mli4
-rw-r--r--kernel/vmvalues.ml21
22 files changed, 285 insertions, 276 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 9118410549..1ba6a8c8fe 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -43,9 +43,7 @@ void init_arity () {
arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
- arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
- arity[LTFLOAT]=arity[LEFLOAT]=
- arity[ISINT]=arity[AREINT2]=0;
+ 0;
/* instruction with one operand */
arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
@@ -75,9 +73,10 @@ void init_arity () {
arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1;
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
- arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]=
- arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]=
- arity[PROJ]=2;
+ arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]=
+ arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]=
+ arity[PROJ]=
+ 2;
/* instruction with four operands */
arity[MAKESWITCHBLOCK]=4;
/* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.c
index 84a3edf1c7..bea47dd47e 100644
--- a/kernel/byterun/coq_float64.h
+++ b/kernel/byterun/coq_float64.c
@@ -8,19 +8,40 @@
/* * (see LICENSE file for the text of the license) */
/************************************************************************/
-#ifndef _COQ_FLOAT64_
-#define _COQ_FLOAT64_
-
#include <math.h>
+#include <stdint.h>
-#define DECLARE_FREL(name, e) \
- int coq_##name(double x, double y) { \
- return e; \
- } \
- \
- value coq_##name##_byte(value x, value y) { \
- return coq_##name(Double_val(x), Double_val(y)); \
- }
+#define CAML_INTERNALS
+#include <caml/alloc.h>
+
+#include "coq_values.h"
+
+union double_bits {
+ double d;
+ uint64_t u;
+};
+
+static double next_up(double x) {
+ union double_bits bits;
+ if (!(x < INFINITY)) return x; // x is +oo or NaN
+ bits.d = x;
+ int64_t i = bits.u;
+ if (i >= 0) ++bits.u; // x >= +0.0, go away from zero
+ else if (bits.u + bits.u == 0) bits.u = 1; // x is -0.0, should almost never happen
+ else --bits.u; // x < 0.0, go toward zero
+ return bits.d;
+}
+
+static double next_down(double x) {
+ union double_bits bits;
+ if (!(x > -INFINITY)) return x; // x is -oo or NaN
+ bits.d = x;
+ int64_t i = bits.u;
+ if (i == 0) bits.u = INT64_MIN + 1; // x is +0.0
+ else if (i < 0) ++bits.u; // x <= -0.0, go away from zero
+ else --bits.u; // x > 0.0, go toward zero
+ return bits.d;
+}
#define DECLARE_FBINOP(name, e) \
double coq_##name(double x, double y) { \
@@ -40,19 +61,14 @@
return caml_copy_double(coq_##name(Double_val(x))); \
}
-DECLARE_FREL(feq, x == y)
-DECLARE_FREL(flt, x < y)
-DECLARE_FREL(fle, x <= y)
DECLARE_FBINOP(fmul, x * y)
DECLARE_FBINOP(fadd, x + y)
DECLARE_FBINOP(fsub, x - y)
DECLARE_FBINOP(fdiv, x / y)
DECLARE_FUNOP(fsqrt, sqrt(x))
-DECLARE_FUNOP(next_up, nextafter(x, INFINITY))
-DECLARE_FUNOP(next_down, nextafter(x, -INFINITY))
+DECLARE_FUNOP(next_up, next_up(x))
+DECLARE_FUNOP(next_down, next_down(x))
value coq_is_double(value x) {
return Val_long(Is_double(x));
}
-
-#endif /* _COQ_FLOAT64_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 1b6da7dd6f..8990743de2 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -28,7 +28,6 @@
#include "coq_fix_code.h"
#include "coq_memory.h"
#include "coq_values.h"
-#include "coq_float64.h"
#if OCAML_VERSION < 41000
extern void caml_minor_collection(void);
@@ -113,7 +112,7 @@ if (sp - num_args < coq_stack_threshold) { \
#define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
#define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
#define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; }
-#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; }
+#define Restore_after_caml_call coq_env = *sp++;
/* Register optimization.
Some compilers underestimate the use of the local variables representing
@@ -193,7 +192,9 @@ if (sp - num_args < coq_stack_threshold) { \
#endif
#endif
-#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate)
+/* We should also check "Code_val(v) == accumulate" to be sure,
+ but Is_accu is only used in places where closures cannot occur. */
+#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag)
#define CheckPrimArgs(cond, apply_lbl) do{ \
if (cond) pc++; \
@@ -237,6 +238,9 @@ extern intnat volatile caml_pending_signals[];
extern void caml_process_pending_signals(void);
#endif
+extern double coq_next_up(double);
+extern double coq_next_down(double);
+
/* The interpreter itself */
value coq_interprete
@@ -1271,11 +1275,8 @@ value coq_interprete
Instruct(CHECKADDINT63){
print_instr("CHECKADDINT63");
CheckInt2();
- }
- Instruct(ADDINT63) {
/* Adds the integer in the accumulator with
the one ontop of the stack (which is poped)*/
- print_instr("ADDINT63");
Uint63_add(accu, *sp++);
Next;
}
@@ -1309,9 +1310,6 @@ value coq_interprete
Instruct (CHECKSUBINT63) {
print_instr("CHECKSUBINT63");
CheckInt2();
- }
- Instruct (SUBINT63) {
- print_instr("SUBINT63");
/* returns the subtraction */
Uint63_sub(accu, *sp++);
Next;
@@ -1517,9 +1515,6 @@ value coq_interprete
Instruct (CHECKLTINT63) {
print_instr("CHECKLTINT63");
CheckInt2();
- }
- Instruct (LTINT63) {
- print_instr("LTINT63");
int b;
Uint63_lt(b,accu,*sp++);
accu = b ? coq_true : coq_false;
@@ -1529,9 +1524,6 @@ value coq_interprete
Instruct (CHECKLEINT63) {
print_instr("CHECKLEINT63");
CheckInt2();
- }
- Instruct (LEINT63) {
- print_instr("LEINT63");
int b;
Uint63_leq(b,accu,*sp++);
accu = b ? coq_true : coq_false;
@@ -1570,20 +1562,6 @@ value coq_interprete
Next;
}
- Instruct (ISINT){
- print_instr("ISINT");
- accu = (Is_uint63(accu)) ? coq_true : coq_false;
- Next;
- }
-
- Instruct (AREINT2){
- print_instr("AREINT2");
- accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
- sp++;
- Next;
- }
-
-
Instruct (CHECKOPPFLOAT) {
print_instr("CHECKOPPFLOAT");
CheckFloat1();
@@ -1601,27 +1579,21 @@ value coq_interprete
Instruct (CHECKEQFLOAT) {
print_instr("CHECKEQFLOAT");
CheckFloat2();
- accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ accu = Double_val(accu) == Double_val(*sp++) ? coq_true : coq_false;
Next;
}
Instruct (CHECKLTFLOAT) {
print_instr("CHECKLTFLOAT");
CheckFloat2();
- }
- Instruct (LTFLOAT) {
- print_instr("LTFLOAT");
- accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ accu = Double_val(accu) < Double_val(*sp++) ? coq_true : coq_false;
Next;
}
Instruct (CHECKLEFLOAT) {
print_instr("CHECKLEFLOAT");
CheckFloat2();
- }
- Instruct (LEFLOAT) {
- print_instr("LEFLOAT");
- accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ accu = Double_val(accu) <= Double_val(*sp++) ? coq_true : coq_false;
Next;
}
@@ -1674,35 +1646,35 @@ value coq_interprete
Instruct (CHECKADDFLOAT) {
print_instr("CHECKADDFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) + Double_val(*sp++));
Next;
}
Instruct (CHECKSUBFLOAT) {
print_instr("CHECKSUBFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) - Double_val(*sp++));
Next;
}
Instruct (CHECKMULFLOAT) {
print_instr("CHECKMULFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) * Double_val(*sp++));
Next;
}
Instruct (CHECKDIVFLOAT) {
print_instr("CHECKDIVFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) / Double_val(*sp++));
Next;
}
Instruct (CHECKSQRTFLOAT) {
print_instr("CHECKSQRTFLOAT");
CheckFloat1();
- Coq_copy_double(coq_fsqrt(Double_val(accu)));
+ Coq_copy_double(sqrt(Double_val(accu)));
Next;
}
@@ -1784,11 +1756,25 @@ value coq_interprete
Next;
}
+ Instruct (CHECKNEXTUPFLOATINPLACE) {
+ print_instr("CHECKNEXTUPFLOATINPLACE");
+ CheckFloat1();
+ Store_double_val(accu, coq_next_up(Double_val(accu)));
+ Next;
+ }
+
+ Instruct (CHECKNEXTDOWNFLOATINPLACE) {
+ print_instr("CHECKNEXTDOWNFLOATINPLACE");
+ CheckFloat1();
+ Store_double_val(accu, coq_next_down(Double_val(accu)));
+ Next;
+ }
- Instruct(ISINT_CAML_CALL2) {
+ Instruct(CHECKCAMLCALL2_1) {
+ // arity-2 callback, the last argument can be an accumulator
value arg;
- print_instr("ISINT_CAML_CALL2");
- if (Is_uint63(accu)) {
+ print_instr("CHECKCAMLCALL2_1");
+ if (!Is_accu(accu)) {
pc++;
print_int(*pc);
arg = sp[0];
@@ -1801,47 +1787,50 @@ value coq_interprete
Next;
}
- Instruct(ISARRAY_CAML_CALL1) {
- print_instr("ISARRAY_CAML_CALL1");
- if (Is_coq_array(accu)) {
- pc++;
- Setup_for_caml_call;
- print_int(*pc);
- accu = caml_callback(Field(coq_global_data, *pc),accu);
- Restore_after_caml_call;
- pc++;
- }
- else pc += *pc;
- Next;
+ Instruct(CHECKCAMLCALL1) {
+ // arity-1 callback, no argument can be an accumulator
+ print_instr("CHECKCAMLCALL1");
+ if (!Is_accu(accu)) {
+ pc++;
+ Setup_for_caml_call;
+ print_int(*pc);
+ accu = caml_callback(Field(coq_global_data, *pc), accu);
+ Restore_after_caml_call;
+ pc++;
+ }
+ else pc += *pc;
+ Next;
}
- Instruct(ISARRAY_INT_CAML_CALL2) {
+ Instruct(CHECKCAMLCALL2) {
+ // arity-2 callback, no argument can be an accumulator
value arg;
- print_instr("ISARRAY_INT_CAML_CALL2");
- if (Is_coq_array(accu) && Is_uint63(sp[0])) {
- pc++;
- arg = sp[0];
- Setup_for_caml_call;
- print_int(*pc);
- accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
- Restore_after_caml_call;
- sp += 1;
- pc++;
- } else pc += *pc;
- Next;
+ print_instr("CHECKCAMLCALL2");
+ if (!Is_accu(accu) && !Is_accu(sp[0])) {
+ pc++;
+ arg = sp[0];
+ Setup_for_caml_call;
+ print_int(*pc);
+ accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
+ Restore_after_caml_call;
+ sp += 1;
+ pc++;
+ } else pc += *pc;
+ Next;
}
- Instruct(ISARRAY_INT_CAML_CALL3) {
+ Instruct(CHECKCAMLCALL3_1) {
+ // arity-3 callback, the last argument can be an accumulator
value arg1;
value arg2;
- print_instr("ISARRAY_INT_CAML_CALL3");
- if (Is_coq_array(accu) && Is_uint63(sp[0])) {
+ print_instr("CHECKCAMLCALL3_1");
+ if (!Is_accu(accu) && !Is_accu(sp[0])) {
pc++;
arg1 = sp[0];
arg2 = sp[1];
Setup_for_caml_call;
print_int(*pc);
- accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2);
+ accu = caml_callback3(Field(coq_global_data, *pc), accu, arg1, arg2);
Restore_after_caml_call;
sp += 2;
pc++;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index ae5251c252..fe076f8f04 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -65,9 +65,10 @@ static void coq_scan_roots(scanning_action action)
register value * i;
/* Scan the stack */
for (i = coq_sp; i < coq_stack_high; i++) {
+ if (!Is_block(*i)) continue;
#ifdef NO_NAKED_POINTERS
/* The VM stack may contain C-allocated bytecode */
- if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue;
+ if (!Is_in_heap_or_young(*i)) continue;
#endif
(*action) (*i, i);
};
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index f07018711b..0cdef34050 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -30,9 +30,6 @@
#define Is_double(v) (Tag_val(v) == Double_tag)
#define Is_tailrec_switch(v) (Field(v,1) == Val_true)
-/* coq array */
-#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1))
-
/* coq values for primitive operations */
#define coq_tag_C1 2
#define coq_tag_C0 1
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 2998178be2..d3e2a2fa7f 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -4,7 +4,7 @@
(public_name coq.vm)
(foreign_stubs
(language c)
- (names coq_fix_code coq_memory coq_values coq_interp)
+ (names coq_fix_code coq_float64 coq_memory coq_values coq_interp)
(flags (:include %{project_root}/config/dune.c_flags))))
(rule
diff --git a/kernel/context.ml b/kernel/context.ml
index 6a99f201f3..ab66898b59 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -365,6 +365,15 @@ struct
let ty' = f ty in
if v == v' && ty == ty' then decl else LocalDef (id, v', ty')
+ let map_constr_het f = function
+ | LocalAssum (id, ty) ->
+ let ty' = f ty in
+ LocalAssum (id, ty')
+ | LocalDef (id, v, ty) ->
+ let v' = f v in
+ let ty' = f ty in
+ LocalDef (id, v', ty')
+
(** Perform a given action on all terms in a given declaration. *)
let iter_constr f = function
| LocalAssum (_, ty) -> f ty
diff --git a/kernel/context.mli b/kernel/context.mli
index 76c4461760..29309daf34 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -231,6 +231,9 @@ sig
(** Map all terms in a given declaration. *)
val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
+ (** Map all terms, with an heterogeneous function. *)
+ val map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) pt
+
(** Perform a given action on all terms in a given declaration. *)
val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit
diff --git a/kernel/entries.ml b/kernel/entries.ml
index ae64112e33..1bfc740017 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -20,6 +20,8 @@ type universes_entry =
| Monomorphic_entry of Univ.ContextSet.t
| Polymorphic_entry of Name.t array * Univ.UContext.t
+type variance_entry = Univ.Variance.t option array
+
type 'a in_universes_entry = 'a * universes_entry
(** {6 Declaration of inductive types. } *)
@@ -50,9 +52,10 @@ type mutual_inductive_entry = {
mind_entry_inds : one_inductive_entry list;
mind_entry_universes : universes_entry;
mind_entry_template : bool; (* Use template polymorphism *)
- mind_entry_cumulative : bool;
- (* universe constraints and the constraints for subtyping of
- inductive types in the block. *)
+ mind_entry_variance : variance_entry option;
+ (* [None] if non-cumulative, otherwise associates each universe of
+ the entry to [None] if to be inferred or [Some v] if to be
+ checked. *)
mind_entry_private : bool option;
}
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index f052e03cde..dc2cd349ce 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -104,11 +104,9 @@ let opcodes =
"MAKEPROD";
"BRANCH";
"CHECKADDINT63";
- "ADDINT63";
"CHECKADDCINT63";
"CHECKADDCARRYCINT63";
"CHECKSUBINT63";
- "SUBINT63";
"CHECKSUBCINT63";
"CHECKSUBCARRYCINT63";
"CHECKMULINT63";
@@ -127,21 +125,15 @@ let opcodes =
"CHECKLSRINT63CONST1";
"CHECKEQINT63";
"CHECKLTINT63";
- "LTINT63";
"CHECKLEINT63";
- "LEINT63";
"CHECKCOMPAREINT63";
"CHECKHEAD0INT63";
"CHECKTAIL0INT63";
- "ISINT";
- "AREINT2";
"CHECKOPPFLOAT";
"CHECKABSFLOAT";
"CHECKEQFLOAT";
"CHECKLTFLOAT";
- "LTFLOAT";
"CHECKLEFLOAT";
- "LEFLOAT";
"CHECKCOMPAREFLOAT";
"CHECKCLASSIFYFLOAT";
"CHECKADDFLOAT";
@@ -155,10 +147,12 @@ let opcodes =
"CHECKLDSHIFTEXP";
"CHECKNEXTUPFLOAT";
"CHECKNEXTDOWNFLOAT";
- "ISINT_CAML_CALL2";
- "ISARRAY_CAML_CALL1";
- "ISARRAY_INT_CAML_CALL2";
- "ISARRAY_INT_CAML_CALL3";
+ "CHECKNEXTUPFLOATINPLACE";
+ "CHECKNEXTDOWNFLOATINPLACE";
+ "CHECKCAMLCALL2_1";
+ "CHECKCAMLCALL1";
+ "CHECKCAMLCALL2";
+ "CHECKCAMLCALL3_1";
"STOP"
|]
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index b2520b780f..33ee8c325a 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -369,15 +369,20 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
data, Some None
in
- let variance = if not mie.mind_entry_cumulative then None
- else match mie.mind_entry_universes with
+ let variance = match mie.mind_entry_variance with
+ | None -> None
+ | Some variances ->
+ match mie.mind_entry_universes with
| Monomorphic_entry _ ->
CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.")
| Polymorphic_entry (_,uctx) ->
let univs = Instance.to_array @@ UContext.instance uctx in
+ let univs = Array.map2 (fun a b -> a,b) univs variances in
let univs = match sec_univs with
| None -> univs
- | Some sec_univs -> Array.append sec_univs univs
+ | Some sec_univs ->
+ let sec_univs = Array.map (fun u -> u, None) sec_univs in
+ Array.append sec_univs univs
in
let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in
Some variances
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 8191a5b0f3..d02f92ef26 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -15,30 +15,82 @@ open Univ
open Variance
open Util
-type inferred = IrrelevantI | CovariantI
-
-(** Throughout this module we modify a map [variances] from local
- universes to [inferred]. It starts as a trivial mapping to
- [Irrelevant] and every time we encounter a local universe we
- restrict it accordingly.
- [Invariant] universes are removed from the map.
-*)
exception TrivialVariance
-let maybe_trivial variances =
- if LMap.is_empty variances then raise TrivialVariance
- else variances
+(** Not the same as Type_errors.BadVariance because we don't have the env where we raise. *)
+exception BadVariance of Level.t * Variance.t * Variance.t
+(* some ocaml bug is triggered if we make this an inline record *)
-let infer_level_eq u variances =
- maybe_trivial (LMap.remove u variances)
+module Inf : sig
+ type variances
+ val infer_level_eq : Level.t -> variances -> variances
+ val infer_level_leq : Level.t -> variances -> variances
+ val start : (Level.t * Variance.t option) array -> variances
+ val finish : variances -> Variance.t array
+end = struct
+ type inferred = IrrelevantI | CovariantI
+ type mode = Check | Infer
-let infer_level_leq u variances =
- (* can only set Irrelevant -> Covariant so nontrivial *)
- LMap.update u (function
- | None -> None
- | Some CovariantI as x -> x
- | Some IrrelevantI -> Some CovariantI)
- variances
+ (**
+ Each local universe is either in the [univs] map or is Invariant.
+
+ If [univs] is empty all universes are Invariant and there is nothing more to do,
+ so we stop by raising [TrivialVariance]. The [soft] check comes before that.
+ *)
+ type variances = {
+ orig_array : (Level.t * Variance.t option) array;
+ univs : (mode * inferred) LMap.t;
+ }
+
+ let to_variance = function
+ | IrrelevantI -> Irrelevant
+ | CovariantI -> Covariant
+
+ let to_variance_opt o = Option.cata to_variance Invariant o
+
+ let infer_level_eq u variances =
+ match LMap.find_opt u variances.univs with
+ | None -> variances
+ | Some (Check, expected) ->
+ let expected = to_variance expected in
+ raise (BadVariance (u, expected, Invariant))
+ | Some (Infer, _) ->
+ let univs = LMap.remove u variances.univs in
+ if LMap.is_empty univs then raise TrivialVariance;
+ {variances with univs}
+
+ let infer_level_leq u variances =
+ (* can only set Irrelevant -> Covariant so no TrivialVariance *)
+ let univs =
+ LMap.update u (function
+ | None -> None
+ | Some (_,CovariantI) as x -> x
+ | Some (Infer,IrrelevantI) -> Some (Infer,CovariantI)
+ | Some (Check,IrrelevantI) ->
+ raise (BadVariance (u, Irrelevant, Covariant)))
+ variances.univs
+ in
+ if univs == variances.univs then variances else {variances with univs}
+
+ let start us =
+ let univs = Array.fold_left (fun univs (u,variance) ->
+ match variance with
+ | None -> LMap.add u (Infer,IrrelevantI) univs
+ | Some Invariant -> univs
+ | Some Covariant -> LMap.add u (Check,CovariantI) univs
+ | Some Irrelevant -> LMap.add u (Check,IrrelevantI) univs)
+ LMap.empty us
+ in
+ if LMap.is_empty univs then raise TrivialVariance;
+ {univs; orig_array=us}
+
+ let finish variances =
+ Array.map
+ (fun (u,_check) -> to_variance_opt (Option.map snd (LMap.find_opt u variances.univs)))
+ variances.orig_array
+
+end
+open Inf
let infer_generic_instance_eq variances u =
Array.fold_left (fun variances u -> infer_level_eq u variances)
@@ -204,11 +256,7 @@ let infer_arity_constructor is_arity env variances arcn =
open Entries
let infer_inductive_core env univs entries =
- if Array.is_empty univs then raise TrivialVariance;
- let variances =
- Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
- LMap.empty univs
- in
+ let variances = Inf.start univs in
let variances = List.fold_left (fun variances entry ->
let variances = infer_arity_constructor true
env variances entry.mind_entry_arity
@@ -218,12 +266,11 @@ let infer_inductive_core env univs entries =
variances
entries
in
- Array.map (fun u -> match LMap.find u variances with
- | exception Not_found -> Invariant
- | IrrelevantI -> Irrelevant
- | CovariantI -> Covariant)
- univs
+ Inf.finish variances
let infer_inductive ~env_params univs entries =
try infer_inductive_core env_params univs entries
- with TrivialVariance -> Array.make (Array.length univs) Invariant
+ with
+ | TrivialVariance -> Array.make (Array.length univs) Invariant
+ | BadVariance (lev, expected, actual) ->
+ Type_errors.error_bad_variance env_params ~lev ~expected ~actual
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index db5539a0ff..99d8f0c98d 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -12,8 +12,8 @@ val infer_inductive
: env_params:Environ.env
(** Environment containing the polymorphic universes and the
parameters. *)
- -> Univ.Level.t array
- (** Universes whose cumulativity we want to infer. *)
+ -> (Univ.Level.t * Univ.Variance.t option) array
+ (** Universes whose cumulativity we want to infer or check. *)
-> Entries.one_inductive_entry list
(** The inductive block data we want to infer cumulativity for.
NB: we ignore the template bool and the names, only the terms
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index ae5c4b6880..bcb7aa88ca 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -69,6 +69,7 @@ type ('constr, 'types) ptype_error =
| DisallowedSProp
| BadRelevance
| BadInvert
+ | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
type type_error = (constr, types) ptype_error
@@ -163,6 +164,9 @@ let error_bad_relevance env =
let error_bad_invert env =
raise (TypeError (env, BadInvert))
+let error_bad_variance env ~lev ~expected ~actual =
+ raise (TypeError (env, BadVariance {lev;expected;actual}))
+
let map_pguard_error f = function
| NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
@@ -207,3 +211,4 @@ let map_ptype_error f = function
| DisallowedSProp -> DisallowedSProp
| BadRelevance -> BadRelevance
| BadInvert -> BadInvert
+| BadVariance u -> BadVariance u
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index b1f7eb8a34..bcdcab9db7 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -70,6 +70,7 @@ type ('constr, 'types) ptype_error =
| DisallowedSProp
| BadRelevance
| BadInvert
+ | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t }
type type_error = (constr, types) ptype_error
@@ -146,5 +147,7 @@ val error_bad_relevance : env -> 'a
val error_bad_invert : env -> 'a
+val error_bad_variance : env -> lev:Level.t -> expected:Variance.t -> actual:Variance.t -> 'a
+
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index c156a21c86..4977aec00a 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -56,13 +56,12 @@ type instruction =
| Kfield of int
| Ksetfield of int
| Kstop
- | Ksequence of bytecodes * bytecodes
+ | Ksequence of bytecodes
| Kproj of Projection.Repr.t
| Kensurestackcapacity of int
| Kbranch of Label.t (* jump to label *)
- | Kprim of CPrimitives.t * pconstant option
+ | Kprim of CPrimitives.t * pconstant
| Kcamlprim of CPrimitives.t * Label.t
- | Kareint of int
and bytecodes = instruction list
@@ -146,21 +145,19 @@ let rec pp_instr i =
| Kensurestackcapacity size -> str "growstack " ++ int size
| Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++
- (match id with Some (id,_u) -> Constant.print id | None -> str "")
+ (Constant.print (fst id))
| Kcamlprim (op, lbl) ->
str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++
pp_lbl lbl
- | Kareint n -> str "areint " ++ int n
-
and pp_bytecodes c =
match c with
| [] -> str ""
| Klabel lbl :: c ->
str "L" ++ int lbl ++ str ":" ++ fnl () ++
pp_bytecodes c
- | Ksequence (l1, l2) :: c ->
- pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c
+ | Ksequence l :: c ->
+ pp_bytecodes l ++ pp_bytecodes c
| i :: c ->
pp_instr i ++ fnl () ++ pp_bytecodes c
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli
index b703058fb7..003a77ab78 100644
--- a/kernel/vmbytecodes.mli
+++ b/kernel/vmbytecodes.mli
@@ -54,14 +54,13 @@ type instruction =
| Kfield of int (** accu = accu[n] *)
| Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *)
| Kstop
- | Ksequence of bytecodes * bytecodes
+ | Ksequence of bytecodes
| Kproj of Projection.Repr.t
| Kensurestackcapacity of int
| Kbranch of Label.t (** jump to label, is it needed ? *)
- | Kprim of CPrimitives.t * pconstant option
+ | Kprim of CPrimitives.t * pconstant
| Kcamlprim of CPrimitives.t * Label.t
- | Kareint of int
and bytecodes = instruction list
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 16a0f42664..70c92fd8f0 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -315,12 +315,10 @@ let pos_evar evk r =
(* non-terminating instruction (branch, raise, return, appterm) *)
(* in front of it. *)
-let discard_dead_code cont = cont
-(*function
- [] -> []
+let rec discard_dead_code = function
+ | [] -> []
| (Klabel _ | Krestart ) :: _ as cont -> cont
| _ :: cont -> discard_dead_code cont
-*)
(* Return a label to the beginning of the given continuation. *)
(* If the sequence starts with a branch, use the target of that branch *)
@@ -581,7 +579,7 @@ let rec compile_lam env cenv lam sz cont =
let cont_fun =
ensure_stack_capacity (compile_lam env r_fun body arity) [Kreturn arity]
in
- fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
+ fun_code := Ksequence (add_grab arity lbl_fun cont_fun) :: !fun_code;
let fv = fv r_fun in
compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
@@ -604,7 +602,7 @@ let rec compile_lam env cenv lam sz cont =
in
let lbl,fcode = label_code fcode in
lbl_types.(i) <- lbl;
- fun_code := [Ksequence(fcode,!fun_code)]
+ fun_code := Ksequence fcode :: !fun_code
done;
(* Compiling bodies *)
for i = 0 to ndef - 1 do
@@ -617,7 +615,7 @@ let rec compile_lam env cenv lam sz cont =
let lbl = Label.create () in
lbl_bodies.(i) <- lbl;
let fcode = add_grabrec rec_args.(i) arity lbl cont1 in
- fun_code := [Ksequence(fcode,!fun_code)]
+ fun_code := Ksequence fcode :: !fun_code
done;
let fv = !rfv in
compile_fv cenv fv.fv_rev sz
@@ -637,7 +635,7 @@ let rec compile_lam env cenv lam sz cont =
in
let lbl,fcode = label_code fcode in
lbl_types.(i) <- lbl;
- fun_code := [Ksequence(fcode,!fun_code)]
+ fun_code := Ksequence fcode :: !fun_code
done;
(* Compiling bodies *)
for i = 0 to ndef - 1 do
@@ -652,25 +650,13 @@ let rec compile_lam env cenv lam sz cont =
in
let cont = ensure_stack_capacity comp arity in
lbl_bodies.(i) <- lbl;
- fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)];
+ fun_code := Ksequence (add_grab (arity+1) lbl cont) :: !fun_code;
done;
let fv = !rfv in
set_max_stack_size (sz + fv.size + ndef + 2);
compile_fv cenv fv.fv_rev sz
(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
- | Lif(t, bt, bf) ->
- let branch, cont = make_branch cont in
- let lbl_true = Label.create() in
- let lbl_false = Label.create() in
- compile_lam env cenv t sz
- (Kswitch([|lbl_true;lbl_false|],[||]) ::
- Klabel lbl_false ::
- compile_lam env cenv bf sz
- (branch ::
- Klabel lbl_true ::
- compile_lam env cenv bt sz cont))
-
| Lcase(ci,rtbl,t,a,branches) ->
let ind = ci.ci_ind in
let mib = lookup_mind (fst ind) env in
@@ -688,7 +674,7 @@ let rec compile_lam env cenv lam sz cont =
ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop]
in
let lbl_typ,fcode = label_code fcode in
- fun_code := [Ksequence(fcode,!fun_code)];
+ fun_code := Ksequence fcode :: !fun_code;
(* Compilation of the branches *)
let lbl_sw = Label.create () in
let sz_b,branch,is_tailcall =
@@ -700,6 +686,7 @@ let rec compile_lam env cenv lam sz cont =
| _ -> assert false
in
+ let cont = discard_dead_code cont in
let c = ref cont in
(* Perform the extra match if needed (too many block constructors) *)
if neblock <> 0 then begin
@@ -770,7 +757,7 @@ let rec compile_lam env cenv lam sz cont =
let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
comp_args (compile_lam env) cenv args sz cont
- | Lprim (Some (kn,u), op, args) when is_caml_prim op ->
+ | Lprim ((kn,u), op, args) when is_caml_prim op ->
let arity = CPrimitives.arity op in
let nparams = CPrimitives.nparams op in
let nargs = arity - nparams in
@@ -788,7 +775,7 @@ let rec compile_lam env cenv lam sz cont =
if Int.equal nparams 0 then cont
else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont)
in
- fun_code := [Ksequence(default, !fun_code)];
+ fun_code := Ksequence default :: !fun_code;
comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont)
| Lprim (kn, op, args) ->
@@ -878,7 +865,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
ensure_stack_capacity (compile_lam env r_fun body full_arity)
[Kreturn full_arity]
in
- fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
+ fun_code := Ksequence (add_grab full_arity lbl_fun cont_fun) :: !fun_code;
let fv = fv r_fun in
let init_code =
ensure_stack_capacity (compile_fv cenv fv.fv_rev 0)
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index babc57794b..c1d8fcb855 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -208,14 +208,6 @@ let slot_for_caml_prim env op =
(* Emission of one instruction *)
-let nocheck_prim_op = function
- | Int63add -> opADDINT63
- | Int63sub -> opSUBINT63
- | Int63lt -> opLTINT63
- | Int63le -> opLEINT63
- | _ -> assert false
-
-
let check_prim_op = function
| Int63head0 -> opCHECKHEAD0INT63
| Int63tail0 -> opCHECKTAIL0INT63
@@ -259,11 +251,20 @@ let check_prim_op = function
| Float64ldshiftexp -> opCHECKLDSHIFTEXP
| Float64next_up -> opCHECKNEXTUPFLOAT
| Float64next_down -> opCHECKNEXTDOWNFLOAT
- | Arraymake -> opISINT_CAML_CALL2
- | Arrayget -> opISARRAY_INT_CAML_CALL2
- | Arrayset -> opISARRAY_INT_CAML_CALL3
+ | Arraymake -> opCHECKCAMLCALL2_1
+ | Arrayget -> opCHECKCAMLCALL2
+ | Arrayset -> opCHECKCAMLCALL3_1
| Arraydefault | Arraycopy | Arraylength ->
- opISARRAY_CAML_CALL1
+ opCHECKCAMLCALL1
+
+let inplace_prim_op = function
+ | Float64next_up | Float64next_down -> true
+ | _ -> false
+
+let check_prim_op_inplace = function
+ | Float64next_up -> opCHECKNEXTUPFLOATINPLACE
+ | Float64next_down -> opCHECKNEXTDOWNFLOATINPLACE
+ | _ -> assert false
let emit_instr env = function
| Klabel lbl -> define_label env lbl
@@ -354,10 +355,7 @@ let emit_instr env = function
| Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
| Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
| Kbranch lbl -> out env opBRANCH; out_label env lbl
- | Kprim (op,None) ->
- out env (nocheck_prim_op op)
-
- | Kprim(op,Some (q,_u)) ->
+ | Kprim (op, (q,_u)) ->
out env (check_prim_op op);
slot_for_getglobal env q
@@ -366,13 +364,8 @@ let emit_instr env = function
out_label env lbl;
slot_for_caml_prim env op
- | Kareint 1 -> out env opISINT
- | Kareint 2 -> out env opAREINT2;
-
| Kstop -> out env opSTOP
- | Kareint _ -> assert false
-
(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
let rec emit env insns remaining = match insns with
@@ -406,8 +399,14 @@ let rec emit env insns remaining = match insns with
emit env c remaining
| Kpop n :: Kjump :: c ->
out env opRETURN; out_int env n; emit env c remaining
- | Ksequence(c1,c2)::c ->
- emit env c1 (c2::c::remaining)
+ | Ksequence c1 :: c ->
+ emit env c1 (c :: remaining)
+ | Kprim (op1, (q1, _)) :: Kprim (op2, (q2, _)) :: c when inplace_prim_op op2 ->
+ out env (check_prim_op op1);
+ slot_for_getglobal env q1;
+ out env (check_prim_op_inplace op2);
+ slot_for_getglobal env q2;
+ emit env c remaining
(* Default case *)
| instr :: c ->
emit_instr env instr; emit env c remaining
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 332a331a7a..9cca204e8c 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -19,10 +19,8 @@ type lambda =
| Llet of Name.t Context.binder_annot * lambda * lambda
| Lapp of lambda * lambda array
| Lconst of pconstant
- | Lprim of pconstant option * CPrimitives.t * lambda array
- (* No check if None *)
+ | Lprim of pconstant * CPrimitives.t * lambda array
| Lcase of case_info * reloc_table * lambda * lambda * lam_branches
- | Lif of lambda * lambda * lambda
| Lfix of (int array * int) * fix_decl
| Lcofix of int * fix_decl
| Lint of int
@@ -112,10 +110,6 @@ let rec pp_lam lam =
pp_names ids ++ str " => " ++ pp_lam c)
(Array.to_list branches.nonconstant_branches)))
++ cut() ++ str "end")
- | Lif (t, bt, bf) ->
- v 0 (str "(if " ++ pp_lam t ++
- cut () ++ str "then " ++ pp_lam bt ++
- cut() ++ str "else " ++ pp_lam bf ++ str ")")
| Lfix((t,i),(lna,tl,bl)) ->
let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in
hov 1
@@ -148,16 +142,11 @@ let rec pp_lam lam =
| Lval _ -> str "values"
| Lsort s -> pp_sort s
| Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
- | Lprim(Some (kn,_u),_op,args) ->
+ | Lprim ((kn,_u),_op,args) ->
hov 1
(str "(PRIM " ++ pr_con kn ++ spc() ++
prlist_with_sep spc pp_lam (Array.to_list args) ++
str")")
- | Lprim(None,op,args) ->
- hov 1
- (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++ spc() ++
- prlist_with_sep spc pp_lam (Array.to_list args) ++
- str")")
| Lproj(p,arg) ->
hov 1
(str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
@@ -237,11 +226,6 @@ let map_lam_with_binders g f n lam =
in
if t == t' && a == a' && branches == branches' then lam else
Lcase(ci,rtbl,t',a',branches')
- | Lif(t,bt,bf) ->
- let t' = f n t in
- let bt' = f n bt in
- let bf' = f n bf in
- if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf')
| Lfix(init,(ids,ltypes,lbodies)) ->
let ltypes' = Array.Smart.map (f n) ltypes in
let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
@@ -312,28 +296,6 @@ let can_subst lam =
| Lval _ | Lsort _ | Lind _ -> true
| _ -> false
-
-let can_merge_if bt bf =
- match bt, bf with
- | Llam(_idst,_), Llam(_idsf,_) -> true
- | _ -> false
-
-let merge_if t bt bf =
- let (idst,bodyt) = decompose_Llam bt in
- let (idsf,bodyf) = decompose_Llam bf in
- let nt = Array.length idst in
- let nf = Array.length idsf in
- let common,idst,idsf =
- if nt = nf then idst, [||], [||]
- else
- if nt < nf then idst,[||], Array.sub idsf nt (nf - nt)
- else idsf, Array.sub idst nf (nt - nf), [||] in
- Llam(common,
- Lif(lam_lift (Array.length common) t,
- mkLlam idst bodyt,
- mkLlam idsf bodyf))
-
-
let rec simplify subst lam =
match lam with
| Lrel(id,i) -> lam_subst_rel lam id i subst
@@ -352,14 +314,6 @@ let rec simplify subst lam =
| lam' -> lam'
end
- | Lif(t,bt,bf) ->
- let t' = simplify subst t in
- let bt' = simplify subst bt in
- let bf' = simplify subst bf in
- if can_merge_if bt' bf' then merge_if t' bt' bf'
- else
- if t == t' && bt == bt' && bf == bf' then lam
- else Lif(t',bt',bf')
| _ -> map_lam_with_binders liftn simplify subst lam
and simplify_app substf f substa args =
@@ -442,9 +396,6 @@ let rec occurrence k kind lam =
in
Array.iter on_b branches.nonconstant_branches;
!r
- | Lif (t, bt, bf) ->
- let kind = occurrence k kind t in
- kind && occurrence k kind bt && occurrence k kind bf
| Lfix(_,(ids,ltypes,lbodies))
| Lcofix(_,(ids,ltypes,lbodies)) ->
let kind = occurrence_args k kind ltypes in
@@ -566,7 +517,7 @@ let rec get_alias env kn =
(* Compilation of primitive *)
let prim kn p args =
- Lprim(Some kn, p, args)
+ Lprim (kn, p, args)
let expand_prim kn op arity =
(* primitives are always Relevant *)
diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli
index bd11c2667f..ad5f81638f 100644
--- a/kernel/vmlambda.mli
+++ b/kernel/vmlambda.mli
@@ -12,10 +12,8 @@ type lambda =
| Llet of Name.t Context.binder_annot * lambda * lambda
| Lapp of lambda * lambda array
| Lconst of pconstant
- | Lprim of pconstant option * CPrimitives.t * lambda array
- (* No check if None *)
+ | Lprim of pconstant * CPrimitives.t * lambda array
| Lcase of case_info * reloc_table * lambda * lambda * lam_branches
- | Lif of lambda * lambda * lambda
| Lfix of (int array * int) * fix_decl
| Lcofix of int * fix_decl
| Lint of int
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 7b4101b9d0..9944458d6b 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -381,7 +381,15 @@ let rec whd_accu a stk =
CErrors.anomaly
Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".")
-external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
+[@@@warning "-37"]
+type vm_closure_kind =
+ | VCfun (** closure, or fixpoint applied past the recursive argument *)
+ | VCfix (** unapplied fixpoint *)
+ | VCfix_partial (** partially applied fixpoint, but not sufficiently for recursion *)
+ | VCaccu (** accumulator *)
+[@@@warning "+37"]
+
+external kind_of_closure : Obj.t -> vm_closure_kind = "coq_kind_of_closure"
external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
external int_tcode : tcode -> int -> int = "coq_int_tcode"
external accumulate : unit -> tcode = "accumulate_code"
@@ -400,12 +408,11 @@ let whd_val (v: values) =
else if Int.equal tag Obj.closure_tag && is_accumulate (fun_code o) then
whd_accu o []
else if Int.equal tag Obj.closure_tag || Int.equal tag Obj.infix_tag then
- (match kind_of_closure o with
- | 0 -> Vfun(Obj.obj o)
- | 1 -> Vfix(Obj.obj o, None)
- | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o))
- | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
- | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
+ match kind_of_closure o with
+ | VCfun -> Vfun (Obj.obj o)
+ | VCfix -> Vfix (Obj.obj o, None)
+ | VCfix_partial -> Vfix (Obj.obj (Obj.field o 2), Some (Obj.obj o))
+ | VCaccu -> Vatom_stk (Aid (RelKey (int_tcode (fun_code o) 1)), [])
else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
else
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:14:33 +0000