Idris Parser Combinators

module Parse.XmlParser

import public Parse
import Data.Vect

testText : String
testText = "<parent-element>
  <single-element attribute=\"value\" />
</parent-element>"

record Element where
  constructor MkElement
  name : String
  attributes : List (String, String)
  children : List Element

attributePair : Parser (String, String)
attributePair = pair identifier (right (literal "=") quotedString)

attributes : Parser (List (String, String))
attributes = zeroOrMore (right space1 attributePair)

elementStart : Parser (String, List (String, String))
elementStart = right (literal "<") (pair identifier attributes)

singleElement : Parser Element
singleElement = (\(name, attrs) => MkElement name attrs []) <$> left elementStart (literal "/>")


----------------------------------------------------------

module Parse

import Data.Vect

%access export


---------------------------------
-- Data    ----------------------
---------------------------------

ParseResult : Type -> Type
ParseResult parseResult = Either String (String, parseResult)

parseFailure : String -> ParseResult parseResult
parseFailure s = Left s

parseSuccess : String -> parseResult -> ParseResult parseResult
parseSuccess s parseResult = Right (s, parseResult)


data Parser parseResult = MkParser (String -> ParseResult parseResult)
implementation Functor Parser where
  map f (MkParser oldP) = MkParser (\s => pushin f (oldP s)) where
    pushin : (f : a -> b) -> ParseResult a -> ParseResult b
    pushin f r = case r of
                  (Left s) => Left s
                  (Right (s, e)) => Right (s, f e)

parse : Parser a -> String -> ParseResult a
parse (MkParser f) = f



maybeStrHead : String -> Maybe Char
maybeStrHead "" = Nothing
maybeStrHead s = Just $ strHead s


--------------------
-- Combinators -----
--------------------
zeroOrMore : Parser a -> Parser (List a)
zeroOrMore p = MkParser (\s => case parse p s of
                      (Right (rest, a)) => case parse (zeroOrMore p) rest of
                                              (Right (rest2, as)) => parseSuccess rest2 (a :: as)
                                              (Left rest2) => parseSuccess rest2 [a] -- can't happen?
                      (Left rest) => parseSuccess rest [])

oneOrMore : Parser a -> Parser (List a)
oneOrMore p = MkParser (\s => case parse p s of
                     (Right (rest, a)) => case parse (zeroOrMore p) rest of
                                             (Right (rest2, as)) => parseSuccess rest2 (a :: as)
                                             (Left rest2) => parseSuccess rest2 [a] -- can't happen?
                     (Left all) => parseFailure all)

pair : Parser a -> Parser b -> Parser (a, b)
pair p1 p2 = MkParser (\s1 => do
  (s2, r1) <- parse p1 s1
  (s3, r2) <- parse p2 s2
  pure (s3, (r1, r2)))

left : Parser a -> Parser b -> Parser a
left p1 p2 = map fst $ pair p1 p2

right : Parser a -> Parser b -> Parser b
right p1 p2 = map snd $ pair p1 p2


---------------------------------
-- Parsers ----------------------
---------------------------------

drop : Nat -> String -> String
drop Z s = s
drop (S k) s = drop k (strTail s)

literal : String -> Parser String
literal expected = MkParser (\s => if isPrefixOf expected s
                             then parseSuccess (drop (length expected) s) expected
                             else parseFailure s)

anyChar : Parser Char
anyChar = MkParser (\s => case maybeStrHead s of
                   Just c => Right (strTail s, c)
                   Nothing => Left "")

predicate : (a -> Bool) -> Parser a -> Parser a
predicate f pa = MkParser (\s => let r = parse pa s in
                          case r of
                               Right (rest, a) => if f a then r else Left s
                               Left fail => r)

isAlphaNumOrDash : Char -> Bool
isAlphaNumOrDash c = isAlphaNum c || ('-' == c)

identifier : Parser String
identifier = MkParser (\s => case s of
                                  "" => parseFailure ""
                                  _ =>  if isAlpha (strHead s)
                                           then let (parsed, rest) = span isAlphaNumOrDash s in
                                                    parseSuccess rest parsed
                                           else parseFailure s)

matchIs : (Char -> Bool) -> Parser String
matchIs cb = MkParser (\s => if s == "" then parseFailure "" else if cb (strHead s)
                 then parseSuccess (strTail s) (singleton (strHead s))
                 else parseFailure s)

whitespaceChar : Parser Char
whitespaceChar = predicate isSpace anyChar

space1 : Parser (List Char)
space1 = oneOrMore whitespaceChar

space0 : Parser (List Char)
space0 = zeroOrMore whitespaceChar

quotedString : Parser String
quotedString = (map pack
                 (right (literal "\"")
                   (left
                     (zeroOrMore (predicate (/= '\"') anyChar))
                     (literal "\""))))