summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
2018-11-19Don't re-check AST repeatedly in exp_lift_assign re-writeAlasdair Armstrong
2018-11-19Ensure sizeof re-writing occurs for configuration registersAlasdair Armstrong
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-10-31Add rewriting pass for not-patternsAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-31Improve error messages for unsolved function quantifiersAlasdair Armstrong
2018-10-22Coq: work around constructors with tupled argumentsBrian Campbell
2018-10-16rewrites: remove now-unnecessary temporary string hack from rewrite_defs_pat_...Jon French
2018-10-11Change the function type in the ASTAlasdair
2018-10-04rename stringappend ids for more readable generated codeJon French
2018-10-01Extend Coq pattern match completeness rewrite to let patternsBrian Campbell
2018-10-01New rewriting pass toplevel_string_appendJon French
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-19rewrite_defs_pat_string_append: fix bug with guarded SomeJon French
2018-09-17Rewrites.rewrite_defs_mapping_patterns: emit an explicit type annotation on t...Jon French
2018-09-13C: Fix an issue with assigning to unitialized variables at end of blocksAlasdair Armstrong
2018-09-12Jenkins: Fix deprecation warningsAlasdair Armstrong
2018-09-04Add a rewrite to minimise the number of functions marked as recursiveBrian Campbell
2018-08-31rewrite_defs_pat_string_append: only guard the innermost recursive pattern, a...Jon French
2018-08-31mappings: Support for unidirectional mapping clausesJon French
2018-08-28add __POS__ argument to Err_unreachable for better error reportingJon French
2018-08-24Fix rewriter issuesAlasdair Armstrong
2018-08-24support for P_or and P_not patterns in rewrite_defs_mapping_patternsJon French
2018-08-24rewrite_defs_mapping_patterns: support for referring to mapping arguments in ...Jon French
2018-08-24pat_to_exp support for vector and string concat patterns; fix typing in exp_o...Jon French
2018-08-24rewrite_defs_pat_lits: rewrite away fewer lits when generating ocaml, for cle...Jon French
2018-08-23Fix interpreter after re-writer changeAlasdair Armstrong
2018-08-23Move vector_string_to_bit_list from its odd place in Rewriter.rewrite_pat to ...Jon French
2018-08-22Fix a bug in nested vector concatenation patternsAlasdair Armstrong
2018-08-22Revert "rewrite_defs_pat_lits: add an explicit type annotation around generat...Jon French
2018-08-22rewrite_defs_pat_lits: add an explicit type annotation around generated id pa...Jon French
2018-08-17Extend guarded patterns rewriting to exception catchingBrian Campbell
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-13Coq: drop redundant final wildcard clausesBrian Campbell
2018-08-13Guarded clauses rewrite: variable patterns subsume enumsBrian Campbell
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian Campbell
2018-08-07Fix propagation of overly-specific types in early_return rewriteBrian Campbell
2018-07-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-27Coq: patterns on bit literalsBrian Campbell
2018-07-26Patterns: add or and not patternsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-07-12Fix bug for large integers in OCaml compilationAlasdair Armstrong
2018-07-09Fix bug in rewriting of try-catch-blocks with variable updatesThomas Bauereiss
2018-07-09Tweak rewriting of literal patterns for LemThomas Bauereiss
2018-07-09Add explanatory comment to guard rewritingThomas Bauereiss
2018-07-03Fix letbind_effects on LEXP_deref with an effectful subexpressionBrian Campbell
2018-06-26In guarded pattern rewriting, irrefutable patterns subsume wildcardsBrian Campbell