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)