{-# OPTIONS --erased-cubical #-}
module Comparision.Hardy where

open import Cubical.Foundations.Prelude

open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_+_; _<_)
open import Agda.Builtin.List using (List; []; _∷_)
open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit

open import PropTrunc

open import BrouwerTree.Core
open import BrouwerTree.Properties.Core
open import BrouwerTree.Arithmetic.Addition

-- Cubical Agda gets stuck transporting in inductive families, so we
-- reimplement the parts of CNF that we need with pure propositional
-- equality, without cubical features
import CantorNormalForm.WithPropositionalEquality.Hardy as CNF
import CantorNormalForm.WithPropositionalEquality.Base as CNF
import CantorNormalForm.WithPropositionalEquality.Addition as CNF


hardy : Brw → ℕ → ∥ ℕ ∥
hardy zero n = ∣ n ∣
hardy (Brw.succ a) n = hardy a (suc n)
hardy (limit f) n = hardy (f n) n
hardy (bisim f {f↑} g {g↑} f∼g i) = λ n → squash  (hardy (f n) n) (hardy (g n) n) i
hardy (trunc x y p q i j) n =
  hcomp (λ { k (i = i0) → squash (hardy x n) (hardy (p j) n) k
           ; k (i = i1) → squash (hardy x n) (hardy (q j) n) k
           ; k (j = i0) → squash (hardy x n) (hardy x n) k
           ; k (j = i1) → squash (hardy x n) (hardy y n) k
           }) (hardy x n)

-- To be able to use --erased-cubical, we reimplement some of the
-- features we need of Brouwer trees that rely on files from the cubical
-- library not declared to work in --erased-cubical
mutual
  ω·_ : Brw → Brw
  ω· zero = zero
  ω· (succ y) = (ω· y) + ω
  ω· (limit f {f↑}) = limit (λ n → ω· f n) {ω·-increasing f↑}
  ω· bisim f {f↑} g {g↑} (f≲g , g≲f) i =
    bisim (λ n → ω· f n) {ω·-increasing f↑}
          (λ n → ω· g n) {ω·-increasing g↑}
          (ω·-preserves-≲ f≲g , ω·-preserves-≲ g≲f) i
  (ω· trunc x y p q i j) =
    trunc (ω· x) (ω· y) (λ j → ω· (p j)) (λ j → ω· (q j)) i j

  ω·-mono : ∀ {y z : Brw} → y ≤ z → (ω· y) ≤ (ω· z)
  ω·-mono ≤-zero = ≤-zero
  ω·-mono (≤-trans p q) = ≤-trans (ω·-mono p) (ω·-mono q)
  ω·-mono (≤-succ-mono {x} {y} p) =
    ≤-limiting _ (λ k → ≤-cocone _ {k = k} (+x-mono (ι k) (ω·-mono p)))
  ω·-mono (≤-cocone f p) = ≤-cocone (λ n → ω· f n) (ω·-mono p)
  ω·-mono (≤-limiting f p) = ≤-limiting (λ n → ω· f n) (λ k → ω·-mono (p k))
  ω·-mono (≤-trunc p q i) = ≤-trunc (ω·-mono p) (ω·-mono q) i

  ω·-mono-< : {y z : Brw} → y < z → (ω· y) < (ω· z)
  ω·-mono-< p = ≤-trans (≤-cocone _ {k = } ≤-refl) (ω·-mono p)

  ω·-increasing : ∀ {f} → increasing f → increasing (λ n → ω· f n)
  ω·-increasing {f} f↑ k = ω·-mono-< (f↑ k)

  {-# TERMINATING #-}
  ω·-preserves-≲ : ∀ {f g} → f ≲ g → (λ n → ω· f n) ≲ (λ n → ω· g n)
  ω·-preserves-≲ f≲g k = ∥-∥rec isPropPropTrunc (λ { (l , fk≤gl) → ∣ l , ω·-mono fk≤gl ∣ }) (f≲g k)

ω^⟨_⟩ : ℕ → Brw
ω^⟨ zero ⟩ = one
ω^⟨ suc n ⟩ = ω· ω^⟨ n ⟩

postulate
  return : ∀ {a} {A : Type a} → A → IO A
  _>>=_  : ∀ {a b} {A : Type a} {B : Type b} → IO A → (A → IO B) → IO B
  putStr      : String → IO ⊤
  putStrLn    : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text    as T   #-}
{-# FOREIGN GHC import qualified Data.Text.IO as TIO #-}
{-# COMPILE GHC putStr     = TIO.putStr                #-}
{-# COMPILE GHC putStrLn   = TIO.putStrLn              #-}

_>>_  : ∀ {a b} {A : Type a} {B : Type b} → IO A → IO B → IO B
ma >> mb = ma >>= (λ _ → mb)

{-# COMPILE GHC return = \_ _ -> return    #-}
{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}


printTrunc : ∥ ℕ ∥ -> IO {Agda.Primitive.lzero} ⊤
printTrunc ∣ x ∣ = putStrLn (primShowNat x)
printTrunc (squash x y i) = admitIO⊤≡ (printTrunc x) (printTrunc y) i where
  -- For printing purposes, we can happily postulate that all IO actions
  -- are equal
  postulate
    admitIO⊤≡ : (p q : IO ⊤) → p ≡ q


{-# FOREIGN GHC import Criterion.Main #-}

postulate
  Benchmarkable : Set
  Benchmark     : Set
  whnf          : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → A → Benchmarkable
  whnfIO        : ∀ {a} {A : Set a} → IO A → Benchmarkable
  bench         : String → Benchmarkable → Benchmark
  bgroup        : String → List Benchmark → Benchmark
  defaultMain   : List Benchmark → IO ⊤

{-# COMPILE GHC Benchmarkable = type Criterion.Main.Benchmarkable #-}
{-# COMPILE GHC Benchmark     = type Criterion.Main.Benchmark     #-}

{-# COMPILE GHC whnf   = \ _ _ _ _ -> Criterion.Main.whnf   #-}
{-# COMPILE GHC whnfIO = \ _ _     -> Criterion.Main.whnfIO #-}

{-# COMPILE GHC bench  = Criterion.Main.bench  . Data.Text.unpack #-}
{-# COMPILE GHC bgroup = Criterion.Main.bgroup . Data.Text.unpack #-}

{-# COMPILE GHC defaultMain = Criterion.Main.defaultMain #-}

sizes =  ∷  ∷  ∷  ∷  ∷  ∷  ∷ []
sizesCNF =  ∷  ∷  ∷  ∷  ∷  ∷  ∷  ∷  ∷  ∷ []

main : IO {Agda.Primitive.lzero} ⊤
main = defaultMain
  ((bgroup "Brw" (map (λ n → bench (show n) (whnf (hardy ω^⟨ n ⟩) )) sizes)) ∷
  (bgroup "Cnf" (map (λ n → bench (show n) (whnf (CNF.hardy CNF.ω^⟨ CNF.NtoC n ⟩) )) sizesCNF)) ∷
  [])
  where
    show = primShowNat
    map : {A B : Set} → (A → B) → List A → List B
    map f [] = []
    map f (a ∷ as) = f a ∷ map f as

-- This relies on the Criterion Haskell library for benchmarking. To install it, run
--
--   cabal install --lib criterion
--
-- in a terminal.