From f93684a412f067622a5026c406bc76032c30b6e9 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 2 Apr 2019 22:39:32 +0200 Subject: Declare type of primitives in CPrimitives Rather than in typeops --- kernel/cPrimitives.ml | 72 +++++++++++++++++++++++++---------------------- kernel/cPrimitives.mli | 22 ++++++++++----- kernel/retroknowledge.ml | 4 +-- kernel/retroknowledge.mli | 4 +-- kernel/safe_typing.ml | 2 +- kernel/safe_typing.mli | 2 +- kernel/typeops.ml | 51 ++++++++++++--------------------- 7 files changed, 77 insertions(+), 80 deletions(-) (limited to 'kernel') diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index d854cadd15..d433cdc1ba 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -90,58 +90,62 @@ let to_string = function | Int63le -> "le" | Int63compare -> "compare" -type arg_kind = - | Kparam (* not needed for the evaluation of the primitive when it reduces *) - | Kwhnf (* need to be reduced in whnf before reducing the primitive *) - | Karg (* no need to be reduced in whnf. example: [v] in [Array.set t i v] *) +type prim_type = + | PT_int63 -type args_red = arg_kind list +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 -(* Invariant only argument of type int63 or an inductive can - have kind Kwhnf *) +type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex -let kind = function - | Int63head0 | Int63tail0 -> [Kwhnf] +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 + function + | Int63head0 | Int63tail0 -> [int_ty; int_ty] | Int63add | Int63sub | Int63mul | Int63div | Int63mod | Int63lsr | Int63lsl - | Int63land | Int63lor | Int63lxor - | Int63addc | Int63subc - | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl - | Int63eq | Int63lt | Int63le | Int63compare -> [Kwhnf; Kwhnf] + | 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] - | Int63div21 | Int63addMulDiv -> [Kwhnf; Kwhnf; Kwhnf] +type arg_kind = + | Kparam (* not needed for the evaluation of the primitive when it reduces *) + | Kwhnf (* need to be reduced in whnf before reducing the primitive *) + | Karg (* no need to be reduced in whnf. example: [v] in [Array.set t i v] *) -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 +type args_red = arg_kind list - | Int63div21 | Int63addMulDiv -> 3 +(* Invariant only argument of type int63 or an inductive can + have kind Kwhnf *) -(** Special Entries for Register **) +let arity t = List.length (types t) - 1 -type prim_ind = - | PIT_bool - | PIT_carry - | PIT_pair - | PIT_cmp +let kind t = + let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in + aux (arity t) -type prim_type = - | PT_int63 +(** Special Entries for Register **) 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" diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 6913371caf..3c825a8018 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -53,18 +53,26 @@ val kind : t -> args_red (** Special Entries for Register **) -type prim_ind = - | PIT_bool - | PIT_carry - | PIT_pair - | PIT_cmp - type prim_type = | PT_int63 +type '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 + +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/retroknowledge.ml b/kernel/retroknowledge.ml index 873c6af93d..48a6ff4c96 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -36,5 +36,5 @@ let empty = { } 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..0eb3eaf940 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -23,5 +23,5 @@ type retroknowledge = { 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/safe_typing.ml b/kernel/safe_typing.ml index e846b17aa0..52bd9a6ada 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1327,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 diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b2f6668577..ae6993b0e2 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -226,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/typeops.ml b/kernel/typeops.ml index b87384d228..a967711a83 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -243,39 +243,24 @@ 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 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 () 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 -- cgit v1.2.3 From b0b3cc67e01b165272588b2d8bc178840ba83945 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Fri, 13 Jul 2018 16:22:35 +0200 Subject: Add primitive float computation in Coq kernel Beware of 0. = -0. issue for primitive floats The IEEE 754 declares that 0. and -0. are treated equal but we cannot say that this is true with Leibniz equality. Therefore we must patch the equality and the total comparison inside the kernel to prevent inconsistency. --- kernel/cClosure.ml | 74 ++++++++++++++++++++++++++++++++++++---- kernel/cClosure.mli | 1 + kernel/cPrimitives.ml | 51 +++++++++++++++++++++++++++- kernel/cPrimitives.mli | 14 ++++++++ kernel/cbytegen.ml | 2 ++ kernel/cemitcodes.ml | 4 ++- kernel/clambda.ml | 9 +++-- kernel/clambda.mli | 1 + kernel/constr.ml | 31 +++++++++++------ kernel/constr.mli | 4 +++ kernel/float64.ml | 82 +++++++++++++++++++++++++++++++++++++++++++++ kernel/float64.mli | 52 ++++++++++++++++++++++++++++ kernel/inductive.ml | 6 ++-- kernel/inferCumulativity.ml | 1 + kernel/kernel.mllib | 1 + kernel/nativelambda.ml | 2 ++ kernel/primred.ml | 74 +++++++++++++++++++++++++++++++++++++++- kernel/primred.mli | 8 +++++ kernel/reduction.ml | 18 ++++++---- kernel/retroknowledge.ml | 4 +++ kernel/retroknowledge.mli | 2 ++ kernel/retypeops.ml | 4 +-- kernel/safe_typing.ml | 21 ++++++++++++ kernel/term.ml | 2 +- kernel/typeops.ml | 25 ++++++++++++-- kernel/typeops.mli | 3 ++ kernel/uint63.mli | 4 +++ kernel/uint63_31.ml | 4 +++ kernel/uint63_63.ml | 3 ++ kernel/vmvalues.ml | 6 ++++ kernel/vmvalues.mli | 1 + 31 files changed, 477 insertions(+), 37 deletions(-) create mode 100644 kernel/float64.ml create mode 100644 kernel/float64.mli (limited to 'kernel') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 3fd613e905..5f0da5da65 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,23 @@ 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_option = ref false + let fSome = ref dummy + let fNone = ref dummy + + let init_option retro = + match retro.Retroknowledge.retro_option with + | Some (cSome, cNone) -> + defined_option := true; + fSome := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cSome) }; + fNone := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNone) } + | None -> defined_option := false + let defined_refl = ref false let frefl = ref dummy @@ -1044,10 +1078,12 @@ 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_option !current_retro; init_refl !current_retro let check_env env = @@ -1057,6 +1093,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 +1113,18 @@ module FNativeEntries = check_env env; assert (!defined_cmp) + let check_option env = + check_env env; + assert (!defined_option) + 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 +1138,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 +1155,15 @@ module FNativeEntries = check_cmp env; !fGt + let mkSomeCmp env v = + check_cmp env; + check_option env; + { mark = mark Cstr KnownR; term = FApp(!fSome, [|!fcmp;v|]) } + + let mkNoneCmp env = + check_cmp env; + check_option env; + { mark = mark Cstr KnownR; term = FApp(!fNone, [|!fcmp|]) } end module FredNative = RedNative(FNativeEntries) @@ -1164,7 +1226,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 +1332,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 d433cdc1ba..3154ee8c75 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -33,6 +33,18 @@ type t = | Int63lt | Int63le | Int63compare + | Float64opp + | Float64abs + | Float64compare + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp let equal (p1 : t) (p2 : t) = p1 == p2 @@ -62,6 +74,18 @@ let hash = function | Int63lt -> 22 | Int63le -> 23 | Int63compare -> 24 + | Float64opp -> 25 + | Float64abs -> 26 + | Float64compare -> 27 + | Float64add -> 28 + | Float64sub -> 29 + | Float64mul -> 30 + | Float64div -> 31 + | Float64sqrt -> 32 + | Float64ofInt63 -> 33 + | Float64normfr_mantissa -> 34 + | Float64frshiftexp -> 35 + | Float64ldshiftexp -> 36 (* Should match names in nativevalues.ml *) let to_string = function @@ -89,15 +113,29 @@ let to_string = function | Int63lt -> "lt" | Int63le -> "le" | Int63compare -> "compare" + | Float64opp -> "fopp" + | Float64abs -> "fabs" + | Float64compare -> "fcompare" + | Float64add -> "fadd" + | Float64sub -> "fsub" + | Float64mul -> "fmul" + | Float64div -> "fdiv" + | Float64sqrt -> "fsqrt" + | Float64ofInt63 -> "float_of_int" + | Float64normfr_mantissa -> "normfr_mantissa" + | Float64frshiftexp -> "frshiftexp" + | Float64ldshiftexp -> "ldshiftexp" 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_option : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex @@ -107,6 +145,7 @@ 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 @@ -122,6 +161,14 @@ let types = | 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 -> [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))] + | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_option, ())] + | 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 *) @@ -130,7 +177,7 @@ 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 arity t = List.length (types t) - 1 @@ -150,9 +197,11 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_carry -> "carry" | PIT_pair -> "pair" | PIT_cmp -> "cmp" + | PIT_option -> "option" 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 3c825a8018..f9424fb09d 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -33,6 +33,18 @@ type t = | Int63lt | Int63le | Int63compare + | Float64opp + | Float64abs + | Float64compare + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp val equal : t -> t -> bool @@ -55,12 +67,14 @@ val kind : t -> args_red 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_option : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex 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..181211d237 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -234,6 +234,7 @@ let check_prim_op = function | Int63lt -> opCHECKLTINT63 | Int63le -> opCHECKLEINT63 | Int63compare -> opCHECKCOMPAREINT63 + | _ -> 0 (* TODO: BERTHOLON add float64 operations *) let emit_instr env = function | Klabel lbl -> define_label env lbl @@ -384,7 +385,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/float64.ml b/kernel/float64.ml new file mode 100644 index 0000000000..e74fd2e9f1 --- /dev/null +++ b/kernel/float64.ml @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* f + +(* OCaml give a sign to nan values which should not be displayed as all nan are + * considered equal *) +let to_string f = if is_nan f then "nan" else string_of_float f +let of_string = float_of_string + +let opp = ( ~-. ) +let abs = abs_float + +type float_comparison = Eq | Lt | Gt | NotComparable + +let compare x y = + if x < y then Lt + else + ( + if x > y then Gt + else + ( + if x = y then Eq + else NotComparable (* NaN case *) + ) + ) + +let mul = ( *. ) +let add = ( +. ) +let sub = ( -. ) +let div = ( /. ) +let sqrt = sqrt + +let of_int63 = Uint63.to_float +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 + +let eshift = 1022 + 52 (* minimum negative exponent + binary precision *) + +(* 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) + +let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) + +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. *) + +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 Util.pervasives_compare (1. /. f1) (1. /. f2) + else Util.pervasives_compare f1 f2 diff --git a/kernel/float64.mli b/kernel/float64.mli new file mode 100644 index 0000000000..fd84f9e61d --- /dev/null +++ b/kernel/float64.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* bool + +val to_string : t -> string +val of_string : string -> t + +val opp : t -> t +val abs : t -> t + +type float_comparison = Eq | Lt | Gt | NotComparable + +(** The IEEE 754 float comparison. + * NotComparable is returned if there is a NaN in the arguments *) +val compare : t -> t -> float_comparison + +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 +val normfr_mantissa : t -> Uint63.t + +(** Shifted exponent extraction *) +val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) +val ldshiftexp : t -> Uint63.t -> t + +(** Return true if two floats are equal. + * All NaN values are considered equal. *) +val equal : t -> t -> bool + +val hash : t -> int + +(** Total order relation over float values. Behaves like [Pervasives.compare].*) +val total_compare : t -> t -> int 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 index 3b8c2cd788..550c81ed82 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -102,6 +102,7 @@ let rec infer_fterm cv_pb infos variances hd stk = 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 diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 20e742d7f8..2b83c2d868 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,6 +1,7 @@ Names TransparentState Uint63 +Float64 CPrimitives Univ UGraph diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 70b3beb2dc..301773143c 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -580,6 +580,8 @@ let rec lambda_of_constr cache env sigma c = | Int i -> Luint i + | Float _ -> assert false (* native computed for primitive float not yet implemented *) + and lambda_of_app cache env sigma f args = match kind f with | Const (_kn,_u as c) -> diff --git a/kernel/primred.ml b/kernel/primred.ml index d6d0a6143a..1b9badfca9 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,12 @@ 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_option -> + let r = + match retro.retro_option with + | None -> ((ind,1), (ind,2)) + | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + { retro with retro_option = Some r } in set_retroknowledge env retro @@ -50,6 +63,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 +94,11 @@ let get_cmp_constructors env = | Some r -> r | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered") +let get_option_constructors env = + match env.retroknowledge.retro_option with + | Some r -> r + | None -> anomaly Pp.(str"Reduction of primitive: option not registered") + exception NativeDestKO module type RedNativeEntries = @@ -80,14 +109,18 @@ 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 mkSomeCmp : env -> elem -> elem + val mkNoneCmp : env -> elem end module type RedNative = @@ -116,6 +149,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 +232,39 @@ 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) + | Float64compare -> + let f1, f2 = get_float2 evd args in + (match Float64.compare f1 f2 with + | Float64.Eq -> E.mkSomeCmp env (E.mkEq env) + | Float64.Lt -> E.mkSomeCmp env (E.mkLt env) + | Float64.Gt -> E.mkSomeCmp env (E.mkGt env) + | Float64.NotComparable -> E.mkNoneCmp 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) let red_prim env evd p args = try diff --git a/kernel/primred.mli b/kernel/primred.mli index f5998982d7..b2c9ebc6ea 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -5,10 +5,13 @@ 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_option_constructors : env -> constructor * constructor exception NativeDestKO (* Should be raised by get_* functions on failure *) @@ -20,13 +23,18 @@ 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 mkSomeCmp : env -> elem -> elem + val mkNoneCmp : env -> elem end module type RedNative = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 327cb2efeb..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 diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 48a6ff4c96..a84353bdc6 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -18,20 +18,24 @@ 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_option : (constructor * constructor) option; (* Some, None *) 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_option = None; retro_refl = None; } diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0eb3eaf940..0aca296d29 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -12,11 +12,13 @@ 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_option : (constructor * constructor) option; (* Some, None *) retro_refl : constructor option; } diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml index f398e6a5da..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 @@ -105,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 52bd9a6ada..000f6125a6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1403,6 +1403,27 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = check_type_cte 1; check_name 2 "Gt"; check_type_cte 2 + | CPrimitives.PIT_option -> + check_nconstr 2; + check_name 0 "Some"; + let cSome = ob.mind_user_lc.(0) in + let s = Pp.str "the first option constructor (Some) has a wrong type" in + begin match Term.decompose_prod cSome with + | ([_,v;_,_V], codom) -> + check_if (is_Type _V) s; + check_if (Constr.equal v (mkRel 1)) s; + check_if (Constr.equal codom (mkApp (mkRel 3, [|mkRel 2|]))) s + | _ -> check_if false s + end; + check_name 1 "None"; + let cNone = ob.mind_user_lc.(1) in + let s = Pp.str "the second option constructor (None) has a wrong type" in + begin match Term.decompose_prod cNone with + | ([_,_V], codom) -> + check_if (is_Type _V) s; + check_if (Constr.equal codom (mkApp (mkRel 2, [|mkRel 1|]))) s + | _ -> check_if false s + end let register_inductive ind prim senv = check_register_ind ind prim senv.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/typeops.ml b/kernel/typeops.ml index a967711a83..a9913772f2 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 @@ -238,6 +246,11 @@ let type_of_prim env t = | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") in + let option_ty ty = + match env.retroknowledge.Retroknowledge.retro_option with + | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|]) + | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.") + in let carry_ty int_ty = match env.retroknowledge.Retroknowledge.retro_carry with | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) @@ -245,12 +258,14 @@ let type_of_prim env t = in let open CPrimitives in let tr_prim_type = function - | PT_int63 -> int_ty in + | 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 () in + | PIT_cmp, () -> compare_ty () + | PIT_option, () -> option_ty (compare_ty ()) in let tr_type = function | PITT_ind (i, a) -> tr_ind i a | PITT_type t -> tr_prim_type t in @@ -270,6 +285,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 = @@ -568,6 +586,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/uint63.mli b/kernel/uint63.mli index d22ba3468f..c7d1e36451 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -21,6 +21,10 @@ val of_int64 : Int64.t -> t val of_uint : int -> t *) + (* conversion to float *) +val of_float : float -> t +val to_float : t -> float + val hash : t -> int (* conversion to a string *) diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index b8eccd19fb..76d768e20a 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -26,6 +26,10 @@ 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 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*) diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 5c4028e1c8..4c9377b628 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -27,6 +27,9 @@ let to_int2 i = (0,i) let of_int64 _i = assert false +let of_float = int_of_float +let to_float i = Int64.to_float (to_uint64 i) + let hash i = i [@@ocaml.inline always] diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index c8f5020d71..fe3c76c960 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 @@ -105,6 +106,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 +118,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 +153,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 @@ -426,6 +431,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 diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index d289e7db9a..1e40801be0 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 -- cgit v1.2.3 From cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Thu, 19 Jul 2018 13:33:17 +0200 Subject: Add primitive floats to 'vm_compute' * This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM. --- kernel/byterun/coq_fix_code.c | 7 +- kernel/byterun/coq_interp.c | 163 ++++++++++++++++++++++++++++++++----- kernel/byterun/coq_uint63_native.h | 3 + kernel/byterun/coq_values.h | 9 +- kernel/cemitcodes.ml | 13 ++- kernel/csymtable.ml | 11 ++- kernel/float64.ml | 2 + kernel/float64.mli | 2 + kernel/genOpcodeFiles.ml | 12 +++ kernel/vconv.ml | 5 +- kernel/vm.ml | 3 +- kernel/vmvalues.ml | 8 ++ kernel/vmvalues.mli | 1 + 13 files changed, 211 insertions(+), 28 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 0865487c98..bca2cc3bd9 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -63,7 +63,12 @@ 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[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= + arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= + arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= + arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= + arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[PROJ]=2; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 4b45608ae5..55b973dcdb 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -17,6 +17,7 @@ #include #include #include +#include #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -167,38 +168,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 +1530,128 @@ 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 (CHECKCOMPAREFLOAT) { + double x, y; + print_instr("CHECKCOMPAREFLOAT"); + CheckFloat2(); + x = Double_val(accu); + y = Double_val(*sp++); + if(x < y) { + Alloc_small(accu, 1, coq_tag_Some); + Field(accu, 0) = coq_Lt; + } + else if(x > y) { + Alloc_small(accu, 1, coq_tag_Some); + Field(accu, 0) = coq_Gt; + } + else if(x == y) { + Alloc_small(accu, 1, coq_tag_Some); + Field(accu, 0) = coq_Eq; + } + else { // nan value + accu = coq_None; + } + Next; + } + + Instruct (CHECKADDFLOAT) { + print_instr("CHECKADDFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) + Double_val(*sp++)); + Next; + } + + Instruct (CHECKSUBFLOAT) { + print_instr("CHECKSUBFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) - Double_val(*sp++)); + Next; + } + + Instruct (CHECKMULFLOAT) { + print_instr("CHECKMULFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) * Double_val(*sp++)); + Next; + } + + Instruct (CHECKDIVFLOAT) { + print_instr("CHECKDIVFLOAT"); + CheckFloat2(); + Coq_copy_double(Double_val(accu) / Double_val(*sp++)); + Next; + } + + Instruct (CHECKSQRTFLOAT) { + print_instr("CHECKSQRTFLOAT"); + CheckFloat1(); + Coq_copy_double(sqrt(Double_val(accu))); + Next; + } + + Instruct (CHECKFLOATOFINT63) { + print_instr("CHECKFLOATOFINT63"); + CheckInt1(); + Coq_copy_double(uint63_to_double(accu)); + Next; + } + + Instruct (CHECKFLOATNORMFRMANTISSA) { + double f; + print_instr("CHECKFLOATNORMFRMANTISSA"); + CheckFloat1(); + f = fabs(Double_val(accu)); + if (f >= 0.5 && f < 1) { + accu = uint63_of_double(ldexp(f, DBL_MANT_DIG)); + } + else { + accu = Val_int(0); + } + Next; + } + + Instruct (CHECKFRSHIFTEXP) { + int exp; + double f; + print_instr("CHECKFRSHIFTEXP"); + CheckFloat1(); + f = frexp(Double_val(accu), &exp); + if (fpclassify(f) == FP_NORMAL) { + exp += FLOAT_EXP_SHIFT; + } + else { + exp = 0; + } + Coq_copy_double(f); + *--sp = accu; + Alloc_small(accu, 2, coq_tag_pair); + Field(accu, 0) = *sp++; + Field(accu, 1) = Val_int(exp); + Next; + } + + Instruct (CHECKLDSHIFTEXP) { + print_instr("CHECKLDSHIFTEXP"); + CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2); + Coq_copy_double(ldexp(Double_val(accu), + uint63_of_value(*sp++) - FLOAT_EXP_SHIFT)); + Next; + } + /* Debugging and machine control */ Instruct(STOP){ diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 9fbd3f83d8..a14ed5c262 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -138,3 +138,6 @@ 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(val) ((double) uint63_of_value(val)) +#define uint63_of_double(f) (Val_long((long int) f)) diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 0cf6ccf532..14f3f152bf 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -14,6 +14,8 @@ #include #include +#include + #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,9 @@ #define coq_Eq Val_int(0) #define coq_Lt Val_int(1) #define coq_Gt Val_int(2) +#define coq_tag_Some 1 +#define coq_None Val_int(0) + +#define FLOAT_EXP_SHIFT (1022 + 52) #endif /* _COQ_VALUES_ */ diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 181211d237..82dd7bd85d 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -234,7 +234,18 @@ let check_prim_op = function | Int63lt -> opCHECKLTINT63 | Int63le -> opCHECKLEINT63 | Int63compare -> opCHECKCOMPAREINT63 - | _ -> 0 (* TODO: BERTHOLON add float64 operations *) + | Float64opp -> opCHECKOPPFLOAT + | Float64abs -> opCHECKABSFLOAT + | Float64compare -> opCHECKCOMPAREFLOAT + | Float64add -> opCHECKADDFLOAT + | Float64sub -> opCHECKSUBFLOAT + | Float64mul -> opCHECKMULFLOAT + | Float64div -> opCHECKDIVFLOAT + | Float64sqrt -> opCHECKSQRTFLOAT + | Float64ofInt63 -> opCHECKFLOATOFINT63 + | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA + | Float64frshiftexp -> opCHECKFRSHIFTEXP + | Float64ldshiftexp -> opCHECKLDSHIFTEXP let emit_instr env = function | Klabel lbl -> define_label env lbl 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/float64.ml b/kernel/float64.ml index e74fd2e9f1..0b22e07e82 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -19,6 +19,8 @@ let is_nan f = f <> f let to_string f = if is_nan f then "nan" else string_of_float f let of_string = float_of_string +let of_float f = f + let opp = ( ~-. ) let abs = abs_float diff --git a/kernel/float64.mli b/kernel/float64.mli index fd84f9e61d..7ced535dc0 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -19,6 +19,8 @@ val is_nan : t -> bool val to_string : t -> string val of_string : string -> t +val of_float : float -> t + val opp : t -> t val abs : t -> t diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index a8a4ffce9c..7deffd030b 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -137,6 +137,18 @@ let opcodes = "CHECKTAIL0INT63"; "ISINT"; "AREINT2"; + "CHECKOPPFLOAT"; + "CHECKABSFLOAT"; + "CHECKCOMPAREFLOAT"; + "CHECKADDFLOAT"; + "CHECKSUBFLOAT"; + "CHECKMULFLOAT"; + "CHECKDIVFLOAT"; + "CHECKSQRTFLOAT"; + "CHECKFLOATOFINT63"; + "CHECKFLOATNORMFRMANTISSA"; + "CHECKFRSHIFTEXP"; + "CHECKLDSHIFTEXP"; "STOP" |] 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 fe3c76c960..5acdd964b1 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -76,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); @@ -289,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 @@ -320,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 @@ -379,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 ".") @@ -408,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) @@ -681,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 1e40801be0..9c24006ff0 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -128,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 -- cgit v1.2.3 From dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Fri, 3 Aug 2018 17:38:48 +0200 Subject: Put axioms on ldshiftexp and frshiftexp Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas. The shift value has been increased to 2 * emax + prec because in ldexp we want to be able to transform the smallest denormalized to the biggest float value in one call. --- kernel/byterun/coq_values.h | 2 +- kernel/float64.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 14f3f152bf..fa51b2d31f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -45,6 +45,6 @@ #define coq_tag_Some 1 #define coq_None Val_int(0) -#define FLOAT_EXP_SHIFT (1022 + 52) +#define FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ #endif /* _COQ_VALUES_ */ diff --git a/kernel/float64.ml b/kernel/float64.ml index 0b22e07e82..a625c0f551 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -51,7 +51,7 @@ let normfr_mantissa f = if f >= 0.5 && f < 1. then Uint63.of_float (ldexp f prec) else Uint63.zero -let eshift = 1022 + 52 (* minimum negative exponent + binary precision *) +let eshift = 2101 (* 2*emax + prec *) (* When calling frexp on a nan or an infinity, the returned value inside the exponent is undefined. -- cgit v1.2.3 From 79605dabb10e889ae998bf72c8483f095277e693 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 14:31:37 +0200 Subject: Change return type of primitive float comparison Replace `option comparison` with `float_comparison` (:= `FEq | FLt | FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid boxing and an extra match when using primitive float comparison. --- kernel/byterun/coq_interp.c | 11 ++++----- kernel/byterun/coq_values.h | 6 +++-- kernel/cClosure.ml | 55 +++++++++++++++++++++++++++------------------ kernel/cPrimitives.ml | 6 ++--- kernel/cPrimitives.mli | 2 +- kernel/float64.ml | 10 ++++----- kernel/float64.mli | 2 +- kernel/primred.ml | 30 +++++++++++++------------ kernel/primred.mli | 8 ++++--- kernel/retroknowledge.ml | 6 +++-- kernel/retroknowledge.mli | 4 +++- kernel/safe_typing.ml | 31 +++++++++---------------- kernel/typeops.ml | 12 +++++----- 13 files changed, 95 insertions(+), 88 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 55b973dcdb..74edd79872 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1551,19 +1551,16 @@ value coq_interprete x = Double_val(accu); y = Double_val(*sp++); if(x < y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Lt; + accu = coq_FLt; } else if(x > y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Gt; + accu = coq_FGt; } else if(x == y) { - Alloc_small(accu, 1, coq_tag_Some); - Field(accu, 0) = coq_Eq; + accu = coq_FEq; } else { // nan value - accu = coq_None; + accu = coq_FNotComparable; } Next; } diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index fa51b2d31f..c79a8f1b4f 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -42,8 +42,10 @@ #define coq_Eq Val_int(0) #define coq_Lt Val_int(1) #define coq_Gt Val_int(2) -#define coq_tag_Some 1 -#define coq_None Val_int(0) +#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 FLOAT_EXP_SHIFT (2101) /* 2*emax + prec */ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5f0da5da65..77352595f1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1052,17 +1052,22 @@ module FNativeEntries = fcmp := { mark = mark Norm KnownR; term = FInd (Univ.in_punivs icmp) } | None -> defined_cmp := false - let defined_option = ref false - let fSome = ref dummy - let fNone = ref dummy - - let init_option retro = - match retro.Retroknowledge.retro_option with - | Some (cSome, cNone) -> - defined_option := true; - fSome := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cSome) }; - fNone := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cNone) } - | None -> defined_option := 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_refl = ref false @@ -1083,7 +1088,7 @@ module FNativeEntries = init_carry !current_retro; init_pair !current_retro; init_cmp !current_retro; - init_option !current_retro; + init_f_cmp !current_retro; init_refl !current_retro let check_env env = @@ -1113,9 +1118,9 @@ module FNativeEntries = check_env env; assert (!defined_cmp) - let check_option env = + let check_f_cmp env = check_env env; - assert (!defined_option) + assert (!defined_f_cmp) let mkInt env i = check_int env; @@ -1155,15 +1160,21 @@ module FNativeEntries = check_cmp env; !fGt - let mkSomeCmp env v = - check_cmp env; - check_option env; - { mark = mark Cstr KnownR; term = FApp(!fSome, [|!fcmp;v|]) } + let mkFLt env = + check_f_cmp env; + !fFLt - let mkNoneCmp env = - check_cmp env; - check_option env; - { mark = mark Cstr KnownR; term = FApp(!fNone, [|!fcmp|]) } + let mkFEq env = + check_f_cmp env; + !fFEq + + let mkFGt env = + check_f_cmp env; + !fFGt + + let mkFNotComparable env = + check_f_cmp env; + !fFNotComparable end module FredNative = RedNative(FNativeEntries) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 3154ee8c75..d5ed2c1a06 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -135,7 +135,7 @@ type 'a prim_ind = | PIT_carry : prim_type prim_ind | PIT_pair : (prim_type * prim_type) prim_ind | PIT_cmp : unit prim_ind - | PIT_option : unit prim_ind + | PIT_f_cmp : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex @@ -165,7 +165,7 @@ let types = | Float64ofInt63 -> [int_ty; float_ty] | Float64normfr_mantissa -> [float_ty; int_ty] | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))] - | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_option, ())] + | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())] | Float64add | Float64sub | Float64mul | Float64div -> [float_ty; float_ty; float_ty] | Float64ldshiftexp -> [float_ty; int_ty; float_ty] @@ -197,7 +197,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_carry -> "carry" | PIT_pair -> "pair" | PIT_cmp -> "cmp" - | PIT_option -> "option" + | PIT_f_cmp -> "f_cmp" let prim_type_to_string = function | PT_int63 -> "int63_type" diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index f9424fb09d..3e6ec8dbcc 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -74,7 +74,7 @@ type 'a prim_ind = | PIT_carry : prim_type prim_ind | PIT_pair : (prim_type * prim_type) prim_ind | PIT_cmp : unit prim_ind - | PIT_option : unit prim_ind + | PIT_f_cmp : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex diff --git a/kernel/float64.ml b/kernel/float64.ml index a625c0f551..eebc8f35ef 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -24,17 +24,17 @@ let of_float f = f let opp = ( ~-. ) let abs = abs_float -type float_comparison = Eq | Lt | Gt | NotComparable +type float_comparison = FEq | FLt | FGt | FNotComparable let compare x y = - if x < y then Lt + if x < y then FLt else ( - if x > y then Gt + if x > y then FGt else ( - if x = y then Eq - else NotComparable (* NaN case *) + if x = y then FEq + else FNotComparable (* NaN case *) ) ) diff --git a/kernel/float64.mli b/kernel/float64.mli index 7ced535dc0..c82f1d84da 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -24,7 +24,7 @@ val of_float : float -> t val opp : t -> t val abs : t -> t -type float_comparison = Eq | Lt | Gt | NotComparable +type float_comparison = FEq | FLt | FGt | FNotComparable (** The IEEE 754 float comparison. * NotComparable is returned if there is a NaN in the arguments *) diff --git a/kernel/primred.ml b/kernel/primred.ml index 1b9badfca9..5fe700cb9a 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -49,12 +49,12 @@ 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_option -> + | PIT_f_cmp -> let r = - match retro.retro_option with - | None -> ((ind,1), (ind,2)) - | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in - { retro with retro_option = Some 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 } in set_retroknowledge env retro @@ -94,10 +94,10 @@ let get_cmp_constructors env = | Some r -> r | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered") -let get_option_constructors env = - match env.retroknowledge.retro_option with +let get_f_cmp_constructors env = + match env.retroknowledge.retro_f_cmp with | Some r -> r - | None -> anomaly Pp.(str"Reduction of primitive: option not registered") + | None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered") exception NativeDestKO @@ -119,8 +119,10 @@ module type RedNativeEntries = val mkLt : env -> elem val mkEq : env -> elem val mkGt : env -> elem - val mkSomeCmp : env -> elem -> elem - val mkNoneCmp : env -> elem + val mkFLt : env -> elem + val mkFEq : env -> elem + val mkFGt : env -> elem + val mkFNotComparable : env -> elem end module type RedNative = @@ -239,10 +241,10 @@ struct | Float64compare -> let f1, f2 = get_float2 evd args in (match Float64.compare f1 f2 with - | Float64.Eq -> E.mkSomeCmp env (E.mkEq env) - | Float64.Lt -> E.mkSomeCmp env (E.mkLt env) - | Float64.Gt -> E.mkSomeCmp env (E.mkGt env) - | Float64.NotComparable -> E.mkNoneCmp env) + | Float64.FEq -> E.mkFEq env + | Float64.FLt -> E.mkFLt env + | Float64.FGt -> E.mkFGt env + | Float64.FNotComparable -> E.mkFNotComparable env) | Float64add -> let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2) | Float64sub -> diff --git a/kernel/primred.mli b/kernel/primred.mli index b2c9ebc6ea..5531c81550 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -11,7 +11,7 @@ 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_option_constructors : env -> constructor * constructor +val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor exception NativeDestKO (* Should be raised by get_* functions on failure *) @@ -33,8 +33,10 @@ module type RedNativeEntries = val mkLt : env -> elem val mkEq : env -> elem val mkGt : env -> elem - val mkSomeCmp : env -> elem -> elem - val mkNoneCmp : env -> elem + val mkFLt : env -> elem + val mkFEq : env -> elem + val mkFGt : env -> elem + val mkFNotComparable : env -> elem end module type RedNative = diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index a84353bdc6..e897be6141 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -24,7 +24,9 @@ type retroknowledge = { retro_pair : constructor option; retro_cmp : (constructor * constructor * constructor) option; (* Eq, Lt, Gt *) - retro_option : (constructor * constructor) option; (* Some, None *) + retro_f_cmp : (constructor * constructor * constructor * constructor) + option; + (* FEq, FLt, FGt, FNotComparable *) retro_refl : constructor option; } @@ -35,7 +37,7 @@ let empty = { retro_carry = None; retro_pair = None; retro_cmp = None; - retro_option = None; + retro_f_cmp = None; retro_refl = None; } diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0aca296d29..7aaf14e176 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -18,7 +18,9 @@ type retroknowledge = { retro_pair : constructor option; retro_cmp : (constructor * constructor * constructor) option; (* Eq, Lt, Gt *) - retro_option : (constructor * constructor) option; (* Some, None *) + retro_f_cmp : (constructor * constructor * constructor * constructor) + option; + (* FEq, FLt, FGt, FNotComparable *) retro_refl : constructor option; } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 000f6125a6..241ee8ada3 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1403,27 +1403,16 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = check_type_cte 1; check_name 2 "Gt"; check_type_cte 2 - | CPrimitives.PIT_option -> - check_nconstr 2; - check_name 0 "Some"; - let cSome = ob.mind_user_lc.(0) in - let s = Pp.str "the first option constructor (Some) has a wrong type" in - begin match Term.decompose_prod cSome with - | ([_,v;_,_V], codom) -> - check_if (is_Type _V) s; - check_if (Constr.equal v (mkRel 1)) s; - check_if (Constr.equal codom (mkApp (mkRel 3, [|mkRel 2|]))) s - | _ -> check_if false s - end; - check_name 1 "None"; - let cNone = ob.mind_user_lc.(1) in - let s = Pp.str "the second option constructor (None) has a wrong type" in - begin match Term.decompose_prod cNone with - | ([_,_V], codom) -> - check_if (is_Type _V) s; - check_if (Constr.equal codom (mkApp (mkRel 2, [|mkRel 1|]))) s - | _ -> check_if false s - end + | 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 let register_inductive ind prim senv = check_register_ind ind prim senv.env; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index a9913772f2..3e79b174b8 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -241,16 +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 pair_ty fst_ty snd_ty = match env.retroknowledge.Retroknowledge.retro_pair with | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") in - let option_ty ty = - match env.retroknowledge.Retroknowledge.retro_option with - | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|ty|]) - | None -> CErrors.user_err Pp.(str"The type option must be registered before this primitive.") - in let carry_ty int_ty = match env.retroknowledge.Retroknowledge.retro_carry with | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) @@ -265,7 +265,7 @@ let type_of_prim env t = | 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_option, () -> option_ty (compare_ty ()) in + | PIT_f_cmp, () -> f_compare_ty () in let tr_type = function | PITT_ind (i, a) -> tr_ind i a | PITT_type t -> tr_prim_type t in -- cgit v1.2.3 From d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 18:56:07 +0200 Subject: Implement classify on primitive float --- kernel/byterun/coq_fix_code.c | 1 + kernel/byterun/coq_interp.c | 25 ++++++++++++++++ kernel/byterun/coq_values.h | 9 ++++++ kernel/cClosure.ml | 67 +++++++++++++++++++++++++++++++++++++++++++ kernel/cPrimitives.ml | 24 ++++++++++------ kernel/cPrimitives.mli | 2 ++ kernel/cemitcodes.ml | 1 + kernel/float64.ml | 11 +++++++ kernel/float64.mli | 5 ++++ kernel/genOpcodeFiles.ml | 1 + kernel/primred.ml | 35 ++++++++++++++++++++++ kernel/primred.mli | 13 +++++++++ kernel/retroknowledge.ml | 10 ++++++- kernel/retroknowledge.mli | 9 +++++- kernel/safe_typing.ml | 20 +++++++++++++ kernel/typeops.ml | 8 +++++- 16 files changed, 229 insertions(+), 12 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index bca2cc3bd9..fb39ca8358 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -65,6 +65,7 @@ void init_arity () { arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= + arity[CHECKCLASSIFYFLOAT]= arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 74edd79872..b862480fda 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1565,6 +1565,31 @@ value coq_interprete 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(); diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index c79a8f1b4f..b027673ac7 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -46,6 +46,15 @@ #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 */ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 77352595f1..72585e5014 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1069,6 +1069,32 @@ module FNativeEntries = { 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 @@ -1089,6 +1115,7 @@ module FNativeEntries = 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 = @@ -1122,6 +1149,10 @@ module FNativeEntries = 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 } @@ -1175,6 +1206,42 @@ module FNativeEntries = 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) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index d5ed2c1a06..02a5351ccf 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -36,6 +36,7 @@ type t = | Float64opp | Float64abs | Float64compare + | Float64classify | Float64add | Float64sub | Float64mul @@ -77,15 +78,16 @@ let hash = function | Float64opp -> 25 | Float64abs -> 26 | Float64compare -> 27 - | Float64add -> 28 - | Float64sub -> 29 - | Float64mul -> 30 - | Float64div -> 31 - | Float64sqrt -> 32 - | Float64ofInt63 -> 33 - | Float64normfr_mantissa -> 34 - | Float64frshiftexp -> 35 - | Float64ldshiftexp -> 36 + | Float64classify -> 28 + | Float64add -> 29 + | Float64sub -> 30 + | Float64mul -> 31 + | Float64div -> 32 + | Float64sqrt -> 33 + | Float64ofInt63 -> 34 + | Float64normfr_mantissa -> 35 + | Float64frshiftexp -> 36 + | Float64ldshiftexp -> 37 (* Should match names in nativevalues.ml *) let to_string = function @@ -116,6 +118,7 @@ let to_string = function | Float64opp -> "fopp" | Float64abs -> "fabs" | Float64compare -> "fcompare" + | Float64classify -> "fclassify" | Float64add -> "fadd" | Float64sub -> "fsub" | Float64mul -> "fmul" @@ -136,6 +139,7 @@ type 'a 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 @@ -166,6 +170,7 @@ let types = | Float64normfr_mantissa -> [float_ty; int_ty] | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))] | 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] @@ -198,6 +203,7 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with | 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" diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3e6ec8dbcc..af95f6c6d7 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -36,6 +36,7 @@ type t = | Float64opp | Float64abs | Float64compare + | Float64classify | Float64add | Float64sub | Float64mul @@ -75,6 +76,7 @@ type 'a 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 diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 82dd7bd85d..535034d8fa 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -237,6 +237,7 @@ let check_prim_op = function | Float64opp -> opCHECKOPPFLOAT | Float64abs -> opCHECKABSFLOAT | Float64compare -> opCHECKCOMPAREFLOAT + | Float64classify -> opCHECKCLASSIFYFLOAT | Float64add -> opCHECKADDFLOAT | Float64sub -> opCHECKSUBFLOAT | Float64mul -> opCHECKMULFLOAT diff --git a/kernel/float64.ml b/kernel/float64.ml index eebc8f35ef..7b54fd0c4b 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -38,6 +38,17 @@ let compare x y = ) ) +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 + let mul = ( *. ) let add = ( +. ) let sub = ( -. ) diff --git a/kernel/float64.mli b/kernel/float64.mli index c82f1d84da..1ad980a691 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -30,6 +30,11 @@ type float_comparison = FEq | FLt | FGt | FNotComparable * NotComparable is returned if there is a NaN in the arguments *) val compare : t -> t -> float_comparison +type float_class = + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN + +val classify : t -> float_class + val mul : t -> t -> t val add : t -> t -> t val sub : t -> t -> t diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 7deffd030b..045a1e361d 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -140,6 +140,7 @@ let opcodes = "CHECKOPPFLOAT"; "CHECKABSFLOAT"; "CHECKCOMPAREFLOAT"; + "CHECKCLASSIFYFLOAT"; "CHECKADDFLOAT"; "CHECKSUBFLOAT"; "CHECKMULFLOAT"; diff --git a/kernel/primred.ml b/kernel/primred.ml index 5fe700cb9a..cfe6c8effe 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -55,6 +55,15 @@ let add_retroknowledge env action = | 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 @@ -99,6 +108,11 @@ let get_f_cmp_constructors env = | 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 = @@ -123,6 +137,15 @@ module type RedNativeEntries = 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 = @@ -245,6 +268,18 @@ struct | 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 -> diff --git a/kernel/primred.mli b/kernel/primred.mli index 5531c81550..bbe564d8e7 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -12,6 +12,10 @@ 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 *) @@ -37,6 +41,15 @@ module type RedNativeEntries = 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/retroknowledge.ml b/kernel/retroknowledge.ml index e897be6141..479fe02295 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -27,7 +27,14 @@ type retroknowledge = { retro_f_cmp : (constructor * constructor * constructor * constructor) option; (* FEq, FLt, FGt, FNotComparable *) - retro_refl : constructor option; + 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 = { @@ -38,6 +45,7 @@ let empty = { retro_pair = None; retro_cmp = None; retro_f_cmp = None; + retro_f_class = None; retro_refl = None; } diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 7aaf14e176..2df8a00465 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -21,7 +21,14 @@ type retroknowledge = { retro_f_cmp : (constructor * constructor * constructor * constructor) option; (* FEq, FLt, FGt, FNotComparable *) - retro_refl : constructor option; + 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 diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 241ee8ada3..d3cffd1546 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1413,6 +1413,26 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = 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/typeops.ml b/kernel/typeops.ml index 3e79b174b8..1cc40a6707 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -246,6 +246,11 @@ let type_of_prim env t = | 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|]) @@ -265,7 +270,8 @@ let type_of_prim env t = | 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 () in + | 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 -- cgit v1.2.3 From 5f1270242f71a0a1da7c868967e1071d28ed83fb Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 28 Aug 2018 23:37:49 +0200 Subject: Add next_{up,down} primitive float functions --- kernel/byterun/coq_fix_code.c | 3 ++- kernel/byterun/coq_interp.c | 14 ++++++++++++++ kernel/cPrimitives.ml | 9 ++++++++- kernel/cPrimitives.mli | 2 ++ kernel/cemitcodes.ml | 2 ++ kernel/float64.ml | 18 ++++++++++++++++++ kernel/float64.mli | 3 +++ kernel/genOpcodeFiles.ml | 2 ++ kernel/primred.ml | 4 ++++ 9 files changed, 55 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index fb39ca8358..3fe77afc2d 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -69,7 +69,8 @@ void init_arity () { arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= - arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=1; + 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_interp.c b/kernel/byterun/coq_interp.c index b862480fda..06042bb753 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1674,6 +1674,20 @@ value coq_interprete Next; } + Instruct (CHECKNEXTUPFLOAT) { + print_instr("CHECKNEXTUPFLOAT"); + CheckFloat1(); + Coq_copy_double(nextafter(Double_val(accu), INFINITY)); + Next; + } + + Instruct (CHECKNEXTDOWNFLOAT) { + print_instr("CHECKNEXTDOWNFLOAT"); + CheckFloat1(); + Coq_copy_double(nextafter(Double_val(accu), -INFINITY)); + Next; + } + /* Debugging and machine control */ Instruct(STOP){ diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 02a5351ccf..342cc29a22 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -46,6 +46,8 @@ type t = | Float64normfr_mantissa | Float64frshiftexp | Float64ldshiftexp + | Float64next_up + | Float64next_down let equal (p1 : t) (p2 : t) = p1 == p2 @@ -88,6 +90,8 @@ let hash = function | Float64normfr_mantissa -> 35 | Float64frshiftexp -> 36 | Float64ldshiftexp -> 37 + | Float64next_up -> 38 + | Float64next_down -> 39 (* Should match names in nativevalues.ml *) let to_string = function @@ -128,6 +132,8 @@ let to_string = function | Float64normfr_mantissa -> "normfr_mantissa" | Float64frshiftexp -> "frshiftexp" | Float64ldshiftexp -> "ldshiftexp" + | Float64next_up -> "next_up" + | Float64next_down -> "next_down" type prim_type = | PT_int63 @@ -165,7 +171,8 @@ let types = | 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 -> [float_ty; float_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))] diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index af95f6c6d7..3cb210233d 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -46,6 +46,8 @@ type t = | Float64normfr_mantissa | Float64frshiftexp | Float64ldshiftexp + | Float64next_up + | Float64next_down val equal : t -> t -> bool diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 535034d8fa..908f84293c 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -247,6 +247,8 @@ let check_prim_op = function | Float64normfr_mantissa -> opCHECKFLOATNORMFRMANTISSA | Float64frshiftexp -> opCHECKFRSHIFTEXP | Float64ldshiftexp -> opCHECKLDSHIFTEXP + | Float64next_up -> opCHECKNEXTUPFLOAT + | Float64next_down -> opCHECKNEXTDOWNFLOAT let emit_instr env = function | Klabel lbl -> define_label env lbl diff --git a/kernel/float64.ml b/kernel/float64.ml index 7b54fd0c4b..351661f44d 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -76,6 +76,24 @@ let frshiftexp f = let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) +let eta_float = ldexp 1. (-1074) (* smallest positive float (subnormal) *) + +let next_up f = + match classify_float f with + | FP_nan -> f + | FP_infinite -> if 0. < f then f else -.max_float + | FP_zero | FP_subnormal -> + let f = f +. eta_float in + if f = 0. then -0. else f (* or next_down may return -0. *) + | FP_normal -> + let f, e = frexp f in + if 0. < f || f <> -0.5 || e = -1021 then + ldexp (f +. epsilon_float /. 2.) e + else + ldexp (-0.5 +. epsilon_float /. 4.) e + +let next_down f = -.(next_up (-.f)) + let equal f1 f2 = match classify_float f1 with | FP_normal | FP_subnormal | FP_infinite -> (f1 = f2) diff --git a/kernel/float64.mli b/kernel/float64.mli index 1ad980a691..580004126d 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -49,6 +49,9 @@ val normfr_mantissa : t -> Uint63.t val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) val ldshiftexp : t -> Uint63.t -> t +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 diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 045a1e361d..52b7a822e3 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -150,6 +150,8 @@ let opcodes = "CHECKFLOATNORMFRMANTISSA"; "CHECKFRSHIFTEXP"; "CHECKLDSHIFTEXP"; + "CHECKNEXTUPFLOAT"; + "CHECKNEXTDOWNFLOAT"; "STOP" |] diff --git a/kernel/primred.ml b/kernel/primred.ml index cfe6c8effe..2766793005 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -302,6 +302,10 @@ struct 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 -- cgit v1.2.3 From 73580b9c5f206e2d3a7107123d207515f2330978 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 23 Oct 2018 17:52:39 +0200 Subject: Add primitive floats to 'native_compute' * Float added to is_value/get_value to avoid stack overflows (cf. #7646) * beware of the use of Array.map with floats (cf. comment in the makeblock function) NB: From here one, the configure option "-native-compiler no" is no longer needed. --- kernel/float64.ml | 40 ++++++++++-- kernel/float64.mli | 27 ++++++++ kernel/nativecode.ml | 90 +++++++++++++++++++-------- kernel/nativeconv.ml | 5 +- kernel/nativelambda.ml | 15 +++-- kernel/nativelambda.mli | 1 + kernel/nativevalues.ml | 159 ++++++++++++++++++++++++++++++++++++++++++++++++ kernel/nativevalues.mli | 73 ++++++++++++++++++++++ 8 files changed, 374 insertions(+), 36 deletions(-) (limited to 'kernel') diff --git a/kernel/float64.ml b/kernel/float64.ml index 351661f44d..c0611f37a0 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -13,12 +13,21 @@ type t = float let is_nan f = f <> f +let is_infinity f = f = infinity +let is_neg_infinity f = f = neg_infinity (* OCaml give a sign to nan values which should not be displayed as all nan are * considered equal *) let to_string f = if is_nan f then "nan" else string_of_float 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 opp = ( ~-. ) @@ -37,6 +46,7 @@ let compare x y = else FNotComparable (* NaN case *) ) ) +[@@ocaml.inline always] type float_class = | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN @@ -48,19 +58,32 @@ let classify x = | 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] + +let mul x y = x *. y +[@@ocaml.inline always] + +let add x y = x +. y +[@@ocaml.inline always] + +let sub x y = x -. y +[@@ocaml.inline always] + +let div x y = x /. y +[@@ocaml.inline always] + +let sqrt x = sqrt x +[@@ocaml.inline always] -let mul = ( *. ) -let add = ( +. ) -let sub = ( -. ) -let div = ( /. ) -let sqrt = sqrt +let of_int63 x = Uint63.to_float x +[@@ocaml.inline always] -let of_int63 = Uint63.to_float 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 *) @@ -73,8 +96,10 @@ let frshiftexp f = | 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 (snd (Uint63.to_int2 e) - eshift) +[@@ocaml.inline always] let eta_float = ldexp 1. (-1074) (* smallest positive float (subnormal) *) @@ -91,14 +116,17 @@ let next_up f = ldexp (f +. epsilon_float /. 2.) e else ldexp (-0.5 +. epsilon_float /. 4.) e +[@@ocaml.inline always] let next_down f = -.(next_up (-.f)) +[@@ocaml.inline always] 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, diff --git a/kernel/float64.mli b/kernel/float64.mli index 580004126d..1e6ea8bb96 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -15,10 +15,14 @@ indistinguishable from Coq's perspective. *) type t 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 val opp : t -> t @@ -29,32 +33,55 @@ type float_comparison = FEq | FLt | FGt | FNotComparable (** 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 +[@@ocaml.inline always] + val add : t -> t -> t +[@@ocaml.inline always] + val sub : t -> t -> t +[@@ocaml.inline always] + val div : t -> t -> t +[@@ocaml.inline always] + val sqrt : t -> t +[@@ocaml.inline always] (** 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 +[@@ocaml.inline always] + val next_down : t -> t +[@@ocaml.inline always] (** 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 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 301773143c..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,7 +587,7 @@ let rec lambda_of_constr cache env sigma c = | Int i -> Luint i - | Float _ -> assert false (* native computed for primitive float not yet implemented *) + | Float f -> Lfloat f and lambda_of_app cache env sigma f args = match kind f with 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 f788832d5b..1d4fb5d39c 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -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,158 @@ let print x = flush stderr; x +(** Support for machine floating point values *) + +let is_float (x:t) = + let o = Obj.repr x in + Int.equal (Obj.tag o) Obj.double_tag +[@@ocaml.inline always] + +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 + +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..d19877c121 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,70 @@ 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 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_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] -- cgit v1.2.3 From 6133877fc097412233a60740fdf94374abb79559 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 20 Feb 2019 18:00:04 +0100 Subject: Add primitive floats to checker --- kernel/float64.ml | 11 +++++++++-- kernel/float64.mli | 3 +++ 2 files changed, 12 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/float64.ml b/kernel/float64.ml index c0611f37a0..72f0d83359 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -35,6 +35,9 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable +(* inspired by lib/util.ml; see also #10471 *) +let pervasives_compare = compare + let compare x y = if x < y then FLt else @@ -137,5 +140,9 @@ let 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 Util.pervasives_compare (1. /. f1) (1. /. f2) - else Util.pervasives_compare f1 f2 + 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] diff --git a/kernel/float64.mli b/kernel/float64.mli index 1e6ea8bb96..927594115e 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -87,3 +87,6 @@ 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] -- cgit v1.2.3 From 3e0db1b645a8653c62b8b5a4978e6d8fbbe9a9cc Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 26 Mar 2019 21:10:17 +0100 Subject: Pretty-printing primitive float constants * map special floats to registered CRef's * kernel/float64.mli: add {is_infinity, is_neg_infinity} functions * kernel/float64.ml: Replace string_of_float with a safe pretty-printing function Namely: let to_string_raw f = Printf.sprintf "%.17g" f let to_string f = if is_nan f then "nan" else to_string_raw f Summary: * printing a binary64 float in 17 decimal places and parsing it again will yield the same float, e.g.: let f1 = 1. +. (0x1p-53 +. 0x1p-105) let f2 = float_of_string (to_string f1) f1 = f2 * OCaml's string_of_float gives a sign to nan values which shouldn't be displayed as all NaNs are considered equal here. --- kernel/float64.ml | 13 ++++++++++--- kernel/float64.mli | 4 ++++ 2 files changed, 14 insertions(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/float64.ml b/kernel/float64.ml index 72f0d83359..5160d32892 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -16,9 +16,14 @@ let is_nan f = f <> f let is_infinity f = f = infinity let is_neg_infinity f = f = neg_infinity -(* OCaml give a sign to nan values which should not be displayed as all nan are - * considered equal *) -let to_string f = if is_nan f then "nan" else string_of_float f +(* 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 *) @@ -30,6 +35,8 @@ let compile f = let of_float f = f +let sign f = copysign 1. f < 0. + let opp = ( ~-. ) let abs = abs_float diff --git a/kernel/float64.mli b/kernel/float64.mli index 927594115e..acc3a556ab 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -14,6 +14,7 @@ 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 @@ -25,6 +26,9 @@ 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 -- cgit v1.2.3 From dca0135a263717b3a1a1d7c4f054f039dc08109e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 4 Apr 2019 00:14:47 +0200 Subject: Make primitive float work on x86_32 Flag -fexcess-precision=standard is not enough on x86_32 where -msse2 -mfpmath=sse is required (-msse is not enough) to avoid double rounding issues in the VM. Most floating-point operation are now implemented in C because OCaml is suffering double rounding issues on x86_32 with 80 bits extended precision registers used for floating-point values, causing double rounding making floating-point arithmetic incorrect with respect to its specification. Add a runtime test for double roundings. --- kernel/byterun/coq_float64.h | 32 +++++++++++++++++++++++ kernel/byterun/coq_interp.c | 35 +++++++++++++++---------- kernel/byterun/coq_uint63_emul.h | 15 +++++++++++ kernel/byterun/coq_uint63_native.h | 25 ++++++++++++++++-- kernel/float64.ml | 52 ++++++++++++++++++-------------------- kernel/float64.mli | 7 ----- kernel/uint63.mli | 1 + kernel/uint63_31.ml | 10 +++++++- kernel/uint63_63.ml | 7 ++++- 9 files changed, 132 insertions(+), 52 deletions(-) create mode 100644 kernel/byterun/coq_float64.h (limited to 'kernel') diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h new file mode 100644 index 0000000000..6814c31642 --- /dev/null +++ b/kernel/byterun/coq_float64.h @@ -0,0 +1,32 @@ +#ifndef _COQ_FLOAT64_ +#define _COQ_FLOAT64_ + +#include + +#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_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)) + +#endif /* _COQ_FLOAT64_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 06042bb753..e67325eb9a 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,6 +23,7 @@ #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" @@ -1593,42 +1594,42 @@ value coq_interprete Instruct (CHECKADDFLOAT) { print_instr("CHECKADDFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) + Double_val(*sp++)); + Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKSUBFLOAT) { print_instr("CHECKSUBFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) - Double_val(*sp++)); + Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKMULFLOAT) { print_instr("CHECKMULFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) * Double_val(*sp++)); + Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKDIVFLOAT) { print_instr("CHECKDIVFLOAT"); CheckFloat2(); - Coq_copy_double(Double_val(accu) / Double_val(*sp++)); + Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++))); Next; } Instruct (CHECKSQRTFLOAT) { print_instr("CHECKSQRTFLOAT"); CheckFloat1(); - Coq_copy_double(sqrt(Double_val(accu))); + Coq_copy_double(coq_fsqrt(Double_val(accu))); Next; } Instruct (CHECKFLOATOFINT63) { print_instr("CHECKFLOATOFINT63"); CheckInt1(); - Coq_copy_double(uint63_to_double(accu)); + Uint63_to_double(accu); Next; } @@ -1638,10 +1639,10 @@ value coq_interprete CheckFloat1(); f = fabs(Double_val(accu)); if (f >= 0.5 && f < 1) { - accu = uint63_of_double(ldexp(f, DBL_MANT_DIG)); + Uint63_of_double(ldexp(f, DBL_MANT_DIG)); } else { - accu = Val_int(0); + Uint63_of_int(Val_int(0)); } Next; } @@ -1660,31 +1661,39 @@ value coq_interprete } Coq_copy_double(f); *--sp = accu; +#ifdef ARCH_SIXTYFOUR Alloc_small(accu, 2, coq_tag_pair); - Field(accu, 0) = *sp++; 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); - Coq_copy_double(ldexp(Double_val(accu), - uint63_of_value(*sp++) - FLOAT_EXP_SHIFT)); + Swap_accu_sp; + Int_of_uint63(accu); + Coq_copy_double(ldexp(Double_val(*sp++), accu - FLOAT_EXP_SHIFT)); Next; } Instruct (CHECKNEXTUPFLOAT) { print_instr("CHECKNEXTUPFLOAT"); CheckFloat1(); - Coq_copy_double(nextafter(Double_val(accu), INFINITY)); + Coq_copy_double(coq_next_up(Double_val(accu))); Next; } Instruct (CHECKNEXTDOWNFLOAT) { print_instr("CHECKNEXTDOWNFLOAT"); CheckFloat1(); - Coq_copy_double(nextafter(Double_val(accu), -INFINITY)); + Coq_copy_double(coq_next_down(Double_val(accu))); Next; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 528cc6fc1f..e09803ae2d 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_UNOP(to_int_saturate) +#define Int_of_uint63(x) CALL_PREDICATE(accu, to_int_saturate, x) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index a14ed5c262..0ab374194e 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -139,5 +139,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(val) ((double) uint63_of_value(val)) -#define uint63_of_double(f) (Val_long((long int) f)) +#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 Int_of_uint63(x) do{ \ + uint64_t int_of_uint63__ = uint63_of_value(x); \ + if ((int_of_uint63__ & 0xFFFFFFFF80000000L) == 0) \ + accu = (int)int_of_uint63__; \ + else \ + accu = 0x7FFFFFFF; \ + }while(0) diff --git a/kernel/float64.ml b/kernel/float64.ml index 5160d32892..55ad472ea9 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -70,20 +70,20 @@ let classify x = | FP_nan -> NaN [@@ocaml.inline always] -let mul x y = x *. y -[@@ocaml.inline always] +external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul" +[@@unboxed] [@@noalloc] -let add x y = x +. y -[@@ocaml.inline always] +external add : float -> float -> float = "coq_fadd_byte" "coq_fadd" +[@@unboxed] [@@noalloc] -let sub x y = x -. y -[@@ocaml.inline always] +external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub" +[@@unboxed] [@@noalloc] -let div x y = x /. y -[@@ocaml.inline always] +external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv" +[@@unboxed] [@@noalloc] -let sqrt x = sqrt x -[@@ocaml.inline always] +external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt" +[@@unboxed] [@@noalloc] let of_int63 x = Uint63.to_float x [@@ocaml.inline always] @@ -111,25 +111,11 @@ let frshiftexp f = let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) [@@ocaml.inline always] -let eta_float = ldexp 1. (-1074) (* smallest positive float (subnormal) *) +external next_up : float -> float = "coq_next_up_byte" "coq_next_up" +[@@unboxed] [@@noalloc] -let next_up f = - match classify_float f with - | FP_nan -> f - | FP_infinite -> if 0. < f then f else -.max_float - | FP_zero | FP_subnormal -> - let f = f +. eta_float in - if f = 0. then -0. else f (* or next_down may return -0. *) - | FP_normal -> - let f, e = frexp f in - if 0. < f || f <> -0.5 || e = -1021 then - ldexp (f +. epsilon_float /. 2.) e - else - ldexp (-0.5 +. epsilon_float /. 4.) e -[@@ocaml.inline always] - -let next_down f = -.(next_up (-.f)) -[@@ocaml.inline always] +external next_down : float -> float = "coq_next_down_byte" "coq_next_down" +[@@unboxed] [@@noalloc] let equal f1 f2 = match classify_float f1 with @@ -153,3 +139,13 @@ let total_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 then + failwith "Detected double rounding due to the use of intermediate \ + 80 bits floating-point representation. Use of Float is \ + thus unsafe." diff --git a/kernel/float64.mli b/kernel/float64.mli index acc3a556ab..78dc1a7bd7 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -46,19 +46,14 @@ val classify : t -> float_class [@@ocaml.inline always] val mul : t -> t -> t -[@@ocaml.inline always] val add : t -> t -> t -[@@ocaml.inline always] val sub : t -> t -> t -[@@ocaml.inline always] val div : t -> t -> t -[@@ocaml.inline always] val sqrt : t -> t -[@@ocaml.inline always] (** Link with integers *) val of_int63 : Uint63.t -> t @@ -77,10 +72,8 @@ val ldshiftexp : t -> Uint63.t -> t [@@ocaml.inline always] val next_up : t -> t -[@@ocaml.inline always] val next_down : t -> t -[@@ocaml.inline always] (** Return true if two floats are equal. * All NaN values are considered equal. *) diff --git a/kernel/uint63.mli b/kernel/uint63.mli index c7d1e36451..7ed3d415e4 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -20,6 +20,7 @@ val of_int64 : Int64.t -> t (* val of_uint : int -> t *) +val to_int_saturate : t -> int (* maxuint31 in case of overflow *) (* conversion to float *) val of_float : float -> t diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 76d768e20a..a5646e87c3 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -27,6 +27,10 @@ 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_saturate i = + let r = if Int64.(equal (logand i maxuint31) i) then i else maxuint31 in + Int64.to_int r + let of_float f = mask63 (Int64.of_float f) let to_float = Int64.to_float @@ -217,4 +221,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_saturate" to_int_saturate diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 4c9377b628..1776f904d6 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -27,8 +27,13 @@ let to_int2 i = (0,i) let of_int64 _i = assert false +let to_int_saturate i = i + let of_float = int_of_float -let to_float i = Int64.to_float (to_uint64 i) + +external to_float : int -> (float [@unboxed]) + = "coq_uint63_to_float_byte" "coq_uint63_to_float" +[@@noalloc] let hash i = i [@@ocaml.inline always] -- cgit v1.2.3 From a2ba4016a64f84193261db9a52196adc39cb5767 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 12 Sep 2019 19:02:18 +0200 Subject: Reimplement is_float is_float was relying on Obj.tag triggering a check that we are in the OCaml heap which is expensive. On extreme examples, this can lead to a global 2x speedup. Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in diagnosing this. --- kernel/byterun/coq_float64.h | 4 ++++ kernel/nativevalues.ml | 6 ++---- 2 files changed, 6 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h index 6814c31642..9fc390bd33 100644 --- a/kernel/byterun/coq_float64.h +++ b/kernel/byterun/coq_float64.h @@ -29,4 +29,8 @@ 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/nativevalues.ml b/kernel/nativevalues.ml index 1d4fb5d39c..6b9d49052d 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -517,10 +517,8 @@ let print x = (** Support for machine floating point values *) -let is_float (x:t) = - let o = Obj.repr x in - Int.equal (Obj.tag o) Obj.double_tag -[@@ocaml.inline always] +external is_float : t -> bool = "coq_is_double" +[@@noalloc] let to_float (x:t) = (Obj.magic x : Float64.t) [@@ocaml.inline always] -- cgit v1.2.3 From f8fdc27f922694edf74a7b608de1596e0a1ac0e3 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Apr 2019 15:29:53 +0200 Subject: Make primitive float work on Windows --- kernel/byterun/coq_interp.c | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e67325eb9a..6e6adb1293 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1652,6 +1652,12 @@ value coq_interprete 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; -- cgit v1.2.3 From f155ba664a782f000e278d97ee5666e2e7d2adea Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Jul 2019 15:08:44 +0200 Subject: Add "==", "<", "<=" in PrimFloat.v * Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux --- kernel/byterun/coq_fix_code.c | 2 ++ kernel/byterun/coq_float64.h | 12 ++++++++++++ kernel/byterun/coq_interp.c | 27 +++++++++++++++++++++++++++ kernel/cPrimitives.ml | 10 ++++++++++ kernel/cPrimitives.mli | 3 +++ kernel/cemitcodes.ml | 3 +++ kernel/float64.ml | 9 +++++++++ kernel/float64.mli | 6 ++++++ kernel/genOpcodeFiles.ml | 5 +++++ kernel/nativevalues.ml | 21 +++++++++++++++++++++ kernel/nativevalues.mli | 12 ++++++++++++ kernel/primred.ml | 9 +++++++++ 12 files changed, 119 insertions(+) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 3fe77afc2d..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]= @@ -64,6 +65,7 @@ void init_arity () { arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= + arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]= arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= arity[CHECKCLASSIFYFLOAT]= arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h index 9fc390bd33..c41079c8ff 100644 --- a/kernel/byterun/coq_float64.h +++ b/kernel/byterun/coq_float64.h @@ -3,6 +3,15 @@ #include +#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; \ @@ -21,6 +30,9 @@ 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) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 6e6adb1293..c21aeecb16 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1545,6 +1545,33 @@ value coq_interprete 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"); diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 342cc29a22..9ff7f69203 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -35,6 +35,9 @@ type t = | Int63compare | Float64opp | Float64abs + | Float64eq + | Float64lt + | Float64le | Float64compare | Float64classify | Float64add @@ -92,6 +95,9 @@ let hash = function | Float64ldshiftexp -> 37 | Float64next_up -> 38 | Float64next_down -> 39 + | Float64eq -> 40 + | Float64lt -> 41 + | Float64le -> 42 (* Should match names in nativevalues.ml *) let to_string = function @@ -121,6 +127,9 @@ let to_string = function | Int63compare -> "compare" | Float64opp -> "fopp" | Float64abs -> "fabs" + | Float64eq -> "feq" + | Float64lt -> "flt" + | Float64le -> "fle" | Float64compare -> "fcompare" | Float64classify -> "fclassify" | Float64add -> "fadd" @@ -176,6 +185,7 @@ let types = | 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 diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3cb210233d..be65ba5305 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -35,6 +35,9 @@ type t = | Int63compare | Float64opp | Float64abs + | Float64eq + | Float64lt + | Float64le | Float64compare | Float64classify | Float64add diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 908f84293c..5e82cef810 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -236,6 +236,9 @@ let check_prim_op = function | Int63compare -> opCHECKCOMPAREINT63 | Float64opp -> opCHECKOPPFLOAT | Float64abs -> opCHECKABSFLOAT + | Float64eq -> opCHECKEQFLOAT + | Float64lt -> opCHECKLTFLOAT + | Float64le -> opCHECKLEFLOAT | Float64compare -> opCHECKCOMPAREFLOAT | Float64classify -> opCHECKCLASSIFYFLOAT | Float64add -> opCHECKADDFLOAT diff --git a/kernel/float64.ml b/kernel/float64.ml index 55ad472ea9..86b14c5cd2 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -42,6 +42,15 @@ 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 diff --git a/kernel/float64.mli b/kernel/float64.mli index 78dc1a7bd7..2aa9796526 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -34,6 +34,12 @@ 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 diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 52b7a822e3..82bb2b584d 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -139,6 +139,11 @@ let opcodes = "AREINT2"; "CHECKOPPFLOAT"; "CHECKABSFLOAT"; + "CHECKEQFLOAT"; + "CHECKLTFLOAT"; + "LTFLOAT"; + "CHECKLEFLOAT"; + "LEFLOAT"; "CHECKCOMPAREFLOAT"; "CHECKCLASSIFYFLOAT"; "CHECKADDFLOAT"; diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 6b9d49052d..e4a8344eaf 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -539,6 +539,27 @@ 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 diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index d19877c121..815ef3e98e 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -261,6 +261,9 @@ val is_float : t -> bool 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 @@ -282,6 +285,15 @@ val no_check_fopp : t -> t 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] diff --git a/kernel/primred.ml b/kernel/primred.ml index 2766793005..c475828cb3 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -261,6 +261,15 @@ struct 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 -- cgit v1.2.3 From d39fab9a7c39d8da868c4481b96cf1086c21b1a4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 10 Oct 2019 20:11:02 +0200 Subject: Fix ldshiftexp * Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel --- kernel/byterun/coq_interp.c | 3 ++- kernel/byterun/coq_uint63_emul.h | 4 ++-- kernel/byterun/coq_uint63_native.h | 9 ++++----- kernel/float64.ml | 2 +- kernel/uint63.mli | 6 ++++-- kernel/uint63_31.ml | 7 +++---- kernel/uint63_63.ml | 6 ++++-- 7 files changed, 20 insertions(+), 17 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index c21aeecb16..ca1308696c 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1711,7 +1711,8 @@ value coq_interprete print_instr("CHECKLDSHIFTEXP"); CheckPrimArgs(Is_double(accu) && Is_uint63(sp[0]), apply2); Swap_accu_sp; - Int_of_uint63(accu); + 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; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index e09803ae2d..143a6d098c 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -169,5 +169,5 @@ DECLARE_UNOP(of_float) DECLARE_UNOP(of_int) #define Uint63_of_int(x) CALL_UNOP(of_int, x) -DECLARE_UNOP(to_int_saturate) -#define Int_of_uint63(x) CALL_PREDICATE(accu, to_int_saturate, 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 0ab374194e..5be7587091 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -155,10 +155,9 @@ value coq_uint63_to_float_byte(value x) { #define Uint63_of_int(x) (accu = (x)) -#define Int_of_uint63(x) do{ \ - uint64_t int_of_uint63__ = uint63_of_value(x); \ - if ((int_of_uint63__ & 0xFFFFFFFF80000000L) == 0) \ - accu = (int)int_of_uint63__; \ +#define Uint63_to_int_min(n, m) do { \ + if (uint63_lt((n),(m))) \ + accu = (n); \ else \ - accu = 0x7FFFFFFF; \ + accu = (m); \ }while(0) diff --git a/kernel/float64.ml b/kernel/float64.ml index 86b14c5cd2..07fb25734b 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -117,7 +117,7 @@ let frshiftexp f = m, Uint63.of_int (e + eshift) [@@ocaml.inline always] -let ldshiftexp f e = ldexp f (snd (Uint63.to_int2 e) - eshift) +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" diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 7ed3d415e4..e0bf44da35 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -19,8 +19,10 @@ val to_int2 : t -> int * int (* msb, lsb *) val of_int64 : Int64.t -> t (* val of_uint : int -> t -*) -val to_int_saturate : t -> int (* maxuint31 in case of overflow *) + *) +(** [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 diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index a5646e87c3..e38389ca13 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -27,9 +27,8 @@ 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_saturate i = - let r = if Int64.(equal (logand i maxuint31) i) then i else maxuint31 in - Int64.to_int r +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 @@ -225,4 +224,4 @@ let () = 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_saturate" to_int_saturate + Callback.register "uint63 to_int_min" to_int_min diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 1776f904d6..85b44528a7 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -27,8 +27,6 @@ let to_int2 i = (0,i) let of_int64 _i = assert false -let to_int_saturate i = i - let of_float = int_of_float external to_float : int -> (float [@unboxed]) @@ -104,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 *) -- cgit v1.2.3 From 7088b2d4981496d5a2acf24566f486219237ef99 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 17 Oct 2019 18:08:36 +0200 Subject: feat: Use SSE2_MATH if available & Die if missing on x87 Co-authored-by: Pierre Roux --- kernel/float64.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/float64.ml b/kernel/float64.ml index 07fb25734b..c08069f3e3 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -155,6 +155,6 @@ let () = let b = ldexp 1. 53 in let s = add 1. (ldexp 1. (-52)) in if add b s <= b || add b 1. <> b then - failwith "Detected double rounding due to the use of intermediate \ - 80 bits floating-point representation. Use of Float is \ + failwith "Detected double-rounding due to the use of intermediate \ + 80-bit floating-point representation. Use of Float is \ thus unsafe." -- cgit v1.2.3 From 0caf27d014853693836ef06b1706502070b032f6 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 18 Oct 2019 12:12:12 +0200 Subject: Add a check for gradual underflows --- kernel/float64.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/float64.ml b/kernel/float64.ml index c08069f3e3..3e36373b77 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -154,7 +154,6 @@ let is_float64 t = let () = let b = ldexp 1. 53 in let s = add 1. (ldexp 1. (-52)) in - if add b s <= b || add b 1. <> b then - failwith "Detected double-rounding due to the use of intermediate \ - 80-bit floating-point representation. Use of Float is \ - thus unsafe." + 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." -- cgit v1.2.3 From 324072c12a164f98d0ffa8125d319ffb49df87d8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 31 Oct 2019 17:04:48 +0100 Subject: Communicate CFLAGS to dune --- kernel/byterun/dune | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'kernel') 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]") -- cgit v1.2.3