summaryrefslogtreecommitdiff
path: root/src/rewrites.mli
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-12-15 21:27:27 +0000
committerAlasdair Armstrong2017-12-15 21:27:27 +0000
commit810dca66a6328fd635f5992256bc24960dcc3899 (patch)
treeb55fed28dd33deebf3c5a97190b0d0366c00ad98 /src/rewrites.mli
parent2162c6586b8024789875c2e619b09ba8348e72e0 (diff)
Experimenting with interactive mode
Diffstat (limited to 'src/rewrites.mli')
-rw-r--r--src/rewrites.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/rewrites.mli b/src/rewrites.mli
index ce24a4c4..db82f679 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -61,6 +61,9 @@ val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list
val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list
(* Perform rewrites to sail intermediate language *)
+val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list
+
+(* Perform rewrites to sail intermediate language *)
val rewrite_defs_sil : (string * (tannot defs -> tannot defs)) list
(* This is a special rewriter pass that checks AST invariants without