diff options
Diffstat (limited to 'language/l2.ml')
| -rw-r--r-- | language/l2.ml | 151 |
1 files changed, 84 insertions, 67 deletions
diff --git a/language/l2.ml b/language/l2.ml index b8e31514..fbc52b10 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -25,6 +25,12 @@ base_kind = type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type kid_aux = (* variables with kind, ticked to differntiate from program variables *) Var of x @@ -35,6 +41,11 @@ kind_aux = (* kinds *) type +id = + Id_aux of id_aux * l + + +type kid = Kid_aux of kid_aux * l @@ -46,11 +57,12 @@ kind = type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) - Nexp_var of kid (* variable *) + Nexp_id of id (* identifier, bound by def Nat x = nexp *) + | Nexp_var of kid (* variable *) | Nexp_constant of int (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) - | Nexp_minus of nexp * nexp (* subtraction, error for nexp1 to be smaller than nexp2 *) + | Nexp_minus of nexp * nexp (* subtraction *) | Nexp_exp of nexp (* exponential *) | Nexp_neg of nexp (* For internal use *) @@ -88,12 +100,6 @@ order_aux = (* vector order specifications, of kind Order *) 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 (base_effect) list (* effect set *) @@ -105,11 +111,6 @@ order = type -id = - Id_aux of id_aux * l - - -type effect = Effect_aux of effect_aux * l @@ -175,10 +176,7 @@ typquant = type -typ_arg = - Typ_arg_aux of typ_arg_aux * l - -and typ_aux = (* Type expressions, of kind $_$ *) +typ_aux = (* Type expressions, of kind $_$ *) Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) | Typ_var of kid (* Type variable *) @@ -195,6 +193,9 @@ and typ_arg_aux = (* Type constructor arguments of all kinds *) | Typ_arg_order of order | Typ_arg_effect of effect +and typ_arg = + Typ_arg_aux of typ_arg_aux * l + type lit = @@ -338,13 +339,9 @@ type_union_aux = (* Type union constructors *) type -tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_some of typquant * typ - - -type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * 'a exp +name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string type @@ -354,9 +351,8 @@ effect_opt_aux = (* Optional effect annotation for functions *) type -name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp type @@ -366,6 +362,11 @@ rec_opt_aux = (* Optional recursive annotation for functions *) type +tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_some of typquant * typ + + +type '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 'a reg_id * id | AL_bit of 'a reg_id * 'a exp @@ -379,13 +380,18 @@ type_union = type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * l +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of int (* single index *) + | BF_range of int * int (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * l type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l type @@ -394,8 +400,8 @@ effect_opt = type -name_scm_opt = - Name_sect_aux of name_scm_opt_aux * l +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type @@ -404,13 +410,8 @@ rec_opt = type -index_range_aux = (* index specification, for bitfields in register types *) - BF_single of int (* single index *) - | BF_range of int * int (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - -and index_range = - BF_aux of index_range_aux * l +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l type @@ -419,13 +420,10 @@ type type -'a scattered_def_aux = (* Function and type union definitions that can be spread across - a file. Each one must end in $_$ *) - SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) - | SD_scattered_funcl of 'a funcl (* scattered function definition clause *) - | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) - | SD_scattered_unioncl of id * type_union (* scattered union definition member *) - | SD_scattered_end of id (* scattered definition end *) +'a default_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * kid + | DT_order of order + | DT_typ of typschm * id type @@ -438,10 +436,30 @@ type type -'a default_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * kid - | DT_order of order - | DT_typ of typschm * id +'a val_spec_aux = (* 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 +'a kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *) + KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) + | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) + | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) + | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) + + +type +'a scattered_def_aux = (* Function and type union definitions that can be spread across + a file. Each one must end in $_$ *) + SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of 'a funcl (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) type @@ -457,25 +475,28 @@ type type -'a val_spec_aux = (* 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 *) +'a default_spec = + DT_aux of 'a default_spec_aux * l type -'a scattered_def = - SD_aux of 'a scattered_def_aux * 'a annot +'a type_def = + TD_aux of 'a type_def_aux * 'a annot type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type -'a default_spec = - DT_aux of 'a default_spec_aux * l +'a kind_def = + KD_aux of 'a kind_def_aux * 'a annot + + +type +'a scattered_def = + SD_aux of 'a scattered_def_aux * 'a annot type @@ -489,17 +510,13 @@ type type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot - - -type 'a dec_comm = (* Top-level generated comments *) DC_comm of string (* generated unstructured comment *) | DC_comm_struct of 'a def (* generated structured comment *) and 'a def = (* Top-level definition *) - DEF_type of 'a type_def (* type definition *) + DEF_kind of 'a kind_def (* definition of named kind identifiers *) + | DEF_type of 'a type_def (* type definition *) | DEF_fundef of 'a fundef (* function definition *) | DEF_val of 'a letbind (* value definition *) | DEF_spec of 'a val_spec (* top-level type constraint *) |