{-# OPTIONS --erased-cubical #-}
module CantorNormalForm.WithPropositionalEquality.Hardy where

open import Agda.Builtin.Nat renaming (Nat to ℕ)

open import CantorNormalForm.WithPropositionalEquality.Base
open import CantorNormalForm.WithPropositionalEquality.Classifiability

open import PropTrunc

φ₀ : ℕ → ∥ ℕ ∥
φ₀ = λ k → ∣ k ∣

φₛ : (ℕ → ∥ ℕ ∥) → ℕ → ∥ ℕ ∥
φₛ = λ g n → g (suc n)

φₗ : (ℕ → ℕ → ∥ ℕ ∥) → ℕ → ∥ ℕ ∥
φₗ = λ h n → h n n

hardy : Cnf → ℕ → ∥ ℕ ∥
hardy = transfinite-rec φ₀ φₛ φₗ

{-
hardy zero n = ∣ n ∣
hardy (succ a) n = hardy a (suc n)
hardy (limit f) n = hardy (f n) n
-}


{-
-- "Higher-order" hierarchy from http://www-compsci.swan.ac.uk/~csulrich/ftp/fast.txt

τ : ℕ → Set
τ zero = ℕ → ∥ ℕ ∥
τ (suc n) = τ n → τ n

r : (n : ℕ) → (ℕ → τ n) → τ n
r zero = φₗ
r (suc n) u v = r n (λ k → u k v)

t : (n : ℕ) → τ n
t zero = φ₀
t (suc zero) = φₛ
t (suc (suc n)) v v' = r n (λ k → iter k v v')

t[_,_] : (n : ℕ) → Cnf → τ n
t[ n , 𝟎 ] = t n
t[ n , ω^ a + b [ r ] ] = t[ suc n , a ] t[ n , b ]

hardy-higher : Cnf → ℕ → ∥ ℕ ∥
hardy-higher x = t[ 0 , x ]
-}

n = 
m = 
-- testC  = hardy-higher (ω^⟨ NtoC n ⟩)  m
testC2 = hardy (ω^⟨ NtoC n ⟩)  m

-- As n increases, testC becomes more efficient, but the difference to testC2 is not big.

-- Fixing n = 2, as m inreases, the difference between testC and testC2 becomes bigger.
-- Try n = 2 and m = 15.