| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-16 | Make the generation of the lem_ast numeric constants automatic for all ↵ | Alasdair Armstrong | |
| numbers below 129 | |||
| 2017-11-16 | Made l2.ott generate an ast.lem which is is valid w.r.t. -lem_ast output. | Alasdair Armstrong | |
| This is the first step towards getting the interpreter working on this branch | |||
| 2017-11-16 | Remove unused Typ_wild constructor | Alasdair Armstrong | |
| 2017-11-08 | Allow for different extern names for different backends | Alasdair Armstrong | |
| For example: val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit val main : unit -> unit function main () = { test (); } for a backend not explicitly provided, the extern name would be simply "test" in this case, i.e. the string version of the id. Also fixed some bugs in the ocaml backend. | |||
| 2017-11-02 | Fix a few AST and parsing-related bugs | Thomas Bauereiss | |
| 2017-10-19 | Follow AST changes in (Lem) pretty-printers | Thomas Bauereiss | |
| 2017-10-06 | Remove BK_effect constructor | Alasdair Armstrong | |
| 2017-10-03 | Fixes to new parser | Alasdair Armstrong | |
| 2017-09-21 | Refactored AST valspecs into single constructor | Alasdair Armstrong | |
| 2017-09-21 | Remove unused kind_def (KD_) nodes from AST | Alasdair Armstrong | |
| 2017-09-21 | Change NC_fixed to NC_equal to match NC_not_equal | Alasdair Armstrong | |
| also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway) | |||
| 2017-09-21 | Simplify AST by removing LB_val_explicit and replace LB_val_implicit with ↵ | Alasdair Armstrong | |
| just LB_val in AST also rename functions in rewriter.ml appropriately. | |||
| 2017-09-21 | Cleaning up the AST and removing redundant and/or unused nodes | Alasdair Armstrong | |
| 2017-09-14 | Fix a regression when writing to a register via a reference in a vector such ↵ | Thomas Bauereiss | |
| as GPR This was wrongly translated as an update of the vector of references. | |||
| 2017-09-08 | Fixed bug when printing Typ_args in Lem AST output | Alasdair Armstrong | |
| 2017-09-02 | Various fixes for Hexapod | Thomas Bauereiss | |
| - Support tuples in lexps - Rewrite trivial sizeofs - Rewrite early returns more aggressively - Support let bindings with ticked variables (binding both a type-level and term-level variable at the same time) | |||
| 2017-08-30 | Fix another bug in local variable update rewriting | Thomas Bauereiss | |
| E_internal_let is only used for introducing local variables, not updating existing ones. | |||
| 2017-08-15 | Removed Typ_arg_effect - nobody used it and it isn't supported by the backends. | Alasdair Armstrong | |
| 2017-08-10 | Existentials in Lem AST output | Brian Campbell | |
| 2017-07-27 | Add cons patterns to pretty-printers | Thomas Bauereiss | |
| 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 | Switch to new typechecker (almost) | Thomas Bauereiss | |
| Initial typecheck still uses previous typechecker | |||
| 2017-05-24 | Merge branch 'master' of bitbucket.org:Peter_Sewell/sail | Shaked Flur | |
| # Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml | |||
| 2017-05-24 | added the exmem effect for AArch64 store-exclusive | Shaked Flur | |
| 2017-05-24 | Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵ | Robert Norton | |
| data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result. | |||
| 2017-03-29 | Factor out pretty printers into separate files. Hopefully this will make ↵ | Robert Norton | |
| searching easier. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |