diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 78 |
1 files changed, 53 insertions, 25 deletions
diff --git a/language/jib.ott b/language/jib.ott index 5f800fcd..447b25e3 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -7,6 +7,10 @@ metavar nat ::= {{ ocaml int }} {{ lem nat }} +metavar big_int ::= + {{ phantom }} + {{ lem integer }} + metavar id ::= {{ phantom }} {{ ocaml id }} @@ -22,11 +26,6 @@ metavar string ::= {{ ocaml string }} {{ lem string }} -metavar op ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - metavar bool ::= {{ phantom }} {{ ocaml bool }} @@ -37,6 +36,10 @@ metavar value ::= {{ lem vl }} {{ ocaml vl }} +metavar alpha ::= + {{ phantom }} + {{ lem 'a }} + embed {{ lem @@ -53,21 +56,49 @@ name :: '' ::= | current_exception nat :: :: current_exception | return nat :: :: return -% Fragments are small pure snippets of (abstract) C code, mostly -% expressions, used by the aval (ANF) and cval (Jib) types. - -fragment :: 'F_' ::= - | name :: :: id - | '&' name :: :: ref - | value :: :: lit - | fragment != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind - | unwrap id ( ctyp0 , ... , ctypn ) fragment :: :: ctor_unwrap - | fragment op fragment' :: :: op - | op fragment :: :: unary - | string ( fragment0 , ... , fragmentn ) :: :: call - | fragment . string :: :: field - | string :: :: raw - | poly fragment :: :: poly +op :: '' ::= + | not :: :: bnot + | hd :: :: list_hd + | tl :: :: list_tl + | bit_to_bool :: :: bit_to_bool + | eq :: :: eq + | neq :: :: neq +% Integer ops + | lt :: :: ilt + | lteq :: :: ilteq + | gt :: :: igt + | gteq :: :: igteq + | add :: :: iadd + | sub :: :: isub + | unsigned nat :: :: unsigned + | signed nat :: :: signed +% Bitvector ops + | bvnot :: :: bvnot + | bvor :: :: bvor + | bvand :: :: bvand + | bvxor :: :: bvxor + | bvadd :: :: bvadd + | bvsub :: :: bvsub + | bvaccess :: :: bvaccess + | concat :: :: concat + | zero_extend nat :: :: zero_extend + | sign_extend nat :: :: sign_extend + | slice nat :: :: slice + | sslice nat :: :: sslice + | set_slice :: :: set_slice + | 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 % Note that init / clear are sometimes refered to as create / kill @@ -81,6 +112,7 @@ ctyp :: 'CT_' ::= % fint(n) is a fixed precision signed integer that is representable in exactly n bits | lint :: :: lint | fint nat :: :: fint + | constant big_int :: :: constant % Bitvector types - flag represents bit indexing direction, true - dec or false - inc % @@ -129,13 +161,9 @@ ctyp :: 'CT_' ::= % lbits, and this must work without compiling to type incorrect C. | poly :: :: poly - -cval :: 'CV_' ::= - {{ ocaml fragment * ctyp }} - {{ lem fragment * ctyp }} - clexp :: 'CL_' ::= | name : ctyp :: :: id + | name0 rmw name1 : ctyp :: :: rmw | clexp . string :: :: field | * clexp :: :: addr | clexp . nat :: :: tuple |