mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
time command: bind result to it
This commit is contained in:
parent
130ae18573
commit
09cf06a8e8
@ -119,6 +119,7 @@ library
|
||||
Cryptol.Utils.Patterns,
|
||||
Cryptol.Utils.Logger,
|
||||
Cryptol.Utils.Benchmark,
|
||||
Cryptol.Utils.Types,
|
||||
Cryptol.Version,
|
||||
|
||||
Cryptol.ModuleSystem,
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user