diff options
Diffstat (limited to 'src/ast.ml')
| -rw-r--r-- | src/ast.ml | 244 |
1 files changed, 123 insertions, 121 deletions
@@ -42,7 +42,6 @@ (* generated by Ott 0.25 from: l2.ott *) - type text = string type l = Parse_ast.l @@ -53,7 +52,7 @@ type 'a annot = l * 'a type x = text (* identifier *) type ix = text (* infix identifier *) -type +type base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) @@ -61,43 +60,43 @@ base_kind_aux = (* base kind *) | BK_effect (* kind of effect sets *) -type -base_kind = +type +base_kind = BK_aux of base_kind_aux * l -type +type id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) -type +type kid_aux = (* variables with kind, ticked to differntiate from program variables *) Var of x -type +type kind_aux = (* kinds *) K_kind of (base_kind) list -type -id = +type +id = Id_aux of id_aux * l -type -kid = +type +kid = Kid_aux of kid_aux * l -type -kind = +type +kind = K_aux of kind_aux * l -type +type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) Nexp_id of id (* identifier, bound by def Nat x = nexp *) | Nexp_var of kid (* variable *) @@ -108,11 +107,11 @@ nexp_aux = (* expression of kind Nat, for vector sizes and origins *) | Nexp_exp of nexp (* exponential *) | Nexp_neg of nexp (* For internal use *) -and nexp = +and nexp = Nexp_aux of nexp_aux * l -type +type base_effect_aux = (* effect *) BE_rreg (* read register *) | BE_wreg (* write register *) @@ -133,76 +132,76 @@ base_effect_aux = (* effect *) | BE_lret (* Local return happened; not user-writable *) -type -base_effect = +type +base_effect = BE_aux of base_effect_aux * l -type +type order_aux = (* vector order specifications, of kind Order *) Ord_var of kid (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) -type +type effect_aux = (* effect set, of kind Effects *) Effect_var of kid | Effect_set of (base_effect) list (* effect set *) -type -order = +type +order = Ord_aux of order_aux * l -type -effect = +type +effect = Effect_aux of effect_aux * l -type +type kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of kid (* identifier *) | KOpt_kind of kind * kid (* kind-annotated variable *) -type +type n_constraint_aux = (* constraint over kind $_$ *) NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp | NC_bounded_le of nexp * nexp + | NC_not_equal of nexp * nexp | NC_nat_set_bounded of kid * (int) list + | NC_or of n_constraint * n_constraint + | NC_and of n_constraint * n_constraint - -type -kinded_id = - KOpt_aux of kinded_id_aux * l - - -type -n_constraint = +and +n_constraint = NC_aux of n_constraint_aux * l +type +kinded_id = + KOpt_aux of kinded_id_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 *) -type -quant_item = +type +quant_item = QI_aux of quant_item_aux * l -type +type typquant_aux = (* type quantifiers and constraints *) TypQ_tq of (quant_item) list | TypQ_no_forall (* sugar, omitting quantifier and constraints *) -type +type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) | L_zero (* $_ : _$ *) @@ -214,14 +213,13 @@ lit_aux = (* Literal constant *) | L_bin of string (* bit vector constant, C-style *) | L_undef (* constant representing undefined values *) | L_string of string (* string constant *) + | L_real of string - -type -typquant = +type +typquant = TypQ_aux of typquant_aux * l - -type +type typ_aux = (* Type expressions, of kind $_$ *) Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) @@ -230,7 +228,7 @@ typ_aux = (* Type expressions, of kind $_$ *) | Typ_tup of (typ) list (* Tuple type *) | Typ_app of id * (typ_arg) list (* type constructor application *) -and typ = +and typ = Typ_aux of typ_aux * l and typ_arg_aux = (* Type constructor arguments of all kinds *) @@ -239,21 +237,21 @@ and typ_arg_aux = (* Type constructor arguments of all kinds *) | Typ_arg_order of order | Typ_arg_effect of effect -and typ_arg = +and typ_arg = Typ_arg_aux of typ_arg_aux * l -type -lit = +type +lit = L_aux of lit_aux * l -type +type typschm_aux = (* type scheme *) TypSchm_ts of typquant * typ -type +type 'a pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) @@ -267,28 +265,29 @@ type | P_vector_concat of ('a pat) list (* concatenated vector pattern *) | P_tup of ('a pat) list (* tuple pattern *) | P_list of ('a pat) list (* list pattern *) + | P_cons of 'a pat * 'a pat -and 'a pat = +and 'a pat = P_aux of 'a pat_aux * 'a annot and 'a fpat_aux = (* Field pattern *) FP_Fpat of id * 'a pat -and 'a fpat = +and 'a fpat = FP_aux of 'a fpat_aux * 'a annot -type -typschm = +type +typschm = TypSchm_aux of typschm_aux * l -type -'a reg_id_aux = +type +'a reg_id_aux = RI_id of id -type +type 'a exp_aux = (* Expression *) E_block of ('a exp) list (* block *) | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) @@ -316,6 +315,7 @@ type | E_let of 'a letbind * 'a exp (* let expression *) | E_assign of 'a lexp * 'a exp (* imperative assignment *) | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) + | E_constraint of n_constraint (* Expression to evaluate the n_constraint at run time *) | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) @@ -329,7 +329,7 @@ type | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) | E_internal_return of 'a exp (* For internal use to embed into monad definition *) -and 'a exp = +and 'a exp = E_aux of 'a exp_aux * 'a annot and 'a lexp_aux = (* lvalue expression *) @@ -341,82 +341,83 @@ and 'a lexp_aux = (* lvalue expression *) | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) | LEXP_field of 'a lexp * id (* struct field *) -and 'a lexp = +and 'a lexp = LEXP_aux of 'a lexp_aux * 'a annot and 'a fexp_aux = (* Field-expression *) FE_Fexp of id * 'a exp -and 'a fexp = +and 'a fexp = FE_aux of 'a fexp_aux * 'a annot and 'a fexps_aux = (* Field-expression list *) FES_Fexps of ('a fexp) list * bool -and 'a fexps = +and 'a fexps = FES_aux of 'a fexps_aux * 'a annot and 'a 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 'a exp -and 'a opt_default = +and 'a opt_default = Def_val_aux of 'a opt_default_aux * 'a annot and 'a pexp_aux = (* Pattern match *) - Pat_exp of 'a pat * 'a exp + Pat_exp of 'a pat * 'a exp +| Pat_when of 'a pat * 'a exp * 'a exp -and 'a pexp = +and 'a pexp = Pat_aux of 'a pexp_aux * 'a annot and 'a letbind_aux = (* Let binding *) LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *) | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *) -and 'a letbind = +and 'a letbind = LB_aux of 'a letbind_aux * 'a annot -type -'a reg_id = +type +'a reg_id = RI_aux of 'a reg_id_aux * 'a annot -type +type type_union_aux = (* Type union constructors *) Tu_id of id | Tu_ty_id of typ * id -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 effect_opt_aux = (* Optional effect annotation for functions *) Effect_opt_pure (* sugar for empty effect set *) | Effect_opt_effect of effect -type +type 'a funcl_aux = (* Function clause *) FCL_Funcl of id * 'a pat * 'a exp -type +type rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) -type +type tannot_opt_aux = (* Optional type annotation for functions *) Typ_annot_opt_some of typquant * typ + | Typ_annot_opt_none - -type +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 @@ -424,60 +425,60 @@ type | AL_concat of 'a reg_id * 'a reg_id -type -type_union = +type +type_union = Tu_aux of type_union_aux * l -type +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 = +and index_range = BF_aux of index_range_aux * l -type -name_scm_opt = +type +name_scm_opt = Name_sect_aux of name_scm_opt_aux * l -type -effect_opt = +type +effect_opt = Effect_opt_aux of effect_opt_aux * l -type -'a funcl = +type +'a funcl = FCL_aux of 'a funcl_aux * 'a annot -type -rec_opt = +type +rec_opt = Rec_aux of rec_opt_aux * l -type -tannot_opt = +type +tannot_opt = Typ_annot_opt_aux of tannot_opt_aux * l -type -'a alias_spec = +type +'a alias_spec = AL_aux of 'a alias_spec_aux * 'a annot -type -'a default_spec_aux = (* Default kinding or typing assumption *) +type +default_spec_aux = (* Default kinding or typing assumption *) DT_kind of base_kind * kid | DT_order of order | DT_typ of typschm * id -type -'a type_def_aux = (* Type definition body *) +type +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 *) | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) @@ -485,14 +486,15 @@ type | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) -type -'a val_spec_aux = (* Value type specification *) +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 (* 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 *) + | VS_cast_spec of typschm * id -type +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 *) @@ -502,7 +504,7 @@ type | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) -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 *) @@ -512,54 +514,54 @@ type | SD_scattered_end of id (* scattered definition end *) -type +type 'a fundef_aux = (* Function definition *) FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list -type +type 'a dec_spec_aux = (* Register declarations *) DEC_reg of typ * id | DEC_alias of id * 'a alias_spec | DEC_typ_alias of typ * id * 'a alias_spec -type -'a default_spec = - DT_aux of 'a default_spec_aux * l +type +'a default_spec = + DT_aux of default_spec_aux * l -type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot +type +'a type_def = + TD_aux of type_def_aux * 'a annot -type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +type +'a val_spec = + VS_aux of val_spec_aux * 'a annot -type -'a kind_def = +type +'a kind_def = KD_aux of 'a kind_def_aux * 'a annot -type -'a scattered_def = +type +'a scattered_def = SD_aux of 'a scattered_def_aux * 'a annot -type -'a fundef = +type +'a fundef = FD_aux of 'a fundef_aux * 'a annot -type -'a dec_spec = +type +'a dec_spec = DEC_aux of 'a dec_spec_aux * 'a annot -type +type 'a dec_comm = (* Top-level generated comments *) DC_comm of string (* generated unstructured comment *) | DC_comm_struct of 'a def (* generated structured comment *) @@ -570,13 +572,13 @@ and 'a def = (* Top-level 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 *) + | DEF_overload of id * id list (* operator overload specification *) | DEF_default of 'a default_spec (* default kind and type assumptions *) | DEF_scattered of 'a scattered_def (* scattered function and type definition *) | DEF_reg_dec of 'a dec_spec (* register declaration *) | DEF_comm of 'a dec_comm (* generated comments *) - -type +type 'a defs = (* Definition sequence *) Defs of ('a def) list |