Noratrieb/idris-learning
1
0
Fork 0
mirror of https://github.com/Noratrieb/idris-learning.git synced 2026-01-14 21:15:02 +01:00
Code Issues Projects Releases Packages Wiki Activity Actions

size command

Browse source
This commit is contained in:
nora 2021-07-15 17:00:20 +02:00
parent 941f8e2020
commit eda0cba251
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
chapter4/DataStore.idr
View file

@ -21,6 +21,7 @@ addToStore (MkData size items) newitem = MkData _ (addToData items)
data Command = Add String data Command = Add String
| Get Integer | Get Integer
| Size
| Quit | Quit
parseCommand : (cmd : String) -> (args : String) -> Maybe Command parseCommand : (cmd : String) -> (args : String) -> Maybe Command
@ -29,6 +30,7 @@ parseCommand "get" val = case all isDigit (unpack val) of
True => Just (Get (cast val)) True => Just (Get (cast val))
False => Nothing False => Nothing
parseCommand "quit" args = Just Quit parseCommand "quit" args = Just Quit
parseCommand "size" args = Just Size
parseCommand _ _ = Nothing parseCommand _ _ = Nothing
parse : (input : String) -> Maybe Command parse : (input : String) -> Maybe Command
@ -46,10 +48,11 @@ getEntry pos store = let store_items = items store in
processInput : DataStore -> String -> Maybe (String, DataStore) processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store inp = case parse inp of processInput store inp = case parse inp of
Nothing => Just ("invalid command\n", store) Nothing => Just ("invalid command\n", store)
(Just (Add item)) => Just (Add item) =>
Just ("ID " ++ show (size store) ++ "\n", addToStore store item) Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
(Just (Get pos)) => getEntry pos store Just (Get pos) => getEntry pos store
(Just Quit) => Nothing Just Size => Just ("Size: " ++ show (size store) ++ "\n", store)
Just Quit => Nothing
main : IO () main : IO ()