libsail 0.15 · OCaml Package

module Big_int = Nat_big_num

type text = string

type l =

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

type 'a annot = l * 'a

type extern = {

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

}

exception Parse_error_locn of l * string

type x = text

type ix = text

type kind_aux =

| K_type
| K_int
| K_order
| K_bool

type kind =

| K_aux of kind_aux * l

type base_effect_aux =

| BE_rreg
| BE_wreg
| BE_rmem
| BE_wmem
| BE_wmv
| BE_eamem
| BE_exmem
| BE_barr
| BE_depend
| BE_undef
| BE_unspec
| BE_nondet
| BE_escape
| BE_config

type kid_aux =

| Var of x

type id_aux =

| Id of x
| Operator of x

type base_effect =

| BE_aux of base_effect_aux * l

type kid =

| Kid_aux of kid_aux * l

type id =

| Id_aux of id_aux * l

type 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

type lit =

| L_aux of lit_aux * l

type atyp_aux =

| ATyp_id of id
| ATyp_var of kid
| ATyp_lit of lit
| ATyp_nset of kid * Big_int.num list
| ATyp_times of atyp * atyp
| ATyp_sum of atyp * atyp
| ATyp_minus of atyp * atyp
| ATyp_exp of atyp
| ATyp_neg of atyp
| ATyp_inc
| ATyp_dec
| ATyp_default_ord
| ATyp_set of base_effect list
| ATyp_fn of atyp * atyp * atyp
| ATyp_bidir of atyp * atyp * atyp
| ATyp_wild
| ATyp_tup of atyp list
| ATyp_app of id * atyp list
| ATyp_exist of kinded_id list * atyp * atyp
| ATyp_base of id * atyp * atyp

and atyp =

| ATyp_aux of atyp_aux * l

and kinded_id_aux =

| KOpt_kind of string option * kid list * kind option

and kinded_id =

| KOpt_aux of kinded_id_aux * l

type quant_item_aux =

| QI_id of kinded_id
| QI_constraint of atyp

type quant_item =

| QI_aux of quant_item_aux * l

type typquant_aux =

| TypQ_tq of quant_item list
| TypQ_no_forall

type typquant =

| TypQ_aux of typquant_aux * l

type typschm_aux =

| TypSchm_ts of typquant * atyp

type typschm =

| TypSchm_aux of typschm_aux * l

type pat_aux =

| P_lit of lit
| P_wild
| P_or of pat * pat
| 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_tup of pat list
| P_list of pat list
| P_cons of pat * pat
| P_string_append of pat list

and pat =

| P_aux of pat_aux * l

and fpat_aux =

| FP_Fpat of id * pat

and fpat =

| FP_aux of fpat_aux * l

type loop =

| While
| Until

type measure_aux =

| Measure_none
| Measure_some of exp

and measure =

| Measure_aux of measure_aux * l

and exp_aux =

| E_block of exp list
| E_id of id
| E_ref of id
| E_deref of exp
| E_lit of lit
| E_cast of atyp * exp
| E_app of id * exp list
| E_app_infix of exp * id * exp
| E_tuple of exp list
| E_if of exp * exp * exp
| 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_record of exp list
| E_record_update of exp * exp list
| E_field of exp * id
| E_case 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_internal_plet of pat * exp * exp
| E_internal_return of exp

and exp =

| E_aux of exp_aux * l

and fexp_aux =

| FE_Fexp of id * exp

and fexp =

| FE_aux of fexp_aux * l

and opt_default_aux =

| Def_val_empty
| Def_val_dec of exp

and opt_default =

| Def_val_aux of opt_default_aux * l

and pexp_aux =

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

and pexp =

| Pat_aux of pexp_aux * l

and letbind_aux =

| LB_val of pat * exp

and letbind =

| LB_aux of letbind_aux * l

type tannot_opt_aux =

| Typ_annot_opt_none
| Typ_annot_opt_some of typquant * atyp

type typschm_opt_aux =

| TypSchm_opt_none
| TypSchm_opt_some of typschm

type typschm_opt =

| TypSchm_opt_aux of typschm_opt_aux * l

type effect_opt_aux =

| Effect_opt_none
| Effect_opt_effect of atyp

type rec_opt_aux =

| Rec_nonrec
| Rec_rec
| Rec_measure of pat * exp

type funcl_aux =

| FCL_Funcl of id * pexp

type type_union_aux =

| Tu_ty_id of atyp * id
| Tu_ty_anon_rec of (atyp * id) list * id

type tannot_opt =

| Typ_annot_opt_aux of tannot_opt_aux * l

type effect_opt =

| Effect_opt_aux of effect_opt_aux * l

type rec_opt =

| Rec_aux of rec_opt_aux * l

type funcl =

| FCL_aux of funcl_aux * l

type type_union =

| Tu_aux of type_union_aux * l

type subst_aux =

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

type subst =

| IS_aux of subst_aux * l

type index_range_aux =

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

and index_range =

| BF_aux of index_range_aux * l

type default_typing_spec_aux =

| DT_order of kind * atyp

type 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_tup 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

and mpat =

| MP_aux of mpat_aux * l

type mpexp_aux =

| MPat_pat of mpat
| MPat_when of mpat * exp

type mpexp =

| MPat_aux of mpexp_aux * l

type mapcl_aux =

| MCL_bidir of mpexp * mpexp
| MCL_forwards of mpexp * exp
| MCL_backwards of mpexp * exp

type mapcl =

| MCL_aux of mapcl_aux * l

type mapdef_aux =

| MD_mapping of id * typschm_opt * mapcl list

type mapdef =

| MD_aux of mapdef_aux * l

type outcome_spec_aux =

| OV_outcome of id * typschm * kinded_id list

type outcome_spec =

| OV_aux of outcome_spec_aux * l

type fundef_aux =

| FD_function of rec_opt * tannot_opt * effect_opt * funcl list

type type_def_aux =

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

type val_spec_aux =

| VS_val_spec of typschm * id * extern option * bool

type dec_spec_aux =

| DEC_reg of atyp * atyp * atyp * id * exp option
| DEC_config of id * atyp * exp

type scattered_def_aux =

| SD_function of rec_opt * tannot_opt * effect_opt * id
| SD_funcl of funcl
| 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

type default_typing_spec =

| DT_aux of default_typing_spec_aux * l

type fundef =

| FD_aux of fundef_aux * l

type type_def =

| TD_aux of type_def_aux * l

type val_spec =

| VS_aux of val_spec_aux * l

type dec_spec =

| DEC_aux of dec_spec_aux * l

type loop_measure =

| Loop of loop * exp

type scattered_def =

| SD_aux of scattered_def_aux * l

type prec =

| Infix
| InfixL
| InfixR

type fixity_token = prec * Big_int.num * string

type def =

| DEF_type of type_def
| DEF_fundef of fundef
| DEF_mapdef of mapdef
| DEF_impl of funcl
| DEF_val of letbind
| DEF_overload of id * id list
| DEF_fixity of prec * Big_int.num * id
| DEF_spec 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_reg_dec of dec_spec
| DEF_pragma of string * string * l
| DEF_internal_mutrec of fundef list

type lexp_aux =

| LEXP_id of id
| LEXP_mem of id * exp list
| LEXP_vector of lexp * exp
| LEXP_vector_range of lexp * exp * exp
| LEXP_vector_concat of lexp list
| LEXP_field of lexp * id

and lexp =

| LEXP_aux of lexp_aux * l

type defs =

| Defs of (string * def list) list

package libsail