Start changing expression semantics

coq/ExpressionSemantics.v

@@ -32,50 +32,66 @@ using a perturbation of the real valued computation by (1 + delta), where
 **)
 Open Scope R_scope.
 
+Definition nonDestrUpd (T: Type) M k (v: T) :=
+  match (M k) with
+  | Some v1 => M
+  | None => (fun x => if R_orderedExps.eq_dec x k then Some v else M x)
+  end.
+
 Inductive eval_expr (E:env)
           (Gamma: expr R -> option mType)
-  :(expr R) -> R -> mType -> Prop :=
-| Var_load m x v:
+  :(expr R -> option R) -> (expr R) -> R -> mType -> Prop :=
+| Var_load DeltaMap m x v:
     Gamma (Var R x) = Some m ->
     E x = Some v ->
-    eval_expr E Gamma (Var R x) v m
-| Const_dist m n delta:
+    eval_expr E Gamma DeltaMap (Var R x) v m
+| Const_dist DeltaMap m n delta:
+    (forall delta', DeltaMap (Const m n) = Some delta' -> delta = delta') ->
     Rabs delta <= mTypeToR m ->
-    eval_expr E Gamma (Const m n) (perturb n m delta) m
-| Unop_neg m mN f1 v1:
+    eval_expr E Gamma (nonDestrUpd DeltaMap (Const m n) delta) (Const m n) (perturb n m delta) m
+    (* eval_expr E Gamma DeltaMap (Const m n) (perturb n m delta) m *)
+| Unop_neg DeltaMap m mN f1 v1:
     Gamma (Unop Neg f1) = Some mN ->
     isCompat m mN = true ->
-    eval_expr E Gamma f1 v1 m ->
-    eval_expr E Gamma (Unop Neg f1) (evalUnop Neg v1) mN
-| Unop_inv m mN f1 v1 delta:
+    eval_expr E Gamma DeltaMap f1 v1 m ->
+    eval_expr E Gamma DeltaMap (Unop Neg f1) (evalUnop Neg v1) mN
+| Unop_inv DeltaMap m mN f1 v1 delta:
+    (forall delta', DeltaMap (Unop Inv f1) = Some delta' -> delta = delta') ->
     Gamma (Unop Inv f1) = Some mN ->
     isCompat m mN = true ->
     Rabs delta <= mTypeToR mN ->
-    eval_expr E Gamma f1 v1 m ->
+    eval_expr E Gamma DeltaMap f1 v1 m ->
     (~ v1 = 0)%R  ->
-    eval_expr E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) mN delta) mN
-| Downcast_dist m m1 f1 v1 delta:
+    eval_expr E Gamma (nonDestrUpd DeltaMap (Unop Inv f1) delta)
+              (Unop Inv f1) (perturb (evalUnop Inv v1) mN delta) mN
+| Downcast_dist DeltaMap m m1 f1 v1 delta:
+    (forall delta', DeltaMap (Downcast m f1) = Some delta' -> delta = delta') ->
     Gamma (Downcast m f1) = Some m ->
     isMorePrecise m1 m = true ->
     Rabs delta <= mTypeToR m ->
-    eval_expr E Gamma f1 v1 m1 ->
-    eval_expr E Gamma (Downcast m f1) (perturb v1 m delta) m
-| Binop_dist m1 m2 op f1 f2 v1 v2 delta m:
+    eval_expr E Gamma DeltaMap f1 v1 m1 ->
+    eval_expr E Gamma (nonDestrUpd DeltaMap  (Downcast m f1) delta)
+              (Downcast m f1) (perturb v1 m delta) m
+| Binop_dist DeltaMap m1 m2 op f1 f2 v1 v2 delta m:
+    (forall delta', DeltaMap (Binop op f1 f2) = Some delta' -> delta = delta') ->
     Gamma (Binop op f1 f2) = Some m ->
     isJoin m1 m2 m = true ->
     Rabs delta <= mTypeToR m ->
-    eval_expr E Gamma f1 v1 m1 ->
-    eval_expr E Gamma f2 v2 m2 ->
+    eval_expr E Gamma DeltaMap f1 v1 m1 ->
+    eval_expr E Gamma DeltaMap f2 v2 m2 ->
     ((op = Div) -> (~ v2 = 0)%R) ->
-    eval_expr E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) m delta) m
-| Fma_dist m1 m2 m3 m f1 f2 f3 v1 v2 v3 delta:
+    eval_expr E Gamma (nonDestrUpd DeltaMap (Binop op f1 f2) delta)
+              (Binop op f1 f2) (perturb (evalBinop op v1 v2) m delta) m
+| Fma_dist DeltaMap m1 m2 m3 m f1 f2 f3 v1 v2 v3 delta:
+    (forall delta', DeltaMap (Fma f1 f2 f3) = Some delta' -> delta = delta') ->
     Gamma (Fma f1 f2 f3) = Some m ->
     isJoin3 m1 m2 m3 m = true ->
     Rabs delta <= mTypeToR m ->
-    eval_expr E Gamma f1 v1 m1 ->
-    eval_expr E Gamma f2 v2 m2 ->
-    eval_expr E Gamma f3 v3 m3 ->
-    eval_expr E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m.
+    eval_expr E Gamma DeltaMap f1 v1 m1 ->
+    eval_expr E Gamma DeltaMap f2 v2 m2 ->
+    eval_expr E Gamma DeltaMap f3 v3 m3 ->
+    eval_expr E Gamma (nonDestrUpd DeltaMap (Fma f1 f2 f3) delta)
+              (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m.
 
 Close Scope R_scope.
 
@@ -84,11 +100,13 @@ Hint Constructors eval_expr.
 (** *)
 (*   Show some simpler (more general) rule lemmata *)
 (* **)
-Lemma Const_dist' m n delta v m' E Gamma:
+Lemma Const_dist' DeltaMap DeltaMap' m n delta v m' E Gamma:
+  (forall delta', DeltaMap' (Const m n) = Some delta' -> delta = delta') ->
   Rle (Rabs delta) (mTypeToR m') ->
+  DeltaMap = nonDestrUpd DeltaMap' (Const m n) delta ->
   v = perturb n m delta ->
   m' = m ->
-  eval_expr E Gamma (Const m n) v m'.
+  eval_expr E Gamma DeltaMap (Const m n) v m'.
 Proof.
   intros; subst; auto.
 Qed.