summaryrefslogtreecommitdiff
path: root/src/rewriter.mli
AgeCommit message (Expand)Author
2020-09-29Refactor: Change AST type from a union to a structAlasdair
2020-09-28Refactor: Rename 'a defs to 'a astAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-04-21Be more careful about type annotations in rewrites to LemThomas Bauereiss
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-01-14Add a function to perform re-writes in parallelAlasdair
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2018-12-04Remove FES_Fexps constructorAlasdair Armstrong
2018-08-24Fix rewriter issuesAlasdair Armstrong
2018-08-23Move vector_string_to_bit_list from its odd place in Rewriter.rewrite_pat to ...Jon French
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian Campbell
2018-07-26Patterns: add or and not patternsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-04Add support for top-level values to monomorphisation singleton rewriteBrian Campbell
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-05-02refactor string append pattern ast to be based on lists rather than pairsJon French
2018-05-01start of string pattern matching: currently only literalsJon French
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-03Lots of experimental changes on this branchAlasdair Armstrong
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:06:42 +0000