mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 10:41:59 +03:00
0f724fbc7f
This means temporarily removing some '%default total' from the libraries and tests, since the input for codata checking isn't right yet (it needs appropriate use of inlining)
28 lines
746 B
Idris
28 lines
746 B
Idris
module Language.JSON.String.Parser
|
|
|
|
import Language.JSON.String.Tokens
|
|
import Text.Lexer
|
|
import Text.Parser
|
|
|
|
-- TODO: totality checking for codata
|
|
-- %default total
|
|
|
|
private
|
|
stringChar : Grammar JSONStringToken True Char
|
|
stringChar = match JSTChar
|
|
<|> match JSTSimpleEscape
|
|
<|> match JSTUnicodeEscape
|
|
|
|
private
|
|
quotedString : Grammar JSONStringToken True String
|
|
quotedString = let q = match JSTQuote in
|
|
do chars <- between q q (many stringChar)
|
|
eof
|
|
pure $ pack chars
|
|
|
|
export
|
|
parseString : List JSONStringToken -> Maybe String
|
|
parseString toks = case parse quotedString toks of
|
|
Right (str, []) => Just str
|
|
_ => Nothing
|