sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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-30	Improvements to enable parsing and checking intermediate rewriting	Alasdair Armstrong
	steps Parser now has syntax for mutual recusion blocks mutual { ... fundefs ... } which is used for parsing and pretty printing DEF_internal_mutrec. It's stripped away by the initial_check, so the typechecker never sees DEF_internal_mutrec. Maybe this could change, as forcing mutual recursion to be explicit would probably be a good thing. Added record syntax to the new parser New option -dmagic_hash is similar to GHC's -XMagicHash in that it allows for identifiers to contain the special hash character, which is used to introduce new autogenerated variables in a way that doesn't clash with existing names. Option -sil compiles sail down to the intermediate language defined in sil.ott (not complete yet).
2017-09-07	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-08-30	Ocaml backend can now run ocamlbuild automatically to build ocaml	Alasdair Armstrong
	files into runable executable.
2017-07-27	Parameterise convert_ast by the bitvector order	Alasdair Armstrong

2017-07-21	Everything moved to new typechecker	Alasdair Armstrong
	Modified initial_check.ml so it no longer requires type_internal. It's still needs cleaned up in a few ways. Most of the things it's trying to do could be done nicer if we took some time to re-factor it, and some of the things should just be handled by the main typechecker, leaving it as a think layer between the parse_ast and the ast. Now that's done everything can be switched to the new typechecker and the _new suffixes were deleted from everything except the monomorphisation pass because I don't know the status of that.
2017-02-03	fix headers	Peter Sewell

2014-07-29	A file can now declare that a default order is either inc or dec, and this ↵	Kathy Gray
	will be reflected in short hand type syntax, inc is still the default if undeclared So: default order dec register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 ) default order inc register bit[32] o ( Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *) It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon.
2014-07-03	Introduce a Sail library	Gabriel Kerneis
	Used by the Power XML extraction tool.
2014-01-17	Type check through type definitions and val specifications, building ↵	Kathy Gray
	definition environment. Skipping function definition, let bind, and expression checking for this commit (to come).
2013-08-08	More forms converting from parse_ast to ast; also removed some annot aux ↵	Kathy Gray
	homs for terms that only need locations and not full annotations
2013-08-07	Starting checks and translation from parse_ast to ast, including an internal ↵	Kathy Gray
	representation of types to support unification; importing support modules from Lem including pp and util