Commit df39f778 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Add initial types for FMA

parent d05a7b09
...@@ -91,6 +91,40 @@ Definition evalUnop (o:unop) (v:R):= ...@@ -91,6 +91,40 @@ Definition evalUnop (o:unop) (v:R):=
|Inv => (/ v)%R |Inv => (/ v)%R
end . 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 b:
teropEq b b = true.
Proof.
now destruct b.
Qed.
Lemma teropEq_compat_eq b1 b2:
teropEq b1 b2 = true <-> b1 = b2.
Proof.
now destruct b1, b2.
Qed.
Lemma teropEq_compat_eq_false b1 b2:
teropEq b1 b2 = false <-> ~ (b1 = b2).
Proof.
now destruct b1, b2.
Qed.
Definition evalTerop (o: terop) (v1: R) (v2: R) (v3: R) :=
match o with
| Fma => Rplus v1 (Rmult v2 v3)
end.
(** (**
Define expressions parametric over some value type V. Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later. Will ease reasoning about different instantiations later.
...@@ -100,6 +134,7 @@ Inductive exp (V:Type): Type := ...@@ -100,6 +134,7 @@ Inductive exp (V:Type): Type :=
| Const: mType -> V -> exp V | Const: mType -> V -> exp V
| Unop: unop -> exp V -> exp V | Unop: unop -> exp V -> exp V
| Binop: binop -> exp V -> exp V -> exp V | Binop: binop -> exp V -> exp V -> exp V
| Terop: terop -> exp V -> exp V -> exp V -> exp V
| Downcast: mType -> exp V -> exp V. | Downcast: mType -> exp V -> exp V.
(** (**
...@@ -115,6 +150,8 @@ Fixpoint expEq (e1:exp Q) (e2:exp Q) := ...@@ -115,6 +150,8 @@ Fixpoint expEq (e1:exp Q) (e2:exp Q) :=
(unopEq o1 o2) && (expEq e11 e22) (unopEq o1 o2) && (expEq e11 e22)
| Binop o1 e11 e12, Binop o2 e21 e22 => | Binop o1 e11 e12, Binop o2 e21 e22 =>
(binopEq o1 o2) && (expEq e11 e21) && (expEq e12 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)
| Downcast m1 f1, Downcast m2 f2 => | Downcast m1 f1, Downcast m2 f2 =>
(mTypeEq m1 m2) && (expEq f1 f2) (mTypeEq m1 m2) && (expEq f1 f2)
| _, _ => false | _, _ => false
...@@ -129,6 +166,7 @@ Proof. ...@@ -129,6 +166,7 @@ Proof.
- apply Qeq_bool_iff; lra. - apply Qeq_bool_iff; lra.
- case u; auto. - case u; auto.
- case b; auto. - case b; auto.
- case t. firstorder.
- apply mTypeEq_refl. - apply mTypeEq_refl.
Qed. Qed.
...@@ -149,6 +187,11 @@ Proof. ...@@ -149,6 +187,11 @@ Proof.
* destruct b; auto. * destruct b; auto.
* apply IHe1. * apply IHe1.
+ apply IHe2. + apply IHe2.
- f_equal.
+ f_equal.
* destruct t, t0. simpl. apply IHe1.
* apply IHe2.
+ apply IHe3.
- f_equal. - f_equal.
+ apply mTypeEq_sym; auto. + apply mTypeEq_sym; auto.
+ apply IHe. + apply IHe.
...@@ -180,6 +223,13 @@ Proof. ...@@ -180,6 +223,13 @@ Proof.
rewrite binopEq_refl; simpl. rewrite binopEq_refl; simpl.
apply andb_true_iff. apply andb_true_iff.
split; [eapply IHe1; eauto | eapply IHe2; eauto]. 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.
firstorder.
- andb_to_prop eq1; - andb_to_prop eq1;
andb_to_prop eq2. andb_to_prop eq2.
rewrite mTypeEq_compat_eq in *; subst. rewrite mTypeEq_compat_eq in *; subst.
...@@ -189,11 +239,12 @@ Qed. ...@@ -189,11 +239,12 @@ Qed.
Fixpoint toRExp (e:exp Q) := Fixpoint toRExp (e:exp Q) :=
match e with match e with
|Var _ v => Var R v | Var _ v => Var R v
|Const m n => Const m (Q2R n) | Const m n => Const m (Q2R n)
|Unop o e1 => Unop o (toRExp e1) | Unop o e1 => Unop o (toRExp e1)
|Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2) | Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
|Downcast m e1 => Downcast m (toRExp e1) | Terop o e1 e2 e3 => Terop o (toRExp e1) (toRExp e2) (toRExp e3)
| Downcast m e1 => Downcast m (toRExp e1)
end. end.
Fixpoint toREval (e:exp R) := Fixpoint toREval (e:exp R) :=
...@@ -202,6 +253,7 @@ Fixpoint toREval (e:exp R) := ...@@ -202,6 +253,7 @@ Fixpoint toREval (e:exp R) :=
| Const _ n => Const M0 n | Const _ n => Const M0 n
| Unop o e1 => Unop o (toREval e1) | Unop o e1 => Unop o (toREval e1)
| Binop o e1 e2 => Binop o (toREval e1) (toREval e2) | Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
| Terop o e1 e2 e3 => Terop o (toREval e1) (toREval e2) (toREval e3)
| Downcast _ e1 => Downcast M0 (toREval e1) | Downcast _ e1 => Downcast M0 (toREval e1)
end. end.
...@@ -493,4 +545,4 @@ Qed. *) ...@@ -493,4 +545,4 @@ Qed. *)
(* Simplify arithmetic later by making > >= only abbreviations *) (* Simplify arithmetic later by making > >= only abbreviations *)
(* **) *) (* **) *)
(* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *) (* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *)
(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *) (* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *)
\ 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