(* iris_heap_lang/class_instances.v *)
From iris.program_logic Require Export language
From iris.heap_lang Require Export lang
From iris.heap_lang Require Import tactics notation
From iris.prelude Require Import options

Global Instanceinto_val_val v : IntoVal (Val v) v.
Proof. done. Qed.

Global Instanceas_val_val v : AsVal (Val v).
Proof. by eexists. Qed.

Local Ltacsolve_atomic :=
    apply strongly_atomic_atomic, ectx_language_atomic;
      [inversion 1; naive_solver
      |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].

Global Instancerec_atomic s f x e : Atomic s (Rec f x e).
  Proof. solve_atomic. Qed.

Global Instancepair_atomic s v1 v2 : Atomic s (Pair (Val v1) (Val v2)).
  Proof. solve_atomic. Qed.

Global Instanceinjl_atomic s v : Atomic s (InjL (Val v)).
  Proof. solve_atomic. Qed.

Global Instanceinjr_atomic s v : Atomic s (InjR (Val v)).
  Proof. solve_atomic. Qed.

Global Instancebeta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
  Proof. destruct f, x; solve_atomic. Qed.

Global Instanceunop_atomic s op v : Atomic s (UnOp op (Val v)).
  Proof. solve_atomic. Qed.

Global Instancebinop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
  Proof. solve_atomic. Qed.

Global Instanceif_true_atomic s v1 e2 :
    Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
  Proof. solve_atomic. Qed.

Global Instanceif_false_atomic s e1 v2 :
    Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
  Proof. solve_atomic. Qed.

Global Instancefst_atomic s v : Atomic s (Fst (Val v)).
  Proof. solve_atomic. Qed.

Global Instancesnd_atomic s v : Atomic s (Snd (Val v)).
  Proof. solve_atomic. Qed.

Global Instancefork_atomic s e : Atomic s (Fork e).
  Proof. solve_atomic. Qed.

Global Instancealloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
  Proof. solve_atomic. Qed.

Global Instancefree_atomic s v : Atomic s (Free (Val v)).
  Proof. solve_atomic. Qed.

Global Instanceload_atomic s v : Atomic s (Load (Val v)).
  Proof. solve_atomic. Qed.

Global Instancexchg_atomic s v1 v2 : Atomic s (Xchg (Val v1) (Val v2)).
  Proof. solve_atomic. Qed.

Global Instancestore_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
  Proof. solve_atomic. Qed.

Global Instancecmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
  Proof. solve_atomic. Qed.

Global Instancefaa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
  Proof. solve_atomic. Qed.

Global Instancenew_proph_atomic s : Atomic s NewProph.
  Proof. solve_atomic. Qed.

Global Instanceresolve_atomic s e v1 v2 :
    Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
  Proof.
    rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
    simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
    - subst. inversion_clear step. by eapply (H σ1 (Val _) _ σ2 efs), base_prim_step.
    - rewrite fill_app. rewrite fill_app in Hfill.
      assert (∀ v, Val v = fill Ks e1' → False) as fill_absurd.
      { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
        apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
      destruct K; (inversion Hfill; clear Hfill; subst; try
        match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
      refine (_ (H σ1 (fill (Ks ++ [_]) e2') _ σ2 efs _)).
      + destruct s; intro Hs; simpl in *.
        * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
        * apply irreducible_resolve. by rewrite fill_app in Hs.
      + econstructor; try done. simpl. by rewrite fill_app.
  Qed.

Class AsRecV(v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.

Global HintMode AsRecV ! - - - : typeclass_instances.

Definition AsRecV_recvf x e : AsRecV (RecV f x e) f x e := eq_refl.

Global HintExtern 0 (AsRecV (RecV _ _ _) _ _ _) =>
  apply AsRecV_recv : typeclass_instances.

Local Ltacsolve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.

Local Ltacsolve_exec_puredet := simpl; intros; by inv_base_step.

Local Ltacsolve_pure_exec :=
    subst; intros ?; apply nsteps_once, pure_base_step_pure_step;
      constructor; [solve_exec_safe | solve_exec_puredet].

Global Instancepure_recc f x (erec : expr) :
    PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
  Proof. solve_pure_exec. Qed.

Global Instancepure_pairc (v1 v2 : val) :
    PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
  Proof. solve_pure_exec. Qed.

Global Instancepure_injlc (v : val) :
    PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
  Proof. solve_pure_exec. Qed.

Global Instancepure_injrc (v : val) :
    PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
  Proof. solve_pure_exec. Qed.

Global Instancepure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
    PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
  Proof. unfold AsRecV in *. solve_pure_exec. Qed.

Global Instancepure_unop op v v' :
    PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
  Proof. solve_pure_exec. Qed.

Global Instancepure_binop op v1 v2 v' :
    PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
  Proof. solve_pure_exec. Qed.

Global Instancepure_eqop v1 v2 :
    PureExec (vals_compare_safe v1 v2) 1
      (BinOp EqOp (Val v1) (Val v2))
      (Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
  Proof.
    intros Hcompare.
    cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
    { intros. revert Hcompare. solve_pure_exec. }
    rewrite /bin_op_eval /= decide_True //.
  Qed.

Global Instancepure_if_true e1 e2 :
    PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
  Proof. solve_pure_exec. Qed.

Global Instancepure_if_false e1 e2 :
    PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
  Proof. solve_pure_exec. Qed.

Global Instancepure_fst v1 v2 :
    PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
  Proof. solve_pure_exec. Qed.

Global Instancepure_snd v1 v2 :
    PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
  Proof. solve_pure_exec. Qed.

Global Instancepure_case_inl v e1 e2 :
    PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
  Proof. solve_pure_exec. Qed.

Global Instancepure_case_inr v e1 e2 :
    PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
  Proof. solve_pure_exec. Qed.