summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-06-12Overloaded multiplicationGabriel Kerneis
Hopefully I got the constraints right again.
2014-06-12Interpret when an unknown is inserted into the program by interp_exhaustiveKathy 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-12Add uint* to default type names for lexerGabriel 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-11power.sail: store mode64bit in a bool registerGabriel Kerneis
This is now possible because we handle coercions better.
2014-06-11Update power.sail: remove some hacksGabriel Kerneis
2014-06-11Equality between range and bit vectorGabriel 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-11Improve error message for missing library functionsGabriel Kerneis
2014-06-10Minor color and build tweaksGabriel Kerneis
2014-06-10More colorsGabriel Kerneis
2014-06-10More robust build systemGabriel Kerneis
2014-06-09Better, colored holeGabriel Kerneis
2014-06-09Improve interaction after chat with PeterGabriel 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-09Support deinfix pretty-printingGabriel Kerneis
2014-06-09Add 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-09Working towards evaluating with interp_exhaustiveKathy Gray
2014-06-09Add "continuation" command in interpreterGabriel 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-09Add switch to show/hide casts in interpreterGabriel 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-09Add explicit flag -r to rebuild in demo.shGabriel Kerneis
./demo.sh now jumps straight into the interpreter. ./demo.sh -r does the fancy "rebuild step-by-step with comments" show
2014-06-09Merge branch 'for-dagstuhl' into masterGabriel Kerneis
Conflicts: src/lem_interp/interp_lib.lem src/lem_interp/run_interp.ml Remove "to_vec_safe" work-around
2014-06-07Interactive demoGabriel Kerneis
2014-06-07Add 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-07Don't use cycle for fetch-decode-executeGabriel Kerneis
2014-06-07exts returns bit[64] instead of natGabriel Kerneis
Update power.sail to new, pretty-printer-based version
2014-06-07Adding type abbreviations for uint8 to uint64 to make for easier castsKathy Gray
2014-06-07Copy main.bin in Sail repository for Power testGabriel Kerneis
2014-06-07Improve help messageGabriel Kerneis
2014-06-07Print mem and envGabriel Kerneis
2014-06-07Pattern-matching exhaustivenessGabriel Kerneis
2014-06-07Stack printingGabriel Kerneis
2014-06-07Print holes as [x]Gabriel Kerneis
2014-06-07Fix E_vector_append in interp pretty-printerGabriel Kerneis
2014-06-07Fix pretty-printing for E_vector_appendGabriel Kerneis
2014-06-06Compact debug output and first draft of interactive loopGabriel Kerneis
2014-06-06Improve work-aroundGabriel Kerneis
Default to 64 bit for vec + range
2014-06-06Add wrapper script and --interactive for demoGabriel Kerneis
2014-06-06Add a pretty-printer for Interp_astGabriel 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-06Adding type abbreviations for uint8 to uint64 to make for easier castsKathy Gray
2014-06-05Shorten debug output for powerGabriel Kerneis
2014-06-05Enable single-stepping for test/power.sailGabriel Kerneis
2014-06-05Refactor to_vec and add work-around to avoid truncationGabriel Kerneis
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-06-02Fix dependent-type for MEM in power.sailGabriel Kerneis
Now, constraint resolution works for test/power.sail
2014-05-30Remove fresh variables from type annotations (have not tested yet that the ↵Kathy Gray
resulting files once pretty-printed will type check)
2014-05-30Change == to eq_big_int in a missed comparisonKathy Gray
2014-05-30Add pretty-printer test (idempotence)Gabriel Kerneis
Fails in most cases because of "fresh" variables in type annotations that cannot be parsed again.
2014-05-30Remove bit-rotted, abonned test fileGabriel Kerneis
2014-05-30More correct arithmetic types, to generate even more constraintsKathy Gray
2014-05-29Check 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-28correct mismatched parens didn't mean to commit...Kathy Gray
2014-05-28Support stepped interpreting, and use normalisation instead of eval_nexp in ↵Kathy Gray
constraints