(* iris/program_logic/ectxi_language.v *)
From iris.prelude Require Export prelude
From iris.program_logic Require Import language ectx_language
From iris.prelude Require Import options

Lemma heap_lang_mixin: EctxiLanguageMixin of_val to_val fill_item base_step.
    Proof.  Qed.

Record EctxiLanguageMixin:= {
    mixin_to_of_val v : to_val (of_val v) = Some v;
    mixin_of_to_val e v : to_val e = Some v → of_val v = e;
    mixin_val_stuck e1 σ1 κ e2 σ2 efs : base_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
    mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);

Structure ectxiLanguage:= EctxiLanguage {
  expr : Type;
  val : Type;
  ectx_item : Type;
  state : Type;
  observation : Type;
  of_val : val → expr;
  to_val : expr → option val;
  fill_item : ectx_item → expr → expr;
  base_step : expr → state → list observation → expr → state → list expr → Prop;
  ectxi_language_mixin :
    EctxiLanguageMixin of_val to_val fill_item base_step
}.
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.

Global ArgumentsEctxiLanguage {_ _ _ _ _ _ _ _ _} _.

Global Argumentsof_val {_} _.

Global Argumentsto_val {_} _.

Global Argumentsfill_item {_} _ _.

Global Argumentsbase_step {_} _ _ _ _ _ _.

Notation ectx:= (list (ectx_item Λ)).

Global Instancefill_item_inj Ki : Inj (=) (=) (fill_item Ki).
  Proof. apply ectxi_language_mixin. Qed.

Lemma fill_item_valKi e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
  Proof. apply ectxi_language_mixin. Qed.

Lemma fill_item_no_val_injKi1 Ki2 e1 e2 :
    to_val e1 = None → to_val e2 = None →
    fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
  Proof. apply ectxi_language_mixin. Qed.

Lemma base_ctx_step_valKi e σ1 κ e2 σ2 efs :
    base_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e).
  Proof. apply ectxi_language_mixin. Qed.

Definition fill(K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.

Lemma fill_app(K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
  Proof. apply foldl_app. Qed.

Definition ectxi_lang_ectx_mixin:
    EctxLanguageMixin of_val to_val [] (flip (++)) fill base_step.
  Proof.
    assert (fill_val : ∀ K e, is_Some (to_val (fill K e)) → is_Some (to_val e)).
    { intros K. induction K as [|Ki K IH]=> e //=. by intros ?%IH%fill_item_val. }
    assert (fill_not_val : ∀ K e, to_val e = None → to_val (fill K e) = None).
    { intros K e. rewrite !eq_None_not_Some. eauto. }
    split.
    - apply ectxi_language_mixin.
    - apply ectxi_language_mixin.
    - apply ectxi_language_mixin.
    - done.
    - intros K1 K2 e. by rewrite /fill /= foldl_app.
    - intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
    - done.
    - intros K K' e1 κ e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
      induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
      destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
      { rewrite fill_app in Hstep. apply base_ctx_step_val in Hstep.
        apply fill_val in Hstep. by apply not_eq_None_Some in Hstep. }
      rewrite !fill_app /= in Hfill.
      assert (Ki = Ki') as ->.
      { eapply fill_item_no_val_inj, Hfill; eauto using val_base_stuck.
        apply fill_not_val. revert Hstep. apply ectxi_language_mixin. }
      simplify_eq. destruct (IH K') as [K'' ->]; auto.
      exists K''. by rewrite assoc.
    - intros K e1 σ1 κ e2 σ2 efs.
      destruct K as [|Ki K _] using rev_ind; simpl; first by auto.
      rewrite fill_app /=.
      intros ?%base_ctx_step_val; eauto using fill_val.
  Qed.
  Canon
...

Lemma fill_not_valK e : to_val e = None → to_val (fill K e) = None.
  Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.

Lemma ectxi_language_sub_redexes_are_valuese :
    (∀ Ki e', e = fill_item Ki e' → is_Some (to_val e')) →
    sub_redexes_are_values e.
  Proof.
    intros Hsub K e' ->. destruct K as [|Ki K _] using @rev_ind=> //=.
    intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
  Qed.

Global Instanceectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
  Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.

Global Argumentsectxi_lang_ectx : clear implicits.

Global Argumentsectxi_lang : clear implicits.

Coercion ectxi_lang_ectx: ectxiLanguage >-> ectxLanguage.

Coercion ectxi_lang: ectxiLanguage >-> language.

Definition EctxLanguageOfEctxi(Λ : ectxiLanguage) : ectxLanguage :=
  let '@EctxiLanguage E V C St K of_val to_val fill base mix := Λ in
  @EctxLanguage E V (list C) St K of_val to_val _ _ _ _
    (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill base mix)).

Global ArgumentsEctxLanguageOfEctxi : simpl never.