| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-24 | move value type definitions to ott, and introduce new E_internal_value ast ↵ | Jon French | |
| node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node | |||
| 2017-07-21 | l2.ott: factor ocaml 'l' type reference into ott definition of 'l' | Jon French | |
| 2017-07-21 | l2.ott, l2_parse.ott: remove unnecessary 'type text = string' | Jon French | |
| 2017-03-15 | rename "manual.tex" to "type_system.tex" | Peter Sewell | |
| fix Makefile clean | |||
| 2017-02-10 | wib | Peter Sewell | |
| 2017-02-09 | tweak pp of initial type environment and l2.ott comments | Peter Sewell | |
| 2016-10-19 | Revert "file missed in previous commit" | Christopher Pulte | |
| This reverts commit d836ac35d82311ae7522937b8b01c140f8616b97. | |||
| 2016-10-19 | file missed in previous commit | Christopher Pulte | |
| 2016-08-14 | Start adding form for (a,b,c) := foo() | Kathy Gray | |
| Not working yet | |||
| 2016-07-23 | Add effect annotation for return, and actually keep a return after type check. | Kathy Gray | |
| 2016-07-23 | Add a return exp form to Sail, supported in type checker and in interpreter. | Kathy Gray | |
| TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem | |||
| 2016-05-27 | Also add to ott | Kathy Gray | |
| 2016-03-02 | Add new language feature to permit definitions of items of kind Nat, etc as ↵ | Kathy Gray | |
| well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required. | |||
| 2016-02-23 | Several fixes | Kathy Gray | |
| Improve printing for asl to sail readability; Add -o option for selecting the name of file generation; Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes | |||
| 2016-01-06 | Add new assert expression to Sail | Kathy Gray | |
| This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified. | |||
| 2015-11-24 | Add BE_escape effect when an E_exit is seen | Kathy Gray | |
| Close #20 | |||
| 2015-10-19 | progress on lem backend | Christopher Pulte | |
| 2015-10-08 | Add another internal let for Christopher | Kathy Gray | |
| 2015-10-07 | Start expanding annot for more refined effect tracking | Kathy Gray | |
| 2015-09-24 | Parameterise the rewriter's for multiple different rewritings | Kathy Gray | |
| Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope | |||
| 2015-06-24 | Support new memory write events in the sail front end and pretty printer | Kathy Gray | |
| Events are eamem to signal the memory address to write to and wmv to pass the value to write | |||
| 2015-05-13 | Add dynamic footprint dependency check event/outcome | Kathy Gray | |
| Also fix type checker bug in not reporting modifications to parameter values | |||
| 2015-05-09 | towards buildability - l2.ml and l2_parse.ml as regenerated with current Ott | Peter Sewell | |
| 2015-05-09 | use less confusing Ott binary | Peter Sewell | |
| 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-13 | Actually use new dependency information in generation of lem/etc. | Kathy Gray | |
| Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass | |||
| 2014-09-30 | Add type annotations to funcls to track effects and constraints from one ↵ | Kathy Gray | |
| function-clause | |||
| 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-18 | Writing to concatenated aliases | Kathy Gray | |
| 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-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-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-03-26 | More steps towards solving and using constraint information | Kathy Gray | |
| 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 | Adding explicit order to for loops | Kathy Gray | |
| 2014-01-07 | lem homs and type headers | 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-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-23 | Don't export list of types to ML AST | Gabriel Kerneis | |
| 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 |