| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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) | |||
| 2018-04-10 | Porting some minisail changes to sail2 branch | Alasdair Armstrong | |
| This commit primarily changes how existential types are bound in letbindings. Essentially, the constraints on both numeric and existentially quantified types are lifted into the surrounding type context automatically, so in ``` val f : nat -> nat let x = f(3) ``` whereas x would have had type nat by default before, it'll now have type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh type variable). This has several advantages: x can be passed to functions expecting an atom argument, such as a vector indexing operation without any clunky cast functions - ex_int, ex_nat, and ex_range are no longer required. The let 'x = something() syntax is also less needed, and is now only really required when we specifically want a name to refer to x's type. This changes slightly the nature of the type pattern syntax---whereas previously it was used to cause an existential to be destructured, it now just provides names for an automatically destructured binding. Usually however, this just works the same. Also: - Fixed an issue where the rewrite_split_fun_constr_pats rewriting pass didn't add type paramemters for newly added type variables in generated function parameters. - Updated string_of_ functions in ast_util to reflect syntax changes - Fixed a C compilation issue where elements of union type constructors were not being coerced between big integers and 64-bit integers where appropriate - Type annotations in patterns now generalise, rather than restrict the type of the pattern. This should be safer and easier to handle in the various backends. I don't think any code we had was relying on this behaviour anyway. - Add inequality operator to lib/flow.sail - Fix an issue whereby top-level let bindings with annotations were checked incorrectly | |||
| 2018-04-10 | Avoid rejecting reasonable pattern matches in monomorphisation | Brian Campbell | |
| (when they're not relevant) | |||
| 2018-04-10 | Add basic reference support to monomorphisation | Brian Campbell | |
| 2018-04-09 | Remove unnecessary restriction on complex nexp rewriting | Brian Campbell | |
| 2018-04-09 | Stop vector_typ_args_of from failing when order is a variable | Brian Campbell | |
| Now it just returns the actual arguments and a separate function calculates the start index when required. | |||
| 2018-04-06 | Fix some error msg typos. | Prashanth Mundkur | |
| 2018-04-06 | Generate better tyvar names for complex nexps in monomorphisation | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |