summaryrefslogtreecommitdiff
path: root/src/rewriter.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/rewriter.mli')
-rw-r--r--src/rewriter.mli13
1 files changed, 7 insertions, 6 deletions
diff --git a/src/rewriter.mli b/src/rewriter.mli
index e25ebe0e..66ba0709 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -5,17 +5,18 @@ type typ = Type_internal.t
type 'a exp = 'a Ast.exp
type 'a emap = 'a Envmap.t
type envs = Type_check.envs
+type nameset = Nameset.t
-type 'a rewriters = { rewrite_exp : 'a rewriters -> nexp_map option -> 'a exp -> 'a exp;
- rewrite_lexp : 'a rewriters -> nexp_map option -> 'a lexp -> 'a lexp;
- rewrite_pat : 'a rewriters -> nexp_map option -> 'a pat -> 'a pat;
- rewrite_let : 'a rewriters -> nexp_map option -> 'a letbind -> 'a letbind;
+type 'a rewriters = { rewrite_exp : 'a rewriters -> (nexp_map * nameset) option -> 'a exp -> 'a exp;
+ rewrite_lexp : 'a rewriters -> (nexp_map * nameset) option -> 'a lexp -> 'a lexp;
+ rewrite_pat : 'a rewriters -> (nexp_map * nameset) option -> 'a pat -> 'a pat;
+ rewrite_let : 'a rewriters -> (nexp_map * nameset) option -> 'a letbind -> 'a letbind;
rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef;
rewrite_def : 'a rewriters -> 'a def -> 'a def;
rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
}
-
-val rewrite_exp : tannot rewriters -> nexp_map option -> tannot exp -> tannot exp
+
+val rewrite_exp : tannot rewriters -> (nexp_map * nameset) option -> tannot exp -> tannot exp
val rewrite_defs : tannot defs -> tannot defs
val rewrite_defs_ocaml : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
val rewrite_defs_lem : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for lem out*)