sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-04-08	Reduce redundant information in AST	Kathy Gray

2014-04-02	Solve more constraints; fix up test suite bugs uncovered by solving more ↵	Kathy Gray
	constraints. Clean up Lem output a little for readability while debugging.
2014-04-01	Allow negative "nat" internally	Gabriel Kerneis
	to_num and to_vec probably still need to be fixed
2014-03-27	Check simple constraints (i.e. ones using only constants).	Kathy Gray
	Changes syntax of tuple type from * to , so that nexps of the form 8 * 'n can be supported in the parser, which was apparently not true before.
2014-03-26	More steps towards solving and using constraint information	Kathy Gray

2014-03-11	Change treatment of type abbreviations so that name and full type are ↵	Kathy Gray
	available for field lookups of registers; this feature still not fully working.
2014-03-03	Fixing assorted bugs. Adding ability to put a type on the identifier being ↵	Kathy Gray
	assigned to in assignments.
2014-02-28	Correct bug in parsing and handling a['a:'b] types	Kathy Gray

2014-02-21	Add type annotations to lem grammar, including printing out the annotated ↵	Kathy Gray
	ast, and extending the interpreter to expect annotations. Annotations and locations are still not used by the interpreter.
2014-02-18	Add function's name for external tag, using register when a register	Kathy Gray

2014-02-18	Adding explicit order to for loops	Kathy Gray

2014-02-14	update syntax of vector slicing.	Kathy Gray

2014-02-12	Change nat to natural in ott	Kathy Gray
	Type checking now recurses through assign, but doesn’t do the proper checks yet
2014-01-07	lem homs and type headers	Kathy Gray

2013-12-18	More lem homs	Kathy Gray

2013-12-18	Tweak formatting in pretty printer, and resolve bugs.	Kathy Gray
	Start specifying lem homs for rules.
2013-12-17	Convert coerce to a relation that generates a new expression, inserting ↵	Kathy Gray
	coercion function calls where applicable.
2013-12-16	fix l2_rules to grammar update	Kathy Gray

2013-12-10	Fixed bug in interpreter	Kathy Gray

2013-12-03	Syntax changes per discussion with Peter, as well as L2.ott document clean up.	Kathy Gray
	Could not at this time return lists to [\| \|] from [\|\| \|\|] as the parser cannot distinguish a cast with enum’s syntactic sugar from the start of a parenthesised list (i.e. ( [\|3\|] ) And there are still conflicts with moving enums to [3], so those changes can’t be pushed in with current parser technology.
2013-11-29	Push syntax changes to type rules	Kathy Gray

2013-11-28	Updated syntax with working examples	Kathy Gray

2013-11-22	Syntax changes per discussions on Thursday.	Kathy Gray
	First pass parser to identify type names is in progress (current test files fail, will correct once pre-parser is in place)
2013-11-11	Merge branch 'new-lem-lib'	Gabriel Kerneis

2013-11-09	Fix up multiple parses issue	Kathy Gray

2013-11-08	Type system, almost certainly has omissions or flaws I've forgotten, but ↵	Kathy Gray
	seems to be complete. Will update with corrections as necessary during implementation phase.
2013-11-07	Port L2 to new Lem	Gabriel Kerneis
	Tests compile and run properly. There is a lot of hackery going on to workaround the rough edges of new Lem. Use at your own risk (you need the "library-format" branch of lem).
2013-11-07	Most of the function type system	Kathy Gray

2013-11-01	Moved metatheory grammars into l2_rules.ott	Kathy Gray
	Added val extern specification to language, parser, printer, and interpreter Added various def level type system support, expressions type system in place Except for assignment
2013-10-30	Type coercions and let expressions	Kathy Gray

2013-10-25	More type rules	Kathy Gray

2013-10-23	Thread type environment through expressions because of block adding new ↵	Kathy Gray
	variables, say in each branch of an if, that we want to be visible beyond it.
2013-10-23	Don't export list of types to ML AST	Gabriel Kerneis

2013-10-22	More type system	Kathy Gray

2013-10-18	Typeing rules for patterns and easy expressions	Kathy Gray

2013-10-11	Supporting all expressions, although vector cacentation pattern matching can ↵	Kathy Gray
	only match simple patterns (until type information is available).
2013-10-09	Adding memory writes. Cleaning up the let in the ott file to reflect what ↵	Kathy Gray
	actually parses
2013-10-09	extend language of lexp to include memory writes	Kathy Gray

2013-10-04	Clean up build system	Gabriel Kerneis

2013-09-26	Adding undefined	Kathy Gray
	Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)
2013-09-09	Fixes bugs in pretty printer to generate legal lem syntax; split ott grammar ↵	Kathy Gray
	and rules for lem ast generation; created a new directory for the lem interpreter and moved the Lem ast to it.
2013-09-09	Pretty printer to Lem ast added; accessed by -lem_ast on the command line	Kathy Gray

2013-09-05	workaround likely aux rule bug	Peter Sewell

2013-09-05	More type checking, and trying to generate Lem from the ott	Kathy Gray

2013-09-04	Kind checking and part of type checking getting started	Kathy Gray

2013-09-02	Fix enumerate syntax in l2.ott	Gabriel Kerneis

2013-08-30	Small clean up of ott files, start of environments for formal representation ↵	Kathy Gray
	of kind and type system
2013-08-22	Pretty printer for whole AST; due to parenthesis not always being placed ↵	Kathy Gray
	where needed, what is generated may not parse
2013-08-19	language.ott: update syntax of index ranges	Gabriel Kerneis

2013-08-19	language.ott: syntax for types in patterns	Gabriel Kerneis