Changes since release v3400:
List.intersperse,
which inserts a given element between every consecutive pair of elements in a list,
has been added to basis.
isLower, isUpper, isDigit, isAlpha and isAlphaNum have been added to the Char module.
String.concatWith has been reimplemented using concat and intersperse,
avoiding potentially quadratic behavior due to left-associative concatenations (#1425).
TextIO.output's behavior is now linear in the size of the string
(previously quadratic -- oops!). This should allow users to output large strings
(as in: much larger than 2kB) without the program hanging (#1425).
BVI now supports multi-arg calls/returns (with a separate constructor).
The parser now supports multi-line string literals.
The CakePB example now has a verified CP encoder frontend.
The basis_ffiLib.whole_prog_thm, which is used to prove semantics
results, has been deleted and a new basis_ffiLib.prove_sem_thm is to
be used instead from now on. The old one used to be slow and clunky to
use; the new one runs within a few seconds at each call site.
The following simps have been added:
Theorem get_mode_fsupdate[simp]:
get_mode (fsupdate fs fd' k pos content) fd = get_mode fs fd
CONCAT_WITH (misc) and concatWith_CONCAT_WITH (mlstring)
have been removed due to being unused.
inferScript.sml now uses the state-exception monad defined in ml_monadBase instead of a locally defined version of it.
Some files have been refactored to use monadsyntax.temp_enable_monad
instead of manual overloads of constants such as monad_bind.
Some files have been refactored to use st_ex_ignore_bind instead of
a locally defined version using st_ex_bind.