diff options
Diffstat (limited to 'kernel')
73 files changed, 2910 insertions, 660 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 0865487c98..931b509f48 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -44,6 +44,7 @@ void init_arity () { arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= + arity[LTFLOAT]=arity[LEFLOAT]= arity[ISINT]=arity[AREINT2]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= @@ -63,7 +64,15 @@ void init_arity () { arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= - arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1; + arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= + arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]= + arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= + arity[CHECKCLASSIFYFLOAT]= + arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= + arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= + arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= + arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]= + arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[PROJ]=2; diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h new file mode 100644 index 0000000000..c41079c8ff --- /dev/null +++ b/kernel/byterun/coq_float64.h @@ -0,0 +1,48 @@ +#ifndef _COQ_FLOAT64_ +#define _COQ_FLOAT64_ + +#include <math.h> + +#define DECLARE_FREL(name, e) \ + int coq_##name(double x, double y) { \ + return e; \ + } \ + \ + value coq_##name##_byte(value x, value y) { \ + return coq_##name(Double_val(x), Double_val(y)); \ + } + +#define DECLARE_FBINOP(name, e) \ + double coq_##name(double x, double y) { \ + return e; \ + } \ + \ + value coq_##name##_byte(value x, value y) { \ + return caml_copy_double(coq_##name(Double_val(x), Double_val(y))); \ + } + +#define DECLARE_FUNOP(name, e) \ + double coq_##name(double x) { \ + return e; \ + } \ + \ + value coq_##name##_byte(value x) { \ + return caml_copy_double(coq_##name(Double_val(x))); \ + } + +DECLARE_FREL(feq, x == y) +DECLARE_FREL(flt, x < y) +DECLARE_FREL(fle, x <= y) +DECLARE_FBINOP(fmul, x * y) +DECLARE_FBINOP(fadd, x + y) +DECLARE_FBINOP(fsub, x - y) +DECLARE_FBINOP(fdiv, x / y) +DECLARE_FUNOP(fsqrt, sqrt(x)) +DECLARE_FUNOP(next_up, nextafter(x, INFINITY)) +DECLARE_FUNOP(next_down, nextafter(x, -INFINITY)) + +value coq_is_double(value x) { + return Val_long(Is_double(x)); +} + +#endif /* _COQ_FLOAT64_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 4b45608ae5..ca1308696c 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -17,11 +17,13 @@ #include <signal.h> #include <stdint.h> #include <caml/memory.h> +#include <math.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" +#include "coq_float64.h" #ifdef ARCH_SIXTYFOUR #include "coq_uint63_native.h" @@ -167,38 +169,34 @@ if (sp - num_args < coq_stack_threshold) { \ #endif #endif -#define CheckInt1() do{ \ - if (Is_uint63(accu)) pc++; \ +#define CheckPrimArgs(cond, apply_lbl) do{ \ + if (cond) 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; \ + goto apply_lbl; \ } \ }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 CheckInt1() CheckPrimArgs(Is_uint63(accu), apply1) +#define CheckInt2() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]), apply2) +#define CheckInt3() CheckPrimArgs(Is_uint63(accu) && Is_uint63(sp[0]) \ + && Is_uint63(sp[1]), apply3) +#define CheckFloat1() CheckPrimArgs(Is_double(accu), apply1) +#define CheckFloat2() CheckPrimArgs(Is_double(accu) && Is_double(sp[0]), apply2) #define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0) #define AllocPair() Alloc_small(accu, 2, coq_tag_pair) +/* Beware: we cannot use caml_copy_double here as it doesn't use + Alloc_small, hence doesn't protect the stack via + Setup_for_gc/Restore_after_gc. */ +#define Coq_copy_double(val) do{ \ + double Coq_copy_double_f__ = (val); \ + Alloc_small(accu, Double_wosize, Double_tag); \ + Store_double_val(accu, Coq_copy_double_f__); \ + }while(0); + #define Swap_accu_sp do{ \ value swap_accu_sp_tmp__ = accu; \ accu = *sp; \ @@ -1533,6 +1531,206 @@ value coq_interprete } + Instruct (CHECKOPPFLOAT) { + print_instr("CHECKOPPFLOAT"); + CheckFloat1(); + Coq_copy_double(-Double_val(accu)); + Next; + } + + Instruct (CHECKABSFLOAT) { + print_instr("CHECKABSFLOAT"); + CheckFloat1(); + Coq_copy_double(fabs(Double_val(accu))); + Next; + } + + Instruct (CHECKEQFLOAT) { + print_instr("CHECKEQFLOAT"); + CheckFloat2(); + accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLTFLOAT) { + print_instr("CHECKLTFLOAT"); + CheckFloat2(); + } + Instruct (LTFLOAT) { + print_instr("LTFLOAT"); + accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLEFLOAT) { + print_instr("CHECKLEFLOAT"); + CheckFloat2(); + } + Instruct (LEFLOAT) { + print_instr("LEFLOAT"); + accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + Next; + } + + Instruct (CHECKCOMPAREFLOAT) { + double x, y; + print_instr("CHECKCOMPAREFLOAT"); + CheckFloat2(); + x = Double_val(accu); + y = Double_val(*sp++); + if(x < y) { + accu = coq_FLt; + } + else if(x > y) { + accu = coq_FGt; + } + else if(x == y) { + accu = coq_FEq; + } + else { // nan value + accu = coq_FNotComparable; + } + Next; + } + + Instruct (CHECKCLASSIFYFLOAT) { + double x; + print_instr("CHECKCLASSIFYFLOAT"); + CheckFloat1(); + x = Double_val(accu); + switch (fpclassify(x)) { + case FP_NORMAL: + accu = signbit(x) ? coq_NNormal : coq_PNormal; + break; + case FP_SUBNORMAL: + accu = signbit(x) ? coq_NSubn : coq_PSubn; + break; + case FP_ZERO: + accu = signbit(x) ? coq_NZero : coq_PZero; + break; + case FP_INFINITE: + accu = signbit(x) ? coq_NInf : coq_PInf; + break; + default: /* FP_NAN */ + accu = coq_NaN; + break; + } + Next; + } + + Instruct (CHECKADDFLOAT) { + print_instr("CHECKADDFLOAT"); + CheckFloat2(); + Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++))); + Next; + } + + Instruct (CHECKSUBFLOAT) { + print_instr("CHECKSUBFLOAT"); + CheckFloat2(); + Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++))); + Next; + } + + Instruct (CHECKMULFLOAT) { + print_instr("CHECKMULFLOAT"); + CheckFloat2(); + Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++))); + Next; + } + + Instruct (CHECKDIVFLOAT) { + print_instr("CHECKDIVFLOAT"); + CheckFloat2(); + Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++))); + Next; + } + + Instruct (CHECKSQRTFLOAT) { + print_instr("CHECKSQRTFLOAT"); + CheckFloat1(); + Coq_copy_double(coq_fsqrt(Double_val(accu))); + Next; + } + + Instruct (CHECKFLOATOFINT63) { + print_instr("CHECKFLOATOFINT63"); + CheckInt1(); + Uint63_to_double(accu); + Next; + } + + Instruct (CHECKFLOATNORMFRMANTISSA) { + double f; + print_instr("CHECKFLOATNORMFRMANTISSA"); + CheckFloat1(); + f = fabs(Double_val(accu)); + if (f >= 0.5 && f < 1) { + Uint63_of_double(ldexp(f, DBL_MANT_DIG)); + } + else { + Uint63_of_int(Val_int(0)); + } + Next; + } + + Instruct (CHECKFRSHIFTEXP) { + int exp; + double f; + print_instr("CHECKFRSHIFTEXP"); + CheckFloat1(); + /* frexp(infinity) incorrectly returns nan on mingw */ +#if defined(__MINGW32__) || defined(__MINGW64__) + if (fpclassify(Double_val(accu)) == FP_INFINITE) { + f = Double_val(accu); + } else +#endif + f = frexp(Double_val(accu), &exp); + if (fpclassify(f) == FP_NORMAL) { + exp += FLOAT_EXP_SHIFT; + } + else { + exp = 0; + } + Coq_copy_double(f); + *--sp = accu; +#ifdef ARCH_SIXTYFOUR + Alloc_small(accu, 2, coq_tag_pair); + Field(accu, 1) = Val_int(exp); +#else + Uint63_of_int(Val_int(exp)); + *--sp = accu; + Alloc_small(accu, 2, coq_tag_pair); + Field(accu, 1) = *sp++; +#endif + Field(accu, 0) = *sp++; + Next; + } + + Instruct (CHECKLDSHIFTEXP) { + print_instr("CHECKLDSHIFTEXP"); + CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2); + Swap_accu_sp; + Uint63_to_int_min(accu, Val_int(2 * FLOAT_EXP_SHIFT)); + accu = Int_val(accu); + Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT)); + Next; + } + + Instruct (CHECKNEXTUPFLOAT) { + print_instr("CHECKNEXTUPFLOAT"); + CheckFloat1(); + Coq_copy_double(coq_next_up(Double_val(accu))); + Next; + } + + Instruct (CHECKNEXTDOWNFLOAT) { + print_instr("CHECKNEXTDOWNFLOAT"); + CheckFloat1(); + Coq_copy_double(coq_next_down(Double_val(accu))); + Next; + } + /* Debugging and machine control */ Instruct(STOP){ diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 528cc6fc1f..143a6d098c 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -156,3 +156,18 @@ DECLARE_BINOP(mulc_ml) *(h) = Field(uint63_return_value__, 0); \ accu = Field(uint63_return_value__, 1); \ }while(0) + +DECLARE_UNOP(to_float) +#define Uint63_to_double(x) CALL_UNOP(to_float, x) + +DECLARE_UNOP(of_float) +#define Uint63_of_double(f) do{ \ + Coq_copy_double(f); \ + CALL_UNOP(of_float, accu); \ + }while(0) + +DECLARE_UNOP(of_int) +#define Uint63_of_int(x) CALL_UNOP(of_int, x) + +DECLARE_BINOP(to_int_min) +#define Uint63_to_int_min(n, m) CALL_BINOP(to_int_min, n, m) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 9fbd3f83d8..5be7587091 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -138,3 +138,26 @@ value uint63_div21(value xh, value xl, value y, value* ql) { } } #define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q)) + +#define Uint63_to_double(x) Coq_copy_double((double) uint63_of_value(x)) + +double coq_uint63_to_float(value x) { + return (double) uint63_of_value(x); +} + +value coq_uint63_to_float_byte(value x) { + return caml_copy_double(coq_uint63_to_float(x)); +} + +#define Uint63_of_double(f) do{ \ + accu = Val_long((uint64_t)(f)); \ + }while(0) + +#define Uint63_of_int(x) (accu = (x)) + +#define Uint63_to_int_min(n, m) do { \ + if (uint63_lt((n),(m))) \ + accu = (n); \ + else \ + accu = (m); \ + }while(0) diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 0cf6ccf532..b027673ac7 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -14,6 +14,8 @@ #include <caml/alloc.h> #include <caml/mlvalues.h> +#include <float.h> + #define Default_tag 0 #define Accu_tag 0 @@ -29,8 +31,9 @@ /* 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 Is_double(v) (Tag_val(v) == Double_tag) -/* */ +/* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 #define coq_tag_pair 1 @@ -39,5 +42,20 @@ #define coq_Eq Val_int(0) #define coq_Lt Val_int(1) #define coq_Gt Val_int(2) +#define coq_FEq Val_int(0) +#define coq_FLt Val_int(1) +#define coq_FGt Val_int(2) +#define coq_FNotComparable Val_int(3) +#define coq_PNormal Val_int(0) +#define coq_NNormal Val_int(1) +#define coq_PSubn Val_int(2) +#define coq_NSubn Val_int(3) +#define coq_PZero Val_int(4) +#define coq_NZero Val_int(5) +#define coq_PInf Val_int(6) +#define coq_NInf Val_int(7) +#define coq_NaN Val_int(8) + +#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ #endif /* _COQ_VALUES_ */ diff --git a/kernel/byterun/dune b/kernel/byterun/dune index 20bdf28e54..d0145176ea 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -1,3 +1,16 @@ +; Dune doesn't use configure's output, but it is still necessary for +; some Coq files to work; will be fixed in the future. +(rule + (targets dune.c_flags) + (mode fallback) + (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) + (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no)))) + +(env + (dev (c_flags (:include dune.c_flags))) + (release (c_flags (:include dune.c_flags))) + (ireport (c_flags (:include dune.c_flags)))) + (library (name byterun) (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 3fd613e905..72585e5014 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -348,6 +348,7 @@ and fterm = | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FInt of Uint63.t + | FFloat of Float64.t | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -428,7 +429,7 @@ let rec stack_args_size = function let rec lft_fconstr n ft = let r = Mark.relevance ft.mark in match ft.term with - | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft + | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _|FFloat _) -> ft | FRel i -> {mark=mark Norm r;term=FRel(i+n)} | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))} | FFix(fx,e) -> @@ -499,6 +500,7 @@ let mk_clos e t = | Ind kn -> {mark = mark Norm KnownR; term = FInd kn } | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn } | Int i -> {mark = mark Cstr Unknown; term = FInt i} + | Float f -> {mark = mark Cstr Unknown; term = FFloat f} | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {mark = mark Red Unknown; term = FCLOS(t,e)} @@ -616,6 +618,8 @@ let rec to_constr lfts v = | FInt i -> Constr.mkInt i + | FFloat f -> + Constr.mkFloat f | FCLOS (t,env) -> if is_subs_id env && is_lift_id lfts then t @@ -926,7 +930,7 @@ let rec knh info m stk = (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| - FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _) -> + FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) -> (m, stk) (* The same for pure terms *) @@ -940,7 +944,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 { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk - | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk) + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk) | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk | Prod (n, t, c) -> @@ -969,6 +973,11 @@ module FNativeEntries = | FInt i -> i | _ -> raise Primred.NativeDestKO + let get_float () e = + match [@ocaml.warning "-4"] e.term with + | FFloat f -> f + | _ -> raise Primred.NativeDestKO + let dummy = {mark = mark Norm KnownR; term = FRel 0} let current_retro = ref Retroknowledge.empty @@ -982,6 +991,16 @@ module FNativeEntries = fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } | None -> defined_int := false + let defined_float = ref false + let ffloat = ref dummy + + let init_float retro = + match retro.Retroknowledge.retro_float64 with + | Some c -> + defined_float := true; + ffloat := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + | None -> defined_float := false + let defined_bool = ref false let ftrue = ref dummy let ffalse = ref dummy @@ -1020,6 +1039,7 @@ module FNativeEntries = let fEq = ref dummy let fLt = ref dummy let fGt = ref dummy + let fcmp = ref dummy let init_cmp retro = match retro.Retroknowledge.retro_cmp with @@ -1027,9 +1047,54 @@ module FNativeEntries = defined_cmp := true; fEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cEq) }; fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) }; - fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) } + fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) }; + let (icmp, _) = cEq in + fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) } | None -> defined_cmp := false + let defined_f_cmp = ref false + let fFEq = ref dummy + let fFLt = ref dummy + let fFGt = ref dummy + let fFNotComparable = ref dummy + + let init_f_cmp retro = + match retro.Retroknowledge.retro_f_cmp with + | Some (cFEq, cFLt, cFGt, cFNotComparable) -> + defined_f_cmp := true; + fFEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFEq) }; + fFLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFLt) }; + fFGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFGt) }; + fFNotComparable := + { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cFNotComparable) }; + | None -> defined_f_cmp := false + + let defined_f_class = ref false + let fPNormal = ref dummy + let fNNormal = ref dummy + let fPSubn = ref dummy + let fNSubn = ref dummy + let fPZero = ref dummy + let fNZero = ref dummy + let fPInf = ref dummy + let fNInf = ref dummy + let fNaN = ref dummy + + let init_f_class retro = + match retro.Retroknowledge.retro_f_class with + | Some (cPNormal, cNNormal, cPSubn, cNSubn, cPZero, cNZero, + cPInf, cNInf, cNaN) -> + defined_f_class := true; + fPNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPNormal) }; + fNNormal := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNNormal) }; + fPSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPSubn) }; + fNSubn := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNSubn) }; + fPZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPZero) }; + fNZero := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNZero) }; + fPInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cPInf) }; + fNInf := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNInf) }; + fNaN := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNaN) }; + | None -> defined_f_class := false let defined_refl = ref false let frefl = ref dummy @@ -1044,10 +1109,13 @@ module FNativeEntries = let init env = current_retro := env.retroknowledge; init_int !current_retro; + init_float !current_retro; init_bool !current_retro; init_carry !current_retro; init_pair !current_retro; init_cmp !current_retro; + init_f_cmp !current_retro; + init_f_class !current_retro; init_refl !current_retro let check_env env = @@ -1057,6 +1125,10 @@ module FNativeEntries = check_env env; assert (!defined_int) + let check_float env = + check_env env; + assert (!defined_float) + let check_bool env = check_env env; assert (!defined_bool) @@ -1073,10 +1145,22 @@ module FNativeEntries = check_env env; assert (!defined_cmp) + let check_f_cmp env = + check_env env; + assert (!defined_f_cmp) + + let check_f_class env = + check_env env; + assert (!defined_f_class) + let mkInt env i = check_int env; { mark = mark Cstr KnownR; term = FInt i } + let mkFloat env f = + check_float env; + { mark = mark Norm KnownR; term = FFloat f } + let mkBool env b = check_bool env; if b then !ftrue else !ffalse @@ -1090,6 +1174,11 @@ module FNativeEntries = check_pair env; { mark = mark Cstr KnownR; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) } + let mkFloatIntPair env f i = + check_pair env; + check_float env; + { mark = mark Cstr KnownR; term = FApp(!fPair, [|!ffloat;!fint;f;i|]) } + let mkLt env = check_cmp env; !fLt @@ -1102,6 +1191,57 @@ module FNativeEntries = check_cmp env; !fGt + let mkFLt env = + check_f_cmp env; + !fFLt + + let mkFEq env = + check_f_cmp env; + !fFEq + + let mkFGt env = + check_f_cmp env; + !fFGt + + let mkFNotComparable env = + check_f_cmp env; + !fFNotComparable + + let mkPNormal env = + check_f_class env; + !fPNormal + + let mkNNormal env = + check_f_class env; + !fNNormal + + let mkPSubn env = + check_f_class env; + !fPSubn + + let mkNSubn env = + check_f_class env; + !fNSubn + + let mkPZero env = + check_f_class env; + !fPZero + + let mkNZero env = + check_f_class env; + !fNZero + + let mkPInf env = + check_f_class env; + !fPInf + + let mkNInf env = + check_f_class env; + !fNInf + + let mkNaN env = + check_f_class env; + !fNaN end module FredNative = RedNative(FNativeEntries) @@ -1164,7 +1304,7 @@ let rec knr info tab m stk = (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) - | FInt _ -> + | FInt _ | FFloat _ -> (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 @@ -1270,7 +1410,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 _ | FInt _ -> term_of_fconstr m + | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m (* Initialization and then normalization *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index cd1de4c834..720f11b8f2 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -115,6 +115,7 @@ type fterm = | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FInt of Uint63.t + | FFloat of Float64.t | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index d854cadd15..9ff7f69203 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -33,6 +33,24 @@ type t = | Int63lt | Int63le | Int63compare + | Float64opp + | Float64abs + | Float64eq + | Float64lt + | Float64le + | Float64compare + | Float64classify + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp + | Float64next_up + | Float64next_down let equal (p1 : t) (p2 : t) = p1 == p2 @@ -62,6 +80,24 @@ let hash = function | Int63lt -> 22 | Int63le -> 23 | Int63compare -> 24 + | Float64opp -> 25 + | Float64abs -> 26 + | Float64compare -> 27 + | Float64classify -> 28 + | Float64add -> 29 + | Float64sub -> 30 + | Float64mul -> 31 + | Float64div -> 32 + | Float64sqrt -> 33 + | Float64ofInt63 -> 34 + | Float64normfr_mantissa -> 35 + | Float64frshiftexp -> 36 + | Float64ldshiftexp -> 37 + | Float64next_up -> 38 + | Float64next_down -> 39 + | Float64eq -> 40 + | Float64lt -> 41 + | Float64le -> 42 (* Should match names in nativevalues.ml *) let to_string = function @@ -89,6 +125,72 @@ let to_string = function | Int63lt -> "lt" | Int63le -> "le" | Int63compare -> "compare" + | Float64opp -> "fopp" + | Float64abs -> "fabs" + | Float64eq -> "feq" + | Float64lt -> "flt" + | Float64le -> "fle" + | Float64compare -> "fcompare" + | Float64classify -> "fclassify" + | Float64add -> "fadd" + | Float64sub -> "fsub" + | Float64mul -> "fmul" + | Float64div -> "fdiv" + | Float64sqrt -> "fsqrt" + | Float64ofInt63 -> "float_of_int" + | Float64normfr_mantissa -> "normfr_mantissa" + | Float64frshiftexp -> "frshiftexp" + | Float64ldshiftexp -> "ldshiftexp" + | Float64next_up -> "next_up" + | Float64next_down -> "next_down" + +type prim_type = + | PT_int63 + | PT_float64 + +type 'a prim_ind = + | PIT_bool : unit prim_ind + | PIT_carry : prim_type prim_ind + | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_cmp : unit prim_ind + | PIT_f_cmp : unit prim_ind + | PIT_f_class : unit prim_ind + +type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex + +type ind_or_type = + | PITT_ind : 'a prim_ind * 'a -> ind_or_type + | PITT_type : prim_type -> ind_or_type + +let types = + let int_ty = PITT_type PT_int63 in + let float_ty = PITT_type PT_float64 in + function + | Int63head0 | Int63tail0 -> [int_ty; int_ty] + | Int63add | Int63sub | Int63mul + | Int63div | Int63mod + | Int63lsr | Int63lsl + | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] + | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> + [int_ty; int_ty; PITT_ind (PIT_carry, PT_int63)] + | Int63mulc | Int63diveucl -> + [int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))] + | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] + | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] + | Int63div21 -> + [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))] + | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] + | Float64opp | Float64abs | Float64sqrt + | Float64next_up | Float64next_down -> [float_ty; float_ty] + | Float64ofInt63 -> [int_ty; float_ty] + | Float64normfr_mantissa -> [float_ty; int_ty] + | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))] + | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())] + | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())] + | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())] + | Float64add | Float64sub | Float64mul + | Float64div -> [float_ty; float_ty; float_ty] + | Float64ldshiftexp -> [float_ty; int_ty; float_ty] type arg_kind = | Kparam (* not needed for the evaluation of the primitive when it reduces *) @@ -97,58 +199,32 @@ type arg_kind = type args_red = arg_kind list -(* Invariant only argument of type int63 or an inductive can +(* Invariant only argument of type int63, float 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] +let arity t = List.length (types t) - 1 - | 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 +let kind t = + let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in + aux (arity t) (** 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 +let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_bool -> "bool" | PIT_carry -> "carry" | PIT_pair -> "pair" | PIT_cmp -> "cmp" + | PIT_f_cmp -> "f_cmp" + | PIT_f_class -> "f_class" let prim_type_to_string = function | PT_int63 -> "int63_type" + | PT_float64 -> "float64_type" let op_or_type_to_string = function | OT_op op -> to_string op diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 6913371caf..be65ba5305 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -33,6 +33,24 @@ type t = | Int63lt | Int63le | Int63compare + | Float64opp + | Float64abs + | Float64eq + | Float64lt + | Float64le + | Float64compare + | Float64classify + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp + | Float64next_up + | Float64next_down val equal : t -> t -> bool @@ -53,18 +71,29 @@ 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 + | PT_float64 + +type 'a prim_ind = + | PIT_bool : unit prim_ind + | PIT_carry : prim_type prim_ind + | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_cmp : unit prim_ind + | PIT_f_cmp : unit prim_ind + | PIT_f_class : unit prim_ind + +type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex type op_or_type = | OT_op of t | OT_type of prim_type -val prim_ind_to_string : prim_ind -> string +val prim_ind_to_string : 'a prim_ind -> string val op_or_type_to_string : op_or_type -> string + +type ind_or_type = + | PITT_ind : 'a prim_ind * 'a -> ind_or_type + | PITT_type : prim_type -> ind_or_type + +val types : t -> ind_or_type list diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 83d2a58d83..13cc6f7ea4 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -528,6 +528,8 @@ let rec compile_lam env cenv lam sz cont = | Luint i -> compile_structured_constant cenv (Const_uint i) sz cont + | Lfloat f -> compile_structured_constant cenv (Const_float f) sz cont + | Lproj (p,arg) -> compile_lam env cenv arg sz (Kproj p :: cont) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 76e2515ea7..5e82cef810 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -234,6 +234,24 @@ let check_prim_op = function | Int63lt -> opCHECKLTINT63 | Int63le -> opCHECKLEINT63 | Int63compare -> opCHECKCOMPAREINT63 + | Float64opp -> opCHECKOPPFLOAT + | Float64abs -> opCHECKABSFLOAT + | Float64eq -> opCHECKEQFLOAT + | Float64lt -> opCHECKLTFLOAT + | Float64le -> opCHECKLEFLOAT + | Float64compare -> opCHECKCOMPAREFLOAT + | Float64classify -> opCHECKCLASSIFYFLOAT + | Float64add -> opCHECKADDFLOAT + | Float64sub -> opCHECKSUBFLOAT + | Float64mul -> opCHECKMULFLOAT + | Float64div -> opCHECKDIVFLOAT + | Float64sqrt -> opCHECKSQRTFLOAT + | Float64ofInt63 -> opCHECKFLOATOFINT63 + | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA + | Float64frshiftexp -> opCHECKFRSHIFTEXP + | Float64ldshiftexp -> opCHECKLDSHIFTEXP + | Float64next_up -> opCHECKNEXTUPFLOAT + | Float64next_down -> opCHECKNEXTDOWNFLOAT let emit_instr env = function | Klabel lbl -> define_label env lbl @@ -384,7 +402,8 @@ type to_patch = emitcodes * patches * fv (* Substitution *) let subst_strcst s sc = match sc with - | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _ -> sc + | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ | Const_uint _ + | Const_float _ -> 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/clambda.ml b/kernel/clambda.ml index a764cca354..8c7aa6b17a 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -28,6 +28,7 @@ type lambda = | Lint of int | Lmakeblock of int * lambda array | Luint of Uint63.t + | Lfloat of Float64.t | Lval of structured_values | Lsort of Sorts.t | Lind of pinductive @@ -143,6 +144,7 @@ let rec pp_lam lam = prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") | Luint i -> str (Uint63.to_string i) + | Lfloat f -> str (Float64.to_string f) | Lval _ -> str "values" | Lsort s -> pp_sort s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i @@ -195,7 +197,8 @@ let shift subst = subs_shft (1, subst) let map_lam_with_binders g f n lam = match lam with - | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ -> lam + | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ + | Lfloat _ -> lam | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') @@ -416,7 +419,8 @@ 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 _ | Luint _ -> kind + | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ | Luint _ + | Lfloat _ -> kind | Levar (_, args) -> occurrence_args k kind args | Lprod(dom, codom) -> @@ -763,6 +767,7 @@ let rec lambda_of_constr env c = Lproj (Projection.repr p,lc) | Int i -> Luint i + | Float f -> Lfloat f and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 1476bb6e45..bd11c2667f 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -21,6 +21,7 @@ type lambda = | Lint of int | Lmakeblock of int * lambda array | Luint of Uint63.t + | Lfloat of Float64.t | Lval of structured_values | Lsort of Sorts.t | Lind of pinductive diff --git a/kernel/constr.ml b/kernel/constr.ml index 8375316003..b60b2d6d04 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -104,6 +104,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr | Int of Uint63.t + | Float of Float64.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 @@ -241,6 +242,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with (* Constructs a primitive integer *) let mkInt i = Int i +(* Constructs a primitive float number *) +let mkFloat f = Float f + (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -446,7 +450,7 @@ let decompose_appvect c = let fold f acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> acc + | Construct _ | Int _ | Float _) -> 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 @@ -466,7 +470,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 _ | Int _) -> () + | Construct _ | Int _ | Float _) -> () | Cast (c,_,t) -> f c; f t | Prod (_,t,c) -> f t; f c | Lambda (_,t,c) -> f t; f c @@ -486,7 +490,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 _ | Int _) -> () + | Construct _ | Int _ | Float _) -> () | 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 @@ -512,7 +516,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 _ | Int _) -> acc + | Construct _ | Int _ | Float _) -> 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 @@ -608,7 +612,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 _ | Int _) -> c + | Construct _ | Int _ | Float _) -> c | Cast (b,k,t) -> let b' = f b in let t' = f t in @@ -673,7 +677,7 @@ let map = map_gen false let fold_map f accu c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> accu, c + | Construct _ | Int _ | Float _) -> accu, c | Cast (b,k,t) -> let accu, b' = f accu b in let accu, t' = f accu t in @@ -733,7 +737,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 _ | Int _) -> c0 + | Construct _ | Int _ | Float _) -> c0 | Cast (c, k, t) -> let c' = f l c in let t' = f l t in @@ -810,7 +814,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 _ | Int _ -> acc + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> 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 @@ -852,6 +856,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Int i1, Int i2 -> Uint63.equal i1 i2 + | Float f1, Float f2 -> Float64.equal f1 f2 | 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 @@ -878,7 +883,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 _ | Int _), _ -> false + | CoFix _ | Int _ | Float _), _ -> 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, @@ -1055,6 +1060,8 @@ let constr_ord_int f t1 t2 = | 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 + | Int _, _ -> -1 | _, Int _ -> 1 + | Float f1, Float f2 -> Float64.total_compare f1 f2 let rec compare m n= constr_ord_int compare m n @@ -1139,9 +1146,10 @@ let hasheq t1 t2 = && array_eqeq tl1 tl2 && array_eqeq bl1 bl2 | Int i1, Int i2 -> i1 == i2 + | Float f1, Float f2 -> Float64.equal f1 f2 | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ - | Fix _ | CoFix _ | Int _), _ -> false + | Fix _ | CoFix _ | Int _ | Float _), _ -> 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 *) @@ -1247,6 +1255,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Int i -> let (h,l) = Uint63.to_int2 i in (t, combinesmall 18 (combine h l)) + | Float f -> (t, combinesmall 19 (Float64.hash f)) and sh_rec t = let (y, h) = hash_term t in @@ -1311,6 +1320,7 @@ let rec hash t = | Proj (p,c) -> combinesmall 17 (combine (Projection.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) + | Float f -> combinesmall 19 (Float64.hash f) and hash_term_array t = Array.fold_left (fun acc t -> combine (hash t) acc) 0 t @@ -1455,3 +1465,4 @@ let rec debug_print c = cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++ str"}") | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" + | Float i -> str"Float("++str (Float64.to_string i) ++ str")" diff --git a/kernel/constr.mli b/kernel/constr.mli index 45ec8a7e64..4f8d682e42 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -76,6 +76,9 @@ val mkVar : Id.t -> constr (** Constructs a machine integer *) val mkInt : Uint63.t -> constr +(** Constructs a machine float number *) +val mkFloat : Float64.t -> constr + (** Constructs an patvar named "?n" *) val mkMeta : metavariable -> constr @@ -234,6 +237,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr | Int of Uint63.t + | Float of Float64.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 0951b07d49..fae06f7163 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -161,7 +161,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Id.Set.t option; } let expmod_constr_subst cache modlist subst c = @@ -239,14 +239,10 @@ let cook_constant { from = cb; info } = | Undef _ as x -> x | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque info o) + OpaqueDef (Opaqueproof.discharge_opaque info o) | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in - let const_hyps = - Context.Named.fold_outside (fun decl hyps -> - List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) - hyps) - hyps0 ~init:cb.const_hyps in + let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in let typ = abstract_constant_type (expmod cb.const_type) hyps in { cook_body = body; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 671cdf51fe..83a8b9edfc 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Names.Id.Set.t option; } val cook_constant : recipe -> Opaqueproof.opaque result diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 6c9e73b50d..cbffdc731e 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -184,7 +184,16 @@ and eval_to_patch env (buff,pl,fv) = | Reloc_proj_name p -> slot_for_proj_name p in let tc = patch buff pl slots in - let vm_env = Array.map (slot_for_fv env) fv in + let vm_env = + (* Beware, this may look like a call to [Array.map], but it's not. + Calling [Array.map f] when the first argument returned by [f] + is a float would lead to [vm_env] being an unboxed Double_array + (Tag_val = Double_array_tag) whereas eval_tcode expects a + regular array (Tag_val = 0). + See test-suite/primitive/float/coq_env_double_array.v + for an actual instance. *) + let a = Array.make (Array.length fv) crazy_val in + Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env and val_of_constr env c = diff --git a/kernel/declarations.ml b/kernel/declarations.ml index dff19dee5e..44676c9da5 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -66,6 +66,10 @@ type typing_flags = { (** If [false] then fixed points and co-fixed points are assumed to be total. *) + check_positive : bool; + (** If [false] then inductive types are assumed positive and co-inductive + types are assumed productive. *) + check_universes : bool; (** If [false] universe constraints are not checked *) @@ -83,6 +87,11 @@ type typing_flags = { indices_matter: bool; (** The universe of an inductive type must be above that of its indices. *) + + check_template : bool; + (* If [false] then we don't check that the universes template-polymorphic + inductive parameterize on are necessarily local and unbounded from below. + This potentially introduces inconsistencies. *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 7a553700e8..7225671a1e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -19,12 +19,14 @@ module RelDecl = Context.Rel.Declaration let safe_flags oracle = { check_guarded = true; + check_positive = true; check_universes = true; conv_oracle = oracle; share_reduction = true; enable_VM = true; enable_native_compiler = true; indices_matter = true; + check_template = true; } (** {6 Arities } *) diff --git a/kernel/dune b/kernel/dune index 4038bf5638..5f7502ef6b 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_31 uint63_63)) (libraries lib byterun dynlink)) (executable @@ -16,7 +16,7 @@ (rule (targets uint63.ml) - (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (deps (:gen-file uint63_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) (documentation diff --git a/kernel/entries.ml b/kernel/entries.ml index 47e2f72b0e..046ea86872 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -61,7 +61,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; (* List of section variables *) - const_entry_secctx : Constr.named_context option; + const_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -70,7 +70,7 @@ type definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Constr.named_context option; + secdef_secctx : Id.Set.t option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -78,7 +78,7 @@ type section_def_entry = { type 'a opaque_entry = { opaque_entry_body : 'a; (* List of section variables *) - opaque_entry_secctx : Constr.named_context; + opaque_entry_secctx : Id.Set.t; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; @@ -88,7 +88,7 @@ type 'a opaque_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Constr.named_context option * types in_universes_entry * inline + Id.Set.t option * types in_universes_entry * inline type primitive_entry = { prim_entry_type : types option; @@ -99,14 +99,10 @@ type primitive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -(** Dummy wrapper type discriminable from unit *) -type 'a seff_wrap = { seff_wrap : 'a } - -type _ constant_entry = - | DefinitionEntry : definition_entry -> unit constant_entry - | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry - | ParameterEntry : parameter_entry -> unit constant_entry - | PrimitiveEntry : primitive_entry -> unit constant_entry +type constant_entry = + | DefinitionEntry : definition_entry -> constant_entry + | ParameterEntry : parameter_entry -> constant_entry + | PrimitiveEntry : primitive_entry -> constant_entry (** {6 Modules } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 9a75f0b682..2bee2f7a8e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -50,17 +50,25 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; -} +module Globals = struct + + type view = + { constants : constant_key Cmap_env.t + ; inductives : mind_key Mindmap_env.t + ; modules : module_body MPmap.t + ; modtypes : module_type_body MPmap.t + } + + type t = view + + let view x = x +end type stratification = { env_universes : UGraph.t; - env_engagement : engagement; env_sprop_allowed : bool; + env_universes_lbound : Univ.Level.t; + env_engagement : engagement } type val_kind = @@ -87,7 +95,7 @@ type rel_context_val = { } type env = { - env_globals : globals; + env_globals : Globals.t; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -109,19 +117,20 @@ let empty_rel_context_val = { } let empty_env = { - env_globals = { - env_constants = Cmap_env.empty; - env_inductives = Mindmap_env.empty; - env_modules = MPmap.empty; - env_modtypes = MPmap.empty}; + env_globals = + { Globals.constants = Cmap_env.empty + ; inductives = Mindmap_env.empty + ; modules = MPmap.empty + ; modtypes = MPmap.empty + }; env_named_context = empty_named_context_val; env_rel_context = empty_rel_context_val; env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet; env_sprop_allowed = false; - }; + env_universes_lbound = Univ.Level.set; + env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab; @@ -214,27 +223,34 @@ let lookup_named_ctxt id ctxt = fst (Id.Map.find id ctxt.env_named_map) let fold_constants f env acc = - Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.constants acc + +let fold_inductives f env acc = + Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.inductives acc (* Global constants *) let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.env_constants + Cmap_env.get kn env.env_globals.Globals.constants let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.env_constants) + fst (lookup_constant_key kn env) + +let mem_constant kn env = Cmap_env.mem kn env.env_globals.Globals.constants (* Mutual Inductives *) +let lookup_mind_key kn env = + Mindmap_env.get kn env.env_globals.Globals.inductives + let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.env_inductives) + fst (lookup_mind_key kn env) + +let mem_mind kn env = Mindmap_env.mem kn env.env_globals.Globals.inductives let mind_context env mind = let mib = lookup_mind mind env in Declareops.inductive_polymorphic_context mib -let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.env_inductives - let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in @@ -259,8 +275,15 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let indices_matter env = env.env_typing_flags.indices_matter +let check_template env = env.env_typing_flags.check_template let universes env = env.env_stratification.env_universes +let universes_lbound env = env.env_stratification.env_universes_lbound + +let set_universes_lbound env lbound = + let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in + { env with env_stratification } + let named_context env = env.env_named_context.env_named_ctx let named_context_val env = env.env_named_context let rel_context env = env.env_rel_context.env_rel_ctx @@ -379,29 +402,30 @@ let check_constraints c env = let push_constraints_to_env (_,univs) env = add_constraints univs env -let add_universes strict ctx g = +let add_universes ~lbound ~strict ctx g = let g = Array.fold_left - (fun g v -> UGraph.add_universe v strict g) + (fun g v -> UGraph.add_universe ~lbound ~strict v g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = - map_universes (add_universes strict ctx) env + map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env -let add_universes_set strict ctx g = +let add_universes_set ~lbound ~strict ctx g = let g = Univ.LSet.fold (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = - map_universes (add_universes_set strict ctx) env + map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env let push_subgraph (levels,csts) env = + let lbound = universes_lbound env in let add_subgraph g = - let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in + let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in let newg = UGraph.merge_constraints csts newg in (if not (Univ.Constraint.is_empty csts) then let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in @@ -418,20 +442,24 @@ let set_engagement c env = (* Unsafe *) (* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *) let same_flags { check_guarded; + check_positive; check_universes; conv_oracle; indices_matter; share_reduction; enable_VM; enable_native_compiler; + check_template; } alt = check_guarded == alt.check_guarded && + check_positive == alt.check_positive && check_universes == alt.check_universes && conv_oracle == alt.conv_oracle && indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler + enable_native_compiler == alt.enable_native_compiler && + check_template == alt.check_template [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -452,10 +480,10 @@ let no_link_info = NotLinked let add_constant_key kn cb linkinfo env = let new_constants = - Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in + Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.Globals.constants in let new_globals = { env.env_globals with - env_constants = new_constants } in + Globals.constants = new_constants } in { env with env_globals = new_globals } let add_constant kn cb env = @@ -563,20 +591,29 @@ let polymorphic_pind (ind,u) env = let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes +let template_checked_ind (mind,_i) env = + (lookup_mind mind env).mind_typing_flags.check_template + let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true | RegularArity _ -> false +let template_polymorphic_variables (mind,i) env = + match (lookup_mind mind env).mind_packets.(i).mind_arity with + | TemplateArity { Declarations.template_param_levels = l; _ } -> + List.map_filter (fun level -> level) l + | RegularArity _ -> [] + let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env let add_mind_key kn (_mind, _ as mind_key) env = - let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_inds = Mindmap_env.add kn mind_key env.env_globals.Globals.inductives in let new_globals = { env.env_globals with - env_inductives = new_inds; } in + Globals.inductives = new_inds; } in { env with env_globals = new_globals } let add_mind kn mib env = @@ -663,22 +700,22 @@ let keep_hyps env needed = let add_modtype mtb env = let mp = mtb.mod_mp in - let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in - let new_globals = { env.env_globals with env_modtypes = new_modtypes } in + let new_modtypes = MPmap.add mp mtb env.env_globals.Globals.modtypes in + let new_globals = { env.env_globals with Globals.modtypes = new_modtypes } in { env with env_globals = new_globals } let shallow_add_module mb env = let mp = mb.mod_mp in - let new_mods = MPmap.add mp mb env.env_globals.env_modules in - let new_globals = { env.env_globals with env_modules = new_mods } in + let new_mods = MPmap.add mp mb env.env_globals.Globals.modules in + let new_globals = { env.env_globals with Globals.modules = new_mods } in { env with env_globals = new_globals } let lookup_module mp env = - MPmap.find mp env.env_globals.env_modules + MPmap.find mp env.env_globals.Globals.modules -let lookup_modtype mp env = - MPmap.find mp env.env_globals.env_modtypes +let lookup_modtype mp env = + MPmap.find mp env.env_globals.Globals.modtypes (*s Judgments. *) @@ -757,6 +794,22 @@ let is_template_polymorphic env r = | IndRef ind -> template_polymorphic_ind ind env | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env +let get_template_polymorphic_variables env r = + let open Names.GlobRef in + match r with + | VarRef _id -> [] + | ConstRef _c -> [] + | IndRef ind -> template_polymorphic_variables ind env + | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env + +let is_template_checked env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef _c -> false + | IndRef ind -> template_checked_ind ind env + | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env + let is_type_in_type env r = let open Names.GlobRef in match r with diff --git a/kernel/environ.mli b/kernel/environ.mli index 6cd4f96645..782ea1c666 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,13 +46,24 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals -(** globals = constants + projections + inductive types + modules + module-types *) +module Globals : sig + type t + + type view = + { constants : constant_key Cmap_env.t + ; inductives : mind_key Mindmap_env.t + ; modules : module_body MPmap.t + ; modtypes : module_type_body MPmap.t + } + + val view : t -> view +end type stratification = { env_universes : UGraph.t; - env_engagement : engagement; env_sprop_allowed : bool; + env_universes_lbound : Univ.Level.t; + env_engagement : engagement } type named_context_val = private { @@ -66,7 +77,7 @@ type rel_context_val = private { } type env = private { - env_globals : globals; + env_globals : Globals.t; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -85,6 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t +val universes_lbound : env -> Univ.Level.t +val set_universes_lbound : env -> Univ.Level.t -> env val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val @@ -99,6 +112,7 @@ val is_impredicative_set : env -> bool val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool +val check_template : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool @@ -176,6 +190,7 @@ val pop_rel_context : int -> env -> env (** Useful for printing *) val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a +val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a (** {5 Global constants } {6 Add entries to global environment } *) @@ -186,10 +201,12 @@ val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_in val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_constant : Constant.t -> env -> Opaqueproof.opaque constant_body val evaluable_constant : Constant.t -> env -> bool +val mem_constant : Constant.t -> env -> bool + (** New-style polymorphism *) val polymorphic_constant : Constant.t -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool @@ -200,7 +217,7 @@ val type_in_type_constant : Constant.t -> env -> bool [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] *) + and an anomaly if it does not exist in [env] *) type const_evaluation_result = | NoBody @@ -239,9 +256,11 @@ val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_mind : MutInd.t -> env -> mutual_inductive_body +val mem_mind : MutInd.t -> env -> bool + (** The universe context associated to the inductive, empty if not polymorphic *) val mind_context : env -> MutInd.t -> Univ.AUContext.t @@ -253,7 +272,9 @@ val type_in_type_ind : inductive -> env -> bool (** Old-style polymorphism *) val template_polymorphic_ind : inductive -> env -> bool +val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool +val template_checked_ind : inductive -> env -> bool (** {5 Modules } *) @@ -345,6 +366,8 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool +val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list +val is_template_checked : env -> GlobRef.t -> bool val is_type_in_type : env -> GlobRef.t -> bool (** Native compiler *) diff --git a/kernel/float64.ml b/kernel/float64.ml new file mode 100644 index 0000000000..3e36373b77 --- /dev/null +++ b/kernel/float64.ml @@ -0,0 +1,159 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(* OCaml's float type follows the IEEE 754 Binary64 (double precision) + format *) +type t = float + +let is_nan f = f <> f +let is_infinity f = f = infinity +let is_neg_infinity f = f = neg_infinity + +(* Printing a binary64 float in 17 decimal places and parsing it again + will yield the same float. We assume [to_string_raw] is not given a + [nan] as input. *) +let to_string_raw f = Printf.sprintf "%.17g" f + +(* OCaml gives a sign to nan values which should not be displayed as + all NaNs are considered equal here *) +let to_string f = if is_nan f then "nan" else to_string_raw f +let of_string = float_of_string + +(* Compiles a float to OCaml code *) +let compile f = + let s = + if is_nan f then "nan" else if is_neg_infinity f then "neg_infinity" + else Printf.sprintf "%h" f in + Printf.sprintf "Float64.of_float (%s)" s + +let of_float f = f + +let sign f = copysign 1. f < 0. + +let opp = ( ~-. ) +let abs = abs_float + +type float_comparison = FEq | FLt | FGt | FNotComparable + +let eq x y = x = y +[@@ocaml.inline always] + +let lt x y = x < y +[@@ocaml.inline always] + +let le x y = x <= y +[@@ocaml.inline always] + +(* inspired by lib/util.ml; see also #10471 *) +let pervasives_compare = compare + +let compare x y = + if x < y then FLt + else + ( + if x > y then FGt + else + ( + if x = y then FEq + else FNotComparable (* NaN case *) + ) + ) +[@@ocaml.inline always] + +type float_class = + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN + +let classify x = + match classify_float x with + | FP_normal -> if 0. < x then PNormal else NNormal + | FP_subnormal -> if 0. < x then PSubn else NSubn + | FP_zero -> if 0. < 1. /. x then PZero else NZero + | FP_infinite -> if 0. < x then PInf else NInf + | FP_nan -> NaN +[@@ocaml.inline always] + +external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul" +[@@unboxed] [@@noalloc] + +external add : float -> float -> float = "coq_fadd_byte" "coq_fadd" +[@@unboxed] [@@noalloc] + +external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub" +[@@unboxed] [@@noalloc] + +external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv" +[@@unboxed] [@@noalloc] + +external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt" +[@@unboxed] [@@noalloc] + +let of_int63 x = Uint63.to_float x +[@@ocaml.inline always] + +let prec = 53 +let normfr_mantissa f = + let f = abs f in + if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec) + else Uint63.zero +[@@ocaml.inline always] + +let eshift = 2101 (* 2*emax + prec *) + +(* When calling frexp on a nan or an infinity, the returned value inside + the exponent is undefined. + Therefore we must always set it to a fixed value (here 0). *) +let frshiftexp f = + match classify_float f with + | FP_zero | FP_infinite | FP_nan -> (f, Uint63.zero) + | FP_normal | FP_subnormal -> + let (m, e) = frexp f in + m, Uint63.of_int (e + eshift) +[@@ocaml.inline always] + +let ldshiftexp f e = ldexp f (Uint63.to_int_min e (2 * eshift) - eshift) +[@@ocaml.inline always] + +external next_up : float -> float = "coq_next_up_byte" "coq_next_up" +[@@unboxed] [@@noalloc] + +external next_down : float -> float = "coq_next_down_byte" "coq_next_down" +[@@unboxed] [@@noalloc] + +let equal f1 f2 = + match classify_float f1 with + | FP_normal | FP_subnormal | FP_infinite -> (f1 = f2) + | FP_nan -> is_nan f2 + | FP_zero -> f1 = f2 && 1. /. f1 = 1. /. f2 (* OCaml consider 0. = -0. *) +[@@ocaml.inline always] + +let hash = + (* Hashtbl.hash already considers all NaNs as equal, + cf. https://github.com/ocaml/ocaml/commit/aea227fdebe0b5361fd3e1d0aaa42cf929052269 + and http://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.html *) + Hashtbl.hash + +let total_compare f1 f2 = + (* pervasives_compare considers all NaNs as equal, which is fine here, + but also considers -0. and +0. as equal *) + if f1 = 0. && f2 = 0. then pervasives_compare (1. /. f1) (1. /. f2) + else pervasives_compare f1 f2 + +let is_float64 t = + Obj.tag t = Obj.double_tag +[@@ocaml.inline always] + +(*** Test at runtime that no harmful double rounding seems to + be performed with an intermediate 80 bits representation (x87). *) +let () = + let b = ldexp 1. 53 in + let s = add 1. (ldexp 1. (-52)) in + if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then + failwith "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." diff --git a/kernel/float64.mli b/kernel/float64.mli new file mode 100644 index 0000000000..2aa9796526 --- /dev/null +++ b/kernel/float64.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** [t] is currently implemented by OCaml's [float] type. + +Beware: NaNs have a sign and a payload, while they should be +indistinguishable from Coq's perspective. *) +type t + +(** Test functions for special values to avoid calling [classify] *) +val is_nan : t -> bool +val is_infinity : t -> bool +val is_neg_infinity : t -> bool + +val to_string : t -> string +val of_string : string -> t + +val compile : t -> string + +val of_float : float -> t + +(** Return [true] for "-", [false] for "+". *) +val sign : t -> bool + +val opp : t -> t +val abs : t -> t + +type float_comparison = FEq | FLt | FGt | FNotComparable + +val eq : t -> t -> bool + +val lt : t -> t -> bool + +val le : t -> t -> bool + +(** The IEEE 754 float comparison. + * NotComparable is returned if there is a NaN in the arguments *) +val compare : t -> t -> float_comparison +[@@ocaml.inline always] + +type float_class = + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN + +val classify : t -> float_class +[@@ocaml.inline always] + +val mul : t -> t -> t + +val add : t -> t -> t + +val sub : t -> t -> t + +val div : t -> t -> t + +val sqrt : t -> t + +(** Link with integers *) +val of_int63 : Uint63.t -> t +[@@ocaml.inline always] + +val normfr_mantissa : t -> Uint63.t +[@@ocaml.inline always] + +(** Shifted exponent extraction *) +val eshift : int + +val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) +[@@ocaml.inline always] + +val ldshiftexp : t -> Uint63.t -> t +[@@ocaml.inline always] + +val next_up : t -> t + +val next_down : t -> t + +(** Return true if two floats are equal. + * All NaN values are considered equal. *) +val equal : t -> t -> bool +[@@ocaml.inline always] + +val hash : t -> int + +(** Total order relation over float values. Behaves like [Pervasives.compare].*) +val total_compare : t -> t -> int + +val is_float64 : Obj.t -> bool +[@@ocaml.inline always] diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index a8a4ffce9c..82bb2b584d 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -137,6 +137,26 @@ let opcodes = "CHECKTAIL0INT63"; "ISINT"; "AREINT2"; + "CHECKOPPFLOAT"; + "CHECKABSFLOAT"; + "CHECKEQFLOAT"; + "CHECKLTFLOAT"; + "LTFLOAT"; + "CHECKLEFLOAT"; + "LEFLOAT"; + "CHECKCOMPAREFLOAT"; + "CHECKCLASSIFYFLOAT"; + "CHECKADDFLOAT"; + "CHECKSUBFLOAT"; + "CHECKMULFLOAT"; + "CHECKDIVFLOAT"; + "CHECKSQRTFLOAT"; + "CHECKFLOATOFINT63"; + "CHECKFLOATNORMFRMANTISSA"; + "CHECKFRSHIFTEXP"; + "CHECKLDSHIFTEXP"; + "CHECKNEXTUPFLOAT"; + "CHECKNEXTDOWNFLOAT"; "STOP" |] diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index c8e04b9fee..06d2e1bb21 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} if not ind_squashed then InType else Sorts.family (Sorts.sort_of_univ ind_univ) +(* For a level to be template polymorphic, it must be introduced + by the definition (so have no constraint except lbound <= l) + and not to be constrained from below, so any universe l' <= l + can be used as an instance of l. All bounds from above, i.e. + l <=/< r will be valid for any l' <= l. *) +let unbounded_from_below u cstrs = + Univ.Constraint.for_all (fun (l, d, r) -> + match d with + | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u) + | Lt | Le -> not (Univ.Level.equal r u)) + cstrs + (* Returns the list [x_1, ..., x_n] of levels contributing to template - polymorphism. The elements x_k is None if the k-th parameter (starting - from the most recent and ignoring let-definitions) is not contributing - or is Some u_k if its level is u_k and is contributing. *) -let param_ccls paramsctxt = + polymorphism. The elements x_k is None if the k-th parameter + (starting from the most recent and ignoring let-definitions) is not + contributing to the inductive type's sort or is Some u_k if its level + is u_k and is contributing. *) +let template_polymorphic_univs ~template_check uctx paramsctxt concl = + let check_level l = + if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + unbounded_from_below l (Univ.ContextSet.constraints uctx) then + Some l + else None + in + let univs = Univ.Universe.levels concl in + let univs = + if template_check then + Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs + else univs (* Doesn't check the universes can be generalized *) + in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with - | Sort (Type u) -> Univ.Universe.level u + | Sort (Type u) -> + if template_check then + (match Univ.Universe.level u with + | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None + | None -> None) + else Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in - List.fold_left fold [] paramsctxt + let params = List.fold_left fold [] paramsctxt in + params, univs -let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = let arity = Vars.subst_univs_level_constr usubst arity in let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in let indices = Vars.subst_univs_level_context usubst indices in @@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in let arity = match univ_info.ind_min_univ with - | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ} + | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ} | Some min_univ -> - ((match univs with - | Monomorphic _ -> () + let ctx = match univs with + | Monomorphic ctx -> ctx | Polymorphic _ -> CErrors.anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.")); - TemplateArity {template_param_levels=param_ccls params; template_level=min_univ}) + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in + let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in + if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + && Univ.LSet.is_empty concl_levels then + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") + else + TemplateArity {template_param_levels = param_levels; template_level = min_univ} in let kelim = allowed_sorts univ_info in @@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); + let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + (* universes *) let env_univs = match mie.mind_entry_universes with - | Monomorphic_entry ctx -> push_context_set ctx env + | Monomorphic_entry ctx -> + let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in + push_context_set ctx env | Polymorphic_entry (_, ctx) -> push_context ctx env in @@ -335,7 +376,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let data = List.map (abstract_packets univs usubst params) data in + let template_check = Environ.check_template env in + let data = List.map (abstract_packets ~template_check univs usubst params) data in let env_ar_par = let ctx = Environ.rel_context env_ar_par in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index aaa0d6a149..8da4e2885c 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry -> (Constr.rel_context * (Constr.rel_context * Constr.types) array) * Sorts.family) array + +(* Utility function to compute the actual universe parameters + of a template polymorphic inductive *) +val template_polymorphic_univs : + template_check:bool -> + Univ.ContextSet.t -> + Constr.rel_context -> + Univ.Universe.t -> + Univ.Level.t option list * Univ.LSet.t diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b0366d6ec0..aa3ef715db 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -546,7 +546,7 @@ let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) - let chkpos = (Environ.typing_flags env).check_guarded in + let chkpos = (Environ.typing_flags env).check_positive in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) mie.mind_entry_inds in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cd969ea457..320bc6a1cd 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -812,7 +812,7 @@ let rec subterm_specif renv stack t = | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ - | Construct _ | CoFix _ | Int _ -> Not_subterm + | Construct _ | CoFix _ | Int _ | Float _ -> Not_subterm (* Other terms are not subterms *) @@ -1057,7 +1057,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(c,l)) end - | Sort _ | Int _ -> + | Sort _ | Int _ | Float _ -> assert (List.is_empty l) (* l is not checked because it is considered as the meta's context *) @@ -1254,7 +1254,7 @@ 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 _ | Int _ -> + | Ind _ | Fix _ | Proj _ | Int _ | Float _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml new file mode 100644 index 0000000000..550c81ed82 --- /dev/null +++ b/kernel/inferCumulativity.ml @@ -0,0 +1,234 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 Reduction +open Declarations +open Constr +open Univ +open Variance +open Util + +type inferred = IrrelevantI | CovariantI + +(** Throughout this module we modify a map [variances] from local + universes to [inferred]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. + [Invariant] universes are removed from the map. +*) +exception TrivialVariance + +let maybe_trivial variances = + if LMap.is_empty variances then raise TrivialVariance + else variances + +let infer_level_eq u variances = + maybe_trivial (LMap.remove u variances) + +let infer_level_leq u variances = + (* can only set Irrelevant -> Covariant so nontrivial *) + LMap.update u (function + | None -> None + | Some CovariantI as x -> x + | Some IrrelevantI -> Some CovariantI) + variances + +let infer_generic_instance_eq variances u = + Array.fold_left (fun variances u -> infer_level_eq u variances) + variances (Instance.to_array u) + +let infer_cumulative_ind_instance cv_pb mind_variance variances u = + Array.fold_left2 (fun variances varu u -> + match cv_pb, varu with + | _, Irrelevant -> variances + | _, Invariant | CONV, Covariant -> infer_level_eq u variances + | CUMUL, Covariant -> infer_level_leq u variances) + variances mind_variance (Instance.to_array u) + +let infer_inductive_instance cv_pb env variances ind nargs u = + let mind = Environ.lookup_mind (fst ind) env in + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some mind_variance -> + if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance cv_pb mind_variance variances u + +let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = + let mind = Environ.lookup_mind mi env in + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some _ -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else variances (* constructors are convertible at common supertype *) + +let infer_sort cv_pb variances s = + match cv_pb with + | CONV -> + LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances + | CUMUL -> + LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances + +let infer_table_key variances c = + let open Names in + match c with + | ConstKey (_, u) -> + infer_generic_instance_eq variances u + | VarKey _ | RelKey _ -> variances + +let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk + +let rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let hd,stk = whd_stack infos hd stk in + let open CClosure in + match fterm_of hd with + | FAtom a -> + begin match kind a with + | Sort s -> infer_sort cv_pb variances s + | Meta _ -> infer_stack infos variances stk + | _ -> assert false + end + | FEvar ((_,args),e) -> + let variances = infer_stack infos variances stk in + infer_vect infos variances (Array.map (mk_clos e) args) + | FRel _ -> infer_stack infos variances stk + | FInt _ -> infer_stack infos variances stk + | FFloat _ -> infer_stack infos variances stk + | FFlex fl -> + let variances = infer_table_key variances fl in + infer_stack infos variances stk + | FProj (_,c) -> + let variances = infer_fterm CONV infos variances c [] in + infer_stack infos variances stk + | FLambda _ -> + let (_,ty,bd) = destFLambda mk_clos hd in + let variances = infer_fterm CONV infos variances ty [] in + infer_fterm CONV infos variances bd [] + | FProd (_,dom,codom,e) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) [] + | FInd (ind, u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u + in + infer_stack infos variances stk + | FConstruct (ctor,u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u + in + infer_stack infos variances stk + | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> + let n = Array.length cl in + let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in + let le = Esubst.subs_liftn n e in + let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in + infer_stack infos variances stk + + (* Removed by whnf *) + | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false + +and infer_stack infos variances (stk:CClosure.stack) = + match stk with + | [] -> variances + | z :: stk -> + let open CClosure in + let variances = match z with + | Zapp v -> infer_vect infos variances v + | Zproj _ -> variances + | Zfix (fx,a) -> + let variances = infer_fterm CONV infos variances fx [] in + infer_stack infos variances a + | ZcaseT (_, p, br, e) -> + let variances = infer_fterm CONV infos variances (mk_clos e p) [] in + infer_vect infos variances (Array.map (mk_clos e) br) + | Zshift _ -> variances + | Zupdate _ -> variances + | Zprimitive (_,_,rargs,kargs) -> + let variances = List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances rargs in + let variances = List.fold_left (fun variances (_,c) -> infer_fterm CONV infos variances c []) variances kargs in + variances + in + infer_stack infos variances stk + +and infer_vect infos variances v = + Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + +let infer_term cv_pb env variances c = + let open CClosure in + let infos = (create_clos_infos all env, create_tab ()) in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor is_arity env variances arcn = + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, infer_term CUMUL env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let typs, codom = Reduction.dest_prod env arcn in + let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) + if not is_arity then infer_term CUMUL env variances codom else variances + +open Entries + +let infer_inductive_core env params entries uctx = + let uarray = Instance.to_array @@ UContext.instance uctx in + if Array.is_empty uarray then raise TrivialVariance; + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) + LMap.empty uarray + in + let env, _ = Typeops.check_context env params in + let variances = List.fold_left (fun variances entry -> + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity + in + List.fold_left (infer_arity_constructor false env) + variances entry.mind_entry_lc) + variances + entries + in + Array.map (fun u -> match LMap.find u variances with + | exception Not_found -> Invariant + | IrrelevantI -> Irrelevant + | CovariantI -> Covariant) + uarray + +let infer_inductive env mie = + let open Entries in + let params = mie.mind_entry_params in + let entries = mie.mind_entry_inds in + let variances = + match mie.mind_entry_variance with + | None -> None + | Some _ -> + let uctx = match mie.mind_entry_universes with + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> uctx + in + try Some (infer_inductive_core env params entries uctx) + with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) + in + { mie with mind_entry_variance = variances } + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli new file mode 100644 index 0000000000..a234e334d1 --- /dev/null +++ b/kernel/inferCumulativity.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry + +val dummy_variance : Entries.universes_entry -> Univ.Variance.t array diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 59c1d5890f..2b83c2d868 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,6 +1,7 @@ Names TransparentState Uint63 +Float64 CPrimitives Univ UGraph @@ -43,9 +44,11 @@ Inductive Typeops IndTyping Indtypes +InferCumulativity Cooking Term_typing Subtyping Mod_typing Nativelibrary +Section Safe_typing diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 9305a91731..ccc218771a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = c', Monomorphic Univ.ContextSet.empty, cst | Polymorphic uctx, Some ctx -> let () = - if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then + if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env) + (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab in (** Terms are compared in a context with De Bruijn universe indices *) diff --git a/kernel/names.ml b/kernel/names.ml index 9802d4f531..b755ff0e08 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -675,6 +675,7 @@ module InductiveOrdered_env = struct end module Indset = Set.Make(InductiveOrdered) +module Indset_env = Set.Make(InductiveOrdered_env) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) @@ -688,6 +689,8 @@ module ConstructorOrdered_env = struct let compare = constructor_user_ord end +module Constrset = Set.Make(ConstructorOrdered) +module Constrset_env = Set.Make(ConstructorOrdered_env) module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 78eb9295d4..0c92a2f2bc 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -471,7 +471,7 @@ end module Mindset : CSig.SetS with type elt = MutInd.t module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset -module Mindmap_env : CSig.MapS with type key = MutInd.t +module Mindmap_env : CMap.ExtS with type key = MutInd.t (** Designation of a (particular) inductive type. *) type inductive = MutInd.t (* the name of the inductive type *) @@ -484,11 +484,14 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) -module Indset : CSig.SetS with type elt = inductive -module Indmap : CSig.MapS with type key = inductive -module Constrmap : CSig.MapS with type key = constructor -module Indmap_env : CSig.MapS with type key = inductive -module Constrmap_env : CSig.MapS with type key = constructor +module Indset : CSet.S with type elt = inductive +module Constrset : CSet.S with type elt = constructor +module Indset_env : CSet.S with type elt = inductive +module Constrset_env : CSet.S with type elt = constructor +module Indmap : CMap.ExtS with type key = inductive and module Set := Indset +module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset +module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env +module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env val ind_modpath : inductive -> ModPath.t val constr_modpath : constructor -> ModPath.t diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 1a5455cf3a..63dc49ba57 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -258,16 +258,19 @@ type primitive = | Mk_var of Id.t | Mk_proj | Is_int + | Is_float | Cast_accu | Upd_cofix | Force_cofix | Mk_uint + | Mk_float | Mk_int | Mk_bool | Val_to_int | Mk_meta | Mk_evar | MLand + | MLnot | MLle | MLlt | MLinteq @@ -349,6 +352,9 @@ let primitive_hash = function | Mk_proj -> 36 | MLarrayget -> 37 | Mk_empty_instance -> 38 + | Mk_float -> 39 + | Is_float -> 40 + | MLnot -> 41 type mllambda = | MLlocal of lname @@ -365,6 +371,7 @@ type mllambda = (* prefix, inductive name, tag, arguments *) | MLint of int | MLuint of Uint63.t + | MLfloat of Float64.t | MLsetref of string * mllambda | MLsequence of mllambda * mllambda | MLarray of mllambda array @@ -436,6 +443,8 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = Int.equal i1 i2 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2 + | MLfloat f1, MLfloat f2 -> + Float64.equal f1 f2 | MLsetref (id1, ml1), MLsetref (id2, ml2) -> String.equal id1 id2 && eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 @@ -450,7 +459,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ | - MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false + MLfloat _ | MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 = let eq_def (_,args1,ml1) (_,args2,ml2) = @@ -535,6 +544,8 @@ let rec hash_mllambda gn n env t = combinesmall 15 (hash_mllambda_array gn n env 1 arr) | MLisaccu (s, ind, c) -> combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c))) + | MLfloat f -> + combinesmall 17 (Float64.hash f) and hash_mllambda_letrec gn n env init defs = let hash_def (_,args,ml) = @@ -568,7 +579,7 @@ let fv_lam l = match l with | MLlocal l -> if LNset.mem l bind then fv else LNset.add l fv - | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> fv + | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> fv | MLlam (ln,body) -> let bind = Array.fold_right LNset.add ln bind in aux body bind fv @@ -757,7 +768,7 @@ type env = env_named : (Id.t * mllambda) list ref; env_univ : lname option} -let empty_env univ () = +let empty_env univ = { env_rel = []; env_bound = 0; env_urel = ref []; @@ -958,25 +969,29 @@ type prim_aux = | PAprim of string * pconstant * CPrimitives.t * prim_aux array | PAml of mllambda -let add_check cond args = - let aux cond a = +let add_check cond targs args = + let aux cond t a = match a with | PAml(MLint _) -> cond | PAml ml -> (* FIXME: use explicit equality function *) - if List.mem ml cond then cond else ml::cond + if List.mem (t, ml) cond then cond else (t, ml)::cond | _ -> cond in - Array.fold_left aux cond args + Array.fold_left2 aux cond targs args let extract_prim ml_of l = let decl = ref [] in let cond = ref [] in + let type_args p = + let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in + Array.of_list (aux (CPrimitives.types p)) in let rec aux l = match l with | Lprim(prefix,kn,p,args) -> + let targs = type_args p in let args = Array.map aux args in - cond := add_check !cond args; + cond := add_check !cond targs args; PAprim(prefix,kn,p,args) | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l) | _ -> @@ -1010,15 +1025,35 @@ let compile_prim decl cond paux = let compile_cond cond paux = match cond with | [] -> opt_prim_aux paux - | [c1] -> + | [CPrimitives.(PITT_type PT_int63), c1] -> 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; 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 ci, cf = + let is_int = + function CPrimitives.(PITT_type PT_int63), _ -> true | _ -> false in + List.partition is_int cond in + let condi = + let cond = + List.fold_left + (fun ml (_, c) -> app_prim MLland [| ml; cast_to_int c|]) + (MLint 0) ci in + app_prim MLmagic [|cond|] in + let condf = match cf with + | [] -> MLint 0 + | [_, c1] -> app_prim Is_float [|c1|] + | (_, c1) :: condf -> + List.fold_left + (fun ml (_, c) -> app_prim MLand [| ml; app_prim Is_float [|c|]|]) + (app_prim Is_float [|c1|]) condf in + match ci, cf with + | [], [] -> opt_prim_aux paux + | _ :: _, [] -> + MLif(condi, naive_prim_aux paux, opt_prim_aux paux) + | [], _ :: _ -> + MLif(condf, opt_prim_aux paux, naive_prim_aux paux) + | _ :: _, _ :: _ -> + let cond = app_prim MLand [|condf; app_prim MLnot [|condi|]|] in + MLif(cond, opt_prim_aux paux, naive_prim_aux paux) in let add_decl decl body = List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in @@ -1095,14 +1130,14 @@ let ml_of_instance instance u = (* Remark: if we do not want to compile the predicate we should a least compute the fv, then store the lambda representation of the predicate (not the mllambda) *) - let env_p = empty_env env.env_univ () in + let env_p = empty_env env.env_univ in let pn = fresh_gpred l in let mlp = ml_of_lam env_p l p in let mlp = generalize_fv env_p mlp in let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in let pn = push_global_let pn mlp in (* Compilation of the case *) - let env_c = empty_env env.env_univ () in + let env_c = empty_env env.env_univ in let a_uid = fresh_lname Anonymous in let la_uid = MLlocal a_uid in (* compilation of branches *) @@ -1158,7 +1193,7 @@ let ml_of_instance instance u = start *) (* Compilation of type *) - let env_t = empty_env env.env_univ () in + let env_t = empty_env env.env_univ in let ml_t = Array.map (ml_of_lam env_t l) tt in let params_t = fv_params env_t in let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in @@ -1167,7 +1202,7 @@ let ml_of_instance instance u = let mk_type = MLapp(MLglobal gft, args_t) in (* Compilation of norm_i *) let ndef = Array.length ids in - let lf,env_n = push_rels (empty_env env.env_univ ()) ids in + let lf,env_n = push_rels (empty_env env.env_univ) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in let mk_let _envi (id,def) t = MLlet (id,def,t) in @@ -1224,7 +1259,7 @@ let ml_of_instance instance u = MLletrec(Array.mapi mkrec lf, lf_args.(start)) | Lcofix (start, (ids, tt, tb)) -> (* Compilation of type *) - let env_t = empty_env env.env_univ () in + let env_t = empty_env env.env_univ in let ml_t = Array.map (ml_of_lam env_t l) tt in let params_t = fv_params env_t in let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in @@ -1233,7 +1268,7 @@ let ml_of_instance instance u = let mk_type = MLapp(MLglobal gft, args_t) in (* Compilation of norm_i *) let ndef = Array.length ids in - let lf,env_n = push_rels (empty_env env.env_univ ()) ids in + let lf,env_n = push_rels (empty_env env.env_univ) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in let ml_of_fix i body = @@ -1297,6 +1332,7 @@ let ml_of_instance instance u = let args = Array.map (ml_of_lam env l) args in MLconstruct(prefix,cn,tag,args) | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) + | Lfloat f -> MLapp(MLprimitive Mk_float, [|MLfloat f|]) | Lval v -> let i = push_symbol (SymbValue v) in get_value_code i | Lsort s -> @@ -1314,7 +1350,7 @@ let ml_of_instance instance u = | Lforce -> MLglobal (Ginternal "Lazy.force") let mllambda_of_lambda univ auxdefs l t = - let env = empty_env univ () in + let env = empty_env univ in global_stack := auxdefs; let ml = ml_of_lam env l t in let fv_rel = !(env.env_urel) in @@ -1347,7 +1383,7 @@ let subst s l = let rec aux l = match l with | MLlocal id -> (try LNmap.find id s with Not_found -> l) - | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l + | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l | MLlam(params,body) -> MLlam(params, aux body) | MLletrec(defs,body) -> let arec (f,params,body) = (f,params,aux body) in @@ -1417,7 +1453,7 @@ let optimize gdef l = let rec optimize s l = match l with | MLlocal id -> (try LNmap.find id s with Not_found -> l) - | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l + | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l | MLlam(params,body) -> MLlam(params, optimize s body) | MLletrec(decls,body) -> @@ -1623,6 +1659,7 @@ let pp_mllam fmt l = (string_of_construct prefix ~constant:false ind tag) pp_cargs args | MLint i -> pp_int fmt i | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i) + | MLfloat f -> Format.fprintf fmt "(%s)" (Float64.compile f) | MLsetref (s, body) -> Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body | MLsequence(l1,l2) -> @@ -1739,16 +1776,19 @@ let pp_mllam fmt l = Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" | Is_int -> Format.fprintf fmt "is_int" + | Is_float -> Format.fprintf fmt "is_float" | Cast_accu -> Format.fprintf fmt "cast_accu" | Upd_cofix -> Format.fprintf fmt "upd_cofix" | Force_cofix -> Format.fprintf fmt "force_cofix" | Mk_uint -> Format.fprintf fmt "mk_uint" + | Mk_float -> Format.fprintf fmt "mk_float" | Mk_int -> Format.fprintf fmt "mk_int" | Mk_bool -> Format.fprintf fmt "mk_bool" | Val_to_int -> Format.fprintf fmt "val_to_int" | Mk_meta -> Format.fprintf fmt "mk_meta_accu" | Mk_evar -> Format.fprintf fmt "mk_evar_accu" | MLand -> Format.fprintf fmt "(&&)" + | MLnot -> Format.fprintf fmt "not" | MLle -> Format.fprintf fmt "(<=)" | MLlt -> Format.fprintf fmt "(<)" | MLinteq -> Format.fprintf fmt "(==)" diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index dd010e5cad..ef610ce7e9 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -35,6 +35,9 @@ let rec conv_val env pb lvl v1 v2 cu = if Int.equal i1 i2 then cu else raise NotConvertible | Vint64 i1, Vint64 i2 -> if Int64.equal i1 i2 then cu else raise NotConvertible + | Vfloat64 f1, Vfloat64 f2 -> + if Float64.(equal (of_float f1) (of_float f2)) then cu + else raise NotConvertible | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -48,7 +51,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 _, _ | Vint64 _, _ | Vblock _, _ -> raise NotConvertible + | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 70b3beb2dc..7a4e62cdfe 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -44,6 +44,7 @@ type lambda = (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) | Luint of Uint63.t + | Lfloat of Float64.t | Lval of Nativevalues.t | Lsort of Sorts.t | Lind of prefix * pinductive @@ -123,7 +124,7 @@ let get_const_prefix env c = let map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _ - | Llazy | Lforce | Lmeta _ | Lint _ -> lam + | Llazy | Lforce | Lmeta _ | Lint _ | Lfloat _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -331,7 +332,7 @@ and reduce_lapp substf lids body substa largs = let is_value lc = match lc with - | Lval _ | Lint _ | Luint _ -> true + | Lval _ | Lint _ | Luint _ | Lfloat _ -> true | _ -> false let get_value lc = @@ -339,6 +340,7 @@ let get_value lc = | Lval v -> v | Lint tag -> Nativevalues.mk_int tag | Luint i -> Nativevalues.mk_uint i + | Lfloat f -> Nativevalues.mk_float f | _ -> raise Not_found let make_args start _end = @@ -364,7 +366,12 @@ let makeblock env ind tag nparams arity args = if Int.equal arity 0 then Lint tag else if Array.for_all is_value args then - let args = Array.map get_value args in + let dummy_val = Obj.magic 0 in + let args = + (* Don't simplify this to Array.map, cf. the related comment in + function eval_to_patch, file kernel/csymtable.ml *) + let a = Array.make (Array.length args) dummy_val in + Array.iteri (fun i v -> a.(i) <- get_value v) args; a in Lval (Nativevalues.mk_block tag args) else let prefix = get_mind_prefix env (fst ind) in @@ -580,6 +587,8 @@ let rec lambda_of_constr cache env sigma c = | Int i -> Luint i + | Float f -> Lfloat f + and lambda_of_app cache env sigma f args = match kind f with | Const (_kn,_u as c) -> diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index f17339f84d..1d7bf5343a 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -38,6 +38,7 @@ type lambda = (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) | Luint of Uint63.t + | Lfloat of Float64.t | Lval of Nativevalues.t | Lsort of Sorts.t | Lind of prefix * pinductive diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index e54118c775..e4a8344eaf 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -96,14 +96,14 @@ let mk_accu (a : atom) : t = else let data = { data with acc_arg = x :: data.acc_arg } in let ans = Obj.repr (accumulate data) in - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in ans in let acc = { acc_atm = a; acc_arg = [] } in let ans = Obj.repr (accumulate acc) in (** FIXME: use another representation for accumulators, this causes naked pointers. *) - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in (Obj.obj ans : t) let get_accu (k : accumulator) = @@ -225,6 +225,9 @@ let mk_bool (b : bool) = (Obj.magic (not b) : t) let mk_uint (x : Uint63.t) = (Obj.magic x : t) [@@ocaml.inline always] +let mk_float (x : Float64.t) = (Obj.magic x : t) +[@@ocaml.inline always] + type block let block_size (b:block) = @@ -240,16 +243,19 @@ type kind_of_value = | Vfun of (t -> t) | Vconst of int | Vint64 of int64 + | Vfloat64 of float | 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) + else if Obj.tag o == Obj.double_tag then Vfloat64 (Obj.magic v) else let tag = Obj.tag o in if Int.equal tag accumulate_tag then Vaccu (Obj.magic v) else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) + else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v) else (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); @@ -261,6 +267,7 @@ let kind_of_value (v:t) = let is_int (x:t) = let o = Obj.repr x in Obj.is_int o || Int.equal (Obj.tag o) Obj.custom_tag +[@@ocaml.inline always] let val_to_int (x:t) = (Obj.magic x : int) [@@ocaml.inline always] @@ -508,6 +515,177 @@ let print x = flush stderr; x +(** Support for machine floating point values *) + +external is_float : t -> bool = "coq_is_double" +[@@noalloc] + +let to_float (x:t) = (Obj.magic x : Float64.t) +[@@ocaml.inline always] + +let no_check_fopp x = + mk_float (Float64.opp (to_float x)) +[@@ocaml.inline always] + +let fopp accu x = + if is_float x then no_check_fopp x + else accu x + +let no_check_fabs x = + mk_float (Float64.abs (to_float x)) +[@@ocaml.inline always] + +let fabs accu x = + if is_float x then no_check_fabs x + else accu x + +let no_check_feq x y = + mk_bool (Float64.eq (to_float x) (to_float y)) + +let feq accu x y = + if is_float x && is_float y then no_check_feq x y + else accu x y + +let no_check_flt x y = + mk_bool (Float64.lt (to_float x) (to_float y)) + +let flt accu x y = + if is_float x && is_float y then no_check_flt x y + else accu x y + +let no_check_fle x y = + mk_bool (Float64.le (to_float x) (to_float y)) + +let fle accu x y = + if is_float x && is_float y then no_check_fle x y + else accu x y + +type coq_fcmp = + | CFcmpAccu of t + | CFcmpEq + | CFcmpLt + | CFcmpGt + | CFcmpNotComparable + +let no_check_fcompare x y = + let c = Float64.compare (to_float x) (to_float y) in + (Obj.magic c:t) +[@@ocaml.inline always] + +let fcompare accu x y = + if is_float x && is_float y then no_check_fcompare x y + else accu x y + +type coq_fclass = + | CFclassAccu of t + | CFclassPNormal + | CFclassNNormal + | CFclassPSubn + | CFclassNSubn + | CFclassPZero + | CFclassNZero + | CFclassPInf + | CFclassNInf + | CFclassNaN + +let no_check_fclassify x = + let c = Float64.classify (to_float x) in + (Obj.magic c:t) +[@@ocaml.inline always] + +let fclassify accu x = + if is_float x then no_check_fclassify x + else accu x + +let no_check_fadd x y = + mk_float (Float64.add (to_float x) (to_float y)) +[@@ocaml.inline always] + +let fadd accu x y = + if is_float x && is_float y then no_check_fadd x y + else accu x y + +let no_check_fsub x y = + mk_float (Float64.sub (to_float x) (to_float y)) +[@@ocaml.inline always] + +let fsub accu x y = + if is_float x && is_float y then no_check_fsub x y + else accu x y + +let no_check_fmul x y = + mk_float (Float64.mul (to_float x) (to_float y)) +[@@ocaml.inline always] + +let fmul accu x y = + if is_float x && is_float y then no_check_fmul x y + else accu x y + +let no_check_fdiv x y = + mk_float (Float64.div (to_float x) (to_float y)) +[@@ocaml.inline always] + +let fdiv accu x y = + if is_float x && is_float y then no_check_fdiv x y + else accu x y + +let no_check_fsqrt x = + mk_float (Float64.sqrt (to_float x)) +[@@ocaml.inline always] + +let fsqrt accu x = + if is_float x then no_check_fsqrt x + else accu x + +let no_check_float_of_int x = + mk_float (Float64.of_int63 (to_uint x)) +[@@ocaml.inline always] + +let float_of_int accu x = + if is_int x then no_check_float_of_int x + else accu x + +let no_check_normfr_mantissa x = + mk_uint (Float64.normfr_mantissa (to_float x)) +[@@ocaml.inline always] + +let normfr_mantissa accu x = + if is_float x then no_check_normfr_mantissa x + else accu x + +let no_check_frshiftexp x = + let f, e = Float64.frshiftexp (to_float x) in + (Obj.magic (PPair(mk_float f, mk_uint e)):t) +[@@ocaml.inline always] + +let frshiftexp accu x = + if is_float x then no_check_frshiftexp x + else accu x + +let no_check_ldshiftexp x e = + mk_float (Float64.ldshiftexp (to_float x) (to_uint e)) +[@@ocaml.inline always] + +let ldshiftexp accu x e = + if is_float x && is_int e then no_check_ldshiftexp x e + else accu x e + +let no_check_next_up x = + mk_float (Float64.next_up (to_float x)) +[@@ocaml.inline always] + +let next_up accu x = + if is_float x then no_check_next_up x + else accu x + +let no_check_next_down x = + mk_float (Float64.next_down (to_float x)) +[@@ocaml.inline always] + +let next_down accu x = + if is_float x then no_check_next_down x + else accu 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) - diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index b54f437e73..815ef3e98e 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -102,6 +102,9 @@ val mk_int : int -> t val mk_uint : Uint63.t -> t [@@ocaml.inline always] +val mk_float : Float64.t -> t +[@@ocaml.inline always] + val napply : t -> t array -> t (* Functions over accumulators *) @@ -130,6 +133,7 @@ type kind_of_value = | Vfun of (t -> t) | Vconst of int | Vint64 of int64 + | Vfloat64 of float | Vblock of block val kind_of_value : t -> kind_of_value @@ -140,7 +144,9 @@ val str_decode : string -> 'a (** Support for machine integers *) val val_to_int : t -> int + val is_int : t -> bool +[@@ocaml.inline always] (* function with check *) val head0 : t -> t -> t @@ -247,3 +253,82 @@ val no_check_le : t -> t -> t [@@ocaml.inline always] val no_check_compare : t -> t -> t + +(** Support for machine floating point values *) + +val is_float : t -> bool +[@@ocaml.inline always] + +val fopp : t -> t -> t +val fabs : t -> t -> t +val feq : t -> t -> t -> t +val flt : t -> t -> t -> t +val fle : t -> t -> t -> t +val fcompare : t -> t -> t -> t +val fclassify : t -> t -> t +val fadd : t -> t -> t -> t +val fsub : t -> t -> t -> t +val fmul : t -> t -> t -> t +val fdiv : t -> t -> t -> t +val fsqrt : t -> t -> t +val float_of_int : t -> t -> t +val normfr_mantissa : t -> t -> t +val frshiftexp : t -> t -> t +val ldshiftexp : t -> t -> t -> t +val next_up : t -> t -> t +val next_down : t -> t -> t + +(* Function without check *) +val no_check_fopp : t -> t +[@@ocaml.inline always] + +val no_check_fabs : t -> t +[@@ocaml.inline always] + +val no_check_feq : t -> t -> t +[@@ocaml.inline always] + +val no_check_flt : t -> t -> t +[@@ocaml.inline always] + +val no_check_fle : t -> t -> t +[@@ocaml.inline always] + +val no_check_fcompare : t -> t -> t +[@@ocaml.inline always] + +val no_check_fclassify : t -> t +[@@ocaml.inline always] + +val no_check_fadd : t -> t -> t +[@@ocaml.inline always] + +val no_check_fsub : t -> t -> t +[@@ocaml.inline always] + +val no_check_fmul : t -> t -> t +[@@ocaml.inline always] + +val no_check_fdiv : t -> t -> t +[@@ocaml.inline always] + +val no_check_fsqrt : t -> t +[@@ocaml.inline always] + +val no_check_float_of_int : t -> t +[@@ocaml.inline always] + +val no_check_normfr_mantissa : t -> t +[@@ocaml.inline always] + +val no_check_frshiftexp : t -> t +[@@ocaml.inline always] + +val no_check_ldshiftexp : t -> t -> t +[@@ocaml.inline always] + +val no_check_next_up : t -> t +[@@ocaml.inline always] + +val no_check_next_down : t -> t +[@@ocaml.inline always] diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index e256466112..f0b706e4f5 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -24,7 +24,7 @@ type 'a delayed_universes = | PrivateMonomorphic of 'a | PrivatePolymorphic of int * Univ.ContextSet.t -type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option +type opaque_proofterm = (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; @@ -38,10 +38,10 @@ let drop_mono = function type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation type opaque = - | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) - | Direct of cooking_info list * proofterm +| Indirect of substitution list * cooking_info list * DirPath.t * int (* subst, discharge, lib, index *) + type opaquetab = { - opaque_val : (cooking_info list * proofterm) Int.Map.t; + opaque_val : proofterm Int.Map.t; (** Actual proof terms *) opaque_len : int; (** Size of the above map *) @@ -56,44 +56,33 @@ let empty_opaquetab = { let not_here () = CErrors.user_err Pp.(str "Cannot access opaque delayed proof") -let create cu = Direct ([],cu) - -let turn_indirect dp o tab = match o with - | Indirect (_,_,i) -> - if not (Int.Map.mem i tab.opaque_val) - then CErrors.anomaly (Pp.str "Indirect in a different table.") - else CErrors.anomaly (Pp.str "Already an indirect opaque.") - | Direct (d, cu) -> - (* Invariant: direct opaques only exist inside sections, we turn them - indirect as soon as we are at toplevel. At this moment, we perform - hashconsing of their contents, potentially as a future. *) - let hcons (c, u) = - let c = Constr.hcons c in - let u = match u with - | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) - | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) - in - (c, u) - in - let cu = Future.chain cu hcons in - let id = tab.opaque_len in - let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in - let opaque_dir = - if DirPath.equal dp tab.opaque_dir then tab.opaque_dir - else if DirPath.equal tab.opaque_dir DirPath.initial then dp - else CErrors.anomaly - (Pp.str "Using the same opaque table for multiple dirpaths.") in - let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in - Indirect ([],dp,id), ntab +let create dp cu tab = + let hcons (c, u) = + let c = Constr.hcons c in + let u = match u with + | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) + | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) + in + (c, u) + in + let cu = Future.chain cu hcons in + let id = tab.opaque_len in + let opaque_val = Int.Map.add id cu tab.opaque_val in + let opaque_dir = + if DirPath.equal dp tab.opaque_dir then tab.opaque_dir + else if DirPath.equal tab.opaque_dir DirPath.initial then dp + else CErrors.anomaly + (Pp.str "Using the same opaque table for multiple dirpaths.") in + let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in + Indirect ([], [], dp, id), ntab let subst_opaque sub = function - | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") +| Indirect (s, ci, dp, i) -> Indirect (sub :: s, ci, dp, i) -let discharge_direct_opaque ci = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d, cu) -> - Direct (ci :: d, cu) +let discharge_opaque info = function +| Indirect (s, ci, dp, i) -> + assert (CList.is_empty s); + Indirect ([], info :: ci, dp, i) let join except cu = match except with | None -> ignore (Future.join cu) @@ -102,25 +91,21 @@ let join except cu = match except with else ignore (Future.join cu) let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> join except cu - | Indirect (_,dp,i) -> - if DirPath.equal dp odp then - let (_, fp) = Int.Map.find i prfs in - join except fp +| Indirect (_,_,dp,i) -> + if DirPath.equal dp odp then + let fp = Int.Map.find i prfs in + join except fp let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (d, cu) -> - let (c, u) = Future.force cu in - access.access_discharge d (c, drop_mono u) - | Indirect (l,dp,i) -> + | Indirect (l,d,dp,i) -> let c, u = if DirPath.equal dp odp then - let (d, cu) = Int.Map.find i prfs in + let cu = Int.Map.find i prfs in let (c, u) = Future.force cu in access.access_discharge d (c, drop_mono u) else - let (d, cu) = access.access_proof dp i in + let cu = access.access_proof dp i in match cu with | None -> not_here () | Some (c, u) -> access.access_discharge d (c, u) @@ -133,26 +118,19 @@ let get_mono (_, u) = match u with | PrivatePolymorphic _ -> Univ.ContextSet.empty let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> - get_mono (Future.force cu) - | Indirect (_,dp,i) -> +| Indirect (_,_,dp,i) -> if DirPath.equal dp odp then - let ( _, cu) = Int.Map.find i prfs in + let cu = Int.Map.find i prfs in get_mono (Future.force cu) else Univ.ContextSet.empty -let get_direct_constraints = function -| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") -| Direct (_, cu) -> - Future.chain cu get_mono - module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n ([], None) in + let opaque_table = Array.make n None in let f2t_map = ref FMap.empty in - let iter n (d, cu) = + let iter n cu = let uid = Future.uuid cu in let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in let c = @@ -165,7 +143,7 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ CErrors.anomaly Pp.(str"Proof object "++int n++str" is not checked nor to be checked") in - opaque_table.(n) <- (d, c) + opaque_table.(n) <- c in let () = Int.Map.iter iter otab in opaque_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 7c53656c3c..1870241dcd 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -16,10 +16,7 @@ open Mod_subst Opaque proof terms are special since: - they can be lazily computed and substituted - they are stored in an optionally loaded segment of .vo files - An [opaque] proof terms holds the real data until fully discharged. - In this case it is called [direct]. - When it is [turn_indirect] the data is relocated to an opaque table - and the [opaque] is turned into an index. *) + An [opaque] proof terms holds an index into an opaque table. *) type 'a delayed_universes = | PrivateMonomorphic of 'a @@ -33,12 +30,7 @@ type opaque val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) -val create : proofterm -> opaque - -(** Turn a direct [opaque] into an indirect one. It is your responsibility to - hashcons the inner term beforehand. The integer is an hint of the maximum id - used so far *) -val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab +val create : DirPath.t -> proofterm -> opaquetab -> opaque * opaquetab type work_list = (Univ.Instance.t * Id.t array) Cmap.t * (Univ.Instance.t * Id.t array) Mindmap.t @@ -47,14 +39,14 @@ type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } -type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option +type opaque_proofterm = (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } -(** When stored indirectly, opaque terms are indexed by their library +(** Opaque terms are indexed by their library dirpath and an integer index. The two functions above activate this indirect storage, by telling how to retrieve terms. *) @@ -63,11 +55,10 @@ type indirect_accessor = { indirect opaque accessor given as an argument. *) val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t -val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation val subst_opaque : substitution -> opaque -> opaque -val discharge_direct_opaque : +val discharge_opaque : cooking_info -> opaque -> opaque val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit diff --git a/kernel/primred.ml b/kernel/primred.ml index d6d0a6143a..c475828cb3 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -14,6 +14,13 @@ let add_retroknowledge env action = | None -> { retro with retro_int63 = Some c } | Some c' -> assert (Constant.equal c c'); retro in set_retroknowledge env retro + | Register_type(PT_float64,c) -> + let retro = env.retroknowledge in + let retro = + match retro.retro_float64 with + | None -> { retro with retro_float64 = 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 = @@ -42,6 +49,21 @@ let add_retroknowledge env action = | None -> ((ind,1), (ind,2), (ind,3)) | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in { retro with retro_cmp = Some r } + | PIT_f_cmp -> + let r = + match retro.retro_f_cmp with + | None -> ((ind,1), (ind,2), (ind,3), (ind,4)) + | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in + { retro with retro_f_cmp = Some r } + | PIT_f_class -> + let r = + match retro.retro_f_class with + | None -> ((ind,1), (ind,2), (ind,3), (ind,4), + (ind,5), (ind,6), (ind,7), (ind,8), + (ind,9)) + | Some (((ind',_),_,_,_,_,_,_,_,_) as t) -> + assert (eq_ind ind ind'); t in + { retro with retro_f_class = Some r } in set_retroknowledge env retro @@ -50,6 +72,17 @@ let get_int_type env = | Some c -> c | None -> anomaly Pp.(str"Reduction of primitive: int63 not registered") +let get_float_type env = + match env.retroknowledge.retro_float64 with + | Some c -> c + | None -> anomaly Pp.(str"Reduction of primitive: float64 not registered") + +let get_cmp_type env = + match env.retroknowledge.retro_cmp with + | Some (((mindcmp,_),_),_,_) -> + Constant.make (MutInd.user mindcmp) (MutInd.canonical mindcmp) + | None -> anomaly Pp.(str"Reduction of primitive: comparison not registered") + let get_bool_constructors env = match env.retroknowledge.retro_bool with | Some r -> r @@ -70,6 +103,16 @@ let get_cmp_constructors env = | Some r -> r | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered") +let get_f_cmp_constructors env = + match env.retroknowledge.retro_f_cmp with + | Some r -> r + | None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered") + +let get_f_class_constructors env = + match env.retroknowledge.retro_f_class with + | Some r -> r + | None -> anomaly Pp.(str"Reduction of primitive: fclass not registered") + exception NativeDestKO module type RedNativeEntries = @@ -80,14 +123,29 @@ module type RedNativeEntries = val get : args -> int -> elem val get_int : evd -> elem -> Uint63.t + val get_float : evd -> elem -> Float64.t val mkInt : env -> Uint63.t -> elem + val mkFloat : env -> Float64.t -> elem val mkBool : env -> bool -> elem val mkCarry : env -> bool -> elem -> elem (* true if carry *) val mkIntPair : env -> elem -> elem -> elem + val mkFloatIntPair : env -> elem -> elem -> elem val mkLt : env -> elem val mkEq : env -> elem val mkGt : env -> elem - + val mkFLt : env -> elem + val mkFEq : env -> elem + val mkFGt : env -> elem + val mkFNotComparable : env -> elem + val mkPNormal : env -> elem + val mkNNormal : env -> elem + val mkPSubn : env -> elem + val mkNSubn : env -> elem + val mkPZero : env -> elem + val mkNZero : env -> elem + val mkPInf : env -> elem + val mkNInf : env -> elem + val mkNaN : env -> elem end module type RedNative = @@ -116,6 +174,12 @@ struct let get_int3 evd args = get_int evd args 0, get_int evd args 1, get_int evd args 2 + let get_float evd args i = E.get_float evd (E.get args i) + + let get_float1 evd args = get_float evd args 0 + + let get_float2 evd args = get_float evd args 0, get_float evd args 1 + let red_prim_aux env evd op args = let open CPrimitives in match op with @@ -193,6 +257,64 @@ struct | 0 -> E.mkEq env | _ -> E.mkGt env end + | Float64opp -> + let f = get_float1 evd args in E.mkFloat env (Float64.opp f) + | Float64abs -> + let f = get_float1 evd args in E.mkFloat env (Float64.abs f) + | Float64eq -> + let i1, i2 = get_float2 evd args in + E.mkBool env (Float64.eq i1 i2) + | Float64lt -> + let i1, i2 = get_float2 evd args in + E.mkBool env (Float64.lt i1 i2) + | Float64le -> + let i1, i2 = get_float2 evd args in + E.mkBool env (Float64.le i1 i2) + | Float64compare -> + let f1, f2 = get_float2 evd args in + (match Float64.compare f1 f2 with + | Float64.FEq -> E.mkFEq env + | Float64.FLt -> E.mkFLt env + | Float64.FGt -> E.mkFGt env + | Float64.FNotComparable -> E.mkFNotComparable env) + | Float64classify -> + let f = get_float1 evd args in + (match Float64.classify f with + | Float64.PNormal -> E.mkPNormal env + | Float64.NNormal -> E.mkNNormal env + | Float64.PSubn -> E.mkPSubn env + | Float64.NSubn -> E.mkNSubn env + | Float64.PZero -> E.mkPZero env + | Float64.NZero -> E.mkNZero env + | Float64.PInf -> E.mkPInf env + | Float64.NInf -> E.mkNInf env + | Float64.NaN -> E.mkNaN env) + | Float64add -> + let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2) + | Float64sub -> + let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.sub f1 f2) + | Float64mul -> + let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.mul f1 f2) + | Float64div -> + let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.div f1 f2) + | Float64sqrt -> + let f = get_float1 evd args in E.mkFloat env (Float64.sqrt f) + | Float64ofInt63 -> + let i = get_int1 evd args in E.mkFloat env (Float64.of_int63 i) + | Float64normfr_mantissa -> + let f = get_float1 evd args in E.mkInt env (Float64.normfr_mantissa f) + | Float64frshiftexp -> + let f = get_float1 evd args in + let (m,e) = Float64.frshiftexp f in + E.mkFloatIntPair env (E.mkFloat env m) (E.mkInt env e) + | Float64ldshiftexp -> + let f = get_float evd args 0 in + let e = get_int evd args 1 in + E.mkFloat env (Float64.ldshiftexp f e) + | Float64next_up -> + let f = get_float1 evd args in E.mkFloat env (Float64.next_up f) + | Float64next_down -> + let f = get_float1 evd args in E.mkFloat env (Float64.next_down f) let red_prim env evd p args = try diff --git a/kernel/primred.mli b/kernel/primred.mli index f5998982d7..bbe564d8e7 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -5,10 +5,17 @@ open Environ val add_retroknowledge : env -> Retroknowledge.action -> env val get_int_type : env -> Constant.t +val get_float_type : env -> Constant.t +val get_cmp_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 +val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor +val get_f_class_constructors : + env -> constructor * constructor * constructor * constructor + * constructor * constructor * constructor * constructor + * constructor exception NativeDestKO (* Should be raised by get_* functions on failure *) @@ -20,13 +27,29 @@ module type RedNativeEntries = val get : args -> int -> elem val get_int : evd -> elem -> Uint63.t + val get_float : evd -> elem -> Float64.t val mkInt : env -> Uint63.t -> elem + val mkFloat : env -> Float64.t -> elem val mkBool : env -> bool -> elem val mkCarry : env -> bool -> elem -> elem (* true if carry *) val mkIntPair : env -> elem -> elem -> elem + val mkFloatIntPair : env -> elem -> elem -> elem val mkLt : env -> elem val mkEq : env -> elem val mkGt : env -> elem + val mkFLt : env -> elem + val mkFEq : env -> elem + val mkFGt : env -> elem + val mkFNotComparable : env -> elem + val mkPNormal : env -> elem + val mkNNormal : env -> elem + val mkPSubn : env -> elem + val mkNSubn : env -> elem + val mkPZero : env -> elem + val mkNZero : env -> elem + val mkPInf : env -> elem + val mkNInf : env -> elem + val mkNaN : env -> elem end module type RedNative = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 53f228c618..0cc7692fcf 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -138,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 _|Int _) -> x + Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> x | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ -> x + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ -> x | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x) @@ -152,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 _|Int _) -> t + Prod _|Lambda _|Fix _|CoFix _|Int _|Float _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Int _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ -> 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) @@ -166,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 _|Int _) -> t + Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t) @@ -627,13 +627,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if Uint63.equal i1 i2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible + | FFloat f1, FFloat f2 -> + if Float64.equal f1 f2 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 _ | FInt _), _ -> raise NotConvertible + | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> 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 @@ -777,7 +781,7 @@ let infer_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u - | Type _u, Prop -> raise NotConvertible + | Type u, Prop -> infer_pb u Univ.type0m_univ | Type u, Set -> infer_pb u Univ.type0_univ | Type u0, Type u1 -> infer_pb u0 u1 diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 873c6af93d..479fe02295 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -18,23 +18,37 @@ open Names type retroknowledge = { retro_int63 : Constant.t option; + retro_float64 : 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; + retro_f_cmp : (constructor * constructor * constructor * constructor) + option; + (* FEq, FLt, FGt, FNotComparable *) + retro_f_class : (constructor * constructor * constructor * constructor + * constructor * constructor * constructor * constructor + * constructor) + option; + (* PNormal, NNormal, PSubn, NSubn, + PZero, NZero, PInf, NInf, + NaN *) + retro_refl : constructor option } let empty = { retro_int63 = None; + retro_float64 = None; retro_bool = None; retro_carry = None; retro_pair = None; retro_cmp = None; + retro_f_cmp = None; + retro_f_class = None; retro_refl = None; } type action = - | Register_ind of CPrimitives.prim_ind * inductive - | Register_type of CPrimitives.prim_type * Constant.t + | Register_ind : 'a CPrimitives.prim_ind * inductive -> action + | Register_type : CPrimitives.prim_type * Constant.t -> action diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 2a7b390951..2df8a00465 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -12,16 +12,27 @@ open Names type retroknowledge = { retro_int63 : Constant.t option; + retro_float64 : 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; + retro_f_cmp : (constructor * constructor * constructor * constructor) + option; + (* FEq, FLt, FGt, FNotComparable *) + retro_f_class : (constructor * constructor * constructor * constructor + * constructor * constructor * constructor * constructor + * constructor) + option; + (* PNormal, NNormal, PSubn, NSubn, + PZero, NZero, PInf, NInf, + NaN *) + retro_refl : constructor option } val empty : retroknowledge type action = - | Register_ind of CPrimitives.prim_ind * inductive - | Register_type of CPrimitives.prim_type * Constant.t + | Register_ind : 'a CPrimitives.prim_ind * inductive -> action + | Register_type : CPrimitives.prim_type * Constant.t -> action diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml index a51b762f95..5c15257511 100644 --- a/kernel/retypeops.ml +++ b/kernel/retypeops.ml @@ -60,7 +60,7 @@ let rec relevance_of_fterm env extra lft f = | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft) | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c | FFlex key -> relevance_of_flex env extra lft key - | FInt _ -> Sorts.Relevant + | FInt _ | FFloat _ -> Sorts.Relevant | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) | FConstruct (c,_) -> relevance_of_constructor env c | FApp (f, _) -> relevance_of_fterm env extra lft f @@ -71,6 +71,7 @@ let rec relevance_of_fterm env extra lft f = | FLambda (len, tys, bdy, e) -> let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in let lft = Esubst.el_liftn len lft in + let e = Esubst.subs_liftn len e in relevance_of_term_extra env extra lft e bdy | FLetIn (x, _, _, bdy, e) -> relevance_of_term_extra env (x.binder_relevance :: extra) @@ -104,7 +105,7 @@ and relevance_of_term_extra env extra lft subs c = | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> relevance_of_projection env p - | Int _ -> Sorts.Relevant + | Int _ | Float _ -> Sorts.Relevant | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ea45f699ce..d3cffd1546 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -113,8 +113,16 @@ type library_info = DirPath.t * vodigest (** Functor and funsig parameters, most recent first *) type module_parameters = (MBId.t * module_type_body) list +(** Part of the safe_env at a section opening time to be backtracked *) +type section_data = { + rev_env : Environ.env; + rev_univ : Univ.ContextSet.t; + rev_objlabels : Label.Set.t; +} + type safe_environment = { env : Environ.env; + sections : section_data Section.t; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -151,6 +159,7 @@ let empty_environment = revstruct = []; modlabels = Label.Set.empty; objlabels = Label.Set.empty; + sections = Section.empty; future_cst = []; univ = Univ.ContextSet.empty; engagement = None; @@ -164,6 +173,8 @@ let is_initial senv = | [], NONE -> ModPath.equal senv.modpath ModPath.initial | _ -> false +let sections_are_opened senv = not (Section.is_empty senv.sections) + let delta_of_senv senv = senv.modresolver,senv.paramresolver let constant_of_delta_kn_senv senv kn = @@ -194,6 +205,18 @@ let set_typing_flags c senv = if env == senv.env then senv else { senv with env } +let set_check_guarded b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_guarded = b } senv + +let set_check_positive b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_positive = b } senv + +let set_check_universes b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_universes = b } senv + let set_indices_matter indices_matter senv = set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv @@ -276,18 +299,11 @@ let lift_constant c = in { c with const_body = body } -let map_constant f c = - let body = match c.const_body with - | OpaqueDef o -> OpaqueDef (f o) - | Def _ | Undef _ | Primitive _ as body -> body - in - { c with const_body = body } - let push_private_constants env eff = let eff = side_effects_of_private_constants eff in let add_if_undefined env eff = - try ignore(Environ.lookup_constant eff.seff_constant env); env - with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env + if Environ.mem_constant eff.seff_constant env then env + else Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env in List.fold_left add_if_undefined env eff @@ -297,22 +313,31 @@ let concat_private = SideEffects.concat let universes_of_private eff = let fold acc eff = match eff.seff_body.const_universes with - | Monomorphic ctx -> ctx :: acc + | Monomorphic ctx -> Univ.ContextSet.union ctx acc | Polymorphic _ -> acc in - List.fold_left fold [] (side_effects_of_private_constants eff) + List.fold_left fold Univ.ContextSet.empty (side_effects_of_private_constants eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env +let sections_of_safe_env senv = senv.sections + type constraints_addition = | Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation let push_context_set poly cst senv = - { senv with - env = Environ.push_context_set ~strict:(not poly) cst senv.env; - univ = Univ.ContextSet.union cst senv.univ } + if Univ.ContextSet.is_empty cst then senv + else + let sections = + if Section.is_empty senv.sections then senv.sections + else Section.push_constraints cst senv.sections + in + { senv with + env = Environ.push_context_set ~strict:(not poly) cst senv.env; + univ = Univ.ContextSet.union cst senv.univ; + sections } let add_constraints cst senv = match cst with @@ -374,7 +399,7 @@ let check_current_library dir senv = match senv.modvariant with (** When operating on modules, we're normally outside sections *) let check_empty_context senv = - assert (Environ.empty_context senv.env) + assert (Environ.empty_context senv.env && Section.is_empty senv.sections) (** When adding a parameter to the current module/modtype, it must have been freshly started *) @@ -421,19 +446,30 @@ let safe_push_named d env = with Not_found -> () in Environ.push_named d env - let push_named_def (id,de) senv = + let sections = Section.push_local senv.sections in let c, r, typ = Term_typing.translate_local_def senv.env id de in let x = Context.make_annot id r in let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in - { senv with env = env'' } + { senv with sections; env = env'' } let push_named_assum (x,t) senv = + let sections = Section.push_local senv.sections in let t, r = Term_typing.translate_local_assum senv.env t in let x = Context.make_annot x r in let env'' = safe_push_named (LocalAssum (x,t)) senv.env in - {senv with env=env''} - + { senv with sections; env = env'' } + +let push_section_context (nas, ctx) senv = + let sections = Section.push_context (nas, ctx) senv.sections in + let senv = { senv with sections } in + let ctx = Univ.ContextSet.of_context ctx in + (* We check that the universes are fresh. FIXME: This should be done + implicitly, but we have to work around the API. *) + let () = assert (Univ.LSet.for_all (fun u -> not (Univ.LSet.mem u (fst senv.univ))) (fst ctx)) in + { senv with + env = Environ.push_context_set ~strict:false ctx senv.env; + univ = Univ.ContextSet.union ctx senv.univ } (** {6 Insertion of new declarations to current environment } *) @@ -515,8 +551,19 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = | SFBmodule mb, M -> Modops.add_module mb senv.env | _ -> assert false in + let sections = match sfb, gn with + | SFBconst cb, C con -> + let poly = Declareops.constant_is_polymorphic cb in + Section.push_constant ~poly con senv.sections + | SFBmind mib, I mind -> + let poly = Declareops.inductive_is_polymorphic mib in + Section.push_inductive ~poly mind senv.sections + | _, (M | MT) -> senv.sections + | _ -> assert false + in { senv with env = env'; + sections; revstruct = field :: senv.revstruct; modlabels = Label.Set.union mlabs senv.modlabels; objlabels = Label.Set.union olabs senv.objlabels } @@ -525,42 +572,17 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = let update_resolver f senv = { senv with modresolver = f senv.modresolver } -(** Insertion of constants and parameters in environment *) -type 'a effect_entry = -| EffectEntry : private_constants Entries.seff_wrap effect_entry -| PureEntry : unit effect_entry - type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration type exported_private_constant = Constant.t -let add_constant_aux ~in_section senv (kn, cb) = +let add_constant_aux senv (kn, cb) = let l = Constant.label kn in - let delayed_cst = match cb.const_body with - | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) -> - let fc = Opaqueproof.get_direct_constraints o in - begin match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now c] - end - | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] - in (* This is the only place where we hashcons the contents of a constant body *) - let cb = if in_section then cb else Declareops.hcons_const_body cb in - let cb, otab = match cb.const_body with - | OpaqueDef lc when not in_section -> - (* In coqc, opaque constants outside sections will be stored - indirectly in a specific table *) - let od, otab = - Opaqueproof.turn_indirect - (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in - { cb with const_body = OpaqueDef od }, otab - | _ -> cb, (Environ.opaque_tables senv.env) - in - let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in + let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in - let senv' = add_constraints_list delayed_cst senv' in let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver @@ -576,8 +598,8 @@ let inline_side_effects env body side_eff = (** First step: remove the constants that are still in the environment *) let filter e = let cb = (e.seff_constant, e.seff_body) in - try ignore (Environ.lookup_constant e.seff_constant env); None - with Not_found -> Some (cb, e.from_env) + if Environ.mem_constant e.seff_constant env then None + else Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) let side_eff = List.map_filter filter (SideEffects.repr side_eff) in @@ -671,7 +693,7 @@ let check_signatures curmb sl = type side_effect_declaration = | DefinitionEff : Entries.definition_entry -> side_effect_declaration -| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration +| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration let constant_entry_of_side_effect eff = let cb = eff.seff_body in @@ -690,8 +712,8 @@ let constant_entry_of_side_effect eff = | _ -> assert false in if Declareops.is_opaque cb then OpaqueEff { - opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - opaque_entry_secctx = cb.const_hyps; + opaque_entry_body = p; + opaque_entry_secctx = Context.Named.to_vars cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; @@ -699,7 +721,7 @@ let constant_entry_of_side_effect eff = else DefinitionEff { const_entry_body = p; - const_entry_secctx = Some cb.const_hyps; + const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps); const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; @@ -708,10 +730,27 @@ let constant_entry_of_side_effect eff = let export_eff eff = (eff.seff_constant, eff.seff_body) +let is_empty_private = function +| Opaqueproof.PrivateMonomorphic ctx -> Univ.ContextSet.is_empty ctx +| Opaqueproof.PrivatePolymorphic (_, ctx) -> Univ.ContextSet.is_empty ctx + +let empty_private univs = match univs with +| Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty +| Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) + +(* Special function to call when the body of an opaque definition is provided. + It performs the type-checking of the body immediately. *) +let translate_direct_opaque env kn ce = + let cb, ctx = Term_typing.translate_opaque env kn ce in + let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in + let handle _env c () = (c, Univ.ContextSet.empty, 0) in + let (c, u) = Term_typing.check_delayed handle ctx (body, ()) in + (* No constraints can be generated, we set it empty everywhere *) + let () = assert (is_empty_private u) in + { cb with const_body = OpaqueDef c } + let export_side_effects mb env (b_ctx, eff) = - let not_exists e = - try ignore(Environ.lookup_constant e.seff_constant env); false - with Not_found -> true in + let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl else e :: acc, e.from_env :: sl in @@ -732,26 +771,14 @@ let export_side_effects mb env (b_ctx, eff) = if Int.equal sl 0 then let env, cb = let kn = eff.seff_constant in - let ce = constant_entry_of_side_effect eff in - let open Entries in - let open Term_typing in - let cb = match ce with - | DefinitionEff ce -> - Term_typing.translate_constant Pure env kn (DefinitionEntry ce) - | OpaqueEff ce -> - let handle _env c () = (c, Univ.ContextSet.empty, 0) in - Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce) - in - let map cu = - let (c, u) = Future.force cu in - let () = match u with - | Opaqueproof.PrivateMonomorphic ctx - | Opaqueproof.PrivatePolymorphic (_, ctx) -> - assert (Univ.ContextSet.is_empty ctx) - in - c + let ce = constant_entry_of_side_effect eff in + let open Entries in + let cb = match ce with + | DefinitionEff ce -> + Term_typing.translate_constant env kn (DefinitionEntry ce) + | OpaqueEff ce -> + translate_direct_opaque env kn ce in - let cb = map_constant map cb in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) in @@ -763,77 +790,103 @@ let export_side_effects mb env (b_ctx, eff) = in translate_seff trusted seff [] env -let export_private_constants ~in_section ce senv = +let push_opaque_proof pf senv = + let o, otab = Opaqueproof.create (library_dp_of_senv senv) pf (Environ.opaque_tables senv.env) in + let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in + senv, o + +let export_private_constants ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map univs p = - let local = match univs with - | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty - | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) - in - Opaqueproof.create (Future.from_val (p, local)) + let map senv (kn, c) = match c.const_body with + | OpaqueDef p -> + let local = empty_private c.const_universes in + let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in + senv, (kn, { c with const_body = OpaqueDef o }) + | Def _ | Undef _ | Primitive _ as body -> + senv, (kn, { c with const_body = body }) in - let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in - let bodies = List.map map exported in + let senv, bodies = List.fold_left_map map senv exported in let exported = List.map (fun (kn, _) -> kn) exported in - let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in + (* No delayed constants to declare *) + let senv = List.fold_left add_constant_aux senv bodies in (ce, exported), senv -let add_recipe ~in_section l r senv = +let add_constant l decl senv = let kn = Constant.make2 senv.modpath l in - let cb = Term_typing.translate_recipe senv.env kn r in - let senv = add_constant_aux ~in_section senv (kn, cb) in - kn, senv - -let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = - let kn = Constant.make2 senv.modpath l in - let cb = + let cb = match decl with - | ConstantEntry (EffectEntry, ce) -> + | OpaqueEntry ce -> let handle env body eff = let body, uctx, signatures = inline_side_effects env body eff in let trusted = check_signatures senv.revstruct signatures in body, uctx, trusted in - Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce - | ConstantEntry (PureEntry, ce) -> - Term_typing.translate_constant Term_typing.Pure senv.env kn ce + let cb, ctx = Term_typing.translate_opaque senv.env kn ce in + let map pf = Term_typing.check_delayed handle ctx pf in + let pf = Future.chain ce.Entries.opaque_entry_body map in + { cb with const_body = OpaqueDef pf } + | ConstantEntry ce -> + Term_typing.translate_constant senv.env kn ce in let senv = - let cb = map_constant (fun c -> Opaqueproof.create c) cb in - add_constant_aux ~in_section senv (kn, cb) in + let senv, cb, delayed_cst = match cb.const_body with + | OpaqueDef fc -> + let senv, o = push_opaque_proof fc senv in + let delayed_cst = + if not (Declareops.constant_is_polymorphic cb) then + let map (_, u) = match u with + | Opaqueproof.PrivateMonomorphic ctx -> ctx + | Opaqueproof.PrivatePolymorphic _ -> assert false + in + let fc = Future.chain fc map in + match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now c] + else [] + in + senv, { cb with const_body = OpaqueDef o }, delayed_cst + | Undef _ | Def _ | Primitive _ as body -> + senv, { cb with const_body = body }, [] + in + let senv = add_constant_aux senv (kn, cb) in + add_constraints_list delayed_cst senv + 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"); + | ConstantEntry (Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ }) -> + if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - let eff : a = match side_effect with - | PureEntry -> () - | EffectEntry -> - let body, univs = match cb.const_body with - | (Primitive _ | Undef _) -> assert false - | Def c -> (Def c, cb.const_universes) - | OpaqueDef o -> - let (b, delayed) = Future.force o in - match cb.const_universes, delayed with - | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx -> - OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') - | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) -> - (* Upper layers enforce that there are no internal constraints *) - let () = assert (Univ.ContextSet.is_empty ctx) in - OpaqueDef b, Polymorphic auctx - | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) -> - assert false + kn, senv + +let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment = + let kn = Constant.make2 senv.modpath l in + let cb = + match decl with + | OpaqueEff ce -> + translate_direct_opaque senv.env kn ce + | DefinitionEff ce -> + Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce) in - let cb = { cb with const_body = body; const_universes = univs } in + let senv, dcb = match cb.const_body with + | Def _ as const_body -> senv, { cb with const_body } + | OpaqueDef c -> + let local = empty_private cb.const_universes in + let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in + senv, { cb with const_body = OpaqueDef o } + | Undef _ | Primitive _ -> assert false + in + let senv = add_constant_aux senv (kn, dcb) in + let eff = let from_env = CEphemeron.create senv.revstruct in let eff = { from_env = from_env; seff_constant = kn; seff_body = cb; } in - { Entries.seff_wrap = SideEffects.add eff empty_private_constants } + SideEffects.add eff empty_private_constants in (kn, eff), senv @@ -890,6 +943,75 @@ let add_module l me inl senv = in (mp,mb.mod_delta),senv'' +(** {6 Interactive sections *) + +let open_section senv = + let custom = { + rev_env = senv.env; + rev_univ = senv.univ; + rev_objlabels = senv.objlabels; + } in + let sections = Section.open_section ~custom senv.sections in + { senv with sections } + +let close_section senv = + let open Section in + let sections0 = senv.sections in + let env0 = senv.env in + (* First phase: revert the declarations added in the section *) + let sections, entries, cstrs, revert = Section.close_section sections0 in + let rec pop_revstruct accu entries revstruct = match entries, revstruct with + | [], revstruct -> accu, revstruct + | _ :: _, [] -> + CErrors.anomaly (Pp.str "Unmatched section data") + | entry :: entries, (lbl, leaf) :: revstruct -> + let data = match entry, leaf with + | SecDefinition kn, SFBconst cb -> + let () = assert (Label.equal lbl (Constant.label kn)) in + `Definition (kn, cb) + | SecInductive ind, SFBmind mib -> + let () = assert (Label.equal lbl (MutInd.label ind)) in + `Inductive (ind, mib) + | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) -> + CErrors.anomaly (Pp.str "Section content mismatch") + | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) -> + CErrors.anomaly (Pp.str "Module inside a section") + in + pop_revstruct (data :: accu) entries revstruct + in + let redo, revstruct = pop_revstruct [] entries senv.revstruct in + (* Don't revert the delayed constraints. If some delayed constraints were + forced inside the section, they have been turned into global monomorphic + that are going to be replayed. Those that are not forced are not readded + by {!add_constant_aux}. *) + let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in + (* Do not revert the opaque table, the discharged opaque constants are + referring to it. *) + let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in + let senv = { senv with env; revstruct; sections; univ; objlabels; } in + (* Second phase: replay the discharged section contents *) + let senv = add_constraints (Now cstrs) senv in + let modlist = Section.replacement_context env0 sections0 in + let cooking_info seg = + let { abstr_ctx; abstr_subst; abstr_uctx } = seg in + let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in + { Opaqueproof.modlist; abstract } + in + let fold senv = function + | `Definition (kn, cb) -> + let info = cooking_info (Section.segment_of_constant env0 kn sections0) in + let r = { Cooking.from = cb; info } in + let cb = Term_typing.translate_recipe senv.env kn r in + (* Delayed constants are already in the global environment *) + add_constant_aux senv (kn, cb) + | `Inductive (ind, mib) -> + let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in + let mie = Cooking.cook_inductive info mib in + let mie = InferCumulativity.infer_inductive senv.env mie in + let _, senv = add_mind (MutInd.label ind) mie senv in + senv + in + List.fold_left fold senv redo (** {6 Starting / ending interactive modules and module types } *) @@ -1205,7 +1327,7 @@ 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 ind r env = +let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = let (mb,ob as spec) = Inductive.lookup_mind_specif env ind in let check_if b msg = if not b then @@ -1281,6 +1403,36 @@ let check_register_ind ind r env = check_type_cte 1; check_name 2 "Gt"; check_type_cte 2 + | CPrimitives.PIT_f_cmp -> + check_nconstr 4; + check_name 0 "FEq"; + check_type_cte 0; + check_name 1 "FLt"; + check_type_cte 1; + check_name 2 "FGt"; + check_type_cte 2; + check_name 3 "FNotComparable"; + check_type_cte 3 + | CPrimitives.PIT_f_class -> + check_nconstr 9; + check_name 0 "PNormal"; + check_type_cte 0; + check_name 1 "NNormal"; + check_type_cte 1; + check_name 2 "PSubn"; + check_type_cte 2; + check_name 3 "NSubn"; + check_type_cte 3; + check_name 4 "PZero"; + check_type_cte 4; + check_name 5 "NZero"; + check_type_cte 5; + check_name 6 "PInf"; + check_type_cte 6; + check_name 7 "NInf"; + check_type_cte 7; + check_name 8 "NaN"; + check_type_cte 8 let register_inductive ind prim senv = check_register_ind ind prim senv.env; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2406b6add1..ae6993b0e2 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -27,12 +27,16 @@ val digest_match : actual:vodigest -> required:vodigest -> bool type safe_environment +type section_data + val empty_environment : safe_environment val is_initial : safe_environment -> bool val env_of_safe_env : safe_environment -> Environ.env +val sections_of_safe_env : safe_environment -> section_data Section.t + (** The safe_environment state monad *) type safe_transformer0 = safe_environment -> safe_environment @@ -55,7 +59,7 @@ val inline_private_constants : val push_private_constants : Environ.env -> private_constants -> Environ.env (** Push the constants in the environment if not already there. *) -val universes_of_private : private_constants -> Univ.ContextSet.t list +val universes_of_private : private_constants -> Univ.ContextSet.t val is_curmod_library : safe_environment -> bool @@ -67,37 +71,29 @@ val join_safe_environment : val is_joined_environment : safe_environment -> bool (** {6 Enriching a safe environment } *) -(** Insertion of local declarations (Local or Variables) *) - -val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 - -(** Returns the full universe context necessary to typecheck the definition - (futures are forced) *) -val push_named_def : - Id.t * Entries.section_def_entry -> safe_transformer0 - (** Insertion of global axioms or definitions *) -type 'a effect_entry = -| EffectEntry : private_constants Entries.seff_wrap effect_entry -| PureEntry : unit effect_entry - type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration + +type side_effect_declaration = +| DefinitionEff : Entries.definition_entry -> side_effect_declaration +| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration type exported_private_constant = Constant.t -val export_private_constants : in_section:bool -> +val export_private_constants : private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer -(** returns the main constant plus a certificate of its validity *) +(** returns the main constant *) val add_constant : - side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> - (Constant.t * 'a) safe_transformer + Label.t -> global_declaration -> Constant.t safe_transformer -val add_recipe : - in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer +(** Similar to add_constant but also returns a certificate *) +val add_private_constant : + Label.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer (** Adding an inductive type *) @@ -130,6 +126,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0 val set_indices_matter : bool -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 val set_share_reduction : bool -> safe_transformer0 +val set_check_guarded : bool -> safe_transformer0 +val set_check_positive : bool -> safe_transformer0 +val set_check_universes : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 val set_native_compiler : bool -> safe_transformer0 val make_sprop_cumulative : safe_transformer0 @@ -137,6 +136,24 @@ val set_allow_sprop : bool -> safe_transformer0 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit +(** {6 Interactive section functions } *) + +val open_section : safe_transformer0 + +val close_section : safe_transformer0 + +val sections_are_opened : safe_environment -> bool + +(** Insertion of local declarations (Local or Variables) *) + +val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 + +val push_named_def : + Id.t * Entries.section_def_entry -> safe_transformer0 + +(** Add local universes to a polymorphic section *) +val push_section_context : (Name.t array * Univ.UContext.t) -> safe_transformer0 + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer @@ -209,7 +226,7 @@ val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t (** {6 Retroknowledge / Native compiler } *) val register_inline : Constant.t -> safe_transformer0 -val register_inductive : inductive -> CPrimitives.prim_ind -> safe_transformer0 +val register_inductive : inductive -> 'a CPrimitives.prim_ind -> safe_transformer0 val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 diff --git a/kernel/section.ml b/kernel/section.ml new file mode 100644 index 0000000000..a1242f0faf --- /dev/null +++ b/kernel/section.ml @@ -0,0 +1,218 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 Util +open Names +open Univ + +module NamedDecl = Context.Named.Declaration + +type section_entry = +| SecDefinition of Constant.t +| SecInductive of MutInd.t + +type 'a entry_map = 'a Cmap.t * 'a Mindmap.t + +type 'a section = { + sec_context : int; + (** Length of the named context suffix that has been introduced locally *) + sec_mono_universes : ContextSet.t; + sec_poly_universes : Name.t array * UContext.t; + (** Universes local to the section *) + has_poly_univs : bool; + (** Are there polymorphic universes or constraints, including in previous sections. *) + sec_entries : section_entry list; + (** Definitions introduced in the section *) + sec_data : (Instance.t * AUContext.t) entry_map; + (** Additional data synchronized with the section *) + sec_custom : 'a; +} + +(** Sections can be nested with the proviso that no monomorphic section can be + opened inside a polymorphic one. The reverse is allowed. *) +type 'a t = 'a section list + +let empty = [] + +let is_empty = List.is_empty + +let depth = List.length + +let has_poly_univs = function + | [] -> false + | sec :: _ -> sec.has_poly_univs + +let find_emap e (cmap, imap) = match e with +| SecDefinition con -> Cmap.find con cmap +| SecInductive ind -> Mindmap.find ind imap + +let add_emap e v (cmap, imap) = match e with +| SecDefinition con -> (Cmap.add con v cmap, imap) +| SecInductive ind -> (cmap, Mindmap.add ind v imap) + +let on_last_section f sections = match sections with +| [] -> CErrors.user_err (Pp.str "No opened section") +| sec :: rem -> f sec :: rem + +let with_last_section f sections = match sections with +| [] -> f None +| sec :: _ -> f (Some sec) + +let push_local s = + let on_sec sec = { sec with sec_context = sec.sec_context + 1 } in + on_last_section on_sec s + +let push_context (nas, ctx) s = + let on_sec sec = + if UContext.is_empty ctx then sec + else + let (snas, sctx) = sec.sec_poly_universes in + let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in + { sec with sec_poly_universes; has_poly_univs = true } + in + on_last_section on_sec s + +let is_polymorphic_univ u s = + let check sec = + let (_, uctx) = sec.sec_poly_universes in + Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) + in + List.exists check s + +let push_constraints uctx s = + let on_sec sec = + if sec.has_poly_univs && Constraint.exists (fun (l,_,r) -> is_polymorphic_univ l s || is_polymorphic_univ r s) (snd uctx) + then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes."); + let uctx' = sec.sec_mono_universes in + let sec_mono_universes = (ContextSet.union uctx uctx') in + { sec with sec_mono_universes } + in + on_last_section on_sec s + +let open_section ~custom sections = + let sec = { + sec_context = 0; + sec_mono_universes = ContextSet.empty; + sec_poly_universes = ([||], UContext.empty); + has_poly_univs = has_poly_univs sections; + sec_entries = []; + sec_data = (Cmap.empty, Mindmap.empty); + sec_custom = custom; + } in + sec :: sections + +let close_section sections = + match sections with + | sec :: sections -> + sections, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom + | [] -> + CErrors.user_err (Pp.str "No opened section.") + +let make_decl_univs (nas,uctx) = abstract_universes nas uctx + +let push_global ~poly e s = + if is_empty s then s + else if has_poly_univs s && not poly + then CErrors.user_err + Pp.(str "Cannot add a universe monomorphic declaration when \ + section polymorphic universes are present.") + else + let on_sec sec = + { sec with + sec_entries = e :: sec.sec_entries; + sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data; + } + in + on_last_section on_sec s + +let push_constant ~poly con s = push_global ~poly (SecDefinition con) s + +let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s + +type abstr_info = { + abstr_ctx : Constr.named_context; + abstr_subst : Instance.t; + abstr_uctx : AUContext.t; +} + +let empty_segment = { + abstr_ctx = []; + abstr_subst = Instance.empty; + abstr_uctx = AUContext.empty; +} + +let extract_hyps sec vars used = + (* Keep the section-local segment of variables *) + let vars = List.firstn sec.sec_context vars in + (* Only keep the part that is used by the declaration *) + List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars + +let section_segment_of_entry vars e hyps sections = + (* [vars] are the named hypotheses, [hyps] the subset that is declared by the + global *) + let with_sec s = match s with + | None -> + CErrors.user_err (Pp.str "No opened section.") + | Some sec -> + let hyps = extract_hyps sec vars hyps in + let inst, auctx = find_emap e sec.sec_data in + { + abstr_ctx = hyps; + abstr_subst = inst; + abstr_uctx = auctx; + } + in + with_last_section with_sec sections + +let segment_of_constant env con s = + let body = Environ.lookup_constant con env in + let vars = Environ.named_context env in + let used = Context.Named.to_vars body.Declarations.const_hyps in + section_segment_of_entry vars (SecDefinition con) used s + +let segment_of_inductive env mind s = + let mib = Environ.lookup_mind mind env in + let vars = Environ.named_context env in + let used = Context.Named.to_vars mib.Declarations.mind_hyps in + section_segment_of_entry vars (SecInductive mind) used s + +let instance_from_variable_context = + List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list + +let extract_worklist info = + let args = instance_from_variable_context info.abstr_ctx in + info.abstr_subst, args + +let replacement_context env s = + let with_sec sec = match sec with + | None -> CErrors.user_err (Pp.str "No opened section.") + | Some sec -> + let cmap, imap = sec.sec_data in + let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in + let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in + (cmap, imap) + in + with_last_section with_sec s + +let is_in_section env gr s = + let with_sec sec = match sec with + | None -> false + | Some sec -> + let open GlobRef in + match gr with + | VarRef id -> + let vars = List.firstn sec.sec_context (Environ.named_context env) in + List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars + | ConstRef con -> + Cmap.mem con (fst sec.sec_data) + | IndRef (ind, _) | ConstructRef ((ind, _), _) -> + Mindmap.mem ind (snd sec.sec_data) + in + with_last_section with_sec s diff --git a/kernel/section.mli b/kernel/section.mli new file mode 100644 index 0000000000..ec863b3b90 --- /dev/null +++ b/kernel/section.mli @@ -0,0 +1,88 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 Univ + +(** Kernel implementation of sections. *) + +type 'a t +(** Type of sections with additional data ['a] *) + +val empty : 'a t + +val is_empty : 'a t -> bool +(** Checks whether there is no opened section *) + +val depth : 'a t -> int +(** Number of nested sections (0 if no sections are open) *) + +(** {6 Manipulating sections} *) + +type section_entry = +| SecDefinition of Constant.t +| SecInductive of MutInd.t + +val open_section : custom:'a -> 'a t -> 'a t +(** Open a new section with the provided universe polymorphic status. Sections + can be nested, with the proviso that polymorphic sections cannot appear + inside a monomorphic one. A custom data can be attached to this section, + that will be returned by {!close_section}. *) + +val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a +(** Close the current section and returns the entries defined inside, the set + of global monomorphic constraints added in this section, and the custom data + provided at the opening of the section. *) + +(** {6 Extending sections} *) + +val push_local : 'a t -> 'a t +(** Extend the current section with a local definition (cf. push_named). *) + +val push_context : Name.t array * UContext.t -> 'a t -> 'a t +(** Extend the current section with a local universe context. Assumes that the + last opened section is polymorphic. *) + +val push_constraints : ContextSet.t -> 'a t -> 'a t +(** Extend the current section with a global universe context. + Assumes that the last opened section is monomorphic. *) + +val push_constant : poly:bool -> Constant.t -> 'a t -> 'a t +(** Make the constant as having been defined in this section. *) + +val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t +(** Make the inductive block as having been defined in this section. *) + +(** {6 Retrieving section data} *) + +type abstr_info = private { + abstr_ctx : Constr.named_context; + (** Section variables of this prefix *) + abstr_subst : Univ.Instance.t; + (** Actual names of the abstracted variables *) + abstr_uctx : Univ.AUContext.t; + (** Universe quantification, same length as the substitution *) +} +(** Data needed to abstract over the section variable and universe hypotheses *) + + +val empty_segment : abstr_info +(** Nothing to abstract *) + +val segment_of_constant : Environ.env -> Constant.t -> 'a t -> abstr_info +(** Section segment at the time of the constant declaration *) + +val segment_of_inductive : Environ.env -> MutInd.t -> 'a t -> abstr_info +(** Section segment at the time of the inductive declaration *) + +val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list +(** Section segments of all declarations from this section. *) + +val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d47dc0c6e1..d22ec3b7ca 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -97,7 +97,8 @@ let check_universes error env u1 u2 = match u1, u2 with | Monomorphic _, Monomorphic _ -> env | Polymorphic auctx1, Polymorphic auctx2 -> - if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then + let lbound = Environ.universes_lbound env in + if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) else Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env diff --git a/kernel/term.ml b/kernel/term.ml index 38c0d043cf..7343507838 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -383,4 +383,4 @@ let kind_of_type t = match kind t with | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) -> AtomicType (t,[||]) - | (Lambda _ | Construct _ | Int _) -> failwith "Not a type" + | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b65e62ba30..f85b3db413 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -29,10 +29,6 @@ module NamedDecl = Context.Named.Declaration type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust - let skip_trusted_seff sl b e = let rec aux sl b e acc = let open Context.Rel.Declaration in @@ -64,7 +60,11 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> Feedback.feedback ~id:state_id Feedback.Complete) -let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = +type typing_context = +| MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option +| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option + +let infer_declaration env (dcl : constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with @@ -112,79 +112,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_relevance = Sorts.Relevant; } - (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, - so we delay the typing and hash consing of its body. *) - - | OpaqueEntry ({ opaque_entry_type = typ; - opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> - let env = push_context_set ~strict:true univs env in - let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in - let tyj = Typeops.infer_type env typ in - let proofterm = - Future.chain body begin fun ((body,uctx),side_eff) -> - (* don't redeclare universes which are declared for the type *) - let uctx = Univ.ContextSet.diff uctx univs in - let SideEffects handle = trust in - let (body, uctx', valid_signatures) = handle env body side_eff in - let uctx = Univ.ContextSet.union uctx uctx' in - let env = push_context_set uctx env in - let body,env,ectx = skip_trusted_seff valid_signatures body env in - let j = Typeops.infer env body in - let j = unzip ectx j in - let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in - let c = j.uj_val in - feedback_completion_typecheck feedback_id; - c, Opaqueproof.PrivateMonomorphic uctx - end in - let def = OpaqueDef proofterm in - { - Cooking.cook_body = def; - cook_type = tyj.utj_val; - cook_universes = Monomorphic univs; - cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = false; - cook_context = Some c.opaque_entry_secctx; - } - - (** Similar case for polymorphic entries. *) - - | OpaqueEntry ({ opaque_entry_type = typ; - opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> - let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in - let env = push_context ~strict:false uctx env in - let tj = Typeops.infer_type env typ in - let sbst, auctx = Univ.abstract_universes nas uctx in - let usubst = Univ.make_instance_subst sbst in - let proofterm = Future.chain body begin fun ((body, ctx), side_eff) -> - let SideEffects handle = trust in - let body, ctx', _ = handle env body side_eff in - let ctx = Univ.ContextSet.union ctx ctx' in - (** [ctx] must contain local universes, such that it has no impact - on the rest of the graph (up to transitivity). *) - let env = push_subgraph ctx env in - let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in - let j = Typeops.infer env body in - let _ = Typeops.judge_of_cast env j DEFAULTcast tj in - let def = Vars.subst_univs_level_constr usubst j.uj_val in - let () = feedback_completion_typecheck feedback_id in - def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) - end in - let def = OpaqueDef proofterm in - let typ = Vars.subst_univs_level_constr usubst tj.utj_val in - { - Cooking.cook_body = def; - cook_type = typ; - cook_universes = Polymorphic auctx; - cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = false; - cook_context = Some c.opaque_entry_secctx; - } - - (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in - let Pure = trust in let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in @@ -218,32 +148,66 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } +(** Definition is opaque (Qed), so we delay the typing of its body. *) +let infer_opaque env = function + | ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> + let env = push_context_set ~strict:true univs env in + let { opaque_entry_feedback = feedback_id; _ } = c in + let tyj = Typeops.infer_type env typ in + let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef () in + { + Cooking.cook_body = def; + cook_type = tyj.utj_val; + cook_universes = Monomorphic univs; + cook_relevance = Sorts.relevance_of_sort tyj.utj_type; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; + }, context + + | ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let { opaque_entry_feedback = feedback_id; _ } = c in + let env = push_context ~strict:false uctx env in + let tj = Typeops.infer_type env typ in + let sbst, auctx = Univ.abstract_universes nas uctx in + let usubst = Univ.make_instance_subst sbst in + let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef () in + let typ = Vars.subst_univs_level_constr usubst tj.utj_val in + { + Cooking.cook_body = def; + cook_type = typ; + cook_universes = Polymorphic auctx; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; + }, context + +let check_section_variables env declared_set typ body = + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env body in + let inferred_set = Environ.really_needed env (Id.Set.union ids_typ ids_def) in + if not (Id.Set.subset inferred_set declared_set) then + let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in + let n = List.length l in + let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in + let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in + let missing_vars = Pp.pr_sequence Id.print (List.rev l) in + user_err Pp.(prlist str + ["The following section "; (String.plural n "variable"); " "; + (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ + missing_vars ++ str "." ++ fnl () ++ fnl () ++ + str "You can either update your proof to not depend on " ++ missing_vars ++ + str ", or you can update your Proof line from" ++ fnl () ++ + str "Proof using " ++ declared_vars ++ fnl () ++ + str "to" ++ fnl () ++ + str "Proof using " ++ inferred_vars) + let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in - let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in - let inferred_set, declared_set = mk_set inferred, mk_set declared in - if not (Id.Set.subset inferred_set declared_set) then - let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in - let n = List.length l in - let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in - let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in - let missing_vars = Pp.pr_sequence Id.print (List.rev l) in - user_err Pp.(prlist str - ["The following section "; (String.plural n "variable"); " "; - (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ - missing_vars ++ str "." ++ fnl () ++ fnl () ++ - str "You can either update your proof to not depend on " ++ missing_vars ++ - str ", or you can update your Proof line from" ++ fnl () ++ - str "Proof using " ++ declared_vars ++ fnl () ++ - str "to" ++ fnl () ++ - str "Proof using " ++ inferred_vars) in - let sort l = - List.filter (fun decl -> - let id = NamedDecl.get_id decl in - List.exists (NamedDecl.get_id %> Names.Id.equal id) l) - (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in @@ -252,7 +216,7 @@ let build_constant_declaration env result = | None -> if List.is_empty context_ids then (* Empty section context: no need to check *) - [], def + Id.Set.empty, def else (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) @@ -264,29 +228,21 @@ let build_constant_declaration env result = (* Opaque definitions always come with their section variables *) assert false in - keep_hyps env (Id.Set.union ids_typ ids_def), def + Environ.really_needed env (Id.Set.union ids_typ ids_def), def | Some declared -> + let needed = Environ.really_needed env declared in + (* Transitive closure ensured by the upper layers *) + let () = assert (Id.Set.equal needed declared) in (* We use the declared set and chain a check of correctness *) - sort declared, + declared, match def with - | Undef _ | Primitive _ as x -> x (* nothing to check *) + | Undef _ | Primitive _ | OpaqueDef _ 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 - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in - check declared inferred; - x - | OpaqueDef lc -> (* In this case we can postpone the check *) - let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in - let kont c = - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in - check declared inferred - in - OpaqueDef (iter kont lc) + let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in + x in let univs = result.cook_universes in + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in Option.map Cemitcodes.from_val res @@ -300,11 +256,46 @@ let build_constant_declaration env result = const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } +let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = match tyenv with +| MonoTyCtx (env, tyj, univs, declared, feedback_id) -> + let ((body, uctx), side_eff) = body in + (* don't redeclare universes which are declared for the type *) + let uctx = Univ.ContextSet.diff uctx univs in + let (body, uctx', valid_signatures) = handle env body side_eff in + let uctx = Univ.ContextSet.union uctx uctx' in + let env = push_context_set uctx env in + let body,env,ectx = skip_trusted_seff valid_signatures body env in + let j = Typeops.infer env body in + let j = unzip ectx j in + let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in + let c = j.uj_val in + let () = check_section_variables env declared tyj.utj_val body in + feedback_completion_typecheck feedback_id; + c, Opaqueproof.PrivateMonomorphic uctx +| PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) -> + let ((body, ctx), side_eff) = body in + let body, ctx', _ = handle env body side_eff in + let ctx = Univ.ContextSet.union ctx ctx' in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) + let env = push_subgraph ctx env in + let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in + let j = Typeops.infer env body in + let _ = Typeops.judge_of_cast env j DEFAULTcast tj in + let () = check_section_variables env declared tj.utj_val body in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + let () = feedback_completion_typecheck feedback_id in + def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + (*s Global and local constant declaration. *) -let translate_constant mb env _kn ce = +let translate_constant env _kn ce = build_constant_declaration env - (infer_declaration ~trust:mb env ce) + (infer_declaration env ce) + +let translate_opaque env _kn ce = + let def, ctx = infer_opaque env ce in + build_constant_declaration env def, ctx let translate_local_assum env t = let j = Typeops.infer env t in @@ -317,7 +308,10 @@ let translate_recipe env _kn r = let univs = result.cook_universes in let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in let tps = Option.map Cemitcodes.from_val res in - { const_hyps = Option.get result.cook_context; + let hyps = Option.get result.cook_context in + (* Trust the set of section hypotheses generated by Cooking *) + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in + { const_hyps = hyps; const_body = result.cook_body; const_type = result.cook_type; const_body_code = tps; @@ -336,7 +330,7 @@ let translate_local_def env _id centry = const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; const_entry_inline_code = false; } in - let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in + let decl = infer_declaration env (DefinitionEntry centry) in let typ = decl.cook_type in let () = match decl.cook_universes with | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ef01ece185..c9f6d66e36 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,9 +22,7 @@ open Entries type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust +type typing_context val translate_local_def : env -> Id.t -> section_def_entry -> constr * Sorts.relevance * types @@ -32,15 +30,21 @@ val translate_local_def : env -> Id.t -> section_def_entry -> val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : - 'a trust -> env -> Constant.t -> 'a constant_entry -> - Opaqueproof.proofterm constant_body + env -> Constant.t -> constant_entry -> + 'a constant_body + +val translate_opaque : + env -> Constant.t -> 'a opaque_entry -> + unit constant_body * typing_context val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body +val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes) + (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Opaqueproof.proofterm Cooking.result +val infer_declaration : env -> + constant_entry -> typing_context Cooking.result val build_constant_declaration : env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b87384d228..1cc40a6707 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -215,14 +215,22 @@ let type_of_apply env func funt argsv argstv = (* Type of primitive constructs *) let type_of_prim_type _env = function | CPrimitives.PT_int63 -> Constr.mkSet + | CPrimitives.PT_float64 -> 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_float env = + match env.retroknowledge.Retroknowledge.retro_float64 with + | Some c -> mkConst c + | None -> raise + (Invalid_argument "Typeops.type_of_float: float64 not_defined") + let type_of_prim env t = - let int_ty = type_of_int env in + let int_ty () = type_of_int env in + let float_ty () = type_of_float env in let bool_ty () = match env.retroknowledge.Retroknowledge.retro_bool with | Some ((ind,_),_) -> Constr.mkInd ind @@ -233,6 +241,16 @@ let type_of_prim env t = | Some ((ind,_),_,_) -> Constr.mkInd ind | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") in + let f_compare_ty () = + match env.retroknowledge.Retroknowledge.retro_f_cmp with + | Some ((ind,_),_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.") + in + let f_class_ty () = + match env.retroknowledge.Retroknowledge.retro_f_class with + | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_class 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|]) @@ -243,39 +261,27 @@ let type_of_prim env t = | 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(Context.nameR (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 open CPrimitives in + let tr_prim_type = function + | PT_int63 -> int_ty () + | PT_float64 -> float_ty () in + let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with + | PIT_bool, () -> bool_ty () + | PIT_carry, t -> carry_ty (tr_prim_type t) + | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2) + | PIT_cmp, () -> compare_ty () + | PIT_f_cmp, () -> f_compare_ty () + | PIT_f_class, () -> f_class_ty () in + let tr_type = function + | PITT_ind (i, a) -> tr_ind i a + | PITT_type t -> tr_prim_type t in + let rec nary_op = function + | [] -> assert false + | [ret_ty] -> tr_type ret_ty + | arg_ty :: r -> + let arg_ty = tr_type arg_ty in + Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in + nary_op (types t) let type_of_prim_or_type env = let open CPrimitives in function @@ -285,6 +291,9 @@ let type_of_prim_or_type env = let open CPrimitives in let judge_of_int env i = make_judge (Constr.mkInt i) (type_of_int env) +let judge_of_float env f = + make_judge (Constr.mkFloat f) (type_of_float env) + (* Type of product *) let sort_of_product env domsort rangsort = @@ -583,6 +592,7 @@ let rec execute env cstr = (* Primitive types *) | Int _ -> cstr, type_of_int env + | Float _ -> cstr, type_of_float env (* Partial proofs: unsupported by the kernel *) | Meta _ -> diff --git a/kernel/typeops.mli b/kernel/typeops.mli index c71a0e0ca4..ae816fe26e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -120,6 +120,9 @@ val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit val type_of_int : env -> types val judge_of_int : env -> Uint63.t -> unsafe_judgment +val type_of_float : env -> types +val judge_of_float : env -> Float64.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/uGraph.ml b/kernel/uGraph.ml index 6fde6e9c5f..33336079bb 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -149,10 +149,10 @@ let enforce_leq_alg u v g = cg exception AlreadyDeclared = G.AlreadyDeclared -let add_universe u strict g = +let add_universe u ~lbound ~strict g = let graph = G.add u g.graph in let d = if strict then Lt else Le in - enforce_constraint (Level.set,d,u) {g with graph} + enforce_constraint (lbound,d,u) {g with graph} let add_universe_unconstrained u g = {g with graph=G.add u g.graph} @@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k (** Subtyping of polymorphic contexts *) -let check_subtype univs ctxT ctx = +let check_subtype ~lbound univs ctxT ctx = if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in - let push accu v = add_universe v false accu in + let push accu v = add_universe v ~lbound ~strict:false accu in let univs = Array.fold_left push univs (Instance.to_array inst) in let univs = merge_constraints cstT univs in check_constraints cst univs diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e1b5868d55..d90f01d8d1 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t exception AlreadyDeclared -val add_universe : Level.t -> bool -> t -> t +val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t @@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t val domain : t -> LSet.t (** Known universes *) -val check_subtype : AUContext.t check_function +val check_subtype : lbound:Level.t -> AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 5542716af2..e0bf44da35 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 val uint_size : int @@ -9,7 +19,14 @@ val to_int2 : t -> int * int (* msb, lsb *) val of_int64 : Int64.t -> t (* val of_uint : int -> t -*) + *) +(** [int_min n m] returns the minimum of [n] and [m], + [m] must be in [0, 2^30-1]. *) +val to_int_min : t -> int -> int + + (* conversion to float *) +val of_float : float -> t +val to_float : t -> float val hash : t -> int diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_31.ml index b8eccd19fb..e38389ca13 100644 --- a/kernel/uint63_i386_31.ml +++ b/kernel/uint63_31.ml @@ -26,6 +26,13 @@ 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 to_int_min n m = + if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m + +let of_float f = mask63 (Int64.of_float f) +let to_float = Int64.to_float + let hash i = let (h,l) = to_int2 i in (*Hashset.combine h l*) @@ -213,4 +220,8 @@ let () = Callback.register "uint63 one" one; Callback.register "uint63 sub" sub; Callback.register "uint63 subcarry" subcarry; - Callback.register "uint63 tail0" tail0 + Callback.register "uint63 tail0" tail0; + Callback.register "uint63 of_float" of_float; + Callback.register "uint63 to_float" to_float; + Callback.register "uint63 of_int" of_int; + Callback.register "uint63 to_int_min" to_int_min diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_63.ml index 5c4028e1c8..85b44528a7 100644 --- a/kernel/uint63_amd64_63.ml +++ b/kernel/uint63_63.ml @@ -27,6 +27,12 @@ let to_int2 i = (0,i) let of_int64 _i = assert false +let of_float = int_of_float + +external to_float : int -> (float [@unboxed]) + = "coq_uint63_to_float_byte" "coq_uint63_to_float" +[@@noalloc] + let hash i = i [@@ocaml.inline always] @@ -96,6 +102,10 @@ let le (x : int) (y : int) = (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) [@@ocaml.inline always] +let to_int_min n m = + if lt n m then n else m +[@@ocaml.inline always] + (* division of two numbers by one *) (* precondition: xh < y *) (* outputs: q, r s.t. x = q * y + r, r < y *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 414c443c4e..5d36ad54a2 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -73,6 +73,9 @@ and conv_whd env pb k whd1 whd2 cu = else raise NotConvertible | Vint64 i1, Vint64 i2 -> if Int64.equal i1 i2 then cu else raise NotConvertible + | Vfloat64 f1, Vfloat64 f2 -> + if Float64.(equal (of_float f1) (of_float f2)) 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 _ -> @@ -80,7 +83,7 @@ and conv_whd env pb k whd1 whd2 cu = conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vint64 _, _ - | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible + | Vfloat64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible and conv_atom env pb k a1 stk1 a2 stk2 cu = diff --git a/kernel/vm.ml b/kernel/vm.ml index 319a26d824..5f08720f77 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -169,7 +169,8 @@ 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 _ | Vint64 _ -> assert false + | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ -> + 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 c8f5020d71..5acdd964b1 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -57,6 +57,7 @@ type structured_constant = | Const_univ_level of Univ.Level.t | Const_val of structured_values | Const_uint of Uint63.t + | Const_float of Float64.t type reloc_table = (tag * int) array @@ -75,6 +76,8 @@ let rec eq_structured_values v1 v2 = Int.equal (Obj.size o1) (Obj.size o2) then if Int.equal t1 Obj.custom_tag then Int64.equal (Obj.magic v1 : int64) (Obj.magic v2 : int64) + else if Int.equal t1 Obj.double_tag + then Float64.(equal (of_float (Obj.magic v1)) (of_float (Obj.magic v2))) else begin assert (t1 <= Obj.last_non_constant_constructor_tag && t2 <= Obj.last_non_constant_constructor_tag); @@ -105,6 +108,8 @@ let eq_structured_constant c1 c2 = match c1, c2 with | Const_val _, _ -> false | Const_uint i1, Const_uint i2 -> Uint63.equal i1 i2 | Const_uint _, _ -> false +| Const_float f1, Const_float f2 -> Float64.equal f1 f2 +| Const_float _, _ -> false let hash_structured_constant c = let open Hashset.Combine in @@ -115,6 +120,7 @@ let hash_structured_constant c = | 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) + | Const_float f -> combinesmall 7 (Float64.hash f) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -149,6 +155,7 @@ let pp_struct_const = function | Const_univ_level l -> Univ.Level.pr l | Const_val _ -> Pp.str "(value)" | Const_uint i -> Pp.str (Uint63.to_string i) + | Const_float f -> Pp.str (Float64.to_string f) (* Abstract data *) type vprod @@ -284,6 +291,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vint64 of int64 + | Vfloat64 of float | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -315,6 +323,7 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vconstr_const _i -> str "Vconstr_const" | Vconstr_block _b -> str "Vconstr_block" | Vint64 _ -> str "Vint64" + | Vfloat64 _ -> str "Vfloat64" | Vatom_stk (_a,_stk) -> str "Vatom_stk" | Vuniv_level _ -> assert false in @@ -374,6 +383,8 @@ let rec whd_accu a stk = end | i when Int.equal i Obj.custom_tag -> Vint64 (Obj.magic i) + | i when Int.equal i Obj.double_tag -> + Vfloat64 (Obj.magic i) | tg -> CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") @@ -403,6 +414,7 @@ let whd_val : values -> whd = | 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 if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else Vconstr_block(Obj.obj o) @@ -426,6 +438,7 @@ let obj_of_str_const str = | Const_univ_level l -> Obj.repr (Vuniv_level l) | Const_val v -> Obj.repr v | Const_uint i -> Obj.repr i + | Const_float f -> Obj.repr f let val_of_block tag (args : structured_values array) = let nargs = Array.length args in @@ -675,6 +688,7 @@ and pr_whd w = | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" | Vconstr_block _b -> str "Vconstr_block" | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str + | Vfloat64 f -> str "Vfloat64(" ++ str (Float64.(to_string (of_float f))) ++ 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 d289e7db9a..9c24006ff0 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -45,6 +45,7 @@ type structured_constant = | Const_univ_level of Univ.Level.t | Const_val of structured_values | Const_uint of Uint63.t + | Const_float of Float64.t val pp_struct_const : structured_constant -> Pp.t @@ -127,6 +128,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vint64 of int64 + | Vfloat64 of float | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml deleted file mode 100644 index 57a170c8f5..0000000000 --- a/kernel/write_uint63.ml +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <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) *) -(************************************************************************) - -(** 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_i386_31.ml" - else (* 64 bits *) "uint63_amd64_63.ml") - "uint63.ml" - -let () = write_uint63 () |