diff options
| -rw-r--r-- | language/l2.lem | 162 | ||||
| -rw-r--r-- | language/l2.ml | 96 | ||||
| -rw-r--r-- | language/l2.ott | 14 | ||||
| -rw-r--r-- | language/l2_parse.ml | 3 | ||||
| -rw-r--r-- | language/l2_parse.ott | 5 |
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 % |