diff options
| author | Alasdair | 2019-04-27 00:20:37 +0100 |
|---|---|---|
| committer | Alasdair | 2019-04-27 00:40:56 +0100 |
| commit | 0c99f19b012205f1be1d4ae18b722ecbdd80e3d4 (patch) | |
| tree | 55f796f9bdf270064bfe87bdf275b93ffcdc1fb2 /src/rewriter.mli | |
| parent | bf240119e43cb4e3b5f5746b5ef21f19a8fac2d2 (diff) | |
| parent | 094c8e254abde44d45097aca7a36203704fe2ef4 (diff) | |
Merge branch 'sail2' into smt_experiments
Diffstat (limited to 'src/rewriter.mli')
| -rw-r--r-- | src/rewriter.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/rewriter.mli b/src/rewriter.mli index ab29d1d9..878e0d15 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -128,7 +128,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux, ; e_tuple : 'exp list -> 'exp_aux ; e_if : 'exp * 'exp * 'exp -> 'exp_aux ; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux - ; e_loop : loop * 'exp * 'exp -> 'exp_aux + ; e_loop : 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 @@ -254,3 +254,7 @@ val fix_eff_pexp : tannot pexp -> tannot pexp val fix_eff_fexp : tannot fexp -> tannot fexp val fix_eff_opt_default : tannot opt_default -> tannot opt_default + +(* In-order fold over expressions *) +val foldin_exp : (('a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b exp -> 'a * 'b exp +val foldin_pexp : (('a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b exp -> 'a * 'b exp) -> 'a -> 'b pexp -> 'a * 'b pexp |