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

Record EctxLanguageMixin:= {
    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_base_stuck e1 σ1 κ e2 σ2 efs :
      base_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
    mixin_fill_empty e : fill empty_ectx e = e;
    mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
    mixin_fill_inj K : Inj (=) (=) (fill K);
    mixin_fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e);

Structure ectxLanguage:= EctxLanguage {
  expr : Type;
  val : Type;
  ectx : Type;
  state : Type;
  observation : Type;
  of_val : val → expr;
  to_val : expr → option val;
  empty_ectx : ectx;
  comp_ectx : ectx → ectx → ectx;
  fill : ectx → expr → expr;
  base_step : expr → state → list observation → expr → state → list expr → Prop;
  ectx_language_mixin :
    EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill base_step
}.
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.

Global ArgumentsEctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.

Global Argumentsof_val {_} _.

Global Argumentsto_val {_} _.

Global Argumentsempty_ectx {_}.

Global Argumentscomp_ectx {_} _ _.

Global Argumentsfill {_} _ _.

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

Lemma val_base_stucke1 σ1 κ e2 σ2 efs : base_step e1 σ1 κ e2 σ2 efs → to_val e1 = None.
  Proof. apply ectx_language_mixin. Qed.

Lemma fill_emptye : fill empty_ectx e = e.
  Proof. apply ectx_language_mixin. Qed.

Lemma fill_compK1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
  Proof. apply ectx_language_mixin. Qed.

Global Instancefill_inj K : Inj (=) (=) (fill K).
  Proof. apply ectx_language_mixin. Qed.

Lemma fill_valK e : is_Some (to_val (fill K e)) → is_Some (to_val e).
  Proof. apply ectx_language_mixin. Qed.

Lemma step_by_valK' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
    fill K' e1' = fill K_redex e1_redex →
    to_val e1' = None →
    base_step e1_redex σ1 κ e2 σ2 efs →
    ∃ K'', K_redex = comp_ectx K' K''.
  Proof. apply ectx_language_mixin. Qed.

Lemma base_ctx_step_valK e σ1 κ e2 σ2 efs :
    base_step (fill K e) σ1 κ e2 σ2 efs → is_Some (to_val e) ∨ K = empty_ectx.
  Proof. apply ectx_language_mixin. Qed.

Definition base_reducible(e : expr Λ) (σ : state Λ) :=
    ∃ κ e' σ' efs, base_step e σ κ e' σ' efs.

Definition base_reducible_no_obs(e : expr Λ) (σ : state Λ) :=
    ∃ e' σ' efs, base_step e σ [] e' σ' efs.

Definition base_irreducible(e : expr Λ) (σ : state Λ) :=
    ∀ κ e' σ' efs, ¬base_step e σ κ e' σ' efs.

Definition base_stuck(e : expr Λ) (σ : state Λ) :=
    to_val e = None ∧ base_irreducible e σ.

Definition sub_redexes_are_values(e : expr Λ) :=
    ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.

Inductive prim_step(e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
      (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
    Ectx_step K e1' e2' :
      e1 = fill K e1' → e2 = fill K e2' →
      base_step e1' σ1 κ e2' σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.

Lemma Ectx_step'K e1 σ1 κ e2 σ2 efs :
    base_step e1 σ1 κ e2 σ2 efs → prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
  Proof. econstructor; eauto. Qed.

Definition ectx_lang_mixin: LanguageMixin of_val to_val prim_step.
  Proof.
    split.
    - apply ectx_language_mixin.
    - apply ectx_language_mixin.
    - intros ?????? [??? -> -> ?%val_base_stuck].
      apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
  Qed.
  Canonical Structure ectx_lang : language := Language ectx_lang_mixin.

Definition base_atomic(a : atomicity) (e : expr Λ) : Prop :=
    ∀ σ κ e' σ' efs,
      base_step e σ κ e' σ' efs →
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').

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 base_reducible_no_obs_reduciblee σ :
    base_reducible_no_obs e σ → base_reducible e σ.
  Proof. intros (?&?&?&?). eexists. eauto. Qed.

Lemma not_base_reduciblee σ : ¬base_reducible e σ ↔ base_irreducible e σ.
  Proof. unfold base_reducible, base_irreducible. naive_solver. Qed.

Lemma base_redex_uniqueK K' e e' σ :
    fill K e = fill K' e' →
    base_reducible e σ →
    base_reducible e' σ →
    K = comp_ectx K' empty_ectx ∧ e = e'.
  Proof.
    intros Heq (κ & e2 & σ2 & efs & Hred) (κ' & e2' & σ2' & efs' & Hred').
    edestruct (step_by_val K' K e' e) as [K'' HK];
      [by eauto using val_base_stuck..|].
    subst K. move: Heq. rewrite -fill_comp. intros <-%(inj (fill _)).
    destruct (base_ctx_step_val _ _ _ _ _ _ _ Hred') as [[]%not_eq_None_Some|HK''].
    { by eapply val_base_stuck. }
    subst K''. rewrite fill_empty. done.
  Qed.

Lemma base_prim_stepe1 σ1 κ e2 σ2 efs :
    base_step e1 σ1 κ e2 σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
  Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.

Lemma base_step_not_stucke σ κ e' σ' efs : base_step e σ κ e' σ' efs → not_stuck e σ.
  Proof. rewrite /not_stuck /reducible /=. eauto 10 using base_prim_step. Qed.

Lemma fill_prim_stepK e1 σ1 κ e2 σ2 efs :
    prim_step e1 σ1 κ e2 σ2 efs → prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
  Proof.
    destruct 1 as [K' e1' e2' -> ->].
    rewrite !fill_comp. by econstructor.
  Qed.

Lemma fill_reducibleK e σ : reducible e σ → reducible (fill K e) σ.
  Proof.
    intros (κ&e'&σ'&efs&?). exists κ, (fill K e'), σ', efs.
    by apply fill_prim_step.
  Qed.

Lemma fill_reducible_no_obsK e σ : reducible_no_obs e σ → reducible_no_obs (fill K e) σ.
  Proof.
    intros (e'&σ'&efs&?). exists (fill K e'), σ', efs.
    by apply fill_prim_step.
  Qed.

Lemma base_prim_reduciblee σ : base_reducible e σ → reducible e σ.
  Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply base_prim_step. Qed.

Lemma base_prim_fill_reduciblee K σ :
    base_reducible e σ → reducible (fill K e) σ.
  Proof. intro. by apply fill_reducible, base_prim_reducible. Qed.

Lemma base_prim_reducible_no_obse σ : base_reducible_no_obs e σ → reducible_no_obs e σ.
  Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply base_prim_step. Qed.

Lemma base_prim_irreduciblee σ : irreducible e σ → base_irreducible e σ.
  Proof.
    rewrite -not_reducible -not_base_reducible. eauto using base_prim_reducible.
  Qed.

Lemma base_prim_fill_reducible_no_obse K σ :
    base_reducible_no_obs e σ → reducible_no_obs (fill K e) σ.
  Proof. intro. by apply fill_reducible_no_obs, base_prim_reducible_no_obs. Qed.

Lemma prim_base_reduciblee σ :
    reducible e σ → sub_redexes_are_values e → base_reducible e σ.
  Proof.
    intros (κ&e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
    assert (K = empty_ectx) as -> by eauto 10 using val_base_stuck.
    rewrite fill_empty /base_reducible; eauto.
  Qed.

Lemma prim_base_irreduciblee σ :
    base_irreducible e σ → sub_redexes_are_values e → irreducible e σ.
  Proof.
    rewrite -not_reducible -not_base_reducible. eauto using prim_base_reducible.
  Qed.

Lemma base_stuck_stucke σ :
    base_stuck e σ → sub_redexes_are_values e → stuck e σ.
  Proof.
    intros [] ?. split; first done.
    by apply prim_base_irreducible.
  Qed.

Lemma ectx_language_atomica e :
    base_atomic a e → sub_redexes_are_values e → Atomic a e.
  Proof.
    intros Hatomic_step Hatomic_fill σ κ e' σ' efs [K e1' e2' -> -> Hstep].
    assert (K = empty_ectx) as -> by eauto 10 using val_base_stuck.
    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
  Qed.

Lemma base_reducible_prim_step_ctxK e1 σ1 κ e2 σ2 efs :
    base_reducible e1 σ1 →
    prim_step (fill K e1) σ1 κ e2 σ2 efs →
    ∃ e2', e2 = fill K e2' ∧ base_step e1 σ1 κ e2' σ2 efs.
  Proof.
    intros (κ'&e2''&σ2''&efs''&HhstepK) [K' e1' e2' HKe1 -> Hstep].
    edestruct (step_by_val K) as [K'' ?];
      eauto using val_base_stuck; simplify_eq/=.
    rewrite -fill_comp in HKe1; simplify_eq.
    exists (fill K'' e2'). rewrite fill_comp; split; first done.
    apply base_ctx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
    { apply val_base_stuck in Hstep; simplify_eq. }
    by rewrite !fill_empty.
  Qed.

Lemma base_reducible_prim_stepe1 σ1 κ e2 σ2 efs :
    base_reducible e1 σ1 →
    prim_step e1 σ1 κ e2 σ2 efs →
    base_step e1 σ1 κ e2 σ2 efs.
  Proof.
    intros.
    edestruct (base_reducible_prim_step_ctx empty_ectx) as (?&?&?);
      rewrite ?fill_empty; eauto.
    by simplify_eq; rewrite fill_empty.
  Qed.

Global Instanceectx_lang_ctx K : LanguageCtx (fill K).
  Proof.
    split; simpl.
    - eauto using fill_not_val.
    - intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
      by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
    - intros e1 σ1 κ e2 σ2 efs Hnval [K'' e1'' e2'' Heq1 -> Hstep].
      destruct (step_by_val K K'' e1 e1'' σ1 κ e2'' σ2 efs) as [K' ->]; eauto.
      rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
      exists (fill K' e2''); rewrite -fill_comp; split; auto.
      econstructor; eauto.
  Qed.

Record pure_base_step(e1 e2 : expr Λ) := {
    pure_base_step_safe σ1 : base_reducible_no_obs e1 σ1;
    pure_base_step_det σ1 κ e2' σ2 efs :
      base_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []
  }.

Lemma pure_base_step_pure_stepe1 e2 : pure_base_step e1 e2 → pure_step e1 e2.
  Proof.
    intros [Hp1 Hp2]. split.
    - intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
      eexists e2', σ2, efs. by apply base_prim_step.
    - intros σ1 κ e2' σ2 efs ?%base_reducible_prim_step; eauto using base_reducible_no_obs_reducible.
  Qed.

Lemma pure_exec_fillK φ n e1 e2 :
    PureExec φ n e1 e2 →
    PureExec φ n (fill K e1) (fill K e2).
  Proof. apply: pure_exec_ctx. Qed.

Global Argumentsectx_lang : clear implicits.

Global ArgumentsEctx_step {Λ e1 σ1 κ e2 σ2 efs}.

Coercion ectx_lang: ectxLanguage >-> language.

Definition LanguageOfEctx(Λ : ectxLanguage) : language :=
  let '@EctxLanguage E V C St K of_val to_val empty comp fill base mix := Λ in
  @Language E V St K of_val to_val _
    (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill base mix)).

Global ArgumentsLanguageOfEctx : simpl never.