module L4 where

----------------------------------------------------------------------
-- Lecture 4 : Shapes and positions
----------------------------------------------------------------------

data List (X : Set) : Set where
  [l] : List X
  _:l:_ : X -> List X -> List X

infixr 40 _:l:_

data One : Set where
  void : One

data Zero : Set where

magic : {X : Set} -> Zero -> X
magic ()

data _:+:_ (S T : Set) : Set where
  inl : S -> S :+: T
  inr : T -> S :+: T

Somewhere : {X : Set} -> (X -> Set) -> List X -> Set
Somewhere P [l]         = Zero
Somewhere P (x :l: xs)  = P x :+: (Somewhere P xs)

get : {X : Set}{P : X -> Set}(xs : List X)(i : Somewhere P xs) -> X
get [l]        ()
get (x :l: xs) (inl p) = x 
get (x :l: xs) (inr i) = get xs i 

data Sigma (S : Set)(T : S -> Set) : Set where
  _,_ : (s : S)(t : T s) -> Sigma S T

_*_ : Set -> Set -> Set
S * T = Sigma S \ s -> T

get2 : {X : Set}{P : X -> Set}(xs : List X)(i : Somewhere P xs) -> Sigma X P
get2 [l]        ()
get2 (x :l: xs) (inl p) = x , p
get2 (x :l: xs) (inr i) = get2 xs i 

-------

data Nat : Set where
  zero  : Nat
  suc   : Nat -> Nat

data _^_ (X : Set) : Nat -> Set where
  [] : X ^ zero
  _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n

List2 : Set -> Set
List2 X = Sigma Nat \ n -> X ^ n

[l2] : {X : Set} -> List2 X
[l2] = zero , []

_:l2:_ : {X : Set} -> X -> List2 X -> List2 X
x :l2: (n , xs) = suc n , (x :: xs)

infixr 40 _:l2:_

foldr2 : {X T : Set} -> (X -> T -> T) -> T -> List2 X -> T
foldr2 f t (zero , []) = t
foldr2 f t (suc n , (x :: xs)) = f x (foldr2 f t (n , xs))

_+2+_ : {X : Set} -> List2 X -> List2 X -> List2 X
xs +2+ ys = foldr2 _:l2:_ ys xs

---------------------

data Fin : Nat -> Set where
  fzero : {n : Nat} -> Fin (suc n)
  fsuc : {n : Nat} -> Fin n -> Fin (suc n)

List3 : Set -> Set
List3 X = Sigma Nat \ n -> Fin n -> X

[l3] : {X : Set} -> List3 X
[l3] = zero , none where
  none : Fin zero -> _
  none ()

_:l3:_ : {X : Set} -> X -> List3 X -> List3 X
_:l3:_ x (n , f) = suc n , xf where
  xf : Fin (suc n) -> _
  xf fzero = x
  xf (fsuc i) = f i

{- think about "shape and position" presentations of other containers -}

ListShape : Set
ListShape = List One

ListPosition : ListShape -> Set
ListPosition s = Somewhere (\ x -> One) s

List4 : Set -> Set
List4 X = Sigma ListShape \ s -> ListPosition s -> X

[l4] : {X : Set} -> List4 X
[l4] = [l] , magic

_:l4:_ : {X : Set} -> X -> List4 X -> List4 X
_:l4:_ x (s , f) = (void :l: s) , xf where
  xf : One :+: _ -> _
  xf (inl void) = x
  xf (inr i) = f i