Commit 705bc223 authored by Ralf Jung's avatar Ralf Jung

test how WP prints when the code gets long

parent bf0b4bd4
Pipeline #9422 passed with stage
in 25 minutes and 34 seconds
......@@ -18,3 +18,15 @@
--------------------------------------∗
WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
1 subgoal
Σ : gFunctors
H : heapG Σ
fun1, fun2, fun3 : expr
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{ _, True }}
......@@ -5,7 +5,7 @@ From iris.heap_lang Require Import adequacy.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Section LiftingTests.
Section tests.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
......@@ -115,7 +115,16 @@ Section LiftingTests.
P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
End LiftingTests.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
True - WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in
if: "val1" = "val2" then "val" else "val3" {{ _, True }}.
Proof.
iIntros "_". Show.
Abort.
End tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
......@@ -54,35 +54,35 @@ Instance: Params (@wp) 6.
Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ s ; E {{ Φ } } ']'") : bi_scope.
format "'[hv' 'WP' e '/' @ s ; E {{ Φ } } ']'") : bi_scope.
Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E {{ Φ } } ']'") : bi_scope.
format "'[hv' 'WP' e '/' @ E {{ Φ } } ']'") : bi_scope.
Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E ? {{ Φ } } ']'") : bi_scope.
format "'[hv' 'WP' e '/' @ E ? {{ Φ } } ']'") : bi_scope.
Notation "'WP' e {{ Φ } }" := (wp NotStuck e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' {{ Φ } } ']'") : bi_scope.
format "'[hv' 'WP' e '/' {{ Φ } } ']'") : bi_scope.
Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' ? {{ Φ } } ']'") : bi_scope.
format "'[hv' 'WP' e '/' ? {{ Φ } } ']'") : bi_scope.
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 } } }" :=
......
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