module fin where

open import Data.Product
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Relation.Binary.PropositionalEquality

open import Function

open import SPF ℕ as SPF

finCode : SPF
finCode =    non-ind ℕ (λ n → done (suc n))
        +SPF non-ind ℕ (λ n → ind ⊤ (λ _ → n) (done (suc n)))

Fin : ℕ → Set
Fin = D finCode

fz : (n : ℕ) → Fin (suc n)
fz n = inn (true , n , refl)

fs : (n : ℕ) → Fin n → Fin (suc n)
fs n k = inn (false , n , ((λ _ → k) , refl))

private
  finCode' : SPF
  finCode' = non-ind ℕ (λ n → done (suc n) +SPF ind ⊤ (λ _ → n) (done (suc n)))

  Fin' : ℕ → Set
  Fin' = D finCode'

  fz' : (n : ℕ) → Fin' (suc n)
  fz' n = inn (n , true , refl)

  fs' : (n : ℕ) → Fin' n → Fin' (suc n)
  fs' n k = inn (n , false , ((λ _ → k) , refl))

sum : (n : ℕ) → (Fin n -> ℕ) → ℕ
sum zero f = 
sum (suc n) f = f (fz _) + sum n (f ∘ (fs _))

prod : (n : ℕ) → (Fin n -> ℕ) → ℕ
prod zero f = 
prod (suc n) f = f (fz _) * prod n (f ∘ (fs _))


mutual

  data FinType : Set where
    fin : ℕ → FinType
    _×f_ : FinType → FinType → FinType
    _+f_ : FinType → FinType → FinType
    σ : (a : FinType) → (Fin (size a) → FinType) → FinType
    π : (a : FinType) → (Fin (size a) → FinType) → FinType

  size : FinType → ℕ
  size (fin n) = n
  size (a ×f b) = size a * size b
  size (a +f b) = size a + size b
  size (σ a b) = sum (size a) (size ∘ b)
  size (π a b) = prod (size a) (size ∘ b)

  -- reduction to inductive family
data FinType' : ℕ → Set where
  fin : (n : ℕ) → FinType' n
  _×f_ : (n : ℕ) → FinType' n → (m : ℕ) → FinType' m → FinType' (n * m)
  _+f_ : (n : ℕ) → FinType' n → (m : ℕ) → FinType' m → FinType' (n + m)
  σ : (n : ℕ) → (a : FinType' n) → (m : Fin n → ℕ) → ((x : Fin n) → FinType' (m x)) → FinType' (sum n m)
  π : (n : ℕ) → (a : FinType' n) → (m : Fin n → ℕ) → ((x : Fin n) → FinType' (m x)) → FinType' (prod n m)

⟦FinType⟧ : Set
⟦FinType⟧ = Σ ℕ FinType'

⟦size⟧ : ⟦FinType⟧ → ℕ
⟦size⟧ = proj₁

⟦fin⟧ : ℕ → ⟦FinType⟧
⟦fin⟧ n = (n , fin n)

_⟦×f⟧_ : ⟦FinType⟧ → ⟦FinType⟧ → ⟦FinType⟧
(n , a) ⟦×f⟧ (m , b) = n * m , _×f_ n a m b

_⟦+f⟧_ : ⟦FinType⟧ → ⟦FinType⟧ → ⟦FinType⟧
(n , a) ⟦+f⟧ (m , b) = n + m , _+f_ n a m b

⟦σ⟧ : (a : ⟦FinType⟧) → (Fin (⟦size⟧ a) → ⟦FinType⟧) → ⟦FinType⟧
⟦σ⟧ (n , a) b = (sum n (proj₁ ∘ b)) , (σ n a (proj₁ ∘ b) (proj₂ ∘ b))

⟦π⟧ : (a : ⟦FinType⟧) → (Fin (⟦size⟧ a) → ⟦FinType⟧) → ⟦FinType⟧
⟦π⟧ (n , a) b = (prod n (proj₁ ∘ b)) , (π n a (proj₁ ∘ b) (proj₂ ∘ b))

-- Equations hold on the nose
_ : ∀ {n} → ⟦size⟧ (⟦fin⟧ n) ≡ n
_ = refl

_ : ∀ {a b} → ⟦size⟧ (a ⟦×f⟧ b) ≡ ⟦size⟧ a * ⟦size⟧ b
_ = refl

_ : ∀ {a b} → ⟦size⟧ (a ⟦+f⟧ b) ≡ ⟦size⟧ a + ⟦size⟧ b
_ = refl

_ : ∀ {a b} → ⟦size⟧ (⟦σ⟧ a b) ≡ sum (⟦size⟧ a) (⟦size⟧ ∘ b)
_ = refl

_ : ∀ {a b} → ⟦size⟧ (⟦π⟧ a b) ≡ prod (⟦size⟧ a) (⟦size⟧ ∘ b)
_ = refl