diff options
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 148 |
1 files changed, 74 insertions, 74 deletions
diff --git a/language/l2.lem b/language/l2.lem index 27af418a..3f02fc88 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -76,30 +76,30 @@ type base_effect = | BE_aux of base_effect_aux * l -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 effect_aux = (* effect set, of kind Effects *) + | Effect_var of kid + | Effect_set of list base_effect (* effect set *) + + 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 effect = - | Effect_aux of effect_aux * l - - type id = | Id_aux of id_aux * l +type effect = + | Effect_aux of effect_aux * l + + type order = | Ord_aux of order_aux * l @@ -156,10 +156,6 @@ type lit_aux = (* Literal constant *) | L_string of string (* string constant *) -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 *) @@ -181,6 +177,10 @@ and typ_arg = | Typ_arg_aux of typ_arg_aux * l +type typquant = + | TypQ_aux of typquant_aux * l + + type lit = | L_aux of lit_aux * l @@ -221,14 +221,7 @@ type reg_id_aux 'a = | RI_id of id -type letbind_aux 'a = (* Let binding *) - | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) - | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) - -and letbind 'a = - | LB_aux of (letbind_aux 'a) * annot 'a - -and exp_aux 'a = (* Expression *) +type exp_aux 'a = (* Expression *) | E_block of list (exp 'a) (* block *) | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) | E_id of id (* identifier *) @@ -297,16 +290,20 @@ and pexp_aux 'a = (* Pattern match *) and pexp 'a = | Pat_aux of (pexp_aux 'a) * annot 'a +and letbind_aux 'a = (* Let binding *) + | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) + | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) + +and letbind 'a = + | LB_aux of (letbind_aux 'a) * annot 'a + type reg_id 'a = | RI_aux of (reg_id_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 (reg_id 'a) * id - | AL_bit of (reg_id 'a) * (exp 'a) - | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) - | AL_concat of (reg_id 'a) * (reg_id 'a) +type tannot_opt_aux = (* Optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ type rec_opt_aux = (* Optional recursive annotation for functions *) @@ -314,19 +311,15 @@ type rec_opt_aux = (* Optional recursive annotation for functions *) | Rec_rec (* recursive *) -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 effect_opt_aux = (* Optional effect annotation for functions *) | Effect_opt_pure (* sugar for empty effect set *) | Effect_opt_effect of effect +type funcl_aux 'a = (* Function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) + + type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) | Name_sect_none | Name_sect_some of string @@ -337,26 +330,29 @@ type type_union_aux = (* Type union constructors *) | Tu_ty_id of typ * id -type alias_spec 'a = - | AL_aux of (alias_spec_aux 'a) * annot 'a - - -type rec_opt = - | Rec_aux of rec_opt_aux * l - - -type funcl 'a = - | FCL_aux of (funcl_aux 'a) * l +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 (reg_id 'a) * id + | AL_bit of (reg_id 'a) * (exp 'a) + | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) + | AL_concat of (reg_id 'a) * (reg_id 'a) type tannot_opt = | Typ_annot_opt_aux of tannot_opt_aux * l +type rec_opt = + | Rec_aux of rec_opt_aux * l + + type effect_opt = | Effect_opt_aux of effect_opt_aux * l +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * l + + type name_scm_opt = | Name_sect_aux of name_scm_opt_aux * l @@ -365,6 +361,10 @@ type type_union = | Tu_aux of type_union_aux * l +type alias_spec 'a = + | AL_aux of (alias_spec_aux 'a) * annot '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 *) @@ -374,16 +374,22 @@ and index_range = | BF_aux of index_range_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 fundef_aux 'a = (* Function definition *) | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) +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 default_spec_aux 'a = (* Default kinding or typing assumption *) + | DT_kind of base_kind * kid + | DT_order of order + | DT_typ of typschm * id + + type scattered_def_aux 'a = (* Function and type union definitions that can be spread across a file. Each one must end in $id$ *) | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) @@ -393,6 +399,12 @@ type scattered_def_aux 'a = (* Function and type union definitions that can be | SD_scattered_end of id (* scattered definition end *) +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 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 *) @@ -401,40 +413,28 @@ type type_def_aux 'a = (* Type definition body *) | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) -type default_spec_aux 'a = (* Default kinding or typing assumption *) - | DT_kind of base_kind * kid - | DT_order of order - | DT_typ of typschm * id - - -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 fundef 'a = + | FD_aux of (fundef_aux 'a) * annot 'a -type dec_spec 'a = - | DEC_aux of (dec_spec_aux 'a) * annot 'a +type val_spec 'a = + | VS_aux of (val_spec_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 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 default_spec 'a = - | DT_aux of (default_spec_aux 'a) * l +type dec_spec 'a = + | DEC_aux of (dec_spec_aux 'a) * annot 'a -type val_spec 'a = - | VS_aux of (val_spec_aux 'a) * annot 'a +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a type def 'a = (* Top-level definition *) @@ -589,10 +589,10 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should -type I = inf +type E = env -type E = env +type I = inf |