From mininix Require Export nix.operational_props.
From stdpp Require Import options.

Definition wp (μ : mode) (e : expr) (Φ : expr → Prop) : Prop :=
  ∃ e', e -{μ}->* e' ∧ final μ e' ∧ Φ e'.

Lemma Lit_wp μ Φ bl :
  base_lit_ok bl →
  Φ (ELit bl) →
  wp μ (ELit bl) Φ.
Proof. exists (ELit bl). by repeat constructor. Qed.

Lemma Abs_wp μ Φ x e :
  Φ (EAbs x e) →
  wp μ (EAbs x e) Φ.
Proof. exists (EAbs x e). by repeat constructor. Qed.

Lemma AbsMatch_wp μ Φ ms strict e :
  Φ (EAbsMatch ms strict e) →
  wp μ (EAbsMatch ms strict e) Φ.
Proof. exists (EAbsMatch ms strict e). by repeat constructor. Qed.

Lemma LetAttr_no_recs_wp μ Φ k αs e :
  no_recs αs →
  wp μ (subst ((k,.) ∘ attr_expr <$> αs) e) Φ →
  wp μ (ELetAttr k (EAttr αs) e) Φ.
Proof.
  intros Hαs (e' & Hsteps & ? & HΦ). exists e'. split; [|done].
  etrans; [|apply Hsteps]. apply rtc_once. by constructor.
Qed.

Lemma BinOp_wp μ Φ op e1 e2 :
  wp SHALLOW e1 (λ e1', ∃ Φop,
    sem_bin_op op e1' Φop ∧ 
    wp SHALLOW e2 (λ e2', ∃ e', Φop e2' e' ∧ wp μ e' Φ)) →
  wp μ (EBinOp op e1 e2) Φ.
Proof.
  intros (e1' & Hsteps1 & ? & Φop & Hop1 & e2' & Hsteps2 & ?
          & e' & Hop2 & e'' & Hsteps & ? & HΦ).
  exists e''. split; [|done].
  etrans; [by apply SBinOpL_rtc|].
  etrans; [by eapply SBinOpR_rtc|].
  eapply rtc_l; [by econstructor|]. done.
Qed.

Lemma Id_wp μ Φ x k e :
  wp μ e Φ →
  wp μ (EId x (Some (k,e))) Φ.
Proof.
  intros (e' & Hsteps & ? & HΦ). exists e'. split; [|done].
  etrans; [|apply Hsteps]. apply rtc_once. constructor.
Qed.

Lemma App_wp μ Φ e1 e2 :
  wp SHALLOW e1 (λ e1', wp μ (EApp e1' e2) Φ) ↔
  wp μ (EApp e1 e2) Φ.
Proof.
  split.
  - intros (e1' & Hsteps1 & ? & e' & Hsteps2 & ? & HΦ).
    exists e'; split; [|done]. etrans; [|apply Hsteps2].
    by apply SAppL_rtc.
  - intros (e' & Hsteps & Hfinal & HΦ).
    cut (∃ e1', e1 -{SHALLOW}->* e1' ∧ final SHALLOW e1' ∧ EApp e1' e2 -{μ}->* e').
    { intros (e1'&?&?&?). exists e1'. split_and!; [done..|]. by exists e'. }
    clear Φ HΦ. apply rtc_nsteps in Hsteps as [n Hsteps].
    revert e1 Hsteps. induction n as [|n IH]; intros e1 Hsteps.
    { inv Hsteps. inv Hfinal. }
    inv Hsteps. inv H0.
    + eexists; split_and!; [done|by constructor|].
      eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
    + eexists; split_and!; [done|by constructor|].
      eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
    + eexists; split_and!; [done|by constructor|].
      eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
    + inv H2.
      * apply IH in H1 as (e'' & Hsteps & ? & ?).
        exists e''; split; [|done]. by eapply rtc_l.
      * eexists; split_and!; [done|by constructor|].
        eapply rtc_l; [by eapply SAppR|]. by eapply rtc_nsteps_2.
Qed.

Lemma Attr_wp_shallow Φ αs :
  Φ (EAttr (AttrN ∘ from_attr (subst (indirects αs)) id <$> αs)) →
  wp SHALLOW (EAttr αs) Φ.
Proof.
  eexists (EAttr (AttrN ∘ _ <$> αs)); split_and!; [ |by constructor|done].
  destruct (decide (no_recs αs)); [|apply rtc_once; by constructor].
  apply reflexive_eq; f_equal. apply map_eq=> x. rewrite lookup_fmap.
  destruct (αs !! x) as [[? e]|] eqn:?; f_equal/=.
  by assert (τ = NONREC) as -> by eauto using no_recs_lookup.
Qed.

Lemma β_wp μ Φ x e1 e2 :
  wp μ (subst {[x:=(ABS, e2)]} e1) Φ →
  wp μ (EApp (EAbs x e1) e2) Φ.
Proof.
  intros (e' & Hsteps & ? & ?). exists e'. split; [|done].
  eapply rtc_l; [|done]. by constructor.
Qed.

Lemma βMatch_wp μ Φ ms strict e1 αs βs :
  no_recs αs →
  matches (attr_expr <$> αs) ms strict βs →
  wp μ (subst (indirects βs) e1) Φ →
  wp μ (EApp (EAbsMatch ms strict e1) (EAttr αs)) Φ.
Proof.
  intros ?? (e' & Hsteps & ? & ?). exists e'. split; [|done].
  eapply rtc_l; [|done]. by constructor.
Qed.

Lemma Functor_wp μ Φ αs e1 e2 :
  no_recs αs →
  αs !! "__functor" = Some (AttrN e1) →
  wp μ (EApp (EApp e1 (EAttr αs)) e2) Φ →
  wp μ (EApp (EAttr αs) e2) Φ.
Proof.
  intros ?? (e' & Hsteps & ? & ?). exists e'. split; [|done].
  eapply rtc_l; [|done]. by constructor.
Qed.

Lemma If_wp μ Φ e1 e2 e3 :
  wp SHALLOW e1 (λ e1', ∃ b : bool,
    e1' = ELit (LitBool b) ∧ wp μ (if b then e2 else e3) Φ) →
  wp μ (EIf e1 e2 e3) Φ.
Proof.
  intros (e1' & Hsteps & ? & b & -> & e' & Hsteps' & ? & HΦ).
  exists e'; split; [|done]. etrans; [by apply SIf_rtc|].
  eapply rtc_l; [|done]. destruct b; constructor.
Qed.

Lemma wp_mono μ e Φ Ψ :
  wp μ e Φ →
  (∀ e', Φ e' → Ψ e') →
  wp μ e Ψ.
Proof. intros (e' & ? & ? & ?) ?. exists e'. naive_solver. Qed.

Lemma union_kinded_abs {A} mkv (v2 : A) :
  union_kinded (pair WITH <$> mkv) (Some (ABS, v2)) = Some (ABS, v2).
Proof. by destruct mkv. Qed.

Lemma union_kinded_with {A} (v : A) mkv2 :
  union_kinded (Some (WITH, v)) (pair WITH <$> mkv2) = Some (WITH, v).
Proof. by destruct mkv2. Qed.