Prototype parser for Idris's machine-readable interaction syntax

SExpParse.idr

module SExpParse

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%default total

data MessageFmt = KWD String
                | STRING
                | INT
                | MANY MessageFmt
                | SEQ (List MessageFmt)


%name MessageFmt fmt, f

data Keyword : String -> Type where
  Kwd : (s : String) -> Keyword s

mutual
  data MessageList : List MessageFmt -> Type where
    Nil : MessageList []
    (::) : (typeOf t) -> MessageList ts -> MessageList (t :: ts)


  typeOf : MessageFmt -> Type
  typeOf (KWD name) = Keyword name
  typeOf STRING = String
  typeOf INT = Integer
  typeOf (MANY fmt) = List (typeOf fmt)
  typeOf (SEQ fmts) = MessageList fmts


--------------------------
-- Client to server
--------------------------
replCompletions : MessageFmt
replCompletions = SEQ [KWD "repl-completions", STRING]

loadFile : MessageFmt
loadFile = SEQ [KWD "load-file", STRING]

interpret : MessageFmt
interpret = SEQ [KWD "interpret", STRING]


-- With continuation nr
clientMsg : MessageFmt -> MessageFmt
clientMsg fmt = SEQ [fmt, INT]

--------------------------
-- Server to client
--------------------------

warning : MessageFmt
warning = SEQ [KWD "warning", STRING, INT, INT, STRING]

completionReturn : MessageFmt
completionReturn = MANY STRING

okMsg : MessageFmt -> MessageFmt
okMsg fmt = SEQ [KWD "ok", fmt]

--------------------------
-- Reading and writing
--------------------------

%default partial

escape : String -> String
escape str = concat (map escapeChar (unpack str))
  where
    escapeChar : Char -> String
    escapeChar '\\' = "\\\\"
    escapeChar '\"' = "\\\""
    escapeChar c = singleton c



serialize : (fmt : MessageFmt) -> (typeOf fmt) -> String
serialize (KWD name) (Kwd name) = ":" ++ name
serialize STRING str = "\"" ++ escape str ++ "\""
serialize INT i = show i
serialize (MANY fmt) xs = "(" ++ concat (intersperse " " (map (serialize fmt) xs)) ++ ")"
serialize (SEQ fmts) xs  = "(" ++ serializeList fmts xs ++ ")"
  where serializeList : (fs : List MessageFmt) -> MessageList fs -> String
        serializeList []  [] = ""
        serializeList (f::List.Nil) (x::MessageList.Nil) = serialize f x
        serializeList (f::fs) (x::xs) = serialize f x ++ " " ++ serializeList fs xs



specialChar : Parser Char
specialChar = do
  c <- satisfy (const True)
  case c of
    '\"' => pure '\"'
    '\\' => pure '\\'
    ch   => pure ch


strContents : Parser (List Char)
strContents = (char '\"' $!> pure [])
          <|> do c <- satisfy (/= '\"')
                 if (c == '\\')
                   then map (::) specialChar <$> strContents
                   else map (c ::) strContents

str : Parser String
str = char '\"' $!> map pack strContents <?> "String"

inParens : Parser a -> Parser a
inParens p = char '(' $!> p <$! char ')'

parser : (fmt : MessageFmt) -> Parser (typeOf fmt)
parser (KWD x)    = string (":"++x) $!> pure (Kwd x)
parser STRING     = str
parser INT        = integer
parser (MANY fmt) = inParens (parser fmt `sepBy` space)
parser (SEQ fmts) = inParens (parserForElts fmts)
  where parserForElts : (fmts : List MessageFmt) -> Parser (MessageList fmts)
        parserForElts []      = pure []
        parserForElts (f::fs) = [| (parser f <$! space) :: lazy (parserForElts fs) |]


----------------------------------------
-- Tests
----------------------------------------

testA : Either String (List String)
testA = parse (parser completionReturn) "(\"foo\" \"fonky\" \"founder\")"

-- The case block even checks my spelling!
extractCompletionString : String -> Either String String
extractCompletionString str = do cmd <- parse (parser replCompletions) str
                                 case cmd of
                                   [Kwd "repl-completions", item] => return item


serializeCompletionCmd : String -> String
serializeCompletionCmd str = serialize replCompletions [Kwd "repl-completions", str]


-- should be Right foo
testSerializeParse : Either String String
testSerializeParse = extractCompletionString (serializeCompletionCmd "foo")