Extend language to support register aliases and to support interrupts, traps and the like.

5 files changed, 166 insertions, 114 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 3b86d2db..e3a52dfa 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -76,30 +76,30 @@ type base_effect =
  | BE_aux of base_effect_aux * l
 
 
-type id_aux =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
 type effect_aux =  (* effect set, of kind Effects *)
  | Effect_var of kid
  | Effect_set of list base_effect (* effect set *)
 
 
+type id_aux =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
 type order_aux =  (* vector order specifications, of kind Order *)
  | Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type id = 
- | Id_aux of id_aux * l
-
-
 type effect = 
  | Effect_aux of effect_aux * l
 
 
+type id = 
+ | Id_aux of id_aux * l
+
+
 type order = 
  | Ord_aux of order_aux * l
 
@@ -143,6 +143,10 @@ type typquant_aux =  (* type quantifiers and constraints *)
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
+type typquant = 
+ | TypQ_aux of typquant_aux * l
+
+
 type typ_aux =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_id of id (* Defined type *)
@@ -164,10 +168,6 @@ and typ_arg =
  | Typ_arg_aux of typ_arg_aux * l
 
 
-type typquant = 
- | TypQ_aux of typquant_aux * l
-
-
 type lit_aux =  (* Literal constant *)
  | L_unit (* $() : unit$ *)
  | L_zero (* $bitzero : bit$ *)
@@ -243,6 +243,7 @@ type exp_aux 'a =  (* Expression *)
  | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
  | E_let of (letbind 'a) * (exp 'a) (* let expression *)
  | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
+ | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
  | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
  | E_internal_exp of annot 'a (* This is an internal use of an nexp (in the annot) for passing length information after resolution of constraints *)
 
@@ -293,6 +294,23 @@ and letbind 'a =
  | LB_aux of (letbind_aux 'a) * annot 'a
 
 
+type alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
+ | AL_subreg of id * id (* id must refer to a register, id' to a declared subregister of id *)
+ | AL_bit of id * (exp 'a)
+ | AL_slice of id * (exp 'a) * (exp 'a)
+ | AL_concat of id * id (* both id and id' must refer to a register *)
+
+
+type type_union_aux =  (* Type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
+
+
+type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
+
+
 type rec_opt_aux =  (* Optional recursive annotation for functions *)
  | Rec_nonrec (* non-recursive *)
  | Rec_rec (* recursive *)
@@ -303,22 +321,33 @@ type effect_opt_aux =  (* Optional effect annotation for functions *)
  | Effect_opt_effect of effect
 
 
-type type_union_aux =  (* Type union constructors *)
- | Tu_id of id
- | Tu_ty_id of typ * id
+type tannot_opt_aux =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
 
 
 type funcl_aux 'a =  (* Function clause *)
  | FCL_Funcl of id * (pat 'a) * (exp 'a)
 
 
-type tannot_opt_aux =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
+type alias_spec 'a = 
+ | AL_aux of (alias_spec_aux 'a) * annot 'a
 
 
-type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
+type type_union = 
+ | Tu_aux of type_union_aux * l
+
+
+type name_scm_opt = 
+ | Name_sect_aux of name_scm_opt_aux * l
+
+
+type index_range_aux =  (* index specification, for bitfields in register types *)
+ | BF_single of integer (* single index *)
+ | BF_range of integer * integer (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+ | BF_aux of index_range_aux * l
 
 
 type rec_opt = 
@@ -329,33 +358,36 @@ type effect_opt =
  | Effect_opt_aux of effect_opt_aux * l
 
 
-type type_union = 
- | Tu_aux of type_union_aux * l
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type funcl 'a = 
  | FCL_aux of (funcl_aux 'a) * l
 
 
-type tannot_opt = 
- | Typ_annot_opt_aux of tannot_opt_aux * l
-
+type val_spec_aux 'a =  (* Value type specification *)
+ | VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
 
-type name_scm_opt = 
- | Name_sect_aux of name_scm_opt_aux * l
 
+type dec_spec_aux 'a =  (* Register declarations *)
+ | DEC_reg of typ * id
+ | DEC_alias of id * (alias_spec 'a)
+ | DEC_typ_alias of typ * id * (alias_spec 'a)
 
-type index_range_aux =  (* index specification, for bitfields in register types *)
- | BF_single of integer (* single index *)
- | BF_range of integer * integer (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
-and index_range = 
- | BF_aux of index_range_aux * l
+type type_def_aux 'a =  (* Type definition body *)
+ | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type dec_spec_aux 'a =  (* Register declarations *)
- | DEC_reg of typ * id
+type fundef_aux 'a =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
 
 type scattered_def_aux 'a =  (* Function and type union definitions that can be spread across
@@ -367,51 +399,33 @@ type scattered_def_aux 'a =  (* Function and type union definitions that can be
  | SD_scattered_end of id (* scattered definition end *)
 
 
-type fundef_aux 'a =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
-
-
 type default_spec_aux 'a =  (* Default kinding or typing assumption *)
  | DT_kind of base_kind * kid
  | DT_typ of typschm * id
 
 
-type type_def_aux 'a =  (* Type definition body *)
- | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
-
-
-type val_spec_aux 'a =  (* Value type specification *)
- | VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+type val_spec 'a = 
+ | VS_aux of (val_spec_aux 'a) * annot 'a
 
 
 type dec_spec 'a = 
  | DEC_aux of (dec_spec_aux 'a) * annot 'a
 
 
-type scattered_def 'a = 
- | SD_aux of (scattered_def_aux 'a) * annot 'a
+type type_def 'a = 
+ | TD_aux of (type_def_aux 'a) * annot 'a
 
 
 type fundef 'a = 
  | FD_aux of (fundef_aux 'a) * annot 'a
 
 
-type default_spec 'a = 
- | DT_aux of (default_spec_aux 'a) * l
-
-
-type type_def 'a = 
- | TD_aux of (type_def_aux 'a) * annot 'a
+type scattered_def 'a = 
+ | SD_aux of (scattered_def_aux 'a) * annot 'a
 
 
-type val_spec 'a = 
- | VS_aux of (val_spec_aux 'a) * annot 'a
+type default_spec 'a = 
+ | DT_aux of (default_spec_aux 'a) * l
 
 
 type def 'a =  (* Top-level definition *)
@@ -488,6 +502,16 @@ type tid =  (* A type identifier or type variable *)
  | Tid_var of kid
 
 
+type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
+ | Tag_empty
+ | Tag_global (* Globally let-bound or enumeration based value/variable *)
+ | Tag_ctor (* Data constructor from a type union *)
+ | Tag_extern of maybe string (* External function, specied only with a val statement *)
+ | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
+ | Tag_spec
+ | Tag_enum
+
+
 type t =  (* Internal types *)
  | T_id of x
  | T_var of x
@@ -506,16 +530,6 @@ and t_args =  (* Arguments to type constructors *)
  | T_args of list t_arg
 
 
-type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
- | Tag_empty
- | Tag_global (* Globally let-bound or enumeration based value/variable *)
- | Tag_ctor (* Data constructor from a type union *)
- | Tag_extern of maybe string (* External function, specied only with a val statement *)
- | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
- | Tag_spec
- | Tag_enum
-
-
 type tinf =  (* Type variables, type, and constraints, bound to an identifier *)
  | Tinf_typ of t
  | Tinf_quant_typ of (map tid kinf) * list nec * tag * t
@@ -565,10 +579,10 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should
 
 
 
-type E = env
+type I = inf
 
 
-type I = inf
+type E = env
 
 
 
diff --git a/language/l2.ml b/language/l2.ml
index a13ce981..60343397 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -164,6 +164,11 @@ lit_aux =  (* Literal constant *)
 
 
 type 
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
 typ_aux =  (* Type expressions, of kind $_$ *)
    Typ_wild (* Unspecified type *)
  | Typ_id of id (* Defined type *)
@@ -186,11 +191,6 @@ and typ_arg =
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
 lit = 
    L_aux of lit_aux * l
 
@@ -257,6 +257,7 @@ type
  | E_case of 'a exp * ('a pexp) list (* pattern matching *)
  | E_let of 'a letbind * 'a exp (* let expression *)
  | E_assign of 'a lexp * 'a exp (* imperative assignment *)
+ | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
  | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
  | E_internal_exp of 'a annot (* This is an internal use of an nexp (in the annot) for passing length information after resolution of constraints *)
 
@@ -308,20 +309,22 @@ and 'a letbind =
 
 
 type 
-effect_opt_aux =  (* Optional effect annotation for functions *)
-   Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of effect
+'a alias_spec_aux =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
+   AL_subreg of id * id (* id must refer to a register, id' to a declared subregister of id *)
+ | AL_bit of id * 'a exp
+ | AL_slice of id * 'a exp * 'a exp
+ | AL_concat of id * id (* both id and id' must refer to a register *)
 
 
 type 
-tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_some of typquant * typ
+type_union_aux =  (* Type union constructors *)
+   Tu_id of id
+ | Tu_ty_id of typ * id
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_some of typquant * typ
 
 
 type 
@@ -330,30 +333,36 @@ type
 
 
 type 
+effect_opt_aux =  (* Optional effect annotation for functions *)
+   Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
+
+
+type 
 name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
    Name_sect_none
  | Name_sect_some of string
 
 
 type 
-type_union_aux =  (* Type union constructors *)
-   Tu_id of id
- | Tu_ty_id of typ * id
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-effect_opt = 
-   Effect_opt_aux of effect_opt_aux * l
+'a alias_spec = 
+   AL_aux of 'a alias_spec_aux * 'a annot
 
 
 type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * l
+type_union = 
+   Tu_aux of type_union_aux * l
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
@@ -362,13 +371,18 @@ type
 
 
 type 
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
+
+
+type 
 name_scm_opt = 
    Name_sect_aux of name_scm_opt_aux * l
 
 
 type 
-type_union = 
-   Tu_aux of type_union_aux * l
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
@@ -382,8 +396,10 @@ and index_range =
 
 
 type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+'a dec_spec_aux =  (* Register declarations *)
+   DEC_reg of typ * id
+ | DEC_alias of id * 'a alias_spec
+ | DEC_typ_alias of typ * id * 'a alias_spec
 
 
 type 
@@ -397,8 +413,12 @@ type
 
 
 type 
-'a dec_spec_aux =  (* Register declarations *)
-   DEC_reg of typ * id
+'a type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
 
 
 type 
@@ -408,12 +428,8 @@ type
 
 
 type 
-'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
 
 
 type 
@@ -424,8 +440,8 @@ type
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a dec_spec = 
+   DEC_aux of 'a dec_spec_aux * 'a annot
 
 
 type 
@@ -434,8 +450,8 @@ type
 
 
 type 
-'a dec_spec = 
-   DEC_aux of 'a dec_spec_aux * 'a annot
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
@@ -444,8 +460,8 @@ type
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
diff --git a/language/l2.ott b/language/l2.ott
index 55bad070..1a4d2038 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -632,6 +632,9 @@ exp :: 'E_' ::=
   | lexp := exp                                      :: :: assign
     {{ com imperative assignment }}
 
+  | exit exp						:: :: exit
+    {{ com expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp }}
+
   | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
   | ( annot ) exp                                       :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }}
   | annot                                               :: :: internal_exp {{ com This is an internal use of an nexp (in the annot) for passing length information after resolution of constraints }}
@@ -825,11 +828,22 @@ scattered_def :: 'SD_' ::=
   | end id  :: :: scattered_end
 {{ com scattered definition end }}
 
+alias_spec :: 'AL_' ::=
+  {{ com Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector }}
+  {{ aux _ annot }} {{ auxparam 'a }}
+  | id . id'							:: :: subreg
+  {{ com id must refer to a register, id' to a declared subregister of id }}
+  | id [ exp ] 							:: :: bit
+  | id [ exp '..' exp' ]					:: :: slice
+  | id : id'  	    						:: :: concat
+  {{ com both id and id' must refer to a register }}
 
 dec_spec :: 'DEC_' ::=
   {{ com Register declarations }}
   {{ aux _ annot }} {{ auxparam 'a }}
   | register typ id                                             :: :: reg
+  | register alias id = alias_spec				:: :: alias
+  | register alias typ id = alias_spec				:: :: typ_alias
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Top-level definitions                                        %
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index a96f1992..d0c8f1a8 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -224,6 +224,7 @@ exp_aux =  (* Expression *)
  | E_case of exp * (pexp) list (* pattern matching *)
  | E_let of letbind * exp (* let expression *)
  | E_assign of exp * exp (* imperative assignment *)
+ | E_exit of exp
 
 and exp = 
    E_aux of exp_aux * l
@@ -353,6 +354,8 @@ fundef_aux =  (* Function definition *)
 type 
 dec_spec_aux =  (* Register declarations *)
    DEC_reg of atyp * id
+ | DEC_alias of id * exp
+ | DEC_typ_alias of atyp * id * exp
 
 
 type 
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index a655959d..9785290f 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -521,6 +521,8 @@ exp :: 'E_' ::=
   | exp := exp'                                      :: :: assign
     {{ com imperative assignment }}
 
+  | exit exp						:: :: exit
+
   | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
 
 
@@ -723,6 +725,9 @@ dec_spec :: 'DEC_' ::=
   {{ com Register declarations }}
   {{ aux _ l }}
   | register atyp id                                             :: :: reg
+  | register alias id = exp	      	 			 :: :: alias
+  | register alias atyp id = exp	  			 :: :: typ_alias
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Top-level definitions                                        %