cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
Currently there is only one entry point in Pancake, the cml_main function. For compatibility with the sel4cp, which requires at least an init function, and possibly a notified and protected...
A mechanism for passing arguments to Pancake's main function would be a usability improvement.
Boolean literal parsing - "true" "false" - currently does not work String literal parsing
Currently the notion of shapes exist, but with only the possibility of loading them. A mechanism to access fields of a struct as well as creating and storing structs is...
Current parser error only states that there was an error in parsing, with no indication as to what caused it.
Necessary in some cases, and the current workarounds for not having access to multiplication and division are not the most elegant.
Having logical "and" and "or" for conditional statements in pancake would be a QoL improvement.
Currently the --explore flag does not output any json when the pancake flag is also present. Would be beneficial to better understand what is happening in the generated byte code.
Currently, if there are any comments placed after the final return statement, a parser error is thrown. Not the most obvious parser error to find. @mn200.
The Pancake compiler currently selects the first function in a file to be the main function, running it immediately when the program starts. It would be nice to be able...
