From 8dafb86dc6d63b4b5d55ae047a5ac0d2b450d293 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 10:44:59 -0700
Subject: [PATCH 01/16] Add :time command

---
 cryptol.cabal                    |  6 ++-
 src/Cryptol/Benchmark.hs         | 28 +++++++++++
 src/Cryptol/ModuleSystem.hs      |  5 ++
 src/Cryptol/ModuleSystem/Base.hs | 17 +++++++
 src/Cryptol/REPL/Command.hs      | 81 +++++++++++++++++++++-----------
 5 files changed, 108 insertions(+), 29 deletions(-)
 create mode 100644 src/Cryptol/Benchmark.hs

diff --git a/cryptol.cabal b/cryptol.cabal
index c191941ff..fa2a4e040 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -52,6 +52,7 @@ library
                        bytestring        >= 0.10,
                        array             >= 0.4,
                        containers        >= 0.5,
+                       criterion-measurement,
                        cryptohash-sha1   >= 0.11 && < 0.12,
                        deepseq           >= 1.3,
                        directory         >= 1.2.2.0,
@@ -75,6 +76,7 @@ library
                        text              >= 1.1,
                        tf-random         >= 0.5,
                        transformers-base >= 0.4,
+                       vector,
                        mtl               >= 2.2.1,
                        time              >= 1.6.0.1,
                        panic             >= 0.3,
@@ -216,7 +218,9 @@ library
                        Cryptol.REPL.Command,
                        Cryptol.REPL.Browse,
                        Cryptol.REPL.Monad,
-                       Cryptol.REPL.Trie
+                       Cryptol.REPL.Trie,
+
+                       Cryptol.Benchmark
 
   Other-modules:       Cryptol.Parser.LexerUtils,
                        Cryptol.Parser.ParserUtils,
diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs
new file mode 100644
index 000000000..b24f7170a
--- /dev/null
+++ b/src/Cryptol/Benchmark.hs
@@ -0,0 +1,28 @@
+module Cryptol.Benchmark
+  ( BenchmarkStats (..)
+  , benchmark
+  , secs
+  ) where
+
+import           Criterion.Measurement       (runBenchmark, secs, threshold)
+import           Criterion.Measurement.Types
+import           Data.Int
+import qualified Data.Vector                 as V
+import qualified Data.Vector.Unboxed         as U
+
+data BenchmarkStats = BenchmarkStats
+  { benchAvgTime    :: !Double
+  , benchAvgCpuTime :: !Double
+  , benchAvgCycles  :: !Int64
+  }
+
+benchmark :: (a -> IO b) -> a -> IO BenchmarkStats
+benchmark f x = do
+  (meas, _) <- runBenchmark (whnfAppIO f x) 10
+  let len = length meas
+      meas' = rescale <$> V.filter ((>= threshold) . measTime) meas
+      sumMeasure sel = U.sum $ measure sel meas'
+  pure BenchmarkStats
+    { benchAvgTime = sumMeasure measTime / fromIntegral len
+    , benchAvgCpuTime = sumMeasure measCpuTime / fromIntegral len
+    , benchAvgCycles = sumMeasure measCycles `div` fromIntegral len }
diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
index 10f9062cb..a7450ee8f 100644
--- a/src/Cryptol/ModuleSystem.hs
+++ b/src/Cryptol/ModuleSystem.hs
@@ -20,6 +20,7 @@ module Cryptol.ModuleSystem (
   , loadModuleByName
   , checkExpr
   , evalExpr
+  , benchmarkExpr
   , checkDecls
   , evalDecls
   , noPat
@@ -35,6 +36,7 @@ module Cryptol.ModuleSystem (
 
 import Data.Map (Map)
 
+import           Cryptol.Benchmark (BenchmarkStats)
 import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.ModuleSystem.Env
 import           Cryptol.ModuleSystem.Interface
@@ -97,6 +99,9 @@ checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
 evalExpr :: T.Expr -> ModuleCmd Concrete.Value
 evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
 
+benchmarkExpr :: T.Expr -> ModuleCmd BenchmarkStats
+benchmarkExpr e env = runModuleM env (interactive (Base.benchmarkExpr e))
+
 -- | Typecheck top-level declarations.
 checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn)
 checkDecls ds env = runModuleM env
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index 7113a488c..83a48d08a 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -51,6 +51,7 @@ import Cryptol.ModuleSystem.Env (lookupModule
                                 , ModContext(..)
                                 , ModulePath(..), modulePathLabel)
 import           Cryptol.Backend.FFI
+import           Cryptol.Benchmark
 import qualified Cryptol.Eval                 as E
 import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.Eval.Concrete (Concrete(..))
@@ -611,6 +612,22 @@ evalExpr e = do
 
   io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e)
 
+benchmarkExpr :: T.Expr -> ModuleM BenchmarkStats
+benchmarkExpr e = do
+  env <- getEvalEnv
+  denv <- getDynEnv
+  evopts <- getEvalOptsAction
+  let env' = env <> deEnv denv
+  let tbl = Concrete.primTable evopts
+  let ?evalPrim = \i -> Right <$> Map.lookup i tbl
+  let ?range = emptyRange
+  callStacks <- getCallStacks
+  let ?callStacks = callStacks
+
+  let eval expr = E.runEval mempty $
+        E.evalExpr Concrete env' expr >>= E.forceValue
+  io $ benchmark eval e
+
 evalDecls :: [T.DeclGroup] -> ModuleM ()
 evalDecls dgs = do
   env <- getEvalEnv
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 0f5404faa..e522ba68b 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -70,6 +70,7 @@ import qualified Cryptol.ModuleSystem.Env as M
 
 import qualified Cryptol.Backend.Monad as E
 import qualified Cryptol.Backend.SeqMap as E
+import qualified Cryptol.Benchmark as Bench
 import           Cryptol.Eval.Concrete( Concrete(..) )
 import qualified Cryptol.Eval.Concrete as Concrete
 import qualified Cryptol.Eval.Env as E
@@ -252,6 +253,9 @@ nbCommandList  =
   , CommandDescr [ ":extract-coq" ] [] (NoArg allTerms)
     "Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format."
     ""
+  , CommandDescr [ ":time" ] ["EXPR"] (ExprArg timeCmd)
+    "Measure the time it takes to evaluate the given expression."
+    ""
   ]
 
 commandList :: [CommandDescr]
@@ -999,6 +1003,19 @@ typeOfCmd str pos fnm = do
   rPrint $ runDoc fDisp $ group $ hang
     (ppPrec 2 expr <+> text ":") 2 (pp sig)
 
+timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
+timeCmd str pos fnm = do
+  pExpr <- replParseExpr str pos fnm
+  (_, def, sig) <- replCheckExpr pExpr
+  replPrepareCheckedExpr def sig >>= \case
+    Nothing -> raise (EvalPolyError sig)
+    Just (_, expr) -> do
+      Bench.BenchmarkStats {..} <-
+        liftModuleCmd (rethrowEvalError . M.benchmarkExpr expr)
+      rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime
+               ++ "\tAvg CPU time: " ++ Bench.secs benchAvgCpuTime
+               ++ "\tAvg cycles: " ++ show benchAvgCycles
+
 readFileCmd :: FilePath -> REPL ()
 readFileCmd fp = do
   bytes <- replReadFile fp (\err -> rPutStrLn (show err) >> return Nothing)
@@ -1569,39 +1586,47 @@ replSpecExpr e = liftModuleCmd $ S.specialize e
 replEvalExpr :: P.Expr P.PName -> REPL (Concrete.Value, T.Type)
 replEvalExpr expr =
   do (_,def,sig) <- replCheckExpr expr
-     replEvalCheckedExpr def sig >>= \mb_res -> case mb_res of
+     replEvalCheckedExpr def sig >>= \case
        Just res -> pure res
        Nothing -> raise (EvalPolyError sig)
 
 replEvalCheckedExpr :: T.Expr -> T.Schema -> REPL (Maybe (Concrete.Value, T.Type))
 replEvalCheckedExpr def sig =
-  do validEvalContext def
-     validEvalContext sig
-
-     s <- getTCSolver
-     mbDef <- io (defaultReplExpr s def sig)
-
-     case mbDef of
-       Nothing -> pure Nothing
-       Just (tys, def1) ->
-           do warnDefaults tys
-              let su = T.listParamSubst tys
-              let ty = T.apSubst su (T.sType sig)
-              whenDebug (rPutStrLn (dump def1))
-
-              tenv <- E.envTypes . M.deEnv <$> getDynEnv
-              let tyv = E.evalValType tenv ty
-
-              -- add "it" to the namespace via a new declaration
-              itVar <- bindItVariable tyv def1
-
-              let itExpr = case getLoc def of
-                              Nothing  -> T.EVar itVar
-                              Just rng -> T.ELocated rng (T.EVar itVar)
-
-              -- evaluate the it variable
-              val <- liftModuleCmd (rethrowEvalError . M.evalExpr itExpr)
-              return $ Just (val,ty)
+  replPrepareCheckedExpr def sig >>=
+    traverse \(tys, def1) -> do
+      let su = T.listParamSubst tys
+      let ty = T.apSubst su (T.sType sig)
+      whenDebug (rPutStrLn (dump def1))
+
+      tenv <- E.envTypes . M.deEnv <$> getDynEnv
+      let tyv = E.evalValType tenv ty
+
+      -- add "it" to the namespace via a new declaration
+      itVar <- bindItVariable tyv def1
+
+      let itExpr = case getLoc def of
+                      Nothing  -> T.EVar itVar
+                      Just rng -> T.ELocated rng (T.EVar itVar)
+
+      -- evaluate the it variable
+      val <- liftModuleCmd (rethrowEvalError . M.evalExpr itExpr)
+      return (val,ty)
+
+-- | Check that we are in a valid evaluation context and apply defaulting.
+replPrepareCheckedExpr :: T.Expr -> T.Schema ->
+  REPL (Maybe ([(T.TParam, T.Type)], T.Expr))
+replPrepareCheckedExpr def sig = do
+  validEvalContext def
+  validEvalContext sig
+
+  s <- getTCSolver
+  mbDef <- io (defaultReplExpr s def sig)
+
+  case mbDef of
+    Nothing -> pure Nothing
+    Just (tys, def1) -> do
+      warnDefaults tys
+      pure $ Just (tys, def1)
   where
   warnDefaults ts =
     case ts of

From c1ede357cb0eadaaec280172972b2f97d9b376ad Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 11:43:21 -0700
Subject: [PATCH 02/16] benchmark: BenchmarkStats deriving Show

---
 src/Cryptol/Benchmark.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs
index b24f7170a..51988dbce 100644
--- a/src/Cryptol/Benchmark.hs
+++ b/src/Cryptol/Benchmark.hs
@@ -14,7 +14,7 @@ data BenchmarkStats = BenchmarkStats
   { benchAvgTime    :: !Double
   , benchAvgCpuTime :: !Double
   , benchAvgCycles  :: !Int64
-  }
+  } deriving Show
 
 benchmark :: (a -> IO b) -> a -> IO BenchmarkStats
 benchmark f x = do

From c98882969389255ad809aed172b151ef4cbef583 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 11:47:04 -0700
Subject: [PATCH 03/16] time command: Improve output formatting

---
 src/Cryptol/REPL/Command.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index e522ba68b..45879d990 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -1013,8 +1013,8 @@ timeCmd str pos fnm = do
       Bench.BenchmarkStats {..} <-
         liftModuleCmd (rethrowEvalError . M.benchmarkExpr expr)
       rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime
-               ++ "\tAvg CPU time: " ++ Bench.secs benchAvgCpuTime
-               ++ "\tAvg cycles: " ++ show benchAvgCycles
+           ++ "    Avg CPU time: " ++ Bench.secs benchAvgCpuTime
+           ++ "    Avg cycles: " ++ show benchAvgCycles
 
 readFileCmd :: FilePath -> REPL ()
 readFileCmd fp = do

From 7ee80344c3fdc248dc857725b58e354561844dbe Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 15:15:12 -0700
Subject: [PATCH 04/16] time command: Make measurement period configurable

---
 src/Cryptol/Benchmark.hs         |  6 +++---
 src/Cryptol/ModuleSystem.hs      |  5 +++--
 src/Cryptol/ModuleSystem/Base.hs |  6 +++---
 src/Cryptol/REPL/Command.hs      |  5 +++--
 src/Cryptol/REPL/Monad.hs        | 17 +++++++++++++++++
 5 files changed, 29 insertions(+), 10 deletions(-)

diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs
index 51988dbce..a3a51964f 100644
--- a/src/Cryptol/Benchmark.hs
+++ b/src/Cryptol/Benchmark.hs
@@ -16,9 +16,9 @@ data BenchmarkStats = BenchmarkStats
   , benchAvgCycles  :: !Int64
   } deriving Show
 
-benchmark :: (a -> IO b) -> a -> IO BenchmarkStats
-benchmark f x = do
-  (meas, _) <- runBenchmark (whnfAppIO f x) 10
+benchmark :: Double -> (a -> IO b) -> a -> IO BenchmarkStats
+benchmark period f x = do
+  (meas, _) <- runBenchmark (whnfAppIO f x) period
   let len = length meas
       meas' = rescale <$> V.filter ((>= threshold) . measTime) meas
       sumMeasure sel = U.sum $ measure sel meas'
diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
index a7450ee8f..17c19576d 100644
--- a/src/Cryptol/ModuleSystem.hs
+++ b/src/Cryptol/ModuleSystem.hs
@@ -99,8 +99,9 @@ checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
 evalExpr :: T.Expr -> ModuleCmd Concrete.Value
 evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
 
-benchmarkExpr :: T.Expr -> ModuleCmd BenchmarkStats
-benchmarkExpr e env = runModuleM env (interactive (Base.benchmarkExpr e))
+benchmarkExpr :: Double -> T.Expr -> ModuleCmd BenchmarkStats
+benchmarkExpr period e env =
+  runModuleM env (interactive (Base.benchmarkExpr period e))
 
 -- | Typecheck top-level declarations.
 checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn)
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index 83a48d08a..570361db1 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -612,8 +612,8 @@ evalExpr e = do
 
   io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e)
 
-benchmarkExpr :: T.Expr -> ModuleM BenchmarkStats
-benchmarkExpr e = do
+benchmarkExpr :: Double -> T.Expr -> ModuleM BenchmarkStats
+benchmarkExpr period e = do
   env <- getEvalEnv
   denv <- getDynEnv
   evopts <- getEvalOptsAction
@@ -626,7 +626,7 @@ benchmarkExpr e = do
 
   let eval expr = E.runEval mempty $
         E.evalExpr Concrete env' expr >>= E.forceValue
-  io $ benchmark eval e
+  io $ benchmark period eval e
 
 evalDecls :: [T.DeclGroup] -> ModuleM ()
 evalDecls dgs = do
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 45879d990..b9ecf49b1 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -1005,13 +1005,14 @@ typeOfCmd str pos fnm = do
 
 timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
 timeCmd str pos fnm = do
+  period <- getKnownUser "timeMeasurementPeriod" :: REPL Int
   pExpr <- replParseExpr str pos fnm
   (_, def, sig) <- replCheckExpr pExpr
   replPrepareCheckedExpr def sig >>= \case
     Nothing -> raise (EvalPolyError sig)
     Just (_, expr) -> do
-      Bench.BenchmarkStats {..} <-
-        liftModuleCmd (rethrowEvalError . M.benchmarkExpr expr)
+      Bench.BenchmarkStats {..} <- liftModuleCmd
+        (rethrowEvalError . M.benchmarkExpr (fromIntegral period) expr)
       rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime
            ++ "    Avg CPU time: " ++ Bench.secs benchAvgCpuTime
            ++ "    Avg cycles: " ++ show benchAvgCycles
diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
index f77cc6d70..062693d1f 100644
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -983,6 +983,15 @@ userOptions  = mkOptionMap
     , "  * display      try to match the order they were written in the source code"
     , "  * canonical    use a predictable, canonical order"
     ]
+
+  , simpleOpt "timeMeasurementPeriod" ["time-measurement-period"] (EnvNum 10)
+    checkTimeMeasurementPeriod
+    $ unlines
+    [ "The period of time in seconds to spend collecting measurements when"
+    , "  running :time."
+    , "This is a lower bound and the actual time taken might be higher if the"
+    , "  evaluation takes a long time."
+    ]
   ]
 
 
@@ -1078,6 +1087,14 @@ getUserSatNum = do
     _                         -> panic "REPL.Monad.getUserSatNum"
                                    [ "invalid satNum option" ]
 
+checkTimeMeasurementPeriod :: Checker
+checkTimeMeasurementPeriod (EnvNum n)
+  | n >= 1 = noWarns Nothing
+  | otherwise = noWarns $
+    Just "timeMeasurementPeriod must be a positive integer"
+checkTimeMeasurementPeriod _ = noWarns $
+  Just "unable to parse value for timeMeasurementPeriod"
+
 -- Environment Utilities -------------------------------------------------------
 
 whenDebug :: REPL () -> REPL ()

From 1c8ff60dc9a209111d4adf5428166c1d929900f5 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 15:22:57 -0700
Subject: [PATCH 05/16] time command: Fix average calculation

---
 src/Cryptol/Benchmark.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs
index a3a51964f..ef2b8efcd 100644
--- a/src/Cryptol/Benchmark.hs
+++ b/src/Cryptol/Benchmark.hs
@@ -19,8 +19,8 @@ data BenchmarkStats = BenchmarkStats
 benchmark :: Double -> (a -> IO b) -> a -> IO BenchmarkStats
 benchmark period f x = do
   (meas, _) <- runBenchmark (whnfAppIO f x) period
-  let len = length meas
-      meas' = rescale <$> V.filter ((>= threshold) . measTime) meas
+  let meas' = rescale <$> V.filter ((>= threshold) . measTime) meas
+      len = length meas'
       sumMeasure sel = U.sum $ measure sel meas'
   pure BenchmarkStats
     { benchAvgTime = sumMeasure measTime / fromIntegral len

From 0d53c059ec177f78b36debafa8ec8c8e9ade31c2 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 22:04:14 -0700
Subject: [PATCH 06/16] time command: Improve command description

---
 src/Cryptol/REPL/Command.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index b9ecf49b1..72cc463bf 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -255,7 +255,10 @@ nbCommandList  =
     ""
   , CommandDescr [ ":time" ] ["EXPR"] (ExprArg timeCmd)
     "Measure the time it takes to evaluate the given expression."
-    ""
+    (unlines
+      [ "The expression will be evaluated many times to get accurate results."
+      , "The amount of time to spend collecting measurements can be changed"
+      , "  with the timeMeasurementPeriod option." ])
   ]
 
 commandList :: [CommandDescr]

From 25d34678901a37b050aafb1a1ff0687dd46a5ed4 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 22:07:46 -0700
Subject: [PATCH 07/16] time command: Print measurement period

---
 src/Cryptol/REPL/Command.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 72cc463bf..1e4497c1e 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -1009,6 +1009,7 @@ typeOfCmd str pos fnm = do
 timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
 timeCmd str pos fnm = do
   period <- getKnownUser "timeMeasurementPeriod" :: REPL Int
+  rPutStrLn $ "Measuring for " ++ show period ++ " seconds"
   pExpr <- replParseExpr str pos fnm
   (_, def, sig) <- replCheckExpr pExpr
   replPrepareCheckedExpr def sig >>= \case

From 4af4f6d7bb599b58cc6bb3e9de0b90da7ba73d13 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 22:39:42 -0700
Subject: [PATCH 08/16] time command: Document command output

---
 src/Cryptol/REPL/Command.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 1e4497c1e..b75d0f639 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -258,7 +258,9 @@ nbCommandList  =
     (unlines
       [ "The expression will be evaluated many times to get accurate results."
       , "The amount of time to spend collecting measurements can be changed"
-      , "  with the timeMeasurementPeriod option." ])
+      , "  with the timeMeasurementPeriod option."
+      , "Reports the average wall clock time, CPU time, and cycles."
+      , "(Cycles are in unspecified units that may be CPU cycles.)"])
   ]
 
 commandList :: [CommandDescr]

From cde5f18dafabfa88405e6c4760fa9d4086f0a37c Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 22:49:52 -0700
Subject: [PATCH 09/16] time command: Add comments

---
 src/Cryptol/Benchmark.hs    | 8 ++++++++
 src/Cryptol/ModuleSystem.hs | 1 +
 2 files changed, 9 insertions(+)

diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Benchmark.hs
index ef2b8efcd..c4ef18b4b 100644
--- a/src/Cryptol/Benchmark.hs
+++ b/src/Cryptol/Benchmark.hs
@@ -1,3 +1,4 @@
+-- | Simple benchmarking of IO functions.
 module Cryptol.Benchmark
   ( BenchmarkStats (..)
   , benchmark
@@ -10,12 +11,19 @@ import           Data.Int
 import qualified Data.Vector                 as V
 import qualified Data.Vector.Unboxed         as U
 
+-- | Statistics returned by 'benchmark'.
+--
+-- This is extremely crude compared to the full analysis that criterion can do,
+-- but is enough for now.
 data BenchmarkStats = BenchmarkStats
   { benchAvgTime    :: !Double
   , benchAvgCpuTime :: !Double
   , benchAvgCycles  :: !Int64
   } deriving Show
 
+-- | Benchmark the application of the given function to the given input and the
+-- execution of the resulting IO action to WHNF, spending at least the given
+-- amount of time in seconds to collect measurements.
 benchmark :: Double -> (a -> IO b) -> a -> IO BenchmarkStats
 benchmark period f x = do
   (meas, _) <- runBenchmark (whnfAppIO f x) period
diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
index 17c19576d..066319b03 100644
--- a/src/Cryptol/ModuleSystem.hs
+++ b/src/Cryptol/ModuleSystem.hs
@@ -99,6 +99,7 @@ checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
 evalExpr :: T.Expr -> ModuleCmd Concrete.Value
 evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
 
+-- | Benchmark an expression.
 benchmarkExpr :: Double -> T.Expr -> ModuleCmd BenchmarkStats
 benchmarkExpr period e env =
   runModuleM env (interactive (Base.benchmarkExpr period e))

From e4b46117112014b65e7ba659b6594fa766577c2f Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 22:56:04 -0700
Subject: [PATCH 10/16] Move Benchmark module to Cryptol.Utils

---
 cryptol.cabal                        | 5 ++---
 src/Cryptol/ModuleSystem.hs          | 2 +-
 src/Cryptol/ModuleSystem/Base.hs     | 2 +-
 src/Cryptol/REPL/Command.hs          | 2 +-
 src/Cryptol/{ => Utils}/Benchmark.hs | 2 +-
 5 files changed, 6 insertions(+), 7 deletions(-)
 rename src/Cryptol/{ => Utils}/Benchmark.hs (97%)

diff --git a/cryptol.cabal b/cryptol.cabal
index fa2a4e040..96f2f3c19 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -118,6 +118,7 @@ library
                        Cryptol.Utils.Misc,
                        Cryptol.Utils.Patterns,
                        Cryptol.Utils.Logger,
+                       Cryptol.Utils.Benchmark,
                        Cryptol.Version,
 
                        Cryptol.ModuleSystem,
@@ -218,9 +219,7 @@ library
                        Cryptol.REPL.Command,
                        Cryptol.REPL.Browse,
                        Cryptol.REPL.Monad,
-                       Cryptol.REPL.Trie,
-
-                       Cryptol.Benchmark
+                       Cryptol.REPL.Trie
 
   Other-modules:       Cryptol.Parser.LexerUtils,
                        Cryptol.Parser.ParserUtils,
diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
index 066319b03..cbb3548ba 100644
--- a/src/Cryptol/ModuleSystem.hs
+++ b/src/Cryptol/ModuleSystem.hs
@@ -36,7 +36,6 @@ module Cryptol.ModuleSystem (
 
 import Data.Map (Map)
 
-import           Cryptol.Benchmark (BenchmarkStats)
 import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.ModuleSystem.Env
 import           Cryptol.ModuleSystem.Interface
@@ -49,6 +48,7 @@ import           Cryptol.Parser.Name (PName)
 import           Cryptol.Parser.NoPat (RemovePatterns)
 import qualified Cryptol.TypeCheck.AST     as T
 import qualified Cryptol.TypeCheck.Interface as T
+import           Cryptol.Utils.Benchmark (BenchmarkStats)
 import qualified Cryptol.Utils.Ident as M
 
 -- Public Interface ------------------------------------------------------------
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index 570361db1..d26938131 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -51,7 +51,6 @@ import Cryptol.ModuleSystem.Env (lookupModule
                                 , ModContext(..)
                                 , ModulePath(..), modulePathLabel)
 import           Cryptol.Backend.FFI
-import           Cryptol.Benchmark
 import qualified Cryptol.Eval                 as E
 import qualified Cryptol.Eval.Concrete as Concrete
 import           Cryptol.Eval.Concrete (Concrete(..))
@@ -76,6 +75,7 @@ import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, prim
 import Cryptol.Utils.PP (pretty)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Logger(logPutStrLn, logPrint)
+import Cryptol.Utils.Benchmark
 
 import Cryptol.Prelude ( preludeContents, floatContents, arrayContents
                        , suiteBContents, primeECContents, preludeReferenceContents )
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index b75d0f639..ca6a1e070 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -70,7 +70,6 @@ import qualified Cryptol.ModuleSystem.Env as M
 
 import qualified Cryptol.Backend.Monad as E
 import qualified Cryptol.Backend.SeqMap as E
-import qualified Cryptol.Benchmark as Bench
 import           Cryptol.Eval.Concrete( Concrete(..) )
 import qualified Cryptol.Eval.Concrete as Concrete
 import qualified Cryptol.Eval.Env as E
@@ -89,6 +88,7 @@ import qualified Cryptol.TypeCheck.Parseable as T
 import qualified Cryptol.TypeCheck.Subst as T
 import           Cryptol.TypeCheck.Solve(defaultReplExpr)
 import           Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap)
+import qualified Cryptol.Utils.Benchmark as Bench
 import           Cryptol.Utils.PP hiding ((</>))
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.RecordMap
diff --git a/src/Cryptol/Benchmark.hs b/src/Cryptol/Utils/Benchmark.hs
similarity index 97%
rename from src/Cryptol/Benchmark.hs
rename to src/Cryptol/Utils/Benchmark.hs
index c4ef18b4b..17bc4a31d 100644
--- a/src/Cryptol/Benchmark.hs
+++ b/src/Cryptol/Utils/Benchmark.hs
@@ -1,5 +1,5 @@
 -- | Simple benchmarking of IO functions.
-module Cryptol.Benchmark
+module Cryptol.Utils.Benchmark
   ( BenchmarkStats (..)
   , benchmark
   , secs

From 130ae18573b47f303c1af1ba49623bfec2a31a97 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Mon, 29 Aug 2022 23:05:58 -0700
Subject: [PATCH 11/16] Add :time to CHANGES.md

---
 CHANGES.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 8207c3258..893da25fb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -5,6 +5,10 @@
 * Fix a bug in the What4 backend that could cause applications of `(@)` with
   symbolic `Integer` indices to become out of bounds (#1359).
 
+## New features
+
+* Add a `:time` command to benchmark the evaluation time of expressions.
+
 # 2.13.0
 
 ## Language changes

From 09cf06a8e819c2ee49110e18f640203fb9d98a81 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Tue, 30 Aug 2022 14:24:47 -0700
Subject: [PATCH 12/16] time command: bind result to it

---
 cryptol.cabal                       |  1 +
 src/Cryptol/Backend/FloatHelpers.hs |  6 ++++++
 src/Cryptol/Eval/Type.hs            |  5 +++++
 src/Cryptol/REPL/Command.hs         | 15 ++++++++++++++-
 src/Cryptol/TypeCheck/FFI.hs        |  5 +++--
 5 files changed, 29 insertions(+), 3 deletions(-)

diff --git a/cryptol.cabal b/cryptol.cabal
index 96f2f3c19..2ddcdff21 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -119,6 +119,7 @@ library
                        Cryptol.Utils.Patterns,
                        Cryptol.Utils.Logger,
                        Cryptol.Utils.Benchmark,
+                       Cryptol.Utils.Types,
                        Cryptol.Version,
 
                        Cryptol.ModuleSystem,
diff --git a/src/Cryptol/Backend/FloatHelpers.hs b/src/Cryptol/Backend/FloatHelpers.hs
index 4aa93d0fd..7c9924cf5 100644
--- a/src/Cryptol/Backend/FloatHelpers.hs
+++ b/src/Cryptol/Backend/FloatHelpers.hs
@@ -8,6 +8,7 @@ import LibBF
 
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic(panic)
+import Cryptol.Utils.Types
 import Cryptol.Backend.Monad( EvalError(..) )
 
 
@@ -176,3 +177,8 @@ floatFromBits e p bv = BF { bfValue = bfFromBits (fpOpts e p NearEven) bv
 -- (most significant bit in the significand is set, the rest of it is 0)
 floatToBits :: Integer -> Integer -> BigFloat -> Integer
 floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf
+
+
+-- | Create a 64-bit IEEE-754 float.
+floatFromDouble :: Double -> BF
+floatFromDouble = uncurry BF float64ExpPrec . bfFromDouble
diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs
index ced6e1c9d..3b7e19aa1 100644
--- a/src/Cryptol/Eval/Type.hs
+++ b/src/Cryptol/Eval/Type.hs
@@ -18,6 +18,7 @@ import Cryptol.TypeCheck.Solver.InfNat
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Ident (Ident)
 import Cryptol.Utils.RecordMap
+import Cryptol.Utils.Types
 
 import Data.Maybe(fromMaybe)
 import qualified Data.IntMap.Strict as IntMap
@@ -86,6 +87,10 @@ tvSeq :: Nat' -> TValue -> TValue
 tvSeq (Nat n) t = TVSeq n t
 tvSeq Inf     t = TVStream t
 
+-- | The Cryptol @Float64@ type.
+tvFloat64 :: TValue
+tvFloat64 = uncurry TVFloat float64ExpPrec
+
 -- | Coerce an extended natural into an integer,
 --   for values known to be finite
 finNat' :: Nat' -> Integer
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index ca6a1e070..a3f4accb3 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -68,6 +68,7 @@ import qualified Cryptol.ModuleSystem.Renamer as M
 import qualified Cryptol.Utils.Ident as M
 import qualified Cryptol.ModuleSystem.Env as M
 
+import           Cryptol.Backend.FloatHelpers as FP
 import qualified Cryptol.Backend.Monad as E
 import qualified Cryptol.Backend.SeqMap as E
 import           Cryptol.Eval.Concrete( Concrete(..) )
@@ -260,7 +261,11 @@ nbCommandList  =
       , "The amount of time to spend collecting measurements can be changed"
       , "  with the timeMeasurementPeriod option."
       , "Reports the average wall clock time, CPU time, and cycles."
-      , "(Cycles are in unspecified units that may be CPU cycles.)"])
+      , "  (Cycles are in unspecified units that may be CPU cycles.)"
+      , "Binds the result to"
+      , "  it : { avgTime : Float64"
+      , "       , avgCpuTime : Float64"
+      , "       , avgCycles : Integer }" ])
   ]
 
 commandList :: [CommandDescr]
@@ -1022,6 +1027,14 @@ timeCmd str pos fnm = do
       rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime
            ++ "    Avg CPU time: " ++ Bench.secs benchAvgCpuTime
            ++ "    Avg cycles: " ++ show benchAvgCycles
+      let mkStatsRec time cpuTime cycles = recordFromFields
+            [("avgTime", time), ("avgCpuTime", cpuTime), ("avgCycles", cycles)]
+          itType = E.TVRec $ mkStatsRec E.tvFloat64 E.tvFloat64 E.TVInteger
+          itVal = E.VRecord $ mkStatsRec
+            (pure $ E.VFloat $ FP.floatFromDouble benchAvgTime)
+            (pure $ E.VFloat $ FP.floatFromDouble benchAvgCpuTime)
+            (pure $ E.VInteger $ toInteger benchAvgCycles)
+      bindItVariableVal itType itVal
 
 readFileCmd :: FilePath -> REPL ()
 readFileCmd fp = do
diff --git a/src/Cryptol/TypeCheck/FFI.hs b/src/Cryptol/TypeCheck/FFI.hs
index 3a845cb06..f4bae6e20 100644
--- a/src/Cryptol/TypeCheck/FFI.hs
+++ b/src/Cryptol/TypeCheck/FFI.hs
@@ -16,6 +16,7 @@ import           Cryptol.TypeCheck.FFI.FFIType
 import           Cryptol.TypeCheck.SimpType
 import           Cryptol.TypeCheck.Type
 import           Cryptol.Utils.RecordMap
+import           Cryptol.Utils.Types
 
 -- | Convert a 'Schema' to a 'FFIFunType', along with any 'Prop's that must be
 -- satisfied for the 'FFIFunType' to be valid.
@@ -96,8 +97,8 @@ toFFIBasicType t =
       | otherwise -> Just $ Left $ FFITypeError t FFIBadWordSize
       where word = Just . Right . FFIWord n
     TCon (TC TCFloat) [TCon (TC (TCNum e)) [], TCon (TC (TCNum p)) []]
-      | e == 8, p == 24 -> float FFIFloat32
-      | e == 11, p == 53 -> float FFIFloat64
+      | (e, p) == float32ExpPrec -> float FFIFloat32
+      | (e, p) == float64ExpPrec -> float FFIFloat64
       | otherwise -> Just $ Left $ FFITypeError t FFIBadFloatSize
       where float = Just . Right . FFIFloat e p
     _ -> Nothing

From f5fc53d2b01a6532c35837406dea4323646ce11c Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Tue, 30 Aug 2022 14:25:28 -0700
Subject: [PATCH 13/16] time command: Add Cryptol.Utils.Types

---
 src/Cryptol/Utils/Types.hs | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 src/Cryptol/Utils/Types.hs

diff --git a/src/Cryptol/Utils/Types.hs b/src/Cryptol/Utils/Types.hs
new file mode 100644
index 000000000..60cff6eeb
--- /dev/null
+++ b/src/Cryptol/Utils/Types.hs
@@ -0,0 +1,10 @@
+-- | Useful information about various types.
+module Cryptol.Utils.Types where
+
+-- | Exponent and precision of 32-bit IEEE-754 floating point.
+float32ExpPrec :: (Integer, Integer)
+float32ExpPrec = (8, 24)
+
+-- | Exponent and precision of 64-bit IEEE-754 floating point.
+float64ExpPrec :: (Integer, Integer)
+float64ExpPrec = (11, 53)

From 0b49544aa946264e189e12c31bcae5432d516db0 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Tue, 30 Aug 2022 14:36:32 -0700
Subject: [PATCH 14/16] time command: add timeQuiet option

---
 src/Cryptol/REPL/Command.hs | 11 +++++++----
 src/Cryptol/REPL/Monad.hs   |  3 +++
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index a3f4accb3..849c7068b 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -1016,7 +1016,9 @@ typeOfCmd str pos fnm = do
 timeCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
 timeCmd str pos fnm = do
   period <- getKnownUser "timeMeasurementPeriod" :: REPL Int
-  rPutStrLn $ "Measuring for " ++ show period ++ " seconds"
+  quiet <- getKnownUser "timeQuiet"
+  unless quiet $
+    rPutStrLn $ "Measuring for " ++ show period ++ " seconds"
   pExpr <- replParseExpr str pos fnm
   (_, def, sig) <- replCheckExpr pExpr
   replPrepareCheckedExpr def sig >>= \case
@@ -1024,9 +1026,10 @@ timeCmd str pos fnm = do
     Just (_, expr) -> do
       Bench.BenchmarkStats {..} <- liftModuleCmd
         (rethrowEvalError . M.benchmarkExpr (fromIntegral period) expr)
-      rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime
-           ++ "    Avg CPU time: " ++ Bench.secs benchAvgCpuTime
-           ++ "    Avg cycles: " ++ show benchAvgCycles
+      unless quiet $
+        rPutStrLn $ "Avg time: " ++ Bench.secs benchAvgTime
+             ++ "    Avg CPU time: " ++ Bench.secs benchAvgCpuTime
+             ++ "    Avg cycles: " ++ show benchAvgCycles
       let mkStatsRec time cpuTime cycles = recordFromFields
             [("avgTime", time), ("avgCpuTime", cpuTime), ("avgCycles", cycles)]
           itType = E.TVRec $ mkStatsRec E.tvFloat64 E.tvFloat64 E.TVInteger
diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
index 062693d1f..ca60dca60 100644
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -992,6 +992,9 @@ userOptions  = mkOptionMap
     , "This is a lower bound and the actual time taken might be higher if the"
     , "  evaluation takes a long time."
     ]
+
+  , simpleOpt "timeQuiet" ["time-quiet"] (EnvBool False) noCheck
+    "Suppress output of :time command and only bind result to `it`."
   ]
 
 

From d1a9971edd1e1a12c7f19f0a109f95234da12bb3 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Tue, 30 Aug 2022 14:42:47 -0700
Subject: [PATCH 15/16] time command: Add test

---
 tests/issues/issue1415.icry        | 3 +++
 tests/issues/issue1415.icry.stdout | 2 ++
 2 files changed, 5 insertions(+)
 create mode 100644 tests/issues/issue1415.icry
 create mode 100644 tests/issues/issue1415.icry.stdout

diff --git a/tests/issues/issue1415.icry b/tests/issues/issue1415.icry
new file mode 100644
index 000000000..85f20a570
--- /dev/null
+++ b/tests/issues/issue1415.icry
@@ -0,0 +1,3 @@
+:set timeQuiet=on
+:time 0x1 + 0x2
+:t it
diff --git a/tests/issues/issue1415.icry.stdout b/tests/issues/issue1415.icry.stdout
new file mode 100644
index 000000000..deb1890a2
--- /dev/null
+++ b/tests/issues/issue1415.icry.stdout
@@ -0,0 +1,2 @@
+Loading module Cryptol
+it : {avgTime : Float 11 53, avgCpuTime : Float 11 53, avgCycles : Integer}

From 7fd1e4dd9a3e3d778d2fe8e5dc54a4e582f94138 Mon Sep 17 00:00:00 2001
From: Bretton <qsctr@users.noreply.github.com>
Date: Tue, 30 Aug 2022 16:34:46 -0700
Subject: [PATCH 16/16] time command: Add note on laziness

---
 src/Cryptol/REPL/Command.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 849c7068b..a988d92ab 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -258,6 +258,10 @@ nbCommandList  =
     "Measure the time it takes to evaluate the given expression."
     (unlines
       [ "The expression will be evaluated many times to get accurate results."
+      , "Note that the first evaluation of a binding may take longer due to"
+      , "  laziness, and this may affect the reported time. If this is not"
+      , "  desired then make sure to evaluate the expression once first before"
+      , "  running :time."
       , "The amount of time to spend collecting measurements can be changed"
       , "  with the timeMeasurementPeriod option."
       , "Reports the average wall clock time, CPU time, and cycles."