Merge branch 'master' into wip/solver

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "external-libs/sbv"]
+	path = external-libs/sbv
+	url = https://github.com/yav/sbv.git

Makefile

@@ -91,6 +91,7 @@ msi: ${PKG}.msi
 # during initial setup, you have to invoke this target again manually
 ${CS}:
 	$(CABAL) sandbox init
+	$(CABAL) sandbox add-source external-libs/sbv
 
 ${CS_BIN}/alex: | ${CS}
 	$(CABAL_INSTALL) alex

cryptol.cabal

@@ -61,7 +61,7 @@ library
                        process           >= 1.2,
                        QuickCheck        >= 2.7,
                        random            >= 1.0.1,
-                       sbv               >= 5.12,
+                       sbv               >= 5.15,
                        smtLib            >= 1.0.7,
                        simple-smt        >= 0.6.0,
                        syb               >= 0.4,

src/Cryptol/REPL/Command.hs

@@ -73,7 +73,7 @@ import Cryptol.Utils.PP
 import Cryptol.Utils.Panic(panic)
 import qualified Cryptol.Parser.AST as P
 import qualified Cryptol.Transform.Specialize as S
-import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..))
+import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..),ProverStats)
 import qualified Cryptol.Symbolic as Symbolic
 
 import qualified Control.Exception as X
@@ -98,10 +98,13 @@ import System.Random.TF(newTFGen)
 import Numeric (showFFloat)
 import qualified Data.Text as ST
 import qualified Data.Text.Lazy as T
+import Data.IORef(newIORef,readIORef)
 
 import Prelude ()
 import Prelude.Compat
 
+import Data.SBV(TimedStep(..),showTDiff)
+
 -- Commands --------------------------------------------------------------------
 
 -- | Commands.
@@ -390,6 +393,20 @@ satCmd, proveCmd :: String -> REPL ()
 satCmd = cmdProveSat True
 proveCmd = cmdProveSat False
 
+showProverStats :: ProverStats -> REPL ()
+showProverStats = rPutStrLn
+                . ('\n':) . parns
+                . intercalate ", " . map sh . Map.toList
+  where
+  lab ProblemConstruction = "simulation"
+  lab Translation         = "export"
+  lab (WorkByProver x)    = x
+
+  sh (x, y) = lab x ++ ":" ++ showTDiff y
+
+  parns x = '(' : x ++ ")"
+
+
 -- | Console-specific version of 'proveSat'. Prints output to the
 -- console, and binds the @it@ variable to a record whose form depends
 -- on the expression given. See ticket #66 for a discussion of this
@@ -430,7 +447,7 @@ cmdProveSat isSat str = do
             Just path -> io $ writeFile path smtlib
             Nothing -> rPutStr smtlib
     _ -> do
-      result <- onlineProveSat isSat str mfile
+      (result,stats) <- onlineProveSat isSat str mfile
       ppOpts <- getPPValOpts
       case result of
         Symbolic.EmptyResult         ->
@@ -468,9 +485,10 @@ cmdProveSat isSat str = do
           case (ty, exprs) of
             (t, [e]) -> bindItVariable t e
             (t, es ) -> bindItVariables t es
+      showProverStats stats
 
 onlineProveSat :: Bool
-               -> String -> Maybe FilePath -> REPL Symbolic.ProverResult
+               -> String -> Maybe FilePath -> REPL (Symbolic.ProverResult,ProverStats)
 onlineProveSat isSat str mfile = do
   EnvString proverName <- getUser "prover"
   EnvBool verbose <- getUser "debug"
@@ -478,16 +496,20 @@ onlineProveSat isSat str mfile = do
   parseExpr <- replParseExpr str
   (_, expr, schema) <- replCheckExpr parseExpr
   decls <- fmap M.deDecls getDynEnv
+  timing <- io (newIORef Map.empty)
   let cmd = Symbolic.ProverCommand {
           pcQueryType    = if isSat then SatQuery satNum else ProveQuery
         , pcProverName   = proverName
         , pcVerbose      = verbose
+        , pcProverStats  = timing
         , pcExtraDecls   = decls
         , pcSmtFile      = mfile
         , pcExpr         = expr
         , pcSchema       = schema
         }
-  liftModuleCmd $ Symbolic.satProve cmd
+  res <- liftModuleCmd $ Symbolic.satProve cmd
+  stas <- io (readIORef timing)
+  return (res,stas)
 
 offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
 offlineProveSat isSat str mfile = do
@@ -495,10 +517,12 @@ offlineProveSat isSat str mfile = do
   parseExpr <- replParseExpr str
   (_, expr, schema) <- replCheckExpr parseExpr
   decls <- fmap M.deDecls getDynEnv
+  timing <- io (newIORef Map.empty)
   let cmd = Symbolic.ProverCommand {
           pcQueryType    = if isSat then SatQuery (SomeSat 0) else ProveQuery
         , pcProverName   = "offline"
         , pcVerbose      = verbose
+        , pcProverStats  = timing
         , pcExtraDecls   = decls
         , pcSmtFile      = mfile
         , pcExpr         = expr

src/Cryptol/Symbolic.hs

@@ -19,9 +19,11 @@ module Cryptol.Symbolic where
 import Control.Monad.IO.Class
 import Control.Monad (replicateM, when, zipWithM, foldM)
 import Data.List (intercalate, genericLength)
+import Data.IORef(IORef)
 import qualified Control.Exception as X
 
 import qualified Data.SBV.Dynamic as SBV
+import           Data.SBV (Timing(SaveTiming),TimingInfo)
 
 import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
 import qualified Cryptol.ModuleSystem.Env as M
@@ -86,6 +88,8 @@ data ProverCommand = ProverCommand {
     -- ^ Which prover to use (one of the strings in 'proverConfigs')
   , pcVerbose :: Bool
     -- ^ Verbosity flag passed to SBV
+  , pcProverStats :: !(IORef ProverStats)
+    -- ^ Record timing information here
   , pcExtraDecls :: [DeclGroup]
     -- ^ Extra declarations to bring into scope for symbolic
     -- simulation
@@ -97,6 +101,8 @@ data ProverCommand = ProverCommand {
     -- ^ The 'Schema' of @pcExpr@
   }
 
+type ProverStats = TimingInfo
+
 -- | A prover result is either an error message, an empty result (eg
 -- for the offline prover), a counterexample or a lazy list of
 -- satisfying assignments.
@@ -117,9 +123,9 @@ thmSMTResults (SBV.ThmResult r) = [r]
 proverError :: String -> M.ModuleCmd ProverResult
 proverError msg modEnv = return (Right (ProverError msg, modEnv), [])
 
-
 satProve :: ProverCommand -> M.ModuleCmd ProverResult
-satProve ProverCommand {..} = protectStack proverError $ \modEnv ->
+satProve ProverCommand {..} =
+  protectStack proverError $ \modEnv ->
   M.runModuleM modEnv $ do
   let (isSat, mSatNum) = case pcQueryType of
         ProveQuery -> (False, Nothing)
@@ -131,7 +137,9 @@ satProve ProverCommand {..} = protectStack proverError $ \modEnv ->
     case pcProverName of
       "any" -> M.io SBV.sbvAvailableSolvers
       _ -> return [(lookupProver pcProverName) { SBV.smtFile = pcSmtFile }]
-  let provers' = [ p { SBV.timing = pcVerbose, SBV.verbose = pcVerbose } | p <- provers ]
+
+
+  let provers' = [ p { SBV.timing = SaveTiming pcProverStats, SBV.verbose = pcVerbose } | p <- provers ]
   let tyFn = if isSat then existsFinType else forallFinType
   let runProver fn tag e = do
         case provers of