{-# 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  _∷_
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  ∃-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  _∈_
_∈_ : 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)))