Lasse Letager Hansen
Lasse Letager Hansen
I have made a compiler stack to code Piet solutions easier. So this "high level language" is a simple language with function calls, local and global variables, and a simple...
@MarkusKL @spitters These statements should hopefully enable simpler proof structure and thus better automation. We seem to be missing some weakening statement, as `ValidPackage` now requires the export interface to...
WIP for #962
This should now be a stable version of the Coq generic printer. There is still some naming issues, which I have fixed directly in Concrete ident and the generic printer....
I could not figure out how to get the sourcemap, however, if possible we should also return the sourcemap.
Alternative to #975
I am currently generating the AST as EBNF, thus we can use tools like https://rr.red-dove.com/ui to render a diagram of the AST.
This should be mostly ready for review. Only missing description for some cases.
Print EBNF formula as a command (not sure the setup is correct). Currently a full generic printer is implemented for this, however, we might be able to instrument e.g. a...
@franziskuskiefer @spitters here is the WIP projects and unmerged branches I could find by looking through github. Please let me know if you want something in addition to this, or...