Introduce class MonadSimplify

[eviefp]

Reviewer checklist

• Test coverage: stack test --coverage
• Public API documentation: stack haddock
• Style conformance: stylish-haskell

---

[ttuegel]

@Vladciobanu I fixed the SMT problems I was having, but I seem to have introduced more failures in unification.

[ttuegel]

@virgil-serbanuta Is it OK if this test no longer explicitly outputs Bottom? I don't actually know what it represents in this case, but it's in a disjunction anway.

[virgil-serbanuta]

In general, for these tests, Bottom means either a branch that we managed to prove, or a branch that ended up as bottom, but we couldn't figure that out early enough (e.g. we applied an axiom, before simplification we didn't know that the result was bottom, but simplification made that clear).

Based on the comments at the top, my guess is that this was the second kind of bottom, perhaps because we applied first the coinductive rule constr11(a) => g(a), then we applied constr11(a) => g(a) to the remainder, without being able to tell that the predicate will become bottom.

[ttuegel]

I think the second explanation makes sense, too. The change that precipitated this change is that we are now using a real simplifier here instead of a mock simplifier for predicates, because the mock simplifier was misbehaving. I switched to using a real simplifier instead of trying to debug the mock; this was the only test output which was affected. I think I know what's happening with the mock simplifier now, so if this test change isn't acceptable I can take another look.

[virgil-serbanuta]

My comment is too late, but: this change is fine.

[ttuegel]

@Vladciobanu I'm going to go ahead and merge this to prevent more conflicts. I think this is already significant progress in the planned refactoring, and it's self-contained (mainly, it just adds MonadSimplify). I think the remaining tasks are:

• Factor SMTT out of SMT
• Remove the MonadIO instance of SMT
• Refactor ReplM onto SMTT IO instead of Simplifier.