module Examples.NF.Sigma where

open import Data.Unit
open import Data.Empty
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Bool hiding (T)

open import Relation.Binary.PropositionalEquality


F0 : (U : Set)(T : U -> Set) -> Set
F0 U T = Bool ⊎ (Σ[ u ∈ U ] (T u -> U))

F1 : (U : Set)(T : U -> Set) -> F0 U T -> Set
F1 U T (inj₁ true) = ⊤
F1 U T (inj₁ false) = ℕ
F1 U T (inj₂ (a , b)) = Σ[ x ∈ (T a) ] T (b x)

pattern ⊤'' = (inj₁ true)

pattern ℕ'' = (inj₁ false)

pattern Σ'' a b = (inj₂ (a , b))


mutual

  data U : Set where
    ⊤' : U
    ℕ' : U
    Σ' : (a : U) -> (T a -> U) -> U

  T : U -> Set
  T ⊤' = ⊤
  T ℕ' = ℕ
  T (Σ' a b) = Σ[ x ∈ (T a) ] T (b x)

_≠⊤ : U -> Set
⊤' ≠⊤ = ⊥
x ≠⊤ = ⊤

-- Normal forms are ⊤, ℕ or right-nested sigmas without ⊤
NF : U -> Set
NF (Σ' ℕ' b) = (x : T ℕ') -> NF (b x) 
NF ⊤' = ⊤
NF ℕ' = ⊤
NF (Σ' ⊤' b) = ⊥
NF (Σ' (Σ' a' b') b) = ⊥
--NF (Σ' a b) = (x : T a) -> b x ≠⊤ × NF (b x) 



not-Σ-right-NF : ∀ {a b c} -> NF (Σ' (Σ' a b) c)  -> ⊥
not-Σ-right-NF {⊤'} ()
not-Σ-right-NF {ℕ'} ()
not-Σ-right-NF {Σ' a b} ()

UNF : Set
UNF = Σ[ u ∈ U ] (NF u)

TNF : UNF -> Set
TNF (u , p) = T u

{-# TERMINATING #-} -- The termination checker is not happy about
                    -- the higher-orderness of the recursive call 
                    -- φ ... (λ y → b (n , y))
φ : F0 UNF TNF -> UNF
φ ⊤'' = ⊤' , _
φ ℕ'' = ℕ' , _
φ (Σ'' (⊤' , p) b) = proj₁ (b _) , proj₂ (b _)
φ (Σ'' (ℕ' , p) b) = Σ' ℕ' (λ n → proj₁ (b n)) , (λ n → proj₂ (b n))
φ (Σ'' (Σ' ℕ' b' , p) b) = Σ' ℕ' (λ n → proj₁ (φ (Σ'' (b' n , p n) (λ y → b (n , y))))) , (λ n → proj₂ (φ (Σ'' (b' n , p n) (λ y → b (n , y)))))
φ (Σ'' (Σ' (Σ' _ _) b' , ()) b)
φ (Σ'' (Σ' ⊤' b' , ()) b)

{-# TERMINATING #-}
η : (x : F0 UNF TNF) -> F1 UNF TNF x -> TNF (φ x)
η ⊤'' y = y
η ℕ'' y = y
η (Σ'' (⊤' , p) b) (_ , y) = y
η (Σ'' (ℕ' , p) b) (n , y) = (n , y)
η (Σ'' (Σ' ℕ' b' , p) b) ((n , y) , z) = n , η (Σ'' (b' n , p n) (λ y → b (n , y))) (y , z)
η (Σ'' (Σ' (Σ' _ _) b' , ()) b)
η (Σ'' (Σ' ⊤' b' , ()) b)

{-# TERMINATING #-}
η⁻¹ : (x : F0 UNF TNF) -> TNF (φ x) -> F1 UNF TNF x
η⁻¹ ⊤'' y = y
η⁻¹ ℕ'' y = y
η⁻¹ (Σ'' (⊤' , p) b) y = (_ , y)
η⁻¹ (Σ'' (ℕ' , p) b) (n , y) = (n , y)
η⁻¹ (Σ'' (Σ' ℕ' b' , p) b) (n , y) = let (y' , z) = η⁻¹ (Σ'' (b' n , p n) (λ y → b (n , y))) y in (n , y') , z
η⁻¹ (Σ'' (Σ' (Σ' _ _) b' , ()) b)
η⁻¹ (Σ'' (Σ' ⊤' b' , ()) b)

{-# TERMINATING #-}
η∘η⁻¹=id : (x : F0 UNF TNF) -> (y : TNF (φ x)) -> η x (η⁻¹ x y) ≡ y
η∘η⁻¹=id ⊤'' y = refl
η∘η⁻¹=id ℕ'' y = refl
η∘η⁻¹=id (Σ'' (⊤' , p) b) y = refl
η∘η⁻¹=id (Σ'' (ℕ' , p) b) (n , y) = refl
η∘η⁻¹=id (Σ'' (Σ' ℕ' b' , p) b) (n , y) rewrite η∘η⁻¹=id (Σ'' (b' n , p n) (λ y → b (n , y))) y = refl
η∘η⁻¹=id (Σ'' (Σ' (Σ' _ _) b' , ()) b)
η∘η⁻¹=id (Σ'' (Σ' ⊤' b' , ()) b)

{-# TERMINATING #-}
η⁻¹∘η=id : (x : F0 UNF TNF) -> (y : F1 UNF TNF x) -> (η⁻¹ x (η x y)) ≡ y
η⁻¹∘η=id ⊤'' y = refl
η⁻¹∘η=id ℕ'' y = refl
η⁻¹∘η=id (Σ'' (⊤' , p) b) (_ , y) = refl
η⁻¹∘η=id (Σ'' (ℕ' , p) b) (n , y) = refl
η⁻¹∘η=id (Σ'' (Σ' ℕ' b' , p) b) ((n , y) , z) rewrite η⁻¹∘η=id ((Σ'' (b' n , p n) (λ y → b (n , y)))) ((y , z)) = refl
η⁻¹∘η=id (Σ'' (Σ' (Σ' _ _) b' , ()) b)
η⁻¹∘η=id (Σ'' (Σ' ⊤' b' , ()) b)