0 | module ParkBench
  1 |
  2 | import Data.String
  3 | import System.Clock
  4 |
  5 | log : Double -> Double -> Double
  6 | log base x = log x / log base -- shh don't tell anyone about this
  7 |
  8 | record FloatingParts a where
  9 |     constructor MkFloatingParts
 10 |     exp : a
 11 |     mant : a
 12 |
 13 | %inline
 14 | floatingParts : (base : Double) -> (x : Double) -> FloatingParts Double
 15 | floatingParts base x =
 16 |     let exp = floor $ log base x
 17 |         mant = x * pow base (-exp)
 18 |      in MkFloatingParts { exp, mant }
 19 |
 20 | roundToDp : (dps : Nat) -> Double -> Double
 21 | roundToDp dps x =
 22 |     let scale = pow 10 $ cast dps
 23 |      in floor (x * scale) / scale
 24 |
 25 | roundToSf : (sfs : Nat) -> Double -> Double
 26 | roundToSf sfs x =
 27 |     let scale = pow 10 $ cast (sfs `minus` 1) - (floatingParts 10 x).exp
 28 |      in floor (x * scale) / scale
 29 |
 30 | standardForm : (sigFigs : Nat) -> Double -> String
 31 | standardForm sigFigs x =
 32 |     let MkFloatingParts { exp, mant } = floatingParts 10 x
 33 |         mant = roundToDp (sigFigs `minus` 1) mant
 34 |      in padRight (sigFigs + 1) '0' (show mant) ++ "e" ++ show (cast {to=Integer} exp)
 35 |
 36 | notQuiteStandardForm : (sigFigs : Nat) -> Double -> String
 37 | notQuiteStandardForm sigFigs x =
 38 |     let MkFloatingParts { exp, mant } = floatingParts 10 x
 39 |         mant = roundToDp (sigFigs `minus` 1) mant
 40 |      in if -1 <= exp && exp <= 3
 41 |         then
 42 |             let exp = cast {to=Integer} exp
 43 |              in show $ roundToSf sigFigs x
 44 |         else padRight (sigFigs + 1) '0' (show mant) ++ "e" ++ show (cast {to=Integer} exp)
 45 |
 46 | nanoInSec : Integer
 47 | nanoInSec = 1000000000
 48 |
 49 | toNano' : Clock type -> Integer
 50 | toNano' (MkClock s ns) = s * nanoInSec + ns
 51 |
 52 | fromNano' : {type : _} -> Integer -> Clock type
 53 | fromNano' nanos =
 54 |     let s = nanos `div` nanoInSec
 55 |         ns = nanos `mod` nanoInSec
 56 |      in MkClock s ns
 57 |
 58 | public export
 59 | record Timed a where
 60 |     constructor MkTimed
 61 |     result : a
 62 |     description : String
 63 |     runs : Nat
 64 |     totalTime : Clock Duration
 65 |     time : Clock Duration
 66 |
 67 | showPlural : String -> Nat -> String
 68 | showPlural str 1 = str
 69 | showPlural str _ = str ++ "s"
 70 |
 71 | getOpsPerSec : (runs : Nat) -> (time : Clock Duration) -> Double
 72 | getOpsPerSec runs time =
 73 |     let runs = cast {to = Double} runs
 74 |         timeNs = cast {to = Double} $ toNano' time
 75 |      in (runs * cast nanoInSec) / timeNs
 76 |
 77 | export
 78 | Show (Timed a) where
 79 |     show timed = """
 80 |     \{timed.description} took \{showTime 0 5 timed.time}
 81 |       \{show timed.runs} \{showPlural "run" timed.runs} (total time: \{showTime 0 5 timed.totalTime})
 82 |     """
 83 |     -- TODO: fix this
 84 |     --   \{notQuiteStandardForm 3 $ getOpsPerSec timed.runs timed.time} operations per second
 85 |     -- """
 86 |
 87 | ||| A black-box function to call a closure.
 88 | |||
 89 | ||| This treats evaluating a closure as a side effect
 90 | %noinline
 91 | call : (a -> b) -> a -> IO b
 92 | call f x = fromPrim $ \w => MkIORes (f x) w
 93 |
 94 | ||| Time an `IO` action
 95 | export
 96 | timeIO : String -> IO a -> IO (Timed a)
 97 | timeIO description act = do
 98 |     start <- clockTime Monotonic
 99 |     result <- act
100 |     end <- clockTime Monotonic
101 |     let time = timeDifference end start
102 |     pure $ MkTimed {description, result, runs = 1, totalTime = time, time}
103 |
104 | repeat : IO a -> Nat -> a -> IO a
105 | repeat act Z acc = pure acc
106 | repeat act (S k) acc = act >>= repeat act k
107 |
108 | %inline
109 | divide : Clock Duration -> Nat -> Clock Duration
110 | divide c runs = fromNano' $ toNano' c `div` cast runs
111 |
112 | ||| Default duration of each benchmark
113 | public export
114 | defaultTime : Clock Duration
115 | defaultTime = makeDuration 1 0
116 |
117 | ||| Benchmark an IO operation.
118 | |||
119 | ||| This runs the given action repeatedly, until the target time has been reached.
120 | export
121 | benchIO :
122 |     {default defaultTime targetTime : Clock Duration} ->
123 |     (description : String) ->
124 |     (act : IO a) ->
125 |     IO (Timed a)
126 | benchIO description act = do
127 |     warmup <- timeIO description act
128 |     if warmup.time > targetTime
129 |         then pure warmup
130 |         else do
131 |             let runs = cast {to=Nat} $ toNano' targetTime `div` toNano' warmup.time
132 |             let False = runs <= 1
133 |                 | True => pure warmup
134 |             res <- timeIO description $ repeat act runs warmup.result
135 |             pure $ { runs := runs, time $= (`divide` runs) } res
136 |
137 | ||| Benchmark a function with a given input.
138 | |||
139 | ||| This runs the function repeatedly until enough time has passed.
140 | ||| The default time to benchmark is 1 second, but this can be changed
141 | ||| with `targetTime`.
142 | export
143 | bench :
144 |     {default defaultTime targetTime : Clock Duration} ->
145 |     (description : String) ->
146 |     (a -> b) ->
147 |     a ->
148 |     IO (Timed b)
149 | bench description f x = benchIO description (call f x)
150 |