diff options
| author | jp | 2020-02-12 17:46:48 +0000 |
|---|---|---|
| committer | jp | 2020-02-12 17:46:48 +0000 |
| commit | ed8bccd927306551f93d5aab8d0e2a92b9e5d227 (patch) | |
| tree | 55bf788c8155f0c7d024f2147f5eb3873729b02a /language | |
| parent | 31a65c9b7383d2a87da0fbcf5c265d533146ac23 (diff) | |
| parent | 4a72cb8084237161d0bccc66f27d5fb6d24315e0 (diff) | |
Merge branch 'sail2' of https://github.com/rems-project/sail into sail2
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 11 | ||||
| -rw-r--r-- | language/sail.ott | 2 |
2 files changed, 9 insertions, 4 deletions
diff --git a/language/jib.ott b/language/jib.ott index 1345ba64..63c86126 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -26,6 +26,11 @@ metavar string ::= {{ ocaml string }} {{ lem string }} +metavar mstring ::= + {{ phantom }} + {{ ocaml string option }} + {{ lem maybe string }} + metavar bool ::= {{ phantom }} {{ ocaml bool }} @@ -54,6 +59,7 @@ name :: '' ::= | id nat :: :: name | have_exception nat :: :: have_exception | current_exception nat :: :: current_exception + | throw_location nat :: :: throw_location | return nat :: :: return op :: '' ::= @@ -62,7 +68,6 @@ op :: '' ::= | and :: :: band | hd :: :: list_hd | tl :: :: list_tl - | bit_to_bool :: :: bit_to_bool | eq :: :: eq | neq :: :: neq % Integer ops @@ -92,7 +97,6 @@ op :: '' ::= cval :: 'V_' ::= | name : ctyp :: :: id - | '&' name : ctyp :: :: ref | value : ctyp :: :: lit | struct { uid0 = cval0 , ... , uidn = cvaln } ctyp :: :: struct | cval != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind @@ -152,6 +156,7 @@ ctyp :: 'CT_' ::= | variant id ( uid0 * ctyp0 , ... , uidn * ctypn ) :: :: variant % A vector type for non-bit vectors, and a (linked) list type. + | fvector ( nat , bool , ctyp ) :: :: fvector | vector ( bool , ctyp ) :: :: vector | list ( ctyp ) :: :: list @@ -240,7 +245,7 @@ cdef :: 'CDEF_' ::= instr0 ; ... ; instrm } :: :: let - | val id ( ctyp0 , ... , ctypn ) -> ctyp :: :: spec + | val id = mstring ( ctyp0 , ... , ctypn ) -> ctyp :: :: spec % If mid = Some id this indicates that the caller should allocate the % return type and passes a pointer to it as an extra argument id for diff --git a/language/sail.ott b/language/sail.ott index c0c8da49..9c47a4f1 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -229,7 +229,7 @@ typ :: 'Typ_' ::= | id :: :: id {{ com defined type }} | kid :: :: var {{ com type variable }} | ( typ1 , ... , typn ) -> typ2 effectkw effect :: :: fn {{ com Function (first-order only) }} - | typ1 <-> typ2 :: :: bidir {{ com Mapping }} + | typ1 <-> typ2 effectkw effect :: :: bidir {{ com Mapping }} | ( typ1 , .... , typn ) :: :: tup {{ com Tuple }} | id ( typ_arg1 , ... , typ_argn ) :: :: app {{ com type constructor application }} | ( typ ) :: S :: paren {{ ichlo [[typ]] }} |