Merge branch 'master' into writeFile

2024-11-30 23:45:23 +03:00 · 2015-12-25 21:39:01 -08:00 · 2015-12-25 21:39:01 -08:00 · 752310cd0d
commit 752310cd0d
parent 6848a834fd 3c524e2cb3
35 changed files with 460 additions and 336 deletions
--- a/5
+++ b/5
@ -131,7 +131,7 @@ endif
 ifneq (,${PREFIX})
  PREFIX_ARG      := --prefix=$(call adjust-path,${PREFIX_ABS})
  DESTDIR_ARG     := --destdir=${PKG}
-  CONFIGURE_ARGS  := -f-relocatable -f-self-contained \
+  CONFIGURE_ARGS  := -f-relocatable \
                     --docdir=$(call adjust-path,${PREFIX}/${PREFIX_SHARE}/${PREFIX_DOC}) \
                     ${SERVER_FLAG}
 else
@ -141,8 +141,7 @@ else
  # `cabal copy` will make a mess in the PKG directory.
  PREFIX_ARG      := --prefix=$(call adjust-path,${ROOT_PATH})
  DESTDIR_ARG     := --destdir=${PKG}
-  CONFIGURE_ARGS  := -f-self-contained \
-                     --docdir=$(call adjust-path,${PREFIX_SHARE}/${PREFIX_DOC}) \
+  CONFIGURE_ARGS  := --docdir=$(call adjust-path,${PREFIX_SHARE}/${PREFIX_DOC}) \
                     ${SERVER_FLAG}
 endif

--- a/README.md
+++ b/README.md
@ -37,17 +37,17 @@ On Mac OS X, Cryptol is also available via
 [Homebrew](http://brew.sh/). Simply run `brew update && brew install
 cryptol` to get the latest stable version.

-## Getting CVC4
+## Getting Z3

-Cryptol currently depends on the
-[CVC4 SMT solver](http://cvc4.cs.nyu.edu/) to solve constraints during
-type checking, and as the default solver for the `:sat` and `:prove`
-commands. You can download CVC4 binaries for a variety of platforms
-from their [download page](http://cvc4.cs.nyu.edu/downloads/). Note
-that if you install Cryptol using Homebrew, CVC4 will be installed
-automatically.
+Cryptol currently uses Microsoft Research's
+[Z3 SMT solver](https://github.com/Z3Prover/z3) by default to solve
+constraints during type checking, and as the default solver for the
+`:sat` and `:prove` commands. You can download Z3 binaries for a
+variety of platforms from their
+[releases page](https://github.com/Z3Prover/z3/releases). Note that if you
+install Cryptol using Homebrew, Z3 will be installed automatically.

-After installation, make sure that `cvc4` (or `cvc4.exe` on Windows)
+After installation, make sure that `z3` (or `z3.exe` on Windows)
 is on your PATH.

 # Building Cryptol From Source
@ -64,9 +64,9 @@ Windows. We regularly build and test it in the following environments:

 ## Prerequisites

-Cryptol is developed using GHC 7.8.4 and cabal-install 1.22. The
-easiest way to get the correct versions is to follow the instructions
-on the
+Cryptol is developed using GHC 7.10.2 and cabal-install 1.22, though
+it is still tested with the previous major version of GHC. The easiest
+way to get the correct versions is to follow the instructions on the
 [haskell.org downloads page](https://www.haskell.org/downloads).

 Some supporting non-Haskell libraries are required to build
@ -76,7 +76,7 @@ you may need to install the following:
 - [The GNU Multiple Precision Arithmetic Library (GMP)](https://gmplib.org/)
 - [ncurses](https://www.gnu.org/software/ncurses/)

-You'll also need [CVC4](#getting-cvc4) installed when running Cryptol.
+You'll also need [Z3](#getting-z3) installed when running Cryptol.

 ## Building Cryptol

--- a/cryptol-server/Cryptol/Aeson.hs
+++ b/cryptol-server/Cryptol/Aeson.hs
@ -30,6 +30,7 @@ import qualified Cryptol.Parser.NoInclude as P
 import qualified Cryptol.Parser.NoPat as NoPat
 import qualified Cryptol.Parser.Position as P
 import Cryptol.REPL.Monad
+import qualified Cryptol.Testing.Concrete as Test
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck.InferTypes as T
 import Cryptol.Utils.PP hiding (empty)
@ -112,6 +113,13 @@ instance FromJSON E.BV where
    bv <- o .: "bitvector"
    E.BV <$> bv .: "width" <*> bv .: "value"

+instance ToJSON Test.TestResult where
+  toJSON = \case
+    Test.Pass -> object [ "Pass" .= Null ]
+    Test.FailFalse args -> object [ "FailFalse" .= args ]
+    Test.FailError err args -> object
+      [ "FailError" .= show (pp err), "args" .= args ]
+
 $(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NameInfo)
 $(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''E.EvalError)
 $(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.ParseError)
@ -153,3 +161,4 @@ $(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Ident)
 $(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Range)
 $(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.PName)
 $(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Pass)
+$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Test.TestReport)
--- a/cryptol-server/Main.hs
+++ b/cryptol-server/Main.hs
@ -14,25 +14,31 @@
 {-# LANGUAGE ExtendedDefaultRules #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# OPTIONS_GHC -Wall -fno-warn-type-defaults #-}
 module Main where

 import Control.Concurrent
 import Control.Monad
 import Control.Monad.IO.Class
+import Control.Monad.Trans.Control
+import qualified Control.Exception as X
 import Data.Aeson
 import Data.Aeson.Encode.Pretty
 import qualified Data.ByteString.Char8 as BS
 import qualified Data.ByteString.Lazy.Char8 as BSL
 import Data.Char
 import Data.IORef
+import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Text (Text)
 import qualified Data.Text as T
 import Data.Word
+import Options.Applicative
 import System.Environment
 import System.Exit
 import System.FilePath
+import System.Posix.Signals
 import System.ZMQ4
 import Text.Read

@ -40,9 +46,10 @@ import qualified Cryptol.Eval.Value as E
 import Cryptol.REPL.Command
 import Cryptol.REPL.Monad
 import Cryptol.Symbolic (ProverResult(..))
+import qualified Cryptol.Testing.Concrete as Test
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.ModuleSystem as M
-import Cryptol.Utils.PP
+import Cryptol.Utils.PP hiding ((<>))

 import Cryptol.Aeson ()

@ -58,6 +65,7 @@ data RCommand
  | RCExhaust Text
  | RCProve Text
  | RCSat Text
+  | RCLoadPrelude
  | RCLoadModule FilePath
  | RCDecls
  | RCUnknownCmd Text
@ -67,18 +75,19 @@ instance FromJSON RCommand where
  parseJSON = withObject "RCommand" $ \o -> do
    tag <- o .: "tag"
    flip (withText "tag") tag $ \case
-      "evalExpr"   -> RCEvalExpr              <$> o .: "expr"
-      "applyFun"   -> RCApplyFun              <$> o .: "handle" <*> o .: "arg"
-      "typeOf"     -> RCTypeOf                <$> o .: "expr"
-      "setOpt"     -> RCSetOpt                <$> o .: "key" <*> o .: "value"
-      "check"      -> RCCheck                 <$> o .: "expr"
-      "exhaust"    -> RCExhaust               <$> o .: "expr"
-      "prove"      -> RCProve                 <$> o .: "expr"
-      "sat"        -> RCSat                   <$> o .: "expr"
-      "loadModule" -> RCLoadModule . T.unpack <$> o .: "filePath"
-      "browse"     -> return RCDecls
-      "exit"       -> return RCExit
-      unknown      -> return (RCUnknownCmd unknown)
+      "evalExpr"    -> RCEvalExpr              <$> o .: "expr"
+      "applyFun"    -> RCApplyFun              <$> o .: "handle" <*> o .: "arg"
+      "typeOf"      -> RCTypeOf                <$> o .: "expr"
+      "setOpt"      -> RCSetOpt                <$> o .: "key" <*> o .: "value"
+      "check"       -> RCCheck                 <$> o .: "expr"
+      "exhaust"     -> RCExhaust               <$> o .: "expr"
+      "prove"       -> RCProve                 <$> o .: "expr"
+      "sat"         -> RCSat                   <$> o .: "expr"
+      "loadPrelude" -> return RCLoadPrelude
+      "loadModule"  -> RCLoadModule . T.unpack <$> o .: "filePath"
+      "browse"      -> return RCDecls
+      "exit"        -> return RCExit
+      unknown       -> return (RCUnknownCmd unknown)

 newtype FunHandle = FH Int
  deriving (Eq, Ord, Enum, Bounded, Show)
@ -94,8 +103,8 @@ data RResult
  | RRFunValue FunHandle T.Type
  | RRType T.Schema String -- pretty-printed type
  | RRDecls M.IfaceDecls
-  | RRCheck String
-  | RRExhaust String
+  | RRCheck [Test.TestReport]
+  | RRExhaust [Test.TestReport]
  | RRSat [[E.Value]]
    -- ^ A list of satisfying assignments. Empty list means unsat, max
    -- length determined by @satNum@ interpreter option
@ -106,6 +115,7 @@ data RResult
  | RRUnknownCmd Text
  | RRBadMessage BS.ByteString String
  | RROk
+  | RRInterrupted

 instance ToJSON RResult where
  toJSON = \case
@ -118,9 +128,9 @@ instance ToJSON RResult where
    RRDecls ifds -> object
      [ "tag" .= "decls", "decls" .= ifds ]
    RRCheck out -> object
-      [ "tag" .= "check", "out" .= out ]
+      [ "tag" .= "check", "testReport" .= out ]
    RRExhaust out -> object
-      [ "tag" .= "exhaust", "out" .= out ]
+      [ "tag" .= "exhaust", "testReport" .= out ]
    RRSat out -> object
      [ "tag" .= "sat", "assignments" .= out ]
    RRProve out -> object
@ -133,31 +143,48 @@ instance ToJSON RResult where
      [ "tag" .= "unknownCommand", "command" .= txt ]
    RRBadMessage msg err -> object
      [ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]
-    RROk -> object [ "tag" .= "ok" ]
+    RROk -> object
+      [ "tag" .= "ok" ]
+    RRInterrupted -> object
+      [ "tag" .= "interrupted" ]

 data ControlMsg
  = CMConnect
+    -- ^ Request a new Cryptol context and connection
+  | CMInterrupt Word16
+    -- ^ Request an interrupt of all current Cryptol contexts
  | CMExit
+    -- ^ Request that the entire server shut down
  | CMUnknown Text
+    -- ^ Unknown message

 instance FromJSON ControlMsg where
  parseJSON = withObject "ControlMsg" $ \o -> do
    tag <- o .: "tag"
    flip (withText "tag") tag $ \case
      "connect" -> return CMConnect
+      "interrupt" -> CMInterrupt <$> o .: "port"
      "exit" -> return CMExit
      other -> return $ CMUnknown other

 data ControlReply
  = CRConnect Word16
-  | CROk
+    -- ^ Return the port for a new connection
+  | CRInterrupted
+    -- ^ Acknowledge receipt of an interrupt command
+  | CRExiting
+    -- ^ Acknowledge receipt of an exit command
  | CRBadMessage BS.ByteString String
+    -- ^ Acknowledge receipt of an ill-formed control message

 instance ToJSON ControlReply where
  toJSON = \case
    CRConnect port -> object
      [ "tag" .= "connect", "port" .= port ]
-    CROk -> object [ "tag" .= "ok" ]
+    CRInterrupted -> object
+      [ "tag" .= "interrupted" ]
+    CRExiting -> object
+      [ "tag" .= "exiting" ]
    CRBadMessage msg err -> object
      [ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]

@ -168,6 +195,7 @@ server port =
  let addr = "tcp://127.0.0.1:" ++ show port
  putStrLn ("[cryptol-server] coming online at " ++ addr)
  bind rep addr
+  workers <- newIORef Map.empty
  let loop = do
        msg <- receive rep
        putStrLn "[cryptol-server] received message:"
@ -182,12 +210,21 @@ server port =
            bind newRep "tcp://127.0.0.1:*"
            newAddr <- lastEndpoint newRep
            let portStr = reverse . takeWhile isDigit . reverse $ newAddr
+                workerPort = read portStr
            putStrLn ("[cryptol-server] starting worker on interface " ++ newAddr)
-            void . forkIO $ runRepl newRep
-            reply rep $ CRConnect (read portStr)
+            tid <- forkFinally (runRepl newRep) (removeWorker workers port)
+            addNewWorker workers workerPort tid
+            reply rep $ CRConnect workerPort
+          Right (CMInterrupt port') -> do
+            s <- readIORef workers
+            case Map.lookup port' s of
+              Nothing -> reply rep $ CRBadMessage msg "invalid worker port"
+              Just tid -> do
+                throwTo tid X.UserInterrupt
+                reply rep $ CRInterrupted
          Right CMExit -> do
            putStrLn "[cryptol-server] shutting down"
-            reply rep $ CROk
+            reply rep $ CRExiting
            exitSuccess
          Right (CMUnknown cmd) -> do
            putStrLn ("[cryptol-server] unknown control command: " ++ T.unpack cmd)
@ -202,6 +239,14 @@ reply rep msg = liftIO $ do
  BS.putStrLn bmsg
  send rep [] bmsg

+addNewWorker :: IORef (Map Word16 ThreadId) -> Word16 -> ThreadId -> IO ()
+addNewWorker workers port tid =
+  atomicModifyIORef workers $ \s -> (Map.insert port tid s, ())
+
+removeWorker :: IORef (Map Word16 ThreadId) -> Word16 -> a -> IO ()
+removeWorker workers port _result =
+  atomicModifyIORef workers $ \s -> (Map.delete port s, ())
+
 runRepl :: Socket Rep -> IO ()
 runRepl rep = runREPL False $ do -- TODO: batch mode?
  mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
@ -214,10 +259,11 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
 #else
      where path' = splitSearchPath path
 #endif
-  loadPrelude
  funHandles <- io $ newIORef (Map.empty, minBound :: FunHandle)
  let handle err = reply rep (RRInteractiveError err (show (pp err)))
-      loop = do
+      handleAsync :: X.AsyncException -> IO ()
+      handleAsync _int = reply rep RRInterrupted
+      loop = liftBaseWith $ \run -> X.handle handleAsync $ run $ do
        msg <- io $ receive rep
        io $ putStrLn "[cryptol-worker] received message:"
        case decodeStrict msg of
@ -241,7 +287,16 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
              (m, _) <- io $ readIORef funHandles
              case Map.lookup fh m of
                Nothing -> reply rep (RRBadMessage "invalid function handle" (show fh))
-                Just f -> reply rep (RRValue (f arg))
+                Just f -> do
+                  case f arg of
+                    E.VFun g -> do
+                      gh <- io $ atomicModifyIORef' funHandles $ \(m', gh) ->
+                        let m'' = Map.insert gh g m'
+                            gh' = succ gh
+                        in ((m'', gh'), gh)
+                      -- TODO: bookkeeping to track the type of this value
+                      reply rep (RRFunValue gh T.tZero)
+                    val -> reply rep (RRValue val)
            RCTypeOf txt -> do
              expr <- replParseExpr (T.unpack txt)
              (_expr, _def, sch) <- replCheckExpr expr
@ -250,11 +305,11 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
              setOptionCmd (T.unpack key ++ "=" ++ T.unpack val)
              reply rep RROk
            RCCheck expr -> do
-              (_, out) <- withCapturedOutput (qcCmd QCRandom (T.unpack expr))
-              reply rep (RRCheck out)
+              reports <- qcCmd QCRandom (T.unpack expr)
+              reply rep (RRCheck reports)
            RCExhaust expr -> do
-              (_, out) <- withCapturedOutput (qcCmd QCExhaust (T.unpack expr))
-              reply rep (RRExhaust out)
+              reports <- qcCmd QCExhaust (T.unpack expr)
+              reply rep (RRExhaust reports)
            RCProve expr -> do
              result <- onlineProveSat False (T.unpack expr) Nothing
              case result of
@ -277,6 +332,9 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
                  reply rep (RRProverError err)
                _ ->
                  reply rep (RRProverError "unexpected prover result")
+            RCLoadPrelude -> do
+              loadPrelude
+              reply rep RROk
            RCLoadModule fp -> do
              loadCmd fp
              reply rep RROk
@ -300,13 +358,29 @@ withCapturedOutput m = do
  setPutStr old
  return (x, s)

+data Server = Server { serverPort :: Word16
+                     , serverMaskSIGINT :: Bool }
+  deriving Show
+
 main :: IO ()
-main = do
-  args <- getArgs
-  case args of
-    [] -> server 5555
-    [portStr] ->
-       case readMaybe portStr of
-         Just port -> server port
-         Nothing -> server 5555
-    _ -> error "port is the only allowed argument"
+main = execParser opts >>= mainWith
+  where
+    opts =
+      info (helper <*> serverOpts)
+           ( fullDesc
+          <> progDesc "Run Cryptol as a server via ZeroMQ and JSON"
+          <> header "cryptol-server" )
+    serverOpts =
+      Server
+      <$> option auto
+         ( long "port"
+        <> short 'p'
+        <> metavar "PORT"
+        <> value 5555
+        <> help "TCP port to bind" )
+      <*> switch
+         ( long "mask-interrupts"
+        <> help "Suppress interrupt signals" )
+    mainWith Server {..} = do
+      when serverMaskSIGINT $ void $ installHandler sigINT Ignore Nothing
+      server serverPort
--- a/cryptol.cabal
+++ b/cryptol.cabal
@ -33,10 +33,6 @@ flag relocatable
  default: True
  description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution.

-flag self-contained
-  default: True
-  description: Compile the text of the Cryptol Prelude into the library
-
 flag server
  default: False
  description: Build with the ZeroMQ/JSON cryptol-server executable
@ -44,36 +40,38 @@ flag server
 library
  Default-language:
    Haskell98
-
-  Build-depends:       base             >= 4.7 && < 5,
-                       base-compat      >= 0.6,
-                       array            >= 0.4,
-                       async            >= 2.0,
-                       bytestring       >= 0.10,
-                       containers       >= 0.5,
-                       deepseq          >= 1.3,
-                       deepseq-generics >= 0.1,
-                       directory        >= 1.2,
-                       filepath         >= 1.3,
-                       gitrev           >= 1.0,
-                       generic-trie     >= 0.3.0.1,
-                       GraphSCC         >= 1.0.4,
-                       monadLib         >= 3.7.2,
-                       old-time         >= 1.1,
-                       presburger       >= 1.3,
-                       pretty           >= 1.1,
-                       process          >= 1.2,
-                       QuickCheck       >= 2.7,
-                       random           >= 1.0.1,
-                       sbv              >= 5.3,
-                       smtLib           >= 1.0.7,
-                       simple-smt       >= 0.6.0,
-                       syb              >= 0.4,
-                       text             >= 1.1,
+  Build-depends:       base              >= 4.7 && < 5,
+                       base-compat       >= 0.6,
+                       bytestring        >= 0.10,
+                       array             >= 0.4,
+                       async             >= 2.0,
+                       containers        >= 0.5,
+                       deepseq           >= 1.3,
+                       deepseq-generics  >= 0.1,
+                       directory         >= 1.2,
+                       filepath          >= 1.3,
+                       gitrev            >= 1.0,
+                       generic-trie      >= 0.3.0.1,
+                       GraphSCC          >= 1.0.4,
+                       heredoc           >= 0.2,
+                       monad-control     >= 1.0,
+                       monadLib          >= 3.7.2,
+                       old-time          >= 1.1,
+                       presburger        >= 1.3,
+                       pretty            >= 1.1,
+                       process           >= 1.2,
+                       QuickCheck        >= 2.7,
+                       random            >= 1.0.1,
+                       sbv               >= 5.7,
+                       smtLib            >= 1.0.7,
+                       simple-smt        >= 0.6.0,
+                       syb               >= 0.4,
+                       text              >= 1.1,
                       template-haskell,
-                       tf-random        >= 0.5,
-                       transformers     >= 0.3,
-                       utf8-string      >= 0.3
+                       tf-random         >= 0.5,
+                       transformers      >= 0.3,
+                       transformers-base >= 0.4,
+                       utf8-string       >= 0.3

  Build-tools:         alex, happy
  hs-source-dirs:      src
@ -152,8 +150,7 @@ library
                       Cryptol.Eval.Type,
                       Cryptol.Eval.Value,

-                       Cryptol.Testing.Eval,
-                       Cryptol.Testing.Exhaust,
+                       Cryptol.Testing.Concrete,
                       Cryptol.Testing.Random,

                       Cryptol.Symbolic,
@ -178,10 +175,6 @@ library
  if flag(relocatable)
      cpp-options: -DRELOCATABLE

-  if flag(self-contained)
-    build-depends:     heredoc >= 0.2
-    cpp-options:       -DSELF_CONTAINED
-
 executable cryptol
  Default-language:
    Haskell98
@ -201,6 +194,7 @@ executable cryptol
                     , filepath
                     , haskeline
                     , monadLib
+                     , monad-control
                     , process
                     , random
                     , sbv
@ -223,18 +217,21 @@ executable cryptol-server
  if os(linux) && flag(static)
      ld-options:      -static -pthread
  if flag(server)
-      build-depends:   aeson >= 0.10
-                     , aeson-pretty >= 0.7
-                     , base
-                     , base-compat
-                     , bytestring >= 0.10
-                     , containers
-                     , cryptol
-                     , filepath
-                     , text
-                     , transformers
-                     , unordered-containers >= 0.2
-                     , zeromq4-haskell >= 0.6
+     build-depends: aeson >= 0.10
+                  , aeson-pretty >= 0.7
+                  , base
+                  , base-compat
+                  , bytestring >= 0.10
+                  , containers
+                  , cryptol
+                  , filepath
+                  , monad-control
+                  , optparse-applicative
+                  , text
+                  , transformers
+                  , unix
+                  , unordered-containers >= 0.2
+                  , zeromq4-haskell >= 0.6
  else
      buildable: False

--- a/cryptol/REPL/Haskeline.hs
+++ b/cryptol/REPL/Haskeline.hs
@ -18,8 +18,9 @@ import           Cryptol.REPL.Trie
 import           Cryptol.Utils.PP

 import qualified Control.Exception as X
-import           Control.Monad (guard, when)
+import           Control.Monad (guard, join, when)
 import qualified Control.Monad.Trans.Class as MTL
+import           Control.Monad.Trans.Control
 import           Data.Char (isAlphaNum, isSpace)
 import           Data.Function (on)
 import           Data.List (isPrefixOf,nub,sortBy)
@ -30,6 +31,9 @@ import           System.Directory ( doesFileExist
                                  , getCurrentDirectory)
 import           System.FilePath ((</>))

+import           Prelude ()
+import           Prelude.Compat
+
 -- | Haskeline-specific repl implementation.
 repl :: Cryptolrc -> Maybe FilePath -> REPL () -> IO ()
 repl cryrc mbBatch begin =
@ -133,11 +137,8 @@ data Cryptolrc =
 -- Utilities -------------------------------------------------------------------

 instance MonadException REPL where
-  controlIO branchIO = REPL $ \ ref -> do
-    runBody <- branchIO $ RunIO $ \ m -> do
-      a <- unREPL m ref
-      return (return a)
-    unREPL runBody ref
+  controlIO f = join $ liftBaseWith $ \f' ->
+    f $ RunIO $ \m -> restoreM <$> (f' m)

 -- Titles ----------------------------------------------------------------------

--- a/docs/ProgrammingCryptol.pdf
+++ b/docs/ProgrammingCryptol.pdf
--- a/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
+++ b/docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
@ -349,13 +349,13 @@ user the proof is complete.\indQED\indProve
 \nb{Cryptol uses off-the-shelf SAT\glosSAT and SMT\glosSMT solvers to
  perform these formal
  proofs~\cite{erkok-matthews-cryptolEqChecking-09}.  By default,
-  Cryptol will use the CVC4 SMT solver~\cite{cvc4WWW} under the hood,
+  Cryptol will use Microsoft Research's Z3 SMT solver under the hood,
  but it can be configured to use other SAT/SMT solvers as well, such
-  as SRI's Yices~\cite{YicesWWW}\indYices, or Microsoft Research's
-  Z3~\cite{Z3WWW}\footnote{To do this, first install the package(s)
+  as SRI's Yices~\cite{YicesWWW}\indYices, or CVC4
+  ~\cite{cvc4WWW}\footnote{To do this, first install the package(s)
    from the URLs provided in the bibliography. Once a prover has been
    installed you can activate it with, for example, {\tt :set
-      prover=z3}.}. Note that the {\tt :prove} command is a
+      prover=cvc4}.}. Note that the {\tt :prove} command is a
  push-button tool: once the proof starts there is no user
  involvement. Of course, the external tool used may not be able to
  complete all the proofs in a feasible amount of time, naturally.
--- a/docs/ProgrammingCryptol/installation/Install.tex
+++ b/docs/ProgrammingCryptol/installation/Install.tex
@ -261,7 +261,7 @@ aliases you have defined, along with their types.
     \texttt{base}            & \texttt{10}    & numeric base for printing words  \\
     \texttt{debug}           & \texttt{off}   & whether to print verbose debugging information \\
     \texttt{infLength}       & \texttt{5}     & number of elements to show from an infinite sequence \\
-     \texttt{prover}          & \texttt{cvc4}  & which SMT solver to use for \texttt{:prove}  \\
+     \texttt{prover}          & \texttt{z3}    & which SMT solver to use for \texttt{:prove}  \\
     \texttt{tests}           & \texttt{100}   & number of tests to run for \texttt{:check} \\
     \texttt{warnDefaulting}  & \texttt{on}    & \todo[inline]{talk to Iavor} \\
    \hline
--- a/src/Cryptol/ModuleSystem/Env.hs
+++ b/src/Cryptol/ModuleSystem/Env.hs
@ -27,6 +27,7 @@ import qualified Cryptol.TypeCheck.AST as T
 import Cryptol.Utils.PP (NameDisp)

 import Control.Monad (guard)
+import qualified Control.Exception as X
 import Data.Foldable (fold)
 import Data.Function (on)
 import qualified Data.Map as Map
@ -82,7 +83,11 @@ initialModuleEnv  = do
 #endif
  binDir <- takeDirectory `fmap` getExecutablePath
  let instDir = normalise . joinPath . init . splitPath $ binDir
-  userDir <- getAppUserDataDirectory "cryptol"
+  -- looking up this directory can fail if no HOME is set, as in some
+  -- CI settings
+  let handle :: X.IOException -> IO String
+      handle _e = return ""
+  userDir <- X.catch (getAppUserDataDirectory "cryptol") handle
  return ModuleEnv
    { meLoadedModules = mempty
    , meNameSeeds     = T.nameSeeds
@ -111,8 +116,8 @@ initialModuleEnv  = do
    , meDynEnv        = mempty
    , meMonoBinds     = True
    , meSolverConfig  = T.SolverConfig
-                          { T.solverPath = "cvc4"
-                          , T.solverArgs = [ "--lang=smt2", "--incremental", "--rewrite-divk" ]
+                          { T.solverPath = "z3"
+                          , T.solverArgs = [ "-smt2", "-in" ]
                          , T.solverVerbose = 0
                          }
    , meCoreLint      = NoCoreLint
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@ -139,7 +139,7 @@ instance PP RenamerWarning where
  ppPrec _ (SymbolShadowed new originals disp) = fixNameDisp disp $
    hang (text "[warning] at" <+> loc)
       4 $ fsep [ text "This binding for" <+> sym
-                , text "shadows the existing binding" <> plural <+> text "from" ]
+                , (text "shadows the existing binding" <> plural) <+> text "from" ]
        $$ vcat (map ppLocName originals)

    where
--- a/src/Cryptol/Parser/AST.hs
+++ b/src/Cryptol/Parser/AST.hs
@ -717,7 +717,7 @@ instance (Show name, PPName name) => PP (Expr name) where
      ESel    e l   -> ppPrec 4 e <> text "." <> pp l

      -- low prec
-      EFun xs e     -> wrap n 0 (text "\\" <> hsep (map (ppPrec 3) xs) <+>
+      EFun xs e     -> wrap n 0 ((text "\\" <> hsep (map (ppPrec 3) xs)) <+>
                                 text "->" <+> pp e)

      EIf e1 e2 e3  -> wrap n 0 $ sep [ text "if"   <+> pp e1
--- a/src/Cryptol/Prelude.hs
+++ b/src/Cryptol/Prelude.hs
@ -6,7 +6,7 @@
 -- Stability   :  provisional
 -- Portability :  portable
 --
-- Include the prelude when building with -fself-contained
+-- Compile the prelude into the executable as a last resort

 {-# LANGUAGE CPP #-}
 {-# LANGUAGE QuasiQuotes #-}
@ -16,8 +16,6 @@ module Cryptol.Prelude (writePreludeContents) where

 import Cryptol.ModuleSystem.Monad

-#ifdef SELF_CONTAINED
-
 import System.Directory (getTemporaryDirectory)
 import System.IO (hClose, hPutStr, openTempFile)
 import Text.Heredoc (there)
@ -34,13 +32,3 @@ writePreludeContents = io $ do
  hPutStr h preludeContents
  hClose h
  return path
-
-#else
-
-import Cryptol.Utils.Ident (preludeName)
-
-- | If we're not self-contained, the Prelude is just missing
-writePreludeContents :: ModuleM FilePath
-writePreludeContents = moduleNotFound preludeName =<< getSearchPath
-
-#endif
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@ -54,9 +54,8 @@ import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowe
 import qualified Cryptol.Utils.Ident as M

 import qualified Cryptol.Eval.Value as E
-import qualified Cryptol.Testing.Eval    as Test
+import Cryptol.Testing.Concrete
 import qualified Cryptol.Testing.Random  as TestR
-import qualified Cryptol.Testing.Exhaust as TestX
 import Cryptol.Parser
    (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
    ,parseModName,parseHelpName)
@ -74,7 +73,7 @@ import qualified Cryptol.Symbolic as Symbolic

 import Control.DeepSeq
 import qualified Control.Exception as X
-import Control.Monad (guard,unless,forM_,when)
+import Control.Monad hiding (mapM, mapM_)
 import qualified Data.ByteString as BS
 import Data.Bits ((.&.))
 import Data.Char (isSpace,isPunctuation,isSymbol)
@ -160,9 +159,9 @@ nbCommandList  =
    "display a brief description about a function"
  , CommandDescr [ ":s", ":set" ] (OptionArg setOptionCmd)
    "set an environmental option (:set on its own displays current values)"
-  , CommandDescr [ ":check" ] (ExprArg (qcCmd QCRandom))
+  , CommandDescr [ ":check" ] (ExprArg (void . qcCmd QCRandom))
    "use random testing to check that the argument always returns true (if no argument, check all properties)"
-  , CommandDescr [ ":exhaust" ] (ExprArg (qcCmd QCExhaust))
+  , CommandDescr [ ":exhaust" ] (ExprArg (void . qcCmd QCExhaust))
    "use exhaustive testing to prove that the argument always returns true (if no argument, check all properties)"
  , CommandDescr [ ":prove" ] (ExprArg proveCmd)
    "use an external solver to prove that the argument always returns true (if no argument, check all properties)"
@ -259,54 +258,78 @@ data QCMode = QCRandom | QCExhaust deriving (Eq, Show)
 -- | Randomly test a property, or exhaustively check it if the number
 -- of values in the type under test is smaller than the @tests@
 -- environment variable, or we specify exhaustive testing.
-qcCmd :: QCMode -> String -> REPL ()
+qcCmd :: QCMode -> String -> REPL [TestReport]
 qcCmd qcMode "" =
  do (xs,disp) <- getPropertyNames
     let nameStr x = show (fixNameDisp disp (pp x))
     if null xs
-        then rPutStrLn "There are no properties in scope."
-        else forM_ xs $ \x ->
+        then rPutStrLn "There are no properties in scope." *> return []
+        else concat <$> (forM xs $ \x ->
               do let str = nameStr x
                  rPutStr $ "property " ++ str ++ " "
-                  qcCmd qcMode str
+                  qcCmd qcMode str)

 qcCmd qcMode str =
  do expr <- replParseExpr str
     (val,ty) <- replEvalExpr expr
     EnvNum testNum  <- getUser "tests"
-     case TestX.testableType ty of
-       Just (sz,vss) | qcMode == QCExhaust || sz <= toInteger testNum ->
-         do rPutStrLn "Using exhaustive testing."
-            let doTest _ [] = panic "We've unexpectedly run out of test cases"
-                                    []
-                doTest _ (vs : vss1) = do
-                  result <- TestX.runOneTest val vs
+     case testableType ty of
+       Just (sz,vss) | qcMode == QCExhaust || sz <= toInteger testNum -> do
+            rPutStrLn "Using exhaustive testing."
+            let f _ [] = panic "Cryptol.REPL.Command"
+                                    ["Exhaustive testing ran out of test cases"]
+                f _ (vs : vss1) = do
+                  result <- io $ runOneTest val vs
                  return (result, vss1)
-            ok <- go doTest sz 0 vss
-            when ok $ rPutStrLn "Q.E.D."
+                testSpec = TestSpec {
+                    testFn = f
+                  , testProp = str
+                  , testTotal = sz
+                  , testPossible = sz
+                  , testRptProgress = ppProgress
+                  , testClrProgress = delProgress
+                  , testRptFailure = ppFailure
+                  , testRptSuccess = do
+                      delTesting
+                      prtLn $ "passed " ++ show sz ++ " tests."
+                      rPutStrLn "Q.E.D."
+                  }
+            prt testingMsg
+            report <- runTests testSpec vss
+            return [report]

-       n -> case TestR.testableType ty of
+       Just (sz,_) -> case TestR.testableType ty of
              Nothing   -> raise (TypeNotTestable ty)
-              Just gens ->
-                do rPutStrLn "Using random testing."
-                   prt testingMsg
-                   g <- io newTFGen
-                   ok <- go (TestR.runOneTest val gens) testNum 0 g
-                   when ok $
-                     case n of
-                       Just (valNum,_) ->
-                         do let valNumD = fromIntegral valNum :: Double
-                                percent = fromIntegral (testNum * 100)
-                                        / valNumD
-                                showValNum
-                                   | valNum > 2 ^ (20::Integer) =
-                                       "2^^" ++ show (lg2 valNum)
-                                   | otherwise = show valNum
-                            rPutStrLn $ "Coverage: "
-                                         ++ showFFloat (Just 2) percent "% ("
-                                         ++ show testNum ++ " of "
-                                         ++ showValNum ++ " values)"
-                       Nothing -> return ()
+              Just gens -> do
+                rPutStrLn "Using random testing."
+                let testSpec = TestSpec {
+                        testFn = \sz' g -> io $ TestR.runOneTest val gens sz' g
+                      , testProp = str
+                      , testTotal = toInteger testNum
+                      , testPossible = sz
+                      , testRptProgress = ppProgress
+                      , testClrProgress = delProgress
+                      , testRptFailure = ppFailure
+                      , testRptSuccess = do
+                          delTesting
+                          prtLn $ "passed " ++ show testNum ++ " tests."
+                      }
+                prt testingMsg
+                g <- io newTFGen
+                report <- runTests testSpec g
+                when (isPass (reportResult report)) $ do
+                  let szD = fromIntegral sz :: Double
+                      percent = fromIntegral (testNum * 100) / szD
+                      showValNum
+                        | sz > 2 ^ (20::Integer) =
+                          "2^^" ++ show (lg2 sz)
+                        | otherwise = show sz
+                  rPutStrLn $ "Coverage: "
+                    ++ showFFloat (Just 2) percent "% ("
+                    ++ show testNum ++ " of "
+                    ++ showValNum ++ " values)"
+                return [report]
+       Nothing -> return []

  where
  testingMsg = "testing..."
@ -332,37 +355,23 @@ qcCmd qcMode str =
  delTesting  = del (length testingMsg)
  delProgress = del totProgressWidth

-  go _ totNum testNum _
-     | testNum >= totNum =
-         do delTesting
-            prtLn $ "passed " ++ show totNum ++ " tests."
-            return True
-
-  go doTest totNum testNum st =
-     do ppProgress testNum totNum
-        res <- io $ doTest (div (100 * (1 + testNum)) totNum) st
-        opts <- getPPValOpts
-        delProgress
-        case res of
-          (Test.Pass, st1) -> do delProgress
-                                 go doTest totNum (testNum + 1) st1
-          (failure, _g1) -> do
-            delTesting
-            case failure of
-              Test.FailFalse [] -> do
-                prtLn "FAILED"
-              Test.FailFalse vs -> do
-                prtLn "FAILED for the following inputs:"
-                mapM_ (rPrint . pp . E.WithBase opts) vs
-              Test.FailError err [] -> do
-                prtLn "ERROR"
-                rPrint (pp err)
-              Test.FailError err vs -> do
-                prtLn "ERROR for the following inputs:"
-                mapM_ (rPrint . pp . E.WithBase opts) vs
-                rPrint (pp err)
-              Test.Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]
-            return False
+  ppFailure failure = do
+    delTesting
+    opts <- getPPValOpts
+    case failure of
+      FailFalse [] -> do
+        prtLn "FAILED"
+      FailFalse vs -> do
+        prtLn "FAILED for the following inputs:"
+        mapM_ (rPrint . pp . E.WithBase opts) vs
+      FailError err [] -> do
+        prtLn "ERROR"
+        rPrint (pp err)
+      FailError err vs -> do
+        prtLn "ERROR for the following inputs:"
+        mapM_ (rPrint . pp . E.WithBase opts) vs
+        rPrint (pp err)
+      Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]

 satCmd, proveCmd :: String -> REPL ()
 satCmd = cmdProveSat True
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@ -6,10 +6,12 @@
 -- Stability   :  provisional
 -- Portability :  portable

-{-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}

 module Cryptol.REPL.Monad (
@ -86,7 +88,9 @@ import qualified Cryptol.Parser.AST as P
 import Cryptol.Symbolic (proverNames, lookupProver, SatNum(..))

 import Control.Monad (ap,unless,when)
+import Control.Monad.Base
 import Control.Monad.IO.Class
+import Control.Monad.Trans.Control
 import Data.Char (isSpace)
 import Data.IORef
    (IORef,newIORef,readIORef,modifyIORef,atomicModifyIORef)
@ -176,12 +180,20 @@ instance Monad REPL where
 instance MonadIO REPL where
  liftIO = io

+instance MonadBase IO REPL where
+  liftBase = liftIO
+
+instance MonadBaseControl IO REPL where
+  type StM REPL a = a
+  liftBaseWith f = REPL $ \ref ->
+    f $ \m -> unREPL m ref
+  restoreM x = return x
+
 instance M.FreshM REPL where
  liftSupply f = modifyRW $ \ RW { .. } ->
    let (a,s') = f (M.meSupply eModuleEnv)
     in (RW { eModuleEnv = eModuleEnv { M.meSupply = s' }, .. },a)

-
 -- Exceptions ------------------------------------------------------------------

 -- | REPL exceptions.
@ -593,7 +605,7 @@ userOptions  = mkOptionMap
    "The number of random tests to try."
  , simpleOpt "satNum" (EnvString "1") checkSatNum
    "The maximum number of :sat solutions to display (\"all\" for no limit)."
-  , simpleOpt "prover" (EnvString "cvc4") checkProver $
+  , simpleOpt "prover" (EnvString "z3") checkProver $
    "The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
  , simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing)
    "Choose if we should display warnings when defaulting."
@ -607,9 +619,7 @@ userOptions  = mkOptionMap
                          setModuleEnv me { M.meMonoBinds = b }
          _         -> return ()

-  , OptionDescr "tc-solver" (EnvProg "cvc4" [ "--lang=smt2"
-                                            , "--incremental"
-                                            , "--rewrite-divk" ])
+  , OptionDescr "tc-solver" (EnvProg "z3" [ "-smt2", "-in" ])
    (const (return Nothing)) -- TODO: check for the program in the path
    "The solver that will be used by the type checker" $
    \case EnvProg prog args -> do me <- getModuleEnv
@ -697,27 +707,27 @@ whenDebug m = do
 smokeTest :: REPL [Smoke]
 smokeTest = catMaybes <$> sequence tests
  where
-    tests = [ cvc4exists ]
+    tests = [ z3exists ]

 type SmokeTest = REPL (Maybe Smoke)

 data Smoke
-  = CVC4NotFound
+  = Z3NotFound
  deriving (Show, Eq)

 instance PP Smoke where
  ppPrec _ smoke =
    case smoke of
-      CVC4NotFound -> text . intercalate " " $ [
-          "[error] cvc4 is required to run Cryptol, but was not found in the"
-        , "system path. See the Cryptol README for more on how to install cvc4."
+      Z3NotFound -> text . intercalate " " $ [
+          "[error] z3 is required to run Cryptol, but was not found in the"
+        , "system path. See the Cryptol README for more on how to install z3."
        ]

-cvc4exists :: SmokeTest
-cvc4exists = do
-  mPath <- io $ findExecutable "cvc4"
+z3exists :: SmokeTest
+z3exists = do
+  mPath <- io $ findExecutable "z3"
  case mPath of
-    Nothing -> return (Just CVC4NotFound)
+    Nothing -> return (Just Z3NotFound)
    Just _  -> return Nothing


--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@ -6,6 +6,7 @@
 -- Stability   :  provisional
 -- Portability :  portable

+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@ -222,7 +223,7 @@ protectStack mkErr cmd modEnv =
  where isOverflow X.StackOverflow = Just ()
        isOverflow _               = Nothing
        msg = "Symbolic evaluation failed to terminate."
-        handler () = mkErr msg modEnv -- (Right (ProverError msg, modEnv), [])
+        handler () = mkErr msg modEnv

 parseValues :: [FinType] -> [SBV.CW] -> ([Eval.Value], [SBV.CW])
 parseValues [] cws = ([], cws)
@ -404,7 +405,7 @@ evalSel sel v =

    ListSel n _   -> case v of
                       VWord s -> VBit (SBV.svTestBit s i)
-                                    where i = SBV.svBitSize s - 1 - n
+                                    where i = SBV.intSizeOf s - 1 - n
                       _       -> fromSeq v !! n  -- 0-based indexing

 -- Declarations ----------------------------------------------------------------
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@ -24,6 +24,7 @@ import Cryptol.Utils.Panic
 import Cryptol.ModuleSystem.Name (asPrim)
 import Cryptol.Utils.Ident (Ident,mkIdent)

+import qualified Data.SBV         as SBV
 import qualified Data.SBV.Dynamic as SBV
 import qualified Data.Map as Map
 import qualified Data.Text as T
@ -286,9 +287,9 @@ atV def vs i =
      case foldr weave vs bits of
        [] -> def
        y : _ -> y
-    VWord x -> foldr f def (zip [0 .. 2 ^ SBV.svBitSize x - 1] vs)
+    VWord x -> foldr f def (zip [0 .. 2 ^ SBV.intSizeOf x - 1] vs)
      where
-        k = SBV.svKind x
+        k = SBV.kindOf x
        f (n, v) y = iteValue (SBV.svEqual x (SBV.svInteger k n)) v y
    _ -> evalPanic "Cryptol.Symbolic.Prims.selectV" ["Invalid index argument"]
  where
@ -315,7 +316,7 @@ nthV err v n =
  case v of
    VStream xs -> nth err xs (fromInteger n)
    VSeq _ xs  -> nth err xs (fromInteger n)
-    VWord x                 -> let i = SBV.svBitSize x - 1 - fromInteger n
+    VWord x                 -> let i = SBV.intSizeOf x - 1 - fromInteger n
                               in if i < 0 then err else
                                    VBit (SBV.svTestBit x i)
    _                       -> err
@ -340,13 +341,13 @@ dropV n xs =
  case xs of
    VSeq b xs'  -> VSeq b (genericDrop n xs')
    VStream xs' -> VStream (genericDrop n xs')
-    VWord w     -> VWord $ SBV.svExtract (SBV.svBitSize w - 1 - fromInteger n) 0 w
+    VWord w     -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1 - fromInteger n) 0 w
    _           -> panic "Cryptol.Symbolic.Prims.dropV" [ "non-droppable value" ]

 takeV :: Integer -> Value -> Value
 takeV n xs =
  case xs of
-    VWord w     -> VWord $ SBV.svExtract (SBV.svBitSize w - 1) (SBV.svBitSize w - fromInteger n) w
+    VWord w     -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1) (SBV.intSizeOf w - fromInteger n) w
    VSeq b xs'  -> VSeq b (genericTake n xs')
    VStream xs' -> VSeq b (genericTake n xs')
                     where b = case xs' of VBit _ : _ -> True
@ -423,7 +424,7 @@ arithUnary op = loop . toTypeVal

 sExp :: SWord -> SWord -> SWord
 sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order
-  where go []       = literalSWord (SBV.svBitSize x) 1
+  where go []       = literalSWord (SBV.intSizeOf x) 1
        go (b : bs) = SBV.svIte b (SBV.svTimes x s) s
            where a = go bs
                  s = SBV.svTimes a a
@ -432,8 +433,8 @@ sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order
 sLg2 :: SWord -> SWord
 sLg2 x = go 0
  where
-    lit n = literalSWord (SBV.svBitSize x) n
-    go i | i < SBV.svBitSize x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
+    lit n = literalSWord (SBV.intSizeOf x) n
+    go i | i < SBV.intSizeOf x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
         | otherwise           = lit (toInteger i)

 -- Cmp -------------------------------------------------------------------------
--- a/src/Cryptol/Symbolic/Value.hs
+++ b/src/Cryptol/Symbolic/Value.hs
@ -29,6 +29,7 @@ module Cryptol.Symbolic.Value

 import Data.List (foldl')

+import Data.SBV (HasKind(..))
 import Data.SBV.Dynamic

 import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,
@ -92,7 +93,7 @@ mergeValue f c v1 v2 =
                                  [ "mergeValue: incompatible values" ]
  where
    mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2
-    mergeWord w1 w2 = svSymbolicMerge (svKind w1) f c w1 w2
+    mergeWord w1 w2 = svSymbolicMerge (kindOf w1) f c w1 w2
    mergeField (n1, x1) (n2, x2)
      | n1 == n2  = (n1, mergeValue f c x1 x2)
      | otherwise = panic "Cryptol.Symbolic.Value"
@ -104,7 +105,7 @@ mergeValue f c v1 v2 =

 instance BitWord SBool SWord where
  packWord bs = fromBitsLE (reverse bs)
-  unpackWord x = [ svTestBit x i | i <- reverse [0 .. svBitSize x - 1] ]
+  unpackWord x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ]

 -- Errors ----------------------------------------------------------------------

--- a/src/Cryptol/Testing/Concrete.hs
+++ b/src/Cryptol/Testing/Concrete.hs
@ -6,17 +6,56 @@
 -- Stability   :  provisional
 -- Portability :  portable

-module Cryptol.Testing.Exhaust where
+{-# LANGUAGE RecordWildCards #-}
+module Cryptol.Testing.Concrete where

-import qualified Cryptol.Testing.Eval as Eval
-import Cryptol.TypeCheck.AST
+import Cryptol.Eval.Error
 import Cryptol.Eval.Value
+import Cryptol.TypeCheck.AST
+import Cryptol.Utils.Panic (panic)

+import qualified Control.Exception as X
 import Data.List(genericReplicate)

 import Prelude ()
 import Prelude.Compat

+-- | A test result is either a pass, a failure due to evaluating to
+-- @False@, or a failure due to an exception raised during evaluation
+data TestResult
+  = Pass
+  | FailFalse [Value]
+  | FailError EvalError [Value]
+
+isPass :: TestResult -> Bool
+isPass Pass = True
+isPass _    = False
+
+-- | Apply a testable value to some arguments.
+-- Note that this function assumes that the values come from a call to
+-- `testableType` (i.e., things are type-correct). We run in the IO
+-- monad in order to catch any @EvalError@s.
+runOneTest :: Value -> [Value] -> IO TestResult
+runOneTest v0 vs0 = run `X.catch` handle
+  where
+    run = do
+      result <- X.evaluate (go v0 vs0)
+      if result
+        then return Pass
+        else return (FailFalse vs0)
+    handle e = return (FailError e vs0)
+
+    go :: Value -> [Value] -> Bool
+    go (VFun f) (v : vs) = go (f v) vs
+    go (VFun _) []       = panic "Not enough arguments while applying function"
+                           []
+    go (VBit b) []       = b
+    go v vs              = panic "Type error while running test" $
+                           [ "Function:"
+                           , show $ ppValue defaultPPOpts v
+                           , "Arguments:"
+                           ] ++ map (show . ppValue defaultPPOpts) vs
+
 {- | Given a (function) type, compute all possible inputs for it.
 We also return the total number of test (i.e., the length of the outer list. -}
 testableType :: Type -> Maybe (Integer, [[Value]])
@ -29,13 +68,6 @@ testableType ty =
    TCon (TC TCBit) [] -> return (1, [[]])
    _ -> Nothing

-{- | Apply a testable value to some arguments.
-    Please note that this function assumes that the values come from
-    a call to `testableType` (i.e., things are type-correct)
- -}
-runOneTest :: Value -> [Value] -> IO Eval.TestResult
-runOneTest = Eval.runOneTest
-
 {- | Given a fully-evaluated type, try to compute the number of values in it.
 Returns `Nothing` for infinite types, user-defined types, polymorhic types,
 and, currently, function spaces.  Of course, we can easily compute the
@ -95,4 +127,40 @@ typeValues ty =

    TCon _ _ -> []

+--------------------------------------------------------------------------------
+-- Driver function

+data TestSpec m s = TestSpec {
+    testFn :: Integer -> s -> m (TestResult, s)
+  , testProp :: String -- ^ The property as entered by the user
+  , testTotal :: Integer
+  , testPossible :: Integer
+  , testRptProgress :: Integer -> Integer -> m ()
+  , testClrProgress :: m ()
+  , testRptFailure :: TestResult -> m ()
+  , testRptSuccess :: m ()
+  }
+
+data TestReport = TestReport {
+    reportResult :: TestResult
+  , reportProp :: String -- ^ The property as entered by the user
+  , reportTestsRun :: Integer
+  , reportTestsPossible :: Integer
+  }
+
+runTests :: Monad m => TestSpec m s -> s -> m TestReport
+runTests TestSpec {..} st0 = go 0 st0
+  where
+  go testNum _ | testNum >= testTotal = do
+    testRptSuccess
+    return $ TestReport Pass testProp testNum testPossible
+  go testNum st =
+   do testRptProgress testNum testTotal
+      res <- testFn (div (100 * (1 + testNum)) testTotal) st
+      testClrProgress
+      case res of
+        (Pass, st') -> do -- delProgress -- unnecessary?
+          go (testNum + 1) st'
+        (failure, _st') -> do
+          testRptFailure failure
+          return $ TestReport failure testProp testNum testPossible
--- a/src/Cryptol/Testing/Eval.hs
+++ b/src/Cryptol/Testing/Eval.hs
@ -1,50 +0,0 @@
-{-# LANGUAGE TupleSections #-}
-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Evaluate test cases and handle exceptions appropriately
-
-module Cryptol.Testing.Eval where
-
-import Cryptol.Eval.Error
-import Cryptol.Eval.Value
-import Cryptol.Utils.Panic (panic)
-
-import qualified Control.Exception as X
-
-- | A test result is either a pass, a failure due to evaluating to
-- @False@, or a failure due to an exception raised during evaluation
-data TestResult
-  = Pass
-  | FailFalse [Value]
-  | FailError EvalError [Value]
-
-- | Apply a testable value to some arguments.
-- Note that this function assumes that the values come from a call to
-- `testableType` (i.e., things are type-correct). We run in the IO
-- monad in order to catch any @EvalError@s.
-runOneTest :: Value -> [Value] -> IO TestResult
-runOneTest v0 vs0 = run `X.catch` handle
-  where
-    run = do
-      result <- X.evaluate (go v0 vs0)
-      if result
-        then return Pass
-        else return (FailFalse vs0)
-    handle e = return (FailError e vs0)
-
-    go :: Value -> [Value] -> Bool
-    go (VFun f) (v : vs) = go (f v) vs
-    go (VFun _) []       = panic "Not enough arguments while applying function"
-                           []
-    go (VBit b) []       = b
-    go v vs              = panic "Type error while running test" $
-                           [ "Function:"
-                           , show $ ppValue defaultPPOpts v
-                           , "Arguments:"
-                           ] ++ map (show . ppValue defaultPPOpts) vs
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@ -12,7 +12,7 @@
 module Cryptol.Testing.Random where

 import Cryptol.Eval.Value     (BV(..),Value,GenValue(..))
-import qualified Cryptol.Testing.Eval as Eval
+import qualified Cryptol.Testing.Concrete as Conc
 import Cryptol.TypeCheck.AST  (Type(..),TCon(..),TC(..),tNoUser)
 import Cryptol.Utils.Ident    (Ident)

@ -20,7 +20,7 @@ import Control.Monad          (forM)
 import Data.List              (unfoldr, genericTake)
 import System.Random          (RandomGen, split, random, randomR)

-type Gen g = Int -> g -> (Value, g)
+type Gen g = Integer -> g -> (Value, g)


 {- | Apply a testable value to some randomly-generated arguments.
@ -33,13 +33,13 @@ type Gen g = Int -> g -> (Value, g)
 runOneTest :: RandomGen g
        => Value   -- ^ Function under test
        -> [Gen g] -- ^ Argument generators
-        -> Int     -- ^ Size
+        -> Integer -- ^ Size
        -> g
-        -> IO (Eval.TestResult, g)
+        -> IO (Conc.TestResult, g)
 runOneTest fun argGens sz g0 = do
  let (args, g1) = foldr mkArg ([], g0) argGens
      mkArg argGen (as, g) = let (a, g') = argGen sz g in (a:as, g')
-  result <- Eval.runOneTest fun args
+  result <- Conc.runOneTest fun args
  return (result, g1)

 {- | Given a (function) type, compute generators for
--- a/src/Cryptol/TypeCheck/Solve.hs
+++ b/src/Cryptol/TypeCheck/Solve.hs
@ -640,8 +640,8 @@ _testSimpGoals = Num.withSolver cfg $ \s ->
       Right _  -> debugLog s "End of test"
       Left _   -> debugLog s "Impossible"
  where
-  cfg = SolverConfig { solverPath = "cvc4"
-                     , solverArgs = [ "--lang=smt2", "--incremental", "--rewrite-divk" ]
+  cfg = SolverConfig { solverPath = "z3"
+                     , solverArgs = [ "-smt2", "-in" ]
                     , solverVerbose = 1
                     }

--- a/src/Cryptol/Utils/PP.hs
+++ b/src/Cryptol/Utils/PP.hs
@ -16,12 +16,14 @@ import           Cryptol.Utils.Ident
 import           Control.DeepSeq.Generics
 import           Control.Monad (mplus)
 import           Data.Maybe (fromMaybe)
-import qualified Data.Monoid as M
 import           Data.String (IsString(..))
 import qualified Data.Text as T
 import           GHC.Generics (Generic)
 import qualified Text.PrettyPrint as PJ

+import Prelude ()
+import Prelude.Compat
+
 -- Name Displaying -------------------------------------------------------------

 -- | How to display names, inspired by the GHC `Outputable` module. Getting a
@ -36,7 +38,7 @@ instance NFData NameDisp where rnf = genericRnf
 instance Show NameDisp where
  show _ = "<NameDisp>"

-instance M.Monoid NameDisp where
+instance Monoid NameDisp where
  mempty = EmptyNameDisp

  mappend (NameDisp f)  (NameDisp g)  = NameDisp (\m n -> f m n `mplus` g m n)
@ -70,7 +72,7 @@ fmtModName mn NotInScope     = mn
 -- | Compose two naming environments, preferring names from the left
 -- environment.
 extend :: NameDisp -> NameDisp -> NameDisp
-extend  = M.mappend
+extend  = mappend

 -- | Get the format for a name. When 'Nothing' is returned, the name is not
 -- currently in scope.
@ -91,19 +93,23 @@ fixNameDisp disp (Doc f) = Doc (\ _ -> f disp)

 newtype Doc = Doc (NameDisp -> PJ.Doc) deriving (Generic)

+instance Monoid Doc where
+  mempty = liftPJ PJ.empty
+  mappend = liftPJ2 (PJ.<>)
+
 instance NFData Doc where rnf = genericRnf

 runDoc :: NameDisp -> Doc -> PJ.Doc
 runDoc names (Doc f) = f names

 instance Show Doc where
-  show d = show (runDoc M.mempty d)
+  show d = show (runDoc mempty d)

 instance IsString Doc where
  fromString = text

 render :: Doc -> String
-render d = PJ.render (runDoc M.mempty d)
+render d = PJ.render (runDoc mempty d)

 class PP a where
  ppPrec :: Int -> a -> Doc
@ -197,12 +203,16 @@ liftPJ2 f (Doc a) (Doc b) = Doc (\e -> f (a e) (b e))
 liftSep :: ([PJ.Doc] -> PJ.Doc) -> ([Doc] -> Doc)
 liftSep f ds = Doc (\e -> f [ d e | Doc d <- ds ])

+infixl 6 <>, <+>
+
 (<>) :: Doc -> Doc -> Doc
 (<>)  = liftPJ2 (PJ.<>)

 (<+>) :: Doc -> Doc -> Doc
 (<+>)  = liftPJ2 (PJ.<+>)

+infixl 5 $$
+
 ($$) :: Doc -> Doc -> Doc
 ($$)  = liftPJ2 (PJ.$$)

--- a/tests/issues/issue066.icry.stdout
+++ b/tests/issues/issue066.icry.stdout
@ -4,9 +4,9 @@ it : {result : Bit, arg1 : [4]}

 Run-time error: no counterexample available
 True
-f 0x0 = False
+f 0xc = False
 it : {result : Bit, arg1 : [4]}
-{result = False, arg1 = 0x0}
+{result = False, arg1 = 0xc}
 False
 f 0x3 = True
 it : {result : Bit, arg1 : [4]}
@ -16,9 +16,9 @@ Unsatisfiable
 it : {result : Bit, arg1 : [4]}

 Run-time error: no satisfying assignment available
-g {x = 0x00000000, y = 0x00000001} = False
+g {x = 0xffffffff, y = 0x00000000} = False
 it : {result : Bit, arg1 : {x : [32], y : [32]}}
-{result = False, arg1 = {x = 0x00000000, y = 0x00000001}}
+{result = False, arg1 = {x = 0xffffffff, y = 0x00000000}}
 g {x = 0x00000000, y = 0x00000000} = True
 it : {result : Bit, arg1 : {x : [32], y : [32]}}
 {result = True, arg1 = {x = 0x00000000, y = 0x00000000}}
--- a/tests/issues/issue072.icry.stdout
+++ b/tests/issues/issue072.icry.stdout
@ -1,30 +1,30 @@
 Loading module Cryptol
-(\x -> x > 0x4) 0x5 = True
-it : {result : Bit, arg1 : [4]}
-{result = True, arg1 = 0x5}
-(\x -> x > 0x4) 0x5 = True
 (\x -> x > 0x4) 0x6 = True
-(\x -> x > 0x4) 0x7 = True
+it : {result : Bit, arg1 : [4]}
+{result = True, arg1 = 0x6}
+(\x -> x > 0x4) 0x6 = True
 (\x -> x > 0x4) 0x8 = True
+(\x -> x > 0x4) 0x5 = True
+(\x -> x > 0x4) 0x7 = True
+(\x -> x > 0x4) 0xd = True
+(\x -> x > 0x4) 0xc = True
 (\x -> x > 0x4) 0x9 = True
 (\x -> x > 0x4) 0xa = True
-(\x -> x > 0x4) 0xb = True
-(\x -> x > 0x4) 0xc = True
-(\x -> x > 0x4) 0xd = True
 (\x -> x > 0x4) 0xe = True
 (\x -> x > 0x4) 0xf = True
+(\x -> x > 0x4) 0xb = True
 it : [11]{result : Bit, arg1 : [4]}
-[{result = True, arg1 = 0x5}, {result = True, arg1 = 0x6},
- {result = True, arg1 = 0x7}, {result = True, arg1 = 0x8},
+[{result = True, arg1 = 0x6}, {result = True, arg1 = 0x8},
+ {result = True, arg1 = 0x5}, {result = True, arg1 = 0x7},
+ {result = True, arg1 = 0xd}, {result = True, arg1 = 0xc},
 {result = True, arg1 = 0x9}, {result = True, arg1 = 0xa},
- {result = True, arg1 = 0xb}, {result = True, arg1 = 0xc},
- {result = True, arg1 = 0xd}, {result = True, arg1 = 0xe},
- {result = True, arg1 = 0xf}]
+ {result = True, arg1 = 0xe}, {result = True, arg1 = 0xf},
+ {result = True, arg1 = 0xb}]
 must be an integer > 0 or "all"
 must be an integer > 0 or "all"
-(\x -> x > 0x4) 0x5 = True
 (\x -> x > 0x4) 0x6 = True
-(\x -> x > 0x4) 0x7 = True
+(\x -> x > 0x4) 0x8 = True
+(\x -> x > 0x4) 0x5 = True
 it : [3]{result : Bit, arg1 : [4]}
-[{result = True, arg1 = 0x5}, {result = True, arg1 = 0x6},
- {result = True, arg1 = 0x7}]
+[{result = True, arg1 = 0x6}, {result = True, arg1 = 0x8},
+ {result = True, arg1 = 0x5}]
--- a/tests/issues/issue093.icry.stdout
+++ b/tests/issues/issue093.icry.stdout
@ -2,9 +2,9 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 property f0 Using exhaustive testing.
-FAILED
+testing...FAILED
 property t0 Using exhaustive testing.
-passed 1 tests.
+testing...passed 1 tests.
 Q.E.D.
 property t1 Using random testing.
 testing...passed 100 tests.
@ -27,4 +27,4 @@ Coverage: 0.00% (100 of 2^^64 values)
 :sat t1
 	t1 0x00000000 = True
 :sat t2
-	t2 0x00000000 0x00000000 = True
+	t2 0xfffffffe 0xffffffff = True
--- a/tests/issues/issue094.icry.stdout
+++ b/tests/issues/issue094.icry.stdout
@ -3,5 +3,5 @@ Using random testing.
 testing...passed 100 tests.
 Coverage: 39.06% (100 of 256 values)
 Using exhaustive testing.
-passed 256 tests.
+testing...passed 256 tests.
 Q.E.D.
--- a/tests/issues/issue103.icry.stdout
+++ b/tests/issues/issue103.icry.stdout
@ -2,6 +2,6 @@ Loading module Cryptol

 Run-time error: undefined
 Using exhaustive testing.
-ERROR for the following inputs:
+testing...ERROR for the following inputs:
 ()
 invalid sequence index: 1
--- a/tests/issues/issue128.icry.stdout
+++ b/tests/issues/issue128.icry.stdout
@ -2,6 +2,6 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 Using exhaustive testing.
-passed 1 tests.
+testing...passed 1 tests.
 Q.E.D.
 Q.E.D.
--- a/tests/issues/issue130.icry.stdout
+++ b/tests/issues/issue130.icry.stdout
@ -2,6 +2,6 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 Using exhaustive testing.
-passed 8 tests.
+testing...passed 8 tests.
 Q.E.D.
 Q.E.D.
--- a/tests/issues/issue133.icry.stdout
+++ b/tests/issues/issue133.icry.stdout
@ -2,6 +2,6 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 Using exhaustive testing.
-passed 256 tests.
+testing...passed 256 tests.
 Q.E.D.
 Q.E.D.
--- a/tests/issues/issue212.icry.fails
+++ b/tests/issues/issue212.icry.fails
@ -0,0 +1 @@
+Known tc failure.  See issue #212.
--- a/tests/issues/issue212.icry.stdout
+++ b/tests/issues/issue212.icry.stdout
--- a/tests/issues/issue289.icry.stdout
+++ b/tests/issues/issue289.icry.stdout
@ -2,5 +2,5 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 Q.E.D.
-av1 0xc00001c9 0xbfffffd5 = False
+av1 0xfdffffe0 0x7fffffe0 = False
 Q.E.D.
--- a/tests/regression/r03.icry.stdout
+++ b/tests/regression/r03.icry.stdout
@ -1,5 +1,5 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module r03
-(nQueens : Solution 5) [0x4, 0x2, 0x0, 0x3, 0x1] = True
+(nQueens : Solution 5) [0x3, 0x1, 0x4, 0x2, 0x0] = True
 (nQueensProve : Solution 4) [0x2, 0x0, 0x3, 0x1] = False