| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-01 | utils mapping over mpats/mpexps | Jon French | |
| 2018-05-01 | conversion from parse_ast to ast | Jon French | |
| 2018-05-01 | add to parser | Jon French | |
| 2018-05-01 | add mpats to asts | Jon French | |
| 2018-05-01 | re-indent Initial_check.to_ast_typ | Jon French | |
| 2018-05-01 | starting to also do integer support | Jon French | |
| 2018-05-01 | starting to also do integer support | Jon French | |
| 2018-05-01 | start of string pattern matching: currently only literals | Jon French | |
| 2018-05-01 | fix refactored rewrite_pexp_with_guards (where type information is and is ↵ | Jon French | |
| not...) | |||
| 2018-05-01 | add { ~~fieldname } sugar to record patterns, expanding to { fieldname = ↵ | Jon French | |
| fieldname }\n\nCan't use ~ for this to be exactly like OCaml, as is used for 'not' and explicitly allowed as an identifier | |||
| 2018-05-01 | more refactoring of pexp rewriters | Jon French | |
| 2018-05-01 | Type_check: factor rewrite_pexps_with_guards out of rewrite_defs_pat_lits | Jon French | |
| 2018-05-01 | tidy | Jon French | |
| 2018-05-01 | Use a naming scheme rather than random fresh ids for union anonymous records | Jon French | |
| 2018-05-01 | fix warnings | Jon French | |
| 2018-05-01 | Add anonymous record arms to unions | Jon French | |
| (Preprocessed into a real record type with a fresh id and a reference to that generated record type.) | |||
| 2018-04-26 | Lem: Add Size class annotations for nested bitvector types | Thomas Bauereiss | |
| 2018-04-26 | Fix bug in rewriting of loops | Thomas Bauereiss | |
| Take into account existential types when determining bounds for the loop variable | |||
| 2018-04-26 | Avoid adding explicit type annotations with generated type variables | Thomas Bauereiss | |
| 2018-04-26 | Make effect propagation in rewriter more efficient | Thomas Bauereiss | |
| Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect, assuming that the effects of subexpressions have already been fixed by the recursive calls of the rewriter. | |||
| 2018-04-26 | Lazily evaluate debugging messages | Thomas Bauereiss | |
| This is meant to increase performance; for example, generating debug messages that include pretty-printed expressions can be very costly, if those expressions are complex (e.g. deeply nested E_internal_plet nodes representing a long sequence of monadic binds). | |||
| 2018-04-26 | Add a new SHARE_DIR argument to use when doing opam build. For non-opam ↵ | Robert Norton | |
| builds this defaults to git root. | |||
| 2018-04-26 | Make ocamlbuild assume lem is in path instead of relative to current directory. | Robert Norton | |
| 2018-04-26 | Opam packaging: add install and uninstall targets and code to find various ↵ | Robert Norton | |
| files in installed location. | |||
| 2018-04-26 | Remove obsolete mips/cheri rules from sail makefile. These are now built in ↵ | Robert Norton | |
| their respective subdirectories. | |||
| 2018-04-25 | Simplify subtyping check | Alasdair Armstrong | |
| This should make subtyping work better for tuples containing constrained types. Removes the intermediate type-normal-form representation from the subtyping check, and replaces it with Env.canonicalize from the canonical branch. | |||
| 2018-04-25 | Start working on documentation | Alasdair Armstrong | |
| 2018-04-23 | Merge branch 'rmn30_latex' into sail2 | Robert Norton | |
| 2018-04-20 | Allow instantiation of type or order type variables without kind declaration | Brian Campbell | |
| 2018-04-20 | Have sign_extend in common Sail Lem library, use it and zero_extend in | Brian Campbell | |
| mono rewrites | |||
| 2018-04-19 | Gloss over UInt/unsigned name difference in monomorphisation | Brian Campbell | |
| 2018-04-19 | Fix bug with function being applied to tuples | Alasdair Armstrong | |
| For some reason there was a desugaring rule that mapped f((x, y)) to f(x, y) in initial_check.ml, this prevented functions and constructors from being applied to tuples. | |||
| 2018-04-18 | Add first draft of Isabelle library documentation | Thomas Bauereiss | |
| 2018-04-18 | Fix bug in pretty-printing loops to Lem | Thomas Bauereiss | |
| 2018-04-18 | Add some lemmas about bitvectors | Thomas Bauereiss | |
| Also clean up some library functions a bit, and add some missing failure handling variants of division operations on bitvectors. | |||
| 2018-04-18 | Move a few printing functions to sail_values.lem | Thomas Bauereiss | |
| They are used in various specs and test cases. | |||
| 2018-04-18 | Fix another reference to BK_nat | Alastair Reid | |
| 2018-04-18 | Fix build on linux | Alasdair Armstrong | |
| Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't allow a space after the -i option. | |||
| 2018-04-18 | Port to Mac: BSD sed != GNU sed | Alastair Reid | |
| For GNU sed, the extension is optional in sed -i ... But in BSD sed, the extension is mandatory sed -i .bak ... | |||
| 2018-04-18 | Move Lem shl_int, shr_int implementations from aarch64_extras to sail lib | Brian Campbell | |
| (note that they're already declared in lib/arith.sail) | |||
| 2018-04-18 | add some experimental support for latex output in multiple files. | Robert Norton | |
| 2018-04-18 | Rename BK_nat to BK_int to be consistent with source syntax | Alasdair Armstrong | |
| 2018-04-18 | Updates to latex mode for documentation | Alasdair Armstrong | |
| 2018-04-17 | Fix slicing in constant propagation | Brian Campbell | |
| 2018-04-17 | Move some Lem library vector operations so that we also have mword versions | Brian Campbell | |
| 2018-04-13 | Check all patterns inside functions with -dsanity | Brian Campbell | |
| 2018-04-12 | Fill in some minor missing cases in monomorphisation | Brian Campbell | |
| 2018-04-11 | Avoid unnecessary rechecking in remove numeral pats rewrite | Brian Campbell | |
| (especially as the environment previously used was a bit dodgy) | |||
| 2018-04-11 | Use more robust method of finding deps of new tyvars in mono analysis | Brian Campbell | |
| 2018-04-11 | Make the atom to singleton type rewriter replace literals with guards | Brian Campbell | |
| (previously the typechecker did this for all literal patterns, but now it's only necessary for the rewritten arguments) | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |