lf

Author: Pzixel

chapter10.1.idr

@@ -9,26 +9,26 @@ showList xs = "[" ++ show' xs ++ "]" where
     show' : List a -> String
     show' Nil        = ""
     show' (x :: Nil) = show x
-    show' (x :: xs)  = show x ++ ", " ++ show' xs   
+    show' (x :: xs)  = show x ++ ", " ++ show' xs
 
 data ListLast : List a -> Type where
     Empty : ListLast []
     NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])
 
 describeHelper : (input : List Int) -> (form : ListLast input) -> String
 describeHelper [] Empty = "Empty"
-describeHelper (xs ++ [x]) (NonEmpty xs x)= "Non-empty, initial portion = " ++ show xs 
+describeHelper (xs ++ [x]) (NonEmpty xs x)= "Non-empty, initial portion = " ++ show xs
 
 listLast : (xs : List a) -> ListLast xs
 listLast [] = Empty
-listLast (x :: xs) = case listLast xs of 
+listLast (x :: xs) = case listLast xs of
     Empty => NonEmpty [] x
     (NonEmpty ys y) => NonEmpty (x :: ys) y
 
 describeListEnd : List Int -> String
 describeListEnd xs with (listLast xs)
   describeListEnd _ | Empty = "Empty"
-  describeListEnd _ | (NonEmpty ys x) ="Non-empty, initial portion = " ++ show ys 
+  describeListEnd _ | (NonEmpty ys x) ="Non-empty, initial portion = " ++ show ys
 
 covering myReverse : List a -> List a
 myReverse xs with (listLast xs)
@@ -39,14 +39,14 @@ data SplitList : List a -> Type where
     SplitNil : SplitList []
     SplitOne : SplitList [x]
     SplitPair : (lefts : List a) -> (rights : List a) -> SplitList (lefts ++ rights)
-    
+
 splitList : (input : List a) -> SplitList input
 splitList input = splitListHelp input input
     where
         splitListHelp : List a -> (input : List a) -> SplitList input
         splitListHelp _ [] = SplitNil
         splitListHelp _ [x] = SplitOne
-        splitListHelp (_ :: _ :: counter) (item :: items) = 
+        splitListHelp (_ :: _ :: counter) (item :: items) =
             case splitListHelp counter items of
                 SplitNil => SplitOne
                 SplitOne {x} => SplitPair [item] [x]
@@ -57,13 +57,13 @@ partial mergeSort : Ord a => List a -> List a
 mergeSort xs with (splitList xs)
   mergeSort [] | SplitNil = []
   mergeSort [x] | SplitOne = [x]
-  mergeSort (lefts ++ rights) | (SplitPair lefts rights) = merge (mergeSort lefts) (mergeSort rights) 
+  mergeSort (lefts ++ rights) | (SplitPair lefts rights) = merge (mergeSort lefts) (mergeSort rights)
 
 data TakeN : List a -> Type where
     Fewer : TakeN xs
     Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)
 
-takeN : (n : Nat) -> (xs : List a) -> TakeN xs    
+takeN : (n : Nat) -> (xs : List a) -> TakeN xs
 takeN Z xs = Exact []
 takeN (S k) [] = Fewer
 takeN (S k) (x :: xs) with (takeN k xs)
@@ -75,18 +75,18 @@ groupByN n xs with (takeN n xs)
   groupByN n xs | Fewer = [xs]
   groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest
 
-half : Nat -> Nat 
+half : Nat -> Nat
 half Z = Z
 half (S Z) = Z
 half (S (S x)) = S (half x)
 
-halves : List a -> (List a, List a)  
-halves xs = 
+halves : List a -> (List a, List a)
+halves xs =
     let mid = half $ length xs
         taken = takeN mid xs
-    in case taken of 
+    in case taken of
         Fewer => ([], xs)
         (Exact n_xs {rest}) => (n_xs, rest)
 
 main : IO ()
-main = pure ()
+main = pure ()

chapter10.2.idr

@@ -10,34 +10,34 @@ mergeSort : Ord a => List a -> List a
 mergeSort xs with (splitRec xs)
     mergeSort [] | SplitRecNil = []
     mergeSort [x] | SplitRecOne = [x]
-    mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) = merge (mergeSort lefts | lrec) (mergeSort rights | rrec) 
+    mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) = merge (mergeSort lefts | lrec) (mergeSort rights | rrec)
 
 equalSuffix : Eq a => List a -> List a -> List a
 equalSuffix xs ys with (snocList xs)
     equalSuffix xs ys | recx with (snocList ys)
         equalSuffix _ _ | Empty | Empty = []
         equalSuffix _ _ | (Snoc _) | Empty = []
         equalSuffix _ _ | Empty | (Snoc _) = []
-        equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc recx) | (Snoc recy) = 
+        equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc recx) | (Snoc recy) =
             if x /= y then [] else (equalSuffix xs ys | recx | recy) ++ [x]
 
 mergeSortV : Ord a => Vect n a -> Vect n a
 mergeSortV xs with (splitRec xs)
     mergeSortV [] | SplitRecNil = []
     mergeSortV [x] | SplitRecOne = [x]
-    mergeSortV (lefts ++ rights) | (SplitRecPair lrec rrec) = merge (mergeSortV lefts | lrec) (mergeSortV rights | rrec) 
-    
+    mergeSortV (lefts ++ rights) | (SplitRecPair lrec rrec) = merge (mergeSortV lefts | lrec) (mergeSortV rights | rrec)
+
 toBinary : Nat -> String
-toBinary k with (halfRec k) 
+toBinary k with (halfRec k)
     toBinary Z | HalfRecZ = "0"
     toBinary (n + n) | (HalfRecEven rec) = (toBinary n | rec) ++ "0"
     toBinary (S (n + n)) | (HalfRecOdd rec) = (toBinary n | rec) ++ "1"
 
-palindrome : List Char -> Bool    
-palindrome s with (vList s) 
+palindrome : List Char -> Bool
+palindrome s with (vList s)
     palindrome [] | VNil = True
     palindrome [x] | VOne = True
     palindrome (x :: (xs ++ [y])) | (VCons rec) = x == y && (palindrome xs | rec)
 
 main : IO ()
-main = print $ mergeSort [1,4,5,2,3,4,7]
+main = print $ mergeSort [1,4,5,2,3,4,7]

chapter10.3/DataStore.idr

@@ -24,17 +24,17 @@ empty = MkData 0 []
 
 export
 addToStore : (value : SchemaType schema) -> (store : DataStore schema) -> DataStore schema
-addToStore value (MkData _ items) = MkData _ (value :: items)    
+addToStore value (MkData _ items) = MkData _ (value :: items)
 
 public export
 data StoreView : DataStore schema -> Type where
     SNil : StoreView empty
     SAdd : (rec : StoreView store) -> StoreView (addToStore value store)
-    
+
 storeViewHelp : (items : Vect size (SchemaType schema)) -> StoreView (MkData size items)
 storeViewHelp [] = SNil
 storeViewHelp (val :: xs) = SAdd (storeViewHelp xs)
 
 export
 storeView : (store : DataStore schema) -> StoreView store
-storeView (MkData size items) = storeViewHelp items
+storeView (MkData size items) = storeViewHelp items

chapter10.3/TestStore.idr

@@ -1,7 +1,7 @@
 import DataStore
 
 testStore : DataStore (SString .+. SString .+. SInt)
-testStore = 
+testStore =
     addToStore ("Mercury", "Mariner 10", 1974) (
         addToStore ("Venus", "Venera", 1961) (
             addToStore ("Uranus", "Voyager 2", 1986)(
@@ -14,9 +14,9 @@ testStore =
 listItems : DataStore schema -> List (SchemaType schema)
 listItems input with (storeView input)
     listItems empty | SNil = []
-    listItems (addToStore value store) | (SAdd rec) = value :: listItems store | rec    
+    listItems (addToStore value store) | (SAdd rec) = value :: listItems store | rec
 
 getValues : DataStore (SString .+. val_schema) -> List (SchemaType val_schema)
 getValues input with (storeView input)
     getValues empty | SNil = []
-    getValues (addToStore (MkPair _ value) store) | (SAdd rec) = value :: listItems store | rec 
+    getValues (addToStore (MkPair _ value) store) | (SAdd rec) = value :: listItems store | rec

chapter11.1.idr

@@ -9,8 +9,8 @@ import Data.Bits
 
 data InfList : Type -> Type where
     (::) : (value : elem) -> Inf (InfList elem) -> InfList elem
- 
-    
+
+
 %name InfList xs, ys, zs
 
 countFrom : Integer -> InfList Integer
@@ -32,8 +32,8 @@ instance Show Face where
     show Heads = "Heads"
     show Tails = "Tails"
 
-isOdd : Int -> Bool 
-isOdd value = 
+isOdd : Int -> Bool
+isOdd value =
     let onePattern = bitAt (the (Fin 1) 0)
     in ((intToBits (cast value)) `Data.Bits.and` onePattern) == onePattern
 
@@ -42,4 +42,4 @@ coinFlips : Stream Int -> Stream Face
 coinFlips (value :: xs) = (if isOdd value then Heads else Tails) :: coinFlips xs
 
 main : IO ()
-main = print $ take 10 (coinFlips [1..]) 
+main = print $ take 10 (coinFlips [1..])

chapter11.2.idr

@@ -16,38 +16,38 @@ data InfIO : Type where
 data Fuel = Dry | More (Lazy Fuel)
 
 loopPrint : String -> InfIO
-loopPrint msg = Do (putStrLn msg) (\_ => loopPrint msg)  
+loopPrint msg = Do (putStrLn msg) (\_ => loopPrint msg)
 
 run : Fuel -> InfIO -> IO ()
-run (More fuel) (Do c f) = 
-    do 
+run (More fuel) (Do c f) =
+    do
         res <- c
         run fuel (f res)
 run Dry p = putStrLn "Out of fuel"
 
 quiz : Stream Int -> (score : Nat) -> InfIO
-quiz (num1 :: num2 :: nums) score = 
-    do 
+quiz (num1 :: num2 :: nums) score =
+    do
         putStrLn ("Score so far: " ++ show score)
         putStr (show num1 ++ "*" ++ show num2 ++ "? ")
         answer <- getLine
-        if (cast answer == num1 * num2) 
-            then 
-                do 
+        if (cast answer == num1 * num2)
+            then
+                do
                     putStrLn "Correct!"
                     quiz nums (score + 1)
-            else 
-                do 
+            else
+                do
                     putStrLn ("Wrong, the answer is " ++ show (num1 * num2))
-                    quiz nums score        
+                    quiz nums score
 
 covering
 forever : Fuel
 forever = More forever
 
 totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
-totalREPL prompt action = 
-    do 
+totalREPL prompt action =
+    do
         putStr prompt
         input <- getLine
         putStr $ action input
@@ -56,4 +56,4 @@ totalREPL prompt action =
 
 covering
 main : IO ()
-main = run forever (quiz [1..] 0)
+main = run forever (quiz [1..] 0)