Instantiate Iris and dlang with our gDOT language.

From iris.program_logic Require ectx_language.
From iris.proofmode Require Import environments. (* Internals, used for extensions! *)
From D.pure_program_logic Require Import weakestpre lifting.

From D Require Import iris_prelude dlang.
From D.Dot Require Export syn.

Include LiftWp VlSorts.

Some tactics/proof automation for gDOT.
Names are inspired by the names of Iris's HeapLang tactics, and the behaviors are vaguely similar, but the implementations are more naive/less efficient.
Reduce pure computation steps.
Ltac wp_pure := rewrite -wp_pure_step_later -1?wp_value; last done; iNext.

Module Import gdot_proofmode.

  (* Taken from iris.heap_lang.tactics and iris.heap_lang.proofmode. *)

The tactic reshape_expr e tac decomposes the expression e into an evaluation context K and a subexpression e', and calls the tactic tac K e'.
  Ltac reshape_expr e tac :=
    let rec go K e :=
      let e := eval hnf in e in
      lazymatch e with
      | tapp (tv ?v1) ?e2go (AppRCtx v1 :: K) e2
      | tapp ?e1 ?e2go (AppLCtx e2 :: K) e1
      | tproj ?e1 ?lgo (ProjCtx l :: K) e1
      | tskip ?e1go (SkipCtx :: K) e1
      | tun ?op ?e1go (UnCtx op :: K) e1
      | tbin ?op (tv ?v1) ?e2go (BinRCtx op v1 :: K) e2
      | tbin ?op ?e1 ?e2go (BinLCtx op e2 :: K) e1
      | tif ?e0 ?e1 ?e2go (IfCtx e1 e2 :: K) e0
      | _tac K e
    in go (@nil ectx_item) e.

  Section CoqTactics.
    Context `{!dlangG Σ}.

    Lemma tac_wp_bind K Δ Φ e f :
      f = (λ e, ectx_language.fill K e) (* as an eta expanded hypothesis so that we can `simpl` it *)
      envs_entails Δ (WP e {{ v, WP f (tv v) {{ Φ }} }})%I
      envs_entails Δ (WP ectx_language.fill K e {{ Φ }}).
    Proof. rewrite envs_entails_unseal⇒ → →. by apply: wp_bind. Qed.
  End CoqTactics.

  Ltac wp_bind_core K :=
    lazymatch eval hnf in K with
    | []idtac
    | _eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify]
End gdot_proofmode.

Apply the wp_bind rule.
Tactic Notation "wp_bind" open_constr(efoc) := wp_bind_core [efoc].

#[local] Ltac wp_binds_core Ks :=
  lazymatch eval hnf in Ks with
  | []idtac
  | ?K :: ?Kswp_bind K; wp_binds_core Ks
Tactic Notation "wp_binds" open_constr(Ks) := wp_binds_core Ks.

Apply wp_bind automatically.

Ltac wp_abind :=
  lazymatch goal with
  | |- envs_entails _ ?P
    let P := eval cbn in P in
    lazymatch P with
    | wp ?s ?E ?e ?Q
      let e := eval cbn in e in
      reshape_expr e ltac:(fun Ks e'wp_binds (reverse Ks))
    | _fail "wp_abind: not a 'wp'"

Apply a WP using the wp_wand rule, applying wp_bind automatically.
Ltac wp_wapply spec_pat := wp_abind; iApply (wp_wand with spec_pat).