Commit f378dbf0 authored by Dan Frumin's avatar Dan Frumin

Finish the rebasing

- Make sure that the whole project compiles
parent d488df51
......@@ -24,7 +24,6 @@ Ltac reshape_val e tac :=
| InjL ?e => let v := go e in constr:(InjLV v)
| InjR ?e => let v := go e in constr:(InjRV v)
| Fold ?e => let v := go e in constr:(FoldV v)
| Pack ?e => let v := go e in constr:(PackV v)
| Loc ?l => constr:(LocV l)
end in let v := go e in tac v.
......@@ -48,8 +47,6 @@ Ltac reshape_expr e tac :=
| Fold ?e => go (FoldCtx :: K) e
| Unfold ?e => go (UnfoldCtx :: K) e
| TApp ?e => go (TAppCtx :: K) e
| Pack ?e => go (PackCtx :: K) e
| Unpack ?e1 ?e2 => go (UnpackLCtx e2 :: K) e
| Alloc ?e => go (AllocCtx :: K) e
| Load ?e => go (LoadCtx :: K) e
| Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
......@@ -134,6 +131,7 @@ Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
Lemma fill_nil e : fill [] e = e.
Proof. by compute. Qed.
(* TODO: if the proposition is of the form
[j e], rewrite it to [j fill [] e] using fill_nil above
TODO: this is quite slow
......@@ -152,18 +150,7 @@ Tactic Notation "tp_normalise" constr(j) :=
(* TODO: figure out why the envs_simple_replace_sound lemma is not
strong enough. Try to see whether you could generalize it
Lemma tac_tp_store `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p j K K' e l e' v' v Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Store (Loc l) e')
envs_lookup i3 Δ1 = Some (false, l ↦ₛ v')%I
to_val e' = Some v
envs_simple_replace i2 false (Esnoc Enil i2 (j fill K' Unit)) Δ1 = Some Δ2
envs_simple_replace i3 false (Esnoc Enil i3 (l ↦ₛ v)) Δ2 = Some Δ3
(Δ3 |={E1,E2}=> Q)
(Δ1 |={E1,E2}=> Q).
strong enough. Try to see whether it is possible to generalize it
*)
Lemma tac_tp_store `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K K' e l e' v' v Q :
......@@ -520,43 +507,6 @@ Tactic Notation "tp_fold" constr(j) :=
|env_cbv; reflexivity || fail "tp_fold: this should not happen"
|(* new goal *)]; try (tp_normalise j).
Lemma tac_tp_pack `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e1 e2 v Q :
nclose specN E1
envs_lookup i1 Δ1 = Some (p, spec_ctx ρ)
envs_lookup i2 Δ1 = Some (false, j fill K e)%I
fill K e = fill K' (Unpack (Pack e1) e2)
to_val e1 = Some v
envs_simple_replace i2 false
(Esnoc Enil i2 (j fill K' (e2.[e1/]))) Δ1 = Some Δ2
(Δ2 |={E1,E2}=> Q)
(Δ1 |={E1,E2}=> Q).
Proof.
intros ??? Hfill ?? HQ.
rewrite -(idemp uPred_and Δ1).
rewrite {2}(envs_lookup_sound' Δ1 _). 2: exact H1.
rewrite uPred.sep_elim_l uPred.always_and_sep_r comm.
rewrite (envs_simple_replace_sound Δ1 Δ2 i2) //; simpl.
rewrite right_id. rewrite Hfill.
(* (S (spec_ctx ρ) (S (j => fill) (S (l v) ..))) *)
rewrite (assoc _ (spec_ctx ρ) (j _)%I).
rewrite step_Pack //.
rewrite -(fupd_trans E1 E1 E2).
rewrite fupd_frame_r.
apply fupd_mono. rewrite uPred.wand_elim_r.
done.
Qed.
Tactic Notation "tp_pack" constr(j) :=
iStartProof;
eapply (tac_tp_pack j);
[solve_ndisj || fail "tp_pack: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "tp_pack: cannot find spec_ctx" (* spec_ctx *)
|iAssumptionCore || fail "tp_pack: cannot find '" j " ⤇ ?'"
|tp_bind_helper
|fast_done || fail "tp_pack: not a value"
|env_cbv; reflexivity || fail "tp_pack: this should not happen"
|(* new goal *)]; try (tp_normalise j).
Lemma tac_tp_fst `{heapIG Σ, !cfgSG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K K' e e1 e2 v1 v2 Q :
nclose specN E1
......
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