Rewriter: Expose rewrite passes to interactive mode

Rather than each rewrite being an opaque function, with separate lists
of rewrites for each backend, instead put all the rewrites into a
single list then have each backend define which of those rewrites it
wants to use and in what order.

For example, rather than having

let rewrite_defs_ocaml = [
    ...
    ("rewrite_undefined", rewrite_undefined_if_gen false);
    ...
  ]

we would now have

let all_rewrites = [
    ...
    ("undefined", Bool_rewriter (fun b -> Basic_rewriter (rewrite_undefined_if_gen b)));
    ...
  ]

let rewriters_ocaml = [
    ...
    ("undefined", [Bool_arg false]);
    ...
  ]

let rewrite_defs_ocaml =
  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewriters_ocaml

This means we can introspect on the arguments required for each
rewrite, allowing a :rewrite command in the interactive mode which can
parse the arguments required for each rewrite, so we can invoke the
above rewrite as

sail> :rewrite undefined false

with completion for the rewrite name based on all_rewrites, and hints
for any arguments.

The idea behind this is if we want to generate a very custom slice of
a specification, we can set it up as a sequence of interpreter
commands, e.g.

...
:rewrite split execute
:slice_roots execute_LOAD
:slice_cuts rX wX
:slice
:rewrite tuple_assignments
...

where we slice a spec just after splitting the execute function. This
should help in avoiding an endless proliferation of additional options
and flags on the command line.

1 files changed, 2 insertions, 0 deletions

diff --git a/src/slice.mli b/src/slice.mli
index 09558ebf..0eefd087 100644
--- a/src/slice.mli
+++ b/src/slice.mli
@@ -66,3 +66,5 @@ end
 val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph
 
 val dot_of_ast : out_channel -> Type_check.tannot defs -> unit
+
+val filter_ast : Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs