DataStore.idr

module Main

import Data.Vect

infixr 5 .+.

data Schema
  = SString
  | SChar
  | SInt
  | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString   = String
SchemaType SInt      = Int
SchemaType SChar     = Char
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
  constructor MkData
  schema : Schema
  size   : Nat
  items  : Vect size (SchemaType schema)

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size xs) newItem =
  MkData schema (S size) (addToData xs) where
    addToData : Vect size' (SchemaType schema) -> Vect (S size') (SchemaType schema)
    addToData [] = [newItem]
    addToData (item :: items) = item :: addToData items

data Command : (schema : Schema) -> Type where
  SetSchema : (newschema : Schema) -> Command schema
  Add       : SchemaType schema -> Command schema
  Get       : Integer -> Command schema
  GetAll    : Command schema
  Size      : Command schema
  Quit      : Command schema

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input) where
  getQuoted : List Char -> Maybe (String, String)
  getQuoted ('"' :: rest1) = case span (/= '"') rest1 of
    (quoted, '"' :: rest2) => Just (pack quoted, ltrim (pack rest2))
    _                      => Nothing
  getQuoted chars          = Nothing
parsePrefix SChar input with (strM input)
  parsePrefix SChar ""                  | StrNil              = Nothing
  parsePrefix SChar (strCons char rest) | (StrCons char rest) = Just (char, ltrim rest)
parsePrefix SInt input = case span isDigit input of
  ("", rest)  => Nothing
  (num, rest) => Just (cast num, ltrim rest)
parsePrefix (schema1 .+. schema2) input = do
  (item1, rest1) <- parsePrefix schema1 input
  (item2, rest2) <- parsePrefix schema2 rest1
  Just ((item1, item2), rest2)

parseBySchema : (schema : Schema) -> (item_str : String) -> Maybe (SchemaType schema)
parseBySchema schema item_str = case parsePrefix schema item_str of
  Just (item, "") => Just item
  Just _          => Nothing
  Nothing         => Nothing

parseSchema : String -> Maybe Schema
parseSchema schema_str = parseTypeList (words schema_str) where
  parseTypeList : List String -> Maybe Schema
  parseTypeList ("String" :: [])   = Just SString
  parseTypeList ("String" :: rest) = (SString .+.) <$> parseTypeList rest
  parseTypeList ("Char"   :: [])   = Just SChar
  parseTypeList ("Char"   :: rest) = (SChar .+.) <$> parseTypeList rest
  parseTypeList ("Int"    :: [])   = Just SInt
  parseTypeList ("Int"    :: rest) = (SInt .+.) <$> parseTypeList rest
  parseTypeList _                  = Nothing

parseCommand : (schema : Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand schema "schema" schema_str = SetSchema <$> parseSchema schema_str
parseCommand schema "add"    item_str   = Add <$> parseBySchema schema item_str
parseCommand schema "get"    ""         = Just GetAll
parseCommand schema "get"    index_str  =
  if all isDigit (unpack index_str)
    then Just (Get (cast index_str))
    else Nothing
parseCommand schema "quit"   "" = Just Quit
parseCommand schema "size"   "" = Just Size
parseCommand schema _        _  = Nothing

parse : (schema : Schema) -> String -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
  (cmd, args) => parseCommand schema cmd (ltrim args)

display : SchemaType schema -> String
display {schema = SString}   item           = item
display {schema = SChar}     item           =  "'" ++ cast item ++ "'"
display {schema = SInt}      item           = show item
display {schema = (x .+. y)} (iteml, itemr) = display iteml ++ ", " ++ display itemr

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store = case integerToFin pos (size store) of
  Nothing   => Just ("Out of range\n", store)
  (Just id) => Just (display (index id (items store)) ++ "\n", store)

setSchema : (store : DataStore) -> (schema : Schema) -> Maybe DataStore
setSchema store schema = case size store of
  Z     => Just (MkData schema _ [])
  (S k) => Nothing

formatStore : (store : DataStore) -> String
formatStore store = formatItems Z (items store) where
  formatItems : (id : Nat) -> Vect _ (SchemaType (schema store)) -> String
  formatItems _  []             = ""
  formatItems id (item :: rest) = show id ++ ": " ++ display item ++ "\n" ++ formatItems (S id) rest

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input =
  case parse (schema store) input of
    Nothing                      => Just ("Invalid command\n", store)
    (Just (SetSchema newschema)) => case setSchema store newschema of
      Nothing       => Just ("Can't update schema\n", store)
      Just newstore => Just ("OK\n", newstore)
    (Just (Add item))            => Just ("ID: " ++ show (size store) ++ "\n", addToStore store item)
    (Just (Get pos))             => getEntry pos store
    (Just GetAll)                => Just (formatStore store, store)
    (Just Size)                  => Just (show (size store) ++ "\n", store)
    (Just Quit)                  => Nothing

main : IO ()
main = replWith (MkData (SString .+. SString .+. SInt) 0 []) "Command: " processInput