chapt3.idr

module Main
import Debug.Trace
import Data.Vect;

-- infix  4 :+:
   
-- data Vect : Nat -> Type -> Type where
--    Nil  : Vect Z a
--    (:+:) : a -> Vect k a -> Vect (S k) a

-- testFunc : (Vect n a) -> (Vect m a) -> (n = m) -> Integer
-- testFunc _ _ _ = 50
    
-- foo : Integer
-- foo = let arr = (1 :+: (2 :+: (3 :+: Nil)))
--           arrWithFour = 4 :+: arr
--       in testFunc arr arr Refl

-- add : (a: Int) -> (b: Int) -> (c: Int, c >= a && c >= b)
-- add a b = (a + b, Refl)

palindrome : String -> Bool 
palindrome s = s == reverse s

counts : String -> (Nat, Nat)
counts s = (length (words s), length s)

top_ten : Ord a => List a -> List a 
top_ten = Prelude.List.take 10 . reverse . sort

over_length : Nat -> List String -> Nat 
over_length n = length . filter (\x => length x > n)

allLengths : List String -> List Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

insSort : (Ord elem) => Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = 
    let sortedXs = insSort xs
        position = findPosition x sortedXs
    in insertAt position x sortedXs
    where 
        findPosition : (Ord elem) => elem -> Vect n elem -> Fin (S n)
        findPosition x xs = let maybeIndex = findIndex (\elm => x < elm) xs in 
            fromMaybe last (weaken <$> maybeIndex)
                    

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = (const []) <$> range
transposeMat (x :: xs) = 
    let transXs = transposeMat xs 
    in appendHeadColumn x transXs where 
        appendHeadColumn = zipWith (::)

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)        
addMatrix = zipWith (zipWith (+))

multMatrix : Num a => Vect n (Vect m a) -> Vect m (Vect p a) -> Vect n (Vect p a)       
multMatrix xs ys =
    let transposedYs = transposeMat ys
    in (\xrow => combineRows xrow <$> transposedYs) <$> xs where 
        combineRows xrow yrow = sum (zipWith (*) xrow yrow)


vectTake : (m: Nat) -> Vect n a -> Vect (minimum m n) a
vectTake Z _ = []
vectTake m [] = rewrite minimumZeroZeroLeft m in []
vectTake (S k) (x :: xs) = x :: vectTake k xs


sumEntries : Num a => {n : Nat} -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = do 
    i <- integerToFin pos n
    pure $ index i xs + index i ys

main : IO ()
main = repl "\n> " (show . palindrome . toLower)

chapt4.idr

module Main
import Debug.Trace
import Data.Vect;
import Data.String

record DataStore where 
    constructor MkData 
    size: Nat
    items: Vect size String
data Command = Add String
    | Get Integer
    | Quit

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items') newitem = MkData _ (addToData items')
    where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [newitem]
    addToData (item :: items') = item :: addToData items'


replMain : DataStore -> String -> Maybe (String, DataStore)    
replMain ds text = 
    let maybeCommand = parseCommand text 
    in case maybeCommand of 
        Nothing => pure ("Unknown command", ds)
        Just command => processCommand command ds
    where 
        parseCommand : String -> Maybe Command
        parseCommand text = 
            case span (/= ' ') (toLower text) of
                ("add", args) => pure $ Add (ltrim args)
                ("get", args) => Get <$> parseInteger args 
                ("quit", _) => pure Quit
                _ => Nothing
        processCommand : Command -> DataStore -> Maybe (String, DataStore)
        processCommand (Add s) ds = 
            let newStore = addToStore ds s
                stringIndex : String = cast (size ds)
            in pure ("ID " ++ stringIndex, newStore)
        processCommand (Get i) ds = 
            let maybeValue = do 
                    fin <- integerToFin i (Main.DataStore.size ds)
                    pure $ Data.Vect.index fin (items ds)

                textToShow = fromMaybe "Out of range" maybeValue
            in pure (textToShow, ds)
        processCommand Quit _ = Nothing


main : IO ()
main = replWith (MkData 0 []) ("\nCommand:") replMain

chapt5.idr

module Main
import Debug.Trace
import Data.Vect;
import Data.String
import Control.IOExcept

data VectUnknown : Type -> Type where
    MkVect : (len : Nat) -> Vect len a -> VectUnknown a 

implementation Show a => Show (VectUnknown a) where 
    show (MkVect len vec) = show len ++ " " ++ show vec

whileM' : (Monad m, Monad f, Alternative f) => (a -> Bool) -> m a -> m (f a)
whileM' p f = go
    where go = do
            x <- f
            if p x
                then do
                        xs <- go
                        pure (pure x <|> xs)
                else pure empty

whileM : Monad m => (a -> Bool) -> m a -> m (List a)
whileM = whileM'     

readToBlank : IO (List String)
readToBlank = whileM (/= "") getLine

readVect : IO (len ** Vect len String)
readVect = do 
    list <- readToBlank
    let vec = fromList list
    pure (_ ** vec)

readAndSave : IO ()
readAndSave = do 
  content <- readToBlank
  filename <- getLine 
  Right _ <- writeFile filename (unlines content)
  pure ()

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do 
    Right content <- readFile filename
    let list = lines content
    let vec = fromList list
    pure (_ ** vec)

zipInputs : IO ()
zipInputs =  
    do putStrLn "Enter first vector (blank line to end):"
       (len1 ** vec1) <- readVect
       putStrLn "Enter second vector (blank line to end):"
       (len2 ** vec2) <- readVect
       case exactLength len1 vec2 of
            Nothing => putStrLn "Vectors are different lengths"
            Just vec2' => printLn (zip vec1 vec2')
    
main : IO ()
main = do
    items <- readVect
    print items

chapt6_part1.idr

module Main
import Debug.Trace
import Data.Vect;
import Data.String
import Control.IOExcept

%default total

VarArgs : Type -> (numargs : Nat) -> Type
VarArgs t Z = t
VarArgs t (S k) = (next : t) -> VarArgs t k

adder : (Num t) => (numargs : Nat) -> VarArgs t (S numargs)
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

data Format = 
      INumber Format
    | FNumber Format  
    | Str Format
    | Ch Format
    | Lit String Format
    | End

PrintfType : Format -> Type
PrintfType (INumber fmt) = (i : Int) -> PrintfType fmt
PrintfType (FNumber fmt) = (f : Double) -> PrintfType fmt
PrintfType (Ch fmt) = (c : Char) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: tail) = INumber (toFormat tail)
toFormat ('%' :: 'f' :: tail) = FNumber (toFormat tail)
toFormat ('%' :: 'c' :: tail) = Ch (toFormat tail)
toFormat ('%' :: 's' :: tail) = Str (toFormat tail)
toFormat (x :: tail) = Lit (cast x) (toFormat tail)

-- reduceFormat : Format -> Format
-- reduceFormat (INumber x) = INumber (reduceFormat x)
-- reduceFormat (Str x) = Str (reduceFormat x)
-- reduceFormat (Lit x (Lit y t)) = reduceFormat (Lit (x ++ y) t)
-- reduceFormat (Lit x y) = Lit x (reduceFormat y)
-- reduceFormat End = End

reduceFormat : Format -> Format
reduceFormat (INumber x) = INumber (reduceFormat x)
reduceFormat (FNumber x) = FNumber (reduceFormat x)
reduceFormat (Ch x) = Ch (reduceFormat x)
reduceFormat (Str x) = Str (reduceFormat x)
reduceFormat (Lit x r) = 
    case reduceFormat r of 
        Lit y t => Lit (x ++ y) t
        other => Lit x other
reduceFormat End = End

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (INumber fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (FNumber fmt) acc = \f => printfFmt fmt (acc ++ show f)
printfFmt (Ch fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc

printf : (fmt : String) -> PrintfType (reduceFormat (toFormat (unpack fmt)))
printf _ = printfFmt _ ""

Matrix : Nat -> Nat -> Type
Matrix m n = Vect m (Vect n Int)

testMatrix : Matrix 2 3
testMatrix = [[0, 0, 0], [0, 0, 0]]

TupleVect : Nat -> Type -> Type
TupleVect Z _ = ()
TupleVect (S n) ty = (ty, TupleVect n ty)

main : IO ()
main = print $ 10

whileM.idr

whileM' : (Monad m, Monad f, Alternative f) => (a -> Bool) -> m a -> m (f a)
whileM' p f = go
    where go = do
            x <- f
            if p x
                then do
                        xs <- go
                        pure (pure x <|> xs)
                else pure empty

whileM : Monad m => (a -> Bool) -> m a -> m (List a)
whileM = whileM'