sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-08-11	Make type checking just clever enough to solve 8*n = constant	Brian Campbell

2017-08-10	Disable menhir on this branch	Brian Campbell
	(until location information is updated)
2017-08-10	Merge branch 'experiments' into mono-experiments	Brian Campbell

2017-08-10	Existentials in Lem AST output	Brian Campbell

2017-08-10	Experimental removal of existentials	Brian Campbell

2017-08-10	Improved existentials and type synonyms	Alasdair Armstrong

2017-08-08	Add infrastructure to play with new menhir parsers.	Alasdair Armstrong
	Added a copy of the current parser/lexer in parser2.mly and lexer2.mll. They can be used with the -new_parser flag. Currently they are just copies of the existing files.
2017-08-08	Switch to using menhir for sail parser in experiments branch	Alasdair Armstrong

2017-08-07	Improvements to existentials for ASL parser	Alasdair Armstrong

2017-08-04	Various improvements for ASL generation	Alasdair Armstrong
	Fixed a bug where existential constraint's weren't used to solve function quantifiers correctly
2017-08-02	Changed some aspects of the typechecker to better support ASL l-values	Alasdair Armstrong

2017-08-02	Merge remote-tracking branch 'origin/sail_new_tc' into experiments	Alasdair Armstrong

2017-08-02	Modified loop typechecking code to generate a new type variable for the loop ↵	Alasdair Armstrong
	index, seems to work better for complex cases in ASL
2017-08-01	Add missing lexp case to Ocaml pretty-printer	Thomas Bauereiss

2017-08-01	Fixed a bug where type_synonyms were not being expanded properly when ↵	Alasdair Armstrong
	considering possible casts
2017-08-01	Fixed a bug where as patterns weren't binding their variable correctly	Alasdair Armstrong

2017-08-01	Added more patterns to ast_util and improved type checking of patterns	Alasdair Armstrong

2017-08-01	Merge remote-tracking branch 'origin/sail_new_tc' into experiments	Alasdair Armstrong

2017-08-01	Added more patterns to ast_util and improved type checking of patterns	Alasdair Armstrong

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

2017-08-01	Remove some hardcoded calls to obsolete Lem library functions	Thomas Bauereiss

2017-08-01	Fix some effect propagation bugs in rewriter	Thomas Bauereiss

2017-07-31	Fixed a bug in the pretty printer that caused ASL parser to output ↵	Alasdair Armstrong
	unparseable sail code
2017-07-31	Changed behavior of return to better match ASL	Alasdair Armstrong

2017-07-31	Removed redundant code in infer_funapp'	Alasdair Armstrong

2017-07-31	Fixed bug in existential return types	Alasdair Armstrong

2017-07-28	Mips TLB existential example	Alasdair Armstrong

2017-07-28	Fix break caused by merge	Alasdair Armstrong

2017-07-28	Merge remote-tracking branch 'origin/sail_new_tc' into experiments	Alasdair Armstrong

2017-07-28	Add true and false to n_constraint language. Also small tweaks for ASL ↵	Alasdair Armstrong
	generation.
2017-07-27	Rewrite guarded patterns for Lem backend	Thomas Bauereiss

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

2017-07-27	Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	sail_new_tc
2017-07-27	Parameterise convert_ast by the bitvector order	Alasdair Armstrong

2017-07-27	Fixed a bug where sail would run out of file descriptors when passed a large ↵	Alasdair Armstrong
	number of files
2017-07-27	P_cons in monomorphisation	Brian Campbell

2017-07-27	Fix up constructor handling in monomorphisation	Brian Campbell

2017-07-27	Mirror AST change	Brian Campbell

2017-07-27	Allow local mutable records, and fix bugs with overlapping record field names.	Alasdair Armstrong

2017-07-27	Merge remote-tracking branch 'origin/sail_new_tc' into experiments	Alasdair Armstrong

2017-07-27	Fixed bug with pattern synonyms in Cons and List patterns	Alasdair Armstrong

2017-07-27	Fixed some bugs with existentials, and added test cases	Alasdair Armstrong

2017-07-27	Fixed pretty printer for existentials	Alasdair Armstrong
	Also fixed substitution functions so as to not substitute captured kind identifiers
2017-07-26	More work on existentials in function calls	Alasdair Armstrong

2017-07-26	Experimental existentials in function calls	Alasdair Armstrong

2017-07-26	Experiment in adding existential types	Alasdair Armstrong

2017-07-26	Added syntax for existential types	Alasdair Armstrong

2017-07-26	Add right shift to lib/prelude.sail, and add case for E_exit in ↵	Alasdair Armstrong
	Ast_util.string_of_exp
2017-07-26	Allow arbitrary identifiers in nexp expressions	Alasdair Armstrong
	Fixed some bugs in the initial check that caused valid code to fail to parse Add a nid utility function that creates an id n-expression, similar to nvar, nconstant etc
2017-07-26	Merge remote-tracking branch 'origin/master' into sail_new_tc	Alasdair Armstrong