Commit 0a00766a authored by Nikita Zyuzin's avatar Nikita Zyuzin

Start resolving compilation issues

parent 37d050e2
......@@ -50,9 +50,9 @@ 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 =>
olet res := eval_exp_float e E in
olet res := eval_expr_float e E in
bstep_float g (updFlEnv x res E)
| Ret e => eval_exp_float e E
| Ret e => eval_expr_float e E
end.
Definition isValid e :=
......@@ -65,9 +65,9 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
| Const m v => True (*isValid (eval_expr_float (Const m v) E)*)
| Unop u e => eval_expr_valid e E
| Binop b e1 e2 =>
(eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\
(let e1_res := eval_exp_float e1 E in
let e2_res := eval_exp_float e2 E in
(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
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
......@@ -78,10 +78,10 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
True)
True)
| Fma e1 e2 e3 =>
(eval_exp_valid e1 E) /\ (eval_exp_valid e2 E) /\ (eval_exp_valid e3 E) /\
(let e1_res := eval_exp_float e1 E in
let e2_res := eval_exp_float e2 E in
let e3_res := eval_exp_float e3 E in
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\ (eval_expr_valid e3 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
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
......@@ -103,8 +103,8 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
Fixpoint bstep_valid f E :=
match f with
| Let m x e g =>
eval_exp_valid e E /\
(optionBind (eval_exp_float e E)
eval_expr_valid 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
......@@ -499,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
......@@ -537,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.
......@@ -556,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.
......@@ -599,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.
......@@ -637,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.
......@@ -668,7 +667,7 @@ 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.
(* 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.
......@@ -678,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.
......
(**
(*
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,18 +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 optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
| Some v => f v
| None => e
end.
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None) (at level 0, t at level 200).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False) (at level 0, t at level 200).
Ltac optionD :=
match goal with
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
(** Ltac definitions **)
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.Abbrevs Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
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,6 +57,23 @@ Ltac Q2R_to_head_step :=
Ltac Q2R_to_head := repeat Q2R_to_head_step.
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
| Some v => f v
| None => e
end.
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.
......@@ -173,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