module A202401.FOR-STLC-Base-WNF where
open import A202401.FOR-STLC-Base public
mutual
data NF {Γ} : ∀ {A} → Γ ⊢ A → Set where
⌜λ⌝- : ∀ {A B} {t : Γ , A ⊢ B} → NF (⌜λ⌝ t)
nnf : ∀ {A} {t : Γ ⊢ A} (p : NNF t) → NF t
data NNF {Γ} : ∀ {A} → Γ ⊢ A → Set where
var- : ∀ {A} {i : Γ ∋ A} → NNF (var i)
_⌜$⌝_ : ∀ {A B} {t₁ : Γ ⊢ A ⌜⊃⌝ B} {t₂ : Γ ⊢ A} (p₁ : NNF t₁) (p₂ : NF t₂) → NNF (t₁ ⌜$⌝ t₂)
mutual
uniNF : ∀ {Γ A} {t : Γ ⊢ A} (p p′ : NF t) → p ≡ p′
uniNF ⌜λ⌝- ⌜λ⌝- = refl
uniNF (nnf p) (nnf p′) = nnf & uniNNF p p′
uniNNF : ∀ {Γ A} {t : Γ ⊢ A} (p p′ : NNF t) → p ≡ p′
uniNNF var- var- = refl
uniNNF (p₁ ⌜$⌝ p₂) (p₁′ ⌜$⌝ p₂′) = _⌜$⌝_ & uniNNF p₁ p₁′ ⊗ uniNF p₂ p₂′
mutual
NF? : ∀ {Γ A} (t : Γ ⊢ A) → Dec (NF t)
NF? (var i) = yes (nnf var-)
NF? (⌜λ⌝ t) = yes ⌜λ⌝-
NF? (t₁ ⌜$⌝ t₂) with NNF? t₁ | NF? t₂
... | yes p₁ | yes p₂ = yes (nnf (p₁ ⌜$⌝ p₂))
... | yes p₁ | no ¬p₂ = no λ { (nnf (p₁ ⌜$⌝ p₂)) → p₂ ↯ ¬p₂ }
... | no ¬p₁ | _ = no λ { (nnf (p₁ ⌜$⌝ p₂)) → p₁ ↯ ¬p₁ }
NNF? : ∀ {Γ A} (t : Γ ⊢ A) → Dec (NNF t)
NNF? (var i) = yes var-
NNF? (⌜λ⌝ t) = no λ ()
NNF? (t₁ ⌜$⌝ t₂) with NNF? t₁ | NF? t₂
... | yes p₁ | yes p₂ = yes (p₁ ⌜$⌝ p₂)
... | yes p₁ | no ¬p₂ = no λ { (p₁ ⌜$⌝ p₂) → p₂ ↯ ¬p₂ }
... | no ¬p₁ | _ = no λ { (p₁ ⌜$⌝ p₂) → p₁ ↯ ¬p₁ }
mutual
renNF : ∀ {Γ Γ′ A} {t : Γ ⊢ A} (ϱ : Γ ⊑ Γ′) → NF t → NF (ren ϱ t)
renNF ϱ ⌜λ⌝- = ⌜λ⌝-
renNF ϱ (nnf p) = nnf (renNNF ϱ p)
renNNF : ∀ {Γ Γ′ A} {t : Γ ⊢ A} (ϱ : Γ ⊑ Γ′) → NNF t → NNF (ren ϱ t)
renNNF ϱ var- = var-
renNNF ϱ (p₁ ⌜$⌝ p₂) = renNNF ϱ p₁ ⌜$⌝ renNF ϱ p₂
open RenNNFKit (kit renkit var- (λ {_} {_} {_} {t} → renNNF {t = t})) public
mutual
subNF : ∀ {Γ Ξ A} {σ : Ξ ⊢§ Γ} {t : Γ ⊢ A} → NNF§ σ → NF t → NF (sub σ t)
subNF ψ ⌜λ⌝- = ⌜λ⌝-
subNF ψ (nnf p) = nnf (subNNF ψ p)
subNNF : ∀ {Γ Ξ A} {σ : Ξ ⊢§ Γ} {t : Γ ⊢ A} → NNF§ σ → NNF t → NNF (sub σ t)
subNNF ψ var- = sub∋NNF ψ
subNNF ψ (p₁ ⌜$⌝ p₂) = subNNF ψ p₁ ⌜$⌝ subNF ψ p₂