package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libsail.Parse_astSource

module Big_int = Nat_big_num
Sourcetype text = string
Sourcetype l =
  1. | Unknown
  2. | Unique of int * l
  3. | Generated of l
  4. | Hint of string * l * l
  5. | Range of Lexing.position * Lexing.position
Sourcetype 'a annot = l * 'a
Sourcetype extern = {
  1. pure : bool;
  2. bindings : (string * string) list;
}
Sourceexception Parse_error_locn of l * string
Sourcetype x = text
Sourcetype ix = text
Sourcetype kind_aux =
  1. | K_type
  2. | K_int
  3. | K_order
  4. | K_bool
Sourcetype kind =
  1. | K_aux of kind_aux * l
Sourcetype base_effect_aux =
  1. | BE_rreg
  2. | BE_wreg
  3. | BE_rmem
  4. | BE_wmem
  5. | BE_wmv
  6. | BE_eamem
  7. | BE_exmem
  8. | BE_barr
  9. | BE_depend
  10. | BE_undef
  11. | BE_unspec
  12. | BE_nondet
  13. | BE_escape
  14. | BE_config
Sourcetype kid_aux =
  1. | Var of x
Sourcetype id_aux =
  1. | Id of x
  2. | Operator of x
Sourcetype base_effect =
  1. | BE_aux of base_effect_aux * l
Sourcetype kid =
  1. | Kid_aux of kid_aux * l
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 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
Sourcetype lit =
  1. | L_aux of lit_aux * l
Sourcetype 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_set of base_effect list
  13. | ATyp_fn of atyp * atyp * atyp
  14. | ATyp_bidir of atyp * atyp * atyp
  15. | ATyp_wild
  16. | ATyp_tuple of atyp list
  17. | ATyp_app of id * atyp list
  18. | ATyp_exist of kinded_id list * atyp * atyp
  19. | ATyp_parens of atyp
Sourceand atyp =
  1. | ATyp_aux of atyp_aux * l
Sourceand kinded_id_aux =
  1. | KOpt_kind of string option * kid list * kind option
Sourceand kinded_id =
  1. | KOpt_aux of kinded_id_aux * l
Sourcetype quant_item_aux =
  1. | QI_id of kinded_id
  2. | QI_constraint of atyp
Sourcetype quant_item =
  1. | QI_aux of quant_item_aux * l
Sourcetype typquant_aux =
  1. | TypQ_tq of quant_item list
  2. | TypQ_no_forall
Sourcetype typquant =
  1. | TypQ_aux of typquant_aux * l
Sourcetype typschm_aux =
  1. | TypSchm_ts of typquant * atyp
Sourcetype typschm =
  1. | TypSchm_aux of typschm_aux * l
Sourcetype pat_aux =
  1. | P_lit of lit
  2. | P_wild
  3. | P_typ of atyp * pat
  4. | P_id of id
  5. | P_var of pat * atyp
  6. | P_app of id * pat list
  7. | P_vector of pat list
  8. | P_vector_concat of pat list
  9. | P_vector_subrange of id * Big_int.num * Big_int.num
  10. | P_tuple of pat list
  11. | P_list of pat list
  12. | P_cons of pat * pat
  13. | P_string_append of pat list
  14. | P_struct of fpat list
  15. | P_attribute of string * string * pat
Sourceand pat =
  1. | P_aux of pat_aux * l
Sourceand fpat_aux =
  1. | FP_field of id * pat
  2. | FP_wild
Sourceand fpat =
  1. | FP_aux of fpat_aux * l
Sourcetype loop =
  1. | While
  2. | Until
Sourcetype if_loc = {
  1. if_loc : l;
  2. then_loc : l;
  3. else_loc : l option;
}
Sourcetype measure_aux =
  1. | Measure_none
  2. | Measure_some of exp
Sourceand measure =
  1. | Measure_aux of measure_aux * l
Sourceand 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_typ 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 * if_loc
  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_struct of exp list
  22. | E_struct_update of exp * exp list
  23. | E_field of exp * id
  24. | E_match 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_attribute of string * string * exp
  36. | E_internal_plet of pat * exp * exp
  37. | E_internal_return of exp
Sourceand exp =
  1. | E_aux of exp_aux * l
Sourceand opt_default_aux =
  1. | Def_val_empty
  2. | Def_val_dec of exp
Sourceand opt_default =
  1. | Def_val_aux of opt_default_aux * l
Sourceand pexp_aux =
  1. | Pat_exp of pat * exp
  2. | Pat_when of pat * exp * exp
Sourceand pexp =
  1. | Pat_aux of pexp_aux * l
Sourceand letbind_aux =
  1. | LB_val of pat * exp
Sourceand letbind =
  1. | LB_aux of letbind_aux * l
Sourcetype tannot_opt_aux =
  1. | Typ_annot_opt_none
  2. | Typ_annot_opt_some of typquant * atyp
Sourcetype typschm_opt_aux =
  1. | TypSchm_opt_none
  2. | TypSchm_opt_some of typschm
Sourcetype typschm_opt =
  1. | TypSchm_opt_aux of typschm_opt_aux * l
Sourcetype effect_opt_aux =
  1. | Effect_opt_none
  2. | Effect_opt_effect of atyp
Sourcetype rec_opt_aux =
  1. | Rec_none
  2. | Rec_measure of pat * exp
Sourcetype funcl_aux =
  1. | FCL_funcl of id * pexp
Sourcetype type_union_aux =
  1. | Tu_ty_id of atyp * id
  2. | Tu_ty_anon_rec of (atyp * id) list * id
Sourcetype tannot_opt =
  1. | Typ_annot_opt_aux of tannot_opt_aux * l
Sourcetype effect_opt =
  1. | Effect_opt_aux of effect_opt_aux * l
Sourcetype rec_opt =
  1. | Rec_aux of rec_opt_aux * l
Sourcetype funcl =
  1. | FCL_aux of funcl_aux * l
Sourcetype type_union =
  1. | Tu_aux of type_union_aux * l
Sourcetype subst_aux =
  1. | IS_typ of kid * atyp
  2. | IS_id of id * id
Sourcetype subst =
  1. | IS_aux of subst_aux * l
Sourcetype index_range_aux =
  1. | BF_single of atyp
  2. | BF_range of atyp * atyp
  3. | BF_concat of index_range * index_range
Sourceand index_range =
  1. | BF_aux of index_range_aux * l
Sourcetype default_typing_spec_aux =
  1. | DT_order of kind * atyp
Sourcetype 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_vector_subrange of id * Big_int.num * Big_int.num
  7. | MP_tuple of mpat list
  8. | MP_list of mpat list
  9. | MP_cons of mpat * mpat
  10. | MP_string_append of mpat list
  11. | MP_typ of mpat * atyp
  12. | MP_as of mpat * id
  13. | MP_struct of (id * mpat) list
Sourceand mpat =
  1. | MP_aux of mpat_aux * l
Sourcetype mpexp_aux =
  1. | MPat_pat of mpat
  2. | MPat_when of mpat * exp
Sourcetype mpexp =
  1. | MPat_aux of mpexp_aux * l
Sourcetype mapcl_aux =
  1. | MCL_bidir of mpexp * mpexp
  2. | MCL_forwards of mpexp * exp
  3. | MCL_backwards of mpexp * exp
Sourcetype mapcl =
  1. | MCL_aux of mapcl_aux * l
Sourcetype mapdef_aux =
  1. | MD_mapping of id * typschm_opt * mapcl list
Sourcetype mapdef =
  1. | MD_aux of mapdef_aux * l
Sourcetype outcome_spec_aux =
  1. | OV_outcome of id * typschm * kinded_id list
Sourcetype outcome_spec =
  1. | OV_aux of outcome_spec_aux * l
Sourcetype fundef_aux =
  1. | FD_function of rec_opt * tannot_opt * effect_opt * funcl list
Sourcetype 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
Sourcetype val_spec_aux =
  1. | VS_val_spec of typschm * id * extern option
Sourcetype dec_spec_aux =
  1. | DEC_reg of atyp * id * exp option
Sourcetype scattered_def_aux =
  1. | SD_function of rec_opt * tannot_opt * effect_opt * id
  2. | SD_funcl of funcl
  3. | SD_enum of id
  4. | SD_enumcl of id * id
  5. | SD_variant of id * typquant
  6. | SD_unioncl of id * type_union
  7. | SD_mapping of id * tannot_opt
  8. | SD_mapcl of id * mapcl
  9. | SD_end of id
Sourcetype default_typing_spec =
  1. | DT_aux of default_typing_spec_aux * l
Sourcetype fundef =
  1. | FD_aux of fundef_aux * l
Sourcetype type_def =
  1. | TD_aux of type_def_aux * l
Sourcetype val_spec =
  1. | VS_aux of val_spec_aux * l
Sourcetype dec_spec =
  1. | DEC_aux of dec_spec_aux * l
Sourcetype loop_measure =
  1. | Loop of loop * exp
Sourcetype scattered_def =
  1. | SD_aux of scattered_def_aux * l
Sourcetype prec =
  1. | Infix
  2. | InfixL
  3. | InfixR
Sourcetype fixity_token = prec * Big_int.num * string
Sourcetype def_aux =
  1. | DEF_type of type_def
  2. | DEF_fundef of fundef
  3. | DEF_mapdef of mapdef
  4. | DEF_impl of funcl
  5. | DEF_let of letbind
  6. | DEF_overload of id * id list
  7. | DEF_fixity of prec * Big_int.num * id
  8. | DEF_val of val_spec
  9. | DEF_outcome of outcome_spec * def list
  10. | DEF_instantiation of id * subst list
  11. | DEF_default of default_typing_spec
  12. | DEF_scattered of scattered_def
  13. | DEF_measure of id * pat * exp
  14. | DEF_loop_measures of id * loop_measure list
  15. | DEF_register of dec_spec
  16. | DEF_pragma of string * string
  17. | DEF_attribute of string * string * def
  18. | DEF_doc of string * def
  19. | DEF_internal_mutrec of fundef list
Sourceand def =
  1. | DEF_aux of def_aux * l
Sourcetype lexp_aux =
  1. | LE_id of id
  2. | LE_mem of id * exp list
  3. | LE_vector of lexp * exp
  4. | LE_vector_range of lexp * exp * exp
  5. | LE_vector_concat of lexp list
  6. | LE_field of lexp * id
Sourceand lexp =
  1. | LE_aux of lexp_aux * l
Sourcetype defs =
  1. | Defs of (string * def list) list