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
module Big_int = Nat_big_numtype !'a annot = l * 'aexception Parse_error_locn of l * stringtype x = texttype ix = texttype lit_aux = | L_unit| L_zero| L_one| L_true| L_false| L_num of Big_int.num| L_hex of string| L_bin of string| L_undef| L_string of string| L_real of string
type atyp_aux = | ATyp_id of id| ATyp_var of kid| ATyp_lit of lit| ATyp_nset of kid * Big_int.num list| ATyp_times of atyp * atyp| ATyp_sum of atyp * atyp| ATyp_minus of atyp * atyp| ATyp_exp of atyp| ATyp_neg of atyp| ATyp_inc| ATyp_dec| ATyp_default_ord| ATyp_set of base_effect list| ATyp_fn of atyp * atyp * atyp| ATyp_bidir of atyp * atyp * atyp| ATyp_wild| ATyp_tup of atyp list| ATyp_app of id * atyp list| ATyp_exist of kinded_id list * atyp * atyp| ATyp_base of id * atyp * atyp
and exp_aux = | E_block of exp list| E_id of id| E_ref of id| E_deref of exp| E_lit of lit| E_cast of atyp * exp| E_app of id * exp list| E_app_infix of exp * id * exp| E_tuple of exp list| E_if of exp * exp * exp| E_loop of loop * measure * exp * exp| E_for of id * exp * exp * exp * atyp * exp| E_vector of exp list| E_vector_access of exp * exp| E_vector_subrange of exp * exp * exp| E_vector_update of exp * exp * exp| E_vector_update_subrange of exp * exp * exp * exp| E_vector_append of exp * exp| E_list of exp list| E_cons of exp * exp| E_record of exp list| E_record_update of exp * exp list| E_field of exp * id| E_case of exp * pexp list| E_let of letbind * exp| E_assign of exp * exp| E_sizeof of atyp| E_constraint of atyp| E_exit of exp| E_throw of exp| E_try of exp * pexp list| E_return of exp| E_assert of exp * exp| E_var of exp * exp * exp| E_internal_plet of pat * exp * exp| E_internal_return of exp
type index_range_aux = | BF_single of atyp| BF_range of atyp * atyp| BF_concat of index_range * index_range
type scattered_def_aux = | SD_function of rec_opt * tannot_opt * effect_opt * id| SD_funcl of funcl| SD_variant of id * typquant| SD_unioncl of id * type_union| SD_mapping of id * tannot_opt| SD_mapcl of id * mapcl| SD_end of id
type fixity_token = prec * Big_int.num * stringtype def = | DEF_type of type_def| DEF_fundef of fundef| DEF_mapdef of mapdef| DEF_val of letbind| DEF_overload of id * id list| DEF_fixity of prec * Big_int.num * id| DEF_spec of val_spec| DEF_default of default_typing_spec| DEF_scattered of scattered_def| DEF_measure of id * pat * exp| DEF_loop_measures of id * loop_measure list| DEF_reg_dec of dec_spec| DEF_pragma of string * string * l| DEF_internal_mutrec of fundef list