Commit dabe846c authored by Robbert Krebbers's avatar Robbert Krebbers

Load should bind more strongly than app.

parent 448a8b62
Pipeline #200 passed with stage
......@@ -2,10 +2,13 @@ From barrier Require Import proof.
From program_logic Require Import auth sts saved_prop hoare ownership.
Import uPred.
Definition worker (n : Z) := (λ: "b" "y", wait "b" ;; (!"y") 'n)%L.
Definition client := (let: "y" := ref '0 in let: "b" := newbarrier '() in
Fork (Fork (worker 12 "b" "y") ;; worker 17 "b" "y") ;;
"y" <- (λ: "z", "z" + '42) ;; signal "b")%L.
Definition worker (n : Z) : val :=
λ: "b" "y", wait "b" ;; !"y" 'n.
Definition client : expr :=
let: "y" := ref '0 in
let: "b" := newbarrier '() in
Fork (Fork (worker 12 "b" "y") ;; worker 17 "b" "y") ;;
"y" <- (λ: "z", "z" + '42) ;; signal "b".
Section client.
Context {Σ : iFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
......
......@@ -24,14 +24,14 @@ Coercion of_val : val >-> expr.
are not put in any scope so as to avoid lots of annoying %L scopes while
pretty printing. *)
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope.
Notation "' l" := (Lit l%Z) (at level 8, format "' l").
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Case e0 x1 e1 x2 e2)
(e0, x1, e1, x2, e2 at level 200) : lang_scope.
Notation "' l" := (Lit l%Z) (at level 8, format "' l").
Notation "' l" := (LitV l%Z) (at level 8, format "' l").
Notation "'()" := (Lit LitUnit) (at level 0).
Notation "'()" := (LitV LitUnit) (at level 0).
Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope.
Notation "! e" := (Load e%L) (at level 9, right associativity) : lang_scope.
Notation "'ref' e" := (Alloc e%L)
(at level 30, right associativity) : lang_scope.
Notation "- e" := (UnOp MinusUnOp e%L)
......
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