ion and json

ion is a json superset

Given

<json:object> ::= '{' (<json:pair>)? (',' <json:pair>)* '}'
<json:array> ::= '[' <json:value>? (',' <json:value>)* ']'
<json:value> ::=
   | <json:object>
   | <json:array>
   | <json:str>
   | <json:num>
   | 'null'
   | 'true' | 'false'

prove that json is a subset of ion:

<json:array>
   \equals '[' <json:value>? (',' <json:value>)* ']'         (* TODO: <nl> *)
   \subset '[' <item>? (<sep> <item>)* ']'
   \subset '[' <chain>? (<sep> <chain>)* ']'
   \subset '[' <anno>? (<sep> <anno>?)* ']'
   \subset '[' <pair>? (<sep> <pair>?)* ']'
   \equals '[' <seq> ']'
   \subset <item>

<json:pair>
   \equals <json:str> ':' <json:value>
   \subset <item> ':' '<item>'
   \subset <chain> ':' <chain>
   \subset <anno>

<json:object>
   \equals '{' <json:pair>? (',' <json:pair>)* '}'
   \subset '{' <anno>? (',' <anno>)* '}'
   \subset '{' <pair>? (',' <pair>)* '}'
   \equals '{' <seq> '}'
   \equals <map>

<json:value>
   \cases
   | ('true'|'false'|'null')     \subset <sym>
   | <json:num>                  \equals <num>
   | <json:str>                  \equals <str>
   | <json:array>                \subset <list>
   | <json:object>               \subset <map>
   \subset <item>

mapping into json

<seq>   <=> [<json:pair>]

<pair>  <=> <json:chain>   // if no $key and no $meta
        <=> {
                "=": <json:chain>,
                "$key": <json:typed>,       // optional
                "$meta": <json:item>,       // optional
            }

<typed> <=> <json:chain>   // if no types
        <=> {
                ":": <json:chain>,
                "$type": <json:typed>,
            }

<chain> <=> <json:item>     // if one item
        <=> {
                " ": [<json:item>]     // non-empty
                "$bind": <json:item>   // optional
            }

<item>  <=> <json:str>
        <=> <json:num>
        <=> <json:sym>
        <=> <json:dot>
        <=> <json:tuple>
        <=> <json:list>
        <=> <json:map>

<map>   <=> {"{}": <json:seq>}

<list>  <=> {"[]": <json:seq>}

<tuple> <=> {"()": <json:seq>}

<dot>   <=> { ".": <json:item> }

<sym>   <=> ".<sym>"

<str>   <=> <str>   // if starts with a dot, must be \.

Examples:

[
// "hello"
"hello"

// hello
".hello"

// ".hello"
"\.hello"

// [1, 2, 3]
{"[]": [1, 2, 3]}

// (a)
{"()": [".a"]}

// {numbers, one=1, two=2}
{"{}": [
  {"=": ".numbers"},
  {"$key": ".one", "=": 1},
  {"$key": ".two", "=": 2},
]}

// x = 42
{"=": 42, "$key": ".x"}}

// f x y
{" ": [".f", ".x", ".y"]}

// f x : Nat .to Nat
{
  ":": {" ", [".f", ".x"]},
  "$ty": {" ", ["Nat", {".": "to"}, "Nat"]}
}

// inc (x: Nat) = x .add 1
{
  "=": {" ": [".x", {".": ".add"}, 1]},
  "$key": {
    " ": [
      ".inc",
      {"()": [
        {":": ".x", "$ty": ".Nat"}
      ]}
    ]
  }
}

// x => x .add 1
{
  " ": [".x", {".": ".add"}, 1],
  "$bind": ".x"
}

// #nat one = 1
{
    "=": 1,
    "$key": ".one",
    "$meta": ".nat"
}

]

mapping to S-exprs

; "hello"
"hello"

; hello
'hello

; .hello
''hello

; x = 42
'(:key x 42)

;; sequences map to lists:
; 1, 2, 3
'(1 2 3)

; [1, 2, 3]:
'(:list 1 2 3)

; (1)
'(:tuple 1)

; ()
'(:tuple)

; f x y
'(:chain f x y)

; f x : Nat .to Nat
'(:type (:app Nat .to Nat)
  :app f x))

; inc (x: Nat) = x .add 1
'(:key (:chain inc (:type Nat x))
  :chain x .add 1)

; x => x .add 1
'(:bind x
  :chain x .add 1)

; #nat one = 1
'(:meta nat
  :key one
  1)