Commit ef6b3f12 authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

Farith2

parent f7659f5f
File added
open BinInt
open Binary
open BinarySingleNaN
open Bits
open Datatypes
open SpecFloat
module B32 =
struct
(** val prec : Farith_Big.big_int **)
let prec =
(Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.succ_double Farith_Big.one))))
(** val emax : Farith_Big.big_int **)
let emax =
(Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.double Farith_Big.one)))))))
(** val mw : Farith_Big.big_int **)
let mw =
(Farith_Big.succ_double (Farith_Big.succ_double (Farith_Big.succ_double
(Farith_Big.double Farith_Big.one))))
(** val ew : Farith_Big.big_int **)
let ew =
(Farith_Big.double (Farith_Big.double (Farith_Big.double Farith_Big.one)))
type t = binary_float
(** val add : Farith_Big.mode -> t -> t -> t **)
let add =
coq_Bplus prec emax
(** val sub : Farith_Big.mode -> t -> t -> t **)
let sub =
coq_Bminus prec emax
(** val mult : Farith_Big.mode -> t -> t -> t **)
let mult =
coq_Bmult prec emax
(** val div : Farith_Big.mode -> t -> t -> t **)
let div =
coq_Bdiv prec emax
(** val sqrt : Farith_Big.mode -> t -> t **)
let sqrt =
coq_Bsqrt prec emax
(** val abs : t -> t **)
let abs =
coq_Babs prec emax
(** val le : t -> t -> bool **)
let le =
coq_Bleb prec emax
(** val lt : t -> t -> bool **)
let lt =
coq_Bltb prec emax
(** val eq : t -> t -> bool **)
let eq =
coq_Beqb prec emax
(** val ge : t -> t -> bool **)
let ge x y =
coq_Bleb prec emax y x
(** val gt : t -> t -> bool **)
let gt x y =
coq_Bltb prec emax y x
(** val of_bits : Farith_Big.big_int -> t **)
let of_bits b =
match binary_float_of_bits mw ew b with
| Binary.B754_zero s -> B754_zero s
| Binary.B754_infinity s -> B754_infinity s
| Binary.B754_nan (_, _) -> B754_nan
| Binary.B754_finite (s, m, e) -> B754_finite (s, m, e)
(** val pl_cst : Farith_Big.big_int **)
let pl_cst =
Farith_Big.iter_nat (fun x -> Farith_Big.double x)
(Z.to_nat (Farith_Big.pred mw)) Farith_Big.one
(** val to_bits : t -> Farith_Big.big_int **)
let to_bits = function
| B754_zero s -> bits_of_binary_float mw ew (Binary.B754_zero s)
| B754_infinity s -> bits_of_binary_float mw ew (Binary.B754_infinity s)
| B754_nan -> bits_of_binary_float mw ew (Binary.B754_nan (true, pl_cst))
| B754_finite (s, m, e) ->
bits_of_binary_float mw ew (Binary.B754_finite (s, m, e))
(** val of_q : Farith_Big.mode -> Q.t -> t **)
let of_q m q =
match Q.classify q with
| Q.INF -> B754_infinity false
| Q.MINF -> B754_infinity true
| Q.UNDEF -> B754_nan
| Q.ZERO -> B754_zero false
| Q.NZERO ->
(Farith_Big.z_case
(fun _ -> B754_nan)
(fun pn ->
coq_SF2B prec emax
(let (p, lz) =
coq_SFdiv_core_binary prec emax pn Farith_Big.zero
(Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero
in
let (mz, ez) = p in
binary_round_aux prec emax m (xorb false false) mz ez lz))
(fun nn ->
coq_SF2B prec emax
(let (p, lz) =
coq_SFdiv_core_binary prec emax nn Farith_Big.zero
(Z.to_pos (Farith_Big.q_den q)) Farith_Big.zero
in
let (mz, ez) = p in
binary_round_aux prec emax m (xorb true false) mz ez lz))
(Farith_Big.q_num q))
end
open BinInt
open Binary
open BinarySingleNaN
open Bits
open Datatypes
open SpecFloat
module B32 :
sig
val prec : Farith_Big.big_int
val emax : Farith_Big.big_int
val mw : Farith_Big.big_int
val ew : Farith_Big.big_int
type t = binary_float
val add : Farith_Big.mode -> t -> t -> t
val sub : Farith_Big.mode -> t -> t -> t
val mult : Farith_Big.mode -> t -> t -> t
val div : Farith_Big.mode -> t -> t -> t
val sqrt : Farith_Big.mode -> t -> t
val abs : t -> t
val le : t -> t -> bool
val lt : t -> t -> bool
val eq : t -> t -> bool
val ge : t -> t -> bool
val gt : t -> t -> bool
val of_bits : Farith_Big.big_int -> t
val pl_cst : Farith_Big.big_int
val to_bits : t -> Farith_Big.big_int
val of_q : Farith_Big.mode -> Q.t -> t
end
module Z =
struct
type t = Farith_Big.big_int
(** val pow :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let pow x y =
Farith_Big.z_case
(fun _ -> Farith_Big.one)
(fun p -> Farith_Big.pow_pos x p)
(fun _ -> Farith_Big.zero)
y
(** val to_nat : Farith_Big.big_int -> Farith_Big.big_int **)
let to_nat z =
Farith_Big.z_case
(fun _ -> Farith_Big.zero)
(fun p -> Farith_Big.identity p)
(fun _ -> Farith_Big.zero)
z
(** val to_pos : Farith_Big.big_int -> Farith_Big.big_int **)
let to_pos z =
Farith_Big.z_case
(fun _ -> Farith_Big.one)
(fun p -> p)
(fun _ -> Farith_Big.one)
z
(** val pos_div_eucl :
Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int * Farith_Big.big_int **)
let rec pos_div_eucl a b =
Farith_Big.positive_case
(fun a' ->
let (q, r) = pos_div_eucl a' b in
let r' =
Farith_Big.add (Farith_Big.mult (Farith_Big.double Farith_Big.one) r)
Farith_Big.one
in
if Farith_Big.lt r' b
then ((Farith_Big.mult (Farith_Big.double Farith_Big.one) q), r')
else ((Farith_Big.add
(Farith_Big.mult (Farith_Big.double Farith_Big.one) q)
Farith_Big.one), (Farith_Big.sub r' b)))
(fun a' ->
let (q, r) = pos_div_eucl a' b in
let r' = Farith_Big.mult (Farith_Big.double Farith_Big.one) r in
if Farith_Big.lt r' b
then ((Farith_Big.mult (Farith_Big.double Farith_Big.one) q), r')
else ((Farith_Big.add
(Farith_Big.mult (Farith_Big.double Farith_Big.one) q)
Farith_Big.one), (Farith_Big.sub r' b)))
(fun _ ->
if Farith_Big.le (Farith_Big.double Farith_Big.one) b
then (Farith_Big.zero, Farith_Big.one)
else (Farith_Big.one, Farith_Big.zero))
a
(** val even : Farith_Big.big_int -> bool **)
let even z =
Farith_Big.z_case
(fun _ -> true)
(fun p ->
Farith_Big.positive_case
(fun _ -> false)
(fun _ -> true)
(fun _ -> false)
p)
(fun p ->
Farith_Big.positive_case
(fun _ -> false)
(fun _ -> true)
(fun _ -> false)
p)
z
end
module Z :
sig
type t = Farith_Big.big_int
val pow : Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
val to_nat : Farith_Big.big_int -> Farith_Big.big_int
val to_pos : Farith_Big.big_int -> Farith_Big.big_int
val pos_div_eucl :
Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int * Farith_Big.big_int
val even : Farith_Big.big_int -> bool
end
open BinPosDef
open Datatypes
module Pos =
struct
(** val add_carry :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let rec add_carry = fun p q -> Farith_Big.succ (Farith_Big.add p q)
type mask = Pos.mask =
| IsNul
| IsPos of Farith_Big.big_int
| IsNeg
(** val succ_double_mask : mask -> mask **)
let succ_double_mask = function
| IsNul -> IsPos Farith_Big.one
| IsPos p -> IsPos (Farith_Big.succ_double p)
| IsNeg -> IsNeg
(** val double_mask : mask -> mask **)
let double_mask = function
| IsPos p -> IsPos (Farith_Big.double p)
| x0 -> x0
(** val double_pred_mask : Farith_Big.big_int -> mask **)
let double_pred_mask x =
Farith_Big.positive_case
(fun p -> IsPos (Farith_Big.double (Farith_Big.double p)))
(fun p -> IsPos (Farith_Big.double
(Farith_Big.pred_double p)))
(fun _ -> IsNul)
x
(** val sub_mask : Farith_Big.big_int -> Farith_Big.big_int -> mask **)
let rec sub_mask x y =
Farith_Big.positive_case
(fun p ->
Farith_Big.positive_case
(fun q -> double_mask (sub_mask p q))
(fun q -> succ_double_mask (sub_mask p q))
(fun _ -> IsPos (Farith_Big.double p))
y)
(fun p ->
Farith_Big.positive_case
(fun q -> succ_double_mask (sub_mask_carry p q))
(fun q -> double_mask (sub_mask p q))
(fun _ -> IsPos (Farith_Big.pred_double p))
y)
(fun _ ->
Farith_Big.positive_case
(fun _ -> IsNeg)
(fun _ -> IsNeg)
(fun _ -> IsNul)
y)
x
(** val sub_mask_carry :
Farith_Big.big_int -> Farith_Big.big_int -> mask **)
and sub_mask_carry x y =
Farith_Big.positive_case
(fun p ->
Farith_Big.positive_case
(fun q -> succ_double_mask (sub_mask_carry p q))
(fun q -> double_mask (sub_mask p q))
(fun _ -> IsPos (Farith_Big.pred_double p))
y)
(fun p ->
Farith_Big.positive_case
(fun q -> double_mask (sub_mask_carry p q))
(fun q -> succ_double_mask (sub_mask_carry p q))
(fun _ -> double_pred_mask p)
y)
(fun _ -> IsNeg)
x
(** val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1 **)
let rec iter f x n =
Farith_Big.positive_case
(fun n' -> f (iter f (iter f x n') n'))
(fun n' -> iter f (iter f x n') n')
(fun _ -> f x)
n
(** val div2 : Farith_Big.big_int -> Farith_Big.big_int **)
let div2 p =
Farith_Big.positive_case
(fun p0 -> p0)
(fun p0 -> p0)
(fun _ -> Farith_Big.one)
p
(** val div2_up : Farith_Big.big_int -> Farith_Big.big_int **)
let div2_up p =
Farith_Big.positive_case
(fun p0 -> Farith_Big.succ p0)
(fun p0 -> p0)
(fun _ -> Farith_Big.one)
p
(** val compare_cont :
comparison -> Farith_Big.big_int -> Farith_Big.big_int -> comparison **)
let rec compare_cont = fun c x y -> Farith_Big.compare_case c Lt Gt x y
(** val sqrtrem_step :
(Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int ->
Farith_Big.big_int) -> (Farith_Big.big_int * mask) ->
Farith_Big.big_int * mask **)
let sqrtrem_step f g = function
| (s, y) ->
(match y with
| IsPos r ->
let s' = Farith_Big.succ_double (Farith_Big.double s) in
let r' = g (f r) in
if Farith_Big.le s' r'
then ((Farith_Big.succ_double s), (sub_mask r' s'))
else ((Farith_Big.double s), (IsPos r'))
| _ ->
((Farith_Big.double s),
(sub_mask (g (f Farith_Big.one)) (Farith_Big.double
(Farith_Big.double Farith_Big.one)))))
(** val sqrtrem : Farith_Big.big_int -> Farith_Big.big_int * mask **)
let rec sqrtrem p =
Farith_Big.positive_case
(fun p0 ->
Farith_Big.positive_case
(fun p1 ->
sqrtrem_step (fun x -> Farith_Big.succ_double x) (fun x ->
Farith_Big.succ_double x) (sqrtrem p1))
(fun p1 ->
sqrtrem_step (fun x -> Farith_Big.double x) (fun x ->
Farith_Big.succ_double x) (sqrtrem p1))
(fun _ -> (Farith_Big.one, (IsPos (Farith_Big.double
Farith_Big.one))))
p0)
(fun p0 ->
Farith_Big.positive_case
(fun p1 ->
sqrtrem_step (fun x -> Farith_Big.succ_double x) (fun x ->
Farith_Big.double x) (sqrtrem p1))
(fun p1 ->
sqrtrem_step (fun x -> Farith_Big.double x) (fun x ->
Farith_Big.double x) (sqrtrem p1))
(fun _ -> (Farith_Big.one, (IsPos Farith_Big.one)))
p0)
(fun _ -> (Farith_Big.one, IsNul))
p
(** val iter_op :
('a1 -> 'a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1 **)
let rec iter_op op p a =
Farith_Big.positive_case
(fun p0 -> op a (iter_op op p0 (op a a)))
(fun p0 -> iter_op op p0 (op a a))
(fun _ -> a)
p
end
open BinPosDef
open Datatypes
module Pos :
sig
val add_carry :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int
type mask = Pos.mask =
| IsNul
| IsPos of Farith_Big.big_int
| IsNeg
val succ_double_mask : mask -> mask
val double_mask : mask -> mask
val double_pred_mask : Farith_Big.big_int -> mask
val sub_mask : Farith_Big.big_int -> Farith_Big.big_int -> mask
val sub_mask_carry : Farith_Big.big_int -> Farith_Big.big_int -> mask
val iter : ('a1 -> 'a1) -> 'a1 -> Farith_Big.big_int -> 'a1
val div2 : Farith_Big.big_int -> Farith_Big.big_int
val div2_up : Farith_Big.big_int -> Farith_Big.big_int
val compare_cont :
comparison -> Farith_Big.big_int -> Farith_Big.big_int -> comparison
val sqrtrem_step :
(Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int ->
Farith_Big.big_int) -> (Farith_Big.big_int * mask) ->
Farith_Big.big_int * mask
val sqrtrem : Farith_Big.big_int -> Farith_Big.big_int * mask
val iter_op : ('a1 -> 'a1 -> 'a1) -> Farith_Big.big_int -> 'a1 -> 'a1
end
module Pos =
struct
type mask =
| IsNul
| IsPos of Farith_Big.big_int
| IsNeg
end
module Pos :
sig
type mask =
| IsNul
| IsPos of Farith_Big.big_int
| IsNeg
end
type full_float =
| F754_zero of bool
| F754_infinity of bool
| F754_nan of bool * Farith_Big.big_int
| F754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
type binary_float =
| B754_zero of bool
| B754_infinity of bool
| B754_nan of bool * Farith_Big.big_int
| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
(** val coq_FF2B :
Farith_Big.big_int -> Farith_Big.big_int -> full_float -> binary_float **)
let coq_FF2B _ _ = function
| F754_zero s -> B754_zero s
| F754_infinity s -> B754_infinity s
| F754_nan (b, pl) -> B754_nan (b, pl)
| F754_finite (s, m, e) -> B754_finite (s, m, e)
type full_float =
| F754_zero of bool
| F754_infinity of bool
| F754_nan of bool * Farith_Big.big_int
| F754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
type binary_float =
| B754_zero of bool
| B754_infinity of bool
| B754_nan of bool * Farith_Big.big_int
| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
val coq_FF2B :
Farith_Big.big_int -> Farith_Big.big_int -> full_float -> binary_float
open BinInt
open Bool
open Datatypes
open Round
open SpecFloat
type binary_float =
| B754_zero of bool
| B754_infinity of bool
| B754_nan
| B754_finite of bool * Farith_Big.big_int * Farith_Big.big_int
(** val coq_SF2B :
Farith_Big.big_int -> Farith_Big.big_int -> spec_float -> binary_float **)
let coq_SF2B _ _ = function
| S754_zero s -> B754_zero s
| S754_infinity s -> B754_infinity s
| S754_nan -> B754_nan
| S754_finite (s, m, e) -> B754_finite (s, m, e)
(** val coq_B2SF :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> spec_float **)
let coq_B2SF _ _ = function
| B754_zero s -> S754_zero s
| B754_infinity s -> S754_infinity s
| B754_nan -> S754_nan
| B754_finite (s, m, e) -> S754_finite (s, m, e)
(** val is_nan :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> bool **)
let is_nan _ _ = function
| B754_nan -> true
| _ -> false
(** val coq_Babs :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float **)
let coq_Babs _ _ x = match x with
| B754_zero _ -> B754_zero false
| B754_infinity _ -> B754_infinity false
| B754_nan -> x
| B754_finite (_, mx, ex) -> B754_finite (false, mx, ex)
(** val coq_Beqb :
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float
-> bool **)