Change with_lock

It now produces a lambda that when evaluated with a value runs the underlying
lambda that value after acquiring the lock. As before, the lock is released
afterwards.

F_mu_ref_par/examples/counter.v

@@ -62,17 +62,17 @@ Section CG_Counter.
   Global Opaque CG_increment.
 
   Definition CG_locked_increment (x l : expr) :=
-    Lam (with_lock (CG_increment x.[ren (+2)]) l.[ren (+2)]).
+    with_lock (CG_increment x) l.
   Definition CG_locked_incrementV (x l : expr) : val :=
-    LamV (with_lock (CG_increment x.[ren (+2)]) l.[ren (+2)]).
+    with_lockV (CG_increment x) l.
 
   Lemma CG_locked_increment_to_val x l :
     to_val (CG_locked_increment x l) = Some (CG_locked_incrementV x l).
-  Proof. trivial. Qed.
+  Proof. by rewrite with_lock_to_val. Qed.
 
   Lemma CG_locked_increment_of_val x l :
     of_val (CG_locked_incrementV x l) = CG_locked_increment x l.
-  Proof. trivial. Qed.
+  Proof. by rewrite with_lock_of_val. Qed.
 
   Global Opaque CG_locked_incrementV.
 
@@ -82,16 +82,14 @@ Section CG_Counter.
     typed Γ (CG_locked_increment x l) (TArrow TUnit TUnit).
   Proof.
     intros H1 H2. repeat econstructor.
-    eapply with_lock_type.
-    - apply CG_increment_type. by eapply (context_weakening [_; _]).
-    - by eapply (context_weakening [_; _]).
+    eapply with_lock_type; auto using CG_increment_type.
   Qed.
 
   Lemma CG_locked_increment_closed (x l : expr) :
     (∀ f, x.[f] = x) → (∀ f, l.[f] = l) →
     ∀ f, (CG_locked_increment x l).[f] = CG_locked_increment x l.
   Proof.
-    intros H1 H2 f. asimpl. unfold CG_locked_increment. rewrite H1 H2.
+    intros H1 H2 f. asimpl. unfold CG_locked_increment.
     rewrite with_lock_closed; trivial. apply CG_increment_closed; trivial.
   Qed.
 
@@ -109,11 +107,9 @@ Section CG_Counter.
                                 (CG_locked_increment (Loc x) (Loc l)) Unit)))%I)
       ⊢ |={E}=>(j ⤇ (fill K (Unit)) ★ x ↦ₛ (♯v S n) ★ l ↦ₛ (♭v false))%I.
   Proof.
-    intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_increment.
-    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial. rewrite with_lock_closed; auto. asimpl.
+    intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]".
     iPvs (steps_with_lock
-            _ _ _ j K _ _ _ _ UnitV _ _ with "[Hj Hx Hl]") as "Hj"; eauto.
+            _ _ _ j K _ _ _ _ UnitV UnitV _ _ with "[Hj Hx Hl]") as "Hj"; eauto.
     - intros K'.
       iIntros "[#Hspec [Hx Hj]]".
       iApply steps_CG_increment; eauto. iFrame "Hspec Hj Hx"; trivial.

F_mu_ref_par/examples/lock.v

@@ -8,15 +8,38 @@ Definition acquire : expr :=
 Definition release : expr := Lam (Store (Var 1) (♭ false)).
 
 Definition with_lock (e : expr) (l : expr) : expr :=
-  App
-    (Lam
-       (App (Lam (App (Lam (App (Lam (Var 3)) (App release (Var 5))))
-                           (App e.[ren (+4)] Unit)))
-            (App acquire (Var 1))
+  Lam
+    (App
+       (Lam
+          (App (Lam (App (Lam (App (Lam (Var 3)) (App release (Var 5))))
+                         (App e.[ren (+6)] (Var 5))))
+               (App acquire (Var 1))
+          )
        )
-    )
-    l
-.
+       l.[ren (+2)]
+    ).
+
+Definition with_lockV (e l : expr) : val :=
+  LamV
+    (App
+       (Lam
+          (App (Lam (App (Lam (App (Lam (Var 3)) (App release (Var 5))))
+                         (App e.[ren (+6)] (Var 5))))
+               (App acquire (Var 1))
+          )
+       )
+       l.[ren (+2)]
+    ).
+
+Lemma with_lock_to_val e l :
+  to_val (with_lock e l) = Some (with_lockV e l).
+Proof. trivial. Qed.
+
+Lemma with_lock_of_val e l :
+  of_val (with_lockV e l) = with_lock e l.
+Proof. trivial. Qed.
+
+Global Opaque with_lockV.
 
 Lemma newlock_closed f : newlock.[f] = newlock.
 Proof. by asimpl. Qed.
@@ -48,14 +71,15 @@ Proof. do 3 econstructor; eauto using EqTBool; repeat constructor. Qed.
 Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
 Proof. repeat econstructor. Qed.
 
-Lemma with_lock_type e l Γ τ :
-  typed Γ e (TArrow TUnit τ) →
+Lemma with_lock_type e l Γ τ τ' :
+  typed Γ e (TArrow τ τ') →
   typed Γ l LockType →
-  typed Γ (with_lock e l) τ.
+  typed Γ (with_lock e l) (TArrow τ τ').
 Proof.
-  intros H1 H2. econstructor; eauto.
-  repeat (econstructor; eauto using release_type, acquire_type).
-  eapply (context_weakening [_; _; _; _]); eauto.
+  intros H1 H2. do 2 econstructor; eauto.
+  - repeat (econstructor; eauto using release_type, acquire_type).
+    eapply (context_weakening [_; _; _; _; _; _]); eauto.
+  - eapply (context_weakening [_; _]); eauto.
 Qed.
 
 Section proof.
@@ -115,30 +139,33 @@ Section proof.
 
   Global Opaque release.
 
-  Lemma steps_with_lock N E ρ j K e l P Q v :
+  Lemma steps_with_lock N E ρ j K e l P Q v w:
     nclose N ⊆ E →
     (∀ f, e.[f] = e) (* e is a closed term *)
     →
-    (∀ K', ((Spec_ctx N ρ ★ P ★ j ⤇ (fill K' (App e Unit)))%I)
+    (∀ K', ((Spec_ctx N ρ ★ P ★ j ⤇ (fill K' (App e (# w))))%I)
             ⊢ |={E}=>(j ⤇ (fill K' (# v)) ★ Q)%I)
     →
     (((Spec_ctx N ρ ★ P ★ l ↦ₛ (♭v false)
-                ★ j ⤇ (fill K (with_lock e (Loc l))))%I)
+                ★ j ⤇ (fill K (App (with_lock e (Loc l)) (# w))))%I)
       ⊢ |={E}=>(j ⤇ (fill K (# v)) ★ Q ★ l ↦ₛ (♭v false))%I).
   Proof.
     intros HNE H1 H2.
     iIntros "[#Hspec [HP [Hl Hj]]]".
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
     iFrame "Hspec Hj"; trivial. simpl.
-    rewrite acquire_closed release_closed H1. asimpl.
+    rewrite ?acquire_closed ?release_closed ?H1. asimpl.
+    iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
+    iFrame "Hspec Hj"; trivial. simpl.
+    rewrite ?acquire_closed ?release_closed ?H1. asimpl.
     iPvs (steps_acquire _ _ _ j (K ++ [AppRCtx (LamV _)])
                    _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
     rewrite fill_app; simpl.
     iFrame "Hspec Hj"; trivial.
     rewrite fill_app; simpl.
     iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
-    iFrame "Hspec Hj"; trivial.
-    rewrite H1. asimpl. rewrite release_closed H1.
+    iFrame "Hspec Hj"; trivial. simpl.
+    rewrite ?release_closed ?H1. asimpl.
     iPvs (H2 (K ++ [AppRCtx (LamV _)]) with "[Hj HP]") as "[Hj HQ]"; eauto.
     rewrite ?fill_app. simpl.
     iFrame "Hspec Hj"; trivial.