Commit ac33f759 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Finish dealing with dVars

parent 4acafade
...@@ -1198,8 +1198,11 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid ...@@ -1198,8 +1198,11 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
olet res__e := validAffineBounds e A P validVars exprsAf currentMaxNoise in olet res__e := validAffineBounds e A P validVars exprsAf currentMaxNoise in
let (exprsAf', noise') := res__e in let (exprsAf', noise') := res__e in
olet eaf := FloverMap.find e exprsAf' in olet eaf := FloverMap.find e exprsAf' in
validAffineBoundsCmd c' A P (NatSet.add x validVars) match FloverMap.find (Var Q x) exprsAf' with
| Some _ => None
| None => validAffineBoundsCmd c' A P (NatSet.add x validVars)
(FloverMap.add (Var Q x) eaf exprsAf') noise' (FloverMap.add (Var Q x) eaf exprsAf') noise'
end
else None else None
| _, _ => None | _, _ => None
end end
...@@ -1244,7 +1247,7 @@ Proof. ...@@ -1244,7 +1247,7 @@ Proof.
destruct p as (exprAfs', noise'). destruct p as (exprAfs', noise').
destruct (FloverMap.find e exprAfs') eqn: Heaf; simpl in valid_bounds_cmd; try congruence. destruct (FloverMap.find e exprAfs') eqn: Heaf; simpl in valid_bounds_cmd; try congruence.
rename a into eaf. rename a into eaf.
simpl in valid_bounds_cmd. destruct (FloverMap.find (elt:=affine_form Q) (Var Q n) exprAfs') eqn: Hvar; try congruence.
inversion Hssa; subst. inversion Hssa; subst.
pose proof validAffineBounds_sound as validab_sound. pose proof validAffineBounds_sound as validab_sound.
simpl in Hsubset. simpl in Hsubset.
...@@ -1378,7 +1381,8 @@ Proof. ...@@ -1378,7 +1381,8 @@ Proof.
exists ihmap, ihaf, ihvR, ihaiv, ihaerr. exists ihmap, ihaf, ihvR, ihaiv, ihaerr.
assert (contained_map map1 ihmap) as ? assert (contained_map map1 ihmap) as ?
by (etransitivity; eassumption). by (etransitivity; eassumption).
assert (contained_flover_map exprAfs' (FloverMap.add (Var Q n) eaf exprAfs')) as ? by admit. assert (contained_flover_map exprAfs' (FloverMap.add (Var Q n) eaf exprAfs')) as ?
by (apply contained_flover_map_extension; assumption).
assert (contained_flover_map iexpmap exprAfs) as ? assert (contained_flover_map iexpmap exprAfs) as ?
by (etransitivity; try eassumption; etransitivity; try eassumption). by (etransitivity; try eassumption; etransitivity; try eassumption).
intuition. intuition.
...@@ -1394,4 +1398,4 @@ Proof. ...@@ -1394,4 +1398,4 @@ Proof.
all: try eassumption. all: try eassumption.
constructor. constructor.
eauto. eauto.
Admitted. 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