package libsail

  1. Overview
  2. Docs
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. | Hint of string * l * l
  5. | Range of Stdlib.Lexing.position * Stdlib.Lexing.position
module Attribute_data : sig ... end

We put the attribute data type in it's own module, so other modules can import it unqualified. The parse AST and the main AST share this type, so modules that wouldn't normally import this module will want to use it.

type 'a annot = l * 'a
type extern = {
  1. pure : bool;
  2. bindings : (string * string) list;
}
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 kid_aux =
  1. | Var of x
type id_aux =
  1. | Id of x
  2. | Operator of x
type kid =
  1. | Kid_aux of kid_aux * l
type id =
  1. | Id_aux of id_aux * l
type 'a infix_token =
  1. | IT_primary of 'a
  2. | IT_op of id
  3. | IT_prefix of id
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 Big_int.num list
  5. | ATyp_in of atyp * atyp
  6. | ATyp_times of atyp * atyp
  7. | ATyp_sum of atyp * atyp
  8. | ATyp_minus of atyp * atyp
  9. | ATyp_exp of atyp
  10. | ATyp_neg of atyp
  11. | ATyp_infix of (atyp infix_token * Stdlib.Lexing.position * Stdlib.Lexing.position) list
  12. | ATyp_inc
  13. | ATyp_dec
  14. | ATyp_set of id list
  15. | ATyp_fn of atyp * atyp * atyp
  16. | ATyp_bidir of atyp * atyp * atyp
  17. | ATyp_wild
  18. | ATyp_tuple of atyp list
  19. | ATyp_app of id * atyp list
  20. | ATyp_if of atyp * atyp * atyp
  21. | ATyp_exist of kinded_id list * atyp * atyp
  22. | ATyp_parens of atyp
and atyp =
  1. | ATyp_aux of atyp_aux * l
and kinded_id_aux =
  1. | KOpt_kind of string option * kid list * kind option * int 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_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 * Attribute_data.attribute_data option * pat
and pat =
  1. | P_aux of pat_aux * l
and fpat_aux =
  1. | FP_field of id * pat
  2. | FP_wild
and fpat =
  1. | FP_aux of fpat_aux * l
type loop =
  1. | While
  2. | Until
type if_loc = {
  1. if_loc : l;
  2. then_loc : l;
  3. else_loc : l option;
}
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_typ of atyp * exp
  7. | E_app of id * exp list
  8. | E_app_infix of exp * id * exp
  9. | E_infix of (exp infix_token * Stdlib.Lexing.position * Stdlib.Lexing.position) list
  10. | E_tuple of exp list
  11. | E_if of exp * exp * exp * if_loc
  12. | E_loop of loop * measure * exp * exp
  13. | E_for of id * exp * exp * exp * atyp * exp
  14. | E_vector of exp list
  15. | E_vector_access of exp * exp
  16. | E_vector_subrange of exp * exp * exp
  17. | E_vector_update of exp * exp * exp
  18. | E_vector_update_subrange of exp * exp * exp * exp
  19. | E_vector_append of exp * exp
  20. | E_list of exp list
  21. | E_cons of exp * exp
  22. | E_struct of exp list
  23. | E_struct_update of exp * exp list
  24. | E_field of exp * id
  25. | E_match of exp * pexp list
  26. | E_let of letbind * exp
  27. | E_assign of exp * exp
  28. | E_sizeof of atyp
  29. | E_constraint of atyp
  30. | E_exit of exp
  31. | E_throw of exp
  32. | E_try of exp * pexp list
  33. | E_return of exp
  34. | E_assert of exp * exp
  35. | E_var of exp * exp * exp
  36. | E_attribute of string * Attribute_data.attribute_data option * exp
  37. | E_internal_plet of pat * exp * exp
  38. | E_internal_return of exp
  39. | E_internal_assume of atyp * exp
and exp =
  1. | E_aux of exp_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_none
  2. | Rec_measure of pat * exp
type funcl =
  1. | FCL_aux of funcl_aux * l
and funcl_aux =
  1. | FCL_private of funcl
  2. | FCL_attribute of string * Attribute_data.attribute_data option * funcl
  3. | FCL_doc of string * funcl
  4. | FCL_funcl of id * pexp
type type_union =
  1. | Tu_aux of type_union_aux * l
and type_union_aux =
  1. | Tu_private of type_union
  2. | Tu_attribute of string * Attribute_data.attribute_data option * type_union
  3. | Tu_doc of string * type_union
  4. | Tu_ty_id of atyp * id
  5. | 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 subst_aux =
  1. | IS_typ of kid * atyp
  2. | IS_id of id * id
type subst =
  1. | IS_aux of subst_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_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
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 =
  1. | MCL_aux of mapcl_aux * l
and mapcl_aux =
  1. | MCL_attribute of string * Attribute_data.attribute_data option * mapcl
  2. | MCL_doc of string * mapcl
  3. | MCL_bidir of mpexp * mpexp
  4. | MCL_forwards_deprecated of mpexp * exp
  5. | MCL_forwards of pexp
  6. | MCL_backwards of pexp
type mapdef_aux =
  1. | MD_mapping of id * typschm_opt * mapcl list
type mapdef =
  1. | MD_aux of mapdef_aux * l
type outcome_spec_aux =
  1. | OV_outcome of id * typschm * kinded_id list
type outcome_spec =
  1. | OV_aux of outcome_spec_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 option * atyp
  2. | TD_record of id * typquant * (atyp * id) list
  3. | TD_variant of id * typquant * type_union list
  4. | TD_enum of id * (id * atyp) list * (id * exp option) list
  5. | TD_abstract of id * kind
  6. | TD_bitfield of id * atyp * (id * index_range) list
type val_spec_aux =
  1. | VS_val_spec of typschm * id * extern option
type dec_spec_aux =
  1. | DEC_reg of atyp * id * exp option
type 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
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_aux =
  1. | DEF_type of type_def
  2. | DEF_constraint of atyp
  3. | DEF_fundef of fundef
  4. | DEF_mapdef of mapdef
  5. | DEF_impl of funcl
  6. | DEF_let of letbind
  7. | DEF_overload of id * id list
  8. | DEF_fixity of prec * Big_int.num * id
  9. | DEF_val of val_spec
  10. | DEF_outcome of outcome_spec * def list
  11. | DEF_instantiation of id * subst list
  12. | DEF_default of default_typing_spec
  13. | DEF_scattered of scattered_def
  14. | DEF_measure of id * pat * exp
  15. | DEF_loop_measures of id * loop_measure list
  16. | DEF_register of dec_spec
  17. | DEF_pragma of string * string * int
  18. | DEF_private of def
  19. | DEF_attribute of string * Attribute_data.attribute_data option * def
  20. | DEF_doc of string * def
  21. | DEF_internal_mutrec of fundef list
and def =
  1. | DEF_aux of def_aux * l
type 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
and lexp =
  1. | LE_aux of lexp_aux * l
type defs =
  1. | Defs of (string * def list) list
OCaml

Innovation. Community. Security.