Commit b9d63736 authored by Heiko Becker's avatar Heiko Becker

Unification of devs, make IEEE eval valid function be a little less strict and forward cakeml

parent b28441ba
......@@ -83,10 +83,11 @@ Fixpoint eval_exp_valid (e:exp fl64) E :=
Fixpoint bstep_valid f E :=
match f with
| Let m x e g => eval_exp_valid e E /\
(optionLift (eval_exp_float e E)
(fun v_e => bstep_valid g (updFlEnv x v_e E))
True)
| Let m x e g =>
eval_exp_valid e E /\
(optionLift (eval_exp_float e E)
(fun v_e => bstep_valid g (updFlEnv x v_e E))
True)
| Ret e => eval_exp_valid e E
end.
......
......@@ -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 3f8f06e6f46b79db0217c67bc1842309900666b4
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