sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Rewriter
module Big_int = Nat_big_num
type !'a rewriters = {
rewrite_exp : 'a rewriters -> 'a Ast.exp -> 'a Ast.exp;
rewrite_lexp : 'a rewriters -> 'a Ast.lexp -> 'a Ast.lexp;
rewrite_pat : 'a rewriters -> 'a Ast.pat -> 'a Ast.pat;
rewrite_let : 'a rewriters -> 'a Ast.letbind -> 'a Ast.letbind;
rewrite_fun : 'a rewriters -> 'a Ast.fundef -> 'a Ast.fundef;
rewrite_def : 'a rewriters -> 'a Ast.def -> 'a Ast.def;
rewrite_ast : 'a rewriters -> 'a Ast_defs.ast -> 'a Ast_defs.ast;
}
val rewriters_base : Type_check.tannot rewriters
type (!'a, !'pat, !'pat_aux) pat_alg = {
p_lit : Ast.lit -> 'pat_aux;
p_wild : 'pat_aux;
p_or : ('pat * 'pat) -> 'pat_aux;
p_not : 'pat -> 'pat_aux;
p_as : ('pat * Ast.id) -> 'pat_aux;
p_typ : (Ast.typ * 'pat) -> 'pat_aux;
p_id : Ast.id -> 'pat_aux;
p_var : ('pat * Ast.typ_pat) -> 'pat_aux;
p_app : (Ast.id * 'pat list) -> 'pat_aux;
p_vector : 'pat list -> 'pat_aux;
p_vector_concat : 'pat list -> 'pat_aux;
p_tup : 'pat list -> 'pat_aux;
p_list : 'pat list -> 'pat_aux;
p_cons : ('pat * 'pat) -> 'pat_aux;
p_string_append : 'pat list -> 'pat_aux;
p_aux : ('pat_aux * 'a Ast.annot) -> 'pat;
}
type (!'a, !'exp, !'exp_aux, !'lexp, !'lexp_aux, !'fexp, !'fexp_aux, !'opt_default_aux, !'opt_default, !'pexp, !'pexp_aux, !'letbind_aux, !'letbind, !'pat, !'pat_aux) exp_alg = {
e_block : 'exp list -> 'exp_aux;
e_id : Ast.id -> 'exp_aux;
e_ref : Ast.id -> 'exp_aux;
e_lit : Ast.lit -> 'exp_aux;
e_cast : (Ast.typ * 'exp) -> 'exp_aux;
e_app : (Ast.id * 'exp list) -> 'exp_aux;
e_app_infix : ('exp * Ast.id * 'exp) -> 'exp_aux;
e_tuple : 'exp list -> 'exp_aux;
e_if : ('exp * 'exp * 'exp) -> 'exp_aux;
e_for : (Ast.id * 'exp * 'exp * 'exp * Ast.order * 'exp) -> 'exp_aux;
e_loop : (Ast.loop * ('exp option * Parse_ast.l) * 'exp * 'exp) -> 'exp_aux;
e_vector : 'exp list -> 'exp_aux;
e_vector_access : ('exp * 'exp) -> 'exp_aux;
e_vector_subrange : ('exp * 'exp * 'exp) -> 'exp_aux;
e_vector_update : ('exp * 'exp * 'exp) -> 'exp_aux;
e_vector_update_subrange : ('exp * 'exp * 'exp * 'exp) -> 'exp_aux;
e_vector_append : ('exp * 'exp) -> 'exp_aux;
e_list : 'exp list -> 'exp_aux;
e_cons : ('exp * 'exp) -> 'exp_aux;
e_record : 'fexp list -> 'exp_aux;
e_record_update : ('exp * 'fexp list) -> 'exp_aux;
e_field : ('exp * Ast.id) -> 'exp_aux;
e_case : ('exp * 'pexp list) -> 'exp_aux;
e_try : ('exp * 'pexp list) -> 'exp_aux;
e_let : ('letbind * 'exp) -> 'exp_aux;
e_assign : ('lexp * 'exp) -> 'exp_aux;
e_sizeof : Ast.nexp -> 'exp_aux;
e_constraint : Ast.n_constraint -> 'exp_aux;
e_exit : 'exp -> 'exp_aux;
e_throw : 'exp -> 'exp_aux;
e_return : 'exp -> 'exp_aux;
e_assert : ('exp * 'exp) -> 'exp_aux;
e_var : ('lexp * 'exp * 'exp) -> 'exp_aux;
e_internal_plet : ('pat * 'exp * 'exp) -> 'exp_aux;
e_internal_return : 'exp -> 'exp_aux;
e_internal_value : Value.value -> 'exp_aux;
e_aux : ('exp_aux * 'a Ast.annot) -> 'exp;
lEXP_id : Ast.id -> 'lexp_aux;
lEXP_deref : 'exp -> 'lexp_aux;
lEXP_memory : (Ast.id * 'exp list) -> 'lexp_aux;
lEXP_cast : (Ast.typ * Ast.id) -> 'lexp_aux;
lEXP_tup : 'lexp list -> 'lexp_aux;
lEXP_vector : ('lexp * 'exp) -> 'lexp_aux;
lEXP_vector_range : ('lexp * 'exp * 'exp) -> 'lexp_aux;
lEXP_vector_concat : 'lexp list -> 'lexp_aux;
lEXP_field : ('lexp * Ast.id) -> 'lexp_aux;
lEXP_aux : ('lexp_aux * 'a Ast.annot) -> 'lexp;
fE_Fexp : (Ast.id * 'exp) -> 'fexp_aux;
fE_aux : ('fexp_aux * 'a Ast.annot) -> 'fexp;
def_val_empty : 'opt_default_aux;
def_val_dec : 'exp -> 'opt_default_aux;
def_val_aux : ('opt_default_aux * 'a Ast.annot) -> 'opt_default;
pat_exp : ('pat * 'exp) -> 'pexp_aux;
pat_when : ('pat * 'exp * 'exp) -> 'pexp_aux;
pat_aux : ('pexp_aux * 'a Ast.annot) -> 'pexp;
lB_val : ('pat * 'exp) -> 'letbind_aux;
lB_aux : ('letbind_aux * 'a Ast.annot) -> 'letbind;
pat_alg : ( 'a, 'pat, 'pat_aux ) pat_alg;
}
val fold_pat : ( 'a, 'pat, 'pat_aux ) pat_alg -> 'a Ast.pat -> 'pat
val fold_exp : ( 'a, 'exp, 'exp_aux, 'lexp, 'lexp_aux, 'fexp, 'fexp_aux, 'opt_default_aux, 'opt_default, 'pexp, 'pexp_aux, 'letbind_aux, 'letbind, 'pat, 'pat_aux ) exp_alg -> 'a Ast.exp -> 'exp
val fold_letbind : ( 'a, 'exp, 'exp_aux, 'lexp, 'lexp_aux, 'fexp, 'fexp_aux, 'opt_default_aux, 'opt_default, 'pexp, 'pexp_aux, 'letbind_aux, 'letbind, 'pat, 'pat_aux ) exp_alg -> 'a Ast.letbind -> 'letbind
val fold_pexp : ( 'a, 'exp, 'exp_aux, 'lexp, 'lexp_aux, 'fexp, 'fexp_aux, 'opt_default_aux, 'opt_default, 'pexp, 'pexp_aux, 'letbind_aux, 'letbind, 'pat, 'pat_aux ) exp_alg -> 'a Ast.pexp -> 'pexp
val fold_funcl : ( 'a, 'exp, 'exp_aux, 'lexp, 'lexp_aux, 'fexp, 'fexp_aux, 'opt_default_aux, 'opt_default, 'a Ast.pexp, 'pexp_aux, 'letbind_aux, 'letbind, 'pat, 'pat_aux ) exp_alg -> 'a Ast.funcl -> 'a Ast.funcl
val fold_function : ( 'a, 'exp, 'exp_aux, 'lexp, 'lexp_aux, 'fexp, 'fexp_aux, 'opt_default_aux, 'opt_default, 'a Ast.pexp, 'pexp_aux, 'letbind_aux, 'letbind, 'pat, 'pat_aux ) exp_alg -> 'a Ast.fundef -> 'a Ast.fundef
val id_pat_alg : ( 'a, 'a Ast.pat, 'a Ast.pat_aux ) pat_alg
val compute_pat_alg : 'b -> ( 'b -> 'b -> 'b ) -> ( 'a, 'b * 'a Ast.pat, 'b * 'a Ast.pat_aux ) pat_alg
val compute_exp_alg : 'b -> ( 'b -> 'b -> 'b ) -> ( 'a, 'b * 'a Ast.exp, 'b * 'a Ast.exp_aux, 'b * 'a Ast.lexp, 'b * 'a Ast.lexp_aux, 'b * 'a Ast.fexp, 'b * 'a Ast.fexp_aux, 'b * 'a Ast.opt_default_aux, 'b * 'a Ast.opt_default, 'b * 'a Ast.pexp, 'b * 'a Ast.pexp_aux, 'b * 'a Ast.letbind_aux, 'b * 'a Ast.letbind, 'b * 'a Ast.pat, 'b * 'a Ast.pat_aux ) exp_alg
val pure_pat_alg : 'b -> ( 'b -> 'b -> 'b ) -> ( 'a, 'b, 'b ) pat_alg
val pure_exp_alg : 'b -> ( 'b -> 'b -> 'b ) -> ( 'a, 'b, 'b, 'b, 'b, 'b, 'b, 'b, 'b, 'b, 'b, 'b, 'b, 'b, 'b ) exp_alg
val add_p_typ : Type_check.Env.t -> Ast.typ -> 'a Ast.pat -> 'a Ast.pat
val add_e_cast : Type_check.Env.t -> Ast.typ -> 'a Ast.exp -> 'a Ast.exp
val add_typs_let : Type_check.Env.t -> Ast.typ -> Ast.typ -> 'a Ast.exp -> 'a Ast.exp
val effect_of_pexp : Type_check.tannot Ast.pexp -> Ast.effect
val union_eff_exps : Type_check.tannot Ast.exp list -> Ast.effect
val foldin_exp : ( ( 'a -> 'b Ast.exp -> 'a * 'b Ast.exp ) -> 'a -> 'b Ast.exp -> 'a * 'b Ast.exp ) -> 'a -> 'b Ast.exp -> 'a * 'b Ast.exp
val foldin_pexp : ( ( 'a -> 'b Ast.exp -> 'a * 'b Ast.exp ) -> 'a -> 'b Ast.exp -> 'a * 'b Ast.exp ) -> 'a -> 'b Ast.pexp -> 'a * 'b Ast.pexp