Commit 3f0f4ba7 authored by ='s avatar =

Cleaning Typing.v

parent 3b48bf01
(* It would be nice to have the theorem typeMapChecks proved someday. *)
Lemma typeMapUnopUnfolding u e e0 defVars m0:
typeMap defVars (Unop u e) e0 = Some m0 ->
expEqBool (Unop u e) e0 = false ->
typeMap defVars e e0 = Some m0.
Proof.
revert e e0 m0; destruct e0; intros.
- simpl in H; auto.
- simpl in H; auto.
- simpl in H, H0; rewrite H0 in H; auto.
- simpl in H; auto.
- simpl in H; auto.
Qed.
Lemma typeCheckLeftUnfolding Gamma u e defVars:
typeCheck (Unop u e) defVars Gamma = true ->
typeCheck e defVars Gamma = true.
Proof.
intros tc_u.
simpl in *.
case_eq (Gamma (Unop u e)); intros; rewrite H in tc_u; [ | inversion tc_u ].
case_eq (Gamma e); intros; rewrite H0 in tc_u; [ | inversion tc_u ].
apply andb_true_iff in tc_u; destruct tc_u; auto.
Qed.
Lemma stupidlemma e defVars Gamma:
typeCheck e defVars Gamma = true ->
exists m, Gamma e = Some m.
Proof.
destruct e; intros * tc.
- simpl in *.
case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ].
eauto.
- simpl in *.
case_eq (Gamma (Const m q)); intros; rewrite H in tc; [ | inversion tc ].
eauto.
- simpl in *.
case_eq (Gamma (Unop u e)); intros; rewrite H in tc; [ | inversion tc ].
eauto.
- simpl in *;
case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in tc; [ | inversion tc ]; eauto.
- simpl in *;
case_eq (Gamma (Downcast m e)); intros; rewrite H in tc; [ | inversion tc ]; eauto.
Qed.
Fixpoint defVarsWellDefined (e:exp Q) (defVars:nat -> option mType) : bool :=
NatSet.for_all (fun v => match defVars v with | Some m => true | _ => false end) (usedVars e).
Fixpoint defVarsWellDefinedCmd c defVars : bool :=
match c with
| Let m x e g => match defVars x with
| Some m' => mTypeEqBool m m' && defVarsWellDefined e defVars && defVarsWellDefinedCmd g defVars
| _ => false
end
| Ret e => defVarsWellDefined e defVars
end.
Theorem typeExpressionChecks e defVars:
defVarsWellDefined e defVars = true ->
typeCheck e defVars (fun e => typeExpression defVars e) = true.
Proof.
intros defVars_wd. induction e.
- simpl in *.
apply NatSet.for_all_spec in defVars_wd; try auto.
Focus 2. intros a b c; rewrite c; auto.
specialize (defVars_wd n).
rewrite NatSet.singleton_spec in defVars_wd.
assert (n = n) by auto; specialize (defVars_wd H).
case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ].
rewrite mTypeEqBool_refl; auto.
- simpl.
rewrite mTypeEqBool_refl; auto.
- simpl in *.
assert (defVarsWellDefined e defVars = true) by admit.
specialize (IHe H).
pose proof (stupidlemma _ _ _ IHe) as [me type_e].
rewrite type_e, mTypeEqBool_refl; simpl.
auto.
- simpl in *.
assert (defVarsWellDefined e1 defVars = true) by admit.
specialize (IHe1 H).
assert (defVarsWellDefined e2 defVars = true) by admit.
specialize (IHe2 H0).
pose proof (stupidlemma _ _ _ IHe1) as [me1 type_e1].
pose proof (stupidlemma _ _ _ IHe2) as [me2 type_e2].
rewrite type_e1,type_e2,mTypeEqBool_refl; simpl; auto.
rewrite IHe1, IHe2; auto.
-
unfold typeCheck.
simpl in *.
assert (defVarsWellDefined e defVars = true) by admit.
specialize (IHe H).
pose proof (stupidlemma _ _ _ IHe) as [me type_e].
rewrite type_e.
assert (typeExpression defVars (Downcast m e) = Some m).
{ simpl; rewrite type_e.
Theorem typeMapChecks e defVars:
defVarsWellDefined e defVars = true ->
(*(forall v, NatSet.In v (usedVars e) -> exists m, defVars v = Some m) ->*)
typeCheck e defVars (typeMap defVars e) = true.
Proof.
intros defVars_wd; induction e; intros.
- simpl in *; rewrite <- beq_nat_refl.
rewrite NatSet.for_all_spec in defVars_wd.
+ unfold NatSet.For_all in defVars_wd.
specialize (defVars_wd n).
rewrite NatSet.singleton_spec in defVars_wd.
assert (n = n) by auto; specialize (defVars_wd H).
case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ].
rewrite mTypeEqBool_refl; auto.
+ intros a b hyp; rewrite hyp; auto.
- simpl in *.
rewrite mTypeEqBool_refl, Qeq_bool_refl; simpl.
rewrite mTypeEqBool_refl; auto.
- simpl.
rewrite unopEqBool_refl, expEqBool_refl; simpl.
assert (defVarsWellDefined e defVars = true) by admit.
specialize (IHe H).
pose proof (stupidlemma _ _ _ IHe) as [m type_e].
apply eqTypeExpression in type_e.
rewrite type_e.
case_eq (expEqBool (Unop u e) e); intros; simpl in H0; rewrite H0.
+ admit.
+ apply eqTypeExpression in type_e; rewrite type_e.
rewrite mTypeEqBool_refl; simpl.
eapply Gamma_strengthening.
Focus 2. eapply IHe.
intros e0 m0 type_e0.
case_eq (expEqBool (Unop u e) e0); intros; simpl in H1; rewrite H1.
* admit.
* auto.
- unfold typeCheck.
assert (defVarsWellDefined e1 defVars = true) by admit.
assert (defVarsWellDefined e2 defVars = true) by admit.
specialize (IHe1 H).
specialize (IHe2 H0).
pose proof (stupidlemma _ _ _ IHe1) as [m1 tMap_e1].
pose proof (stupidlemma _ _ _ IHe2) as [m2 tMap_e2].
assert (typeMap defVars (Binop b e1 e2) (Binop b e1 e2) = Some (computeJoin m1 m2)) as tMap_binop.
{ simpl; rewrite binopEqBool_refl,?expEqBool_refl; simpl.
rewrite eqTypeExpression in tMap_e1, tMap_e2.
rewrite tMap_e1, tMap_e2.
auto. }
rewrite tMap_binop.
assert (typeMap defVars (Binop b e1 e2) e1 = Some m1).
{ simpl.
assert (expEqBool (Binop b e1 e2) e1 = false) by admit; simpl in H1; rewrite H1.
rewrite tMap_e1.
Admitted.
Theorem typeMapCmdChecks c defVars:
defVarsWellDefinedCmd c defVars = true ->
typeCheckCmd c defVars (typeMapCmd defVars c) = true.
Proof.
intros defVars_wd; induction c; intros.
- unfold typeCheckCmd.
assert (typeMapCmd defVars (Let m n e c) (Var Q n) = Some m).
{ unfold typeMapCmd. simpl; rewrite <- beq_nat_refl.
simpl in defVars_wd.
case_eq (defVars n); intros; rewrite H in defVars_wd; [ | inversion defVars_wd ].
andb_to_prop defVars_wd.
rewrite L0; simpl; auto. }
rewrite H.
assert (typeMapCmd defVars (Let m n e c) e = Some m).
{ simpl.
case_eq (expEqBool e (Var Q n)); intros.
- admit.
-
Admitted.
Theorem typeMapChecks2 e defVars Gamma:
(forall v, NatSet.In v (usedVars e) -> exists m, defVars v = Some m) ->
Gamma_stronger (typeMap defVars e) Gamma ->
typeCheck e defVars Gamma = true.
Proof.
intros defVars_wd gamma_st.
induction e; intros.
- simpl.
unfold Gamma_stronger in gamma_st.
specialize (gamma_st (Var Q n)); simpl in gamma_st.
rewrite <- beq_nat_refl in gamma_st.
simpl in defVars_wd.
specialize (defVars_wd n).
rewrite NatSet.singleton_spec in defVars_wd.
assert (n = n) by auto.
specialize (defVars_wd H).
destruct defVars_wd as [m defVars_wd].
rewrite defVars_wd.
specialize (gamma_st _ defVars_wd).
rewrite gamma_st.
apply mTypeEqBool_refl.
- simpl.
unfold Gamma_stronger in gamma_st.
specialize (gamma_st (Const m v)); simpl in gamma_st.
rewrite mTypeEqBool_refl, Qeq_bool_refl in gamma_st; simpl in gamma_st.
specialize (gamma_st m).
assert (Some m = Some m) by auto.
rewrite (gamma_st H).
rewrite mTypeEqBool_refl; auto.
- simpl.
simpl in defVars_wd.
specialize (IHe defVars_wd).
assert (Gamma_stronger (typeMap defVars e) Gamma).
{
eapply Gamma_stronger_trans; eauto.
intros e0 m0 typemap_e.
simpl.
case_eq (expEqBool (Unop u e) e0); intros; simpl in H; rewrite H.
+ admit.
+ auto. }
specialize (IHe H); rewrite IHe; simpl.
unfold Gamma_stronger in gamma_st.
specialize (gamma_st (Unop u e)); simpl in gamma_st.
rewrite unopEqBool_refl, expEqBool_refl in gamma_st; simpl in gamma_st.
unfold Gamma_stronger in H.
pose proof (stupidlemma _ _ _ IHe) as [m type_e].
rewrite type_e.
apply eqTypeExpression in type_e.
rewrite type_e.
case_eq (expEqBool (Unop u e) e); intros; simpl in H; rewrite H.
+ admit.
+ apply eqTypeExpression in type_e; rewrite type_e.
rewrite mTypeEqBool_refl; simpl.
\ No newline at end of file
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