diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/bytecode.ott | 4 | ||||
| -rw-r--r-- | language/sail.ott | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/language/bytecode.ott b/language/bytecode.ott index 895ac34b..32b04bb4 100644 --- a/language/bytecode.ott +++ b/language/bytecode.ott @@ -145,7 +145,9 @@ instr :: 'I_' ::= | ctyp id = cval :: :: reinit cdef :: 'CDEF_' ::= - | register id : ctyp :: :: reg_dec + | register id : ctyp = { + instr0 ; ... ; instrn + } :: :: reg_dec | ctype_def :: :: type | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = { instr0 ; ... ; instrm diff --git a/language/sail.ott b/language/sail.ott index 3332034f..12a71b9f 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -230,6 +230,7 @@ base_effect :: 'BE_' ::= | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} | escape :: :: escape {{ com potential exception }} + | config :: :: config {{ com configuration option }} effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} @@ -1096,6 +1097,7 @@ dec_spec :: 'DEC_' ::= {{ com register declarations }} {{ aux _ annot }} {{ auxparam 'a }} | register typ id :: :: reg + | register configuration id : typ = exp :: :: config | register alias id = alias_spec :: :: alias | register alias typ id = alias_spec :: :: typ_alias |