| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
The type-constraints are inspired from those for (+). They seem to work
but I am not sure they make sense.
The vector is interpreted as unsigned.
|
|
|
|
Conflicts:
src/lem_interp/interp_lib.lem
src/lem_interp/run_interp.ml
Remove "to_vec_safe" work-around
|
|
solving; get test_power running again by supporting the correct operations and bit operations
|
|
Update power.sail to new, pretty-printer-based version
|
|
Default to 64 bit for vec + range
|
|
|
|
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
|
|
Change type of + on vectors to (bit vector,bit vector) -> bit vector
|
|
vectors) and make the test suite pass again
|
|
WARNING: vector test breaks due to not having implemented the full range of different + functions
In general, we need to decide whether vector + vector, vector + range and range + vector should all return ranges, vectors or a mixture
|
|
|
|
|
|
Again, this is necessary to compare big_int
|
|
constraints. Clean up Lem output a little for readability while debugging.
|
|
|
|
|
|
to_num and to_vec probably still need to be fixed
|
|
Two bugs are worked-around here:
- missing cast to nat when a vector is wrapped in exts
(exts is a no-op currently anyway, so we are discarding it)
- missing cast (due to limited type-inference) in one if branch:
type given explicitly.
|
|
This patch should be reverted when the interpreter is fixed.
The first instruction of main.bin is now executed. The second
one fails, seemingly because of a similar missing cast issue
(external function add receives register GPR1 as value).
|
|
|
|
|
|
|
|
In fact, increasing order is big-endian, not little-endian.
This is good news for us, because it means we do not need any
switch for the POWER spec.
|
|
Many limitations and bugs currently, but loads binary and decodes
opcodes correctly (using endianness hacks). Disabled in the default
test suite (but still compiled), run "make test_power" to try it.
|
|
Lem's word library does some dark magic because of its assumption that
words represent signed integers. Therefore, it is unreliable to truncate
words, as well as to use the internal representation. boolListFrombitSeq
seems safe for our purposes, though (provided the bitseq has been
created with an infinite length from a positive integer).
|
|
ast, and extending the interpreter to expect annotations.
Annotations and locations are still not used by the interpreter.
|
|
|
|
There is now enough stuff to decode and execute a very basic Branch
instruction (encoding everything as little-endian rather than big-
endian among many other work-arounds).
|
|
|
|
|
|
|
|
Only chapter about branches (except system calls because of sail
typechecking issue). Decoding seems to work. Execution typechecks
currently, but is pretty surely broken otherwise.
|
|
Notice the need for double parentheses in test/test3.sail, because the
interpreter does not perform curryfication automatically (only the first
parameter in kept with List_extra.head):
add ((1, 3)) (* works *)
add (1, 3) (* fails, equivalent to: add (1) *)
Fortunately enough, infix functions work correctly by default. A dirty
quickfix would be easy, but I'm not sure at which level this should be
addressed properly (interpreter? typing? etc.).
|
|
|
|
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).
|
|
|
