sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Parse_ast
module Big_int = Nat_big_num
type text = string
type l =
| Unknown
| Unique of int * l
| Generated of l
| Range of Lexing.position * Lexing.position
| Documented of string * l
type !'a annot = l * 'a
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_rmemt
| BE_wmem
| BE_wmv
| BE_wmvt
| 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 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 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 * (string * string) list * bool
type dec_spec_aux =
| DEC_reg of atyp * atyp * atyp * id
| DEC_config of id * atyp * exp
| DEC_alias of id * exp
| DEC_typ_alias of atyp * id * 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_val of letbind
| DEF_overload of id * id list
| DEF_fixity of prec * Big_int.num * id
| DEF_spec of val_spec
| 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