module Examples.NF.Prod 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)


F0 : (U : Set)(T : U -> Set) -> Set
F0 U T = Bool ⊎ 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)) = T a × T b

pattern ⊤'' = (inj₁ true)

pattern ℕ'' = (inj₁ false)

pattern _×''_ a b = (inj₂ (a , b))


mutual

  data U : Set where
    ⊤' : U
    ℕ' : U
    _×'_ : U -> U -> U

  T : U -> Set
  T ⊤' = ⊤
  T ℕ' = ℕ
  T (a ×' b) = T a × T b


-- Normal forms are ⊤, ℕ or left-nested products without ⊤
NF : U -> Set
NF (a ×' ℕ') = NF a
NF ⊤' = ⊤
NF ℕ' = ⊤
NF (⊤' ×' b) = ⊥
NF (a ×' ⊤') = ⊥
NF (a ×' (c ×' d)) = ⊥



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

not-a×⊤-NF : {a : U} -> NF  (a ×' ⊤') -> ⊥
not-a×⊤-NF {⊤'} ()
not-a×⊤-NF {ℕ'} ()
not-a×⊤-NF {a ×' b} ()

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

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

φ : F0 UNF TNF -> UNF
φ ⊤'' = ⊤' , _
φ ℕ'' = ℕ' , _
φ ((⊤' , _) ×'' (b , q)) = b , q
φ ((a , p) ×'' (⊤' , _)) = a , p
φ ((ℕ' , _) ×'' (ℕ' , _)) = ℕ' ×' ℕ' , _
φ ((a , p) ×'' (b ×' ⊤' , q)) = ⊥-elim (not-a×⊤-NF {b} q)
φ ((ℕ' , _) ×'' (b ×' ℕ' , q)) = (b ×' ℕ') ×' ℕ' , q
φ ((a ×' a' , p) ×'' (b ×' ℕ' , q))
  = let (c , r) = φ ((a ×' a' , p) ×'' (b , q)) in c ×' ℕ' , r
φ ((a ×' a' , p) ×'' (ℕ' , _)) = ((a ×' a') ×' ℕ' , p)
φ ((a , p) ×'' (b ×' (b' ×' b'') , q)) = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)


η : (x : F0 UNF TNF) -> F1 UNF TNF x -> TNF (φ x)
η ⊤'' y = y
η ℕ'' y = y
η ((⊤' , p) ×'' b) (_ , y) = y
-- b = ⊤'
η ((ℕ' , p) ×'' (⊤' , _)) (y , _) = y
η ((a ×' a' , p) ×'' (⊤' , _)) (y , _) = y
-- a = ℕ'
η ((ℕ' , p) ×'' (ℕ' , q)) (n , m) = n , m
η ((ℕ' , p) ×'' (⊤' ×' ℕ' , q)) (n , (y , m)) = (y , n) , m
η ((ℕ' , p) ×'' (ℕ' ×' ℕ' , q)) (n , (y , m)) = (y , n) , m
η ((ℕ' , p) ×'' ((b ×' b') ×' ℕ' , q)) (n , (y , m)) = (y , n) , m
-- a = a' ×' a''
η ((a ×' a' , p) ×'' (ℕ' , q)) y = y
η ((a ×' a' , p) ×'' (b ×' ℕ' , q)) (y , (z , n)) = η ((a ×' a' , p) ×'' (b , q))  (y , z) , n
-- Impossible cases
η ((ℕ' , p) ×'' (b ×' (b' ×' b'') , q)) (n , y) = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)
η ((a ×' a' , p) ×'' (b ×' ⊤' , q)) y = ⊥-elim (not-a×⊤-NF {b} q)
η ((ℕ' , p) ×'' (b ×' ⊤' , q)) (n , y) = ⊥-elim (not-a×⊤-NF {b} q)
η ((a ×' a' , p) ×'' (b ×' (b' ×' b'') , q)) y = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)


η⁻¹ : (x : F0 UNF TNF) -> TNF (φ x) -> F1 UNF TNF x
η⁻¹ ⊤'' y = y
η⁻¹ ℕ'' y = y
η⁻¹ ((⊤' , p) ×'' b) y = (_ , y)
-- b = ⊤'
η⁻¹ ((ℕ' , p) ×'' (⊤' , _)) y = (y , _)
η⁻¹ ((a ×' a' , p) ×'' (⊤' , _)) y = (y , _)
-- a = ℕ'
η⁻¹ ((ℕ' , p) ×'' (ℕ' , q)) (n , m) = n , m
η⁻¹ ((ℕ' , p) ×'' (⊤' ×' ℕ' , q)) ((y , n) , m) = (n , (y , m))
η⁻¹ ((ℕ' , p) ×'' (ℕ' ×' ℕ' , q)) ((y , n) , m) = (n , (y , m))
η⁻¹ ((ℕ' , p) ×'' ((b ×' b') ×' ℕ' , q)) ((y , n) , m) = (n , (y , m))
-- a = a' ×' a''
η⁻¹ ((a ×' a' , p) ×'' (ℕ' , q)) y = y
η⁻¹ ((a ×' a' , p) ×'' (b ×' ℕ' , q)) (y , n)
 = let (y' , z) = η⁻¹ ((a ×' a' , p) ×'' (b , q)) y in y' , (z , n)
-- Impossible cases
η⁻¹ ((ℕ' , p) ×'' (b ×' ⊤' , q)) y = ⊥-elim (not-a×⊤-NF {b} q)
η⁻¹ ((a ×' a' , p) ×'' (b ×' ⊤' , q)) y = ⊥-elim (not-a×⊤-NF {b} q)
η⁻¹ ((ℕ' , p) ×'' (b ×' (b' ×' b'') , q)) y = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)
η⁻¹ ((a ×' a' , p) ×'' (b ×' (b' ×' b'') , q)) y = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)

open import Relation.Binary.PropositionalEquality

η∘η⁻¹=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) ×'' (⊤' , _)) y = refl
η∘η⁻¹=id ((a ×' a' , p) ×'' (⊤' , _)) y = refl

η∘η⁻¹=id ((ℕ' , p) ×'' (ℕ' , q)) (n , m) = refl

η∘η⁻¹=id ((ℕ' , p) ×'' (⊤' ×' ℕ' , q)) ((y , n) , m) = refl
η∘η⁻¹=id ((ℕ' , p) ×'' (ℕ' ×' ℕ' , q)) ((y , n) , m) = refl
η∘η⁻¹=id ((ℕ' , p) ×'' ((b ×' b') ×' ℕ' , q)) ((y , n) , m) = refl

η∘η⁻¹=id ((a ×' a' , p) ×'' (ℕ' , q)) y = refl
η∘η⁻¹=id ((a ×' a' , p) ×'' (b ×' ℕ' , q)) (y , n) 
 rewrite η∘η⁻¹=id ((a ×' a' , p) ×'' (b , q)) y = refl
-- Impossible cases
η∘η⁻¹=id ((a ×' a' , p) ×'' (b ×' ⊤' , q)) y = ⊥-elim (not-a×⊤-NF {b} q)
η∘η⁻¹=id ((a ×' a' , p) ×'' (b ×' (b' ×' b'') , q)) y = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)
η∘η⁻¹=id ((ℕ' , p) ×'' (b ×' ⊤' , q)) y = ⊥-elim (not-a×⊤-NF {b} q)
η∘η⁻¹=id ((ℕ' , p) ×'' (b ×' (b' ×' b'') , q)) y = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)

η⁻¹∘η=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) ×'' (⊤' , _)) (y , _) = refl
η⁻¹∘η=id ((a ×' a' , p) ×'' (⊤' , _)) (y , _) = refl

η⁻¹∘η=id ((ℕ' , p) ×'' (ℕ' , q)) (n , m) = refl

η⁻¹∘η=id ((ℕ' , p) ×'' (⊤' ×' ℕ' , q)) (n , (y , m)) = refl
η⁻¹∘η=id ((ℕ' , p) ×'' (ℕ' ×' ℕ' , q)) (n , (y , m)) = refl
η⁻¹∘η=id ((ℕ' , p) ×'' ((b ×' b') ×' ℕ' , q)) (n , (y , m)) = refl

η⁻¹∘η=id ((a ×' a' , p) ×'' (ℕ' , q)) y = refl
η⁻¹∘η=id ((a ×' a' , p) ×'' (b ×' ℕ' , q)) (y , (z , n))
  rewrite η⁻¹∘η=id ((a ×' a' , p) ×'' (b , q))  ((y , z)) = refl
-- Impossible cases
η⁻¹∘η=id ((ℕ' , p) ×'' (b ×' ⊤' , q)) (n , y) = ⊥-elim (not-a×⊤-NF {b} q)
η⁻¹∘η=id ((a ×' a' , p) ×'' (b ×' ⊤' , q)) y = ⊥-elim (not-a×⊤-NF {b} q)
η⁻¹∘η=id ((a ×' a' , p) ×'' (b ×' (b' ×' b'') , q)) y = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)
η⁻¹∘η=id ((ℕ' , p) ×'' (b ×' (b' ×' b'') , q)) (n , y) = ⊥-elim (not-×-right-NF {b} {b'} {b''} q)