SHARE
TWEET

Idris Parser Combinators

a guest Apr 21st, 2019 102 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. module Parse.XmlParser
  2.  
  3. import public Parse
  4. import Data.Vect
  5.  
  6. testText : String
  7. testText = "<parent-element>
  8.  <single-element attribute=\"value\" />
  9. </parent-element>"
  10.  
  11. record Element where
  12.   constructor MkElement
  13.   name : String
  14.   attributes : List (String, String)
  15.   children : List Element
  16.  
  17. attributePair : Parser (String, String)
  18. attributePair = pair identifier (right (literal "=") quotedString)
  19.  
  20. attributes : Parser (List (String, String))
  21. attributes = zeroOrMore (right space1 attributePair)
  22.  
  23. elementStart : Parser (String, List (String, String))
  24. elementStart = right (literal "<") (pair identifier attributes)
  25.  
  26. singleElement : Parser Element
  27. singleElement = (\(name, attrs) => MkElement name attrs []) <$> left elementStart (literal "/>")
  28.  
  29.  
  30. ----------------------------------------------------------
  31.  
  32. module Parse
  33.  
  34. import Data.Vect
  35.  
  36. %access export
  37.  
  38.  
  39. ---------------------------------
  40. -- Data    ----------------------
  41. ---------------------------------
  42.  
  43. ParseResult : Type -> Type
  44. ParseResult parseResult = Either String (String, parseResult)
  45.  
  46. parseFailure : String -> ParseResult parseResult
  47. parseFailure s = Left s
  48.  
  49. parseSuccess : String -> parseResult -> ParseResult parseResult
  50. parseSuccess s parseResult = Right (s, parseResult)
  51.  
  52.  
  53. data Parser parseResult = MkParser (String -> ParseResult parseResult)
  54. implementation Functor Parser where
  55.   map f (MkParser oldP) = MkParser (\s => pushin f (oldP s)) where
  56.     pushin : (f : a -> b) -> ParseResult a -> ParseResult b
  57.     pushin f r = case r of
  58.                   (Left s) => Left s
  59.                   (Right (s, e)) => Right (s, f e)
  60.  
  61. parse : Parser a -> String -> ParseResult a
  62. parse (MkParser f) = f
  63.  
  64.  
  65.  
  66. maybeStrHead : String -> Maybe Char
  67. maybeStrHead "" = Nothing
  68. maybeStrHead s = Just $ strHead s
  69.  
  70.  
  71. --------------------
  72. -- Combinators -----
  73. --------------------
  74. zeroOrMore : Parser a -> Parser (List a)
  75. zeroOrMore p = MkParser (\s => case parse p s of
  76.                       (Right (rest, a)) => case parse (zeroOrMore p) rest of
  77.                                               (Right (rest2, as)) => parseSuccess rest2 (a :: as)
  78.                                               (Left rest2) => parseSuccess rest2 [a] -- can't happen?
  79.                       (Left rest) => parseSuccess rest [])
  80.  
  81. oneOrMore : Parser a -> Parser (List a)
  82. oneOrMore p = MkParser (\s => case parse p s of
  83.                      (Right (rest, a)) => case parse (zeroOrMore p) rest of
  84.                                              (Right (rest2, as)) => parseSuccess rest2 (a :: as)
  85.                                              (Left rest2) => parseSuccess rest2 [a] -- can't happen?
  86.                      (Left all) => parseFailure all)
  87.  
  88. pair : Parser a -> Parser b -> Parser (a, b)
  89. pair p1 p2 = MkParser (\s1 => do
  90.   (s2, r1) <- parse p1 s1
  91.   (s3, r2) <- parse p2 s2
  92.   pure (s3, (r1, r2)))
  93.  
  94. left : Parser a -> Parser b -> Parser a
  95. left p1 p2 = map fst $ pair p1 p2
  96.  
  97. right : Parser a -> Parser b -> Parser b
  98. right p1 p2 = map snd $ pair p1 p2
  99.  
  100.  
  101. ---------------------------------
  102. -- Parsers ----------------------
  103. ---------------------------------
  104.  
  105. drop : Nat -> String -> String
  106. drop Z s = s
  107. drop (S k) s = drop k (strTail s)
  108.  
  109. literal : String -> Parser String
  110. literal expected = MkParser (\s => if isPrefixOf expected s
  111.                              then parseSuccess (drop (length expected) s) expected
  112.                              else parseFailure s)
  113.  
  114. anyChar : Parser Char
  115. anyChar = MkParser (\s => case maybeStrHead s of
  116.                    Just c => Right (strTail s, c)
  117.                    Nothing => Left "")
  118.  
  119. predicate : (a -> Bool) -> Parser a -> Parser a
  120. predicate f pa = MkParser (\s => let r = parse pa s in
  121.                           case r of
  122.                                Right (rest, a) => if f a then r else Left s
  123.                                Left fail => r)
  124.  
  125. isAlphaNumOrDash : Char -> Bool
  126. isAlphaNumOrDash c = isAlphaNum c || ('-' == c)
  127.  
  128. identifier : Parser String
  129. identifier = MkParser (\s => case s of
  130.                                   "" => parseFailure ""
  131.                                   _ =>  if isAlpha (strHead s)
  132.                                            then let (parsed, rest) = span isAlphaNumOrDash s in
  133.                                                     parseSuccess rest parsed
  134.                                            else parseFailure s)
  135.  
  136. matchIs : (Char -> Bool) -> Parser String
  137. matchIs cb = MkParser (\s => if s == "" then parseFailure "" else if cb (strHead s)
  138.                  then parseSuccess (strTail s) (singleton (strHead s))
  139.                  else parseFailure s)
  140.  
  141. whitespaceChar : Parser Char
  142. whitespaceChar = predicate isSpace anyChar
  143.  
  144. space1 : Parser (List Char)
  145. space1 = oneOrMore whitespaceChar
  146.  
  147. space0 : Parser (List Char)
  148. space0 = zeroOrMore whitespaceChar
  149.  
  150. quotedString : Parser String
  151. quotedString = (map pack
  152.                  (right (literal "\"")
  153.                    (left
  154.                      (zeroOrMore (predicate (/= '\"') anyChar))
  155.                      (literal "\""))))
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top