summaryrefslogtreecommitdiff
path: root/src/process_file.mli
AgeCommit message (Expand)Author
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
2017-07-21Everything moved to new typecheckerAlasdair Armstrong
2017-07-21Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into sa...Alasdair Armstrong
2017-07-21Improvements to sail n_constraintsAlasdair Armstrong
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
2017-07-13Make new-tc monomorphisation actually workBrian Campbell
2017-07-12Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into sa...Alasdair Armstrong
2017-07-12Removed inital_check_full_astAlasdair Armstrong
2017-07-12Add checks for variable identifiers in pattern subsumptionThomas Bauereiss
2017-06-29Various improvements to typecheckerAlasdair Armstrong
2017-06-22Can now typecheck register declarations and assignmentsAlasdair Armstrong
2017-06-15Prototype Bi-directional type checking algorithm for sailAlasdair Armstrong
2017-02-03fix headersPeter Sewell
2016-11-28make sail produce prompt and state version of shallow embedding files at the ...Christopher Pulte
2016-11-14add option -lem_sequential for producing shallow embedding that refers to sta...Christopher Pulte
2016-10-18Expose type environment after checking, for use in analysisKathy Gray
2016-02-24Small mixups to get the initial check infrastructure working for full ast pro...Kathy Gray
2015-10-06added the preliminary lem output option that for now uses ocaml ppChristopher Pulte
2015-09-29Boiler plate to generate an ml file from a sail spec. Now debugging the outpu...Kathy Gray
2015-09-28basic untested ocaml boiler plateKathy Gray
2015-02-13Actually use new dependency information in generation of lem/etc.Kathy Gray
2014-07-29A file can now declare that a default order is either inc or dec, and this wi...Kathy Gray
2014-01-17Type check through type definitions and val specifications, building definiti...Kathy Gray
2013-09-09Pretty printer to Lem ast added; accessed by -lem_ast on the command lineKathy Gray
2013-08-07Starting checks and translation from parse_ast to ast, including an internal ...Kathy Gray
2013-07-26Remove white space/terminal trackingKathy Gray
2013-07-25Clean trailing whitespaceGabriel Kerneis
2013-07-24Parser compiles and compiles some very small test programs.Kathy Gray
2013-07-12Parser in progress, and more src files for plumbing parsing, lexing and event...Kathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:22:27 +0000