Library iris.heap_lang.tactics

From iris.heap_lang Require Export lang.
Set Default Proof Using "Type".
Import heap_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_expr e tac :=
  let rec go K vs e :=
    match e with
    | _lazymatch vs with []tac K e | _fail end
    | App ?e (Val ?v) ⇒ add_item (AppLCtx v) vs K e
    | App ?e1 ?e2add_item (AppRCtx e1) vs K e2
    | UnOp ?op ?eadd_item (UnOpCtx op) vs K e
    | BinOp ?op ?e (Val ?v) ⇒ add_item (BinOpLCtx op v) vs K e
    | BinOp ?op ?e1 ?e2add_item (BinOpRCtx op e1) vs K e2
    | If ?e0 ?e1 ?e2add_item (IfCtx e1 e2) vs K e0
    | Pair ?e (Val ?v) ⇒ add_item (PairLCtx v) vs K e
    | Pair ?e1 ?e2add_item (PairRCtx e1) vs K e2
    | Fst ?eadd_item FstCtx vs K e
    | Snd ?eadd_item SndCtx vs K e
    | InjL ?eadd_item InjLCtx vs K e
    | InjR ?eadd_item InjRCtx vs K e
    | Case ?e0 ?e1 ?e2add_item (CaseCtx e1 e2) vs K e0
    | AllocN ?e (Val ?v) ⇒ add_item (AllocNLCtx v) vs K e
    | AllocN ?e1 ?e2add_item (AllocNRCtx e1) vs K e2
    | Load ?eadd_item LoadCtx vs K e
    | Store ?e (Val ?v) ⇒ add_item (StoreLCtx v) vs K e
    | Store ?e1 ?e2add_item (StoreRCtx e1) vs K e2
    | CmpXchg ?e0 (Val ?v1) (Val ?v2) ⇒ add_item (CmpXchgLCtx v1 v2) vs K e0
    | CmpXchg ?e0 ?e1 (Val ?v2) ⇒ add_item (CmpXchgMCtx e0 v2) vs K e1
    | CmpXchg ?e0 ?e1 ?e2add_item (CmpXchgRCtx e0 e1) vs K e2
    | FAA ?e (Val ?v) ⇒ add_item (FaaLCtx v) vs K e
    | FAA ?e1 ?e2add_item (FaaRCtx e1) vs K e2
    | Resolve ?ex (Val ?v1) (Val ?v2) ⇒ go K ((v1,v2) :: vs) ex
    | Resolve ?ex ?e1 (Val ?v2) ⇒ add_item (ResolveMCtx ex v2) vs K e1
    | Resolve ?ex ?e1 ?e2add_item (ResolveRCtx ex e1) vs K e2
  with add_item Ki vs K e :=
    lazymatch vs with
    | []go (Ki :: K) (@nil (val × val)) e
    | (?v1,?v2) :: ?vsadd_item (ResolveLCtx Ki v1 v2) vs K e
  go (@nil ectx_item) (@nil (val × val)) e.