sail
  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Big_int = Nat_big_num
type text = string
type l =
  1. | Unknown
  2. | Unique of int * l
  3. | Generated of l
  4. | Range of Lexing.position * Lexing.position
  5. | Documented of string * l
type !'a annot = l * 'a
exception Parse_error_locn of l * string
type x = text
type ix = text
type kind_aux =
  1. | K_type
  2. | K_int
  3. | K_order
  4. | K_bool
type kind =
  1. | K_aux of kind_aux * l
type base_effect_aux =
  1. | BE_rreg
  2. | BE_wreg
  3. | BE_rmem
  4. | BE_rmemt
  5. | BE_wmem
  6. | BE_wmv
  7. | BE_wmvt
  8. | BE_eamem
  9. | BE_exmem
  10. | BE_barr
  11. | BE_depend
  12. | BE_undef
  13. | BE_unspec
  14. | BE_nondet
  15. | BE_escape
  16. | BE_config
type kid_aux =
  1. | Var of x
type id_aux =
  1. | Id of x
  2. | Operator of x
type base_effect =
  1. | BE_aux of base_effect_aux * l
type kid =
  1. | Kid_aux of kid_aux * l
type id =
  1. | Id_aux of 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 Big_int.num
  7. | L_hex of string
  8. | L_bin of string
  9. | L_undef
  10. | L_string of string
  11. | L_real of string
type lit =
  1. | L_aux of lit_aux * l
type atyp_aux =
  1. | ATyp_id of id
  2. | ATyp_var of kid
  3. | ATyp_lit of lit
  4. | ATyp_nset of kid * Big_int.num list
  5. | ATyp_times of atyp * atyp
  6. | ATyp_sum of atyp * atyp
  7. | ATyp_minus of atyp * atyp
  8. | ATyp_exp of atyp
  9. | ATyp_neg of atyp
  10. | ATyp_inc
  11. | ATyp_dec
  12. | ATyp_default_ord
  13. | ATyp_set of base_effect list
  14. | ATyp_fn of atyp * atyp * atyp
  15. | ATyp_bidir of atyp * atyp * atyp
  16. | ATyp_wild
  17. | ATyp_tup of atyp list
  18. | ATyp_app of id * atyp list
  19. | ATyp_exist of kinded_id list * atyp * atyp
  20. | ATyp_base of id * atyp * atyp
and atyp =
  1. | ATyp_aux of atyp_aux * l
and kinded_id_aux =
  1. | KOpt_kind of string option * kid list * kind option
and kinded_id =
  1. | KOpt_aux of kinded_id_aux * l
type quant_item_aux =
  1. | QI_id of kinded_id
  2. | QI_constraint of atyp
type quant_item =
  1. | QI_aux of quant_item_aux * l
type typquant_aux =
  1. | TypQ_tq of quant_item list
  2. | TypQ_no_forall
type typquant =
  1. | TypQ_aux of typquant_aux * l
type typschm_aux =
  1. | TypSchm_ts of typquant * atyp
type typschm =
  1. | TypSchm_aux of typschm_aux * l
type pat_aux =
  1. | P_lit of lit
  2. | P_wild
  3. | P_or of pat * pat
  4. | P_typ of atyp * pat
  5. | P_id of id
  6. | P_var of pat * atyp
  7. | P_app of id * pat list
  8. | P_vector of pat list
  9. | P_vector_concat of pat list
  10. | P_tup of pat list
  11. | P_list of pat list
  12. | P_cons of pat * pat
  13. | P_string_append of pat list
and pat =
  1. | P_aux of pat_aux * l
and fpat_aux =
  1. | FP_Fpat of id * pat
and fpat =
  1. | FP_aux of fpat_aux * l
type loop =
  1. | While
  2. | Until
type measure_aux =
  1. | Measure_none
  2. | Measure_some of exp
and measure =
  1. | Measure_aux of measure_aux * l
and exp_aux =
  1. | E_block of exp list
  2. | E_id of id
  3. | E_ref of id
  4. | E_deref of exp
  5. | E_lit of lit
  6. | E_cast of atyp * exp
  7. | E_app of id * exp list
  8. | E_app_infix of exp * id * exp
  9. | E_tuple of exp list
  10. | E_if of exp * exp * exp
  11. | E_loop of loop * measure * exp * exp
  12. | E_for of id * exp * exp * exp * atyp * exp
  13. | E_vector of exp list
  14. | E_vector_access of exp * exp
  15. | E_vector_subrange of exp * exp * exp
  16. | E_vector_update of exp * exp * exp
  17. | E_vector_update_subrange of exp * exp * exp * exp
  18. | E_vector_append of exp * exp
  19. | E_list of exp list
  20. | E_cons of exp * exp
  21. | E_record of exp list
  22. | E_record_update of exp * exp list
  23. | E_field of exp * id
  24. | E_case of exp * pexp list
  25. | E_let of letbind * exp
  26. | E_assign of exp * exp
  27. | E_sizeof of atyp
  28. | E_constraint of atyp
  29. | E_exit of exp
  30. | E_throw of exp
  31. | E_try of exp * pexp list
  32. | E_return of exp
  33. | E_assert of exp * exp
  34. | E_var of exp * exp * exp
  35. | E_internal_plet of pat * exp * exp
  36. | E_internal_return of exp
and exp =
  1. | E_aux of exp_aux * l
and fexp_aux =
  1. | FE_Fexp of id * exp
and fexp =
  1. | FE_aux of fexp_aux * l
and opt_default_aux =
  1. | Def_val_empty
  2. | Def_val_dec of exp
and opt_default =
  1. | Def_val_aux of opt_default_aux * l
and pexp_aux =
  1. | Pat_exp of pat * exp
  2. | Pat_when of pat * exp * exp
and pexp =
  1. | Pat_aux of pexp_aux * l
and letbind_aux =
  1. | LB_val of pat * exp
and letbind =
  1. | LB_aux of letbind_aux * l
type tannot_opt_aux =
  1. | Typ_annot_opt_none
  2. | Typ_annot_opt_some of typquant * atyp
type typschm_opt_aux =
  1. | TypSchm_opt_none
  2. | TypSchm_opt_some of typschm
type typschm_opt =
  1. | TypSchm_opt_aux of typschm_opt_aux * l
type effect_opt_aux =
  1. | Effect_opt_none
  2. | Effect_opt_effect of atyp
type rec_opt_aux =
  1. | Rec_nonrec
  2. | Rec_rec
  3. | Rec_measure of pat * exp
type funcl_aux =
  1. | FCL_Funcl of id * pexp
type type_union_aux =
  1. | Tu_ty_id of atyp * id
  2. | Tu_ty_anon_rec of (atyp * id) list * id
type tannot_opt =
  1. | Typ_annot_opt_aux of tannot_opt_aux * l
type effect_opt =
  1. | Effect_opt_aux of effect_opt_aux * l
type rec_opt =
  1. | Rec_aux of rec_opt_aux * l
type funcl =
  1. | FCL_aux of funcl_aux * l
type type_union =
  1. | Tu_aux of type_union_aux * l
type index_range_aux =
  1. | BF_single of atyp
  2. | BF_range of atyp * atyp
  3. | BF_concat of index_range * index_range
and index_range =
  1. | BF_aux of index_range_aux * l
type default_typing_spec_aux =
  1. | DT_order of kind * atyp
type mpat_aux =
  1. | MP_lit of lit
  2. | MP_id of id
  3. | MP_app of id * mpat list
  4. | MP_vector of mpat list
  5. | MP_vector_concat of mpat list
  6. | MP_tup of mpat list
  7. | MP_list of mpat list
  8. | MP_cons of mpat * mpat
  9. | MP_string_append of mpat list
  10. | MP_typ of mpat * atyp
  11. | MP_as of mpat * id
and mpat =
  1. | MP_aux of mpat_aux * l
type mpexp_aux =
  1. | MPat_pat of mpat
  2. | MPat_when of mpat * exp
type mpexp =
  1. | MPat_aux of mpexp_aux * l
type mapcl_aux =
  1. | MCL_bidir of mpexp * mpexp
  2. | MCL_forwards of mpexp * exp
  3. | MCL_backwards of mpexp * exp
type mapcl =
  1. | MCL_aux of mapcl_aux * l
type mapdef_aux =
  1. | MD_mapping of id * typschm_opt * mapcl list
type mapdef =
  1. | MD_aux of mapdef_aux * l
type fundef_aux =
  1. | FD_function of rec_opt * tannot_opt * effect_opt * funcl list
type type_def_aux =
  1. | TD_abbrev of id * typquant * kind * atyp
  2. | TD_record of id * typquant * (atyp * id) list * bool
  3. | TD_variant of id * typquant * type_union list * bool
  4. | TD_enum of id * (id * atyp) list * (id * exp option) list * bool
  5. | TD_bitfield of id * atyp * (id * index_range) list
type val_spec_aux =
  1. | VS_val_spec of typschm * id * (string * string) list * bool
type dec_spec_aux =
  1. | DEC_reg of atyp * atyp * atyp * id
  2. | DEC_config of id * atyp * exp
  3. | DEC_alias of id * exp
  4. | DEC_typ_alias of atyp * id * exp
type scattered_def_aux =
  1. | SD_function of rec_opt * tannot_opt * effect_opt * id
  2. | SD_funcl of 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 * mapcl
  7. | SD_end of id
type default_typing_spec =
  1. | DT_aux of default_typing_spec_aux * l
type fundef =
  1. | FD_aux of fundef_aux * l
type type_def =
  1. | TD_aux of type_def_aux * l
type val_spec =
  1. | VS_aux of val_spec_aux * l
type dec_spec =
  1. | DEC_aux of dec_spec_aux * l
type loop_measure =
  1. | Loop of loop * exp
type scattered_def =
  1. | SD_aux of scattered_def_aux * l
type prec =
  1. | Infix
  2. | InfixL
  3. | InfixR
type fixity_token = prec * Big_int.num * string
type def =
  1. | DEF_type of type_def
  2. | DEF_fundef of fundef
  3. | DEF_mapdef of mapdef
  4. | DEF_val of letbind
  5. | DEF_overload of id * id list
  6. | DEF_fixity of prec * Big_int.num * id
  7. | DEF_spec of val_spec
  8. | DEF_default of default_typing_spec
  9. | DEF_scattered of scattered_def
  10. | DEF_measure of id * pat * exp
  11. | DEF_loop_measures of id * loop_measure list
  12. | DEF_reg_dec of dec_spec
  13. | DEF_pragma of string * string * l
  14. | DEF_internal_mutrec of fundef list
type lexp_aux =
  1. | LEXP_id of id
  2. | LEXP_mem of id * exp list
  3. | LEXP_vector of lexp * exp
  4. | LEXP_vector_range of lexp * exp * exp
  5. | LEXP_vector_concat of lexp list
  6. | LEXP_field of lexp * id
and lexp =
  1. | LEXP_aux of lexp_aux * l
type defs =
  1. | Defs of (string * def list) list