Module `Libsail.Parse_ast`Source

module Big_int = Nat_big_num

Sourcetype text = string

Sourcetype l =

| Unknown
| Unique of int * l
| Generated of l
| Hint of string * l * l
| Range of Lexing.position * Lexing.position

Sourcemodule 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.

Sourcetype 'a annot = l * 'a

Sourcetype extern = {

pure : bool;
bindings : (string * string) list;

}

Sourceexception Parse_error_locn of l * string

Sourcetype x = text

Sourcetype ix = text

Sourcetype kind_aux =

| K_type
| K_int
| K_order
| K_bool

Sourcetype kind =

| K_aux of kind_aux * l

Sourcetype kid_aux =

| Var of x

Sourcetype id_aux =

| Id of x
| Operator of x

Sourcetype kid =

| Kid_aux of kid_aux * l

Sourcetype id =

| Id_aux of id_aux * l

Sourcetype 'a infix_token =

| IT_primary of 'a
| IT_op of id
| IT_prefix of id

Sourcetype lit_aux =

| L_unit
| L_zero
| L_one
| L_true
| L_false
| L_num of Big_int.num
| L_hex of string
| L_bin of string
| L_undef
| L_string of string
| L_real of string

Sourcetype lit =

| L_aux of lit_aux * l

Sourcetype atyp_aux =

| ATyp_id of id
| ATyp_var of kid
| ATyp_lit of lit
| ATyp_nset of Big_int.num list
| ATyp_in of atyp * atyp
| ATyp_times of atyp * atyp
| ATyp_sum of atyp * atyp
| ATyp_minus of atyp * atyp
| ATyp_exp of atyp
| ATyp_neg of atyp
| ATyp_infix of (atyp infix_token * Lexing.position * Lexing.position) list
| ATyp_inc
| ATyp_dec
| ATyp_set of id list
| ATyp_fn of atyp * atyp * atyp
| ATyp_bidir of atyp * atyp * atyp
| ATyp_wild
| ATyp_tuple of atyp list
| ATyp_app of id * atyp list
| ATyp_if of atyp * atyp * atyp
| ATyp_exist of kinded_id list * atyp * atyp
| ATyp_parens of atyp

Sourceand atyp =

| ATyp_aux of atyp_aux * l

Sourceand kinded_id_aux =

| KOpt_kind of string option * kid list * kind option * int option

Sourceand kinded_id =

| KOpt_aux of kinded_id_aux * l

Sourcetype quant_item_aux =

| QI_id of kinded_id
| QI_constraint of atyp

Sourcetype quant_item =

| QI_aux of quant_item_aux * l

Sourcetype typquant_aux =

| TypQ_tq of quant_item list
| TypQ_no_forall

Sourcetype typquant =

| TypQ_aux of typquant_aux * l

Sourcetype typschm_aux =

| TypSchm_ts of typquant * atyp

Sourcetype typschm =

| TypSchm_aux of typschm_aux * l

Sourcetype pat_aux =

| P_lit of lit
| P_wild
| P_typ of atyp * pat
| P_id of id
| P_var of pat * atyp
| P_app of id * pat list
| P_vector of pat list
| P_vector_concat of pat list
| P_vector_subrange of id * Big_int.num * Big_int.num
| P_tuple of pat list
| P_list of pat list
| P_cons of pat * pat
| P_string_append of pat list
| P_struct of fpat list
| P_attribute of string * Attribute_data.attribute_data option * pat

Sourceand pat =

| P_aux of pat_aux * l

Sourceand fpat_aux =

| FP_field of id * pat
| FP_wild

Sourceand fpat =

| FP_aux of fpat_aux * l

Sourcetype loop =

| While
| Until

Sourcetype if_loc = {

if_loc : l;
then_loc : l;
else_loc : l option;

}

Sourcetype measure_aux =

| Measure_none
| Measure_some of exp

Sourceand measure =

| Measure_aux of measure_aux * l

Sourceand exp_aux =

| E_block of exp list
| E_id of id
| E_ref of id
| E_deref of exp
| E_lit of lit
| E_typ of atyp * exp
| E_app of id * exp list
| E_app_infix of exp * id * exp
| E_infix of (exp infix_token * Lexing.position * Lexing.position) list
| E_tuple of exp list
| E_if of exp * exp * exp * if_loc
| E_loop of loop * measure * exp * exp
| E_for of id * exp * exp * exp * atyp * exp
| E_vector of exp list
| E_vector_access of exp * exp
| E_vector_subrange of exp * exp * exp
| E_vector_update of exp * exp * exp
| E_vector_update_subrange of exp * exp * exp * exp
| E_vector_append of exp * exp
| E_list of exp list
| E_cons of exp * exp
| E_struct of exp list
| E_struct_update of exp * exp list
| E_field of exp * id
| E_match of exp * pexp list
| E_let of letbind * exp
| E_assign of exp * exp
| E_sizeof of atyp
| E_constraint of atyp
| E_exit of exp
| E_throw of exp
| E_try of exp * pexp list
| E_return of exp
| E_assert of exp * exp
| E_var of exp * exp * exp
| E_attribute of string * Attribute_data.attribute_data option * exp
| E_internal_plet of pat * exp * exp
| E_internal_return of exp
| E_internal_assume of atyp * exp

Sourceand exp =

| E_aux of exp_aux * l

Sourceand opt_default_aux =

| Def_val_empty
| Def_val_dec of exp

Sourceand opt_default =

| Def_val_aux of opt_default_aux * l

Sourceand pexp_aux =

| Pat_exp of pat * exp
| Pat_when of pat * exp * exp

Sourceand pexp =

| Pat_aux of pexp_aux * l

Sourceand letbind_aux =

| LB_val of pat * exp

Sourceand letbind =

| LB_aux of letbind_aux * l

Sourcetype tannot_opt_aux =

| Typ_annot_opt_none
| Typ_annot_opt_some of typquant * atyp

Sourcetype typschm_opt_aux =

| TypSchm_opt_none
| TypSchm_opt_some of typschm

Sourcetype typschm_opt =

| TypSchm_opt_aux of typschm_opt_aux * l

Sourcetype effect_opt_aux =

| Effect_opt_none
| Effect_opt_effect of atyp

Sourcetype rec_opt_aux =

| Rec_none
| Rec_measure of pat * exp

Sourcetype funcl =

| FCL_aux of funcl_aux * l

Sourceand funcl_aux =

| FCL_private of funcl
| FCL_attribute of string * Attribute_data.attribute_data option * funcl
| FCL_doc of string * funcl
| FCL_funcl of id * pexp

Sourcetype type_union =

| Tu_aux of type_union_aux * l

Sourceand type_union_aux =

| Tu_private of type_union
| Tu_attribute of string * Attribute_data.attribute_data option * type_union
| Tu_doc of string * type_union
| Tu_ty_id of atyp * id
| Tu_ty_anon_rec of (atyp * id) list * id

Sourcetype tannot_opt =

| Typ_annot_opt_aux of tannot_opt_aux * l

Sourcetype effect_opt =

| Effect_opt_aux of effect_opt_aux * l

Sourcetype rec_opt =

| Rec_aux of rec_opt_aux * l

Sourcetype subst_aux =

| IS_typ of kid * atyp
| IS_id of id * id

Sourcetype subst =

| IS_aux of subst_aux * l

Sourcetype index_range_aux =

| BF_single of atyp
| BF_range of atyp * atyp
| BF_concat of index_range * index_range

Sourceand index_range =

| BF_aux of index_range_aux * l

Sourcetype default_typing_spec_aux =

| DT_order of kind * atyp

Sourcetype mpat_aux =

| MP_lit of lit
| MP_id of id
| MP_app of id * mpat list
| MP_vector of mpat list
| MP_vector_concat of mpat list
| MP_vector_subrange of id * Big_int.num * Big_int.num
| MP_tuple of mpat list
| MP_list of mpat list
| MP_cons of mpat * mpat
| MP_string_append of mpat list
| MP_typ of mpat * atyp
| MP_as of mpat * id
| MP_struct of (id * mpat) list

Sourceand mpat =

| MP_aux of mpat_aux * l

Sourcetype mpexp_aux =

| MPat_pat of mpat
| MPat_when of mpat * exp

Sourcetype mpexp =

| MPat_aux of mpexp_aux * l

Sourcetype mapcl =

| MCL_aux of mapcl_aux * l

Sourceand mapcl_aux =

| MCL_attribute of string * Attribute_data.attribute_data option * mapcl
| MCL_doc of string * mapcl
| MCL_bidir of mpexp * mpexp
| MCL_forwards_deprecated of mpexp * exp
| MCL_forwards of pexp
| MCL_backwards of pexp

Sourcetype mapdef_aux =

| MD_mapping of id * typschm_opt * mapcl list

Sourcetype mapdef =

| MD_aux of mapdef_aux * l

Sourcetype outcome_spec_aux =

| OV_outcome of id * typschm * kinded_id list

Sourcetype outcome_spec =

| OV_aux of outcome_spec_aux * l

Sourcetype fundef_aux =

| FD_function of rec_opt * tannot_opt * effect_opt * funcl list

Sourcetype type_def_aux =

| TD_abbrev of id * typquant * kind option * atyp
| TD_record of id * typquant * (atyp * id) list
| TD_variant of id * typquant * type_union list
| TD_enum of id * (id * atyp) list * (id * exp option) list
| TD_abstract of id * kind
| TD_bitfield of id * atyp * (id * index_range) list

Sourcetype val_spec_aux =

| VS_val_spec of typschm * id * extern option

Sourcetype dec_spec_aux =

| DEC_reg of atyp * id * exp option

Sourcetype scattered_def_aux =

| SD_function of rec_opt * tannot_opt * effect_opt * id
| SD_funcl of funcl
| SD_enum of id
| SD_enumcl of id * id
| SD_variant of id * typquant
| SD_unioncl of id * type_union
| SD_mapping of id * tannot_opt
| SD_mapcl of id * mapcl
| SD_end of id

Sourcetype default_typing_spec =

| DT_aux of default_typing_spec_aux * l

Sourcetype fundef =

| FD_aux of fundef_aux * l

Sourcetype type_def =

| TD_aux of type_def_aux * l

Sourcetype val_spec =

| VS_aux of val_spec_aux * l

Sourcetype dec_spec =

| DEC_aux of dec_spec_aux * l

Sourcetype loop_measure =

| Loop of loop * exp

Sourcetype scattered_def =

| SD_aux of scattered_def_aux * l

Sourcetype prec =

| Infix
| InfixL
| InfixR

Sourcetype fixity_token = prec * Big_int.num * string

Sourcetype def_aux =

| DEF_type of type_def
| DEF_constraint of atyp
| DEF_fundef of fundef
| DEF_mapdef of mapdef
| DEF_impl of funcl
| DEF_let of letbind
| DEF_overload of id * id list
| DEF_fixity of prec * Big_int.num * id
| DEF_val of val_spec
| DEF_outcome of outcome_spec * def list
| DEF_instantiation of id * subst list
| DEF_default of default_typing_spec
| DEF_scattered of scattered_def
| DEF_measure of id * pat * exp
| DEF_loop_measures of id * loop_measure list
| DEF_register of dec_spec
| DEF_pragma of string * string * int
| DEF_private of def
| DEF_attribute of string * Attribute_data.attribute_data option * def
| DEF_doc of string * def
| DEF_internal_mutrec of fundef list

Sourceand def =

| DEF_aux of def_aux * l

Sourcetype lexp_aux =

| LE_id of id
| LE_mem of id * exp list
| LE_vector of lexp * exp
| LE_vector_range of lexp * exp * exp
| LE_vector_concat of lexp list
| LE_field of lexp * id

Sourceand lexp =

| LE_aux of lexp_aux * l

Sourcetype defs =

| Defs of (string * def list) list

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libsail/Libsail/Parse_ast/index.html

Module `Libsail.Parse_ast`Source

package libsail

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libsail/Libsail/Parse_ast/index.html

Module Libsail.Parse_astSource

Module `Libsail.Parse_ast`Source