diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /kernel | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
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 () |
