summaryrefslogtreecommitdiff
path: root/src/process_file.ml
AgeCommit message (Expand)Author
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-06-29Constant folding improvementsAlasdair
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-07Add a constant folding optimization passAlasdair
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-05-18more riscv mappings; riscv now builds successfully to lem which builds to isa...Jon French
2018-05-17Remove sequential code againBrian Campbell
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-05-03Work in progress on the coq backendBrian Campbell
2018-05-01tidyJon French
2018-05-01Use a naming scheme rather than random fresh ids for union anonymous recordsJon French
2018-05-01Add anonymous record arms to unionsJon French
2018-04-26Add a new SHARE_DIR argument to use when doing opam build. For non-opam build...Robert Norton
2018-04-26Opam packaging: add install and uninstall targets and code to find various fi...Robert Norton
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-04-04Use solver properly to simplify nexps in mono analysis, Lem printingBrian Campbell
2018-04-04Initial rewrite to move complex nexps in fn sigs into constraintsBrian Campbell
2018-02-27Get MIPS translated to LemThomas Bauereiss
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-01-31Add wrappers around Lem operators using bitvector type classThomas Bauereiss
2018-01-31Split base definitions of Lem monads and further built-ins (e.g. loop combina...Thomas Bauereiss
2018-01-30Optionally give *all* monomorphisation errors at onceBrian Campbell
2018-01-30Fix failing Lem testsAlasdair Armstrong
2018-01-29Turn off warnings when rechecking after monoBrian Campbell
2018-01-25Add simple conditional processing and file includeAlasdair Armstrong
2018-01-24Have some simple sail programs compiling to CAlasdair Armstrong
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2018-01-18Clean up command line options slightlyAlasdair Armstrong
2018-01-15Add help to interactive mode, and load files incrementallyAlasdair Armstrong
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-10Add an all_split_errors optionBrian Campbell
2018-01-09Tidy up monomorphisation interfaceBrian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
2018-01-05Moved parser, lexer and pretty printer to correct locations.Alasdair Armstrong
2018-01-05Removed legacy parser/lexer and pretty printerAlasdair Armstrong
2018-01-05Fix duplicate definitions created by mergeAlasdair Armstrong
2018-01-05Merge remote-tracking branch 'origin/interactive' into vectorAlasdair Armstrong
2018-01-03Lots of experimental changes on this branchAlasdair Armstrong
2018-01-03Updates to interpreterAlasdair Armstrong
2017-12-18Clean up last commitBrian Campbell
2017-12-18Handle multiple -lem_lib optionsBrian Campbell
2017-12-15Experimenting with interactive modeAlasdair Armstrong
2017-12-14Make sequential and mwords global variables in Lem pretty-printerThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:57:36 +0000