Commit be477b4d by Nikita Zyuzin

### Remove terop abstraction and use Fma directly as an expression

parent 934d48f0
 ... ... @@ -91,33 +91,8 @@ Definition evalUnop (o:unop) (v:R):= |Inv => (/ v)%R end . (** Expressions will use ternary operators Define them first **) Inductive terop: Type := Fma. Definition teropEq (o1: terop) (o2: terop) := match o1, o2 with | Fma, Fma => true end. Lemma teropEq_refl t: teropEq t t = true. Proof. now destruct t. Qed. Lemma teropEq_compat_eq t1 t2: teropEq t1 t2 = true <-> t1 = t2. Proof. now destruct t1, t2. Qed. Definition evalTerop (o: terop) (v1: R) (v2: R) (v3: R) := match o with | Fma => Rplus v1 (Rmult v2 v3) end. Definition evalFma (v1:R) (v2:R) (v3:R):= Rplus v1 (Rmult v2 v3). (** Define expressions parametric over some value type V. ... ... @@ -128,7 +103,7 @@ Inductive exp (V:Type): Type := | Const: mType -> V -> exp V | Unop: unop -> exp V -> exp V | Binop: binop -> exp V -> exp V -> exp V | Terop: terop -> exp V -> exp V -> exp V -> exp V | Fma: exp V -> exp V -> exp V -> exp V | Downcast: mType -> exp V -> exp V. (** ... ... @@ -144,8 +119,8 @@ Fixpoint expEq (e1:exp Q) (e2:exp Q) := (unopEq o1 o2) && (expEq e11 e22) | Binop o1 e11 e12, Binop o2 e21 e22 => (binopEq o1 o2) && (expEq e11 e21) && (expEq e12 e22) | Terop o1 e11 e12 e13, Terop o2 e21 e22 e23 => (teropEq o1 o2) && (expEq e11 e21) && (expEq e12 e22) && (expEq e13 e23) | Fma e11 e12 e13, Fma e21 e22 e23 => (expEq e11 e21) && (expEq e12 e22) && (expEq e13 e23) | Downcast m1 f1, Downcast m2 f2 => (mTypeEq m1 m2) && (expEq f1 f2) | _, _ => false ... ... @@ -160,7 +135,7 @@ Proof. - apply Qeq_bool_iff; lra. - case u; auto. - case b; auto. - case t. firstorder. - firstorder. - apply mTypeEq_refl. Qed. ... ... @@ -182,10 +157,8 @@ Proof. * apply IHe1. + apply IHe2. - f_equal. + f_equal. * destruct t, t0. simpl. apply IHe1. * apply IHe2. + apply IHe3. + f_equal; auto. + auto. - f_equal. + apply mTypeEq_sym; auto. + apply IHe. ... ... @@ -219,8 +192,6 @@ Proof. split; [eapply IHe1; eauto | eapply IHe2; eauto]. - andb_to_prop eq1; andb_to_prop eq2. rewrite teropEq_compat_eq in *; subst. rewrite teropEq_refl; simpl. rewrite andb_true_iff. rewrite andb_true_iff. split; [split; [eapply IHe1; eauto | eapply IHe2; eauto] | eapply IHe3; eauto]. ... ... @@ -237,7 +208,7 @@ Fixpoint toRExp (e:exp Q) := | Const m n => Const m (Q2R n) | Unop o e1 => Unop o (toRExp e1) | Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2) | Terop o e1 e2 e3 => Terop o (toRExp e1) (toRExp e2) (toRExp e3) | Fma e1 e2 e3 => Fma (toRExp e1) (toRExp e2) (toRExp e3) | Downcast m e1 => Downcast m (toRExp e1) end. ... ... @@ -247,7 +218,7 @@ Fixpoint toREval (e:exp R) := | Const _ n => Const M0 n | Unop o e1 => Unop o (toREval e1) | Binop o e1 e2 => Binop o (toREval e1) (toREval e2) | Terop o e1 e2 e3 => Terop o (toREval e1) (toREval e2) (toREval e3) | Fma e1 e2 e3 => Fma (toREval e1) (toREval e2) (toREval e3) | Downcast _ e1 => Downcast M0 (toREval e1) end. ... ... @@ -301,13 +272,13 @@ Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType - eval_exp E Gamma f2 v2 m2 -> ((op = Div) -> (~ v2 = 0)%R) -> eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (join m1 m2) | Terop_dist m1 m2 m3 op f1 f2 f3 v1 v2 v3 delta: | Fma_dist m1 m2 m3 f1 f2 f3 v1 v2 v3 delta: Rle (Rabs delta) (Q2R (mTypeToQ (join3 m1 m2 m3))) -> eval_exp E Gamma f1 v1 m1 -> eval_exp E Gamma f2 v2 m2 -> eval_exp E Gamma f3 v3 m3 -> eval_exp E Gamma (Terop op f1 f2 f3) (perturb (evalTerop op v1 v2 v3) delta) eval_exp E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3). Hint Constructors eval_exp. ... ... @@ -377,19 +348,19 @@ Qed. Hint Resolve Binop_dist'. Lemma Terop_dist' m1 m2 m3 op f1 f2 f3 v1 v2 v3 delta v m' E Gamma: Lemma Fma_dist' m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma: Rle (Rabs delta) (Q2R (mTypeToQ m')) -> eval_exp E Gamma f1 v1 m1 -> eval_exp E Gamma f2 v2 m2 -> eval_exp E Gamma f3 v3 m3 -> v = perturb (evalTerop op v1 v2 v3) delta -> v = perturb (evalFma v1 v2 v3) delta -> m' = join3 m1 m2 m3 -> eval_exp E Gamma (Terop op f1 f2 f3) v m'. eval_exp E Gamma (Fma f1 f2 f3) v m'. Proof. intros; subst; auto. Qed. Hint Resolve Terop_dist'. Hint Resolve Fma_dist'. (** Define the set of "used" variables of an expression to be the set of variables ... ... @@ -400,7 +371,7 @@ Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t := | Var _ x => NatSet.singleton x | Unop u e1 => usedVars e1 | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2) | Terop t e1 e2 e3 => NatSet.union (usedVars e1) (NatSet.union (usedVars e2) (usedVars e3)) | Fma e1 e2 e3 => NatSet.union (usedVars e1) (NatSet.union (usedVars e2) (usedVars e3)) | Downcast _ e1 => usedVars e1 | _ => NatSet.empty end. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!