Json2ast
Build Leo abstract syntax trees from Leo AST JSON files.
Leo abstract syntax trees are represented in many forms. Here we discuss
the steps in which they are translated from JSON files to ACL2 fixtypes.
We usually omit the term "Leo abstract syntax trees" for brevity.
Currently we call jsonfile-to-formal as the entry point.
It calls jsonfile-to-spanfree, which handles the first few steps,
followed by j2f-file, which handles the last step.
A JSON file is parsed into an ACL2 JSON list structure using
acl2::parse-file-as-json. All further processing is done in ACL2,
so we will omit that term.
Then the JSON list structure is translated to a
JSON abstract syntax structure using json::parsed-to-value.
By a JSON abstract syntax structure we mean
a value of type json::value that
represents the JSON that was seen in the file. At this point ACL2 does not
know anything about the meaning of this value as a Leo program.
Operating on the JSON abstract syntax, we remove span objects using
json-remove-spans-in-value.
For more details see json-fixtype-span-removal.
Finally, the spanfree JSON abstract syntax is translated to
Leo abstract syntax
using j2f-file.
The result is a Leo abstract syntax tree represented as an ACL2 value
of type file.
Subtopics
- Json2ast-mutual-recursion-expressions
- Converts a Leo expression from JSON AST to fixtype AST.
- Json-fixtype-span-removal
- Removes spans recursively in a parsed JSON fixtype.
- Json2ast-mutual-recursion-statements
- Converts a Leo statement from JSON AST to fixtype AST.
- Json-value-is-span-object-p
- Checks if this json value looks like either a span object or a wrapped span object.
- Json-value-is-core-span-object-p
- Checks if this json value looks like a span object.
- Json2ast-mutual-recursion-types
- Convert Leo types from JSON to formal AST.
- J2f-struct-declaration
- Converts a single member of the structs of a file to a leo::topdecl-struct.
- J2f-console-statement
- Converts a json-member console statement to a leo::statement of kind :console
- Jsonast-looks-like-function-definition-p
- Checks if THING is a JSON AST function definition object member.
- J2f-function-definition
- Converts a single member of the functions of a file to a leo::definition.
- J2f-assign-statement
- Converts a json-member Assign statement to a leo::statement of kind :assign
- Json-member-is-span-p
- Checks if this json object member looks like a span.
- J2f-struct-declarations
- Converts list of members, all of which are supposed to be struct declarations,
to a list of leo::topdecl.
- J2f-let-or-const-statement
- Converts a json-member let statement to a leo::statmement of kind :let.
- J2f-console-error
- Converts a json-member console error statement to a leo::statement of kind :console
- J2f-struct-members
- Converts a list of json struct members to a leo::compdecl-list.
- J2f-return-statement
- Converts a json-member return statement to a leo::statement of kind :return.
- J2f-function-definitions
- Converts list of json-members, all of which are supposed to be functions, to a list of leo::definitions.
- J2f-console-log
- Converts a json-member console log statement to a leo::statement of kind :console
- J2f-console-assert
- Converts a json-member console assert statement to a leo::statement of kind :console
- Jsonast-looks-like-struct-declaration-p
- Checks if THING is a JSON AST outer struct declaration object member, including the duplicate name.
- J2f-funinputs
- Converts a list of json fn input parameters to a leo::funinput-list.
- J2f-if-statement-tail
- Converts a JSON if statement's 'otherwise' object into a
leo::branch-list and a final else leo::statement-list.
- Jsonast-looks-like-file-p
- Checks if THING is a JSON AST file object.
- J2f-iteration-statement
- Converts a json-member Iteration statement to a leo::statement of kind :for
- J2f-if-statement
- Converts a JSON if statement into a leo::statement of kind :if.
- J2f-block-statement
- Converts a JSON block statement into a leo::statement of kind :block.
- J2f-statements
- Converts a list of json-statement to a leo::statement-list.
- J2f-statement
- Converts a json-statement to a leo::statement.
- J2f-type
- Converts a json-type into a leo::type.
