summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
AgeCommit message (Expand)Author
2018-05-04Rename type vars in Coq backend when they clash with identifiersBrian Campbell
2018-05-03Flow typing and l-expression changes for ASL parserAlasdair Armstrong
2018-04-26Avoid adding explicit type annotations with generated type variablesThomas Bauereiss
2018-04-26Make effect propagation in rewriter more efficientThomas Bauereiss
2018-02-16Avoid nested explicit type annotationsThomas Bauereiss
2018-02-05Add typ patterns for destructuring existentialsAlasdair Armstrong
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-12OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.Alasdair Armstrong
2018-01-03Lots of experimental changes on this branchAlasdair Armstrong
2018-01-02Experimenting with power specAlasdair Armstrong
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-14Fix all compiler warning except in lem pretty printer and monomorphisationAlasdair Armstrong
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-07More OCaml test casesAlasdair Armstrong
2017-12-07Fix regressions in OCaml outputAlasdair Armstrong
2017-12-06Add top-level pattern match guards internallyBrian Campbell
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
2017-12-05Better support for exceptions in sail for ASL specs that need them.Alasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-27Split rewriter into separate rewriting library and rewrite passesAlasdair Armstrong
2017-11-27Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-11-27Compile assertions into OCamlAlasdair Armstrong
2017-11-27Fix bitvector pattern removal typoBrian Campbell
2017-11-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
2017-11-16Remove unused Typ_wild constructorAlasdair Armstrong
2017-11-10Fixed some tricky typechecking bugsAlasdair Armstrong
2017-11-07Fix typo in constraint rewriterThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
2017-11-03Fixed a bug where true and false get mixed up in rewriterAlasdair Armstrong
2017-11-02Optionally generate an initial register state for the sequential Lem shallow ...Thomas Bauereiss
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
2017-10-31Remove redundant nexp simplification functionThomas Bauereiss
2017-10-26Unfold nexp abbreviations for pretty-printingThomas Bauereiss
2017-10-26Update val specs after rewriting functionsThomas Bauereiss
2017-10-25Allow mutually recursive functionsThomas Bauereiss
2017-10-24Generate undefined_bitvector function when targeting machine wordsBrian Campbell
2017-10-19Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-10-19Rewrite undefined values, add type annotations to early returnsThomas Bauereiss
2017-10-19Preserve more type environment information during rewritingThomas Bauereiss
2017-10-18Fixes and updates to ocaml backend to compile aarch64_no_vectorAlasdair Armstrong
2017-10-13Fix some bugs that surfaced in the ASL exportThomas Bauereiss
2017-10-13Add rewriting step for tuple-vector assignmentsThomas Bauereiss
2017-10-13Add rewriting step for function effect propagationThomas Bauereiss
2017-10-13Improve debugging outputThomas Bauereiss
2017-10-09Improvements to menhir pretty printer and ocaml backendAlasdair Armstrong
2017-10-04Merge branch 'cleanup' into experimentsAlasdair Armstrong
2017-10-03Fixes to new parserAlasdair Armstrong
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:16:23 +0000