sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-12-01	Coq: remove last use and definition of doc_nc_prop	Brian Campbell
	(plus test, as it wasn't covered before)
2019-10-02	Coq: limited support for existentially-typed tuples	Brian Campbell
	- in particular at monadic interfaces (i.e., sufficient for instruction ast types) - see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an example that's not currently supported - generate definitions for type-level Bool definitions (i.e., predicates)
2019-09-02	Enable part of a test that's been fixed recently.	Brian Campbell

2019-08-30	Add a couple of overlooked tests	Brian Campbell

2019-06-21	Coq: add missing property derivation casts for effectful expressions	Brian Campbell
	These don't appear much, but are now showing up in the sail-arm model due to an innocent change elsewhere.
2019-06-21	Coq: be more careful when dealing with wildcard argument patterns	Brian Campbell
	If they're merged with a type variable then we still need to name the argument so that it can be used in other types.
2019-06-03	Test case for previous commit	Brian Campbell

2019-05-24	Coq: support if-then-throw typechecking special case	Brian Campbell

2019-05-21	Coq: introduce autocasts at variables	Brian Campbell
	Usually we do this at function applications and casts, but occasionally a variable is used at a different type.
2019-04-17	Coq: support pure loops with termination measures	Brian Campbell

2019-04-15	Basic loop termination measures for Coq	Brian Campbell
	Currently only supports pure termination measures for loops with effects. The user syntax uses separate termination measure declarations, as in the previous recursive termination measures, which are rewritten into the loop AST nodes before type checking (because it would be rather difficult to calculate the correct environment to type check the separate declaration in).
2019-04-05	Coq: add missing effectful existential unpacking case	Brian Campbell

2019-04-02	Coq: replace n_constraints with equivalent bool variables	Brian Campbell
	Prevents some type variables that came from unpacking existentials leaking into generated Coq types.
2019-03-20	Coq: be more careful about merging Sail variables and type variables	Brian Campbell
	In particular, spot variable shadowing and handle (n as 'm) patterns.
2019-03-15	Add coq test case for for-loop type variable	Brian Campbell

2018-12-27	Coq: avoid putting ambiguous numeric literals in Coq output	Brian Campbell
	There are situations when we really want a more refined expression, such as 8 * n instead of 64 (when we know n = 8 from a case split), but we might not be able to generate it. For now we generate an underscore and let Coq figure it out from the context.
2018-12-27	Coq: fix name clashes and instantiation calculation	Brian Campbell

2018-12-19	Coq: handle pairs of ranges (and other existential types) properly	Brian Campbell
	(Needed for current CHERI.)
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-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