Commit 2bdd961a authored by François Bobot's avatar François Bobot
Browse files

[Farith2] Use dune for the compilation

  and start adding generic version for interval
parent fc3f06ed
-R ./thry F
./thry/Interval.v
./thry/All.v
./thry/Intv32.v
./thry/Tactics.v
./thry/Rextended.v
./thry/Qextended.v
./thry/Utils.v
./thry/B32.v
./thry/Correction_thms.v
./thry/Fle0.v
./extraction.v
\ No newline at end of file
-R ../_build/default/farith2/thry Farith2
(include_subdirs unqualified)
(library
(name farith2)
(public_name farith2)
(libraries zarith)
(flags "-w" "-33"))
(copy_files# extracted/*.ml*)
(copy_files# extract/farith_Big.ml)
(lang dune 2.8)
(generate_opam_files true)
(package
(name farith2)
(synopsis "formaly verified floating-points valuations based on Flocq"))
(coq.extraction
(prelude extraction)
(extracted_modules B32 BinNums Bool Qextended Utils Binary BinPosDef Datatypes Round Zaux BinarySingleNaN
BinPos Interval SpecFloat Zbool BinInt Bits Intv32 Specif Zpower Assert GenericFloat)
(theories Farith2))
From Flocq Require Import Core.Zaux IEEE754.BinarySingleNaN IEEE754.Bits.
From F Require Import Qextended B32 Intv32.
From Farith2 Require Import Qextended B32 Intv32 GenericFloat.
From Coq Require Import Extraction Lia Arith.Wf_nat ZArith.
Goal (Beqb (B32.add mode_NE (B32.of_q mode_NE Qx_half) (B32.of_q mode_NE Qx_half)) (B32.of_q mode_NE Qx_one) = true).
......@@ -269,6 +269,4 @@ Extract Inductive mode => "Farith_Big.mode" [
"Farith_Big.NE" "Farith_Big.ZR" "Farith_Big.DN" "Farith_Big.UP" "Farith_Big.NA"
].
Cd "extracted".
Separate Extraction B32.B32 Intv32.
Cd "..".
Separate Extraction B32.B32 Intv32 GenericFloat GenericInterval.
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
module type Inhabited =
sig
type t
val dummy : t
end
module Assert =
functor (M:Inhabited) ->
struct
(** val coq_assert : bool -> (__ -> M.t) -> M.t **)
let coq_assert x f =
if x then f __ else M.dummy
end
type __ = Obj.t
module type Inhabited =
sig
type t
val dummy : t
end
module Assert :
functor (M:Inhabited) ->
sig
val coq_assert : bool -> (__ -> M.t) -> M.t
end
open BinarySingleNaN
open Interval
type __ = Obj.t
type 'v coq_Generic = { prec : Farith_Big.big_int; emax : Farith_Big.big_int;
value : 'v }
(** val same_format_cast :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int -> 'a1 -> 'a1 **)
let same_format_cast _ _ _ _ f =
f
(** val same_format : 'a1 coq_Generic -> 'a2 coq_Generic -> bool **)
let same_format x y =
(&&) (Farith_Big.eq x.prec y.prec) (Farith_Big.eq x.emax y.emax)
(** val mk_with : 'a1 coq_Generic -> 'a2 -> 'a2 coq_Generic **)
let mk_with x y =
{ prec = x.prec; emax = x.emax; value = y }
module GenericFloat =
struct
type coq_F = binary_float coq_Generic
module F_inhab =
struct
type t = coq_F
(** val dummy : binary_float coq_Generic **)
let dummy =
{ prec = (Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.succ_double Farith_Big.one)))); 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))))))); value = B754_nan }
end
module AssertF = Assert.Assert(F_inhab)
module B_inhab =
struct
type t = bool
(** val dummy : bool **)
let dummy =
true
end
module AssertB = Assert.Assert(B_inhab)
(** val add :
Farith_Big.mode -> coq_F -> coq_F -> binary_float coq_Generic option **)
let add m x y =
let filtered_var = same_format x y in
if filtered_var
then Some { prec = x.prec; emax = x.emax; value =
(coq_Bplus x.prec x.emax m x.value
(same_format_cast x.prec x.emax y.prec y.emax y.value)) }
else None
(** val coq_Fadd : Farith_Big.mode -> coq_F -> coq_F -> coq_F **)
let coq_Fadd m x y =
(fun x f -> assert x; f ()) (same_format x y) (fun _ ->
mk_with x
(coq_Bplus x.prec x.emax m x.value
(same_format_cast x.prec x.emax y.prec y.emax y.value)))
(** val coq_Fsub : Farith_Big.mode -> coq_F -> coq_F -> coq_F **)
let coq_Fsub m x y =
(fun x f -> assert x; f ()) (same_format x y) (fun _ -> { prec = x.prec;
emax = x.emax; value =
(coq_Bminus x.prec x.emax m x.value
(same_format_cast x.prec x.emax y.prec y.emax y.value)) })
end
module GenericInterval =
struct
module Coq__1 = struct
type t = coq_Interval coq_Generic
end
include Coq__1
module I_inhab =
struct
type t = Coq__1.t
(** val dummy : t **)
let dummy =
{ prec = (Farith_Big.double (Farith_Big.double (Farith_Big.double
(Farith_Big.succ_double Farith_Big.one)))); 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))))))); value = (Intv ((B754_infinity true),
(B754_infinity false), true)) }
end
module AssertI = Assert.Assert(I_inhab)
module O_inhab =
struct
type t = Coq__1.t option
(** val dummy : t **)
let dummy =
None
end
module AssertO = Assert.Assert(O_inhab)
(** val inter : t -> t -> t option **)
let inter x y =
(fun x f -> assert x; f ()) (same_format x y) (fun _ ->
let r =
inter x.prec x.emax x.value
(same_format_cast x.prec x.emax y.prec y.emax y.value)
in
(match r with
| Some r0 -> Some (mk_with x r0)
| None -> None))
end
open BinarySingleNaN
open Interval
type __ = Obj.t
type 'v coq_Generic = { prec : Farith_Big.big_int; emax : Farith_Big.big_int;
value : 'v }
val same_format_cast :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int -> 'a1 -> 'a1
val same_format : 'a1 coq_Generic -> 'a2 coq_Generic -> bool
val mk_with : 'a1 coq_Generic -> 'a2 -> 'a2 coq_Generic
module GenericFloat :
sig
type coq_F = binary_float coq_Generic
module F_inhab :
sig
type t = coq_F
val dummy : binary_float coq_Generic
end
module AssertF :
sig
end
module B_inhab :
sig
type t = bool
val dummy : bool
end
module AssertB :
sig
end
val add :
Farith_Big.mode -> coq_F -> coq_F -> binary_float coq_Generic option
val coq_Fadd : Farith_Big.mode -> coq_F -> coq_F -> coq_F
val coq_Fsub : Farith_Big.mode -> coq_F -> coq_F -> coq_F
end
module GenericInterval :
sig
module Coq__1 : sig
type t = coq_Interval coq_Generic
end
include module type of struct include Coq__1 end
module I_inhab :
sig
type t = Coq__1.t
val dummy : t
end
module AssertI :
sig
end
module O_inhab :
sig
type t = Coq__1.t option
val dummy : t
end
module AssertO :
sig
end
val inter : t -> t -> t option
end
......@@ -9,7 +9,15 @@ type coq_Interval' =
type coq_Interval = coq_Interval'
type coq_Interval_opt = coq_Interval' option
type coq_Interval_opt = coq_Interval option
(** val to_Interval_opt :
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' option ->
coq_Interval_opt **)
let to_Interval_opt _ _ = function
| Some j -> Some j
| None -> None
(** val inter' :
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' ->
......@@ -34,8 +42,8 @@ let inter' prec emax i1 i2 =
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval -> coq_Interval
-> coq_Interval_opt **)
let inter =
inter'
let inter prec emax i1 i2 =
to_Interval_opt prec emax (inter' prec emax i1 i2)
(** val coq_Iadd' :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
......
......@@ -9,7 +9,11 @@ type coq_Interval' =
type coq_Interval = coq_Interval'
type coq_Interval_opt = coq_Interval' option
type coq_Interval_opt = coq_Interval option
val to_Interval_opt :
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' option ->
coq_Interval_opt
val inter' :
Farith_Big.big_int -> Farith_Big.big_int -> coq_Interval' -> coq_Interval'
......
(rule
(targets B32.ml BinNums.ml Bool.ml Qextended.ml Utils.ml
B32.mli BinNums.mli Bool.mli Qextended.mli Utils.mli
Binary.ml BinPosDef.ml Datatypes.ml Round.ml Zaux.ml
Binary.mli BinPosDef.mli Datatypes.mli Round.mli Zaux.mli
BinarySingleNaN.ml BinPos.ml Interval.ml SpecFloat.ml Zbool.ml
BinarySingleNaN.mli BinPos.mli Interval.mli SpecFloat.mli Zbool.mli
BinInt.ml Bits.ml Intv32.ml Specif.ml Zpower.ml
BinInt.mli Bits.mli Intv32.mli Specif.mli Zpower.mli
)
(deps (source_tree ../thry/) ../Makefile ../_CoqProject ../extraction.v)
(action (run make -C ..))
(mode promote)
)
(rule (action (copy ../extract/B32.ml B32.ml)) (mode promote))
(rule (action (copy ../extract/BinNums.ml BinNums.ml)) (mode promote))
(rule (action (copy ../extract/Bool.ml Bool.ml)) (mode promote))
(rule (action (copy ../extract/Qextended.ml Qextended.ml)) (mode promote))
(rule (action (copy ../extract/Utils.ml Utils.ml)) (mode promote))
(rule (action (copy ../extract/B32.mli B32.mli)) (mode promote))
(rule (action (copy ../extract/BinNums.mli BinNums.mli)) (mode promote))
(rule (action (copy ../extract/Bool.mli Bool.mli)) (mode promote))
(rule (action (copy ../extract/Qextended.mli Qextended.mli)) (mode promote))
(rule (action (copy ../extract/Utils.mli Utils.mli)) (mode promote))
(rule (action (copy ../extract/Binary.ml Binary.ml)) (mode promote))
(rule (action (copy ../extract/BinPosDef.ml BinPosDef.ml)) (mode promote))
(rule (action (copy ../extract/Datatypes.ml Datatypes.ml)) (mode promote))
(rule (action (copy ../extract/Round.ml Round.ml)) (mode promote))
(rule (action (copy ../extract/Zaux.ml Zaux.ml)) (mode promote))
(rule (action (copy ../extract/Binary.mli Binary.mli)) (mode promote))
(rule (action (copy ../extract/BinPosDef.mli BinPosDef.mli)) (mode promote))
(rule (action (copy ../extract/Datatypes.mli Datatypes.mli)) (mode promote))
(rule (action (copy ../extract/Round.mli Round.mli)) (mode promote))
(rule (action (copy ../extract/Zaux.mli Zaux.mli)) (mode promote))
(rule (action (copy ../extract/BinarySingleNaN.ml BinarySingleNaN.ml)) (mode promote))
(rule (action (copy ../extract/BinPos.ml BinPos.ml)) (mode promote))
(rule (action (copy ../extract/Interval.ml Interval.ml)) (mode promote))
(rule (action (copy ../extract/SpecFloat.ml SpecFloat.ml)) (mode promote))
(rule (action (copy ../extract/Zbool.ml Zbool.ml)) (mode promote))
(rule (action (copy ../extract/BinarySingleNaN.mli BinarySingleNaN.mli)) (mode promote))
(rule (action (copy ../extract/BinPos.mli BinPos.mli)) (mode promote))
(rule (action (copy ../extract/Interval.mli Interval.mli)) (mode promote))
(rule (action (copy ../extract/SpecFloat.mli SpecFloat.mli)) (mode promote))
(rule (action (copy ../extract/Zbool.mli Zbool.mli)) (mode promote))
(rule (action (copy ../extract/BinInt.ml BinInt.ml)) (mode promote))
(rule (action (copy ../extract/Bits.ml Bits.ml)) (mode promote))
(rule (action (copy ../extract/Intv32.ml Intv32.ml)) (mode promote))
(rule (action (copy ../extract/Specif.ml Specif.ml)) (mode promote))
(rule (action (copy ../extract/Zpower.ml Zpower.ml)) (mode promote))
(rule (action (copy ../extract/BinInt.mli BinInt.mli)) (mode promote))
(rule (action (copy ../extract/Bits.mli Bits.mli)) (mode promote))
(rule (action (copy ../extract/Intv32.mli Intv32.mli)) (mode promote))
(rule (action (copy ../extract/Specif.mli Specif.mli)) (mode promote))
(rule (action (copy ../extract/Zpower.mli Zpower.mli)) (mode promote))
(rule (action (copy ../extract/Assert.ml Assert.ml)) (mode promote))
(rule (action (copy ../extract/Assert.mli Assert.mli)) (mode promote))
(rule (action (copy ../extract/GenericFloat.ml GenericFloat.ml)) (mode promote))
(rule (action (copy ../extract/GenericFloat.mli GenericFloat.mli)) (mode promote))
doc/
.*.aux
.*.d
*.a
*.cma
*.cmi
*.cmo
*.cmx
*.cmxa
*.cmxs
*.glob
*.ml.d
*.ml4.d
*.mlg.d
*.mli.d
*.mllib.d
*.mlpack.d
*.native
*.o
*.v.d
*.vio
*.vo
*.vok
*.vos
.coq-native
.csdp.cache
.lia.cache
.nia.cache
.nlia.cache
.nra.cache
csdp.cache
lia.cache
nia.cache
nlia.cache
nra.cache
native_compute_profile_*.data
# generated timing files
*.timing.diff
*.v.after-timing
*.v.before-timing
*.v.timing
time-of-build-after.log
time-of-build-before.log
time-of-build-both.log
time-of-build-pretty.log
\ No newline at end of file
......@@ -24,75 +24,3 @@ Module Assert (M : Inhabited).
now rewrite H.
Qed.
End Assert.
Module GenericFloat.
Record F : Type := {
prec : Z;
emax : Z;
Hprec : FLX.Prec_gt_0 prec;
Hemax : Prec_lt_emax prec emax;
value : binary_float prec emax;
}.
Require Import Bool.
Program Definition unify (p e p' e' : Z) (f : binary_float p' e') (Hp : p = p') (Hp : e = e') : binary_float p e := f.
Program Definition same_format_cast {p e p' e' : Z} (H : ((p =? p') && (e =? e') = true)%Z) (f : binary_float p' e') : binary_float p e := f.
Next Obligation.
apply andb_true_iff in H as [A _].
now rewrite (proj1 (Z.eqb_eq _ _) A).
Defined.
Next Obligation.
apply andb_true_iff in H as [_ B].
now rewrite (proj1 (Z.eqb_eq _ _) B).
Defined.
Module F_inhab.
Definition t : Type := F.
Program Definition dummy := {|
prec := 24;
emax := 128;
value := BinarySingleNaN.B754_nan;
Hprec := _;
Hemax := _;
|}.
Solve All Obligations with easy.
End F_inhab.
Module AssertF := Assert (F_inhab).
Definition same_format (x y : F) : bool :=
Z.eqb (prec x) (prec y) && Z.eqb (emax x) (emax y).
Program Definition add (m : mode) (x y : F) :=
match same_format x y with
| true => Some {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := @Bplus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast _ (value y))
|}
| false => None
end.
Definition Fadd (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun H => {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := @Bplus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y));
|}).
Definition Fsub (m : mode) (x y : F) : F :=
AssertF.assert (same_format x y) (fun H => {|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := @Bminus _ _ (Hprec x) (Hemax x) m (value x) (same_format_cast H (value y));
|}).
End GenericFloat.
\ No newline at end of file
......@@ -6,7 +6,7 @@ Require Import ZBits.
Require Import Lia Lra.
Require Coq.Arith.Wf_nat.
Require Import Extraction.
From F Require Import Qextended Rextended.
Require Import Qextended Rextended.
(** * An instanciation of Flocq's BinarySingleNan for 32 bits IEEE-754 floating points *)
......@@ -131,4 +131,4 @@ Proof.
+ admit.
Admitted.
End B32.
\ No newline at end of file
End B32.
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith Lia Reals Psatz.
From F Require Import Utils Rextended.
Require Import Utils Rextended.
Section Correction.
......@@ -186,4 +186,4 @@ Proof.
- apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ H2)).
Qed.
End Correction.
\ No newline at end of file
End Correction.
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import Program ZArith Bool.
Require Import Assert Utils Interval B32.
Record Generic { v } : Type := {
prec : Z;
emax : Z;
Hprec : FLX.Prec_gt_0 prec;
Hemax : Prec_lt_emax prec emax;
value : v prec emax;
}.
Program Definition unify { v } (p e p' e' : Z) (f : v p' e') (Hp : p = p') (Hp : e = e') : v p e := f.
Program Definition same_format_cast {v } {p e p' e' : Z} (H : ((p =? p') && (e =? e') = true)%Z) (f : v p' e') : v p e := f.
Next Obligation.
apply andb_true_iff in H as [A _].
now rewrite (proj1 (Z.eqb_eq _ _) A).
Defined.
Next Obligation.
apply andb_true_iff in H as [_ B].
now rewrite (proj1 (Z.eqb_eq _ _) B).
Defined.
Definition same_format { v1 v2 } (x : @Generic v1) (y : @Generic v2) : bool :=
Z.eqb (prec x) (prec y) && Z.eqb (emax x) (emax y).
Definition mk_with {v1 v2} (x : @Generic v1) (y:v2 (prec x) (emax x)) : @Generic v2 :=
{|
prec := prec x;
emax := emax x;
Hprec := Hprec x;
Hemax := Hemax x;
value := y;
|}.
Module GenericFloat.
Definition F : Type := @Generic binary_float.
Module F_inhab.
Definition t : Type := F.
Program Definition dummy := {|
prec := 24;
emax := 128;
value := BinarySingleNaN.B754_nan;
Hprec := _;
Hemax := _;
|}.
Solve All Obligations with easy.
End F_inhab.
Module AssertF := Assert (F_inhab).
Module B_inhab.
Definition t : Type := bool.
Program Definition dummy := true.
Solve All Obligations with easy.