package libsail

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

Module Libsail.AstSource

module Bit = Extraction.Bit
module BitList = Extraction.BitList
include module type of struct include Extraction.Ast end
type l = Parse_ast.l
type visibility = Extraction.Ast.visibility =
  1. | Public
  2. | Private of Parse_ast.l
module Coq_extern = Extraction.Ast.Coq_extern
type extern = Coq_extern.record
module Coq_def_annot = Extraction.Ast.Coq_def_annot
type 'a def_annot = 'a Coq_def_annot.record
type 'a clause_annot = unit def_annot * 'a
type 'a annot = Parse_ast.l * 'a
type 'a non_empty = 'a Extraction.Ast.non_empty =
  1. | Non_empty of 'a * 'a list
type loop = Extraction.Ast.loop =
  1. | While
  2. | Until
type kind_aux = Extraction.Ast.kind_aux =
  1. | K_type
  2. | K_int
  3. | K_bool
type kind = Extraction.Ast.kind =
  1. | K_aux of kind_aux * Parse_ast.l
type kid_aux = Extraction.Ast.kid_aux =
  1. | Var of string
type kid = Extraction.Ast.kid =
  1. | Kid_aux of kid_aux * Parse_ast.l
type kinded_id_aux = Extraction.Ast.kinded_id_aux =
  1. | KOpt_kind of kind * kid
type kinded_id = Extraction.Ast.kinded_id =
  1. | KOpt_aux of kinded_id_aux * Parse_ast.l
type id_aux = Extraction.Ast.id_aux =
  1. | And_bool
  2. | Or_bool
  3. | Id of string
  4. | Operator of string
type id = Extraction.Ast.id =
  1. | Id_aux of id_aux * Parse_ast.l
type value = Extraction.Ast.value =
  1. | V_bitvector of Extraction.Bit.bit list
  2. | V_vector of value list
  3. | V_list of value list
  4. | V_int of Big_int_Z.big_int
  5. | V_real of Extraction.QArith_base.coq_Q
  6. | V_bool of bool
  7. | V_tuple of value list
  8. | V_unit
  9. | V_string of string
  10. | V_ref of id
  11. | V_member of id
  12. | V_ctor of id * value list
  13. | V_record of (id * value) list
type hex_digit = Extraction.Ast.hex_digit =
  1. | Hex_0
  2. | Hex_1
  3. | Hex_2
  4. | Hex_3
  5. | Hex_4
  6. | Hex_5
  7. | Hex_6
  8. | Hex_7
  9. | Hex_8
  10. | Hex_9
  11. | Hex_A
  12. | Hex_B
  13. | Hex_C
  14. | Hex_D
  15. | Hex_E
  16. | Hex_F
type bin_digit = Extraction.Ast.bin_digit =
  1. | Bin_0
  2. | Bin_1
type lit_aux = Extraction.Ast.lit_aux =
  1. | L_unit
  2. | L_true
  3. | L_false
  4. | L_num of Big_int_Z.big_int
  5. | L_hex of hex_digit non_empty list
  6. | L_bin of bin_digit non_empty list
  7. | L_string of string
  8. | L_real of Extraction.QArith_base.coq_Q
type lit = Extraction.Ast.lit =
  1. | L_aux of lit_aux * Parse_ast.l
type nexp_aux = Extraction.Ast.nexp_aux =
  1. | Nexp_id of id
  2. | Nexp_var of kid
  3. | Nexp_constant of Big_int_Z.big_int
  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
and nexp = Extraction.Ast.nexp =
  1. | Nexp_aux of nexp_aux * Parse_ast.l
and typ_aux = Extraction.Ast.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
and typ = Extraction.Ast.typ =
  1. | Typ_aux of typ_aux * Parse_ast.l
and typ_arg_aux = Extraction.Ast.typ_arg_aux =
  1. | A_nexp of nexp
  2. | A_typ of typ
  3. | A_bool of n_constraint
and typ_arg = Extraction.Ast.typ_arg =
  1. | A_aux of typ_arg_aux * Parse_ast.l
and n_constraint_aux = Extraction.Ast.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 * Big_int_Z.big_int list
  8. | NC_and of n_constraint * n_constraint
  9. | NC_or 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
and n_constraint = Extraction.Ast.n_constraint =
  1. | NC_aux of n_constraint_aux * Parse_ast.l
type order_aux = Extraction.Ast.order_aux =
  1. | Ord_inc
  2. | Ord_dec
type quant_item_aux = Extraction.Ast.quant_item_aux =
  1. | QI_id of kinded_id
  2. | QI_constraint of n_constraint
type quant_item = Extraction.Ast.quant_item =
  1. | QI_aux of quant_item_aux * Parse_ast.l
type order = Extraction.Ast.order =
  1. | Ord_aux of order_aux * Parse_ast.l
type struct_name = Extraction.Ast.struct_name =
  1. | SN_id of id
  2. | SN_anon
type field_pat_wildcard = Extraction.Ast.field_pat_wildcard =
  1. | FP_wild of Parse_ast.l
  2. | FP_no_wild
type typ_pat_aux = Extraction.Ast.typ_pat_aux =
  1. | TP_wild
  2. | TP_var of kid
  3. | TP_app of id * typ_pat list
and typ_pat = Extraction.Ast.typ_pat =
  1. | TP_aux of typ_pat_aux * Parse_ast.l
type 'a pat_aux = 'a Extraction.Ast.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 * Big_int_Z.big_int * Big_int_Z.big_int
  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 struct_name * (id * 'a pat) list * field_pat_wildcard
and 'a pat = 'a Extraction.Ast.pat =
  1. | P_aux of 'a pat_aux * 'a annot
type 'a mpat_aux = 'a Extraction.Ast.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 * Big_int_Z.big_int * Big_int_Z.big_int
  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 struct_name * (id * 'a mpat) list
and 'a mpat = 'a Extraction.Ast.mpat =
  1. | MP_aux of 'a mpat_aux * 'a annot
type 'a in_place_loop_measure_aux = 'a Extraction.Ast.in_place_loop_measure_aux =
  1. | Measure_none
  2. | Measure_some of 'a exp
and 'a in_place_loop_measure = 'a Extraction.Ast.in_place_loop_measure =
  1. | Measure_aux of 'a in_place_loop_measure_aux * Parse_ast.l
and 'a exp_aux = 'a Extraction.Ast.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_tuple of 'a exp list
  7. | E_if of 'a exp * 'a exp * 'a exp
  8. | E_loop of loop * 'a in_place_loop_measure * 'a exp * 'a exp
  9. | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp
  10. | E_vector of 'a exp list
  11. | E_vector_append of 'a exp * 'a exp
  12. | E_list of 'a exp list
  13. | E_cons of 'a exp * 'a exp
  14. | E_struct of struct_name * 'a fexp list
  15. | E_struct_update of 'a exp * 'a fexp list
  16. | E_field of 'a exp * id
  17. | E_match of 'a exp * 'a pexp list
  18. | E_let of 'a pat * 'a exp * 'a exp
  19. | E_assign of 'a lexp * 'a exp
  20. | E_sizeof of nexp
  21. | E_return of 'a exp
  22. | E_exit of 'a exp
  23. | E_config of string list
  24. | E_ref of id
  25. | E_throw of 'a exp
  26. | E_try of 'a exp * 'a pexp list
  27. | E_assert of 'a exp * 'a exp
  28. | E_var of 'a lexp * 'a exp * 'a exp
  29. | E_undef
  30. | E_internal_plet of 'a pat * 'a exp * 'a exp
  31. | E_internal_return of 'a exp
  32. | E_internal_value of value
  33. | E_internal_assume of n_constraint * 'a exp
  34. | E_constraint of n_constraint
and 'a exp = 'a Extraction.Ast.exp =
  1. | E_aux of 'a exp_aux * 'a annot
and 'a lexp_aux = 'a Extraction.Ast.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
and 'a lexp = 'a Extraction.Ast.lexp =
  1. | LE_aux of 'a lexp_aux * 'a annot
and 'a fexp_aux = 'a Extraction.Ast.fexp_aux =
  1. | FE_fexp of id * 'a exp
and 'a fexp = 'a Extraction.Ast.fexp =
  1. | FE_aux of 'a fexp_aux * 'a annot
and 'a pexp_aux = 'a Extraction.Ast.pexp_aux =
  1. | Pat_exp of 'a pat * 'a exp
  2. | Pat_when of 'a pat * 'a exp * 'a exp
and 'a pexp = 'a Extraction.Ast.pexp =
  1. | Pat_aux of 'a pexp_aux * 'a annot
type 'a mpexp_aux = 'a Extraction.Ast.mpexp_aux =
  1. | MPat_pat of 'a mpat
  2. | MPat_when of 'a mpat * 'a exp
type 'a mpexp = 'a Extraction.Ast.mpexp =
  1. | MPat_aux of 'a mpexp_aux * 'a annot
type 'a pexp_funcl = 'a pexp
type typquant = quant_item list
type typschm_aux = Extraction.Ast.typschm_aux =
  1. | TypSchm_ts of typquant * typ
type 'a mapcl_aux = 'a Extraction.Ast.mapcl_aux =
  1. | MCL_bidir of 'a mpexp * 'a mpexp
  2. | MCL_forwards of 'a pexp
  3. | MCL_backwards of 'a pexp
type 'a funcl_aux = 'a Extraction.Ast.funcl_aux =
  1. | FCL_funcl of id * 'a pexp_funcl
type tannot_opt_aux = Extraction.Ast.tannot_opt_aux =
  1. | Typ_annot_opt_none
  2. | Typ_annot_opt_some of typquant * typ
type type_union_aux = Extraction.Ast.type_union_aux =
  1. | Tu_ty_id of typ * id
type 'a rec_opt_aux = 'a Extraction.Ast.rec_opt_aux =
  1. | Rec_nonrec
  2. | Rec_rec
  3. | Rec_measure of 'a pat * 'a exp
type typschm = Extraction.Ast.typschm =
  1. | TypSchm_aux of typschm_aux * Parse_ast.l
type 'a mapcl = 'a Extraction.Ast.mapcl =
  1. | MCL_aux of 'a mapcl_aux * 'a clause_annot
type 'a funcl = 'a Extraction.Ast.funcl =
  1. | FCL_aux of 'a funcl_aux * 'a clause_annot
type tannot_opt = Extraction.Ast.tannot_opt =
  1. | Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l
type type_union = Extraction.Ast.type_union =
  1. | Tu_aux of type_union_aux * unit def_annot
type 'a rec_opt = 'a Extraction.Ast.rec_opt =
  1. | Rec_aux of 'a rec_opt_aux * Parse_ast.l
type index_range_aux = Extraction.Ast.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 = Extraction.Ast.index_range =
  1. | BF_aux of index_range_aux * Parse_ast.l
type opt_abstract_config = Extraction.Ast.opt_abstract_config =
  1. | TDC_key of string list
  2. | TDC_none
type outcome_spec_aux = Extraction.Ast.outcome_spec_aux =
  1. | OV_outcome of id * typschm * typquant
type 'a instantiation_spec_aux = 'a Extraction.Ast.instantiation_spec_aux =
  1. | IN_id of id
type val_spec_aux = Extraction.Ast.val_spec_aux =
  1. | VS_val_spec of typschm * id * extern option
type default_spec_aux = Extraction.Ast.default_spec_aux =
  1. | DT_order of order
type 'a scattered_def_aux = 'a Extraction.Ast.scattered_def_aux =
  1. | SD_function of id * tannot_opt
  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 * ((id * typ) * unit def_annot) 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
type 'a dec_spec_aux = 'a Extraction.Ast.dec_spec_aux =
  1. | DEC_reg of typ * id * 'a exp option
type subst_aux = Extraction.Ast.subst_aux =
  1. | IS_typ of kid * typ_arg
  2. | IS_id of id * id
type 'a mapdef_aux = 'a Extraction.Ast.mapdef_aux =
  1. | MD_mapping of id * tannot_opt * 'a mapcl list
type 'a fundef_aux = 'a Extraction.Ast.fundef_aux =
  1. | FD_function of 'a rec_opt * tannot_opt * 'a funcl list
type type_def_aux = Extraction.Ast.type_def_aux =
  1. | TD_abbrev of id * typquant * typ_arg
  2. | TD_record of id * typquant * ((id * typ) * unit def_annot) list * bool
  3. | TD_variant of id * typquant * type_union list * bool
  4. | TD_enum of id * (id * unit def_annot) list * bool
  5. | TD_abstract of id * kind * opt_abstract_config
  6. | TD_bitfield of id * typ * ((id * index_range) * unit def_annot) list
type outcome_spec = Extraction.Ast.outcome_spec =
  1. | OV_aux of outcome_spec_aux * Parse_ast.l
type 'a instantiation_spec = 'a Extraction.Ast.instantiation_spec =
  1. | IN_aux of 'a instantiation_spec_aux * 'a annot
type 'a val_spec = 'a Extraction.Ast.val_spec =
  1. | VS_aux of val_spec_aux * 'a annot
type default_spec = Extraction.Ast.default_spec =
  1. | DT_aux of default_spec_aux * Parse_ast.l
type 'a scattered_def = 'a Extraction.Ast.scattered_def =
  1. | SD_aux of 'a scattered_def_aux * 'a annot
type 'a dec_spec = 'a Extraction.Ast.dec_spec =
  1. | DEC_aux of 'a dec_spec_aux * 'a annot
type prec = Extraction.Ast.prec =
  1. | Infix
  2. | InfixL
  3. | InfixR
type loop_measure = loop * unit exp
type pragma = Extraction.Ast.pragma =
  1. | Pragma_line of string * Parse_ast.l
  2. | Pragma_structured of (string * attribute_data) list
type subst = Extraction.Ast.subst =
  1. | IS_aux of subst_aux * Parse_ast.l
type 'a mapdef = 'a Extraction.Ast.mapdef =
  1. | MD_aux of 'a mapdef_aux * 'a annot
type 'a fundef = 'a Extraction.Ast.fundef =
  1. | FD_aux of 'a fundef_aux * 'a annot
type 'a type_def = 'a Extraction.Ast.type_def =
  1. | TD_aux of type_def_aux * 'a annot
type ('a, 'b) def_aux = ('a, 'b) Extraction.Ast.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 pat * 'a exp
  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 * Big_int_Z.big_int * 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 * loop_measure list
  16. | DEF_register of 'a dec_spec
  17. | DEF_internal_mutrec of 'a fundef list
  18. | DEF_pragma of string * pragma
and ('a, 'b) def = ('a, 'b) Extraction.Ast.def =
  1. | DEF_aux of ('a, 'b) def_aux * 'b def_annot