		Search-engine friendly clone of the ACL2 documentation.

Json

Parser-output-to-abstract-syntax

A translator from the JSON parser's output to the JSON abstract syntax.

The JSON parser in kestrel/json-parser/ produces output (parsed and abstracted JSON) in a form that is slightly different from the JSON abstract syntax formalized in this JSON library; in particular, the parser's output is not a fixtype.

Thus, here we provide a translator from the parser's output to the JSON abstract syntax. Since at the time that this translator was first written the parser did not include a type (i.e. recognizer) for its output, the translator is defined over all possible ACL2 values, but it returns an error if given something that does not belong to the parser's implicit output type. After that, recognizers have been added in kestrel/json-parser/, so we plan to improve this translator to take them into account.

Subtopics

Parsed-to-value: Translate the JSON values generated by the parser to the corresponding fixtype JSON values.
Value-irrelevant: An irrelevant JSON value.
Member-irrelevant: An irrelevant JSON member.