-- A procrastination project of simply typed lambda calculus (Curry-style and de Bruijn-indices)
open import Data.Nat
open import Data.Fin hiding (#_)
open import Data.Sum
open import Data.Product
open import Level using (Lift ; lift)

module stlc {ℓ} where

  infixl 7  _∙_
  data Λ : ℕ → Set ℓ where
    #_ : ∀ {n} → Fin n → Λ n

    ƛ_ : ∀ {n} → Λ (suc n) → Λ n

    _∙_ : ∀ {n} → Λ n → Λ n → Λ n

  ext : ∀ {n m} → (ρ : Fin n → Fin m) → Fin (suc n) → Fin (suc m)
  ext ρ zero = zero
  ext ρ (suc x) = suc (ρ x)

  Subst : ℕ → ℕ → Set ℓ
  Subst n m = Fin n → Λ m

  rename : ∀ {n m} → (ρ : Fin n → Fin m) → Λ n → Λ m
  rename ρ (# x) = # (ρ x)
  rename ρ (ƛ t) = ƛ (rename (ext ρ) t)
  rename ρ (s ∙ t) = (rename ρ s) ∙ (rename ρ t)

  exts : ∀ {n m} → (σ : Subst n m) → Fin (suc n) → Λ (suc m)
  exts σ zero = # zero
  exts σ (suc x) = rename suc (σ x)

  subst : ∀ {n m} → (σ : Subst n m) → Λ n → Λ m
  subst σ (# x) = σ x
  subst σ (ƛ t) = ƛ subst (exts σ) t
  subst σ (s ∙ t) = (subst σ s) ∙ (subst σ t)

  _⟪_⟫ : ∀ {n m} → Λ n → Subst n m → Λ m
  t ⟪ σ ⟫ = subst σ t

  _[0↦_] : ∀ {n} → Λ (suc n) → Λ n → Λ n
  _[0↦_] {n} s t  = s ⟪ σ ⟫
    where σ : Subst (suc n) n
          σ zero = t
          σ (suc n) = # n

  infixr 7 _⇒_
  data type : Set ℓ where
    _⇒_ : type → type → type
    ⋆ : type

  infixl 5 _⨾_
  data context : ℕ → Set ℓ where
    [] : context zero
    _⨾_ : ∀ {n} → context n → type → context (suc n)

  infix 3 _∋_⦂_

  data _∋_⦂_ : ∀ {n} → context n → Fin n → type → Set ℓ where
    Z : ∀ {n : ℕ} {Γ : context n} {α} →
      Γ ⨾ α ∋ zero ⦂ α

    S : ∀ {n : ℕ} {Γ : context n} {x α β} →
      Γ ∋ x ⦂ α →
      Γ ⨾ β ∋ (suc x) ⦂ α


  infix 4 _⊢_⦂_
  data _⊢_⦂_ {n} : context n → Λ n → type → Set ℓ where
    var : ∀ {Γ x α} →
      Γ ∋ x ⦂ α →
      Γ ⊢ # x ⦂ α

    abs : ∀ {Γ α β t} →
      Γ ⨾ α ⊢ t ⦂ β →
      ------------------
      Γ ⊢ ƛ t ⦂ α ⇒ β

    app : ∀ {Γ α β t u} →
      Γ ⊢ t ⦂ α ⇒ β →
      Γ ⊢ u ⦂ α →
      Γ ⊢ t ∙ u ⦂ β

  module example where
    types : [] ⨾ ⋆ ⊢ ƛ (# zero ∙ (# zero ∙ # (suc zero))) ⦂ (⋆ ⇒ ⋆) ⇒ ⋆
    types = abs (app (var Z) (app (var Z) (var (S Z))))

    types' : [] ⨾ ⋆ ⨾ ⋆ ⊢ (ƛ (# zero ∙ (# zero ∙ # (suc zero)))) ∙ (ƛ (# (suc (suc zero)))) ⦂ ⋆
    types' = app (abs (app (var Z) (app (var Z) (var (S Z))))) (abs (var (S (S Z))))

    open import Relation.Nullary
    notypes : ¬ ∃ λ α → [] ⊢ ƛ (# zero ∙ # zero) ⦂ α
    notypes (α , abs (app (var Z) (var ())))

  data value {n} : Λ n → Set ℓ where
    ƛ-value : ∀ {t} → value (ƛ t)

  infix 2 _⟶_
  data _⟶_ {n} : Λ n → Λ n → Set ℓ where
    ξₗ : ∀ {s s' t : Λ n} →
      s ⟶ s' →
      s ∙ t ⟶ s' ∙ t

    ξᵣ : ∀ {s t t' : Λ n} →
      value s →
      t ⟶ t' →
      s ∙ t ⟶ s ∙ t'

    β : ∀ {s : Λ (suc n)} {t : Λ n} →
      value t →
      (ƛ s) ∙ t ⟶ s [0↦ t ]

  progress : ∀ {α} (s : Λ 0) →
    [] ⊢ s ⦂ α →
    value s ⊎ ∃ λ t → s ⟶ t
  progress (ƛ s) (abs x) = inj₁ ƛ-value
  progress (s ∙ u) (app s⦂α⇒β u⦂α) with progress s s⦂α⇒β | progress u u⦂α
  ... | inj₁ (ƛ-value {t}) | inj₁ vu = inj₂ (t [0↦ u ] , (β vu))
  ... | inj₁ (ƛ-value {t}) | inj₂ (u' , u⟶u') = inj₂ ((ƛ t) ∙ u' , ξᵣ ƛ-value u⟶u')
  ... | inj₂ (t , s⟶t) | _ = inj₂ (t ∙ u , ξₗ s⟶t)


  ↑ : ∀ {n} → Fin (suc n) → Λ n → Λ (suc n)
  ↑ k (# x) = # (punchIn k x)
  ↑ k (ƛ t) = ƛ ↑ (suc k) t
  ↑ k (s ∙ t) = (↑ k s) ∙ (↑ k t)

  weaken : ∀ {n} {Γ α β} {s : Λ n} →
    Γ ⊢ s ⦂ α →
    Γ ⨾ β ⊢ ↑ zero s ⦂ α
  weaken (var x) = var (S x)
  weaken (abs x) = abs {!!}
  weaken (app x y) = app (weaken x) (weaken y)

  substitutive : ∀ {α β} {s : Λ (suc zero)} {t : Λ zero} →
    [] ⨾ β ⊢ s ⦂ α →
    [] ⊢ t ⦂ β →
    [] ⊢ (s [0↦ t ]) ⦂ α
  substitutive {s = # zero} {t} (var Z) t⦂β = t⦂β
  substitutive {s = ƛ s} (abs s⦂α) t⦂β = abs {!!}
  substitutive {s = a ∙ b} (app a⦂α⇒β b⦂α) t⦂β = app (substitutive a⦂α⇒β t⦂β) (substitutive b⦂α t⦂β)

  preservation : ∀ {s t : Λ zero} {α : type} →
    [] ⊢ s ⦂ α →
    s ⟶ t →
    [] ⊢ t ⦂ α
  preservation (var x) ()
  preservation (abs x) ()
  preservation (app t⦂α⇒β u⦂α) (ξₗ t⟶s') = app (preservation t⦂α⇒β t⟶s') u⦂α
  preservation (app t⦂α⇒β u⦂α) (ξᵣ v u⟶t') = app t⦂α⇒β (preservation u⦂α u⟶t')
  preservation (app (abs t⦂α) u⦂α) (β v) = substitutive t⦂α u⦂α