diff options
Diffstat (limited to 'src/parse_ast.ml')
| -rw-r--r-- | src/parse_ast.ml | 123 |
1 files changed, 45 insertions, 78 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml index a4052d82..65b11373 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -56,7 +56,7 @@ type text = string type l = | Unknown - | Int of string * l option + | Unique of int * l | Generated of l | Range of Lexing.position * Lexing.position | Documented of string * l @@ -70,15 +70,16 @@ type x = text (* identifier *) type ix = text (* infix identifier *) type -base_kind_aux = (* base kind *) - BK_type (* kind of types *) - | BK_int (* kind of natural number size expressions *) - | BK_order (* kind of vector order specifications *) +kind_aux = (* base kind *) + K_type (* kind of types *) + | K_int (* kind of natural number size expressions *) + | K_order (* kind of vector order specifications *) + | K_bool (* kind of constraints *) type -base_kind = - BK_aux of base_kind_aux * l +kind = + K_aux of kind_aux * l type @@ -110,13 +111,7 @@ id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) - -type -kind_aux = (* kinds *) - K_kind of (base_kind) list - - -type +type base_effect = BE_aux of base_effect_aux * l @@ -128,19 +123,32 @@ kid = type id = - Id_aux of id_aux * l + Id_aux of id_aux * l +type +lit_aux = (* Literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | 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 -kind = - K_aux of kind_aux * l - +type +lit = + L_aux of lit_aux * l -type +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 Big_int.num (* constant *) + | ATyp_lit of lit (* literal *) + | ATyp_nset of kid * (Big_int.num) list (* set type *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_minus of atyp * atyp (* subtraction *) @@ -155,7 +163,8 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | 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 + | ATyp_exist of kinded_id list * atyp * atyp + | ATyp_base of id * atyp * atyp and atyp = ATyp_aux of atyp_aux * l @@ -166,31 +175,14 @@ kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of kid (* identifier *) | KOpt_kind of kind * kid (* kind-annotated variable *) - -and -n_constraint_aux = (* constraint over kind $_$ *) - NC_equal of atyp * atyp - | NC_bounded_ge of atyp * atyp - | NC_bounded_le of atyp * atyp - | 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 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 *) + | QI_const of atyp (* A constraint for this type *) type @@ -208,32 +200,12 @@ type typquant = TypQ_aux of typquant_aux * l - -type -lit_aux = (* Literal constant *) - L_unit (* $() : _$ *) - | L_zero (* $_ : _$ *) - | L_one (* $_ : _$ *) - | L_true (* $_ : _$ *) - | L_false (* $_ : _$ *) - | 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 +type typschm_aux = (* type scheme *) TypSchm_ts of typquant * atyp type -lit = - L_aux of lit_aux * l - - -type typschm = TypSchm_aux of typschm_aux * l @@ -296,7 +268,7 @@ exp_aux = (* Expression *) | E_let of letbind * exp (* let expression *) | E_assign of exp * exp (* imperative assignment *) | E_sizeof of atyp - | E_constraint of n_constraint + | E_constraint of atyp | E_exit of exp | E_throw of exp | E_try of exp * pexp list @@ -313,12 +285,6 @@ and fexp_aux = (* Field-expression *) and fexp = FE_aux of fexp_aux * l -and fexps_aux = (* Field-expression list *) - FES_Fexps of (fexp) list * bool - -and fexps = - FES_aux of fexps_aux * l - and opt_default_aux = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) Def_val_empty | Def_val_dec of exp @@ -364,6 +330,7 @@ type rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) + | Rec_measure of pat * exp (* recursive with termination measure *) type @@ -424,7 +391,7 @@ name_scm_opt = type default_typing_spec_aux = (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *) - DT_order of base_kind * atyp + DT_order of kind * atyp type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only constructible parts *) @@ -479,7 +446,7 @@ fundef_aux = (* Function definition *) type type_def_aux = (* Type definition body *) - TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + TD_abbrev of id * typquant * kind * atyp (* 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 *) @@ -492,7 +459,7 @@ val_spec_aux = (* Value type specification *) 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_nabbrev of kind * id * name_scm_opt * atyp (* type abbreviation *) type dec_spec_aux = (* Register declarations *) @@ -505,13 +472,13 @@ dec_spec_aux = (* Register declarations *) type 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_mapping of id * tannot_opt - | SD_scattered_mapcl of id * mapcl - | SD_scattered_end of id (* scattered definition end *) + SD_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_funcl of funcl (* scattered function definition clause *) + | SD_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_unioncl of id * type_union (* scattered union definition member *) + | SD_mapping of id * tannot_opt + | SD_mapcl of id * mapcl + | SD_end of id (* scattered definition end *) type |