Nbe Is A Semantics

NbeIsASemantics.agda

module NbeIsASemantics where

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Agda.Builtin.List

data Ty : Set where
  α   : Ty
  _⇒_ : Ty → Ty → Ty


module _ {I : Set} where

  infixr 5 _⟶_
  infix  8 _⊢_
  infixr 7 _∙×_

  _⟶_ : (I → Set) → (I → Set) → (I → Set)
  (S ⟶ T) i = S i → T i

  [_] : (I → Set) → Set
  [ T ] = ∀ {i} → T i

  _⊢_ : (I → I) → (I → Set) → (I → Set)
  (f ⊢ T) i = T (f i)

  _∙×_ : (I → Set) → (I → Set) → (I → Set)
  (S ∙× T) i = S i × T i

  κ : Set → (I → Set)
  κ S i = S

Model : Set₁
Model = Ty → List Ty → Set

data Var : Model where
  z : {σ : Ty}   → [          (σ ∷_) ⊢ Var σ ]
  s : {σ τ : Ty} → [ Var σ ⟶ (τ ∷_) ⊢ Var σ ]

infix 3 _─Env
record _─Env (Γ : List Ty) (M : Model) (Δ : List Ty) : Set where
  constructor pack
  field lookup : {σ : Ty} → Var σ Γ → M σ Δ
open _─Env


_<$>_ : {M N : Model} {Γ Δ Θ : List Ty} → ({σ : Ty} → M σ Δ → N σ Θ) → (Γ ─Env) M Δ → (Γ ─Env) N Θ
lookup (f <$> ρ) k = f (lookup ρ k)


ε : ∀ {M Δ} → ([] ─Env) M Δ
lookup ε ()
 
infixl 10 _∙_
_∙_ : ∀ {M Γ Δ σ} → (Γ ─Env) M Δ → M σ Δ → (σ ∷ Γ ─Env) M Δ
lookup (ρ ∙ v) z    = v
lookup (ρ ∙ v) (s k) = lookup ρ k

refl : ∀ {Γ} → (Γ ─Env) Var Γ
lookup refl v = v

Thinning : List Ty → List Ty → Set
Thinning Γ Δ = (Γ ─Env) Var Δ

select : ∀ {Γ Δ Θ M} → Thinning Γ Δ → (Δ ─Env) M Θ → (Γ ─Env) M Θ
lookup (select ren ρ) k = lookup ρ (lookup ren k)

extend : ∀ {Γ σ} → Thinning Γ (σ ∷ Γ)
extend = pack s

□ : (List Ty → Set) → (List Ty → Set)
(□ T) Γ = [ Thinning Γ ⟶ T ]

duplicate : {T : List Ty → Set} → [ □ T ⟶ □ (□ T) ]
duplicate t ρ σ = t (select ρ σ)

module Syntax {CUT : Ty → Set} where

  data Chk : Model
  data Syn : Model

  data Chk where
    l : {σ τ : Ty} → [ (σ ∷_) ⊢ Chk τ ⟶ Chk (σ ⇒ τ) ]
    e : {σ : Ty}   → [ Syn σ          ⟶ Chk σ       ]

  data Syn where
    v : {σ : Ty}               → [ Var σ                ⟶ Syn σ ]
    c : {σ : Ty} {{p : CUT σ}} → [ Chk σ                ⟶ Syn σ ]
    a : {σ τ : Ty}             → [ Syn (σ ⇒ τ) ⟶ Chk σ ⟶ Syn τ ]

  ren^Chk : {σ : Ty} {Γ Δ : List Ty} →
            Thinning Γ Δ → Chk σ Γ → Chk σ Δ
  ren^Syn : {σ : Ty} {Γ Δ : List Ty} →
            Thinning Γ Δ → Syn σ Γ → Syn σ Δ

  ren^Chk ρ (l b)   = l (ren^Chk (select ρ extend ∙ z) b)
  ren^Chk ρ (e t)   = e (ren^Syn ρ t)
  ren^Syn ρ (v x)   = v (lookup ρ x)
  ren^Syn ρ (c t)   = c (ren^Chk ρ t)
  ren^Syn ρ (a f t) = a (ren^Syn ρ f) (ren^Chk ρ t)

open Syntax


NoCut : Ty → Set
NoCut α = ⊤
NoCut _ = ⊥

Nf = Syntax.Chk {NoCut}
Ne = Syntax.Syn {NoCut}

NBE : Model
GO! : Model

NBE σ = Nf σ ∙× GO! σ

GO! α       = Ne α
GO! (σ ⇒ τ) = □ (NBE σ ⟶ NBE τ)

ren^NBE : (σ : Ty) {Γ Δ : List Ty} →
          Thinning Γ Δ → NBE σ Γ → NBE σ Δ
ren^GO! : (σ : Ty) {Γ Δ : List Ty} →
          Thinning Γ Δ → GO! σ Γ → GO! σ Δ

ren^NBE σ       ρ (t , T) = ren^Chk ρ t , ren^GO! σ ρ T
ren^GO! α       ρ T       = ren^Syn ρ T
ren^GO! (σ ⇒ τ) ρ T       = duplicate T ρ

reify   : (σ : Ty) → [ GO! σ ⟶ Nf σ ]
reflect : (σ : Ty) → [ Ne σ ⟶ GO! σ ]

reify   α       T = e T
reify   (σ ⇒ τ) T = let v = e (v z) , reflect σ (v z)
                    in l (reify τ (proj₂ (T extend v)))
reflect α       t = t
reflect (σ ⇒ τ) t = λ r v →
  let t⌞v⌟ = a (ren^Syn r t) (proj₁ v)
  in e t⌞v⌟ , reflect τ t⌞v⌟

Trm = Syntax.Chk {λ _ → ⊤}
Elm = Syntax.Syn {λ _ → ⊤}

nbe^Trm : {σ : Ty} {Γ Δ : List Ty} →
          (Γ ─Env) NBE Δ → Trm σ Γ → NBE σ Δ
nbe^Elm : {σ : Ty} {Γ Δ : List Ty} →
          (Γ ─Env) NBE Δ → Elm σ Γ → NBE σ Δ

nbe^Trm {ty@(σ ⇒ τ)} {Γ} {Δ} ρ (l b)   =
  let T : GO! ty Δ
      T = λ r v → nbe^Trm ((ren^NBE _ r <$> ρ) ∙ v) b
  in reify ty T , T
nbe^Trm ρ (e t)   = nbe^Elm ρ t
nbe^Elm ρ (v x)   = lookup ρ x
nbe^Elm ρ (c t)   = nbe^Trm ρ t
nbe^Elm ρ (a f t) = proj₂ (nbe^Elm ρ f) refl (nbe^Trm ρ t)

norm : {σ : Ty} → [ Trm σ ⟶ Nf σ ]
norm t = proj₁ (nbe^Trm (pack (λ x → e (v x) , reflect _ (v x))) t)