Commit 2a5c4420 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Revert "Start changing expression semantics"

This reverts commit 6ef96566.
parent 579e5d38
......@@ -32,66 +32,50 @@ 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 -> option R) -> (expr R) -> R -> mType -> Prop :=
| Var_load DeltaMap m x v:
:(expr R) -> R -> mType -> Prop :=
| Var_load m x v:
Gamma (Var R x) = Some m ->
E x = Some v ->
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') ->
eval_expr E Gamma (Var R x) v m
| Const_dist m n delta:
Rabs delta <= mTypeToR m ->
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:
eval_expr E Gamma (Const m n) (perturb n m delta) m
| Unop_neg m mN f1 v1:
Gamma (Unop Neg f1) = Some mN ->
isCompat m mN = true ->
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') ->
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:
Gamma (Unop Inv f1) = Some mN ->
isCompat m mN = true ->
Rabs delta <= mTypeToR mN ->
eval_expr E Gamma DeltaMap f1 v1 m ->
eval_expr E Gamma f1 v1 m ->
(~ v1 = 0)%R ->
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') ->
eval_expr E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) mN delta) mN
| Downcast_dist m m1 f1 v1 delta:
Gamma (Downcast m f1) = Some m ->
isMorePrecise m1 m = true ->
Rabs delta <= mTypeToR 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') ->
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:
Gamma (Binop op f1 f2) = Some m ->
isJoin m1 m2 m = true ->
Rabs delta <= mTypeToR m ->
eval_expr E Gamma DeltaMap f1 v1 m1 ->
eval_expr E Gamma DeltaMap f2 v2 m2 ->
eval_expr E Gamma f1 v1 m1 ->
eval_expr E Gamma f2 v2 m2 ->
((op = Div) -> (~ v2 = 0)%R) ->
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') ->
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:
Gamma (Fma f1 f2 f3) = Some m ->
isJoin3 m1 m2 m3 m = true ->
Rabs delta <= mTypeToR 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.
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.
Close Scope R_scope.
......@@ -100,13 +84,11 @@ Hint Constructors eval_expr.
(** *)
(* Show some simpler (more general) rule lemmata *)
(* **)
Lemma Const_dist' DeltaMap DeltaMap' m n delta v m' E Gamma:
(forall delta', DeltaMap' (Const m n) = Some delta' -> delta = delta') ->
Lemma Const_dist' m n delta v m' E Gamma:
Rle (Rabs delta) (mTypeToR m') ->
DeltaMap = nonDestrUpd DeltaMap' (Const m n) delta ->
v = perturb n m delta ->
m' = m ->
eval_expr E Gamma DeltaMap (Const m n) v m'.
eval_expr E Gamma (Const m n) v m'.
Proof.
intros; subst; auto.
Qed.
......@@ -421,4 +403,4 @@ Lemma Rmap_updVars_comm Gamma n m:
Proof.
unfold updDefVars, toRMap; simpl.
intros x; destruct (R_orderedExps.compare x n); auto.
Qed.
Qed.
\ 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