| Age | Commit message (Collapse) | Author |
|---|
|
function-clause
|
|
temporarily use other version of Lem
|
|
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.
|
|
|
|
interpreter.
An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
|
|
and the like.
|
|
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
|
|
|
|
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.
|
|
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
|
|
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>)
|
|
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.
|
|
to_num and to_vec probably still need to be fixed
|
|
|
|
available for field lookups of registers; this feature still not fully working.
|
|
assigned to in assignments.
|
|
|
|
ast, and extending the interpreter to expect annotations.
Annotations and locations are still not used by the interpreter.
|
|
|
|
Type checking now recurses through assign, but doesn’t do the proper checks yet
|
|
|
|
|
|
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)
|
|
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).
|
|
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).
|
|
actually parses
|
|
|
