git.iko.soy/Idris-dev
on master help sign in
Language.JSON: total JSON parsing
commit4777dce8828e56d94dffed53237b67b764050485 authorMichael Morgan <morgan.michael@me.com> dateMon 4 Dec 2017, 11:40 (9 years ago) parent905b7fc
10 files changed+409
compare with master
unifiedsplit
libs/contrib/Language/JSON.idr+14 libs/contrib/Language/JSON/Data.idr+63 libs/contrib/Language/JSON/Lexer.idr+40 libs/contrib/Language/JSON/Parser.idr+71 libs/contrib/Language/JSON/String.idr+16 libs/contrib/Language/JSON/String/Lexer.idr+38 libs/contrib/Language/JSON/String/Parser.idr+25 libs/contrib/Language/JSON/String/Tokens.idr+60 libs/contrib/Language/JSON/Tokens.idr+72 libs/contrib/contrib.ipkg+10
libs/contrib/Language/JSON.idrnew file+14
@@ -0,0 +1,14 @@
1+||| The JSON language, as described at http://json.org/
2+module Language.JSON
3+
4+import Language.JSON.Lexer
5+import Language.JSON.Parser
6+
7+import public Language.JSON.Data
8+
9+%access export
10+%default total
11+
12+||| Parse a JSON string.
13+parse : String -> Maybe JSON
14+parse x = parseJSON !(lexJSON x)
libs/contrib/Language/JSON/Data.idrnew file+63
@@ -0,0 +1,63 @@
1+module Language.JSON.Data
2+
3+%access private
4+%default total
5+
6+public export
7+data JSON
8+ = JNull
9+ | JBoolean Bool
10+ | JNumber Double
11+ | JString String
12+ | JArray (List JSON)
13+ | JObject (List (String, JSON))
14+
15+%name JSON json
16+
17+showChar : Char -> String
18+showChar c
19+ = case c of
20+ '\b' => "\\b"
21+ '\f' => "\\f"
22+ '\n' => "\\n"
23+ '\r' => "\\r"
24+ '\t' => "\\t"
25+ '\\' => "\\\\"
26+ '"' => "\\\""
27+ c => if isControl c || c >= '\127'
28+ then "\\u" ++ b16ToHexString (fromInteger (cast (ord c)))
29+ else singleton c
30+
31+showString : String -> String
32+showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""
33+
34+||| Convert a JSON value into its string representation.
35+||| No whitespace is added.
36+stringify : JSON -> String
37+stringify JNull = "null"
38+stringify (JBoolean x) = if x then "true" else "false"
39+stringify (JNumber x) = show x
40+stringify (JString x) = showString x
41+stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
42+ where
43+ stringifyValues : List JSON -> String
44+ stringifyValues [] = ""
45+ stringifyValues (x :: xs) = stringify x
46+ ++ if isNil xs
47+ then ""
48+ else "," ++ stringifyValues xs
49+stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
50+ where
51+ stringifyProp : (String, JSON) -> String
52+ stringifyProp (key, value) = showString key ++ ":" ++ stringify value
53+
54+ stringifyProps : List (String, JSON) -> String
55+ stringifyProps [] = ""
56+ stringifyProps (x :: xs) = stringifyProp x
57+ ++ if isNil xs
58+ then ""
59+ else "," ++ stringifyProps xs
60+
61+export
62+Show JSON where
63+ show = stringify
libs/contrib/Language/JSON/Lexer.idrnew file+40
@@ -0,0 +1,40 @@
1+module Language.JSON.Lexer
2+
3+import Language.JSON.String
4+import Text.Lexer
5+import Text.Token
6+
7+import public Language.JSON.Tokens
8+
9+%access private
10+%default total
11+
12+numberLit : Lexer
13+numberLit
14+ = let sign = is '-'
15+ whole = is '0' <|> range '1' '9' <+> many digit
16+ frac = is '.' <+> digits
17+ exp = like 'e' <+> opt (oneOf "+-") <+> digits in
18+ opt sign <+> whole <+> opt frac <+> opt exp
19+
20+jsonTokenMap : TokenMap JSONToken
21+jsonTokenMap = toTokenMap $
22+ [ (spaces, JTIgnore)
23+ , (is ',', JTPunct Comma)
24+ , (is ':', JTPunct Colon)
25+ , (is '[', JTPunct $ Square Open)
26+ , (is ']', JTPunct $ Square Close)
27+ , (is '{', JTPunct $ Curly Open)
28+ , (is '}', JTPunct $ Curly Close)
29+ , (exact "null", JTNull)
30+ , (exact strTrue <|> exact strFalse, JTBoolean)
31+ , (numberLit, JTNumber)
32+ , (permissiveStringLit, JTString)
33+ ]
34+
35+export
36+lexJSON : String -> Maybe (List JSONToken)
37+lexJSON str
38+ = case lex jsonTokenMap str of
39+ (tokens, _, _, "") => Just $ map TokenData.tok tokens
40+ _ => Nothing
libs/contrib/Language/JSON/Parser.idrnew file+71
@@ -0,0 +1,71 @@
1+module Language.JSON.Parser
2+
3+import Language.JSON.Data
4+import Text.Parser
5+import Text.Token
6+
7+import public Language.JSON.Tokens
8+
9+%access private
10+%default total
11+
12+punct : Punctuation -> Grammar JSONToken True ()
13+punct p = match $ JTPunct p
14+
15+rawString : Grammar JSONToken True String
16+rawString = do mstr <- match JTString
17+ the (Grammar _ False _) $
18+ case mstr of
19+ Just str => pure str
20+ Nothing => fail "invalid string"
21+
22+mutual
23+ json : Grammar JSONToken True JSON
24+ json = object
25+ <|> array
26+ <|> string
27+ <|> boolean
28+ <|> number
29+ <|> null
30+
31+ object : Grammar JSONToken True JSON
32+ object = do punct $ Curly Open
33+ commit
34+ props <- properties
35+ punct $ Curly Close
36+ pure $ JObject props
37+ where
38+ properties : Grammar JSONToken False (List (String, JSON))
39+ properties = sepBy (punct Comma) $
40+ do key <- rawString
41+ punct Colon
42+ value <- json
43+ pure (key, value)
44+
45+ array : Grammar JSONToken True JSON
46+ array = do punct (Square Open)
47+ commit
48+ vals <- values
49+ punct (Square Close)
50+ pure (JArray vals)
51+ where
52+ values : Grammar JSONToken False (List JSON)
53+ values = sepBy (punct Comma) json
54+
55+ string : Grammar JSONToken True JSON
56+ string = map JString rawString
57+
58+ boolean : Grammar JSONToken True JSON
59+ boolean = map JBoolean $ match JTBoolean
60+
61+ number : Grammar JSONToken True JSON
62+ number = map JNumber $ match JTNumber
63+
64+ null : Grammar JSONToken True JSON
65+ null = map (const JNull) $ match JTNull
66+
67+export
68+parseJSON : List JSONToken -> Maybe JSON
69+parseJSON toks = case parse json $ filter (not . ignored) toks of
70+ Right (j, []) => Just j
71+ _ => Nothing
libs/contrib/Language/JSON/String.idrnew file+16
@@ -0,0 +1,16 @@
1+module Language.JSON.String
2+
3+import Language.JSON.String.Lexer
4+import Language.JSON.String.Parser
5+import Language.JSON.String.Tokens
6+import Text.Lexer
7+
8+%access export
9+%default total
10+
11+permissiveStringLit : Lexer
12+permissiveStringLit
13+ = quo <+> manyUntil quo (esc any <|> any) <+> opt quo
14+
15+stringValue : String -> Maybe String
16+stringValue x = parseString !(lexString x)
libs/contrib/Language/JSON/String/Lexer.idrnew file+38
@@ -0,0 +1,38 @@
1+module Language.JSON.String.Lexer
2+
3+import Language.JSON.String.Tokens
4+import Text.Lexer
5+
6+%access private
7+%default total
8+
9+export
10+quo : Lexer
11+quo = is '"'
12+
13+export
14+esc : Lexer -> Lexer
15+esc = escape '\\'
16+
17+unicodeEscape : Lexer
18+unicodeEscape = esc $ is 'u' <+> count (exactly 4) hexDigit
19+
20+simpleEscape : Lexer
21+simpleEscape = esc $ oneOf "\"\\/bfnrt"
22+
23+legalChar : Lexer
24+legalChar = non (quo <|> is '\\' <|> control)
25+
26+jsonStringTokenMap : TokenMap JSONStringToken
27+jsonStringTokenMap = toTokenMap $
28+ [ (quo, JSTQuote)
29+ , (unicodeEscape, JSTUnicodeEscape)
30+ , (simpleEscape, JSTSimpleEscape)
31+ , (legalChar, JSTChar)
32+ ]
33+
34+export
35+lexString : String -> Maybe (List JSONStringToken)
36+lexString x = case lex jsonStringTokenMap x of
37+ (toks, _, _, "") => Just $ map TokenData.tok toks
38+ _ => Nothing
libs/contrib/Language/JSON/String/Parser.idrnew file+25
@@ -0,0 +1,25 @@
1+module Language.JSON.String.Parser
2+
3+import Language.JSON.String.Tokens
4+import Text.Lexer
5+import Text.Parser
6+
7+%access private
8+%default total
9+
10+stringChar : Grammar JSONStringToken True Char
11+stringChar = match JSTChar
12+ <|> match JSTSimpleEscape
13+ <|> match JSTUnicodeEscape
14+
15+quotedString : Grammar JSONStringToken True String
16+quotedString = let q = match JSTQuote in
17+ do chars <- between q q (many stringChar)
18+ eof
19+ pure $ pack chars
20+
21+export
22+parseString : List JSONStringToken -> Maybe String
23+parseString toks = case parse quotedString toks of
24+ Right (str, []) => Just str
25+ _ => Nothing
libs/contrib/Language/JSON/String/Tokens.idrnew file+60
@@ -0,0 +1,60 @@
1+module Language.JSON.String.Tokens
2+
3+import Data.String.Extra
4+import Text.Token
5+
6+%access public export
7+%default total
8+
9+data JSONStringTokenKind
10+ = JSTQuote
11+ | JSTChar
12+ | JSTSimpleEscape
13+ | JSTUnicodeEscape
14+
15+JSONStringToken : Type
16+JSONStringToken = Token JSONStringTokenKind
17+
18+Eq JSONStringTokenKind where
19+ (==) JSTQuote JSTQuote = True
20+ (==) JSTChar JSTChar = True
21+ (==) JSTSimpleEscape JSTSimpleEscape = True
22+ (==) JSTUnicodeEscape JSTUnicodeEscape = True
23+ (==) _ _ = False
24+
25+private
26+charValue : String -> Char
27+charValue x = case index 0 x of
28+ Nothing => '\NUL'
29+ Just c => c
30+
31+private
32+simpleEscapeValue : String -> Char
33+simpleEscapeValue x
34+ = case index 1 x of
35+ Nothing => '\NUL'
36+ Just c => case c of
37+ '"' => '"'
38+ '\\' => '\\'
39+ '/' => '/'
40+ 'b' => '\b'
41+ 'f' => '\f'
42+ 'n' => '\n'
43+ 'r' => '\r'
44+ 't' => '\t'
45+ _ => '\NUL'
46+
47+private
48+unicodeEscapeValue : String -> Char
49+unicodeEscapeValue x = chr $ cast ("0x" ++ drop 2 x)
50+
51+TokenKind JSONStringTokenKind where
52+ TokType JSTQuote = ()
53+ TokType JSTChar = Char
54+ TokType JSTSimpleEscape = Char
55+ TokType JSTUnicodeEscape = Char
56+
57+ tokValue JSTQuote = const ()
58+ tokValue JSTChar = charValue
59+ tokValue JSTSimpleEscape = simpleEscapeValue
60+ tokValue JSTUnicodeEscape = unicodeEscapeValue
libs/contrib/Language/JSON/Tokens.idrnew file+72
@@ -0,0 +1,72 @@
1+module Language.JSON.Tokens
2+
3+import Language.JSON.String
4+import Text.Token
5+
6+%access public export
7+%default total
8+
9+strTrue : String
10+strTrue = "true"
11+
12+strFalse : String
13+strFalse = "false"
14+
15+data Bracket = Open | Close
16+
17+Eq Bracket where
18+ (==) Open Open = True
19+ (==) Close Close = True
20+ (==) _ _ = False
21+
22+data Punctuation
23+ = Comma
24+ | Colon
25+ | Square Bracket
26+ | Curly Bracket
27+
28+Eq Punctuation where
29+ (==) Comma Comma = True
30+ (==) Colon Colon = True
31+ (==) (Square b1) (Square b2) = b1 == b2
32+ (==) (Curly b1) (Curly b2) = b1 == b2
33+ (==) _ _ = False
34+
35+data JSONTokenKind
36+ = JTBoolean
37+ | JTNumber
38+ | JTString
39+ | JTNull
40+ | JTPunct Punctuation
41+ | JTIgnore
42+
43+JSONToken : Type
44+JSONToken = Token JSONTokenKind
45+
46+Eq JSONTokenKind where
47+ (==) JTBoolean JTBoolean = True
48+ (==) JTNumber JTNumber = True
49+ (==) JTString JTString = True
50+ (==) JTNull JTNull = True
51+ (==) (JTPunct p1) (JTPunct p2) = p1 == p2
52+ (==) _ _ = False
53+
54+TokenKind JSONTokenKind where
55+ TokType JTBoolean = Bool
56+ TokType JTNumber = Double
57+ TokType JTString = Maybe String
58+ TokType JTNull = ()
59+ TokType (JTPunct _) = ()
60+ TokType JTIgnore = ()
61+
62+ tokValue JTBoolean x = x == strTrue
63+ tokValue JTNumber x = cast x
64+ tokValue JTString x = stringValue x
65+ tokValue JTNull _ = ()
66+ tokValue (JTPunct _) _ = ()
67+ tokValue JTIgnore _ = ()
68+
69+export
70+ignored : JSONToken -> Bool
71+ignored (Tok JTIgnore _) = True
72+ignored _ = False
libs/contrib/contrib.ipkg+10
@@ -58,6 +58,16 @@ modules = CFFI
5858 , Interfaces.Correlative
5959 , Interfaces.Verified
6060
61+ , Language.JSON
62+ , Language.JSON.Data
63+ , Language.JSON.Lexer
64+ , Language.JSON.Parser
65+ , Language.JSON.String
66+ , Language.JSON.String.Lexer
67+ , Language.JSON.String.Parser
68+ , Language.JSON.String.Tokens
69+ , Language.JSON.Tokens
70+
6171 , Network.Cgi
6272 , Network.Socket
6373 , Network.Socket.Data