package libsail

  1. Overview
  2. Docs

General rewriting framework for Sail to Sail rewrites

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

The identity re-writer

Same as rewrite_defs_base but display a progress bar when verbosity >= 1

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_vector_subrange : (Ast.id * Libsail.Type_check.Big_int.num * Libsail.Type_check.Big_int.num) -> 'pat_aux;
  13. p_tuple : 'pat list -> 'pat_aux;
  14. p_list : 'pat list -> 'pat_aux;
  15. p_cons : ('pat * 'pat) -> 'pat_aux;
  16. p_string_append : 'pat list -> 'pat_aux;
  17. p_struct : ((Ast.id * 'pat) list * Ast.field_pat_wildcard) -> 'pat_aux;
  18. p_aux : ('pat_aux * 'a Ast.annot) -> 'pat;
}

the type of interpretations of patterns

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_typ : (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_struct : 'fexp list -> 'exp_aux;
  21. e_struct_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_internal_assume : (Ast.n_constraint * 'exp) -> 'exp_aux;
  38. e_aux : ('exp_aux * 'a Ast.annot) -> 'exp;
  39. le_id : Ast.id -> 'lexp_aux;
  40. le_deref : 'exp -> 'lexp_aux;
  41. le_app : (Ast.id * 'exp list) -> 'lexp_aux;
  42. le_typ : (Ast.typ * Ast.id) -> 'lexp_aux;
  43. le_tuple : 'lexp list -> 'lexp_aux;
  44. le_vector : ('lexp * 'exp) -> 'lexp_aux;
  45. le_vector_range : ('lexp * 'exp * 'exp) -> 'lexp_aux;
  46. le_vector_concat : 'lexp list -> 'lexp_aux;
  47. le_field : ('lexp * Ast.id) -> 'lexp_aux;
  48. le_aux : ('lexp_aux * 'a Ast.annot) -> 'lexp;
  49. fe_fexp : (Ast.id * 'exp) -> 'fexp_aux;
  50. fe_aux : ('fexp_aux * 'a Ast.annot) -> 'fexp;
  51. def_val_empty : 'opt_default_aux;
  52. def_val_dec : 'exp -> 'opt_default_aux;
  53. def_val_aux : ('opt_default_aux * 'a Ast.annot) -> 'opt_default;
  54. pat_exp : ('pat * 'exp) -> 'pexp_aux;
  55. pat_when : ('pat * 'exp * 'exp) -> 'pexp_aux;
  56. pat_aux : ('pexp_aux * 'a Ast.annot) -> 'pexp;
  57. lb_val : ('pat * 'exp) -> 'letbind_aux;
  58. lb_aux : ('letbind_aux * 'a Ast.annot) -> 'letbind;
  59. pat_alg : ('a, 'pat, 'pat_aux) pat_alg;
}

the type of interpretations of expressions

val fold_pat : ('a, 'pat, 'pat_aux) pat_alg -> 'a Ast.pat -> 'pat
val fold_mpat : ('a, 'mpat, 'mpat_aux) pat_alg -> 'a Ast.mpat -> 'mpat
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 id_mpat_alg : ('a, 'a Ast.mpat option, 'a Ast.mpat_aux option) 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_typ : 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 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
OCaml

Innovation. Community. Security.