Commit 6350c89b authored by Heiko Becker's avatar Heiko Becker

Changing TypeMap Algorithm and Type to be finite maps

parent 2cb96884
......@@ -27,119 +27,106 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
(* Inductive approxParams :env -> env -> Prop := *)
(* |approxParamRefl: *)
(* approxParams emptyEnv emptyEnv *)
(* |approxParamUpd E1 E2 m x v1 v2 : *)
(* approxParams E1 E2 -> *)
(* (Rabs (v1 - v2) <= Q2R (meps m))%R -> *)
(* approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). *)
Section RelationProperties.
Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType) (A:analysisResult) (fVars dVars: NatSet.t).
Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType)
(A:analysisResult) (fVars dVars: NatSet.t).
Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2.
Lemma approxEnv_gives_value:
E1 x = Some v ->
NatSet.In x (NatSet.union fVars dVars) ->
exists v',
E2 x = Some v'.
Proof.
induction approxEnvs;
intros E1_def x_valid.
- unfold emptyEnv in E1_def; simpl in E1_def. congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; auto.
set_tac.
rewrite NatSet.union_spec in x_valid.
destruct x_valid; set_tac.
rewrite NatSet.add_spec in H1.
destruct H1; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; auto.
set_tac.
rewrite NatSet.union_spec in x_valid.
destruct x_valid; set_tac.
rewrite NatSet.add_spec in H2.
destruct H2; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
Qed.
Lemma approxEnv_gives_value:
E1 x = Some v ->
NatSet.In x (NatSet.union fVars dVars) ->
exists v',
E2 x = Some v'.
Proof.
induction approxEnvs;
intros E1_def x_valid.
- unfold emptyEnv in E1_def; simpl in E1_def. congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; eauto.
set_tac.
destruct x_valid; set_tac.
destruct H1 as [? | [? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+ eexists; eauto.
+ eapply IHa; auto.
set_tac.
destruct x_valid; set_tac.
destruct H2 as [? | [ ? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
Qed.
Arguments mTypeToQ _ : simpl nomatch.
Arguments mTypeToQ _ : simpl nomatch.
Lemma approxEnv_fVar_bounded v2 m:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x fVars ->
Gamma x = Some m ->
(Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_free x_typed.
- unfold emptyEnv in *; simpl in *; congruence.
- set_tac.
rewrite add_spec_strong in x_free.
destruct x_free as [x_x0 | [x_neq x_free]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
unfold updDefVars in x_typed.
rewrite Nat.eqb_refl in x_typed.
inversion x_typed; subst.
inversion E1_def; inversion E2_def; subst; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
Lemma approxEnv_fVar_bounded v2 m:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x fVars ->
Gamma x = Some m ->
(Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_free x_typed.
- unfold emptyEnv in *; simpl in *; congruence.
- set_tac.
destruct x_free as [x_x0 | [x_neq x_free]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
unfold updDefVars in x_typed.
rewrite Nat.eqb_refl in x_typed.
inversion x_typed; subst.
inversion E1_def; inversion E2_def; subst; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
apply IHa; auto.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H1.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
apply IHa; auto.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H1.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
apply IHa; auto.
unfold updDefVars in x_typed;
rewrite x_x0_neq in x_typed; auto.
Qed.
unfold updDefVars in x_typed;
rewrite x_x0_neq in x_typed; auto.
Qed.
Lemma approxEnv_dVar_bounded v2 m iv e:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
DaisyMap.find (Var Q x) A = Some (iv, e) ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_def x_typed A_e; subst.
- unfold emptyEnv in *; simpl in *; congruence.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H0; set_tac.
}
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
apply IHa; auto.
- set_tac.
rewrite add_spec_strong in x_def.
destruct x_def as [x_x0 | [x_neq x_def]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
inversion E1_def; inversion E2_def; subst.
rewrite A_e in *; inversion H; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
Lemma approxEnv_dVar_bounded v2 m iv e:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
DaisyMap.find (Var Q x) A = Some (iv, e) ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
induction approxEnvs;
intros E1_def E2_def x_def x_typed A_e; subst.
- unfold emptyEnv in *; simpl in *; congruence.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H0; set_tac.
}
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
apply IHa; auto.
Qed.
- set_tac.
destruct x_def as [x_x0 | [x_neq x_def]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
inversion E1_def; inversion E2_def; subst.
rewrite A_e in *; inversion H; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
unfold updDefVars in x_typed; rewrite x_neq in x_typed.
apply IHa; auto.
Qed.
End RelationProperties.
\ No newline at end of file
......@@ -82,6 +82,7 @@ Ltac set_hnf_tac :=
| [ H: NatSet.In ?x (NatSet.singleton ?y) |- _] => apply NatSetProps.Dec.F.singleton_1 in H
| [ H: NatSet.In ?x NatSet.empty |- _ ] => inversion H
| [ H: NatSet.In ?x (NatSet.union ?S1 ?S2) |- _ ] => rewrite NatSet.union_spec in H
| [ H: NatSet.In ?x (NatSet.add ?y ?S) |- _ ] => rewrite NatSet.add_spec_strong in H
| [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec
| [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec
| [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec
......
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 Daisy.Infra.RationalSimps.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
(**
Implementation of machine-precision as a datatype for mixed-precision computations
@author: Raphael Monat
@maintainer: Heiko Becker
**)
From Coq
Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals
MSets.MSets.
From Daisy
Require Import Infra.RationalSimps Infra.RealRationalProps Infra.Ltacs
Commands ssaPrgs.
From Daisy
Require Export Infra.ExpressionAbbrevs Infra.RealSimps Infra.NatSet
IntervalArithQ IntervalArith Infra.MachineType.
Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option mType :=
match e with
......@@ -38,44 +50,42 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (e': exp Q) : option mTyp
| 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) : exp Q -> option mType :=
match e with
| Var _ v => (fun e' => if expEq e e' then Gamma v else None)
| Const m n => (fun e' => if expEq e e' then Some m else None)
| Unop u e1 =>
let tMap := typeMap Gamma e1 in
(fun e' => if expEq e e' then tMap e1 else tMap e')
Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (tMap:DaisyMap.t mType)
: DaisyMap.t mType :=
if (DaisyMap.mem e tMap)
then tMap
else
match e with
| Var _ v => match Gamma v with
| Some m => DaisyMap.add e m tMap
| None => DaisyMap.empty mType
end
| Const m n => DaisyMap.add e m tMap
| Unop u e1 =>
let tMap_new := typeMap Gamma e1 tMap in
match DaisyMap.find e1 tMap_new with
| Some m_e1 => DaisyMap.add e m_e1 tMap
| None => DaisyMap.empty mType
end
| Binop b e1 e2 =>
let tMap1 := typeMap Gamma e1 in
let tMap2 := typeMap Gamma e2 in
let m1 := tMap1 e1 in
let m2 := tMap2 e2 in
(fun e' =>
if expEq e e'
then
match m1, m2 with
|Some t1, Some t2 => Some (join t1 t2)
|_ , _ => None
end
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)
let tMap1 := typeMap Gamma e1 tMap in
let tMap2 := typeMap Gamma e2 tMap1 in
let m1 := DaisyMap.find e1 tMap2 in
let m2 := DaisyMap.find e2 tMap2 in
match m1, m2 with
|Some t1, Some t2 => DaisyMap.add e (join t1 t2) tMap2
| _, _ => DaisyMap.empty mType
end
| Downcast m e1 =>
let tMap := typeMap Gamma e1 in
let m1 := tMap e1 in
(fun e' =>
if expEq e e'
then
match m1 with
|Some t1 =>
(if morePrecise t1 m then Some m else None)
| _ => None
end
else tMap e')
let tMap_new := typeMap Gamma e1 tMap in
let m1 := DaisyMap.find e1 tMap in
match m1 with
| Some t1 =>
if (morePrecise t1 m)
then DaisyMap.add e m tMap_new
else DaisyMap.empty mType
| None => DaisyMap.empty mType
end
end.
Fixpoint typeCmd (Gamma:nat -> option mType) (f:cmd Q): option mType :=
......@@ -88,66 +98,21 @@ Fixpoint typeCmd (Gamma:nat -> option mType) (f:cmd Q): option mType :=
|Ret e => typeExpression Gamma e
end.
Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) :=
Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) tMap :=
match f with
|Let m n e c =>
let tMap := typeMap Gamma e in
let tc := typeMapCmd Gamma c in
let tMap_new := typeMap Gamma e tMap in
let tc := typeMapCmd Gamma c tMap_new in
let mN := Gamma n in
(fun e' => if expEq e' (Var Q n)
then
match mN with
|Some m' => if morePrecise m m' then Some m else None
| None => None
end
else match (tMap e'), (tc 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
end)
|Ret e => typeMap Gamma e
match mN with
| Some m_n =>
if morePrecise m m_n
then DaisyMap.add (Var Q n) m tc
else DaisyMap.empty mType
| None => DaisyMap.empty mType
end
|Ret e => typeMap Gamma e tMap
end.
(* fun f' =>
if expEq f' (Var Q n) then
match Gamma n with
| Some m' => if isMorePrecise m m' then Some m else None
| None => None
end
else
let te := typeMap Gamma e in
let tc := typeMapCmd Gamma c in
match (te f'), (tc f') 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
|Ret e => (typeMap Gamma e)
end. *)
Definition ExpCst12 :exp Q := Const M64 ((1657)#(5)).
Definition ExpCst34 :exp Q := Const M64 ((3)#(5)).
Definition ExpVarT2 :exp Q := Var Q 2.
Definition MultExpCst34ExpVarT2 :exp Q := Binop Mult ExpCst34 ExpVarT2.
Definition PlusExpCst12MultExpCst34ExpVarT2 :exp Q := Binop Plus ExpCst12 MultExpCst34ExpVarT2.
Definition DowncastM32PlusExpCst12MultExpCst34ExpVarT2 :exp Q := Downcast M32 PlusExpCst12MultExpCst34ExpVarT2.
Definition ExpVart15 :exp Q := Var Q 5.
Definition UMinExpVart15 :exp Q := Unop Neg ExpVart15.
Definition ExpVarv1 :exp Q := Var Q 1.
Definition MultUMinExpVart15ExpVarv1 :exp Q := Binop Mult UMinExpVart15 ExpVarv1.
Definition ExpVaru0 :exp Q := Var Q 0.
Definition PlusExpVart15ExpVaru0 :exp Q := Binop Plus ExpVart15 ExpVaru0.
Definition MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0 :exp Q := Binop Mult PlusExpVart15ExpVaru0 PlusExpVart15ExpVaru0.
Definition DivMultUMinExpVart15ExpVarv1MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0 :exp Q := Binop Div MultUMinExpVart15ExpVarv1 MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0.
Definition RetDivMultUMinExpVart15ExpVarv1MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0 := Ret DivMultUMinExpVart15ExpVarv1MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0.
Definition LetExpVart15DowncastM32PlusExpCst12MultExpCst34ExpVarT2RetDivMultUMinExpVart15ExpVarv1MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0 := Let M32 5 DowncastM32PlusExpCst12MultExpCst34ExpVarT2 RetDivMultUMinExpVart15ExpVarv1MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0.
Definition defVars_doppler :(nat -> option mType) := fun n =>
if n =? 2 then Some M64 else if n =? 5 then Some M32 else if n =? 1 then Some M32 else if n =? 0 then Some M64 else None.
Time Eval compute in typeMapCmd defVars_doppler LetExpVart15DowncastM32PlusExpCst12MultExpCst34ExpVarT2RetDivMultUMinExpVart15ExpVarv1MultPlusExpVart15ExpVaru0PlusExpVart15ExpVaru0.
Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType) (tMap: exp Q -> option mType) : bool :=
match e with
......@@ -193,15 +158,6 @@ Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType) (tMap:exp Q -> optio
| Ret e => typeCheck e Gamma tMap
end.
(* Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType) (tMap:exp Q -> option mType) : bool := *)
(* match c with *)
(* | Let m x e g => match tMap (Var Q x), tMap e with *)
(* | Some mx, Some me => (mTypeEq mx m) && (isMorePrecise mx me) && typeCheck e Gamma tMap && typeCheckCmd g Gamma tMap *)
(* | _, _ => false *)
(* end *)
(* | Ret e => typeCheck e Gamma tMap *)
(* end. *)
(* Lemma eqTypeExpression e m Gamma: *)
(* typeMap Gamma e e = Some m <-> typeExpression Gamma e = Some m. *)
(* Proof. *)
......
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