Commit 37d050e2 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Rename 'optionLift' with 'optionBind'

Introduce useful notations for it
parent ddc04b14
......@@ -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
| Ret e => eval_expr_float e E
| Let m x e g =>
olet res := eval_exp_float e E in
bstep_float g (updFlEnv x res E)
| Ret e => eval_exp_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
......@@ -71,30 +65,30 @@ 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_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
(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
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))
True)
True)
| Fma e1 e2 e3 =>
(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
optionLift e1_res
(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
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 *)
......@@ -109,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_expr_valid e E /\
(optionLift (eval_expr_float e E)
eval_exp_valid e E /\
(optionBind (eval_exp_float e E)
(fun v_e => bstep_valid g (updFlEnv x v_e E))
True)
| Ret e => eval_expr_valid e 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.
......@@ -675,7 +669,7 @@ Proof.
(-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 *.
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.
......@@ -896,7 +890,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 +931,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 +1046,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 +1088,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:?.
......
......@@ -63,14 +63,17 @@ 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) :=
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
| None => default
| Some val => f val
| 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[optionLift ?v ?default ?f] |- _ =>
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
\ No newline at end of file
end.
(** Ltac definitions **)
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.
Require Import Flover.Infra.RealSimps Flover.Infra.Abbrevs Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
......@@ -55,42 +55,36 @@ 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) :=
match v with
|Some val => f val
| 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.
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 +146,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. *)
......
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