summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
AgeCommit message (Expand)Author
2019-01-14Add a function to perform re-writes in parallelAlasdair
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-26More cleanupAlasdair Armstrong
2018-12-26Some cleanupAlasdair Armstrong
2018-12-13Merge remote-tracking branch 'origin/sail2' into asl_flowAlasdair
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
2018-12-07Working on better flow typing for ASLAlasdair Armstrong
2018-12-04Remove FES_Fexps constructorAlasdair Armstrong
2018-11-30Remove constraint synonymsAlasdair Armstrong
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-31Improve error messages for unsolved function quantifiersAlasdair Armstrong
2018-08-28add __POS__ argument to Err_unreachable for better error reportingJon French
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-18Correctly specialise type annotation in polymorphic functionsAlasdair
2018-08-17Extend guarded patterns rewriting to exception catchingBrian Campbell
2018-08-07Revert "Warnings: deal with all the deprecation warnings"Alasdair Armstrong
2018-07-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-26Some tweaks to not and or patternsAlasdair Armstrong
2018-07-26Patterns: add or and not patternsAlastair Reid
2018-07-26Warnings: deal with all the deprecation warningsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-06-26Add configuration registers so __SetConfig ASL can be translatedAlasdair Armstrong
2018-05-10Merge branch 'sail2' into mappingsJon French
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-01mostly added mappings to type-checker and pretty-printerJon 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:37:05 +0000