diff options
Diffstat (limited to 'kernel')
34 files changed, 644 insertions, 344 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4bc6848ba7..20890a28dc 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -21,68 +21,12 @@ #include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" +#include "coq_arity.h" #include "coq_fix_code.h" #ifdef THREADED_CODE char ** coq_instr_table; char * coq_instr_base; -int arity[STOP+1]; - -void init_arity () { - /* instruction with zero operand */ - arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= - arity[ACC6]=arity[ACC7]= - arity[PUSH]=arity[PUSHACC1]= - arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= - arity[PUSHACC6]=arity[PUSHACC7]= - arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]= - arity[PUSHENVACC0]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]= - arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]= - arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]= - arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]= - arity[GETFIELD0]=arity[GETFIELD1]= - arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= - arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]= - 0; - /* instruction with one operand */ - arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= - arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= - arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]= - arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= - arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= - arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= - arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]= - arity[BRANCH]=arity[ENSURESTACKCAPACITY]= - arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]= - arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]= - arity[CHECKMULINT63]=arity[CHECKMULCINT63]= - arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]= - arity[CHECKDIV21INT63]= - arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]= - arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= - arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= - arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= - arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]= - arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= - arity[CHECKCLASSIFYFLOAT]= - arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= - arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= - arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= - arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]= - arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; - /* instruction with two operands */ - arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= - arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]= - arity[PROJ]= - 2; - /* instruction with four operands */ - arity[MAKESWITCHBLOCK]=4; - /* instruction with arbitrary operands */ - arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; -} - #endif /* THREADED_CODE */ @@ -164,9 +108,7 @@ value coq_tcode_of_code (value code) { opcode_t instr; COPY32(&instr,p); p++; - if (instr < 0 || instr > STOP){ - instr = STOP; - }; + if (instr < 0 || instr > STOP) abort(); *q++ = VALINSTR(instr); if (instr == SWITCH) { uint32_t i, sizes, const_size, block_size; @@ -183,8 +125,9 @@ value coq_tcode_of_code (value code) { q++; for(i=1; i<n; i++) { COPY32(q,p); p++; q++; }; } else { - uint32_t i, ar; + int i, ar; ar = arity[instr]; + if (ar < 0) abort(); for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; }; } } diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 5a233e6178..916d9753a4 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -18,7 +18,6 @@ void * coq_stat_alloc (asize_t sz); #ifdef THREADED_CODE extern char ** coq_instr_table; extern char * coq_instr_base; -void init_arity(); #define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base)) #else #define VALINSTR(instr) instr diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a9ea6d9f46..704eb1ef98 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -547,7 +547,7 @@ value coq_interprete CHECK_STACK(0); /* We also check for signals */ #if OCAML_VERSION >= 41000 - { + if (caml_something_to_do) { value res = caml_process_pending_actions_exn(); if (Is_exception_result(res)) { /* If there is an asynchronous exception, we reset the vm */ @@ -1426,6 +1426,41 @@ value coq_interprete Next; } + Instruct(CHECKDIVSINT63) { + print_instr("CHEKDIVSINT63"); + CheckInt2(); + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; + } + else { + Uint63_eqm1(b, *sp); + if (b) { + Uint63_neg(accu); + sp++; + } + else { + Uint63_divs(accu, *sp++); + } + } + Next; + } + + Instruct(CHECKMODSINT63) { + print_instr("CHEKMODSINT63"); + CheckInt2(); + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; + } + else { + Uint63_mods(accu,*sp++); + } + Next; + } + Instruct (CHECKDIV21INT63) { print_instr("DIV21INT63"); CheckInt3(); @@ -1473,6 +1508,13 @@ value coq_interprete Next; } + Instruct(CHECKASRINT63) { + print_instr("CHECKASRINT63"); + CheckInt2(); + Uint63_asr(accu,*sp++); + Next; + } + Instruct (CHECKADDMULDIVINT63) { print_instr("CHECKADDMULDIVINT63"); CheckInt3(); @@ -1508,6 +1550,24 @@ value coq_interprete Next; } + Instruct (CHECKLTSINT63) { + print_instr("CHECKLTSINT63"); + CheckInt2(); + int b; + Uint63_lts(b,accu,*sp++); + accu = b ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLESINT63) { + print_instr("CHECKLESINT63"); + CheckInt2(); + int b; + Uint63_les(b,accu,*sp++); + accu = b ? coq_true : coq_false; + Next; + } + Instruct (CHECKCOMPAREINT63) { /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ /* assumes Inductive _ : _ := Eq | Lt | Gt */ @@ -1526,6 +1586,24 @@ value coq_interprete Next; } + Instruct (CHECKCOMPARESINT63) { + /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ + /* assumes Inductive _ : _ := Eq | Lt | Gt */ + print_instr("CHECKCOMPARESINT63"); + CheckInt2(); + int b; + Uint63_eq(b, accu, *sp); + if (b) { + accu = coq_Eq; + sp++; + } + else { + Uint63_lts(b, accu, *sp++); + accu = b ? coq_Lt : coq_Gt; + } + Next; + } + Instruct (CHECKHEAD0INT63) { print_instr("CHECKHEAD0INT63"); CheckInt1(); diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index fe076f8f04..a55ff57c8d 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -100,9 +100,6 @@ value init_coq_vm(value unit) /* ML */ fprintf(stderr,"already open \n");fflush(stderr);} else { drawinstr=0; -#ifdef THREADED_CODE - init_arity(); -#endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); /* Initialing the interpreter */ diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index dd9b9e55be..693716ee90 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -96,7 +96,10 @@ value uint63_##name##_ml(value x, value y, value z) { \ accu = uint63_return_value__; \ }while(0) +DECLARE_NULLOP(zero) DECLARE_NULLOP(one) +DECLARE_UNOP(neg) +#define Uint63_neg(x) CALL_UNOP(neg, x) DECLARE_BINOP(add) #define Uint63_add(x, y) CALL_BINOP(add, x, y) DECLARE_BINOP(addcarry) @@ -105,28 +108,40 @@ DECLARE_TEROP(addmuldiv) #define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z) DECLARE_BINOP(div) #define Uint63_div(x, y) CALL_BINOP(div, x, y) +DECLARE_BINOP(divs) +#define Uint63_divs(x, y) CALL_BINOP(divs, x, y) DECLARE_BINOP(eq) #define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y) DECLARE_UNOP(eq0) #define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x) +DECLARE_UNOP(eqm1) +#define Uint63_eqm1(r, x) CALL_PREDICATE(r, eqm1, x) DECLARE_UNOP(head0) #define Uint63_head0(x) CALL_UNOP(head0, x) DECLARE_BINOP(land) #define Uint63_land(x, y) CALL_BINOP(land, x, y) DECLARE_BINOP(leq) #define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y) +DECLARE_BINOP(les) +#define Uint63_les(r, x, y) CALL_RELATION(r, les, x, y) DECLARE_BINOP(lor) #define Uint63_lor(x, y) CALL_BINOP(lor, x, y) DECLARE_BINOP(lsl) #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y) DECLARE_BINOP(lsr) #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y) +DECLARE_BINOP(asr) +#define Uint63_asr(x, y) CALL_BINOP(asr, x, y) DECLARE_BINOP(lt) #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y) +DECLARE_BINOP(lts) +#define Uint63_lts(r, x, y) CALL_RELATION(r, lts, x, y) DECLARE_BINOP(lxor) #define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y) DECLARE_BINOP(mod) #define Uint63_mod(x, y) CALL_BINOP(mod, x, y) +DECLARE_BINOP(mods) +#define Uint63_mods(x, y) CALL_BINOP(mods, x, y) DECLARE_BINOP(mul) #define Uint63_mul(x, y) CALL_BINOP(mul, x, y) DECLARE_BINOP(sub) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 731ae8f46e..da9ae7f147 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -12,21 +12,28 @@ #define uint_of_value(val) (((uint64_t)(val)) >> 1) #define uint63_of_value(val) ((uint64_t)(val) >> 1) +#define int63_of_value(val) ((int64_t)(val) >> 1) /* 2^63 * y + x as a value */ //#define Val_intint(x,y) ((value)(((uint64_t)(x)) << 1 + ((uint64_t)(y) << 64))) -#define uint63_zero ((value) 1) /* 2*0 + 1 */ +#define uint63_zero() ((value) 1) /* 2*0 + 1 */ #define uint63_one() ((value) 3) /* 2*1 + 1 */ #define uint63_eq(x,y) ((x) == (y)) #define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y)) #define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1)) +#define Uint63_eqm1(r,x) ((r) = ((x) == (uint64_t)(int64_t)(-1))) #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y)) #define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y)) #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y)) #define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y)) +#define uint63_lts(x,y) ((int64_t) (x) < (int64_t) (y)) +#define Uint63_lts(r,x,y) ((r) = uint63_lts(x,y)) +#define uint63_les(x,y) ((int64_t) (x) <= (int64_t) (y)) +#define Uint63_les(r,x,y) ((r) = uint63_les(x,y)) +#define Uint63_neg(x) (accu = (value)(2 - (uint64_t) x)) #define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1)) #define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1)) #define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1)) @@ -34,6 +41,8 @@ #define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y))) #define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y))) #define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y))) +#define Uint63_divs(x,y) (accu = Val_long(int63_of_value(x) / int63_of_value(y))) +#define Uint63_mods(x,y) (accu = Val_long(int63_of_value(x) % int63_of_value(y))) #define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) #define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y))) @@ -46,14 +55,21 @@ if (uint63_lsl_y__ < (uint64_t) 127) \ accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \ else \ - accu = uint63_zero; \ + accu = uint63_zero(); \ }while(0) #define Uint63_lsr(x,y) do{ \ value uint63_lsl_y__ = (y); \ if (uint63_lsl_y__ < (uint64_t) 127) \ accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \ else \ - accu = uint63_zero; \ + accu = uint63_zero(); \ + }while(0) +#define Uint63_asr(x,y) do{ \ + value uint63_asr_y__ = (y); \ + if (uint63_asr_y__ < (uint64_t) 127) \ + accu = (value)(((int64_t)(x) >> uint63_of_value(uint63_asr_y__)) | 1); \ + else \ + accu = uint63_zero(); \ }while(0) /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ diff --git a/kernel/byterun/dune b/kernel/byterun/dune index d3e2a2fa7f..b14ad5c558 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -1,7 +1,7 @@ (library (name byterun) (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") - (public_name coq.vm) + (public_name coq-core.vm) (foreign_stubs (language c) (names coq_fix_code coq_float64 coq_memory coq_values coq_interp) @@ -14,3 +14,7 @@ (rule (targets coq_jumptbl.h) (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) + +(rule + (targets coq_arity.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe arity)))) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 5cd91b4e74..6ef0e9fa15 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -8,6 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* Note: don't forget to update v_primitive in checker/values.ml if the *) +(* number of primitives is changed. *) + open Univ type t = @@ -18,8 +21,11 @@ type t = | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -34,7 +40,10 @@ type t = | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq @@ -68,8 +77,11 @@ let parse = function | "int63_mul" -> Int63mul | "int63_div" -> Int63div | "int63_mod" -> Int63mod + | "int63_divs" -> Int63divs + | "int63_mods" -> Int63mods | "int63_lsr" -> Int63lsr | "int63_lsl" -> Int63lsl + | "int63_asr" -> Int63asr | "int63_land" -> Int63land | "int63_lor" -> Int63lor | "int63_lxor" -> Int63lxor @@ -84,7 +96,10 @@ let parse = function | "int63_eq" -> Int63eq | "int63_lt" -> Int63lt | "int63_le" -> Int63le + | "int63_lts" -> Int63lts + | "int63_les" -> Int63les | "int63_compare" -> Int63compare + | "int63_compares" -> Int63compares | "float64_opp" -> Float64opp | "float64_abs" -> Float64abs | "float64_eq" -> Float64eq @@ -163,6 +178,12 @@ let hash = function | Arrayset -> 46 | Arraycopy -> 47 | Arraylength -> 48 + | Int63lts -> 49 + | Int63les -> 50 + | Int63divs -> 51 + | Int63mods -> 52 + | Int63asr -> 53 + | Int63compares -> 54 (* Should match names in nativevalues.ml *) let to_string = function @@ -173,8 +194,11 @@ let to_string = function | Int63mul -> "mul" | Int63div -> "div" | Int63mod -> "rem" + | Int63divs -> "divs" + | Int63mods -> "rems" | Int63lsr -> "l_sr" | Int63lsl -> "l_sl" + | Int63asr -> "a_sr" | Int63land -> "l_and" | Int63lor -> "l_or" | Int63lxor -> "l_xor" @@ -189,7 +213,10 @@ let to_string = function | Int63eq -> "eq" | Int63lt -> "lt" | Int63le -> "le" + | Int63lts -> "lts" + | Int63les -> "les" | Int63compare -> "compare" + | Int63compares -> "compares" | Float64opp -> "fopp" | Float64abs -> "fabs" | Float64eq -> "feq" @@ -271,14 +298,15 @@ let types = | Int63head0 | Int63tail0 -> [int_ty; int_ty] | Int63add | Int63sub | Int63mul | Int63div | Int63mod - | Int63lsr | Int63lsl + | Int63divs | Int63mods + | Int63lsr | Int63lsl | Int63asr | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)] | Int63mulc | Int63diveucl -> [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] - | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] - | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] + | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] + | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] | Int63div21 -> [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] @@ -314,8 +342,11 @@ let params = function | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -330,7 +361,10 @@ let params = function | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq @@ -367,8 +401,11 @@ let univs = function | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -383,7 +420,10 @@ let univs = function | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 0db643faf4..de90179726 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -16,8 +16,11 @@ type t = | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -32,7 +35,10 @@ type t = | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq diff --git a/kernel/dune b/kernel/dune index bd663974da..0bf51f80ec 100644 --- a/kernel/dune +++ b/kernel/dune @@ -1,7 +1,7 @@ (library (name kernel) (synopsis "The Coq Kernel") - (public_name coq.kernel) + (public_name coq-core.kernel) (wrapped false) (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63)) (libraries lib byterun dynlink)) @@ -25,7 +25,7 @@ (action (copy# %{gen-file} %{targets}))) (documentation - (package coq)) + (package coq-core)) ; In dev profile, we check the kernel against a more strict set of ; warnings. diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 0e1cd0c56a..20220dd9d2 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -10,192 +10,201 @@ (** List of opcodes. - It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and - [vmopcodes.ml] files. + It is used to generate the files [coq_instruct.h], [coq_jumptbl.h], + [coq_arity.h], and [vmopcodes.ml]. - If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c - with the arity of the instruction and maybe coq_tcode_of_code. + [STOP] needs to be the last opcode. + + Arity -1 designates opcodes that need special handling in [coq_fix_code.c]. *) let opcodes = [| - "ACC0"; - "ACC1"; - "ACC2"; - "ACC3"; - "ACC4"; - "ACC5"; - "ACC6"; - "ACC7"; - "ACC"; - "PUSH"; - "PUSHACC1"; - "PUSHACC2"; - "PUSHACC3"; - "PUSHACC4"; - "PUSHACC5"; - "PUSHACC6"; - "PUSHACC7"; - "PUSHACC"; - "POP"; - "ENVACC0"; - "ENVACC1"; - "ENVACC2"; - "ENVACC3"; - "ENVACC"; - "PUSHENVACC0"; - "PUSHENVACC1"; - "PUSHENVACC2"; - "PUSHENVACC3"; - "PUSHENVACC"; - "PUSH_RETADDR"; - "APPLY"; - "APPLY1"; - "APPLY2"; - "APPLY3"; - "APPLY4"; - "APPTERM"; - "APPTERM1"; - "APPTERM2"; - "APPTERM3"; - "RETURN"; - "RESTART"; - "GRAB"; - "GRABREC"; - "CLOSURE"; - "CLOSUREREC"; - "CLOSURECOFIX"; - "OFFSETCLOSURE0"; - "OFFSETCLOSURE1"; - "OFFSETCLOSURE"; - "PUSHOFFSETCLOSURE0"; - "PUSHOFFSETCLOSURE1"; - "PUSHOFFSETCLOSURE"; - "GETGLOBAL"; - "PUSHGETGLOBAL"; - "MAKEBLOCK"; - "MAKEBLOCK1"; - "MAKEBLOCK2"; - "MAKEBLOCK3"; - "MAKEBLOCK4"; - "SWITCH"; - "PUSHFIELDS"; - "GETFIELD0"; - "GETFIELD1"; - "GETFIELD"; - "SETFIELD"; - "PROJ"; - "ENSURESTACKCAPACITY"; - "CONST0"; - "CONST1"; - "CONST2"; - "CONST3"; - "CONSTINT"; - "PUSHCONST0"; - "PUSHCONST1"; - "PUSHCONST2"; - "PUSHCONST3"; - "PUSHCONSTINT"; - "ACCUMULATE"; - "MAKESWITCHBLOCK"; - "MAKEACCU"; - "BRANCH"; - "CHECKADDINT63"; - "CHECKADDCINT63"; - "CHECKADDCARRYCINT63"; - "CHECKSUBINT63"; - "CHECKSUBCINT63"; - "CHECKSUBCARRYCINT63"; - "CHECKMULINT63"; - "CHECKMULCINT63"; - "CHECKDIVINT63"; - "CHECKMODINT63"; - "CHECKDIVEUCLINT63"; - "CHECKDIV21INT63"; - "CHECKLXORINT63"; - "CHECKLORINT63"; - "CHECKLANDINT63"; - "CHECKLSLINT63"; - "CHECKLSRINT63"; - "CHECKADDMULDIVINT63"; - "CHECKEQINT63"; - "CHECKLTINT63"; - "CHECKLEINT63"; - "CHECKCOMPAREINT63"; - "CHECKHEAD0INT63"; - "CHECKTAIL0INT63"; - "CHECKOPPFLOAT"; - "CHECKABSFLOAT"; - "CHECKEQFLOAT"; - "CHECKLTFLOAT"; - "CHECKLEFLOAT"; - "CHECKCOMPAREFLOAT"; - "CHECKCLASSIFYFLOAT"; - "CHECKADDFLOAT"; - "CHECKSUBFLOAT"; - "CHECKMULFLOAT"; - "CHECKDIVFLOAT"; - "CHECKSQRTFLOAT"; - "CHECKFLOATOFINT63"; - "CHECKFLOATNORMFRMANTISSA"; - "CHECKFRSHIFTEXP"; - "CHECKLDSHIFTEXP"; - "CHECKNEXTUPFLOAT"; - "CHECKNEXTDOWNFLOAT"; - "CHECKNEXTUPFLOATINPLACE"; - "CHECKNEXTDOWNFLOATINPLACE"; - "CHECKCAMLCALL2_1"; - "CHECKCAMLCALL1"; - "CHECKCAMLCALL2"; - "CHECKCAMLCALL3_1"; - "STOP" + "ACC0", 0; + "ACC1", 0; + "ACC2", 0; + "ACC3", 0; + "ACC4", 0; + "ACC5", 0; + "ACC6", 0; + "ACC7", 0; + "ACC", 1; + "PUSH", 0; + "PUSHACC1", 0; + "PUSHACC2", 0; + "PUSHACC3", 0; + "PUSHACC4", 0; + "PUSHACC5", 0; + "PUSHACC6", 0; + "PUSHACC7", 0; + "PUSHACC", 1; + "POP", 1; + "ENVACC0", 0; + "ENVACC1", 0; + "ENVACC2", 0; + "ENVACC3", 0; + "ENVACC", 1; + "PUSHENVACC0", 0; + "PUSHENVACC1", 0; + "PUSHENVACC2", 0; + "PUSHENVACC3", 0; + "PUSHENVACC", 1; + "PUSH_RETADDR", 1; + "APPLY", 1; + "APPLY1", 0; + "APPLY2", 0; + "APPLY3", 0; + "APPLY4", 0; + "APPTERM", 2; + "APPTERM1", 1; + "APPTERM2", 1; + "APPTERM3", 1; + "RETURN", 1; + "RESTART", 0; + "GRAB", 1; + "GRABREC", 1; + "CLOSURE", 2; + "CLOSUREREC", -1; + "CLOSURECOFIX", -1; + "OFFSETCLOSURE0", 0; + "OFFSETCLOSURE1", 0; + "OFFSETCLOSURE", 1; + "PUSHOFFSETCLOSURE0", 0; + "PUSHOFFSETCLOSURE1", 0; + "PUSHOFFSETCLOSURE", 1; + "GETGLOBAL", 1; + "PUSHGETGLOBAL", 1; + "MAKEBLOCK", 2; + "MAKEBLOCK1", 1; + "MAKEBLOCK2", 1; + "MAKEBLOCK3", 1; + "MAKEBLOCK4", 1; + "SWITCH", -1; + "PUSHFIELDS", 1; + "GETFIELD0", 0; + "GETFIELD1", 0; + "GETFIELD", 1; + "SETFIELD", 1; + "PROJ", 2; + "ENSURESTACKCAPACITY", 1; + "CONST0", 0; + "CONST1", 0; + "CONST2", 0; + "CONST3", 0; + "CONSTINT", 1; + "PUSHCONST0", 0; + "PUSHCONST1", 0; + "PUSHCONST2", 0; + "PUSHCONST3", 0; + "PUSHCONSTINT", 1; + "ACCUMULATE", 0; + "MAKESWITCHBLOCK", 4; + "MAKEACCU", 1; + "BRANCH", 1; + "CHECKADDINT63", 1; + "CHECKADDCINT63", 1; + "CHECKADDCARRYCINT63", 1; + "CHECKSUBINT63", 1; + "CHECKSUBCINT63", 1; + "CHECKSUBCARRYCINT63", 1; + "CHECKMULINT63", 1; + "CHECKMULCINT63", 1; + "CHECKDIVINT63", 1; + "CHECKMODINT63", 1; + "CHECKDIVSINT63", 1; + "CHECKMODSINT63", 1; + "CHECKDIVEUCLINT63", 1; + "CHECKDIV21INT63", 1; + "CHECKLXORINT63", 1; + "CHECKLORINT63", 1; + "CHECKLANDINT63", 1; + "CHECKLSLINT63", 1; + "CHECKLSRINT63", 1; + "CHECKASRINT63", 1; + "CHECKADDMULDIVINT63", 1; + "CHECKEQINT63", 1; + "CHECKLTINT63", 1; + "CHECKLEINT63", 1; + "CHECKLTSINT63", 1; + "CHECKLESINT63", 1; + "CHECKCOMPAREINT63", 1; + "CHECKCOMPARESINT63", 1; + "CHECKHEAD0INT63", 1; + "CHECKTAIL0INT63", 1; + "CHECKOPPFLOAT", 1; + "CHECKABSFLOAT", 1; + "CHECKEQFLOAT", 1; + "CHECKLTFLOAT", 1; + "CHECKLEFLOAT", 1; + "CHECKCOMPAREFLOAT", 1; + "CHECKCLASSIFYFLOAT", 1; + "CHECKADDFLOAT", 1; + "CHECKSUBFLOAT", 1; + "CHECKMULFLOAT", 1; + "CHECKDIVFLOAT", 1; + "CHECKSQRTFLOAT", 1; + "CHECKFLOATOFINT63", 1; + "CHECKFLOATNORMFRMANTISSA", 1; + "CHECKFRSHIFTEXP", 1; + "CHECKLDSHIFTEXP", 1; + "CHECKNEXTUPFLOAT", 1; + "CHECKNEXTDOWNFLOAT", 1; + "CHECKNEXTUPFLOATINPLACE", 1; + "CHECKNEXTDOWNFLOATINPLACE", 1; + "CHECKCAMLCALL2_1", 2; + "CHECKCAMLCALL1", 2; + "CHECKCAMLCALL2", 2; + "CHECKCAMLCALL3_1", 2; + "STOP", 0 |] let pp_c_comment fmt = - Format.fprintf fmt "/* %a */" + Format.fprintf fmt "/* %s */" let pp_ocaml_comment fmt = - Format.fprintf fmt "(* %a *)" + Format.fprintf fmt "(* %s *)" let pp_header isOcaml fmt = Format.fprintf fmt "%a" - (fun fmt -> - (if isOcaml then pp_ocaml_comment else pp_c_comment) fmt - Format.pp_print_string) + (if isOcaml then pp_ocaml_comment else pp_c_comment) "DO NOT EDIT: automatically generated by kernel/genOpcodeFiles.ml" -let pp_with_commas fmt k = - Array.iteri (fun n s -> - Format.fprintf fmt " %a%s@." - k s - (if n + 1 < Array.length opcodes - then "," else "") - ) opcodes - let pp_coq_instruct_h fmt = - let line = Format.fprintf fmt "%s@." in pp_header false fmt; - line "#pragma once"; - line "enum instructions {"; - pp_with_commas fmt Format.pp_print_string; - line "};" + Format.fprintf fmt "#pragma once@.enum instructions {@."; + Array.iter (fun (name, _) -> + Format.fprintf fmt " %s,@." name + ) opcodes; + Format.fprintf fmt "};@." let pp_coq_jumptbl_h fmt = - pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s") + pp_header false fmt; + Array.iter (fun (name, _) -> + Format.fprintf fmt " &&coq_lbl_%s,@." name + ) opcodes + +let pp_coq_arity_h fmt = + pp_header false fmt; + Format.fprintf fmt "static signed char arity[] = {@."; + Array.iter (fun (_, arity) -> + Format.fprintf fmt " %d,@." arity + ) opcodes; + Format.fprintf fmt "};@." let pp_vmopcodes_ml fmt = pp_header true fmt; Array.iteri (fun n s -> Format.fprintf fmt "let op%s = %d@.@." s n - ) opcodes + ) (Array.map fst opcodes) let usage () = - Format.eprintf "usage: %s [enum|jump|copml]@." Sys.argv.(0); + Format.eprintf "usage: %s [enum|jump|arity|copml]@." Sys.argv.(0); exit 1 let main () = match Sys.argv.(1) with | "enum" -> pp_coq_instruct_h Format.std_formatter | "jump" -> pp_coq_jumptbl_h Format.std_formatter + | "arity" -> pp_coq_arity_h Format.std_formatter | "copml" -> pp_vmopcodes_ml Format.std_formatter | _ -> usage () | exception Invalid_argument _ -> usage () diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c19b883e3d..9ce388929c 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -24,6 +24,11 @@ open Environ compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code. *) +let debug_native_flag, debug_native_compiler = CDebug.create_full ~name:"native-compiler" () + +let keep_debug_files () = + CDebug.get_flag debug_native_flag + (** Local names **) (* The first component is there for debugging purposes only *) @@ -1939,7 +1944,7 @@ let compile_constant env sigma con cb = | Def t -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in - if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); + debug_native_compiler (fun () -> Pp.str "Generated lambda code"); let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in let l = Constant.label con in @@ -1950,11 +1955,11 @@ let compile_constant env sigma con cb = let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in (auxdefs,mkMLlam [|univ|] code) in - if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code"); + debug_native_compiler (fun () -> Pp.str "Generated mllambda code"); let code = optimize_stk (Glet(Gconstant ("", con),code)::auxdefs) in - if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); + debug_native_compiler (fun () -> Pp.str "Optimized mllambda code"); code | _ -> let i = push_symbol (SymbConst con) in @@ -2125,7 +2130,7 @@ let compile_deps env sigma prefix init t = in aux env 0 init t -let compile_constant_field env _prefix con acc cb = +let compile_constant_field env con acc cb = let gl = compile_constant env empty_evars con cb in gl@acc diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index aab6e1d4a0..17312ec8ea 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -21,6 +21,10 @@ to OCaml code. *) type mllambda type global +val debug_native_compiler : CDebug.t + +val keep_debug_files : unit -> bool + val pp_global : Format.formatter -> global -> unit val mk_open : string -> global @@ -59,7 +63,9 @@ val empty_updates : code_location_updates val register_native_file : string -> unit -val compile_constant_field : env -> string -> Constant.t -> +val is_loaded_native_file : string -> bool + +val compile_constant_field : env -> Constant.t -> global list -> 'a constant_body -> global list val compile_mind_field : ModPath.t -> Label.t -> diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d77ee759c6..f0ae5e2fbf 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Nativelib open Reduction open Util open Nativevalues @@ -151,22 +150,25 @@ let warn_no_native_compiler = strbrk " falling back to VM conversion test.") let native_conv_gen pb sigma env univs t1 t2 = - 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 - else - let ml_filename, prefix = get_ml_filename () in + Nativelib.link_libraries (); + let ml_filename, prefix = Nativelib.get_ml_filename () in let code, upds = mk_conv_code env sigma prefix t1 t2 in - let fn = compile ml_filename code ~profile:false in - if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); + let fn = Nativelib.compile ml_filename code ~profile:false in + debug_native_compiler (fun () -> Pp.str "Running test..."); let t0 = Sys.time () in - call_linker ~fatal:true ~prefix fn (Some upds); + let (rt1, rt2) = Nativelib.execute_library ~prefix fn upds in let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + debug_native_compiler (fun () -> Pp.str time_info); (* TODO change 0 when we can have de Bruijn *) - fst (conv_val env pb 0 !rt1 !rt2 univs) + fst (conv_val env pb 0 rt1 rt2 univs) + +let native_conv_gen pb sigma env univs t1 t2 = + 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 + else native_conv_gen pb sigma env univs t1 t2 (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1e1085d5ff..73567e34cf 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -38,7 +38,7 @@ let ( / ) = Filename.concat let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") let () = at_exit (fun () -> - if not !Flags.debug && Lazy.is_val my_temp_dir then + if not (keep_debug_files ()) && Lazy.is_val my_temp_dir then try let d = Lazy.force my_temp_dir in Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); @@ -129,7 +129,7 @@ let call_compiler ?profile:(profile=false) ml_filename = ::"-w"::"a" ::include_dirs) @ ["-impl"; ml_filename] in - if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); + debug_native_compiler (fun () -> Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (Envars.ocamlfind ()) args in match res with @@ -142,7 +142,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let compile fn code ~profile:profile = write_ml_code fn code; let r = call_compiler ~profile fn in - if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; + if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn; r type native_library = Nativecode.global list * Nativevalues.symbols @@ -160,34 +160,43 @@ let compile_library (code, symb) fn = let fn = dirname / basename in write_ml_code fn ~header code; let _ = call_compiler fn in - if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn + if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn -(* call_linker links dynamically the code for constants in environment or a *) -(* conversion test. *) -let call_linker ?(fatal=true) ~prefix f upds = +let execute_library ~prefix f upds = rt1 := dummy_value (); rt2 := dummy_value (); if not (Sys.file_exists f) then - begin - let msg = "Cannot find native compiler file " ^ f in - if fatal then CErrors.user_err Pp.(str msg) - else if !Flags.debug then Feedback.msg_debug (Pp.str msg) - end - else - (try - if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; - register_native_file prefix - with Dynlink.Error _ as exn -> - let exn = Exninfo.capture exn in - if fatal then Exninfo.iraise exn - else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); - match upds with Some upds -> update_locations upds | _ -> () - -let link_library ~prefix ~dirname ~basename = + CErrors.user_err Pp.(str "Cannot find native compiler file " ++ str f); + if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; + register_native_file prefix; + update_locations upds; + (!rt1, !rt2) + +let link_library dirname prefix = + let basename = Dynlink.adapt_filename (prefix ^ "cmo") in (* We try both [output_dir] and [.coq-native], unfortunately from [Require] we don't know if we are loading a library in the build dir or in the installed layout *) let install_location = dirname / dft_output_dir / basename in let build_location = dirname / !output_dir / basename in let f = if Sys.file_exists build_location then build_location else install_location in - call_linker ~fatal:false ~prefix f None + try + if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; + register_native_file prefix + with + | Dynlink.Error _ as exn -> + debug_native_compiler (fun () -> CErrors.iprint (Exninfo.capture exn)) + +let delayed_link = ref [] + +let link_libraries () = + let delayed = List.rev !delayed_link in + delayed_link := []; + List.iter (fun (dirname, libname) -> + let prefix = mod_uid_of_dirpath libname ^ "." in + if not (Nativecode.is_loaded_native_file prefix) then + link_library dirname prefix + ) delayed + +let enable_library dirname libname = + delayed_link := (dirname, libname) :: !delayed_link diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 0c0fe3acc9..ba04c28ab0 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Nativecode (** This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler. *) @@ -25,7 +24,7 @@ val get_ml_filename : unit -> string * string (** [compile file code ~profile] will compile native [code] to [file], and return the name of the object file; this name depends on whether are in byte mode or not; file is expected to be .ml file *) -val compile : string -> global list -> profile:bool -> string +val compile : string -> Nativecode.global list -> profile:bool -> string type native_library = Nativecode.global list * Nativevalues.symbols @@ -33,18 +32,19 @@ type native_library = Nativecode.global list * Nativevalues.symbols but will perform some extra tweaks to handle [code] as a Coq lib. *) val compile_library : native_library -> string -> unit -val call_linker - : ?fatal:bool - -> prefix:string - -> string - -> code_location_updates option - -> unit +(** [execute_library file upds] dynamically loads library [file], + updates the library locations [upds], and returns the values stored + in [rt1] and [rt2] *) +val execute_library : + prefix:string -> string -> Nativecode.code_location_updates -> + Nativevalues.t * Nativevalues.t -val link_library - : prefix:string - -> dirname:string - -> basename:string - -> unit +(** [enable_library] marks the given library for dynamic loading + the next time [link_libraries] is called. *) +val enable_library : string -> Names.DirPath.t -> unit +val link_libraries : unit -> unit + +(* used for communication with the loaded libraries *) val rt1 : Nativevalues.t ref val rt2 : Nativevalues.t ref diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c95880dc36..6dd7f315e0 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -17,55 +17,54 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -let rec translate_mod prefix mp env mod_expr acc = +let rec translate_mod mp env mod_expr acc = match mod_expr with | NoFunctor struc -> let env' = add_structure mp struc empty_delta_resolver env in - List.fold_left (translate_field prefix mp env') acc struc + List.fold_left (translate_field mp env') acc struc | MoreFunctor _ -> acc -and translate_field prefix mp env acc (l,x) = +and translate_field mp env acc (l,x) = match x with | SFBconst cb -> let con = Constant.make2 mp l in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in - Feedback.msg_debug (Pp.str msg)); - compile_constant_field env prefix con acc cb + Pp.str msg)); + compile_constant_field env con acc cb | SFBmind mb -> - (if !Flags.debug then + (debug_native_compiler (fun () -> let id = mb.mind_packets.(0).mind_typename in let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); compile_mind_field mp l acc mb | SFBmodule md -> let mp = md.mod_mp in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module %s..." (ModPath.to_string mp) in - Feedback.msg_debug (Pp.str msg)); - translate_mod prefix mp env md.mod_type acc + Pp.str msg)); + translate_mod mp env md.mod_type acc | SFBmodtype mdtyp -> let mp = mdtyp.mod_mp in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp) in - Feedback.msg_debug (Pp.str msg)); - translate_mod prefix mp env mdtyp.mod_type acc + Pp.str msg)); + translate_mod mp env mdtyp.mod_type acc -let dump_library mp dp env mod_expr = - if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library..."); +let dump_library mp env mod_expr = + debug_native_compiler (fun () -> Pp.str "Compiling library..."); match mod_expr with | NoFunctor struc -> let env = add_structure mp struc empty_delta_resolver env in - let prefix = mod_uid_of_dirpath dp ^ "." in let t0 = Sys.time () in clear_global_tbl (); clear_symbols (); let mlcode = - List.fold_left (translate_field prefix mp env) [] struc + List.fold_left (translate_field mp env) [] struc in let t1 = Sys.time () in let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 8f58dfa8d3..1d0d56703d 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -15,5 +15,5 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -val dump_library : ModPath.t -> DirPath.t -> env -> module_signature -> +val dump_library : ModPath.t -> env -> module_signature -> global list * Nativevalues.symbols diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index bd6241ae67..c986cb473d 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -333,6 +333,22 @@ let rem accu x y = if is_int x && is_int y then no_check_rem x y else accu x y +let no_check_divs x y = + mk_uint (Uint63.divs (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let divs accu x y = + if is_int x && is_int y then no_check_divs x y + else accu x y + +let no_check_rems x y = + mk_uint (Uint63.rems (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let rems accu x y = + if is_int x && is_int y then no_check_rems x y + else accu x y + let no_check_l_sr x y = mk_uint (Uint63.l_sr (to_uint x) (to_uint y)) [@@ocaml.inline always] @@ -349,6 +365,14 @@ let l_sl accu x y = if is_int x && is_int y then no_check_l_sl x y else accu x y +let no_check_a_sr x y = + mk_uint (Uint63.a_sr (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let a_sr accu x y = + if is_int x && is_int y then no_check_a_sr x y + else accu x y + let no_check_l_and x y = mk_uint (Uint63.l_and (to_uint x) (to_uint y)) [@@ocaml.inline always] @@ -502,6 +526,22 @@ let le accu x y = if is_int x && is_int y then no_check_le x y else accu x y +let no_check_lts x y = + mk_bool (Uint63.lts (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let lts accu x y = + if is_int x && is_int y then no_check_lts x y + else accu x y + +let no_check_les x y = + mk_bool (Uint63.les (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let les accu x y = + if is_int x && is_int y then no_check_les x y + else accu x y + let no_check_compare x y = match Uint63.compare (to_uint x) (to_uint y) with | x when x < 0 -> (Obj.magic CmpLt:t) @@ -512,6 +552,16 @@ let compare accu x y = if is_int x && is_int y then no_check_compare x y else accu x y +let no_check_compares x y = + match Uint63.compares (to_uint x) (to_uint y) with + | x when x < 0 -> (Obj.magic CmpLt:t) + | 0 -> (Obj.magic CmpEq:t) + | _ -> (Obj.magic CmpGt:t) + +let compares accu x y = + if is_int x && is_int y then no_check_compares x y + else accu x y + let print x = Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x)); flush stderr; diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index b9b75a9d7c..98cf4219a0 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -158,9 +158,12 @@ val sub : t -> t -> t -> t val mul : t -> t -> t -> t val div : t -> t -> t -> t val rem : t -> t -> t -> t +val divs : t -> t -> t -> t +val rems : t -> t -> t -> t val l_sr : t -> t -> t -> t val l_sl : t -> t -> t -> t +val a_sr : t -> t -> t -> t val l_and : t -> t -> t -> t val l_xor : t -> t -> t -> t val l_or : t -> t -> t -> t @@ -179,7 +182,10 @@ val addMulDiv : t -> t -> t -> t -> t val eq : t -> t -> t -> t val lt : t -> t -> t -> t val le : t -> t -> t -> t +val lts : t -> t -> t -> t +val les : t -> t -> t -> t val compare : t -> t -> t -> t +val compares : t -> t -> t -> t val print : t -> t @@ -205,12 +211,21 @@ val no_check_div : t -> t -> t val no_check_rem : t -> t -> t [@@ocaml.inline always] +val no_check_divs : t -> t -> t +[@@ocaml.inline always] + +val no_check_rems : t -> t -> t +[@@ocaml.inline always] + val no_check_l_sr : t -> t -> t [@@ocaml.inline always] val no_check_l_sl : t -> t -> t [@@ocaml.inline always] +val no_check_a_sr : t -> t -> t +[@@ocaml.inline always] + val no_check_l_and : t -> t -> t [@@ocaml.inline always] @@ -253,8 +268,16 @@ val no_check_lt : t -> t -> t val no_check_le : t -> t -> t [@@ocaml.inline always] +val no_check_lts : t -> t -> t +[@@ocaml.inline always] + +val no_check_les : t -> t -> t +[@@ocaml.inline always] + val no_check_compare : t -> t -> t +val no_check_compares : t -> t -> t + (** Support for machine floating point values *) val is_float : t -> bool diff --git a/kernel/primred.ml b/kernel/primred.ml index f0b4d6d362..23b7e13ab8 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -223,10 +223,16 @@ struct let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.div i1 i2) | Int63mod -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rem i1 i2) + | Int63divs -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.divs i1 i2) + | Int63mods -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rems i1 i2) | Int63lsr -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sr i1 i2) | Int63lsl -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sl i1 i2) + | Int63asr -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.a_sr i1 i2) | Int63land -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2) | Int63lor -> @@ -276,6 +282,12 @@ struct | Int63le -> let i1, i2 = get_int2 evd args in E.mkBool env (Uint63.le i1 i2) + | Int63lts -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.lts i1 i2) + | Int63les -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.les i1 i2) | Int63compare -> let i1, i2 = get_int2 evd args in begin match Uint63.compare i1 i2 with @@ -283,6 +295,13 @@ struct | 0 -> E.mkEq env | _ -> E.mkGt env end + | Int63compares -> + let i1, i2 = get_int2 evd args in + begin match Uint63.compares i1 i2 with + | x when x < 0 -> E.mkLt env + | 0 -> E.mkEq env + | _ -> E.mkGt env + end | Float64opp -> let f = get_float1 evd args in E.mkFloat env (Float64.opp f) | Float64abs -> diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a35f94e3ce..5f83e78eb0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1273,7 +1273,7 @@ let export ?except ~output_native_objects senv dir = in let ast, symbols = if output_native_objects then - Nativelibrary.dump_library mp dir senv.env str + Nativelibrary.dump_library mp senv.env str else [], Nativevalues.empty_symbols in let lib = { diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 24aa4ed771..013892ad74 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -269,16 +269,14 @@ let build_constant_declaration env result = in Environ.really_needed env (Id.Set.union ids_typ ids_def), def | Some declared -> - let needed = Environ.really_needed env declared in - (* Transitive closure ensured by the upper layers *) - let () = assert (Id.Set.equal needed declared) in - (* We use the declared set and chain a check of correctness *) - declared, - match def with - | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *) - | Def cs as x -> - let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in - x + let declared = Environ.really_needed env declared in + (* We use the declared set and chain a check of correctness *) + declared, + match def with + | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *) + | Def cs as x -> + let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in + x in let univs = result.cook_universes in let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 6b2519918a..ff8d1eefb7 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -48,6 +48,7 @@ val l_xor : t -> t -> t val l_or : t -> t -> t (* Arithmetic operations *) +val a_sr : t -> t -> t val add : t -> t -> t val sub : t -> t -> t val mul : t -> t -> t @@ -56,6 +57,10 @@ val rem : t -> t -> t val diveucl : t -> t -> t * t + (* Signed arithmetic opeartions *) +val divs : t -> t -> t +val rems : t -> t -> t + (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t @@ -71,6 +76,11 @@ val equal : t -> t -> bool val le : t -> t -> bool val compare : t -> t -> int + (* signed comparision *) +val lts : t -> t -> bool +val les : t -> t -> bool +val compares : t -> t -> int + (* head and tail *) val head0 : t -> t val tail0 : t -> t diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 4f2cbc4262..9c8401105e 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -52,6 +52,15 @@ let lt x y = let le x y = Int64.compare x y <= 0 + (* signed comparison *) +(* We shift the arguments by 1 to the left so that the top-most bit is interpreted as a sign *) +(* The zero at the end doesn't change the order (it is stable by multiplication by 2) *) +let lts x y = + Int64.(compare (shift_left x 1) (shift_left y 1)) < 0 + +let les x y = + Int64.(compare (shift_left x 1) (shift_left y 1)) <= 0 + (* logical shift *) let l_sl x y = if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L @@ -59,6 +68,12 @@ let l_sl x y = let l_sr x y = if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L + (* arithmetic shift (for sint63) *) +let a_sr x y = + if les 0L y && lts y 63L then + mask63 (Int64.shift_right (Int64.shift_left x 1) ((Int64.to_int y) + 1)) + else 0L + let l_and x y = Int64.logand x y let l_or x y = Int64.logor x y let l_xor x y = Int64.logxor x y @@ -86,6 +101,15 @@ let rem x y = let diveucl x y = (div x y, rem x y) + (* signed division *) +let divs x y = + if y = 0L then 0L else mask63 Int64.(div (shift_left x 1) (shift_left y 1)) + + (* signed modulo *) +let rems x y = + if y = 0L then 0L else + Int64.shift_right_logical (Int64.(rem (shift_left x 1) (shift_left y 1))) 1 + let addmuldiv p x y = l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p)) @@ -139,6 +163,8 @@ let equal (x : t) y = x = y let compare x y = Int64.compare x y +let compares x y = Int64.(compare (shift_left x 1) (shift_left y 1)) + (* Number of leading zeroes *) let head0 x = let r = ref 0 in @@ -198,22 +224,30 @@ let () = Callback.register "uint63 addcarry" addcarry; Callback.register "uint63 addmuldiv" addmuldiv; Callback.register "uint63 div" div; + Callback.register "uint63 divs" divs; Callback.register "uint63 div21_ml" div21; Callback.register "uint63 eq" equal; Callback.register "uint63 eq0" (equal Int64.zero); + Callback.register "uint63 eqm1" (equal (sub zero one)); Callback.register "uint63 head0" head0; Callback.register "uint63 land" l_and; Callback.register "uint63 leq" le; + Callback.register "uint63 les" les; Callback.register "uint63 lor" l_or; Callback.register "uint63 lsl" l_sl; Callback.register "uint63 lsr" l_sr; + Callback.register "uint63 asr" a_sr; Callback.register "uint63 lt" lt; + Callback.register "uint63 lts" lts; Callback.register "uint63 lxor" l_xor; Callback.register "uint63 mod" rem; + Callback.register "uint63 mods" rems; Callback.register "uint63 mul" mul; Callback.register "uint63 mulc_ml" mulc; + Callback.register "uint63 zero" zero; Callback.register "uint63 one" one; Callback.register "uint63 sub" sub; + Callback.register "uint63 neg" (sub zero); Callback.register "uint63 subcarry" subcarry; Callback.register "uint63 tail0" tail0; Callback.register "uint63 of_float" of_float; diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 8d052d6593..d017dafd3c 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -53,6 +53,10 @@ let l_sl x y = let l_sr x y = if 0 <= y && y < 63 then x lsr y else 0 + (* arithmetic shift (for sint63) *) +let a_sr x y = + if 0 <= y && y < 63 then x asr y else 0 + let l_and x y = x land y [@@ocaml.inline always] @@ -84,6 +88,14 @@ let rem (x : int) (y : int) = let diveucl x y = (div x y, rem x y) + (* signed division *) +let divs (x : int) (y : int) = + if y = 0 then 0 else x / y + + (* modulo *) +let rems (x : int) (y : int) = + if y = 0 then 0 else x mod y + let addmuldiv p x y = l_or (l_sl x p) (l_sr y (uint_size - p)) @@ -96,6 +108,15 @@ let le (x : int) (y : int) = (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) [@@ocaml.inline always] + (* signed comparison *) +let lts (x : int) (y : int) = + x < y +[@@ocaml.inline always] + +let les (x : int) (y : int) = + x <= y +[@@ocaml.inline always] + let to_int_min n m = if lt n m then n else m [@@ocaml.inline always] @@ -175,9 +196,10 @@ let equal (x : int) (y : int) = x = y let compare (x:int) (y:int) = let x = x lxor 0x4000000000000000 in let y = y lxor 0x4000000000000000 in - if x > y then 1 - else if y > x then -1 - else 0 + Int.compare x y + +let compares (x : int) (y : int) = + Int.compare x y (* head tail *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 1432fb9310..d31d7a03b6 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -196,8 +196,9 @@ let vm_conv_gen cv_pb env univs t1 t2 = TransparentState.full env univs t1 t2 else try - let v1 = val_of_constr env t1 in - let v2 = val_of_constr env t2 in + let sigma _ = assert false in + let v1 = val_of_constr env sigma t1 in + let v2 = val_of_constr env sigma t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 20de4bc81b..7d3b3469b0 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -840,21 +840,21 @@ let dump_bytecodes init code fvs = prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ fnl ()) -let compile ~fail_on_error ?universes:(universes=0) env c = +let compile ~fail_on_error ?universes:(universes=0) env sigma c = init_fun_code (); Label.reset_label_counter (); let cont = [Kstop] in try let cenv, init_code = if Int.equal universes 0 then - let lam = lambda_of_constr ~optimize:true env c in + let lam = lambda_of_constr ~optimize:true env sigma c in let cenv = empty_comp_env () in cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. *) - let lam = lambda_of_constr ~optimize:true env c in + let lam = lambda_of_constr ~optimize:true env sigma c in let params, body = decompose_Llam lam in let arity = Array.length params in let cenv = empty_comp_env () in @@ -896,7 +896,8 @@ let compile_constant_body ~fail_on_error env univs = function let con= Constant.make1 (Constant.canonical kn') in Some (BCalias (get_alias env con)) | _ -> - let res = compile ~fail_on_error ~universes:instance_size env body in + let sigma _ = assert false in + let res = compile ~fail_on_error ~universes:instance_size env sigma body in Option.map (fun x -> BCdefined (to_memory x)) res (* Shortcut of the previous function used during module strengthening *) diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli index aef7ac3d6b..c724cad5ec 100644 --- a/kernel/vmbytegen.mli +++ b/kernel/vmbytegen.mli @@ -15,8 +15,10 @@ open Declarations open Environ (** Should only be used for monomorphic terms *) -val compile : fail_on_error:bool -> - ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option +val compile : + fail_on_error:bool -> ?universes:int -> + env -> (existential -> constr option) -> constr -> + (bytecodes * bytecodes * fv) option (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index d3af8bf09b..caa263432e 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -226,8 +226,11 @@ let check_prim_op = function | Int63mul -> opCHECKMULINT63 | Int63div -> opCHECKDIVINT63 | Int63mod -> opCHECKMODINT63 + | Int63divs -> opCHECKDIVSINT63 + | Int63mods -> opCHECKMODSINT63 | Int63lsr -> opCHECKLSRINT63 | Int63lsl -> opCHECKLSLINT63 + | Int63asr -> opCHECKASRINT63 | Int63land -> opCHECKLANDINT63 | Int63lor -> opCHECKLORINT63 | Int63lxor -> opCHECKLXORINT63 @@ -242,7 +245,10 @@ let check_prim_op = function | Int63eq -> opCHECKEQINT63 | Int63lt -> opCHECKLTINT63 | Int63le -> opCHECKLEINT63 + | Int63lts -> opCHECKLTSINT63 + | Int63les -> opCHECKLESINT63 | Int63compare -> opCHECKCOMPAREINT63 + | Int63compares -> opCHECKCOMPARESINT63 | Float64opp -> opCHECKOPPFLOAT | Float64abs -> opCHECKABSFLOAT | Float64eq -> opCHECKEQFLOAT diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 91de58b0e6..e353348ac7 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -591,12 +591,14 @@ struct type t = { global_env : env; + evar_body : existential -> constr option; name_rel : Name.t Vect.t; construct_tbl : (constructor, constructor_info) Hashtbl.t; } - let make env = { + let make env sigma = { global_env = env; + evar_body = sigma; name_rel = Vect.make 16 Anonymous; construct_tbl = Hashtbl.create 111 } @@ -633,9 +635,13 @@ open Renv let rec lambda_of_constr env c = match Constr.kind c with | Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta") - | Evar (evk, args) -> - let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in - Levar (evk, args) + | Evar (evk, args as ev) -> + begin match env.evar_body ev with + | None -> + let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in + Levar (evk, args) + | Some t -> lambda_of_constr env t + end | Cast (c, _, _) -> lambda_of_constr env c @@ -774,8 +780,8 @@ let optimize_lambda lam = let lam = simplify subst_id lam in remove_let subst_id lam -let lambda_of_constr ~optimize genv c = - let env = Renv.make genv in +let lambda_of_constr ~optimize genv sigma c = + let env = Renv.make genv sigma in let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli index ad5f81638f..03d3393219 100644 --- a/kernel/vmlambda.mli +++ b/kernel/vmlambda.mli @@ -33,7 +33,7 @@ and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array exception TooLargeInductive of Pp.t -val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda +val lambda_of_constr : optimize:bool -> env -> (existential -> constr option) -> Constr.t -> lambda val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml index ae0fa38571..90ee1c5378 100644 --- a/kernel/vmsymtable.ml +++ b/kernel/vmsymtable.ml @@ -144,7 +144,7 @@ let slot_for_proj_name key = ProjNameTable.add proj_name_tbl key n; n -let rec slot_for_getglobal env kn = +let rec slot_for_getglobal env sigma kn = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> @@ -155,22 +155,22 @@ let rec slot_for_getglobal env kn = | Some code -> match Vmemitcodes.force code with | BCdefined(code,pl,fv) -> - let v = eval_to_patch env (code,pl,fv) in + let v = eval_to_patch env sigma (code,pl,fv) in set_global v - | BCalias kn' -> slot_for_getglobal env kn' + | BCalias kn' -> slot_for_getglobal env sigma kn' | BCconstant -> set_global (val_of_constant kn) in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (CEphemeron.create pos); pos -and slot_for_fv env fv = +and slot_for_fv env sigma fv = let fill_fv_cache cache id v_of_id env_of_id b = let v,d = match b with | None -> v_of_id id, Id.Set.empty | Some c -> - val_of_constr (env_of_id id env) c, + val_of_constr (env_of_id id env) sigma c, Environ.global_vars_set env c in build_lazy_val cache (v, d); v in let val_of_rel i = val_of_rel (nb_rel env - i) in @@ -194,11 +194,11 @@ and slot_for_fv env fv = | FVuniv_var _idu -> assert false -and eval_to_patch env (buff,pl,fv) = +and eval_to_patch env sigma (buff,pl,fv) = let slots = function | Reloc_annot a -> slot_for_annot a | Reloc_const sc -> slot_for_str_cst sc - | Reloc_getglobal kn -> slot_for_getglobal env kn + | Reloc_getglobal kn -> slot_for_getglobal env sigma kn | Reloc_proj_name p -> slot_for_proj_name p | Reloc_caml_prim op -> slot_for_caml_prim op in @@ -207,13 +207,13 @@ and eval_to_patch env (buff,pl,fv) = (* Environment should look like a closure, so free variables start at slot 2. *) let a = Array.make (Array.length fv + 2) crazy_val in a.(1) <- Obj.magic 2; - Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env v) fv; + Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env sigma v) fv; a in eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env -and val_of_constr env c = - match compile ~fail_on_error:true env c with - | Some v -> eval_to_patch env (to_memory v) +and val_of_constr env sigma c = + match compile ~fail_on_error:true env sigma c with + | Some v -> eval_to_patch env sigma (to_memory v) | None -> assert false let set_transparent_const _kn = () (* !?! *) diff --git a/kernel/vmsymtable.mli b/kernel/vmsymtable.mli index e480bfcec1..c6dc09d944 100644 --- a/kernel/vmsymtable.mli +++ b/kernel/vmsymtable.mli @@ -14,7 +14,7 @@ open Names open Constr open Environ -val val_of_constr : env -> constr -> Vmvalues.values +val val_of_constr : env -> (existential -> constr option) -> constr -> Vmvalues.values val set_opaque_const : Constant.t -> unit val set_transparent_const : Constant.t -> unit |