summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-10-13Make Sail_values.repeat total, and remove duplicateBrian Campbell
2017-10-06Produce type signatures in Lem outputBrian Campbell
Necessary for machine words due to the type variables Also add Size type classes for machine word bitvectors
2017-10-06Implement replicate_bits for mwordsBrian Campbell
2017-10-06Fix constant propagation on multi-argument functionsBrian Campbell
2017-10-02Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-02Make undefined constant propagation stop at ex_intBrian Campbell
2017-09-29Support vector registers (other than bitvectors)Thomas Bauereiss
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
- Remove start indices and indexing order from bitvector types. Instead add them as arguments to functions accessing/updating bitvectors. These arguments are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a "sizeof" rewriting pass. - Add a typeclass for bitvectors with a few basic functions (converting to/from bitlists, converting to an integer, getting and setting bits). Make both monads use this interface, so that they work with both the bitlist and the machine word representation of bitvectors.
2017-09-29Add MIPS->Isabelle target to MakefileThomas Bauereiss
2017-09-28Use (K)Bindings from ast_util rather than making new onesBrian Campbell
2017-09-28Add loops to monomorphisationBrian Campbell
2017-09-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-28Refine constructors during monomorphisationBrian Campbell
2017-09-27Add while-loops to Lem backendThomas Bauereiss
2017-09-26Remove obsolete existential removal codeBrian Campbell
2017-09-26Added while-do and repeat-until loops to sail for translating ASLAlasdair Armstrong
2017-09-26Remove debugging statements included accidentallyBrian Campbell
2017-09-26Add propagation of local assignments to monomorphisationBrian Campbell
2017-09-21Support more functions and vector construction in mono for hexapodBrian Campbell
2017-09-21Substitute into constraints to make assert work with monoBrian Campbell
2017-09-21Disable existential removal for nowBrian Campbell
2017-09-20Handle let (exists 't...[:'t:]) 't = lit in monoBrian Campbell
2017-09-20Remove obsolete nexp refinementBrian Campbell
2017-09-20Support splitting on multiple variables in monoBrian Campbell
2017-09-19Added additional case for tuple l-expressions to increase compatability for ASL.Alasdair Armstrong
2017-09-18Added additional utility functions in ast_utilAlasdair Armstrong
Also fixed basic ocaml test suite
2017-09-18Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-14Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-09-14Two thirds of monomorphising union types with an existentialBrian Campbell
Still need some way of picking the appropriate constructor
2017-09-14Fix bug in topological sortingThomas Bauereiss
2017-09-14Fix some more test casesThomas Bauereiss
2017-09-14Fix 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-13Fixed code display in error messages that span multiple linesAlasdair Armstrong
2017-09-13Work on improving Sail error messagesAlasdair Armstrong
- Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases
2017-09-08Fixed bug when printing Typ_args in Lem AST outputAlasdair Armstrong
2017-09-07Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-09-07Add ocaml run-time and updates to sail for ocaml backendAlasdair Armstrong
2017-09-05Fix printing of negative numbersAlastair Reid
2017-09-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments
2017-09-02Various fixes for HexapodThomas 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-09-02Remove dependency of state.lem on bitvector operationsThomas Bauereiss
2017-09-02Add command line flags to toggle sequential monad and native machine wordsThomas Bauereiss
2017-09-01Testing typedef generation for ocamlAlasdair Armstrong
2017-09-01Started work on test suite for ocaml backendAlasdair Armstrong
2017-08-30Remove debug print statement from rewriterAlasdair Armstrong
2017-08-30Improved ocaml backend to the point where the hexapod spec produces ↵Alasdair Armstrong
syntactically correct ocaml
2017-08-30Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-08-30Ocaml backend can now run ocamlbuild automatically to build ocamlAlasdair Armstrong
files into runable executable.
2017-08-30Fix another bug in local variable update rewritingThomas Bauereiss
E_internal_let is only used for introducing local variables, not updating existing ones.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:57:06 +0000