Minor change to expressions and commands

coq/Commands.v

@@ -47,11 +47,10 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
   result value
  **)
 Inductive bstep : cmd R -> env -> R -> mType -> Prop :=
-  let_b m m1 x e s E v res:
-    isMorePrecise m1 m = true ->
+  let_b m x e s E v res:
     eval_exp E e v m ->
     bstep s (updEnv x m v E) res m ->
-    bstep (Let m1 x e s) E res m
+    bstep (Let m x e s) E res m
  |ret_b m e E v:
     eval_exp E e v m ->
     bstep (Ret e) E v m.

coq/Expressions.v

@@ -11,6 +11,7 @@ Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Dais
 **)
 Inductive binop : Type := Plus | Sub | Mult | Div.
 
+(** TODO: simplify pattern matching **)
 Definition binopEqBool (b1:binop) (b2:binop) :=
   match b1 with
     Plus => match b2 with Plus => true |_ => false end
@@ -31,6 +32,12 @@ Definition evalBinop (o:binop) (v1:R) (v2:R) :=
   | Div => Rdiv v1 v2
   end.
 
+Lemma binopEqBool_refl b:
+  binopEqBool b b = true.
+Proof.
+  case b; auto.
+Qed.
+
 (**
    Expressions will use unary operators.
    Define them first
@@ -61,7 +68,7 @@ Definition evalUnop (o:unop) (v:R):=
 **)
 Inductive exp (V:Type): Type :=
   Var: mType -> nat -> exp V
-| Const: V -> exp V
+| Const: mType -> V -> exp V
 | Unop: unop -> exp V -> exp V
 | Binop: binop -> exp V -> exp V -> exp V
 | Downcast: mType -> exp V -> exp V.
@@ -77,9 +84,9 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
    |Var _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2)
    | _=> false
    end
-  |Const n1 =>
+  |Const m1 n1 =>
    match e2 with
-   |Const n2 => (Qeq_bool n1 n2)
+   |Const m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2)
    | _=> false
    end
   |Unop o1 e11 =>
@@ -99,11 +106,22 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
    end
   end.
 
+Lemma expEqBool_refl e:
+  expEqBool e e = true.
+Proof.
+  induction e; apply andb_true_iff; split; simpl in *; auto; try (apply EquivEqBoolEq; auto). 
+  - symmetry; apply beq_nat_refl.
+  - apply Qeq_bool_iff; lra.
+  - case u; auto.
+  - case b; auto.
+  - apply andb_true_iff; split.
+    apply IHe1. apply IHe2.
+Qed.
 
 Fixpoint toRExp (e:exp Q) :=
   match e with
   |Var _ m v => Var R m v
-  |Const n => Const (Q2R n)
+  |Const m n => Const m (Q2R n)
   |Unop o e1 => Unop o (toRExp e1)
   |Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
   |Downcast m e1 => Downcast m (toRExp e1)
@@ -112,7 +130,7 @@ Fixpoint toRExp (e:exp Q) :=
 Fixpoint toREval (e:exp R) :=
   match e with
   | Var _ _ v => Var R M0 v
-  | Const n => Const n
+  | Const _ n => Const M0 n
   | Unop o e1 => Unop o (toREval e1)
   | Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
   | Downcast _ e1 =>  (toREval e1)
@@ -140,14 +158,14 @@ using a perturbation of the real valued computation by (1 + delta), where
 |delta| <= machine epsilon.
 **)
 Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
-| Var_load m m1 x v:
-    isMorePrecise m m1 = true ->
+| Var_load m (*m1*) x v:
+    (* isMorePrecise m m1 = true ->*)
     (**mTypeEqBool m m1 = true ->*)
-    E x = Some (v, m1) ->
-    eval_exp E (Var R m1 x) v m
+    E x = Some (v, m) ->
+    eval_exp E (Var R m x) v m
 | Const_dist m n delta:
     Rle (Rabs delta) (Q2R (meps m)) ->
-    eval_exp E (Const n) (perturb n delta) m
+    eval_exp E (Const m n) (perturb n delta) m
 | Unop_neg m f1 v1:
     eval_exp E f1 v1 m ->
     eval_exp E (Unop Neg f1) (evalUnop Neg v1) m
@@ -162,7 +180,7 @@ Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
     eval_exp E f2 v2 m2 ->
     eval_exp E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) m
 | Downcast_dist m m1 f1 v1 delta:
-    (*    Qle_bool (meps m1) (meps m) = true ->*)
+    (* Downcast expression f1 (evaluating to machine type m1), to a machine type m, less precise than m1.*)
     isMorePrecise m1 m = true ->
     Rle (Rabs delta) (Q2R (meps m)) ->
     eval_exp E f1 v1 m1 ->
@@ -204,7 +222,7 @@ Proof.
   induction f; intros v1 v2 m1 m10_eq eval_v1 eval_v2.
   - inversion eval_v1; inversion eval_v2; subst; auto;
       try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
-    rewrite H4 in H10; inversion H10; subst; auto.
+    rewrite H7 in H3; inversion H3; subst; auto.
   - inversion eval_v1; inversion eval_v2; subst; auto;
       try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
   - inversion eval_v1; inversion eval_v2; subst; auto;