Skip to content
GitLab
Commit b42b601e authored by François Bobot's avatar François Bobot
Browse files

Coq 8.6 and flocq v4161c990053985f6819e

parent c051efaf
Expand all Hide whitespace changes
Inline Side-by-side
F_aux.v
View file @ b42b601e
......@@ -19,13 +19,14 @@
(* *)
(**************************************************************************)
Require Import Fcore.
Require Import Fappli_IEEE.
Require Import Fappli_IEEE_bits.
Require Import Flocq.Core.Fcore.
Require Import Flocq.Appli.Fappli_IEEE.
Require Import Flocq.Appli.Fappli_IEEE_bits.
Require Import QArith.
Require Import Qreals.
Require Import Reals.
Require Import ZBits.
Require Coq.Arith.Wf_nat.
Parameter assert : forall (b:bool) (t:Type), ((b=true) -> t) -> t.
......@@ -36,7 +37,7 @@ Fixpoint least_bit_Pnat (n : positive) :=
| xI p => O
end.
Definition shiftr_pos a p := nat_iter p Z.div2 a.
Definition shiftr_pos a p := Wf_nat.iter_nat p _ Z.div2 a.
Lemma shiftr_pos_is_shiftr :
forall a p, shiftr_pos a p = Z.shiftr a (Z.of_nat p).
......@@ -136,10 +137,10 @@ Defined.
Definition B2Rplus prec emax (f:binary_float prec emax) : Rplus :=
match f with
| B754_zero _ => Rp_finite 0%R
| B754_infinity b => Rp_infinity b
| B754_nan b pl => Rp_nan (b,pl)
| B754_finite _ _ _ _ => Rp_finite (B2R prec emax f)
| B754_zero _ _ _ => Rp_finite 0%R
| B754_infinity _ _ b => Rp_infinity b
| B754_nan _ _ b pl => Rp_nan (b,pl)
| B754_finite _ _ _ _ _ _ => Rp_finite (B2R prec emax f)
end.
Definition int_native bw := { i | match Z.shiftr i (bw-1) with
......@@ -228,13 +229,14 @@ Section Direct.
Implicit Arguments B754_nan [[prec] [emax]].
Implicit Arguments B754_zero [[prec] [emax]].
Implicit Arguments B754_infinity [[prec] [emax]].
Implicit Arguments B754_finite [[prec] [emax]].
Let Hmw : (0 < mw)%Z := Hmw t' conf.
Let Hew : (0 < ew)%Z := Hew t' conf.
Let Hemax : (cprec mw < cemax ew)%Z := Hemax t' conf.
Let Hprec : (0 < cprec mw)%Z := Hprec t' conf.
Definition pl_cst := (iter_nat xO (Z.to_nat (Z.pred mw)) xH)%Z.
Definition pl_cst := (Fcore_Zaux.iter_nat xO (Z.to_nat (Z.pred mw)) xH)%Z.
Lemma pl_valid : (Z.pos (Fcore_digits.digits2_pos pl_cst) <? prec)%Z = true.
Proof.
......@@ -426,11 +428,11 @@ Section Direct.
Definition of_q mode q : t :=
match Qz_classify q with
| Qz_ZERO _ _ _ => B754_zero false
| Qz_INF _ _ => B754_infinity false
| Qz_MINF _ _ => B754_infinity true
| Qz_UNDEF _ _ => default_nan
| Qz_NZERO _ _ _ _ =>
| Qz_ZERO _ _ _ _ => B754_zero false
| Qz_INF _ _ _ => B754_infinity false
| Qz_MINF _ _ _ => B754_infinity true
| Qz_UNDEF _ _ _ => default_nan
| Qz_NZERO _ _ _ _ _ =>
match num q with
| Z0 => default_nan (** absurd *)
| Z.pos pn =>
......@@ -506,7 +508,7 @@ Section Direct.
replace (least_bit_Pnat m~0) with (S (least_bit_Pnat m)) in * by reflexivity;
intros e' m';
replace (shiftr_pos m' e') with (shiftr_pos (Z.div2 m') (least_bit_Pnat m)) by
(unfold shiftr_pos, e'; rewrite nat_iter_succ_r; reflexivity).
(unfold shiftr_pos, e'; rewrite nat_rect_succ_r; reflexivity).
* replace (Z.div2 m') with (Z.neg m) by reflexivity.
exact H.
* replace (Z.div2 m') with (Z.pos m) by reflexivity.
......@@ -530,8 +532,8 @@ Section Direct.
* rewrite Pos.iter_succ.
unfold Pos.gcd.
simpl.
replace (Pos.size_nat p + S (Pos.size_nat (Pos.iter n xO 1%positive)))%nat
with (S (Pos.size_nat p + Pos.size_nat (Pos.iter n xO 1%positive))) by auto with *.
replace (Pos.size_nat p + S (Pos.size_nat (Pos.iter xO 1%positive n)))%nat
with (S (Pos.size_nat p + Pos.size_nat (Pos.iter xO 1%positive n))) by auto with *.
exact IHn.
- unfold Pos.gcd.
reflexivity.
......@@ -648,7 +650,7 @@ Section Direct.
| false, true => Gt
end in
match f1, f2 with
| B754_nan b1 (exist pl1 _),B754_nan b2 (exist pl2 _) =>
| B754_nan b1 (exist _ pl1 _),B754_nan b2 (exist _ pl2 _) =>
match cmp_bool b1 b2 with
| Eq => Pos.compare pl1 pl2
| r => r
......@@ -751,7 +753,7 @@ Section Direct.
hash_bool b
| B754_infinity b =>
hash_combine nativeint_three (hash_bool b)
| B754_nan b (exist n _) =>
| B754_nan b (exist _ n _) =>
hash_combine nativeint_five (hash_combine (hash_z (Z.pos n)) (hash_bool b))
| B754_finite b m e _ =>
hash_combine (hash_z (Z.pos m)) (hash_combine (hash_z e) (hash_bool b))
......@@ -787,7 +789,7 @@ Section Direct.
forall f1 f2,
is_finite prec emax f1 = true -> is_finite prec emax f2 = true ->
match fcompare f1 f2 with
| Some (exist x _) => Z.compare x 0 = Rcompare (B2R prec emax f1) (B2R prec emax f2)
| Some (exist _ x _) => Z.compare x 0 = Rcompare (B2R prec emax f1) (B2R prec emax f2)
| None => False
end.
Proof.
......@@ -964,10 +966,10 @@ Section Direct.
rewrite (Ht t1 conf1).
exact (fun f =>
match f with
| B754_zero b => B754_zero _ _ b
| B754_nan b _ => B754_nan _ _ b (snd (Aux.default_nan_pl _ conf2))
| B754_infinity b => B754_infinity _ _ b
| B754_finite sx mx ex _ => FF2B _ _ _ (proj1 (binary_round_correct (cprec (mw _ conf2)) (cemax (ew _ conf2)) (Hprec _ conf2) (Hemax _ conf2) mode sx mx ex))
| B754_zero _ _ b => B754_zero _ _ b
| B754_nan _ _ b _ => B754_nan _ _ b (snd (Aux.default_nan_pl _ conf2))
| B754_infinity _ _ b => B754_infinity _ _ b
| B754_finite _ _ sx mx ex _ => FF2B _ _ _ (proj1 (binary_round_correct (cprec (mw _ conf2)) (cemax (ew _ conf2)) (Hprec _ conf2) (Hemax _ conf2) mode sx mx ex))
end).
Defined.
......
extract.sh
View file @ b42b601e
......@@ -8,9 +8,10 @@ rm -rf extracted
mkdir extracted
cd extracted
coqtop.opt -I .. -batch -l ../extract.v
cp ../F_aux.vo .
coqtop -batch -l ../extract.v
rm Peano.ml* Zbool.ml* BinNums.ml*
rm -f Peano.ml* Zbool.ml* BinNums.ml*
for file in *.ml*; do
case $file in
......
extract.v
View file @ b42b601e
......@@ -83,8 +83,6 @@ Extract Constant Euclid.eucl_dev => "fun n m -> Farith_Big.quomod m n".
Extract Constant Euclid.quotient => "fun n m -> Farith_Big.div m n".
Extract Constant Euclid.modulo => "fun n m -> Farith_Big.modulo m n".
Extract Inlined Constant nat_iter => "Farith_Big.nat_iter".
(** From ExtrOcamlZBigInt of coq archive *)
Require Import ZArith NArith.
......@@ -125,7 +123,7 @@ Extract Inlined Constant Pos.min => "Farith_Big.min".
Extract Inlined Constant Pos.max => "Farith_Big.max".
Extract Inlined Constant Pos.compare => "(Farith_Big.compare_case Eq Lt Gt)".
Extract Constant Pos.compare_cont =>
"fun x y c -> Farith_Big.compare_case c Lt Gt x y".
"fun c x y -> Farith_Big.compare_case c Lt Gt x y".
Extract Inlined Constant Pos.eqb => "Farith_Big.eq".
Extract Inlined Constant Pos.leb => "Farith_Big.le".
Extract Inlined Constant Pos.ltb => "Farith_Big.lt".
......@@ -227,9 +225,11 @@ Extract Inlined Constant Z.pow_pos => "Farith_Big.pow_pos".
Require Import Fcore_Zaux.
Require Import Flocq.Core.Fcore_Zaux.
Require Coq.Arith.Wf_nat.
(* Extract Inlined Constant shiftl_pos => "Farith_Big.shiftl_pos". *)
Extract Inlined Constant iter_nat => "Farith_Big.iter_nat".
Extract Inlined Constant Fcore_Zaux.iter_nat => "Farith_Big.iter_nat".
Extract Inlined Constant nat_rect => "Farith_Big.nat_rect".
(** Some proofs used in function realization *)
......@@ -260,14 +260,14 @@ Qed.
(* Avoid name clashes *)
Extraction Blacklist Big List String Int Z Q.
Require Import Flocq_version F_aux.
Require Import Flocq.Flocq_version F_aux.
Extract Inductive F_aux.Qz => "Q.t" [ "Farith_Big.q_mk" ] "Farith_Big.q_case".
Extract Inlined Constant F_aux.den => "Farith_Big.q_den".
Extract Inlined Constant F_aux.num => "Farith_Big.q_num".
Extract Inlined Constant F_aux.Qz_classify => "Q.classify".
Extract Inductive Qz_kind => "Q.kind" [ "Q.ZERO" "Q.INF" "Q.MINF" "Q.UNDEF" "Q.NZERO" ].
Extract Inductive Qz_kind => "Q.kind" [ "Q.INF" "Q.MINF" "Q.UNDEF" "Q.ZERO" "Q.NZERO" ].
Extract Inlined Constant Qz_classify => "Q.classify".
Extract Inlined Constant F_aux.int31 => "int".
......
extracted/farith_BinInt.ml
View file @ b42b601e
......@@ -17,98 +17,51 @@
(* COPYING file for more details. *)
(**************************************************************************)
open Farith_BinNat
open Farith_BinPos
open Farith_Bool
open Farith_Datatypes
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
module Z =
struct
module Z =
struct
type t = Farith_Big.big_int
(** val zero : Farith_Big.big_int **)
let zero =
Farith_Big.zero
(** val one : Farith_Big.big_int **)
let one =
Farith_Big.one
(** val two : Farith_Big.big_int **)
let two =
(Farith_Big.double Farith_Big.one)
(** 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 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 p ->
Farith_Big.zero)
z
(** val to_N : Farith_Big.big_int -> Farith_Big.big_int **)
let to_N z =
Farith_Big.z_case
(fun _ ->
Farith_Big.zero)
(fun p ->
p)
(fun p ->
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 p ->
(fun _ ->
Farith_Big.one)
z
(** val iter : Farith_Big.big_int -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
let iter n f x =
Farith_Big.z_case
(fun _ ->
x)
(fun p ->
Pos.iter p f x)
(fun p ->
x)
n
(** 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' ->
......@@ -135,323 +88,4 @@ module Z =
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 p0 ->
false)
(fun p0 ->
true)
(fun _ ->
false)
p)
(fun p ->
Farith_Big.positive_case
(fun p0 ->
false)
(fun p0 ->
true)
(fun _ ->
false)
p)
z
(** val odd : Farith_Big.big_int -> bool **)
let odd z =
Farith_Big.z_case
(fun _ ->
false)
(fun p ->
Farith_Big.positive_case
(fun p0 ->
true)
(fun p0 ->
false)
(fun _ ->
true)
p)
(fun p ->
Farith_Big.positive_case
(fun p0 ->
true)
(fun p0 ->
false)
(fun _ ->
true)
p)
z
(** val log2 : Farith_Big.big_int -> Farith_Big.big_int **)
let log2 z =
Farith_Big.z_case
(fun _ ->
Farith_Big.zero)
(fun p0 ->
Farith_Big.positive_case
(fun p ->
(Pos.size p))
(fun p ->
(Pos.size p))
(fun _ ->
Farith_Big.zero)
p0)
(fun p ->
Farith_Big.zero)
z
(** val ggcd :
Farith_Big.big_int -> Farith_Big.big_int ->
Farith_Big.big_int * (Farith_Big.big_int * Farith_Big.big_int) **)
let ggcd a b =
Farith_Big.z_case
(fun _ -> ((Farith_Big.abs b), (Farith_Big.zero,
(Farith_Big.sgn b))))
(fun a0 ->
Farith_Big.z_case
(fun _ -> ((Farith_Big.abs a), ((Farith_Big.sgn a),
Farith_Big.zero)))
(fun b0 ->
let (g, p) = Pos.ggcd a0 b0 in let (aa, bb) = p in (g, (aa, bb)))
(fun b0 ->
let (g, p) = Pos.ggcd a0 b0 in
let (aa, bb) = p in (g, (aa, (Farith_Big.opp bb))))
b)
(fun a0 ->
Farith_Big.z_case
(fun _ -> ((Farith_Big.abs a), ((Farith_Big.sgn a),
Farith_Big.zero)))
(fun b0 ->
let (g, p) = Pos.ggcd a0 b0 in
let (aa, bb) = p in (g, ((Farith_Big.opp aa), bb)))
(fun b0 ->
let (g, p) = Pos.ggcd a0 b0 in
let (aa, bb) = p in (g, ((Farith_Big.opp aa), (Farith_Big.opp bb))))
b)
a
(** val testbit : Farith_Big.big_int -> Farith_Big.big_int -> bool **)
let testbit a n =
Farith_Big.z_case
(fun _ ->
odd a)
(fun p ->
Farith_Big.z_case
(fun _ ->
false)
(fun a0 ->
Pos.testbit a0 p)
(fun a0 ->
Pervasives.not (N.testbit (Pos.pred_N a0) p))
a)
(fun p ->
false)
n
module Private_BootStrap =
struct
end
(** val leb_spec0 : Farith_Big.big_int -> Farith_Big.big_int -> reflect **)
let leb_spec0 x y =
iff_reflect (Farith_Big.le x y)
(** val ltb_spec0 : Farith_Big.big_int -> Farith_Big.big_int -> reflect **)
let ltb_spec0 x y =
iff_reflect (Farith_Big.lt x y)
module Private_OrderTac =
struct
module IsTotal =
struct
end
module Tac =
struct
end
end
(** val sqrt_up : Farith_Big.big_int -> Farith_Big.big_int **)
let sqrt_up a =
match (Farith_Big.compare_case Eq Lt Gt) Farith_Big.zero a with
| Lt -> Farith_Big.succ (Farith_Big.Z.sqrt (Farith_Big.pred a))
| _ -> Farith_Big.zero
(** val log2_up : Farith_Big.big_int -> Farith_Big.big_int **)
let log2_up a =
match (Farith_Big.compare_case Eq Lt Gt) Farith_Big.one a with
| Lt -> Farith_Big.succ (log2 (Farith_Big.pred a))
| _ -> Farith_Big.zero
module Private_NZDiv =
struct
end
module Private_Div =
struct
module Quot2Div =
struct
(** val div :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let div =
Farith_Big.Z.div
(** val modulo :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let modulo =
Farith_Big.Z.rem
end
module NZQuot =
struct
end
end
(** val lcm :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let lcm a b =
Farith_Big.abs
(Farith_Big.mult a (Farith_Big.div_floor b (Farith_Big.Z.gcd a b)))
(** val eqb_spec : Farith_Big.big_int -> Farith_Big.big_int -> reflect **)
let eqb_spec x y =
iff_reflect (Farith_Big.eq x y)
(** val b2z : bool -> Farith_Big.big_int **)
let b2z = function
| true -> Farith_Big.one
| false -> Farith_Big.zero
(** val setbit :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let setbit a n =
Farith_Big.Z.logor a (Farith_Big.shiftl Farith_Big.one n)
(** val clearbit :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.big_int **)
let clearbit a n =
Farith_Big.ldiff a (Farith_Big.shiftl Farith_Big.one n)
(** val ones : Farith_Big.big_int -> Farith_Big.big_int **)
let ones n =
Farith_Big.pred (Farith_Big.shiftl Farith_Big.one n)
module Private_Tac =
struct
end
module Private_Dec =
struct
(** val max_case_strong :
Farith_Big.big_int -> Farith_Big.big_int -> (Farith_Big.big_int ->
Farith_Big.big_int -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> 'a1 **)
let max_case_strong n m compat hl hr =
let c = coq_CompSpec2Type n m ((Farith_Big.compare_case Eq Lt Gt) n m)
in
(match c with
| CompGtT -> compat n (Farith_Big.max n m) __ (hl __)
| _ -> compat m (Farith_Big.max n m) __ (hr __))
(** val max_case :
Farith_Big.big_int -> Farith_Big.big_int -> (Farith_Big.big_int ->
Farith_Big.big_int -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
let max_case n m x x0 x1 =
max_case_strong n m x (fun _ -> x0) (fun _ -> x1)
(** val max_dec : Farith_Big.big_int -> Farith_Big.big_int -> bool **)
let max_dec n m =
max_case n m (fun x y _ h0 -> h0) true false
(** val min_case_strong :
Farith_Big.big_int -> Farith_Big.big_int -> (Farith_Big.big_int ->
Farith_Big.big_int -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
-> 'a1 **)
let min_case_strong n m compat hl hr =
let c = coq_CompSpec2Type n m ((Farith_Big.compare_case Eq Lt Gt) n m)
in
(match c with
| CompGtT -> compat m (Farith_Big.min n m) __ (hr __)
| _ -> compat n (Farith_Big.min n m) __ (hl __))
(** val min_case :
Farith_Big.big_int -> Farith_Big.big_int -> (Farith_Big.big_int ->
Farith_Big.big_int -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **)
let min_case n m x x0 x1 =
min_case_strong n m x (fun _ -> x0) (fun _ -> x1)
(** val min_dec : Farith_Big.big_int -> Farith_Big.big_int -> bool **)
let min_dec n m =
min_case n m (fun x y _ h0 -> h0) true false
end
(** val max_case_strong :
Farith_Big.big_int -> Farith_Big.big_int -> (__ -> 'a1) -> (__ -> 'a1)
-> 'a1 **)
let max_case_strong n m x x0 =
Private_Dec.max_case_strong n m (fun x1 y _ x2 -> x2) x x0
(** val max_case :
Farith_Big.big_int -> Farith_Big.big_int -> 'a1 -> 'a1 -> 'a1 **)
let max_case n m x x0 =
max_case_strong n m (fun _ -> x) (fun _ -> x0)
(** val max_dec : Farith_Big.big_int -> Farith_Big.big_int -> bool **)
let max_dec =
Private_Dec.max_dec
(** val min_case_strong :
Farith_Big.big_int -> Farith_Big.big_int -> (__ -> 'a1) -> (__ -> 'a1)
-> 'a1 **)
let min_case_strong n m x x0 =
Private_Dec.min_case_strong n m (fun x1 y _ x2 -> x2) x x0
(** val min_case : <