From iris.heap_lang Require Export proofmode notation.
From iris_c.c_translation Require Export monad.
From iris.proofmode Require Import coq_tactics.

Lemma tac_cwp_bind `{cmonadG Σ} K Δ R Φ e f :
  f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
  envs_entails Δ (WP e {{ v, cwp (f (of_val v)) R Φ }})%I →
  envs_entails Δ (cwp (fill K e) R Φ).
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_cwp_bind. Qed.

Ltac cwp_bind_core K :=
  lazymatch eval hnf in K with
  | [] => idtac
  | _ => eapply (tac_cwp_bind K); [simpl; reflexivity|lazy beta]
  end.

Tactic Notation "cwp_apply" open_constr(lem) :=
  iPoseProofCore lem as false true (fun H =>
    lazymatch goal with
    | |- envs_entails _ (cwp ?e ?R ?Q) =>
      reshape_expr e ltac:(fun K e' =>
        cwp_bind_core K; iApplyHyp H; try iNext (*; try wp_expr_simpl*) ) ||
      lazymatch iTypeOf H with
      | Some (_,?P) => fail "cwp_apply: cannot apply" P
      end
    | _ => fail "cwp_apply: not a 'cwp'"
    end).

Lemma tac_cwp_pure `{cmonadG Σ} Δ Δ' K e1 e2 e φ n R Φ :
  e = fill K e1 →
  PureExec φ n e1 e2 →
  φ →
  MaybeIntoLaterNEnvs n Δ Δ' →
  envs_entails Δ' (cwp (fill K e2) R Φ) →
  envs_entails Δ (cwp e R Φ).
Proof.
  rewrite envs_entails_eq=> -> ??? HΔ'.
  rewrite into_laterN_env_sound /=.
  rewrite HΔ' -cwp_pure //.
Qed.

Tactic Notation "tac_bind_helper" :=
  lazymatch goal with
  | |- fill ?K ?e = fill _ ?efoc =>
     reshape_expr e ltac:(fun K' e' =>
       unify e' efoc;
       let K'' := eval cbn[app] in (K' ++ K) in
       replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
  | |- ?e = fill _ ?efoc =>
     reshape_expr e ltac:(fun K' e' =>
       unify e' efoc;
       replace e with (fill K' e') by (by rewrite ?fill_app))
  end; reflexivity.

Tactic Notation "cwp_pure" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
  | |- envs_entails _ (cwp ?e ?R ?Q) =>
    let e := eval simpl in e in
    reshape_expr e ltac:(fun K e' =>
      unify e' efoc;
      eapply (tac_cwp_pure _ _ _ _ _ (fill K e'));
      [tac_bind_helper                (* e = fill K e' *)
      |apply _                        (* PureExec *)
      |try fast_done                  (* The pure condition for PureExec *)
      |apply _                        (* IntoLaters *)
      |simpl
      ])
    || fail "cwp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
  | _ => fail "cwp_pure: not an 'cwp'"
  end.

(* See Iris for documentation on this tactic *)
Ltac cwp_pures :=
  iStartProof;
  repeat (cwp_pure _; []). (* The `;[]` makes sure that no side-condition
                             magically spawns. *)

Tactic Notation "cwp_rec" :=
  let H := fresh in
  assert (H := AsRecV_recv_locked);
  cwp_pure (App _ _);
  clear H.

Tactic Notation "cwp_if" := cwp_pure (If _ _ _).
Tactic Notation "cwp_if_true" := cwp_pure (If (LitV (LitBool true)) _ _).
Tactic Notation "cwp_if_false" := cwp_pure (If (LitV (LitBool false)) _ _).
Tactic Notation "cwp_unop" := cwp_pure (UnOp _ _).
Tactic Notation "cwp_binop" := cwp_pure (BinOp _ _ _).
Tactic Notation "cwp_op" := cwp_unop || cwp_binop.
Tactic Notation "cwp_lam" := cwp_rec.
Tactic Notation "cwp_let" := cwp_lam.
Tactic Notation "cwp_seq" := cwp_lam.
Tactic Notation "cwp_proj" := cwp_pure (Fst _) || cwp_pure (Snd _).
Tactic Notation "cwp_case" := cwp_pure (Case _ _ _).
Tactic Notation "cwp_match" := cwp_case; cwp_let.
Tactic Notation "cwp_inj" := cwp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "cwp_pair" := cwp_pure (Pair _ _).
Tactic Notation "cwp_closure" := cwp_pure (Rec _ _ _).