summaryrefslogtreecommitdiff
path: root/language/l2.ml
AgeCommit message (Collapse)Author
2015-05-13Add dynamic footprint dependency check event/outcomeKathy Gray
Also fix type checker bug in not reporting modifications to parameter values
2015-05-09towards buildability - l2.ml and l2_parse.ml as regenerated with current OttPeter Sewell
2015-05-09use less confusing Ott binaryPeter Sewell
2015-03-26Add 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-13Actually 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-30Add type annotations to funcls to track effects and constraints from one ↵Kathy Gray
function-clause
2014-08-13Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to ↵Peter Sewell
temporarily use other version of Lem
2014-07-29A 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-18Writing to concatenated aliasesKathy Gray
2014-07-08Extend language to support register aliases and to support interrupts, traps ↵Kathy Gray
and the like.
2014-06-26Adding better support for unspecified values in indexed vectorsKathy Gray
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
2014-06-25Add support for memory barrierKathy Gray
2014-06-04Fixup type coercions and overloadingKathy 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-14More 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-08Reduce redundant information in ASTKathy Gray
2014-03-26More steps towards solving and using constraint informationKathy Gray
2014-03-03Fixing assorted bugs. Adding ability to put a type on the identifier being ↵Kathy Gray
assigned to in assignments.
2014-02-28Correct bug in parsing and handling a['a:'b] typesKathy Gray
2014-02-21Add 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-18Adding explicit order to for loopsKathy Gray
2014-01-07lem homs and type headersKathy Gray
2013-12-03Syntax 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-29Push syntax changes to type rulesKathy Gray
2013-11-28Updated syntax with working examplesKathy Gray
2013-11-22Syntax 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-01Moved metatheory grammars into l2_rules.ottKathy 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-23Don't export list of types to ML ASTGabriel Kerneis
2013-10-18Typeing rules for patterns and easy expressionsKathy Gray
2013-10-11Supporting all expressions, although vector cacentation pattern matching can ↵Kathy Gray
only match simple patterns (until type information is available).
2013-10-09Adding memory writes. Cleaning up the let in the ott file to reflect what ↵Kathy Gray
actually parses
2013-10-04Clean up build systemGabriel Kerneis