| Age | Commit message (Collapse) | Author |
|---|
|
Rename l2.ott to sail.ott
|
|
|
|
Not working yet
|
|
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
|
|
|
|
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.
|
|
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.
|
|
|
|
Events are eamem to signal the memory address to write to and wmv to pass the value to write
|
|
Also fix type checker bug in not reporting modifications to parameter values
|
|
|
|
|
|
Fix up parsing on 2** precedence
Fix errors on type variables in function definition
|
|
shorthand syntax, needed for arm spec
|
|
and the like.
|
|
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
|
|
|
|
|
|
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
|
|
functions for connecting the interpreter to a memory model)
Also adding default values to index vectors for supporting sparse vectors/maps
|
|
|
|
constraints. Clean up Lem output a little for readability while debugging.
|
|
|
|
|
|
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.
|
|
|
|
First pass parser to identify type names is in progress (current test files fail, will correct once pre-parser is in place)
|
|
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
|
|
only match simple patterns (until type information is available).
|
|
|
