Commit 1090f98c authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Better behaved wp_tick_match.

parent f149a710
......@@ -134,7 +134,7 @@ Proof.
rewrite !translation_of_val. setoid_rewrite translation_of_val.
iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
wp_tick_rec.
wp_tick_match ; wp_lam.
wp_tick_match.
wp_tick_load. wp_tick_proj. wp_tick_let.
wp_tick_load. wp_tick_proj. wp_tick_let.
iDestruct "Htc" as "[Htc1 Htc]".
......
......@@ -126,7 +126,7 @@ Section Thunk.
| iDestruct "Hevaluated" as (v) "(>Ht & Hv & >%)" ].
(* (1) if it is UNEVALUATED, we evaluate it: *)
{
wp_tick_load. wp_tick_match ; wp_let.
wp_tick_load. wp_tick_match.
iDestruct (own_auth_mnat_le with "Hγ● Hγ◯") as %I.
iDestruct (TC_weaken _ _ I with "Htc") as "Htc".
wp_tick ; wp_apply ("Hf" with "Htc") ; iIntros (v) "Hv".
......@@ -138,7 +138,7 @@ Section Thunk.
}
(* (2) if it is EVALUATED, we get the result which is already memoized: *)
{
wp_tick_load. wp_tick_match ; wp_let.
wp_tick_load. wp_tick_match.
iApply "Post".
iDestruct (Hφdup with "Hv") as "[Hv $]".
iApply "Hclose". iFrame "Hp".
......
......@@ -644,8 +644,6 @@ Ltac wp_tick :=
iAssumptionCore || fail "wp_tick: cannot find TC_invariant" in
let solve_TC _ :=
iAssumptionCore || fail "wp_tick: cannot find TC (S _)" in
let finish _ :=
wp_expr_simpl ; try first [ wp_pure (Seq (Lit LitUnit) _) | wp_value_head ] in
iStartProof ;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
......@@ -659,7 +657,7 @@ Ltac wp_tick :=
| solve_TICKCTXT ()
| solve_TC ()
| proofmode.reduction.pm_reflexivity
| finish () ]
| wp_expr_simpl ]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
fail "wp_tick is not implemented for twp"
| _ => fail "wp_tick: not a 'wp'"
......@@ -679,10 +677,10 @@ Ltac wp_tick_rec :=
| fail ].
Ltac wp_tick_lam := wp_tick_rec.
Ltac wp_tick_let := wp_tick ; wp_let.
Ltac wp_tick_seq := wp_tick.
Ltac wp_tick_seq := wp_tick ; wp_seq.
Ltac wp_tick_op := wp_tick ; wp_op.
Ltac wp_tick_if := wp_tick ; wp_if.
Ltac wp_tick_match := wp_tick ; wp_match ; do 2 wp_lam ; wp_tick.
Ltac wp_tick_match := wp_tick ; wp_match ; do 2 wp_lam ; wp_tick ; wp_lam.
Ltac wp_tick_proj := wp_tick ; wp_proj.
Ltac wp_tick_alloc loc := wp_tick ; wp_alloc loc.
Ltac wp_tick_load := wp_tick ; wp_load.
......
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