Commit e3dfce9e authored by Joachim Bard's avatar Joachim Bard

removing conditionals from IEEE

parent 08ae87fa
...@@ -112,7 +112,7 @@ Fixpoint eval_expr_valid (e:expr fl64) E := ...@@ -112,7 +112,7 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
(optionBind (eval_expr_float e1 E) (optionBind (eval_expr_float e1 E)
(fun v_e => eval_expr_valid e2 (updFlEnv x v_e E)) (fun v_e => eval_expr_valid e2 (updFlEnv x v_e E))
True) True)
| Cond e1 e2 e3 => False (* | Cond e1 e2 e3 => False *)
end. end.
(* (*
...@@ -195,7 +195,7 @@ Fixpoint B2Qexpr (e: expr fl64) := ...@@ -195,7 +195,7 @@ Fixpoint B2Qexpr (e: expr fl64) :=
| Fma e1 e2 e3 => Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3) | Fma e1 e2 e3 => Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)
| Downcast m e => Downcast m (B2Qexpr e) | Downcast m e => Downcast m (B2Qexpr e)
| Let m x e1 e2 => Let m x (B2Qexpr e1) (B2Qexpr e2) | Let m x e1 e2 => Let m x (B2Qexpr e1) (B2Qexpr e2)
| Cond e1 e2 e3 => Cond (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3) (* | Cond e1 e2 e3 => Cond (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3) *)
end. end.
(* (*
...@@ -226,7 +226,7 @@ Fixpoint is64BitEval (V:Type) (e:expr V) := ...@@ -226,7 +226,7 @@ Fixpoint is64BitEval (V:Type) (e:expr V) :=
| Fma e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3 | Fma e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3
| Downcast m e => m = M64 /\ is64BitEval e | Downcast m e => m = M64 /\ is64BitEval e
| Let m x e g => is64BitEval e /\ m = M64 /\ is64BitEval g | Let m x e g => is64BitEval e /\ m = M64 /\ is64BitEval g
| Cond e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3 (* | Cond e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3 *)
end. end.
(* (*
...@@ -246,7 +246,7 @@ Fixpoint noDowncast (V:Type) (e:expr V) := ...@@ -246,7 +246,7 @@ Fixpoint noDowncast (V:Type) (e:expr V) :=
| Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3 | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
| Downcast m e => False | Downcast m e => False
| Let m x e1 e2 => noDowncast e1 /\ noDowncast e2 | Let m x e1 e2 => noDowncast e1 /\ noDowncast e2
| Cond e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3 (* | Cond e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3 *)
end. end.
(* (*
...@@ -1151,6 +1151,7 @@ Proof. ...@@ -1151,6 +1151,7 @@ Proof.
destruct (mTypeEq M64 m1) eqn:?; congruence. destruct (mTypeEq M64 m1) eqn:?; congruence.
*) *)
admit. admit.
(*
- destruct (getValidMap defVars e1 akk) eqn:?; - destruct (getValidMap defVars e1 akk) eqn:?;
simpl in *; try congruence. simpl in *; try congruence.
destruct (getValidMap defVars e2 t) eqn:?; destruct (getValidMap defVars e2 t) eqn:?;
...@@ -1189,6 +1190,7 @@ Proof. ...@@ -1189,6 +1190,7 @@ Proof.
inversion getMap_succeeds; subst. inversion getMap_succeeds; subst.
find_cases; try (eapply valid_t1; now eauto). find_cases; try (eapply valid_t1; now eauto).
congruence. congruence.
*)
Admitted. Admitted.
(* (*
......
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