add David's Keccak implementation
Only print `Loading` when the module is going to be loaded

  Looks like we were re-loading everything afterall!  This closes #10
Merge branch 'master' into devel
add travis.yml
install the Cabal library before starting the Travis build
disable email notifications for travis
fix expected output for tests after fix in #10
:sat and :prove print counterexamples in the user-configured number base
REPL handles printing of :sat/prove results; parenthesize predicates as appropriate
Update regression tests for :prove and :sat output

As of ee8685e4f283968b236b9328b43b5d72eb49cee6, :sat and :prove now
parse and then pretty print the given predicate with appropriate
parenthesization.
Pretty-print hex literals in parser AST using lowercase "abcdef".

This makes the Cryptol.Parser.AST pretty printer consistent with the
one for values in Cryptol.Eval.Value.
Fix compiler warnings
Optimize symbolic "extract" to produce literal value if result has width 0
prove/sat commands avoid generating SBV bitvector variables of zero width
Merge changes from SBV release version 3.1
Update regression test number 289, which now runs successfully.

This test works as of revision db08bfafa9a67e20fc3ddc5157075cc471ea2b04.

Versions of SBV prior to 3.1 did not distinguish the boolean type from
the size-1 bitvector type; this example uses literals like "0b0" and
"0b1", so it triggered the SBV bug, which manifested as a type error from
the external SMT solver.
Update output for regression test number 290
Update output for regression test 086.

(cf. revision 0ee396d434269e0bee0def34fc3201d38e4a1d22)
Update output for regression test 226
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.