sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-02-06	coerce bit to bool when not a literal bit. Note: this will only add a ↵	Kathy Gray
	conversion function for expressions of bit type, an explicit cast to bit would be needed to come from an enum or nat.
2014-02-06	coercians for bits to bools for literals	Kathy Gray

2014-02-06	type check more vectors	Kathy Gray

2014-02-06	push effect information around while checking expressions	Kathy Gray

2014-02-05	Replace symbolic link by actual file	Gabriel Kerneis

2014-02-05	Test scattered typedef cross-reference	Gabriel Kerneis

2014-02-05	Fix type id parsing error ans associated type checking bugs in scattereds	Kathy Gray

2014-02-05	Fix pattern constructor bug in type checking (darn tuples/not tuples)	Kathy Gray

2014-02-05	Typechecking lets, concrete vectors, and function calls (minus effects)	Kathy Gray

2014-02-05	First bit of Power spec	Gabriel Kerneis
	Only chapter about branches (except system calls because of sail typechecking issue). Decoding seems to work. Execution typechecks currently, but is pretty surely broken otherwise.
2014-02-05	Adding failing typechecking test	Gabriel Kerneis
	File "test/test1.sail", line 27, character 22 to line 27, character 26 Type error: Type mismatch :(6() * ) , bit
2014-02-05	Revert "Accept single bits as boolean values for if in interpreter"	Gabriel Kerneis
	This reverts commit 828f19828e41ced146f06e9a7eb4183cd9ef3ab4. It was a temporary workaround now fixed when we generate Sail code.
2014-02-05	Deinfixable colon	Gabriel Kerneis

2014-02-03	More type checking, including coercing 0 and 1 into bits when appropriate ↵	Kathy Gray
	(in limited circumstances at the moment due to which expressions are actually checked, so test files should not yet be changed)
2014-01-31	More type checking and conversions	Kathy Gray
	(Temporarily turning off unbound identifier checks, until all variable-introducing forms are checked)
2014-01-30	Expression type checking, not complete	Kathy Gray

2014-01-29	Type check function headers and parameters	Kathy Gray

2014-01-17	Type check through type definitions and val specifications, building ↵	Kathy Gray
	definition environment. Skipping function definition, let bind, and expression checking for this commit (to come).
2014-01-15	Accept single bits as boolean values for if in interpreter	Gabriel Kerneis

2014-01-15	Improve error messages	Gabriel Kerneis

2014-01-15	Test indexed match	Gabriel Kerneis

2014-01-14	Fix vector concat pattern matching	Gabriel Kerneis
	The concatenation list was reversed.
2014-01-09	Type equality	Kathy Gray

2014-01-09	Fixed pattern concatenation bug	Kathy Gray

2014-01-09	Fixed a single-argument tuple bug on function calls	Kathy Gray

2014-01-09	Fixed bug in resuming after an action (which was manifesting as an apparent ↵	Kathy Gray
	pattern match bug, which was actually working fine).
2014-01-08	Fixed literal vectors for binary vectors (pattern matching and as ↵	Kathy Gray
	expressions), hex vectors will only produce 0 length vectors.
2014-01-08	Baby step to seeing a literal vector as a vector (ie. testing string support ↵	Kathy Gray
	from Lem)
2014-01-08	More tests for various vector patterns bugs	Gabriel Kerneis

2014-01-08	Between Scylla and Charybdis	Gabriel Kerneis

2014-01-08	Fix pretty-printing of switch-cases	Gabriel Kerneis
	Weird bug, cf. test/pattern.sail.
2014-01-08	Add support for letbound toplevel defs in interpreter	Kathy Gray

2014-01-08	type eq first	Kathy Gray

2014-01-07	Add first operationnal tests for vectors	Gabriel Kerneis

2014-01-07	interp: recover identifiers in error messages	Gabriel Kerneis
	Not displayed currently because of new-lem's lack of string concatenation.
2014-01-07	Lex bitzero and bitone literals	Gabriel Kerneis

2014-01-07	bug: unbound let-defined (and local?) variables	Gabriel Kerneis
	In test/test1.sail, trying to resolve variable v1 in main yields: test1: error: unbound identifier
2014-01-07	Add bit and bitvector literal test	Gabriel Kerneis

2014-01-07	lem homs and type headers	Kathy Gray

2013-12-19	pretty-print: missing quotes for num literals (lem)	Gabriel Kerneis

2013-12-19	pretty-print: pattern-matching of indexed vectors in Lem output	Gabriel Kerneis
	Lem tuples must be surrounded by parentheses (contrary to OCaml ones).
2013-12-18	Tweak formatting in pretty printer, and resolve bugs.	Kathy Gray
	Start specifying lem homs for rules.
2013-12-17	pretty-printer: fix union constructor application	Gabriel Kerneis
	Foo (1,2,3) is stored internally as the function Foo applied to [1; 2; 3]. We need to add commas when pretty-printing. This should not affect pretty-printing of regular functions application, since those always take a single parameter anyway (which may be a tuple).
2013-12-17	Remove spurious lexing tokens	Gabriel Kerneis

2013-12-16	minor wip on tiny model	Gabriel Kerneis

2013-12-16	test: catch and print exceptions	Gabriel Kerneis

2013-12-16	pretty-printer: typo	Gabriel Kerneis

2013-12-16	lexer: inc and dec keywords	Gabriel Kerneis

2013-12-13	Fix effect annotation bug, take 2	Kathy Gray

2013-12-13	Fix effect annotation pretty-printing	Gabriel Kerneis
	There is also a bug for parsing effect annotations (in fundecl). But for some reason, my fix for the parser does not work: test/test2.sail still refuses to parse (chokes on "effect pure"), even with "Effect" added to parser.mly.