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