
  0 | module Profile.Statistics
  1 | 
  2 | import Data.Vect
  3 | import Profile.Types
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | mean : Vect (S n) (Scalar u) -> Scalar u
  9 | mean as = scalarSum as `div` posLength as
 10 | 
 11 | square : Scalar u -> Scalar (times u u)
 12 | square n = mult n n
 13 | 
 14 | public export
 15 | record Stats where
 16 |   constructor MkStats
 17 |   slope : AttoSecondsPerRun
 18 |   mean  : AttoSecondsPerRun
 19 |   r2    : Double
 20 | 
 21 | calcR2 : Scalar (U 1 1) -> Scalar (U 2 0) -> Scalar (U 0 2) -> Double
 22 | calcR2 it_at at2 it2 = toFloat (square it_at) / toFloat (mult at2 it2)
 23 | 
 24 | export
 25 | regr : (ms : Vect (S n) Measured) -> Stats
 26 | regr ms =
 27 |   let iters      := map iterations ms
 28 |       attos      := map tot ms
 29 |       mean_iter  := mean iters
 30 |       mean_attos := mean attos
 31 |       mean_avrg  := mean (map avrg ms)
 32 |       ss_iter    :=
 33 |         scalarSum (map square iters) `minus`
 34 |         mult (posLength ms) (square mean_iter)
 35 |       ss_atto    :=
 36 |         scalarSum (map square attos) `minus`
 37 |         mult (posLength ms) (square mean_attos)
 38 |       ss_it_at   :=
 39 |         scalarSum (zipWith mult iters attos) `minus`
 40 |         mult (posLength ms) (mult mean_iter mean_attos)
 41 |    in MkStats
 42 |         (ss_it_at `div` ss_iter)
 43 |         mean_avrg
 44 |         (calcR2 ss_it_at ss_atto ss_iter)
 45 |