{-# OPTIONS --cubical #-}

module Data.Binary.Testing where

open import Data.Binary.Increment
open import Data.Binary.Definition
open import Agda.Builtin.List
open import Data.Binary.Helpers
open import Agda.Builtin.Strict

force : š”¹ ā†’ š”¹
force 0įµ‡ = 0įµ‡
force (1įµ‡ xs) = primForce (force xs) 1įµ‡_
force (2įµ‡ xs) = primForce (force xs) 2įµ‡_

incā€² : š”¹ ā†’ š”¹
incā€² 0įµ‡ = 1įµ‡ 0įµ‡
incā€² (1įµ‡ xs) = 2įµ‡ xs
incā€² (2įµ‡ xs) = primForce (incā€² xs) 1įµ‡_

up-to : ā„• ā†’ List š”¹
up-to = go 0įµ‡
  where
  go : š”¹ ā†’ ā„• ā†’ List š”¹
  go i zero    = []
  go i (suc n) = primForce i Ī» i ā†’ i āˆ· go (incā€² i) n

up-toā€² : ā„• ā†’ List ā„•
up-toā€² = go zero
  where
  go : ā„• ā†’ ā„• ā†’ List ā„•
  go i zero = []
  go i (suc n) = i āˆ· go (suc i) n

module _ {A : Set} (f : A ā†’ A ā†’ A) where
  combā€² : A ā†’ List A ā†’ List A ā†’ List A
  combā€² x []       zs = zs
  combā€² x (y āˆ· ys) zs = f x y āˆ· combā€² x ys zs

  comb : List A ā†’ List A ā†’ List A
  comb []       ys = []
  comb (x āˆ· xs) ys = combā€² x ys (comb xs ys)

forces : List š”¹ ā†’ List š”¹
forces [] = []
forces (x āˆ· xs) = primForce (force x) Ī» xā€² ā†’ primForce (forces xs) Ī» xsā€² ā†’ xā€² āˆ· xsā€²

open import Data.Binary.Conversion.Fast
open import Data.Binary.Properties.Helpers using (_ā‰”_; refl) public
open import Agda.Builtin.Bool using (true)

perf-test : (š”¹ ā†’ š”¹ ā†’ š”¹) ā†’ ā„• ā†’ Set
perf-test f n = true ā‰” primForce (forces (comb f (up-to n) (up-to n))) (Ī» _ ā†’ true) 

map : {A B : Set} ā†’ (A ā†’ B) ā†’ List A ā†’ List B
map _ [] = []
map f (x āˆ· xs) = f x āˆ· map f xs

test : (š”¹ ā†’ š”¹ ā†’ š”¹) ā†’ (ā„• ā†’ ā„• ā†’ ā„•) ā†’ ā„• ā†’ Set
test f g n =
  let xs = comb f (up-to n) (up-to n)
      ys = comb g (up-toā€² n) (up-toā€² n)
  in xs ā‰” forces (map āŸ¦_ā‡‘āŸ§ ys)