| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-02 | Modified loop typechecking code to generate a new type variable for the loop ↵ | Alasdair Armstrong | |
| index, seems to work better for complex cases in ASL | |||
| 2017-08-01 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-08-01 | Added more patterns to ast_util and improved type checking of patterns | Alasdair Armstrong | |
| 2017-08-01 | Modified the typechecker for ASL generation | Alasdair Armstrong | |
| 2017-08-01 | Remove some hardcoded calls to obsolete Lem library functions | Thomas Bauereiss | |
| 2017-08-01 | Fix some effect propagation bugs in rewriter | Thomas Bauereiss | |
| 2017-07-31 | Fixed a bug in the pretty printer that caused ASL parser to output ↵ | Alasdair Armstrong | |
| unparseable sail code | |||
| 2017-07-31 | Changed behavior of return to better match ASL | Alasdair Armstrong | |
| 2017-07-31 | Removed redundant code in infer_funapp' | Alasdair Armstrong | |
| 2017-07-31 | Fixed bug in existential return types | Alasdair Armstrong | |
| 2017-07-28 | Mips TLB existential example | Alasdair Armstrong | |
| 2017-07-28 | Fix break caused by merge | Alasdair Armstrong | |
| 2017-07-28 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-07-28 | Add true and false to n_constraint language. Also small tweaks for ASL ↵ | Alasdair Armstrong | |
| generation. | |||
| 2017-07-27 | Rewrite guarded patterns for Lem backend | Thomas Bauereiss | |
| 2017-07-27 | Add cons patterns to pretty-printers | Thomas Bauereiss | |
| 2017-07-27 | Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| sail_new_tc | |||
| 2017-07-27 | Parameterise convert_ast by the bitvector order | Alasdair Armstrong | |
| 2017-07-27 | Fixed a bug where sail would run out of file descriptors when passed a large ↵ | Alasdair Armstrong | |
| number of files | |||
| 2017-07-27 | P_cons in monomorphisation | Brian Campbell | |
| 2017-07-27 | Fix up constructor handling in monomorphisation | Brian Campbell | |
| 2017-07-27 | Mirror AST change | Brian Campbell | |
| 2017-07-27 | Allow local mutable records, and fix bugs with overlapping record field names. | Alasdair Armstrong | |
| 2017-07-27 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| 2017-07-27 | Fixed bug with pattern synonyms in Cons and List patterns | Alasdair Armstrong | |
| 2017-07-27 | Fixed some bugs with existentials, and added test cases | Alasdair Armstrong | |
| 2017-07-27 | Fixed pretty printer for existentials | Alasdair Armstrong | |
| Also fixed substitution functions so as to not substitute captured kind identifiers | |||
| 2017-07-26 | More work on existentials in function calls | Alasdair Armstrong | |
| 2017-07-26 | Experimental existentials in function calls | Alasdair Armstrong | |
| 2017-07-26 | Experiment in adding existential types | Alasdair Armstrong | |
| 2017-07-26 | Added syntax for existential types | Alasdair Armstrong | |
| 2017-07-26 | Add right shift to lib/prelude.sail, and add case for E_exit in ↵ | Alasdair Armstrong | |
| Ast_util.string_of_exp | |||
| 2017-07-26 | Allow arbitrary identifiers in nexp expressions | Alasdair Armstrong | |
| Fixed some bugs in the initial check that caused valid code to fail to parse Add a nid utility function that creates an id n-expression, similar to nvar, nconstant etc | |||
| 2017-07-26 | Merge remote-tracking branch 'origin/master' into sail_new_tc | Alasdair Armstrong | |
| 2017-07-26 | Improve rewriting of sizeof expressions | Thomas Bauereiss | |
| If some type-level variables in a sizeof expression in a function body cannot be directly extracted from the parameters of the function, add a new parameter for each unresolved parameter, and rewrite calls to the function accordingly | |||
| 2017-07-26 | Merge | Thomas Bauereiss | |
| 2017-07-25 | Fixed bug where strings were not escaped correctly within string | Alasdair Armstrong | |
| literals when pretty printing sail. | |||
| 2017-07-25 | Add instantiation_of helper function to type_check.mli that returns | Alasdair Armstrong | |
| the instantiated type variables in a function application | |||
| 2017-07-25 | Improved l-expressions | Alasdair Armstrong | |
| - Fixed a bug where some l-expressions which wrote registers wern't picking up register writes. - Can now write to registers with record types. e.g. ARM's ProcState record from ASL. | |||
| 2017-07-25 | Add partial support for rewriting of sizeof expressions | Thomas Bauereiss | |
| Tries to extract values of nexps from the (type annotations of) parameters passed to the function. This seems to correspond to the behaviour of the previous typechecker. | |||
| 2017-07-24 | interpreter: optionally print debugging traces | Jon French | |
| 2017-07-24 | vector parts of interpreter now evaluate all arguments of expression before ↵ | Jon French | |
| exiting due to one of them being unknown; fixes incorrect exhaustive analysis for footprints | |||
| 2017-07-24 | move value type definitions to ott, and introduce new E_internal_value ast ↵ | Jon French | |
| node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node | |||
| 2017-07-24 | Added cons patterns to sail | Alasdair Armstrong | |
| See test/typecheck/pass/cons_pattern.sail for an example. Also cleaned up the propagating effects code by making some of the variable names less verbose | |||
| 2017-07-24 | Separate monomorphisation from top-level type checking | Brian Campbell | |
| 2017-07-24 | Remove monomorphisation for old type checker | Brian Campbell | |
| 2017-07-24 | Tidy comments in monomorphisation | Brian Campbell | |
| 2017-07-21 | Everything moved to new typechecker | Alasdair Armstrong | |
| Modified initial_check.ml so it no longer requires type_internal. It's still needs cleaned up in a few ways. Most of the things it's trying to do could be done nicer if we took some time to re-factor it, and some of the things should just be handled by the main typechecker, leaving it as a think layer between the parse_ast and the ast. Now that's done everything can be switched to the new typechecker and the _new suffixes were deleted from everything except the monomorphisation pass because I don't know the status of that. | |||
| 2017-07-21 | Add a prove builtin that allows testing flow typing | Alasdair Armstrong | |
| For example: default Order dec val bit[64] -> unit effect pure test64 val cast forall 'n, 'n = 32 | 'n = 64. bit['n] -> unit effect pure test function forall 'n. unit test addr = { _prove(constraint('n != 16)); assert(constraint('n = 64), "64-bit mode"); _prove(constraint('n = 64)); test64(addr); } This doesn't affect the AST at all as _prove is just a ordinary function that the typechecker treats specially. | |||
| 2017-07-21 | Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵ | Alasdair Armstrong | |
| sail_new_tc | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |