
   0 | module Profile.Types
   1 | 
   2 | import Debug.Trace
   3 | import public Data.DPair
   4 | import public Data.Nat
   5 | import public Data.Vect
   6 | import public System.Clock
   7 | 
   8 | %default total
   9 | 
  10 | --------------------------------------------------------------------------------
  11 | --          Format
  12 | --------------------------------------------------------------------------------
  13 | 
  14 | public export
  15 | data Format = Table | Details
  16 | 
  17 | --------------------------------------------------------------------------------
  18 | --          Pos
  19 | --------------------------------------------------------------------------------
  20 | 
  21 | ||| A strictly positive natural number.
  22 | public export
  23 | record Pos where
  24 |   constructor MkPos
  25 |   val   : Nat
  26 |   {auto 0 prf : IsSucc val}
  27 | 
  28 | export
  29 | Eq Pos where (==) = (==) `on` val
  30 | 
  31 | export
  32 | Ord Pos where compare = compare `on` val
  33 | 
  34 | public export
  35 | fromInteger : (n : Integer) -> (0 prf : IsSucc (cast n)) => Pos
  36 | fromInteger n = MkPos (cast n)
  37 | 
  38 | --------------------------------------------------------------------------------
  39 | --          Benchmarkable
  40 | --------------------------------------------------------------------------------
  41 | 
  42 | ||| A benchmarkable computation, which can fail with error `err`.
  43 | public export
  44 | record Benchmarkable (err : Type) where
  45 |   constructor MkBenchmarkable
  46 |   {0 environment : Type}
  47 | 
  48 |   {0 result      : Type}
  49 | 
  50 |   ||| Allocates an environment for running the benchmark
  51 |   ||| the given number of times.
  52 |   allocEnv      : Pos -> IO environment
  53 | 
  54 |   ||| Cleanup the environment after running the benchmark
  55 |   ||| the given number of times.
  56 |   cleanEnv      : Pos -> environment -> IO ()
  57 | 
  58 |   ||| Run a benchmurk in the given environment for
  59 |   ||| the given number of times.
  60 |   runRepeatedly : environment -> Pos -> IO (Either err result)
  61 | 
  62 |   ||| True, if this is a pure computation and we are only interested
  63 |   ||| in the time spent on the CPU.
  64 |   cpuOnly       : Bool
  65 | 
  66 | repeatedly_ : Nat -> PrimIO (Either err ()) -> PrimIO (Either err ())
  67 | repeatedly_ 0     _ w = MkIORes (Right ()) w
  68 | repeatedly_ (S k) f w =
  69 |   let MkIORes (Right _) w2 := f w | res => res
  70 |    in repeatedly_ k f w2
  71 | 
  72 | ||| Tail-recursively runs an IO action the given number
  73 | ||| of times or until it returns `False`, signaling a
  74 | ||| failure.
  75 | export
  76 | repeatedly : Pos -> IO (Either err ()) -> IO (Either err ())
  77 | repeatedly (MkPos n) io = fromPrim $ repeatedly_ n (toPrim io)
  78 | 
  79 | export
  80 | singleIO : IO () -> Benchmarkable Void
  81 | singleIO io =
  82 |   MkBenchmarkable
  83 |     { allocEnv = \_ => pure ()
  84 |     , cleanEnv = \_,_ => pure ()
  85 |     , runRepeatedly = \(),n => repeatedly n (map Right io)
  86 |     , cpuOnly  = False
  87 |     }
  88 | 
  89 | repeatedlyPure_ : Nat -> a -> (() -> Either err a) -> Either err a
  90 | repeatedlyPure_ 0     v _ = Right v
  91 | repeatedlyPure_ (S k) v f = case f () of
  92 |   Right v2 => repeatedlyPure_ k v2 f
  93 |   Left err => Left err
  94 | 
  95 | export
  96 | repeatedlyPure : Pos -> (() -> Either err a) -> Either err a
  97 | repeatedlyPure (MkPos $ S n) f = case f () of
  98 |   Left err => Left err
  99 |   Right v  => repeatedlyPure_ n v f
 100 | 
 101 | export
 102 | singlePure : (() -> Either err a) -> Benchmarkable err
 103 | singlePure f =
 104 |   MkBenchmarkable
 105 |     { allocEnv = \_ => pure ()
 106 |     , cleanEnv = \_,_ => pure ()
 107 |     , runRepeatedly = \(),n => map (`repeatedlyPure` f) (pure n)
 108 |     , cpuOnly  = True
 109 |     }
 110 | 
 111 | export
 112 | basic : (a -> b) -> a -> Benchmarkable Void
 113 | basic f va = singlePure (\_ => let v = f va in Right v)
 114 | 
 115 | --------------------------------------------------------------------------------
 116 | --          Benchmarks
 117 | --------------------------------------------------------------------------------
 118 | 
 119 | public export
 120 | data Benchmark : (err : Type) -> Type where
 121 |   Single : (name : String) -> (bench : Benchmarkable err) -> Benchmark err
 122 |   Group  : (name : String) -> (benchs : List (Benchmark err)) -> Benchmark err
 123 | 
 124 | export
 125 | addPrefix : (pre : String) -> (rst : String) -> String
 126 | addPrefix ""  rst = rst
 127 | addPrefix pre rst = "\{pre}/\{rst}"
 128 | 
 129 | --------------------------------------------------------------------------------
 130 | --          Scalars
 131 | --------------------------------------------------------------------------------
 132 | 
 133 | public export
 134 | record SUnit where
 135 |   constructor U
 136 |   atto : Integer
 137 |   run  : Integer
 138 | 
 139 | namespace SUnit
 140 |   public export
 141 |   times : SUnit -> SUnit -> SUnit
 142 |   -- this makes sure that multiplication by a unit-less scalar
 143 |   -- reduces during unification
 144 |   times (U 0 0)   u         = u
 145 |   times (U a1 r1) (U a2 r2) = U (a1 + a2) (r1 + r2)
 146 | 
 147 |   public export
 148 |   div : SUnit -> SUnit -> SUnit
 149 |   -- this makes sure that division by a unit-less scalar
 150 |   -- reduces during unification
 151 |   div u         (U 0 0)   = u
 152 |   div (U a1 r1) (U a2 r2) = U (a1 - a2) (r1 - r2)
 153 | 
 154 | public export
 155 | record Scalar (u : SUnit) where
 156 |   constructor MkScalar
 157 |   val : Integer
 158 | 
 159 | public export
 160 | Eq (Scalar u) where (==) = (==) `on` val
 161 | 
 162 | public export
 163 | Ord (Scalar u) where compare = compare `on` val
 164 | 
 165 | namespace Scalar
 166 |   public export
 167 |   fromInteger : Integer -> Scalar u
 168 |   fromInteger = MkScalar
 169 | 
 170 | public export
 171 | 0 AttoSeconds : Type
 172 | AttoSeconds = Scalar (U 1 0)
 173 | 
 174 | public export
 175 | 0 AttoSecondsPerRun : Type
 176 | AttoSecondsPerRun = Scalar (U 1 (-1))
 177 | 
 178 | public export
 179 | 0 Runs : Type
 180 | Runs = Scalar (U 0 1)
 181 | 
 182 | public export
 183 | plus : Scalar u -> Scalar u -> Scalar u
 184 | plus x y = MkScalar $ x.val + y.val
 185 | 
 186 | public export
 187 | minus : Scalar u -> Scalar u -> Scalar u
 188 | minus x y = MkScalar $ x.val - y.val
 189 | 
 190 | public export
 191 | scalarSum : Foldable t => t (Scalar u) -> Scalar u
 192 | scalarSum = foldl plus 0
 193 | 
 194 | public export
 195 | mult : Scalar u1 -> Scalar u2 -> Scalar (times u1 u2)
 196 | mult x y = MkScalar $ x.val * y.val
 197 | 
 198 | public export
 199 | div : Scalar u1 -> Scalar u2 -> Scalar (div u1 u2)
 200 | div x y = MkScalar $ x.val `div` y.val
 201 | 
 202 | public export
 203 | posLength : Vect (S n) a -> Scalar (U 0 0)
 204 | posLength = MkScalar . cast . length
 205 | 
 206 | public export
 207 | fromFemtoSeconds : Integer -> AttoSeconds
 208 | fromFemtoSeconds = fromInteger . (* 1000)
 209 | 
 210 | public export
 211 | fromPicoSeconds : Integer -> AttoSeconds
 212 | fromPicoSeconds = fromFemtoSeconds . (* 1000)
 213 | 
 214 | public export
 215 | fromNanoSeconds : Integer -> AttoSeconds
 216 | fromNanoSeconds = fromPicoSeconds . (* 1000)
 217 | 
 218 | public export
 219 | fromMicroSeconds : Integer -> AttoSeconds
 220 | fromMicroSeconds = fromNanoSeconds . (* 1000)
 221 | 
 222 | public export
 223 | fromMilliSeconds : Integer -> AttoSeconds
 224 | fromMilliSeconds = fromMicroSeconds . (* 1000)
 225 | 
 226 | public export
 227 | fromSeconds : Integer -> AttoSeconds
 228 | fromSeconds = fromMilliSeconds . (* 1000)
 229 | 
 230 | public export
 231 | fromClock : Clock Duration -> AttoSeconds
 232 | fromClock c =
 233 |   plus
 234 |     (fromNanoSeconds $ nanoseconds c)
 235 |     (fromSeconds $ seconds c)
 236 | 
 237 | export
 238 | timeDelta : Clock t -> Clock t -> AttoSeconds
 239 | timeDelta c1 c2 = fromClock $ timeDifference (max c1 c2) (min c1 c2)
 240 | 
 241 | export
 242 | toFloat : Scalar u -> Double
 243 | toFloat = cast . val
 244 | 
 245 | --------------------------------------------------------------------------------
 246 | --          Measured
 247 | --------------------------------------------------------------------------------
 248 | 
 249 | ||| A collection of measurements made while benchmarking
 250 | public export
 251 | record Measured where
 252 |   constructor MkMeasured
 253 |   ||| Number of iterations
 254 |   iterations : Runs
 255 | 
 256 |   ||| True, if we are interested only in the CPU time
 257 |   cpuOnly    : Bool
 258 | 
 259 |   ||| Wall clock time when starting the measurement
 260 |   startTime  : Clock Monotonic
 261 | 
 262 |   ||| Wall clock time when stopping the measurement
 263 |   stopTime   : Clock Monotonic
 264 | 
 265 |   ||| Total wall clock time elapsed in atto seconds
 266 |   totalTime  : AttoSeconds
 267 | 
 268 |   ||| Average wall clock time elapsed per iteration
 269 |   avrgTime   : AttoSecondsPerRun
 270 | 
 271 |   ||| Total CPU time elapsed
 272 |   cpuTime    : AttoSeconds
 273 | 
 274 |   ||| Average CPU time elapsed per iteration
 275 |   avrgCPU    : AttoSecondsPerRun
 276 | 
 277 | export
 278 | tot : Measured -> AttoSeconds
 279 | tot m = if m.cpuOnly then m.cpuTime else m.totalTime
 280 | 
 281 | export
 282 | avrg : Measured -> AttoSecondsPerRun
 283 | avrg m = if m.cpuOnly then m.avrgCPU else m.avrgTime
 284 | 
 285 | --------------------------------------------------------------------------------
 286 | --          Result of running a single benchmark
 287 | --------------------------------------------------------------------------------
 288 | 
 289 | public export
 290 | record Result where
 291 |   constructor MkResult
 292 |   name      : String
 293 |   runs      : List Measured
 294 |