diff options
Diffstat (limited to 'src/ast.ml')
| -rw-r--r-- | src/ast.ml | 397 |
1 files changed, 206 insertions, 191 deletions
@@ -1,26 +1,30 @@ (* generated by Ott 0.22 from: l2.ott *) -type text = Ulib.Text.t -type l = + +type text = string (* was Ulib.Text.t *) + +type 'a l = 'a +(* | Unknown | Trans of string * l option | Range of Lexing.position * Lexing.position - -exception Parse_error_locn of l * string +*) +exception Parse_error_locn of string l * string type ml_comment = - | Chars of Ulib.Text.t + | Chars of text | Comment of ml_comment list type lex_skip = | Com of ml_comment - | Ws of Ulib.Text.t + | Ws of text | Nl type lex_skips = lex_skip list option +(* let pp_lex_skips ppf sk = match sk with | None -> () @@ -41,7 +45,7 @@ let combine_lex_skips s1 s2 = | (None,_) -> s2 | (_,None) -> s1 | (Some(s1),Some(s2)) -> Some(s2@s1) - +*) type terminal = lex_skips @@ -49,31 +53,36 @@ type x = terminal * text (* identifier *) type ix = terminal * text (* infix identifier *) type -id_aux = (* Identifier *) +'a base_kind_aux = (* base kind *) + BK_type of terminal (* kind of types *) + | BK_nat of terminal (* kind of natural number size expressions *) + | BK_order of terminal (* kind of vector order specifications *) + | BK_effects of terminal (* kind of effect sets *) + + +type +'a id_aux = (* Identifier *) Id of x | DeIid of terminal * x * terminal (* remove infix status *) type -base_kind_aux = (* base kind *) - BK_type of terminal (* kind of types *) - | BK_nat of terminal (* kind of natural number size expressions *) - | BK_order of terminal (* kind of vector order specifications *) - | BK_effects of terminal (* kind of effect sets *) +'a base_kind = + BK_aux of 'a base_kind_aux * 'a l type -id = - Id_aux of id_aux * l +'a id = + Id_aux of 'a id_aux * 'a l type -base_kind = - BK_aux of base_kind_aux * l +'a kind_aux = (* kinds *) + K_kind of ('a base_kind * terminal) list type -effect_aux = (* effect *) +'a effect_aux = (* effect *) Effect_rreg of terminal (* read register *) | Effect_wreg of terminal (* write register *) | Effect_rmem of terminal (* read memory *) @@ -84,104 +93,110 @@ effect_aux = (* effect *) type -nexp_aux = (* expression of kind $_$, for vector sizes and origins *) - Nexp_id of id (* identifier *) +'a nexp_aux = (* expression of kind $_$, for vector sizes and origins *) + Nexp_id of 'a id (* identifier *) | Nexp_constant of terminal * int (* constant *) - | Nexp_times of nexp * terminal * nexp (* product *) - | Nexp_sum of nexp * terminal * nexp (* sum *) - | Nexp_exp of terminal * terminal * nexp (* exponential *) + | Nexp_times of 'a nexp * terminal * 'a nexp (* product *) + | Nexp_sum of 'a nexp * terminal * 'a nexp (* sum *) + | Nexp_exp of terminal * terminal * 'a nexp (* exponential *) -and nexp = - Nexp_aux of nexp_aux * l +and 'a nexp = + Nexp_aux of 'a nexp_aux * 'a l type -kind_aux = (* kinds *) - K_kind of (base_kind * terminal) list +'a kind = + K_aux of 'a kind_aux * 'a l type -effect = - Effect_aux of effect_aux * l +'a effect = + Effect_aux of 'a effect_aux * 'a l type -nexp_constraint_aux = (* constraint over kind $_$ *) - NC_fixed of nexp * terminal * nexp - | NC_bounded_ge of nexp * terminal * nexp - | NC_bounded_le of nexp * terminal * nexp - | NC_nat_set_bounded of id * terminal * terminal * (terminal * int * terminal) list * terminal +'a nexp_constraint_aux = (* constraint over kind $_$ *) + NC_fixed of 'a nexp * terminal * 'a nexp + | NC_bounded_ge of 'a nexp * terminal * 'a nexp + | NC_bounded_le of 'a nexp * terminal * 'a nexp + | NC_nat_set_bounded of 'a id * terminal * terminal * (terminal * int * terminal) list * terminal type -kind = - K_aux of kind_aux * l +'a kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of 'a id (* identifier *) + | KOpt_kind of 'a kind * 'a id (* kind-annotated variable *) type -effects_aux = (* effect set, of kind $_$ *) - Effects_var of id - | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) +'a order_aux = (* vector order specifications, of kind $_$ *) + Ord_id of 'a id (* identifier *) + | Ord_inc of terminal (* increasing (little-endian) *) + | Ord_dec of terminal (* decreasing (big-endian) *) type -order_aux = (* vector order specifications, of kind $_$ *) - Ord_id of id (* identifier *) - | Ord_inc of terminal (* increasing (little-endian) *) - | Ord_dec of terminal (* decreasing (big-endian) *) +'a effects_aux = (* effect set, of kind $_$ *) + Effects_var of 'a id + | Effects_set of terminal * ('a effect * terminal) list * terminal (* effect set *) type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +'a nexp_constraint = + NC_aux of 'a nexp_constraint_aux * 'a l type -kinded_id = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) +'a kinded_id = + KOpt_aux of 'a kinded_id_aux * 'a l type -effects = - Effects_aux of effects_aux * l +'a order = + Ord_aux of 'a order_aux * 'a l type -order = - Ord_aux of order_aux * l +'a effects = + Effects_aux of 'a effects_aux * 'a l type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal - | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) +'a typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of terminal * ('a kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal + | TypQ_no_constraint of terminal * ('a kinded_id) list * terminal (* sugar, omitting constraints *) | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type -typ = (* Type expressions, of kind $_$ *) +'a typ_aux = (* Type expressions, of kind $_$ *) Typ_wild of terminal (* Unspecified type *) - | Typ_var of id (* Type variable *) - | Typ_fn of typ * terminal * typ * effects (* Function type (first-order only in user code) *) - | Typ_tup of (typ * terminal) list (* Tuple type *) - | Typ_app of id * (typ_arg) list (* type constructor application *) + | Typ_var of 'a id (* Type variable *) + | Typ_fn of 'a typ * terminal * 'a typ * 'a effects (* Function type (first-order only in user code) *) + | Typ_tup of ('a typ * terminal) list (* Tuple type *) + | Typ_app of 'a id * (typ_arg) list (* type constructor application *) + +and 'a typ = + Typ_aux of 'a typ_aux * 'a l + +and typ_arg_aux = (* Type constructor arguments of all kinds *) + Typ_arg_nexp of 'a nexp + | Typ_arg_typ of 'a typ + | Typ_arg_order of 'a order + | Typ_arg_effects of 'a effects -and typ_arg = (* Type constructor arguments of all kinds *) - Typ_arg_nexp of nexp - | Typ_arg_typ of typ - | Typ_arg_order of order - | Typ_arg_effects of effects +and typ_arg = + Typ_arg_aux of typ_arg_aux * 'a l type -typquant = - TypQ_aux of typquant_aux * l +'a typquant = + TypQ_aux of 'a typquant_aux * 'a l type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * typ +'a typschm_aux = (* type scheme *) + TypSchm_ts of 'a typquant * 'a typ type @@ -198,131 +213,131 @@ lit = (* Literal constant *) type -typschm = - TypSchm_aux of typschm_aux * l +'a typschm = + TypSchm_aux of 'a typschm_aux * 'a l type -pat_aux = (* Pattern *) +'a pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild of terminal (* wildcard *) - | P_as of terminal * pat * terminal * id * terminal (* named pattern *) - | P_typ of terminal * typ * pat * terminal (* typed pattern *) - | P_id of id (* identifier *) - | P_app of id * (pat) list (* union constructor pattern *) - | P_record of terminal * (fpat * terminal) list * terminal * bool * terminal (* struct pattern *) - | P_vector of terminal * (pat * terminal) list * terminal (* vector pattern *) - | P_vector_indexed of terminal * ((terminal * int * terminal * pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) - | P_vector_concat of (pat * terminal) list (* concatenated vector pattern *) - | P_tup of terminal * (pat * terminal) list * terminal (* tuple pattern *) - | P_list of terminal * (pat * terminal) list * terminal (* list pattern *) + | P_as of terminal * 'a pat * terminal * 'a id * terminal (* named pattern *) + | P_typ of terminal * 'a typ * 'a pat * terminal (* typed pattern *) + | P_id of 'a id (* identifier *) + | P_app of 'a id * ('a pat) list (* union constructor pattern *) + | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *) + | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *) + | P_vector_indexed of terminal * ((terminal * int * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *) + | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *) + | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *) + | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *) -and pat = - P_aux of pat_aux * l +and 'a pat = + P_aux of 'a pat_aux * 'a l -and fpat_aux = (* Field pattern *) - FP_Fpat of id * terminal * pat +and 'a fpat_aux = (* Field pattern *) + FP_Fpat of 'a id * terminal * 'a pat -and fpat = - FP_aux of fpat_aux * l +and 'a fpat = + FP_aux of 'a fpat_aux * 'a l type -exp_aux = (* Expression *) - E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *) - | E_id of id (* identifier *) +'a exp_aux = (* Expression *) + E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) + | E_id of 'a id (* identifier *) | E_lit of lit (* literal constant *) - | E_cast of terminal * typ * terminal * exp (* cast *) - | E_app of exp * (exp) list (* function application *) - | E_app_infix of exp * id * exp (* infix function application *) - | E_tuple of terminal * (exp * terminal) list * terminal (* tuple *) - | E_if of terminal * exp * terminal * exp * terminal * exp (* conditional *) - | E_vector of terminal * (exp * terminal) list * terminal (* vector (indexed from 0) *) - | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal (* vector (indexed consecutively) *) - | E_vector_access of exp * terminal * exp * terminal (* vector access *) - | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *) - | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *) - | E_vector_update_subrange of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *) - | E_list of terminal * (exp * terminal) list * terminal (* list *) - | E_cons of exp * terminal * exp (* cons *) - | E_record of terminal * fexps * terminal (* struct *) - | E_record_update of terminal * exp * terminal * fexps * terminal (* functional update of struct *) - | E_field of exp * terminal * id (* field projection from struct *) - | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* pattern matching *) - | E_let of letbind * terminal * exp (* let expression *) - | E_assign of lexp * terminal * exp (* imperative assignment *) - -and exp = - E_aux of exp_aux * l + | E_cast of terminal * 'a typ * terminal * 'a exp (* cast *) + | E_app of 'a exp * ('a exp) list (* function application *) + | E_app_infix of 'a exp * 'a id * 'a exp (* infix function application *) + | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *) + | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *) + | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *) + | E_vector_indexed of terminal * ((terminal * int * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *) + | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *) + | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *) + | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *) + | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *) + | E_list of terminal * ('a exp * terminal) list * terminal (* list *) + | E_cons of 'a exp * terminal * 'a exp (* cons *) + | E_record of terminal * 'a fexps * terminal (* struct *) + | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *) + | E_field of 'a exp * terminal * 'a id (* field projection from struct *) + | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *) + | E_let of 'a letbind * terminal * 'a exp (* let expression *) + | E_assign of lexp * terminal * 'a exp (* imperative assignment *) + +and 'a exp = + E_aux of 'a exp_aux * 'a l and lexp = (* lvalue expression *) - LEXP_id of id (* identifier *) - | LEXP_vector of lexp * terminal * exp * terminal (* vector element *) - | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal (* subvector *) - | LEXP_field of lexp * terminal * id (* struct field *) + LEXP_id of 'a id (* identifier *) + | LEXP_vector of lexp * terminal * 'a exp * terminal (* vector element *) + | LEXP_vector_range of lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *) + | LEXP_field of lexp * terminal * 'a id (* struct field *) -and fexp_aux = (* Field-expression *) - FE_Fexp of id * terminal * exp +and 'a fexp_aux = (* Field-expression *) + FE_Fexp of 'a id * terminal * 'a exp -and fexp = - FE_aux of fexp_aux * l +and 'a fexp = + FE_aux of 'a fexp_aux * 'a l -and fexps_aux = (* Field-expression list *) - FES_Fexps of (fexp * terminal) list * terminal * bool +and 'a fexps_aux = (* Field-expression list *) + FES_Fexps of ('a fexp * terminal) list * terminal * bool -and fexps = - FES_aux of fexps_aux * l +and 'a fexps = + FES_aux of 'a fexps_aux * 'a l -and pexp_aux = (* Pattern match *) - Pat_exp of pat * terminal * exp +and 'a pexp_aux = (* Pattern match *) + Pat_exp of 'a pat * terminal * 'a exp -and pexp = - Pat_aux of pexp_aux * l +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a l -and letbind_aux = (* Let binding *) - LB_val_explicit of typschm * pat * terminal * exp (* value binding, explicit type (pat must be total) *) - | LB_val_implicit of terminal * pat * terminal * exp (* value binding, implicit type (pat must be total) *) +and 'a letbind_aux = (* Let binding *) + LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *) + | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *) -and letbind = - LB_aux of letbind_aux * l +and 'a letbind = + LB_aux of 'a letbind_aux * 'a l type -rec_opt_aux = (* Optional recursive annotation for functions *) +'a rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec of terminal (* recursive *) type -effects_opt_aux = (* Optional effect annotation for functions *) +'a effects_opt_aux = (* Optional effect annotation for functions *) Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects + | Effects_opt_effects of 'a effects type -funcl_aux = (* Function clause *) - FCL_Funcl of id * pat * terminal * exp +'a funcl_aux = (* Function clause *) + FCL_Funcl of 'a id * 'a pat * terminal * 'a exp type tannot_opt = (* Optional type annotation for functions *) Typ_annot_opt_none - | Typ_annot_opt_some of terminal * typ + | Typ_annot_opt_some of terminal * 'a typ type -rec_opt = - Rec_aux of rec_opt_aux * l +'a rec_opt = + Rec_aux of 'a rec_opt_aux * 'a l type -effects_opt = - Effects_opt_aux of effects_opt_aux * l +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a l type -funcl = - FCL_aux of funcl_aux * l +'a funcl = + FCL_aux of 'a funcl_aux * 'a l type @@ -339,96 +354,96 @@ index_range = (* index specification, for bitfields in register types *) type -fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list +'a fundef_aux = (* Function definition *) + FD_function of terminal * 'a rec_opt * tannot_opt * 'a effects_opt * ('a funcl * terminal) list type -val_spec_aux = (* Value type specification *) - VS_val_spec of terminal * typschm * id +'a val_spec_aux = (* Value type specification *) + VS_val_spec of terminal * 'a typschm * 'a id type -default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of terminal * base_kind * id - | DT_typ of terminal * typschm * id +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * 'a base_kind * 'a id + | DT_typ of terminal * 'a typschm * 'a id type type_def = (* Type definition body *) - TD_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* type abbreviation *) - | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *) - | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* union type definition *) - | TD_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *) - | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *) + TD_abbrev of terminal * 'a id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *) + | TD_record of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* struct type definition *) + | TD_variant of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * (('a typ * 'a id) * terminal) list * terminal * bool * terminal (* union type definition *) + | TD_enum of terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * ('a id * terminal) list * terminal * bool * terminal (* enumeration type definition *) + | TD_register of terminal * 'a id * terminal * terminal * terminal * terminal * 'a nexp * terminal * 'a nexp * terminal * terminal * ((index_range * terminal * 'a id) * terminal) list * terminal (* register mutable bitfield type definition *) type -fundef = - FD_aux of fundef_aux * l +'a fundef = + FD_aux of 'a fundef_aux * 'a l type -val_spec = - VS_aux of val_spec_aux * l +'a val_spec = + VS_aux of 'a val_spec_aux * 'a l type -default_typing_spec = - DT_aux of default_typing_spec_aux * l +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a l type -def_aux = (* Top-level definition *) +'a 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_reg_dec of terminal * typ * id (* register declaration *) - | DEF_scattered_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of terminal * terminal * funcl (* scattered function definition clause *) - | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of terminal * id * terminal * typ * id (* scattered union definition member *) - | DEF_scattered_end of terminal * id (* scattered definition end *) + | 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_default of 'a default_typing_spec (* default kind and type assumptions *) + | DEF_reg_dec of terminal * 'a typ * 'a id (* register declaration *) + | DEF_scattered_function of terminal * terminal * 'a rec_opt * tannot_opt * 'a effects_opt * 'a id (* scattered function definition header *) + | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *) + | DEF_scattered_variant of terminal * terminal * 'a id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *) + | DEF_scattered_unioncl of terminal * 'a id * terminal * 'a typ * 'a id (* scattered union definition member *) + | DEF_scattered_end of terminal * 'a id (* scattered definition end *) type -typ_lib_aux = (* library types and syntactic sugar for them *) +'a typ_lib_aux = (* library types and syntactic sugar for them *) Typ_lib_unit of terminal (* unit type with value $()$ *) | Typ_lib_bool of terminal (* booleans $_$ and $_$ *) | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *) | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *) | Typ_lib_string of terminal * Ulib.UTF8.t (* UTF8 strings *) - | Typ_lib_enum of terminal * nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) - | Typ_lib_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of terminal * nexp * nexp * order * typ (* vector of typ, indexed by natural range *) - | Typ_lib_vector2 of typ * terminal * nexp * terminal (* sugar for vector indexed by [ nexp ] *) - | Typ_lib_vector3 of typ * terminal * nexp * terminal * nexp * terminal (* sugar for vector indexed by [ nexp..nexp ] *) - | Typ_lib_list of terminal * typ (* list of typ *) - | Typ_lib_set of terminal * typ (* finite set of typ *) - | Typ_lib_reg of terminal * typ (* mutable register components holding typ *) + | Typ_lib_enum of terminal * 'a nexp * 'a nexp * 'a order (* natural numbers 'a nexp .. 'a nexp+'a nexp-1, ordered by 'a order *) + | Typ_lib_enum1 of terminal * 'a nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) + | Typ_lib_enum2 of terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) + | Typ_lib_vector of terminal * 'a nexp * 'a nexp * 'a order * 'a typ (* vector of 'a typ, indexed by natural range *) + | Typ_lib_vector2 of 'a typ * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp ] *) + | Typ_lib_vector3 of 'a typ * terminal * 'a nexp * terminal * 'a nexp * terminal (* sugar for vector indexed by [ 'a nexp..'a nexp ] *) + | Typ_lib_list of terminal * 'a typ (* list of 'a typ *) + | Typ_lib_set of terminal * 'a typ (* finite set of 'a typ *) + | Typ_lib_reg of terminal * 'a typ (* mutable register components holding 'a typ *) type -def = - DEF_aux of def_aux * l +'a def = + DEF_aux of 'a def_aux * 'a l type -typ_lib = - Typ_lib_aux of typ_lib_aux * l +'a typ_lib = + Typ_lib_aux of 'a typ_lib_aux * 'a l type ctor_def = (* Datatype constructor definition clause *) - CT_ct of id * terminal * typschm + CT_ct of 'a id * terminal * 'a typschm type defs = (* Definition sequence *) - Defs of (def) list + Defs of ('a def) list |