Commit 01439787 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Another test, and fix bug in optimizer.

parent ecdbeb34
......@@ -52,8 +52,34 @@ Section tests_vcg.
been introduced like the `#10` in this example.
- `simpl` will probably unfold too much, and as such, it does not work in
a nested fashion. *)
iApply (optimize_sound []);
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iExists (dValUnknown (#12)). done.
iExists (dValUnknown (#12)). eauto.
Qed.
Lemma test5 (l k : loc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
( Φ, Φ #11 - awp e1 True Φ) -
( Φ, Φ #12 - awp e2 True Φ) -
l C #1 -
k C #1 -
awp (a_bin_op PlusOp
(a_store (a_ret #l) (a_ret #2))
(a_store (a_ret #k) e1 ;;;; e2)) True (λ v, l C[LLvl] #2 k C #11).
Proof.
iIntros "He1 He2 Hl Hk". vcg_solver.
iIntros "Hk".
iApply "He1".
(* Now we need some way to mechanically continue *)
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
(* This stuff should happen automagically *)
iExists _. iFrame "Hk".
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iIntros "?".
iApply "He2".
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iExists (dValUnknown (#14)). eauto with iFrame.
Qed.
End tests_vcg.
......@@ -111,7 +111,7 @@ Section vcg.
Fixpoint optimize (m : denv) (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => Base Φ1
| Base Φ1 => mapsto_wand_list m (Base Φ1)
| MapstoStar (dLoc i) Φ1 =>
match denv_delete_frac i m with
| Some (m1, q1, dv) => optimize m1 (Φ1 q1 dv)
......
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