initial commit

Average.idr

@@ -0,0 +1,17 @@
+module Average
+
+import Data.String
+
+
+||| Calculate the average word length of a string
+||| @str a string containing words seperated by whitespace
+export
+average : (str : String) -> Double
+average str = let totalLength = sum (wordLengths str)
+                  wordAmount = wordCount str in
+                  cast totalLength / cast wordAmount
+  where
+    wordCount : String -> Nat
+    wordCount str = length (words str)
+    wordLengths : String -> List Nat
+    wordLengths str = map length (words str)

AverageMain.idr

@@ -0,0 +1,8 @@
+module Main
+import Average
+
+showAverage : String -> String
+showAverage str = show (average str)
+
+main : IO ()
+main = repl "\n> " showAverage

AverageWord.idr

@@ -0,0 +1,25 @@
+module Main
+-- import System.REPL oh god my setup is horrible
+import Data.String
+
+average : String -> Double
+average str = let numWords = wordCount str
+                  totalLength = sum (allLengths (words str)) in
+                  cast totalLength / cast numWords
+  where
+    wordCount : String -> Nat
+    wordCount str = length (words str)
+    allLengths : List String -> List Nat
+    allLengths strs = map length strs
+
+showAverage : String -> String
+showAverage str = "The average word length is: " ++ show (average str) ++ "\n"
+
+
+main : IO ()
+main = repl "Enter a string: " showAverage
+
+
+doubleSum : List Nat -> List Nat
+doubleSum xs = let sum = sum xs in
+                  [sum, sum]

Composites.idr

@@ -0,0 +1,2 @@
+totalLength : List String -> Nat
+totalLength xs = sum (map length xs)

Functions.idr

@@ -0,0 +1,43 @@
+double : Num ty => ty -> ty
+double x = x + x
+
+add : Int -> Int -> Int
+add x y = x + y
+
+identity : ty -> ty
+identity x = x
+
+-- the
+der : (ty : Type) -> ty -> ty
+der ty x = x
+
+
+||| Higher-Order-Functions
+
+twice : (a -> a) -> a -> a
+twice f x = f (f x)
+
+Shape : Type
+
+rotate : Shape -> Shape
+
+quadruple : Num a => a -> a
+quadruple = twice double
+
+turn_around : Shape -> Shape
+turn_around = twice rotate
+
+apply_n : (a -> a) -> Nat -> a -> a
+
+longer : String -> String -> Nat
+longer word1 word2 =
+    let len1 = length word1
+        len2 = length word2 in
+        max len1 len2
+
+
+pythagoras : Double -> Double -> Double
+pythagoras x y = sqrt (square x + square y)
+  where
+    square : Double -> Double
+    square x = x * x

Hello.idr

@@ -0,0 +1,26 @@
+module Main
+main : IO ()
+main = putStrLn "hello world"
+
+StringOrInt : Bool -> Type
+StringOrInt x = case x of
+                    True => Int
+                    False => String
+
+
+getStringOrInt : (x : Bool) -> StringOrInt x
+getStringOrInt x = case x of
+                        True => 94
+                        False => "Ninety four"
+
+TypeChooser : String -> Type
+TypeChooser x = case x of
+  "Int" => Int
+  "Bool" => Bool
+  "String" => String
+  "Char" => Char
+
+valToString : (typeChoice : Bool) -> StringOrInt typeChoice -> String
+valToString typeChoice val = case typeChoice of
+                          True => cast val  -- True means that our argument type is Int, so cast
+                          False => val -- False means that our agumet type is String, so no need to cast

Palindrome.idr

@@ -0,0 +1,17 @@
+module Palindrome
+
+palindrome : String -> Bool
+palindrome str = let halfs = splitHalf str in
+                     fst halfs == (reverse (snd halfs))
+  where
+    halfLength : String -> Nat
+    halfLength str = (length str) `div` 2
+
+    splitHalf : String -> (String, String)
+    splitHalf str = let firstHalf = substr 0 (halfLength str) str
+                        startIndex = if even (length str) then halfLength str else halfLength str + 1
+                        secondHalf = substr startIndex (length str) str in
+                        (firstHalf, secondHalf)
+      where
+        even : Nat -> Bool
+        even n = n `mod` 2 == 0

Reverse.idr

@@ -0,0 +1,4 @@
+module Main
+
+main : IO ()
+main = repl "\n> " reverse