diff options
| author | Alasdair | 2019-03-14 23:39:11 +0000 |
|---|---|---|
| committer | Alasdair | 2019-03-15 00:34:41 +0000 |
| commit | 6137b6b5b788138dd02503cb1e88242a618a3677 (patch) | |
| tree | e0848601a9aa177dbf8879c46dd81a4fc2db2a06 /language | |
| parent | c741e731afe4a6d2c65d43ca299a1a48a1534ec0 (diff) | |
C: Wrap Jib identifiers
Avoids duplication between l-expressions and expressions. Also means that
special variables like current_exception and have_exception are treated
normally by functions such as instr_reads and instr_writes etc. Furthermore
we can now easily annotate Jib identifiers in ways that were not previously
possible with plain sail ids.
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/language/jib.ott b/language/jib.ott index e54e2ea5..5a0e3eba 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -47,15 +47,19 @@ 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 + | name :: :: id + | '&' name :: :: ref | value :: :: lit - | have_exception :: :: have_exception - | current_exception :: :: current_exception | fragment op fragment' :: :: op | op fragment :: :: unary | string ( fragment0 , ... , fragmentn ) :: :: call @@ -129,13 +133,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,14 +153,14 @@ 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 @@ -187,8 +188,8 @@ instr :: 'I_' ::= | return cval :: :: return % For optimising away allocations and copying. - | reset ctyp id :: :: reset - | ctyp id = cval :: :: reinit + | reset ctyp name :: :: reset + | ctyp name = cval :: :: reinit | alias clexp = cval :: :: alias cdef :: 'CDEF_' ::= |