diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index b2c248e6b5db44cf5fa4dfda60663115b7a744c9..c248f3411aba054c334a55b1cbd78f8b10b55954 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -56,24 +56,28 @@ Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
-(** Notations with binder. The indentation for the inner format block is chosen
-such that *if* one has a single-character mask (e.g. [E]), the second line
-should align with the binder(s) on the first line. *)
+(** Notations with binder. *)
+(** The general approach we use for all these complex notations: an outer '[hv'
+to switch bwteen "horizontal mode" where it all fits on one line, and "vertical
+mode" where each '/' becomes a line break. Then, as appropriate, nested boxes
+('['...']') for things like preconditions and postconditions such that they are
+maximally horizontal and suitably indented inside the parentheses that surround
+them. *)
Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' @ s ; E {{ v , Q } } ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' @ '[' s ; '/' E ']' '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' @ E {{ v , Q } } ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' @ E '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' @ E ? {{ v , Q } } ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' @ E '/' ? {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' {{ v , Q } } ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' ? {{ v , Q } } ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' ? {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
(* Texan triples *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
@@ -159,24 +163,22 @@ Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
-(** Notations with binder. The indentation for the inner format block is chosen
-such that *if* one has a single-character mask (e.g. [E]), the second line
-should align with the binder(s) on the first line. *)
+(** Notations with binder. *)
Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' @ s ; E [{ v , Q } ] ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' @ '[' s ; '/' E ']' '/' [{ '[' v , '/' Q ']' } ] ']'") : bi_scope.
Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' @ E [{ v , Q } ] ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' @ E '/' [{ '[' v , '/' Q ']' } ] ']'") : bi_scope.
Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' @ E ? [{ v , Q } ] ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' @ E '/' ? [{ '[' v , '/' Q ']' } ] ']'") : bi_scope.
Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' [{ v , Q } ] ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' [{ '[' v , '/' Q ']' } ] ']'") : bi_scope.
Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
- format "'[' 'WP' e '/' '[ ' ? [{ v , Q } ] ']' ']'") : bi_scope.
+ format "'[hv' 'WP' e '/' ? [{ '[' v , '/' Q ']' } ] ']'") : bi_scope.
(* Texan triples *)
Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 2cf9ac222f035deeae5075af0599ac7b9c7f0473..ecab7bdd6a9a190f402ca6ecec3c33c3ace5c769 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -32,7 +32,8 @@
"Hl" : l ↦ #1
--------------------------------------∗
WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
- @ E [{ v, ⌜v = #2⌠}]
+ @ E
+ [{ v, ⌜v = #2⌠}]
1 goal
diff --git a/tests/heap_lang_printing.ref b/tests/heap_lang_printing.ref
index b9f357b8ad41ef51565a202f9668dacf0d3f609d..d45a1612fa2b9dc8fbef1223a19b36213da2bf50 100644
--- a/tests/heap_lang_printing.ref
+++ b/tests/heap_lang_printing.ref
@@ -26,11 +26,12 @@
============================
--------------------------------------∗
WP fun1 #()
- {{ v, WP let: "val1" := v in
- let: "val2" := fun2 "val1" in
- let: "val3" := fun3 "val2" in
- if: "val1" = "val2" then "val" else "val3"
- {{ _, True }} }}
+ {{ v,
+ WP let: "val1" := v in
+ let: "val2" := fun2 "val1" in
+ let: "val3" := fun3 "val2" in
+ if: "val1" = "val2" then "val" else "val3"
+ {{ _, True }} }}
1 goal
@@ -43,9 +44,9 @@
WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
- {{ _, long_post
- ∗ long_post
- ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
+ {{ _,
+ long_post
+ ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
1 goal
@@ -56,12 +57,14 @@
============================
--------------------------------------∗
WP fun1 #()
- {{ v, WP let: "val1" := v in
- let: "val2" := fun2 "val1" in
- let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
- {{ _, long_post
- ∗ long_post
- ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }} }}
+ {{ v,
+ WP let: "val1" := v in
+ let: "val2" := fun2 "val1" in
+ let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
+ {{ _,
+ long_post
+ ∗ long_post
+ ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }} }}
1 goal
@@ -79,10 +82,10 @@
WP let: "val1" := ! #l1 in
let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
- @ E_long {{ _, long_post
- ∗ long_post
- ∗ long_post
- ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
+ @ E_long
+ {{ _,
+ long_post
+ ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
1 goal
@@ -98,14 +101,16 @@
"Hinv" : inv N True
--------------------------------------∗
WP ! #l1
- @ E_long {{ v, WP let: "val1" := v in
- let: "val2" := fun2 "val1" in
- let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
- @ E_long {{ _, long_post
- ∗ long_post
- ∗ long_post
- ∗ long_post
- ∗ long_post ∗ long_post ∗ long_post }} }}
+ @ E_long
+ {{ v,
+ WP let: "val1" := v in
+ let: "val2" := fun2 "val1" in
+ let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
+ @ E_long
+ {{ _,
+ long_post
+ ∗ long_post
+ ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }} }}
1 goal
@@ -120,26 +125,20 @@
============================
--------------------------------------∗
WP ! #l1
- @ E_long ∖ ↑N {{ v, |={E_long ∖ ↑N}=> ▷ True
- ∗ WP let: "val1" :=
- v in
- let: "val2" :=
- fun2 "val1" in
- let: "v" :=
- fun3 "v" in
- if: "v" = "v" then "v" else "v"
- @ E_long {{ _,
- long_post
- ∗
- long_post
- ∗
- long_post
- ∗
- long_post
- ∗
- long_post
- ∗
- long_post ∗ long_post }} }}
+ @ E_long ∖ ↑N
+ {{ v,
+ |={E_long ∖ ↑N}=> ▷ True
+ ∗ WP let: "val1" := v in
+ let: "val2" := fun2 "val1" in
+ let: "v" := fun3 "v" in
+ if: "v" = "v" then "v" else "v"
+ @ E_long
+ {{ _,
+ long_post
+ ∗ long_post
+ ∗ long_post
+ ∗ long_post
+ ∗ long_post ∗ long_post ∗ long_post }} }}
1 goal
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index cd47ff4bdd1763eb219c002b3b74f50dd5d0308e..f673d83d48d901ecd528dbb5b0fe60093d725090 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -29,5 +29,6 @@
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
- end [{ v, Φ v }]
+ end
+ [{ v, Φ v }]
diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index 94a3ddc05772f1ed1db1cd01a26a0c45d7698dfc..a4b6aa00646ce84d2e23352a30ae09ec3d36a974 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -38,6 +38,7 @@
∗ WP match: InjRV #m' with
InjL <> => assert: #false
| InjR "m" => assert: #m = "m"
- end {{ _, True }}
+ end
+ {{ _, True }}
Closed under the global context
diff --git a/tests/one_shot_once.ref b/tests/one_shot_once.ref
index 4be43be0dc1b52d1098fb69503a0791d46ee5469..5fb4112bd12fd42d37a9dfb3ff764765b2f0baf9 100644
--- a/tests/one_shot_once.ref
+++ b/tests/one_shot_once.ref
@@ -39,5 +39,6 @@
match: InjRV #m with
InjL <> => #()
| InjR <> => assert: InjRV #m = "y'"
- end {{ _, True }}
+ end
+ {{ _, True }}