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

data store search

Browse source
This commit is contained in:
nora 2021-08-17 21:39:45 +02:00
parent eda0cba251
commit 94ed1401fe
4 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
chapter4/DataStore.idr
View file

@ -18,10 +18,16 @@ addToStore (MkData size items) newitem = MkData _ (addToData items)
addToData [] = [newitem]
addToData (x :: xs) = x :: addToData xs
search : DataStore -> String -> List String
search store query = let predicate = isInfixOf query
allItems = toList (items store) in -- can't be bothered to work with dependant pairs
filter predicate allItems
data Command = Add String
| Get Integer
| Size
| Search String
| Quit
parseCommand : (cmd : String) -> (args : String) -> Maybe Command
@ -31,6 +37,7 @@ parseCommand "get" val = case all isDigit (unpack val) of
False => Nothing
parseCommand "quit" args = Just Quit
parseCommand "size" args = Just Size
parseCommand "search" args = Just (Search args)
parseCommand _ _ = Nothing
parse : (input : String) -> Maybe Command
@ -52,6 +59,9 @@ processInput store inp = case parse inp of
Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
Just (Get pos) => getEntry pos store
Just Size => Just ("Size: " ++ show (size store) ++ "\n", store)
Just (Search query) => case (search store query) of
[] => Just ("Item Not Found\n", store)
items => Just (show items ++ "\n", store)
Just Quit => Nothing