-
-
- -
-
- - - - - -

- - /jscert - -

- -
-
- - - -
-
- -
-
- - - -Permalink - - - -
- -
- - - -
- -
- - Find file - - -
-
- jscert/coq/JsNumber.v -
-
- - -
- - - da30e0c - - Jul 20, 2015 - - - -
- - @charguer - @brabalan - @edgemaster - @Mbodin - @PetarMax - - -
- - -
- -
-
-
- -
- Raw - Blame - History -
- - - - -
- -
- 108 lines (68 sloc) - - 3.14 KB -
-
- - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Set Implicit Arguments.
Require Export Shared.
Require Flocq.Appli.Fappli_IEEE Flocq.Appli.Fappli_IEEE_bits.
-
-
(**************************************************************)
(** ** Type for number (IEEE floats) *)
-
Definition number : Type :=
Fappli_IEEE_bits.binary64.
-
-
(**************************************************************)
(** ** Particular values of numbers *)
-
(* LATER: find definitions in Flocq *)
Parameter nan : number.
Parameter zero : number.
Parameter neg_zero : number.
Definition one := Fappli_IEEE.binary_normalize 53 1024 eq_refl eq_refl Fappli_IEEE.mode_NE 1 0 false.
Parameter infinity : number.
Parameter neg_infinity : number.
Parameter max_value : number.
Parameter min_value : number.
Parameter pi : number.
Parameter e : number.
Parameter ln2 : number.
-
(**************************************************************)
(** ** Conversions on numbers *)
-
(* LATER: implement definitions *)
Parameter from_string : string -> number.
Parameter to_string : number -> string.
-
(**************************************************************)
(** ** Unary operations on numbers *)
-
(* LATER: find definitions in Flocq *)
-
Parameter neg : number -> number.
Parameter floor : number -> number.
Parameter absolute : number -> number.
Parameter sign : number -> number. (* returns arbitrary when x is zero or nan *)
Parameter lt_bool : number -> number -> bool.
-
-
(**************************************************************)
(** ** Binary operations on numbers *)
-
Definition add : number -> number -> number :=
Fappli_IEEE_bits.b64_plus Fappli_IEEE.mode_NE.
-
Parameter sub : number -> number -> number. (* todo: bind *)
-
Parameter fmod : number -> number -> number. (* todo: bind *)
-
Definition mult : number -> number -> number :=
Fappli_IEEE_bits.b64_mult Fappli_IEEE.mode_NE.
-
Definition div : number -> number -> number :=
Fappli_IEEE_bits.b64_div Fappli_IEEE.mode_NE.
-
(* Todo: find comparison operator *)
Global Instance number_comparable : Comparable number.
Proof. Admitted.
-
-
-
(**************************************************************)
(** ** Conversions with Int32 *)
-
Parameter of_int : int -> number. (* LATER: this is quite complex. Should we make it precise? *)
-
Parameter to_int32 : number -> int. (* Remark: extracted code could, for efficiency reasons, use Ocaml Int32 *)
-
Parameter to_uint32 : number -> int.
-
Parameter to_int16 : number -> int. (* currently not used *)
-
(* LATER: Check that the OCaml extraction is correct. *)
-
-
(**************************************************************)
-
(** Implements the operation that masks all but the 5 least significant bits
of a non-negative number (obtained as the result of to_uint32 *)
-
Parameter modulo_32 : int -> int.
-
(** Implements int32 operation *)
-
Parameter int32_bitwise_not : int -> int.
-
Parameter int32_bitwise_and : int -> int -> int.
Parameter int32_bitwise_or : int -> int -> int.
Parameter int32_bitwise_xor : int -> int -> int.
-
Parameter int32_left_shift : int -> int -> int.
Parameter int32_right_shift : int -> int -> int.
Parameter uint32_right_shift : int -> int -> int.
-
-
-
-
(**************************************************************)
(** ** Int32 related conversion *)
- -
- -
- - - - -
-
-
- - -
-
- -