------------------------------------------------------------------------
-- The syntax of, and a type system for, the untyped λ-calculus with
-- constants
------------------------------------------------------------------------

module Lambda.Syntax where

open import Codata.Musical.Notation
open import Data.Nat
open import Data.Fin hiding (_≤?_)
open import Data.Vec
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- Terms

-- Variables are represented using de Bruijn indices.

infixl 9 _·_

data Tm (n : ) : Set where
  con : (i : )  Tm n
  var : (x : Fin n)  Tm n
  ƛ   : (t : Tm (suc n))  Tm n
  _·_ : (t₁ t₂ : Tm n)  Tm n

-- Convenient helper.

vr :  m {n} {m<n : True (suc m ≤? n)}  Tm n
vr _ {m<n = m<n} = var (#_ _ {m<n = m<n})

------------------------------------------------------------------------
-- Values, potentially with free variables

module WHNF where

  data Value (n : ) : Set where
    con : (i : )  Value n
    ƛ   : (t : Tm (suc n))  Value n

  ⌜_⌝ :  {n}  Value n  Tm n
   con i  = con i
   ƛ t    = ƛ t

------------------------------------------------------------------------
-- Closure-based definition of values

-- Environments and values. Defined in a module parametrised on the
-- type of terms.

module Closure (Tm :   Set) where

  mutual

    -- Environments.

    Env :   Set
    Env n = Vec Value n

    -- Values. Lambdas are represented using closures, so values do
    -- not contain any free variables.

    data Value : Set where
      con : (i : )  Value
      ƛ   :  {n} (t : Tm (suc n)) (ρ : Env n)  Value

------------------------------------------------------------------------
-- Type system (following Leroy and Grall)

-- Recursive, simple types, defined coinductively.

infixr 8 _⇾_

data Ty : Set where
  nat : Ty
  _⇾_ : (σ τ :  Ty)  Ty

-- Contexts.

Ctxt :   Set
Ctxt n = Vec Ty n

-- Type system.

infix 4 _⊢_∈_

data _⊢_∈_ {n} (Γ : Ctxt n) : Tm n  Ty  Set where
  con :  {i}  Γ  con i  nat
  var :  {x}  Γ  var x  lookup Γ x
  ƛ   :  {t σ τ} (t∈ :  σ  Γ  t   τ)  Γ  ƛ t  σ  τ
  _·_ :  {t₁ t₂ σ τ} (t₁∈ : Γ  t₁  σ  τ) (t₂∈ : Γ  t₂   σ) 
        Γ  t₁ · t₂   τ

------------------------------------------------------------------------
-- Example

-- A non-terminating term.

ω : Tm 0
ω = ƛ (vr 0 · vr 0)

Ω : Tm 0
Ω = ω · ω

-- Ω is well-typed.

Ω-well-typed : (τ : Ty)  []  Ω  τ
Ω-well-typed τ =
  _·_ {σ =  σ} {τ =  τ} (ƛ (var · var)) (ƛ (var · var))
  where σ =  σ   τ

-- A call-by-value fix-point combinator.

Z : Tm 0
Z = ƛ (t · t)
  where t = ƛ (vr 1 · ƛ (vr 1 · vr 1 · vr 0))

-- This combinator is also well-typed.

fix-well-typed :
   {σ τ}  []  Z   ( (σ  τ)   (σ  τ))   (σ  τ)
fix-well-typed =
  ƛ (_·_ {σ = υ} {τ =  _}
         (ƛ (var · ƛ (var · var · var)))
         (ƛ (var · ƛ (var · var · var))))
  where
  υ :  Ty
  υ =  (υ   _)