| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-17 | a-normalisation for lem backend | Christopher Pulte | |
| 2015-10-13 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-13 | some progress on sequentialise_effects | Christopher Pulte | |
| 2015-10-13 | Refine local vs cumulative effects for lexp | Kathy Gray | |
| More ocaml output, better treatment of registers. | |||
| 2015-10-12 | fixes | Christopher Pulte | |
| 2015-10-12 | apply rewriter changes to master as well | Christopher Pulte | |
| 2015-10-08 | augment annot of interpreter | Kathy Gray | |
| 2015-10-07 | Compiling again after refactoring. Haven't pushed to interpreter and lem yet | Kathy Gray | |
| 2015-10-07 | refactor type_internal | Kathy Gray | |
| 2015-10-07 | adapted pretty_print and rewriter to new tannot type | Christopher Pulte | |
| 2015-10-07 | Start expanding annot for more refined effect tracking | Kathy Gray | |
| 2015-10-07 | start changing representation of registers for ocaml | Kathy Gray | |
| 2015-10-06 | better printing for register writing, whole register (maybe not "right" yet) | Kathy Gray | |
| more library | |||
| 2015-10-06 | added the preliminary lem output option that for now uses ocaml pp | Christopher Pulte | |
| 2015-10-06 | fix generated message to have correct file extension | Christopher Pulte | |
| 2015-10-06 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-06 | fixes | Christopher Pulte | |
| 2015-10-06 | make let and case actually call pattern rewriter | Kathy Gray | |
| 2015-10-05 | made vector_concat pass remove typ annotation expression inside ↵ | Christopher Pulte | |
| vector_concat patterns, fixed a pp missing newline | |||
| 2015-10-05 | some fixes | Christopher Pulte | |
| 2015-10-05 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-10-05 | added pattern rewriting for DEF_val expressions | Christopher Pulte | |
| 2015-10-05 | More library functions | Kathy Gray | |
| Tweak to rewriter to actually rewrite function patterns | |||
| 2015-10-05 | added funcl pattern rewriting to remove vector concat patterns | Christopher Pulte | |
| 2015-10-04 | add find_updated_vars to support for-loops for lem or prover backend, add ↵ | Christopher Pulte | |
| normalise_exp exp that should transform expressions into a form where they can be embedded into monadic lem or prover definitions. Both untested | |||
| 2015-09-30 | Alias support for ocaml mode | Kathy Gray | |
| 2015-09-29 | capitalise and uncapitalise according to ocaml requirements | Kathy Gray | |
| 2015-09-29 | ml output passing simple test suite, except for register aliases | Kathy Gray | |
| Known todo: Write library functions in ocaml Properly upper-case/lower-case the first letter of names to conform to ocaml requirements Handle register aliases Turn id reads to dereferences for local ref variables | |||
| 2015-09-29 | Boiler plate to generate an ml file from a sail spec. Now debugging the ↵ | Kathy Gray | |
| output of such | |||
| 2015-09-28 | for loop variant without closure required | Kathy Gray | |
| 2015-09-28 | basic untested ocaml boiler plate | Kathy Gray | |
| 2015-09-28 | Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2 | Christopher Pulte | |
| 2015-09-28 | completed pp for E_for expressions, necessary OCaml foreach_inc and ↵ | Christopher Pulte | |
| foreach_dec declarations in comment | |||
| 2015-09-28 | Add initial support for register fields | Kathy Gray | |
| 2015-09-28 | tweak what the output expects | Kathy Gray | |
| 2015-09-28 | added rewriter rewrite_defs_remove_vector_concat that should get rid of ↵ | Christopher Pulte | |
| vector-concat patterns. Not tested. | |||
| 2015-09-25 | added something for remove_vector_string_patterns that for a give ↵ | Christopher Pulte | |
| pattern-match expression produces one without vector_concat patterns, plus a list of variable bindings for slices of the vector. Not finished yet | |||
| 2015-09-25 | added something for remove_vector_string_patterns that for a give ↵ | Christopher Pulte | |
| pattern-match expression produces one without vector_concat patterns, plus a list of variable bindings for slices of the vector. Not finished yet | |||
| 2015-09-25 | Potentially working ocaml mode, minus registers with fields, awaiting ↵ | Kathy Gray | |
| pattern-match rewriting | |||
| 2015-09-25 | building version of last change, removing stray ) | Kathy Gray | |
| 2015-09-25 | Rewrite expressions for ocaml, lifting assignment introductions into a ↵ | Kathy Gray | |
| special let form to set the scope | |||
| 2015-09-24 | Beginning of expression rewriter for ocaml | Kathy Gray | |
| 2015-09-24 | basic pattern rewriter | Kathy Gray | |
| 2015-09-24 | Parameterise the rewriter's for multiple different rewritings | Kathy Gray | |
| Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope | |||
| 2015-09-24 | added 'remove_vector_string_patterns and .._expressions functions | Christopher Pulte | |
| 2015-09-23 | More pretty printing | Kathy Gray | |
| A few more expressive tags for introducing mutable variables and for tracking local mutations A new pred for detecting bit vectors | |||
| 2015-09-22 | Start pretty printing ocaml for sequential | Kathy Gray | |
| 2015-09-17 | Type checker checking on case splits properly, and dependency ↵ | Kathy Gray | |
| transformations restored :) | |||
| 2015-09-06 | Turn off debug print outs | Kathy Gray | |
| 2015-09-06 | Improved type system, so that it catches int where there should be nat | Kathy Gray | |
| Note: the resulting Lem file generated may or may not actually work properly with the interpreter (i.e. it might have too many unknowns); still in the process of debugging some changes there. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |