diff options
| author | Maxime Dénès | 2018-02-16 01:02:17 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-04 13:12:40 +0000 |
| commit | e43b1768d0f8399f426b92f4dfe31955daceb1a4 (patch) | |
| tree | d46d10f8893205750e7238e69512736243315ef6 /kernel | |
| parent | a1b7f53a68c9ccae637f2c357fbe50a09e211a4a (diff) | |
Primitive integers
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'kernel')
65 files changed, 3015 insertions, 2361 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index be2b05da8d..0865487c98 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -36,20 +36,15 @@ void init_arity () { arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]= arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]= arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]= - arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]= + arity[APPLY3]=arity[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]= arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= - arity[ADDINT31]=arity[ADDCINT31]=arity[ADDCARRYCINT31]= - arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]= - arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]= - arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]= - arity[HEAD0INT31]=arity[TAIL0INT31]= - arity[COMPINT31]=arity[DECOMPINT31]= - arity[ORINT31]=arity[ANDINT31]=arity[XORINT31]=0; + arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= + arity[ISINT]=arity[AREINT2]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= @@ -58,10 +53,20 @@ void init_arity () { 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[ISCONST]=arity[ENSURESTACKCAPACITY]=1; + 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[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= + arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= + arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[ARECONST]=arity[PROJ]=2; + arity[PROJ]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 638d6b5ab5..5a233e6178 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -29,6 +29,7 @@ void init_arity(); value coq_tcode_of_code(value code); value coq_makeaccu (value i); value coq_pushpop (value i); +value coq_accucond (value i); value coq_is_accumulate_code(value code); #endif /* _COQ_FIX_CODE_ */ diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index d92e85fdf8..c7abedaed6 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -26,7 +26,7 @@ enum instructions { ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC, PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC, PUSH_RETADDR, - APPLY, APPLY1, APPLY2, APPLY3, + APPLY, APPLY1, APPLY2, APPLY3, APPLY4, APPTERM, APPTERM1, APPTERM2, APPTERM3, RETURN, RESTART, GRAB, GRABREC, CLOSURE, CLOSUREREC, CLOSURECOFIX, @@ -46,15 +46,21 @@ enum instructions { MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, /* spiwack: */ BRANCH, - ADDINT31, ADDCINT31, ADDCARRYCINT31, - SUBINT31, SUBCINT31, SUBCARRYCINT31, - MULCINT31, MULINT31, DIV21INT31, DIVINT31, - ADDMULDIVINT31, COMPAREINT31, - HEAD0INT31, TAIL0INT31, - ISCONST, ARECONST, - COMPINT31, DECOMPINT31, - ORINT31, ANDINT31, XORINT31, -/* /spiwack */ + CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63, + CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63, + CHECKMULINT63, CHECKMULCINT63, + CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63, + CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63, + CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63, + CHECKLSLINT63CONST1, CHECKLSRINT63CONST1, + + CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63, + CHECKCOMPAREINT63, + + CHECKHEAD0INT63, CHECKTAIL0INT63, + + ISINT, AREINT2, + STOP }; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a944dbb06c..d2c88bffcc 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,6 +23,12 @@ #include "coq_memory.h" #include "coq_values.h" +#ifdef ARCH_SIXTYFOUR +#include "coq_uint63_native.h" +#else +#include "coq_uint63_emul.h" +#endif + /* spiwack: I append here a few macros for value/number manipulation */ #define uint32_of_value(val) (((uint32_t)(val)) >> 1) #define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1)) @@ -155,6 +161,38 @@ if (sp - num_args < coq_stack_threshold) { \ #endif #endif +#define CheckInt1() do{ \ + if (Is_uint63(accu)) pc++; \ + else{ \ + *--sp=accu; \ + accu = Field(coq_global_data, *pc++); \ + goto apply1; \ + } \ + }while(0) + +#define CheckInt2() do{ \ + if (Is_uint63(accu) && Is_uint63(sp[0])) pc++; \ + else{ \ + *--sp=accu; \ + accu = Field(coq_global_data, *pc++); \ + goto apply2; \ + } \ + }while(0) + + + +#define CheckInt3() do{ \ + if (Is_uint63(accu) && Is_uint63(sp[0]) && Is_uint63(sp[1]) ) pc++; \ + else{ \ + *--sp=accu; \ + accu = Field(coq_global_data, *pc++); \ + goto apply3; \ + } \ + }while(0) + +#define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0) +#define AllocPair() Alloc_small(accu, 2, coq_tag_pair) + /* For signal handling, we hijack some code from the caml runtime */ extern intnat caml_signals_are_pending; @@ -372,8 +410,10 @@ value coq_interprete goto check_stack; } Instruct(APPLY1) { - value arg1 = sp[0]; + value arg1; + apply1: print_instr("APPLY1"); + arg1 = sp[0]; sp -= 3; sp[0] = arg1; sp[1] = (value)pc; @@ -388,10 +428,14 @@ value coq_interprete coq_extra_args = 0; goto check_stack; } + Instruct(APPLY2) { - value arg1 = sp[0]; - value arg2 = sp[1]; + value arg1; + value arg2; + apply2: print_instr("APPLY2"); + arg1 = sp[0]; + arg2 = sp[1]; sp -= 3; sp[0] = arg1; sp[1] = arg2; @@ -403,11 +447,16 @@ value coq_interprete coq_extra_args = 1; goto check_stack; } + Instruct(APPLY3) { - value arg1 = sp[0]; - value arg2 = sp[1]; - value arg3 = sp[2]; + value arg1; + value arg2; + value arg3; + apply3: print_instr("APPLY3"); + arg1 = sp[0]; + arg2 = sp[1]; + arg3 = sp[2]; sp -= 3; sp[0] = arg1; sp[1] = arg2; @@ -420,7 +469,28 @@ value coq_interprete coq_extra_args = 2; goto check_stack; } - /* Stack checks */ + + Instruct(APPLY4) { + value arg1 = sp[0]; + value arg2 = sp[1]; + value arg3 = sp[2]; + value arg4 = sp[3]; + print_instr("APPLY4"); + sp -= 3; + sp[0] = arg1; + sp[1] = arg2; + sp[2] = arg3; + sp[3] = arg4; + sp[4] = (value)pc; + sp[5] = coq_env; + sp[6] = Val_long(coq_extra_args); + pc = Code_val(accu); + coq_env = accu; + coq_extra_args = 3; + goto check_stack; + } + + /* Stack checks */ check_stack: print_instr("check_stack"); @@ -1127,7 +1197,6 @@ value coq_interprete Next; } - /* spiwack: code for interpreting compiled integers */ Instruct(BRANCH) { /* unconditional branching */ print_instr("BRANCH"); @@ -1136,338 +1205,339 @@ value coq_interprete Next; } - Instruct(ADDINT31) { + 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("ADDINT31"); - accu = - (value)((uint32_t) accu + (uint32_t) *sp++ - 1); - /* nota,unlike CaML we don't want - to have a different behavior depending on the - architecture. Thus we cast the operand to uint32 */ + print_instr("ADDINT63"); + accu = uint63_add(accu, *sp++); Next; } - Instruct (ADDCINT31) { - print_instr("ADDCINT31"); + Instruct (CHECKADDCINT63) { + print_instr("CHECKADDCINT63"); + CheckInt2(); /* returns the sum with a carry */ - uint32_t s; - s = (uint32_t)accu + (uint32_t)*sp++ - 1; - if( (uint32_t)s < (uint32_t)accu ) { - /* carry */ - Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */ - } - else { - /*no carry */ - Alloc_small(accu, 1, 1); - } - Field(accu, 0)=(value)s; + value s; + s = uint63_add(accu, *sp++); + AllocCarry(uint63_lt(s,accu)); + Field(accu, 0) = s; Next; } - Instruct (ADDCARRYCINT31) { - print_instr("ADDCARRYCINT31"); + Instruct (CHECKADDCARRYCINT63) { + print_instr("ADDCARRYCINT63"); + CheckInt2(); /* returns the sum plus one with a carry */ - uint32_t s; - s = (uint32_t)accu + (uint32_t)*sp++ + 1; - if( (uint32_t)s <= (uint32_t)accu ) { - /* carry */ - Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */ - } - else { - /*no carry */ - Alloc_small(accu, 1, 1); - } - Field(accu, 0)=(value)s; + value s; + s = uint63_addcarry(accu, *sp++); + AllocCarry(uint63_leq(s, accu)); + Field(accu, 0) = s; Next; } - Instruct (SUBINT31) { - print_instr("SUBINT31"); + Instruct (CHECKSUBINT63) { + print_instr("CHECKSUBINT63"); + CheckInt2(); + } + Instruct (SUBINT63) { + print_instr("SUBINT63"); /* returns the subtraction */ - accu = - (value)((uint32_t) accu - (uint32_t) *sp++ + 1); + accu = uint63_sub(accu, *sp++); Next; } - Instruct (SUBCINT31) { - print_instr("SUBCINT31"); + Instruct (CHECKSUBCINT63) { + print_instr("SUBCINT63"); + CheckInt2(); /* returns the subtraction with a carry */ - uint32_t b; - uint32_t s; - b = (uint32_t)*sp++; - s = (uint32_t)accu - b + 1; - if( (uint32_t)accu < b ) { - /* carry */ - Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */ - } - else { - /*no carry */ - Alloc_small(accu, 1, 1); - } - Field(accu, 0)=(value)s; + value b; + value s; + b = *sp++; + s = uint63_sub(accu,b); + AllocCarry(uint63_lt(accu,b)); + Field(accu, 0) = s; Next; } - Instruct (SUBCARRYCINT31) { - print_instr("SUBCARRYCINT31"); + Instruct (CHECKSUBCARRYCINT63) { + print_instr("SUBCARRYCINT63"); + CheckInt2(); /* returns the subtraction minus one with a carry */ - uint32_t b; - uint32_t s; - b = (uint32_t)*sp++; - s = (value)((uint32_t)accu - b - 1); - if( (uint32_t)accu <= b ) { - /* carry */ - Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */ - } - else { - /*no carry */ - Alloc_small(accu, 1, 1); - } - Field(accu, 0)=(value)s; + value b; + value s; + b = *sp++; + s = uint63_subcarry(accu,b); + AllocCarry(uint63_leq(accu,b)); + Field(accu, 0) = s; Next; } - Instruct (MULINT31) { + Instruct (CHECKMULINT63) { + print_instr("MULINT63"); + CheckInt2(); /* returns the multiplication */ - print_instr("MULINT31"); - accu = - value_of_uint32((uint32_of_value(accu)) * (uint32_of_value(*sp++))); + accu = uint63_mul(accu,*sp++); Next; } - Instruct (MULCINT31) { - /*returns the multiplication on a double size word - (special case for 0) */ - print_instr("MULCINT31"); - uint64_t p; + Instruct (CHECKMULCINT63) { + /*returns the multiplication on a pair */ + print_instr("MULCINT63"); + CheckInt2(); /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */ - p = UI64_of_value (accu) * UI64_of_uint32 ((*sp++)^1); - if (p == 0) { - accu = (value)1; + /* TODO: implement + p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1)); + AllocPair(); */ + /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/ + /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/ + value x = accu; + AllocPair(); + Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0)); + Next; + } + + Instruct(CHECKDIVINT63) { + print_instr("CHEKDIVINT63"); + CheckInt2(); + /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag + since it probably only concerns negative number. + needs to be checked at this point */ + value divisor; + divisor = *sp++; + if (uint63_eq0(divisor)) { + accu = divisor; } else { - /* the output type is supposed to have a constant constructor - and a non-constant constructor (in that order), the tag - of the non-constant constructor is then 1 */ - Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - /*unsigned shift*/ - Field(accu, 0) = (value)((p >> 31)|1) ; /*higher part*/ - Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/ - } + accu = uint63_div(accu, divisor); + } Next; } - Instruct (DIV21INT31) { - print_instr("DIV21INT31"); - /* spiwack: takes three int31 (the two first ones represent an - int62) and performs the euclidian division of the - int62 by the int31 */ - uint64_t bigint; - bigint = UI64_of_value(accu); - bigint = (bigint << 31) | UI64_of_value(*sp++); - uint64_t divisor; - divisor = UI64_of_value(*sp++); - Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - if (divisor == 0) { - Field(accu, 0) = 1; /* 2*0+1 */ - Field(accu, 1) = 1; /* 2*0+1 */ + Instruct(CHECKMODINT63) { + print_instr("CHEKMODINT63"); + CheckInt2(); + value divisor; + divisor = *sp++; + if (uint63_eq0(divisor)) { + accu = divisor; } - else { - uint64_t quo, mod; - quo = bigint / divisor; - mod = bigint % divisor; - Field(accu, 0) = value_of_uint32((uint32_t)(quo)); - Field(accu, 1) = value_of_uint32((uint32_t)(mod)); + else { + accu = uint63_mod(accu,divisor); } Next; } - Instruct (DIVINT31) { - print_instr("DIVINT31"); + Instruct (CHECKDIVEUCLINT63) { + print_instr("DIVEUCLINT63"); + CheckInt2(); /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag since it probably only concerns negative number. needs to be checked at this point */ - uint32_t divisor; - divisor = uint32_of_value(*sp++); - if (divisor == 0) { + value divisor; + divisor = *sp++; + if (uint63_eq0(divisor)) { Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - Field(accu, 0) = 1; /* 2*0+1 */ - Field(accu, 1) = 1; /* 2*0+1 */ + Field(accu, 0) = divisor; + Field(accu, 1) = divisor; } else { - uint32_t modulus; - modulus = uint32_of_value(accu); + value modulus; + modulus = accu; Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - Field(accu, 0) = value_of_uint32(modulus/divisor); - Field(accu, 1) = value_of_uint32(modulus%divisor); + Field(accu, 0) = uint63_div(modulus,divisor); + Field(accu, 1) = uint63_mod(modulus,divisor); } Next; } - Instruct (ADDMULDIVINT31) { - print_instr("ADDMULDIVINT31"); - /* higher level shift (does shifts and cycles and such) */ - uint32_t shiftby; - shiftby = uint32_of_value(accu); - if (shiftby > 31) { - if (shiftby < 62) { - sp++; - accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1); - } - else { - sp+=2; - accu = (value)(1); - } + Instruct (CHECKDIV21INT63) { + print_instr("DIV21INT63"); + CheckInt3(); + /* spiwack: takes three int31 (the two first ones represent an + int62) and performs the euclidian division of the + int62 by the int31 */ + /* TODO: implement this + bigint = UI64_of_value(accu); + bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++)); + uint64 divisor; + divisor = UI64_of_value(*sp++); + Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */ + /* if (I64_is_zero (divisor)) { + Field(accu, 0) = 1; */ /* 2*0+1 */ + /* Field(accu, 1) = 1; */ /* 2*0+1 */ + /* } + else { + uint64 quo, mod; + I64_udivmod(bigint, divisor, &quo, &mod); + Field(accu, 0) = value_of_uint32(I64_to_int32(quo)); + Field(accu, 1) = value_of_uint32(I64_to_int32(mod)); + } */ + value bigint; /* TODO: fix */ + bigint = *sp++; /* TODO: take accu into account */ + value divisor; + divisor = *sp++; + if (uint63_eq0(divisor)) { + Alloc_small(accu, 2, 1); + Field(accu, 0) = divisor; + Field(accu, 1) = divisor; } - else{ - /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */ - accu = (value)((((uint32_t)*sp++)^1) << shiftby); - /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */ - accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1); + else { + value quo, mod; + mod = uint63_div21(accu, bigint, divisor, &quo); + Alloc_small(accu, 2, 1); + Field(accu, 0) = quo; + Field(accu, 1) = mod; } Next; } - Instruct (COMPAREINT31) { - /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ - /* assumes Inductive _ : _ := Eq | Lt | Gt */ - print_instr("COMPAREINT31"); - if ((uint32_t)accu == (uint32_t)*sp) { - accu = 1; /* 2*0+1 */ - sp++; - } - else{if ((uint32_t)accu < (uint32_t)(*sp++)) { - accu = 3; /* 2*1+1 */ - } - else{ - accu = 5; /* 2*2+1 */ - }} + Instruct(CHECKLXORINT63) { + print_instr("CHECKLXORINT63"); + CheckInt2(); + accu = uint63_lxor(accu,*sp++); Next; } - - Instruct (HEAD0INT31) { - int r = 0; - uint32_t x; - print_instr("HEAD0INT31"); - x = (uint32_t) accu; - if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; } - if (!(x & 0xFF000000)) { x <<= 8; r += 8; } - if (!(x & 0xF0000000)) { x <<= 4; r += 4; } - if (!(x & 0xC0000000)) { x <<= 2; r += 2; } - if (!(x & 0x80000000)) { x <<=1; r += 1; } - if (!(x & 0x80000000)) { r += 1; } - accu = value_of_uint32(r); + + Instruct(CHECKLORINT63) { + print_instr("CHECKLORINT63"); + CheckInt2(); + accu = uint63_lor(accu,*sp++); Next; } - - Instruct (TAIL0INT31) { - int r = 0; - uint32_t x; - print_instr("TAIL0INT31"); - x = (((uint32_t) accu >> 1) | 0x80000000); - if (!(x & 0xFFFF)) { x >>= 16; r += 16; } - if (!(x & 0x00FF)) { x >>= 8; r += 8; } - if (!(x & 0x000F)) { x >>= 4; r += 4; } - if (!(x & 0x0003)) { x >>= 2; r += 2; } - if (!(x & 0x0001)) { x >>=1; r += 1; } - if (!(x & 0x0001)) { r += 1; } - accu = value_of_uint32(r); + + Instruct(CHECKLANDINT63) { + print_instr("CHECKLANDINT63"); + CheckInt2(); + accu = uint63_land(accu,*sp++); Next; } - Instruct (ISCONST) { - /* Branches if the accu does not contain a constant - (i.e., a non-block value) */ - print_instr("ISCONST"); - if ((accu & 1) == 0) /* last bit is 0 -> it is a block */ - pc += *pc; - else - pc++; + Instruct(CHECKLSLINT63) { + print_instr("CHECKLSLINT63"); + CheckInt2(); + value p = *sp++; + accu = uint63_lsl(accu,p); Next; + } + Instruct(CHECKLSRINT63) { + print_instr("CHECKLSRINT63"); + CheckInt2(); + value p = *sp++; + accu = uint63_lsr(accu,p); + Next; } - Instruct (ARECONST) { - /* Branches if the n first values on the stack are not - all constansts */ - print_instr("ARECONST"); - int i, n, ok; - ok = 1; - n = *pc++; - for(i=0; i < n; i++) { - if ((sp[i] & 1) == 0) { - ok = 0; - break; - } + Instruct(CHECKLSLINT63CONST1) { + print_instr("CHECKLSLINT63CONST1"); + if (Is_uint63(accu)) { + pc++; + accu = uint63_lsl1(accu); + Next; + } else { + *--sp = uint63_one(); + *--sp = accu; + accu = Field(coq_global_data, *pc++); + goto apply2; } - if(ok) pc++; else pc += *pc; + } + + Instruct(CHECKLSRINT63CONST1) { + print_instr("CHECKLSRINT63CONST1"); + if (Is_uint63(accu)) { + pc++; + accu = uint63_lsr1(accu); + Next; + } else { + *--sp = uint63_one(); + *--sp = accu; + accu = Field(coq_global_data, *pc++); + goto apply2; + } + } + + Instruct (CHECKADDMULDIVINT63) { + print_instr("CHECKADDMULDIVINT63"); + CheckInt3(); + value x; + value y; + x = *sp++; + y = *sp++; + accu = uint63_addmuldiv(accu,x,y); Next; } - Instruct (COMPINT31) { - /* makes an 31-bit integer out of the accumulator and - the 30 first values of the stack - and put it in the accumulator (the accumulator then the - topmost get to be the heavier bits) */ - print_instr("COMPINT31"); - int i; - /*accu=accu or accu = (value)((unsigned long)1-accu) if bool - is used for the bits */ - for(i=0; i < 30; i++) { - accu = (value) ((((uint32_t)accu-1) << 1) | *sp++); - /* -1 removes the tag bit, << 1 multiplies the value by 2, - | *sp++ pops the last value and add it (no carry involved) - not that it reintroduces a tag bit */ - /* alternative, if bool is used for the bits : - accu = (value) ((((unsigned long)accu) << 1) & !*sp++); */ + Instruct (CHECKEQINT63) { + print_instr("CHECKEQINT63"); + CheckInt2(); + accu = uint63_eq(accu,*sp++) ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLTINT63) { + print_instr("CHECKLTINT63"); + CheckInt2(); + } + Instruct (LTINT63) { + print_instr("LTINT63"); + accu = uint63_lt(accu,*sp++) ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLEINT63) { + print_instr("CHECKLEINT63"); + CheckInt2(); + } + Instruct (LEINT63) { + print_instr("LEINT63"); + accu = uint63_leq(accu,*sp++) ? 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 */ + print_instr("CHECKCOMPAREINT63"); + CheckInt2(); + if (uint63_eq(accu,*sp)) { + accu = coq_Eq; + sp++; } + else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt; Next; } - Instruct (DECOMPINT31) { - /* builds a block out of a 31-bit integer (from the accumulator), - used before cases */ - int i; - value block; - print_instr("DECOMPINT31"); - Alloc_small(block, 31, 1); // Alloc_small(*, size, tag) - for(i = 30; i >= 0; i--) { - Field(block, i) = (value)(accu & 3); /* two last bits of the accumulator */ - //Field(block, i) = 3; - accu = (value) ((uint32_t)accu >> 1) | 1; /* last bit must be a one */ - }; - accu = block; + Instruct (CHECKHEAD0INT63) { + print_instr("CHECKHEAD0INT63"); + CheckInt1(); + accu = uint63_head0(accu); Next; } - Instruct (ORINT31) { - /* returns the bitwise or */ - print_instr("ORINT31"); - accu = - value_of_uint32((uint32_of_value(accu)) | (uint32_of_value(*sp++))); - Next; + Instruct (CHECKTAIL0INT63) { + print_instr("CHECKTAIL0INT63"); + CheckInt1(); + accu = uint63_tail0(accu); + Next; } - Instruct (ANDINT31) { - /* returns the bitwise and */ - print_instr("ANDINT31"); - accu = - value_of_uint32((uint32_of_value(accu)) & (uint32_of_value(*sp++))); + Instruct (ISINT){ + print_instr("ISINT"); + accu = (Is_uint63(accu)) ? coq_true : coq_false; Next; } - Instruct (XORINT31) { - /* returns the bitwise xor */ - print_instr("XORINT31"); - accu = - value_of_uint32((uint32_of_value(accu)) ^ (uint32_of_value(*sp++))); + Instruct (AREINT2){ + print_instr("AREINT2"); + accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false; + sp++; Next; } - /* /spiwack */ - - /* Debugging and machine control */ diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h new file mode 100644 index 0000000000..5499f124a2 --- /dev/null +++ b/kernel/byterun/coq_uint63_emul.h @@ -0,0 +1,97 @@ +# pragma once + +# include <caml/callback.h> +# include <caml/stack.h> + + +#define Is_uint63(v) (Tag_val(v) == Custom_tag) + +# define DECLARE_NULLOP(name) \ +value uint63_##name() { \ + static value* cb = 0; \ + CAMLparam0(); \ + if (!cb) cb = caml_named_value("uint63 " #name); \ + CAMLreturn(*cb); \ + } + +# define DECLARE_UNOP(name) \ +value uint63_##name(value x) { \ + static value* cb = 0; \ + CAMLparam1(x); \ + if (!cb) cb = caml_named_value("uint63 " #name); \ + CAMLreturn(caml_callback(*cb, x)); \ + } + +# define DECLARE_PREDICATE(name) \ +value uint63_##name(value x) { \ + static value* cb = 0; \ + CAMLparam1(x); \ + if (!cb) cb = caml_named_value("uint63 " #name); \ + CAMLreturn(Int_val(caml_callback(*cb, x))); \ + } + +# define DECLARE_BINOP(name) \ +value uint63_##name(value x, value y) { \ + static value* cb = 0; \ + CAMLparam2(x, y); \ + if (!cb) cb = caml_named_value("uint63 " #name); \ + CAMLreturn(caml_callback2(*cb, x, y)); \ + } + +# define DECLARE_RELATION(name) \ +value uint63_##name(value x, value y) { \ + static value* cb = 0; \ + CAMLparam2(x, y); \ + if (!cb) cb = caml_named_value("uint63 " #name); \ + CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \ + } + +# define DECLARE_TEROP(name) \ +value uint63_##name(value x, value y, value z) { \ + static value* cb = 0; \ + CAMLparam3(x, y, z); \ + if (!cb) cb = caml_named_value("uint63 " #name); \ + CAMLreturn(caml_callback3(*cb, x, y, z)); \ + } + + +DECLARE_NULLOP(one) +DECLARE_BINOP(add) +DECLARE_BINOP(addcarry) +DECLARE_TEROP(addmuldiv) +DECLARE_BINOP(div) +DECLARE_TEROP(div21_ml) +DECLARE_RELATION(eq) +DECLARE_PREDICATE(eq0) +DECLARE_UNOP(head0) +DECLARE_BINOP(land) +DECLARE_RELATION(leq) +DECLARE_BINOP(lor) +DECLARE_BINOP(lsl) +DECLARE_UNOP(lsl1) +DECLARE_BINOP(lsr) +DECLARE_UNOP(lsr1) +DECLARE_RELATION(lt) +DECLARE_BINOP(lxor) +DECLARE_BINOP(mod) +DECLARE_BINOP(mul) +DECLARE_BINOP(mulc_ml) +DECLARE_BINOP(sub) +DECLARE_BINOP(subcarry) +DECLARE_UNOP(tail0) + +value uint63_div21(value x, value y, value z, value* q) { + CAMLparam3(x, y, z); + CAMLlocal1(qr); + qr = uint63_div21_ml(x, y, z); + *q = Field(qr, 0); + CAMLreturn(Field(qr, 1)); +} + +value uint63_mulc(value x, value y, value* h) { + CAMLparam2(x, y); + CAMLlocal1(hl); + hl = uint63_mulc_ml(x, y); + *h = Field(hl, 0); + CAMLreturn(Field(hl, 1)); +} diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h new file mode 100644 index 0000000000..92f4dc79bc --- /dev/null +++ b/kernel/byterun/coq_uint63_native.h @@ -0,0 +1,125 @@ +#define Is_uint63(v) (Is_long(v)) + +#define uint63_of_value(val) ((uint64_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_one() ((value) 3) /* 2*1 + 1 */ + +#define uint63_eq(x,y) ((x) == (y)) +#define uint63_eq0(x) ((x) == (uint64_t)1) +#define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y)) +#define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y)) + +#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1)) +#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1)) +#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1)) +#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1)) +#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y))) +#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y))) +#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y))) + +#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) +#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y))) +#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y))) + +/* TODO: is + or | better? OCAML uses + */ +/* TODO: is - or ^ better? */ +#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero) +#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero) +#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1)) +#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1)) + +/* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ +/* (modulo 2^63) for p <= 63 */ +value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) { + uint64_t shiftby = uint63_of_value(p); + value r = (value)((uint64_t)(x^1) << shiftby); + r |= ((uint64_t)y >> (63-shiftby)) | 1; + return r; +} + +value uint63_head0(uint64_t x) { + int r = 0; + if (!(x & 0xFFFFFFFF00000000)) { x <<= 32; r += 32; } + if (!(x & 0xFFFF000000000000)) { x <<= 16; r += 16; } + if (!(x & 0xFF00000000000000)) { x <<= 8; r += 8; } + if (!(x & 0xF000000000000000)) { x <<= 4; r += 4; } + if (!(x & 0xC000000000000000)) { x <<= 2; r += 2; } + if (!(x & 0x8000000000000000)) { x <<=1; r += 1; } + return Val_int(r); +} + +value uint63_tail0(value x) { + int r = 0; + x = (uint64_t)x >> 1; + if (!(x & 0xFFFFFFFF)) { x >>= 32; r += 32; } + if (!(x & 0x0000FFFF)) { x >>= 16; r += 16; } + if (!(x & 0x000000FF)) { x >>= 8; r += 8; } + if (!(x & 0x0000000F)) { x >>= 4; r += 4; } + if (!(x & 0x00000003)) { x >>= 2; r += 2; } + if (!(x & 0x00000001)) { x >>=1; r += 1; } + return Val_int(r); +} + +value uint63_mulc(value x, value y, value* h) { + x = (uint64_t)x >> 1; + y = (uint64_t)y >> 1; + uint64_t lx = x & 0xFFFFFFFF; + uint64_t ly = y & 0xFFFFFFFF; + uint64_t hx = x >> 32; + uint64_t hy = y >> 32; + uint64_t hr = hx * hy; + uint64_t lr = lx * ly; + lx *= hy; + ly *= hx; + hr += (lx >> 32) + (ly >> 32); + lx <<= 32; + lr += lx; + if (lr < lx) { hr++; } + ly <<= 32; + lr += ly; + if (lr < ly) { hr++; } + hr = (hr << 1) | (lr >> 63); + *h = Val_int(hr); + return Val_int(lr); +} + +#define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl))) +#define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl))) + +value uint63_div21(value xh, value xl, value y, value* q) { + xh = (uint64_t)xh >> 1; + xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63); + xh = (uint64_t)xh >> 1; + uint64_t maskh = 0; + uint64_t maskl = 1; + uint64_t dh = 0; + uint64_t dl = (uint64_t)y >> 1; + int cmp = 1; + while (dh >= 0 && cmp) { + cmp = lt128(dh,dl,xh,xl); + dh = (dh << 1) | (dl >> 63); + dl = dl << 1; + maskh = (maskh << 1) | (maskl >> 63); + maskl = maskl << 1; + } + uint64_t remh = xh; + uint64_t reml = xl; + uint64_t quotient = 0; + while (maskh | maskl) { + if (le128(dh,dl,remh,reml)) { + quotient = quotient | maskl; + if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;} + reml = reml - dl; + } + maskl = (maskl >> 1) | (maskh << 63); + maskh = maskh >> 1; + dl = (dl >> 1) | (dh << 63); + dh = dh >> 1; + } + *q = Val_int(quotient); + return Val_int(reml); +} diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index bb0f0eb5e4..0cf6ccf532 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -28,6 +28,16 @@ /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) - #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) + +/* */ +#define coq_tag_C1 2 +#define coq_tag_C0 1 +#define coq_tag_pair 1 +#define coq_true Val_int(0) +#define coq_false Val_int(1) +#define coq_Eq Val_int(0) +#define coq_Lt Val_int(1) +#define coq_Gt Val_int(2) + #endif /* _COQ_VALUES_ */ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 196bb16f32..5fec55fea1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -28,8 +28,9 @@ open Util open Pp open Names open Constr -open Vars +open Declarations open Environ +open Vars open Esubst let stats = ref false @@ -303,6 +304,7 @@ and fterm = | FProd of Name.t * fconstr * constr * fconstr subs | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs + | FInt of Uint63.t | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -335,19 +337,22 @@ type clos_infos = { i_flags : reds; i_cache : infos_cache } -type clos_tab = fconstr KeyTable.t +type clos_tab = fconstr constant_def KeyTable.t let info_flags info = info.i_flags let info_env info = info.i_cache.i_env (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) +type 'a next_native_args = (CPrimitives.arg_kind * 'a) list type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of Projection.Repr.t | Zfix of fconstr * stack + | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args + (* operator, constr def, arguments already seen (in rev order), next arguments *) | Zshift of int | Zupdate of fconstr @@ -358,7 +363,7 @@ let append_stack v s = if Int.equal (Array.length v) 0 then s else match s with | Zapp l :: s -> Zapp (Array.append v l) :: s - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] -> Zapp v :: s (* Collapse the shifts in the stack *) @@ -366,20 +371,20 @@ let zshift n s = match (n,s) with (0,_) -> s | (_,Zshift(k)::s) -> Zshift(n+k)::s - | (_,(ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zupdate _) :: _) | _,[] -> Zshift(n)::s + | (_,(ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zupdate _ | Zprimitive _) :: _) | _,[] -> Zshift(n)::s let rec stack_args_size = function | Zapp v :: s -> Array.length v + stack_args_size s | Zshift(_)::s -> stack_args_size s | Zupdate(_)::s -> stack_args_size s - | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0 + | (ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | [] -> 0 (* Lifting. Preserves sharing (useful only for cell with norm=Red). lft_fconstr always create a new cell, while lift_fconstr avoids it when the lift is 0. *) let rec lft_fconstr n ft = match ft.term with - | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)) -> ft + | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft | FRel i -> {norm=Norm;term=FRel(i+n)} | FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))} | FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))} @@ -411,7 +416,7 @@ let compact_stack head stk = (** The stack contains [Zupdate] marks only if in sharing mode *) let _ = update ~share:true m h'.norm h'.term in strip_rec depth s - | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _) :: _ | []) as stk -> zshift depth stk + | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zprimitive _) :: _ | []) as stk -> zshift depth stk in strip_rec 0 stk @@ -447,6 +452,7 @@ let mk_clos e t = | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } | Ind kn -> { norm = Norm; term = FInd kn } | Construct kn -> { norm = Cstr; term = FConstruct kn } + | Int i -> {norm = Cstr; term = FInt i} | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} @@ -465,32 +471,34 @@ let mk_clos_vect env v = match v with let ref_value_cache ({ i_cache = cache; _ }) tab ref = try - Some (KeyTable.find tab ref) + KeyTable.find tab ref with Not_found -> - try - let body = - match ref with - | RelKey n -> - let open! Context.Rel.Declaration in - let i = n - 1 in - let (d, _) = - try Range.get cache.i_env.env_rel_context.env_rel_map i - with Invalid_argument _ -> raise Not_found - in - begin match d with - | LocalAssum _ -> raise Not_found - | LocalDef (_, t, _) -> lift n t - end - | VarKey id -> assoc_defined id cache.i_env - | ConstKey cst -> constant_value_in cache.i_env cst + let v = + try + let body = + match ref with + | RelKey n -> + let open! Context.Rel.Declaration in + let i = n - 1 in + let (d, _) = + try Range.get cache.i_env.env_rel_context.env_rel_map i + with Invalid_argument _ -> raise Not_found + in + begin match d with + | LocalAssum _ -> raise Not_found + | LocalDef (_, t, _) -> lift n t + end + | VarKey id -> assoc_defined id cache.i_env + | ConstKey cst -> constant_value_in cache.i_env cst + in + Def (inject body) + with + | NotEvaluableConst (IsPrimitive op) (* Const *) -> Primitive op + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> Undef None in - let v = inject body in - KeyTable.add tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None + KeyTable.add tab ref v; v (* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = @@ -559,6 +567,10 @@ let rec to_constr lfts v = let subs = comp_subs lfts env in mkEvar(ev,Array.map (fun a -> subst_constr subs a) args) | FLIFT (k,a) -> to_constr (el_shft k lfts) a + + | FInt i -> + Constr.mkInt i + | FCLOS (t,env) -> if is_subs_id env && is_lift_id lfts then t else @@ -607,6 +619,10 @@ let rec zip m stk = | Zupdate(rf)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) zip (update ~share:true rf m.norm m.term) s + | Zprimitive(_op,c,rargs,kargs)::s -> + let args = List.rev_append rargs (m::List.map snd kargs) in + let f = {norm = Red;term = FFlex (ConstKey c)} in + zip {norm=neutr m.norm; term = FApp (f, Array.of_list args)} s let fapp_stack (m,stk) = zip m stk @@ -628,7 +644,7 @@ let strip_update_shift_app_red head stk = | Zupdate(m)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) strip_rec rstk (update ~share:true m h.norm h.term) depth s - | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> (depth,List.rev rstk, stk) in strip_rec [] head 0 stk @@ -656,7 +672,7 @@ let get_nth_arg head n stk = | Zupdate(m)::s -> (** The stack contains [Zupdate] mark only if in sharing mode *) strip_rec rstk (update ~share:true m h.norm h.term) n s - | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as s -> (None, List.rev rstk @ s) in + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in strip_rec [] head n stk (* Beta reduction: look for an applied argument in the stack. @@ -678,24 +694,70 @@ let rec get_args n tys f e = function else (* more lambdas *) let etys = List.skipn na tys in get_args (n-na) etys f (subs_cons(l,e)) s - | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _ - | Zshift _ | Zupdate _ as e) :: s -> + | Zshift _ | Zupdate _ | Zprimitive _ as e) :: s -> e :: eta_expand_stack s | [] -> [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] +(* Get the arguments of a native operator *) +let rec skip_native_args rargs nargs = + match nargs with + | (kd, a) :: nargs' -> + if kd = CPrimitives.Kwhnf then rargs, nargs + else skip_native_args (a::rargs) nargs' + | [] -> rargs, [] + +let get_native_args op c stk = + let kargs = CPrimitives.kind op in + let rec get_args rnargs kargs args = + match kargs, args with + | kd::kargs, a::args -> get_args ((kd,a)::rnargs) kargs args + | _, _ -> rnargs, kargs, args in + let rec strip_rec rnargs h depth kargs = function + | Zshift k :: s -> + strip_rec (List.map (fun (kd,f) -> kd,lift_fconstr k f) rnargs) + (lift_fconstr k h) (depth+k) kargs s + | Zapp args :: s' -> + begin match get_args rnargs kargs (Array.to_list args) with + | rnargs, [], [] -> + (skip_native_args [] (List.rev rnargs), s') + | rnargs, [], eargs -> + (skip_native_args [] (List.rev rnargs), + Zapp (Array.of_list eargs) :: s') + | rnargs, kargs, _ -> + strip_rec rnargs {norm = h.norm;term=FApp(h, args)} depth kargs s' + end + | Zupdate(m) :: s -> + strip_rec rnargs (update ~share:true m h.norm h.term) depth kargs s + | (Zprimitive _ | ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> assert false + in strip_rec [] {norm = Red;term = FFlex(ConstKey c)} 0 kargs stk + +let get_native_args1 op c stk = + match get_native_args op c stk with + | ((rargs, (kd,a):: nargs), stk) -> + assert (kd = CPrimitives.Kwhnf); + (rargs, a, nargs, stk) + | _ -> assert false + +let check_native_args op stk = + let nargs = CPrimitives.arity op in + let rargs = stack_args_size stk in + nargs <= rargs + + (* Iota reduction: extract the arguments to be passed to the Case branches *) let rec reloc_rargs_rec depth = function | Zapp args :: s -> Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s - | ((ZcaseT _ | Zproj _ | Zfix _ | Zupdate _) :: _ | []) as stk -> stk + | ((ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ | []) as stk -> stk let reloc_rargs depth stk = if Int.equal depth 0 then stk else reloc_rargs_rec depth stk @@ -712,7 +774,7 @@ let rec try_drop_parameters depth n = function | [] -> if Int.equal n 0 then [] else raise Not_found - | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _) :: _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) let drop_parameters depth n argstk = @@ -757,7 +819,7 @@ let rec project_nth_arg n = function let q = Array.length args in if n >= q then project_nth_arg (n - q) s else (* n < q *) args.(n) - | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _) :: _ | [] -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> assert false (* After drop_parameters we have a purely applicative stack *) @@ -814,7 +876,7 @@ let rec knh info m stk = (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| - FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> + FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _) -> (m, stk) (* The same for pure terms *) @@ -828,7 +890,7 @@ and knht info e t stk = | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk - | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> (mk_clos e t, stk) + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk) | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk | Prod (n, t, c) -> @@ -837,6 +899,162 @@ and knht info e t stk = { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk +let inject c = mk_clos (subs_id 0) c + +(************************************************************************) +(* Reduction of Native operators *) + +open Primred + +module FNativeEntries = + struct + type elem = fconstr + type args = fconstr array + type evd = unit + + let get = Array.get + + let get_int () e = + match [@ocaml.warning "-4"] e.term with + | FInt i -> i + | _ -> raise Primred.NativeDestKO + + let dummy = {norm = Norm; term = FRel 0} + + let current_retro = ref Retroknowledge.empty + let defined_int = ref false + let fint = ref dummy + + let init_int retro = + match retro.Retroknowledge.retro_int63 with + | Some c -> + defined_int := true; + fint := { norm = Norm; term = FFlex (ConstKey (Univ.in_punivs c)) } + | None -> defined_int := false + + let defined_bool = ref false + let ftrue = ref dummy + let ffalse = ref dummy + + let init_bool retro = + match retro.Retroknowledge.retro_bool with + | Some (ct,cf) -> + defined_bool := true; + ftrue := { norm = Cstr; term = FConstruct (Univ.in_punivs ct) }; + ffalse := { norm = Cstr; term = FConstruct (Univ.in_punivs cf) } + | None -> defined_bool :=false + + let defined_carry = ref false + let fC0 = ref dummy + let fC1 = ref dummy + + let init_carry retro = + match retro.Retroknowledge.retro_carry with + | Some(c0,c1) -> + defined_carry := true; + fC0 := { norm = Cstr; term = FConstruct (Univ.in_punivs c0) }; + fC1 := { norm = Cstr; term = FConstruct (Univ.in_punivs c1) } + | None -> defined_carry := false + + let defined_pair = ref false + let fPair = ref dummy + + let init_pair retro = + match retro.Retroknowledge.retro_pair with + | Some c -> + defined_pair := true; + fPair := { norm = Cstr; term = FConstruct (Univ.in_punivs c) } + | None -> defined_pair := false + + let defined_cmp = ref false + let fEq = ref dummy + let fLt = ref dummy + let fGt = ref dummy + + let init_cmp retro = + match retro.Retroknowledge.retro_cmp with + | Some (cEq, cLt, cGt) -> + defined_cmp := true; + fEq := { norm = Cstr; term = FConstruct (Univ.in_punivs cEq) }; + fLt := { norm = Cstr; term = FConstruct (Univ.in_punivs cLt) }; + fGt := { norm = Cstr; term = FConstruct (Univ.in_punivs cGt) } + | None -> defined_cmp := false + + let defined_refl = ref false + + let frefl = ref dummy + + let init_refl retro = + match retro.Retroknowledge.retro_refl with + | Some crefl -> + defined_refl := true; + frefl := { norm = Cstr; term = FConstruct (Univ.in_punivs crefl) } + | None -> defined_refl := false + + let init env = + current_retro := env.retroknowledge; + init_int !current_retro; + init_bool !current_retro; + init_carry !current_retro; + init_pair !current_retro; + init_cmp !current_retro; + init_refl !current_retro + + let check_env env = + if not (!current_retro == env.retroknowledge) then init env + + let check_int env = + check_env env; + assert (!defined_int) + + let check_bool env = + check_env env; + assert (!defined_bool) + + let check_carry env = + check_env env; + assert (!defined_carry && !defined_int) + + let check_pair env = + check_env env; + assert (!defined_pair && !defined_int) + + let check_cmp env = + check_env env; + assert (!defined_cmp) + + let mkInt env i = + check_int env; + { norm = Norm; term = FInt i } + + let mkBool env b = + check_bool env; + if b then !ftrue else !ffalse + + let mkCarry env b e = + check_carry env; + {norm = Cstr; + term = FApp ((if b then !fC1 else !fC0),[|!fint;e|])} + + let mkIntPair env e1 e2 = + check_pair env; + { norm = Cstr; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) } + + let mkLt env = + check_cmp env; + !fLt + + let mkEq env = + check_cmp env; + !fEq + + let mkGt env = + check_cmp env; + !fGt + + end + +module FredNative = RedNative(FNativeEntries) (************************************************************************) @@ -849,16 +1067,21 @@ let rec knr info tab m stk = | Inr lam, s -> (lam,s)) | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info tab (ConstKey c) with - Some v -> kni info tab v stk - | None -> (set_norm m; (m,stk))) + | Def v -> kni info tab v stk + | Primitive op when check_native_args op stk -> + let rargs, a, nargs, stk = get_native_args1 op c stk in + kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) + | Undef _ | OpaqueDef _ | Primitive _ -> (set_norm m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> (match ref_value_cache info tab (VarKey id) with - Some v -> kni info tab v stk - | None -> (set_norm m; (m,stk))) + | Def v -> kni info tab v stk + | Primitive _ -> assert false + | OpaqueDef _ | Undef _ -> (set_norm m; (m,stk))) | FFlex(RelKey k) when red_set info.i_flags fDELTA -> (match ref_value_cache info tab (RelKey k) with - Some v -> kni info tab v stk - | None -> (set_norm m; (m,stk))) + | Def v -> kni info tab v stk + | Primitive _ -> assert false + | OpaqueDef _ | Undef _ -> (set_norm 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 @@ -884,13 +1107,32 @@ let rec knr info tab m stk = | (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info tab fxe fxbd (args@stk') - | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] as s)) -> (m,args@s)) + | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] as s)) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info tab (subs_cons([|v|],e)) bd stk | FEvar(ev,env) -> (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) + | FInt _ -> + (match [@ocaml.warning "-4"] strip_update_shift_app m stk with + | (_, _, Zprimitive(op,c,rargs,nargs)::s) -> + let (rargs, nargs) = skip_native_args (m::rargs) nargs in + begin match nargs with + | [] -> + let args = Array.of_list (List.rev rargs) in + begin match FredNative.red_prim (info_env info) () op args with + | Some m -> kni info tab m s + | None -> + let f = {norm = Whnf; term = FFlex (ConstKey c)} in + let m = {norm = Whnf; term = FApp(f,args)} in + (m,s) + end + | (kd,a)::nargs -> + assert (kd = CPrimitives.Kwhnf); + kni info tab a (Zprimitive(op,c,rargs,nargs)::s) + end + | (_, _, s) -> (m, s)) | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ | FCLOS _ -> (m, stk) @@ -927,6 +1169,12 @@ let rec zip_term zfun m stk = zip_term zfun (lift n m) s | Zupdate(_rf)::s -> zip_term zfun m s + | Zprimitive(_,c,rargs, kargs)::s -> + let kargs = List.map (fun (_,a) -> zfun a) kargs in + let args = + List.fold_left (fun args a -> zfun a ::args) (m::kargs) rargs in + let h = mkApp (mkConstU c, Array.of_list args) in + zip_term zfun h s (* Computes the strong normal form of a term. 1- Calls kni @@ -972,7 +1220,7 @@ and norm_head info tab m = | FProj (p,c) -> mkProj (p, kl info tab c) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _ - | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m + | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ -> term_of_fconstr m (* Initialization and then normalization *) @@ -1015,9 +1263,9 @@ let unfold_reference info tab key = | ConstKey (kn,_) -> if red_set info.i_flags (fCONST kn) then ref_value_cache info tab key - else None + else Undef None | VarKey i -> if red_set info.i_flags (fVAR i) then ref_value_cache info tab key - else None + else Undef None | RelKey _ -> ref_value_cache info tab key diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 46be1bb279..bd04677374 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -10,6 +10,7 @@ open Names open Constr +open Declarations open Environ open Esubst @@ -117,6 +118,7 @@ type fterm = | FProd of Name.t * fconstr * constr * fconstr subs | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs + | FInt of Uint63.t | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -124,12 +126,15 @@ type fterm = (*********************************************************************** s A [stack] is a context of arguments, arguments are pushed by [append_stack] one array at a time *) +type 'a next_native_args = (CPrimitives.arg_kind * 'a) list type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of Projection.Repr.t | Zfix of fconstr * stack + | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args + (* operator, constr def, reduced arguments rev, next arguments *) | Zshift of int | Zupdate of fconstr @@ -138,6 +143,10 @@ and stack = stack_member list val empty_stack : stack val append_stack : fconstr array -> stack -> stack +val check_native_args : CPrimitives.t -> stack -> bool +val get_native_args1 : CPrimitives.t -> pconstant -> stack -> + fconstr list * fconstr * fconstr next_native_args * stack + val stack_args_size : stack -> int val eta_expand_stack : stack -> stack @@ -201,7 +210,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option +val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def (*********************************************************************** i This is for lazy debug *) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 5b91a9b572..da5c4fb07b 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -9,85 +9,147 @@ (************************************************************************) type t = - | Int31head0 - | Int31tail0 - | Int31add - | Int31sub - | Int31mul - | Int31div - | Int31mod -(* - | Int31lsr - | Int31lsl - *) - | Int31land - | Int31lor - | Int31lxor - | Int31addc - | Int31subc - | Int31addcarryc - | Int31subcarryc - | Int31mulc - | Int31diveucl - | Int31div21 - | Int31addmuldiv - | Int31eq - | Int31lt - | Int31le - | Int31compare + | Int63head0 + | Int63tail0 + | Int63add + | Int63sub + | Int63mul + | Int63div + | Int63mod + | Int63lsr + | Int63lsl + | Int63land + | Int63lor + | Int63lxor + | Int63addc + | Int63subc + | Int63addCarryC + | Int63subCarryC + | Int63mulc + | Int63diveucl + | Int63div21 + | Int63addMulDiv + | Int63eq + | Int63lt + | Int63le + | Int63compare + +let equal (p1 : t) (p2 : t) = + p1 == p2 let hash = function - | Int31head0 -> 1 - | Int31tail0 -> 2 - | Int31add -> 3 - | Int31sub -> 4 - | Int31mul -> 5 - | Int31div -> 6 - | Int31mod -> 7 -(* - | Int31lsr -> 8 - | Int31lsl -> 9 - *) - | Int31land -> 10 - | Int31lor -> 11 - | Int31lxor -> 12 - | Int31addc -> 13 - | Int31subc -> 14 - | Int31addcarryc -> 15 - | Int31subcarryc -> 16 - | Int31mulc -> 17 - | Int31diveucl -> 18 - | Int31div21 -> 19 - | Int31addmuldiv -> 20 - | Int31eq -> 21 - | Int31lt -> 22 - | Int31le -> 23 - | Int31compare -> 24 + | Int63head0 -> 1 + | Int63tail0 -> 2 + | Int63add -> 3 + | Int63sub -> 4 + | Int63mul -> 5 + | Int63div -> 6 + | Int63mod -> 7 + | Int63lsr -> 8 + | Int63lsl -> 9 + | Int63land -> 10 + | Int63lor -> 11 + | Int63lxor -> 12 + | Int63addc -> 13 + | Int63subc -> 14 + | Int63addCarryC -> 15 + | Int63subCarryC -> 16 + | Int63mulc -> 17 + | Int63diveucl -> 18 + | Int63div21 -> 19 + | Int63addMulDiv -> 20 + | Int63eq -> 21 + | Int63lt -> 22 + | Int63le -> 23 + | Int63compare -> 24 +(* Should match names in nativevalues.ml *) let to_string = function - | Int31head0 -> "head0" - | Int31tail0 -> "tail0" - | Int31add -> "add" - | Int31sub -> "sub" - | Int31mul -> "mul" - | Int31div -> "div" - | Int31mod -> "mod" -(* - | Int31lsr -> "l_sr" - | Int31lsl -> "l_sl" - *) - | Int31land -> "l_and" - | Int31lor -> "l_or" - | Int31lxor -> "l_xor" - | Int31addc -> "addc" - | Int31subc -> "subc" - | Int31addcarryc -> "addcarryc" - | Int31subcarryc -> "subcarryc" - | Int31mulc -> "mulc" - | Int31diveucl -> "diveucl" - | Int31div21 -> "div21" - | Int31addmuldiv -> "addmuldiv" - | Int31eq -> "eq" - | Int31lt -> "lt" - | Int31le -> "le" - | Int31compare -> "compare" + | Int63head0 -> "head0" + | Int63tail0 -> "tail0" + | Int63add -> "add" + | Int63sub -> "sub" + | Int63mul -> "mul" + | Int63div -> "div" + | Int63mod -> "rem" + | Int63lsr -> "l_sr" + | Int63lsl -> "l_sl" + | Int63land -> "l_and" + | Int63lor -> "l_or" + | Int63lxor -> "l_xor" + | Int63addc -> "addc" + | Int63subc -> "subc" + | Int63addCarryC -> "addCarryC" + | Int63subCarryC -> "subCarryC" + | Int63mulc -> "mulc" + | Int63diveucl -> "diveucl" + | Int63div21 -> "div21" + | Int63addMulDiv -> "addMulDiv" + | Int63eq -> "eq" + | Int63lt -> "lt" + | Int63le -> "le" + | Int63compare -> "compare" + +type arg_kind = + | Kparam (* not needed for the evaluation of the primitive when it reduces *) + | Kwhnf (* need to be reduced in whnf before reducing the primitive *) + | Karg (* no need to be reduced in whnf. example: [v] in [Array.set t i v] *) + +type args_red = arg_kind list + +(* Invariant only argument of type int63 or an inductive can + have kind Kwhnf *) + +let kind = function + | Int63head0 | Int63tail0 -> [Kwhnf] + + | Int63add | Int63sub | Int63mul + | Int63div | Int63mod + | Int63lsr | Int63lsl + | Int63land | Int63lor | Int63lxor + | Int63addc | Int63subc + | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl + | Int63eq | Int63lt | Int63le | Int63compare -> [Kwhnf; Kwhnf] + + | Int63div21 | Int63addMulDiv -> [Kwhnf; Kwhnf; Kwhnf] + +let arity = function + | Int63head0 | Int63tail0 -> 1 + | Int63add | Int63sub | Int63mul + | Int63div | Int63mod + | Int63lsr | Int63lsl + | Int63land | Int63lor | Int63lxor + | Int63addc | Int63subc + | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl + | Int63eq | Int63lt | Int63le + | Int63compare -> 2 + + | Int63div21 | Int63addMulDiv -> 3 + +(** Special Entries for Register **) + +type prim_ind = + | PIT_bool + | PIT_carry + | PIT_pair + | PIT_cmp + +type prim_type = + | PT_int63 + +type op_or_type = + | OT_op of t + | OT_type of prim_type + +let prim_ind_to_string = function + | PIT_bool -> "bool" + | PIT_carry -> "carry" + | PIT_pair -> "pair" + | PIT_cmp -> "cmp" + +let prim_type_to_string = function + | PT_int63 -> "int63" + +let op_or_type_to_string = function + | OT_op op -> to_string op + | OT_type t -> prim_type_to_string t diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 1e99a69d2f..3f8174bd7b 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -9,33 +9,62 @@ (************************************************************************) type t = - | Int31head0 - | Int31tail0 - | Int31add - | Int31sub - | Int31mul - | Int31div - | Int31mod -(* - | Int31lsr - | Int31lsl - *) - | Int31land - | Int31lor - | Int31lxor - | Int31addc - | Int31subc - | Int31addcarryc - | Int31subcarryc - | Int31mulc - | Int31diveucl - | Int31div21 - | Int31addmuldiv - | Int31eq - | Int31lt - | Int31le - | Int31compare + | Int63head0 + | Int63tail0 + | Int63add + | Int63sub + | Int63mul + | Int63div + | Int63mod + | Int63lsr + | Int63lsl + | Int63land + | Int63lor + | Int63lxor + | Int63addc + | Int63subc + | Int63addCarryC + | Int63subCarryC + | Int63mulc + | Int63diveucl + | Int63div21 + | Int63addMulDiv + | Int63eq + | Int63lt + | Int63le + | Int63compare + +val equal : t -> t -> bool + +type arg_kind = + | Kparam (* not needed for the elavuation of the primitive*) + | Kwhnf (* need to be reduced in whnf before reducing the primitive *) + | Karg (* no need to be reduced in whnf *) + +type args_red = arg_kind list val hash : t -> int val to_string : t -> string + +val arity : t -> int + +val kind : t -> args_red + +(** Special Entries for Register **) + +type prim_ind = + | PIT_bool + | PIT_carry + | PIT_pair + | PIT_cmp + +type prim_type = + | PT_int63 + +type op_or_type = + | OT_op of t + | OT_type of prim_type + +val prim_ind_to_string : prim_ind -> string +val op_or_type_to_string : op_or_type -> string diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index c63795b295..7570004fe5 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -16,6 +16,7 @@ open Names open Vmvalues +open Constr module Label = struct @@ -26,7 +27,6 @@ module Label = let reset_label_counter () = counter := no end - type instruction = | Klabel of Label.t | Kacc of int @@ -59,46 +59,9 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of Projection.Repr.t | Kensurestackcapacity of int -(* spiwack: instructions concerning integers *) | Kbranch of Label.t (* jump to label *) - | Kaddint31 (* adds the int31 in the accu - and the one ontop of the stack *) - | Kaddcint31 (* makes the sum and keeps the carry *) - | Kaddcarrycint31 (* sum +1, keeps the carry *) - | Ksubint31 (* subtraction modulo *) - | Ksubcint31 (* subtraction, keeps the carry *) - | Ksubcarrycint31 (* subtraction -1, keeps the carry *) - | Kmulint31 (* multiplication modulo *) - | Kmulcint31 (* multiplication, result in two - int31, for exact computation *) - | Kdiv21int31 (* divides a double size integer - (represented by an int31 in the - accumulator and one on the top of - the stack) by an int31. The result - is a pair of the quotient and the - rest. - If the divisor is 0, it returns - 0. *) - | Kdivint31 (* euclidian division (returns a pair - quotient,rest) *) - | Kaddmuldivint31 (* generic operation for shifting and - cycling. Takes 3 int31 i j and s, - and returns x*2^s+y/(2^(31-s) *) - | Kcompareint31 (* unsigned comparison of int31 - cf COMPAREINT31 in - kernel/byterun/coq_interp.c - for more info *) - | Khead0int31 (* Give the numbers of 0 in head of a in31*) - | Ktail0int31 (* Give the numbers of 0 in tail of a in31 - ie low bits *) - | Kisconst of Label.t (* conditional jump *) - | Kareconst of int*Label.t (* conditional jump *) - | Kcompint31 (* dynamic compilation of int31 *) - | Kdecompint31 (* dynamic decompilation of int31 *) - | Klorint31 (* bitwise operations: or and xor *) - | Klandint31 - | Klxorint31 -(* /spiwack *) + | Kprim of CPrimitives.t * pconstant option + | Kareint of int and bytecodes = instruction list @@ -110,53 +73,6 @@ type fv_elem = type fv = fv_elem array -(* spiwack: this exception is expected to be raised by function expecting - closed terms. *) -exception NotClosed - - -module Fv_elem = -struct -type t = fv_elem - -let compare e1 e2 = match e1, e2 with -| FVnamed id1, FVnamed id2 -> Id.compare id1 id2 -| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 -| FVrel _, FVnamed _ -> 1 -| FVrel r1, FVrel r2 -> Int.compare r1 r2 -| FVrel _, (FVuniv_var _ | FVevar _) -> -1 -| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var _i1, (FVnamed _ | FVrel _) -> 1 -| FVuniv_var _i1, FVevar _ -> -1 -| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 -| FVevar e1, FVevar e2 -> Evar.compare e1 e2 - -end - -module FvMap = Map.Make(Fv_elem) - -(*spiwack: both type have been moved from Cbytegen because I needed then - for the retroknowledge *) -type vm_env = { - size : int; (* longueur de la liste [n] *) - fv_rev : fv_elem list; (* [fvn; ... ;fv1] *) - fv_fwd : int FvMap.t; (* reverse mapping *) - } - - -type comp_env = { - arity : int; (* arity of the current function, 0 if none *) - nb_uni_stack : int ; (* number of universes on the stack, *) - (* universes are always at the bottom. *) - nb_stack : int; (* number of variables on the stack *) - in_stack : int list; (* position in the stack *) - nb_rec : int; (* number of mutually recursive functions *) - pos_rec : instruction list; (* instruction d'acces pour les variables *) - (* de point fix ou de cofix *) - offset : int; - in_env : vm_env ref (* The free variables of the expression *) - } - (* --- Pretty print *) open Pp open Util @@ -228,28 +144,10 @@ let rec pp_instr i = | Kensurestackcapacity size -> str "growstack " ++ int size - | Kaddint31 -> str "addint31" - | Kaddcint31 -> str "addcint31" - | Kaddcarrycint31 -> str "addcarrycint31" - | Ksubint31 -> str "subint31" - | Ksubcint31 -> str "subcint31" - | Ksubcarrycint31 -> str "subcarrycint31" - | Kmulint31 -> str "mulint31" - | Kmulcint31 -> str "mulcint31" - | Kdiv21int31 -> str "div21int31" - | Kdivint31 -> str "divint31" - | Kcompareint31 -> str "compareint31" - | Khead0int31 -> str "head0int31" - | Ktail0int31 -> str "tail0int31" - | Kaddmuldivint31 -> str "addmuldivint31" - | Kisconst lbl -> str "isconst " ++ int lbl - | Kareconst(n,lbl) -> str "areconst " ++ int n ++ spc () ++ int lbl - | Kcompint31 -> str "compint31" - | Kdecompint31 -> str "decompint" - | Klorint31 -> str "lorint31" - | Klandint31 -> str "landint31" - | Klxorint31 -> str "lxorint31" + | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++ + (match id with Some (id,_u) -> Constant.print id | None -> str "") + | Kareint n -> str "areint " ++ int n and pp_bytecodes c = match c with diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 9c04c166a2..423e7bbe65 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -12,6 +12,7 @@ open Names open Vmvalues +open Constr module Label : sig @@ -57,48 +58,15 @@ type instruction = | Kproj of Projection.Repr.t | Kensurestackcapacity of int -(** spiwack: instructions concerning integers *) | Kbranch of Label.t (** jump to label, is it needed ? *) - | Kaddint31 (** adds the int31 in the accu - and the one ontop of the stack *) - | Kaddcint31 (** makes the sum and keeps the carry *) - | Kaddcarrycint31 (** sum +1, keeps the carry *) - | Ksubint31 (** subtraction modulo *) - | Ksubcint31 (** subtraction, keeps the carry *) - | Ksubcarrycint31 (** subtraction -1, keeps the carry *) - | Kmulint31 (** multiplication modulo *) - | Kmulcint31 (** multiplication, result in two - int31, for exact computation *) - | Kdiv21int31 (** divides a double size integer - (represented by an int31 in the - accumulator and one on the top of - the stack) by an int31. The result - is a pair of the quotient and the - rest. - If the divisor is 0, it returns - 0. *) - | Kdivint31 (** euclidian division (returns a pair - quotient,rest) *) - | Kaddmuldivint31 (** generic operation for shifting and - cycling. Takes 3 int31 i j and s, - and returns x*2^s+y/(2^(31-s) *) - | Kcompareint31 (** unsigned comparison of int31 - cf COMPAREINT31 in - kernel/byterun/coq_interp.c - for more info *) - | Khead0int31 (** Give the numbers of 0 in head of a in31*) - | Ktail0int31 (** Give the numbers of 0 in tail of a in31 - ie low bits *) - | Kisconst of Label.t (** conditional jump *) - | Kareconst of int*Label.t (** conditional jump *) - | Kcompint31 (** dynamic compilation of int31 *) - | Kdecompint31 (** dynamix decompilation of int31 *) - | Klorint31 (** bitwise operations: or and xor *) - | Klandint31 - | Klxorint31 + | Kprim of CPrimitives.t * pconstant option + + | Kareint of int and bytecodes = instruction list +val pp_bytecodes : bytecodes -> Pp.t + type fv_elem = FVnamed of Id.t | FVrel of int @@ -107,34 +75,4 @@ type fv_elem = type fv = fv_elem array - -(** spiwack: this exception is expected to be raised by function expecting - closed terms. *) -exception NotClosed - -module FvMap : Map.S with type key = fv_elem - -(*spiwack: both type have been moved from Cbytegen because I needed them - for the retroknowledge *) -type vm_env = { - size : int; (** length of the list [n] *) - fv_rev : fv_elem list; (** [fvn; ... ;fv1] *) - fv_fwd : int FvMap.t; (** reverse mapping *) - } - - -type comp_env = { - arity : int; (* arity of the current function, 0 if none *) - nb_uni_stack : int ; (** number of universes on the stack *) - nb_stack : int; (** number of variables on the stack *) - in_stack : int list; (** position in the stack *) - nb_rec : int; (** number of mutually recursive functions *) - (** (= nbr) *) - pos_rec : instruction list; (** instruction d'acces pour les variables *) - (** de point fix ou de cofix *) - offset : int; - in_env : vm_env ref (** the variables that are accessed *) - } - -val pp_bytecodes : bytecodes -> Pp.t val pp_fv_elem : fv_elem -> Pp.t diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 73620ae578..b95a940c14 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -17,7 +17,6 @@ open Names open Vmvalues open Cbytecodes open Cemitcodes -open Cinstr open Clambda open Constr open Declarations @@ -97,6 +96,48 @@ open Environ (* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) (* conversion of cofixpoints (which is intentional). *) +module Fv_elem = +struct +type t = fv_elem + +let compare e1 e2 = match e1, e2 with +| FVnamed id1, FVnamed id2 -> Id.compare id1 id2 +| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 +| FVrel _, FVnamed _ -> 1 +| FVrel r1, FVrel r2 -> Int.compare r1 r2 +| FVrel _, (FVuniv_var _ | FVevar _) -> -1 +| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 +| FVuniv_var _, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var _, FVevar _ -> -1 +| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 +| FVevar e1, FVevar e2 -> Evar.compare e1 e2 + +end + +module FvMap = Map.Make(Fv_elem) + +(*spiwack: both type have been moved from Cbytegen because I needed then + for the retroknowledge *) +type vm_env = { + size : int; (* longueur de la liste [n] *) + fv_rev : fv_elem list; (* [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (* reverse mapping *) + } + + +type comp_env = { + arity : int; (* arity of the current function, 0 if none *) + nb_uni_stack : int ; (* number of universes on the stack, *) + (* universes are always at the bottom. *) + nb_stack : int; (* number of variables on the stack *) + in_stack : int list; (* position in the stack *) + nb_rec : int; (* number of mutually recursive functions *) + pos_rec : instruction list; (* instruction d'acces pour les variables *) + (* de point fix ou de cofix *) + offset : int; + in_env : vm_env ref (* The free variables of the expression *) + } + module Config = struct let stack_threshold = 256 (* see byterun/coq_memory.h *) let stack_safety_margin = 15 @@ -391,7 +432,6 @@ let init_fun_code () = fun_code := [] (* Compilation of constructors and inductive types *) -(* Inv: arity > 0 *) (* If [tag] hits the OCaml limitation for non constant constructors, we switch to @@ -437,7 +477,7 @@ let comp_app comp_fun comp_arg cenv f args sz cont = comp_fun cenv f (sz + nargs) (Kappterm(nargs, k + nargs) :: (discard_dead_code cont))) | None -> - if nargs < 4 then + if nargs <= 4 then comp_args comp_arg cenv args sz (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) else @@ -476,15 +516,6 @@ let rec get_alias env kn = | BCalias kn' -> get_alias env kn' | _ -> kn) -(* spiwack: additional function which allow different part of compilation of the - 31-bit integers *) - -let make_areconst n else_lbl cont = - if n <= 0 then - cont - else - Kareconst (n, else_lbl)::cont - (* sz is the size of the local stack *) let rec compile_lam env cenv lam sz cont = set_max_stack_size sz; @@ -495,6 +526,8 @@ let rec compile_lam env cenv lam sz cont = | Lval v -> compile_structured_constant cenv (Const_val v) sz cont + | Luint i -> compile_structured_constant cenv (Const_uint i) sz cont + | Lproj (p,arg) -> compile_lam env cenv arg sz (Kproj p :: cont) @@ -629,6 +662,17 @@ let rec compile_lam env cenv lam sz cont = 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 @@ -729,41 +773,9 @@ 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 (kn, ar, op, args) -> - op_compilation env ar op kn cenv args sz cont - - | Luint v -> - (match v with - | UintVal i -> compile_structured_constant cenv (Const_b0 (Uint31.to_int i)) sz cont - | UintDigits ds -> - let nargs = Array.length ds in - if Int.equal nargs 31 then - let (escape,labeled_cont) = make_branch cont in - let else_lbl = Label.create() in - comp_args (compile_lam env) cenv ds sz - ( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont) - else - let code_construct cont = (* spiwack: variant of the global code_construct - which handles dynamic compilation of - integers *) - let f_cont = - let else_lbl = Label.create () in - [Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl); - Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0] - in - let lbl = Label.create() in - fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)]; - Kclosure(lbl,0) :: cont - in - comp_app (fun _ _ _ cont -> code_construct cont) - (compile_lam env) cenv () ds sz cont - | UintDecomp t -> - let escape_lbl, labeled_cont = label_code cont in - compile_lam env cenv t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont)) - - -(* spiwack : compilation of constants with their arguments. - Makes a special treatment with 31-bit integer addition *) + | Lprim (kn, op, args) -> + comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) + and compile_get_global cenv (kn,u) sz cont = set_max_stack_size sz; if Univ.Instance.is_empty u then @@ -800,43 +812,6 @@ and compile_constant env cenv kn u args sz cont = comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont) compile_arg cenv () all sz cont -(*template for n-ary operation, invariant: n>=1, - the operations does the following : - 1/ checks if all the arguments are constants (i.e. non-block values) - 2/ if they are, uses the "op" instruction to execute - 3/ if at least one is not, branches to the normal behavior: - Kgetglobal (get_alias !global_env kn) *) -and op_compilation env n op = - let code_construct cenv kn sz cont = - let f_cont = - let else_lbl = Label.create () in - Kareconst(n, else_lbl):: Kacc 0:: Kpop 1:: - op:: Kreturn 0:: Klabel else_lbl:: - (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*) - compile_get_global cenv kn sz ( - Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *) - in - let lbl = Label.create () in - fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)]; - Kclosure(lbl, 0)::cont - in - fun kn cenv args sz cont -> - let nargs = Array.length args in - if Int.equal nargs n then (*if it is a fully applied addition*) - let (escape, labeled_cont) = make_branch cont in - let else_lbl = Label.create () in - assert (n < 4); - comp_args (compile_lam env) cenv args sz - (Kisconst else_lbl::(make_areconst (n-1) else_lbl - (*Kaddint31::escape::Klabel else_lbl::Kpush::*) - (op::escape::Klabel else_lbl::Kpush:: - (* works as comp_app with nargs < 4 and non-tailcall cont*) - compile_get_global cenv kn (sz+n) (Kapply n::labeled_cont)))) - else - comp_app (fun cenv _ sz cont -> code_construct cenv kn sz cont) - (compile_lam env) cenv () args sz cont - - let is_univ_copy max u = let u = Univ.Instance.to_array u in if Array.length u = max then @@ -903,7 +878,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = fn msg; None let compile_constant_body ~fail_on_error env univs = function - | Undef _ | OpaqueDef _ -> Some BCconstant + | Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in let instance_size = @@ -923,41 +898,3 @@ let compile_constant_body ~fail_on_error env univs = function (* Shortcut of the previous function used during module strengthening *) let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn)) - -(*(* template compilation for 2ary operation, it probably possible - to make a generic such function with arity abstracted *) -let op2_compilation op = - let code_construct normal cont = (*kn cont =*) - let f_cont = - let else_lbl = Label.create () in - Kareconst(2, else_lbl):: Kacc 0:: Kpop 1:: - op:: Kreturn 0:: Klabel else_lbl:: - (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*) - (*Kgetglobal (get_alias !global_env kn):: *) - normal:: - Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *) - in - let lbl = Label.create () in - fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)]; - Kclosure(lbl, 0)::cont - in - fun normal fc _ cenv args sz cont -> - if not fc then raise Not_found else - let nargs = Array.length args in - if nargs=2 then (*if it is a fully applied addition*) - let (escape, labeled_cont) = make_branch cont in - let else_lbl = Label.create () in - comp_args compile_constr cenv args sz - (Kisconst else_lbl::(make_areconst 1 else_lbl - (*Kaddint31::escape::Klabel else_lbl::Kpush::*) - (op::escape::Klabel else_lbl::Kpush:: - (* works as comp_app with nargs = 2 and non-tailcall cont*) - (*Kgetglobal (get_alias !global_env kn):: *) - normal:: - Kapply 2::labeled_cont))) - else if nargs=0 then - code_construct normal cont - else - comp_app (fun _ _ _ cont -> code_construct normal cont) - compile_constr cenv () args sz cont *) - diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 57d3e6fc27..b1b55aef48 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -20,7 +20,8 @@ val compile : fail_on_error:bool -> (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> - env -> constant_universes -> constant_def -> body_code option + env -> constant_universes -> Constr.t Mod_subst.substituted constant_def -> + body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 50f5607e31..a84a7c0cf9 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -18,6 +18,7 @@ open Vmvalues open Cbytecodes open Copcodes open Mod_subst +open CPrimitives type emitcodes = String.t @@ -129,6 +130,8 @@ let out_word env b1 b2 b3 b4 = let out env opcode = out_word env opcode 0 0 0 +let is_immed i = Uint63.le (Uint63.of_int i) Uint63.maxuint31 + let out_int env n = out_word env n (n asr 8) (n asr 16) (n asr 24) @@ -198,6 +201,39 @@ let slot_for_proj_name env p = (* 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 + | Int63add -> opCHECKADDINT63 + | Int63sub -> opCHECKSUBINT63 + | Int63mul -> opCHECKMULINT63 + | Int63div -> opCHECKDIVINT63 + | Int63mod -> opCHECKMODINT63 + | Int63lsr -> opCHECKLSRINT63 + | Int63lsl -> opCHECKLSLINT63 + | Int63land -> opCHECKLANDINT63 + | Int63lor -> opCHECKLORINT63 + | Int63lxor -> opCHECKLXORINT63 + | Int63addc -> opCHECKADDCINT63 + | Int63subc -> opCHECKSUBCINT63 + | Int63addCarryC -> opCHECKADDCARRYCINT63 + | Int63subCarryC -> opCHECKSUBCARRYCINT63 + | Int63mulc -> opCHECKMULCINT63 + | Int63diveucl -> opCHECKDIVEUCLINT63 + | Int63div21 -> opCHECKDIV21INT63 + | Int63addMulDiv -> opCHECKADDMULDIVINT63 + | Int63eq -> opCHECKEQINT63 + | Int63lt -> opCHECKLTINT63 + | Int63le -> opCHECKLEINT63 + | Int63compare -> opCHECKCOMPAREINT63 let emit_instr env = function | Klabel lbl -> define_label env lbl @@ -218,7 +254,7 @@ let emit_instr env = function | Kpush_retaddr lbl -> out env opPUSH_RETADDR; out_label env lbl | Kapply n -> - if n < 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n) + if n <= 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n) | Kappterm(n, sz) -> if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz) else (out env opAPPTERM; out_int env n; out_int env sz) @@ -250,7 +286,7 @@ let emit_instr env = function Array.iter (out_label_with_orig env org) lbl_bodies | Kgetglobal q -> out env opGETGLOBAL; slot_for_getglobal env q - | Kconst (Const_b0 i) -> + | Kconst (Const_b0 i) when is_immed i -> if i >= 0 && i <= 3 then out env (opCONST0 + i) else (out env opCONSTINT; out_int env i) @@ -287,32 +323,20 @@ let emit_instr env = function | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" | 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 - (* spiwack *) | Kbranch lbl -> out env opBRANCH; out_label env lbl - | Kaddint31 -> out env opADDINT31 - | Kaddcint31 -> out env opADDCINT31 - | Kaddcarrycint31 -> out env opADDCARRYCINT31 - | Ksubint31 -> out env opSUBINT31 - | Ksubcint31 -> out env opSUBCINT31 - | Ksubcarrycint31 -> out env opSUBCARRYCINT31 - | Kmulint31 -> out env opMULINT31 - | Kmulcint31 -> out env opMULCINT31 - | Kdiv21int31 -> out env opDIV21INT31 - | Kdivint31 -> out env opDIVINT31 - | Kaddmuldivint31 -> out env opADDMULDIVINT31 - | Kcompareint31 -> out env opCOMPAREINT31 - | Khead0int31 -> out env opHEAD0INT31 - | Ktail0int31 -> out env opTAIL0INT31 - | Kisconst lbl -> out env opISCONST; out_label env lbl - | Kareconst(n,lbl) -> out env opARECONST; out_int env n; out_label env lbl - | Kcompint31 -> out env opCOMPINT31 - | Kdecompint31 -> out env opDECOMPINT31 - | Klorint31 -> out env opORINT31 - | Klandint31 -> out env opANDINT31 - | Klxorint31 -> out env opXORINT31 - (*/spiwack *) - | Kstop -> - out env opSTOP + | Kprim (op,None) -> + out env (nocheck_prim_op op) + + | Kprim(op,Some (q,_u)) -> + out env (check_prim_op op); + slot_for_getglobal env q + + | 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. *) @@ -337,7 +361,7 @@ let rec emit env insns remaining = match insns with emit env c remaining | Kpush :: Kgetglobal id :: c -> out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining - | Kpush :: Kconst (Const_b0 i) :: c -> + | Kpush :: Kconst (Const_b0 i) :: c when is_immed i -> if i >= 0 && i <= 3 then out env (opPUSHCONST0 + i) else (out env opPUSHCONSTINT; out_int env i); @@ -360,7 +384,7 @@ type to_patch = emitcodes * patches * fv (* Substitution *) let subst_strcst s sc = match sc with - | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ -> sc + | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _ -> sc | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_reloc s ri = diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 39ddf4a047..41cc641dc8 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -1,3 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names open Vmvalues open Cbytecodes diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli deleted file mode 100644 index dca1757b7d..0000000000 --- a/kernel/cinstr.mli +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -open Names -open Constr -open Vmvalues -open Cbytecodes - -(** This file defines the lambda code for the bytecode compiler. It has been -extracted from Clambda.ml because of the retroknowledge architecture. *) - -type uint = - | UintVal of Uint31.t - | UintDigits of lambda array - | UintDecomp of lambda - -and lambda = - | Lrel of Name.t * int - | Lvar of Id.t - | Levar of Evar.t * lambda array - | Lprod of lambda * lambda - | Llam of Name.t array * lambda - | Llet of Name.t * lambda * lambda - | Lapp of lambda * lambda array - | Lconst of pconstant - | Lprim of pconstant * int (* arity *) * instruction * lambda array - | Lcase of case_info * reloc_table * lambda * lambda * lam_branches - | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl (* must be in eta-expanded form *) - | Lmakeblock of int * lambda array - | Lval of structured_values - | Lsort of Sorts.t - | Lind of pinductive - | Lproj of Projection.Repr.t * lambda - | Lint of int - | Luint of uint - -(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation -to be correct. Otherwise, memoization of previous evaluations will be applied -again to extra arguments (see #7333). *) - -and lam_branches = - { constant_branches : lambda array; - nonconstant_branches : (Name.t array * lambda) array } - -and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 1e4dbfd418..5c21a5ec25 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -5,13 +5,44 @@ open Term open Constr open Declarations open Vmvalues -open Cbytecodes -open Cinstr open Environ open Pp let pr_con sp = str(Names.Label.to_string (Constant.label sp)) +type lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Levar of Evar.t * lambda array + | Lprod of lambda * lambda + | Llam of Name.t array * lambda + | Llet of Name.t * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of pconstant + | Lprim of pconstant option * CPrimitives.t * lambda array + (* No check if None *) + | 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 + | Lmakeblock of int * lambda array + | Luint of Uint63.t + | Lval of structured_values + | Lsort of Sorts.t + | Lind of pinductive + | Lproj of Projection.Repr.t * lambda + +(* We separate branches for constant and non-constant constructors. If the OCaml + limitation on non-constant constructors is reached, remaining branches are + stored in [extra_branches]. *) +and lam_branches = + { constant_branches : lambda array; + nonconstant_branches : (Name.t array * lambda) array } +(* extra_branches : (name array * lambda) array } *) + +and fix_decl = Name.t array * lambda array * lambda array + (** Printing **) let pp_names ids = @@ -77,6 +108,10 @@ 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 @@ -104,22 +139,26 @@ let rec pp_lam lam = (str "(makeblock " ++ int tag ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") + | Luint i -> str (Uint63.to_string i) | Lval _ -> str "values" | Lsort s -> pp_sort s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i - | Lprim((kn,_u),_ar,_op,args) -> - hov 1 - (str "(PRIM " ++ pr_con kn ++ spc() ++ - prlist_with_sep spc pp_lam (Array.to_list args) ++ - str")") + | Lprim(Some (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 ++ str ")") | Lint i -> Pp.(str "(int:" ++ int i ++ str ")") - | Luint _ -> - str "(uint)" (*s Constructors *) @@ -151,9 +190,9 @@ let shift subst = subs_shft (1, subst) (* A generic map function *) -let rec map_lam_with_binders g f n lam = +let map_lam_with_binders g f n lam = match lam with - | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> lam + | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> lam | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') @@ -192,6 +231,11 @@ let rec 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 @@ -205,25 +249,12 @@ let rec map_lam_with_binders g f n lam = | Lmakeblock(tag,args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Lmakeblock(tag,args') - | Lprim(kn,ar,op,args) -> + | Lprim(kn,op,args) -> let args' = Array.Smart.map (f n) args in - if args == args' then lam else Lprim(kn,ar,op,args') + if args == args' then lam else Lprim(kn,op,args') | Lproj(p,arg) -> let arg' = f n arg in if arg == arg' then lam else Lproj(p,arg') - | Luint u -> - let u' = map_uint g f n u in - if u == u' then lam else Luint u' - -and map_uint _g f n u = - match u with - | UintVal _ -> u - | UintDigits(args) -> - let args' = Array.Smart.map (f n) args in - if args == args' then u else UintDigits(args') - | UintDecomp(a) -> - let a' = f n a in - if a == a' then u else UintDecomp(a') (*s Lift and substitution *) @@ -271,28 +302,58 @@ let lam_subst_args subst args = let can_subst lam = match lam with - | Lrel _ | Lvar _ | Lconst _ + | Lrel _ | Lvar _ | Lconst _ | Luint _ | 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 | Llet(id,def,body) -> - let def' = simplify subst def in - if can_subst def' then simplify (cons def' subst) body - else - let body' = simplify (lift subst) body in - if def == def' && body == body' then lam - else Llet(id,def',body') + let def' = simplify subst def in + if can_subst def' then simplify (cons def' subst) body + else + let body' = simplify (lift subst) body in + if def == def' && body == body' then lam + else Llet(id,def',body') | Lapp(f,args) -> - begin match simplify_app subst f subst args with + begin match simplify_app subst f subst args with | Lapp(f',args') when f == f' && args == args' -> lam | lam' -> lam' - end + 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 = @@ -352,7 +413,7 @@ let rec occurrence k kind lam = if n = k then if kind then false else raise Not_found else kind - | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> kind + | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> kind | Levar (_, args) -> occurrence_args k kind args | Lprod(dom, codom) -> @@ -363,7 +424,7 @@ let rec occurrence k kind lam = occurrence (k+1) (occurrence k kind def) body | Lapp(f, args) -> occurrence_args k (occurrence k kind f) args - | Lprim(_,_,_,args) | Lmakeblock(_,args) -> + | Lprim(_,_,args) | Lmakeblock(_,args) -> occurrence_args k kind args | Lcase(_ci,_rtbl,t,a,branches) -> let kind = occurrence k (occurrence k kind t) a in @@ -374,6 +435,9 @@ 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 @@ -381,17 +445,10 @@ let rec occurrence k kind lam = kind | Lproj(_,arg) -> occurrence k kind arg - | Luint u -> occurrence_uint k kind u and occurrence_args k kind args = Array.fold_left (occurrence k) kind args -and occurrence_uint k kind u = - match u with - | UintVal _ -> kind - | UintDigits args -> occurrence_args k kind args - | UintDecomp t -> occurrence k kind t - let occur_once lam = try let _ = occurrence 1 true lam in true with Not_found -> false @@ -439,11 +496,12 @@ let check_compilable ib = let is_value lc = match lc with - | Lval _ | Lint _ -> true + | Lval _ | Lint _ | Luint _ -> true | _ -> false let get_value lc = match lc with + | Luint i -> val_of_uint i | Lval v -> v | Lint i -> val_of_int i | _ -> raise Not_found @@ -491,26 +549,18 @@ let rec get_alias env kn = (* Compilation of primitive *) -let _h = Name(Id.of_string "f") +let prim kn p args = + Lprim(Some kn, p, args) -(* let expand_prim kn op arity = let ids = Array.make arity Anonymous in let args = make_args arity 1 in Llam(ids, prim kn op args) -*) -let compile_prim n op kn fc args = - if not fc then raise Not_found - else - Lprim(kn, n, op, args) - - (* - let (nparams, arity) = CPrimitives.arity op in - let expected = nparams + arity in - if Array.length args >= expected then prim kn op args - else mkLapp (expand_prim kn op expected) args -*) +let lambda_of_prim kn op args = + let arity = CPrimitives.arity op in + if Array.length args >= arity then prim kn op args + else mkLapp (expand_prim kn op arity) args (*i Global environment *) @@ -661,13 +711,6 @@ let rec lambda_of_constr env c = (* translation of the argument *) let la = lambda_of_constr env a in - let gr = GlobRef.IndRef ind in - let la = - try - Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge - gr la - with Not_found -> la - in (* translation of the type *) let lt = lambda_of_constr env t in (* translation of branches *) @@ -713,88 +756,30 @@ let rec lambda_of_constr env c = let lc = lambda_of_constr env c in Lproj (Projection.repr p,lc) + | Int i -> Luint i + and lambda_of_app env f args = match Constr.kind f with - | Const (kn,_u as c) -> - let kn = get_alias env.global_env kn in - (* spiwack: checks if there is a specific way to compile the constant - if there is not, Not_found is raised, and the function - falls back on its normal behavior *) - (try - (* We delay the compilation of arguments to avoid an exponential behavior *) - let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge - (GlobRef.ConstRef kn) in - let args = lambda_of_args env 0 args in - f args - with Not_found -> - let cb = lookup_constant kn env.global_env in - begin match cb.const_body with + | Const (kn,u as c) -> + let kn = get_alias env.global_env kn in + let cb = lookup_constant kn env.global_env in + begin match cb.const_body with + | Primitive op -> lambda_of_prim (kn,u) op (lambda_of_args env 0 args) | Def csubst when cb.const_inline_code -> - lambda_of_app env (Mod_subst.force_constr csubst) args + lambda_of_app env (Mod_subst.force_constr csubst) args | Def _ | OpaqueDef _ | Undef _ -> mkLapp (Lconst c) (lambda_of_args env 0 args) - end) + end | Construct (c,_) -> - let tag, nparams, arity = Renv.get_construct_info env c in - let nargs = Array.length args in - let gr = GlobRef.ConstructRef c in - if Int.equal (nparams + arity) nargs then (* fully applied *) - (* spiwack: *) - (* 1/ tries to compile the constructor in an optimal way, - it is supposed to work only if the arguments are - all fully constructed, fails with Cbytecodes.NotClosed. - it can also raise Not_found when there is no special - treatment for this constructor - for instance: tries to to compile an integer of the - form I31 D1 D2 ... D31 to [D1D2...D31] as - a processor number (a caml number actually) *) - try - try - Retroknowledge.get_vm_constant_static_info - env.global_env.retroknowledge - gr args - with NotClosed -> - (* 2/ if the arguments are not all closed (this is - expectingly (and it is currently the case) the only - reason why this exception is raised) tries to - give a clever, run-time behavior to the constructor. - Raises Not_found if there is no special treatment - for this integer. - this is done in a lazy fashion, using the constructor - Bspecial because it needs to know the continuation - and such, which can't be done at this time. - for instance, for int31: if one of the digit is - not closed, it's not impossible that the number - gets fully instantiated at run-time, thus to ensure - uniqueness of the representation in the vm - it is necessary to try and build a caml integer - during the execution *) - let rargs = Array.sub args nparams arity in - let args = lambda_of_args env nparams rargs in - Retroknowledge.get_vm_constant_dynamic_info - env.global_env.retroknowledge - gr args - with Not_found -> - (* 3/ if no special behavior is available, then the compiler - falls back to the normal behavior *) + let tag, nparams, arity = Renv.get_construct_info env c in + let nargs = Array.length args in + if nparams < nargs then (* got all parameters *) let args = lambda_of_args env nparams args in makeblock tag 0 arity args - else - let args = lambda_of_args env nparams args in - (* spiwack: tries first to apply the run-time compilation - behavior of the constructor, as in 2/ above *) - (try - (Retroknowledge.get_vm_constant_dynamic_info - env.global_env.retroknowledge - gr) args - with Not_found -> - if nparams <= nargs then (* got all parameters *) - makeblock tag 0 arity args - else (* still expecting some parameters *) - makeblock tag (nparams - nargs) arity empty_args) + else makeblock tag (nparams - nargs) arity empty_args | _ -> - let f = lambda_of_constr env f in - let args = lambda_of_args env 0 args in - mkLapp f args + let f = lambda_of_constr env f in + let args = lambda_of_args env 0 args in + mkLapp f args and lambda_of_args env start args = let nargs = Array.length args in @@ -822,43 +807,3 @@ let lambda_of_constr ~optimize genv c = if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam - -(** Retroknowledge, to be removed once we move to primitive machine integers *) -let compile_structured_int31 fc args = - if not fc then raise Not_found else - Luint (UintVal - (Uint31.of_int (Array.fold_left - (fun temp_i -> fun t -> match kind t with - | Construct ((_,d),_) -> 2*temp_i+d-1 - | _ -> raise NotClosed) - 0 args))) - -let dynamic_int31_compilation fc args = - if not fc then raise Not_found else - Luint (UintDigits args) - -let d0 = Lint 0 -let d1 = Lint 1 - -(* We are relying here on the tags of digits constructors *) -let digits_from_uint i = - let digits = Array.make 31 d0 in - for k = 0 to 30 do - if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then - digits.(30-k) <- d1 - done; - digits - -let int31_escape_before_match fc t = - if not fc then - raise Not_found - else - match t with - | Luint (UintVal i) -> - let digits = digits_from_uint i in - Lmakeblock (1, digits) - | Luint (UintDigits args) -> - Lmakeblock (1,args) - | Luint (UintDecomp _) -> - assert false - | _ -> Luint (UintDecomp t) diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 8ff10b4549..4d921fd45e 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -1,7 +1,37 @@ open Names -open Cinstr +open Constr +open Vmvalues open Environ +type lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Levar of Evar.t * lambda array + | Lprod of lambda * lambda + | Llam of Name.t array * lambda + | Llet of Name.t * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of pconstant + | Lprim of pconstant option * CPrimitives.t * lambda array + (* No check if None *) + | 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 + | Lmakeblock of int * lambda array + | Luint of Uint63.t + | Lval of structured_values + | Lsort of Sorts.t + | Lind of pinductive + | Lproj of Projection.Repr.t * lambda + +and lam_branches = + { constant_branches : lambda array; + nonconstant_branches : (Name.t array * lambda) array } + +and fix_decl = Name.t array * lambda array * lambda array + exception TooLargeInductive of Pp.t val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda @@ -10,22 +40,5 @@ val decompose_Llam : lambda -> Name.t array * lambda val get_alias : env -> Constant.t -> Constant.t -val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda - -(** spiwack: this function contains the information needed to perform - the static compilation of int31 (trying and obtaining - a 31-bit integer in processor representation at compile time) *) -val compile_structured_int31 : bool -> Constr.t array -> lambda - -(** this function contains the information needed to perform - the dynamic compilation of int31 (trying and obtaining a - 31-bit integer in processor representation at runtime when - it failed at compile time *) -val dynamic_int31_compilation : bool -> lambda array -> lambda - -(*spiwack: compiling function to insert dynamic decompilation before - matching integers (in case they are in processor representation) *) -val int31_escape_before_match : bool -> lambda -> lambda - (** Dump the VM lambda code after compilation (for debugging purposes) *) val dump_lambda : bool ref diff --git a/kernel/constr.ml b/kernel/constr.ml index d67d15b23b..c392494e95 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -101,6 +101,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr + | Int of Uint63.t (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t, t, Sorts.t, Instance.t) kind_of_term @@ -233,6 +234,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with | ConstructRef c -> mkConstructU (c,u) | VarRef x -> mkVar x +(* Constructs a primitive integer *) +let mkInt i = Int i + (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -438,7 +442,7 @@ let decompose_appvect c = let fold f acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc + | Construct _ | Int _) -> acc | Cast (c,_,t) -> f (f acc c) t | Prod (_,t,c) -> f (f acc t) c | Lambda (_,t,c) -> f (f acc t) c @@ -458,7 +462,7 @@ let fold f acc c = match kind c with let iter f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () + | Construct _ | Int _) -> () | Cast (c,_,t) -> f c; f t | Prod (_,t,c) -> f t; f c | Lambda (_,t,c) -> f t; f c @@ -478,7 +482,7 @@ let iter f c = match kind c with let iter_with_binders g f n c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () + | Construct _ | Int _) -> () | Cast (c,_,t) -> f n c; f n t | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c @@ -504,7 +508,7 @@ let iter_with_binders g f n c = match kind c with let fold_constr_with_binders g f n acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc + | Construct _ | Int _) -> acc | Cast (c,_, t) -> f n (f n acc c) t | Prod (_na,t,c) -> f (g n) (f n acc t) c | Lambda (_na,t,c) -> f (g n) (f n acc t) c @@ -600,7 +604,7 @@ let map_return_predicate_with_full_binders g f l ci p = let map_gen userview f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c + | Construct _ | Int _) -> c | Cast (b,k,t) -> let b' = f b in let t' = f t in @@ -665,7 +669,7 @@ let map = map_gen false let fold_map f accu c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> accu, c + | Construct _ | Int _) -> accu, c | Cast (b,k,t) -> let accu, b' = f accu b in let accu, t' = f accu t in @@ -725,7 +729,7 @@ let fold_map f accu c = match kind c with let map_with_binders g f l c0 = match kind c0 with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c0 + | Construct _ | Int _) -> c0 | Cast (c, k, t) -> let c' = f l c in let t' = f l t in @@ -802,7 +806,7 @@ let lift n = liftn n 1 let fold_with_full_binders g f n acc c = let open Context.Rel.Declaration in match kind c with - | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ -> acc | Cast (c,_, t) -> f n (f n acc c) t | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c @@ -843,6 +847,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 + | Int i1, Int i2 -> Uint63.equal i1 i2 | Sort s1, Sort s2 -> leq_sorts s1 s2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 @@ -869,7 +874,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ - | CoFix _), _ -> false + | CoFix _ | Int _), _ -> false (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, @@ -1044,6 +1049,8 @@ let constr_ord_int f t1 t2 = ln1 ln2 tl1 tl2 bl1 bl2 | CoFix _, _ -> -1 | _, CoFix _ -> 1 | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 + | Proj _, _ -> -1 | _, Proj _ -> 1 + | Int i1, Int i2 -> Uint63.compare i1 i2 let rec compare m n= constr_ord_int compare m n @@ -1127,9 +1134,10 @@ let hasheq t1 t2 = && array_eqeq lna1 lna2 && array_eqeq tl1 tl2 && array_eqeq bl1 bl2 + | Int i1, Int i2 -> i1 == i2 | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ - | Fix _ | CoFix _), _ -> false + | Fix _ | CoFix _ | Int _), _ -> false (** Note that the following Make has the side effect of creating once and for all the table we'll use for hash-consing all constr *) @@ -1190,10 +1198,6 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Evar (e,l) -> let l, hl = hash_term_array l in (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) - | Proj (p,c) -> - let c, hc = sh_rec c in - let p' = Projection.hcons p in - (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in @@ -1232,6 +1236,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = (t, combinesmall 15 n) | Rel n -> (t, combinesmall 16 n) + | Proj (p,c) -> + let c, hc = sh_rec c in + let p' = Projection.hcons p in + (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc)) + | Int i -> + let (h,l) = Uint63.to_int2 i in + (t, combinesmall 18 (combine h l)) and sh_rec t = let (y, h) = hash_term t in @@ -1277,8 +1288,6 @@ let rec hash t = | App (Cast(c, _, _),l) -> hash (mkApp (c,l)) | App (c,l) -> combinesmall 7 (combine (hash_term_array l) (hash c)) - | Proj (p,c) -> - combinesmall 17 (combine (Projection.hash p) (hash c)) | Evar (e,l) -> combinesmall 8 (combine (Evar.hash e) (hash_term_array l)) | Const (c,u) -> @@ -1295,6 +1304,9 @@ let rec hash t = combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n + | Proj (p,c) -> + combinesmall 17 (combine (Projection.hash p) (hash c)) + | Int i -> combinesmall 18 (Uint63.hash i) and hash_term_array t = Array.fold_left (fun acc t -> combine (hash t) acc) 0 t @@ -1425,3 +1437,4 @@ let rec debug_print c = Name.print na ++ str":" ++ debug_print ty ++ cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++ str"}") + | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" diff --git a/kernel/constr.mli b/kernel/constr.mli index f2cedcdabb..fdc3296a6a 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -72,6 +72,9 @@ val mkRel : int -> constr (** Constructs a Variable *) val mkVar : Id.t -> constr +(** Constructs a machine integer *) +val mkInt : Uint63.t -> constr + (** Constructs an patvar named "?n" *) val mkMeta : metavariable -> constr @@ -228,6 +231,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr + | Int of Uint63.t (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f4b4834d98..88586352f6 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -155,7 +155,7 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool type result = { - cook_body : constant_def; + cook_body : constr Mod_subst.substituted constant_def; cook_type : types; cook_universes : constant_universes; cook_private_univs : Univ.ContextSet.t option; @@ -169,6 +169,7 @@ let on_body ml hy f = function | OpaqueDef o -> OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f { Opaqueproof.modlist = ml; abstract = hy } o) + | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") let expmod_constr_subst cache modlist subst c = let subst = Univ.make_instance_subst subst in diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7ff4b657d3..07c6f37fab 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -18,7 +18,7 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool type result = { - cook_body : constant_def; + cook_body : constr Mod_subst.substituted constant_def; cook_type : types; cook_universes : constant_universes; cook_private_univs : Univ.ContextSet.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 016b63be09..1008492825 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -47,10 +47,11 @@ type inline = int option transparent body, or an opaque one *) (* Global declarations (i.e. constants) can be either: *) -type constant_def = +type 'a constant_def = | Undef of inline (** a global assumption *) - | Def of constr Mod_subst.substituted (** or a transparent global definition *) + | Def of 'a (** or a transparent global definition *) | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) + | Primitive of CPrimitives.t (** or a primitive operation *) type constant_universes = | Monomorphic_const of Univ.ContextSet.t @@ -88,7 +89,7 @@ type typing_flags = { * the OpaqueDef *) type constant_body = { const_hyps : Constr.named_context; (** New: younger hyp at top *) - const_body : constant_def; + const_body : Constr.t Mod_subst.substituted constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 707c46048b..5686c4071d 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -56,8 +56,9 @@ let constant_is_polymorphic cb = | Monomorphic_const _ -> false | Polymorphic_const _ -> true + let constant_has_body cb = match cb.const_body with - | Undef _ -> false + | Undef _ | Primitive _ -> false | Def _ | OpaqueDef _ -> true let constant_polymorphic_context cb = @@ -67,7 +68,7 @@ let constant_polymorphic_context cb = let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true - | Undef _ | Def _ -> false + | Undef _ | Def _ | Primitive _ -> false (** {7 Constant substitutions } *) @@ -83,7 +84,7 @@ let subst_const_type sub arity = (** No need here to check for physical equality after substitution, at least for Def due to the delayed substitution [subst_constr_subst]. *) let subst_const_def sub def = match def with - | Undef _ -> def + | Undef _ | Primitive _ -> def | Def c -> Def (subst_constr sub c) | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) @@ -119,6 +120,7 @@ let hcons_rel_context l = List.Smart.map hcons_rel_decl l let hcons_const_def = function | Undef inl -> Undef inl + | Primitive p -> Primitive p | Def l_constr -> let constr = force_constr l_constr in Def (from_val (Constr.hcons constr)) diff --git a/kernel/dune b/kernel/dune index 01abdb8f67..79161519ba 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules_without_implementation cinstr nativeinstr) + (modules (:standard \ uint63_x86 uint63_amd64 write_uint63)) (libraries lib byterun)) (rule @@ -11,6 +11,16 @@ (deps (:h-file byterun/coq_instruct.h) make-opcodes) (action (run ./make_opcodes.sh %{h-file} %{targets}))) +(executable + (name write_uint63) + (modules write_uint63) + (libraries unix)) + +(rule + (targets uint63.ml) + (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml) + (action (run %{gen}))) + (documentation (package coq)) diff --git a/kernel/entries.ml b/kernel/entries.ml index 58bb782f15..013327599d 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -87,9 +87,16 @@ type inline = int option (* inlining level, None for no inlining *) type parameter_entry = Constr.named_context option * types in_constant_universes_entry * inline +type primitive_entry = { + prim_entry_type : types option; + prim_entry_univs : Univ.ContextSet.t; (* always monomorphic *) + prim_entry_content : CPrimitives.op_or_type; +} + type 'a constant_entry = | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry + | PrimitiveEntry of primitive_entry (** {6 Modules } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 77820a301e..02f38e7214 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -119,7 +119,7 @@ let empty_env = { env_universes = UGraph.initial_universes; env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; - retroknowledge = Retroknowledge.initial_retroknowledge; + retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab } @@ -450,7 +450,10 @@ let constant_type env (kn,u) = let csts = Univ.AUContext.instantiate u uctx in (subst_instance_constr u cb.const_type, csts) -type const_evaluation_result = NoBody | Opaque +type const_evaluation_result = + | NoBody + | Opaque + | IsPrimitive of CPrimitives.t exception NotEvaluableConst of const_evaluation_result @@ -461,14 +464,14 @@ let constant_value_and_type env (kn, u) = let b' = match cb.const_body with | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) | OpaqueDef _ -> None - | Undef _ -> None + | Undef _ | Primitive _ -> None in b', subst_instance_constr u cb.const_type, cst let body_of_constant_body env cb = let otab = opaque_tables env in match cb.const_body with - | Undef _ -> + | Undef _ | Primitive _ -> None | Def c -> Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) @@ -492,6 +495,7 @@ let constant_value_in env (kn,u) = subst_instance_constr u b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) + | Primitive p -> raise (NotEvaluableConst (IsPrimitive p)) let constant_opt_value_in env cst = try Some (constant_value_in env cst) @@ -503,7 +507,13 @@ let evaluable_constant kn env = match cb.const_body with | Def _ -> true | OpaqueDef _ -> false - | Undef _ -> false + | Undef _ | Primitive _ -> false + +let is_primitive env c = + let cb = lookup_constant c env in + match cb.Declarations.const_body with + | Declarations.Primitive _ -> true + | _ -> false let polymorphic_constant cst env = Declareops.constant_is_polymorphic (lookup_constant cst env) @@ -743,29 +753,4 @@ let is_type_in_type env r = | IndRef ind -> type_in_type_ind ind env | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env -(*spiwack: the following functions assemble the pieces of the retroknowledge - note that the "consistent" register function is available in the module - Safetyping, Environ only synchronizes the proactive and the reactive parts*) - -open Retroknowledge - -(* lifting of the "get" functions works also for "mem"*) -let retroknowledge f env = - f env.retroknowledge - -let registered env field = - retroknowledge mem env field - -let register_one env field entry = - { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry } - -(* [register env field entry] may register several fields when needed *) -let register env field gr = - match field with - | KInt31 Int31Type -> - let i31c = match gr with - | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1) - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") - in - register_one (register_one env (KInt31 Int31Constructor) i31c) field gr - | field -> register_one env field gr +let set_retroknowledge env r = { env with retroknowledge = r } diff --git a/kernel/environ.mli b/kernel/environ.mli index 6d4d3b282b..8d5bd85b94 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -195,11 +195,15 @@ val type_in_type_constant : Constant.t -> env -> bool (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if - [c] is opaque and [NotEvaluableConst NoBody] if it has no - body and [NotEvaluableConst IsProj] if [c] is a projection + [c] is opaque, [NotEvaluableConst NoBody] if it has no + body, [NotEvaluableConst IsProj] if [c] is a projection, + [NotEvaluableConst (IsPrimitive p)] if [c] is primitive [p] and [Not_found] if it does not exist in [env] *) -type const_evaluation_result = NoBody | Opaque +type const_evaluation_result = + | NoBody + | Opaque + | IsPrimitive of CPrimitives.t exception NotEvaluableConst of const_evaluation_result val constant_type : env -> Constant.t puniverses -> types constrained @@ -223,6 +227,8 @@ val constant_value_in : env -> Constant.t puniverses -> constr val constant_type_in : env -> Constant.t puniverses -> types val constant_opt_value_in : env -> Constant.t puniverses -> constr option +val is_primitive : env -> Constant.t -> bool + (** {6 Primitive projections} *) (** Checks that the number of parameters is correct. *) @@ -334,13 +340,8 @@ val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool val is_type_in_type : env -> GlobRef.t -> bool -open Retroknowledge -(** functions manipulating the retroknowledge - @author spiwack *) - -val registered : env -> field -> bool - -val register : env -> field -> GlobRef.t -> env - (** Native compiler *) val no_link_info : link_info + +(** Primitives *) +val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 05c5c0e821..c62d0e7ded 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -804,7 +804,7 @@ let rec subterm_specif renv stack t = | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ - | Construct _ | CoFix _ -> Not_subterm + | Construct _ | CoFix _ | Int _ -> Not_subterm (* Other terms are not subterms *) @@ -1008,7 +1008,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(c,l)) end - | Sort _ -> + | Sort _ | Int _ -> assert (List.is_empty l) (* l is not checked because it is considered as the meta's context *) @@ -1194,7 +1194,8 @@ let check_one_cofix env nbfix def deftype = | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ - | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in + | Ind _ | Fix _ | Proj _ | Int _ -> + raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in let vlra = lookup_subterms env mind in diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 0b10e788b6..5108744bde 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,6 +1,7 @@ Names TransparentState -Uint31 +Uint63 +CPrimitives Univ UGraph Esubst @@ -19,11 +20,11 @@ Opaqueproof Declarations Entries Nativevalues -CPrimitives Declareops Retroknowledge Conv_oracle Environ +Primred CClosure Reduction Clambda diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 52fb39e1d0..cd675653cb 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -330,6 +330,19 @@ let subst_proj_repr sub p = let subst_proj sub p = Projection.map (subst_mind sub) p +let subst_retro_action subst action = + let open Retroknowledge in + match action with + | Register_ind(prim,ind) -> + let ind' = subst_ind subst ind in + if ind == ind' then action else Register_ind(prim, ind') + | Register_type(prim,c) -> + let c' = subst_constant subst c in + if c == c' then action else Register_type(prim, c') + | Register_inline(c) -> + let c' = subst_constant subst c in + if c == c' then action else Register_inline(c') + (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index ea391b3de7..8ab3d04402 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -144,6 +144,8 @@ val subst_constant : val subst_proj_repr : substitution -> Projection.Repr.t -> Projection.Repr.t val subst_proj : substitution -> Projection.t -> Projection.t +val subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.action + (** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index d63dc057b4..f68dd158c2 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -68,12 +68,12 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = if List.is_empty idl then (* Toplevel definition *) let cb = match spec with - | SFBconst cb -> cb - | _ -> error_not_a_constant lab + | SFBconst cb -> cb + | _ -> error_not_a_constant lab in (* In the spirit of subtyping.check_constant, we accept any implementations of parameters and opaques terms, - as long as they have the right type *) + as long as they have the right type *) let c', univs, ctx' = match cb.const_universes, ctx with | Monomorphic_const _, None -> @@ -87,6 +87,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Def cs -> let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' + | Primitive _ -> + error_incorrect_with_constraint lab in c', Monomorphic_const Univ.ContextSet.empty, cst | Polymorphic_const uctx, Some ctx -> @@ -95,52 +97,54 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = error_incorrect_with_constraint lab in (** Terms are compared in a context with De Bruijn universe indices *) - let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in - let cst = match cb.const_body with - | Undef _ | OpaqueDef _ -> - let j = Typeops.infer env' c in - let typ = cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in - cst' - | Def cs -> - let c' = Mod_subst.force_constr cs in - let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in - cst' - in - if not (Univ.Constraint.is_empty cst) then - error_incorrect_with_constraint lab; - c, Polymorphic_const ctx, Univ.Constraint.empty + let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in + let cst = match cb.const_body with + | Undef _ | OpaqueDef _ -> + let j = Typeops.infer env' c in + let typ = cb.const_type in + let cst' = Reduction.infer_conv_leq env' (Environ.universes env') + j.uj_type typ in + cst' + | Def cs -> + let c' = Mod_subst.force_constr cs in + let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in + cst' + | Primitive _ -> + error_incorrect_with_constraint lab + in + if not (Univ.Constraint.is_empty cst) then + error_incorrect_with_constraint lab; + c, Polymorphic_const ctx, Univ.Constraint.empty | _ -> error_incorrect_with_constraint lab in let def = Def (Mod_subst.from_val c') in -(* let ctx' = Univ.UContext.make (newus, cst) in *) + (* let ctx' = Univ.UContext.make (newus, cst) in *) let cb' = - { cb with - const_body = def; + { cb with + const_body = def; const_universes = univs ; - const_body_code = Option.map Cemitcodes.from_val - (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) } + const_body_code = Option.map Cemitcodes.from_val + (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else (* Definition inside a sub-module *) let mb = match spec with - | SFBmodule mb -> mb - | _ -> error_not_a_module (Label.to_string lab) + | SFBmodule mb -> mb + | _ -> error_not_a_module (Label.to_string lab) in begin match mb.mod_expr with - | Abstract -> - let struc = Modops.destr_nofunctor mb.mod_type in - let struc',c',cst = - check_with_def env' struc (idl,(c,ctx)) (MPdot(mp,lab)) mb.mod_delta - in - let mb' = { mb with - mod_type = NoFunctor struc'; - mod_type_alg = None } - in - before@(lab,SFBmodule mb')::after, c', cst - | _ -> error_generative_module_expected lab + | Abstract -> + let struc = Modops.destr_nofunctor mb.mod_type in + let struc',c',cst = + check_with_def env' struc (idl,(c,ctx)) (MPdot(mp,lab)) mb.mod_delta + in + let mb' = { mb with + mod_type = NoFunctor struc'; + mod_type_alg = None } + in + before@(lab,SFBmodule mb')::after, c', cst + | _ -> error_generative_module_expected lab end with | Not_found -> error_no_such_label lab diff --git a/kernel/modops.ml b/kernel/modops.ml index 97ac3cdebb..1dc8eec0da 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -197,9 +197,18 @@ let rec subst_structure sub do_delta sign = in List.Smart.map subst_body sign +and subst_retro : type a. Mod_subst.substitution -> a module_retroknowledge -> a module_retroknowledge = + fun subst retro -> + match retro with + | ModTypeRK as r -> r + | ModBodyRK l as r -> + let l' = List.Smart.map (subst_retro_action subst) l in + if l == l' then r else ModBodyRK l + and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> - let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; _ } = mb in + let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; + mod_retroknowledge=retro; _ } = mb in let mp' = subst_mp sub mp in let sub = if ModPath.equal mp mp' then sub @@ -209,8 +218,10 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> let ty' = subst_signature sub do_delta ty in let me' = subst_impl sub me in let aty' = Option.Smart.map (subst_expression sub id_delta) aty in + let retro' = subst_retro sub retro in let delta' = do_delta mb.mod_delta sub in - if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta + if mp==mp' && me==me' && ty==ty' && aty==aty' + && retro==retro' && delta'==mb.mod_delta then mb else { mb with @@ -218,7 +229,9 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> mod_expr = me'; mod_type = ty'; mod_type_alg = aty'; - mod_delta = delta' } + mod_retroknowledge = retro'; + mod_delta = delta'; + } and subst_module sub do_delta mb = subst_body true sub subst_impl do_delta mb @@ -259,32 +272,12 @@ let do_delta_dom_codom reso sub = subst_dom_codom_delta_resolver sub reso let subst_signature subst = subst_signature subst do_delta_codom let subst_structure subst = subst_structure subst do_delta_codom -(** {6 Retroknowledge } *) - -(* spiwack: here comes the function which takes care of importing - the retroknowledge declared in the library *) -(* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) -let add_retroknowledge = - let perform rkaction env = match rkaction with - | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) -> - Environ.register env f e - | _ -> - CErrors.anomaly ~label:"Modops.add_retroknowledge" - (Pp.str "had to import an unsupported kind of term.") - in - fun (ModBodyRK lclrk) env -> - (* The order of the declaration matters, for instance (and it's at the - time this comment is being written, the only relevent instance) the - int31 type registration absolutely needs int31 bits to be registered. - Since the local_retroknowledge is stored in reverse order (each new - registration is added at the top of the list) we need a fold_right - for things to go right (the pun is not intented). So we lose - tail recursivity, but the world will have exploded before any module - imports 10 000 retroknowledge registration.*) - List.fold_right perform lclrk env - (** {6 Adding a module in the environment } *) +let add_retroknowledge r env = + match r with + | ModBodyRK l -> List.fold_left Primred.add_retroknowledge env l + let rec add_structure mp sign resolver linkinfo env = let add_one env (l,elem) = match elem with |SFBconst cb -> @@ -399,7 +392,7 @@ let inline_delta_resolver env inl mp mbid mtb delta = let constant = lookup_constant con env in let l = make_inline delta r in match constant.const_body with - | Undef _ | OpaqueDef _ -> l + | Undef _ | OpaqueDef _ | Primitive _ -> l | Def body -> let constr = Mod_subst.force_constr body in let ctx = Declareops.constant_polymorphic_context constant in diff --git a/kernel/modops.mli b/kernel/modops.mli index 0acd09fb12..bb97f0171e 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -57,6 +57,8 @@ val add_linked_module : module_body -> link_info -> env -> env (** same, for a module type *) val add_module_type : ModPath.t -> module_type_body -> env -> env +val add_retroknowledge : module_implementation module_retroknowledge -> env -> env + (** {6 Strengthening } *) val strengthen : module_type_body -> ModPath.t -> module_type_body diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 482a2f3a3c..c32bdb85d6 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -14,7 +14,6 @@ open Constr open Declarations open Util open Nativevalues -open Nativeinstr open Nativelambda open Environ @@ -286,8 +285,6 @@ type primitive = | Mk_int | Mk_bool | Val_to_int - | Mk_I31_accu - | Decomp_uint | Mk_meta | Mk_evar | MLand @@ -305,7 +302,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of CPrimitives.t * (prefix * Constant.t) option + | Coq_primitive of CPrimitives.t * (prefix * pconstant) option let eq_primitive p1 p2 = match p1, p2 with @@ -351,29 +348,27 @@ let primitive_hash = function | Mk_int -> 16 | Mk_bool -> 17 | Val_to_int -> 18 - | Mk_I31_accu -> 19 - | Decomp_uint -> 20 - | Mk_meta -> 21 - | Mk_evar -> 22 - | MLand -> 23 - | MLle -> 24 - | MLlt -> 25 - | MLinteq -> 26 - | MLlsl -> 27 - | MLlsr -> 28 - | MLland -> 29 - | MLlor -> 30 - | MLlxor -> 31 - | MLadd -> 32 - | MLsub -> 33 - | MLmul -> 34 - | MLmagic -> 35 - | Coq_primitive (prim, None) -> combinesmall 36 (CPrimitives.hash prim) - | Coq_primitive (prim, Some (prefix,kn)) -> - combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) - | Mk_proj -> 38 - | MLarrayget -> 39 - | Mk_empty_instance -> 40 + | Mk_meta -> 19 + | Mk_evar -> 20 + | MLand -> 21 + | MLle -> 22 + | MLlt -> 23 + | MLinteq -> 24 + | MLlsl -> 25 + | MLlsr -> 26 + | MLland -> 27 + | MLlor -> 28 + | MLlxor -> 29 + | MLadd -> 30 + | MLsub -> 31 + | MLmul -> 32 + | MLmagic -> 33 + | Coq_primitive (prim, None) -> combinesmall 34 (CPrimitives.hash prim) + | Coq_primitive (prim, Some (prefix,(kn,_))) -> + combinesmall 35 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) + | Mk_proj -> 36 + | MLarrayget -> 37 + | Mk_empty_instance -> 38 type mllambda = | MLlocal of lname @@ -389,7 +384,7 @@ type mllambda = | MLconstruct of string * constructor * mllambda array (* prefix, constructor name, arguments *) | MLint of int - | MLuint of Uint31.t + | MLuint of Uint63.t | MLsetref of string * mllambda | MLsequence of mllambda * mllambda | MLarray of mllambda array @@ -455,7 +450,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = | MLint i1, MLint i2 -> Int.equal i1 i2 | MLuint i1, MLuint i2 -> - Uint31.equal i1 i2 + Uint63.equal i1 i2 | MLsetref (id1, ml1), MLsetref (id2, ml2) -> String.equal id1 id2 && eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 @@ -534,7 +529,7 @@ let rec hash_mllambda gn n env t = | MLint i -> combinesmall 11 i | MLuint i -> - combinesmall 12 (Uint31.to_int i) + combinesmall 12 (Uint63.hash i) | MLsetref (id, ml) -> let hid = String.hash id in let hml = hash_mllambda gn n env ml in @@ -947,9 +942,10 @@ let merge_branches t = Array.iter (fun (c,args,body) -> insert (c,args) body newt) t; Array.of_list (to_list newt) +let app_prim p args = MLapp(MLprimitive p, args) -type prim_aux = - | PAprim of string * Constant.t * CPrimitives.t * prim_aux array +type prim_aux = + | PAprim of string * pconstant * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -962,97 +958,67 @@ let add_check cond args = | _ -> cond in Array.fold_left aux cond args - + let extract_prim ml_of l = let decl = ref [] in let cond = ref [] in - let rec aux l = + let rec aux l = match l with | Lprim(prefix,kn,p,args) -> - let args = Array.map aux args in - cond := add_check !cond args; - PAprim(prefix,kn,p,args) + let args = Array.map aux args in + cond := add_check !cond args; + PAprim(prefix,kn,p,args) | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l) - | _ -> - let x = fresh_lname Anonymous in - decl := (x,ml_of l)::!decl; - PAml (MLlocal x) in + | _ -> + let x = fresh_lname Anonymous in + decl := (x,ml_of l)::!decl; + PAml (MLlocal x) in let res = aux l in (!decl, !cond, res) -let app_prim p args = MLapp(MLprimitive p, args) - -let to_int v = +let cast_to_int v = match v with - | MLapp(MLprimitive Mk_uint, t) -> - begin match t.(0) with - | MLuint i -> MLint (Uint31.to_int i) - | _ -> MLapp(MLprimitive Val_to_int, [|v|]) - end - | MLapp(MLprimitive Mk_int, t) -> t.(0) - | _ -> MLapp(MLprimitive Val_to_int, [|v|]) - -let of_int v = - match v with - | MLapp(MLprimitive Val_to_int, t) -> t.(0) - | _ -> MLapp(MLprimitive Mk_int,[|v|]) + | MLint _ -> v + | _ -> MLapp(MLprimitive Val_to_int, [|v|]) let compile_prim decl cond paux = -(* - let args_to_int args = - for i = 0 to Array.length args - 1 do - args.(i) <- to_int args.(i) - done; - args in - *) + let rec opt_prim_aux paux = match paux with | PAprim(_prefix, _kn, op, args) -> - let args = Array.map opt_prim_aux args in - app_prim (Coq_primitive(op,None)) args -(* - TODO: check if this inlining was useful - begin match op with - | Int31lt -> - if Sys.word_size = 64 then - app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|] - else app_prim (Coq_primitive (CPrimitives.Int31lt,None)) args - | Int31le -> - if Sys.word_size = 64 then - app_prim Mk_bool [|(app_prim MLle (args_to_int args))|] - else app_prim (Coq_primitive (CPrimitives.Int31le, None)) args - | Int31lsl -> of_int (mk_lsl (args_to_int args)) - | Int31lsr -> of_int (mk_lsr (args_to_int args)) - | Int31land -> of_int (mk_land (args_to_int args)) - | Int31lor -> of_int (mk_lor (args_to_int args)) - | Int31lxor -> of_int (mk_lxor (args_to_int args)) - | Int31add -> of_int (mk_add (args_to_int args)) - | Int31sub -> of_int (mk_sub (args_to_int args)) - | Int31mul -> of_int (mk_mul (args_to_int args)) - | _ -> app_prim (Coq_primitive(op,None)) args - end *) - | PAml ml -> ml - and naive_prim_aux paux = + let args = Array.map opt_prim_aux args in + app_prim (Coq_primitive(op,None)) args + | PAml ml -> ml + + and naive_prim_aux paux = match paux with | PAprim(prefix, kn, op, args) -> - app_prim (Coq_primitive(op, Some (prefix, kn))) (Array.map naive_prim_aux args) - | PAml ml -> ml in + app_prim (Coq_primitive(op, Some (prefix,kn))) (Array.map naive_prim_aux args) + | PAml ml -> ml + in - let compile_cond cond paux = + let compile_cond cond paux = match cond with - | [] -> opt_prim_aux paux + | [] -> opt_prim_aux paux | [c1] -> - MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux) + MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux) | c1::cond -> - let cond = - List.fold_left - (fun ml c -> app_prim MLland [| ml; to_int c|]) - (app_prim MLland [|to_int c1; MLint 0 |]) cond in - let cond = app_prim MLmagic [|cond|] in - MLif(cond, naive_prim_aux paux, opt_prim_aux paux) in + let cond = + List.fold_left + (fun ml c -> app_prim MLland [| ml; cast_to_int c|]) + (app_prim MLland [| cast_to_int c1; MLint 0 |]) cond in + let cond = app_prim MLmagic [|cond|] in + MLif(cond, naive_prim_aux paux, opt_prim_aux paux) in + let add_decl decl body = List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in - add_decl decl (compile_cond cond paux) + + (* The optimizations done for checking if integer values are closed are valid + only on 64-bit architectures. So on 32-bit architectures, we fall back to less optimized checks. *) + if max_int = 1073741823 (* 32-bits *) then + add_decl decl (naive_prim_aux paux) + else + add_decl decl (compile_cond cond paux) let ml_of_instance instance u = let ml_of_level l = @@ -1089,6 +1055,11 @@ let ml_of_instance instance u = | Llam(ids,body) -> let lnames,env = push_rels env ids in MLlam(lnames, ml_of_lam env l body) + | Lrec(id,body) -> + let ids,body = decompose_Llam body in + let lname, env = push_rel env id in + let lnames, env = push_rels env ids in + MLletrec([|lname, lnames, ml_of_lam env l body|], MLlocal lname) | Llet(id,def,body) -> let def = ml_of_lam env l def in let lname, env = push_rel env id in @@ -1101,8 +1072,8 @@ let ml_of_instance instance u = mkMLapp (MLglobal(Gconstant (prefix, c))) args | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> - let decl,cond,paux = extract_prim (ml_of_lam env l) t in - compile_prim decl cond paux + let decl,cond,paux = extract_prim (ml_of_lam env l) t in + compile_prim decl cond paux | Lcase (annot,p,a,bs) -> (* let predicate_uid fv_pred = compilation of p let rec case_uid fv a_uid = @@ -1311,18 +1282,7 @@ let ml_of_instance instance u = | Lconstruct (prefix, (cn,u)) -> let uargs = ml_of_instance env.env_univ u in mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs - | Luint v -> - (match v with - | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) - | UintDigits (prefix,cn,ds) -> - let c = MLglobal (Gconstruct (prefix, cn)) in - let ds = Array.map (ml_of_lam env l) ds in - let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in - MLapp(i31, ds) - | UintDecomp (prefix,cn,t) -> - let c = MLglobal (Gconstruct (prefix, cn)) in - let t = ml_of_lam env l t in - MLapp (MLprimitive Decomp_uint, [|c;t|])) + | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | Lval v -> let i = push_symbol (SymbValue v) in get_value_code i | Lsort s -> @@ -1646,7 +1606,7 @@ let pp_mllam fmt l = Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" (string_of_construct prefix c) pp_cargs args | MLint i -> pp_int fmt i - | MLuint i -> Format.fprintf fmt "(Uint31.of_int %a)" pp_int (Uint31.to_int i) + | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i) | MLsetref (s, body) -> Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body | MLsequence(l1,l2) -> @@ -1766,8 +1726,6 @@ let pp_mllam fmt l = | Mk_int -> Format.fprintf fmt "mk_int" | Mk_bool -> Format.fprintf fmt "mk_bool" | Val_to_int -> Format.fprintf fmt "val_to_int" - | Mk_I31_accu -> Format.fprintf fmt "mk_I31_accu" - | Decomp_uint -> Format.fprintf fmt "decomp_uint" | Mk_meta -> Format.fprintf fmt "mk_meta_accu" | Mk_evar -> Format.fprintf fmt "mk_evar_accu" | MLand -> Format.fprintf fmt "(&&)" @@ -1787,9 +1745,9 @@ let pp_mllam fmt l = | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" | Coq_primitive (op,None) -> Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op) - | Coq_primitive (op, Some (prefix,kn)) -> + | Coq_primitive (op, Some (prefix,(c,_))) -> Format.fprintf fmt "%s %a" (CPrimitives.to_string op) - pp_mllam (MLglobal (Gconstant (prefix, kn))) + pp_mllam (MLglobal (Gconstant (prefix,c))) in Format.fprintf fmt "@[%a@]" pp_mllam l @@ -1903,7 +1861,7 @@ let compile_constant env sigma prefix ~interactive con cb = 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"); - let is_lazy = is_lazy env prefix t in + let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in let name = if interactive then LinkedInteractive prefix diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index f5d7ab3c9d..baa290367f 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -34,6 +34,8 @@ let rec conv_val env pb lvl v1 v2 cu = conv_accu env pb lvl k1 k2 cu | Vconst i1, Vconst i2 -> if Int.equal i1 i2 then cu else raise NotConvertible + | Vint64 i1, Vint64 i2 -> + if Int64.equal i1 i2 then cu else raise NotConvertible | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -47,7 +49,7 @@ let rec conv_val env pb lvl v1 v2 cu = aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu - | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible + | Vaccu _, _ | Vconst _, _ | Vint64 _, _ | Vblock _, _ -> raise NotConvertible and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli deleted file mode 100644 index 2d8e2ba2f0..0000000000 --- a/kernel/nativeinstr.mli +++ /dev/null @@ -1,59 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -open Names -open Constr -open Nativevalues - -(** This file defines the lambda code for the native compiler. It has been -extracted from Nativelambda.ml because of the retroknowledge architecture. *) - -type prefix = string - -type uint = - | UintVal of Uint31.t - | UintDigits of prefix * constructor * lambda array - | UintDecomp of prefix * constructor * lambda - -and lambda = - | Lrel of Name.t * int - | Lvar of Id.t - | Lmeta of metavariable * lambda (* type *) - | Levar of Evar.t * lambda array (* arguments *) - | Lprod of lambda * lambda - | Llam of Name.t array * lambda - | Llet of Name.t * lambda * lambda - | Lapp of lambda * lambda array - | Lconst of prefix * pconstant - | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) - | Lprim of prefix * Constant.t * CPrimitives.t * lambda array - | Lcase of annot_sw * lambda * lambda * lam_branches - (* annotations, term being matched, accu, branches *) - | Lif of lambda * lambda * lambda - | Lfix of (int array * (string * inductive) array * int) * fix_decl - | Lcofix of int * fix_decl (* must be in eta-expanded form *) - | Lmakeblock of prefix * pconstructor * int * lambda array - (* prefix, constructor name, constructor tag, arguments *) - (* A fully applied constructor *) - | Lconstruct of prefix * pconstructor - (* A partially applied constructor *) - | Luint of uint - | Lval of Nativevalues.t - | Lsort of Sorts.t - | Lind of prefix * pinductive - | Llazy - | Lforce - -(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation -to be correct. Otherwise, memoization of previous evaluations will be applied -again to extra arguments (see #7333). *) - -and lam_branches = (constructor * Name.t array * lambda) array - -and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 70cb8691c6..0869f94042 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,12 +14,46 @@ open Constr open Declarations open Environ open Nativevalues -open Nativeinstr module RelDecl = Context.Rel.Declaration - -exception NotClosed +(** This file defines the lambda code generation phase of the native compiler *) +type prefix = string + +type lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Lmeta of metavariable * lambda (* type *) + | Levar of Evar.t * lambda array (* arguments *) + | Lprod of lambda * lambda + | Llam of Name.t array * lambda + | Lrec of Name.t * lambda + | Llet of Name.t * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of prefix * pconstant + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) + | Lprim of prefix * pconstant * CPrimitives.t * lambda array + (* No check if None *) + | Lcase of annot_sw * lambda * lambda * lam_branches + (* annotations, term being matched, accu, branches *) + | Lif of lambda * lambda * lambda + | Lfix of (int array * (string * inductive) array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of prefix * pconstructor * int * lambda array + (* prefix, constructor Name.t, constructor tag, arguments *) + (* A fully applied constructor *) + | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *) + (* A partially applied constructor *) + | Luint of Uint63.t + | Lval of Nativevalues.t + | Lsort of Sorts.t + | Lind of prefix * pinductive + | Llazy + | Lforce + +and lam_branches = (constructor * Name.t array * lambda) array + +and fix_decl = Name.t array * lambda array * lambda array type evars = { evars_val : existential -> constr option; @@ -84,9 +118,9 @@ let get_const_prefix env c = (* A generic map function *) -let rec map_lam_with_binders g f n lam = +let map_lam_with_binders g f n lam = match lam with - | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ + | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _ | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in @@ -95,6 +129,9 @@ let rec map_lam_with_binders g f n lam = | Llam(ids,body) -> let body' = f (g (Array.length ids) n) body in if body == body' then lam else mkLlam ids body' + | Lrec(id,body) -> + let body' = f (g 1 n) body in + if body == body' then lam else Lrec(id,body') | Llet(id,def,body) -> let def' = f n def in let body' = f (g 1 n) body in @@ -135,23 +172,10 @@ let rec map_lam_with_binders g f n lam = | Lmakeblock(prefix,cn,tag,args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Lmakeblock(prefix,cn,tag,args') - | Luint u -> - let u' = map_uint g f n u in - if u == u' then lam else Luint u' | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') -and map_uint _g f n u = - match u with - | UintVal _ -> u - | UintDigits(prefix,c,args) -> - let args' = Array.Smart.map (f n) args in - if args == args' then u else UintDigits(prefix,c,args') - | UintDecomp(prefix,c,a) -> - let a' = f n a in - if a == a' then u else UintDecomp(prefix,c,a') - (*s Lift and substitution *) let rec lam_exlift el lam = @@ -186,7 +210,7 @@ let lam_subst_args subst args = (* [simplify subst lam] simplify the expression [lam_subst subst lam] *) (* that is : *) (* - Reduce [let] is the definition can be substituted i.e: *) -(* - a variable (rel or identifier) *) +(* - a variable (rel or Id.t) *) (* - a constant *) (* - a structured constant *) (* - a function *) @@ -298,7 +322,7 @@ let is_value lc = match lc with | Lval _ -> true | Lmakeblock(_,_,_,args) when Array.is_empty args -> true - | Luint (UintVal _) -> true + | Luint _ -> true | _ -> false let get_value lc = @@ -306,7 +330,7 @@ let get_value lc = | Lval v -> v | Lmakeblock(_,_,tag,args) when Array.is_empty args -> Nativevalues.mk_int tag - | Luint (UintVal i) -> Nativevalues.mk_uint i + | Luint i -> Nativevalues.mk_uint i | _ -> raise Not_found let make_args start _end = @@ -333,6 +357,20 @@ let rec get_alias env (kn, u as p) = | Cemitcodes.BCalias kn' -> get_alias env (kn', u) | _ -> p +let prim env kn p args = + let prefix = get_const_prefix env (fst kn) in + Lprim(prefix, kn, p, args) + +let expand_prim env kn op arity = + let ids = Array.make arity Anonymous in + let args = make_args arity 1 in + Llam(ids, prim env kn op args) + +let lambda_of_prim env kn op args = + let arity = CPrimitives.arity op in + if Array.length args >= arity then prim env kn op args + else mkLapp (expand_prim env kn op arity) args + (*i Global environment *) let get_names decl = @@ -368,22 +406,9 @@ module Cache = r end -let is_lazy env prefix t = - match kind t with - | App (f,_args) -> - begin match kind f with - | Construct (c,_) -> - let gr = GlobRef.IndRef (fst c) in - (try - let _ = - Retroknowledge.get_native_before_match_info env.retroknowledge - gr prefix c Llazy; - in - false - with Not_found -> true) - | _ -> true - end - | LetIn _ | Case _ | Proj _ -> true +let is_lazy t = + match Constr.kind t with + | App _ | LetIn _ | Case _ | Proj _ -> true | _ -> false let evar_value sigma ev = sigma.evars_val ev @@ -482,13 +507,6 @@ let rec lambda_of_constr cache env sigma c = in (* translation of the argument *) let la = lambda_of_constr cache env sigma a in - let gr = GlobRef.IndRef ind in - let la = - try - Retroknowledge.get_native_before_match_info (env).retroknowledge - gr prefix (ind,1) la - with Not_found -> la - in (* translation of the type *) let lt = lambda_of_constr cache env sigma t in (* translation of branches *) @@ -519,7 +537,7 @@ let rec lambda_of_constr cache env sigma c = let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in let lbodies = lambda_of_args cache env sigma 0 rec_bodies in Lfix((pos, inds, i), (names, ltypes, lbodies)) - + | CoFix(init,(names,type_bodies,rec_bodies)) -> let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in let ltypes = lambda_of_args cache env sigma 0 type_bodies in @@ -527,27 +545,22 @@ let rec lambda_of_constr cache env sigma c = let lbodies = lambda_of_args cache env sigma 0 rec_bodies in Lcofix(init, (names, ltypes, lbodies)) + | Int i -> Luint i + and lambda_of_app cache env sigma f args = match kind f with | Const (_kn,_u as c) -> let kn,u = get_alias env c in let cb = lookup_constant kn env in - (try - let prefix = get_const_prefix env kn in - (* We delay the compilation of arguments to avoid an exponential behavior *) - let f = Retroknowledge.get_native_compiling_info - (env).retroknowledge (GlobRef.ConstRef kn) prefix in - let args = lambda_of_args cache env sigma 0 args in - f args - with Not_found -> begin match cb.const_body with + | Primitive op -> lambda_of_prim env c op (lambda_of_args cache env sigma 0 args) | Def csubst -> (* TODO optimize if f is a proj and argument is known *) if cb.const_inline_code then lambda_of_app cache env sigma (Mod_subst.force_constr csubst) args else let prefix = get_const_prefix env kn in let t = - if is_lazy env prefix (Mod_subst.force_constr csubst) then + if is_lazy (Mod_subst.force_constr csubst) then mkLapp Lforce [|Lconst (prefix, (kn,u))|] else Lconst (prefix, (kn,u)) in @@ -555,34 +568,18 @@ and lambda_of_app cache env sigma f args = | OpaqueDef _ | Undef _ -> let prefix = get_const_prefix env kn in mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args) - end) + end | Construct (c,u) -> let tag, nparams, arity = Cache.get_construct_info cache env c in let expected = nparams + arity in let nargs = Array.length args in let prefix = get_mind_prefix env (fst (fst c)) in - let gr = GlobRef.ConstructRef c in if Int.equal nargs expected then - try - try - Retroknowledge.get_native_constant_static_info - (env).retroknowledge - gr args - with NotClosed -> - assert (Int.equal nparams 0); (* should be fine for int31 *) - let args = lambda_of_args cache env sigma nparams args in - Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge gr prefix c args - with Not_found -> let args = lambda_of_args cache env sigma nparams args in makeblock env c u tag args else let args = lambda_of_args cache env sigma 0 args in - (try - Retroknowledge.get_native_constant_dynamic_info - (env).retroknowledge gr prefix c args - with Not_found -> - mkLapp (Lconstruct (prefix, (c,u))) args) + mkLapp (Lconstruct (prefix, (c,u))) args | _ -> let f = lambda_of_constr cache env sigma f in let args = lambda_of_args cache env sigma 0 args in @@ -615,45 +612,3 @@ let lambda_of_constr env sigma c = let mk_lazy c = mkLapp Llazy [|c|] - -(** Retroknowledge, to be removed once we move to primitive machine integers *) -let compile_static_int31 fc args = - if not fc then raise Not_found else - Luint (UintVal - (Uint31.of_int (Array.fold_left - (fun temp_i -> fun t -> match kind t with - | Construct ((_,d),_) -> 2*temp_i+d-1 - | _ -> raise NotClosed) - 0 args))) - -let compile_dynamic_int31 fc prefix c args = - if not fc then raise Not_found else - Luint (UintDigits (prefix,c,args)) - -(* We are relying here on the order of digits constructors *) -let digits_from_uint digits_ind prefix i = - let d0 = Lconstruct (prefix, ((digits_ind, 1), Univ.Instance.empty)) in - let d1 = Lconstruct (prefix, ((digits_ind, 2), Univ.Instance.empty)) in - let digits = Array.make 31 d0 in - for k = 0 to 30 do - if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then - digits.(30-k) <- d1 - done; - digits - -let before_match_int31 digits_ind fc prefix c t = - if not fc then - raise Not_found - else - match t with - | Luint (UintVal i) -> - let digits = digits_from_uint digits_ind prefix i in - mkLapp (Lconstruct (prefix,(c, Univ.Instance.empty))) digits - | Luint (UintDigits (prefix,c,args)) -> - mkLapp (Lconstruct (prefix,(c, Univ.Instance.empty))) args - | _ -> Luint (UintDecomp (prefix,c,t)) - -let compile_prim prim kn fc prefix args = - if not fc then raise Not_found - else - Lprim(prefix, kn, prim, args) diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 7b20258929..eb06522a33 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -10,9 +10,45 @@ open Names open Constr open Environ -open Nativeinstr +open Nativevalues (** This file defines the lambda code generation phase of the native compiler *) +type prefix = string + +type lambda = + | Lrel of Name.t * int + | Lvar of Id.t + | Lmeta of metavariable * lambda (* type *) + | Levar of Evar.t * lambda array (* arguments *) + | Lprod of lambda * lambda + | Llam of Name.t array * lambda + | Lrec of Name.t * lambda + | Llet of Name.t * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of prefix * pconstant + | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) + | Lprim of prefix * pconstant * CPrimitives.t * lambda array + | Lcase of annot_sw * lambda * lambda * lam_branches + (* annotations, term being matched, accu, branches *) + | Lif of lambda * lambda * lambda + | Lfix of (int array * (string * inductive) array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of prefix * pconstructor * int * lambda array + (* prefix, constructor Name.t, constructor tag, arguments *) + (* A fully applied constructor *) + | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *) + (* A partially applied constructor *) + | Luint of Uint63.t + | Lval of Nativevalues.t + | Lsort of Sorts.t + | Lind of prefix * pinductive + | Llazy + | Lforce + +and lam_branches = (constructor * Name.t array * lambda) array + +and fix_decl = Name.t array * lambda array * lambda array + type evars = { evars_val : existential -> constr option; evars_metas : metavariable -> types } @@ -22,7 +58,7 @@ val empty_evars : evars val decompose_Llam : lambda -> Name.t array * lambda val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda -val is_lazy : env -> prefix -> constr -> bool +val is_lazy : constr -> bool val mk_lazy : lambda -> lambda val get_mind_prefix : env -> MutInd.t -> string @@ -30,14 +66,3 @@ val get_mind_prefix : env -> MutInd.t -> string val get_alias : env -> pconstant -> pconstant val lambda_of_constr : env -> evars -> Constr.constr -> lambda - -val compile_static_int31 : bool -> Constr.constr array -> lambda - -val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array -> - lambda - -val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda -> - lambda - -val compile_prim : CPrimitives.t -> Constant.t -> bool -> prefix -> lambda array -> - lambda diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 93e74af845..a6b48cd7e3 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -196,11 +196,17 @@ let dummy_value : unit -> t = fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed.") let cast_accu v = (Obj.magic v:accumulator) +[@@ocaml.inline always] let mk_int (x : int) = (Obj.magic x : t) +[@@ocaml.inline always] + (* Coq's booleans are reversed... *) let mk_bool (b : bool) = (Obj.magic (not b) : t) -let mk_uint (x : Uint31.t) = (Obj.magic x : t) +[@@ocaml.inline always] + +let mk_uint (x : Uint63.t) = (Obj.magic x : t) +[@@ocaml.inline always] type block @@ -216,8 +222,9 @@ type kind_of_value = | Vaccu of accumulator | Vfun of (t -> t) | Vconst of int + | Vint64 of int64 | Vblock of block - + let kind_of_value (v:t) = let o = Obj.repr v in if Obj.is_int o then Vconst (Obj.magic v) @@ -225,8 +232,8 @@ let kind_of_value (v:t) = let tag = Obj.tag o in if Int.equal tag accumulate_tag then Vaccu (Obj.magic v) - else - if (tag < Obj.lazy_tag) then Vblock (Obj.magic v) + else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) + else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v) else (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); or ??? what is 1002*) @@ -236,92 +243,105 @@ let kind_of_value (v:t) = let is_int (x:t) = let o = Obj.repr x in - Obj.is_int o + Obj.is_int o || Int.equal (Obj.tag o) Obj.custom_tag let val_to_int (x:t) = (Obj.magic x : int) +[@@ocaml.inline always] -let to_uint (x:t) = (Obj.magic x : Uint31.t) -let of_uint (x: Uint31.t) = (Obj.magic x : t) +let to_uint (x:t) = (Obj.magic x : Uint63.t) +[@@ocaml.inline always] let no_check_head0 x = - of_uint (Uint31.head0 (to_uint x)) + mk_uint (Uint63.head0 (to_uint x)) +[@@ocaml.inline always] let head0 accu x = if is_int x then no_check_head0 x else accu x let no_check_tail0 x = - of_uint (Uint31.tail0 (to_uint x)) + mk_uint (Uint63.tail0 (to_uint x)) +[@@ocaml.inline always] let tail0 accu x = if is_int x then no_check_tail0 x else accu x let no_check_add x y = - of_uint (Uint31.add (to_uint x) (to_uint y)) + mk_uint (Uint63.add (to_uint x) (to_uint y)) +[@@ocaml.inline always] let add accu x y = if is_int x && is_int y then no_check_add x y else accu x y let no_check_sub x y = - of_uint (Uint31.sub (to_uint x) (to_uint y)) + mk_uint (Uint63.sub (to_uint x) (to_uint y)) +[@@ocaml.inline always] let sub accu x y = if is_int x && is_int y then no_check_sub x y else accu x y let no_check_mul x y = - of_uint (Uint31.mul (to_uint x) (to_uint y)) + mk_uint (Uint63.mul (to_uint x) (to_uint y)) +[@@ocaml.inline always] let mul accu x y = if is_int x && is_int y then no_check_mul x y else accu x y let no_check_div x y = - of_uint (Uint31.div (to_uint x) (to_uint y)) + mk_uint (Uint63.div (to_uint x) (to_uint y)) +[@@ocaml.inline always] let div accu x y = if is_int x && is_int y then no_check_div x y else accu x y let no_check_rem x y = - of_uint (Uint31.rem (to_uint x) (to_uint y)) + mk_uint (Uint63.rem (to_uint x) (to_uint y)) +[@@ocaml.inline always] 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_l_sr x y = - of_uint (Uint31.l_sr (to_uint x) (to_uint y)) + mk_uint (Uint63.l_sr (to_uint x) (to_uint y)) +[@@ocaml.inline always] let l_sr accu x y = if is_int x && is_int y then no_check_l_sr x y else accu x y let no_check_l_sl x y = - of_uint (Uint31.l_sl (to_uint x) (to_uint y)) + mk_uint (Uint63.l_sl (to_uint x) (to_uint y)) +[@@ocaml.inline always] 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_l_and x y = - of_uint (Uint31.l_and (to_uint x) (to_uint y)) + mk_uint (Uint63.l_and (to_uint x) (to_uint y)) +[@@ocaml.inline always] let l_and accu x y = if is_int x && is_int y then no_check_l_and x y else accu x y let no_check_l_xor x y = - of_uint (Uint31.l_xor (to_uint x) (to_uint y)) + mk_uint (Uint63.l_xor (to_uint x) (to_uint y)) +[@@ocaml.inline always] let l_xor accu x y = if is_int x && is_int y then no_check_l_xor x y else accu x y let no_check_l_or x y = - of_uint (Uint31.l_or (to_uint x) (to_uint y)) + mk_uint (Uint63.l_or (to_uint x) (to_uint y)) +[@@ocaml.inline always] let l_or accu x y = if is_int x && is_int y then no_check_l_or x y @@ -337,61 +357,57 @@ type coq_pair = | Paccu of t | PPair of t * t -type coq_zn2z = - | Zaccu of t - | ZW0 - | ZWW of t * t - let mkCarry b i = - if b then (Obj.magic (C1(of_uint i)):t) - else (Obj.magic (C0(of_uint i)):t) + if b then (Obj.magic (C1(mk_uint i)):t) + else (Obj.magic (C0(mk_uint i)):t) let no_check_addc x y = - let s = Uint31.add (to_uint x) (to_uint y) in - mkCarry (Uint31.lt s (to_uint x)) s + let s = Uint63.add (to_uint x) (to_uint y) in + mkCarry (Uint63.lt s (to_uint x)) s +[@@ocaml.inline always] let addc accu x y = if is_int x && is_int y then no_check_addc x y else accu x y let no_check_subc x y = - let s = Uint31.sub (to_uint x) (to_uint y) in - mkCarry (Uint31.lt (to_uint x) (to_uint y)) s + let s = Uint63.sub (to_uint x) (to_uint y) in + mkCarry (Uint63.lt (to_uint x) (to_uint y)) s +[@@ocaml.inline always] let subc accu x y = if is_int x && is_int y then no_check_subc x y else accu x y -let no_check_addcarryc x y = +let no_check_addCarryC x y = let s = - Uint31.add (Uint31.add (to_uint x) (to_uint y)) - (Uint31.of_int 1) in - mkCarry (Uint31.le s (to_uint x)) s + Uint63.add (Uint63.add (to_uint x) (to_uint y)) + (Uint63.of_int 1) in + mkCarry (Uint63.le s (to_uint x)) s +[@@ocaml.inline always] -let addcarryc accu x y = - if is_int x && is_int y then no_check_addcarryc x y +let addCarryC accu x y = + if is_int x && is_int y then no_check_addCarryC x y else accu x y -let no_check_subcarryc x y = +let no_check_subCarryC x y = let s = - Uint31.sub (Uint31.sub (to_uint x) (to_uint y)) - (Uint31.of_int 1) in - mkCarry (Uint31.le (to_uint x) (to_uint y)) s + Uint63.sub (Uint63.sub (to_uint x) (to_uint y)) + (Uint63.of_int 1) in + mkCarry (Uint63.le (to_uint x) (to_uint y)) s +[@@ocaml.inline always] -let subcarryc accu x y = - if is_int x && is_int y then no_check_subcarryc x y +let subCarryC accu x y = + if is_int x && is_int y then no_check_subCarryC x y else accu x y let of_pair (x, y) = - (Obj.magic (PPair(of_uint x, of_uint y)):t) - -let zn2z_of_pair (x,y) = - if Uint31.equal x (Uint31.of_uint 0) && - Uint31.equal y (Uint31.of_uint 0) then Obj.magic ZW0 - else (Obj.magic (ZWW(of_uint x, of_uint y)) : t) + (Obj.magic (PPair(mk_uint x, mk_uint y)):t) +[@@ocaml.inline always] let no_check_mulc x y = - zn2z_of_pair(Uint31.mulc (to_uint x) (to_uint y)) + of_pair (Uint63.mulc (to_uint x) (to_uint y)) +[@@ocaml.inline always] let mulc accu x y = if is_int x && is_int y then no_check_mulc x y @@ -399,7 +415,8 @@ let mulc accu x y = let no_check_diveucl x y = let i1, i2 = to_uint x, to_uint y in - of_pair(Uint31.div i1 i2, Uint31.rem i1 i2) + of_pair(Uint63.div i1 i2, Uint63.rem i1 i2) +[@@ocaml.inline always] let diveucl accu x y = if is_int x && is_int y then no_check_diveucl x y @@ -407,21 +424,20 @@ let diveucl accu x y = let no_check_div21 x y z = let i1, i2, i3 = to_uint x, to_uint y, to_uint z in - of_pair (Uint31.div21 i1 i2 i3) + of_pair (Uint63.div21 i1 i2 i3) +[@@ocaml.inline always] let div21 accu x y z = if is_int x && is_int y && is_int z then no_check_div21 x y z else accu x y z -let no_check_addmuldiv x y z = +let no_check_addMulDiv x y z = let p, i, j = to_uint x, to_uint y, to_uint z in - let p' = Uint31.to_int p in - of_uint (Uint31.l_or - (Uint31.l_sl i p) - (Uint31.l_sr j (Uint31.of_int (31 - p')))) + mk_uint (Uint63.addmuldiv p i j) +[@@ocaml.inline always] -let addmuldiv accu x y z = - if is_int x && is_int y && is_int z then no_check_addmuldiv x y z +let addMulDiv accu x y z = + if is_int x && is_int y && is_int z then no_check_addMulDiv x y z else accu x y z [@@@ocaml.warning "-34"] @@ -436,29 +452,32 @@ type coq_cmp = | CmpLt | CmpGt -let no_check_eq x y = - mk_bool (Uint31.equal (to_uint x) (to_uint y)) +let no_check_eq x y = + mk_bool (Uint63.equal (to_uint x) (to_uint y)) +[@@ocaml.inline always] let eq accu x y = if is_int x && is_int y then no_check_eq x y else accu x y let no_check_lt x y = - mk_bool (Uint31.lt (to_uint x) (to_uint y)) + mk_bool (Uint63.lt (to_uint x) (to_uint y)) +[@@ocaml.inline always] let lt accu x y = if is_int x && is_int y then no_check_lt x y else accu x y let no_check_le x y = - mk_bool (Uint31.le (to_uint x) (to_uint y)) + mk_bool (Uint63.le (to_uint x) (to_uint y)) +[@@ocaml.inline always] 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_compare x y = - match Uint31.compare (to_uint x) (to_uint y) with + match Uint63.compare (to_uint x) (to_uint y) with | x when x < 0 -> (Obj.magic CmpLt:t) | 0 -> (Obj.magic CmpEq:t) | _ -> (Obj.magic CmpGt:t) @@ -467,6 +486,11 @@ let compare accu x y = if is_int x && is_int y then no_check_compare x y else accu x y +let print x = + Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x)); + flush stderr; + x + let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i) let bohcnv = Array.init 256 (fun i -> i - (if 0x30 <= i then 0x30 else 0) - @@ -491,63 +515,3 @@ let str_decode s = Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0 - -(** Retroknowledge, to be removed when we switch to primitive integers *) - -(* This will be unsafe with 63-bits integers *) -let digit_to_uint d = (Obj.magic d : Uint31.t) - -let mk_I31_accu c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 - x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 = - if is_int x0 && is_int x1 && is_int x2 && is_int x3 && is_int x4 && is_int x5 - && is_int x6 && is_int x7 && is_int x8 && is_int x9 && is_int x10 - && is_int x11 && is_int x12 && is_int x13 && is_int x14 && is_int x15 - && is_int x16 && is_int x17 && is_int x18 && is_int x19 && is_int x20 - && is_int x21 && is_int x22 && is_int x23 && is_int x24 && is_int x25 - && is_int x26 && is_int x27 && is_int x28 && is_int x29 && is_int x30 - then - let r = digit_to_uint x0 in - let r = Uint31.add_digit r (digit_to_uint x1) in - let r = Uint31.add_digit r (digit_to_uint x2) in - let r = Uint31.add_digit r (digit_to_uint x3) in - let r = Uint31.add_digit r (digit_to_uint x4) in - let r = Uint31.add_digit r (digit_to_uint x5) in - let r = Uint31.add_digit r (digit_to_uint x6) in - let r = Uint31.add_digit r (digit_to_uint x7) in - let r = Uint31.add_digit r (digit_to_uint x8) in - let r = Uint31.add_digit r (digit_to_uint x9) in - let r = Uint31.add_digit r (digit_to_uint x10) in - let r = Uint31.add_digit r (digit_to_uint x11) in - let r = Uint31.add_digit r (digit_to_uint x12) in - let r = Uint31.add_digit r (digit_to_uint x13) in - let r = Uint31.add_digit r (digit_to_uint x14) in - let r = Uint31.add_digit r (digit_to_uint x15) in - let r = Uint31.add_digit r (digit_to_uint x16) in - let r = Uint31.add_digit r (digit_to_uint x17) in - let r = Uint31.add_digit r (digit_to_uint x18) in - let r = Uint31.add_digit r (digit_to_uint x19) in - let r = Uint31.add_digit r (digit_to_uint x20) in - let r = Uint31.add_digit r (digit_to_uint x21) in - let r = Uint31.add_digit r (digit_to_uint x22) in - let r = Uint31.add_digit r (digit_to_uint x23) in - let r = Uint31.add_digit r (digit_to_uint x24) in - let r = Uint31.add_digit r (digit_to_uint x25) in - let r = Uint31.add_digit r (digit_to_uint x26) in - let r = Uint31.add_digit r (digit_to_uint x27) in - let r = Uint31.add_digit r (digit_to_uint x28) in - let r = Uint31.add_digit r (digit_to_uint x29) in - let r = Uint31.add_digit r (digit_to_uint x30) in - mk_uint r - else - c x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 - x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 - -let decomp_uint c v = - if is_int v then - let r = ref c in - let v = val_to_int v in - for i = 30 downto 0 do - r := (!r) (mk_int ((v lsr i) land 1)); - done; - !r - else v diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 10689941e8..58cb6e2c30 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -78,8 +78,13 @@ val mk_const : tag -> t val mk_block : tag -> t array -> t val mk_bool : bool -> t +[@@ocaml.inline always] + val mk_int : int -> t -val mk_uint : Uint31.t -> t +[@@ocaml.inline always] + +val mk_uint : Uint63.t -> t +[@@ocaml.inline always] val napply : t -> t array -> t (* Functions over accumulators *) @@ -90,6 +95,8 @@ val args_of_accu : accumulator -> t array val accu_nargs : accumulator -> int val cast_accu : t -> accumulator +[@@ocaml.inline always] + (* Functions over block: i.e constructors *) type block @@ -106,6 +113,7 @@ type kind_of_value = | Vaccu of accumulator | Vfun of (t -> t) | Vconst of int + | Vint64 of int64 | Vblock of block val kind_of_value : t -> kind_of_value @@ -136,51 +144,90 @@ val l_or : t -> t -> t -> t val addc : t -> t -> t -> t val subc : t -> t -> t -> t -val addcarryc : t -> t -> t -> t -val subcarryc : t -> t -> t -> t +val addCarryC : t -> t -> t -> t +val subCarryC : t -> t -> t -> t val mulc : t -> t -> t -> t val diveucl : t -> t -> t -> t val div21 : t -> t -> t -> t -> t -val addmuldiv : t -> t -> t -> t -> t +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 compare : t -> t -> t -> t +val print : t -> t + (* Function without check *) val no_check_head0 : t -> t +[@@ocaml.inline always] + val no_check_tail0 : t -> t +[@@ocaml.inline always] val no_check_add : t -> t -> t +[@@ocaml.inline always] + val no_check_sub : t -> t -> t +[@@ocaml.inline always] + val no_check_mul : t -> t -> t +[@@ocaml.inline always] + val no_check_div : t -> t -> t +[@@ocaml.inline always] + val no_check_rem : 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_l_and : t -> t -> t +[@@ocaml.inline always] + val no_check_l_xor : t -> t -> t +[@@ocaml.inline always] + val no_check_l_or : t -> t -> t +[@@ocaml.inline always] val no_check_addc : t -> t -> t +[@@ocaml.inline always] + val no_check_subc : t -> t -> t -val no_check_addcarryc : t -> t -> t -val no_check_subcarryc : t -> t -> t +[@@ocaml.inline always] + +val no_check_addCarryC : t -> t -> t +[@@ocaml.inline always] + +val no_check_subCarryC : t -> t -> t +[@@ocaml.inline always] val no_check_mulc : t -> t -> t +[@@ocaml.inline always] + val no_check_diveucl : t -> t -> t +[@@ocaml.inline always] val no_check_div21 : t -> t -> t -> t -val no_check_addmuldiv : t -> t -> t -> t +[@@ocaml.inline always] + +val no_check_addMulDiv : t -> t -> t -> t +[@@ocaml.inline always] val no_check_eq : t -> t -> t +[@@ocaml.inline always] + val no_check_lt : t -> t -> t +[@@ocaml.inline always] + val no_check_le : t -> t -> t -val no_check_compare : t -> t -> t +[@@ocaml.inline always] -val mk_I31_accu : t -val decomp_uint : t -> t -> t +val no_check_compare : t -> t -> t diff --git a/kernel/primred.ml b/kernel/primred.ml new file mode 100644 index 0000000000..d95d7de7aa --- /dev/null +++ b/kernel/primred.ml @@ -0,0 +1,208 @@ +(* Reduction of native operators *) +open Names +open CPrimitives +open Retroknowledge +open Environ +open CErrors + +let add_retroknowledge env action = + match action with + | Register_type(PT_int63,c) -> + let retro = env.retroknowledge in + let retro = + match retro.retro_int63 with + | None -> { retro with retro_int63 = Some c } + | Some c' -> assert (Constant.equal c c'); retro in + set_retroknowledge env retro + | Register_ind(pit,ind) -> + let retro = env.retroknowledge in + let retro = + match pit with + | PIT_bool -> + let r = + match retro.retro_bool with + | None -> ((ind,1), (ind,2)) + | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + { retro with retro_bool = Some r } + | PIT_carry -> + let r = + match retro.retro_carry with + | None -> ((ind,1), (ind,2)) + | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + { retro with retro_carry = Some r } + | PIT_pair -> + let r = + match retro.retro_pair with + | None -> (ind,1) + | Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in + { retro with retro_pair = Some r } + | PIT_cmp -> + let r = + match retro.retro_cmp with + | None -> ((ind,1), (ind,2), (ind,3)) + | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in + { retro with retro_cmp = Some r } + in + set_retroknowledge env retro + | Register_inline(c) -> + let (cb,r) = lookup_constant_key c env in + let cb = {cb with Declarations.const_inline_code = true} in + add_constant_key c cb !(fst r) env + +let get_int_type env = + match env.retroknowledge.retro_int63 with + | Some c -> c + | None -> anomaly Pp.(str"Reduction of primitive: int63 not registered") + +let get_bool_constructors env = + match env.retroknowledge.retro_bool with + | Some r -> r + | None -> anomaly Pp.(str"Reduction of primitive: bool not registered") + +let get_carry_constructors env = + match env.retroknowledge.retro_carry with + | Some r -> r + | None -> anomaly Pp.(str"Reduction of primitive: carry not registered") + +let get_pair_constructor env = + match env.retroknowledge.retro_pair with + | Some c -> c + | None -> anomaly Pp.(str"Reduction of primitive: pair not registered") + +let get_cmp_constructors env = + match env.retroknowledge.retro_cmp with + | Some r -> r + | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered") + +exception NativeDestKO + +module type RedNativeEntries = + sig + type elem + type args + type evd (* will be unit in kernel, evar_map outside *) + + val get : args -> int -> elem + val get_int : evd -> elem -> Uint63.t + val mkInt : env -> Uint63.t -> elem + val mkBool : env -> bool -> elem + val mkCarry : env -> bool -> elem -> elem (* true if carry *) + val mkIntPair : env -> elem -> elem -> elem + val mkLt : env -> elem + val mkEq : env -> elem + val mkGt : env -> elem + + end + +module type RedNative = + sig + type elem + type args + type evd + val red_prim : env -> evd -> CPrimitives.t -> args -> elem option + end + +module RedNative (E:RedNativeEntries) : + RedNative with type elem = E.elem + with type args = E.args + with type evd = E.evd = +struct + type elem = E.elem + type args = E.args + type evd = E.evd + + let get_int evd args i = E.get_int evd (E.get args i) + + let get_int1 evd args = get_int evd args 0 + + let get_int2 evd args = get_int evd args 0, get_int evd args 1 + + let get_int3 evd args = + get_int evd args 0, get_int evd args 1, get_int evd args 2 + + let red_prim_aux env evd op args = + let open CPrimitives in + match op with + | Int63head0 -> + let i = get_int1 evd args in E.mkInt env (Uint63.head0 i) + | Int63tail0 -> + let i = get_int1 evd args in E.mkInt env (Uint63.tail0 i) + | Int63add -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.add i1 i2) + | Int63sub -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.sub i1 i2) + | Int63mul -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.mul i1 i2) + | Int63div -> + 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) + | 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) + | Int63land -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2) + | Int63lor -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_or i1 i2) + | Int63lxor -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_xor i1 i2) + | Int63addc -> + let i1, i2 = get_int2 evd args in + let s = Uint63.add i1 i2 in + E.mkCarry env (Uint63.lt s i1) (E.mkInt env s) + | Int63subc -> + let i1, i2 = get_int2 evd args in + let s = Uint63.sub i1 i2 in + E.mkCarry env (Uint63.lt i1 i2) (E.mkInt env s) + | Int63addCarryC -> + let i1, i2 = get_int2 evd args in + let s = Uint63.add (Uint63.add i1 i2) (Uint63.of_int 1) in + E.mkCarry env (Uint63.le s i1) (E.mkInt env s) + | Int63subCarryC -> + let i1, i2 = get_int2 evd args in + let s = Uint63.sub (Uint63.sub i1 i2) (Uint63.of_int 1) in + E.mkCarry env (Uint63.le i1 i2) (E.mkInt env s) + | Int63mulc -> + let i1, i2 = get_int2 evd args in + let (h, l) = Uint63.mulc i1 i2 in + E.mkIntPair env (E.mkInt env h) (E.mkInt env l) + | Int63diveucl -> + let i1, i2 = get_int2 evd args in + let q,r = Uint63.div i1 i2, Uint63.rem i1 i2 in + E.mkIntPair env (E.mkInt env q) (E.mkInt env r) + | Int63div21 -> + let i1, i2, i3 = get_int3 evd args in + let q,r = Uint63.div21 i1 i2 i3 in + E.mkIntPair env (E.mkInt env q) (E.mkInt env r) + | Int63addMulDiv -> + let p, i, j = get_int3 evd args in + E.mkInt env + (Uint63.l_or + (Uint63.l_sl i p) + (Uint63.l_sr j (Uint63.sub (Uint63.of_int Uint63.uint_size) p))) + | Int63eq -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.equal i1 i2) + | Int63lt -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.lt i1 i2) + | Int63le -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.le i1 i2) + | Int63compare -> + let i1, i2 = get_int2 evd args in + begin match Uint63.compare i1 i2 with + | x when x < 0 -> E.mkLt env + | 0 -> E.mkEq env + | _ -> E.mkGt env + end + + let red_prim env evd p args = + try + let r = + red_prim_aux env evd p args + in Some r + with NativeDestKO -> None + +end diff --git a/kernel/primred.mli b/kernel/primred.mli new file mode 100644 index 0000000000..f5998982d7 --- /dev/null +++ b/kernel/primred.mli @@ -0,0 +1,44 @@ +open Names +open Environ + +(** {5 Reduction of primitives} *) +val add_retroknowledge : env -> Retroknowledge.action -> env + +val get_int_type : env -> Constant.t +val get_bool_constructors : env -> constructor * constructor +val get_carry_constructors : env -> constructor * constructor +val get_pair_constructor : env -> constructor +val get_cmp_constructors : env -> constructor * constructor * constructor + +exception NativeDestKO (* Should be raised by get_* functions on failure *) + +module type RedNativeEntries = + sig + type elem + type args + type evd (* will be unit in kernel, evar_map outside *) + + val get : args -> int -> elem + val get_int : evd -> elem -> Uint63.t + val mkInt : env -> Uint63.t -> elem + val mkBool : env -> bool -> elem + val mkCarry : env -> bool -> elem -> elem (* true if carry *) + val mkIntPair : env -> elem -> elem -> elem + val mkLt : env -> elem + val mkEq : env -> elem + val mkGt : env -> elem + end + +module type RedNative = + sig + type elem + type args + type evd + val red_prim : env -> evd -> CPrimitives.t -> args -> elem option + end + +module RedNative : + functor (E:RedNativeEntries) -> + RedNative with type elem = E.elem + with type args = E.args + with type evd = E.evd diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 97cd4c00d7..61051c001d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -21,6 +21,7 @@ open CErrors open Util open Names open Constr +open Declarations open Vars open Environ open CClosure @@ -59,16 +60,23 @@ let compare_stack_shape stk1 stk2 = Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 + | Zprimitive(op1,_,rargs1, _kargs1)::s1, Zprimitive(op2,_,rargs2, _kargs2)::s2 -> + bal=0 && op1=op2 && List.length rargs1=List.length rargs2 && + compare_rec 0 s1 s2 | [], _ :: _ - | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false + | (Zproj _ | ZcaseT _ | Zfix _ | Zprimitive _) :: _, _ -> false in compare_rec 0 stk1 stk2 +type lft_fconstr = lift * fconstr + type lft_constr_stack_elt = Zlapp of (lift * fconstr) array | Zlproj of Projection.Repr.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * constr * constr array * fconstr subs + | Zlprimitive of + CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args and lft_constr_stack = lft_constr_stack_elt list let rec zlapp v = function @@ -102,7 +110,10 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,p,br,e)::pstk)) + (l,Zlcase(ci,l,p,br,e)::pstk) + | (Zprimitive(op,c,rargs,kargs),(l,pstk)) -> + (l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs, + List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk)) in snd (pure_rec lfts stk) @@ -127,10 +138,10 @@ let nf_betaiota env t = let whd_betaiotazeta env x = match kind x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _) -> x + Prod _|Lambda _|Fix _|CoFix _|Int _) -> x | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ -> x | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x) @@ -141,10 +152,10 @@ let whd_betaiotazeta env x = let whd_all env t = match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _) -> t + Prod _|Lambda _|Fix _|CoFix _|Int _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | Int _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ |Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos all env) (create_tab ()) (inject t) @@ -155,10 +166,10 @@ let whd_all env t = let whd_allnolet env t = match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t + Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t) @@ -296,6 +307,15 @@ let rec skip_pattern n c = | Lambda (_, _, c) -> skip_pattern (pred n) c | _ -> raise IrregularPatternShape +let unfold_ref_with_args infos tab fl v = + match unfold_reference infos tab fl with + | Def def -> Some (def, v) + | Primitive op when check_native_args op v -> + let c = match fl with ConstKey c -> c | _ -> assert false in + let rargs, a, nargs, v = get_native_args1 op c v in + Some (whd_stack infos tab a (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v))) + | Undef _ | OpaqueDef _ | Primitive _ -> None + type conv_tab = { cnv_inf : clos_infos; lft_tab : clos_tab; @@ -355,28 +375,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try - let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> - (* else the oracle tells which constant is to be expanded *) + (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos.cnv_inf in let (app1,app2) = + let aux appr1 lft1 fl1 tab1 v1 appr2 lft2 fl2 tab2 v2 = + match unfold_ref_with_args infos.cnv_inf tab1 fl1 v1 with + | Some t1 -> ((lft1, t1), appr2) + | None -> match unfold_ref_with_args infos.cnv_inf tab2 fl2 v2 with + | Some t2 -> (appr1, (lft2, t2)) + | None -> raise NotConvertible + in if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then - match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> ((lft1, (def1, v1)), appr2) - | None -> - (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> (appr1, (lft2, (def2, v2))) - | None -> raise NotConvertible) + aux appr1 lft1 fl1 infos.lft_tab v1 appr2 lft2 fl2 infos.rgt_tab v2 else - match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> (appr1, (lft2, (def2, v2))) - | None -> - (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> ((lft1, (def1, v1)), appr2) - | None -> raise NotConvertible) - in - eqappr cv_pb l2r infos app1 app2 cuniv) + let (app2,app1) = aux appr2 lft2 fl2 infos.rgt_tab v2 appr1 lft1 fl1 infos.lft_tab v1 in + (app1,app2) + in + eqappr cv_pb l2r infos app1 app2 cuniv) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, @@ -400,31 +418,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = raise NotConvertible) | (FProj (p1,c1), t2) -> - (match unfold_projection infos.cnv_inf p1 with - | Some s1 -> + begin match unfold_projection infos.cnv_inf p1 with + | Some s1 -> eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv - | None -> - (match t2 with - | FFlex fl2 -> - (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv - | None -> raise NotConvertible) - | _ -> raise NotConvertible)) - + | None -> + begin match t2 with + | FFlex fl2 -> + begin match unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 with + | Some t2 -> + eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv + | None -> raise NotConvertible + end + | _ -> raise NotConvertible + end + end + | (t1, FProj (p2,c2)) -> - (match unfold_projection infos.cnv_inf p2 with - | Some s2 -> + begin match unfold_projection infos.cnv_inf p2 with + | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv - | None -> - (match t1 with - | FFlex fl1 -> - (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> - eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv - | None -> raise NotConvertible) - | _ -> raise NotConvertible)) - + | None -> + begin match t1 with + | FFlex fl1 -> + begin match unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 with + | Some t1 -> + eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv + | None -> raise NotConvertible + end + | _ -> raise NotConvertible + end + end + (* other constructors *) | (FLambda _, FLambda _) -> (* Inconsistency: we tolerate that v1, v2 contain shift and update but @@ -469,8 +493,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> - (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> + begin match unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 with + | Some (def1,v1) -> (** By virtue of the previous case analyses, we know [c2] is rigid. Conversion check to rigid terms eventually implies full weak-head reduction, so instead of repeatedly performing small-step @@ -478,32 +502,34 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv - | None -> - match c2 with + | None -> + (match c2 with | FConstruct ((ind2,_j2),_u2) -> - (try - let v2, v1 = - eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with Not_found -> raise NotConvertible) - | _ -> raise NotConvertible) - + (try + let v2, v1 = + eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) + end + | (c1, FFlex fl2) -> - (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> + begin match unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 with + | Some (def2, v2) -> (** Symmetrical case of above. *) let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv - | None -> - match c1 with - | FConstruct ((ind1,_j1),_u1) -> - (try let v1, v2 = - eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with Not_found -> raise NotConvertible) - | _ -> raise NotConvertible) - + | None -> + match c1 with + | FConstruct ((ind1,_j1),_u1) -> + (try let v1, v2 = + eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible + end + (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then @@ -584,13 +610,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible + | FInt i1, FInt i2 -> + if Uint63.equal i1 i2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + else raise NotConvertible + (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ - | FProd _ | FEvar _), _ -> raise NotConvertible + | FProd _ | FEvar _ | FInt _), _ -> raise NotConvertible and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in @@ -613,7 +643,12 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = raise NotConvertible; let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 - | _ -> assert false) + | (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) -> + if not (CPrimitives.equal op1 op2) then raise NotConvertible else + let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in + let fk (_,a1) (_,a2) cu = f a1 a2 cu in + List.fold_right2 fk kargs1 kargs2 cu2 + | ((Zlapp _ | Zlproj _ | Zlfix _| Zlcase _| Zlprimitive _), _) -> assert false) | _ -> cuniv in if compare_stack_shape stk1 stk2 then cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index e51c25c06b..18fafdb6d3 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -12,249 +12,30 @@ (* Addition of native Head (nb of heading 0) and Tail (nb of trailing 0) by Benjamin Grégoire, Jun 2007 *) -(* This file defines the knowledge that the kernel is able to optimize - for evaluation in the bytecode virtual machine *) +(* This file defines the knowledge that the kernel is able to optimize. *) open Names -open Constr - -(* The retroknowledge defines a bijective correspondance between some - [entry]-s (which are, in fact, merely names) and [field]-s which - are roles assigned to these entries. *) - -type int31_field = - | Int31Bits - | Int31Type - | Int31Constructor - | Int31Twice - | Int31TwicePlusOne - | Int31Phi - | Int31PhiInv - | Int31Plus - | Int31PlusC - | Int31PlusCarryC - | Int31Minus - | Int31MinusC - | Int31MinusCarryC - | Int31Times - | Int31TimesC - | Int31Div21 - | Int31Div - | Int31Diveucl - | Int31AddMulDiv - | Int31Compare - | Int31Head0 - | Int31Tail0 - | Int31Lor - | Int31Land - | Int31Lxor - -type field = - | KInt31 of int31_field - -let int31_field_of_string = - function - | "bits" -> Int31Bits - | "type" -> Int31Type - | "twice" -> Int31Twice - | "twice_plus_one" -> Int31TwicePlusOne - | "phi" -> Int31Phi - | "phi_inv" -> Int31PhiInv - | "plus" -> Int31Plus - | "plusc" -> Int31PlusC - | "pluscarryc" -> Int31PlusCarryC - | "minus" -> Int31Minus - | "minusc" -> Int31MinusC - | "minuscarryc" -> Int31MinusCarryC - | "times" -> Int31Times - | "timesc" -> Int31TimesC - | "div21" -> Int31Div21 - | "div" -> Int31Div - | "diveucl" -> Int31Diveucl - | "addmuldiv" -> Int31AddMulDiv - | "compare" -> Int31Compare - | "head0" -> Int31Head0 - | "tail0" -> Int31Tail0 - | "lor" -> Int31Lor - | "land" -> Int31Land - | "lxor" -> Int31Lxor - | s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s) - -let int31_path = DirPath.make [ Id.of_string "int31" ] - -(* record representing all the flags of the internal state of the kernel *) -type flags = {fastcomputation : bool} - - - - - -(* The [proactive] knowledge contains the mapping [field->entry]. *) - -module Proactive = - Map.Make (struct type t = field let compare = Pervasives.compare end) - -type proactive = GlobRef.t Proactive.t - -(* The [reactive] knowledge contains the mapping - [entry->field]. Fields are later to be interpreted as a - [reactive_info]. *) - -module Reactive = GlobRef.Map - -type reactive_info = {(*information required by the compiler of the VM *) - vm_compiling : - (*fastcomputation flag -> continuation -> result *) - (bool -> Cinstr.lambda array -> Cinstr.lambda) - option; - vm_constant_static : - (*fastcomputation flag -> constructor -> args -> result*) - (bool -> constr array -> Cinstr.lambda) - option; - vm_constant_dynamic : - (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *) - (bool -> Cinstr.lambda array -> Cinstr.lambda) - option; - (* fastcomputation flag -> cont -> result *) - vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option; - (* tag (= compiled int for instance) -> result *) - vm_decompile_const : (int -> constr) option; - - native_compiling : - (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> - Nativeinstr.lambda) option; - - native_constant_static : - (bool -> constr array -> Nativeinstr.lambda) option; - - native_constant_dynamic : - (bool -> Nativeinstr.prefix -> constructor -> - Nativeinstr.lambda array -> Nativeinstr.lambda) option; - - native_before_match : (bool -> Nativeinstr.prefix -> constructor -> - Nativeinstr.lambda -> Nativeinstr.lambda) option +type retroknowledge = { + retro_int63 : Constant.t option; + retro_bool : (constructor * constructor) option; (* true, false *) + retro_carry : (constructor * constructor) option; (* C0, C1 *) + retro_pair : constructor option; + retro_cmp : (constructor * constructor * constructor) option; + (* Eq, Lt, Gt *) + retro_refl : constructor option; } +let empty = { + retro_int63 = None; + retro_bool = None; + retro_carry = None; + retro_pair = None; + retro_cmp = None; + retro_refl = None; +} - -and reactive = field Reactive.t - -and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive} - -(* This type represent an atomic action of the retroknowledge. It - is stored in the compiled libraries *) -(* As per now, there is only the possibility of registering things - the possibility of unregistering or changing the flag is under study *) type action = - | RKRegister of field * GlobRef.t - - -(*initialisation*) -let initial_flags = - {fastcomputation = true;} - -let initial_proactive = - (Proactive.empty:proactive) - -let initial_reactive = - (Reactive.empty:reactive) - -let initial_retroknowledge = - {flags = initial_flags; - proactive = initial_proactive; - reactive = initial_reactive } - -let empty_reactive_info = - { vm_compiling = None ; - vm_constant_static = None; - vm_constant_dynamic = None; - vm_before_match = None; - vm_decompile_const = None; - native_compiling = None; - native_constant_static = None; - native_constant_dynamic = None; - native_before_match = None; - } - - - -(* adds a binding [entry<->field]. *) -let add_field knowledge field entry = - {knowledge with - proactive = Proactive.add field entry knowledge.proactive; - reactive = Reactive.add entry field knowledge.reactive} - -(* acces functions for proactive retroknowledge *) -let mem knowledge field = - Proactive.mem field knowledge.proactive - -let find knowledge field = - Proactive.find field knowledge.proactive - - -let (dispatch,dispatch_hook) = Hook.make () - -let dispatch_reactive entry retroknowledge = - Hook.get dispatch retroknowledge entry (Reactive.find entry retroknowledge.reactive) - -(*access functions for reactive retroknowledge*) - -(* used for compiling of functions (add, mult, etc..) *) -let get_vm_compiling_info knowledge key = - match (dispatch_reactive key knowledge).vm_compiling - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation - -(* used for compilation of fully applied constructors *) -let get_vm_constant_static_info knowledge key = - match (dispatch_reactive key knowledge).vm_constant_static - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation - -(* used for compilation of partially applied constructors *) -let get_vm_constant_dynamic_info knowledge key = - match (dispatch_reactive key knowledge).vm_constant_dynamic - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation - -let get_vm_before_match_info knowledge key = - match (dispatch_reactive key knowledge).vm_before_match - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation - -let get_vm_decompile_constant_info knowledge key = - match (dispatch_reactive key knowledge).vm_decompile_const - with - | None -> raise Not_found - | Some f -> f - -let get_native_compiling_info knowledge key = - match (dispatch_reactive key knowledge).native_compiling - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation - -(* used for compilation of fully applied constructors *) -let get_native_constant_static_info knowledge key = - match (dispatch_reactive key knowledge).native_constant_static - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation - -(* used for compilation of partially applied constructors *) -let get_native_constant_dynamic_info knowledge key = - match (dispatch_reactive key knowledge).native_constant_dynamic - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation - -let get_native_before_match_info knowledge key = - match (dispatch_reactive key knowledge).native_before_match - with - | None -> raise Not_found - | Some f -> f knowledge.flags.fastcomputation + | Register_ind of CPrimitives.prim_ind * inductive + | Register_type of CPrimitives.prim_type * Constant.t + | Register_inline of Constant.t diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0a2ef5300e..1554fe88da 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -9,157 +9,20 @@ (************************************************************************) open Names -open Constr - -type retroknowledge - -(** the following types correspond to the different "things" - the kernel can learn about.*) -type int31_field = - | Int31Bits - | Int31Type - | Int31Constructor - | Int31Twice - | Int31TwicePlusOne - | Int31Phi - | Int31PhiInv - | Int31Plus - | Int31PlusC - | Int31PlusCarryC - | Int31Minus - | Int31MinusC - | Int31MinusCarryC - | Int31Times - | Int31TimesC - | Int31Div21 - | Int31Div - | Int31Diveucl - | Int31AddMulDiv - | Int31Compare - | Int31Head0 - | Int31Tail0 - | Int31Lor - | Int31Land - | Int31Lxor - -type field = - | KInt31 of int31_field - -val int31_field_of_string : string -> int31_field - -val int31_path : DirPath.t - -(** This type represent an atomic action of the retroknowledge. It - is stored in the compiled libraries - As per now, there is only the possibility of registering things - the possibility of unregistering or changing the flag is under study *) -type action = - | RKRegister of field * GlobRef.t - - -(** initial value for retroknowledge *) -val initial_retroknowledge : retroknowledge - - -(** Given an identifier id (usually Const _) - and the continuation cont of the bytecode compilation - returns the compilation of id in cont if it has a specific treatment - or raises Not_found if id should be compiled as usual *) -val get_vm_compiling_info : retroknowledge -> GlobRef.t -> - Cinstr.lambda array -> Cinstr.lambda -(*Given an identifier id (usually Construct _) - and its argument array, returns a function that tries an ad-hoc optimisated - compilation (in the case of the 31-bit integers it means compiling them - directly into an integer) - raises Not_found if id should be compiled as usual, and expectingly - CBytecodes.NotClosed if the term is not a closed constructor pattern - (a constant for the compiler) *) -val get_vm_constant_static_info : retroknowledge -> GlobRef.t -> - constr array -> Cinstr.lambda - -(*Given an identifier id (usually Construct _ ) - its argument array and a continuation, returns the compiled version - of id+args+cont when id has a specific treatment (in the case of - 31-bit integers, that would be the dynamic compilation into integers) - or raises Not_found if id should be compiled as usual *) -val get_vm_constant_dynamic_info : retroknowledge -> GlobRef.t -> - Cinstr.lambda array -> Cinstr.lambda - -(** Given a type identifier, this function is used before compiling a match - over this type. In the case of 31-bit integers for instance, it is used - to add the instruction sequence which would perform a dynamic decompilation - in case the argument of the match is not in coq representation *) -val get_vm_before_match_info : retroknowledge -> GlobRef.t -> Cinstr.lambda - -> Cinstr.lambda - -(** Given a type identifier, this function is used by pretyping/vnorm.ml to - recover the elements of that type from their compiled form if it's non - standard (it is used (and can be used) only when the compiled form - is not a block *) -val get_vm_decompile_constant_info : retroknowledge -> GlobRef.t -> int -> constr - - -val get_native_compiling_info : retroknowledge -> GlobRef.t -> Nativeinstr.prefix -> - Nativeinstr.lambda array -> Nativeinstr.lambda - -val get_native_constant_static_info : retroknowledge -> GlobRef.t -> - constr array -> Nativeinstr.lambda - -val get_native_constant_dynamic_info : retroknowledge -> GlobRef.t -> - Nativeinstr.prefix -> constructor -> - Nativeinstr.lambda array -> - Nativeinstr.lambda - -val get_native_before_match_info : retroknowledge -> GlobRef.t -> - Nativeinstr.prefix -> constructor -> - Nativeinstr.lambda -> Nativeinstr.lambda - - -(** the following functions are solely used in Environ and Safe_typing to implement - the functions register and unregister (and mem) of Environ *) -val add_field : retroknowledge -> field -> GlobRef.t -> retroknowledge -val mem : retroknowledge -> field -> bool -(* val remove : retroknowledge -> field -> retroknowledge *) -val find : retroknowledge -> field -> GlobRef.t - - -(** Dispatching type for the above [get_*] functions. *) -type reactive_info = {(*information required by the compiler of the VM *) - vm_compiling : - (*fastcomputation flag -> continuation -> result *) - (bool -> Cinstr.lambda array -> Cinstr.lambda) - option; - vm_constant_static : - (*fastcomputation flag -> constructor -> args -> result*) - (bool -> constr array -> Cinstr.lambda) - option; - vm_constant_dynamic : - (*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *) - (bool -> Cinstr.lambda array -> Cinstr.lambda) - option; - (* fastcomputation flag -> cont -> result *) - vm_before_match : (bool -> Cinstr.lambda -> Cinstr.lambda) option; - (* tag (= compiled int for instance) -> result *) - vm_decompile_const : (int -> constr) option; - - native_compiling : - (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> - Nativeinstr.lambda) option; - - native_constant_static : - (bool -> constr array -> Nativeinstr.lambda) option; - - native_constant_dynamic : - (bool -> Nativeinstr.prefix -> constructor -> - Nativeinstr.lambda array -> Nativeinstr.lambda) option; - - native_before_match : (bool -> Nativeinstr.prefix -> constructor -> - Nativeinstr.lambda -> Nativeinstr.lambda) option +type retroknowledge = { + retro_int63 : Constant.t option; + retro_bool : (constructor * constructor) option; (* true, false *) + retro_carry : (constructor * constructor) option; (* C0, C1 *) + retro_pair : constructor option; + retro_cmp : (constructor * constructor * constructor) option; + (* Eq, Lt, Gt *) + retro_refl : constructor option; } -val empty_reactive_info : reactive_info +val empty : retroknowledge -(** Hook to be set after the compiler are installed to dispatch fields - into the above [get_*] functions. *) -val dispatch_hook : (retroknowledge -> GlobRef.t -> field -> reactive_info) Hook.t +type action = + | Register_ind of CPrimitives.prim_ind * inductive + | Register_type of CPrimitives.prim_type * Constant.t + | Register_inline of Constant.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index df9e253135..474ce3e871 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -59,10 +59,10 @@ etc. *) -open CErrors open Util open Names open Declarations +open Constr open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -227,6 +227,7 @@ let check_engagement env expected_impredicative_set = let get_opaque_body env cbo = match cbo.const_body with | Undef _ -> assert false + | Primitive _ -> assert false | Def _ -> `Nothing | OpaqueDef opaque -> `Opaque @@ -467,7 +468,7 @@ let globalize_constant_universes env cb = | Monomorphic_const cstrs -> Now (false, cstrs) :: (match cb.const_body with - | (Undef _ | Def _) -> [] + | (Undef _ | Def _ | Primitive _) -> [] | OpaqueDef lc -> match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with | None -> [] @@ -492,6 +493,11 @@ let constraints_of_sfb env sfb = | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)] | SFBmodule mb -> [Now (false, mb.mod_constraints)] +let add_retroknowledge pttc senv = + { senv with + env = Primred.add_retroknowledge senv.env pttc; + local_retroknowledge = pttc::senv.local_retroknowledge } + (** A generic function for adding a new field in a same environment. It also performs the corresponding [add_constraints]. *) @@ -809,6 +815,13 @@ let add_constant ~in_section l decl senv = let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in if in_section then cb else Declareops.hcons_const_body cb in add_constant_aux ~in_section senv (kn, cb) in + let senv = + match decl with + | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> + if in_section then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); + add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv + | _ -> senv + in kn, senv (** Insertion of inductive types *) @@ -1173,18 +1186,6 @@ let typing senv = Typeops.infer (env_of_senv senv) (** {6 Retroknowledge / native compiler } *) -let register field value senv = - (* todo : value closed *) - (* spiwack : updates the safe_env with the information that the register - action has to be performed (again) when the environment is imported *) - { senv with - env = Environ.register senv.env field value; - local_retroknowledge = - Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge - } - -(* This function serves only for inlining constants in native compiler for now, -but it is meant to become a replacement for environ.register *) let register_inline kn senv = let open Environ in if not (evaluable_constant kn senv.env) then @@ -1194,6 +1195,80 @@ let register_inline kn senv = let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} +let check_register_ind (mind,i) r env = + let mb = Environ.lookup_mind mind env in + let check_if b s = + if not b then + CErrors.user_err ~hdr:"check_register_ind" (Pp.str s) in + check_if (Int.equal (Array.length mb.mind_packets) 1) "A non mutual inductive is expected"; + let ob = mb.mind_packets.(i) in + let check_nconstr n = + check_if (Int.equal (Array.length ob.mind_consnames) n) + ("an inductive type with "^(string_of_int n)^" constructors is expected") + in + let check_name pos s = + check_if (Id.equal ob.mind_consnames.(pos) (Id.of_string s)) + ("the "^(string_of_int (pos + 1))^ + "th constructor does not have the expected name: " ^ s) in + let check_type pos t = + check_if (Constr.equal t ob.mind_user_lc.(pos)) + ("the "^(string_of_int (pos + 1))^ + "th constructor does not have the expected type") in + let check_type_cte pos = check_type pos (Constr.mkRel 1) in + match r with + | CPrimitives.PIT_bool -> + check_nconstr 2; + check_name 0 "true"; + check_type_cte 0; + check_name 1 "false"; + check_type_cte 1 + | CPrimitives.PIT_carry -> + check_nconstr 2; + let test_type pos = + let c = ob.mind_user_lc.(pos) in + let s = "the "^(string_of_int (pos + 1))^ + "th constructor does not have the expected type" in + check_if (Constr.isProd c) s; + let (_,d,cd) = Constr.destProd c in + check_if (Constr.is_Type d) s; + check_if + (Constr.equal + (mkProd (Anonymous,mkRel 1, mkApp (mkRel 3,[|mkRel 2|]))) + cd) + s in + check_name 0 "C0"; + test_type 0; + check_name 1 "C1"; + test_type 1; + | CPrimitives.PIT_pair -> + check_nconstr 1; + check_name 0 "pair"; + let c = ob.mind_user_lc.(0) in + let s = "the "^(string_of_int 1)^ + "th constructor does not have the expected type" in + begin match Term.decompose_prod c with + | ([_,b;_,a;_,_B;_,_A], codom) -> + check_if (is_Type _A) s; + check_if (is_Type _B) s; + check_if (Constr.equal a (mkRel 2)) s; + check_if (Constr.equal b (mkRel 2)) s; + check_if (Constr.equal codom (mkApp (mkRel 5,[|mkRel 4; mkRel 3|]))) s + | _ -> check_if false s + end + | CPrimitives.PIT_cmp -> + check_nconstr 3; + check_name 0 "Eq"; + check_type_cte 0; + check_name 1 "Lt"; + check_type_cte 1; + check_name 2 "Gt"; + check_type_cte 2 + +let register_inductive ind prim senv = + check_register_ind ind prim senv.env; + let action = Retroknowledge.Register_ind(prim,ind) in + add_retroknowledge action senv + let add_constraints c = add_constraints (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty)) @@ -1222,125 +1297,3 @@ Would this be correct with respect to undo's and stuff ? let set_strategy k l e = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } - -(** Register retroknowledge hooks *) - -open Retroknowledge - -(* the Environ.register function synchronizes the proactive and reactive - retroknowledge. *) -let dispatch = - - (* subfunction used for static decompilation of int31 (after a vm_compute, - see pretyping/vnorm.ml for more information) *) - let constr_of_int31 = - let nth_digit_plus_one i n = (* calculates the nth (starting with 0) - digit of i and adds 1 to it - (nth_digit_plus_one 1 3 = 2) *) - if Int.equal (i land (1 lsl n)) 0 then - 1 - else - 2 - in - fun ind -> fun digit_ind -> fun tag -> - let array_of_int i = - Array.init 31 (fun n -> Constr.mkConstruct - (digit_ind, nth_digit_plus_one i (30-n))) - in - (* We check that no bit above 31 is set to one. This assertion used to - fail in the VM, and led to conversion tests failing at Qed. *) - assert (Int.equal (tag lsr 31) 0); - Constr.mkApp(Constr.mkConstruct(ind, 1), array_of_int tag) - in - - (* subfunction which dispatches the compiling information of an - int31 operation which has a specific vm instruction (associates - it to the name of the coq definition in the reactive retroknowledge) *) - let int31_op n op prim kn = - { empty_reactive_info with - vm_compiling = Some (Clambda.compile_prim n op (kn, Univ.Instance.empty)); (*XXX: FIXME universes? *) - native_compiling = Some (Nativelambda.compile_prim prim kn); - } - in - -fun rk value field -> - (* subfunction which shortens the (very common) dispatch of operations *) - let int31_op_from_const n op prim = - match value with - | GlobRef.ConstRef kn -> int31_op n op prim kn - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") - in - let int31_binop_from_const op prim = int31_op_from_const 2 op prim in - let int31_unop_from_const op prim = int31_op_from_const 1 op prim in - match field with - | KInt31 Int31Type -> - let int31bit = - (* invariant : the type of bits is registered, otherwise the function - would raise Not_found. The invariant is enforced in safe_typing.ml *) - match field with - | KInt31 Int31Type -> Retroknowledge.find rk (KInt31 Int31Bits) - | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") - in - let i31bit_type = - match int31bit with - | GlobRef.IndRef i31bit_type -> i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type.") - in - let int31_decompilation = - match value with - | GlobRef.IndRef i31t -> - constr_of_int31 i31t i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type.") - in - { empty_reactive_info with - vm_decompile_const = Some int31_decompilation; - vm_before_match = Some Clambda.int31_escape_before_match; - native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); - } - | KInt31 Int31Constructor -> - { empty_reactive_info with - vm_constant_static = Some Clambda.compile_structured_int31; - vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; - native_constant_static = Some Nativelambda.compile_static_int31; - native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; - } - | KInt31 Int31Plus -> int31_binop_from_const Cbytecodes.Kaddint31 - CPrimitives.Int31add - | KInt31 Int31PlusC -> int31_binop_from_const Cbytecodes.Kaddcint31 - CPrimitives.Int31addc - | KInt31 Int31PlusCarryC -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - CPrimitives.Int31addcarryc - | KInt31 Int31Minus -> int31_binop_from_const Cbytecodes.Ksubint31 - CPrimitives.Int31sub - | KInt31 Int31MinusC -> int31_binop_from_const Cbytecodes.Ksubcint31 - CPrimitives.Int31subc - | KInt31 Int31MinusCarryC -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 Int31Times -> int31_binop_from_const Cbytecodes.Kmulint31 - CPrimitives.Int31mul - | KInt31 Int31TimesC -> int31_binop_from_const Cbytecodes.Kmulcint31 - CPrimitives.Int31mulc - | KInt31 Int31Div21 -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - CPrimitives.Int31div21 - | KInt31 Int31Diveucl -> int31_binop_from_const Cbytecodes.Kdivint31 - CPrimitives.Int31diveucl - | KInt31 Int31AddMulDiv -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - CPrimitives.Int31addmuldiv - | KInt31 Int31Compare -> int31_binop_from_const Cbytecodes.Kcompareint31 - CPrimitives.Int31compare - | KInt31 Int31Head0 -> int31_unop_from_const Cbytecodes.Khead0int31 - CPrimitives.Int31head0 - | KInt31 Int31Tail0 -> int31_unop_from_const Cbytecodes.Ktail0int31 - CPrimitives.Int31tail0 - | KInt31 Int31Lor -> int31_binop_from_const Cbytecodes.Klorint31 - CPrimitives.Int31lor - | KInt31 Int31Land -> int31_binop_from_const Cbytecodes.Klandint31 - CPrimitives.Int31land - | KInt31 Int31Lxor -> int31_binop_from_const Cbytecodes.Klxorint31 - CPrimitives.Int31lxor - | _ -> empty_reactive_info - -let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 57b01f15e3..1b7239da23 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -217,12 +217,8 @@ val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t (** {6 Retroknowledge / Native compiler } *) -open Retroknowledge - -val register : - field -> GlobRef.t -> safe_transformer0 - val register_inline : Constant.t -> safe_transformer0 +val register_inductive : inductive -> CPrimitives.prim_ind -> safe_transformer0 val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 347c30dd64..2fc3aa99b5 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -257,10 +257,10 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = anything of the right type can implement it, even if bodies differ. *) (match cb2.const_body with - | Undef _ | OpaqueDef _ -> cst + | Primitive _ | Undef _ | OpaqueDef _ -> cst | Def lc2 -> (match cb1.const_body with - | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField + | Primitive _ | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField | Def lc1 -> (* NB: cb1 might have been strengthened and appear as transparent. Anyway [check_conv] will handle that afterwards. *) diff --git a/kernel/term.ml b/kernel/term.ml index 795cdeb040..58b289eaa5 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -379,4 +379,4 @@ let kind_of_type t = match kind t with | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) -> AtomicType (t,[||]) - | (Lambda _ | Construct _) -> failwith "Not a type" + | (Lambda _ | Construct _ | Int _) -> failwith "Not a type" diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f9fdbdd68e..3cb5d17d34 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -93,10 +93,45 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = ctx; } + (** Primitives cannot be universe polymorphic *) + | PrimitiveEntry ({ prim_entry_type = otyp; + prim_entry_univs = uctxt; + prim_entry_content = op_t; + }) -> + let env = push_context_set ~strict:true uctxt env in + let ty = match otyp with + | Some typ -> + let tyj = infer_type env typ in + check_primitive_type env op_t tyj.utj_val; + Constr.hcons tyj.utj_val + | None -> + match op_t with + | CPrimitives.OT_op op -> type_of_prim env op + | CPrimitives.OT_type _ -> mkSet + in + let cd = + match op_t with + | CPrimitives.OT_op op -> Declarations.Primitive op + | CPrimitives.OT_type _ -> Undef None in + { Cooking.cook_body = cd; + cook_type = ty; + cook_universes = Monomorphic_const uctxt; + cook_private_univs = None; + cook_inline = false; + cook_context = None + } + (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. Remark: when the universe quantification is given explicitly, we could delay even in the polymorphic case. *) + +(** Definition is opaque (Qed) and non polymorphic with known type, so we delay +the typing and hash consing of its body. + +TODO: if the universe quantification is given explicitly, we could delay even in +the polymorphic case + *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_universes = Monomorphic_const_entry univs; _ } as c) -> @@ -238,7 +273,7 @@ let build_constant_declaration _kn env result = we must look at the body NOW, if any *) let ids_typ = global_vars_set env typ in let ids_def = match def with - | Undef _ -> Id.Set.empty + | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> let vars = @@ -258,7 +293,7 @@ let build_constant_declaration _kn env result = (* We use the declared set and chain a check of correctness *) sort declared, match def with - | Undef _ as x -> x (* nothing to check *) + | Undef _ | Primitive _ as x -> x (* nothing to check *) | Def cs as x -> let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in @@ -316,6 +351,7 @@ let translate_local_def env _id centry = if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin match decl.cook_body with | Undef _ -> () + | Primitive _ -> () | Def _ -> () | OpaqueDef lc -> let ids_typ = global_vars_set env typ in @@ -336,7 +372,7 @@ let translate_local_def env _id centry = the body by virtue of the typing of [Entries.section_def_entry]. *) let () = assert (Univ.ContextSet.is_empty cst) in p - | Undef _ -> assert false + | Undef _ | Primitive _ -> assert false in c, typ diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c9acd168e8..7eb8e803b3 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,7 +12,7 @@ open CErrors open Util open Names open Univ -open Sorts +open Term open Constr open Vars open Declarations @@ -187,6 +187,74 @@ let type_of_apply env func funt argsv argstv = in apply_rec 0 (inject funt) +(* Type of primitive constructs *) +let type_of_prim_type _env = function + | CPrimitives.PT_int63 -> Constr.mkSet + +let type_of_int env = + match env.retroknowledge.Retroknowledge.retro_int63 with + | Some c -> mkConst c + | None -> CErrors.user_err Pp.(str"The type int must be registered before this construction can be typechecked.") + +let type_of_prim env t = + let int_ty = type_of_int env in + let bool_ty () = + match env.retroknowledge.Retroknowledge.retro_bool with + | Some ((ind,_),_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.") + in + let compare_ty () = + match env.retroknowledge.Retroknowledge.retro_cmp with + | Some ((ind,_),_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") + in + let pair_ty fst_ty snd_ty = + match env.retroknowledge.Retroknowledge.retro_pair with + | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) + | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") + in + let carry_ty int_ty = + match env.retroknowledge.Retroknowledge.retro_carry with + | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) + | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.") + in + let rec nary_int63_op arity ty = + if Int.equal arity 0 then ty + else Constr.mkProd(Name (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty) + in + let return_ty = + let open CPrimitives in + match t with + | Int63head0 + | Int63tail0 + | Int63add + | Int63sub + | Int63mul + | Int63div + | Int63mod + | Int63lsr + | Int63lsl + | Int63land + | Int63lor + | Int63lxor + | Int63addMulDiv -> int_ty + | Int63eq + | Int63lt + | Int63le -> bool_ty () + | Int63mulc + | Int63div21 + | Int63diveucl -> pair_ty int_ty int_ty + | Int63addc + | Int63subc + | Int63addCarryC + | Int63subCarryC -> carry_ty int_ty + | Int63compare -> compare_ty () + in + nary_int63_op (CPrimitives.arity t) return_ty + +let judge_of_int env i = + make_judge (Constr.mkInt i) (type_of_int env) + (* Type of product *) let sort_of_product env domsort rangsort = @@ -468,6 +536,9 @@ let rec execute env cstr = let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in check_cofix env cofix; fix_ty + + (* Primitive types *) + | Int _ -> type_of_int env (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -590,3 +661,20 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + +(* Building type of primitive operators and type *) + +open CPrimitives + +let check_primitive_type env op_t t = + match op_t with + | OT_type PT_int63 -> + (try + default_conv ~l2r:false CUMUL env mkSet t + with NotConvertible -> + CErrors.user_err Pp.(str"Was expecting the sort of this primitive type to be Set")) + | OT_op p -> + (try + default_conv ~l2r:false CUMUL env (type_of_prim env p) t + with NotConvertible -> + CErrors.user_err Pp.(str"Not the expected type for this primitive")) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 4193324136..52c261c5e8 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -118,3 +118,13 @@ val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> ('a -> constr) -> 'a -> Constr.named_context -> unit + +val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit + +(** Types for primitives *) + +val type_of_int : env -> types +val judge_of_int : env -> Uint63.t -> unsafe_judgment + +val type_of_prim_type : env -> CPrimitives.prim_type -> types +val type_of_prim : env -> CPrimitives.t -> types diff --git a/kernel/uint31.ml b/kernel/uint31.ml deleted file mode 100644 index d9c723c243..0000000000 --- a/kernel/uint31.ml +++ /dev/null @@ -1,153 +0,0 @@ - (* Invariant: For arch64 all extra bytes are set to 0 *) -type t = int - - (* to be used only on 32 bits architectures *) -let maxuint31 = Int32.of_string "0x7FFFFFFF" -let uint_32 i = Int32.logand (Int32.of_int i) maxuint31 - -let select f32 f64 = if Sys.word_size = 64 then f64 else f32 - - (* conversion to an int *) -let to_int i = i - -let of_int_32 i = i -let of_int_64 i = i land 0x7FFFFFFF - -let of_int = select of_int_32 of_int_64 -let of_uint i = i - - (* conversion of an uint31 to a string *) -let to_string_32 i = Int32.to_string (uint_32 i) -let to_string_64 = string_of_int - -let to_string = select to_string_32 to_string_64 -let of_string s = - let i32 = Int32.of_string s in - if Int32.compare Int32.zero i32 <= 0 - && Int32.compare i32 maxuint31 <= 0 - then Int32.to_int i32 - else raise (Failure "int_of_string") - - - - (* logical shift *) -let l_sl x y = - of_int (if 0 <= y && y < 31 then x lsl y else 0) - -let l_sr x y = - if 0 <= y && y < 31 then x lsr y else 0 - -let l_and x y = x land y -let l_or x y = x lor y -let l_xor x y = x lxor y - - (* addition of int31 *) -let add x y = of_int (x + y) - - (* subtraction *) -let sub x y = of_int (x - y) - - (* multiplication *) -let mul x y = of_int (x * y) - - (* exact multiplication *) -let mulc_32 x y = - let x = Int64.of_int32 (uint_32 x) in - let y = Int64.of_int32 (uint_32 y) in - let m = Int64.mul x y in - let l = Int64.to_int m in - let h = Int64.to_int (Int64.shift_right_logical m 31) in - h,l - -let mulc_64 x y = - let m = x * y in - let l = of_int_64 m in - let h = of_int_64 (m lsr 31) in - h, l -let mulc = select mulc_32 mulc_64 - - (* division *) -let div_32 x y = - if y = 0 then 0 else - Int32.to_int (Int32.div (uint_32 x) (uint_32 y)) -let div_64 x y = if y = 0 then 0 else x / y -let div = select div_32 div_64 - - (* modulo *) -let rem_32 x y = - if y = 0 then 0 - else Int32.to_int (Int32.rem (uint_32 x) (uint_32 y)) -let rem_64 x y = if y = 0 then 0 else x mod y -let rem = select rem_32 rem_64 - - (* division of two numbers by one *) -let div21_32 xh xl y = - if y = 0 then (0,0) - else - let x = - Int64.logor - (Int64.shift_left (Int64.of_int32 (uint_32 xh)) 31) - (Int64.of_int32 (uint_32 xl)) in - let y = Int64.of_int32 (uint_32 y) in - let q = Int64.div x y in - let r = Int64.rem x y in - Int64.to_int q, Int64.to_int r -let div21_64 xh xl y = - if y = 0 then (0,0) - else - let x = (xh lsl 31) lor xl in - let q = x / y in - let r = x mod y in - q, r -let div21 = select div21_32 div21_64 - - (* comparison *) -let lt_32 x y = (x lxor 0x40000000) < (y lxor 0x40000000) - -(* Do not remove the type information it is really important for - efficiency *) -let lt_64 (x:int) (y:int) = x < y -let lt = select lt_32 lt_64 - -let le_32 x y = - (x lxor 0x40000000) <= (y lxor 0x40000000) - -(* Do not remove the type information it is really important for - efficiency *) -let le_64 (x:int) (y:int) = x <= y -let le = select le_32 le_64 - -let equal (x:int) (y:int) = x == y - -let cmp_32 x y = Int32.compare (uint_32 x) (uint_32 y) -(* Do not remove the type information it is really important for - efficiency *) -let cmp_64 (x:int) (y:int) = compare x y -let compare = select cmp_32 cmp_64 - - (* head tail *) - -let head0 x = - let r = ref 0 in - let x = ref x in - if !x land 0x7FFF0000 = 0 then r := !r + 15 - else x := !x lsr 15; - if !x land 0xFF00 = 0 then (x := !x lsl 8; r := !r + 8); - if !x land 0xF000 = 0 then (x := !x lsl 4; r := !r + 4); - if !x land 0xC000 = 0 then (x := !x lsl 2; r := !r + 2); - if !x land 0x8000 = 0 then (x := !x lsl 1; r := !r + 1); - if !x land 0x8000 = 0 then ( r := !r + 1); - !r;; - -let tail0 x = - let r = ref 0 in - let x = ref x in - if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16); - if !x land 0xFF = 0 then (x := !x lsr 8; r := !r + 8); - if !x land 0xF = 0 then (x := !x lsr 4; r := !r + 4); - if !x land 0x3 = 0 then (x := !x lsr 2; r := !r + 2); - if !x land 0x1 = 0 then ( r := !r + 1); - !r - -let add_digit x d = - (x lsl 1) lor d diff --git a/kernel/uint31.mli b/kernel/uint63.mli index d1f933cc4e..b5f40ca804 100644 --- a/kernel/uint31.mli +++ b/kernel/uint63.mli @@ -1,14 +1,28 @@ type t +val uint_size : int +val maxuint31 : t + (* conversion to int *) -val to_int : t -> int val of_int : int -> t +val to_int2 : t -> int * int (* msb, lsb *) +val of_int64 : Int64.t -> t +(* val of_uint : int -> t +*) + +val hash : t -> int - (* conversion to a string *) + (* convertion to a string *) val to_string : t -> string val of_string : string -> t +val compile : t -> string + +(* constants *) +val zero : t +val one : t + (* logical operations *) val l_sl : t -> t -> t val l_sr : t -> t -> t @@ -16,20 +30,21 @@ val l_and : t -> t -> t val l_xor : t -> t -> t val l_or : t -> t -> t - (* Arithmetic operations *) + (* Arithmetic operations *) val add : t -> t -> t val sub : t -> t -> t val mul : t -> t -> t val div : t -> t -> t val rem : t -> t -> t - + (* Specific arithmetic operations *) val mulc : t -> t -> t * t +val addmuldiv : t -> t -> t -> t val div21 : t -> t -> t -> t * t - + (* comparison *) val lt : t -> t -> bool -val equal : t -> t -> bool +val equal : t -> t -> bool val le : t -> t -> bool val compare : t -> t -> int @@ -37,5 +52,4 @@ val compare : t -> t -> int val head0 : t -> t val tail0 : t -> t -(** Used by retroknowledge *) -val add_digit : t -> t -> t +val is_uint63 : Obj.t -> bool diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64.ml new file mode 100644 index 0000000000..010b594de8 --- /dev/null +++ b/kernel/uint63_amd64.ml @@ -0,0 +1,215 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t = int + +let _ = assert (Sys.word_size = 64) + +let uint_size = 63 + +let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF" +let maxuint31 = 0x7FFFFFFF + + (* conversion from an int *) +let to_uint64 i = Int64.logand (Int64.of_int i) maxuint63 + +let of_int i = i +[@@ocaml.inline always] + +let to_int2 i = (0,i) + +let of_int64 _i = assert false + +let hash i = i +[@@ocaml.inline always] + + (* conversion of an uint63 to a string *) +let to_string i = Int64.to_string (to_uint64 i) + +let of_string s = + let i64 = Int64.of_string s in + if Int64.compare Int64.zero i64 <= 0 + && Int64.compare i64 maxuint63 <= 0 + then Int64.to_int i64 + else raise (Failure "Int64.of_string") + +(* Compiles an unsigned int to OCaml code *) +let compile i = Printf.sprintf "Uint63.of_int (%i)" i + +let zero = 0 +let one = 1 + + (* logical shift *) +let l_sl x y = + if 0 <= y && y < 63 then x lsl y else 0 + +let l_sr x y = + if 0 <= y && y < 63 then x lsr y else 0 + +let l_and x y = x land y +[@@ocaml.inline always] + +let l_or x y = x lor y +[@@ocaml.inline always] + +let l_xor x y = x lxor y +[@@ocaml.inline always] + + (* addition of int63 *) +let add x y = x + y +[@@ocaml.inline always] + + (* subtraction *) +let sub x y = x - y +[@@ocaml.inline always] + + (* multiplication *) +let mul x y = x * y +[@@ocaml.inline always] + + (* division *) +let div (x : int) (y : int) = + if y = 0 then 0 else Int64.to_int (Int64.div (to_uint64 x) (to_uint64 y)) + + (* modulo *) +let rem (x : int) (y : int) = + if y = 0 then 0 else Int64.to_int (Int64.rem (to_uint64 x) (to_uint64 y)) + +let addmuldiv p x y = + l_or (l_sl x p) (l_sr y (uint_size - p)) + + (* comparison *) +let lt (x : int) (y : int) = + (x lxor 0x4000000000000000) < (y lxor 0x4000000000000000) +[@@ocaml.inline always] + +let le (x : int) (y : int) = + (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) +[@@ocaml.inline always] + +(* A few helper functions on 128 bits *) +let lt128 xh xl yh yl = + lt xh yh || (xh = yh && lt xl yl) + +let le128 xh xl yh yl = + lt xh yh || (xh = yh && le xl yl) + + (* division of two numbers by one *) +let div21 xh xl y = + let maskh = ref 0 in + let maskl = ref 1 in + let dh = ref 0 in + let dl = ref y in + let cmp = ref true in + while !dh >= 0 && !cmp do + cmp := lt128 !dh !dl xh xl; + (* We don't use addmuldiv below to avoid checks on 1 *) + dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1)); + dl := !dl lsl 1; + maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1)); + maskl := !maskl lsl 1 + done; (* mask = 2^N, d = 2^N * d, d >= x *) + let remh = ref xh in + let reml = ref xl in + let quotient = ref 0 in + while !maskh lor !maskl <> 0 do + if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) + quotient := !quotient lor !maskl; + remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh; + reml := !reml - !dl; + end; + maskl := (!maskl lsr 1) lor (!maskh lsl (uint_size - 1)); + maskh := !maskh lsr 1; + dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1)); + dh := !dh lsr 1; + done; + !quotient, !reml + + (* exact multiplication *) +(* TODO: check that none of these additions could be a logical or *) + + +(* size = 32 + 31 + (hx << 31 + lx) * (hy << 31 + ly) = + hxhy << 62 + (hxly + lxhy) << 31 + lxly +*) + +(* precondition : (x lsr 62 = 0 || y lsr 62 = 0) *) +let mulc_aux x y = + let lx = x land maxuint31 in + let ly = y land maxuint31 in + let hx = x lsr 31 in + let hy = y lsr 31 in + (* hx and hy are 32 bits value but at most one is 32 *) + let hxy = hx * hy in (* 63 bits *) + let hxly = hx * ly in (* 63 bits *) + let lxhy = lx * hy in (* 63 bits *) + let lxy = lx * ly in (* 62 bits *) + let l = lxy lor (hxy lsl 62) (* 63 bits *) in + let h = hxy lsr 1 in (* 62 bits *) + let hl = hxly + lxhy in (* We can have a carry *) + let h = if lt hl hxly then h + (1 lsl 31) else h in + let hl'= hl lsl 31 in + let l = l + hl' in + let h = if lt l hl' then h + 1 else h in + let h = h + (hl lsr 32) in + (h,l) + +let mulc x y = + if (x lsr 62 = 0 || y lsr 62 = 0) then mulc_aux x y + else + let yl = y lxor (1 lsl 62) in + let (h,l) = mulc_aux x yl in + (* h << 63 + l = x * yl + x * y = x * (1 << 62 + yl) = + x << 62 + x*yl = x << 62 + h << 63 + l *) + let l' = l + (x lsl 62) in + let h = if lt l' l then h + 1 else h in + (h + (x lsr 1), l') + +let equal (x : int) (y : int) = x = y +[@@ocaml.inline always] + +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 + + (* head tail *) + +let head0 x = + let r = ref 0 in + let x = ref x in + if !x land 0x7FFFFFFF00000000 = 0 then r := !r + 31 + else x := !x lsr 31; + if !x land 0xFFFF0000 = 0 then (x := !x lsl 16; r := !r + 16); + if !x land 0xFF000000 = 0 then (x := !x lsl 8; r := !r + 8); + if !x land 0xF0000000 = 0 then (x := !x lsl 4; r := !r + 4); + if !x land 0xC0000000 = 0 then (x := !x lsl 2; r := !r + 2); + if !x land 0x80000000 = 0 then (x := !x lsl 1; r := !r + 1); + if !x land 0x80000000 = 0 then ( r := !r + 1); + !r;; + +let tail0 x = + let r = ref 0 in + let x = ref x in + if !x land 0xFFFFFFFF = 0 then (x := !x lsr 32; r := !r + 32); + if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16); + if !x land 0xFF = 0 then (x := !x lsr 8; r := !r + 8); + if !x land 0xF = 0 then (x := !x lsr 4; r := !r + 4); + if !x land 0x3 = 0 then (x := !x lsr 2; r := !r + 2); + if !x land 0x1 = 0 then ( r := !r + 1); + !r + +let is_uint63 t = + Obj.is_int t +[@@ocaml.inline always] diff --git a/kernel/uint63_x86.ml b/kernel/uint63_x86.ml new file mode 100644 index 0000000000..461184c432 --- /dev/null +++ b/kernel/uint63_x86.ml @@ -0,0 +1,209 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Invariant: the msb should be 0 *) +type t = Int64.t + +let _ = assert (Sys.word_size = 32) + +let uint_size = 63 + +let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF" +let maxuint31 = Int64.of_string "0x7FFFFFFF" + +let zero = Int64.zero +let one = Int64.one + + (* conversion from an int *) +let mask63 i = Int64.logand i maxuint63 +let of_int i = Int64.of_int i +let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i) +let of_int64 i = i +let hash i = + let (h,l) = to_int2 i in + (*Hashset.combine h l*) + h * 65599 + l + + (* conversion of an uint63 to a string *) +let to_string i = Int64.to_string i + +let of_string s = + let i64 = Int64.of_string s in + if Int64.compare Int64.zero i64 <= 0 + && Int64.compare i64 maxuint63 <= 0 + then i64 + else raise (Failure "Int63.of_string") + +(* Compiles an unsigned int to OCaml code *) +let compile i = Printf.sprintf "Uint63.of_int64 (%LiL)" i + + (* comparison *) +let lt x y = + Int64.compare x y < 0 + +let le x y = + Int64.compare x y <= 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 + +let l_sr x y = + if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) 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 + + (* addition of int63 *) +let add x y = mask63 (Int64.add x y) + +let addcarry x y = add (add x y) Int64.one + + (* subtraction *) +let sub x y = mask63 (Int64.sub x y) + +let subcarry x y = sub (sub x y) Int64.one + + (* multiplication *) +let mul x y = mask63 (Int64.mul x y) + + (* division *) +let div x y = + if y = 0L then 0L else Int64.div x y + + (* modulo *) +let rem x y = + if y = 0L then 0L else Int64.rem x y + +let addmuldiv p x y = + l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p)) + +(* A few helper functions on 128 bits *) +let lt128 xh xl yh yl = + lt xh yh || (xh = yh && lt xl yl) + +let le128 xh xl yh yl = + lt xh yh || (xh = yh && le xl yl) + + (* division of two numbers by one *) +let div21 xh xl y = + let maskh = ref zero in + let maskl = ref one in + let dh = ref zero in + let dl = ref y in + let cmp = ref true in + while le zero !dh && !cmp do + cmp := lt128 !dh !dl xh xl; + (* We don't use addmuldiv below to avoid checks on 1 *) + dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1))); + dl := l_sl !dl one; + maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1))); + maskl := l_sl !maskl one + done; (* mask = 2^N, d = 2^N * d, d >= x *) + let remh = ref xh in + let reml = ref xl in + let quotient = ref zero in + while not (Int64.equal (l_or !maskh !maskl) zero) do + if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) + quotient := l_or !quotient !maskl; + remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh; + reml := sub !reml !dl + end; + maskl := l_or (l_sr !maskl one) (l_sl !maskh (of_int (uint_size - 1))); + maskh := l_sr !maskh one; + dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1))); + dh := l_sr !dh one + done; + !quotient, !reml + + + (* exact multiplication *) +let mulc x y = + let lx = ref (Int64.logand x maxuint31) in + let ly = ref (Int64.logand y maxuint31) in + let hx = Int64.shift_right x 31 in + let hy = Int64.shift_right y 31 in + let hr = ref (Int64.mul hx hy) in + let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in + hr := (Int64.shift_right_logical !hr 1); + lx := Int64.mul !lx hy; + ly := Int64.mul hx !ly; + hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32)); + lr := Int64.add !lr (Int64.shift_left !lx 31); + hr := Int64.add !hr (Int64.shift_right_logical !lr 63); + lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr); + hr := Int64.add !hr (Int64.shift_right_logical !lr 63); + if Int64.logand !lr Int64.min_int <> 0L + then Int64.(sub !hr one, mask63 !lr) + else (!hr, !lr) + +let equal x y = mask63 x = mask63 y + +let compare x y = Int64.compare x y + +(* Number of leading zeroes *) +let head0 x = + let r = ref 0 in + let x = ref x in + if Int64.logand !x 0x7FFFFFFF00000000L = 0L then r := !r + 31 + else x := Int64.shift_right !x 31; + if Int64.logand !x 0xFFFF0000L = 0L then (x := Int64.shift_left !x 16; r := !r + 16); + if Int64.logand !x 0xFF000000L = 0L then (x := Int64.shift_left !x 8; r := !r + 8); + if Int64.logand !x 0xF0000000L = 0L then (x := Int64.shift_left !x 4; r := !r + 4); + if Int64.logand !x 0xC0000000L = 0L then (x := Int64.shift_left !x 2; r := !r + 2); + if Int64.logand !x 0x80000000L = 0L then (x := Int64.shift_left !x 1; r := !r + 1); + if Int64.logand !x 0x80000000L = 0L then (r := !r + 1); + Int64.of_int !r + +(* Number of trailing zeroes *) +let tail0 x = + let r = ref 0 in + let x = ref x in + if Int64.logand !x 0xFFFFFFFFL = 0L then (x := Int64.shift_right !x 32; r := !r + 32); + if Int64.logand !x 0xFFFFL = 0L then (x := Int64.shift_right !x 16; r := !r + 16); + if Int64.logand !x 0xFFL = 0L then (x := Int64.shift_right !x 8; r := !r + 8); + if Int64.logand !x 0xFL = 0L then (x := Int64.shift_right !x 4; r := !r + 4); + if Int64.logand !x 0x3L = 0L then (x := Int64.shift_right !x 2; r := !r + 2); + if Int64.logand !x 0x1L = 0L then (r := !r + 1); + Int64.of_int !r + +(* May an object be safely cast into an Uint63.t ? *) +let is_uint63 t = + Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag + && le (Obj.magic t) maxuint63 + +(* Register all exported functions so that they can be called from C code *) + +let () = + Callback.register "uint63 add" add; + Callback.register "uint63 addcarry" addcarry; + Callback.register "uint63 addmuldiv" addmuldiv; + Callback.register "uint63 div" div; + Callback.register "uint63 div21_ml" div21; + Callback.register "uint63 eq" equal; + Callback.register "uint63 eq0" (equal Int64.zero); + Callback.register "uint63 head0" head0; + Callback.register "uint63 land" l_and; + Callback.register "uint63 leq" le; + Callback.register "uint63 lor" l_or; + Callback.register "uint63 lsl" l_sl; + Callback.register "uint63 lsl1" (fun x -> l_sl x Int64.one); + Callback.register "uint63 lsr" l_sr; + Callback.register "uint63 lsr1" (fun x -> l_sr x Int64.one); + Callback.register "uint63 lt" lt; + Callback.register "uint63 lxor" l_xor; + Callback.register "uint63 mod" rem; + Callback.register "uint63 mul" mul; + Callback.register "uint63 mulc_ml" mulc; + Callback.register "uint63 one" one; + Callback.register "uint63 sub" sub; + Callback.register "uint63 subcarry" subcarry; + Callback.register "uint63 tail0" tail0 diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 246c90c09d..04a17f7b08 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -71,13 +71,15 @@ and conv_whd env pb k whd1 whd2 cu = done; !rcu else raise NotConvertible + | Vint64 i1, Vint64 i2 -> + if Int64.equal i1 i2 then cu else raise NotConvertible | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu - | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ + | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vint64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible diff --git a/kernel/vm.ml b/kernel/vm.ml index eaf64ba4af..83312a8530 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) - open Vmvalues external set_drawinstr : unit -> unit = "coq_set_drawinstr" @@ -170,7 +169,7 @@ let rec apply_stack a stk v = let apply_whd k whd = let v = val_of_rel k in match whd with - | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false + | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ -> assert false | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 217ef4b8e5..9a3eadf747 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -57,6 +57,7 @@ type structured_constant = | Const_b0 of tag | Const_univ_level of Univ.Level.t | Const_val of structured_values + | Const_uint of Uint63.t type reloc_table = (tag * int) array @@ -73,7 +74,9 @@ let rec eq_structured_values v1 v2 = let t2 = Obj.tag o2 in if Int.equal t1 t2 && Int.equal (Obj.size o1) (Obj.size o2) - then begin + then if Int.equal t1 Obj.custom_tag + then Int64.equal (Obj.magic v1 : int64) (Obj.magic v2 : int64) + else begin assert (t1 <= Obj.last_non_constant_constructor_tag && t2 <= Obj.last_non_constant_constructor_tag); let i = ref 0 in @@ -100,7 +103,9 @@ let eq_structured_constant c1 c2 = match c1, c2 with | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false | Const_val v1, Const_val v2 -> eq_structured_values v1 v2 -| Const_val _v1, _ -> false +| Const_val _, _ -> false +| Const_uint i1, Const_uint i2 -> Uint63.equal i1 i2 +| Const_uint _, _ -> false let hash_structured_constant c = let open Hashset.Combine in @@ -110,6 +115,7 @@ let hash_structured_constant c = | Const_b0 t -> combinesmall 3 (Int.hash t) | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l) | Const_val v -> combinesmall 5 (hash_structured_values v) + | Const_uint i -> combinesmall 6 (Uint63.hash i) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -142,6 +148,7 @@ let pp_struct_const = function | Const_b0 i -> Pp.int i | Const_univ_level l -> Univ.Level.pr l | Const_val _ -> Pp.str "(value)" + | Const_uint i -> Pp.str (Uint63.to_string i) (* Abstract data *) type vprod @@ -276,6 +283,7 @@ type whd = | Vcofix of vcofix * to_update * arguments option | Vconstr_const of int | Vconstr_block of vblock + | Vint64 of int64 | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -306,8 +314,9 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vcofix _ -> str "Vcofix" | Vconstr_const _i -> str "Vconstr_const" | Vconstr_block _b -> str "Vconstr_block" + | Vint64 _ -> str "Vint64" | Vatom_stk (_a,_stk) -> str "Vatom_stk" - | _ -> assert false + | Vuniv_level _ -> assert false in CErrors.anomaly Pp.( strbrk "Parsing virtual machine value expected universe level, got " @@ -363,6 +372,8 @@ let rec whd_accu a stk = | [Zapp args] -> Vcofix(vcofix, res, Some args) | _ -> assert false end + | i when Int.equal i Obj.custom_tag -> + Vint64 (Obj.magic i) | tg -> CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") @@ -391,6 +402,7 @@ let whd_val : values -> whd = | 2 -> Vfix(Obj.obj (Obj.field o 1), 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.")) + else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) else Vconstr_block(Obj.obj o) @@ -413,6 +425,7 @@ let obj_of_str_const str = | Const_b0 tag -> Obj.repr tag | Const_univ_level l -> Obj.repr (Vuniv_level l) | Const_val v -> Obj.repr v + | Const_uint i -> Obj.repr i let val_of_block tag (args : structured_values array) = let nargs = Array.length args in @@ -430,6 +443,8 @@ let val_of_atom a = val_of_obj (obj_of_atom a) let val_of_int i = (Obj.magic i : values) +let val_of_uint i = (Obj.magic i : values) + let atom_of_proj kn v = let r = Obj.new_block proj_tag 2 in Obj.set_field r 0 (Obj.repr kn); @@ -659,6 +674,7 @@ and pr_whd w = | Vcofix _ -> str "Vcofix" | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" | Vconstr_block _b -> str "Vconstr_block" + | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" | Vuniv_level _ -> assert false) and pr_stack stk = diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index ae1d416ed5..6d984d5f49 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -44,6 +44,7 @@ type structured_constant = | Const_b0 of tag | Const_univ_level of Univ.Level.t | Const_val of structured_values + | Const_uint of Uint63.t val pp_struct_const : structured_constant -> Pp.t @@ -125,6 +126,7 @@ type whd = | Vcofix of vcofix * to_update * arguments option | Vconstr_const of int | Vconstr_block of vblock + | Vint64 of int64 | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -145,6 +147,7 @@ val val_of_proj : Projection.Repr.t -> values -> values val val_of_atom : atom -> values val val_of_int : int -> structured_values val val_of_block : tag -> structured_values array -> structured_values +val val_of_uint : Uint63.t -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml new file mode 100644 index 0000000000..0fcaf4f10a --- /dev/null +++ b/kernel/write_uint63.ml @@ -0,0 +1,30 @@ +(** Equivalent of rm -f *) + +let safe_remove f = + try Unix.chmod f 0o644; Sys.remove f with _ -> () + +(** * Generate an implementation of 63-bit arithmetic *) + +let ml_file_copy input output = + safe_remove output; + let i = open_in input in + let o = open_out output in + let pr s = Printf.fprintf o s in + pr "(* DO NOT EDIT THIS FILE: automatically generated by ./write_uint63.ml *)\n"; + pr "(* see uint63_amd64.ml and uint63_x86.ml *)\n"; + try + while true do + output_string o (input_line i); output_char o '\n' + done + with End_of_file -> + close_in i; + close_out o; + Unix.chmod output 0o444 + +let write_uint63 () = + ml_file_copy + (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml" + else (* 64 bits *) "uint63_amd64.ml") + "uint63.ml" + +let () = write_uint63 () |