summaryrefslogtreecommitdiff
path: root/src/monomorphise.ml
AgeCommit message (Expand)Author
2020-11-19Make mono rewrites be more careful to produce constant-sized typesBrian Campbell
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-09-07Fix typo a mono_rewrites definitionBrian Campbell
2020-05-08Only check int kids when simplifying nexpsThomas Bauereiss
2020-05-08Add another type annotation in bitvector cast rewriteThomas Bauereiss
2020-05-04Add some more cases in mono rewritesThomas Bauereiss
2020-05-04Mono: Try to fix bug in inter-procedural analysisThomas Bauereiss
2020-05-04Try to fix bug in size parameter rewritingThomas Bauereiss
2020-04-29Add progress reporting to monomorphisationThomas Bauereiss
2020-04-21Fix build with OCaml 4.06.1Thomas Bauereiss
2020-04-21Add more monomorphisation rewritesThomas Bauereiss
2020-04-21Mono: Check for non-constant calls to make_the_valueThomas Bauereiss
2020-04-21Mono: Extract more kid instantiations from assertionsThomas Bauereiss
2020-04-21Mono: Propagate constants after applying pattern choicesThomas Bauereiss
2020-04-21Various monomorphisation fixesThomas Bauereiss
2020-04-21Mono: Extract set constraints from (in)equalitiesThomas Bauereiss
2020-04-21Handle more cases in bitvector cast rewriteThomas Bauereiss
2020-04-21Add support for some ASL idioms in mono rewritesThomas Bauereiss
2020-04-21Add more mono rewrites for bitvector subrangesThomas Bauereiss
2020-04-10Check more types in monomorphisation rewritesThomas Bauereiss
2020-01-16Allow effects on mappingsAlasdair Armstrong
2019-11-21Mono: Use more environment information when adding bitvector castsThomas Bauereiss
2019-11-11Make sure we include LEXP_cast register refs when slicing the specificationAlasdair Armstrong
2019-08-14Add a mono rewrite for (ones(n) @ zeros(m))Thomas Bauereiss
2019-08-14Use bitvector type in mono rewritesThomas Bauereiss
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-07-11Make sure constant folding won't fold external definitions that also have sai...Alasdair Armstrong
2019-06-28Monomorphisation: add some alternative names for ones and zero_extend as used...Robert Norton
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
2019-06-19Monomorphisation improvements for aarch64_smallBrian Campbell
2019-06-13Add AST for greater-than and less-than constraintsBrian Campbell
2019-06-10Add well-formedness check for type schemes in valspecs.Brian Campbell
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-06Handle type variables generated while inferring applications in monomorphisationBrian Campbell
2019-05-06Avoid degenerate construction monomorphisation, use # in generated namesBrian Campbell
2019-05-06Apply constructor monomorphisation in preference to variable splitsBrian Campbell
2019-05-06Handle global constants in monomorphisationBrian Campbell
2019-05-06Cope with irrelevant existentials when monomorphising constructorsBrian Campbell
2019-05-06Expand constraints while looking for sets during monomorphisationBrian Campbell
2019-04-26More constructor monomorphisation supportBrian Campbell
2019-04-25Get basic constructor monomorphisation working againBrian Campbell
2019-04-25Make constructor splitting in monomorphisation obey -dall_split_errorsBrian Campbell
2019-04-25Don't try to insert monomorphisation casts when the types are the sameBrian Campbell
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French