Commit 5f393110 authored by Ralf Jung's avatar Ralf Jung

make some nested function calls in heap_lang/ more readable

parent 41a4028c
......@@ -165,11 +165,11 @@ Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
match op, l1, l2 with
| PlusOp, LitNat n1, LitNat n2 => Some (LitNat (n1 + n2))
| MinusOp, LitNat n1, LitNat n2 => Some (LitNat (n1 - n2))
| LeOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 n2)))
| LtOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 < n2)))
| EqOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 = n2)))
| PlusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 + n2)
| MinusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 - n2)
| LeOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 n2)
| LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 < n2)
| EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 = n2)
| _, _, _ => None
end.
......
......@@ -130,7 +130,7 @@ Qed.
Lemma wp_fst E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2
Q v1 wp E (Fst (Pair e1 e2)) Q.
Q v1 wp E (Fst $ Pair e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
last by intros; inv_step; eauto.
......@@ -139,7 +139,7 @@ Qed.
Lemma wp_snd E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2
Q v2 wp E (Snd (Pair e1 e2)) Q.
Q v2 wp E (Snd $ Pair e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
last by intros; inv_step; eauto.
......
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