Skip to content

Instantly share code, notes, and snippets.

@PeterHajdu

PeterHajdu/.gitignore

Last active June 25, 2017 18:43
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save PeterHajdu/0a4a0de909660921e5da1034e8b17360 to your computer and use it in GitHub Desktop.
Save PeterHajdu/0a4a0de909660921e5da1034e8b17360 to your computer and use it in GitHub Desktop.
Download ZIP
idris
Raw
.gitignore
*.ibc
*.idr~
Raw
1.idr
module Main
import Data.Vect
total mylength : List a -> Nat
mylength [] = 0
mylength (x :: xs) = S $ mylength xs
total myreverse : List a -> List a
myreverse [] = []
myreverse (x :: xs) = myreverse xs ++ [x]
total mymap : (a -> b) -> List a -> List b
mymap f [] = []
mymap f (x :: xs) = f x :: mymap f xs
total myvectmap : (a -> b) -> Vect n a -> Vect n b
myvectmap f [] = []
myvectmap f (x :: xs) = f x :: myvectmap f xs
main : IO ()
main = do
print $ mylength [1..10]
print $ myreverse [1..10]
print $ mymap (*2) [1..10]
print $ myvectmap (*2) [100, 200]
Raw
Adder.idr
module Main
AdderType : (numargs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next: Int) -> AdderType k
adder : (numargs: Nat) -> (acc: Int) -> AdderType numargs
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)
main : IO ()
main = print "kutyus"
Raw
AdderChannel.idr
module Main
import System.Concurrency.Channels
data Message = Add Nat Nat
adder : IO ()
adder = do Just sender_chan <- listen 1
| Nothing => adder
Just msg <- unsafeRecv Message sender_chan
| Nothing => adder
case msg of
Add x y => do ok <- unsafeSend sender_chan (x + y)
adder
main : IO ()
main = do Just adder_id <- spawn adder
| Nothing => putStrLn "Spawn failed"
Just chan <- connect adder_id
| Nothing => putStrLn "Connection failed"
ok <- unsafeSend chan (Add 2 3)
Just answer <- unsafeRecv Nat chan
| Nothing => putStrLn "Receive failed"
printLn answer
Raw
Arith.idr
module Arith
import Data.Primitives.Views
quiz : Stream Int -> (score : Nat) -> IO ()
quiz (num1 :: num2 :: xs) score = do
putStrLn ("Score so far: " ++ show score)
putStrLn (show num1 ++ " * " ++ show num2 ++ " ?")
answer <- getLine
if cast answer == num1 * num2
then do putStrLn "Correct!"
quiz xs (score + 1)
else do putStrLn ("Wrong, the answer is: " ++ show (num1 * num2))
quiz xs score
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
(seed' `shiftR` 2) :: randoms seed'
arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
where
bound : Int -> Int
bound x with (Data.Primitives.Views.Int.divides x 12)
bound ((12 * div) + rem) | (DivBy prf) = rem + 1
Raw
ArithCmd.idr
module ArithCmd
import Data.Primitives.Views
import System
%default total
public export
data Command : Type -> Type where
PutStr : String -> Command ()
GetLine : Command String
public export
data ConsoleIO : Type -> Type where
Quit : a -> ConsoleIO a
Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
public export
(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
(>>=) = Do
public export
runCommand : Command a -> IO a
runCommand (PutStr msg) = putStrLn msg
runCommand GetLine = getLine
public export
data Fuel = Dry | More (Lazy Fuel)
public export
partial
forever : Fuel
forever = More forever
public export
run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Dry y = pure Nothing
run (More fuel) (Quit x) = pure (Just x)
run (More fuel) (Do command continuation) = do
result <- runCommand command
run fuel (continuation result)
mutual
wrong : Stream Int -> (score : Nat) -> ConsoleIO Nat
wrong xs score = do PutStr "Wrong!"
quiz xs score
correct : Stream Int -> (score : Nat) -> ConsoleIO Nat
correct xs score = do PutStr "correct!"
quiz xs (score + 1)
quiz : Stream Int -> (score : Nat) -> ConsoleIO Nat
quiz (num1 :: num2 :: xs) score = do
PutStr ("Score so far: " ++ show score)
PutStr ((show num1) ++ " * " ++ (show num2))
line <- GetLine
if line == "quit"
then Quit score
else if cast line == num1 * num2
then correct xs score
else wrong xs score
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
(seed' `shiftR` 2) :: randoms seed'
arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
where
bound : Int -> Int
bound x with (Data.Primitives.Views.Int.divides x 12)
bound ((12 * div) + rem) | (DivBy prf) = rem + 1
partial
main : IO ()
main = do seed <- time
Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0)
| Nothing => putStrLn "Ran out of fuel."
putStrLn ("Final score: " ++ (show score))
Raw
ArithCmdDo.idr
module ArithCmdDo
import Data.Primitives.Views
import System
%default total
public export
data Input = Answer Int
| QuitCmd
public export
data Command : Type -> Type where
PutStr : String -> Command ()
GetLine : Command String
Pure : ty -> Command ty
Bind : Command a -> (a -> Command b) -> Command b
public export
runCommand : Command a -> IO a
runCommand (PutStr msg) = putStrLn msg
runCommand GetLine = getLine
runCommand (Pure value) = pure value
runCommand (Bind c f) = do res <- runCommand c
runCommand (f res)
namespace CommandDo
public export
(>>=) : Command a -> (a -> Command b) -> Command b
(>>=) = Bind
public export
readInput : (prompt : String) -> Command Input
readInput prompt = do PutStr prompt
answer <- GetLine
if answer == "quit"
then Pure QuitCmd
else Pure (Answer (cast answer))
public export
data ConsoleIO : Type -> Type where
Quit : a -> ConsoleIO a
Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
namespace ConsoleDo
public export
(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
(>>=) = Do
mutual
wrong : Stream Int -> (score : Nat) -> (rounds : Nat) -> ConsoleIO Nat
wrong xs score rounds = do PutStr "Wrong!"
quiz xs score rounds
correct : Stream Int -> (score : Nat) -> (rounds : Nat) -> ConsoleIO Nat
correct xs score rounds = do PutStr "correct!"
quiz xs (score + 1) rounds
quiz : Stream Int -> (score : Nat) -> (rounds : Nat) -> ConsoleIO Nat
quiz (num1 :: num2 :: xs) score rounds = do
PutStr ("Score so far: " ++ (show score) ++ " / " ++ (show rounds))
input <- readInput ((show num1) ++ " * " ++ (show num2))
case input of
Answer answer => if answer == num1 * num2
then correct xs score (rounds + 1)
else wrong xs score (rounds + 1)
QuitCmd => Quit score
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
(seed' `shiftR` 2) :: randoms seed'
arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
where
bound : Int -> Int
bound x with (Data.Primitives.Views.Int.divides x 12)
bound ((12 * div) + rem) | (DivBy prf) = rem + 1
public export
data Fuel = Dry | More (Lazy Fuel)
public export
partial
forever : Fuel
forever = More forever
public export
run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Dry y = pure Nothing
run (More fuel) (Quit x) = pure (Just x)
run (More fuel) (Do command continuation) = do
result <- runCommand command
run fuel (continuation result)
partial
main : IO ()
main = do seed <- time
Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0 0)
| Nothing => putStrLn "Ran out of fuel."
putStrLn ("Final score: " ++ (show score))
Raw
ArithState.idr
module ArithState
import Data.Primitives.Views
import System
%default total
record Score where
constructor MkScore
correct : Nat
attempted : Nat
record GameState where
constructor MkGameState
score : Score
difficulty : Int
initState : GameState
initState = MkGameState (MkScore 0 0) 12
addWrong : GameState -> GameState
addWrong = record { score -> attempted $= (+1) }
addCorrect : GameState -> GameState
addCorrect = record { score -> attempted $= (+1),
score -> correct $= (+1) }
Show GameState where
show (MkGameState (MkScore correct attempted) difficulty) = (show correct) ++ "/" ++ (show attempted)
data Command : Type -> Type where
PutStr : String -> Command ()
GetLine : Command String
GetRandom : Command Int
GetGameState : Command GameState
PutGameState : GameState -> Command ()
Pure : ty -> Command ty
Bind : Command a -> (a -> Command b) -> Command b
Functor Command where
map f fa = Bind fa (\a => Pure (f a))
Applicative Command where
pure = Pure
(<*>) af aa = Bind af (\f =>
Bind aa (\a =>
Pure (f a)))
Monad Command where
(>>=) = Bind
data ConsoleIO : Type -> Type where
Quit : a -> ConsoleIO a
Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
namespace ConsoleDo
(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
(>>=) = Do
data Fuel = Dry | More (Lazy Fuel)
partial
forever : Fuel
forever = More forever
runCommand : Stream Int -> GameState -> Command a -> IO (a, Stream Int, GameState)
runCommand rnds state (PutStr x) = do putStr x
pure ((), rnds, state)
runCommand rnds state GetLine = do str <- getLine
pure (str, rnds, state)
runCommand (random :: randoms) state GetRandom = pure (getRandom random (difficulty state), randoms, state)
where getRandom : Int -> Int -> Int
getRandom val max with (divides val max)
getRandom val 0 | DivByZero = 1
getRandom ((max * div) + rem) max | (DivBy prf) = abs rem + 1
runCommand rnds state GetGameState = pure (state, rnds, state)
runCommand rnds state (PutGameState newState) = pure ((), rnds, newState)
runCommand rnds state (Pure x) = pure (x, rnds, state)
runCommand rnds state (Bind c f) = do (res, rnds', state') <- runCommand rnds state c
runCommand rnds' state' (f res)
run : Fuel -> Stream Int -> GameState -> ConsoleIO a -> IO (Maybe a, Stream Int, GameState)
run fuel randoms state (Quit val) = pure (Just val, randoms, state)
run (More fuel) randoms state (Do c f) = do (res, newRandoms, newState) <- runCommand randoms state c
run fuel newRandoms newState (f res)
run Dry randoms state (Do c f) = pure (Nothing, randoms, state)
data Input = Answer Int
| QuitCmd
updateGameState : (GameState -> GameState) -> Command ()
updateGameState f = do
state <- GetGameState
PutGameState (f state)
mutual
correct : ConsoleIO GameState
correct = do PutStr "Correct!\n"
updateGameState addCorrect
quiz
wrong : Int -> ConsoleIO GameState
wrong ans = do PutStr ("Wrong! " ++ show ans)
updateGameState addWrong
quiz
readInput : (prompt : String) -> Command Input
readInput prompt = do PutStr prompt
answer <- GetLine
if answer == "quit"
then Pure QuitCmd
else Pure (Answer (cast answer))
quiz : ConsoleIO GameState
quiz = do num1 <- GetRandom
num2 <- GetRandom
st <- GetGameState
PutStr (show st ++ "\n")
input <- readInput ((show num1) ++ " * " ++ (show num2))
case input of
Answer answer => if answer == num1 * num2
then correct
else wrong (num1 * num2)
QuitCmd => Quit st
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
(seed' `shiftR` 2) :: randoms seed'
partial
main : IO ()
main = do seed <- time
(Just score, _, state) <-
run forever (randoms (fromInteger seed)) initState quiz
| _ => putStrLn "Ran out of fuel."
putStrLn ("Final score: " ++ (show state))
Raw
ArithTotal.idr
module Main
import Data.Primitives.Views
import System
%default total
data InfIO : Type where
Do : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do
data Fuel = Dry | More (Lazy Fuel)
partial
forever : Fuel
forever = More forever
run : Fuel -> InfIO -> IO ()
run Dry y = putStrLn "Out of fuel."
run (More fuel) (Do action continuation) = do
result <- action
run fuel (continuation result)
quiz : Stream Int -> (score : Nat) -> InfIO
quiz (num1 :: num2 :: xs) score = do
putStrLn ("You current score is: " ++ show score)
putStrLn ((show num1) ++ " * " ++ (show num2) ++ " ?")
line <- getLine
if cast line == (num1 * num2)
then do
putStrLn "Correct!"
quiz xs (score +1)
else do
putStrLn "Wrong!"
quiz xs score
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
(seed' `shiftR` 2) :: randoms seed'
arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
where
bound : Int -> Int
bound x with (Data.Primitives.Views.Int.divides x 12)
bound ((12 * div) + rem) | (DivBy prf) = rem + 1
totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
totalREPL prompt action = do
putStrLn prompt
line <- getLine
putStrLn (action line)
totalREPL prompt action
partial
main : IO ()
main = do seed <- time
run forever (quiz (arithInputs (fromInteger seed)) 0)
Raw
ATM.idr
module ATM
import Data.Vect
%default total
PIN : Type
PIN = Vect 4 Char
data ATMState = Ready | CardInserted | Session
data PINCheck = CorrectPIN | IncorrectPIN
data HasCard : ATMState -> Type where
HasCI : HasCard CardInserted
HasSession : HasCard Session
data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where
InsertCard : ATMCmd () Ready (const CardInserted)
EjectCard : {auto prf : HasCard state} -> ATMCmd () state (const Ready)
GetPIN : ATMCmd PIN CardInserted (const CardInserted)
CheckPIN : PIN -> ATMCmd PINCheck CardInserted
(\check => case check of
CorrectPIN => Session
IncorrectPIN => CardInserted)
GetAmount : ATMCmd Nat state (const state)
Dispense : (amount : Nat) -> ATMCmd () Session (const Session)
Message : (message : String) -> ATMCmd () state (const state)
Pure : (res : ty) -> ATMCmd ty (state_fn res) state_fn
(>>=) : ATMCmd a state1 state2_fn ->
((res : a) -> ATMCmd b (state2_fn res) state3_fn) ->
ATMCmd b state1 state3_fn
atm : ATMCmd () Ready (const Ready)
atm = do InsertCard
pin <- GetPIN
cash <- GetAmount
pinOK <- CheckPIN pin
case pinOK of
CorrectPIN => do Dispense cash
EjectCard
Message "Please remove your card and cash"
IncorrectPIN => do Message "Incorrect PIN"
EjectCard
testPIN : PIN
testPIN = ['1', '2', '3', '4']
readVect : (n : Nat) -> IO (Vect n Char)
readVect Z = do discard <- getLine
pure []
readVect (S k) = do ch <- getChar
rest <- readVect k
pure (ch :: rest)
runATM : ATMCmd res inState outState_fn -> IO res
runATM InsertCard = do putStrLn "Please insert your card (press enter)"
discard <- getLine
pure ()
runATM EjectCard = putStrLn "Card ejected."
runATM GetPIN = do putStrLn "Enter PIN: "
readVect 4
runATM (CheckPIN pin) = pure $ if (pin == testPIN)
then CorrectPIN
else IncorrectPIN
runATM GetAmount = do putStrLn "How much would you like?"
amount <- getLine
pure (cast amount)
runATM (Dispense amount) = putStrLn ("Here is " ++ show amount)
runATM (Message message) = putStrLn message
runATM (Pure res) = pure res
runATM (x >>= f) = do x' <- runATM x
runATM (f x')
Raw
CheckEqMaybe.idr
module CheckEqMaybe
checkEqNat : (j : Nat) -> (k : Nat) -> Maybe (j = k)
checkEqNat Z Z = Just $ Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S j) Z = Nothing
checkEqNat (S j) (S k) = case checkEqNat j k of
Nothing => Nothing
Just prf => Just $ cong prf
Raw
DataStore.idr
module main
import Data.Vect
data DataStore : Type where
MkData : (size : Nat) ->
(items : Vect size String) ->
DataStore
size : DataStore -> Nat
size (MkData size' items) = size'
items : (store : DataStore) -> Vect (size store) String
items (MkData size items) = items
addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newitem = MkData _ (addToData items)
where
addToData : Vect oldLength String -> Vect (S oldLength) String
addToData [] = [newitem]
addToData (x :: xs) = x :: (addToData xs)
data Command = Add String
| Get Integer
| Size
| Search String
| Quit
parseCommand : String -> String -> Maybe Command
parseCommand "add" rest = Just $ Add (ltrim rest)
parseCommand "get" id = if all isDigit (unpack $ ltrim id)
then Just $ Get $ cast id
else Nothing
parseCommand "quit" "" = Just Quit
parseCommand "size" "" = Just Size
parseCommand "search" pattern = Just $ Search (ltrim pattern)
parseCommand _ _ = Nothing
parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
(cmd, args) => parseCommand cmd args
getEntry : (pos : Integer) -> (store : DataStore) -> Maybe String
getEntry pos store = let storeItems = items store in
case integerToFin pos (size store) of
Nothing => Just "out of range\n"
Just id => Just $ (index id storeItems) ++ "\n"
searchData : (pattern : String) -> (store : DataStore) -> List String
searchData pattern (MkData size items) = searchItem Z items
where
searchItem : Nat -> Vect n String -> List String
searchItem index [] = []
searchItem index (x :: xs) = if isInfixOf pattern x
then ((show index) ++ " - " ++ x) :: searchItem (S index) xs
else searchItem (S index) xs
processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse input of
Nothing => Just ("Invalid command\n", store)
Just (Add item) => Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
Just (Get id) => (\x => (x,store)) <$> (getEntry id store)
Just Quit => Nothing
Just Size => Just ("Size: " ++ (show $ size store) ++ "\n", store)
Just (Search pattern) => Just (show (searchData pattern store) ++ "\n", store)
main : IO ()
main = replWith (MkData _ []) "Command: " processInput
Raw
DataStore2.idr
module main
import Data.Vect
infixr 5 .+.
data Schema = SString
| SInt
| (.+.) Schema Schema
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)
record DataStore where
constructor MkData
schema : Schema
size : Nat
items : Vect size (SchemaType schema)
addToStore : (store : DataStore) -> (SchemaType (schema store)) -> DataStore
addToStore (MkData schema size items) newitem = MkData schema _ (addToData items)
where
addToData : Vect oldLength (SchemaType schema) -> Vect (S oldLength) (SchemaType schema)
addToData [] = [newitem]
addToData (x :: xs) = x :: (addToData xs)
getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (SchemaType (schema store))
getEntry pos store = let storeItems = items store in
case integerToFin pos (size store) of
Nothing => Nothing
Just id => Just $ (index id storeItems)
data Command : Schema -> Type where
Add : SchemaType schema -> Command schema
Get : Integer -> Command schema
Quit : Command schema
parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input)
where getQuoted : List Char -> Maybe (String, String)
getQuoted ('"' :: xs) = case span (/= '"') xs of
(quoted, '"' :: rest) => Just (pack quoted, ltrim $ pack rest)
_ => Nothing
getQuoted _ = Nothing
parsePrefix SInt x = case span isDigit x of
("", rest) => Nothing
(num, rest) => Just (cast num, ltrim rest)
parsePrefix (l .+. r) input = do
(leftVal, input') <- parsePrefix l input
(rightVal, input'') <- parsePrefix r input'
pure ((leftVal, rightVal), input'')
parseBySchema : (schema : Schema) -> (rest : String) -> Maybe (SchemaType schema)
parseBySchema schema rest = case parsePrefix schema rest of
Just (res, "") => Just res
Just _ => Nothing
Nothing => Nothing
parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema "add" rest = case parseBySchema schema rest of
Nothing => Nothing
Just restok => Just (Add restok)
parseCommand schema "get" id = if all isDigit (unpack $ id)
then Just $ Get $ cast id
else Nothing
parseCommand schema "quit" "" = Just Quit
parseCommand _ _ _ = Nothing
parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
(cmd, args) => parseCommand schema cmd (ltrim args)
display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (l, r) = display l ++ ", " ++ display r
processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse (schema store) input of
Nothing => Just ("Invalid command\n", store)
Just (Add item) => Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
Just (Get id) => (\x => (display x,store)) <$> (getEntry id store)
Just Quit => Nothing
main : IO ()
main = replWith (MkData SString _ []) "Command: " processInput
Raw
DataStore3.idr
module DataStrore
import Data.Vect
infixr 5 .+.
public export
data Schema = SString
| SInt
| (.+.) Schema Schema
public export
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)
export
record DataStore (schema : Schema) where
constructor MkData
size : Nat
items : Vect size (SchemaType schema)
export
empty : DataStore schema
empty = MkData 0 []
export
addToStore : (value : SchemaType schema) -> (store : DataStore schema) -> DataStore schema
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)
private
storeViewHelp : (items : Vect size (SchemaType schema)) -> StoreView (MkData size items)
storeViewHelp [] = SNil
storeViewHelp (x :: xs) = SAdd (storeViewHelp xs)
export
storeView : (store : DataStore schema) -> StoreView store
storeView (MkData size items) = storeViewHelp items
export
testStore : DataStore (SString .+. SString .+. SInt)
testStore = addToStore ("Mercury", "Mariner 10", 1974) $
addToStore ("Venus", "Venera", 1961) $
addToStore ("Uranus", "Voyager 2", 1986) $
addToStore ("Pluto", "New Horizons", 2015) $
empty
export
listItems : DataStore schema -> List (SchemaType schema)
listItems store with (storeView store)
listItems store | SNil = []
listItems (addToStore value rest) | (SAdd rec) = value :: (listItems rest | rec)
export
filterKeys : (test: SchemaType val_schema -> Bool) ->
DataStore (SString .+. val_schema) ->
List String
filterKeys test store with (storeView store)
filterKeys test store | SNil = []
filterKeys test (addToStore (key, value) rest) | (SAdd rec) =
if test value then key :: (filterKeys test rest | rec)
else (filterKeys test rest |rec)
export
getValues : DataStore (SString .+. val_schema) -> List (SchemaType val_schema)
getValues store with (storeView store)
getValues store | SNil = []
getValues (addToStore (key, value) rest) | (SAdd rec) = value :: (getValues rest | rec)
Raw
DescribeList.idr
module Main
data ListLast : List a -> Type where
Empty : ListLast []
Nonempty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
Empty => Nonempty [] x
Nonempty ys y => Nonempty (x :: ys) y
describeHelper : (input : List Int) -> (form : ListLast input) -> String
describeHelper [] Empty = "Empty list"
describeHelper (xs ++ [x]) (Nonempty xs x) = "Non empty, initial portion = " ++ show xs
describeListEnd : List Int -> String
describeListEnd xs with (listLast xs)
describeListEnd [] | Empty = "Empty"
describeListEnd (ys ++ [x]) | (Nonempty ys x) = "Non empty, initial portion = " ++ show ys
myReverse : List a -> List a
myReverse xs with (listLast xs)
myReverse [] | Empty = []
myReverse (ys ++ [x]) | (Nonempty ys x) = x :: myReverse ys
Raw
Door.idr
module Door
data DoorState = DoorClosed | DoorOpen
data DoorCmd : Type -> DoorState -> DoorState -> Type where
Open : DoorCmd () DoorClosed DoorOpen
Close : DoorCmd () DoorOpen DoorClosed
RingBell : DoorCmd () s s
Pure : ty -> DoorCmd ty state state
(>>=) : DoorCmd a state1 state2 ->
(a -> DoorCmd b state2 state3) ->
DoorCmd b state1 state3
doorProg : DoorCmd () DoorClosed DoorClosed
doorProg = do RingBell
Open
Close
doorProg2 : DoorCmd () DoorClosed DoorClosed
doorProg2 = do
RingBell
Open
RingBell
Close
Raw
ElemDemo.idr
module ElemDemo
import Data.Vect
maryInVector : Elem "Mary" ["Peter", "Paul", "Mary"]
maryInVector = There (There Here)
Raw
ElemType.idr
module ElemType
import Data.Vect
data MyElem : a -> Vect k a -> Type where
Here : MyElem x (x::xs)
There : (later : MyElem x xs) -> MyElem x (y::xs)
notInNil : MyElem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible
notInTail : (notHere : (value = x) -> Void) ->
(notThere : MyElem value xs -> Void) ->
MyElem value (x :: xs) -> Void
notInTail notHere notThere Here = notHere Refl
notInTail notHere notThere (There later) = notThere later
myIsElem : DecEq a => (value : a) -> (xs : Vect len a) -> Dec (MyElem value xs)
myIsElem value [] = No notInNil
myIsElem value (x :: xs) = case decEq value x of
Yes Refl => Yes Here
No notHere => case myIsElem value xs of
Yes prf => Yes (There prf)
No notThere => No (notInTail notHere notThere)
Raw
EqExercises.idr
module EqExercises
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons prf = cong prf
same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl lstSame = cong lstSame
data ThreeEq : a -> b -> c -> Type where
Same : (x : a) -> ThreeEq x x x
allSames : (x : Nat) -> (y : Nat) -> (z : Nat) -> (ThreeEq x y z) -> ThreeEq (S x) (S y) (S z)
allSames z z z (Same z) = Same (S z)
Raw
EqNat.idr
module EqNat
public export
data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
Same : (num : Nat) -> EqNat num num
sameS : (k : Nat) -> (j : Nat) -> (EqNat k j) -> EqNat (S k) (S j)
sameS j j (Same j) = Same (S j)
public export
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just $ Same Z
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
Nothing => Nothing
Just eq => Just $ sameS k j eq
zeroNotSuc : (0 = S k) -> Void
zeroNotSuc Refl impossible
sucNotZero : (S k = 0) -> Void
sucNotZero Refl impossible
noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl
checkEqNatDec : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNatDec Z Z = Yes Refl
checkEqNatDec Z (S k) = No zeroNotSuc
checkEqNatDec (S k) Z = No sucNotZero
checkEqNatDec (S k) (S j) = case checkEqNatDec k j of
Yes prf => Yes (cong prf)
No contra => No (noRec contra)
Raw
Equality.idr
module Equality
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : (x : a) -> (xs : Vect k a) -> (Vect (S k) a)
headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
(contra : (x = y) -> Void) ->
((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl
tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
(contra : (xs = ys) -> Void) ->
((x :: xs) = (y :: ys)) -> Void
tailUnequal contra Refl = contra Refl
implementation DecEq a => DecEq (Vect n a) where
decEq [] [] = Yes Refl
decEq (x :: xs) (y :: ys) = case decEq x y of
No contra => No $ headUnequal contra
Yes Refl => case decEq xs ys of
No contra' => No $ tailUnequal contra'
Yes Refl => Yes Refl
Raw
ExactLengthFirst.idr
module ExactLength
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : (elem : a) -> Vect len a -> Vect (S len) a
exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case m == len of
False => Nothing
True => Just ?unableToConvertVectmaToVectlena
Raw
ExactLengthSecond.idr
module ExactLength
import EqNat
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : (elem : a) -> Vect len a -> Vect (S len) a
exactLength : (len1 : Nat) -> (input : Vect len2 a) -> Maybe (Vect len1 a)
exactLength {len2} len1 input = case checkEqNat len1 len2 of
Nothing => Nothing
Just (Same len2) => Just $ input
Raw
ExactLengthThird.idr
module ExactLength
import Data.Vect
exactLength : (len : Nat) -> (Vect n a) -> Maybe (Vect len a)
exactLength {n} len xs = case decEq len n of
Yes Refl => Just xs
No _ => Nothing
Raw
Exercise102.idr
module Exercise102
import Data.List.Views
import Data.Vect.Views
import Data.Vect
import Data.Nat.Views
equalSuffix : Eq a => List a -> List a -> List a
equalSuffix input1 input2 with (snocList input1)
equalSuffix [] input2 | Empty = []
equalSuffix (xs ++ [x]) input2 | (Snoc xrec) with (snocList input2)
equalSuffix (xs ++ [x]) [] | (Snoc xrec) | Empty = []
equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xrec) | (Snoc yrec) =
if x == y then (equalSuffix xs ys | xrec | yrec) ++ [x]
else []
mergeSort : Ord a => Vect n a -> Vect n a
mergeSort xs with (splitRec xs)
mergeSort [] | SplitRecNil = []
mergeSort [x] | SplitRecOne = [x]
mergeSort (ys ++ zs) | (SplitRecPair lrec rrec) = merge (mergeSort ys | lrec) (mergeSort zs | rrec)
toBinary : Nat -> String
toBinary k with (halfRec k)
toBinary Z | HalfRecZ = ""
toBinary (n + n) | (HalfRecEven rec) = (toBinary n) ++ "0"
toBinary (S (n + n)) | (HalfRecOdd rec) = (toBinary n) ++ "1"
palindrome : Eq a => List a -> Bool
palindrome input with (vList input)
palindrome [] | VNil = True
palindrome [x] | VOne = True
palindrome (x :: (xs ++ [y])) | (VCons rec) = x == y && palindrome xs | rec
Raw
Exercise111.idr
module Exercise111
import Data.Primitives.Views
import InfList
import Arith
every_other : Stream a -> Stream a
every_other (x1 :: x2 :: xs) = x2 :: every_other xs
data Face : Type where
Heads : Face
Tails : Face
coinFlips : (count : Nat) -> Stream Int -> List Face
coinFlips Z (value :: xs) = []
coinFlips (S k) (value :: xs) with (divides value 2)
coinFlips (S k) (((2 * div) + rem) :: xs) | (DivBy prf) =
let current = if rem == 0 then Heads else Tails in
current :: coinFlips k xs
square_root_approx : (number : Double) -> (approx : Double) -> Stream Double
square_root_approx number approx = let next = (approx + (number / approx)) / 2 in
approx :: square_root_approx number next
square_root_bound : (max : Nat) -> (number : Double) -> (bound : Double) ->
(approxs : Stream Double) -> Double
square_root_bound Z number bound (value :: xs) = value
square_root_bound (S k) number bound (value :: xs) = let diff = abs (number - (value * value)) in
if diff < bound
then value
else square_root_bound k number bound xs
square_root : (number : Double) -> Double
square_root number = square_root_bound 100 number 0.00000000001 (square_root_approx number number)
Raw
Exercise123.idr
module Exercise123
record Votes where
constructor MkVotes
upvotes : Integer
downvotes : Integer
record Article where
constructor MkArticle
title : String
url : String
score : Votes
addUpVote : Article -> Article
addUpVote = record {score->upvotes $= (+1)}
addDownVote : Article -> Article
addDownVote = record {score->downvotes $= (+1)}
initPage : (title: String) -> (url: String) -> Article
initPage title url = MkArticle title url (MkVotes 0 0)
getScore : Article -> Integer
getScore a = (upvotes (score a)) - (downvotes (score a))
badSite : Article
badSite = MkArticle "Bad Site Title" "badsite.com" (MkVotes 5 47)
Raw
Greet.idr
module Main
import RunIO
%default total
greet : RunIO ()
greet = do putStrLn "Enter your name: "
name <- getLine
if name == ""
then do putStrLn "Bye."
Quit ()
else do putStrLn ("Hello " ++ name)
greet
partial
main : IO ()
main = do
run forever greet
pure ()
Raw
GuessExercise.idr
module GuessExercise
data GuessCmd : Type -> Nat -> Nat -> Type where
Try : Integer -> GuessCmd Ordering (S guessesLeft) guessesLeft
Pure : ty -> GuessCmd ty state state
(>>=) : GuessCmd a state1 state2 -> (a -> GuessCmd b state2 state3) -> GuessCmd b state1 state3
threeGuesses : GuessCmd () 3 0
threeGuesses = do
Try 10
Try 20
Try 15
Pure ()
--noGuesses : GuessCmd () 0 0
--noGuesses = do Try 10
-- Pure ()
Raw
Hangman.idr
module Main
import Data.Vect
removeElem : (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem {n = (S k)} value (y :: ys) {prf = (There later)} = y :: removeElem value ys
removeElem {n = Z} value (y :: []) {prf = (There later)} = absurd later
data WordState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
MkWordState : (word : String) ->
(missingLetters : Vect letters Char) ->
WordState guesses_remaining letters
data Finished : Type where
Lost: (game : WordState Z (S letters)) -> Finished
Won: (game : WordState (S guesses_remaining) Z) -> Finished
data ValidInput : List Char -> Type where
Letter : (c : Char) -> ValidInput [c]
isNilValid : ValidInput [] -> Void
isNilValid (Letter _) impossible
isValidTwo : ValidInput (x :: (y :: xs)) -> Void
isValidTwo (Letter _) impossible
isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No isNilValid
isValidInput (x :: []) = Yes $ Letter x
isValidInput (x :: (y :: xs)) = No isValidTwo
isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)
processGuess : (letter : Char) ->
WordState (S guesses) (S letters) ->
Either (WordState guesses (S letters))
(WordState (S guesses) letters)
processGuess letter (MkWordState word missing) = case isElem letter missing of
Yes prf => Right $ MkWordState word (removeElem letter missing)
No contra => Left $ MkWordState word missing
readGuess : IO (x ** ValidInput x)
readGuess = do putStr "Guess: "
line <- getLine
case isValidString line of
Yes prf => pure (_ ** prf)
No contra => do putStrLn "Invalid guess"
readGuess
game : WordState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st =
do (_ ** Letter guess) <- readGuess
case processGuess guess st of
Left l => do putStrLn "Wrong!"
case guesses of
Z => pure (Lost l)
S k => game l
Right r => do putStrLn "Right!"
case letters of
Z => pure (Won r)
S k => game r
main : IO ()
main = do result <- game {guesses = 2} (MkWordState "Test" ['T', 'e', 's', 't'])
case result of
Lost game => putStrLn "You loose."
Won game => putStrLn "You Win!"
Raw
Hangman2.idr
module Hangman2
import Data.Vect
%default total
data GameState : Type where
NotRunning : GameState
Running : (guesses : Nat) -> (letters : Nat) -> GameState
data Game : GameState -> Type where
GameStart : Game NotRunning
GameWon : (word : String) -> Game NotRunning
GameLost : (word : String) -> Game NotRunning
InProgress : (word : String) ->
(guesses : Nat) ->
(missing : Vect letters Char) ->
Game (Running guesses letters)
Show (Game g) where
show GameStart = "Starting"
show (GameWon word) = "Game won: " ++ word
show (GameLost word) = "Game lost: " ++ word
show (InProgress word guesses missing) = "\n" ++ pack (map hideMissing (unpack word)) ++ "\n" ++ show guesses ++ " guesses left"
where hideMissing : Char -> Char
hideMissing c = if c `elem` missing then '-' else c
data GuessResult = Correct | Incorrect
uniqueLetters : String -> List Char
uniqueLetters str = nub (toUpper <$> (unpack str))
data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
NewGame : (word : String) -> GameCmd () NotRunning (const (Running 6 (List.length (uniqueLetters word))))
Won : GameCmd () (Running (S guesses) 0) (const NotRunning)
Lost : GameCmd () (Running 0 (S letters)) (const NotRunning)
Guess : (c : Char) -> GameCmd GuessResult (Running (S guesses) (S letters)) (\res => case res of
Correct => Running (S guesses) letters
Incorrect => Running guesses (S letters))
ShowState : GameCmd () state (const state)
Message : String -> GameCmd () state (const state)
ReadGuess : GameCmd Char state (const state)
Pure : (res : ty) -> GameCmd ty (state_fn res) state_fn
(>>=) : GameCmd a state1 state2_fn ->
((res : a) -> GameCmd b (state2_fn res) state3_fn) ->
GameCmd b state1 state3_fn
namespace Loop
data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
(>>=) : GameCmd a state1 state2_fn ->
((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
GameLoop b state1 state3_fn
Exit : GameLoop () NotRunning (const NotRunning)
gameLoop : GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
gameLoop {guesses} {letters} = do
ShowState
g <- ReadGuess
ok <- Guess g
case ok of
Correct => case letters of
Z => do Won
ShowState
Exit
(S k) => do Message "Correct"
gameLoop
Incorrect => case guesses of
Z => do Lost
ShowState
Exit
(S k) => do Message "Incorrect"
gameLoop
hangman : GameLoop () NotRunning (const NotRunning)
hangman = do NewGame "testing"
gameLoop
data Fuel = Dry | More (Lazy Fuel)
partial
forever : Fuel
forever = More forever
data GameResult : (ty : Type) -> (ty -> GameState) -> Type where
OK : (res : ty) -> Game (outstate_fn res) -> GameResult ty outstate_fn
OutOfFuel : GameResult ty outstate_fn
ok : (res : ty) -> Game (outstate_fn res) -> IO (GameResult ty outstate_fn)
ok res st = pure (OK res st)
removeElem : (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem {n = (S k)} value (y :: ys) {prf = (There later)} = y :: removeElem value ys
removeElem {n = Z} value (y :: []) {prf = (There later)} = absurd later
runCmd : Fuel ->
Game instate ->
GameCmd ty instate outstate_fn ->
IO (GameResult ty outstate_fn)
runCmd fuel state (NewGame word) = ok () (InProgress (toUpper word) _ (fromList (uniqueLetters word)))
runCmd fuel (InProgress word _ missing) Won = ok () (GameWon word)
runCmd fuel (InProgress word _ missing) Lost = ok () (GameLost word)
runCmd fuel (InProgress word _ missing) (Guess c) = case isElem c missing of
Yes prf => ok Correct (InProgress word _ (removeElem c missing))
No contra => ok Incorrect (InProgress word _ missing)
runCmd fuel state ShowState = do printLn state
ok () state
runCmd fuel state (Message x) = do putStrLn x
ok () state
runCmd (More fuel) state ReadGuess = do putStr "Guess: "
input <- getLine
case unpack input of
[x] => if isAlpha x
then ok (toUpper x) state
else do putStrLn "Invalid input"
runCmd fuel state ReadGuess
_ => do putStrLn "Invalid input"
runCmd fuel state ReadGuess
runCmd fuel state (Pure res) = ok res state
runCmd fuel state (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel state cmd
| OutOfFuel => pure OutOfFuel
runCmd fuel newSt (next cmdRes)
runCmd Dry _ _ = pure OutOfFuel
run : Fuel ->
Game instate ->
GameLoop ty instate outstate_fn ->
IO (GameResult ty outstate_fn)
run Dry _ _ = pure OutOfFuel
run (More fuel) st (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel st cmd
| OutOfFuel => pure OutOfFuel
run fuel newSt (next cmdRes)
run (More x) st Exit = ok () st
partial
main : IO ()
main = do run forever GameStart hangman
pure ()
Raw
InfIO.idr
module InfIO
%default total
public export
data InfIO : Type where
Do : IO a -> (a -> Inf InfIO) -> InfIO
public export
(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do
loopPrint : String -> InfIO
loopPrint msg = do
putStrLn msg
loopPrint msg
public export
data Fuel = Dry | More (Lazy Fuel)
public export
partial
forever : Fuel
forever = More forever
public export
run : Fuel -> InfIO -> IO ()
run Dry y = putStrLn "Out of fuel."
run (More x) (Do action continuation) = do
result <- action
run x (continuation result)
Raw
InfList.idr
module InfList
data InfList : Type -> Type where
(::) : (item : elem) -> Inf (InfList elem) -> InfList elem
Functor InfList where
map f (item :: xs) = (f item) :: map f xs
%name InfList xs, ys, zs
countFrom : Integer -> InfList Integer
countFrom x = x :: (countFrom (x+1))
getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z xs = []
getPrefix (S k) (item :: xs) = item :: getPrefix k xs
Raw
LastList.idr
module LastList
data Last : List a -> a -> Type where
LastOne : Last [value] value
LastCons : (pfr : Last xs value) -> Last (x::xs) value
notInNil : Last [] value -> Void
notInNil LastOne impossible
notInNil (LastCons _) impossible
lastNotEqual : (notEqualProof : (x = value) -> Void) -> (notLastInTailProof : Last [] value -> Void) -> Last [x] value -> Void
lastNotEqual notEqualProof notLastInTailProof LastOne = notEqualProof Refl
lastNotEqual _ _ (LastCons LastOne) impossible
lastNotEqual _ _ (LastCons (LastCons _)) impossible
cantBeLast : (notLastInTailProof : Last (y :: ys) value -> Void) -> Last (x :: (y :: ys)) value -> Void
cantBeLast notLastInTailProof (LastCons pfr) = notLastInTailProof pfr
isLastHelper : DecEq a => {xs : List a} -> {value : a} -> (notLastInTailProof : Last xs value -> Void) -> Dec (Last (x :: xs) value)
isLastHelper {xs = []} {x = x} {value = value} notLastInTailProof = case decEq x value of
Yes Refl => Yes $ LastOne
No notEqualProof => No $ (lastNotEqual notEqualProof notLastInTailProof)
isLastHelper {xs = (y :: ys)} {x = x} {value = value} notLastInTailProof = No (cantBeLast notLastInTailProof)
isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No notInNil
isLast (x :: xs) value = case isLast xs value of
Yes lastInTailProof => Yes (LastCons lastInTailProof)
No notLastInTailProof => isLastHelper notLastInTailProof
Raw
ListElem.idr
module ListElem
data Elem : (value : a) -> (xs : List a) -> Type where
Here : Elem value (x::rest)
There : Elem value xs -> Elem value (y::xs)
Raw
ListProc.idr
module ListProc
import ProcessLib
%default total
data ListAction : Type where
Length : List elem -> ListAction
Append : List elem -> List elem -> ListAction
ListType : ListAction -> Type
ListType (Length lst) = Nat
ListType (Append {elem} l r) = List elem
procList : Process ListType () NoRequest Complete
procList = do Respond (\msg => (case msg of
(Length xs) => Pure (length xs)
(Append xs ys) => Pure (xs ++ ys)))
Loop procList
procMain : Process ListType () NoRequest NoRequest
procMain = do Just list <- Spawn procList
| Nothing => Action (putStrLn "Spawn failed")
len <- Request list (Length [1,2,3])
Action (printLn len)
app <- Request list (Append [1,2,3] [10,42])
Action (printLn app)
Raw
Matrix.idr
module Main
import Data.Vect
createEmpties : Vect m (Vect 0 elem)
createEmpties = replicate _ []
transposeHelper : (x : Vect m elem) -> (transposedXs : Vect m (Vect len elem)) -> Vect m (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: ys) (y :: xs) = (x :: y) :: transposeHelper ys xs
transposeMat : Vect n (Vect m elem) -> Vect m (Vect n elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let transposedXs = transposeMat xs in
transposeHelper x transposedXs
total transposeMat2 : Vect n (Vect m elem) -> Vect m (Vect n elem)
transposeMat2 [] = createEmpties
transposeMat2 (x :: xs) = zipWith (::) x (transposeMat2 xs)
addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix = zipWith (zipWith (+))
anothermult : Num a => (x : Vect m a) -> (ys : Vect m (Vect p a)) -> Vect m a -> Vect p (Vect m a) -> Vect p a
multmap : Num a => (x : Vect m a) -> (ys : Vect m (Vect p a)) -> Vect p a
multmap x ys = anothermult x ys x (transposeMat2 ys)
multMatrix : Num a => Vect n (Vect m a) -> Vect m (Vect p a) -> Vect n (Vect p a)
multMatrix [] _ = []
multMatrix (x :: xs) ys = let finalRow = multmap x ys in
finalRow :: multMatrix xs ys
main : IO ()
main = do
--print $ transposeMat [[1, 2], [3, 4], [5, 6]]
--print $ transposeMat2 [[1, 2], [3, 4], [5, 6]]
--print $ addMatrix [[1,2,3], [4,5,6]] [[1,1,1], [1,1,1]]
print $ multMatrix [[1, 2], [3, 4], [5, 6]] [[7, 8, 9, 10], [11, 12, 13, 14]]
Raw
Matrix2.idr
module Main
import Data.Vect
Matrix : Nat -> Nat -> Type
Matrix k j = Vect k (Vect j Double)
testMatrix : Matrix 2 3
testMatrix = [[0,0,0], [0,0,0]]
main : IO ()
main = print "kutyus"
Raw
Matter.idr
module Matter
%default total
data Matter = Solid | Liquid | Gas
data MatterCmd : Type -> Matter -> Matter -> Type where
Melt : MatterCmd () Solid Liquid
Boil : MatterCmd () Liquid Gas
Condense : MatterCmd () Gas Liquid
Freeze : MatterCmd () Liquid Solid
(>>=) : MatterCmd a state1 state2 -> (a -> MatterCmd b state2 state3) -> MatterCmd b state1 state
iceSteam : MatterCmd () Solid Gas
iceSteam = do
Melt
Boil
steamIce : MatterCmd () Gas Solid
steamIce = do
Condense
Freeze
-- overMelt : MatterCmd () Solid Gas
-- overMelt = do
-- Melt
-- Melt
Raw
MergeSort.idr
module Main
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) =
case splitListHelp counter items of
SplitNil => SplitOne
SplitOne {x} => SplitPair [item] [x]
SplitPair lefts rights => SplitPair (item :: lefts) rights
splitListHelp _ items = SplitPair [] items
mergeSort : Ord a => List a -> List a
mergeSort input with (splitList input)
mergeSort [] | SplitNil = []
mergeSort [x] | SplitOne = [x]
mergeSort (lefts ++ rights) | (SplitPair lefts rights) = merge (mergeSort lefts) (mergeSort rights)
Raw
MergeSortView.idr
module MergeSortView
import Data.List.Views
%default total
mergeSort : Ord a => List a -> List a
mergeSort input with (splitRec input)
mergeSort [] | SplitRecNil = []
mergeSort [x] | SplitRecOne = [x]
mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) =
merge (mergeSort lefts | lrec)
(mergeSort rights | rrec)
Raw
PlusCommutes.idr
module PlusCommutes
myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = sym $ plusZeroRightNeutral m
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in plusSuccRightSucc m k
Raw
Printf.idr
module Main
data Format = Number Format
| Str Format
| Chr Format
| Dbl Format
| Lit String Format
| End
PrintfType : Format -> Type
PrintfType (Number fmt) = (i: Int) -> PrintfType fmt
PrintfType (Str fmt) = (s: String) -> PrintfType fmt
PrintfType (Chr fmt) = (c: Char) -> PrintfType fmt
PrintfType (Dbl fmt) = (d: Double) -> PrintfType fmt
PrintfType (Lit x fmt) = PrintfType fmt
PrintfType End = String
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number x) acc = \i => printfFmt x (acc ++ show i)
printfFmt (Str x) acc = \s => printfFmt x (acc ++ s)
printfFmt (Chr x) acc = \c => printfFmt x (acc ++ strCons c "")
printfFmt (Dbl x) acc = \d => printfFmt x (acc ++ show d)
printfFmt (Lit x y) acc = printfFmt y (acc ++ x)
printfFmt End acc = acc
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: xs) = Number $ toFormat xs
toFormat ('%' :: 's' :: xs) = Str $ toFormat xs
toFormat ('%' :: 'c' :: xs) = Chr $ toFormat xs
toFormat ('%' :: 'f' :: xs) = Dbl $ toFormat xs
toFormat ('%' :: xs) = Lit "%" (toFormat xs)
toFormat (x :: xs) = case toFormat xs of
Lit lit chars' => Lit (strCons x lit) chars'
fmt => Lit (strCons x "") fmt
printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""
main : IO ()
main = print "kutyus"
Raw
Process.idr
module Main
import System.Concurrency.Channels
%default total
data Message = Add Nat Nat
data MessagePID = MkMessage PID
data Fuel = Dry | More (Lazy Fuel)
data Process : Type -> Type where
Action : IO a -> Process a
Spawn : Process () -> Process (Maybe MessagePID)
Request : MessagePID -> Message -> Process (Maybe Nat)
Respond : ((msg : Message) -> Process Nat) -> Process (Maybe Message)
Loop : Inf (Process a) -> Process a
Pure : a -> Process a
(>>=) : Process a -> (a -> Process b) -> Process b
run : Fuel -> Process t -> IO (Maybe t)
run Dry _ = pure Nothing
run fuel (Action act) = do res <- act
pure (Just res)
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
pure ())
| Nothing => pure Nothing
pure (Just (Just (MkMessage pid)))
run fuel (Request (MkMessage process) msg) = do Just chan <- connect process
| _ => pure (Just Nothing)
ok <- unsafeSend chan msg
if ok then do Just x <- unsafeRecv Nat chan
| Nothing => pure (Just Nothing)
pure (Just (Just x))
else pure (Just Nothing)
run fuel (Respond calc) = do Just sender <- listen 1
| Nothing => pure (Just Nothing)
Just msg <- unsafeRecv Message sender
| Nothing => pure (Just Nothing)
Just res <- run fuel (calc msg)
| Nothing => pure Nothing
unsafeSend sender res
pure (Just (Just msg))
run (More fuel) (Loop act) = run fuel act
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
| Nothing => pure Nothing
run fuel (next x)
procAdder : Process ()
procAdder = do Respond (\msg => case msg of Add x y => Pure (x + y))
Loop procAdder
procMain : Process ()
procMain = do Just adder_id <- Spawn procAdder
| Nothing => Action (putStrLn "Spawn failed")
Just answer <- Request adder_id (Add 2 3)
| Nothing => Action (putStrLn "Request failed")
Action (printLn answer)
partial
forever : Fuel
forever = More forever
partial
runProc : Process () -> IO ()
runProc proc = do run forever proc
pure ()
Raw
ProcessIFace.idr
module Main
import System.Concurrency.Channels
%default total
data ProcState = NoRequest | Sent | Complete
data Message = Add Nat Nat
data MessagePID : (iface :reqType -> Type) -> Type where
MkMessage : PID -> MessagePID iface
data Fuel = Dry | More (Lazy Fuel)
data Process : (iface : reqType -> Type) -> Type -> (inState : ProcState) -> (outState : ProcState) -> Type where
Action : IO a -> Process iface a st st
Spawn : Process iface () NoRequest Complete -> Process iface (Maybe (MessagePID iface)) st st
Request : MessagePID service_iface -> (msg : service_reqType) -> Process iface (iface msg) st st
Respond : ((msg : reqType) -> Process iface (iface msg) NoRequest NoRequest) -> Process iface (Maybe reqType) st Sent
Loop : Inf (Process iface a NoRequest Complete) -> Process iface a Sent Complete
Pure : a -> Process iface a st st
(>>=) : Process iface a st1 st2 -> (a -> Process iface b st2 st3) -> Process iface b st1 st3
run : Fuel -> Process iface t instate outstate-> IO (Maybe t)
run Dry _ = pure Nothing
run fuel (Action act) = do res <- act
pure (Just res)
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
pure ())
| Nothing => pure Nothing
pure (Just (Just (MkMessage pid)))
run fuel (Request {iface} (MkMessage process) msg) =
do Just chan <- connect process
| _ => pure Nothing
ok <- unsafeSend chan msg
if ok then do Just x <- unsafeRecv (iface msg) chan
| Nothing => pure Nothing
pure (Just x)
else pure Nothing
run fuel (Respond {reqType} calc) = do Just sender <- listen 1
| Nothing => pure (Just Nothing)
Just msg <- unsafeRecv reqType sender
| Nothing => pure (Just Nothing)
Just res <- run fuel (calc msg)
| Nothing => pure Nothing
unsafeSend sender res
pure (Just (Just msg))
run (More fuel) (Loop act) = run fuel act
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
| Nothing => pure Nothing
run fuel (next x)
AdderType : Message -> Type
AdderType (Add x y) = Nat
procAdder : Process AdderType () NoRequest Complete
procAdder = do Respond (\msg => case msg of Add x y => Pure (x + y))
Loop procAdder
procMain : Process AdderType () NoRequest NoRequest
procMain = do Just adder_id <- Spawn procAdder
| Nothing => Action (putStrLn "Spawn failed")
answer <- Request adder_id (Add 2 3)
Action (printLn answer)
partial
forever : Fuel
forever = More forever
partial
runProc : Process iface () instate outstate -> IO ()
runProc proc = do run forever proc
pure ()
Raw
ProcessLib.idr
module ProcessLib
import System.Concurrency.Channels
%default total
export
data MessagePID : (iface : reqType -> Type) -> Type where
MkMessage : PID -> MessagePID iface
public export
data ProcState = NoRequest | Sent | Complete
public export
data Process : (iface : reqType -> Type) ->
Type ->
(inState : ProcState) ->
(outState : ProcState) ->
Type where
Action : IO a -> Process iface a st st
Spawn : Process iface () NoRequest Complete -> Process iface (Maybe (MessagePID iface)) st st
Request : MessagePID service_iface -> (msg : service_reqType) -> Process iface (iface msg) st st
Respond : ((msg : reqType) -> Process iface (iface msg) NoRequest NoRequest) -> Process iface (Maybe reqType) st Sent
Loop : Inf (Process iface a NoRequest Complete) -> Process iface a Sent Complete
Pure : a -> Process iface a st st
(>>=) : Process iface a st1 st2 -> (a -> Process iface b st2 st3) -> Process iface b st1 st3
public export
data Fuel = Dry | More (Lazy Fuel)
export
run : Fuel -> Process iface t instate outstate-> IO (Maybe t)
run Dry _ = pure Nothing
run fuel (Action act) = do res <- act
pure (Just res)
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
pure ())
| Nothing => pure Nothing
pure (Just (Just (MkMessage pid)))
run fuel (Request {iface} (MkMessage process) msg) =
do Just chan <- connect process
| _ => pure Nothing
ok <- unsafeSend chan msg
if ok then do Just x <- unsafeRecv (iface msg) chan
| Nothing => pure Nothing
pure (Just x)
else pure Nothing
run fuel (Respond {reqType} calc) = do Just sender <- listen 1
| Nothing => pure (Just Nothing)
Just msg <- unsafeRecv reqType sender
| Nothing => pure (Just Nothing)
Just res <- run fuel (calc msg)
| Nothing => pure Nothing
unsafeSend sender res
pure (Just (Just msg))
run (More fuel) (Loop act) = run fuel act
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
| Nothing => pure Nothing
run fuel (next x)
export partial
forever : Fuel
forever = More forever
export partial
runProc : Process iface () instate outstate -> IO ()
runProc proc = do run forever proc
pure ()
Raw
ProcessState.idr
module Main
import System.Concurrency.Channels
%default total
data ProcState = NoRequest | Sent | Complete
data Message = Add Nat Nat
AdderType : Message -> Type
AdderType (Add x y) = Nat
data MessagePID = MkMessage PID
data Fuel = Dry | More (Lazy Fuel)
data Process : Type -> (inState : ProcState) -> (outState : ProcState) -> Type where
Action : IO a -> Process a st st
Spawn : Process () NoRequest Complete -> Process (Maybe MessagePID) st st
Request : MessagePID -> Message -> Process Nat st st
Respond : ((msg : Message) -> Process Nat NoRequest NoRequest) -> Process (Maybe Message) st Sent
Loop : Inf (Process a NoRequest Complete) -> Process a Sent Complete
Pure : a -> Process a st st
(>>=) : Process a st1 st2 -> (a -> Process b st2 st3) -> Process b st1 st3
run : Fuel -> Process t instate outstate-> IO (Maybe t)
run Dry _ = pure Nothing
run fuel (Action act) = do res <- act
pure (Just res)
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
pure ())
| Nothing => pure Nothing
pure (Just (Just (MkMessage pid)))
run fuel (Request (MkMessage process) msg) = do Just chan <- connect process
| _ => pure Nothing
ok <- unsafeSend chan msg
if ok then do Just x <- unsafeRecv Nat chan
| Nothing => pure Nothing
pure (Just x)
else pure Nothing
run fuel (Respond calc) = do Just sender <- listen 1
| Nothing => pure (Just Nothing)
Just msg <- unsafeRecv Message sender
| Nothing => pure (Just Nothing)
Just res <- run fuel (calc msg)
| Nothing => pure Nothing
unsafeSend sender res
pure (Just (Just msg))
run (More fuel) (Loop act) = run fuel act
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
| Nothing => pure Nothing
run fuel (next x)
Service : Type -> Type
Service a = Process a NoRequest Complete
Client : Type -> Type
Client a = Process a NoRequest NoRequest
procAdder : Service ()
procAdder = do Respond (\msg => case msg of Add x y => Pure (x + y))
Loop procAdder
procMain : Client ()
procMain = do Just adder_id <- Spawn procAdder
| Nothing => Action (putStrLn "Spawn failed")
answer <- Request adder_id (Add 2 3)
Action (printLn answer)
partial
forever : Fuel
forever = More forever
partial
runProc : Process () instate outstate -> IO ()
runProc proc = do run forever proc
pure ()
Raw
ReadToBlank.idr
module Main
import Data.Vect
readToBlank : IO (List String)
readToBlank = do
line <- getLine
if line == ""
then pure []
else (line ::) <$> readToBlank
saveContentTo : List String -> String -> IO ()
saveContentTo contents fileName = do
let content = concat $ intersperse "\n" contents
Right () <- writeFile fileName content
| Left error => printLn error
pure ()
readAndSave : IO ()
readAndSave = do
putStrLn "Enter the file content."
lines <- readToBlank
putStr "Enter the name of the file: "
fileName <- getLine
saveContentTo lines fileName
readFromFile : (file : File) -> IO (n ** Vect n String)
readFromFile file = do
endOfFile <- fEOF file
if endOfFile
then pure (_ ** [])
else do
Right line <- fGetLine file
| Left error => do
printLn error
pure (_ ** [])
(n ** rest) <- readFromFile file
pure (S n ** line :: rest)
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do
Right file <- openFile filename Read
| Left error => do
printLn error
pure (_ ** [])
content <- readFromFile file
closeFile file
pure content
main : IO ()
main = (readVectFile "./ReadToBlank.idr") >>= printLn
Raw
ReadWriteFile.idr
module Main
main : IO ()
main = ?main_rhs
Raw
RemoveElemFirst.idr
module RemoveElemFirst
import Data.Vect
removeElem : DecEq a => (value : a) -> (xs : Vect (S n) a) -> Vect n a
removeElem value (x :: xs) = case decEq x value of
Yes prf => xs
No contra => x :: removeElem value xs
Raw
RemoveElemSecond.idr
module RemoveElemSecond
import Data.Vect
removeElem : (value : a) -> (xs : Vect (S n) a) -> Elem value xs -> Vect n a
removeElem value (value :: ys) Here = ys
removeElem {n = (S k)} value (y :: ys) (There later) = y :: removeElem value ys later
removeElem {n = Z} value (y :: []) (There later) = absurd later
Raw
RemoveElemThird.idr
module RemoveElemThird
import Data.Vect
removeElem : (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem {n = (S k)} value (y :: ys) {prf = (There later)} = y :: removeElem value ys
removeElem {n = Z} value (y :: []) {prf = (There later)} = absurd later
Raw
ReverseVec.idr
module ReverseVec
import Data.Vect
myReverse : Vect len a -> Vect len a
myReverse [] = []
myReverse (x :: xs) = reverseProof (myReverse xs ++ [x])
where reverseProof : Vect (k + 1) a -> Vect (S k) a
reverseProof {k} xs = rewrite plusCommutative 1 k in xs
myReverse2 : Vect len a -> Vect len a
myReverse2 xs = reverse' [] xs
where proofXs : Vect (S (k + j)) a -> Vect (k + (S j)) a
proofXs {k} {j} ys = rewrite sym $ plusSuccRightSucc k j in ys
proofNil : Vect n a -> Vect (plus n 0) a
proofNil {n} xs = rewrite plusZeroRightNeutral n in xs
reverse' : Vect n a -> Vect m a -> Vect (n + m) a
reverse' acc [] = proofNil acc
reverse' acc (y :: ys) = proofXs $ reverse' (y::acc) ys
Raw
RunIO.idr
module RunIO
%default total
public export
data RunIO : Type -> Type where
Quit : a -> RunIO a
Do : IO a -> (a -> Inf (RunIO b)) -> RunIO b
public export
(>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b
(>>=) = Do
public export
data Fuel = Dry | More (Lazy Fuel)
public export
partial
forever : Fuel
forever = More forever
public export
run : Fuel -> RunIO a -> IO (Maybe a)
run Dry y = pure Nothing
run (More x) (Quit value) = pure (Just value)
run (More fuel) (Do action continuation) = do
result <- action
run fuel (continuation result)
Raw
Sec.idr
module Sec
%default total
data Access = LoggedOut | LoggedIn
data PwdCheck = Correct | Incorrect
data ShellCmd : (ty : Type) -> Access -> (ty -> Access) -> Type where
Password : String -> ShellCmd PwdCheck LoggedOut (\check => case check of
Correct => LoggedIn
Incorrect => LoggedOut)
Logout : ShellCmd () LoggedIn (const LoggedOut)
GetSecret : ShellCmd String LoggedIn (const LoggedIn)
PutStr : String -> ShellCmd () state (const state)
Pure : (res : ty) -> ShellCmd ty (state_fn res) state_fn
(>>=) : ShellCmd a state1 state2_fn ->
((res : a) -> ShellCmd b (state2_fn res) state3_fn) ->
ShellCmd b state1 state3_fn
session : ShellCmd () LoggedOut (const LoggedOut)
session = do Correct <- Password "wurzel"
| Incorrect => PutStr "Wrond password"
message <- GetSecret
PutStr ("secret: " ++ (show message))
Logout
Raw
Shape.idr
module shape
public export
data Shape = Triangle Double Double
| Rectangle Double Double
| Circle Double
private
rectangle_area : Double -> Double -> Double
rectangle_area w h = w * h
export
area : Shape -> Double
area (Triangle base height) = 0.5 * rectangle_area base height
area (Rectangle w h ) = rectangle_area w h
area (Circle r ) = pi * r * r
Raw
Shape_abs.idr
module Shape
export
data Shape : Type where
Rectangle : (width : Double) -> (height : Double) -> Shape
Triangle : (base : Double) -> (height : Double) -> Shape
Circle : (radius : Double) -> Shape
export
rectangle : Double -> Double -> Shape
rectangle = Rectangle
export
triangle : Double -> Double -> Shape
triangle = Triangle
export
circle : Double -> Shape
circle = Circle
data ShapeView : Shape -> Type where
STriangle : ShapeView (triangle base height)
SRectangle : ShapeView (rectangle width height)
SCircle : ShapeView (circle radius)
shapeView : (shape : Shape) -> ShapeView shape
shapeView (Rectangle width height) = SRectangle
shapeView (Triangle base height) = STriangle
shapeView (Circle radius) = SCircle
area : Shape -> Double
area shape with (shapeView shape)
area (triangle base height) | STriangle = base * height / 2
area (rectangle width height) | SRectangle = width * height
area (circle radius) | SCircle = pi * radius * radius
Raw
Shell.idr
module Shell
import Data.Primitives.Views
import System
%default total
public export
data Command : Type -> Type where
PutStr : String -> Command ()
GetLine : Command String
ReadFile : String -> Command (Either FileError String)
WriteFile : String -> String -> Command (Either FileError ())
public export
data ConsoleIO : Type -> Type where
Quit : a -> ConsoleIO a
Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
public export
(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
(>>=) = Do
public export
runCommand : Command a -> IO a
runCommand (PutStr msg) = putStrLn msg
runCommand GetLine = getLine
runCommand (ReadFile path) = readFile path
runCommand (WriteFile path content) = writeFile path content
public export
data Fuel = Dry | More (Lazy Fuel)
public export
partial
forever : Fuel
forever = More forever
public export
run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Dry y = pure Nothing
run (More fuel) (Quit x) = pure (Just x)
run (More fuel) (Do command continuation) = do
result <- runCommand command
run fuel (continuation result)
mutual
copyFile : String -> String -> ConsoleIO String
copyFile source destination = do
Right content <- ReadFile source
| Left error => do PutStr ("unable to read content" ++ (show error))
shell
Right () <- WriteFile destination content
| Left error => do PutStr ("unable to write to file" ++ (show error))
shell
shell
readTheFile : String -> ConsoleIO String
readTheFile path = do
Right content <- ReadFile path
| Left error => do PutStr "unable to read file"
shell
PutStr content
shell
shell : ConsoleIO String
shell = do
line <- GetLine
case words line of
("cat"::filename::rest) => readTheFile filename
("copy"::source::destination::rest) => copyFile source destination
("quit"::rest) => Quit "Bye"
_ => do PutStr "unknown command"
shell
partial
main : IO ()
main = do seed <- time
Just result <- run forever shell
| Nothing => putStrLn "Ran out of fuel."
putStrLn ("result: " ++ result)
Raw
SnocList.idr
module SnocList
data SnocList : List a -> Type where
Empty : SnocList []
Snoc : (rec : SnocList xs) -> SnocList (xs ++ [x])
snocListHelp : (snoc : SnocList input) -> (rest : List a) -> SnocList (input ++ rest)
snocListHelp {input} snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp {input} snoc (x :: xs) = rewrite appendAssociative input [x] xs in
snocListHelp (Snoc snoc {x}) xs
snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelp Empty xs
myReverse : List a -> List a
myReverse xs with (snocList xs)
myReverse [] | Empty = []
myReverse (ys ++ [x]) | (Snoc rec) = x :: myReverse ys | rec
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
isSuffix [] input2 | Empty = True
isSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
isSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = False
isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec) =
if x == y then isSuffix xs ys | xsrec | ysrec
else False
Raw
Stack.idr
module Stack
import Data.Vect
%default total
data StackCmd : Type -> Nat -> Nat -> Type where
Push : Integer -> StackCmd () height (S height)
Pop : StackCmd Integer (S height) height
Top : StackCmd Integer (S height) (S height)
GetStr : StackCmd String h h
PutStr : String -> StackCmd () h h
Pure : ty -> StackCmd ty height height
(>>=) : StackCmd a height1 height2 -> (a -> StackCmd b height2 height3) -> StackCmd b height1 height3
testAdd : StackCmd Integer 0 0
testAdd = do
Push 10
Push 20
val1 <- Pop
val2 <- Pop
Pure (val1 + val2)
doBinary : (Integer -> Integer -> Integer) -> StackCmd () (S (S h)) (S h)
doBinary op = do
a <- Pop
b <- Pop
Push (a `op` b)
doDiscard : StackCmd Integer (S h) h
doDiscard = do
old <- Pop
Pure old
doDuplicate : StackCmd () (S h) (S h)
doDuplicate = do
x <- Pop
Push (x * 2)
doNegate : StackCmd () (S h) (S h)
doNegate = do
x <- Pop
Push (x * (-1))
doAdd : StackCmd () (S (S h)) (S h)
doAdd = doBinary (+)
doMultiply : StackCmd () (S (S h)) (S h)
doMultiply = doBinary (*)
doSubtract : StackCmd () (S (S h)) (S h)
doSubtract = doBinary (-)
runStack : (stk : Vect inHeight Integer) ->
StackCmd ty inHeight outHeight ->
IO (ty, Vect outHeight Integer)
runStack stk (Push x) = pure ((), x :: stk)
runStack (x :: xs) Pop = pure (x, xs)
runStack (x :: xs) Top = pure (x, x :: xs)
runStack stk GetStr = do line <- getLine
pure (line, stk)
runStack stk (PutStr str) = do putStr str
pure ((), stk)
runStack stk (Pure x) = pure (x, stk)
runStack stk (x >>= f) = do (res, newStk) <- runStack stk x
runStack newStk (f res)
data StackIO : Nat -> Type where
Do : StackCmd a h1 h2 ->
(a -> Inf (StackIO h2)) ->
StackIO h1
namespace StackDo
(>>=) : StackCmd a h1 h2 ->
(a -> Inf (StackIO h2)) ->
StackIO h1
(>>=) = Do
data Fuel = Dry | More (Lazy Fuel)
partial
forever : Fuel
forever = More forever
run : Fuel -> Vect height Integer -> StackIO height -> IO ()
run Dry xs y = pure ()
run (More fuel) stk (Do c f) = do (res, newStk) <- runStack stk c
run fuel newStk (f res)
data StkInput = Number Integer
| Add
| Subtract
| Multiply
| Negate
| Discard
| Duplicate
strToInput : String -> Maybe StkInput
strToInput "" = Nothing
strToInput "+" = Just Add
strToInput "-" = Just Subtract
strToInput "*" = Just Multiply
strToInput "negate" = Just Negate
strToInput "discard" = Just Discard
strToInput "duplicate" = Just Duplicate
strToInput x = if all isDigit (unpack x)
then Just (Number (cast x))
else Nothing
mutual
stackCalc : StackIO height
stackCalc = do PutStr "> "
input <- GetStr
case strToInput input of
Nothing => do PutStr "Invalid input\n"
stackCalc
Just (Number x) => do Push x
stackCalc
Just Add => tryAdd
Just Multiply => tryMultiply
Just Subtract => trySubtract
Just Negate => tryNegate
Just Discard => tryDiscard
Just Duplicate => tryDuplicate
tryDuplicate : StackIO height
tryDuplicate {height = (S h)} = do
doDuplicate
result <- Top
PutStr (show result ++ "\n")
stackCalc
tryDuplicate = do
PutStr "Fewer than one item on the stack.\n"
stackCalc
tryDiscard : StackIO height
tryDiscard {height = (S h)} = do
oldTop <- doDiscard
PutStr (show oldTop ++ "\n")
stackCalc
tryDiscard = do
PutStr "Fewer than one item on the stack.\n"
stackCalc
tryNegate : StackIO height
tryNegate {height = (S h)} = do
doNegate
result <- Top
PutStr (show result ++ "\n")
stackCalc
tryNegate = do
PutStr "Fewer than one item on the stack.\n"
stackCalc
tryAdd : StackIO height
tryAdd {height = (S (S h))} = do
doAdd
result <- Top
PutStr (show result ++ "\n")
stackCalc
tryAdd = do
PutStr "Fewer than two items on the stack.\n"
stackCalc
tryMultiply : StackIO height
tryMultiply {height = (S (S h))} = do
doMultiply
result <- Top
PutStr (show result ++ "\n")
stackCalc
tryMultiply = do
PutStr "Fewer than two items on the stack.\n"
stackCalc
trySubtract : StackIO height
trySubtract {height = (S (S h))} = do
doSubtract
result <- Top
PutStr (show result ++ "\n")
stackCalc
trySubtract = do
PutStr "Fewer than two items on the stack.\n"
stackCalc
partial
main : IO ()
main = run forever [] stackCalc
Raw
State.idr
module St
import Control.Monad.State
update : (stateType -> stateType) -> State stateType ()
update f = do
current <- get
put (f current)
increase : Nat -> State Nat ()
increase inc = do
update (+inc)
Raw
Streams.idr
module Streams
%default total
labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith xs [] = []
labelWith (value :: xs) (x :: ys) = (value, x) :: labelWith xs ys
Raw
SumInputs.idr
module Main
sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs acc input = let val = cast input in
if val < 0
then Nothing
else let newVal = acc + val in
Just ("Subtotal: " ++ show newVal ++ "\n", newVal)
main : IO ()
main = replWith 0 "Value: " sumInputs
Raw
TakeN.idr
module TakeN
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 Z xs = Exact []
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) = case takeN k xs of
Fewer => Fewer
Exact ys => Exact (x::ys)
groupByN : (n : Nat) -> (xs : List a) -> List (List a)
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
halves : List a -> (List a, List a)
halves xs with (takeN (div (length xs) 2) xs)
halves xs | Fewer = (xs, [])
halves (n_xs ++ rest) | (Exact n_xs) = (n_xs, rest)
Raw
test.txt
test oiwjef
test
test test test
a
a
a
Raw
TreeLabel.idr
module TreeLabel
import Control.Monad.State
data Tree a = Empty
| Node (Tree a) a (Tree a)
testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
(Node Empty "Sheila" Empty)) "Alice"
(Node Empty "Bob" (Node Empty "eve" Empty))
treeLabelWith : Stream labelType -> Tree a -> (Stream labelType, Tree (labelType, a))
treeLabelWith labels Empty = (labels, Empty)
treeLabelWith labels (Node left val right) = let (thisLabel::restLabels, labeledLeft) = treeLabelWith labels left
(labels', labeledRight) = treeLabelWith restLabels right in
(labels', Node labeledLeft (thisLabel, val) labeledRight)
treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = snd (treeLabelWith [1..] tree)
flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = (flatten left) ++ (val :: (flatten right))
treeLabelState : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelState Empty = pure Empty
treeLabelState (Node l c r) = do
leftLabeled <- treeLabelState l
(this::rest) <- get
put rest
rightLabeled <- treeLabelState r
pure (Node leftLabeled (this, c) rightLabeled)
treeLabelWithState : Tree a -> Tree (Integer, a)
treeLabelWithState tree = evalState (treeLabelState tree) [1..]
countEmpty : Tree a -> State Nat ()
countEmpty Empty = modify (S)
countEmpty (Node x y z) = do
countEmpty x
countEmpty z
countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty = modify (\(x, y) => (S x, y))
countEmptyNode (Node x y z) = do
countEmptyNode x
countEmptyNode z
modify (\(x, y) => (x, S y))
Raw
TreeLabelType.idr
module TreeLabelType
data State : (stateType : Type) -> Type -> Type where
Get : State stateType stateType
Put : stateType -> State stateType ()
Pure : ty -> State stateType ty
Bind : State stateType a -> (a -> State stateType b) -> State stateType b
Functor (State stateType) where
map func fa = Bind fa (\a => Pure (func a))
Applicative (State stateType) where
pure = Pure
(<*>) afunc aval = Bind afunc (\f =>
Bind aval (\val =>
Pure (f val)))
Monad (State stateType) where
(>>=) = Bind
runState : State stateType a -> (st : stateType) -> (a, stateType)
runState Get st = (st, st)
runState (Put newSt) st = ((), newSt)
runState (Pure val) st = (val, st)
runState (Bind ma f) st = let (val1, nextState) = runState ma st in
runState (f val1) nextState
Raw
TuplVect.idr
module TuplVector
TupleVector : (len : Nat) -> (elem : Type) -> Type
TupleVector Z elem = ()
TupleVector (S k) elem = (elem, TupleVector k elem)
test : TupleVector 4 Nat
test = (1,2,3,4,())
Raw
TypeFuns.idr
module Main
StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int
getStringOrInt : (isInt: Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety four"
getStringOrInt True = 94
valToString : (isInt: Bool) -> (StringOrInt isInt) -> String
valToString False x = trim x
valToString True x = cast x
main : IO ()
main = print $ getStringOrInt False
Raw
Vect.idr
module Main
import Data.Fin
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : (x : a) -> (xs : Vect k a) -> (Vect (S k) a)
%name Vect xs, ys, zs
total vectInd : Fin n -> Vect n a -> a
vectInd FZ (x :: xs) = x
vectInd (FS k) (y :: ys) = vectInd k ys
total append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
total zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] ys = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys
total takeVect : (n: Nat) -> Vect (n + m) a -> Vect n a
takeVect Z xs = []
takeVect (S k) (x :: xs) = x :: (takeVect k xs)
total sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
Nothing => Nothing
Just ind => Just $ (vectInd ind xs) + (vectInd ind ys)
main : IO ()
main = ?main_rhs
Raw
VectorUnknown.idr
module Main
import Data.Vect
data VectUnknown : Type -> Type where
MkVect : (len : Nat) -> Vect len a -> VectUnknown a
readVect : IO (VectUnknown String)
readVect = do
line <- getLine
if (line == "")
then pure $ MkVect _ []
else do
MkVect _ xs <- readVect
pure $ MkVect _ (line :: xs)
printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs) = putStrLn $ (show xs) ++ " " ++ (show len)
rVect : IO (len : Nat ** Vect len String)
rVect = do
line <- getLine
if (line == "")
then pure $ (_ ** [])
else do (_ ** xs) <- rVect
pure $ (_ ** line :: xs)
main : IO ()
main = do
putStrLn "type in first vector"
(len1 ** vec1) <- rVect
putStrLn "type in second vector"
(len2 ** vec2) <- rVect
case exactLength len1 vec2 of
Nothing => putStrLn "vectors are of different length"
Just vec2' => printLn (zip vec2' vec1)
Raw
Vehicle.idr
module Main
data PowerSource = Petrol | Pedal
data Vehicle : PowerSource -> Type where
Bicycle : Vehicle Pedal
Car : (fuel: Nat) -> Vehicle Petrol
Bus : (fuel: Nat) -> Vehicle Petrol
Unicycle : Vehicle Pedal
MotorCycle : (fuel: Nat) -> Vehicle Petrol
total wheels : Vehicle _ -> Nat
wheels Bicycle = 2
wheels Unicycle = 1
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels (MotorCycle fuel) = 2
total refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel (MotorCycle fuel) = MotorCycle 200
refuel Bicycle impossible
refuel Unicycle impossible
main : IO ()
main = ?main
Raw
Vending.idr
module Vending
%default total
VendState : Type
VendState = (Nat, Nat)
data CoinResult = Inserted | Rejected
data Input = COIN
| VEND
| CHANGE
| REFILL Nat
data MachineCmd : (ty : Type) -> VendState -> (ty -> VendState) -> Type where
InsertCoin : MachineCmd CoinResult (pounds, chocs) (\res => case res of
Inserted => (S pounds, chocs)
Rejected => (pounds, chocs))
Vend : MachineCmd () (S pounds, S chocs) (const (pounds, chocs))
GetCoins : MachineCmd () (pounds, chocs) (const (Z, chocs))
Refill : (bars : Nat) -> MachineCmd () (Z, chocs) (const (Z, bars + chocs))
Display : String -> MachineCmd () state (const state)
GetInput : MachineCmd (Maybe Input) state (const state)
Pure : ty -> MachineCmd ty state (const state)
(>>=) : MachineCmd a state1 state2_fn -> ((res : a) -> MachineCmd b (state2_fn res) state3_fn) -> MachineCmd b state1 state3_fn
data MachineIO : VendState -> Type where
Do : MachineCmd a state1 state2_fn ->
((res : a) -> Inf (MachineIO (state2_fn res))) ->
MachineIO state1
namespace MachineDo
(>>=) : MachineCmd a state1 state2_fn ->
((res : a) -> Inf (MachineIO (state2_fn res))) -> MachineIO state1
(>>=) = Do
mutual
insertCoin : MachineIO (pounds, chocs)
insertCoin = do
result <- InsertCoin
case result of
Rejected => do Display "Coin rejected."
machineLoop
Inserted => do Display "Coin accepted."
machineLoop
vend : MachineIO (pounds, chocs)
vend {pounds = S p} {chocs = S c} = do
Vend
Display "Enjoy!"
machineLoop
vend {pounds = Z} = do
Display "Insert a coin"
machineLoop
vend {chocs = Z} = do
Display "Out of chocs"
machineLoop
refill : (num : Nat) -> MachineIO (pounds, chocs)
refill num {pounds = Z} = do
Refill num
machineLoop
refill num = do
Display "Can't refill: Coins in machine."
machineLoop
machineLoop : MachineIO (pounds, chocs)
machineLoop = do
Just x <- GetInput
| Nothing => do Display "Invalid input"
machineLoop
case x of
COIN => insertCoin
VEND => vend
CHANGE => do GetCoins
Display "Change returned"
machineLoop
REFILL num => refill num
Raw
Void.idr
module Void
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible
valueNotSucc : (x : Nat) -> x = S x -> Void
valueNotSucc _ Refl impossible
Raw
WordCount.idr
module WordCount
import ProcessLib
%default total
record WCData where
constructor MkWCData
wordCount : Nat
lineCount : Nat
doCount : (content : String) -> WCData
doCount content = let lcount = length (lines content)
wcount = length (words content) in
MkWCData lcount wcount
data WC = CountFile String
| GetData String
WCType : WC -> Type
WCType (CountFile x) = ()
WCType (GetData x) = Maybe WCData
countFile : List (String, WCData) -> String -> Process WCType (List (String, WCData)) Sent Sent
countFile files fname =
do Right content <- Action (readFile fname)
| Left err => Pure files
let count = doCount content
Action (putStrLn ("Counting complete for " ++ fname))
Pure ((fname, count)::files)
wcService : (loaded : List (String, WCData)) ->
Process WCType () NoRequest Complete
wcService loaded =
do msg <- Respond (\msg => case msg of
CountFile fname => Pure ()
GetData fname => Pure (lookup fname loaded))
newLoaded <- case msg of
Just (CountFile fname) => countFile loaded fname
_ => Pure loaded
Loop (wcService newLoaded)
procMain : Process WCType () NoRequest NoRequest
procMain = do Just wc <- Spawn (wcService [])
| Nothing => Action (putStrLn "Spawn failed")
Action (putStrLn "Counting test.txt")
Request wc (CountFile "test.txt")
Action (putStrLn "Processing")
Just wcData <- Request wc (GetData "test.txt")
| Nothing => Action (putStrLn "File error")
Action (putStrLn ("Words: " ++ show (wordCount wcData)))
Action (putStrLn ("Lines: " ++ show (lineCount wcData)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment