diff options
Diffstat (limited to 'language/l2.ml')
| -rw-r--r-- | language/l2.ml | 154 |
1 files changed, 77 insertions, 77 deletions
diff --git a/language/l2.ml b/language/l2.ml index bdbec809..ab0e7b66 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -150,6 +150,20 @@ typquant_aux = (* type quantifiers and constraints *) type +lit_aux = (* Literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | L_num of int (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* constant representing undefined values *) + | L_string of string (* string constant *) + + +type typquant = TypQ_aux of typquant_aux * l @@ -177,32 +191,13 @@ and typ_arg = type -lit_aux = (* Literal constant *) - L_unit (* $() : _$ *) - | L_zero (* $_ : _$ *) - | L_one (* $_ : _$ *) - | L_true (* $_ : _$ *) - | L_false (* $_ : _$ *) - | L_num of int (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) - - -type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * typ - - -type lit = L_aux of lit_aux * l type -typschm = - TypSchm_aux of typschm_aux * l +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ type @@ -231,6 +226,11 @@ and 'a fpat = type +typschm = + TypSchm_aux of typschm_aux * l + + +type 'a reg_id_aux = RI_id of id @@ -319,12 +319,6 @@ type 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 @@ -336,9 +330,8 @@ tannot_opt_aux = (* Optional type annotation for functions *) type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp type @@ -348,8 +341,15 @@ effect_opt_aux = (* Optional effect annotation for functions *) 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 +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type @@ -361,28 +361,28 @@ type type -name_scm_opt = - Name_sect_aux of name_scm_opt_aux * l +type_union = + Tu_aux of type_union_aux * l type -type_union = - Tu_aux of type_union_aux * l +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l 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 *) +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot -and index_range = - BF_aux of index_range_aux * l + +type +effect_opt = + Effect_opt_aux of effect_opt_aux * l type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * l +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l type @@ -391,13 +391,13 @@ rec_opt = type -effect_opt = - Effect_opt_aux of effect_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 *) -type -'a funcl = - FCL_aux of 'a funcl_aux * l +and index_range = + BF_aux of index_range_aux * l type @@ -406,6 +406,16 @@ 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 *) + + +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 *) @@ -415,18 +425,6 @@ type type -'a fundef_aux = (* Function definition *) - FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list - - -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 *) - - -type 'a default_spec_aux = (* Default kinding or typing assumption *) DT_kind of base_kind * kid | DT_order of order @@ -434,13 +432,8 @@ 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 fundef_aux = (* Function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list type @@ -451,18 +444,20 @@ type type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot +'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 fundef = - FD_aux of 'a fundef_aux * 'a annot +'a scattered_def = + SD_aux of 'a scattered_def_aux * 'a annot type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +'a type_def = + TD_aux of 'a type_def_aux * 'a annot type @@ -471,8 +466,8 @@ type type -'a scattered_def = - SD_aux of 'a scattered_def_aux * 'a annot +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type @@ -481,6 +476,11 @@ type type +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot + + +type 'a def = (* Top-level definition *) DEF_type of 'a type_def (* type definition *) | DEF_fundef of 'a fundef (* function definition *) |