sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-10-12	Prevent accidental test failures when Coq compiles in the wrong order	Brian Campbell

2018-07-27	Coq: patterns on bit literals	Brian Campbell

2018-07-23	Coq test for a few non-trivial atom types	Brian Campbell

2018-07-23	Coq: make all pattern matches in the output exhaustive	Brian Campbell
	Uses previous stage to deal with (e.g.) guards. New option -dcoq_warn_nonex tells you where all of the extra default cases were added.
2018-07-07	Coq: bbv have reorganised their repository	Brian Campbell

2018-06-26	In guarded pattern rewriting, irrefutable patterns subsume wildcards	Brian Campbell
	Necessary to prevent redundant clauses that Coq will reject (There's still a problem if you use a variable rather than a wildcard, see the test)
2018-06-12	Coq: support for range type, along with related existential improvements	Brian Campbell
	Plus - Complete solver support for inequalities - Reduce exponentials in solver
2018-06-08	Coq: add destructuring of atom existentials in patterns	Brian Campbell
	Plus test case, broken builtin name
2018-06-08	Coq: ignore some currently unsupported tests	Brian Campbell

2018-06-08	Coq: skip two tests with redundant pattern matches	Brian Campbell

2018-05-28	Coq: add back tests with undefined functions	Brian Campbell

2018-05-28	Coq: add option to produce axioms for unimplemented functions	Brian Campbell
	Useful for partial test cases (e.g., some of the typechecking tests) Also a bonus warning for such functions in normal use
2018-05-24	Import (rather hacky) Coq Sail libraries	Brian Campbell

2018-05-03	Work in progress on the coq backend	Brian Campbell
	- originally based on the Lem backend - added externs to some of the library files and tests - added wildcard to extern valspecs in parser - added Type_check.get_val_spec_orig to return the valspec with the function's original names for bound type variables Note that most of the tests will fail currently