module Definition.Untyped.Normal-form {a} (M : Set a) where
open import Definition.Untyped M
open import Tools.Fin
open import Tools.Nat
private variable
A B C c g k n t u : Term _
p q r : M
b : BinderMode
s : SigmaMode
mutual
data Nf {m : Nat} : Term m → Set a where
Uₙ : Nf U
ΠΣₙ : Nf A → Nf B → Nf (ΠΣ⟨ b ⟩ p , q ▷ A ▹ B)
ℕₙ : Nf ℕ
Emptyₙ : Nf Empty
Unitₙ : Nf Unit
lamₙ : Nf t → Nf (lam q t)
prodₙ : Nf t → Nf u → Nf (prod s p t u)
zeroₙ : Nf zero
sucₙ : Nf t → Nf (suc t)
starₙ : Nf star
ne : NfNeutral n → Nf n
data NfNeutral {m : Nat} : Term m → Set a where
var : (x : Fin m) → NfNeutral (var x)
∘ₙ : NfNeutral k → Nf u → NfNeutral (k ∘⟨ q ⟩ u)
fstₙ : NfNeutral t → NfNeutral (fst p t)
sndₙ : NfNeutral t → NfNeutral (snd p t)
natrecₙ : Nf C → Nf c → Nf g → NfNeutral k →
NfNeutral (natrec p q r C c g k)
prodrecₙ : Nf C → NfNeutral t → Nf u →
NfNeutral (prodrec r p q C t u)
emptyrecₙ : Nf C → NfNeutral k → NfNeutral (emptyrec p C k)
nfNeutral : NfNeutral n → Neutral n
nfNeutral = λ where
(var _) → var _
(∘ₙ n _) → ∘ₙ (nfNeutral n)
(fstₙ n) → fstₙ (nfNeutral n)
(sndₙ n) → sndₙ (nfNeutral n)
(natrecₙ _ _ _ n) → natrecₙ (nfNeutral n)
(prodrecₙ _ n _) → prodrecₙ (nfNeutral n)
(emptyrecₙ _ n) → emptyrecₙ (nfNeutral n)
nfWhnf : Nf n → Whnf n
nfWhnf = λ where
Uₙ → Uₙ
(ΠΣₙ _ _) → ΠΣₙ
ℕₙ → ℕₙ
Emptyₙ → Emptyₙ
Unitₙ → Unitₙ
(lamₙ _) → lamₙ
(prodₙ _ _) → prodₙ
zeroₙ → zeroₙ
(sucₙ _) → sucₙ
starₙ → starₙ
(ne n) → ne (nfNeutral n)