Commit 08ae87fa authored by Joachim Bard's avatar Joachim Bard

removing conditionals from validators

parent 89142369
......@@ -126,8 +126,7 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
| _,_ => false
end
else false
| Cond e1 e2 e3 => false
(* TODO *)
(* | Cond e1 e2 e3 => false *)
end
else false
| _, _ => false
......
......@@ -455,7 +455,7 @@ Proof.
intros ?; subst. apply H3. set_tac. }
eapply validErrorBounds_single in H2; eauto.
destruct H2. eapply H3; eauto.
- cbn in *. Flover_compute; congruence.
(* - cbn in *. Flover_compute; congruence. *)
Qed.
(*
......
......@@ -22,10 +22,12 @@ Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e}
| Let _ x e1 e2 =>
FPRangeValidator e1 A typeMap dVars &&
FPRangeValidator e2 A typeMap (NatSet.add x dVars)
(*
| Cond e1 e2 e3 =>
FPRangeValidator e1 A typeMap dVars &&
FPRangeValidator e2 A typeMap dVars &&
FPRangeValidator e3 A typeMap dVars
*)
| _ => true
end
in
......@@ -157,6 +159,7 @@ Proof.
subst.
Flover_compute; try congruence.
prove_fprangeval m v L1 R.
(*
- inversion H1; subst.
+ destruct H2 as [mE [find_mE [[validt_e1 [validt_e2 [validt_e3 [m_e1 [m_e2 [m_e3 [find_m1 [find_m2 [find_m3 join_valid]]]]]]]]] _ ]]].
assert (m_e1 = m1) by (eapply validTypes_exec in find_m1; eauto).
......@@ -170,6 +173,7 @@ Proof.
subst.
Flover_compute; try congruence.
prove_fprangeval m v L1 R.
*)
Qed.
(*
......
......@@ -113,7 +113,7 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv)
| _, _, _ => false
end
else false
| Cond f1 f2 f3 => false
(* | Cond f1 f2 f3 => false *)
(*
if ((validIntervalbounds f1 A P validVars) &&
(validIntervalbounds f2 A P validVars) &&
......@@ -438,7 +438,7 @@ Proof.
repeat split; eauto; try lra.
econstructor; eauto; try reflexivity.
rewrite Rabs_R0. cbn; lra.
- Flover_compute. congruence.
(* - Flover_compute. congruence. *)
Qed.
(*
......
......@@ -257,7 +257,7 @@ Proof.
destruct m1; try discriminate.
now apply IHe'.
- cbn. congruence.
- cbn. congruence.
(* - cbn. congruence. *)
Qed.
Lemma eval_smt_expr E e v :
......@@ -535,7 +535,7 @@ Proof with try discriminate.
destruct P as [Piv C]. cbn.
induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl] in q |- *.
- cbn. intros Heq [_ H]. now apply (SMTLogic_eqb_sound _ C).
- destruct e as [x| | | | | | |].
- destruct e as [x| | | | | |].
all: try now (cbn; intros Heq [H1 H2]; apply IHl; auto).
cbn.
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
......
......@@ -40,7 +40,7 @@ Fixpoint inlineLets (L: let_env) (e: expr Q) :=
| Fma e1 e2 e3 => Fma (inlineLets L e1) (inlineLets L e2) (inlineLets L e3)
| Downcast m e' => Downcast m (inlineLets L e')
| Let m x e1 e2 => Let m x (inlineLets L e1) (inlineLets L e2)
| Cond e1 e2 e3 => Cond (inlineLets L e1) (inlineLets L e2) (inlineLets L e3)
(* | Cond e1 e2 e3 => Cond (inlineLets L e1) (inlineLets L e2) (inlineLets L e3) *)
end.
Lemma inlineLets_sound L E Gamma inVars outVars e v :
......@@ -119,6 +119,7 @@ Proof.
set_tac. intros ?.
apply H12. eapply LfVars_valid; eauto.
set_tac.
(*
- inversion H; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
......@@ -130,6 +131,7 @@ Proof.
subst.
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eapply Cond_else; eauto.
*)
Qed.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P L :=
......@@ -324,7 +326,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
| _, _, _ => false
end
else false
| Cond f1 f2 f3 => false
(* | Cond f1 f2 f3 => false *)
(*
if ((validSMTIntervalbounds f1 A P validVars) &&
(validSMTIntervalbounds f2 A P validVars) &&
......@@ -667,7 +669,7 @@ Proof.
repeat split; eauto; try lra.
econstructor; eauto; try reflexivity.
rewrite Rabs_R0. cbn; lra.
- Flover_compute. congruence.
(* - Flover_compute. congruence. *)
Qed.
(*
......
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