Oskar Abrahamsson

Definition/store_thm/etc to collect position metadata from location pragmas

1

This would allow editor modes (and humans) to find this information about theorems and constants using e.g. DB.find or the upcoming Defnbase functionality.

BNFC should reject 'bad' filenames names instead of silently sanitizing them

4

BNFC generates various names (files, directories, classes, ...) based on the filename of the input grammar (e.g. `Lang.cf`). Not all backends will be able to deal with all legal choices...

The following operations would be useful additions to the Word{8,64} modules: - `val * : word -> word -> word` - `val / : word -> word -> word` -...

Add more functionality to floating point number type

5

Currently, the only way to create floating point numbers is to parse them from string. Pretty much the only useful things I can do with these floating point numbers is...

This issue will track the progress of adding `open` and `let open` forms to the CakeML syntax and semantics. It is _almolst_ possible to emulate the functionality of `open` using...

This issue proposes adding the following forms to the CakeML syntax and semantics: - Structure abbreviations: `structure S = SuperLongStructName` - Exception abbreviations: `exception E = AnotherException`

The translator should not accept types where mangled constructor names would clash

2

The translator mangles the names of functions and type constructors to fit with the CakeML grammar. This mangling can produce non-distinct constructor names, which makes the translator fail. This issue...

Using compilationLib with custom configs doesn't work because the library is hard-coded to use only the standard configs, see here: https://github.com/CakeML/cakeml/blob/master/compiler/compilationLib.sml#L165-L184. Here are some things that might differ between configs:...

The translator accepts constants with preconditions, and duplicates preconditions: ```sml > val foo_def = Define` foo = 5 DIV 0`; Definition has been stored under "foo_def" val foo_def = []...

The lexer does not accept numerical escape sequences inside string or character literals, e.g.: `#"\100"` or `"\100"` should be turned into `#"d"` and `"d"` respectively. The relevant code is [here](https://github.com/CakeML/cakeml/blob/master/semantics/lexer_funScript.sml#L78-L83).