Commit 81c0aaee authored by Robbert Krebbers's avatar Robbert Krebbers

Make of_val reduce by simpl.

And make constants P for which we do not want of_val P to reduce Opaque.
parent 131e53d4
Pipeline #926 passed with stage
......@@ -4,3 +4,4 @@ Definition newbarrier : val := λ: <>, ref #0.
Definition signal : val := λ: "x", '"x" <- #1.
Definition wait : val :=
rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
Global Opaque newbarrier signal wait.
......@@ -8,6 +8,7 @@ Definition acquire : val :=
rec: "acquire" "l" :=
if: CAS '"l" #false #true then #() else '"acquire" '"l".
Definition release : val := λ: "l", '"l" <- #false.
Global Opaque newlock acquire release.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......
......@@ -14,7 +14,7 @@ Infix "||" := Par : expr_scope.
Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
WSubst x es H par par := do_wsubst_closed _ x es H _.
Typeclasses Opaque par.
Global Opaque par.
Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
......
......@@ -13,6 +13,7 @@ Definition join : val :=
InjR "x" => '"x"
| InjL <> => '"join" '"c"
end.
Global Opaque spawn join.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......
......@@ -196,4 +196,3 @@ Ltac simpl_subst :=
Arguments wexpr : simpl never.
Arguments subst : simpl never.
Arguments wsubst : simpl never.
Arguments of_val : simpl never.
......@@ -9,7 +9,7 @@ Ltac wp_bind K :=
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl
end.
Ltac wp_done := rewrite -/of_val /= ?to_of_val; fast_done.
Ltac wp_done := rewrite /= ?to_of_val; fast_done.
Ltac wp_value_head :=
match goal with
......@@ -23,7 +23,7 @@ Ltac wp_value_head :=
end.
Ltac wp_finish := intros_revert ltac:(
rewrite -/of_val /= ?to_of_val; try strip_later; try wp_value_head).
rewrite /= ?to_of_val; try strip_later; try wp_value_head).
Tactic Notation "wp_value" :=
lazymatch goal with
......
......@@ -11,6 +11,7 @@ Definition client : expr [] :=
let: "b" := ^newbarrier #() in
('"y" <- (λ: "z", '"z" + #42) ;; ^signal '"b") ||
(^(worker 12) '"b" '"y" || ^(worker 17) '"b" '"y").
Global Opaque worker client.
Section client.
Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
......
......@@ -37,6 +37,7 @@ Section LiftingTests.
Definition Pred : val :=
λ: "x",
if: '"x" #0 then -^FindPred (-'"x" + #2) #0 else ^FindPred '"x" #0.
Global Opaque FindPred Pred.
Lemma FindPred_spec n1 n2 E Φ :
n1 < n2
......
......@@ -7,6 +7,7 @@ Import uPred.
Definition client eM eW1 eW2 : expr [] :=
let: "b" := newbarrier #() in
(eM ;; ^signal '"b") || ((^wait '"b" ;; eW1) || (^wait '"b" ;; eW2)).
Global Opaque client.
Section proof.
Context (G : cFunctor).
......
......@@ -18,6 +18,7 @@ Definition one_shot_example : val := λ: <>,
| InjR "m" => Assert ('"n" = '"m")
end
end)).
Global Opaque one_shot_example.
Class one_shotG Σ :=
OneShotG { one_shot_inG :> inG heap_lang Σ (one_shotR (dec_agreeR Z)) }.
......
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