Fix the rest of the code wrt the AWP definition change

theories/c_translation/lifting.v

@@ -31,23 +31,6 @@ Section lifting.
 
   Qed.
 
-  Lemma awp_ctx_bind (v1 v2 : val) (e1 e2 : expr) R Φ :
-    IntoVal e1 v1 →
-    IntoVal e2 v2 →
-    awp e2 R (fun w => awp (e1 w) R Φ) -∗
-    awp (a_bind e1 e2) R Φ.
-  Proof.
-    intros <-%of_to_val <-%of_to_val.
-    iIntros "HAWP". rewrite /awp.
-    iIntros (γ π env l) "#Hflock Hunfl".
-    rewrite /a_bind. wp_rec. wp_rec. wp_rec. wp_rec.
-    wp_bind (v2 env l).
-    iApply (wp_wand with "[HAWP Hunfl]").
-    { by iApply "HAWP". }
-    iIntros (w) "[H Hunfl]".
-    wp_rec. by iApply "H".
-  Qed.
-
 End lifting.
 
 Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).

theories/c_translation/monad.v

@@ -114,7 +114,7 @@ Section a_wp_rules.
     IntoVal e ev →
     (∀ env, env_inv env -∗ R -∗
       WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗
-    awp (a_atomic_env ev) R Φ.
+    awp (a_atomic_env e) R Φ.
   Proof.
     iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env. wp_lam.
     iIntros (γ π env l) "#Hlock Hunfl". do 2 wp_lam.
@@ -127,13 +127,13 @@ Section a_wp_rules.
     iIntros "Hunfl". wp_seq. iFrame.
   Qed.
 
-  Lemma awp_par e1 e2 (ev1 ev2 : val) R (Ψ1 Ψ2 Φ : val → iProp Σ) :
+  Lemma awp_par (Ψ1 Ψ2 : val → iProp Σ) e1 e2 (ev1 ev2 : val) R (Φ : val → iProp Σ) :
     IntoVal e1 ev1 →
     IntoVal e2 ev2 →
     awp ev1 R Ψ1 -∗
     awp ev2 R Ψ2 -∗
     ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗
-    awp (a_par ev1 ev2) R Φ.
+    awp (a_par e1 e2) R Φ.
   Proof.
     iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ".
     rewrite /awp /a_par. do 2 wp_lam.

theories/c_translation/translation.v

@@ -35,8 +35,8 @@ Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
 
 (* M () *)
 (* The eta expansion is used to turn it into a value *)
-Definition a_seq : val := λ: "env",
-  a_atomic_env (λ: "env", mset_clear "env") "env".
+Definition a_seq : val := λ: <>,
+  a_atomic_env (λ: "env", mset_clear "env").
 
 Definition a_sequence : val := λ: "e1" "e2",
   a_bind (λ: <>, a_bind (λ: <>, "e2") a_seq) "e1".
@@ -58,11 +58,9 @@ Section proofs.
 
   Lemma a_seq_spec R `{Timeless _ R} Φ :
     U (Φ #()) -∗
-    awp a_seq R Φ.
+    awp (a_seq #()) R Φ.
   Proof.
-    iIntros "HΦ". rewrite /a_seq.
-    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
-    wp_rec. iRevert "Hflock Hunfl". iRevert (γ π env lk).
+    iIntros "HΦ". rewrite /a_seq. awp_lam.
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
     iApply wp_fupd.
@@ -157,17 +155,13 @@ Section proofs.
     awp (a_store (a_ret #l) (a_ret w)) R Φ.
   Proof.
     unfold a_store. iIntros "Hv HΦ".
-    rewrite /a_ret.
-    repeat (awp_pure _).
-    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
-    Opaque par. repeat (wp_pure _).
-    wp_bind (_ ||| _)%E.
-    iApply (wp_par (fun v => ⌜v = #l⌝) (fun v => ⌜v = w⌝))%I.
-    { repeat wp_pure _. eauto. }
-    { repeat wp_pure _. eauto. }
-    iIntros (? ?) "[% %]"; simplify_eq/=. iNext.
-    wp_let. wp_let.
-    iRevert "Hflock Hunfl". iRevert (γ π env lk).
+    rewrite /a_ret. do 4 awp_lam.
+    iApply awp_bind.
+    iApply (awp_par (fun v => ⌜v = #l⌝) (fun v => ⌜v = w⌝))%I.
+    { by iApply awp_value. }
+    { by iApply awp_value. }
+    iNext. iIntros (? ?) "% %"; simplify_eq/=. iNext.
+    awp_let.
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
     rewrite {2}/env_inv.
@@ -209,22 +203,20 @@ Section proofs.
      awp e1 R Φ -∗ awp (a_if (a_ret #true) e1 e2) R Φ.
   Proof.
     unfold a_if. iIntros "HΦ".
-    rewrite /a_ret.
-    repeat awp_pure _.
-    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
-    repeat (wp_pure _).
-    by iApply ("HΦ" with "Hflock Hunfl").
+    awp_lam. awp_lam. awp_lam. awp_lam.
+    iApply awp_bind.
+    iApply awp_value.
+    awp_lam. by awp_if_true.
   Qed.
 
   Lemma a_if_false_spec `{Timeless _ R} (e1 e2 : val) Φ :
      awp e2 R Φ -∗ awp (a_if (a_ret #false) e1 e2) R Φ.
   Proof.
     unfold a_if. iIntros "HΦ".
-    rewrite /a_ret.
-    repeat awp_pure _.
-    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
-    repeat (wp_pure _).
-    by iApply ("HΦ" with "Hflock Hunfl").
+    awp_lam. awp_lam. awp_lam. awp_lam.
+    iApply awp_bind.
+    iApply awp_value.
+    awp_lam. by awp_if_false.
   Qed.
 
 End proofs.

theories/tests/test1.v

@@ -10,10 +10,10 @@ Section test.
 
   Lemma test1 (l : loc) :
     l ↦L #1 -∗
-    awp (a_seq;;; a_load (a_ret #l))%E True (fun v => ⌜v = #1⌝).
+    awp (a_seq #();;; a_load (a_ret #l))%E True (fun v => ⌜v = #1⌝).
   Proof.
     iIntros "Hl".
-    iApply awp_ctx_bind.
+    iApply awp_bind.
     iApply a_seq_spec.
     rewrite U_unlock. iRevert "Hl". rewrite -(U_mono (l ↦U #1) (awp _ _ _))%I. eauto.
     iIntros "Hl". awp_pure _.