| 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 | remove -merge true from ott makefile -- lem at least doesn't build with it | Jon French | |
| 2017-07-21 | l2.ott: port across additions to base_effect from rmem | Jon French | |
| 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-04-06 | typesetting tt vs non-tt | Peter Sewell | |
| 2017-04-06 | fix typesetting of standalone grammar document | Peter Sewell | |
| 2017-03-15 | rename "manual.tex" to "type_system.tex" | Peter Sewell | |
| fix Makefile clean | |||
| 2017-02-25 | wib | Peter Sewell | |
| 2017-02-13 | wib | Peter Sewell | |
| 2017-02-13 | make syntax typeset in manual in ASCII-friendly style rather than using | Peter Sewell | |
| math symbols. This breaks the l2.pdf build in language/ (for the moment). | |||
| 2017-02-13 | tidying | Peter Sewell | |
| 2017-02-13 | tidying | Peter Sewell | |
| 2017-02-10 | wib | Peter Sewell | |
| 2017-02-10 | wib | Peter Sewell | |
| 2017-02-10 | tidy l2.ott | Peter Sewell | |
| 2017-02-09 | tweak pp of initial type environment and l2.ott comments | Peter Sewell | |
| 2017-02-05 | Merge branch 'master' of bitbucket.org:Peter_Sewell/sail | Peter Sewell | |
| Conflicts: language/manual.pdf | |||
| 2017-02-05 | wib | Peter Sewell | |
| 2017-02-02 | K,P debrief | Peter Sewell | |
| 2017-01-31 | Kathy, Peter: pp of initial type environment | Peter Sewell | |
| 2017-01-30 | switch to github ott | Peter Sewell | |
| 2017-01-30 | remove "rm *.tex" from language/Makefile "make clean" | Peter Sewell | |
| 2017-01-30 | Restore manual.tex, accidentally deleted | Kathy Gray | |
| Minor updates to README, still in progress | |||
| 2017-01-23 | Extend lib with min and max | Kathy Gray | |
| 2016-11-23 | Add new type checking file. Small changes to type inference, temporary ↵ | Kathy Gray | |
| change to printing | |||
| 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-09-25 | Catch formal type system up to reality, in progress | Kathy Gray | |
| 2016-08-17 | tuple assignment now implemented so (a,b) := foo() will now work | Kathy Gray | |
| 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-03 | Fix typo in manual which had true instead of false on assert documentation | Kathy Gray | |
| Fix bug in local register access | |||
| 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-25 | A bit better readme | Kathy Gray | |
| A few more tips Trying to fix up and bring up to date the built-in types and library | |||
| 2016-02-25 | Expand what advice and information is in the manual slightly | Kathy Gray | |
| 2016-02-25 | Add the manual, such as it is, for others to be able to use and have without ↵ | Kathy Gray | |
| needing ott | |||
| 2016-02-25 | Restore manual.tex mysteriously deleted by peter in May 2015. | Robert Norton | |
| 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-12-17 | First bit of gluing mips onto interpreter and eventually ppcmem infrastructure | Kathy Gray | |
| 2015-12-14 | Adding new location constructor for location of generated terms | Kathy Gray | |
| 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-30 | Alias support for ocaml mode | 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 | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |