package sail
-
sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type l = Parse_ast.ltype !'a annot = l * 'atype 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
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
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 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
type !'a pexp_funcl = 'a pexptype index_range_aux = | BF_single of nexp| BF_range of nexp * nexp| BF_concat of index_range * index_range
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 !'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