| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-09 | Fix bug in rewriting of try-catch-blocks with variable updates | Thomas Bauereiss | |
| 2018-07-09 | Tweak rewriting of literal patterns for Lem | Thomas Bauereiss | |
| 2018-07-09 | Add explanatory comment to guard rewriting | Thomas Bauereiss | |
| 2018-07-03 | Fix letbind_effects on LEXP_deref with an effectful subexpression | Brian Campbell | |
| 2018-06-26 | In guarded pattern rewriting, irrefutable patterns subsume wildcards | Brian Campbell | |
| Necessary to prevent redundant clauses that Coq will reject (There's still a problem if you use a variable rather than a wildcard, see the test) | |||
| 2018-06-25 | Check for variables in disjointness check | Thomas Bauereiss | |
| 2018-06-25 | Fix a bug in pattern guard rewriting | Thomas Bauereiss | |
| Remember and use fallthrough clauses instead of dropping them when the last clause in a group has a guard | |||
| 2018-06-11 | add 'pat as id' mapping-patterns | Jon French | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| (involved some manual tinkering with gitignore, type_check, riscv) | |||
| 2018-06-06 | Some work on improving error messages | Alasdair Armstrong | |
| We now store the location where type variables were bound, so we can use this information when printing error messages. Factor type errors out into type_error.ml. This means that Type_check.check is now Type_error.check, as it previously it handled wrapping the type_errors into reporting_basic errors. Type_check.check' has therefore been renamed to Type_check.check. | |||
| 2018-05-21 | fix bug in rewrite_defs_mapping_patterns where pattern-uses of mappings with ↵ | Jon French | |
| multiple arguments weren't type-checking correctly | |||
| 2018-05-18 | Fix bug in rewriting variable updates | Thomas Bauereiss | |
| 2018-05-18 | temporary HACK for aarch64: make rewrite_defs_pat_lits ignore strings | Jon French | |
| 2018-05-18 | more riscv mappings; riscv now builds successfully to lem which builds to ↵ | Jon French | |
| isabelle (but isabelle almost certainly broken) | |||
| 2018-05-17 | fix bug in rewrite_defs_pat_string_append -- make it pass types through ↵ | Jon French | |
| correctly | |||
| 2018-05-16 | Add support for inline val-spec declaration for mappings | Jon French | |
| This means that a mapping which formerly had to be pre-declared like val name : a <-> b ... mapping name { x <-> y, ... } can now be shortened to mapping name : a <-> b { x <-> y, ... } | |||
| 2018-05-15 | reorder lem rewrite passes and explicitly remove mapping valspecs; string ↵ | Jon French | |
| stuff now compiles to Lem | |||
| 2018-05-15 | rewrite_defs_guarded_pats: guards deserve rewriting too | Jon French | |
| 2018-05-14 | make debug printing of realised mappings both optional and lazy | Jon French | |
| 2018-05-11 | support for mapping-patterns inside (should be) all other pattern types | Jon French | |
| 2018-05-10 | Merge branch 'sail2' into mappings | Jon French | |
| 2018-05-10 | generalise string pattern matching to arbitrary arguments rather than just ↵ | Jon French | |
| an id; also remove builtin special-casing as it's not needed! | |||
| 2018-05-09 | Add more annotations for loop bounds in Lem rewriting | Thomas Bauereiss | |
| Typechecking for-loops failed after the Lem rewriting passes in some cases: if the lower bound for the loop may be greater than the upper bound, the loop variable's type might be empty, and it cannot be initialised. This patch adds a guard "lower <= upper" around the loop body, and removes it again during pretty-printing. | |||
| 2018-05-09 | Support short-circuiting of Boolean expressions in Lem | Thomas Bauereiss | |
| 2018-05-08 | fixed sub-mappings | Jon French | |
| 2018-05-04 | Checked that variable names in split_fun rewrites are really variables | Brian Campbell | |
| Otherwise some clauses disappear | |||
| 2018-05-04 | Fix missing nexp id rewriting | Brian Campbell | |
| 2018-05-04 | Rewrite constant nexps in specs | Brian Campbell | |
| (from Thomas) | |||
| 2018-05-03 | Flow typing and l-expression changes for ASL parser | Alasdair Armstrong | |
| 1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/ | |||
| 2018-05-03 | support sub-mappings in string-append-patterns | Jon French | |
| 2018-05-03 | synthesise string-prefix-check functions for mappings where either side is ↵ | Jon French | |
| string (kind of hacky but there you go) | |||
| 2018-05-02 | scattered mappings | Jon French | |
| 2018-05-02 | refactor string append pattern ast to be based on lists rather than pairs | Jon French | |
| 2018-05-01 | add type annotation patterns to mpats | Jon French | |
| 2018-05-01 | rewriting of builtin mappings e.g. int | Jon French | |
| 2018-05-01 | further progress but confounds the type checker? | Jon French | |
| 2018-05-01 | progress on debugging string pattern matching | Jon French | |
| 2018-05-01 | oops, not every pattern is in fact string_typ, remember to pass through the ↵ | Jon French | |
| original type in rewrite_defs_pat_string_append when not doing anything | |||
| 2018-05-01 | create a single funcl with a match, rather than converting mapcls to funcls, ↵ | Jon French | |
| because OCaml among others doesn't allow top-level guards | |||
| 2018-05-01 | further progress | Jon French | |
| 2018-05-01 | starting to also do integer support | Jon French | |
| 2018-05-01 | starting to also do integer support | Jon French | |
| 2018-05-01 | start of string pattern matching: currently only literals | Jon French | |
| 2018-05-01 | fix refactored rewrite_pexp_with_guards (where type information is and is ↵ | Jon French | |
| not...) | |||
| 2018-05-01 | more refactoring of pexp rewriters | Jon French | |
| 2018-05-01 | Type_check: factor rewrite_pexps_with_guards out of rewrite_defs_pat_lits | Jon French | |
| 2018-04-26 | Fix bug in rewriting of loops | Thomas Bauereiss | |
| Take into account existential types when determining bounds for the loop variable | |||
| 2018-04-26 | Avoid adding explicit type annotations with generated type variables | Thomas Bauereiss | |
| 2018-04-26 | Make effect propagation in rewriter more efficient | Thomas Bauereiss | |
| Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect, assuming that the effects of subexpressions have already been fixed by the recursive calls of the rewriter. | |||
| 2018-04-18 | Rename BK_nat to BK_int to be consistent with source syntax | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |