Commit 51afb8bd authored by Ralf Jung's avatar Ralf Jung

fix newlines being inserted in bad places for WP

parent a85a8e2f
Pipeline #9722 failed with stage
in 7 minutes and 38 seconds
......@@ -119,6 +119,10 @@ End tests.
Section printing_tests.
Context `{heapG Σ}.
(* These terms aren't even closed, but that's not what this is about. The
length of the variable names etc. has been carefully chosen to trigger
particular behavior of the Coq pretty printer. *)
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
True - WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
......@@ -128,6 +132,24 @@ Section printing_tests.
iIntros "_". Show.
Abort.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
True - WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in
if: "v" = "v" then "v" else "v" {{ Φ }}.
Proof.
iIntros "_". Show.
Abort.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
True - WP let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "v" := fun3 "v" in
if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
Proof.
iIntros "_". Show.
Abort.
Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
{{{ True }}}
let: "val1" := fun1 #() in
......
......@@ -53,53 +53,48 @@ Arguments wp {_ _ _} _ _ _%E _.
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.
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E {{ Φ } } ']'") : bi_scope.
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' @ E ? {{ Φ } } ']'") : bi_scope.
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e {{ Φ } }" := (wp NotStuck e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' {{ Φ } } ']'") : bi_scope.
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck e%E Φ)
(at level 20, e, Φ at level 200,
format "'[' 'WP' e '/' ? {{ Φ } } ']'") : bi_scope.
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
  • Why are these only parsing, can you please write a comment why that's so.

  • I'll add a comment in the sources tomorrow, but the answer is: They are overlapping with the other instances (this matches all postconditions, the others match postconditions that are lambdas), and in practice the others were used anyway (hence the v, Φ v that we always see).

  • Done.

Please register or sign in to reply
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 "'[' '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 "'[' '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 "'[' '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 "'[' '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 "'[' 'WP' e '/' '[ ' ? {{ v , Q } } ']' ']'") : bi_scope.
  • The seemingly arbitrary numbers of spaces in all of these notations require some explanation.

  • Yeah I had no idea what would be good here... the number of spaces makes it so that the second line is aligned with the binder (v) if the mask is a single character (like E).

  • Alright, please write a comment for that :)

  • Done.

Please register or sign in to reply
(* Texan triples *)
Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ s; E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e @ s ; E '/' {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' @ s ; E {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e @ E '/' {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e @ E ? '/' {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})%I
......@@ -109,20 +104,20 @@ Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e ?{{ Φ }})%I
(at level 20, x closed binder, y closed binder,
format "'[hv' {{{ P } } } '/ ' e ? '/' {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ x .. y , RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e @ s; E {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e @ s ; E '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' @ s ; E {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e @ E {{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e @ E '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' @ E {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e @ E ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e @ E ? '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' @ E ? {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e {{ Φ }})%I
(at level 20,
......@@ -130,7 +125,7 @@ Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e ?{{ Φ }})%I
(at level 20,
format "'[hv' {{{ P } } } '/ ' e ? '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' ? {{{ RET pat ; Q } } } ']'") : bi_scope.
(* Aliases for stdpp scope -- they inherit the levels and format from above. *)
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