{-# OPTIONS --cubical --safe --sized-types --postfix-projections #-}

module Post.Prelude where

open import Agda.Builtin.Size public
open import Agda.Primitive
open import Cubical.Foundations.Prelude public

variable
a b c : Level
A : Type a
B : Type b
C : Type c
i j : Size

open import Agda.Builtin.Sigma public
open import Agda.Builtin.Nat renaming (Nat to )

_×_ : Type a  Type b  Type (a  b)
A × B = Σ A λ _  B

_∘_ : (B  C)  (A  B)  A  C
f  g = λ x  f (g x)

infixr 5 _∷_
data List (A : Type a) : Type a where
[] : List A
_∷_ : A  List A  List A

foldr : (A  B  B)  B  List A  B
foldr f b [] = b
foldr f b (x  xs) = f x (foldr f b xs)

map : (A  B)  List A  List B
map f = foldr  x xs  f x  xs) []

data  : Type lzero where

¬_ : Type a  Type a
¬ A = A

open import Agda.Builtin.Bool using (Bool; true; false) public

data Reflects (A : Type a) : Bool  Type a where
ofʸ :   A  Reflects A true
ofⁿ : ¬ A  Reflects A false

record Dec (A : Type a) : Type a where
constructor _because_
field
does : Bool
why : Reflects A does
open Dec public

pattern yes p = true because ofʸ p
pattern no ¬p = false because ofⁿ ¬p

open import Agda.Builtin.Nat using (suc; zero) renaming (Nat to )
open import Agda.Builtin.Unit

data Maybe (A : Type a) : Type a where
nothing : Maybe A
just : A  Maybe A

Fin :   Type₀
Fin zero =
Fin (suc n) = Maybe (Fin n)

const : A  B  A
const x _ = x

length : List A
length = foldr (const suc) zero

pattern f0 = nothing
pattern fs x = just x

_!_ : (xs : List A)  Fin (length xs)  A
(x  xs) ! f0 = x
(x  xs) ! fs i = xs ! i

: (A  Type b)  Type _
B = Σ _ B

infixr 2 ∃-syntax
∃-syntax : (A  Type b)  Type _
∃-syntax =

syntax ∃-syntax  x  P) = ∃[ x ] P

:  {p}  (A  Type p)  List A  Type p
P xs = Σ[ i  Fin (length xs) ] (P (xs ! i))

_and_ : Bool  Bool  Bool
false and y = false
true and y = y

_or_ : Bool  Bool  Bool
false or y = y
true  or y = true

data _⊎_ (A : Type a) (B : Type b) : Type (a  b) where
inl : A  A  B
inr : B  A  B

_||_ : Dec A  Dec B  Dec (A  B)
(L || R) .does = L .does or R .does
(yes p || R) .why = ofʸ (inl p)
(no ¬p || yes p) .why = ofʸ (inr p)
(no ¬p || no ¬q) .why = ofⁿ λ { (inl x)  ¬p x ; (inr x)  ¬q x}

map-dec : (A  B)  (B  A)  Dec A  Dec B
map-dec to fro xs .does = xs .does
map-dec to fro (yes p) .why = ofʸ (to p)
map-dec to fro (no ¬p) .why = ofⁿ λ x  ¬p (fro x)

either : (A  C)  (B  C)  A  B  C
either f g (inl x) = f x
either f g (inr x) = g x

◇? :  {p} {P : A  Type p}  (∀ x  Dec (P x))   xs  Dec ( P xs)
◇? P? [] = no fst
◇? P? (x  xs) = map-dec (either (_,_ f0) λ (n , x)  fs n , x)  { (f0 , x)  inl x ; (fs x₁ , x)  inr (x₁ , x) }) (P? x || ◇? P? xs)

infixr 5 _∈_
_∈_ : A  List A  Type _
x  xs =  (_≡ x) xs

Discrete : Type a  Type a
Discrete A = (x y : A)  Dec (x  y)

record IsDiscrete (A : Type a) : Type a where
field _≟_ : Discrete A
open IsDiscrete  ...  public

_∈?_ :   _ : IsDiscrete A   (x : A) (xs : List A)  Dec (x  xs)
x ∈? xs = ◇? (_≟ x) xs

id : A  A
id x = x

maybe : B  (A  B)  Maybe A  B
maybe b f nothing = b
maybe b f (just x) = f x

just-inj :  (x y : A)  just x  just y  x  y
just-inj x y = cong (maybe x id)

discreteFin :  {n} (x y : Fin n)  Dec (x  y)
discreteFin {suc n} f0 f0 = yes refl
discreteFin {suc n} f0 (fs x) = no λ p  subst (maybe  (const )) p tt
discreteFin {suc n} (fs x) f0 = no λ p  subst (maybe  (const )) p tt
discreteFin {suc n} (fs x) (fs y) = map-dec (cong fs) (just-inj x y) (discreteFin x y)

T : Bool  Type₀
T true  =
T false =

not : Bool  Bool
not false = true
not true = false

_≢ᶠ_ :  {n}  Fin n  Fin n  Type₀
x ≢ᶠ y = T (not (does (discreteFin x y)))

Dup : List A  Type _
Dup xs = ∃[ x ] Σ[ i  (x  xs) ] Σ[ j  (x  xs) ] (i .fst ≢ᶠ j .fst)

data NoethAcc {a} {A : Type a} (xs : List A) : Type a where
stop : Dup xs  NoethAcc xs
step : (∀ x  NoethAcc (x  xs))  NoethAcc xs

Noeth : Type a  Type a
Noeth A = NoethAcc {A = A} []

data Braun (A : Type a) : Type a where
leaf : Braun A
node : A  Braun A  Braun A  Braun A

-- infixr 5 _◂_
-- data Colist (A : Type a) (i : Size) : Type a where
--   [] : Colist A i
--   _◂_ : A → Thunk (Colist A) i → Colist A i

-- levels : Stream (List A) i → Colist (A × List A) i
-- levels xs with xs .head
-- levels xs | [] = []
-- levels xs | y ∷ ys = (y , ys) ◂ λ where .force → levels (xs .tail)

-- app : List A → Colist A i → Colist A i
-- app [] ys = ys
-- app (x ∷ xs) ys = x ◂ λ where .force → app xs ys

-- concat : Colist (A × List A) i → Colist A i
-- concat [] = []
-- concat ((x , xt) ◂ xs) = x ◂ λ where .force → app xt (concat (xs .force))

-- toList : ∀ {xs : List A} → NoethAcc xs → Colist A ∞ → List A
-- toList f [] = []
-- toList (stop _) _ = []
-- toList (step f) (x ◂ xs) = x ∷ toList (f x) (xs .force)

-- ◻ : ∀ {p} → (A → Type p) → List A → Type p
-- ◻ P xs = ∀ n → P (xs ! n)

-- -- module _ {a} {A : Type a} where
-- --   Noeth→DecEq : Noeth A → (x y : A) → Dec (x ≡ y)
-- --   Noeth→DecEq fn x y = {!!}
-- --     where
-- --     go : ∀ xs → ◻ (_≡ x) xs → NoethAcc xs → ∃[ ys ] (◻ (_≡ x) ys × Dup ys)
-- --     go xs ◻xs (stop x) = xs , ◻xs , x
-- --     go xs ◻xs (step r) = go (x ∷ xs) (λ { f0 → refl ; (fs n) → ◻xs n}) (r x)

-- -- bfe : Fin A → (A → List A) → A → List A
-- -- bfe f g r = toList f (concat (levels (bfs f g r)))