Commit 235270e4 authored by Heiko Becker's avatar Heiko Becker

Merge with Nikitas changes, adding FMAs

parent 61171aef
......@@ -2265,8 +2265,9 @@ Proof.
+ exists (perturb vF (Q2R (mTypeToQ m0)));
exists m0.
econstructor; eauto.
rewrite Rabs_right; try lra.
auto using Rle_ge, mTypeToQ_pos_R.
* rewrite isMorePrecise_morePrecise; auto.
* rewrite Rabs_right; try lra.
auto using Rle_ge, mTypeToQ_pos_R.
+ rewrite Q2R0_is_0 in *. rewrite (delta_0_deterministic _ delta) in *; try auto.
intros * eval_float.
clear eval_float_e.
......
......@@ -109,38 +109,6 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validV
validIntervalbounds e A P validVars
end.
Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err:
validIntervalbounds f A P dVars = true ->
forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) dVars) ->
DaisyMap.find (Var Q v) A = Some (iv, err) ->
Is_true(isSupersetIntv (P v) iv).
Proof.
induction f; cbn; intros approx_true var var_in_fV find_A; set_tac.
- subst.
Daisy_compute.
destruct (var mem dVars) eqn:?; set_tac; try congruence.
Daisy_compute.
unfold isSupersetIntv.
apply andb_prop_intro; split;
apply Is_true_eq_left; auto.
- Daisy_compute; try congruence.
apply IHf; try auto.
set_tac.
- Daisy_compute; try congruence.
destruct H.
+ apply IHf1; try auto; set_tac.
+ apply IHf2; try auto; set_tac.
- Daisy_compute; try congruence.
destruct H.
+ apply IHf1; try auto; set_tac.
+ set_tac.
destruct H.
* apply IHf2; try auto; set_tac.
* apply IHf3; try auto; set_tac.
- Daisy_compute; try congruence.
apply IHf; try auto; set_tac.
Qed.
Corollary Q2R_max4 a b c d:
Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
......@@ -445,8 +413,8 @@ Proof.
eapply swap_Gamma_eval_exp; eauto.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma:
forall E fVars dVars outVars P,
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
forall Gamma E fVars dVars outVars P,
ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A ->
fVars_P_sound fVars E P ->
......@@ -458,7 +426,6 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma:
bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
(Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R.
Proof.
revert Gamma.
induction f;
intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
cbn in *.
......
......@@ -12,7 +12,7 @@ From Daisy
Commands ssaPrgs.
From Daisy
Require Export Infra.ExpressionAbbrevs Infra.RealSimps Infra.NatSet
IntervalArithQ IntervalArith Infra.MachineType.
Infra.MachineType.
Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option mType :=
match e with
......@@ -37,32 +37,10 @@ Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option
| Downcast m e1 =>
let tm1 := typeExpression Gamma e1 in
match tm1 with
|Some m1 => if (isMorePrecise m1 m) then Some m else None
|Some m1 => if (morePrecise m1 m) then Some m else None
|_ => None
end
end.
(*
Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (e': exp Q) : option mType :=
match e with
| Var _ v => if expEq e e' then Gamma v else None
| Const m n => if expEq e e' then Some m else None
| Unop u e1 => if expEq e e' then typeExpression Gamma e else typeMap Gamma e1 e'
| Binop b e1 e2 => if expEq e e' then typeExpression Gamma e
else
match (typeMap Gamma e1 e'), (typeMap Gamma e2 e') with
| Some m1, Some m2 => if (mTypeEq m1 m2) then Some m1 else None
| Some m1, None => Some m1
| None, Some m2 => Some m2
| None, None => None
end
| Fma e1 e2 e3 => if expEq e e' then typeExpression Gamma e
else
match (typeMap Gamma e1 e'), (typeMap Gamma e2 e'), (typeMap Gamma e3 e') with
| Some m1, Some m2, Some m3 => Some (join3 m1 m2 m3)
| _, _, _ => None
end
| Downcast m e1 => if expEq e e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'
end. *)
Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (tMap:DaisyMap.t mType)
: DaisyMap.t mType :=
......@@ -103,7 +81,7 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (tMap:DaisyMap.t mType)
end
| Downcast m e1 =>
let tMap_new := typeMap Gamma e1 tMap in
let m1 := DaisyMap.find e1 tMap in
let m1 := DaisyMap.find e1 tMap_new in
match m1 with
| Some t1 =>
if (morePrecise t1 m)
......@@ -116,7 +94,7 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (tMap:DaisyMap.t mType)
Fixpoint typeCmd (Gamma:nat -> option mType) (f:cmd Q): option mType :=
match f with
|Let m n e c => match typeExpression Gamma e with
|Some m' => if isMorePrecise m m' then typeCmd Gamma c
|Some m' => if morePrecise m m' then typeCmd Gamma c
else None
|None => None
end
......@@ -173,7 +151,7 @@ Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType)
| _, _, _, _ => false
end
| Downcast m e1 => match DaisyMap.find e tMap, DaisyMap.find e1 tMap with
| Some m', Some m1 => mTypeEq m m' && isMorePrecise m1 m && typeCheck e1 Gamma tMap
| Some m', Some m1 => mTypeEq m m' && morePrecise m1 m && typeCheck e1 Gamma tMap
| _, _ => false
end
end.
......@@ -193,86 +171,6 @@ Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType)
| Ret e => typeCheck e Gamma tMap
end.
(* Lemma eqTypeExpression e m Gamma: *)
(* typeMap Gamma e e = Some m <-> typeExpression Gamma e = Some m. *)
(* Proof. *)
(* revert m Gamma; induction e; intros. *)
(* - split; intros. *)
(* + simpl in *. *)
(* rewrite <- beq_nat_refl in H; simpl in H; auto. *)
(* + simpl in *. *)
(* rewrite <- beq_nat_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite mTypeEq_refl,Qeq_bool_refl in H; simpl in H; auto. *)
(* + rewrite mTypeEq_refl,Qeq_bool_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite unopEqBool_refl,expEq_refl in H; simpl in H; auto. *)
(* + rewrite unopEqBool_refl,expEq_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite binopEqBool_refl,expEq_refl,expEq_refl in H; simpl in H; auto. *)
(* + rewrite binopEqBool_refl,expEq_refl,expEq_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite mTypeEq_refl,expEq_refl in H; simpl in H; auto. *)
(* + rewrite mTypeEq_refl,expEq_refl; simpl; auto. *)
(* Qed. *)
(* Definition Gamma_stronger (Gamma1 Gamma2: exp Q -> option mType):= *)
(* (forall e m, Gamma1 e = Some m -> Gamma2 e = Some m). *)
(* Lemma Gamma_stronger_trans Gamma1 Gamma2 Gamma3 : *)
(* Gamma_stronger Gamma1 Gamma2 -> *)
(* Gamma_stronger Gamma2 Gamma3 -> *)
(* Gamma_stronger Gamma1 Gamma3. *)
(* Proof. *)
(* intros g12 g23 e m hyp. *)
(* unfold Gamma_stronger in g12,g23. *)
(* apply g23; apply g12; auto. *)
(* Qed. *)
(* Lemma Gamma_strengthening e Gamma1 Gamma2 Gamma: *)
(* Gamma_stronger Gamma1 Gamma2 -> *)
(* typeCheck e Gamma Gamma1 = true -> *)
(* typeCheck e Gamma Gamma2 = true. *)
(* Proof. *)
(* revert Gamma1 Gamma2; induction e; intros. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Var Q n)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* specialize (H _ _ H1); rewrite H. *)
(* auto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Const m v)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* specialize (H _ _ H1); rewrite H. *)
(* auto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Unop u e)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* rewrite (H _ _ H1). *)
(* case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ]. *)
(* apply andb_true_iff in H0; destruct H0. *)
(* apply mTypeEq_compat_eq in H0; subst. *)
(* rewrite (H _ _ H2). *)
(* rewrite mTypeEq_refl; simpl. *)
(* eapply IHe; eauto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Binop b e1 e2)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* case_eq (Gamma1 e1); intros; rewrite H2 in H0; [ | inversion H0 ]. *)
(* case_eq (Gamma1 e2); intros; rewrite H3 in H0; [ | inversion H0 ]. *)
(* rewrite (H _ _ H1), (H _ _ H2), (H _ _ H3). *)
(* andb_to_prop H0. *)
(* rewrite L0; simpl. *)
(* apply andb_true_iff; split. *)
(* + eapply IHe1; eauto. *)
(* + eapply IHe2; eauto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Downcast m e)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ]. *)
(* rewrite (H _ _ H1), (H _ _ H2). *)
(* andb_to_prop H0. *)
(* rewrite L0, R0; simpl. *)
(* eapply IHe; eauto. *)
(* Qed. *)
Theorem typingSoundnessExp Gamma E:
forall e v m expTypes,
typeCheck e Gamma expTypes = true ->
......
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