module stlcN where

open import Data.Nat
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

data Type : Set where
  N : Type
  _↠_ : Type → Type → Type
  
infixr 7 _↠_

data Λ : Set where
  `_ : ℕ → Λ
  _∙_ : Λ → Λ → Λ
  ƛ_⇒_ : Type → Λ → Λ
  $_ : ℕ → Λ
  _⊹_ : Λ → Λ → Λ

infix 10 `_
infixl 8 _∙_
infix 5 _⊹_
infix 5 ƛ_⇒_

Context : Set
Context = ℕ → Type

[-↦_] : Type → Context
[-↦ α ] = λ _ → α  

_[0↦_] : Context → Type → Context
(Γ [0↦ α ]) zero = α
(Γ [0↦ α ]) (suc n) = Γ n

data _⊢_∶_ : Context → Λ → Type → Set where
  var : ∀ {Γ} {v} → 
  ----------------------
    Γ ⊢ ` v ∶ (Γ v)

  app : ∀ {Γ} {f} {α} {β} {x} →
    Γ ⊢ f ∶ α ↠ β →
    Γ ⊢ x ∶ α → 
  ----------------------
    Γ ⊢ f ∙ x ∶ β

  abs : ∀ {Γ} {α} {β} {t} {v} →
    Γ [0↦ α ] ⊢ t ∶ β →
  ----------------------
    Γ ⊢ ƛ v ⇒ t ∶ α ↠ β
    
  const : ∀ {Γ} (n : ℕ) → 
  ----------------------
    Γ ⊢ $ n ∶ N

  plus : ∀ {Γ a b}  →
    Γ ⊢ a ∶ N →
    Γ ⊢ b ∶ N →
  ----------------------
    Γ ⊢ a ⊹ b ∶ N
  
  
infix 2 _⊢_∶_

𝓥 : Type → Set
𝓥 N = ℕ
𝓥 (α ↠ β) = 𝓥 α → 𝓥 β

Env : Context → Set
Env Γ = ∀ n → 𝓥 (Γ n)

[-↦_]' : ∀ {α} → 𝓥 α → Env ([-↦ α ])
[-↦ X ]' = λ _ → X  

_[0↦_]' : ∀ {Γ α} → Env Γ → 𝓥 α → Env (Γ [0↦ α ])
(γ [0↦ X ]') zero = X
(γ [0↦ X ]') (suc n) = γ n

⟦_⟧_ : ∀ {Γ t α} → Γ ⊢ t ∶ α → Env Γ → 𝓥 α
⟦ var {v = v} ⟧ γ = γ v
⟦ app t s ⟧ γ     = (⟦ t ⟧ γ) (⟦ s ⟧ γ)
⟦ abs t ⟧ γ       = λ X → ⟦ t ⟧ (γ [0↦ X ]')
⟦ const n ⟧ γ     = n 
⟦ plus a b ⟧ γ    = ⟦ a ⟧ γ + ⟦ b ⟧ γ