module L1 where

----------------------------------------------------------------------
-- Lecture 1 : Learning by Testing                                  --
----------------------------------------------------------------------

{- Not all things are the same. -}

data Bool : Set where
  true  : Bool
  false : Bool

{- It is sometimes important to treat different things in different
ways. Some might argue that this is the reason for having different
things in the first place. -}

{-

if_then_else_ : {T : Set} -> Bool -> T -> T -> T
if true  then t else f = f
if false then t else f = t

-}

if_then_else_ : {T : Set} -> Bool -> T -> T -> T
if true  then t else f = t
if false then t else f = f

_or_ : Bool -> Bool -> Bool
true  or _ = true
false or b = b

{- The application rule for dependent functions allows the output
type of a function to depend on the input value. -}

apply : {S : Set}{T : S -> Set}
        (f : (x : S) -> T x)(s : S) ->
        T s
apply f s = f s



{- -}

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

map : {S T : Set} -> (S -> T) -> List S -> List T
map f [] = []
map f (x :: xs) = f x :: map f xs

_++_ : {X : Set} -> List X -> List X -> List X
[] ++ ys = ys 
(x :: xs) ++ ys = x  :: (xs ++ ys  ) 


exists : {X : Set} -> (X -> Bool) -> List X -> Bool
exists p [] = false
exists p (x :: xs) = p x or exists p xs

firstSatisfying : {X : Set} -> (X -> Bool) -> List X -> X
firstSatisfying p (x :: xs) = if p x then x else firstSatisfying p xs
firstSatisfying p [] = {! !}


data Maybe (X : Set) : Set where
  just : X -> Maybe X
  nothing : Maybe X

maybeFirstSat : {X : Set} -> (X -> Bool) -> List X -> Maybe X
maybeFirstSat p (x :: xs) = if p x then just x else maybeFirstSat p xs
maybeFirstSat p [] = nothing

data One : Set where
  void : One

data Zero : Set where

Know : Bool -> Set
Know true  = One
Know false = Zero

firstSuchThat : {X : Set}(p : X -> Bool)(xs : List X) -> Know (exists p xs) -> X
firstSuchThat p [] ()
firstSuchThat p (x :: xs) k with p x
firstSuchThat p (x :: xs) k | true  = x 
firstSuchThat p (x :: xs) k | false = firstSuchThat p xs k 

{-
depIf : (b : Bool)(P : Bool -> Set) -> P true -> P false -> P b
depIf true P pt pf = pt
depIf false P pt pf = pf

fST :  {X : Set}(p : X -> Bool)(xs : List X) -> Know (exists p xs) -> X
fST p [] = magic where
  magic : {X : Set} -> Zero -> X
  magic ()
fST p (x :: xs) = depIf (p x) {! !} x (fST p xs {! !})
-}

data _*_ (S T : Set) : Set where
  _,_ : S -> T -> S * T

zip : {S T : Set} -> List S -> List T -> List (S * T)
zip [] [] = []
zip [] (t :: ts) = {! !}
zip (s :: ss) [] = {! !}
zip (s :: ss) (t :: ts) = (s , t) :: zip ss ts

_eqLen_ : {S T : Set} -> List S -> List T -> Bool
[] eqLen [] = true
(s :: ss) eqLen (t :: ts) = ss eqLen ts
_ eqLen _ = false

zipQ : {S T : Set}(ss : List S)(ts : List T) ->
       Know (ss eqLen ts) -> List (S * T)
zipQ [] [] _ = []
zipQ [] (t :: ts) ()
zipQ (s :: ss) [] ()
zipQ (s :: ss) (t :: ts) k = (s , t) :: zipQ ss ts k