summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-05-09Fix printing of hex strings in LemThomas Bauereiss
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-09Add more annotations for loop bounds in Lem rewritingThomas Bauereiss
2018-05-09Run ARM built-in tests for Lem backend (via OCaml)Thomas Bauereiss
2018-05-09Support short-circuiting of Boolean expressions in LemThomas Bauereiss
2018-05-09Generate initial register state recordThomas Bauereiss
2018-05-09allow empty brackets to pass unit to sub-mpatsJon French
2018-05-09Fix Byte_sequence errors due to linksem updateemersion
2018-05-08fixed sub-mappingsJon French
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
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-04Add support for top-level values to monomorphisation singleton rewriteBrian Campbell
2018-05-04Fix mono cast introduction to avoid a checking to inference changeBrian Campbell
2018-05-04Start updating monomorphisationBrian Campbell
2018-05-04Rename type vars in Coq backend when they clash with identifiersBrian Campbell
2018-05-04Basic Coq constraintsBrian Campbell
2018-05-03Flow typing and l-expression changes for ASL parserAlasdair Armstrong
2018-05-03Add typing rule for checking tuples as well as inferring themAlasdair Armstrong
2018-05-03Fix interpreter messages for failing assertsAlasdair 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-03Work in progress on the coq backendBrian Campbell
2018-05-02scattered mappingsJon French
2018-05-02re-indent to_ast_defJon French
2018-05-02refactor string append pattern ast to be based on lists rather than pairsJon French
2018-05-01update for lazy evaluation of typechecker debugging after rebaseJon French
2018-05-01add type annotation patterns to mpatsJon French
2018-05-01it worksJon French
2018-05-01inferring is also requiredJon French
2018-05-01type-checking of calls to mappings, by synthing val-specs for the realised fu...Jon 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-01fv funcs for bidir typesJon French
2018-05-01mostly added mappings to type-checker and pretty-printerJon French
2018-05-01utils mapping over mpats/mpexpsJon French
2018-05-01conversion from parse_ast to astJon French
2018-05-01add to parserJon French
2018-05-01add mpats to astsJon French
2018-05-01re-indent Initial_check.to_ast_typJon 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-01add { ~~fieldname } sugar to record patterns, expanding to { fieldname = fiel...Jon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 06:22:05 +0000