sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-04-18	Add some lemmas about bitvectors	Thomas Bauereiss
	Also clean up some library functions a bit, and add some missing failure handling variants of division operations on bitvectors.
2018-03-22	Tune Lem pretty-printing	Thomas Bauereiss
	In particular, improve indentation of if-expressions, and provide infix syntax for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
2018-03-14	Make partiality more explicit in library functions of Lem shallow embedding	Thomas Bauereiss
	Some functions are partial, e.g. converting a bitvector to an integer, which might fail for the bit list representation due to undefined bits. Undefined cases can be handled in different ways: - call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the default so far), - return an option type, - raise a failure in the monad, or - use a bitstream oracle to resolve undefined bits. This patch adds different versions of partial functions corresponding to those options. The desired behaviour can be selected by choosing a binding in the Sail prelude. The naming scheme is that the failwith version is the default, while the other versions have the suffixes _maybe, _fail, and _oracle, respectively.
2018-02-26	Rename some Isabelle theories	Thomas Bauereiss
	The suffix _lemmas is more descriptive than _extras.