sail
  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Big_int = Nat_big_num
type !'a rewriters = {
  1. rewrite_exp : 'a rewriters -> 'a Ast.exp -> 'a Ast.exp;
  2. rewrite_lexp : 'a rewriters -> 'a Ast.lexp -> 'a Ast.lexp;
  3. rewrite_pat : 'a rewriters -> 'a Ast.pat -> 'a Ast.pat;
  4. rewrite_let : 'a rewriters -> 'a Ast.letbind -> 'a Ast.letbind;
  5. rewrite_fun : 'a rewriters -> 'a Ast.fundef -> 'a Ast.fundef;
  6. rewrite_def : 'a rewriters -> 'a Ast.def -> 'a Ast.def;
  7. 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 = {
  1. p_lit : Ast.lit -> 'pat_aux;
  2. p_wild : 'pat_aux;
  3. p_or : ('pat * 'pat) -> 'pat_aux;
  4. p_not : 'pat -> 'pat_aux;
  5. p_as : ('pat * Ast.id) -> 'pat_aux;
  6. p_typ : (Ast.typ * 'pat) -> 'pat_aux;
  7. p_id : Ast.id -> 'pat_aux;
  8. p_var : ('pat * Ast.typ_pat) -> 'pat_aux;
  9. p_app : (Ast.id * 'pat list) -> 'pat_aux;
  10. p_vector : 'pat list -> 'pat_aux;
  11. p_vector_concat : 'pat list -> 'pat_aux;
  12. p_tup : 'pat list -> 'pat_aux;
  13. p_list : 'pat list -> 'pat_aux;
  14. p_cons : ('pat * 'pat) -> 'pat_aux;
  15. p_string_append : 'pat list -> 'pat_aux;
  16. 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 = {
  1. e_block : 'exp list -> 'exp_aux;
  2. e_id : Ast.id -> 'exp_aux;
  3. e_ref : Ast.id -> 'exp_aux;
  4. e_lit : Ast.lit -> 'exp_aux;
  5. e_cast : (Ast.typ * 'exp) -> 'exp_aux;
  6. e_app : (Ast.id * 'exp list) -> 'exp_aux;
  7. e_app_infix : ('exp * Ast.id * 'exp) -> 'exp_aux;
  8. e_tuple : 'exp list -> 'exp_aux;
  9. e_if : ('exp * 'exp * 'exp) -> 'exp_aux;
  10. e_for : (Ast.id * 'exp * 'exp * 'exp * Ast.order * 'exp) -> 'exp_aux;
  11. e_loop : (Ast.loop * ('exp option * Parse_ast.l) * 'exp * 'exp) -> 'exp_aux;
  12. e_vector : 'exp list -> 'exp_aux;
  13. e_vector_access : ('exp * 'exp) -> 'exp_aux;
  14. e_vector_subrange : ('exp * 'exp * 'exp) -> 'exp_aux;
  15. e_vector_update : ('exp * 'exp * 'exp) -> 'exp_aux;
  16. e_vector_update_subrange : ('exp * 'exp * 'exp * 'exp) -> 'exp_aux;
  17. e_vector_append : ('exp * 'exp) -> 'exp_aux;
  18. e_list : 'exp list -> 'exp_aux;
  19. e_cons : ('exp * 'exp) -> 'exp_aux;
  20. e_record : 'fexp list -> 'exp_aux;
  21. e_record_update : ('exp * 'fexp list) -> 'exp_aux;
  22. e_field : ('exp * Ast.id) -> 'exp_aux;
  23. e_case : ('exp * 'pexp list) -> 'exp_aux;
  24. e_try : ('exp * 'pexp list) -> 'exp_aux;
  25. e_let : ('letbind * 'exp) -> 'exp_aux;
  26. e_assign : ('lexp * 'exp) -> 'exp_aux;
  27. e_sizeof : Ast.nexp -> 'exp_aux;
  28. e_constraint : Ast.n_constraint -> 'exp_aux;
  29. e_exit : 'exp -> 'exp_aux;
  30. e_throw : 'exp -> 'exp_aux;
  31. e_return : 'exp -> 'exp_aux;
  32. e_assert : ('exp * 'exp) -> 'exp_aux;
  33. e_var : ('lexp * 'exp * 'exp) -> 'exp_aux;
  34. e_internal_plet : ('pat * 'exp * 'exp) -> 'exp_aux;
  35. e_internal_return : 'exp -> 'exp_aux;
  36. e_internal_value : Value.value -> 'exp_aux;
  37. e_aux : ('exp_aux * 'a Ast.annot) -> 'exp;
  38. lEXP_id : Ast.id -> 'lexp_aux;
  39. lEXP_deref : 'exp -> 'lexp_aux;
  40. lEXP_memory : (Ast.id * 'exp list) -> 'lexp_aux;
  41. lEXP_cast : (Ast.typ * Ast.id) -> 'lexp_aux;
  42. lEXP_tup : 'lexp list -> 'lexp_aux;
  43. lEXP_vector : ('lexp * 'exp) -> 'lexp_aux;
  44. lEXP_vector_range : ('lexp * 'exp * 'exp) -> 'lexp_aux;
  45. lEXP_vector_concat : 'lexp list -> 'lexp_aux;
  46. lEXP_field : ('lexp * Ast.id) -> 'lexp_aux;
  47. lEXP_aux : ('lexp_aux * 'a Ast.annot) -> 'lexp;
  48. fE_Fexp : (Ast.id * 'exp) -> 'fexp_aux;
  49. fE_aux : ('fexp_aux * 'a Ast.annot) -> 'fexp;
  50. def_val_empty : 'opt_default_aux;
  51. def_val_dec : 'exp -> 'opt_default_aux;
  52. def_val_aux : ('opt_default_aux * 'a Ast.annot) -> 'opt_default;
  53. pat_exp : ('pat * 'exp) -> 'pexp_aux;
  54. pat_when : ('pat * 'exp * 'exp) -> 'pexp_aux;
  55. pat_aux : ('pexp_aux * 'a Ast.annot) -> 'pexp;
  56. lB_val : ('pat * 'exp) -> 'letbind_aux;
  57. lB_aux : ('letbind_aux * 'a Ast.annot) -> 'letbind;
  58. 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