Add mrsolver tactic, remove old MRSolver interface

[m-yac]

This PR removes the mr_solver_prove, mr_solver_test, etc. commands in lieu of an interface more in line with the rest of SAW. Now there is a tactic mrsolver which can be applied to any goal of the form refinesS ... f1 f2. (For ease of building refinement goals like this, this PR adds the refines command.) For example, here's how the first proof in sha512_mr_solver.saw changes with this PR:

- mr_solver_prove round_00_15 {{ round_00_15_spec }};
+ thm_round_00_15 <-
+   prove_extcore mrsolver (refines [] round_00_15 {{ round_00_15_spec }});

Additionally, instead of every goal proved with MRSolver being implicitly added to a global set of rewrites, the user provides to the mrsolver tactic a set of the rewrites they wish to apply. This is done using a Refnset, inspired heavily by the design of Simpsets. For example, here's how the next proof in sha512_mr_solver.saw changes with this PR:

- mr_solver_prove round_16_80 {{ round_16_80_spec }};
+ thm_round_16_80 <-
+   prove_extcore
+     (mrsolver_with (addrefns [thm_round_00_15] empty_rs))
+     (refines [] round_16_80 {{ round_16_80_spec }});

These changes are in support of a future development where if MRSolver fails to prove a subgoal, the user will be able to continue the proof script and attempt to prove it themselves. For example, this might look like:

thm_round_16_80 <-
  prove_extcore do {
      mrsolver_with (addrefns [thm_round_00_15] empty_rs);
      unfolding [...];
      simplify (...);
      trivial;
    } (refines [] round_16_80 {{ round_16_80_spec }});

Note: MRSolver currently has some bugs in how it handles Heapster-generated terms caused by changes made last year. Thus most of the Heapster-related MRSolver tests are commented-out – though mr_solver_unit_tests.saw still passes.

[bboston7]

Looks good! Just a few readability comments to address before merging.

[eddywestbrook]

I feel like the evidence is the least important part of what is currently in this file. Maybe it should be called something else? Also, why is it now separate from Term.hs?

[m-yac]

I think my motivation to make this separate from Term.hs is generally because I prefer smaller, easier to digest Haskell files over larger files containing many separate linked ideas. This set of definitions seem like a linked idea, so I decide to break them out – though I realized I never actually explained how they were linked. I added a comment at the top now but here it is reproduced here:

Note: In order to avoid circular dependencies, the 'FunAssump' type and its
dependents in this file ('Refnset' and 'MREvidence') are given a type
parameter `t` which in practice always be 'TheoremNonce' from `Value.hs`.
The reason we cannot just import `Value.hs` here directly is because the
'Refnset' type is used in `Value.hs` - specifically, in the 'VRefnset'
constructor of the 'Value' datatype.

I am not sold on the name Evidence.hs, though. My thoughts were: (1) at some point that Evidence datatype will needed to be fleshed out, at which point that section of the file will get much bigger, and (2) the FunAssump and Refnset datatypes both share the type parameter described above and are both used as key components in Evidence, so Evidence might be a good way to center the file. But, (1) is not the case now and for (2), you could make the argument that FunAssump or Refnset are just as central.

So as for the name, up to you. If you think strongly it should be merged back into Term.hs that's fine too, I'm just worried about these files having too many parts which can make them harder to read.