summaryrefslogtreecommitdiff
path: root/src/jib.lem
AgeCommit message (Collapse)Author
2019-10-28Fix jib.ott and SMT regressionsAlasdair Armstrong
SMT seems sensitive to gensym counter being reset between definitions, but it shouldn't care due to unique_per_function_ids... need to investigate further. Only causes a single test to fail so must be subtle. Diffing between the bad/good versions reveals a few lines of generated SMT go missing when the gensym counter is reset.
2019-10-28Some C backend refactoringAlasdair
Make it so that jib_compile.ml never relies on specific string encodings for various constructs in C. Previously this happened when monomorphisation occured for union constructors and fields, i.e. x.foo -> x.zfoo_bitsz632z7 Now identifiers that can be modified are represented as (id, ctyp list) tuples, so we can keep the types x.foo -> x.foo::<bits(32)> This then enables us to do jib IR -> jib IR rewrites that modify types In particular there is now a rewrite that removes tuples as an IR->IR pass rather than doing it ad-hoc in the C code generation, although this is not on by default Note that this change seems to have triggered an Ott bug so jib.lem is now checked in and not generated from Ott