Inductive barrier := Hide | Show.

Definition sel (b : barrier) (p d : bool) :=
  match b with Show => p | Hide => d end.

Inductive expr : Type :=
| EVar (h : var)
| ETApp (e : expr) (s : term)
| EApp (e d : expr)
| ETLam (e : {bind term in expr})
| ELam (e : {bind expr}) (ρ : type)
| EBar (I : barrier) (e : expr)
| EDef (e : {bind expr}) (I : barrier) (π : type) (d : {bind expr}).
(* EDef e I π d is e / I h π = d
   where π is an annotation
   and d must be of the form ELam (… (ELam d' U) …) V
   with π = Arr V (… (Arr U Void)). *)

Global Instance HSubst_term_expr : HSubst term expr. derive. Defined.
Global Instance Ids_expr : Ids expr. derive. Defined.
Global Instance Rename_expr : Rename expr. derive. Defined.
Global Instance Subst_expr : Subst expr. derive. Defined.

Global Instance HSubstLemmas_term_expr : HSubstLemmas term expr. derive. Qed.
Global Instance SubstHSubstComp_term_expr : SubstHSubstComp term expr. derive. Qed.
Global Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.

Declare Scope coma_scope.
Delimit Scope coma_scope with coma.

Reserved Notation "[ Γ ⊩ e :- π ]" (format "[ Γ ⊩ e :- π ]").
Reserved Notation "[ Γ ⊩ π ↦ d ]" (format "[ Γ ⊩ π ↦ d ]").

Inductive cty : ctx -> expr -> type -> Prop :=
| cty_sym Γ h π :
    Γ h = π ->
    [ Γ ⊩ EVar h :- π ]
| cty_appt Γ e s π :
    [ Γ ⊩ e :- TArr π ] ->
    [ Γ ⊩ ETApp e s :- π ]
| cty_appc Γ e d ρ π :
    [ Γ ⊩ e :- Arr ρ π ] ->
    [ Γ ⊩ d :- ρ ] ->
    [ Γ ⊩ EApp e d :- π ]
| cty_part Γ e π :
    [ Γ ⊩ e :- π ] ->
    [ Γ ⊩ ETLam e :- TArr π ]
| cty_parc Γ e ρ π :
    [ ρ .: Γ ⊩ e :- π ] ->
    [ Γ ⊩ ELam e ρ :- Arr ρ π ]
| cty_box Γ I e π :
    [ Γ ⊩ e :- π ] ->
    [ Γ ⊩ EBar I e :- π ] (* mettre π *)
| cty_defn Γ e I π d :
    [ π .: Γ ⊩ e :- Void ] ->
    [ π .: Γ ⊩ π ↦ d ] ->
    [ Γ ⊩ EDef e I π d :- Void ]

with cabs : ctx -> type -> expr -> Prop :=
| cabs_void Γ d :
    [ Γ ⊩ d :- Void ] ->
    [ Γ ⊩ Void ↦ d ]
| cabs_t Γ π d :
    [ Γ ⊩ π ↦ d ] ->
    [ Γ ⊩ TArr π ↦ ETLam d ]
| cabs_c Γ ρ π d :
    [ ρ .: Γ ⊩ π ↦ d ] ->
    [ Γ ⊩ Arr ρ π ↦ ELam d ρ ]

where "[ Γ ⊩ e :- π ]" := (cty Γ e π) : coma_scope
and "[ Γ ⊩ π ↦ d ]" := (cabs Γ π d) : coma_scope.

Open Scope coma_scope.

Scheme cty_mut := Induction for cty Sort Prop
with cabs_mut := Induction for cabs Sort Prop.

Combined Scheme cty_cabs_mut from cty_mut, cabs_mut.

Lemma cabs_cty Γ π d :
  [ Γ ⊩ π ↦ d ] -> [ Γ ⊩ d :- π ].
Proof.
  elim=> * //.
  - by constructor.
  - by constructor.
Qed.

Lemma sel_eq B b :
  sel B b b = b.
Proof.
  by case B.
Qed.

Inductive arg :=
| AT (s : term)
| AC (d : expr).

Definition args := seq arg.

Definition arg_ren ξ a :=
  match a with
  | AT s => AT s
  | AC d => AC d.[ren ξ]
  end.

Fixpoint eappl e (l : args) :=
  match l with
  | [::] => e
  | AT s :: l => eappl (ETApp e s) l
  | AC d :: l => eappl (EApp e d) l
  end.

Record def := Def { dbar : barrier; dty : type; dbody : expr }.

Definition defs := seq def.

Fixpoint edefs e Λ :=
  match Λ with
  | [::] => e
  | λ :: Λ => edefs (EDef e (dbar λ) (dty λ) (dbody λ)) Λ
  end.

Fixpoint olookup Λ h : option def :=
  match Λ, h with
  | [::], _ => None
  | λ :: _, 0 => Some λ
  | _ :: Λ, h.+1 => olookup Λ h
  end.

Fixpoint eta (U : type) (d : expr) : expr :=
  match U with
  | Void => EBar Show d
  | TArr V => ETLam (eta V (ETApp d.|[ren (+1)] (TVar 0)))
  | Arr U V => ELam (eta V (EApp d.[ren (+1)] (EVar 0))) U
  end.

Definition config : Type := (expr * args * defs).

Definition config2expr (c : config) := edefs (eappl c.1.1 c.1.2) c.2.

Definition halt (Λ : defs) := EVar (size Λ).
Definition fail (Λ : defs) := EVar (size Λ).+1.
Definition if_ (Λ : defs) := EVar (size Λ).+2.

Section OpSem.

Parameter valid : term -> Prop.

Inductive step : config -> config -> Prop :=
(* “context” rules *)
| step_tapp e s l Λ : step (ETApp e s, l, Λ) (e, AT s :: l, Λ)
| step_app e d l Λ : step (EApp e d, l, Λ) (e, AC d :: l, Λ)
| step_defn e I π d Λ : step (EDef e I π d, [::], Λ) (e, [::], Def I π d :: Λ)
(* “paper” rules *)
| step_sym h d l Λ :
    olookup Λ h = Some d ->
    step (EVar h, l, Λ) ((dbody d).[ren (+h)], l, Λ)
| step_appt e s l Λ :
    step (ETLam e, AT s :: l, Λ) (e.|[s/], l, Λ)
| step_appc e ρ d l Λ :
    step (ELam e ρ, AC d :: l, Λ)
         (e, map (arg_ren (+1)) l, Def Show ρ (eta ρ d.[ren (+1)]) :: Λ)
| step_box b e Λ :
    step (EBar b e, [::], Λ) (e, [::], Λ)
| step_if_true h s e d l Λ :
    EVar h = if_ Λ ->
    valid s ->
    step (EVar h, AT s :: AC e :: AC d :: l, Λ) (e, l, Λ)
| step_if_false h s e d l Λ :
    EVar h = if_ Λ ->
    valid (FNot s) ->
    step (EVar h, AT s :: AC e :: AC d :: l, Λ) (d, l, Λ).

End OpSem.

Inductive steps : config -> config -> Prop :=
| steps_refl c :
    steps c c
| steps_step c1 c2 c3 :
    step c1 c2 -> steps c2 c3 -> steps c1 c3.

Definition halted (c : config) := c.1.1 = halt c.2 /\ c.1.2 = [::].
Definition failed (c : config) := c.1.1 = fail c.2 /\ c.1.2 = [::].

Inductive args_ty (Γ : ctx) : args -> type -> Prop :=
| args_ty_nil :
    args_ty Γ [::] Void
| args_ty_t s l π :
    args_ty Γ l π ->
    args_ty Γ (AT s :: l) (TArr π)
| args_ty_c d l ρ π :
    [ Γ ⊩ d :- ρ ] ->
    args_ty Γ l π ->
    args_ty Γ (AC d :: l) (Arr ρ π).

Definition ctx_defs Γ Λ :=
  foldr (fun λ Γ => dty λ .: Γ) Γ Λ.

Inductive defs_ty (Γ : ctx) : defs -> Prop :=
| defs_ty_nil :
    defs_ty Γ [::]
| defs_ty_cons Δ Λ :
    defs_ty Γ Λ ->
    [ dty Δ .: ctx_defs Γ Λ ⊩ dty Δ ↦ dbody Δ ] ->
    defs_ty Γ (Δ :: Λ).

Definition wf_config (Γ : ctx) (c : config) :=
  let Δ := ctx_defs Γ c.2 in
  defs_ty Γ c.2 /\
  exists π, [ Δ ⊩ c.1.1 :- π ] /\ args_ty Δ c.1.2 π.

Lemma eappl_ty Γ l π :
  args_ty Γ l π ->
  forall e,
  [ Γ ⊩ e :- π ] ->
  [ Γ ⊩ eappl e l :- Void ].
Proof.
  elim=>//.
  - move=> > ? ih *.
    apply ih.
    by apply cty_appt.
  - move=> ?? U ??? ih *.
    apply ih.
    by apply cty_appc with U.
Qed.

Lemma edefs_ty Γ Λ :
  defs_ty Γ Λ ->
  forall e,
  [ ctx_defs Γ Λ ⊩ e :- Void ] ->
  [ Γ ⊩ edefs e Λ :- Void ].
Proof.
  elim=> //.
  move=> > ? ih *.
  apply ih.
  by apply cty_defn.
Qed.

Lemma wt_config2expr Γ c :
  wf_config Γ c ->
  [ Γ ⊩ config2expr c :- Void ].
Proof.
  move=> [? [π [??]]].
  apply edefs_ty=>//.
  by apply eappl_ty with π.
Qed.