open import Relation.Nullary
open import Data.List
open import Data.Product
open import Data.Empty
open import Data.Sum
open import Data.Unit hiding (_≟_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality as PEq hiding ([_])
open import Data.List.Relation.Unary.Any
open import Data.List.Membership.Propositional
open import Relation.Binary.Construct.Closure.Equivalence as Eq
open import Relation.Binary.Construct.Union
open import Data.List.Relation.Binary.Pointwise as Pw hiding (refl)

open import Stoughton.Var

module NormalForm {𝒞 𝒱 : Set} (enum : Enum 𝒱) (𝒜 : 𝒞 → 𝒞 → Set) (ℛ : 𝒞 → 𝒞 → 𝒞 → Set) where

  open Enum enum

  open import Stoughton.Chi encode decode inverse
  open import Stoughton.Syntax 𝒞 𝒱 _≟_
  open import Stoughton.Substitution 𝒞 enum
  open import Stoughton.SubstitutionLemmas 𝒞 enum  
  open import Stoughton.Alpha 𝒞 enum
  open import Stoughton.Renaming 𝒞 enum
  
  open import PTSs enum 𝒜 ℛ
  open import PTSs.Metatheory enum 𝒜 ℛ
  open import Beta 𝒞 enum  
  open import BetaReduction 𝒞 enum
  open import BetaConversion 𝒞 enum
  open import Context 𝒱 Λ _≟_
  open import Utils

  open import ChurchRosser 𝒞 enum

  -- absurd propositions and auxiliary lemmas
  
  reduceVar : ∀ {x A} → v x →β*₀ A → A ≡ v x
  reduceVar ε = PEq.refl
  reduceVar (→cxt () ◅ _)
  
  reduceConst : ∀ {s A} → c s →β*₀ A → A ≡ c s
  reduceConst ε = PEq.refl
  reduceConst (→cxt () ◅ _) 

  absurd₁ : ∀ {x s A B} → ¬(Π[ x ∶ A ] B ≃β c s)
  absurd₁ Π[x:A]B≃s with CR2 Π[x:A]B≃s
  ... | M , N , Π[x:A]B→*M , s→*N , M∼N with genRedProd Π[x:A]B→*M | reduceConst s→*N
  absurd₁ {x} {s} Π[x:A]B≃s | .(Π[ x ∶ A' ] B') , .(c s) , _ , _ , () | A' , B' , refl , _ , _ | refl

  absurd₂ : ∀ {x s} → ¬(v x ≃β c s)
  absurd₂ x≃s with CR2 x≃s
  ... | M , N , x→*M , s→*N , M∼N with reduceVar x→*M | reduceConst s→*N
  absurd₂ {x} {s} x≃s | .(v x) , .(c s) , _ , _ , () | refl | refl

  absurd₃ : ∀ {y x A B} → ¬(v y ≃β Π[ x ∶ A ] B)
  absurd₃ y≃Π[x:A]B with CR2 y≃Π[x:A]B
  ... | M , N , y→*M , Π[x:A]B→*N , M∼N with reduceVar y→*M | genRedProd Π[x:A]B→*N
  absurd₃ {y} {x} y≃Π[x:A]B | .(v y) , .(Π[ x ∶ A' ] B') , _ , _ , () | refl | A' , B' , refl , _ , _

  absurd₋₁ : ∀ {Γ x y A B C D} → ¬(Γ ⊢ₛ Π[ x ∶ A ] B ∶ Π[ y ∶ C ] D)
  absurd₋₁ Γ⊢Π[x:A]B:Π[y:C]D with genProd Γ⊢Π[x:A]B:Π[y:C]D
  ... | _ , _ , _ , _ , _ , _ , _ , _ , Π[y:C]D≃s = absurd₁ Π[y:C]D≃s
  
  absurd₀ : ∀ {Γ s x A B} → ¬(Γ ⊢ₛ c s ∶ Π[ x ∶ A ] B)
  absurd₀ Γ⊢s:Π[x:A]B with genSort Γ⊢s:Π[x:A]B
  ... | _ , _ , _ , Π[x:A]B≃s = absurd₁ Π[x:A]B≃s

  mutual 
    data Nf : Λ → Set where
      sort : ∀ {s} → Nf (c s)
      abs : ∀ {x A M} → Nf A → Nf M → Nf (λ[ x ∶ A ] M)
      prod : ∀ {x A B} → Nf A → Nf B → Nf (Π[ x ∶ A ] B)
      neu : ∀ {x M} → Ne x M → Nf M

    data Ne (x : 𝒱) : Λ → Set where
      var : Ne x (v x)
      app : ∀ {M N} → Ne x M → Nf N → Ne x (M · N)

  nf : Λ → Set
  nf M = ∀ {N} → ¬(M →β N)

  ne : Λ → Set
  ne (v x) = ⊤
  ne (M · N) = ne M × nf N
  ne _ = ⊥

  -- inversion lemmas for nf
  
  nfApp : ∀ {M N} → nf (M · N) → nf M × nf N
  nfApp nfMN = (λ M→M' → ⊥-elim (nfMN (→·L M→M'))) , (λ N→N' → ⊥-elim (nfMN (→·R N→N')))

  nfAbs : ∀ {x A M} → nf (λ[ x ∶ A ] M) → nf A × nf M
  nfAbs nfλ[x:A]M = (λ A→B → ⊥-elim (nfλ[x:A]M (→λL A→B))) , λ M→N → ⊥-elim (nfλ[x:A]M (→λR M→N))

  nfProd : ∀ {x A B} → nf (Π[ x ∶ A ] B) → nf A × nf B
  nfProd nfΠ[x:A]M = (λ A→B → ⊥-elim (nfΠ[x:A]M (→ΠL A→B))) , λ M→N → ⊥-elim (nfΠ[x:A]M (→ΠR M→N))
  
  nf→ne : ∀ M N {Γ A} → Γ ⊢ₛ M · N ∶ A → nf (M · N) → ne M × nf N
  nf→ne M N Γ⊢MN:A _ with genApp Γ⊢MN:A  
  nf→ne (c s) N _ _ | _ , _ , _ , Γ⊢s:Π[x:A']B , _ , _ = ⊥-elim (absurd₀ Γ⊢s:Π[x:A']B)
  nf→ne (v x) N _ nfMN | _ , _ , _ , _ , Γ⊢N:A , _ = tt , λ {P} N→P → (nfMN (→·R N→P))
  nf→ne (λ[ x ∶ A ] M) N _ nfλ[x:A]MN | _ , _ , _ , _ , _ , _ = ⊥-elim (nfλ[x:A]MN (→cxt β))
  nf→ne (Π[ x ∶ A ] B) N _ _ | _ , _ , _ , Γ⊢Π[x:A]B:Π[x':A']B' , _ , _ = ⊥-elim (absurd₋₁ Γ⊢Π[x:A]B:Π[x':A']B')
  nf→ne (M · N) P _ nfMNP | _ , _ , _ , Γ⊢MN:Π[x:A]B , _ , _ with nfApp nfMNP
  ... | nfMN , nfP with nf→ne M N Γ⊢MN:Π[x:A]B nfMN
  ... | neM , nfN = (neM , nfN) , nfP

  -- soundness of nf

  mutual
    soundNf : ∀ {M} → Nf M → nf M
    soundNf sort (→cxt ())
    soundNf (abs NfA NfM) (→λL A→B) = soundNf NfA A→B
    soundNf (abs NfA NfM) (→λR M→N) = soundNf NfM M→N
    soundNf (prod NfA NfM) (→ΠL A→B) = soundNf NfA A→B
    soundNf (prod NfA NfM) (→ΠR M→N) = soundNf NfM M→N
    soundNf (neu NeM) = soundNe NeM
    
    soundNe : ∀ {x M} → Ne x M → nf M
    soundNe var (→cxt ())
    soundNe (app () NfN) (→cxt β)
    soundNe (app NeM NfN) (→·L M→M') = soundNe NeM M→M'
    soundNe (app NeM NfN) (→·R N→N') = soundNf NfN N→N'
    
  -- renamings

  nfCompatRen : ∀ {M ρ} → Ren ρ → nf M → nf (M ∙ ρ)
  nfCompatRen {c _} _ _ (→cxt ())
  nfCompatRen {v x} {ρ} ren _ with ρ x | ren x
  ... | .(v y) | isVar {y} = λ {(→cxt ())}
  nfCompatRen {λ[ x ∶ A ] M} ren nfλ[x:A]M (→λL Aρ→B) = nfCompatRen ren (proj₁ (nfAbs nfλ[x:A]M)) Aρ→B
  nfCompatRen {λ[ x ∶ A ] M} ren nfλ[x:A]M (→λR Mρ,x=y→N) = nfCompatRen (updRen ren) (proj₂ (nfAbs nfλ[x:A]M)) Mρ,x=y→N
  nfCompatRen {Π[ x ∶ A ] M} ren nfΠ[x:A]M (→ΠL Aρ→B) = nfCompatRen ren (proj₁ (nfProd nfΠ[x:A]M)) Aρ→B
  nfCompatRen {Π[ x ∶ A ] M} ren nfΠ[x:A]M (→ΠR Mρ,x=y→N) = nfCompatRen (updRen ren) (proj₂ (nfProd nfΠ[x:A]M)) Mρ,x=y→N
  nfCompatRen {M · N} ren nfMN (→·L M→M') = nfCompatRen ren (proj₁ (nfApp nfMN)) M→M'
  nfCompatRen {M · N} ren nfMN (→·R N→N') = nfCompatRen ren (proj₂ (nfApp nfMN)) N→N'
  nfCompatRen {(λ[ x ∶ A ] M) · N} {ρ} ren nfλ[x:A]MN (→cxt β) = ⊥-elim (nfλ[x:A]MN (→cxt β))
  nfCompatRen {v x · _} {ρ} ren nfMN (→cxt _) with ρ x | ren x
  nfCompatRen {v x · _} ren nfMN (→cxt ()) | .(v y) | isVar {y}

  mutual
    renameNf : ∀ {M ρ} → Ren ρ → Nf M → Nf (M ∙ ρ)
    renameNf ren sort = sort
    renameNf ren (abs NfA NfM) = abs (renameNf ren NfA) (renameNf (updRen ren) NfM)
    renameNf ren (prod NfA NfB) = prod (renameNf ren NfA) (renameNf (updRen ren) NfB)
    renameNf ren (neu NeM) = neu (proj₂ (renameNe ren NeM))

    renameNe : ∀ {x ρ M} → Ren ρ → Ne x M → ∃ λ y → Ne y (M ∙ ρ)
    renameNe {x} {ρ} ren var with ρ x | ren x
    ... | .(v y) | isVar {y} = y , var
    renameNe ren (app NeM NfN) with renameNe ren NeM
    ... | y , NeMρ = y , app NeMρ (renameNf ren NfN)
    
  mutual
    antiRenameNf : ∀ {M ρ} → Ren ρ → Nf (M ∙ ρ) → Nf M
    antiRenameNf {v x} {ρ} ren Nfxρ with ρ x | ren x
    antiRenameNf {v x} {ρ} ren (neu var) | .(v y) | isVar {y} = neu var
    antiRenameNf {c _} ren sort = sort
    antiRenameNf {λ[ x ∶ A ] M} ren (abs NfA NfM) = abs (antiRenameNf ren NfA) (antiRenameNf (updRen ren) NfM)
    antiRenameNf {Π[ x ∶ A ] B} ren (prod NfA NfB) = prod (antiRenameNf ren NfA) (antiRenameNf (updRen ren) NfB)
    antiRenameNf {M} ren (neu NeM) =  neu (proj₂ (antiRenameNe ren NeM))

    antiRenameNe : ∀ {x ρ M} → Ren ρ → Ne x (M ∙ ρ) → ∃ λ y → Ne y M
    antiRenameNe {x} {ρ} {v x'} ren Nex with ρ x' | ren x'
    antiRenameNe {.y} {ρ} {v x} ren var | .(v y) | isVar {y} = x , var
    antiRenameNe {_} {ρ} {M · N} ren (app NeM NfN) with antiRenameNe ren NeM
    ... | y , NeMρ = y , app NeMρ (antiRenameNf ren NfN)
    
  -- completeness of Nf
    
  mutual
    completeNe : ∀ {M Γ A} → Γ ⊢ₛ M ∶ A → ne M → ∃ λ x → Ne x M
    completeNe (⊢var {x} _ _) neM = x , var
    completeNe (⊢app Γ⊢M:Π[x:A]B Γ⊢N:A) (neM , nfM) with completeNe Γ⊢M:Π[x:A]B neM
    ... | x , NeM = x , app NeM (completeNf Γ⊢N:A nfM)
    completeNe (⊢conv Γ⊢M:B _ _) neM = completeNe Γ⊢M:B neM

    completeNf : ∀ {Γ M A} → Γ ⊢ₛ M ∶ A → nf M → Nf M
    completeNf (⊢sort _ _) _ = sort 
    completeNf (⊢var _ _) _ = neu var
    completeNf {Γ} (⊢abs {x} {x'} {y} {A = A} {_} {M} _ _ _ Γ⊢A:s₁ Γ,y:A⊢M[x=y]:B[x'=y] _) nfλ[x:A]M =
      abs (completeNf Γ⊢A:s₁ (proj₁ (nfAbs nfλ[x:A]M))) NfM
      where
      nfM[x=y] : nf (M [ x := v y ])
      nfM[x=y] = nfCompatRen unaryRename (proj₂ (nfAbs nfλ[x:A]M))
      NfM[x=y] : Nf (M [ x := v y ])
      NfM[x=y] = completeNf Γ,y:A⊢M[x=y]:B[x'=y] nfM[x=y]
      NfM : Nf M
      NfM = antiRenameNf unaryRename NfM[x=y]
    completeNf (⊢prod {x} {y} {B = B} _ Γ⊢A:s₁ _ Γ,y:A⊢B[x=y]:s₂) nfΠ[x:A]B = 
      prod (completeNf Γ⊢A:s₁ (proj₁ (nfProd nfΠ[x:A]B))) NfB
      where
      nfB[x=y] : nf (B [ x := v y ])
      nfB[x=y] = nfCompatRen unaryRename (proj₂ (nfProd nfΠ[x:A]B))
      NfB[x=y] : Nf (B [ x := v y ])
      NfB[x=y] = completeNf Γ,y:A⊢B[x=y]:s₂ nfB[x=y]
      NfB : Nf B
      NfB = antiRenameNf unaryRename NfB[x=y]    
    completeNf {_} {M · N} Γ⊢MN:A@(⊢app Γ⊢M:Π[x:A]B Γ⊢N:A) nfMN with nf→ne M N Γ⊢MN:A nfMN 
    ... | neM , nfN  = neu (app (proj₂ (completeNe Γ⊢M:Π[x:A]B neM)) (completeNf Γ⊢N:A nfN))
    completeNf (⊢conv Γ⊢M:B _ _) nfM = completeNf Γ⊢M:B nfM
  
  NfConvSort : ∀ {A s} → nf A → A ≃β c s → A ≡ c s
  NfConvSort _ A≃s with CR2 A≃s
  ... | B , C , A→*B , s→*C , B∼C with reduceConst s→*C
  NfConvSort {.(c s)} {s} _ A≃s | .(c s) , .(c s) , ε , s→*s , ∼c | refl = PEq.refl
  NfConvSort {A} {s} nfA A≃s | .(c s) , .(c s) , A→D ◅ _ , s→*s , ∼c | refl = ⊥-elim (nfA A→D)
  
  headFunctional : ∀ {Γ x M N A} → Ne x M → Γ ⊢ₛ M · N ∶ A → ∃₄ λ y B C D → (x , B) ∈ Γ × B ≃β Π[ y ∶ C ] D
  headFunctional var Γ⊢xM:A with genApp Γ⊢xM:A
  ... | y , C , D , Γ⊢x:Π[y:C]D , _ , _ with genVar Γ⊢x:Π[y:C]D
  ... | E , _ , x,E∈Γ , Π[y:C]D≃E = y , E , C , D , x,E∈Γ , Eq.symmetric (_∼α_ ∪ _→β_) Π[y:C]D≃E
  headFunctional (app NeM _) Γ⊢MPN:A with genApp Γ⊢MPN:A
  ... | _ , _ , _ , Γ⊢MP:B , _ , _ = headFunctional NeM Γ⊢MP:B