sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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.