module CoDeBruijn where

open import Agda.Builtin.Nat using (Nat; zero; suc; _+_)
open import Data.List using (List; _∷_; []; _++_)
open import Level using (Level)
open import Data.Unit using (⊤; tt)

ℕ = Nat

module Untyped where
  variable k l : ℕ

  -- A binary sequence of length k containing l 1s
  data Filter : (k l : ℕ) → Set where
    done :              Filter      0       0
    yes  : Filter k l → Filter (suc k) (suc l)
    no   : Filter k l → Filter (suc k)      l

  data Term : ℕ → Set where
    var  : Term 1
    app  : Term k → Term l → Term (k + l)
    -- Each variable filtered out by the sequence is bound here
    lam  : Filter k l → Term k → Term l

  -- λ0
  identity : Term 0
  identity = lam (no done) var

  -- λλ1
  const : Term 0
  const = lam (no done) (lam (yes done) var)

  -- λλλ201
  flip : Term 0
  flip = 
    lam (no done) (
      lam (yes (no done)) (
        lam (yes (no (yes done))) (
          app (app var var) var
        )
      )
    )

  -- This operator showcases how we can reference the same variable more than once
  -- λλ110, i.e. λs. λz. s (s z)
  two : Term 0
  two = 
    lam (no (no done)) (
      lam (yes (yes (no done))) (
        app var (app var var)
      )
    )

module Typed where
  data Ty (b : Set) : Set where
    base : b → Ty b
    func : Ty b → Ty b → Ty b

  variable 
    b : Set
    ta tb : Ty b
    Γ Δ : List (Ty b)

  data TypedFilter (t : Ty b) : (Γ Δ : List (Ty b)) → Set where
    done : TypedFilter t [] []
    yes  : TypedFilter t Γ Δ → TypedFilter t (ta ∷ Γ) (ta ∷ Δ)
    no   : TypedFilter t Γ Δ → TypedFilter t (t ∷ Γ) Δ

  data STLC {b : Set} : List (Ty b) → Ty b → Set where
    var : STLC (ta ∷ []) ta
    app : STLC Γ (func ta tb) → STLC Δ ta → STLC (Γ ++ Δ) tb 
    lam : TypedFilter ta Γ Δ  → STLC Γ tb → STLC Δ (func ta tb)

  tx = base 0
  ty = base 1
  tz = base 2

  identity : STLC [] _
  identity = 
    lam {ta = tx} (no done) var

  const : STLC [] _
  const = 
    lam {ta = tx} (no done) (
      lam {ta = ty} (yes done) var
    )

  flip : STLC {b = ℕ} [] (func (func tx (func ty tz)) (func ty (func tx tz)))
  flip = 
    lam (no done) (
      lam (yes (no done)) (
        lam (yes (no (yes done))) (
          app (app var var) var
        )
      )
    )