diff options
Diffstat (limited to 'language/l2_parse.ml')
| -rw-r--r-- | language/l2_parse.ml | 174 |
1 files changed, 80 insertions, 94 deletions
diff --git a/language/l2_parse.ml b/language/l2_parse.ml index b196f007..a6ada0ec 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.22 from: l2_parse.ott *) +(* generated by Ott 0.23 from: l2_parse.ott *) type text = string @@ -21,7 +21,7 @@ base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) + | BK_effect (* kind of effect sets *) type @@ -31,19 +31,19 @@ id_aux = (* Identifier *) type -var_aux = (* variables with kind, ticked to differntiate from program variables *) +kid_aux = (* identifiers with kind, ticked to differntiate from program variables *) Var of x type -efct_aux = (* effect *) - Effect_rreg (* read register *) - | Effect_wreg (* write register *) - | Effect_rmem (* read memory *) - | Effect_wmem (* write memory *) - | Effect_undef (* undefined-instruction exception *) - | Effect_unspec (* unspecified values *) - | Effect_nondet (* nondeterminism from intra-instruction parallelism *) +base_effect_aux = (* effect *) + BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) type @@ -57,13 +57,13 @@ id = type -var = - Var_aux of var_aux * l +kid = + Kid_aux of kid_aux * l type -efct = - Effect_aux of efct_aux * l +base_effect = + BE_aux of base_effect_aux * l type @@ -74,17 +74,14 @@ kind_aux = (* kinds *) type atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) ATyp_id of id (* identifier *) - | ATyp_var of var (* ticked variable *) + | ATyp_var of kid (* ticked variable *) | ATyp_constant of int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_exp of atyp (* exponential *) | ATyp_inc (* increasing (little-endian) *) | ATyp_dec (* decreasing (big-endian) *) - | ATyp_efid of id - | ATyp_efvar of var - | ATyp_set of (efct) list (* effect set *) - | ATyp_wild (* Unspecified type *) + | ATyp_set of (base_effect) list (* effect set *) | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) @@ -99,22 +96,22 @@ kind = type -nexp_constraint_aux = (* constraint over kind $_$ *) +n_constraint_aux = (* constraint over kind $_$ *) NC_fixed of atyp * atyp | NC_bounded_ge of atyp * atyp | NC_bounded_le of atyp * atyp - | NC_nat_set_bounded of id * (int) list + | NC_nat_set_bounded of kid * (int) list type kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of var (* identifier *) - | KOpt_kind of kind * var (* kind-annotated variable *) + KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +n_constraint = + NC_aux of n_constraint_aux * l type @@ -125,7 +122,7 @@ kinded_id = type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) + | QI_const of n_constraint (* A constraint for this type *) type @@ -254,15 +251,21 @@ and letbind = 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 atyp * id type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type @@ -272,9 +275,9 @@ tannot_opt_aux = (* Optional type annotation for functions *) type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of atyp type @@ -283,14 +286,8 @@ funcl_aux = (* Function clause *) type -effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of atyp - - -type -type_union = - Tu_aux of type_union_aux * l +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l type @@ -304,8 +301,13 @@ and index_range = type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +type_union = + Tu_aux of type_union_aux * l + + +type +rec_opt = + Rec_aux of rec_opt_aux * l type @@ -314,8 +316,8 @@ tannot_opt = type -rec_opt = - Rec_aux of rec_opt_aux * l +effect_opt = + Effect_opt_aux of effect_opt_aux * l type @@ -324,40 +326,55 @@ funcl = type -effects_opt = - Effects_opt_aux of effects_opt_aux * l +type_def_aux = (* Type definition body *) + TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * ((atyp * 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 * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) type -type_def_aux = (* Type definition body *) - TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * (type_union) list * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *) - | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) +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 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 +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 type default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * var + DT_kind of base_kind * kid | DT_typ of typschm * id type fundef_aux = (* Function definition *) - FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list + FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list type -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 +type_def = + TD_aux of type_def_aux * l type -type_def = - TD_aux of type_def_aux * l +scattered_def = + SD_aux of scattered_def_aux * l + + +type +val_spec = + VS_aux of val_spec_aux * l type @@ -371,23 +388,14 @@ fundef = type -val_spec = - VS_aux of val_spec_aux * l - - -type def_aux = (* Top-level definition *) DEF_type of type_def (* type definition *) | DEF_fundef of fundef (* function definition *) | DEF_val of letbind (* value definition *) | DEF_spec of val_spec (* top-level type constraint *) | DEF_default of default_typing_spec (* default kind and type assumptions *) + | DEF_scattered of scattered_def (* scattered definition *) | DEF_reg_dec of atyp * id (* register declaration *) - | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of funcl (* scattered function definition clause *) - | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of id * atyp * id (* scattered union definition member *) - | DEF_scattered_end of id (* scattered definition end *) type @@ -396,26 +404,9 @@ def = type -typ_lib_aux = (* library types and syntactic sugar for them *) - Typ_lib_unit (* unit type with value $()$ *) - | Typ_lib_bool (* booleans $_$ and $_$ *) - | Typ_lib_bit (* pure bit values (not mutable bits) *) - | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) - | Typ_lib_enum (* natural numbers _ .. _+_-1, ordered by order *) - | Typ_lib_enum1 (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of atyp (* vector of atyp, indexed by natural range *) - | Typ_lib_vector2 of atyp (* sugar for vector indexed by [ atyp ] *) - | Typ_lib_vector3 of atyp (* sugar for vector indexed by [ atyp.._ ] *) - | Typ_lib_list of atyp (* list of atyp *) - | Typ_lib_set of atyp (* finite set of atyp *) - | Typ_lib_reg of atyp (* mutable register components holding atyp *) - - -type lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) + | LEXP_mem of id * (exp) list | LEXP_vector of lexp * exp (* vector element *) | LEXP_vector_range of lexp * exp * exp (* subvector *) | LEXP_field of lexp * id (* struct field *) @@ -429,9 +420,4 @@ defs = (* Definition sequence *) Defs of (def) list -type -typ_lib = - Typ_lib_aux of typ_lib_aux * l - - |