diff options
| author | Guillaume Bertholon | 2018-07-13 16:22:35 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:03 +0100 |
| commit | b0b3cc67e01b165272588b2d8bc178840ba83945 (patch) | |
| tree | 0fc62f69eb0b56a3cae6dd81f82ca869dac6fbc9 | |
| parent | f93684a412f067622a5026c406bc76032c30b6e9 (diff) | |
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.
68 files changed, 664 insertions, 91 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index aa28bce018..ccb8658eee 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -307,6 +307,8 @@ let constr_display csr = ^(array_display bl)^")" | Int i -> "Int("^(Uint63.to_string i)^")" + | Float f -> + "Float("^(Float64.to_string f)^")" and array_display v = "[|"^ @@ -439,6 +441,8 @@ let print_pure_constr csr = in print_string"{"; print_fix (); print_string"}" | Int i -> print_string ("Int("^(Uint63.to_string i)^")") + | Float f -> + print_string ("Float("^(Float64.to_string f)^")") and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 23d066df58..46a80239cf 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -76,6 +76,7 @@ let mkProj (p, c) = of_kind (Proj (p, c)) let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2)) let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2 let mkInt i = of_kind (Int i) +let mkFloat f = of_kind (Float f) let mkRef (gr,u) = let open GlobRef in match gr with | ConstRef c -> mkConstU (c,u) @@ -334,7 +335,7 @@ let iter_with_full_binders sigma g f n c = let open Context.Rel.Declaration in match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> () + | Construct _ | Int _ | Float _) -> () | Cast (c,_,t) -> f n c; f n t | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 2afce38db7..90f50b764c 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -127,6 +127,7 @@ val mkCoFix : (t, t) pcofixpoint -> t val mkArrow : t -> Sorts.relevance -> t -> t val mkArrowR : t -> t -> t val mkInt : Uint63.t -> t +val mkFloat : Float64.t -> t val mkRef : GlobRef.t * EInstance.t -> t diff --git a/engine/namegen.ml b/engine/namegen.ml index 89c2fade62..b850f38b4d 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i).binder_name with Name id -> id | _ -> assert false) - | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None + | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None in hdrec c @@ -165,6 +165,7 @@ let hdchar env sigma c = | Evar _ (* We could do better... *) | Meta _ | Case (_, _, _, _) -> "y" | Int _ -> "i" + | Float _ -> "f" in hdrec 0 c diff --git a/engine/termops.ml b/engine/termops.ml index 2ab2f60421..90fa8546ce 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -600,7 +600,7 @@ let map_constr_with_binders_left_to_right sigma g f l c = let open EConstr in match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> c + | Construct _ | Int _ | Float _) -> c | Cast (b,k,t) -> let b' = f l b in let t' = f l t in @@ -681,7 +681,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let open EConstr in match EConstr.kind sigma cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> cstr + | Construct _ | Int _ | Float _) -> cstr | Cast (c,k, t) -> let c' = f l c in let t' = f l t in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 217381d854..589df6af07 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -972,6 +972,9 @@ let rec extern inctx scopes vars r = (Numeral (SPlus, NumTok.int (Uint63.to_string i))) "int63" "int63_scope" (snd scopes) + | GFloat f -> + CPrim(String (Float64.to_string f)) + in insert_coercion coercion (CAst.make ?loc c) and extern_typ (subentry,(_,scopes)) = @@ -1314,6 +1317,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PSort Sorts.InSet -> GSort (UNamed [GSet,0]) | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i + | PFloat f -> GFloat f let extern_constr_pattern env sigma pat = extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) diff --git a/interp/impargs.ml b/interp/impargs.ml index 5f41c2a366..0de4eb5fa1 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -216,7 +216,7 @@ let rec is_rigid_head sigma t = match kind sigma t with | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i))) | _ -> is_rigid_head sigma f) | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ - | Prod _ | Meta _ | Cast _ | Int _ -> assert false + | Prod _ | Meta _ | Cast _ | Int _ | Float _ -> assert false let is_rigid env sigma t = let open Context.Rel.Declaration in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f30a874426..7e146754b2 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -90,9 +90,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | NInt i1, NInt i2 -> Uint63.equal i1 i2 +| NFloat f1, NFloat f2 -> + Float64.equal f1 f2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _ | NInt _), _ -> false + | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -222,6 +224,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) | NInt i -> GInt i + | NFloat f -> GFloat f let glob_constr_of_notation_constr ?loc x = let rec aux () x = @@ -438,6 +441,7 @@ let notation_constr_and_vars_of_glob_constr recvars a = | GCast (c,k) -> NCast (aux c,map_cast_type aux k) | GSort s -> NSort s | GInt i -> NInt i + | GFloat f -> NFloat f | GHole (w,naming,arg) -> if arg != None then has_ltac := true; NHole (w, naming, arg) @@ -627,6 +631,7 @@ let rec subst_notation_constr subst bound raw = | NSort _ -> raw | NInt _ -> raw + | NFloat _ -> raw | NHole (knd, naming, solve) -> let nknd = match knd with @@ -1196,6 +1201,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma + | GFloat f1, NFloat f2 when Float64.equal f1 f2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, NHole _ -> sigma @@ -1223,7 +1229,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _ | GInt _ ), _ -> raise No_match + | GCast _ | GInt _ | GFloat _), _ -> raise No_match and match_in u = match_ true u diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 908455bd05..c6ddd9ac95 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -44,6 +44,7 @@ type notation_constr = | NSort of glob_sort | NCast of notation_constr * notation_constr cast_type | NInt of Uint63.t + | NFloat of Float64.t (** Note concerning NList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted 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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* OCaml's float type follows the IEEE 754 Binary64 (double precision) + format *) +type t = float + +let is_nan f = f <> f + +(* 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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** [t] is currently implemented by OCaml's [float] type. + +Beware: NaNs have a sign and a payload, while they should be +indistinguishable from Coq's perspective. *) +type t + +val is_nan : t -> 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 diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index cca212f332..872f30135f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -351,7 +351,7 @@ let rec extract_type env sg db j c args = | (Info, TypeScheme) -> extract_type_app env sg db (r, type_sign env sg ty) args | (Info, Default) -> Tunknown)) - | Cast _ | LetIn _ | Construct _ | Int _ -> assert false + | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], @@ -690,6 +690,7 @@ let rec extract_term env sg mle mlt c args = let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in extract_app env sg mle mlt extract_var args | Int i -> assert (args = []); MLuint i + | Float _ -> assert false (* TODO: Implement primitive float for extraction *) | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 7be049269c..6db0a1119b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -692,13 +692,14 @@ let build_proof end | Cast(t,_,_) -> build_proof do_finalize {dyn_infos with info = t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ -> do_finalize dyn_infos g | App(_,_) -> let f,args = decompose_app sigma dyn_infos.info in begin match EConstr.kind sigma f with - | Int _ -> user_err Pp.(str "integer cannot be applied") + | Int _ -> user_err Pp.(str "integer cannot be applied") + | Float _ -> user_err Pp.(str "float cannot be applied") | App _ -> assert false (* we have collected all the app in decompose_app *) | Proj _ -> assert false (*FIXME*) | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 0452665585..6add56dd5b 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -68,7 +68,7 @@ let is_rec names = let check_id id names = Id.Set.mem id names in let rec lookup names gt = match DAst.get gt with | GVar(id) -> check_id id names - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ -> false | GCast(b,_) -> lookup names b | GRec _ -> CErrors.user_err (Pp.str "GRec not handled") | GIf(b,_,lhs,rhs) -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7c17ecdba0..895b6a37ee 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -478,7 +478,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid | GApp(_,_) -> @@ -590,6 +590,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret | GRec _ -> user_err Pp.(str "Not handled GRec") | GProd _ -> user_err Pp.(str "Cannot apply a type") | GInt _ -> user_err Pp.(str "Cannot apply an integer") + | GFloat _ -> user_err Pp.(str "Cannot apply a float") end (* end of the application treatement *) | GLambda(n,_,t,b) -> @@ -1231,7 +1232,7 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) let rec compute_cst_params relnames params gt = DAst.with_val (function - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params | GApp(f,args) -> begin match DAst.get f with | GVar relname' when Id.Set.mem relname' relnames -> diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 8abccabae6..5f54bad598 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -115,6 +115,7 @@ let change_vars = | GSort _ as x -> x | GHole _ as x -> x | GInt _ as x -> x + | GFloat _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, Glob_ops.map_cast_type (change_vars mapping) c) @@ -295,6 +296,7 @@ let rec alpha_rt excluded rt = | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ | GInt _ + | GFloat _ | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, @@ -354,7 +356,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b - | GInt _ -> false + | GInt _ | GFloat _ -> false ) x and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt @@ -447,6 +449,7 @@ let replace_var_by_term x_id term = | GSort _ | GHole _ as rt -> rt | GInt _ as rt -> rt + | GFloat _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, Glob_ops.map_cast_type replace_var_by_pattern c) @@ -529,7 +532,7 @@ let expand_as = | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map = DAst.map (function - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ as rt -> rt | GVar id as rt -> begin try diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 29356df81d..66ed1961ba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -270,7 +270,7 @@ let check_not_nested env sigma forbidden e = let rec check_not_nested e = match EConstr.kind sigma e with | Rel _ -> () - | Int _ -> () + | Int _ | Float _ -> () | Var x -> if Id.List.mem x forbidden then user_err ~hdr:"Recdef.check_not_nested" @@ -452,7 +452,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ -> let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in new_continuation_tac expr_info g diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4d7a04f5ee..9682487a22 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -319,7 +319,7 @@ let iter_constr_LR f c = match kind c with for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done | Proj(_,a) -> f a | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ - | Int _) -> () + | Int _ | Float _) -> () (* The comparison used to determine which subterms matches is KEYED *) (* CONVERSION. This looks for convertible terms that either have the same *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 43b94aed3d..520bcd6b41 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -220,14 +220,29 @@ module VNativeEntries = | _ -> raise Primred.NativeDestKO) | _ -> raise Primred.NativeDestKO + let get_float () e = + match e with + | VAL(_, cf) -> + (match kind cf with + | Float f -> f + | _ -> raise Primred.NativeDestKO) + | _ -> raise Primred.NativeDestKO + + let mkInt env i = VAL(0, mkInt i) + let mkFloat env f = VAL(0, mkFloat f) + let mkBool env b = let (ct,cf) = get_bool_constructors env in CONSTR(Univ.in_punivs (if b then ct else cf), [||]) let int_ty env = VAL(0, mkConst @@ get_int_type env) + let float_ty env = VAL(0, mkConst @@ get_float_type env) + + let cmp_ty env = VAL(0, mkConst @@ get_cmp_type env) + let mkCarry env b e = let (c0,c1) = get_carry_constructors env in CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|]) @@ -237,6 +252,12 @@ module VNativeEntries = let c = get_pair_constructor env in CONSTR(Univ.in_punivs c, [|int_ty;int_ty;e1;e2|]) + let mkFloatIntPair env f i = + let float_ty = float_ty env in + let int_ty = int_ty env in + let c = get_pair_constructor env in + CONSTR(Univ.in_punivs c, [|float_ty;int_ty;f;i|]) + let mkLt env = let (_eq,lt,_gt) = get_cmp_constructors env in CONSTR(Univ.in_punivs lt, [||]) @@ -249,6 +270,15 @@ module VNativeEntries = let (_eq,_lt,gt) = get_cmp_constructors env in CONSTR(Univ.in_punivs gt, [||]) + let mkSomeCmp env v = + let cmp_ty = cmp_ty env in + let (some,_none) = get_option_constructors env in + CONSTR(Univ.in_punivs some, [|cmp_ty;v|]) + + let mkNoneCmp env = + let cmp_ty = cmp_ty env in + let (_some,none) = get_option_constructors env in + CONSTR(Univ.in_punivs none, [|cmp_ty|]) end module VredNative = RedNative(VNativeEntries) @@ -381,7 +411,7 @@ let rec norm_head info env t stack = | Construct c -> (CONSTR(c, [||]), stack) (* neutral cases *) - | (Sort _ | Meta _ | Ind _ | Int _) -> (VAL(0, t), stack) + | (Sort _ | Meta _ | Ind _ | Int _ | Float _) -> (VAL(0, t), stack) | Prod _ -> (CBN(t,env), stack) and norm_head_ref k info env stack normt t = diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index e85c888b2e..d1cc21d82f 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -406,9 +406,10 @@ let matches_core env sigma allow_bound_rels | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> Array.fold_left2 (sorec ctx env) subst args1 args2 | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst + | PFloat f1, Float f2 when Float64.equal f1 f2 -> subst | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _ - | PFix _ | PCoFix _| PEvar _ | PInt _), _ -> raise PatternMatchingFailure + | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _), _ -> raise PatternMatchingFailure in sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c @@ -526,7 +527,7 @@ let sub_match ?(closed=true) env sigma pat c = aux env term mk_ctx next with Retyping.RetypeError _ -> next () end - | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ | Int _ -> + | Construct _|Ind _|Evar _|Const _|Rel _|Meta _|Var _|Sort _|Int _|Float _ -> next () in here next diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e8c83c7de9..5dd4772bcc 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -834,6 +834,7 @@ and detype_r d flags avoid env sigma t = | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef | Int i -> GInt i + | Float f -> GFloat f and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try @@ -1027,6 +1028,7 @@ let rec subst_glob_constr env subst = DAst.map (function | GVar _ | GEvar _ | GInt _ + | GFloat _ | GPatVar _ as raw -> raw | GApp (r,rl) as raw -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 288a349b8b..73d0c6f821 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -138,7 +138,7 @@ let flex_kind_of_term flags env evd c sk = | Evar ev -> if is_frozen flags ev then Rigid else Flexible ev - | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ -> Rigid + | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ -> Rigid | Meta _ -> Rigid | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false @@ -220,7 +220,7 @@ let occur_rigidly flags env evd (evk,_) t = (match aux c with | Rigid b -> Rigid b | _ -> Reducible) - | Meta _ | Fix _ | CoFix _ | Int _ -> Reducible + | Meta _ | Fix _ | CoFix _ | Int _ | Float _ -> Reducible in match aux t with | Rigid b -> b @@ -899,7 +899,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty only if necessary) or the second argument is potentially usable as a canonical projection or canonical value *) let rec is_unnamed (hd, args) = match EConstr.kind i hd with - | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _) -> + | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _) -> Stack.not_purely_applicative args | (CoFix _|Meta _|Rel _)-> true | Evar _ -> Stack.not_purely_applicative args @@ -1019,7 +1019,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | Const _, Const _ | Ind _, Ind _ | Construct _, Construct _ - | Int _, Int _ -> + | Int _, Int _ + | Float _, Float _ -> rigids env evd sk1 term1 sk2 term2 | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *) @@ -1064,7 +1065,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) end - | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _), _ -> + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Evar _ | Lambda _), _ -> UnifFailure (evd,NotSameHead) | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) -> UnifFailure (evd,NotSameHead) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 93f5923474..03bb633fa0 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -156,9 +156,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 | GInt i1, GInt i2 -> Uint63.equal i1 i2 + | GFloat f1, GFloat f2 -> Float64.equal f1 f2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | - GInt _), _ -> false + GInt _ | GFloat _), _ -> false let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c @@ -219,7 +220,7 @@ let map_glob_constr_left_to_right f = DAst.map (function let comp1 = f c in let comp2 = map_cast_type f k in GCast (comp1,comp2) - | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) as x -> x + | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) as x -> x ) let map_glob_constr = map_glob_constr_left_to_right @@ -251,7 +252,7 @@ let fold_glob_constr f acc = DAst.with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc ) let fold_return_type_with_binders f g v acc (na,tyopt) = Option.fold_left (f (Name.fold_right g na v)) acc tyopt @@ -293,7 +294,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in f v acc c - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc)) + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc)) let iter_glob_constr f = fold_glob_constr (fun () -> f) () diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 10e9d60fd5..44323441b6 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -91,6 +91,7 @@ type 'a glob_constr_r = | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type | GInt of Uint63.t + | GFloat of Float64.t and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 870df62500..7740628c21 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -79,7 +79,7 @@ and kind_of_head env t = | Proj (p,c) -> RigidHead RigidOther | Case (_,_,c,_) -> aux k [] c true - | Int _ -> ConstructorHead + | Int _ | Float _ -> ConstructorHead | Fix ((i,j),_) -> let n = i.(j) in try aux k [] (List.nth l n) true diff --git a/pretyping/keys.ml b/pretyping/keys.ml index f8eecd80d4..39a4a525ef 100644 --- a/pretyping/keys.ml +++ b/pretyping/keys.ml @@ -26,6 +26,7 @@ type key = | KCoFix | KRel | KInt + | KFloat module KeyOrdered = struct type t = key @@ -42,6 +43,7 @@ module KeyOrdered = struct | KCoFix -> 6 | KRel -> 7 | KInt -> 8 + | KFloat -> 9 let compare gr1 gr2 = match gr1, gr2 with @@ -135,6 +137,7 @@ let constr_key kind c = | Sort _ -> KSort | LetIn _ -> KLet | Int _ -> KInt + | Float _ -> KFloat in Some (aux c) with Not_found -> None @@ -151,6 +154,7 @@ let pr_key pr_global = function | KCoFix -> str"CoFix" | KRel -> str"Rel" | KInt -> str"Int" + | KFloat -> str"Float" let pr_keyset pr_global v = prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index e0beb383b5..2d7a152817 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -40,6 +40,7 @@ type constr_pattern = | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) | PInt of Uint63.t + | PFloat of Float64.t (** Nota : in a [PCase], the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index ccc3b6e83c..0c4312dc77 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -62,9 +62,12 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with Projection.equal p1 p2 && constr_pattern_eq t1 t2 | PInt i1, PInt i2 -> Uint63.equal i1 i2 +| PFloat f1, PFloat f2 -> + Float64.equal f1 f2 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _ - | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _), _ -> false + | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _ + | PFloat _), _ -> false (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq (i1, j1, p1) (i2, j2, p2) = @@ -92,7 +95,7 @@ let rec occur_meta_pattern = function (List.exists (fun (_,_,p) -> occur_meta_pattern p) br) | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ - | PInt _ -> false + | PInt _ | PFloat _ -> false let rec occurn_pattern n = function | PRel p -> Int.equal n p @@ -113,7 +116,7 @@ let rec occurn_pattern n = function (List.exists (fun (_,_,p) -> occurn_pattern n p) br) | PMeta _ | PSoApp _ -> true | PEvar (_,args) -> Array.exists (occurn_pattern n) args - | PVar _ | PRef _ | PSort _ | PInt _ -> false + | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false | PFix (_,(_,tl,bl)) -> Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl | PCoFix (_,(_,tl,bl)) -> @@ -136,7 +139,7 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ | PInt _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") + | PCoFix _ | PInt _ | PFloat _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> GlobRef.ConstRef sp @@ -213,7 +216,8 @@ let pattern_of_constr env sigma t = let env' = Array.fold_left2 push env lna tl in PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) - | Int i -> PInt i in + | Int i -> PInt i + | Float f -> PFloat f in pattern_of_constr env t (* To process patterns, we need a translation without typing at all. *) @@ -235,7 +239,8 @@ let map_pattern_with_binders g f l = function let l' = Array.fold_left (fun l na -> g na l) l lna in PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* Non recursive *) - | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ | PInt _ as x) -> x + | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ | PInt _ + | PFloat _ as x) -> x let error_instantiate_pattern id l = let is = match l with @@ -290,7 +295,8 @@ let rec subst_pattern env sigma subst pat = | PVar _ | PEvar _ | PRel _ - | PInt _ -> pat + | PInt _ + | PFloat _ -> pat | PProj (p,c) -> let p' = Projection.map (subst_mind subst) p in let c' = subst_pattern env sigma subst c in @@ -495,6 +501,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PCoFix (n, (names, tl, cl)) | GInt i -> PInt i + | GFloat f -> PFloat f | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ -> err ?loc (Pp.str "Non supported pattern.")) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4fed526cfc..2e1cb9ff08 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1026,6 +1026,13 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.") in inh_conv_coerce_to_tycon ?loc env sigma resj tycon + | GFloat f -> + let resj = + try Typing.judge_of_float !!env f + with Invalid_argument _ -> + user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.") + in + inh_conv_coerce_to_tycon ?loc env sigma resj tycon and pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk update = let f decl (subst,update,sigma) = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index df161b747a..12419c04bc 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -848,9 +848,17 @@ struct | Int i -> i | _ -> raise Primred.NativeDestKO + let get_float evd e = + match EConstr.kind evd e with + | Float f -> f + | _ -> raise Primred.NativeDestKO + let mkInt env i = mkInt i + let mkFloat env f = + mkFloat f + let mkBool env b = let (ct,cf) = get_bool_constructors env in mkConstruct (if b then ct else cf) @@ -865,6 +873,12 @@ struct let c = get_pair_constructor env in mkApp(mkConstruct c, [|int_ty;int_ty;e1;e2|]) + let mkFloatIntPair env f i = + let float_ty = mkConst @@ get_float_type env in + let int_ty = mkConst @@ get_int_type env in + let c = get_pair_constructor env in + mkApp(mkConstruct c, [|float_ty;int_ty;f;i|]) + let mkLt env = let (_eq, lt, _gt) = get_cmp_constructors env in mkConstruct lt @@ -877,6 +891,15 @@ struct let (_eq, _lt, gt) = get_cmp_constructors env in mkConstruct gt + let mkSomeCmp env v = + let cmp_ty = mkConst @@ get_cmp_type env in + let (some, _none) = get_option_constructors env in + mkApp(mkConstruct some, [|cmp_ty;v|]) + + let mkNoneCmp env = + let cmp_ty = mkConst @@ get_cmp_type env in + let (_some, none) = get_option_constructors env in + mkApp(mkConstruct none, [|cmp_ty|]) end module CredNative = RedNative(CNativeEntries) @@ -1135,7 +1158,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |_ -> fold () else fold () - | Int i -> + | Int _ | Float _ -> begin match Stack.strip_app stack with | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) -> let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in @@ -1238,7 +1261,7 @@ let local_whd_state_gen flags sigma = else s | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ - | Int _ -> s + | Int _ | Float _ -> s in whrec diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index cc341afac3..966c8f6e12 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -146,6 +146,7 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, t) -> t | Sort _ | Prod _ -> mkSort (sort_of env cstr) | Int _ -> EConstr.of_constr (Typeops.type_of_int env) + | Float _ -> EConstr.of_constr (Typeops.type_of_float env) and sort_of env t = match EConstr.kind sigma t with @@ -281,7 +282,7 @@ let relevance_of_term env sigma c = | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> Retypeops.relevance_of_projection env p - | Int _ -> Sorts.Relevant + | Int _ | Float _ -> Sorts.Relevant | Meta _ | Evar _ -> Sorts.Relevant diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 2db5512ff4..1a145fe1b2 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -319,6 +319,9 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) = let judge_of_int env v = Environ.on_judgment EConstr.of_constr (judge_of_int env v) +let judge_of_float env v = + Environ.on_judgment EConstr.of_constr (judge_of_float env v) + (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env sigma cstr = @@ -430,6 +433,9 @@ let rec execute env sigma cstr = | Int i -> sigma, judge_of_int env i + | Float f -> + sigma, judge_of_float env f + and execute_recdef env sigma (names,lar,vdef) = let sigma, larj = execute_array env sigma lar in let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 63fb0679f1..1b07b2bb78 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -57,3 +57,4 @@ val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment val judge_of_int : Environ.env -> Uint63.t -> unsafe_judgment +val judge_of_float : Environ.env -> Float64.t -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4d34139ec0..7147580b3d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -566,7 +566,7 @@ let is_rigid_head sigma flags t = match EConstr.kind sigma t with | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst) | Ind (i,u) -> true - | Construct _ | Int _ -> true + | Construct _ | Int _ | Float _ -> true | Fix _ | CoFix _ -> true | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _ | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _) @@ -661,7 +661,7 @@ let rec is_neutral env sigma ts t = | Evar _ | Meta _ -> true | Case (_, p, c, cl) -> is_neutral env sigma ts c | Proj (p, c) -> is_neutral env sigma ts c - | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ -> false + | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *) | Fix _ -> false (* This is an approximation *) | App _ -> assert false @@ -1821,7 +1821,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = | Cast (_, _, _) (* Is this expected? *) | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _ -> user_err Pp.(str "Match_subterm"))) + | Construct _ | Int _ | Float _ -> user_err Pp.(str "Match_subterm"))) in try matchrec cl with ex when precatchable_exception ex -> @@ -1890,7 +1890,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = | Cast (_, _, _) -> fail "Match_subterm" (* Is this expected? *) | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _ -> fail "Match_subterm")) + | Construct _ | Int _ | Float _ -> fail "Match_subterm")) in let res = matchrec cl [] in diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index ccd7a818b9..58db147b10 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -45,6 +45,7 @@ struct | DFix of int array * int * 't array * 't array | DCoFix of int * 't array * 't array | DInt of Uint63.t + | DFloat of Float64.t (* special constructors only inside the left-hand side of DCtx or DApp. Used to encode lists of foralls/letins/apps as contexts *) @@ -63,6 +64,7 @@ struct | DFix _ -> str "fix" | DCoFix _ -> str "cofix" | DInt _ -> str "INT" + | DFloat _ -> str "FLOAT" | DCons ((t,dopt),tl) -> f t ++ (match dopt with Some t' -> str ":=" ++ f t' | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl @@ -74,7 +76,7 @@ struct *) let map f = function - | (DRel | DSort | DNil | DRef _ | DInt _) as c -> c + | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) as c -> c | DCtx (ctx,c) -> DCtx (f ctx, f c) | DLambda (t,c) -> DLambda (f t, f c) | DApp (t,u) -> DApp (f t,f u) @@ -151,6 +153,10 @@ struct | DInt _, _ -> -1 | _, DInt _ -> 1 + | DFloat f1, DFloat f2 -> Float64.total_compare f1 f2 + + | DFloat _, _ -> -1 | _, DFloat _ -> 1 + | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) -> let c = cmp t1 t2 in if Int.equal c 0 then @@ -163,7 +169,7 @@ struct | DNil, DNil -> 0 let fold f acc = function - | (DRel | DNil | DSort | DRef _ | DInt _) -> acc + | (DRel | DNil | DSort | DRef _ | DInt _ | DFloat _) -> acc | DCtx (ctx,c) -> f (f acc ctx) c | DLambda (t,c) -> f (f acc t) c | DApp (t,u) -> f (f acc t) u @@ -175,7 +181,7 @@ struct | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u let choose f = function - | (DRel | DSort | DNil | DRef _ | DInt _) -> invalid_arg "choose" + | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) -> invalid_arg "choose" | DCtx (ctx,c) -> f ctx | DLambda (t,c) -> f t | DApp (t,u) -> f u @@ -192,7 +198,7 @@ struct then invalid_arg "fold2:compare" else match c1,c2 with | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _ - | DInt _, DInt _) -> acc + | DInt _, DInt _ | DFloat _, DFloat _) -> acc | (DCtx (c1,t1), DCtx (c2,t2) | DApp (c1,t1), DApp (c2,t2) | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2 @@ -205,7 +211,7 @@ struct | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ - | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = let head w = map (fun _ -> ()) w in @@ -213,7 +219,7 @@ struct then invalid_arg "map2_t:compare" else match c1,c2 with | (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _ - | DInt _, DInt _) as cc -> + | DInt _, DInt _ | DFloat _, DFloat _) as cc -> let (c,_) = cc in c | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2) | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2) @@ -227,10 +233,10 @@ struct | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ - | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false let terminal = function - | (DRel | DSort | DNil | DRef _ | DInt _) -> true + | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) -> true | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ -> false @@ -325,6 +331,7 @@ struct | Proj (p,c) -> Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c)) | Int i -> Term (DInt i) + | Float f -> Term (DFloat f) and ctx_of_constr ctx c = match Constr.kind c with | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 0268e8f9ef..6ab80575dd 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -450,6 +450,7 @@ let () = define1 "constr_kind" constr begin fun c -> |] | Int n -> v_blk 17 [|Value.of_uint63 n|] + | Float _ -> assert false end end diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 98fe436a22..5822a1a586 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -248,6 +248,7 @@ let build_beq_scheme mode kn = | Meta _ -> raise (EqUnknown "meta-variable") | Evar _ -> raise (EqUnknown "existential variable") | Int _ -> raise (EqUnknown "int") + | Float _ -> raise (EqUnknown "float") in aux t in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1387ca4675..78e4c89521 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -244,7 +244,8 @@ GRAMMAR EXTEND Gram ; register_type_token: - [ [ "#int63_type" -> { CPrimitives.PT_int63 } ] ] + [ [ "#int63_type" -> { CPrimitives.PT_int63 } + | "#float64_type" -> { CPrimitives.PT_float64 } ] ] ; register_prim_token: @@ -272,6 +273,18 @@ GRAMMAR EXTEND Gram | "#int63_lt" -> { CPrimitives.Int63lt } | "#int63_le" -> { CPrimitives.Int63le } | "#int63_compare" -> { CPrimitives.Int63compare } + | "#float64_opp" -> { CPrimitives.Float64opp } + | "#float64_abs" -> { CPrimitives.Float64abs } + | "#float64_compare" -> { CPrimitives.Float64compare } + | "#float64_add" -> { CPrimitives.Float64add } + | "#float64_sub" -> { CPrimitives.Float64sub } + | "#float64_mul" -> { CPrimitives.Float64mul } + | "#float64_div" -> { CPrimitives.Float64div } + | "#float64_sqrt" -> { CPrimitives.Float64sqrt } + | "#float64_of_int63" -> { CPrimitives.Float64ofInt63 } + | "#float64_normfr_mantissa" -> { CPrimitives.Float64normfr_mantissa } + | "#float64_frshiftexp" -> { CPrimitives.Float64frshiftexp } + | "#float64_ldshiftexp" -> { CPrimitives.Float64ldshiftexp } ] ] ; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7aa053e029..ec32c83670 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1847,6 +1847,7 @@ let vernac_register qid r = | "ind_carry" -> CPrimitives.(PIE PIT_carry) | "ind_pair" -> CPrimitives.(PIE PIT_pair) | "ind_cmp" -> CPrimitives.(PIE PIT_cmp) + | "ind_option" -> CPrimitives.(PIE PIT_option) | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace") in match gr with |