diff options
Diffstat (limited to 'src/parse_ast.ml')
| -rw-r--r-- | src/parse_ast.ml | 85 |
1 files changed, 46 insertions, 39 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 62c90132..ba948040 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -50,6 +50,7 @@ (* generated by Ott 0.25 from: l2_parse.ott *) +module Big_int = Nat_big_num type text = string @@ -72,7 +73,6 @@ 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_effect (* kind of effect sets *) type @@ -139,7 +139,7 @@ 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 kid (* ticked variable *) - | ATyp_constant of int (* constant *) + | ATyp_constant of Big_int.num (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_minus of atyp * atyp (* subtraction *) @@ -150,38 +150,42 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) | 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_wild | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) + | ATyp_exist of kid list * n_constraint * atyp and atyp = ATyp_aux of atyp_aux * l -type +and kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of kid (* identifier *) | KOpt_kind of kind * kid (* kind-annotated variable *) -type +and n_constraint_aux = (* constraint over kind $_$ *) - NC_fixed of atyp * atyp + NC_equal of atyp * atyp | NC_bounded_ge of atyp * atyp | NC_bounded_le of atyp * atyp - | NC_nat_set_bounded of kid * (int) list - + | NC_not_equal of atyp * atyp + | NC_set of kid * (Big_int.num) list + | NC_or of n_constraint * n_constraint + | NC_and of n_constraint * n_constraint + | NC_true + | NC_false + +and +n_constraint = + NC_aux of n_constraint_aux * l type kinded_id = KOpt_aux of kinded_id_aux * l - -type -n_constraint = - NC_aux of n_constraint_aux * l - - -type +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 n_constraint (* A constraint for this type *) @@ -210,12 +214,12 @@ lit_aux = (* Literal constant *) | L_one (* $_ : _$ *) | L_true (* $_ : _$ *) | L_false (* $_ : _$ *) - | L_num of int (* natural number constant *) + | L_num of Big_int.num (* natural number constant *) | L_hex of string (* bit vector constant, C-style *) | L_bin of string (* bit vector constant, C-style *) | L_undef (* undefined value *) | L_string of string (* string constant *) - + | L_real of string type typschm_aux = (* type scheme *) @@ -236,16 +240,16 @@ type pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) - | P_as of pat * id (* named pattern *) | P_typ of atyp * pat (* typed pattern *) | P_id of id (* identifier *) + | P_var of pat * atyp (* bind pat to type variable *) | P_app of id * (pat) list (* union constructor pattern *) | P_record of (fpat) list * bool (* struct pattern *) | P_vector of (pat) list (* vector pattern *) - | P_vector_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *) | P_vector_concat of (pat) list (* concatenated vector pattern *) | P_tup of (pat) list (* tuple pattern *) | P_list of (pat) list (* list pattern *) + | P_cons of pat * pat (* cons pattern *) and pat = P_aux of pat_aux * l @@ -256,21 +260,24 @@ and fpat_aux = (* Field pattern *) and fpat = FP_aux of fpat_aux * l +type loop = While | Until type exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) | E_id of id (* identifier *) + | E_ref of id + | E_deref of exp | E_lit of lit (* literal constant *) | E_cast of atyp * exp (* cast *) | E_app of id * (exp) list (* function application *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of (exp) list (* tuple *) | E_if of exp * exp * exp (* conditional *) + | E_loop of loop * exp * exp | E_for of id * exp * exp * exp * atyp * exp (* loop *) | E_vector of (exp) list (* vector (indexed from 0) *) - | E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *) | E_vector_access of exp * exp (* vector access *) | E_vector_subrange of exp * exp * exp (* subvector extraction *) | E_vector_update of exp * exp * exp (* vector functional update *) @@ -278,16 +285,20 @@ exp_aux = (* Expression *) | E_vector_append of exp * exp (* vector concatenation *) | E_list of (exp) list (* list *) | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) + | E_record of exp list (* struct *) | E_record_update of exp * (exp) list (* functional update of struct *) | E_field of exp * id (* field projection from struct *) | E_case of exp * (pexp) list (* pattern matching *) | E_let of letbind * exp (* let expression *) | E_assign of exp * exp (* imperative assignment *) | E_sizeof of atyp + | E_constraint of n_constraint | E_exit of exp + | E_throw of exp + | E_try of exp * pexp list | E_return of exp | E_assert of exp * exp + | E_var of exp * exp * exp and exp = E_aux of exp_aux * l @@ -313,13 +324,13 @@ and opt_default = and pexp_aux = (* Pattern match *) Pat_exp of pat * exp + | Pat_when of pat * exp * exp and pexp = Pat_aux of pexp_aux * l and letbind_aux = (* Let binding *) - LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) + LB_val of pat * exp (* value binding, implicit type (pat must be total) *) and letbind = LB_aux of letbind_aux * l @@ -345,7 +356,7 @@ rec_opt_aux = (* Optional recursive annotation for functions *) type funcl_aux = (* Function clause *) - FCL_Funcl of id * pat * exp + FCL_Funcl of id * pexp type @@ -387,8 +398,8 @@ type_union = 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_single of Big_int.num (* single index *) + | BF_range of Big_int.num * Big_int.num (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) and index_range = @@ -418,24 +429,16 @@ type_def_aux = (* Type definition body *) | 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 *) - + | TD_bitfield of id * atyp * (id * index_range) list (* register mutable bitfield type definition *) 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 + VS_val_spec of typschm * id * (string -> string option) * bool type kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *) KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) - | KD_record of kind * id * name_scm_opt * typquant * ((atyp * 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 * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) - type dec_spec_aux = (* Register declarations *) @@ -488,17 +491,24 @@ type scattered_def = SD_aux of scattered_def_aux * l +type prec = Infix | InfixL | InfixR -type +type fixity_token = (prec * Big_int.num * string) + +type def = (* Top-level definition *) DEF_kind of kind_def (* definition of named kind identifiers *) | DEF_type of type_def (* type definition *) | DEF_fundef of fundef (* function definition *) | DEF_val of letbind (* value definition *) + | DEF_overload of id * id list (* operator overload specifications *) + | DEF_fixity of prec * Big_int.num * id (* fixity declaration *) | 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 dec_spec (* register declaration *) + | DEF_pragma of string * string * l + | DEF_internal_mutrec of fundef list type @@ -516,6 +526,3 @@ and lexp = type defs = (* Definition sequence *) Defs of (def) list - - - |