summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:49:17 +0000