summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
AgeCommit message (Expand)Author
2018-05-17Remove sequential code againBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
2018-05-11Add Boolean short-circuiting to state monadThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
2018-05-11Remove buggy bit list comparison functions from Lem libraryThomas Bauereiss
2018-05-09Add more annotations for loop bounds in Lem rewritingThomas Bauereiss
2018-05-09Support short-circuiting of Boolean expressions in LemThomas Bauereiss
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-04-26Lem: Add Size class annotations for nested bitvector typesThomas Bauereiss
2018-04-18Fix bug in pretty-printing loops to LemThomas Bauereiss
2018-04-09Stop vector_typ_args_of from failing when order is a variableBrian Campbell
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-03-23Fix indentation of loops in generated IsabelleThomas Bauereiss
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add rewriting step for moving execute clauses into auxiliary functionsThomas Bauereiss
2018-03-13Merge funcls for Lem output, making it suitable for testing with OCamlBrian Campbell
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-20Report unsupported nexps properly in Lem backendBrian Campbell
2018-02-20Look for alternative size annotations when pretty printing LemBrian Campbell
2018-02-16Avoid nested explicit type annotationsThomas Bauereiss
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-02-05Merge changes to type_check.mlAlasdair Armstrong
2018-02-05Add typ patterns for destructuring existentialsAlasdair Armstrong
2018-02-01Comment out special casing of execute function in Lem pretty-printerThomas Bauereiss
2018-01-31Split base definitions of Lem monads and further built-ins (e.g. loop combina...Thomas Bauereiss
2018-01-29Output a few more type annotations for LemThomas Bauereiss
2018-01-23Run tests for Lem shallow embeddingThomas Bauereiss
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2018-01-18Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-17Fix use of nexps in type annotations when not using machine wordsThomas Bauereiss
2018-01-16Output more type annotations in Lem backendThomas Bauereiss
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-05Added bitfield syntax to replicate register bits typeAlasdair Armstrong
2018-01-03Updates to interpreterAlasdair Armstrong
2018-01-02Experimenting with power specAlasdair Armstrong
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-19Fix a bug in untupling function arguments for LemThomas Bauereiss
2017-12-14An experimental version of sail without bitvector start indexes.Alasdair Armstrong
2017-12-14Un-tuple function arguments when pretty-printing to LemThomas Bauereiss
2017-12-14Make sequential and mwords global variables in Lem pretty-printerThomas Bauereiss
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-06Add top-level pattern match guards internallyBrian Campbell
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Use doc_typdef_lem from experimentsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:45:49 +0000