summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2015-10-20ocaml output now produces parsing power.sailKathy Gray
2015-10-20more fixesKathy Gray
2015-10-20Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-20compiling prettyprinterKathy Gray
2015-10-20Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-20fix a-normalisation bugChristopher Pulte
2015-10-20Fixing bugs in pretty printer to ocamlKathy Gray
2015-10-19progress on lem backendChristopher Pulte
2015-10-17clean up, more readabilityChristopher Pulte
2015-10-17a-normalisation for lem backendChristopher Pulte
2015-10-13Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-13some progress on sequentialise_effectsChristopher Pulte
2015-10-13Refine local vs cumulative effects for lexpKathy Gray
More ocaml output, better treatment of registers.
2015-10-12fixesChristopher Pulte
2015-10-12apply rewriter changes to master as wellChristopher Pulte
2015-10-08augment annot of interpreterKathy Gray
2015-10-07Compiling again after refactoring. Haven't pushed to interpreter and lem yetKathy Gray
2015-10-07refactor type_internalKathy Gray
2015-10-07adapted pretty_print and rewriter to new tannot typeChristopher Pulte
2015-10-07Start expanding annot for more refined effect trackingKathy Gray
2015-10-07start changing representation of registers for ocamlKathy Gray
2015-10-06better printing for register writing, whole register (maybe not "right" yet)Kathy Gray
more library
2015-10-06added the preliminary lem output option that for now uses ocaml ppChristopher Pulte
2015-10-06fix generated message to have correct file extensionChristopher Pulte
2015-10-06Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-06fixesChristopher Pulte
2015-10-06make let and case actually call pattern rewriterKathy Gray
2015-10-05made vector_concat pass remove typ annotation expression inside ↵Christopher Pulte
vector_concat patterns, fixed a pp missing newline
2015-10-05some fixesChristopher Pulte
2015-10-05Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-05added pattern rewriting for DEF_val expressionsChristopher Pulte
2015-10-05More library functionsKathy Gray
Tweak to rewriter to actually rewrite function patterns
2015-10-05added funcl pattern rewriting to remove vector concat patternsChristopher Pulte
2015-10-04add 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-30Alias support for ocaml modeKathy Gray
2015-09-29capitalise and uncapitalise according to ocaml requirementsKathy Gray
2015-09-29ml output passing simple test suite, except for register aliasesKathy 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-29Boiler plate to generate an ml file from a sail spec. Now debugging the ↵Kathy Gray
output of such
2015-09-28for loop variant without closure requiredKathy Gray
2015-09-28basic untested ocaml boiler plateKathy Gray
2015-09-28Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-09-28completed pp for E_for expressions, necessary OCaml foreach_inc and ↵Christopher Pulte
foreach_dec declarations in comment
2015-09-28Add initial support for register fieldsKathy Gray
2015-09-28tweak what the output expectsKathy Gray
2015-09-28added rewriter rewrite_defs_remove_vector_concat that should get rid of ↵Christopher Pulte
vector-concat patterns. Not tested.
2015-09-25added 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-25added 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-25Potentially working ocaml mode, minus registers with fields, awaiting ↵Kathy Gray
pattern-match rewriting
2015-09-25building version of last change, removing stray )Kathy Gray
2015-09-25Rewrite expressions for ocaml, lifting assignment introductions into a ↵Kathy Gray
special let form to set the scope
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:52:59 +0000