summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-01-10Add an all_split_errors optionBrian Campbell
2018-01-10Fix control dependencies in monomorphisation analysisBrian Campbell
2018-01-09More monomorphisation rewrites for aarch64Brian Campbell
2018-01-09Tidy up monomorphisation interfaceBrian Campbell
2018-01-09Proper location for no set constraint errorsBrian Campbell
2018-01-09Move reordering in alpha_equivalent before relabelling to giveBrian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
2018-01-08Improved fix for alpha-equivalence re-ordering issueAlasdair Armstrong
2018-01-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2018-01-08Potential fix for bug where different quantifer order in existentials will br...Alasdair Armstrong
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-19Add rewriting step for numeral patternsThomas Bauereiss
2017-12-19Fix a bug in untupling function arguments for LemThomas Bauereiss
2017-12-18Clean up last commitBrian Campbell
2017-12-18Handle multiple -lem_lib optionsBrian Campbell
2017-12-14Un-tuple function arguments when pretty-printing to LemThomas Bauereiss
2017-12-14Make sequential and mwords global variables in Lem pretty-printerThomas Bauereiss
2017-12-12Add a few helper functions for bit listsThomas Bauereiss
2017-12-12Make mono analysis fail properly on effectful functionsBrian Campbell
2017-12-11Remove some duplication from monomorphisation analysis failure reportsBrian Campbell
2017-12-07More OCaml test casesAlasdair Armstrong
2017-12-07Fix boolean literal constraintsAlasdair Armstrong
2017-12-07Fix regressions in OCaml outputAlasdair Armstrong
2017-12-07Support monomorphisation with set constrained integersBrian Campbell
2017-12-07Resolve function clause guard parsing ambiguity by requiring parenthesesBrian Campbell
2017-12-07Functions with guards changes in rewritesBrian Campbell
2017-12-06Add parsing for guards in function clausesBrian Campbell
2017-12-06Remove filename mangling in monomorphisationBrian Campbell
2017-12-06Rework case checking to only introduce guards when necessaryBrian Campbell
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-12-05Pretty printer now prints operator precedence correctly.Alasdair Armstrong
2017-12-04Fix warnings in test suiteAlasdair Armstrong
2017-11-30Use doc_typdef_lem from experimentsAlasdair Armstrong
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-30Improvements to enable parsing and checking intermediate rewritingAlasdair Armstrong
2017-11-29Better lem_ast tagging and interpreter tweaksAlasdair Armstrong
2017-11-29Switched to bytecode compiler for executing interpreter to avoid stack overflowAlasdair Armstrong
2017-11-29Fix lem_ast output bugsAlasdair Armstrong
2017-11-29Added location information for fixity and overloads in ast_util.mlAlasdair Armstrong
2017-11-28Make pretty printer able to print several internal constructs for debuggingAlasdair Armstrong
2017-11-28Small update to trivial sizeof rewrites so we can handle all cases inAlasdair Armstrong
2017-11-28Fix issue where statements in blocks had incorrect environmentsAlasdair Armstrong
2017-11-27Utility functions in ast_util for asl_parserAlasdair Armstrong
2017-11-27Split rewriter into separate rewriting library and rewrite passesAlasdair Armstrong
2017-11-27Use guards from when patterns when typing casesBrian Campbell
2017-11-27Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong