(* iris/program_logic/language.v *)
From iris.algebra Require Export ofe
From iris.bi Require Export weakestpre
From iris.prelude Require Import options

Record LanguageMixin:= {
    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 e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None
  }.

Structure language:= Language {
  expr : Type;
  val : Type;
  state : Type;
  observation : Type;
  of_val : val → expr;
  to_val : expr → option val;
  prim_step : expr → state → list observation → expr → state → list expr → Prop;
  language_mixin : LanguageMixin of_val to_val prim_step
}.
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.

Global ArgumentsLanguage {_ _ _ _ _ _ _} _.

Global Argumentsof_val {_} _.

Global Argumentsto_val {_} _.

Global Argumentsprim_step {_} _ _ _ _ _ _.
Canonical Structure stateO Λ := leibnizO (state Λ).
Canonical Structure valO Λ := leibnizO (val Λ).
Canonical Structure exprO Λ := leibnizO (expr Λ).

Definition cfg(Λ : language) := (list (expr Λ) * state Λ)%type.

Class LanguageCtx{Λ : language} (K : expr Λ → expr Λ) := {
  fill_not_val e :
    to_val e = None → to_val (K e) = None;
  fill_step e1 σ1 κ e2 σ2 efs :
    prim_step e1 σ1 κ e2 σ2 efs →
    prim_step (K e1) σ1 κ (K e2) σ2 efs;
  fill_step_inv e1' σ1 κ e2 σ2 efs :
    to_val e1' = None → prim_step (K e1') σ1 κ e2 σ2 efs →
    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
}.

Global Instancelanguage_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Proof. constructor; naive_solver. Qed.

Inductive atomicity:= StronglyAtomic | WeaklyAtomic.

Definition stuckness_to_atomicity(s : stuckness) : atomicity :=
  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.

Lemma to_of_valv : to_val (of_val v) = Some v.
  Proof. apply language_mixin. Qed.

Lemma of_to_vale v : to_val e = Some v → of_val v = e.
  Proof. apply language_mixin. Qed.

Lemma val_stucke σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None.
  Proof. apply language_mixin. Qed.

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

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

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

Definition stuck(e : expr Λ) (σ : state Λ) :=
    to_val e = None ∧ irreducible e σ.

Definition not_stuck(e : expr Λ) (σ : state Λ) :=
    is_Some (to_val e) ∨ reducible e σ.

Class Atomic(a : atomicity) (e : expr Λ) : Prop :=
    atomic σ e' κ σ' efs :
      prim_step e σ κ e' σ' efs →
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').

Inductive step(ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop :=
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
       ρ1 = (t1 ++ e1 :: t2, σ1) →
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
       prim_step e1 σ1 κ e2 σ2 efs →
       step ρ1 κ ρ2.

Local HintConstructors step : core.

Inductive nsteps: nat → cfg Λ → list (observation Λ) → cfg Λ → Prop :=
    | nsteps_refl ρ :
       nsteps 0 ρ [] ρ
    | nsteps_l n ρ1 ρ2 ρ3 κ κs :
       step ρ1 κ ρ2 →
       nsteps n ρ2 κs ρ3 →
       nsteps (S n) ρ1 (κ ++ κs) ρ3.

Local HintConstructors nsteps : core.

Definition erased_step(ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.

Lemma erased_steps_nstepsρ1 ρ2 :
    rtc erased_step ρ1 ρ2 ↔ ∃ n κs, nsteps n ρ1 κs ρ2.
  Proof.
    split.
    - induction 1; firstorder eauto.
    - intros (n & κs & Hsteps). unfold erased_step.
      induction Hsteps; eauto using rtc_refl, rtc_l.
  Qed.

Lemma of_to_val_flipv e : of_val v = e → to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.

Lemma not_reduciblee σ : ¬reducible e σ ↔ irreducible e σ.
  Proof. unfold reducible, irreducible. naive_solver. Qed.

Lemma reducible_not_vale σ : reducible e σ → to_val e = None.
  Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.

Lemma reducible_no_obs_reduciblee σ : reducible_no_obs e σ → reducible e σ.
  Proof. intros (?&?&?&?); eexists; eauto. Qed.

Lemma val_irreduciblee σ : is_Some (to_val e) → irreducible e σ.
  Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.

Global Instanceof_val_inj : Inj (=) (=) (@of_val Λ).
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.

Lemma not_not_stucke σ : ¬not_stuck e σ ↔ stuck e σ.
  Proof.
    rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible.
    destruct (decide (to_val e = None)); naive_solver.
  Qed.

Lemma strongly_atomic_atomice a :
    Atomic StronglyAtomic e → Atomic a e.
  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.

Lemma reducible_fill`{!@LanguageCtx Λ K} e σ :
    reducible e σ → reducible (K e) σ.
  Proof. unfold reducible in *. naive_solver eauto using fill_step. Qed.

Lemma reducible_fill_inv`{!@LanguageCtx Λ K} e σ :
    to_val e = None → reducible (K e) σ → reducible e σ.
  Proof.
    intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.

Lemma reducible_no_obs_fill`{!@LanguageCtx Λ K} e σ :
    reducible_no_obs e σ → reducible_no_obs (K e) σ.
  Proof. unfold reducible_no_obs in *. naive_solver eauto using fill_step. Qed.

Lemma reducible_no_obs_fill_inv`{!@LanguageCtx Λ K} e σ :
    to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ.
  Proof.
    intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.

Lemma irreducible_fill`{!@LanguageCtx Λ K} e σ :
    to_val e = None → irreducible e σ → irreducible (K e) σ.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill_inv. Qed.

Lemma irreducible_fill_inv`{!@LanguageCtx Λ K} e σ :
    irreducible (K e) σ → irreducible e σ.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.

Lemma not_stuck_fill_invK `{!@LanguageCtx Λ K} e σ :
    not_stuck (K e) σ → not_stuck e σ.
  Proof.
    rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
    - auto using fill_not_val.
    - destruct (decide (to_val e = None)); eauto using reducible_fill_inv.
  Qed.

Lemma stuck_fill`{!@LanguageCtx Λ K} e σ :
    stuck e σ → stuck (K e) σ.
  Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill_inv. Qed.

Lemma step_Permutation(t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
    t1 ≡ₚ t1' → step (t1,σ1) κ (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) κ (t2',σ2).
  Proof.
    intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
    move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
    intros (tl'&tr'&->&Ht)%Permutation_cons_inv_r.
    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
    by rewrite -!Permutation_middle !assoc_L Ht.
  Qed.

Lemma step_inserti t2 σ2 e κ e' σ3 efs :
    t2 !! i = Some e →
    prim_step e σ2 κ e' σ3 efs →
    step (t2, σ2) κ (<[i:=e']>t2 ++ efs, σ3).
  Proof.
    intros.
    edestruct (list_elem_of_split_length t2) as (t21&t22&?&?);
      first (by eauto using list_elem_of_lookup_2); simplify_eq.
    econstructor; eauto.
    by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
  Qed.

Lemma erased_step_Permutation(t1 t1' t2 : list (expr Λ)) σ1 σ2 :
    t1 ≡ₚ t1' → erased_step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ erased_step (t1',σ1) (t2',σ2).
  Proof.
    intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.

Record pure_step(e1 e2 : expr Λ) := {
    pure_step_safe σ1 : reducible_no_obs e1 σ1;
    pure_step_det σ1 κ e2' σ2 efs :
      prim_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []
  }.

Notation pure_steps_tp:= (Forall2 (rtc pure_step)).

Class PureExec(φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
    pure_exec : φ → relations.nsteps pure_step n e1 e2.

Lemma pure_step_ctxK `{!@LanguageCtx Λ K} e1 e2 :
    pure_step e1 e2 →
    pure_step (K e1) (K e2).
  Proof.
    intros [Hred Hstep]. split.
    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
    - intros σ1 κ e2' σ2 efs Hpstep.
      destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
      + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
  Qed.

Lemma pure_step_nsteps_ctxK `{!@LanguageCtx Λ K} n e1 e2 :
    relations.nsteps pure_step n e1 e2 →
    relations.nsteps pure_step n (K e1) (K e2).
  Proof. eauto using nsteps_congruence, pure_step_ctx. Qed.

Lemma rtc_pure_step_ctxK `{!@LanguageCtx Λ K} e1 e2 :
    rtc pure_step e1 e2 → rtc pure_step (K e1) (K e2).
  Proof. eauto using rtc_congruence, pure_step_ctx. Qed.

Lemma pure_exec_ctxK `{!@LanguageCtx Λ K} φ n e1 e2 :
    PureExec φ n e1 e2 →
    PureExec φ n (K e1) (K e2).
  Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.

Class IntoVal(e : expr Λ) (v : val Λ) :=
    into_val : of_val v = e.

Class AsVal(e : expr Λ) := as_val : ∃ v, of_val v = e.

Global Instanceas_vals_of_val vs : TCForall AsVal (of_val <$> vs).
  Proof.
    apply TCForall_Forall, Forall_fmap, Forall_true=> v.
    rewrite /AsVal /=; eauto.
  Qed.

Lemma as_val_is_Somee :
    (∃ v, of_val v = e) → is_Some (to_val e).
  Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.

Lemma prim_step_not_stucke σ κ e' σ' efs :
    prim_step e σ κ e' σ' efs → not_stuck e σ.
  Proof. rewrite /not_stuck /reducible. eauto 10. Qed.

Lemma rtc_pure_step_val`{!Inhabited (state Λ)} v e :
    rtc pure_step (of_val v) e → to_val e = Some v.
  Proof.
    intros ?; rewrite <- to_of_val.
    f_equal; symmetry; eapply rtc_nf; first done.
    intros [e' [Hstep _]].
    destruct (Hstep inhabitant) as (?&?&?&Hval%val_stuck).
    by rewrite to_of_val in Hval.
  Qed.

Lemma erased_step_pure_step_tpt1 σ1 t2 σ2 t3 :
    erased_step (t1, σ1) (t2, σ2) →
    pure_steps_tp t1 t3 →
    (σ1 = σ2 ∧ pure_steps_tp t2 t3) ∨
    (∃ i e efs e' κ,
      t1 !! i = Some e ∧ t3 !! i = Some e ∧
      t2 = <[i:=e']>t1 ++ efs ∧
      prim_step e σ1 κ e' σ2 efs).
  Proof.
    intros [κ [e σ e' σ' efs t11 t12 ?? Hstep]] Hps; simplify_eq/=.
    apply Forall2_app_inv_l in Hps
      as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
    destruct Hps as [e|e1 e2 e3 [_ Hprs]].
    - right.
      exists (length t11), e, efs, e', κ; split_and!; last done.
      + by rewrite lookup_app_r // Nat.sub_diag.
      + apply Forall2_length in Hpsteps.
        by rewrite lookup_app_r Hpsteps // Nat.sub_diag.
      + by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
    - edestruct Hprs as (?&?&?&?); first done; simplify_eq.
      left; split; first done.
      rewrite right_id_L.
      eauto using Forall2_app.
  Qed.

Global HintMode PureExec + - - ! - : typeclass_instances.

Global Argumentsstep_atomic {Λ ρ1 κ ρ2}.

Notation pure_steps_tp:= (Forall2 (rtc pure_step)).