Add support for general sum types

[RyanGlScott]

what4 currently supports encoding sum types in one very limited circumstance: when the sum type is an optional type that resembles Haskell's Maybe type. This is done by way of the What4.Partial module, whose PE and Unassigned patterns roughly correspond to Just and Nothing in Haskell's Maybe type.

In GaloisInc/cryptol#1588, we want to add support for user-defined sum types, and in order to do this, we will need SMT solver integration, and as a result, we will need to be able to support general sum types in what4. To my knowledge, there is currently no way to do this in what4, but I can think of two possible routes for getting there:

1. Extend BaseType with a BaseVariantType constructor, and translate BaseVariantType to use SMT-LIB 2.6's declare-datatype command under the hood. This is already how we translate BaseStructType, so it is possible that we could re-use some existing translation machinery to implement this.

2. Add a What4.Variant module that contains definitions that look like this:

   newtype VariantExpr sym (ctx :: Ctx BaseType) = VariantExpr (Assignment (VariantBranch sym) ctx)
   newtype VariantBranch sym (tp :: BaseType) = VariantBranch (PartExpr (Pred sym) (SymExpr sym tp))

   The idea is that instead of extending BaseTypeRepr, we would instead add a separate notion of a VariantExpr that consists of a sequence of pairs, one pair for each constructor. Each pair contains a Pred that indicates if that constructor was used to construct the VariantExpr, along with a SymExpr which represents the fields of the constructor. For concrete VariantExprs, only one Pred in the sequence would ever be equal to truePred.

   This representation is heavily inspired by how Crucible represents sum types here.

Each approach would have its pros and cons:

• Option (1) would likely be the "cleanest" in the sense that it directly uses SMT-LIB and wouldn't require what4 users to analyze a separate concept that is indirectly defined in terms of SymExpr. On the other hand, not all SMT solvers support everything in SMT-LIB 2.6, so this approach would prevent some SMT solvers from working with what4's sum types. (Those same solvers would not be able to use what4's structs either.)
• Option (2) would allow more solvers to work with what4's sum types. The downside is that VariantExpr is not a part of SymExpr, so hooking up a VariantExpr to an actual solver would likely require an extra post-processing step to turn it into a sequence of SymExprs.