Infer that terms are defined to send to SMT solver

[ttuegel]

The backend should use the Defined marker when it sends terms to the SMT solver, to infer that terms are defined. Specifically, if the backend passes here, then this check should be skipped.

---

Reported by @denis-bogdanas

[ttuegel]

Plan

• Write tests for translating a partial function:
  • by itself (cannot translate)
  • under a total function (cannot translate)
  • under Defined (can translate)
  • under a total function with both under Defined (can translate)
• Make Translator a newtype. Derive the necessary classes: Monad, MonadTrans, etc.
• Change StateT in Translator to RWST; the "reader" and "writer" components can both be () at first.
• Add a data type TranslatorEnv (below) and give a Default instance where assumeDefined = False.
• Make TranslatorEnv the "reader" component of Translator.
• Where the Application pattern is translated, if assumeDefined is true, then only check that the pattern is function-like instead of functional.
• When a Defined pattern is encountered, use local to set assumeDefined = True.

Definitions

data TranslatorEnv = TranslatorEnv { assumeDefined :: !Bool }