|
|
|---|
|
|
|
|---|
Simple encoder to convert ACL2 Objects into JSON Objects.
Sensibly converting ACL2 objects into JSON is not at all straightforward.
On one hand, JSON is very rich. Should we try to map association lists into JSON objects, or should we just treat all cons trees the same and use arrays? Since JSON has distinct NULL and FALSE values, which should we map NIL into?
On the other, JSON is missing some types that we would like. Should we just map ACL2 symbols and strings into strings, and lose the distinction between them? What on earth should we do with rationals and complex numbers? Should we assume that the JSON consumer supports bignums, or use a separate bignum encoding?
Arguably, the "safe" approach would be: develop a reliable JSON encoding that ensures a unique interpretation of each ACL2 object. For instance, we should keep symbols and strings separate, record the name/package of each symbol separately, etc.
But that would suck. The resulting JSON objects would be full of unwieldy type information, which most of the time we wouldn't care about. Usually, we are hooking up ACL2 to web pages or other interfaces that want to get some simple, small fragments of data. In this context, I'd prefer a simple representation that is easy to work with, even at the cost of losing some precision.
I encode every ACL2 atom as a JSON string. For example:
Lisp Atom JSON --------------------------------------- NIL "NIL" T "T" FOO "FOO" :FOO ":FOO" "foo" "foo" #\f "f" 123 "123" -123 "-123" -1/2 "-1/2" #c(17/2 -3/8) "#C(17/2 -3/8)" ---------------------------------------
This has many quirks. The main weirdness is that there are many ACL2 objects which, although they are not EQUAL, cannot be told apart from one another in the JSON world. For instance, the atoms on each line below have identical JSON encodings:
Some motivation behind this approach:
With one exception (see below), I encode any true-lists as a JSON arrays containing its encoded elements, and I encode any "improper" list as a JSON array containing its encoded elements AND its final cdr. For example:
Lisp Object JSON ------------------------------------------------------------- (a . nil) ["A"] (a . b) ["A","B"] (a b . nil) ["A","B"] (a b . c) ["A","B","C"] (a b c . nil) ["A","B","C"] ((a . b) (c . d) . e) [["A","B"],["C","D"],"E"]
This has its own quirks. For instance, as with atoms, you can't tell the difference between Lisp objects like: (A B C) and (A B . C).
The exception is that, for proper ALISTS whose every key is an atom, I instead generate the corresponding JSON Object. For example:
Lisp Object JSON
-------------------------------------------------------------
((a . b)) {"A":"B"}
((a . b) (c . d)) {"A":"B","C":"D"}
((a . b) (c . d) . e) [["A","B"],["C","D"],"E"]
In certain cases, this runs the risk that you might see a different encoding for an alist, depending on whether or not you have inserted a cons. But many alists have atoms as keys, and it seems nice to use a real JSON object here instead of a nested array of arrays.
Earlier versions of the JSON grammar required top-level
We found this to be useful in our client code. It's nice to create a JSON object that says: the return value is such and so, the standard output was such and so, and the error value was such and so. In this context, we just want to stitch our ACL2 object into a larger piece of JSON text, and strings are okay.