aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml74
-rw-r--r--kernel/cClosure.mli1
-rw-r--r--kernel/cPrimitives.ml51
-rw-r--r--kernel/cPrimitives.mli14
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/cemitcodes.ml4
-rw-r--r--kernel/clambda.ml9
-rw-r--r--kernel/clambda.mli1
-rw-r--r--kernel/constr.ml31
-rw-r--r--kernel/constr.mli4
-rw-r--r--kernel/float64.ml82
-rw-r--r--kernel/float64.mli52
-rw-r--r--kernel/inductive.ml6
-rw-r--r--kernel/inferCumulativity.ml1
-rw-r--r--kernel/kernel.mllib1
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/primred.ml74
-rw-r--r--kernel/primred.mli8
-rw-r--r--kernel/reduction.ml18
-rw-r--r--kernel/retroknowledge.ml4
-rw-r--r--kernel/retroknowledge.mli2
-rw-r--r--kernel/retypeops.ml4
-rw-r--r--kernel/safe_typing.ml21
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/typeops.ml25
-rw-r--r--kernel/typeops.mli3
-rw-r--r--kernel/uint63.mli4
-rw-r--r--kernel/uint63_31.ml4
-rw-r--r--kernel/uint63_63.ml3
-rw-r--r--kernel/vmvalues.ml6
-rw-r--r--kernel/vmvalues.mli1
31 files changed, 477 insertions, 37 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:17:19 +0000