| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-06-12 | Overloaded multiplication | Gabriel Kerneis | |
| Hopefully I got the constraints right again. | |||
| 2014-06-12 | Interpret when an unknown is inserted into the program by interp_exhaustive | Kathy Gray | |
| 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. | |||
| 2014-06-12 | Add uint* to default type names for lexer | Gabriel Kerneis | |
| This is necessary to avoid a parse error. It might make sense to merge this list and the one in type_internal.ml somehow, to avoid duplication and similar bugs in the future. | |||
| 2014-06-11 | power.sail: store mode64bit in a bool register | Gabriel Kerneis | |
| This is now possible because we handle coercions better. | |||
| 2014-06-11 | Update power.sail: remove some hacks | Gabriel Kerneis | |
| 2014-06-11 | Equality between range and bit vector | Gabriel Kerneis | |
| 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. | |||
| 2014-06-11 | Improve error message for missing library functions | Gabriel Kerneis | |
| 2014-06-10 | Minor color and build tweaks | Gabriel Kerneis | |
| 2014-06-10 | More colors | Gabriel Kerneis | |
| 2014-06-10 | More robust build system | Gabriel Kerneis | |
| 2014-06-09 | Better, colored hole | Gabriel Kerneis | |
| 2014-06-09 | Improve interaction after chat with Peter | Gabriel Kerneis | |
| - remember mode (run, step or next) between instructions - display continuation by default in step mode - start in step mode by default - incompatible change: the shorthand for stack is now bt (=backtrace), since s becomes the shorthand for step - incompatible change: pressing enter now repeats the current mode, instead of "step" | |||
| 2014-06-09 | Support deinfix pretty-printing | Gabriel Kerneis | |
| 2014-06-09 | Add more stops in interpreter (stopping just at the point of each internal ↵ | Kathy Gray | |
| function call) Also turning off an annoying printf I left in. | |||
| 2014-06-09 | Working towards evaluating with interp_exhaustive | Kathy Gray | |
| 2014-06-09 | Add "continuation" command in interpreter | Gabriel Kerneis | |
| This displays the full continuation of the current breakpoint, which is basically the closest that we have from the "context" requested by Peter. Especially using it after the "execute" breakpoint shows the code of the instruction to be executed. | |||
| 2014-06-09 | Add switch to show/hide casts in interpreter | Gabriel Kerneis | |
| Use "show_casts" and "hide_casts" in interactive interpreter to display or show casts in expressions. Hidden by default (makes things much less readable otherwise). | |||
| 2014-06-09 | Add explicit flag -r to rebuild in demo.sh | Gabriel Kerneis | |
| ./demo.sh now jumps straight into the interpreter. ./demo.sh -r does the fancy "rebuild step-by-step with comments" show | |||
| 2014-06-09 | Merge branch 'for-dagstuhl' into master | Gabriel Kerneis | |
| Conflicts: src/lem_interp/interp_lib.lem src/lem_interp/run_interp.ml Remove "to_vec_safe" work-around | |||
| 2014-06-07 | Interactive demo | Gabriel Kerneis | |
| 2014-06-07 | Add optional overloading on expected return type to fix bug in constraint ↵ | Kathy Gray | |
| solving; get test_power running again by supporting the correct operations and bit operations | |||
| 2014-06-07 | Don't use cycle for fetch-decode-execute | Gabriel Kerneis | |
| 2014-06-07 | exts returns bit[64] instead of nat | Gabriel Kerneis | |
| Update power.sail to new, pretty-printer-based version | |||
| 2014-06-07 | Adding type abbreviations for uint8 to uint64 to make for easier casts | Kathy Gray | |
| 2014-06-07 | Copy main.bin in Sail repository for Power test | Gabriel Kerneis | |
| 2014-06-07 | Improve help message | Gabriel Kerneis | |
| 2014-06-07 | Print mem and env | Gabriel Kerneis | |
| 2014-06-07 | Pattern-matching exhaustiveness | Gabriel Kerneis | |
| 2014-06-07 | Stack printing | Gabriel Kerneis | |
| 2014-06-07 | Print holes as [x] | Gabriel Kerneis | |
| 2014-06-07 | Fix E_vector_append in interp pretty-printer | Gabriel Kerneis | |
| 2014-06-07 | Fix pretty-printing for E_vector_append | Gabriel Kerneis | |
| 2014-06-06 | Compact debug output and first draft of interactive loop | Gabriel Kerneis | |
| 2014-06-06 | Improve work-around | Gabriel Kerneis | |
| Default to 64 bit for vec + range | |||
| 2014-06-06 | Add wrapper script and --interactive for demo | Gabriel Kerneis | |
| 2014-06-06 | Add a pretty-printer for Interp_ast | Gabriel Kerneis | |
| Copy-pasted with a few tweaks from Pretty_printer. Should really make a functor instead, but not sure how to deal with E_internal_cast yet. Note that Interp_ast and Ast are *not* generated from the same ott file (resp. l2.ott and l2_type.ott), but they are close enough that the code almost "just works". | |||
| 2014-06-06 | Adding type abbreviations for uint8 to uint64 to make for easier casts | Kathy Gray | |
| 2014-06-05 | Shorten debug output for power | Gabriel Kerneis | |
| 2014-06-05 | Enable single-stepping for test/power.sail | Gabriel Kerneis | |
| 2014-06-05 | Refactor to_vec and add work-around to avoid truncation | Gabriel Kerneis | |
| 2014-06-04 | Fixup type coercions and overloading | Kathy 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-06-02 | Fix dependent-type for MEM in power.sail | Gabriel Kerneis | |
| Now, constraint resolution works for test/power.sail | |||
| 2014-05-30 | Remove fresh variables from type annotations (have not tested yet that the ↵ | Kathy Gray | |
| resulting files once pretty-printed will type check) | |||
| 2014-05-30 | Change == to eq_big_int in a missed comparison | Kathy Gray | |
| 2014-05-30 | Add pretty-printer test (idempotence) | Gabriel Kerneis | |
| Fails in most cases because of "fresh" variables in type annotations that cannot be parsed again. | |||
| 2014-05-30 | Remove bit-rotted, abonned test file | Gabriel Kerneis | |
| 2014-05-30 | More correct arithmetic types, to generate even more constraints | Kathy Gray | |
| 2014-05-29 | Check constraints in power.sail; this required using big_int instead of int ↵ | Kathy Gray | |
| 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>) | |||
| 2014-05-28 | correct mismatched parens didn't mean to commit... | Kathy Gray | |
| 2014-05-28 | Support stepped interpreting, and use normalisation instead of eval_nexp in ↵ | Kathy Gray | |
| constraints | |||
