Dynamic typesafe datastore with Idris lang

Datastore.idr

{-
   This is the program for interactive maintaining datastore of strings.
   We can use three commands:
     1) Adding string to the store:

        add somestring

       Added string receives a numeric id.
     2) Extracting string from a store by its numeric id

        get id

     3) Finishing interaction:

        quit

   Extend this program to support storing values corresponded to some schema
   as defined at the lecture:
   1) add datatypes and utility functions for schema support
   2) update DataStore record for schema support
   3) correct compilation errors
   4) implement displaying values from the store according to the schema
   5) implement parsing input values according to the schema
   6) implement updating schema (only when the store is empty)
-}

-- module Main
import Data.Vect

infixr 5 .+.

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

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

char2schema : Char -> Maybe Schema
char2schema 'i' = Just SInt
char2schema 's' = Just SString
char2schema _ = Nothing

parseSchema : String -> Maybe Schema
parseSchema s = case unpack s of
                  [] => Nothing
                  [c] => char2schema c
                  (c :: cs) => [| char2schema c .+. parseSchema (pack cs) |]

DatabaseSchema : String -> Nat -> Maybe Type
DatabaseSchema s k = parseSchema s >>= Just . Vect k . SchemaType

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

getSchema : DataStore sh -> Schema
getSchema {sh} _ = sh


-- ===========================
--      database manip
-- ===========================

addToStore : {sh : Schema} -> SchemaType sh -> DataStore sh -> DataStore sh
addToStore {sh} newitem (MkData size store) = MkData _ (addToData store)
  where
   addToData : Vect oldsize (SchemaType sh) -> Vect (S oldsize) (SchemaType sh)
   addToData [] = [newitem]
   addToData (x :: xs) = x :: addToData xs


getEntry :  {sh : Schema} ->
            (pos : Integer) -> DataStore sh -> Maybe (SchemaType sh, DataStore sh)
getEntry pos store = integerToFin pos (size store) >>=
                        \x => Just (index x (items store), store)


show' : {sh : Schema} -> SchemaType sh -> String
show' {sh = SInt} val = show val
show' {sh = SString} val = val
show' {sh = (sh1 .+. sh2)} (v1, v2) = show' v1 ++ " " ++ show' v2

show'' : Schema -> String
show'' SInt = "SInt"
show'' SString = "SString"
show'' (sh1 .+. sh2) = show'' sh1 ++ " " ++ show'' sh2

-- ===========================
--      commands
-- ===========================

data Command =  Add (List String)
                | Get Integer
                | Quit
                | Change Schema
                | TypeT
                | Clear
                | Size

parseNum : String -> Maybe Integer
parseNum s =  case all isDigit (unpack s) of
              False => Nothing
              True => Just (cast s)

parseCommand : String -> List String -> Maybe Command
parseCommand "add" ss = Just (Add ss)
parseCommand "get" [val] = Get <$> parseNum val
parseCommand "quit" [] = Just Quit
parseCommand "change" [x] = Change <$> parseSchema x
parseCommand "type" [] = Just TypeT
parseCommand "clear" [] = Just Clear
parseCommand "size" [] = Just Size
parseCommand _ _ = Nothing


parse : (input : String) -> Maybe Command
parse input = case words input of
                (cmd :: args) => parseCommand cmd args
                _ => Nothing


parseRecH : (sh : Schema) -> List String -> Maybe (SchemaType sh, List String)
parseRecH SString (x :: xs) = Just (x, xs)
parseRecH SInt (x :: xs) = parseNum x >>= \el => return (el, xs)
parseRecH (sh1 .+. sh2) ss = do
  (lh, ss2) <- parseRecH sh1 ss
  (rh, ss3) <- parseRecH sh2 ss2
  return ((lh, rh), ss3)
parseRecH _ _ = Nothing


parseRec : (sh : Schema) -> List String -> Maybe (SchemaType sh)
parseRec sh ss = do
  (val, rem) <- parseRecH sh ss
  guard (isNil rem)
  return val

-- ===========================
--      interaction
-- ===========================

record Wrap where
  constructor MkWrap
  schema : Schema
  store : DataStore schema

wrapIt : DataStore sh -> Wrap
wrapIt {sh} store = MkWrap sh store

getEmpty : (sh : Schema) -> DataStore sh
getEmpty sh = MkData _ (the (Vect _ (SchemaType sh)) [])




getRec : DataStore sh -> Integer -> Maybe (String, Wrap)
getRec store pos = do
  (rec, nstore) <- getEntry pos store
  return (show' rec ++ "\n", wrapIt nstore)

addRec : DataStore schema -> List String -> Maybe (String, Wrap)
addRec {schema} store ss = do
  val <- parseRec schema ss
  let nStore = addToStore val store
  let msg = "ID " ++ show (size store) ++ "\n"
  return (msg, wrapIt nStore)

changeSchema : DataStore sh -> Schema -> Maybe (String, Wrap)
changeSchema store nsh = do
    guard (size store == 0)
    return ("Success!\n", wrapIt (getEmpty nsh))


processInput : Wrap -> String -> Maybe (String, Wrap)
processInput wrapper@(MkWrap sh store) input =
  case parse input of
    Nothing => Just ("Invalid command\n", wrapper)
    Just Quit => Nothing
    Just (Add items) => addRec store items <|> Just ("Invalid format\n", wrapper)
    Just (Get pos) => getRec store pos <|> Just ("Invalid index\n", wrapper)
    Just (Change sh) => changeSchema store sh <|> Just ("Not empty\n", wrapper)
    Just TypeT => Just (show'' (getSchema store) ++ "\n", wrapper)
    Just Clear => Just ("clearing...\n", wrapIt (getEmpty (getSchema store)))
    Just Size => Just (show (size store) ++ "\n", wrapper)


initStore : DataStore SInt
initStore = getEmpty SInt

main : IO ()
main = replWith (wrapIt initStore) "Command: " processInput