Summary:
We use a modest set of annotations in ast.dart to describe how the Kernel AST
should be converted into Coq definitions.
We define a Kernel transformation that converts the kernel tree of ast.dart into
a valid Coq file containing the corresponding definitions.
Currently generating the Coq file is not done in the build system because
compiling it requires having Coq installed, and I don't want to introduce a
depedency on Coq into the build system.
Some parts of the AST are not represented because they don't significantly
contribute to the typing semantics:
- asserts
- typedefs
- most literals/basic types (excl. bool, which is needed for "is" tests)
- switch
- for-in
- parts
- yield/await
Test Plan:
Ran the output KernelSyntax.v file through "coqc".
Change-Id: Ic573163a017eaaf3759b741b9eec5ce3ce19225c
Reviewed-on: https://dart-review.googlesource.com/2960
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
Commit-Queue: Dmitry Stefantsov <dmitryas@google.com>
Samir Jindel