summaryrefslogtreecommitdiff
path: root/src/state.ml
AgeCommit message (Expand)Author
2020-09-29Refactor: Change AST type from a union to a structAlasdair
2020-09-28Refactor: Rename 'a defs to 'a astAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-05-13Make Isabelle lemma generation work with grouped regstateThomas Bauereiss
2019-11-29Tweak generated register_value typeThomas Bauereiss
2019-11-21Add option to generate grouped register state recordThomas Bauereiss
2019-05-17Get all Lem tests working with separate bitvector typeAlasdair Armstrong
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-29Improve generation of initial register stateThomas Bauereiss
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2018-12-26More cleanupAlasdair Armstrong
2018-12-12Remove KOpt_none constructorAlasdair
2018-12-08Compiling againAlasdair
2018-12-07Working on better flow typing for ASLAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-07-27Make type annotations abstract in type_check.mliAlasdair Armstrong
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-07Coq: precise generic vectorsBrian Campbell
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-12Fix bug in handling of registers with option typeThomas Bauereiss
2018-05-09Generate initial register state recordThomas Bauereiss
2018-05-03Work in progress on the coq backendBrian Campbell
2018-04-18Add first draft of Isabelle library documentationThomas Bauereiss
2018-04-09Stop vector_typ_args_of from failing when order is a variableBrian Campbell
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-22Some Lem/OCaml compatibility fixesBrian Campbell
2018-02-16Don't generate undefined functions for generated register typesThomas Bauereiss
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss