Commit cde85898 authored by Ralf Jung's avatar Ralf Jung

move printing-only tests to their own sections

parent 705bc223
......@@ -115,6 +115,11 @@ Section tests.
P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
End tests.
Section printing_tests.
Context `{heapG Σ}.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
True - WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
......@@ -124,7 +129,7 @@ Section tests.
iIntros "_". Show.
Abort.
End tests.
End printing_tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
......@@ -22,6 +22,19 @@
1 subgoal
PROP : sbi
P, Q : PROP
Persistent0 : Persistent P
Persistent1 : Persistent Q
============================
_ : P
_ : Q
--------------------------------------□
<affine> (P ∗ Q)
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
"HP" : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
......@@ -32,6 +45,7 @@
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
_ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
......@@ -42,6 +56,7 @@
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
"HP" : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P |
......@@ -52,6 +67,7 @@
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
============================
_ : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P |
......@@ -59,15 +75,3 @@
--------------------------------------∗
True
1 subgoal
PROP : sbi
P, Q : PROP
Persistent0 : Persistent P
Persistent1 : Persistent Q
============================
_ : P
_ : Q
--------------------------------------□
<affine> (P ∗ Q)
......@@ -37,41 +37,6 @@ Lemma demo_3 P1 P2 P3 :
P1 P2 P3 - P1 (P2 x, (P3 x = 0) P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
(* Test line breaking of long assumptions. *)
Section linebreaks.
Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
- True.
Proof.
iIntros "HP". Show.
Abort.
Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
- True.
Proof.
iIntros "?". Show.
Abort.
(* This is specifically crafted such that not having the `hv` in
the proofmode notation breaks the output. *)
Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P Q)%I
(format "'TESTNOTATION' '{{' P '|' '/' Q '}' '}'") : bi_scope.
Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
- True.
Proof.
iIntros "HP". Show.
Abort.
Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
- True.
Proof.
iIntros "?". Show.
Abort.
End linebreaks.
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
......@@ -513,3 +478,45 @@ Proof.
lazymatch goal with |- coq_tactics.envs_entails _ ( P) => done end.
Qed.
End tests.
(** Test specifically if certain things print correctly. *)
Section printing_tests.
Context {PROP : sbi} `{!BiFUpd PROP}.
Implicit Types P Q R : PROP.
(* Test line breaking of long assumptions. *)
Section linebreaks.
Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
- True.
Proof.
iIntros "HP". Show.
Abort.
Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
- True.
Proof.
iIntros "?". Show.
Abort.
(* This is specifically crafted such that not having the `hv` in
the proofmode notation breaks the output. *)
Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P Q)%I
(format "'TESTNOTATION' '{{' P '|' '/' Q '}' '}'") : bi_scope.
Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
- True.
Proof.
iIntros "HP". Show.
Abort.
Lemma print_long_line_anon (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
- True.
Proof.
iIntros "?". Show.
Abort.
End linebreaks.
End printing_tests.
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