Commit 81e8172d authored by Nikita Zyuzin's avatar Nikita Zyuzin

Fix merge errors in Typing

parent ecccb575
......@@ -99,7 +99,7 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (tMap:DaisyMap.t mType)
let m3 := DaisyMap.find e3 tMap3 in
match m1, m2, m3 with
|Some t1, Some t2, Some t3 => DaisyMap.add e (join3 t1 t2 t3) tMap3
| _, _ => DaisyMap.empty mType
| _, _, _ => DaisyMap.empty mType
end
| Downcast m e1 =>
let tMap_new := typeMap Gamma e1 tMap in
......@@ -164,7 +164,7 @@ Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType)
&& typeCheck e2 Gamma tMap
| _, _, _ => false
end
| Fma e1 e2 e3 => match DaisyMap.find e, DaisyMap.find e1, DaisyMap.find e2, DaisyMap.find e3 with
| Fma e1 e2 e3 => match DaisyMap.find e tMap, DaisyMap.find e1 tMap, DaisyMap.find e2 tMap, DaisyMap.find e3 tMap with
| Some m, Some m1, Some m2, Some m3 =>
mTypeEq m (join3 m1 m2 m3)
&& typeCheck e1 Gamma tMap
......@@ -287,19 +287,10 @@ Proof.
- erewrite IHe1 in *; eauto.
erewrite IHe2 in *; eauto.
inversion Heqo0; subst; inversion Heqo1; subst; auto.
- inversion evals; subst.
simpl in typechecks.
case_eq (expTypes (Fma e1 e2 e3)); intros; rewrite H in typechecks; [ | inversion typechecks ].
case_eq (expTypes e1); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
case_eq (expTypes e2); intros; rewrite H1 in typechecks; [ | inversion typechecks ].
case_eq (expTypes e3); intros; rewrite H4 in typechecks; [ | inversion typechecks ].
andb_to_prop typechecks.
apply mTypeEq_compat_eq in L; subst.
assert (expTypes e1 = Some m1) by (eapply IHe1; eauto).
assert (expTypes e2 = Some m2) by (eapply IHe2; eauto).
assert (expTypes e3 = Some m3) by (eapply IHe3; eauto).
rewrite H0 in H5; rewrite H1 in H8; rewrite H4 in H9.
now inversion H5; inversion H8; inversion H9.
- erewrite IHe1 in *; eauto.
erewrite IHe2 in *; eauto.
erewrite IHe3 in *; eauto.
inversion Heqo0; subst; inversion Heqo1; subst; inversion Heqo2; subst; auto.
Qed.
Theorem typingSoundnessCmd c Gamma E v m expTypes:
......
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