module stlc where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

data Type : Set where
  base : ℕ → Type
  _↠_ : Type → Type → Type
  
infixr 7 _↠_

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

infix 10 `_
infixl 8 _∙_
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 ∶ α ↠ β
  
infix 2 _⊢_∶_

myderiv : ∀ {Γ α} → Γ ⊢ ƛ (α ↠ α) ⇒ ƛ α ⇒ ` 1 ∙ (` 1 ∙ ` 0) ∶ (α ↠ α) ↠ α ↠ α
myderiv = abs (abs (app var (app var var)))

myderiv' : ∀ {α} → [-↦ α ] ⊢ (ƛ (α ↠ α) ⇒ ƛ α ⇒ ` 1 ∙ (` 1 ∙ ` 0)) ∙ (ƛ α ⇒ ` 0) ∙ (` 8) ∶ α
myderiv' = app (app myderiv (abs (var))) var

𝓥 : Type → Set
𝓥 (base x) = Λ
𝓥 (α ↠ β) = 𝓥 α → 𝓥 β

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 ]')

t : ∀ {n} → ⟦ myderiv' {base 0} ⟧ ([-↦_]' {base 0} n) ≡ n
t = refl

ℕ-eq-dec : ∀ (n m : ℕ) → n ≡ m ⊎ ¬ (n ≡ m)
ℕ-eq-dec zero zero = inj₁ refl
ℕ-eq-dec zero (suc m) = inj₂ (λ ())
ℕ-eq-dec (suc n) zero = inj₂ (λ ())
ℕ-eq-dec (suc n) (suc m) with ℕ-eq-dec n m
... | inj₁ n≡m = inj₁ (cong suc n≡m)
... | inj₂ y = inj₂ (λ sn≡sm → y (suc-injective sn≡sm))

↠-injective₁ : ∀ {α β γ δ} → α ↠ β ≡ γ ↠ δ → α ≡ γ
↠-injective₁ {α} {β} {.α} {.β} refl = refl

↠-injective₂ : ∀ {α β γ δ} → α ↠ β ≡ γ ↠ δ → β ≡ δ
↠-injective₂ {α} {β} {.α} {.β} refl = refl

typeEqDec : ∀ (α β : Type) → α ≡ β ⊎ ¬ (α ≡ β)
typeEqDec (base n) (base m) with ℕ-eq-dec n m
... | inj₁ n≡m = inj₁ (cong base n≡m)
... | inj₂ ¬n≡m = inj₂ (λ { refl → ¬n≡m refl })
typeEqDec (base x) (β ↠ β₁) = inj₂ (λ ())
typeEqDec (α ↠ α₁) (base x) = inj₂ (λ ())
typeEqDec (α ↠ β) (γ ↠ δ) with typeEqDec α γ | typeEqDec β δ
... | inj₁ refl | inj₁ refl = inj₁ refl
... | inj₁ refl | inj₂ y = inj₂ λ x → y (↠-injective₂ {α = α} {γ = γ} x)
... | inj₂ x | inj₁ refl = inj₂ λ x₁ → x (↠-injective₁ {β = β} {δ = δ} x₁)
... | inj₂ x | inj₂ y = inj₂ (λ x₁ → y (↠-injective₂ {α = α} {γ = γ} x₁))

typingDec : ∀ Γ t α → (Γ ⊢ t ∶ α) ⊎ (¬ (Γ ⊢ t ∶ α))
typingDec Γ (` x) α with typeEqDec α (Γ x)
... | inj₁ refl = inj₁ var
... | inj₂ y = inj₂ λ x₁ → y (⊢-injection x₁)
  where ⊢-injection : ∀ {Γ v α} → Γ ⊢ ` v ∶ α → α ≡ Γ v
        ⊢-injection var = refl
typingDec Γ (f ∙ x) α = {!!}
typingDec Γ (ƛ x ⇒ t₁) α = {!!}

--------------------------------------------------------------

lift_by_above_ : Λ → ℕ → ℕ → Λ
lift ` x by n above i with compare x i
... | less _ _ = ` x
... | equal _ = ` x
... | greater _ _ = ` (x + i)
lift t ∙ s by n above i = (lift t by n above i) ∙ (lift s by n above i)
lift ƛ x ⇒ t by n above i = ƛ x ⇒ (lift t by n above (suc i))


_[_↦_] : Λ → ℕ → Λ → Λ
(` x) [ n ↦ rep ] with compare x n
... | less _ _ = ` x
... | equal _ = lift rep by x above 0
... | greater .n k = ` (n + k)
(t ∙ s) [ n ↦ rep ] = (t [ n ↦ rep ]) ∙ (s [ n ↦ rep ])
(ƛ x ⇒ t) [ n ↦ rep ] = ƛ x ⇒ t [ n ↦ rep ]

data _⟶_ : Λ → Λ → Set where
  ⟶∙r : ∀ {s s' t} →
    s ⟶ s' →
    ----------------------
    t ∙ s ⟶ t ∙ s'
    
  ⟶∙l : ∀ {s t t'} →
    t ⟶ t' →
    ----------------------
    t ∙ s ⟶ t' ∙ s

  ⟶λ : ∀ {t t' α} →
    t ⟶ t' →
    ----------------------
    (ƛ α ⇒ t) ⟶ (ƛ α ⇒ t')
    
  ⟶β : ∀  {s t α} →
    ----------------------
    ((ƛ α ⇒ t) ∙ s) ⟶ (t [ 0 ↦ s ])

infix 2 _⟶_