cakeml
cakeml copied to clipboard
Concrete syntax or s-expression basis
The basis is 230k as S-expressions but removing it from the sexpr-bootstrap compiler (unscientifically by editing the sexp file) shrinks the binary by 7197k, so replacing the current basis init code with code that parses a S-expression would save nearly 7MB in the compiler and would likely speed up bootstrap proportionally. (This assumes that string literals are stored in rodata; #773) Concrete syntax would be even smaller but may not exist for all constructs in the basis, and would likely be slower to parse.
Bump this up to medium if we don't already have all of the necessary round-trip theorems for the parser.