sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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-11-27	Split rewriter into separate rewriting library and rewrite passes	Alasdair Armstrong
	As discussed previously, we wanted to start refactoring the re-writer to make it a bit less monolithic, and in the future potentially break it into separate files for backend-specific rewrites and stuff. - rewriter.ml now contains the generic re-writing code - rewrites.ml contains the rewriting passes themselves It would be nice if the generic rewriting code didn't depend on the typechecker, because then it could be used in ASL parser on untyped code.