| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-01 | update for lazy evaluation of typechecker debugging after rebase | Jon French | |
| 2018-05-01 | add type annotation patterns to mpats | Jon French | |
| 2018-05-01 | it works | Jon French | |
| 2018-05-01 | inferring is also required | Jon French | |
| 2018-05-01 | type-checking of calls to mappings, by synthing val-specs for the realised ↵ | Jon French | |
| functions early and then mimicing the overload machinery | |||
| 2018-05-01 | rewriting of builtin mappings e.g. int | Jon French | |
| 2018-05-01 | further progress but confounds the type checker? | Jon French | |
| 2018-05-01 | progress on debugging string pattern matching | Jon French | |
| 2018-05-01 | oops, not every pattern is in fact string_typ, remember to pass through the ↵ | Jon French | |
| original type in rewrite_defs_pat_string_append when not doing anything | |||
| 2018-05-01 | create a single funcl with a match, rather than converting mapcls to funcls, ↵ | Jon French | |
| because OCaml among others doesn't allow top-level guards | |||
| 2018-05-01 | further progress | Jon French | |
| 2018-05-01 | fv funcs for bidir types | Jon French | |
| 2018-05-01 | mostly added mappings to type-checker and pretty-printer | Jon French | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |