| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-29 | Set maximum split size to work with aarch64 no vector | Brian Campbell | |
| 2018-01-29 | Turn off constraint substitution in mono | Brian Campbell | |
| (Type checker doesn't seem to use false aggressively enough for this) | |||
| 2018-01-29 | Turn off warnings when rechecking after mono | Brian Campbell | |
| 2018-01-29 | Avoid generating (_ as n) in mono, broke atom type rewriting | Brian Campbell | |
| 2018-01-26 | One more mono rewrite | Brian Campbell | |
| 2018-01-26 | Add replacement of complex nexp sizes by equivalent variables in mono | Brian Campbell | |
| 2018-01-26 | Preserve more typing info in monomorphisation for later stages | Brian Campbell | |
| 2018-01-25 | Use set asserts as case splits in monomorphisation | Brian Campbell | |
| 2018-01-25 | Missing type expansion | Brian Campbell | |
| 2018-01-25 | Handle bound variables properly with precise case splitting | Brian Campbell | |
| 2018-01-25 | Basic support for match x[5 .. 2] with case splits | Brian Campbell | |
| 2018-01-25 | Implement basic case splitting based on found case expressions | Brian Campbell | |
| (makes some of the monomorphisation case splits smaller) | |||
| 2018-01-19 | Update monomorphisation for sail2 | Brian Campbell | |
| (no vector type start position, comment syntax) | |||
| 2018-01-18 | Merge remote-tracking branch 'origin/experiments' into sail2 | Alasdair Armstrong | |
| 2018-01-16 | Fix problem with let-bindings in pattern guards | Thomas Bauereiss | |
| Monomorphisation sometimes produces pattern guard with let-bindings, e.g. | ... if (let regsize = size_itself(regsize) in eq(regsize, 32)) -> ... Previously, the rewriting pass for let-bindings (and pattern guards) pulled these out of the guard condition and into the same scope as the case expression, which potentially clashed with let-bindings for the same variables in that case expression. The rewriter now leaves let-bindings in place within pure if-conditions, solving this problem. | |||
| 2018-01-16 | Handle for loops correctly when rewriting size parameters | Brian Campbell | |
| 2018-01-16 | Another useful monomorphisation rewrite | Brian Campbell | |
| 2018-01-15 | Check monomorphisation case split size once for each pattern | Brian Campbell | |
| (rather than for each argument separately) | |||
| 2018-01-12 | Merge remote-tracking branch 'origin/experiments' into sail2 | Alasdair Armstrong | |
| 2018-01-12 | Try to keep types for undefined around during monomorphisation | Brian Campbell | |
| Otherwise the type checker can't figure it out when we substitute | |||
| 2018-01-12 | Merge remote-tracking branch 'origin/experiments' into sail2 | Alasdair Armstrong | |
| 2018-01-12 | Remove generic comparison | Brian Campbell | |
| 2018-01-12 | Support constant propagation on casts in monomorphisation | Brian Campbell | |
| 2018-01-10 | Add an all_split_errors option | Brian Campbell | |
| 2018-01-10 | Fix control dependencies in monomorphisation analysis | Brian Campbell | |
| 2018-01-09 | More monomorphisation rewrites for aarch64 | Brian Campbell | |
| 2018-01-09 | Tidy up monomorphisation interface | Brian Campbell | |
| 2018-01-09 | Proper location for no set constraint errors | Brian Campbell | |
| 2018-01-09 | Add some optional experimental rewrites to help with monomorphisation | Brian Campbell | |
| 2018-01-02 | Experimenting with power spec | Alasdair Armstrong | |
| 2017-12-19 | Support user-defined exceptions in Lem shallow embedding | Thomas Bauereiss | |
| The type-checker already supports a user-defined "exception" type that can be used in throw and try-catch expressions. This patch adds support for that to the Lem shallow embedding by adapting the existing exception mechanisms of the state and prompt monads. User-defined exceptions are distinguished from builtin exception cases. For example, the state monad uses type ex 'e = | Exit | Assert of string | Throw of 'e to distinguish between calls to "exit", failed assertions, and user-defined exceptions, respectively. Early return is also handled using the exception mechanism, by lifting to a monad with "either 'r exception" as the exception type, where 'r is the expected return type and "exception" is the user-defined exception type. | |||
| 2017-12-14 | Make sequential and mwords global variables in Lem pretty-printer | Thomas Bauereiss | |
| 2017-12-14 | Merge remote-tracking branch 'origin/experiments' into interactive | Alasdair Armstrong | |
| 2017-12-13 | Use big_nums from Lem | Alasdair Armstrong | |
| 2017-12-12 | Make mono analysis fail properly on effectful functions | Brian Campbell | |
| 2017-12-11 | Remove some duplication from monomorphisation analysis failure reports | Brian Campbell | |
| 2017-12-07 | Support monomorphisation with set constrained integers | Brian Campbell | |
| Also, to support this, constant propagation for integer multiply, fix substitution of concrete values for nvars, size parameters in single argument functions, fix kind for itself, add eq_atom to prelude | |||
| 2017-12-06 | Remove filename mangling in monomorphisation | Brian Campbell | |
| Broke analysis a little | |||
| 2017-12-06 | Add top-level pattern match guards internally | Brian Campbell | |
| Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next. | |||
| 2017-12-05 | Update license headers for Sail source | Alasdair Armstrong | |
| 2017-11-27 | Replace bad generic comparisons in mono | Brian Campbell | |
| 2017-11-27 | Case splitting on bools | Brian Campbell | |
| (mostly to make test cases easier) | |||
| 2017-11-24 | Use unbound precision big_ints throughout sail. | Alasdair Armstrong | |
| Alastair's test cases revealed that using regular ints causes issues throughout sail, where all kinds of things can internally overflow in edge cases. This either causes crashes (e.g. int_of_string fails for big ints) or bizarre inexplicable behaviour. This patch switches the sail AST to use big_int rather than int, and updates everything accordingly. This touches everything and there may be bugs where I mistranslated things, and also n = m will still typecheck with big_ints but fail at runtime (ocaml seems to have decided that static typing is unnecessary for equality...), as it needs to be changed to eq_big_int. I also got rid of the old unused ocaml backend while I was updating things, so as to not have to fix it. | |||
| 2017-11-21 | Merge Thomas' suggested changes | Brian Campbell | |
| Use overloading to find eq/neq Track range/atom split Missing type expansion | |||
| 2017-11-20 | Tidy last up | Brian Campbell | |
| 2017-11-20 | Constant propagation in guards | Brian Campbell | |
| 2017-11-20 | Basic handling of recursive calls in monomorphisation analysis | Brian Campbell | |
| 2017-11-20 | Look up the right type variables in monomorphisation analysis | Brian Campbell | |
| 2017-11-20 | Support new nexp in mono | Brian Campbell | |
| 2017-11-16 | Remove unused Typ_wild constructor | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |