Commit c77e6a53 authored by Heiko Becker's avatar Heiko Becker
Browse files

update cakeml, merge

parents 31101bbd b9d63736
......@@ -86,3 +86,19 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
| Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
| Ret e => usedVars e
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
+ auto.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
\ No newline at end of file
......@@ -432,6 +432,19 @@ Proof.
econstructor; try auto.
Qed.
Lemma eval_eq_env e:
forall E1 E2 Gamma v m,
(forall x, E1 x = E2 x) ->
eval_exp E1 Gamma e v m ->
eval_exp E2 Gamma e v m.
Proof.
induction e; intros;
(match_pat (eval_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
try eauto.
eapply Var_load; auto.
rewrite <- (H n); auto.
Qed.
(*
(**
Analogous lemma for unary expressions.
......
This diff is collapsed.
......@@ -146,17 +146,17 @@ Definition join (m1:mType) (m2:mType) :=
(* destruct m1, m2; simpl in *; cbv in *; try congruence; try auto. *)
(* Qed. *)
Definition maxExponent (m:mType) :Z :=
Definition maxExponent (m:mType) :positive :=
match m with
| M0 => 0
| M0 => 1
| M16 => 15
| M32 => 127
| M64 => 1023
end.
Definition minExponentPos (m:mType) :Z :=
Definition minExponentPos (m:mType) :positive :=
match m with
| M0 => 0
| M0 => 1
| M16 => 14
| M32 => 126
| M64 => 1022
......@@ -169,16 +169,16 @@ Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
which simplifies to 2^(e_max) for base 2
**)
Definition maxValue (m:mType) :=
Qpower (2#1) (maxExponent m).
(Z.pow_pos 2 (maxExponent m)) # 1.
Definition minValue (m:mType) :=
Qinv (Qpower (2#1) (minExponentPos m)).
Qinv ((Z.pow_pos 2 (minExponentPos m)) # 1).
(** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
𝛃^(e_min -p + 1) = 𝛃^(e_min -1) for base 2
**)
Definition minDenormalValue (m:mType) :=
Qinv (Qpower (2#1) (minExponentPos m - 1)).
Qinv (Z.pow_pos 2 (minExponentPos m - 1) # 1).
Definition normal (v:Q) (m:mType) :=
Qle_bool (minValue m) (Qabs v) && Qle_bool (Qabs v) (maxValue m).
......@@ -190,7 +190,7 @@ Definition Normal (v:R) (m:mType) :=
(Q2R (minValue m) <= (Rabs v) /\ (Rabs v) <= Q2R (maxValue m))%R.
Definition Denormal (v:R) (m:mType) :=
((Rabs v) <= Q2R (minValue m) /\ ~ (v = 0))%R.
((Rabs v) < Q2R (minValue m) /\ ~ (v = 0))%R.
(**
Predicate that is true if and only if the given value v is a valid
floating-point value according to the the type m.
......
......@@ -58,29 +58,31 @@ val isValid_def = Define `
optionLift trans_e normal_or_zero F`;
val eval_exp_valid_def = Define `
(eval_exp_valid (Var n) E = T (*isValid (eval_exp_float (Var n) E)*)) /\
(eval_exp_valid (Const m v) E = T (*isValid (eval_exp_float (Const m v) E)*)) /\
(eval_exp_valid (Var n) E = T) /\
(eval_exp_valid (Const m v) E = T) /\
(eval_exp_valid (Unop u e) E = eval_exp_valid e E) /\
(*if eval_exp_valid e E
then isValid (eval_exp_float (Unop u e) E)
else F *)
(eval_exp_valid (Binop b e1 e2) E =
if (eval_exp_valid e1 E /\ eval_exp_valid e2 E)
then
let e1_res = eval_exp_float e1 E in
let e2_res = eval_exp_float e2 E in
optionLift (e1_res)
(\ v1. let v1_real = float_to_real (fp64_to_float v1) in
optionLift e2_res (\ v2.
let v2_real = float_to_real (fp64_to_float v2) in
normal_or_zero (evalBinop b v1_real v2_real)) F) F
else F)`;
(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
optionLift (e1_res)
(\ v1. let v1_real = float_to_real (fp64_to_float v1)
in
optionLift e2_res
(\ v2.
let v2_real = float_to_real (fp64_to_float v2)
in
normal_or_zero (evalBinop b v1_real v2_real))
T)
T)) /\
(eval_exp_valid (Downcast m e) E = eval_exp_valid e E)`;
val bstep_valid_def = Define `
(bstep_valid (Let m x e g) E =
optionLift (eval_exp_float e E)
(\v_e. eval_exp_valid e E /\ bstep_valid g (updFlEnv x v_e E))
F) /\
(eval_exp_valid e E /\
optionLift (eval_exp_float e E)
(\v_e. bstep_valid g (updFlEnv x v_e E))
T)) /\
(bstep_valid (Ret e) E = eval_exp_valid e E)`;
val toRExp_def = Define `
......@@ -1125,8 +1127,6 @@ val bstep_gives_IEEE = store_thm (
\\ fs[SUBSET_DEF, domain_union]
\\ `n IN domain fVars \/ n IN domain dVars`
by (first_x_assum irule \\ fs[]))
>- (fs[optionLift_def] \\ Cases_on `eval_exp_float e E2`
\\ fs[optionLift_def])
>- (rveq \\ asm_exists_tac \\ fs[])
\\ fs [Once validIntervalboundsCmd_def, Once validErrorboundCmd_def,
Once typeCheckCmd_def, Once FPRangeValidatorCmd_def]
......@@ -1167,7 +1167,6 @@ val bstep_gives_IEEE = store_thm (
\\ qexists_tac `M64` \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
(* Now construct a new evaluation according to our big-step semantics
using lemma validErrorboundCmd_gives_eval *)
(* CONTINUE HERE *)
\\ Cases_on `A (getRetExp (toRCmd f))`
\\ rename1 `A (getRetExp _) = (iv_f,err_f)`
\\ Cases_on `iv_f` \\ rename1 `A (getRetExp _) = ((f_lo, f_hi), err_f)`
......
Subproject commit 9f7a2e8b53e4f091ae49340aed425376ed30ae26
Subproject commit 4273d509b99f86716a40d18895a091bbd043f24d
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