libsail 0.16 · OCaml Package

type l = Parse_ast.l

type loop =

| While
| Until

type 'a annot = l * 'a

type extern = {

pure : bool;
bindings : (string * string) list;

}

type def_annot = {

doc_comment : string option;
attrs : (l * string * string) list;
loc : l;

}

type 'a clause_annot = def_annot * 'a

type x = string

type ix = string

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 kid =

| Kid_aux of kid_aux * l

type kind =

| K_aux of kind_aux * l

type id =

| Id_aux of id_aux * l

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 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
| Typ_bidir of typ * typ
| Typ_tuple 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 field_pat_wildcard =

| FP_wild of l
| FP_no_wild

type quant_item_aux =

| QI_id of kinded_id
| QI_constraint of n_constraint

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_vector_subrange of id * Nat_big_num.num * Nat_big_num.num
| P_tuple of 'a pat list
| P_list of 'a pat list
| P_cons of 'a pat * 'a pat
| P_string_append of 'a pat list
| P_struct of (id * 'a pat) list * field_pat_wildcard

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_typ 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_struct of 'a fexp list
| E_struct_update of 'a exp * 'a fexp list
| E_field of 'a exp * id
| E_match 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_internal_assume of n_constraint * 'a exp
| E_constraint of n_constraint

and 'a exp =

| E_aux of 'a exp_aux * 'a annot

and 'a lexp_aux =

| LE_id of id
| LE_deref of 'a exp
| LE_app of id * 'a exp list
| LE_typ of typ * id
| LE_tuple of 'a lexp list
| LE_vector_concat of 'a lexp list
| LE_vector of 'a lexp * 'a exp
| LE_vector_range of 'a lexp * 'a exp * 'a exp
| LE_field of 'a lexp * id

and 'a lexp =

| LE_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_vector_subrange of id * Nat_big_num.num * Nat_big_num.num
| MP_tuple 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
| MP_struct of (id * 'a mpat) list

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 mpexp_aux =

| MPat_pat of 'a mpat
| MPat_when of 'a mpat * 'a exp

type typquant =

| TypQ_aux of typquant_aux * l

type 'a pexp_funcl = 'a pexp

type 'a mpexp =

| MPat_aux of 'a mpexp_aux * 'a annot

type type_union_aux =

| Tu_ty_id of typ * id

type tannot_opt_aux =

| Typ_annot_opt_none
| Typ_annot_opt_some of typquant * typ

type 'a rec_opt_aux =

| Rec_nonrec
| Rec_rec
| Rec_measure of 'a pat * 'a exp

type 'a funcl_aux =

| FCL_funcl of id * 'a pexp_funcl

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_aux =

| TypSchm_ts of typquant * typ

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 type_union =

| Tu_aux of type_union_aux * l

type tannot_opt =

| Typ_annot_opt_aux of tannot_opt_aux * l

type 'a rec_opt =

| Rec_aux of 'a rec_opt_aux * l

type 'a funcl =

| FCL_aux of 'a funcl_aux * 'a clause_annot

type 'a mapcl =

| MCL_aux of 'a mapcl_aux * 'a clause_annot

type typschm =

| TypSchm_aux of typschm_aux * l

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 fundef_aux =

| FD_function of 'a rec_opt * tannot_opt * 'a funcl list

type 'a mapdef_aux =

| MD_mapping of id * tannot_opt * 'a mapcl list

type subst_aux =

| IS_typ of kid * typ
| IS_id of id * id

type outcome_spec_aux =

| OV_outcome of id * typschm * kinded_id list

type 'a instantiation_spec_aux =

| IN_id of id

type val_spec_aux =

| VS_val_spec of typschm * id * extern option

type default_spec_aux =

| DT_order of order

type 'a scattered_def_aux =

| SD_function of 'a rec_opt * tannot_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_enum of id
| SD_enumcl of id * id
| SD_end of id

type 'a dec_spec_aux =

| DEC_reg of typ * id * 'a exp option

type 'a opt_default_aux =

| Def_val_empty
| Def_val_dec of 'a exp

type 'a impldef_aux =

| Impl_impl of 'a funcl

type 'a type_def =

| TD_aux of type_def_aux * 'a annot

type 'a fundef =

| FD_aux of 'a fundef_aux * 'a annot

type 'a mapdef =

| MD_aux of 'a mapdef_aux * 'a annot

type subst =

| IS_aux of subst_aux * l

type outcome_spec =

| OV_aux of outcome_spec_aux * l

type 'a instantiation_spec =

| IN_aux of 'a instantiation_spec_aux * 'a annot

type 'a val_spec =

| VS_aux of val_spec_aux * 'a annot

type default_spec =

| DT_aux of default_spec_aux * l

type 'a scattered_def =

| SD_aux of 'a scattered_def_aux * 'a annot

type 'a dec_spec =

| DEC_aux of 'a dec_spec_aux * 'a annot

type prec =

| Infix
| InfixL
| InfixR

type 'a loop_measure =

| Loop of loop * 'a exp

type 'a opt_default =

| Def_val_aux of 'a opt_default_aux * 'a annot

type 'a impldef =

| Impl_aux of 'a impldef_aux * l

type 'a def_aux =

| DEF_type of 'a type_def
| DEF_fundef of 'a fundef
| DEF_mapdef of 'a mapdef
| DEF_impl of 'a funcl
| DEF_let of 'a letbind
| DEF_val of 'a val_spec
| DEF_outcome of outcome_spec * 'a def list
| DEF_instantiation of 'a instantiation_spec * subst list
| 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_register of 'a dec_spec
| DEF_internal_mutrec of 'a fundef list
| DEF_pragma of string * string * l

and 'a def =

| DEF_aux of 'a def_aux * def_annot

package libsail