diff options
| author | Jon French | 2019-04-15 16:18:18 +0100 |
|---|---|---|
| committer | Jon French | 2019-04-15 16:18:18 +0100 |
| commit | a9f0b829507e9882efdb59cce4d83ea7e87f5f71 (patch) | |
| tree | 11cde6c1918bc15f4dda9a8e40afd4a1fe912a0a /language/jib.ott | |
| parent | 0f6fd188ca232cb539592801fcbb873d59611d81 (diff) | |
| parent | 57443173923e87f33713c99dbab9eba7e3db0660 (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'language/jib.ott')
| -rw-r--r-- | language/jib.ott | 48 |
1 files changed, 25 insertions, 23 deletions
diff --git a/language/jib.ott b/language/jib.ott index e54e2ea5..5f800fcd 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -47,21 +47,27 @@ open import Value2 grammar +name :: '' ::= + | id nat :: :: name + | have_exception nat :: :: have_exception + | current_exception nat :: :: current_exception + | return nat :: :: return + % Fragments are small pure snippets of (abstract) C code, mostly -% expressions, used by the aval and cval types. +% expressions, used by the aval (ANF) and cval (Jib) types. fragment :: 'F_' ::= - | id :: :: id - | '&' id :: :: ref - | value :: :: lit - | have_exception :: :: have_exception - | current_exception :: :: current_exception - | fragment op fragment' :: :: op - | op fragment :: :: unary - | string ( fragment0 , ... , fragmentn ) :: :: call - | fragment . string :: :: field - | string :: :: raw - | poly fragment :: :: poly + | 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 % Note that init / clear are sometimes refered to as create / kill @@ -129,13 +135,10 @@ cval :: 'CV_' ::= {{ lem fragment * ctyp }} clexp :: 'CL_' ::= - | id : ctyp :: :: id + | name : ctyp :: :: id | clexp . string :: :: field | * clexp :: :: addr | clexp . nat :: :: tuple - | current_exception : ctyp :: :: current_exception - | have_exception :: :: have_exception - | return : ctyp :: :: return | void :: :: void ctype_def :: 'CTD_' ::= @@ -152,17 +155,17 @@ instr :: 'I_' ::= {{ aux _ iannot }} % The following are the minimal set of instructions output by % Jib_compile.ml. - | ctyp id :: :: decl - | ctyp id = cval :: :: init + | ctyp name :: :: decl + | ctyp name = cval :: :: init | jump ( cval ) string :: :: jump | goto string :: :: goto | string : :: :: label | clexp = bool id ( cval0 , ... , cvaln ) :: :: funcall | clexp = cval :: :: copy - | clear ctyp id :: :: clear + | clear ctyp name :: :: clear | undefined ctyp :: :: undefined | match_failure :: :: match_failure - | end :: :: end + | end name :: :: end % All instructions containing nested instructions can be flattened % away. try and throw only exist for internal use within @@ -187,9 +190,8 @@ instr :: 'I_' ::= | return cval :: :: return % For optimising away allocations and copying. - | reset ctyp id :: :: reset - | ctyp id = cval :: :: reinit - | alias clexp = cval :: :: alias + | reset ctyp name :: :: reset + | ctyp name = cval :: :: reinit cdef :: 'CDEF_' ::= | register id : ctyp = { |