| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-08-13 | Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to ↵ | Peter Sewell | |
| temporarily use other version of Lem | |||
| 2014-07-29 | A file can now declare that a default order is either inc or dec, and this ↵ | Kathy Gray | |
| will be reflected in short hand type syntax, inc is still the default if undeclared So: default order dec register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *) default order inc register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *) It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon. | |||
| 2014-07-25 | Start of setting a default order for literal vectors and for vector ↵ | Kathy Gray | |
| shorthand syntax, needed for arm spec | |||
| 2014-07-18 | Writing to concatenated aliases | 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-07-08 | Extend language to support register aliases and to support interrupts, traps ↵ | Kathy Gray | |
| and the like. | |||
| 2014-06-26 | Adding better support for unspecified values in indexed vectors | Kathy Gray | |
| Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches | |||
| 2014-06-25 | Add support for memory barrier | Kathy Gray | |
| 2014-06-25 | Add support for actions that read just a slice or single bit of a register | Kathy Gray | |
| 2014-06-23 | Get indexed vectors, particularly with default values, working | Kathy Gray | |
| 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-06-04 | Fixup type coercions and overloading | Kathy Gray | |
| Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions. Warning: test_power does not run as not all overloaded funcitons are implemented Warning: vector concatenation does not pretty print to sail source yet | |||
| 2014-05-29 | Check constraints in power.sail; this required using big_int instead of int ↵ | Kathy Gray | |
| to support 2**64. 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,2**32>) | |||
| 2014-05-14 | More interface update for connecting externally (interp_interface provides ↵ | Kathy Gray | |
| functions for connecting the interpreter to a memory model) Also adding default values to index vectors for supporting sparse vectors/maps | |||
| 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). | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |