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. --- pretyping/cbv.ml | 32 +++++++++++++++++++++++++++++++- pretyping/constr_matching.ml | 5 +++-- pretyping/detyping.ml | 2 ++ pretyping/evarconv.ml | 11 ++++++----- pretyping/glob_ops.ml | 9 +++++---- pretyping/glob_term.ml | 1 + pretyping/heads.ml | 2 +- pretyping/keys.ml | 4 ++++ pretyping/pattern.ml | 1 + pretyping/patternops.ml | 21 ++++++++++++++------- pretyping/pretyping.ml | 7 +++++++ pretyping/reductionops.ml | 27 +++++++++++++++++++++++++-- pretyping/retyping.ml | 3 ++- pretyping/typing.ml | 6 ++++++ pretyping/typing.mli | 1 + pretyping/unification.ml | 8 ++++---- 16 files changed, 113 insertions(+), 27 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3 From cc7dfa82705b64d1cf43408244ef6c7dd930a6e9 Mon Sep 17 00:00:00 2001 From: Guillaume Bertholon Date: Thu, 19 Jul 2018 13:33:17 +0200 Subject: Add primitive floats to 'vm_compute' * This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM. --- pretyping/vnorm.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index da0a92f284..d15eb578c3 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -169,6 +169,7 @@ and nf_whd env sigma whd typ = let args = nf_bargs env sigma b ofs ctyp in mkApp(capp,args) | Vint64 i -> i |> Uint63.of_int64 |> mkInt + | Vfloat64 f -> f |> Float64.of_float |> mkFloat | Vatom_stk(Aid idkey, stk) -> constr_type_of_idkey env sigma idkey stk | Vatom_stk(Aind ((mi,i) as ind), stk) -> -- 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. --- pretyping/cbv.ml | 24 ++++++++++++++---------- pretyping/reductionops.ml | 24 +++++++++++++++--------- 2 files changed, 29 insertions(+), 19 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 520bcd6b41..bac13a0bd7 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -241,8 +241,6 @@ module VNativeEntries = 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|]) @@ -270,15 +268,21 @@ 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 mkFLt env = + let (_eq,lt,_gt,_nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs lt, [||]) + + let mkFEq env = + let (eq,_lt,_gt,_nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs eq, [||]) + + let mkFGt env = + let (_eq,_lt,gt,_nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs gt, [||]) - 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|]) + let mkFNotComparable env = + let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs nc, [||]) end module VredNative = RedNative(VNativeEntries) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 12419c04bc..321c64e411 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -891,15 +891,21 @@ 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|]) + let mkFLt env = + let (_eq, lt, _gt, _nc) = get_f_cmp_constructors env in + mkConstruct lt + + let mkFEq env = + let (eq, _lt, _gt, _nc) = get_f_cmp_constructors env in + mkConstruct eq + + let mkFGt env = + let (_eq, _lt, gt, _nc) = get_f_cmp_constructors env in + mkConstruct gt + + let mkFNotComparable env = + let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in + mkConstruct nc end module CredNative = RedNative(CNativeEntries) -- 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 --- pretyping/cbv.ml | 46 +++++++++++++++++++++++++++++++++++++++++++++- pretyping/reductionops.ml | 45 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 90 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index bac13a0bd7..c78f791a5a 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -228,7 +228,6 @@ module VNativeEntries = | _ -> raise Primred.NativeDestKO) | _ -> raise Primred.NativeDestKO - let mkInt env i = VAL(0, mkInt i) let mkFloat env f = VAL(0, mkFloat f) @@ -283,6 +282,51 @@ module VNativeEntries = let mkFNotComparable env = let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in CONSTR(Univ.in_punivs nc, [||]) + + let mkPNormal env = + let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs pNormal, [||]) + + let mkNNormal env = + let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs nNormal, [||]) + + let mkPSubn env = + let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs pSubn, [||]) + + let mkNSubn env = + let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs nSubn, [||]) + + let mkPZero env = + let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs pZero, [||]) + + let mkNZero env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs nZero, [||]) + + let mkPInf env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs pInf, [||]) + + let mkNInf env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs nInf, [||]) + + let mkNaN env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) = + get_f_class_constructors env in + CONSTR(Univ.in_punivs nan, [||]) end module VredNative = RedNative(VNativeEntries) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 321c64e411..2952466fbb 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -906,6 +906,51 @@ struct let mkFNotComparable env = let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in mkConstruct nc + + let mkPNormal env = + let (pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + mkConstruct pNormal + + let mkNNormal env = + let (_pNormal,nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + mkConstruct nNormal + + let mkPSubn env = + let (_pNormal,_nNormal,pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + mkConstruct pSubn + + let mkNSubn env = + let (_pNormal,_nNormal,_pSubn,nSubn,_pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + mkConstruct nSubn + + let mkPZero env = + let (_pNormal,_nNormal,_pSubn,_nSubn,pZero,_nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + mkConstruct pZero + + let mkNZero env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,nZero,_pInf,_nInf,_nan) = + get_f_class_constructors env in + mkConstruct nZero + + let mkPInf env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,pInf,_nInf,_nan) = + get_f_class_constructors env in + mkConstruct pInf + + let mkNInf env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,nInf,_nan) = + get_f_class_constructors env in + mkConstruct nInf + + let mkNaN env = + let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) = + get_f_class_constructors env in + mkConstruct nan end module CredNative = RedNative(CNativeEntries) -- cgit v1.2.3 From 73580b9c5f206e2d3a7107123d207515f2330978 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 23 Oct 2018 17:52:39 +0200 Subject: Add primitive floats to 'native_compute' * Float added to is_value/get_value to avoid stack overflows (cf. #7646) * beware of the use of Array.map with floats (cf. comment in the makeblock function) NB: From here one, the configure option "-native-compiler no" is no longer needed. --- pretyping/nativenorm.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'pretyping') diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index e5aed300a2..0178d5c009 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -208,6 +208,7 @@ let rec nf_val env sigma v typ = mkLambda(name,dom,body) | Vconst n -> construct_of_constr_const env sigma n typ | Vint64 i -> i |> Uint63.of_int64 |> mkInt + | Vfloat64 f -> f |> Float64.of_float |> mkFloat | Vblock b -> let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in let args = nf_bargs env sigma b ctyp in -- cgit v1.2.3