diff options
| author | Alasdair | 2019-10-26 04:59:49 +0100 |
|---|---|---|
| committer | Alasdair | 2019-10-28 13:38:10 +0000 |
| commit | 7f9371921cfcec819d9e0c778f8b817fb1566bce (patch) | |
| tree | 0bdf7c59c3192884f0e706baa46805abcece6fb3 /language | |
| parent | 5bcbe357c72382c1076ea7fd7c3ca6ea9f2f035c (diff) | |
Some C backend refactoring
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
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/language/jib.ott b/language/jib.ott index dfda3bbc..1d097c80 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -106,6 +106,10 @@ cval :: 'V_' ::= %%% IR types +uid :: 'UId_' ::= + {{ lem id * list ctyp }} + {{ ocaml id * ctyp list }} + ctyp :: 'CT_' ::= {{ com C type }} % Integer types @@ -144,7 +148,7 @@ ctyp :: 'CT_' ::= % need to be encoded. | enum id ( id0 , ... , idn ) :: :: enum | struct id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: struct - | variant id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: variant + | variant id ( uid0 * ctyp0 , ... , uidn * ctypn ) :: :: variant % A vector type for non-bit vectors, and a (linked) list type. | vector ( bool , ctyp ) :: :: vector @@ -175,9 +179,9 @@ ctype_def :: 'CTD_' ::= {{ com C type definition }} | enum id = id0 '|' ... '|' idn :: :: enum | struct id = { id0 : ctyp0 , ... , idn : ctypn } :: :: struct - | variant id = { id0 : ctyp0 , ... , idn : ctypn } :: :: variant + | variant id = { uid0 : ctyp0 , ... , uidn : ctypn } :: :: variant -iannot :: 'IA_' ::= +iannot :: '' ::= {{ lem nat * nat * nat }} {{ ocaml int * int * int }} |