HigherOrderCO / monobook

AGDA
22 stars 5 forks source link

29 json support #33

Closed Lorenzobattistela closed 1 week ago

Lorenzobattistela commented 1 week ago

Implements #29 .

Implements a simple JSON parser. It correctly compiles to haskell through agda-compile command.

The javascript compilation kinda works, but faces the same bind problem that is being investigated. (the js compilation is not a problem since we can just use JSON.parse and JSON.stringify). Example:

module Data.JSON.Main where

open import Data.String.Type
open import Data.String.show
open import Data.String.append
open import Data.JSON.Type
open import Data.JSON.parse
open import Data.Parser.State
open import Data.Parser.Error
open import Data.Parser.Reply
open import Data.Result.Type
open import Data.IO.print
open import Data.IO.Type
open import Data.IO.bind
open import Data.IO.seq
open import Data.Unit.Type
open import Data.Function.case
open import Data.JSON.show renaming (show to show-json)

main : IO Unit
main = do
  let json-string = "[1, true, null, [\"nested\", [2.5]], {\"key\": \"value\"}]"
  print ("Parsing JSON string: " ++ show json-string) 
  case parse-json-string json-string of λ where
    (Done reply) → do
      print "Parsing successful!"
      print ("Parsed JSON: " ++ show-json (Reply.value reply))
    (Fail error) → do
      print "Parsing failed!"

This compiles correctly to Haskell and parses the JSON.

NOTE: the order of list elements is not preserved.