Commit bd7a1b96 authored by Ralf Jung's avatar Ralf Jung

improve printing of texan triples

parent 9fc544a3
......@@ -30,3 +30,14 @@
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{ _, True }}
1 subgoal
Σ : gFunctors
H : heapG Σ
fun1, fun2, fun3 : expr
============================
{{{ True }}}
let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
......@@ -128,6 +128,15 @@ Section printing_tests.
iIntros "_". Show.
Abort.
Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
{{{ True }}}
let: "val1" := fun1 #() in
let: "val2" := fun2 "val1" in
let: "val3" := fun3 "val2" in
if: "val1" = "val2" then "val" else "val3"
{{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
Proof. Show. Abort.
End printing_tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
......
......@@ -89,93 +89,75 @@ 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 "{{{ 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 "{{{ 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 "{{{ 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
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : bi_scope.
format "'[hv' {{{ P } } } '/ ' 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
(at level 20, x closed binder, y closed binder,
format "{{{ 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 "{{{ 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 "{{{ 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 "{{{ 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,
format "{{{ P } } } e {{{ RET pat ; Q } } }") : bi_scope.
format "'[hv' {{{ P } } } '/ ' e '/' {{{ RET pat ; Q } } } ']'") : bi_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
( Φ, P - (Q - Φ pat%V) - WP e ?{{ Φ }})%I
(at level 20,
format "{{{ 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 } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ s; E {{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ s; E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
P - ( x, .. ( y, Q - Φ pat%V) .. ) - WP e ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ s; E {{ Φ }})
(at level 20,
format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : stdpp_scope.
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ s; E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ E {{ Φ }})
(at level 20,
format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : stdpp_scope.
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ E {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ E ?{{ Φ }})
(at level 20,
format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : stdpp_scope.
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ E ?{{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e {{ Φ }})
(at level 20,
format "{{{ P } } } e {{{ RET pat ; Q } } }") : stdpp_scope.
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e {{ Φ }}) : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e ?{{ Φ }})
(at level 20,
format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : stdpp_scope.
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e ?{{ Φ }}) : stdpp_scope.
Section wp.
Context `{irisG Λ Σ}.
......
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