Desugaring

Require Export Coq.Program.Equality.
Require Export Definitions Infrastructure.
Require Export Metalib.Metatheory.
Require Export Blame Safety.

Fixpoint typ_of_ityp C :=
  match C with
  | ityp_basetyp_null dtyp_base
  | ityp_arrow A Btyp_null (dtyp_arrow (typ_of_ityp A) (typ_of_ityp B))
  end.

Definition elvis L M := (t_case L M (t_var_b 0)).
Definition elvis_blame L p := elvis L (t_blame (label_name p)).

Definition blame_label_op := 0.
Definition blame_label_deref := 1.
Definition blame_label_ei := 2.
Definition blame_label_ie := 3.

Fixpoint trm_of_itrm N :=
  match N with
  | itrm_var_b nt_var_b n
  | itrm_var_f xt_var_f x
  | itrm_const ct_lift (t_const c)
  | itrm_binop M Nt_lift (t_binop
      (elvis_blame (trm_of_itrm M) blame_label_op)
      (elvis_blame (trm_of_itrm N) blame_label_op))
  | itrm_abs A Nt_lift (t_abs (typ_of_ityp A) (trm_of_itrm N))
  | itrm_app L Mt_app
      (elvis_blame (trm_of_itrm L) blame_label_deref)
      (trm_of_itrm M)
  | itrm_nullt_null
  end.

Definition ictx := list ( atom × ityp ).

Definition ctx_of_ictx (G:ictx) : ctx := map typ_of_ityp G.

Lemma ctx_of_ictx_binds_ityp:
   (G:ictx) x (A:ityp),
  binds x A G
  binds x (typ_of_ityp A) (ctx_of_ictx G).
Proof.
  intros.
  eapply binds_map_2; eauto.
Qed.

Lemma uniq_ctx:
   G,
  uniq G
  uniq (ctx_of_ictx G).
Proof.
  intros.
  eapply uniq_map_2; eauto.
Qed.

Lemma open_trm_of_itrm :
   N M k,
  trm_of_itrm (open_itrm_wrt_itrm_rec k M N) =
  open_trm_wrt_trm_rec k (trm_of_itrm M) (trm_of_itrm N).
Proof.
  intros.
  dependent induction N; default_simp.
  - unfold elvis_blame, elvis. f_equal. eauto.
  - unfold elvis_blame, elvis. f_equal. eauto.
  - unfold elvis_blame, elvis. f_equal. eauto.
Qed.

Hint Resolve ctx_of_ictx_binds_ityp uniq_ctx : core.

Lemma open_trm_of_itrm_rec_var :
   N x k,
  trm_of_itrm (open_itrm_wrt_itrm_rec k (itrm_var_f x) N) =
  open_trm_wrt_trm_rec k (t_var_f x) (trm_of_itrm N).
Proof.
  intros.
  assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
  eapply open_trm_of_itrm.
Qed.

Lemma open_trm_of_itrm_var:
   N x,
  trm_of_itrm (open_itrm_wrt_itrm N (itrm_var_f x)) =
  open_trm_wrt_trm (trm_of_itrm N) (t_var_f x).
Proof.
  intros. eapply open_trm_of_itrm_rec_var.
Qed.

Lemma desugaring_typing:
   iG iN iA,
    ityping iG iN iA
    typing (ctx_of_ictx iG) (trm_of_itrm iN) (typ_of_ityp iA).
Proof.
  intros.
  induction H; intros; pose (ctx_of_ictx iG) as G'; default_simp; eauto.
  - constructor.
    constructor;
      unfold elvis_blame, elvis;
      pick fresh x and apply typing_case; eauto;
      constructor; try eapply uniq_cons_3; eauto.
  - constructor.
    pick fresh x and apply typing_abs; eauto.
    rewrite <- open_trm_of_itrm_var.
    eapply H0; eauto.
  - eapply typing_app; eauto.
    unfold elvis_blame, elvis.
    pick fresh x and apply typing_case; eauto.
    constructor;
    try eapply uniq_cons_3; eauto.
  - induction iA; default_simp; eauto.
Qed.

Lemma blame_eq_dec:
   (p q:label),
  p = q p q.
Proof.
  intros.
  destruct p; destruct q;
  destruct (eq_nat_dec bl bl0); eauto; right;
  inversion 1; auto.
Qed.

Lemma close_pres_safe:
   N x k p,
  safe (open_trm_wrt_trm_rec k (t_var_f x) N) p
  safe N p.
Proof.
  intros.
  dependent induction N; eauto; inversion H; subst; eauto.
Qed.

Hint Resolve close_pres_safe : core.

Fixpoint typ_of_ityp_naive A :=
  match A with
  | ityp_basetyp_def dtyp_base
  | ityp_arrow B Ctyp_def (dtyp_arrow (typ_of_ityp_naive B) (typ_of_ityp_naive C))
  end.

Lemma imp_naive_subtyp A :
  subtyp_n (typ_of_ityp_naive A) (typ_of_ityp A).
Proof.
  induction A; simpl; eauto.
Qed.

Fixpoint ityp_of_typ A : ityp :=
  match A with
  | typ_null dtyp_baseityp_base
  | typ_null (dtyp_arrow A B) ⇒ ityp_arrow (ityp_of_typ A) (ityp_of_typ B)
  | typ_def dtyp_baseityp_base
  | typ_def (dtyp_arrow A B) ⇒ ityp_arrow (ityp_of_typ A) (ityp_of_typ B)
  end.

Lemma exp_naive_subtyp :
  ( A, subtyp_n A (typ_of_ityp (ityp_of_typ A)))
  ( D, subtyp_n (typ_def D) (typ_of_ityp (ityp_of_typ (typ_def D)))
             subtyp_n (typ_null D) (typ_of_ityp (ityp_of_typ (typ_null D))))
.
Proof.
  apply_mutual_ind typ_dtyp_mutind; default_simp.
Qed.

Lemma compat_naive_subtyp A B :
  subtyp_n A B compat A B.
Proof.
  induction 1; eauto.
Qed.

Lemma compat_typ_ityp A:
    compat A (typ_of_ityp (ityp_of_typ A)).
Proof.
  apply compat_naive_subtyp. apply exp_naive_subtyp.
Qed.

Definition ctrm_elvis_blame CL p := (ctrm_case_scrutinee CL (t_blame (label_name p)) (t_var_b 0)).

Fixpoint ctrm_of_ictrm iC :=
  match iC with
  | ictrm_holectrm_hole
  | ictrm_binop_left iC Nctrm_lift (ctrm_binop_left
      (ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_op)
      (elvis_blame (trm_of_itrm N) blame_label_op))
  | ictrm_binop_right N iCctrm_lift (ctrm_binop_right
      (elvis_blame (trm_of_itrm N) blame_label_op)
      (ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_op))
  | ictrm_abs A iCctrm_lift (ctrm_abs (typ_of_ityp A) (ctrm_of_ictrm iC))
  | ictrm_app_left iC Nctrm_app_left
      (ctrm_elvis_blame (ctrm_of_ictrm iC) blame_label_deref)
      (trm_of_itrm N)
  | ictrm_app_right N iCctrm_app_right
      (elvis_blame (trm_of_itrm N) blame_label_deref)
      (ctrm_of_ictrm iC)
  end.

Lemma open_ctrm_of_ictrm :
   N M k,
  ctrm_of_ictrm (open_ictrm_wrt_itrm_rec k M N) =
  open_ctrm_wrt_trm_rec k (trm_of_itrm M) (ctrm_of_ictrm N).
Proof.
  intros.
  dependent induction N; default_simp;
  unfold ctrm_elvis_blame, elvis_blame, elvis;
  try f_equal; eauto; eapply open_trm_of_itrm.
Qed.

Lemma open_ctrm_of_itrm_rec_var :
   N x k,
  ctrm_of_ictrm (open_ictrm_wrt_itrm_rec k (itrm_var_f x) N) =
  open_ctrm_wrt_trm_rec k (t_var_f x) (ctrm_of_ictrm N).
Proof.
  intros.
  assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
  eapply open_ctrm_of_ictrm.
Qed.

Lemma open_ctrm_of_itrm_var:
   N x,
  ctrm_of_ictrm (open_ictrm_wrt_itrm N (itrm_var_f x)) =
  open_ctrm_wrt_trm (ctrm_of_ictrm N) (t_var_f x).
Proof.
  intros. eapply open_ctrm_of_itrm_rec_var.
Qed.

Ltac desugar_ityping :=
      match goal with
      | [ H : ityping _ _ _ |- _ ] ⇒
        pose proof (desugaring_typing _ _ _ H) end.

Lemma ictrm_desugaring_typing:
   iG' iA' iG iCN iA,
    ictyping iG' iA' iG iCN iA
    ctyping (ctx_of_ictx iG') (typ_of_ityp iA') (ctx_of_ictx iG) (ctrm_of_ictrm iCN) (typ_of_ityp iA).
Proof.
  intros.
  dependent induction H; intros; pose (ctx_of_ictx iG) as G'; default_simp; try desugar_ityping; eauto.
  - constructor. apply ctyping_binop_left.
    + pick fresh x and apply ctyping_case_scrutinee; eauto;
      constructor; try eapply uniq_cons_3; eauto.
    + pick fresh x and apply typing_case; eauto;
      constructor; try eapply uniq_cons_3; eauto.
  - constructor. apply ctyping_binop_right.
    + pick fresh x and apply typing_case; eauto;
      constructor; try eapply uniq_cons_3; eauto.
    + pick fresh x and apply ctyping_case_scrutinee; eauto;
      constructor; try eapply uniq_cons_3; eauto.
  - constructor.
    pick fresh x and apply ctyping_abs; eauto.
    assert (t_var_f x = trm_of_itrm (itrm_var_f x)) by eauto.
    rewrite <- open_ctrm_of_itrm_var.
    eapply H0; eauto.
  - eapply ctyping_app_left; eauto.
    pick fresh x and apply ctyping_case_scrutinee; eauto;
    constructor; try eapply uniq_cons_3; eauto.
  - eapply ctyping_app_right; eauto.
    pick fresh x and apply typing_case; eauto;
    constructor; try eapply uniq_cons_3; eauto.
Qed.

Inductive plug_ctrm : ctrm trm trm Prop :=
  | plug_ctrm_hole M : plug_ctrm ctrm_hole M M
  | plug_ctrm_binop_left CM M' M N : plug_ctrm CM M' M plug_ctrm (ctrm_binop_left CM N) M' (t_binop M N)
  | plug_ctrm_binop_right CN M N' N : plug_ctrm CN N' N plug_ctrm (ctrm_binop_right M CN) N' (t_binop M N)
  | plug_ctrm_abs L CM A M' M :
      ( x , x \notin L
        plug_ctrm
          (open_ctrm_wrt_trm CM (t_var_f x))
          (open_trm_wrt_trm M' (t_var_f x))
          (open_trm_wrt_trm M (t_var_f x)))
      plug_ctrm (ctrm_abs A CM) M' (t_abs A M)
  | plug_ctrm_app_left CM M' M N : plug_ctrm CM M' M plug_ctrm (ctrm_app_left CM N) M' (t_app M N)
  | plug_ctrm_app_right CN M N' N : plug_ctrm CN N' N plug_ctrm (ctrm_app_right M CN) N' (t_app M N)
  | plug_ctrm_lift CM M' M : plug_ctrm CM M' M plug_ctrm (ctrm_lift CM) M' (t_lift M)
  | plug_ctrm_case_scrutinee CL L' L M N : plug_ctrm CL L' L plug_ctrm (ctrm_case_scrutinee CL M N) L' (t_case L M N)
  | plug_ctrm_case_null CM L M' M N : plug_ctrm CM M' M plug_ctrm (ctrm_case_null L CM N) M' (t_case L M N)
  | plug_ctrm_case_nonnull L CN LL M N' N :
      ( x , x \notin L
        plug_ctrm
          (open_ctrm_wrt_trm CN (t_var_f x))
          (open_trm_wrt_trm N' (t_var_f x))
          (open_trm_wrt_trm N (t_var_f x)))
      plug_ctrm (ctrm_case_nonnull LL M CN) N' (t_case LL M N)
  | plug_ctrm_cast CM M' M A B p : plug_ctrm CM M' M plug_ctrm (ctrm_cast CM A B p) M' (t_cast M A B p).

Lemma typing_plugged:
   G' A' G C A,
    ctyping G' A' G C A
   M',
    typing G' M' A'
   M,
    plug_ctrm C M' M
    typing G M A.
Proof.
  intros × CTyp.
  dependent induction CTyp; intros × Typ × PG; inversion PG; subst; eauto.
  - pick fresh x and apply typing_abs; eauto.
    assert (open_trm_wrt_trm M' (t_var_f x) = M') by eauto with lngen.
    eapply H0; eauto.
    rewrite <- H1.
    eapply H5. eauto.
  - pick fresh x and apply typing_case; eauto.
    assert (open_trm_wrt_trm M' (t_var_f x) = M') by eauto with lngen.
    eapply H2; eauto.
    rewrite <- H3.
    eapply H8. eauto.
Qed.

Lemma nest_trm_in_ictx:
   iG' M' A' iG iC iA M,
    ictyping iG' (ityp_of_typ A') iG iC iA
    typing (ctx_of_ictx iG') M' A'
    plug_ctrm (ctrm_of_ictrm iC)
      (M' A' (typ_of_ityp (ityp_of_typ A')) @@ (label_name blame_label_ei))
      M
    typing
      (ctx_of_ictx iG)
      M
      (typ_of_ityp iA).
Proof.
  intros.
  apply typing_plugged with
    (G':=(ctx_of_ictx iG'))
    (A':=(typ_of_ityp (ityp_of_typ A')))
    (C:=(ctrm_of_ictrm iC))
    (M':=(M' A' (typ_of_ityp (ityp_of_typ A')) @@ (label_name blame_label_ei)))
    ; eauto.
  - apply ictrm_desugaring_typing; eauto.
  - apply typing_cast; eauto.
    apply compat_typ_ityp; eauto.
Qed.

Inductive plug_ictrm : ictrm itrm itrm Prop :=
  | plug_ictrm_hole M : plug_ictrm ictrm_hole M M
  | plug_ictrm_binop_left CM M' M N : plug_ictrm CM M' M plug_ictrm (ictrm_binop_left CM N) M' (itrm_binop M N)
  | plug_ictrm_binop_right CN M N' N : plug_ictrm CN N' N plug_ictrm (ictrm_binop_right M CN) N' (itrm_binop M N)
  | plug_ictrm_abs L CM A M' M :
      ( x , x \notin L
        plug_ictrm
          (open_ictrm_wrt_itrm CM (itrm_var_f x))
          (open_itrm_wrt_itrm M' (itrm_var_f x))
          (open_itrm_wrt_itrm M (itrm_var_f x)))
      plug_ictrm (ictrm_abs A CM) M' (itrm_abs A M)
  | plug_ictrm_app_left CM M' M N : plug_ictrm CM M' M plug_ictrm (ictrm_app_left CM N) M' (itrm_app M N)
  | plug_ictrm_app_right CN M N' N : plug_ictrm CN N' N plug_ictrm (ictrm_app_right M CN) N' (itrm_app M N).

Lemma ityping_to_lc_itrm : G N A,
  ityping G N A lc_itrm N.
Proof.
  intros G N A H. induction H; eauto.
Qed.

Hint Resolve ityping_to_lc_itrm : core.

Lemma ityping_plugged:
   G' A' G C A,
    ictyping G' A' G C A
   M',
    ityping G' M' A'
   M,
    plug_ictrm C M' M
    ityping G M A.
Proof.
  intros × CTyp.
  dependent induction CTyp; intros × Typ × PG; inversion PG; subst; eauto.
  - pick fresh x and apply ityping_abs; eauto.
    assert (open_itrm_wrt_itrm M' (itrm_var_f x) = M') by eauto with lngen.
    eapply H0; eauto.
    rewrite <- H1.
    eapply H5. eauto.
Qed.

Definition ictx_of_ctx (G:ctx) : ictx := map ityp_of_typ G.

Lemma nest_itrm_in_ctx:
   G' iM' iA' G C A M,
    ctyping (ctx_of_ictx (ictx_of_ctx G')) (typ_of_ityp_naive iA') G C A
    ityping (ictx_of_ctx G') iM' iA'
    plug_ctrm C
      ((trm_of_itrm iM') (typ_of_ityp iA') (typ_of_ityp_naive iA') @@ (label_name blame_label_ie))
      M
    typing G M A.
Proof.
  intros.
  eapply typing_plugged; eauto.
  desugar_ityping.
  apply typing_cast; eauto.
  apply compat_sym. apply compat_naive_subtyp. apply imp_naive_subtyp.
Qed.