package sail

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