{-# OPTIONS --rewriting #-}

module A201706.ISLPSyntaxTerms where

open import A201706.ISLP public


-- Contexts.

Cx : Nat  Nat  Set
Cx d g = BoxTy⋆ d  Ty⋆ g


-- Derivations.

mutual
  infix 3 _⊢_∷_
  data _⊢_∷_ {d g} : Cx d g  Tm d g  Ty  Set where
    var   :  {Δ Γ i A} 
              Γ ∋⟨ i  A 
              Δ  Γ  VAR i  A
    mvar  :  {`d `g Δ Γ q p} {Φ : BoxTy⋆ `d} {Ψ : Ty⋆ `g} {i Q A} 
              Δ   ⊢⧆ q  Φ  Δ  Γ ⊢⋆ p  Ψ  Δ ∋⟨ i  [ Φ  Ψ  Q ] A 
              Δ  Γ  MVAR q p i  A
    lam   :  {Δ Γ M A B} 
              Δ  Γ , A  M  B 
              Δ  Γ  LAM M  A  B
    app   :  {Δ Γ M N A B} 
              Δ  Γ  M  A  B  Δ  Γ  N  A 
              Δ  Γ  APP M N  B
    box   :  {`d `g Δ Γ} {Φ : BoxTy⋆ `d} {Ψ : Ty⋆ `g} {M A} 
              Φ  Ψ  M  A 
              Δ  Γ  BOX M  [ Φ  Ψ  M ] A
    unbox :  {`d `g Δ Γ} {Φ : BoxTy⋆ `d} {Ψ : Ty⋆ `g} {M N Q A C} 
              Δ  Γ  M  [ Φ  Ψ  Q ] A  Δ , [ Φ  Ψ  Q ] A  Γ  N  C 
              Δ  Γ  UNBOX M N  C

  infix 3 _⊢⧆_∷_
  data _⊢⧆_∷_ {d g} :  {n}  Cx d g  Tm⋆ d g n  BoxTy⋆ n  Set where
       :  {Δ Γ} 
            Δ  Γ ⊢⧆   
    _,_ :  {`d `g n Δ Γ} {Φ : BoxTy⋆ `d} {Ψ : Ty⋆ `g} {x} {Ξ : BoxTy⋆ n} {M Q A} 
            Δ  Γ ⊢⧆ x  Ξ  Δ  Γ  M  [ Φ  Ψ  Q ] A 
            Δ  Γ ⊢⧆ x , M  Ξ , [ Φ  Ψ  Q ] A

  infix 3 _⊢⋆_∷_
  data _⊢⋆_∷_ {d g} :  {n}  Cx d g  Tm⋆ d g n  Ty⋆ n  Set where
       :  {Δ Γ} 
            Δ  Γ ⊢⋆   
    _,_ :  {n Δ Γ x} {Ξ : Ty⋆ n} {M A} 
            Δ  Γ ⊢⋆ x  Ξ  Δ  Γ  M  A 
            Δ  Γ ⊢⋆ x , M  Ξ , A

mutual
  mono⊢ :  {d g d′ g′} {Δ : BoxTy⋆ d} {Γ : Ty⋆ g} {Δ′ : BoxTy⋆ d′} {Γ′ : Ty⋆ g′} {M A z e} 
             Δ′ ⊇⟨ z  Δ  Γ′ ⊇⟨ e  Γ  Δ  Γ  M  A  Δ′  Γ′  monoTm z e M  A
  mono⊢ ζ η (var 𝒾)      = var (mono∋ η 𝒾)
  mono⊢ ζ η (mvar φ ψ 𝒾) = mvar (mono⊢⧆ ζ done φ) (mono⊢⋆ ζ η ψ) (mono∋ ζ 𝒾)
  mono⊢ ζ η (lam 𝒟)      = lam (mono⊢ ζ (lift η) 𝒟)
  mono⊢ ζ η (app 𝒟 )    = app (mono⊢ ζ η 𝒟) (mono⊢ ζ η )
  mono⊢ ζ η (box 𝒟)      = box 𝒟
  mono⊢ ζ η (unbox 𝒟 )  = unbox (mono⊢ ζ η 𝒟) (mono⊢ (lift ζ) η )

  mono⊢⧆ :  {d g d′ g′ n} {Δ : BoxTy⋆ d} {Γ : Ty⋆ g} {Δ′ : BoxTy⋆ d′} {Γ′ : Ty⋆ g′} {x} {Ξ : BoxTy⋆ n} {z e} 
               Δ′ ⊇⟨ z  Δ  Γ′ ⊇⟨ e  Γ  Δ  Γ ⊢⧆ x  Ξ  Δ′  Γ′ ⊢⧆ monoTm⋆ z e x  Ξ
  mono⊢⧆ ζ η        = 
  mono⊢⧆ ζ η (ξ , 𝒟) = mono⊢⧆ ζ η ξ , mono⊢ ζ η 𝒟

  mono⊢⋆ :  {d g d′ g′ n} {Δ : BoxTy⋆ d} {Γ : Ty⋆ g} {Δ′ : BoxTy⋆ d′} {Γ′ : Ty⋆ g′} {x} {Ξ : Ty⋆ n} {z e} 
              Δ′ ⊇⟨ z  Δ  Γ′ ⊇⟨ e  Γ  Δ  Γ ⊢⋆ x  Ξ  Δ′  Γ′ ⊢⋆ monoTm⋆ z e x  Ξ
  mono⊢⋆ ζ η        = 
  mono⊢⋆ ζ η (ξ , 𝒟) = mono⊢⋆ ζ η ξ , mono⊢ ζ η 𝒟

refl⊢⋆ :  {d g} {Δ : BoxTy⋆ d} {Γ : Ty⋆ g}  Δ  Γ ⊢⋆ reflTm⋆  Γ
refl⊢⋆ {Γ = }     = 
refl⊢⋆ {Γ = Γ , A} = mono⊢⋆ refl⊇ (weak refl⊇) refl⊢⋆ , var zero

-- TODO: What is going on here?
-- mrefl⊢⋆ : ∀ {d g} {Δ : BoxTy⋆ d} {Γ : Ty⋆ g} → Δ ⁏ Γ ⊢⧆ {!!} ∷ Δ
-- mrefl⊢⋆ {Δ = ∅}                   = ∅
-- mrefl⊢⋆ {Δ = Δ , [ Φ ⁏ Ψ ⊦ M ] A} =
--   mono⊢⧆ (weak refl⊇) refl⊇ mrefl⊢⋆ ,
--   {!box (mvar ? ? zero)!}