summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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
2018-05-04Checked that variable names in split_fun rewrites are really variablesBrian Campbell
2018-05-04Fix missing nexp id rewritingBrian Campbell
2018-05-04Rewrite constant nexps in specsBrian Campbell
2018-05-03Flow typing and l-expression changes for ASL parserAlasdair Armstrong
2018-05-03support sub-mappings in string-append-patternsJon French
2018-05-03synthesise string-prefix-check functions for mappings where either side is st...Jon French
2018-05-02scattered mappingsJon French
2018-05-02refactor string append pattern ast to be based on lists rather than pairsJon French
2018-05-01add type annotation patterns to mpatsJon French
2018-05-01rewriting of builtin mappings e.g. intJon French
2018-05-01further progress but confounds the type checker?Jon French
2018-05-01progress on debugging string pattern matchingJon French
2018-05-01oops, not every pattern is in fact string_typ, remember to pass through the o...Jon French
2018-05-01create a single funcl with a match, rather than converting mapcls to funcls, ...Jon French
2018-05-01further progressJon French
2018-05-01starting to also do integer supportJon French
2018-05-01starting to also do integer supportJon French
2018-05-01start of string pattern matching: currently only literalsJon French
2018-05-01fix refactored rewrite_pexp_with_guards (where type information is and is not...Jon French
2018-05-01more refactoring of pexp rewritersJon French
2018-05-01Type_check: factor rewrite_pexps_with_guards out of rewrite_defs_pat_litsJon French
2018-04-26Fix bug in rewriting of loopsThomas Bauereiss
2018-04-26Avoid adding explicit type annotations with generated type variablesThomas Bauereiss
2018-04-26Make effect propagation in rewriter more efficientThomas Bauereiss
2018-04-18Rename BK_nat to BK_int to be consistent with source syntaxAlasdair Armstrong
2018-04-13Check all patterns inside functions with -dsanityBrian Campbell
2018-04-11Avoid unnecessary rechecking in remove numeral pats rewriteBrian Campbell
2018-04-10Porting some minisail changes to sail2 branchAlasdair Armstrong
2018-04-09Stop vector_typ_args_of from failing when order is a variableBrian Campbell
2018-03-22Try removing superfluous returns more aggressively for LemThomas Bauereiss
2018-03-14Fix compilation for OCaml 4.02Thomas Bauereiss
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss