diff options
Diffstat (limited to 'language/jib.ott')
| -rw-r--r-- | language/jib.ott | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/language/jib.ott b/language/jib.ott index 1d097c80..1345ba64 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -91,24 +91,25 @@ op :: '' ::= | replicate nat :: :: replicate cval :: 'V_' ::= - | name : ctyp :: :: id - | '&' name : ctyp :: :: ref - | value : ctyp :: :: lit - | struct { id0 = cval0 , ... , idn = cvaln } ctyp :: :: struct - | cval != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind - | unwrap id cval ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_unwrap - | cval nat0 nat1 :: :: tuple_member - | op ( cval0 , ... , cvaln ) :: :: call - | cval . string :: :: field - | poly cval ctyp :: :: poly + | name : ctyp :: :: id + | '&' name : ctyp :: :: ref + | value : ctyp :: :: lit + | struct { uid0 = cval0 , ... , uidn = cvaln } ctyp :: :: struct + | cval != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind + | unwrap id cval ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_unwrap + | cval nat0 nat1 :: :: tuple_member + | op ( cval0 , ... , cvaln ) :: :: call + | cval . uid :: :: field + | poly cval ctyp :: :: poly % Note that init / clear are sometimes refered to as create / kill %%% IR types uid :: 'UId_' ::= - {{ lem id * list ctyp }} - {{ ocaml id * ctyp list }} + {{ phantom }} + {{ lem (id * list ctyp) }} + {{ ocaml (id * ctyp list) }} ctyp :: 'CT_' ::= {{ com C type }} @@ -146,8 +147,8 @@ ctyp :: 'CT_' ::= % into C. We don't fully worry about precise implementation details at % this point, as C doesn't have variants or tuples natively, but these % need to be encoded. - | enum id ( id0 , ... , idn ) :: :: enum - | struct id ( id0 * ctyp0 , ... , idn * ctypn ) :: :: struct + | enum id ( id0 , ... , idn ) :: :: enum + | struct id ( uid0 * ctyp0 , ... , uidn * ctypn ) :: :: struct | variant id ( uid0 * ctyp0 , ... , uidn * ctypn ) :: :: variant % A vector type for non-bit vectors, and a (linked) list type. @@ -170,15 +171,15 @@ ctyp :: 'CT_' ::= clexp :: 'CL_' ::= | name : ctyp :: :: id | name0 rmw name1 : ctyp :: :: rmw - | clexp . string :: :: field + | clexp . uid :: :: field | * clexp :: :: addr | clexp . nat :: :: tuple | void :: :: void ctype_def :: 'CTD_' ::= {{ com C type definition }} - | enum id = id0 '|' ... '|' idn :: :: enum - | struct id = { id0 : ctyp0 , ... , idn : ctypn } :: :: struct + | enum id = id0 '|' ... '|' idn :: :: enum + | struct id = { uid0 : ctyp0 , ... , uidn : ctypn } :: :: struct | variant id = { uid0 : ctyp0 , ... , uidn : ctypn } :: :: variant iannot :: '' ::= @@ -194,7 +195,7 @@ instr :: 'I_' ::= | jump ( cval ) string :: :: jump | goto string :: :: goto | string : :: :: label - | clexp = bool id ( cval0 , ... , cvaln ) :: :: funcall + | clexp = bool uid ( cval0 , ... , cvaln ) :: :: funcall | clexp = cval :: :: copy | clear ctyp name :: :: clear | undefined ctyp :: :: undefined |