| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.
This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.
I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
|
|
|
|
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
|
|
|
|
|
|
Conflicts:
src/pretty_print_common.ml
|
|
|
|
|
|
|
|
Also fixed substitution functions so as to not substitute captured kind identifiers
|
|
Fixed some bugs in the initial check that caused valid code to fail to
parse
Add a nid utility function that creates an id n-expression, similar to
nvar, nconstant etc
|
|
Commented out some buggy re-sugaring logic from pretty_print_common
where it re-sugared vectors incorrectly
Fixed a bug where the type checker forgot to preserve type signatures
in top-level letbinds
|
|
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
|
|
|
|
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
|
|
searching easier.
|
