Commit 46c47dcf authored by Heiko Becker's avatar Heiko Becker
Browse files

Add some comments to IEEE connection script

parent b1a06c0a
......@@ -13,22 +13,34 @@ Definition valid_div a b (f:binary_float a b):=
Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_float 53 1024)):=
match e with
|Const c => Some c
|Const c => if (is_finite 53 1024 c) then Some c else None
|Var _ x => E x
|Binop b e1 e2 =>
match eval_exp_float e1 E, eval_exp_float e2 E with
|Some f1, Some f2 =>
|Some f1, Some f2 =>
if (is_finite 53 1024 f1 && is_finite 53 1024 f2)
then
match b with
|Plus => Some (b64_plus mode_NE f1 f2)
|Sub => Some (b64_minus mode_NE f1 f2)
|Mult => Some (b64_mult mode_NE f1 f2)
|Div => if (valid_div f2) then Some (b64_div mode_NE f1 f2) else None
end
else
None
|_ , _ => None
end
| _ => None
end.
Lemma eval_exp_float_finite e E:
forall v, eval_exp_float e E = Some v ->
(forall n, exists v, E n = Some v -> Is_true (is_finite 53 1024 v)) ->
Is_true (is_finite 53 1024 v).
Proof.
induction e.
- intros v eval_v; simpl in
Fixpoint toRExp e :=
match e with
|Const c => Const (B2R 53 1024 c)
......@@ -142,7 +154,13 @@ Proof.
try congruence; try auto.
Qed.
(* Hypothesis Environment not finite --> remove finiteness assumption
no_overflow and no_underflow need to check only for expression in question.
As is they are ~ false, move the checks into eval function!
*)
Theorem eval_gives_sem e E v:
(forall v,
exists q, E v = Some q -> is_finite 53 1024 q = true) ->
eval_exp_float e E = Some v ->
no_overflow_in_eval ->
no_underflow_in_eval ->
......
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