diff options
| author | Alasdair Armstrong | 2019-11-08 17:22:25 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-11-08 17:22:25 +0000 |
| commit | bf657ba085f40838a4048b18b19ce889310f3ddd (patch) | |
| tree | f3e266de5dc0fe1cb0589d3d016cedf4719a2179 /language | |
| parent | 90a5dcd4bfb2f414cda201d1c7e3c6a0e6f173de (diff) | |
Refactor Jib compilation
Split the dynamic context into the ctx struct, and the static
configuration into a module which parameterises the sail->jib
compilation step rather than just having a giant ctx struct.
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/language/jib.ott b/language/jib.ott index 6332c403..eaa6e643 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -26,6 +26,11 @@ metavar string ::= {{ ocaml string }} {{ lem string }} +metavar mstring ::= + {{ phantom }} + {{ ocaml string option }} + {{ lem maybe string }} + metavar bool ::= {{ phantom }} {{ ocaml bool }} @@ -239,7 +244,7 @@ cdef :: 'CDEF_' ::= instr0 ; ... ; instrm } :: :: let - | val id ( ctyp0 , ... , ctypn ) -> ctyp :: :: spec + | val id = mstring ( ctyp0 , ... , ctypn ) -> ctyp :: :: spec % If mid = Some id this indicates that the caller should allocate the % return type and passes a pointer to it as an extra argument id for |