sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-01-12	OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.	Alasdair Armstrong

2018-01-05	Moved parser, lexer and pretty printer to correct locations.	Alasdair Armstrong

2018-01-05	Added bitfield syntax to replicate register bits type	Alasdair Armstrong
	For example: bitfield cr : vector(8, dec, bit) = { CR0 : 7 .. 4, LT : 7, CR1 : 3 .. 2, CR2 : 1, CR3 : 0, } The difference this creates a newtype wrapper around the vector type, then generates getters and setters for all the fields once, rather than having to handle this construct separately in every backend.
2018-01-02	Experimenting with power spec	Alasdair Armstrong

2017-12-14	Fix all compiler warning except in lem pretty printer and monomorphisation	Alasdair Armstrong

2017-12-13	Use big_nums from Lem	Alasdair Armstrong

2017-12-06	Add top-level pattern match guards internally	Brian Campbell
	Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next.
2017-12-06	Merge remote branch 'experiments' into experiments	Thomas Bauereiss

2017-12-06	Make AST after rewriting for Lem backend type-checkable	Thomas Bauereiss
	- Add support for some internal nodes to type checker - Add more explicit type annotations during rewriting - Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer; these will be resolved by the type checker during rewriting now
2017-12-05	Update license headers for Sail source	Alasdair Armstrong

2017-11-16	Remove unused Typ_wild constructor	Alasdair Armstrong

2017-10-31	Fix bug in topological sorting of val-specs	Thomas Bauereiss
	Put them before the function they declare
2017-10-25	Allow mutually recursive functions	Thomas Bauereiss

2017-10-24	Remove special case for boolean (as opposed to bool)	Brian Campbell

2017-10-19	Follow AST changes in (Lem) pretty-printers	Thomas Bauereiss

2017-09-21	Refactored AST valspecs into single constructor	Alasdair Armstrong

2017-09-21	Remove unused kind_def (KD_) nodes from AST	Alasdair Armstrong

2017-09-21	Simplify AST by removing LB_val_explicit and replace LB_val_implicit with ↵	Alasdair Armstrong
	just LB_val in AST also rename functions in rewriter.ml appropriately.
2017-09-21	Cleaning up the AST and removing redundant and/or unused nodes	Alasdair Armstrong

2017-09-14	Fix bug in topological sorting	Thomas Bauereiss

2017-08-14	Existentials in free type var functions	Brian Campbell

2017-08-01	Modified the typechecker for ASL generation	Alasdair Armstrong

2017-07-27	Add cons patterns to pretty-printers	Thomas Bauereiss

2017-07-21	Switch to new typechecker (almost)	Thomas Bauereiss
	Initial typecheck still uses previous typechecker
2017-02-03	fix headers	Peter Sewell

2016-10-13	make sail-to-lem rewriting passes use dependency analysis, make dependency ↵	Christopher Pulte
	analysis include type information, small pp fix
2016-10-12	Add free variable and dependency sorting functions, lifted from internal to ↵	Kathy Gray
	external repository
2016-01-21	Start splitting values/etc into int/big_int for ocaml generation	Kathy Gray

2016-01-19	Put None and Some into interpreter environments	Kathy Gray
	Also making progress towards separating int sized things from integer sized things
2015-11-10	Make first half of sequential interpreter driver compile again	Kathy Gray

2015-11-06	fixes	Christopher Pulte

2015-11-04	Add a new module for writing queries/analyses that aren't type checking but ↵	Kathy Gray
	could be useful Define in that a function for determining a default direction for vectors