Commit 1b23f935 authored by Dan Frumin's avatar Dan Frumin

Add simple tacticals for binding in the threadpool

parent 07aac180
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris_logrel.F_mu_ref_conc Require Import rules.
From iris_logrel.F_mu_ref_conc Require Export lang.
Set Default Proof Using "Type".
Import lang.
(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds. *)
Ltac reshape_val e tac :=
let rec go e :=
lazymatch e with
| of_val ?v => v
| Rec ?e => constr:(RecV e)
| TLam ?e => constr:(TLamV e)
| Unit => constr:(UnitV)
| Nat ?n => constr:(NatV n)
| Bool ?b => constr:(BoolV b)
| Pair ?e1 ?e2 =>
let v1 := go e1 in let v2 := go e2 in constr:(PairV v1 v2)
| 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.
Ltac reshape_expr e tac :=
let rec go K e :=
match e with
| _ => tac (reverse K) e
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| BinOp ?op ?e1 ?e2 =>
reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
| BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
| If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
| Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
| Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
| Fst ?e => go (FstCtx :: K) e
| Snd ?e => go (SndCtx :: K) e
| InjL ?e => go (InjLCtx :: K) e
| InjR ?e => go (InjRCtx :: K) e
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
| 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)
| Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
| CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
[ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
| go (CasMCtx v0 e2 :: K) e1 ])
| CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
end in go (@nil ectx_item) e.
(** wp-specific helper tactics *)
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl
end.
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind_core K
end)
| _ => fail "wp_bind: not a 'wp'"
end.
From iris_logrel.F_mu_ref_conc Require Import rules_binary.
Ltac tp_bind_helper j K e efoc :=
reshape_expr e ltac:(fun K' e' =>
match e' with
| efoc => unify e' efoc;
lazymatch eval cbn in (K ++ K') with
| ?K'' =>
replace (tpool_mapsto j (fill K e))
with (tpool_mapsto j (fill K'' e'))
by (rewrite ?fill_app; reflexivity)
end
end).
(* Todo: implement this as a tac-lemma *)
Tactic Notation "tp_bind" constr(H) open_constr(efoc) :=
iStartProof;
let rec find p Γ H :=
match Γ with
| Esnoc ?Γ H (tpool_mapsto ?j (fill ?K ?e)) =>
tp_bind_helper j K e efoc
| Esnoc ?Γ ?i ?P => find p Γ H
end in
match goal with
| |- of_envs (Envs ?Γp ?Γs) ?Q =>
first [find true Γp H | find false Γs H
|fail "tp_bind:" H "not found or its contents is not understood"]
end.
......@@ -34,6 +34,7 @@ F_mu_ref_conc/fundamental_binary.v
F_mu_ref_conc/soundness_unary.v
F_mu_ref_conc/context_refinement.v
F_mu_ref_conc/soundness_binary.v
F_mu_ref_conc/tactics.v
F_mu_ref_conc/examples/lock.v
F_mu_ref_conc/examples/counter.v
F_mu_ref_conc/examples/stack/stack_rules.v
......
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