From eda0cba2512b4e8eff423d1d13a68557c05e529f Mon Sep 17 00:00:00 2001
From: nils <48135649+Nilstrieb@users.noreply.github.com>
Date: Thu, 15 Jul 2021 17:00:20 +0200
Subject: [PATCH] size command

---
 chapter4/DataStore.idr | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/chapter4/DataStore.idr b/chapter4/DataStore.idr
index be8d667..e3f966a 100644
--- a/chapter4/DataStore.idr
+++ b/chapter4/DataStore.idr
@@ -21,6 +21,7 @@ addToStore (MkData size items) newitem = MkData _ (addToData items)
 
 data Command = Add String
              | Get Integer
+             | Size
              | Quit
 
 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))
                                False => Nothing
 parseCommand "quit" args = Just Quit
+parseCommand "size" args = Just Size
 parseCommand _ _ = Nothing
 
 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 store inp = case parse inp of
                               Nothing => Just ("invalid command\n", store)
-                              (Just (Add item)) =>
+                              Just (Add item) =>
                                   Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
-                              (Just (Get pos)) => getEntry pos store
-                              (Just Quit) => Nothing
+                              Just (Get pos) => getEntry pos store
+                              Just Size => Just ("Size: " ++ show (size store) ++ "\n", store)
+                              Just Quit => Nothing
 
 
 main : IO ()