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 +++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 68 insertions(+), 6 deletions(-) (limited to 'kernel/cClosure.ml') 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 *) -- 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/cClosure.ml | 55 ++++++++++++++++++++++++++++++++---------------------- 1 file changed, 33 insertions(+), 22 deletions(-) (limited to 'kernel/cClosure.ml') 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) -- 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/cClosure.ml | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) (limited to 'kernel/cClosure.ml') 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) -- cgit v1.2.3