Commit 3fa5e0ce authored by ='s avatar =

A new version of typing, separating computations and props

parent 0816e06e
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals Coq.MSets.MSets.
Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs Daisy.Commands Daisy.ssaPrgs.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
Fixpoint typeExpression (V:Type) (e:exp V) : option mType :=
match e with
| Var _ m v => Some m
| Const m n => Some m
| Unop u e1 => typeExpression e1
| Binop b e1 e2 =>
let tm1 := typeExpression e1 in
let tm2 := typeExpression e2 in
match tm1, tm2 with
| Some m1, Some m2 => Some (computeJoin m1 m2)
| _, _=> None
end
| Downcast m e1 =>
let tm1 := typeExpression e1 in
match tm1 with
|Some m1 => if (isMorePrecise m1 m) then Some m else None
|_ => None
end
end.
Fixpoint typeMap (e:exp Q) (e': exp Q) : option mType :=
match e with
| Var _ m v => if expEqBool e e' then Some m else None
| Const m n => if expEqBool e e' then Some m else None
| Unop u e1 => if expEqBool e e' then typeExpression e else typeMap e1 e'
| Binop b e1 e2 => if expEqBool e e' then typeExpression e
else
match (typeMap e1 e') with
| None => typeMap e2 e'
| x => x
end
| Downcast m e1 => if expEqBool e e' then Some m else typeMap e1 e'
end.
Lemma typeGivesTypeMap e m :
typeExpression e = Some m ->
typeMap e e = Some m.
Proof.
intros; induction e; simpl in *; auto.
- admit.
- admit.
- admit.
- pose proof (expEqBool_refl (Binop b e1 e2)).
simpl in H0; rewrite H0.
auto.
- admit.
Admitted.
Inductive validType (Gamma:exp Q -> option mType) : exp Q -> mType -> Prop :=
|tVar m v: Gamma (Var Q m v) = Some m -> validType Gamma (Var Q m v) m
|tConst m n: Gamma (Const m n) = Some m -> validType Gamma (Const m n) m
|tUnop u e1 m: validType Gamma e1 m ->
Gamma (Unop u e1) = Some m ->
validType Gamma (Unop u e1) m
|tBinop b e1 e2 m m1 m2:
validType Gamma e1 m1 ->
validType Gamma e2 m2 ->
m = computeJoin m1 m2 ->
Gamma (Binop b e1 e2) = Some m ->
validType Gamma (Binop b e1 e2) m
|tDowncast m e1 m1:
validType Gamma e1 m1 ->
isMorePrecise m1 m = true ->
Gamma (Downcast m e1) = Some m ->
validType Gamma (Downcast m e1) m.
Lemma Gamma_strengthening e m Gamma1 Gamma2:
(forall e m, Gamma1 e = Some m -> Gamma2 e = Some m ) ->
validType Gamma1 e m ->
validType Gamma2 e m.
Proof.
revert Gamma1 Gamma2 m; induction e;
intros;
inversion H0; subst;
econstructor; eauto.
Qed.
Lemma typeExpressionSoundness e m:
typeExpression e = Some m ->
validType (typeMap e) e m.
Proof.
revert m; induction e; intros; auto.
- simpl in *.
inversion H; subst; econstructor; eauto.
admit.
- simpl in *.
inversion H; subst; econstructor; eauto.
admit.
- constructor.
+ simpl in H. specialize (IHe m H); clear H.
induction e.
* inversion IHe; econstructor; subst.
simpl. admit.
* inversion IHe; subst.
econstructor.
simpl.
admit.
* inversion IHe; subst.
eapply Gamma_strengthening.
Focus 2.
apply IHe.
intros e0 m0 typeMap_Unop_e0.
unfold typeMap.
case_eq (expEqBool (Unop u (Unop u0 e)) e0); intros eq_case.
{ assert (typeExpression e0 = Some m0).
-
simpl.
induction e; auto.
simpl in H.
case_eq (unopEqBool u0 u1 && expEqBool e e0); intros case_unop; rewrite case_unop in *; try auto.
Focus 2.
rewrite <- IHe1.
destruct e0; simpl; auto.
+ apply typeGivesTypeMap; auto.
simpl in *.
s
(**
......@@ -16,34 +179,6 @@ Definition updTEnv (e:exp Q) (t:mType) (cont:exp Q-> option mType) :=
Definition emptyTEnv :exp Q -> option mType := fun e => None.
Fixpoint typeExpression_trec e (cont:exp Q -> option mType) : exp Q -> option mType :=
match e with
| Var _ m v => updTEnv e m cont
| Const m n => updTEnv e m cont
| Unop u e1 =>
let tEnv := typeExpression_trec e1 cont in
let t := tEnv e1 in
match t with
| Some m => updTEnv e m tEnv
| None => emptyTEnv
end
| Binop b e1 e2 =>
let tEnv_e1 := typeExpression_trec e1 cont in
let tEnv_e2 := typeExpression_trec e2 tEnv_e1 in (* TODO: This may cause trouble e.g. in (x:F) + (x:D) *)
let (t_e1,t_e2) := (tEnv_e2 e1, tEnv_e2 e2) in
match t_e1, t_e2 with
|Some m, Some m' => updTEnv e (computeJoin m m') tEnv_e2
| _, _ => emptyTEnv
end
| Downcast m e1 =>
let tEnv_e1 := typeExpression_trec e1 cont in
let t := tEnv_e1 e1 in
match t with
|Some m1 => if (isMorePrecise m1 m) then updTEnv e m tEnv_e1
else emptyTEnv
|_ => emptyTEnv
end
end.
Definition typeExpression e := typeExpression_trec e emptyTEnv.
......
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