summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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
2018-06-25Check for variables in disjointness checkThomas Bauereiss
2018-06-25Fix a bug in pattern guard rewritingThomas Bauereiss
2018-06-11add 'pat as id' mapping-patternsJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-05-21fix bug in rewrite_defs_mapping_patterns where pattern-uses of mappings with ...Jon French
2018-05-18Fix bug in rewriting variable updatesThomas Bauereiss
2018-05-18temporary HACK for aarch64: make rewrite_defs_pat_lits ignore stringsJon French
2018-05-18more riscv mappings; riscv now builds successfully to lem which builds to isa...Jon French
2018-05-17fix bug in rewrite_defs_pat_string_append -- make it pass types through corre...Jon French
2018-05-16Add support for inline val-spec declaration for mappingsJon French
2018-05-15reorder lem rewrite passes and explicitly remove mapping valspecs; string stu...Jon French
2018-05-15rewrite_defs_guarded_pats: guards deserve rewriting tooJon French
2018-05-14make debug printing of realised mappings both optional and lazyJon French
2018-05-11support for mapping-patterns inside (should be) all other pattern typesJon French
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-10generalise string pattern matching to arbitrary arguments rather than just an...Jon French
2018-05-09Add more annotations for loop bounds in Lem rewritingThomas Bauereiss
2018-05-09Support short-circuiting of Boolean expressions in LemThomas Bauereiss
2018-05-08fixed sub-mappingsJon French