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.c201
-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/cClosure.ml58
-rw-r--r--kernel/genOpcodeFiles.ml18
-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
15 files changed, 248 insertions, 280 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..6255250218 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
@@ -712,8 +716,8 @@ value coq_interprete
coq_extra_args = Long_val(sp[2]);
sp += 3;
} else {
- /* The recursif argument is an accumulator */
- mlsize_t num_args, i;
+ /* The recursive argument is an accumulator */
+ mlsize_t num_args, sz, i;
value block;
/* Construction of fixpoint applied to its [rec_pos-1] first arguments */
Alloc_small(accu, rec_pos + 3, Closure_tag);
@@ -728,11 +732,22 @@ value coq_interprete
accu = block;
/* Construction of the accumulator */
num_args = coq_extra_args - rec_pos;
- Alloc_small(block, 3 + num_args, Closure_tag);
+ sz = 3 + num_args;
+ if (sz <= Max_young_wosize) {
+ Alloc_small(block, sz, Closure_tag);
+ Field(block, 2) = accu;
+ for (i = 3; i < sz; ++i)
+ Field(block, i) = *sp++;
+ } else {
+ // too large for Alloc_small, so use caml_alloc_shr instead
+ // it never triggers a GC, so no need for Setup_for_gc
+ block = caml_alloc_shr(sz, Closure_tag);
+ caml_initialize(&Field(block, 2), accu);
+ for (i = 3; i < sz; ++i)
+ caml_initialize(&Field(block, i), *sp++);
+ }
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
- Field(block, 2) = accu;
- for (i = 0; i < num_args; i++) Field(block, i + 3) = *sp++;
accu = block;
pc = (code_t)(sp[0]);
coq_env = sp[1];
@@ -1126,13 +1141,25 @@ value coq_interprete
/* Special operations for reduction of open term */
Instruct(ACCUMULATE) {
- mlsize_t i, size;
+ mlsize_t i, size, sz;
print_instr("ACCUMULATE");
size = Wosize_val(coq_env);
- Alloc_small(accu, size + coq_extra_args + 1, Closure_tag);
- for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
- for(i = size; i <= coq_extra_args + size; i++)
- Field(accu, i) = *sp++;
+ sz = size + coq_extra_args + 1;
+ if (sz <= Max_young_wosize) {
+ Alloc_small(accu, sz, Closure_tag);
+ for (i = 0; i < size; ++i)
+ Field(accu, i) = Field(coq_env, i);
+ for (i = size; i < sz; ++i)
+ Field(accu, i) = *sp++;
+ } else {
+ // too large for Alloc_small, so use caml_alloc_shr instead
+ // it never triggers a GC, so no need for Setup_for_gc
+ accu = caml_alloc_shr(sz, Closure_tag);
+ for (i = 0; i < size; ++i)
+ caml_initialize(&Field(accu, i), Field(coq_env, i));
+ for (i = size; i < sz; ++i)
+ caml_initialize(&Field(accu, i), *sp++);
+ }
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -1236,13 +1263,24 @@ value coq_interprete
Instruct(MAKEACCU) {
- int i;
+ mlsize_t i, sz;
print_instr("MAKEACCU");
- Alloc_small(accu, coq_extra_args + 4, Closure_tag);
+ sz = coq_extra_args + 4;
+ if (sz <= Max_young_wosize) {
+ Alloc_small(accu, sz, Closure_tag);
+ Field(accu, 2) = Field(coq_atom_tbl, *pc);
+ for (i = 3; i < sz; ++i)
+ Field(accu, i) = *sp++;
+ } else {
+ // too large for Alloc_small, so use caml_alloc_shr instead
+ // it never triggers a GC, so no need for Setup_for_gc
+ accu = caml_alloc_shr(sz, Closure_tag);
+ caml_initialize(&Field(accu, 2), Field(coq_atom_tbl, *pc));
+ for (i = 3; i < sz; ++i)
+ caml_initialize(&Field(accu, i), *sp++);
+ }
Code_val(accu) = accumulate;
Field(accu, 1) = Val_int(2);
- Field(accu, 2) = Field(coq_atom_tbl, *pc);
- for (i = 2; i < coq_extra_args + 3; i++) Field(accu, i + 1) = *sp++;
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -1271,11 +1309,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 +1344,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 +1549,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 +1558,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 +1596,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 +1613,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 +1680,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 +1790,25 @@ value coq_interprete
Next;
}
+ Instruct (CHECKNEXTUPFLOATINPLACE) {
+ print_instr("CHECKNEXTUPFLOATINPLACE");
+ CheckFloat1();
+ Store_double_val(accu, coq_next_up(Double_val(accu)));
+ Next;
+ }
- Instruct(ISINT_CAML_CALL2) {
+ Instruct (CHECKNEXTDOWNFLOATINPLACE) {
+ print_instr("CHECKNEXTDOWNFLOATINPLACE");
+ CheckFloat1();
+ Store_double_val(accu, coq_next_down(Double_val(accu)));
+ Next;
+ }
+
+ 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 +1821,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/cClosure.ml b/kernel/cClosure.ml
index 17feeb9b5a..c9326615dc 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -263,7 +263,7 @@ let assoc_defined id env = match Environ.lookup_named id env with
* before the term is computed.
*)
-(* Norm means the term is fully normalized and cannot create a redex
+(* Ntrl means the term is fully normalized and cannot create a redex
when substituted
Cstr means the term is in head normal form and that it can
create a redex when substituted (i.e. constructor, fix, lambda)
@@ -271,10 +271,10 @@ let assoc_defined id env = match Environ.lookup_named id env with
create a redex when substituted
Red is used for terms that might be reduced
*)
-type red_state = Norm | Cstr | Whnf | Red
+type red_state = Ntrl | Cstr | Whnf | Red
let neutr = function
- | Whnf|Norm -> Whnf
+ | Whnf|Ntrl -> Whnf
| Red|Cstr -> Red
type optrel = Unknown | KnownR | KnownI
@@ -293,13 +293,13 @@ module Mark : sig
val neutr : t -> t
- val set_norm : t -> t
+ val set_ntrl : t -> t
end = struct
type t = int
let[@inline] of_state = function
- | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11
+ | Ntrl -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11
let[@inline] of_relevance = function
| Unknown -> 0
@@ -315,15 +315,15 @@ end = struct
| _ -> assert false
let[@inline] red_state x = match x land 0b1100 with
- | 0b0000 -> Norm
+ | 0b0000 -> Ntrl
| 0b0100 -> Cstr
| 0b1000 -> Whnf
| 0b1100 -> Red
| _ -> assert false
- let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *)
+ let[@inline] neutr x = x lor 0b1000 (* Whnf|Ntrl -> Whnf | Red|Cstr -> Red *)
- let[@inline] set_norm x = x land 0b0011
+ let[@inline] set_ntrl x = x land 0b0011
end
let mark = Mark.mark
@@ -358,10 +358,10 @@ and fterm =
and finvert = Univ.Instance.t * fconstr array
let fterm_of v = v.term
-let set_norm v = v.mark <- Mark.set_norm v.mark
-let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false
+let set_ntrl v = v.mark <- Mark.set_ntrl v.mark
+let is_val v = match Mark.red_state v.mark with Ntrl -> true | Cstr | Whnf | Red -> false
-let mk_atom c = {mark=mark Norm Unknown;term=FAtom c}
+let mk_atom c = {mark=mark Ntrl Unknown;term=FAtom c}
let mk_red f = {mark=mark Red Unknown;term=f}
(* Could issue a warning if no is still Red, pointing out that we loose
@@ -448,7 +448,7 @@ let rec lft_fconstr n ft =
let r = Mark.relevance ft.mark in
match ft.term with
| (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft
- | FRel i -> {mark=mark Norm r;term=FRel(i+n)}
+ | FRel i -> {mark=mark Ntrl r;term=FRel(i+n)}
| FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))}
| FFix(fx,e) ->
{mark=mark Cstr r; term=FFix(fx,subs_shft(n,e))}
@@ -466,7 +466,7 @@ let lift_fconstr_vect k v =
let clos_rel e i =
match expand_rel i e with
| Inl(n,mt) -> lift_fconstr n mt
- | Inr(k,None) -> {mark=mark Norm Unknown; term= FRel k}
+ | Inr(k,None) -> {mark=mark Ntrl Unknown; term= FRel k}
| Inr(k,Some p) ->
lift_fconstr (k-p) {mark=mark Red Unknown;term=FFlex(RelKey p)}
@@ -488,7 +488,7 @@ let compact_stack head stk =
(* Put an update mark in the stack, only if needed *)
let zupdate info m s =
let share = info.i_cache.i_share in
- if share && begin match Mark.red_state m.mark with Red -> true | Norm | Whnf | Cstr -> false end
+ if share && begin match Mark.red_state m.mark with Red -> true | Ntrl | Whnf | Cstr -> false end
then
let s' = compact_stack m s in
let _ = m.term <- FLOCKED in
@@ -514,8 +514,8 @@ let mk_clos e t =
| Rel i -> clos_rel e i
| Var x -> {mark = mark Red Unknown; term = FFlex (VarKey x) }
| Const c -> {mark = mark Red Unknown; term = FFlex (ConstKey c) }
- | Meta _ | Sort _ -> {mark = mark Norm KnownR; term = FAtom t }
- | Ind kn -> {mark = mark Norm KnownR; term = FInd kn }
+ | Meta _ | Sort _ -> {mark = mark Ntrl KnownR; term = FAtom t }
+ | Ind kn -> {mark = mark Ntrl KnownR; term = FInd kn }
| Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn }
| Int i -> {mark = mark Cstr Unknown; term = FInt i}
| Float f -> {mark = mark Cstr Unknown; term = FFloat f}
@@ -734,11 +734,11 @@ let strip_update_shift_app_red head stk =
strip_rec [] head 0 stk
let strip_update_shift_app head stack =
- assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true);
+ assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true);
strip_update_shift_app_red head stack
let get_nth_arg head n stk =
- assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true);
+ assert (match Mark.red_state head.mark with Red -> false | Ntrl | Cstr | Whnf -> true);
let rec strip_rec rstk h n = function
| Zshift(k) as e :: s ->
strip_rec (e::rstk) (lift_fconstr k h) n s
@@ -787,7 +787,7 @@ let rec eta_expand_stack = function
| Zshift _ | Zupdate _ | Zprimitive _ as e) :: s ->
e :: eta_expand_stack s
| [] ->
- [Zshift 1; Zapp [|{mark=mark Norm Unknown; term= FRel 1}|]]
+ [Zshift 1; Zapp [|{mark=mark Ntrl Unknown; term= FRel 1}|]]
(* Get the arguments of a native operator *)
let rec skip_native_args rargs nargs =
@@ -968,7 +968,7 @@ module FNativeEntries =
| FArray (_u,t,_ty) -> t
| _ -> raise Not_found
- let dummy = {mark = mark Norm KnownR; term = FRel 0}
+ let dummy = {mark = mark Ntrl KnownR; term = FRel 0}
let current_retro = ref Retroknowledge.empty
let defined_int = ref false
@@ -978,7 +978,7 @@ module FNativeEntries =
match retro.Retroknowledge.retro_int63 with
| Some c ->
defined_int := true;
- fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+ fint := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
| None -> defined_int := false
let defined_float = ref false
@@ -988,7 +988,7 @@ module FNativeEntries =
match retro.Retroknowledge.retro_float64 with
| Some c ->
defined_float := true;
- ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
+ ffloat := { mark = mark Ntrl KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) }
| None -> defined_float := false
let defined_bool = ref false
@@ -1039,7 +1039,7 @@ module FNativeEntries =
fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) };
fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) };
let (icmp, _) = cEq in
- fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) }
+ fcmp := { mark = mark Ntrl KnownR; term = FInd (Univ.in_punivs icmp) }
| None -> defined_cmp := false
let defined_f_cmp = ref false
@@ -1327,19 +1327,19 @@ let rec knr info tab m stk =
let rargs, a, nargs, stk = get_native_args1 op c stk in
kni info tab a (Zprimitive(op,c,rargs,nargs)::stk)
else
- (* Similarly to fix, partially applied primitives are not Norm! *)
+ (* Similarly to fix, partially applied primitives are not Ntrl! *)
(m, stk)
- | Undef _ | OpaqueDef _ -> (set_norm m; (m,stk)))
+ | Undef _ | OpaqueDef _ -> (set_ntrl m; (m,stk)))
| FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
(match ref_value_cache info tab (VarKey id) with
| Def v -> kni info tab v stk
| Primitive _ -> assert false
- | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk)))
+ | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk)))
| FFlex(RelKey k) when red_set info.i_flags fDELTA ->
(match ref_value_cache info tab (RelKey k) with
| Def v -> kni info tab v stk
| Primitive _ -> assert false
- | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk)))
+ | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk)))
| FConstruct((_ind,c),_u) ->
let use_match = red_set info.i_flags fMATCH in
let use_fix = red_set info.i_flags fFIX in
@@ -1523,9 +1523,9 @@ let norm_val info tab v =
with_stats (lazy (kl info tab v))
let whd_stack infos tab m stk = match Mark.red_state m.mark with
-| Whnf | Norm ->
+| Whnf | Ntrl ->
(** No need to perform [kni] nor to unlock updates because
- every head subterm of [m] is [Whnf] or [Norm] *)
+ every head subterm of [m] is [Whnf] or [Ntrl] *)
knh infos m stk
| Red | Cstr ->
let k = kni infos tab m stk in
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/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-05-01 19:30:47 +0000