Commit be61af35 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'option_bind' into 'WIP_fix_broken_Flover_compute'

Rename 'optionLift' with 'optionBind'

See merge request AVA/FloVer!2
parents ddc04b14 0a00766a
......@@ -10,12 +10,6 @@ Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE
Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024.
Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :=
match e with
| Some v => some_cont v
| None => none_cont
end.
Definition normal_or_zero v :=
(v = 0 \/ (Q2R (minValue_pos M64)) <= (Rabs v))%R.
......@@ -55,15 +49,15 @@ Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):
Fixpoint bstep_float f E :option fl64 :=
match f with
| Let m x e g => optionLift (eval_expr_float e E)
(fun v => bstep_float g (updFlEnv x v E))
None
| Let m x e g =>
olet res := eval_expr_float e E in
bstep_float g (updFlEnv x res E)
| Ret e => eval_expr_float e E
end.
Definition isValid e :=
let trans_e := optionLift e (fun v => Some (B2R 53 1024 v)) None in
optionLift trans_e normal_or_zero False.
plet v := e in
normal_or_zero (B2R 53 1024 v).
Fixpoint eval_expr_valid (e:expr fl64) E :=
match e with
......@@ -74,10 +68,10 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
optionLift e1_res
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionLift e2_res
optionBind e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
normal_or_zero (evalBinop b v1_real v2_real))
......@@ -88,13 +82,13 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
let e3_res := eval_expr_float e3 E in
optionLift e1_res
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionLift e2_res
optionBind e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
optionLift e3_res
optionBind e3_res
(fun v3 =>
let v3_real := B2R 53 1024 v3 in
(* No support for fma yet *)
......@@ -110,7 +104,7 @@ Fixpoint bstep_valid f E :=
match f with
| Let m x e g =>
eval_expr_valid e E /\
(optionLift (eval_expr_float e E)
(optionBind (eval_expr_float e E)
(fun v_e => bstep_valid g (updFlEnv x v_e E))
True)
| Ret e => eval_expr_valid e E
......@@ -505,7 +499,7 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) :
eval_expr_float e E2 = Some v /\
eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
Proof.
induction e; simpl in *;
induction e; simpl in *;
intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
valid_roundoffs valid_float_ranges eval_e_float
usedVars_sound is64BitEval_e noDowncast_e eval_IEEE_valid_e
......@@ -513,7 +507,7 @@ Proof.
usedVars_64bit;
(match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
Flover_compute_asm; try congruence; type_conv; subst;
unfold Ltacs.optionLift.
unfold optionBind.
- unfold toREnv in *.
destruct (E2 n) eqn:HE2; try congruence.
exists f; split; try eauto.
......@@ -543,7 +537,7 @@ Proof.
{ repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
- intros; apply usedVars_64bit; set_tac.
- intros; apply usedVars_64bit; set_tac.
- rewrite Heqo, Heqo4, Heqo6.
- rewrite Heqo1, Heqo6, Heqo8.
apply Is_true_eq_true; apply andb_prop_intro; split.
+ apply andb_prop_intro; split; apply Is_true_eq_left; auto.
apply mTypeEq_refl.
......@@ -562,7 +556,7 @@ Proof.
as [v_e2 [eval_float_e2 eval_rel_e2]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
rewrite eval_float_e1, eval_float_e2.
(* rewrite eval_float_e1, eval_float_e2. *)
edestruct (validIntervalbounds_sound (B2Qexpr e2))
as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]];
eauto; set_tac.
......@@ -605,14 +599,13 @@ Proof.
apply Is_true_eq_true.
repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
apply andb_prop_intro; split; auto using Is_true_eq_left.
- inversion Heqo1; subst. rewrite Heqo0. rewrite Heqo.
- inversion Heqo3; subst. Flover_compute.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
rewrite Heqo3, Heqo5.
apply Is_true_eq_left. inversion Heqo2; subst. auto.
- rewrite Heqo, Heqo0.
apply Is_true_eq_left. inversion Heqo4; subst. auto.
- rewrite Heqo1, Heqo2.
apply Is_true_eq_true.
inversion Heqo1; inversion Heqo2; subst.
inversion Heqo3; inversion Heqo4; subst.
repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
assert (validFloatValue (Q2R (B2Q v_e1)) M64).
{ eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac.
......@@ -643,11 +636,11 @@ Proof.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- cbn. Flover_compute.
inversion Heqo1; inversion Heqo2; subst.
inversion Heqo3; inversion Heqo4; subst.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- cbn. Flover_compute.
inversion Heqo1; inversion Heqo2; subst.
inversion Heqo3; inversion Heqo4; subst.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). }
assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R) as no_div_zero_float.
......@@ -674,8 +667,8 @@ Proof.
pose proof (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
(-1022)%Z 53%Z expr_valid)
as rel_error_exists.
rewrite eval_float_e1, eval_float_e2 in H1.
unfold optionLift, normal_or_zero in *; simpl in *.
(* rewrite eval_float_e1, eval_float_e2 in H1. *)
unfold optionBind, normal_or_zero in *; simpl in *.
assert (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64 \/
(evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R.
{ revert H1; intros case_val. destruct case_val; try auto.
......@@ -684,7 +677,7 @@ Proof.
- repeat rewrite <- B2Q_B2R_eq; try auto.
- destruct denormal_b.
assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
{ eapply Rlt_le_trans; eauto.
{ eapply Rlt_le_trans with (r2 := 0); eauto.
repeat rewrite B2Q_B2R_eq; auto. }
lra.
- rewrite B2Q_B2R_eq in zero_b; auto.
......@@ -896,7 +889,7 @@ Proof.
as [v_e3 [eval_float_e3 eval_rel_e3]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
unfold optionLift in H4.
unfold optionBind in H4.
rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H4.
contradiction H4.
- inversion noDowncast_e.
......@@ -937,7 +930,7 @@ Proof.
dVars_sound fVars_defined vars_typed dVars_valid
freeVars_typed;
cbn in *; Flover_compute_asm; try congruence; type_conv; subst;
unfold Ltacs.optionLift;
unfold Ltacs.optionBind;
inversion bstep_float; inversion bstep_real;
inversion ssa_f; subst; simpl in *;
repeat (match goal with
......@@ -1052,7 +1045,7 @@ Proof.
destruct H1 as [HA |[HB | HC]]; try auto; congruence.
- destruct iv_ret; auto.
}
unfold optionLift. rewrite eval_float_e.
unfold optionBind. rewrite eval_float_e.
assert (FloverMap.find (getRetExp (B2Qcmd f)) tMap= Some M64).
{ eapply typingSoundnessCmd; eauto. }
destruct H1 as [vF_new [m_f bstep_float_new]].
......@@ -1094,7 +1087,7 @@ Proof.
+ destruct is64_eval as [HA [HB HC]]; auto.
+ destruct nodowncast_f as [HA HB]; auto.
+ destruct bstep_sound as [eval_sound bstep_sound].
rewrite eval_float_e in bstep_sound; unfold optionLift in bstep_sound.
rewrite eval_float_e in bstep_sound; unfold optionBind in bstep_sound.
auto.
+ unfold dVars_range_valid in *; intros; unfold updEnv.
destruct (v1 =? n) eqn:?.
......
(**
(*
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.MachineType.
Global Set Implicit Arguments.
(**
We define Intervals twice.
First we define intervals of reals and fractions.
......@@ -62,15 +61,3 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) :=
if (y =? x) then Some m else defVars y.
Definition optionLift (V T:Type) (v:option V) default (f: V -> T) :=
match v with
| None => default
| Some val => f val
end.
Ltac optionD :=
match goal with
|H: context[optionLift ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
\ No newline at end of file
......@@ -2,6 +2,8 @@
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Global Set Implicit Arguments.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
......@@ -55,42 +57,53 @@ Ltac Q2R_to_head_step :=
Ltac Q2R_to_head := repeat Q2R_to_head_step.
Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
|Some val => f val
| Some v => f v
| None => e
end.
Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
match v with |Some val => f val | None => e end = optionLift X Y v f e.
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None)
(only parsing, at level 0, t at level 200).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False)
(only parsing, at level 0, t at level 200).
Ltac optionD :=
match goal with
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
Lemma optionBind_eq (X Y: Type) v (f: X -> Y) (e: Y):
match v with |Some val => f val | None => e end = optionBind v f e.
Proof.
reflexivity.
Qed.
Lemma optionLift_cond X (a:bool) (b c :X):
Lemma optionBind_cond X (a:bool) (b c: X):
(if a then b else c) = match a with |true => b |false => c end.
Proof.
reflexivity.
Qed.
Ltac remove_matches := rewrite optionLift_eq in *.
Ltac remove_matches := rewrite optionBind_eq in *.
Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.
Ltac remove_conds := rewrite <- andb_lazy_alt, optionBind_cond in *.
Ltac match_factorize_asm :=
match goal with
| [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
| [ H: ?t = ?u |- context [optionBind ?t _ _]]
=> rewrite H; cbn
| [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
| [ H1: ?t = ?u, H2: context [optionBind ?t _ _] |- _ ]
=> rewrite H1 in H2; cbn in H2
| [ H: context [optionLift _ _ ?t _ _] |- _ ]
| [ H: context [optionBind ?t _ _] |- _ ]
=> destruct t eqn:?; cbn in H; try congruence
end.
Ltac match_factorize :=
match_factorize_asm ||
match goal with
| [ |- context [optionLift _ _ ?t _ _] ]
| [ |- context [optionBind ?t _ _] ]
=> destruct t eqn:?; cbn; try congruence
end.
......@@ -152,7 +165,7 @@ Ltac Flover_compute :=
(* Ltac match_destr t:= *)
(* match goal with *)
(* | H: context [optionLift (FloverMap.find ?k ?M) _ _] |- _ => *)
(* | H: context [optionBind (FloverMap.find ?k ?M) _ _] |- _ => *)
(* destruct (FloverMap.find (elt:=intv * error) k M); idtac H *)
(* end. *)
......@@ -179,4 +192,4 @@ Ltac destruct_ex H pat :=
| _ => destruct H as pat
end.
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
\ No newline at end of file
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment