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

add some more challenging printing tests

parent eb05e835
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/heap_lang_printing.ref
+ 131
− 8
View file @ 4f711829
...@@ -23,27 +23,123 @@ ...@@ -23,27 +23,123 @@
Σ : gFunctors Σ : gFunctors
heapGS0 : heapGS Σ heapGS0 : heapGS Σ
fun1, fun2, fun3 : expr fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ ============================
--------------------------------------∗
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 }} }}
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
fun1, fun2, fun3 : expr
long_post : iPropI Σ
============================ ============================
--------------------------------------∗ --------------------------------------∗
WP let: "val1" := fun1 #() in WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
{{ v, Φ v }} {{ _, long_post
∗ long_post
∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
1 goal 1 goal
Σ : gFunctors Σ : gFunctors
heapGS0 : heapGS Σ heapGS0 : heapGS Σ
fun1, fun2, fun3 : expr fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ long_post : iPropI Σ
E : coPset
============================ ============================
--------------------------------------∗ --------------------------------------∗
WP let: "val1" := fun1 #() in 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 }} }}
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
l1 : loc
fun2, fun3 : expr
long_post : iPropI Σ
N : namespace
E_long : coPset
H : ↑N ⊆ E_long
============================
"Hinv" : inv N True
--------------------------------------∗
WP let: "val1" := ! #l1 in
let: "val2" := fun2 "val1" in let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
@ E {{ v, Φ v }} @ E_long {{ _, long_post
∗ long_post
∗ long_post
∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
l1 : loc
fun2, fun3 : expr
long_post : iPropI Σ
N : namespace
E_long : coPset
H : ↑N ⊆ E_long
============================
"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 }} }}
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
l1 : loc
fun2, fun3 : expr
long_post : iPropI Σ
N : namespace
E_long : coPset
H : ↑N ⊆ E_long
============================
--------------------------------------∗
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 }} }}
1 goal 1 goal
...@@ -56,3 +152,30 @@ ...@@ -56,3 +152,30 @@
let: "val2" := fun2 "val1" in let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3" let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}} {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
fun1, fun2, fun3 : expr
E_mask_is_long_too : coPset
============================
{{{ True }}}
let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
@ E_mask_is_long_too {{{ (x y : val) (z : Z), RET
(x, y, #z); True }}}
1 goal
Σ : gFunctors
heapGS0 : heapGS Σ
fun1, fun2, fun3 : expr
long_post : iPropI Σ
E_mask_is_long_too : coPset
============================
{{{ True }}}
let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
@ E_mask_is_long_too {{{ (x y : val) (z : Z), RET
(x, y, #z); long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}}
tests/heap_lang_printing.v
+ 34
− 6
View file @ 4f711829
...@@ -27,24 +27,32 @@ Section printing_tests. ...@@ -27,24 +27,32 @@ Section printing_tests.
if: "val1" = "val2" then "val" else "val3" {{ _, True }}. if: "val1" = "val2" then "val" else "val3" {{ _, True }}.
Proof. Proof.
iIntros "_". Show. iIntros "_". Show.
wp_bind (fun1 #()). Show.
Abort. Abort.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ : Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) long_post :
True -∗ WP let: "val1" := fun1 #() in True -∗ WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in let: "v" := fun3 "v" in
if: "v" = "v" then "v" else "v" {{ Φ }}. if: "v" = "v" then "v" else "v"
{{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
Proof. Proof.
iIntros "_". Show. iIntros "_". Show.
wp_bind (fun1 #()). Show.
Abort. Abort.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E : Lemma wp_print_long_expr (l1 : loc) (fun2 fun3 : expr) long_post N E_long :
True -∗ WP let: "val1" := fun1 #() in ↑N ⊆ E_long →
inv N True -∗ WP let: "val1" := ! #l1 in
let: "val2" := fun2 "val1" in let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in let: "v" := fun3 "v" in
if: "v" = "v" then "v" else "v" @ E {{ Φ }}. if: "v" = "v" then "v" else "v"
@ E_long
{{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
Proof. Proof.
iIntros "_". Show. iIntros (?) "Hinv". Show.
wp_bind (! #l1)%E. Show.
iInv "Hinv" as "_". Show.
Abort. Abort.
Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) : Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
...@@ -56,4 +64,24 @@ Section printing_tests. ...@@ -56,4 +64,24 @@ Section printing_tests.
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}. {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
Proof. Show. Abort. Proof. Show. Abort.
Lemma texan_triple_long_expr_mask (fun1 fun2 fun3 : expr) E_mask_is_long_too :
{{{ True }}}
let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in
if: "val1" = "val2" then "val" else "val3"
@ E_mask_is_long_too
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
Proof. Show. Abort.
Lemma texan_triple_long_expr_mask_post (fun1 fun2 fun3 : expr) long_post E_mask_is_long_too :
{{{ True }}}
let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in
if: "val1" = "val2" then "val" else "val3"
@ E_mask_is_long_too
{{{ (x y : val) (z : Z), RET (x, y, #z); long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}}.
Proof. Show. Abort.
End printing_tests. End printing_tests.
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