sum-types: Support symbolic evaluation via SBV and What4

[RyanGlScott]

On the sum-types branch (#1602), there is currently no support for symbolic evaluation, e.g.,

enum T = MkT

f : T -> Bool
f _ = True

Main> :prove f
cryptol: src/Cryptol/Symbolic.hs:(295,7)-(296,62): Non-exhaustive patterns in case

At a minimum, we should make Cryptol produce a proper error message here. We should also consider adding symbolic evaluation support via Cryptol's SBV and What4 backends.

SBV's "static" API only supports symbolic Maybe values and symbolic Either values. Cryptol, on the other hand, uses SBV's "dynamic" API. Neither does the dynamic API supports general sum types, as far as I can tell. See also this discussion: LeventErkok/sbv#343

Currently, What4 does not have direct support for general sum types, but this is planned (GaloisInc/what4#251).

[RyanGlScott]

We implemented a slightly different approach in dd6313c than what is described in GaloisInc/what4#251. Instead of translating enums to declare-datatype commands, we instead encode enums as tagged unions. This means that we are able to support all current SBV and What4 solver configurations without any further changes.