module Demo where

data Bool : Set where
  True : Bool
  False : Bool

not : Bool -> Bool
not True = False
not False = True

if_then_else_ : Bool -> Bool -> Bool -> Bool
if True then t else e = t
if False then t else e = e

data Nat : Set where
  Zero : Nat
  Succ : Nat → Nat

_+_ : Nat → Nat → Nat
Zero + y = y
Succ x + y = Succ (x + y)

{-# BUILTIN NATURAL Nat #-}

cond : ∀ {a : Set} -> Bool -> a -> a -> a
cond True t e = t
cond False t e = e

test : Nat
test = cond True  

id : ∀ {a : Set} -> a -> a 
id x = x

data List (a : Set) : Set where
  Nil : List a 
  Cons : a -> List a -> List a

_++_ : {a : Set} -> List a -> List a -> List a
Nil ++ ys = ys
Cons x xs ++ ys = Cons x (xs ++ ys)

xs : List Nat
xs = Cons  (Cons  (Cons  Nil))

data Maybe (a : Set) : Set where
  Nothing : Maybe a
  Just : a -> Maybe a

_!!_ : {a : Set} -> List a -> Nat -> Maybe a
Nil !! Zero = Nothing
Cons x xs !! Zero = Just x
Nil !! Succ i = Nothing
Cons x xs !! Succ i = xs !! i

length : {a : Set} -> List a -> Nat
length Nil = Zero
length (Cons x xs) = Succ (length xs)

data _<_ : Nat -> Nat -> Set where
  Base : forall {n} -> Zero < Succ n
  Step : ∀ {n m} -> n < m -> Succ n < Succ m

lemma :  < 
lemma = Step (Step (Step Base))

impossible : {a : Set} -> (n : Nat) -> n < Zero -> a
impossible n ()

lookup : {a : Set} -> (n : Nat) -> (xs : List a) -> n < length xs -> a
lookup n Nil ()
lookup Zero (Cons x xs) p = x
lookup (Succ n) (Cons x xs) (Step p) = lookup n xs p

data Vec (a : Set) : Nat -> Set where
  Nil : Vec a Zero
  Cons : {n : Nat} -> a -> Vec a n -> Vec a (Succ n)

head : {a : Set} -> (xs : List a) ->  < length xs -> a
head Nil ()
head (Cons x xs) p = x

vhead : {a : Set} {n : Nat} -> Vec a (Succ n) -> a
vhead (Cons x xs) = x

vlookup : {a : Set} {n : Nat} -> Vec a n -> (m : Nat) -> m < n -> a
vlookup Nil m ()
vlookup (Cons x xs) Zero p = x
vlookup (Cons x xs) (Succ n) (Step p) = vlookup xs n p

data Fin : Nat -> Set where
  FZero : {n : Nat} -> Fin (Succ n)
  FSucc : {n : Nat} -> Fin n -> Fin (Succ n)

vlookup' : {a : Set} {n : Nat} -> Vec a n -> Fin n -> a
vlookup' (Cons x xs) FZero = x
vlookup' (Cons x xs) (FSucc i) = vlookup' xs i

vappend : {a : Set} {n m : Nat} -> Vec a n -> Vec a m -> Vec a (n + m)
vappend Nil ys = ys
vappend (Cons x xs) ys = Cons x (vappend xs ys) -- Cons x (vappend xs ys)