summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem_ast.ml
AgeCommit message (Expand)Author
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-04-18Rename BK_nat to BK_int to be consistent with source syntaxAlasdair Armstrong
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-02-05Add typ patterns for destructuring existentialsAlasdair Armstrong
2018-01-12OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.Alasdair Armstrong
2018-01-05Added bitfield syntax to replicate register bits typeAlasdair Armstrong
2018-01-02Experimenting with power specAlasdair Armstrong
2017-12-14Fix all compiler warning except in lem pretty printer and monomorphisationAlasdair Armstrong
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-29Better lem_ast tagging and interpreter tweaksAlasdair Armstrong
2017-11-29Switched to bytecode compiler for executing interpreter to avoid stack overflowAlasdair Armstrong
2017-11-29Fix lem_ast output bugsAlasdair Armstrong
2017-11-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
2017-11-16Make the generation of the lem_ast numeric constants automatic for all number...Alasdair Armstrong
2017-11-16Made l2.ott generate an ast.lem which is is valid w.r.t. -lem_ast output.Alasdair Armstrong
2017-11-16Remove unused Typ_wild constructorAlasdair Armstrong
2017-11-08Allow for different extern names for different backendsAlasdair Armstrong
2017-11-02Fix a few AST and parsing-related bugsThomas Bauereiss
2017-10-19Follow AST changes in (Lem) pretty-printersThomas Bauereiss
2017-10-06Remove BK_effect constructorAlasdair Armstrong
2017-10-03Fixes to new parserAlasdair Armstrong
2017-09-21Refactored AST valspecs into single constructorAlasdair Armstrong
2017-09-21Remove unused kind_def (KD_) nodes from ASTAlasdair Armstrong
2017-09-21Change NC_fixed to NC_equal to match NC_not_equalAlasdair Armstrong
2017-09-21Simplify AST by removing LB_val_explicit and replace LB_val_implicit with jus...Alasdair Armstrong
2017-09-21Cleaning up the AST and removing redundant and/or unused nodesAlasdair Armstrong
2017-09-14Fix a regression when writing to a register via a reference in a vector such ...Thomas Bauereiss
2017-09-08Fixed bug when printing Typ_args in Lem AST outputAlasdair Armstrong
2017-09-02Various fixes for HexapodThomas Bauereiss
2017-08-30Fix another bug in local variable update rewritingThomas Bauereiss
2017-08-15Removed Typ_arg_effect - nobody used it and it isn't supported by the backends.Alasdair Armstrong
2017-08-10Existentials in Lem AST outputBrian Campbell
2017-07-27Add cons patterns to pretty-printersThomas Bauereiss
2017-07-21Everything moved to new typecheckerAlasdair Armstrong
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
2017-05-24Merge branch 'master' of bitbucket.org:Peter_Sewell/sailShaked Flur
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-05-24Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from dat...Robert Norton
2017-03-29Factor out pretty printers into separate files. Hopefully this will make sear...Robert Norton