package libsail

  1. Overview
  2. Docs

Module Libsail.AstSource

Sourcetype loop =
  1. | While
  2. | Until
Sourcetype 'a annot = l * 'a
Sourcetype extern = {
  1. pure : bool;
  2. bindings : (string * string) list;
}
Sourcetype visibility =
  1. | Public
  2. | Private of l
Sourcetype 'a def_annot = {
  1. doc_comment : string option;
  2. attrs : (l * string * attribute_data option) list;
  3. visibility : visibility;
  4. loc : l;
  5. env : 'a;
}
Sourcetype 'a clause_annot = unit def_annot * 'a
Sourcetype x = string
Sourcetype ix = string
Sourcetype kid_aux =
  1. | Var of x
Sourcetype kind_aux =
  1. | K_type
  2. | K_int
  3. | K_bool
Sourcetype kid =
  1. | Kid_aux of kid_aux * l
Sourcetype kind =
  1. | K_aux of kind_aux * l
Sourcetype id_aux =
  1. | Id of x
  2. | Operator of x
Sourcetype kinded_id_aux =
  1. | KOpt_kind of kind * kid
Sourcetype id =
  1. | Id_aux of id_aux * l
Sourcetype 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
Sourcetype kinded_id =
  1. | KOpt_aux of kinded_id_aux * l
Sourcetype field_pat_wildcard =
  1. | FP_wild of l
  2. | FP_no_wild
Sourcetype typ_pat_aux =
  1. | TP_wild
  2. | TP_var of kid
  3. | TP_app of id * typ_pat list
Sourceand typ_pat =
  1. | TP_aux of typ_pat_aux * l
Sourcetype lit =
  1. | L_aux of lit_aux * l
Sourcetype 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_if of n_constraint * nexp * nexp
  6. | Nexp_times of nexp * nexp
  7. | Nexp_sum of nexp * nexp
  8. | Nexp_minus of nexp * nexp
  9. | Nexp_exp of nexp
  10. | Nexp_neg of nexp
Sourceand nexp =
  1. | Nexp_aux of nexp_aux * l
Sourceand typ_aux =
  1. | Typ_internal_unknown
  2. | Typ_id of id
  3. | Typ_var of kid
  4. | Typ_fn of typ list * typ
  5. | Typ_bidir of typ * typ
  6. | Typ_tuple of typ list
  7. | Typ_app of id * typ_arg list
  8. | Typ_exist of kinded_id list * n_constraint * typ
Sourceand typ =
  1. | Typ_aux of typ_aux * l
Sourceand typ_arg_aux =
  1. | A_nexp of nexp
  2. | A_typ of typ
  3. | A_bool of n_constraint
Sourceand typ_arg =
  1. | A_aux of typ_arg_aux * l
Sourceand n_constraint_aux =
  1. | NC_equal of typ_arg * typ_arg
  2. | NC_not_equal of typ_arg * typ_arg
  3. | NC_ge of nexp * nexp
  4. | NC_gt of nexp * nexp
  5. | NC_le of nexp * nexp
  6. | NC_lt of nexp * nexp
  7. | NC_set of nexp * 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_id of id
  12. | NC_var of kid
  13. | NC_true
  14. | NC_false
Sourceand n_constraint =
  1. | NC_aux of n_constraint_aux * l
Sourcetype order_aux =
  1. | Ord_inc
  2. | Ord_dec
Sourcetype '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_vector_subrange of id * Nat_big_num.num * Nat_big_num.num
  13. | P_tuple of 'a pat list
  14. | P_list of 'a pat list
  15. | P_cons of 'a pat * 'a pat
  16. | P_string_append of 'a pat list
  17. | P_struct of (id * 'a pat) list * field_pat_wildcard
Sourceand 'a pat =
  1. | P_aux of 'a pat_aux * 'a annot
Sourcetype order =
  1. | Ord_aux of order_aux * l
Sourcetype quant_item_aux =
  1. | QI_id of kinded_id
  2. | QI_constraint of n_constraint
Sourcetype 'a internal_loop_measure_aux =
  1. | Measure_none
  2. | Measure_some of 'a exp
Sourceand 'a internal_loop_measure =
  1. | Measure_aux of 'a internal_loop_measure_aux * l
Sourceand 'a exp_aux =
  1. | E_block of 'a exp list
  2. | E_id of id
  3. | E_lit of lit
  4. | E_typ 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_struct of 'a fexp list
  20. | E_struct_update of 'a exp * 'a fexp list
  21. | E_field of 'a exp * id
  22. | E_match 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_internal_assume of n_constraint * 'a exp
  37. | E_constraint of n_constraint
Sourceand 'a exp =
  1. | E_aux of 'a exp_aux * 'a annot
Sourceand 'a lexp_aux =
  1. | LE_id of id
  2. | LE_deref of 'a exp
  3. | LE_app of id * 'a exp list
  4. | LE_typ of typ * id
  5. | LE_tuple of 'a lexp list
  6. | LE_vector_concat of 'a lexp list
  7. | LE_vector of 'a lexp * 'a exp
  8. | LE_vector_range of 'a lexp * 'a exp * 'a exp
  9. | LE_field of 'a lexp * id
Sourceand 'a lexp =
  1. | LE_aux of 'a lexp_aux * 'a annot
Sourceand 'a fexp_aux =
  1. | FE_fexp of id * 'a exp
Sourceand 'a fexp =
  1. | FE_aux of 'a fexp_aux * 'a annot
Sourceand 'a pexp_aux =
  1. | Pat_exp of 'a pat * 'a exp
  2. | Pat_when of 'a pat * 'a exp * 'a exp
Sourceand 'a pexp =
  1. | Pat_aux of 'a pexp_aux * 'a annot
Sourceand 'a letbind_aux =
  1. | LB_val of 'a pat * 'a exp
Sourceand 'a letbind =
  1. | LB_aux of 'a letbind_aux * 'a annot
Sourcetype '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_vector_subrange of id * Nat_big_num.num * Nat_big_num.num
  7. | MP_tuple of 'a mpat list
  8. | MP_list of 'a mpat list
  9. | MP_cons of 'a mpat * 'a mpat
  10. | MP_string_append of 'a mpat list
  11. | MP_typ of 'a mpat * typ
  12. | MP_as of 'a mpat * id
  13. | MP_struct of (id * 'a mpat) list
Sourceand 'a mpat =
  1. | MP_aux of 'a mpat_aux * 'a annot
Sourcetype quant_item =
  1. | QI_aux of quant_item_aux * l
Sourcetype 'a mpexp_aux =
  1. | MPat_pat of 'a mpat
  2. | MPat_when of 'a mpat * 'a exp
Sourcetype typquant_aux =
  1. | TypQ_tq of quant_item list
  2. | TypQ_no_forall
Sourcetype 'a mpexp =
  1. | MPat_aux of 'a mpexp_aux * 'a annot
Sourcetype 'a pexp_funcl = 'a pexp
Sourcetype typquant =
  1. | TypQ_aux of typquant_aux * l
Sourcetype 'a mapcl_aux =
  1. | MCL_bidir of 'a mpexp * 'a mpexp
  2. | MCL_forwards of 'a pexp
  3. | MCL_backwards of 'a pexp
Sourcetype 'a funcl_aux =
  1. | FCL_funcl of id * 'a pexp_funcl
Sourcetype 'a rec_opt_aux =
  1. | Rec_nonrec
  2. | Rec_rec
  3. | Rec_measure of 'a pat * 'a exp
Sourcetype tannot_opt_aux =
  1. | Typ_annot_opt_none
  2. | Typ_annot_opt_some of typquant * typ
Sourcetype type_union_aux =
  1. | Tu_ty_id of typ * id
Sourcetype typschm_aux =
  1. | TypSchm_ts of typquant * typ
Sourcetype 'a mapcl =
  1. | MCL_aux of 'a mapcl_aux * 'a clause_annot
Sourcetype 'a funcl =
  1. | FCL_aux of 'a funcl_aux * 'a clause_annot
Sourcetype 'a rec_opt =
  1. | Rec_aux of 'a rec_opt_aux * l
Sourcetype tannot_opt =
  1. | Typ_annot_opt_aux of tannot_opt_aux * l
Sourcetype type_union =
  1. | Tu_aux of type_union_aux * unit def_annot
Sourcetype typschm =
  1. | TypSchm_aux of typschm_aux * l
Sourcetype index_range_aux =
  1. | BF_single of nexp
  2. | BF_range of nexp * nexp
  3. | BF_concat of index_range * index_range
Sourceand index_range =
  1. | BF_aux of index_range_aux * l
Sourcetype 'a dec_spec_aux =
  1. | DEC_reg of typ * id * 'a exp option
Sourcetype 'a scattered_def_aux =
  1. | SD_function of 'a rec_opt * tannot_opt * id
  2. | SD_funcl of 'a funcl
  3. | SD_variant of id * typquant
  4. | SD_unioncl of id * type_union
  5. | SD_internal_unioncl_record of id * id * typquant * (typ * id) list
  6. | SD_mapping of id * tannot_opt
  7. | SD_mapcl of id * 'a mapcl
  8. | SD_enum of id
  9. | SD_enumcl of id * id
  10. | SD_end of id
Sourcetype default_spec_aux =
  1. | DT_order of order
Sourcetype val_spec_aux =
  1. | VS_val_spec of typschm * id * extern option
Sourcetype 'a instantiation_spec_aux =
  1. | IN_id of id
Sourcetype outcome_spec_aux =
  1. | OV_outcome of id * typschm * kinded_id list
Sourcetype subst_aux =
  1. | IS_typ of kid * typ
  2. | IS_id of id * id
Sourcetype 'a mapdef_aux =
  1. | MD_mapping of id * tannot_opt * 'a mapcl list
Sourcetype 'a fundef_aux =
  1. | FD_function of 'a rec_opt * tannot_opt * 'a funcl list
Sourcetype 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_abstract of id * kind
  6. | TD_bitfield of id * typ * (id * index_range) list
Sourcetype 'a loop_measure =
  1. | Loop of loop * 'a exp
Sourcetype prec =
  1. | Infix
  2. | InfixL
  3. | InfixR
Sourcetype 'a dec_spec =
  1. | DEC_aux of 'a dec_spec_aux * 'a annot
Sourcetype 'a scattered_def =
  1. | SD_aux of 'a scattered_def_aux * 'a annot
Sourcetype default_spec =
  1. | DT_aux of default_spec_aux * l
Sourcetype 'a val_spec =
  1. | VS_aux of val_spec_aux * 'a annot
Sourcetype 'a instantiation_spec =
  1. | IN_aux of 'a instantiation_spec_aux * 'a annot
Sourcetype outcome_spec =
  1. | OV_aux of outcome_spec_aux * l
Sourcetype subst =
  1. | IS_aux of subst_aux * l
Sourcetype 'a mapdef =
  1. | MD_aux of 'a mapdef_aux * 'a annot
Sourcetype 'a fundef =
  1. | FD_aux of 'a fundef_aux * 'a annot
Sourcetype 'a type_def =
  1. | TD_aux of type_def_aux * 'a annot
Sourcetype 'a impldef_aux =
  1. | Impl_impl of 'a funcl
Sourcetype 'a opt_default_aux =
  1. | Def_val_empty
  2. | Def_val_dec of 'a exp
Sourcetype ('a, 'b) def_aux =
  1. | DEF_type of 'a type_def
  2. | DEF_constraint of n_constraint
  3. | DEF_fundef of 'a fundef
  4. | DEF_mapdef of 'a mapdef
  5. | DEF_impl of 'a funcl
  6. | DEF_let of 'a letbind
  7. | DEF_val of 'a val_spec
  8. | DEF_outcome of outcome_spec * ('a, 'b) def list
  9. | DEF_instantiation of 'a instantiation_spec * subst list
  10. | DEF_fixity of prec * Nat_big_num.num * id
  11. | DEF_overload of id * id list
  12. | DEF_default of default_spec
  13. | DEF_scattered of 'a scattered_def
  14. | DEF_measure of id * 'a pat * 'a exp
  15. | DEF_loop_measures of id * 'a loop_measure list
  16. | DEF_register of 'a dec_spec
  17. | DEF_internal_mutrec of 'a fundef list
  18. | DEF_pragma of string * string * l
Sourceand ('a, 'b) def =
  1. | DEF_aux of ('a, 'b) def_aux * 'b def_annot
Sourcetype 'a impldef =
  1. | Impl_aux of 'a impldef_aux * l
Sourcetype 'a opt_default =
  1. | Def_val_aux of 'a opt_default_aux * 'a annot