sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2015-09-30	Alias support for ocaml mode	Kathy Gray

2015-08-06	Update analysis to merge states and values after branches taken due to ↵	Kathy Gray
	unknown conditions. Does not merge if one path has resulted in an exit
2015-07-24	Begin doing better analysis on case splits over unknowns	Kathy Gray

2015-06-02	Fix errors around ARM not being able to decode due to instruction_extractor ↵	Kathy Gray
	being very power-specific. Note: slight interface change to instruction_extractor
2015-03-26	Add subtraction to nexp grammar (removing the need to do a + (-1 * b))	Kathy Gray
	Fix up parsing on 2** precedence Fix errors on type variables in function definition
2015-02-24	Overloading formal relation	Kathy Gray

2015-02-18	All existing type rules in line with implementation (and no more red)	Kathy Gray
	Still to do: type rules for register aliases and relation for overloading selection
2015-02-18	expression type checking inline with rules, lexp still out of date; ↵	Kathy Gray
	overloading resolution not modelled
2015-02-17	Bring type rules more into modern state of type checker	Kathy Gray

2015-01-12	Add specialised support for numeric singleton types (i.e. what used to be ↵	Kathy Gray
	range<'N,'N>) Non-sugar syntax is -- forall Nat 'N. atom<'N> Sugar syntax is -- [: 'N :] Also begin adding pp support for generating ocaml from ast types.
2014-12-09	Some of the type rules for expressions	Kathy Gray

2014-12-04	ott rules for type checking pattern match	Kathy Gray

2014-12-03	Type rules unto coercion now represented in ott	Kathy Gray

2014-07-14	Initial support for aliases and exit through the type system and the ↵	Kathy Gray
	interpreter. An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
2014-06-12	Interpret when an unknown is inserted into the program by interp_exhaustive	Kathy Gray
	Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet. If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables. In a function call, the cases are all collected but the support is not in place at the moment to evaluate them. If an unknown is the result of the cond expression in an if, the then and else case become a block. Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet.
2014-05-29	Check constraints in power.sail; this required using big_int instead of int ↵	Kathy Gray
	to support 264. Note: now nat (short hand for range<0,infinity>) should only be used if you really mean a nat instead of a bounded number (i.e. range<0,232>)
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-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-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.