Is there a better way to write nested cases in Idris?
Here is a piece of Idris code from Edwin's book:
data DataStore : Type where MkData : (size : Nat) -> (items : Vect size String) -> DataStore proccessInput : DataStore -> String -> Maybe (String, DataStore) proccessInput store@(MkData size items) input = case map trim $ span (/= ' ') input of ("add", item) => Just ("ID " ++ show size ++ "\n", MkData _ (item :: items)) ("get", val) => case all isDigit (unpack val) of False => Just ("Invalid command\n", store) True => case integerToFin (cast val) size of Nothing => Just ("Out of range\n", store) (Just id) => Just (index id items ++ " \n", store) ("quit", "") => Nothing (_, _) => Just ("Invalid command\n", store)
I've already eliminate out some pieces of codes that I think is redundant( some helper functions), But I still found that the code is somewhat redundant. The case split is really ugly I think.