summaryrefslogtreecommitdiff
path: root/src/process_file.mli
AgeCommit message (Expand)Author
2020-09-28Refactor: Rename 'a defs to 'a astAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-08-21Add reformat option to SailAlasdair
2020-08-13Preserve file structure through initial checkAlasdair
2020-04-14Add add_symbol to the API of Process_fileAlasdair
2019-11-11Update libsail slightly with recent changesAlasdair Armstrong
2019-08-22additional option to tweak Coq output to support user-defined monad:pes20
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-07-18Add a option to check for a feature symbolAlasdair Armstrong
2019-06-19Rewriting improvements for monomorphic aarch64_smallBrian Campbell
2019-03-27Interactive: Refactor sail.mlAlasdair Armstrong
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