summaryrefslogtreecommitdiff
path: root/src/process_file.mli
AgeCommit message (Expand)Author
2019-02-08Rewrite type definitions in rewrite_nexp_idsThomas Bauereiss
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
2019-02-06Improve emacs modeAlasdair Armstrong
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-21Add output directory option for generated Isabelle auxiliary theoriesThomas Bauereiss
2019-01-17Work around an issue with type abbreviations in HOLThomas Bauereiss
2019-01-14Add options for output directories for the lem and coq backends.Prashanth Mundkur
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-09-06Allow options to be set in the interactive modeAlasdair Armstrong
2018-09-04Improve error messages for include and ifdef statementsAlasdair Armstrong
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-05-03Work in progress on the coq backendBrian Campbell
2018-04-04Initial rewrite to move complex nexps in fn sigs into constraintsBrian Campbell
2018-01-30Optionally give *all* monomorphisation errors at onceBrian Campbell
2018-01-25Add simple conditional processing and file includeAlasdair Armstrong
2018-01-24Have some simple sail programs compiling to CAlasdair Armstrong
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-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
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
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
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Improvements to enable parsing and checking intermediate rewritingAlasdair Armstrong
2017-11-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
2017-11-14Automatic analysis for monomorphisationBrian Campbell
2017-11-10Fixed some tricky typechecking bugsAlasdair Armstrong
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Rewrite undefined values, add type annotations to early returnsThomas Bauereiss
2017-09-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-exper...Brian Campbell
2017-09-02Add command line flags to toggle sequential monad and native machine wordsThomas Bauereiss
2017-08-22Add option to dump monomorphised ast before (re-)typecheckingBrian Campbell
2017-08-10Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
2017-08-10Experimenting with alternate parserAlasdair Armstrong
2017-08-08Add infrastructure to play with new menhir parsers.Alasdair Armstrong
2017-08-02Add debugging option to dump AST after rewriting stepsThomas Bauereiss
2017-07-27Parameterise convert_ast by the bitvector orderAlasdair Armstrong
2017-07-27Fixed a bug where sail would run out of file descriptors when passed a large ...Alasdair Armstrong
2017-07-24Separate monomorphisation from top-level type checkingBrian Campbell