Created
January 25, 2021 10:20
-
-
Save SekiT/852b0b353fecdce1090ddbee5efe0ec9 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment