From bb8c2f552ea70868a388afdc7d3f828eb3e2cd7b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 7 Sep 2016 00:26:51 +0200
Subject: [PATCH] Use bool instead of int in barrier implementation.

---
 heap_lang/lib/barrier/barrier.v | 6 +++---
 heap_lang/lib/barrier/proof.v   | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/heap_lang/lib/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
index b9ebaf60b..f30edf8dd 100644
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export notation.
 
-Definition newbarrier : val := λ: <>, ref #0.
-Definition signal : val := λ: "x", "x" <- #1.
+Definition newbarrier : val := λ: <>, ref #false.
+Definition signal : val := λ: "x", "x" <- #true.
 Definition wait : val :=
-  rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
+  rec: "wait" "x" := if: !"x" then #() else "wait" "x".
 Global Opaque newbarrier signal wait.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index b427bb5b3..9be41c4de 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -28,7 +28,7 @@ Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
     ▷ (P -★ [★ set] i ∈ I, Ψ i) ★ [★ set] i ∈ I, saved_prop_own i (Ψ i))%I.
 
 Coercion state_to_val (s : state) : val :=
-  match s with State Low _ => #0 | State High _ => #1 end.
+  match s with State Low _ => #false | State High _ => #true end.
 Arguments state_to_val !_ / : simpl nomatch.
 
 Definition state_to_prop (s : state) (P : iProp Σ) : iProp Σ :=
@@ -145,7 +145,7 @@ Proof.
     { iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
     iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "==>[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
-    iVsIntro. wp_op=> ?; simplify_eq; wp_if.
+    iVsIntro. wp_if.
     iApply ("IH" with "Hγ [HQR] HΦ"). auto.
   - (* a High state: the comparison succeeds, and we perform a transition and
     return to the client *)
@@ -157,7 +157,7 @@ Proof.
     { iSplit; [iPureIntro; by eauto using wait_step|].
       iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
     iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
-    iVsIntro. wp_op=> ?; simplify_eq/=; wp_if.
+    iVsIntro. wp_if.
     iVsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
 Qed.
 
-- 
GitLab