summaryrefslogtreecommitdiff
path: root/src/state.ml
AgeCommit message (Expand)Author
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