git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4181 from msmorgan/json
5d52a94Ahmad Salim Al-Sibahi
libs/contrib/Data/String/Extra.idr+13
compare with master
unifiedsplit
@@ -73,3 +73,16 @@ index n str with (unpack str)
73 index n str | [] = Nothing
73 index n str | [] = Nothing
74 index Z str | (x :: xs) = Just x
74 index Z str | (x :: xs) = Just x
75 index (S n) str | (x :: xs) = index n str | xs
75 index (S n) str | (x :: xs) = index n str | xs
76+
77+||| Produce a string by repeating the character `c` `n` times.
78+replicate : (n : Nat) -> (c : Char) -> String
79+replicate n c = pack $ replicate n c
80+
81+||| Indent a given string by `n` spaces.
82+indent : (n : Nat) -> String -> String
83+indent n x = replicate n ' ' ++ x
84+
85+||| Indent each line of a given string by `n` spaces.
86+indentLines : (n : Nat) -> String -> String
87+indentLines n str = unlines $ map (indent n) $ lines str
88+
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+98
@@ -0,0 +1,98 @@
1+module Language.JSON.Data
2+
3+import Data.String.Extra
4+
5+%access private
6+%default total
7+
8+public export
9+data JSON
10+ = JNull
11+ | JBoolean Bool
12+ | JNumber Double
13+ | JString String
14+ | JArray (List JSON)
15+ | JObject (List (String, JSON))
16+
17+%name JSON json
18+
19+showChar : Char -> String
20+showChar c
21+ = case c of
22+ '\b' => "\\b"
23+ '\f' => "\\f"
24+ '\n' => "\\n"
25+ '\r' => "\\r"
26+ '\t' => "\\t"
27+ '\\' => "\\\\"
28+ '"' => "\\\""
29+ c => if isControl c || c >= '\127'
30+ then "\\u" ++ b16ToHexString (fromInteger (cast (ord c)))
31+ else singleton c
32+
33+showString : String -> String
34+showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""
35+
36+||| Convert a JSON value into its string representation.
37+||| No whitespace is added.
38+stringify : JSON -> String
39+stringify JNull = "null"
40+stringify (JBoolean x) = if x then "true" else "false"
41+stringify (JNumber x) = show x
42+stringify (JString x) = showString x
43+stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
44+ where
45+ stringifyValues : List JSON -> String
46+ stringifyValues [] = ""
47+ stringifyValues (x :: xs) = stringify x
48+ ++ if isNil xs
49+ then ""
50+ else "," ++ stringifyValues xs
51+stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
52+ where
53+ stringifyProp : (String, JSON) -> String
54+ stringifyProp (key, value) = showString key ++ ":" ++ stringify value
55+
56+ stringifyProps : List (String, JSON) -> String
57+ stringifyProps [] = ""
58+ stringifyProps (x :: xs) = stringifyProp x
59+ ++ if isNil xs
60+ then ""
61+ else "," ++ stringifyProps xs
62+
63+export
64+Show JSON where
65+ show = stringify
66+
67+||| Format a JSON value, indenting by `n` spaces per nesting level.
68+|||
69+||| @curr The current indentation amount, measured in spaces.
70+||| @n The amount of spaces to indent per nesting level.
71+export
72+format : {default 0 curr : Nat} -> (n : Nat) -> JSON -> String
73+format {curr} n json = indent curr $ formatValue curr n json
74+ where
75+ formatValue : (curr, n : Nat) -> JSON -> String
76+ formatValue _ _ (JArray []) = "[]"
77+ formatValue curr n (JArray xs@(_ :: _)) = "[\n" ++ formatValues xs
78+ ++ indent curr "]"
79+ where
80+ formatValues : (xs : List JSON) -> {auto ok : NonEmpty xs} -> String
81+ formatValues (x :: xs) = format {curr=(curr + n)} n x
82+ ++ case nonEmpty xs of
83+ Yes ok => ",\n" ++ formatValues xs
84+ No _ => "\n"
85+ formatValue _ _ (JObject []) = "{}"
86+ formatValue curr n (JObject xs@(_ :: _)) = "{\n" ++ formatProps xs
87+ ++ indent curr "}"
88+ where
89+ formatProp : (String, JSON) -> String
90+ formatProp (key, value) = indent (curr + n) (showString key ++ ": ")
91+ ++ formatValue (curr + n) n value
92+
93+ formatProps : (xs : List (String, JSON)) -> {auto ok : NonEmpty xs} -> String
94+ formatProps (x :: xs) = formatProp x
95+ ++ case nonEmpty xs of
96+ Yes ok => ",\n" ++ formatProps xs
97+ No _ => "\n"
98+ formatValue _ _ x = stringify x
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/Text/Lexer.idr+8
@@ -197,6 +197,14 @@ symbol = pred (\x => not (isSpace x || isAlphaNum x))
197symbols : Lexer
197symbols : Lexer
198symbols = some symbol
198symbols = some symbol
199
199
200+||| Recognise a single control character
201+control : Lexer
202+control = pred isControl
203+
204+||| Recognise one or more control characters
205+controls : Lexer
206+controls = some control
207+
200||| Recognise zero or more occurrences of a sub-lexer between
208||| Recognise zero or more occurrences of a sub-lexer between
201||| delimiting lexers
209||| delimiting lexers
202surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
210surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
libs/contrib/contrib.ipkg+10
@@ -58,6 +58,16 @@ modules = CFFI
58 , Interfaces.Correlative
58 , Interfaces.Correlative
59 , Interfaces.Verified
59 , Interfaces.Verified
60
60
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+
61 , Network.Cgi
71 , Network.Cgi
62 , Network.Socket
72 , Network.Socket
63 , Network.Socket.Data
73 , Network.Socket.Data
libs/prelude/Prelude/Chars.idr+5
@@ -81,3 +81,8 @@ isHexDigit x = elem (toUpper x) hexChars where
81||| Returns true if the character is an octal digit.
81||| Returns true if the character is an octal digit.
82isOctDigit : Char -> Bool
82isOctDigit : Char -> Bool
83isOctDigit x = (x >= '0' && x <= '7')
83isOctDigit x = (x >= '0' && x <= '7')
84+
85+||| Returns true if the character is a control character.
86+isControl : Char -> Bool
87+isControl x = (x >= '\x0000' && x <= '\x001f')
88+ || (x >= '\x007f' && x <= '\x009f')