From iris_logrel.prelude Require Export hax.
From iris_logrel.F_mu_ref_conc Require Export lang subst notation.

Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pureexec :=
  apply hoist_pred_pureexec; intros; destruct_and?;
  apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].

Instance pure_binop op e1 v1 e2 v2 v `(to_val e1 = Some v1) `(to_val e2 = Some v2):
  PureExec (binop_eval op v1 v2 = Some v)
           (BinOp op e1 e2)
           (of_val v).
Proof. solve_pureexec. Qed.

Instance pure_rec f x e1 e2 v2 `{Closed ∅ (Rec f x e1)} `(to_val e2 = Some v2) :
  PureExec True
           (App (Rec f x e1) e2)
           (subst' f (Rec f x e1) (subst' x e2 e1)).
Proof. solve_pureexec. Qed.

(* TODO: give this one a correct priority? *)
Instance pure_rec_locked e f x e1 e2 v2 `(to_val e2 = Some v2) `(e = Rec f x e1) `{Closed (x :b: f :b: ∅) e1} :
  PureExec True
           (App e e2)
           (e $/ v2) | 100.
Proof.
  apply hoist_pred_pureexec; intros; destruct_and?;
  apply det_head_step_pureexec. 
  - solve_exec_safe.
  - destruct f; solve_exec_puredet.
Qed.

Instance pure_fst e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
  PureExec True (Fst (Pair e1 e2)) e1.
Proof. solve_pureexec. Qed.

Instance pure_snd e1 v1 e2 v2 `(to_val e1 = Some v1) `(to_val e2 = Some v2) :
  PureExec True (Snd (Pair e1 e2)) e2.
Proof. solve_pureexec. Qed.

Instance pure_unfold e1 v1 `(to_val e1 = Some v1) :
  PureExec True (Unfold (Fold e1)) e1.
Proof. solve_pureexec. Qed.

Instance pure_unpack e1 e2 v1 `(to_val e1 = Some v1) :
  PureExec True (Unpack (Pack e1) e2) (e2 e1).
Proof. solve_pureexec. Qed.

Instance pure_if_true e1 e2 :
  PureExec True (If #true e1 e2) e1.
Proof. solve_pureexec. Qed.

Instance pure_if_false e1 e2 :
  PureExec True (If #false e1 e2) e2.
Proof. solve_pureexec. Qed.

Instance pure_case_inl e0 v `(to_val e0 = Some v) e1 e2  :
  PureExec True (Case (InjL e0) e1 e2) (e1 e0).
Proof. solve_pureexec. Qed.

Instance pure_case_inr e0 v `(to_val e0 = Some v) e1 e2  :
  PureExec True (Case (InjR e0) e1 e2) (e2 e0).
Proof. solve_pureexec. Qed.

Instance pure_tlam e `{Closed ∅ e} :
  PureExec True
           (TApp (TLam e))
           e.
Proof. solve_pureexec. Qed.