Merge pull request #322 from rbarreiro/copy_json_from_idris_dev

added json

libs/contrib/Data/String/Extra.idr

@@ -0,0 +1,102 @@
+module Data.String.Extra
+
+import Data.Strings
+
+%default total
+
+
+infixl 5 +>
+infixr 5 <+
+
+||| Adds a character to the end of the specified string.
+|||
+||| ```idris example
+||| strSnoc "AB" 'C'
+||| ```
+||| ```idris example
+||| strSnoc "" 'A'
+||| ```
+public export
+strSnoc : String -> Char -> String
+strSnoc s c = s ++ (singleton c)
+
+||| Alias of `strSnoc`
+|||
+||| ```idris example
+||| "AB" +> 'C'
+||| ```
+public export
+(+>) : String -> Char -> String
+(+>) = strSnoc
+
+||| Alias of `strCons`
+|||
+||| ```idris example
+||| 'A' <+ "AB"
+||| ```
+public export
+(<+) : Char -> String -> String
+(<+) = strCons
+
+||| Take the first `n` characters from a string. Returns the whole string
+||| if it's too short.
+public export
+take : (n : Nat) -> (input : String) -> String
+take n str = substr Z n str
+
+||| Take the last `n` characters from a string. Returns the whole string
+||| if it's too short.
+public export
+takeLast : (n : Nat) -> (input : String) -> String
+takeLast n str with (length str)
+  takeLast n str | len with (isLTE n len)
+    takeLast n str | len | Yes prf = substr (len `minus` n) len str
+    takeLast n str | len | No contra = str
+
+||| Remove the first `n` characters from a string. Returns the empty string if
+||| the input string is too short.
+public export
+drop : (n : Nat) -> (input : String) -> String
+drop n str = substr n (length str) str
+
+||| Remove the last `n` characters from a string. Returns the empty string if
+||| the input string is too short.
+public export
+dropLast : (n : Nat) -> (input : String) -> String
+dropLast n str = reverse (drop n (reverse str))
+
+||| Remove the first and last `n` characters from a string. Returns the empty
+||| string if the input string is too short.
+public export
+shrink : (n : Nat) -> (input : String) -> String
+shrink n str = dropLast n (drop n str)
+
+||| Concatenate the strings from a `Foldable` containing strings, separated by
+||| the given string.
+public export
+join : (sep : String) -> Foldable t => (xs : t String) -> String
+join sep xs = drop (length sep)
+                   (foldl (\acc, x => acc ++ sep ++ x) "" xs)
+
+||| Get a character from a string if the string is long enough.
+public export
+index : (n : Nat) -> (input : String) -> Maybe Char
+index n str with (unpack str)
+  index n str | [] = Nothing
+  index Z str | (x :: xs) = Just x
+  index (S n) str | (x :: xs) = index n str | xs
+
+||| Produce a string by repeating the character `c` `n` times.
+public export
+replicate : (n : Nat) -> (c : Char) -> String
+replicate n c = pack $ replicate n c
+
+||| Indent a given string by `n` spaces.
+public export
+indent : (n : Nat) -> String -> String
+indent n x = replicate n ' ' ++ x
+
+||| Indent each line of a given string by `n` spaces.
+public export
+indentLines : (n : Nat) -> String -> String
+indentLines n str = unlines $ map (indent n) $ lines str

libs/contrib/Language/JSON.idr

@@ -0,0 +1,14 @@
+||| The JSON language, as described at https://json.org/
+module Language.JSON
+
+import Language.JSON.Lexer
+import Language.JSON.Parser
+
+import public Language.JSON.Data
+
+%default total
+
+||| Parse a JSON string.
+export
+parse : String -> Maybe JSON
+parse x = parseJSON !(lexJSON x)

libs/contrib/Language/JSON/Data.idr

@@ -0,0 +1,126 @@
+module Language.JSON.Data
+
+import Data.String.Extra
+import Data.Strings
+import Data.List
+
+%default total
+
+public export
+data JSON
+   = JNull
+   | JBoolean Bool
+   | JNumber Double
+   | JString String
+   | JArray (List JSON)
+   | JObject (List (String, JSON))
+
+%name JSON json
+
+
+private
+intToHexString : Int -> String
+intToHexString n =
+  case n of
+    0 => "0"
+    1 => "1"
+    2 => "2"
+    3 => "3"
+    4 => "4"
+    5 => "5"
+    6 => "6"
+    7 => "7"
+    8 => "8"
+    9 => "9"
+    10 => "A"
+    11 => "B"
+    12 => "C"
+    13 => "D"
+    14 => "E"
+    15 => "F"
+    other => intToHexString (shiftR n 4) ++ intToHexString (mod n 16)
+
+private
+showChar : Char -> String
+showChar c
+  = case c of
+         '\b' => "\\b"
+         '\f' => "\\f"
+         '\n' => "\\n"
+         '\r' => "\\r"
+         '\t' => "\\t"
+         '\\' => "\\\\"
+         '"'  => "\\\""
+         c => if isControl c || c >= '\127'
+--                 then "\\u" ++ b16ToHexString (fromInteger (cast (ord c)))
+                 then "\\u" ++ intToHexString (ord c)-- quick hack until b16ToHexString is available in idris2
+                 else singleton c
+
+private
+showString : String -> String
+showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""
+
+||| Convert a JSON value into its string representation.
+||| No whitespace is added.
+private
+stringify : JSON -> String
+stringify JNull = "null"
+stringify (JBoolean x) = if x then "true" else "false"
+stringify (JNumber x) = show x
+stringify (JString x) = showString x
+stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
+  where
+    stringifyValues : List JSON -> String
+    stringifyValues [] = ""
+    stringifyValues (x :: xs) = stringify x
+                             ++ if isNil xs
+                                   then ""
+                                   else "," ++ stringifyValues xs
+stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
+  where
+    stringifyProp : (String, JSON) -> String
+    stringifyProp (key, value) = showString key ++ ":" ++ stringify value
+
+    stringifyProps : List (String, JSON) -> String
+    stringifyProps [] = ""
+    stringifyProps (x :: xs) = stringifyProp x
+                            ++ if isNil xs
+                                  then ""
+                                  else "," ++ stringifyProps xs
+
+export
+Show JSON where
+  show = stringify
+
+||| Format a JSON value, indenting by `n` spaces per nesting level.
+|||
+||| @curr The current indentation amount, measured in spaces.
+||| @n The amount of spaces to indent per nesting level.
+export
+format : {default 0 curr : Nat} -> (n : Nat) -> JSON -> String
+format {curr} n json = indent curr $ formatValue curr n json
+  where
+    formatValue : (curr, n : Nat) -> JSON -> String
+    formatValue _ _ (JArray []) = "[]"
+    formatValue curr n (JArray xs@(_ :: _)) = "[\n" ++ formatValues xs
+                                           ++ indent curr "]"
+      where
+        formatValues : (xs : List JSON) -> {auto ok : NonEmpty xs} -> String
+        formatValues (x :: xs) = format {curr=(curr + n)} n x
+                              ++ case xs of
+                                      _ :: _ => ",\n" ++ formatValues xs
+                                      [] => "\n"
+    formatValue _ _ (JObject []) = "{}"
+    formatValue curr n (JObject xs@(_ :: _)) = "{\n" ++ formatProps xs
+                                            ++ indent curr "}"
+      where
+        formatProp : (String, JSON) -> String
+        formatProp (key, value) = indent (curr + n) (showString key ++ ": ")
+                               ++ formatValue (curr + n) n value
+
+        formatProps : (xs : List (String, JSON)) -> {auto ok : NonEmpty xs} -> String
+        formatProps (x :: xs) = formatProp x
+                             ++ case xs of
+                                     _ :: _ => ",\n" ++ formatProps xs
+                                     [] => "\n"
+    formatValue _ _ x = stringify x

libs/contrib/Language/JSON/Lexer.idr

@@ -0,0 +1,41 @@
+module Language.JSON.Lexer
+
+import Language.JSON.String
+import Text.Lexer
+import Text.Token
+
+import public Language.JSON.Tokens
+
+%default total
+
+private
+numberLit : Lexer
+numberLit
+  = let sign  = is '-'
+        whole = is '0' <|> range '1' '9' <+> many digit
+        frac  = is '.' <+> digits
+        exp   = like 'e' <+> opt (oneOf "+-") <+> digits in
+        opt sign <+> whole <+> opt frac <+> opt exp
+
+private
+jsonTokenMap : TokenMap JSONToken
+jsonTokenMap = toTokenMap $
+  [ (spaces, JTIgnore)
+  , (is ',', JTPunct Comma)
+  , (is ':', JTPunct Colon)
+  , (is '[', JTPunct $ Square Open)
+  , (is ']', JTPunct $ Square Close)
+  , (is '{', JTPunct $ Curly Open)
+  , (is '}', JTPunct $ Curly Close)
+  , (exact "null", JTNull)
+  , (exact strTrue <|> exact strFalse, JTBoolean)
+  , (numberLit, JTNumber)
+  , (permissiveStringLit, JTString)
+  ]
+
+export
+lexJSON : String -> Maybe (List JSONToken)
+lexJSON str
+  = case lex jsonTokenMap str of
+         (tokens, _, _, "") => Just $ map TokenData.tok tokens
+         _ => Nothing

libs/contrib/Language/JSON/Parser.idr

@@ -0,0 +1,80 @@
+module Language.JSON.Parser
+
+import Language.JSON.Data
+import Text.Parser
+import Text.Token
+import Data.List
+
+import public Language.JSON.Tokens
+
+%default total
+
+private
+punct : Punctuation -> Grammar JSONToken True ()
+punct p = match $ JTPunct p
+
+private
+rawString : Grammar JSONToken True String
+rawString = do mstr <- match JTString
+               the (Grammar _ False _) $
+                   case mstr of
+                        Just str => pure str
+                        Nothing => fail "invalid string"
+
+mutual
+  private
+  json : Grammar JSONToken True JSON
+  json = object
+     <|> array
+     <|> string
+     <|> boolean
+     <|> number
+     <|> null
+
+  private
+  object : Grammar JSONToken True JSON
+  object = do punct $ Curly Open
+              commit
+              props <- properties
+              punct $ Curly Close
+              pure $ JObject props
+    where
+      properties : Grammar JSONToken False (List (String, JSON))
+      properties = sepBy (punct Comma) $
+                         do key <- rawString
+                            punct Colon
+                            value <- json
+                            pure (key, value)
+
+  private
+  array : Grammar JSONToken True JSON
+  array = do punct (Square Open)
+             commit
+             vals <- values
+             punct (Square Close)
+             pure (JArray vals)
+    where
+      values : Grammar JSONToken False (List JSON)
+      values = sepBy (punct Comma) json
+
+  private
+  string : Grammar JSONToken True JSON
+  string = map JString rawString
+
+  private
+  boolean : Grammar JSONToken True JSON
+  boolean = map JBoolean $ match JTBoolean
+
+  private
+  number : Grammar JSONToken True JSON
+  number = map JNumber $ match JTNumber
+
+  private
+  null : Grammar JSONToken True JSON
+  null = map (const JNull) $ match JTNull
+
+export
+parseJSON : List JSONToken -> Maybe JSON
+parseJSON toks = case parse json $ filter (not . ignored) toks of
+                      Right (j, []) => Just j
+                      _ => Nothing

libs/contrib/Language/JSON/String.idr

@@ -0,0 +1,17 @@
+module Language.JSON.String
+
+import Language.JSON.String.Lexer
+import Language.JSON.String.Parser
+import Language.JSON.String.Tokens
+import Text.Lexer
+
+%default total
+
+export
+permissiveStringLit : Lexer
+permissiveStringLit
+  = quo <+> manyUntil quo (esc any <|> any) <+> opt quo
+
+export
+stringValue : String -> Maybe String
+stringValue x = parseString !(lexString x)

libs/contrib/Language/JSON/String/Lexer.idr

@@ -0,0 +1,41 @@
+module Language.JSON.String.Lexer
+
+import Language.JSON.String.Tokens
+import Text.Lexer
+
+%default total
+
+export
+quo : Lexer
+quo = is '"'
+
+export
+esc : Lexer -> Lexer
+esc = escape '\\'
+
+private
+unicodeEscape : Lexer
+unicodeEscape = esc $ is 'u' <+> count (exactly 4) hexDigit
+
+private
+simpleEscape : Lexer
+simpleEscape = esc $ oneOf "\"\\/bfnrt"
+
+private
+legalChar : Lexer
+legalChar = non (quo <|> is '\\' <|> control)
+
+private
+jsonStringTokenMap : TokenMap JSONStringToken
+jsonStringTokenMap = toTokenMap $
+  [ (quo, JSTQuote)
+  , (unicodeEscape, JSTUnicodeEscape)
+  , (simpleEscape, JSTSimpleEscape)
+  , (legalChar, JSTChar)
+  ]
+
+export
+lexString : String -> Maybe (List JSONStringToken)
+lexString x = case lex jsonStringTokenMap x of
+                   (toks, _, _, "") => Just $ map TokenData.tok toks
+                   _ => Nothing

libs/contrib/Language/JSON/String/Parser.idr

@@ -0,0 +1,26 @@
+module Language.JSON.String.Parser
+
+import Language.JSON.String.Tokens
+import Text.Lexer
+import Text.Parser
+
+%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

libs/contrib/Language/JSON/String/Tokens.idr

@@ -0,0 +1,63 @@
+module Language.JSON.String.Tokens
+
+import Data.String.Extra
+import Text.Token
+
+%default total
+
+public export
+data JSONStringTokenKind
+  = JSTQuote
+  | JSTChar
+  | JSTSimpleEscape
+  | JSTUnicodeEscape
+
+public export
+JSONStringToken : Type
+JSONStringToken = Token JSONStringTokenKind
+
+public export
+Eq JSONStringTokenKind where
+  (==) JSTQuote JSTQuote = True
+  (==) JSTChar JSTChar = True
+  (==) JSTSimpleEscape JSTSimpleEscape = True
+  (==) JSTUnicodeEscape JSTUnicodeEscape = True
+  (==) _ _ = False
+
+private
+charValue : String -> Char
+charValue x = case index 0 x of
+                   Nothing => '\NUL'
+                   Just c  => c
+
+private
+simpleEscapeValue : String -> Char
+simpleEscapeValue x
+  = case index 1 x of
+         Nothing => '\NUL'
+         Just c => case c of
+                        '"'  => '"'
+                        '\\' => '\\'
+                        '/'  => '/'
+                        'b'  => '\b'
+                        'f'  => '\f'
+                        'n'  => '\n'
+                        'r'  => '\r'
+                        't'  => '\t'
+                        _    => '\NUL'
+
+private
+unicodeEscapeValue : String -> Char
+unicodeEscapeValue x = chr $ cast ("0x" ++ drop 2 x)
+
+public export
+TokenKind JSONStringTokenKind where
+  TokType JSTQuote = ()
+  TokType JSTChar = Char
+  TokType JSTSimpleEscape = Char
+  TokType JSTUnicodeEscape = Char
+
+  tokValue JSTQuote = const ()
+  tokValue JSTChar = charValue
+  tokValue JSTSimpleEscape = simpleEscapeValue
+  tokValue JSTUnicodeEscape = unicodeEscapeValue

libs/contrib/Language/JSON/Tokens.idr

@@ -0,0 +1,81 @@
+module Language.JSON.Tokens
+
+import Language.JSON.String
+import Text.Token
+
+%default total
+
+public export
+strTrue : String
+strTrue = "true"
+
+public export
+strFalse : String
+strFalse = "false"
+
+public export
+data Bracket = Open | Close
+
+public export
+Eq Bracket where
+  (==) Open Open = True
+  (==) Close Close = True
+  (==) _ _ = False
+
+public export
+data Punctuation
+  = Comma
+  | Colon
+  | Square Bracket
+  | Curly Bracket
+
+public export
+Eq Punctuation where
+  (==) Comma Comma = True
+  (==) Colon Colon = True
+  (==) (Square b1) (Square b2) = b1 == b2
+  (==) (Curly b1) (Curly b2) = b1 == b2
+  (==) _ _ = False
+
+public export
+data JSONTokenKind
+  = JTBoolean
+  | JTNumber
+  | JTString
+  | JTNull
+  | JTPunct Punctuation
+  | JTIgnore
+
+public export
+JSONToken : Type
+JSONToken = Token JSONTokenKind
+
+public export
+Eq JSONTokenKind where
+  (==) JTBoolean JTBoolean = True
+  (==) JTNumber JTNumber = True
+  (==) JTString JTString = True
+  (==) JTNull JTNull = True
+  (==) (JTPunct p1) (JTPunct p2) = p1 == p2
+  (==) _ _ = False
+
+public export
+TokenKind JSONTokenKind where
+  TokType JTBoolean = Bool
+  TokType JTNumber = Double
+  TokType JTString = Maybe String
+  TokType JTNull = ()
+  TokType (JTPunct _) = ()
+  TokType JTIgnore = ()
+
+  tokValue JTBoolean x = x == strTrue
+  tokValue JTNumber x = cast x
+  tokValue JTString x = stringValue x
+  tokValue JTNull _ = ()
+  tokValue (JTPunct _) _ = ()
+  tokValue JTIgnore _ = ()
+
+export
+ignored : JSONToken -> Bool
+ignored (Tok JTIgnore _) = True
+ignored _ = False

libs/contrib/contrib.ipkg

@@ -6,10 +6,20 @@ modules = Syntax.WithProof,
           Data.Bool.Extra,
           Data.SortedMap,
           Data.SortedSet,
+          Data.String.Extra,
           Text.Token,
           Text.Quantity,
           Control.Delayed,
           Text.Parser,
           Text.Lexer,
           Text.Parser.Core,
-          Text.Lexer.Core
+          Text.Lexer.Core,
+          Language.JSON,
+          Language.JSON.Data,
+          Language.JSON.Lexer,
+          Language.JSON.Parser,
+          Language.JSON.String,
+          Language.JSON.String.Lexer,
+          Language.JSON.String.Parser,
+          Language.JSON.String.Tokens,
+          Language.JSON.Tokens