summaryrefslogtreecommitdiff
path: root/src/rewriter.mli
AgeCommit message (Expand)Author
2017-12-07More OCaml test casesAlasdair Armstrong
2017-12-06Add top-level pattern match guards internallyBrian Campbell
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-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
2017-11-10Fixed some tricky typechecking bugsAlasdair Armstrong
2017-11-01Support bitvector-size-parametric functions in Lem outputBrian Campbell
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-18Fixes and updates to ocaml backend to compile aarch64_no_vectorAlasdair Armstrong
2017-10-13Improve debugging outputThomas Bauereiss
2017-10-04Merge branch 'cleanup' into experimentsAlasdair Armstrong
2017-10-03Fixes to new parserAlasdair Armstrong
2017-09-26Added while-do and repeat-until loops to sail for translating ASLAlasdair Armstrong
2017-09-21Simplify AST by removing LB_val_explicit and replace LB_val_implicit with jus...Alasdair Armstrong
2017-09-21Cleaning up the AST and removing redundant and/or unused nodesAlasdair Armstrong
2017-08-17Add E_constraint support to re-writerAlasdair Armstrong
2017-08-17Various sail fixes for ASL hexapodAlasdair Armstrong
2017-08-10Add support for early return to Lem backendThomas Bauereiss
2017-08-02Add debugging option to dump AST after rewriting stepsThomas Bauereiss
2017-07-27Add cons patterns to pretty-printersThomas Bauereiss
2017-07-21Everything moved to new typecheckerAlasdair Armstrong
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
2017-07-12Add checks for variable identifiers in pattern subsumptionThomas Bauereiss
2017-02-03fix headersPeter Sewell
2016-09-19sail-to-lem progressChristopher Pulte
2016-08-14Start adding form for (a,b,c) := foo()Kathy Gray
2016-07-23Add a return exp form to Sail, supported in type checker and in interpreter.Kathy Gray
2016-01-07Add E_assert to basic rewritersKathy Gray
2015-11-05some progress on lem backend: rewrite away mutable variable assignments, rewr...Christopher Pulte
2015-10-26Switch name set to name map to include type and expression dataKathy Gray
2015-10-26Add variable set to rewritersKathy Gray
2015-10-19progress on lem backendChristopher Pulte
2015-10-06added the preliminary lem output option that for now uses ocaml ppChristopher Pulte
2015-10-04add find_updated_vars to support for-loops for lem or prover backend, add nor...Christopher Pulte
2015-09-24Beginning of expression rewriter for ocamlKathy Gray
2015-09-24Parameterise the rewriter's for multiple different rewritingsKathy Gray
2015-09-17Type checker checking on case splits properly, and dependency transformations...Kathy Gray
2015-02-13Actually use new dependency information in generation of lem/etc.Kathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:05:49 +0000