Module Ast

type l = Parse_ast.l
type loop =
| While
| Until
type !'a annot = l * 'a
type x = string
type ix = string
type base_effect_aux =
| BE_rreg
| BE_wreg
| BE_rmem
| BE_rmemt
| BE_wmem
| BE_eamem
| BE_exmem
| BE_wmv
| BE_wmvt
| BE_barr
| BE_depend
| BE_undef
| BE_unspec
| BE_nondet
| BE_escape
| BE_config
type kid_aux =
| Var of x
type kind_aux =
| K_type
| K_int
| K_order
| K_bool
type id_aux =
| Id of x
| Operator of x
type base_effect =
| BE_aux of base_effect_aux * l
type kid =
| Kid_aux of kid_aux * l
type kind =
| K_aux of kind_aux * l
type id =
| Id_aux of id_aux * l
type effect_aux =
| Effect_set of base_effect list
type order_aux =
| Ord_var of kid
| Ord_inc
| Ord_dec
type kinded_id_aux =
| KOpt_kind of kind * kid
type nexp_aux =
| Nexp_id of id
| Nexp_var of kid
| Nexp_constant of Nat_big_num.num
| Nexp_app of id * nexp list
| Nexp_times of nexp * nexp
| Nexp_sum of nexp * nexp
| Nexp_minus of nexp * nexp
| Nexp_exp of nexp
| Nexp_neg of nexp
and nexp =
| Nexp_aux of nexp_aux * l
type effect =
| Effect_aux of effect_aux * l
type order =
| Ord_aux of order_aux * l
type kinded_id =
| KOpt_aux of kinded_id_aux * l
type lit_aux =
| L_unit
| L_zero
| L_one
| L_true
| L_false
| L_num of Nat_big_num.num
| L_hex of string
| L_bin of string
| L_string of string
| L_undef
| L_real of string
type typ_aux =
| Typ_internal_unknown
| Typ_id of id
| Typ_var of kid
| Typ_fn of typ list * typ * effect
| Typ_bidir of typ * typ * effect
| Typ_tup of typ list
| Typ_app of id * typ_arg list
| Typ_exist of kinded_id list * n_constraint * typ
and typ =
| Typ_aux of typ_aux * l
and typ_arg_aux =
| A_nexp of nexp
| A_typ of typ
| A_order of order
| A_bool of n_constraint
and typ_arg =
| A_aux of typ_arg_aux * l
and n_constraint_aux =
| NC_equal of nexp * nexp
| NC_bounded_ge of nexp * nexp
| NC_bounded_gt of nexp * nexp
| NC_bounded_le of nexp * nexp
| NC_bounded_lt of nexp * nexp
| NC_not_equal of nexp * nexp
| NC_set of kid * Nat_big_num.num list
| NC_or of n_constraint * n_constraint
| NC_and of n_constraint * n_constraint
| NC_app of id * typ_arg list
| NC_var of kid
| NC_true
| NC_false
and n_constraint =
| NC_aux of n_constraint_aux * l
type lit =
| L_aux of lit_aux * l
type typ_pat_aux =
| TP_wild
| TP_var of kid
| TP_app of id * typ_pat list
and typ_pat =
| TP_aux of typ_pat_aux * l
type quant_item_aux =
| QI_id of kinded_id
| QI_constraint of n_constraint
| QI_constant of kinded_id list
type !'a pat_aux =
| P_lit of lit
| P_wild
| P_or of 'a pat * 'a pat
| P_not of 'a pat
| P_as of 'a pat * id
| P_typ of typ * 'a pat
| P_id of id
| P_var of 'a pat * typ_pat
| P_app of id * 'a pat list
| P_vector of 'a pat list
| P_vector_concat of 'a pat list
| P_tup of 'a pat list
| P_list of 'a pat list
| P_cons of 'a pat * 'a pat
| P_string_append of 'a pat list
and !'a pat =
| P_aux of 'a pat_aux * 'a annot
type quant_item =
| QI_aux of quant_item_aux * l
type !'a internal_loop_measure_aux =
| Measure_none
| Measure_some of 'a exp
and !'a internal_loop_measure =
| Measure_aux of 'a internal_loop_measure_aux * l
and !'a exp_aux =
| E_block of 'a exp list
| E_id of id
| E_lit of lit
| E_cast of typ * 'a exp
| E_app of id * 'a exp list
| E_app_infix of 'a exp * id * 'a exp
| E_tuple of 'a exp list
| E_if of 'a exp * 'a exp * 'a exp
| E_loop of loop * 'a internal_loop_measure * 'a exp * 'a exp
| E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp
| E_vector of 'a exp list
| E_vector_access of 'a exp * 'a exp
| E_vector_subrange of 'a exp * 'a exp * 'a exp
| E_vector_update of 'a exp * 'a exp * 'a exp
| E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp
| E_vector_append of 'a exp * 'a exp
| E_list of 'a exp list
| E_cons of 'a exp * 'a exp
| E_record of 'a fexp list
| E_record_update of 'a exp * 'a fexp list
| E_field of 'a exp * id
| E_case of 'a exp * 'a pexp list
| E_let of 'a letbind * 'a exp
| E_assign of 'a lexp * 'a exp
| E_sizeof of nexp
| E_return of 'a exp
| E_exit of 'a exp
| E_ref of id
| E_throw of 'a exp
| E_try of 'a exp * 'a pexp list
| E_assert of 'a exp * 'a exp
| E_var of 'a lexp * 'a exp * 'a exp
| E_internal_plet of 'a pat * 'a exp * 'a exp
| E_internal_return of 'a exp
| E_internal_value of Value.value
| E_constraint of n_constraint
and !'a exp =
| E_aux of 'a exp_aux * 'a annot
and !'a lexp_aux =
| LEXP_id of id
| LEXP_deref of 'a exp
| LEXP_memory of id * 'a exp list
| LEXP_cast of typ * id
| LEXP_tup of 'a lexp list
| LEXP_vector_concat of 'a lexp list
| LEXP_vector of 'a lexp * 'a exp
| LEXP_vector_range of 'a lexp * 'a exp * 'a exp
| LEXP_field of 'a lexp * id
and !'a lexp =
| LEXP_aux of 'a lexp_aux * 'a annot
and !'a fexp_aux =
| FE_Fexp of id * 'a exp
and !'a fexp =
| FE_aux of 'a fexp_aux * 'a annot
and !'a pexp_aux =
| Pat_exp of 'a pat * 'a exp
| Pat_when of 'a pat * 'a exp * 'a exp
and !'a pexp =
| Pat_aux of 'a pexp_aux * 'a annot
and !'a letbind_aux =
| LB_val of 'a pat * 'a exp
and !'a letbind =
| LB_aux of 'a letbind_aux * 'a annot
type !'a mpat_aux =
| MP_lit of lit
| MP_id of id
| MP_app of id * 'a mpat list
| MP_vector of 'a mpat list
| MP_vector_concat of 'a mpat list
| MP_tup of 'a mpat list
| MP_list of 'a mpat list
| MP_cons of 'a mpat * 'a mpat
| MP_string_append of 'a mpat list
| MP_typ of 'a mpat * typ
| MP_as of 'a mpat * id
and !'a mpat =
| MP_aux of 'a mpat_aux * 'a annot
type typquant_aux =
| TypQ_tq of quant_item list
| TypQ_no_forall
type !'a reg_id_aux =
| RI_id of id
type !'a mpexp_aux =
| MPat_pat of 'a mpat
| MPat_when of 'a mpat * 'a exp
type typquant =
| TypQ_aux of typquant_aux * l
type !'a reg_id =
| RI_aux of 'a reg_id_aux * 'a annot
type !'a pexp_funcl = 'a pexp
type !'a mpexp =
| MPat_aux of 'a mpexp_aux * 'a annot
type typschm_aux =
| TypSchm_ts of typquant * typ
type !'a alias_spec_aux =
| AL_subreg of 'a reg_id * id
| AL_bit of 'a reg_id * 'a exp
| AL_slice of 'a reg_id * 'a exp * 'a exp
| AL_concat of 'a reg_id * 'a reg_id
type tannot_opt_aux =
| Typ_annot_opt_none
| Typ_annot_opt_some of typquant * typ
type !'a funcl_aux =
| FCL_Funcl of id * 'a pexp_funcl
type !'a rec_opt_aux =
| Rec_nonrec
| Rec_rec
| Rec_measure of 'a pat * 'a exp
type effect_opt_aux =
| Effect_opt_none
| Effect_opt_effect of effect
type type_union_aux =
| Tu_ty_id of typ * id
type !'a mapcl_aux =
| MCL_bidir of 'a mpexp * 'a mpexp
| MCL_forwards of 'a mpexp * 'a exp
| MCL_backwards of 'a mpexp * 'a exp
type typschm =
| TypSchm_aux of typschm_aux * l
type !'a alias_spec =
| AL_aux of 'a alias_spec_aux * 'a annot
type tannot_opt =
| Typ_annot_opt_aux of tannot_opt_aux * l
type !'a funcl =
| FCL_aux of 'a funcl_aux * 'a annot
type !'a rec_opt =
| Rec_aux of 'a rec_opt_aux * l
type effect_opt =
| Effect_opt_aux of effect_opt_aux * l
type type_union =
| Tu_aux of type_union_aux * l
type !'a mapcl =
| MCL_aux of 'a mapcl_aux * 'a annot
type index_range_aux =
| BF_single of nexp
| BF_range of nexp * nexp
| BF_concat of index_range * index_range
and index_range =
| BF_aux of index_range_aux * l
type val_spec_aux =
| VS_val_spec of typschm * id * (string * string) list * bool
type !'a dec_spec_aux =
| DEC_reg of effect * effect * typ * id
| DEC_config of id * typ * 'a exp
| DEC_alias of id * 'a alias_spec
| DEC_typ_alias of typ * id * 'a alias_spec
type !'a fundef_aux =
| FD_function of 'a rec_opt * tannot_opt * effect_opt * 'a funcl list
type default_spec_aux =
| DT_order of order
type !'a scattered_def_aux =
| SD_function of 'a rec_opt * tannot_opt * effect_opt * id
| SD_funcl of 'a funcl
| SD_variant of id * typquant
| SD_unioncl of id * type_union
| SD_mapping of id * tannot_opt
| SD_mapcl of id * 'a mapcl
| SD_end of id
type type_def_aux =
| TD_abbrev of id * typquant * typ_arg
| TD_record of id * typquant * (typ * id) list * bool
| TD_variant of id * typquant * type_union list * bool
| TD_enum of id * id list * bool
| TD_bitfield of id * typ * (id * index_range) list
type !'a mapdef_aux =
| MD_mapping of id * tannot_opt * 'a mapcl list
type !'a opt_default_aux =
| Def_val_empty
| Def_val_dec of 'a exp
type !'a val_spec =
| VS_aux of val_spec_aux * 'a annot
type !'a dec_spec =
| DEC_aux of 'a dec_spec_aux * 'a annot
type !'a fundef =
| FD_aux of 'a fundef_aux * 'a annot
type default_spec =
| DT_aux of default_spec_aux * l
type prec =
| Infix
| InfixL
| InfixR
type !'a loop_measure =
| Loop of loop * 'a exp
type !'a scattered_def =
| SD_aux of 'a scattered_def_aux * 'a annot
type !'a type_def =
| TD_aux of type_def_aux * 'a annot
type !'a mapdef =
| MD_aux of 'a mapdef_aux * 'a annot
type !'a opt_default =
| Def_val_aux of 'a opt_default_aux * 'a annot
type cast_opt = bool
type !'a def =
| DEF_type of 'a type_def
| DEF_fundef of 'a fundef
| DEF_mapdef of 'a mapdef
| DEF_val of 'a letbind
| DEF_spec of 'a val_spec
| DEF_fixity of prec * Nat_big_num.num * id
| DEF_overload of id * id list
| DEF_default of default_spec
| DEF_scattered of 'a scattered_def
| DEF_measure of id * 'a pat * 'a exp
| DEF_loop_measures of id * 'a loop_measure list
| DEF_reg_dec of 'a dec_spec
| DEF_internal_mutrec of 'a fundef list
| DEF_pragma of string * string * l