Skip to content
Snippets Groups Projects
Commit 28b051a0 authored by Ralf Jung's avatar Ralf Jung
Browse files

improve WP printing

parent 4f711829
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/bi/weakestpre.v
+ 18
− 16
View file @ 28b051a0
......@@ -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 } ] ]" :=
......
tests/heap_lang.ref
+ 2
− 1
View file @ 28b051a0
......@@ -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
......
tests/heap_lang_printing.ref
+ 45
− 46
View file @ 28b051a0
......@@ -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
......
tests/list_reverse.ref
+ 2
− 1
View file @ 28b051a0
......@@ -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 }]
tests/one_shot.ref
+ 2
− 1
View file @ 28b051a0
......@@ -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
tests/one_shot_once.ref
+ 2
− 1
View file @ 28b051a0
......@@ -39,5 +39,6 @@
match: InjRV #m with
InjL <> => #()
| InjR <> => assert: InjRV #m = "y'"
end {{ _, True }}
end
{{ _, True }}
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