diff --git a/chapter6_part2.idr b/chapter6_part2.idr index 71d40e1..ad64140 100644 --- a/chapter6_part2.idr +++ b/chapter6_part2.idr @@ -18,6 +18,10 @@ data Command = Add String | Schema (List Type) | Quit +VarArgs : List Type -> Type +VarArgs [] = () +VarArgs (x :: xs) = (x, VarArgs xs) + addToStore : DataStore a -> a -> DataStore a addToStore (MkData size items') newitem = MkData _ (addToData items') where @@ -26,7 +30,7 @@ addToStore (MkData size items') newitem = MkData _ (addToData items') addToData (item :: items') = item :: addToData items' -replMain : DataStoreState String -> String -> Maybe (String, DataStoreState String) +replMain : DataStoreState a -> String -> Maybe (String, DataStoreState b) replMain ds text = let maybeCommand = parseCommand text in case maybeCommand of @@ -47,11 +51,13 @@ replMain ds text = ("quit", _) => pure Quit _ => Nothing - partial processCommand : Command -> DataStoreState String -> Maybe (String, DataStoreState String) + processCommand : Command -> DataStoreState a -> Maybe (String, DataStoreState b) + processCommand (Add _) NotInited = pure ("Initialize schema first", NotInited) processCommand (Add s) (Inited ds) = let newStore = addToStore ds s stringIndex : String = cast (size ds) in pure ("ID " ++ stringIndex, Inited newStore) + processCommand (Get _) NotInited = pure ("Initialize schema first", NotInited) processCommand (Get i) (Inited ds) = let maybeValue = do fin <- integerToFin i (Main.DataStore.size ds) @@ -59,9 +65,13 @@ replMain ds text = textToShow = fromMaybe "Out of range" maybeValue in pure (textToShow, Inited ds) - processCommand Schema _ = Nothing + processCommand (Schema s) _ = + let result : DataStore (VarArgs s) = MkData 0 [] + in pure ("schema accepted", Inited result) processCommand Quit _ = Nothing -covering main : IO () -main = replWith NotInited ("\nCommand:") replMain \ No newline at end of file +partial main : IO () +main = + let initialState : DataStoreState () = NotInited + in replWith initialState ("\nCommand:") replMain \ No newline at end of file