|
|
|---|
|
|
|
|---|
Fixtypes of JSON values.
A JSON value is
an object,
an array,
a number,
a string,
We model an object as a list of members, where a member consists of a name and a value. For now we use ACL2 strings for the names, which are ISO-8859-1; JSON allows Unicode here, so we may generalize this aspect of our JSON abstract syntax in the future. Despite the recommendation of avoiding members with the same name, such duplications are not strictly illegal in JSON: this is why we use a list of members, instead of an omap from names to values; this way, we can handle duplicates if they ever occur, and we also preserve information about the ordering.
We model an array as a list of values.
We model numbers as rationals, which suffices to represent the value of all JSON numbers, but it abstracts away some information from the JSON text. Thus, in the future we may change our model of numbers to preserve more information from the JSON text.
We model strings as ACL2 strings, similarly to object member names. The remarks made above, about ISO-8859-1 vs. Unicode, and therefore possible extensions of our model of strings, apply here as well.