sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-03-13	Polymorphic option types now compile to C	Alasdair Armstrong
	Fixed an issue whereby an option constructor that was never constructed, but only matched on, would cause compilation to fail. Temporarily fixed an issue where union types that can be entirely stack-allocated were not being treated as such, by simply heap-allocating all unions. Need to adapt the code generator to handle this case properly. Fixed a further small issue whereby multiple union types would confuse the type specialisation pass. Added a test case for compiling option types. RISCV now generates C code, but there are still some bugs that need to be squashed before it compile and work.
2018-03-09	Specialise constructors for polymorphic unions	Alasdair Armstrong
	Also work on making C backend compile RISC-V
2018-03-05	Fix specialisation pass to handle polymorphic substitutions	Alasdair Armstrong
	Can now handle when an instantiation introduces more polymorphism. We can now deal with the case where, for example, a type variable gets specialised in two two steps, e.g. 'a => list('a) => list(int). Also handle the case where a Type-kinded type variable gets substituted with an Int-polymorphic type, e.g. 'a => atom('n). This also fixes an issue where specialisation would loop due to generated type variable names. This was fixed by ensuring that when we convert an instantiation to a string to name the newly specialised definition, we ensure that any alpha-equivalent instantiations map to the same name.
2018-02-19	Have generic vectors working in C backend	Alasdair Armstrong

2018-02-15	List support in C backend	Alasdair Armstrong

2018-02-07	Have exceptions working in C backend	Alasdair Armstrong

2018-01-23	Started working on C backend for sail	Alasdair Armstrong
	Also updated some of the documentation in the sail source code
2018-01-22	Added rewriter that specializes all function calls in a specification.	Alasdair Armstrong
	This removes all type polymorphism, so we can generate optimized bitvector code and compile to languages without parametric polymorphism.
2018-01-18	Modified unification so Type_check.instantiation_of works after sizeof rewriting	Alasdair Armstrong
	This change allows the AST to be type-checked after sizeof re-writing. It modifies the unification algorithm to better support checking multiplication in constraints, by using division and modulus SMT operators if they are defined. Also made sure the typechecker doesn't re-introduce E_constraint nodes, otherwise re-checking after sizeof-rewriting will re-introduce constraint nodes.