Merge branch 'sail2' into rmem_interpreter

2 files changed, 43 insertions, 69 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 = {
diff --git a/language/sail.ott b/language/sail.ott
index b3df66bb..00a62fe3 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -119,44 +119,16 @@ l :: '' ::=                                     {{ phantom }}
     {{ hol () }}
 
 annot :: '' ::=
-                                                {{ phantom }}
-                                                {{ ocaml 'a annot }}
-                                                {{ lem annot 'a }}
-                                                {{ hol unit }}
+  {{ phantom }}
+  {{ ocaml 'a annot }}
+  {{ lem annot 'a }}
+  {{ hol unit }}
 
 id :: '' ::=
   {{ com Identifier }}
   {{ aux _ l }}
-  | x                           :: :: id
-  | ( deinfix x )                       :: D :: deIid {{ com remove infix status }}
-  | bool      		   	 :: M :: bool {{ com built in type identifiers }} {{ ichlo (Id "bool") }}
-  | bit				 :: M :: bit {{ ichlo (Id "bit") }}
-  | unit			 :: M :: unit {{ ichlo (Id "unit") }}
-  | nat				 :: M :: nat  {{ ichlo (Id "nat") }}
-  | int				 :: M :: int  {{ ichlo (Id "int") }}
-  | string                       :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }}
-  | range                        :: M :: range {{ ichlo (Id "range") }}
-  | atom			 :: M :: atom {{ ichlo (Id "atom") }}
-  | vector			 :: M :: vector {{ ichlo (Id "vector") }}
-  | list			 :: M :: list {{ ichlo (Id "list") }}
-%  | set                          :: M :: set {{ ichlo (Id "set") }}
-  | reg                          :: M :: reg {{ ichlo (Id "reg") }}
-  | to_num			 :: M :: tonum {{ com built-in function identifiers }} {{ ichlo (Id "to_num") }}
-  | to_vec			 :: M :: tovec {{ ichlo (Id "to_vec") }}
-  | msb                          :: M :: msb {{ ichlo (Id "msb") }}
-% Note: we have just a single namespace. We don't want the same
-% identifier to be reused as a type name or variable, expression
-% variable, and field name.  We don't enforce any lexical convention
-% on type variables (or variables of other kinds)
-% We don't enforce a lexical convention on infix operators, as some of the 
-% targets use alphabetical infix operators.
-
-% Vector builtins
-  | vector_access          :: M :: vector_access  {{ ichlo (Id "vector_access") }} 
-  | vector_update          :: M :: vector_update  {{ ichlo (Id "vector_update") }}
-  | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }}
-  | vector_subrange        :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }}
-  | vector_append          :: M :: vector_append {{ ichlo (Id "vector_append") }}
+  | x              :: :: id
+  | ( operator x ) :: D :: operator {{ com remove infix status }}
 
 kid :: '' ::=
   {{ com kinded IDs: Type, Int, and Order variables }}
@@ -180,23 +152,23 @@ kind :: 'K_' ::=
 nexp :: 'Nexp_' ::=
   {{ com numeric expression, of kind Int }}
   {{ aux _ l }}
-  | id                                  :: :: id       {{ com abbreviation identifier }}
-  | kid                                 :: :: var      {{ com variable }}
-  | num                                 :: :: constant {{ com constant }}
-  | id ( nexp1 , ... , nexpn )          :: :: app      {{ com app }}
-  | nexp1 * nexp2                       :: :: times    {{ com product }}
-  | nexp1 + nexp2                       :: :: sum      {{ com sum }}
-  | nexp1 - nexp2                       :: :: minus    {{ com subtraction }}
-  | 2** nexp                            :: :: exp      {{ com exponential }}
-  | neg nexp                            :: I :: neg    {{ com for internal use only}}
-  | ( nexp )                            :: S :: paren  {{ ichlo [[nexp]] }}
+  | id                         :: :: id       {{ com abbreviation identifier }}
+  | kid                        :: :: var      {{ com variable }}
+  | num                        :: :: constant {{ com constant }}
+  | id ( nexp1 , ... , nexpn ) :: :: app      {{ com app }}
+  | nexp1 * nexp2              :: :: times    {{ com product }}
+  | nexp1 + nexp2              :: :: sum      {{ com sum }}
+  | nexp1 - nexp2              :: :: minus    {{ com subtraction }}
+  | 2 ^ nexp                   :: :: exp      {{ com exponential }}
+  | - nexp                     :: :: neg      {{ com unary negation}}
+  | ( nexp )                   :: S :: paren  {{ ichlo [[nexp]] }}
 
 order :: 'Ord_' ::=
   {{ com vector order specifications, of kind Order }}
   {{ aux _ l }}
   | kid                                 :: :: var {{ com variable }} 
-  | inc                                 :: :: inc  {{ com increasing }}
-  | dec                                 :: :: dec  {{ com decreasing }}
+  | inc                                 :: :: inc {{ com increasing }}
+  | dec                                 :: :: dec {{ com decreasing }}
   | ( order )                           :: S :: paren {{ ichlo [[order]] }}
 
 base_effect :: 'BE_' ::=