module Live where

data Nat : Set where
  z : Nat
  s : Nat → Nat

_+_ : Nat → Nat → Nat
z   + n = n
s m + n = s (m + n)

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO    z   #-}
{-# BUILTIN SUC     s   #-}

_*_ : Nat → Nat → Nat
z   * n = z
s m * n = n + (m * n)

data Bool : Set where
  tt : Bool
  ff : Bool

_==_ : Nat → Nat → Bool
z   == z   = tt
z   == s n = ff
s m == z   = ff
s m == s n = m == n


-- Pairs
record _×_ (A B : Set) : Set where
--  constructor _,_ 
  field fst : A
        snd : B
open _×_

-- if we want to define the constructor by hand
_,_ : {A B : Set} → A → B → A × B
a , b = record{fst = a;snd = b}

curry : {A B C : Set} → (A × B → C) → A → B → C
curry f a b = f (a , b)

uncurry : {A B C : Set} → (A → B → C) → A × B → C
uncurry f p = f (fst p) (snd p)

papp : {A B C D : Set} → ((A → B) × (C → D)) → (A × C) → (B × D)
papp p q = fst p (fst q) , snd p (snd q)

-- Lists 

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

-- asside on parameters and indices
data List' : Set → Set1 where
  [] : ∀{X} → List' X
  _::_ : ∀{X} → X → List' X → List' X

_++_ : ∀{X} → List X → List X → List X
[]        ++ vs' = vs'
(v :: vs) ++ vs' = v :: (vs ++ vs')

zip : ∀{A B} → List A → List B → List (A × B)
zip []        bs        = []
zip as        []        = []
zip (a :: as) (b :: bs) = (a , b) :: zip as bs

unzip : ∀{A B} → List (A × B) → List A × List B
unzip []        = [] , []
--unzip (p :: ps) = (fst p :: fst (unzip ps)) , (snd p :: snd (unzip ps))
{-
unzip (p :: ps) = let x = unzip ps 
                  in (fst p :: fst x) , (snd p :: snd x)
-}
unzip (p :: ps) = (fst p :: fst x) , (snd p :: snd x) 
  where 
  x = unzip ps

-- Wednesday

head : ∀{X} → List X → X
head []        = {!!}
head (x :: xs) = x

data Maybe (A : Set) : Set where
  Just : A → Maybe A
  Nothing : Maybe A

-- safe head
mhead : ∀{X} → List X → Maybe X
mhead []        = Nothing
mhead (x :: xs) = Just x

-- safe tail
mtail : ∀{X} → List X → Maybe (List X)
mtail []        = Nothing
mtail (x :: xs) = Just xs

mreturn : ∀{X} → X → Maybe X
mreturn = Just 

mbind : ∀{X Y} → (X → Maybe Y) → Maybe X → Maybe Y
mbind f (Just x) = f x
mbind f Nothing  = Nothing

mjoin : ∀{X} → Maybe (Maybe X) → Maybe X
mjoin (Just mx) = mx
mjoin Nothing   = Nothing

-- Vectors

data Vec (X : Set) : Nat → Set where
  []   : Vec X z
  _::_ : ∀{n} → X → Vec X n → Vec X (s n)

vhead : ∀{X n} → Vec X (s n) → X
vhead (x :: xs) = x

vtail : ∀{X n} → Vec X (s n) → Vec X n
vtail (x :: xs) = xs

vec2List : ∀{X n} → Vec X n → List X
vec2List []        = []
vec2List (x :: xs) = x :: (vec2List xs)

length : ∀{X} → List X → Nat
length []        = z
length (x :: xs) = s (length xs)

list2Vec : ∀{X}(xs : List X) → Vec X (length xs)
list2Vec [] = []
list2Vec (x :: xs) = x :: list2Vec xs

test1 : List Nat
test1 = 1 :: (2 :: (3 :: (4 :: (5 :: []))))

lookup : ∀{X} → Nat → List X → Maybe X
lookup n []            = Nothing
lookup z (x :: xs)     = Just x
lookup (s n) (x :: xs) = lookup n xs

data Fin : Nat → Set where
  fz : ∀ {n} → Fin (s n)
  fs : ∀{n} → Fin n → Fin (s n)

vlookup : ∀{X n}(i : Fin n) → Vec X n → X
vlookup fz     (x :: xs) = x
vlookup (fs i) (x :: xs) = vlookup i xs

-- Thursday 

-- The empty type and pattern matching
data False : Set where

weird : {X : Set} → False → X
weird ()