------------------------------------------------------------------------
-- Normal and neutral terms
------------------------------------------------------------------------

open import Level using (zero)
open import Data.Universe

(Uni₀ : Universe zero zero) where

open import Data.Product as Prod renaming (curry to c; uncurry to uc)
open import Function hiding (_∋_) renaming (const to k; _∘_ to _⊚_)
import README.DependentlyTyped.Term as Term; open Term Uni₀
import Relation.Binary.PropositionalEquality as P

-- Atomic types (types for which the normaliser does not do
-- η-expansion).

data _⊢_atomic-type (Γ : Ctxt) : Type Γ  Set where
:  {σ}  Γ    , σ atomic-type
el :  {σ}  Γ  el , σ atomic-type

-- Two kinds: normal and neutral.

data Kind : Set where
no ne : Kind

mutual

-- Γ ⊢ σ ⟨ no ⟩ represents η-long, β-normal terms, Γ ⊢ σ ⟨ ne ⟩
-- represents neutral terms.

infixl 9 _·_
infix  3 _⊢_⟨_⟩

data _⊢_⟨_⟩ (Γ : Ctxt) : Type Γ  Kind  Set where
ne  :  {σ} (σ′ : Γ  σ atomic-type) (t : Γ  σ  ne )
Γ  σ  no
var :  {σ} (x : Γ  σ)  Γ  σ  ne
ƛ   :  {σ τ} (t : Γ  σ  τ  no )  Γ  Type-π σ τ  no
_·_ :  {sp₁ sp₂ σ}
(t₁ : Γ  π sp₁ sp₂ , σ  ne ) (t₂ : Γ  fst σ  no )
Γ  snd σ  ŝub   t₂    ne

-- Normal and neutral terms can be turned into ordinary terms.

⌊_⌋ :  {Γ σ k}  Γ  σ  k   Γ  σ
ne σ′ t  =  t
var x    = var x
ƛ t      = ƛ  t
t₁ · t₂  =  t₁  ·  t₂

-- Normal and neutral terms are "term-like".

Tm-n : Kind  Term-like _
Tm-n k = record { _⊢_ = λ Γ σ  Γ  σ  k ; ⟦_⟧ = ⟦_⟧  ⌊_⌋ }

private
open module T {k} = Term-like (Tm-n k) public
using ([_])
renaming ( ⟦_⟧ to ⟦_⟧n; _≅-⊢_ to _≅-⊢n_
; drop-subst-⊢ to drop-subst-⊢n; ⟦⟧-cong to ⟦⟧n-cong
)

-- As mentioned above normal and neutral terms can be turned into
-- ordinary terms.

forget-n :  {k}  [ Tm-n k ⟶⁼ Tm ]
forget-n = record
{ function    = λ _  ⌊_⌋
; corresponds = λ _ _  P.refl
}

-- Various congruences.

ne-cong :  {Γ σ} {σ′ : Γ  σ atomic-type}
{t₁ t₂ : Γ  σ  ne }
t₁ ≅-⊢n t₂  ne σ′ t₁ ≅-⊢n ne σ′ t₂
ne-cong P.refl = P.refl

var-n-cong :  {Γ₁ σ₁} {x₁ : Γ₁  σ₁}
{Γ₂ σ₂} {x₂ : Γ₂  σ₂}
x₁ ≅-∋ x₂  var x₁ ≅-⊢n var x₂
var-n-cong P.refl = P.refl

ƛn-cong :  {Γ₁ σ₁ τ₁} {t₁ : Γ₁  σ₁  τ₁  no }
{Γ₂ σ₂ τ₂} {t₂ : Γ₂  σ₂  τ₂  no }
t₁ ≅-⊢n t₂  ƛ t₁ ≅-⊢n ƛ t₂
ƛn-cong P.refl = P.refl

·n-cong :
{Γ₁ sp₁₁ sp₂₁ σ₁}
{t₁₁ : Γ₁  π sp₁₁ sp₂₁ , σ₁  ne } {t₂₁ : Γ₁  fst σ₁  no }
{Γ₂ sp₁₂ sp₂₂ σ₂}
{t₁₂ : Γ₂  π sp₁₂ sp₂₂ , σ₂  ne } {t₂₂ : Γ₂  fst σ₂  no }
t₁₁ ≅-⊢n t₁₂  t₂₁ ≅-⊢n t₂₂  t₁₁ · t₂₁ ≅-⊢n t₁₂ · t₂₂
·n-cong P.refl P.refl = P.refl