module DataStructures where

-- Some definitions of standard things
-- (sorry for not using libraries).

open import Naturals
open import Addition
open import Finite
open import LogicalFacts


data List (X : Set) : Set where
 [] : List X
 _::_  : X → List X → List X

infixr  _::_


-- Transforms a finite list given as a map to an enumerated finite
-- list:

list : {m : ℕ} {X : Set} → (smaller m → X) → List X
list {} s = []
list {succ m} s = s fzero :: list {m} (s ∘ fsucc)


-- Binary products:

data _×_ (X Y : Set) : Set where
 _,_ : X → Y → X × Y


infixr  _,_


-- The cons operation for the Cantor space:

open import Cantor
open import Two

_^_ : ℕ → ₂ℕ → ₂ℕ
( ^ α)  = ₀
((succ n) ^ α)  = ₁
(b ^ α) (succ n) = α n

infixr  _^_


-- Take a finite initial sublist of an infinite sequence.

take : (m : ℕ) {X : Set} → (ℕ → X) → List X
take  α = []
take (succ m) α = α  :: take m (α ∘ succ)

-- Index a finite sequence:

_!_ : {m : ℕ} → (smaller(m + ) → ℕ) → ℕ → ℕ
_!_ {m} s n = s(fmin m n)