Rewrite symbolic simulator in pure functional style

We now take advantage of new features of SBV 3.1, including
the "sBranch" mechanism for evaluating reachability of conditional
branches.
Fix typo in comment
Modify symbolic Value type to match the interpreter's Value type

This is a step towards unifying the two modules.
Remove unused length tag from interpreter tuple values
Factor out separate type "BV" for words in evaluator's Value datatype

Instead of constructor VWord Integer Integer, we use VWord BV,
where data BV = BV !Integer !Integer.
Unify Value datatypes for interpreter and symbolic simulator

Some Value constructors and destructors are now polymorphic as well.