sdfds.idr

module Test.SimpleTime

import Data.List

-- Helpers
-----------------------------------------------------------

infixr 10 ^
(^) : Num a => a -> Nat -> a
(^) m 0 = 1
(^) m (S k) = m * (m ^ k)

-- This is quotRem not divMod
-- since it gives divMod (-123) 10 == (-12,-3)
-- as opposed to  divMod (-123) 10 == (-13, 7)
quotRem : Integral a => a -> a -> (a,a)
quotRem x y = (div x y, mod x y)

-- assertion just to make sure div and mod do what I need it to as
-- libs change
divAndModAssert : quotRem (-123) 10 = (-12,-3)
divAndModAssert = Refl
-- If this is failing it's because quoteRem is no longer correct.

-----------------------------------------------------------


-- issues: relax the requirement for %foreign syntax, why should/does it parse how it does?

{-

Proposal for foreign specifier change:

Proposed general %foreign specifier shape, only language and function
required:

Shape: "language:[dialect:]function[(,supportfile)+]"

Specific backends can accept more specific variants
-- C examples
Shape: "C:function,libfile[,cheader]"

"C:puts,libc"
"C:puts,libc,stdio.h"
"C:myputs,mylib"

-- Scheme examples
Shape: "scheme:[dialect:]function[,schemesourcefile]"

"scheme:blodwen-sleep"
"scheme:chez:real-time"
"scheme:racket:current-milliseconds"
"scheme:racket:myfunc,mysupport.rkt"
"scheme:myfunc,mysupport.ss"
-- ^ Should specifiers with support/glue files _require_ dialect?


-}

-- Timing Lib starts here
-----------------------------------------------------------


data TimePtr : Type where
data TimeObj : Type where
  MkT : (time : Ptr TimePtr) -> TimeObj

-- extract seconds from a Time Object
racketSec : String
racketSec = "(lambda (t) (truncate (inexact->exact (/ t 1000))))"

-- seems sketchy, Racket only says it has US not NS but then has NS
-- when you multiply further
racketNanosec : String
racketNanosec = "(lambda (t) (inexact->exact (modulo (truncate (* t 1e6)) 1e9)))"

%foreign "scheme:chez,current-time"
         "scheme:racket,current-inexact-milliseconds"
primGetTime : PrimIO (Ptr TimePtr)

%foreign "scheme:chez,time-second"
         "scheme:racket," ++ racketSec
primGetSeconds : Ptr TimePtr -> Int

%foreign "scheme:chez,time-nanosecond"
         "scheme:racket," ++ racketNanosec
primGetNanoseconds : Ptr TimePtr -> Int

getTimeObj : IO TimeObj
getTimeObj = MkT <$> primIO primGetTime

-- supported timing resolutions
data Res = S | MS | US | NS

-- A point in time
data Timestamp : Type where
  MkTS : (s : Int) -> (ns : Int) -> Timestamp

getTime : IO Timestamp
getTime = do (MkT t) <- getTimeObj
             let s  = primGetSeconds t
                 ns = primGetNanoseconds t
             pure $ MkTS s ns

-- We're using Integer because time is infinite
-- Is there a reason to keep seconds around?
data DiffTime : Type where
  MkDT : (s : Integer) -> (ns : Integer) -> DiffTime

public export
implementation
Num DiffTime where
  MkDT s1 ns1 + MkDT s2 ns2
    = let nsp   = ns1 + ns2
          sp    = s1  + s2
          (d,r) = quotRem nsp (10^9)
      in if r < 0 then MkDT (sp + d - 1) (10^9 - r)
                  else MkDT (sp + d) r
  MkDT s1 ns1 * MkDT s2 ns2
    = let nsp   = ns1 * ns2
          sp    = s1  * s2
          (d,r) = quotRem nsp (10^9)
      in if r < 0 then MkDT (sp + d - 1) (10^9 - r)
                  else MkDT (sp + d) r
  fromInteger x = MkDT x 0
  -- Don't use this. Use - to construct DiffTime

public export
implementation
Neg DiffTime where
  MkDT s1 ns1 - MkDT s2 ns2
    = let nsp   = ns1 - ns2
          sp    = s1  - s2
          (d,r) = quotRem nsp (10^9)
      in if r < 0 then MkDT (sp + d - 1) (10^9 - r)
                  else MkDT (sp + d) r

public export
implementation
Eq DiffTime where
  MkDT s1 ns1 == MkDT s2 ns2 = s1 == s2 && ns1 == ns2

public export
implementation
Ord DiffTime where
  compare (MkDT s1 ns1) (MkDT s2 ns2) = compare (s1, ns1) (s2, ns2)

-- The main method for creating DiffTime
(-) : Timestamp -> Timestamp -> DiffTime
(-) (MkTS s1 ns1) (MkTS s2 ns2)
    = let dt1 = MkDT (cast s1) (cast ns1)
          dt2 = MkDT (cast s2) (cast ns2)
      in Prelude.(-) dt1 dt2

-- Get a difftime's value as a specific resolution
-- add rounding?
ofRes : DiffTime -> Res -> Integer
ofRes (MkDT s ns) r
    = case r of
        S  => s
        MS => s * 10^3 + ns `div` 10^6
        US => s * 10^6 + ns `div` 10^3
        NS => s * 10^9 + ns

-- Get the string of a difftime at a specific resolution
strMeasure : (r : Res) -> DiffTime -> String
strMeasure r ts
    = case r of
        S  => show (ts `ofRes` S) ++ "s"
        MS => show (ts `ofRes` MS) ++ "ms"
        US => show (ts `ofRes` US) ++ "μs"
        NS => show (ts `ofRes` NS) ++ "ns"

-- Like fromInteger this is purely for convenience. No gurantees are
-- made about this. Do not use it for anything but debugging.
Show DiffTime where
  show (MkDT s ns) = "MkDT " ++ show s ++ " " ++ show ns

-- If your value isn't generated by IO actions then use this
-- otherwise it might be evaluted too eagerly and void the timing
-- by doing upfront computing.
pureLazy : Monad m => Lazy a -> m a
pureLazy x = pure () >>= \() => pure x
-- In an actual program this probably wouldn't be needed since you
-- could just move the timing up a level to get the time that section
-- of your program took if it's spending time doing eager
-- calculations. But in testing we have cases that are very granular
-- so we might need the above.

-- Time an action
measure : IO a -> IO DiffTime
measure act = do
    t1 <- getTime
    act
    t2 <- getTime
    pure (t2 - t1)

-- just a computation that takes some time
fef : Int
fef = foldl (+) 0 [1..20000000]

run : IO a -> Nat -> IO ()
run act n = do
    t <- measure $ do
      putStrLn $ "Running " ++ show n ++ " tests."
      times <- for (indexed n (replicate n act)) $ \(i,act) => do
        putStr $ "Runnning test " ++ show i ++ "... "
        t <- measure act
        putStrLn $ showSandNS t
        pure t
      let tot = sum times
          avg = cast {to=Double} (tot `ofRes` NS) / cast n
          avgsecs = avg / 1000
      putStrLn $ "Total time " ++ strMeasure S tot ++ wrap (strMeasure US tot) ++ ", average of " ++ show avgsecs ++ wrap (show avg)
    putStrLn $ "Total testing time (for fun): " ++ strMeasure S t ++ wrap (strMeasure S t)
  where
    wrap : String -> String
    wrap s = "(" ++ s ++ ")"
    showSandNS : DiffTime -> String
    showSandNS dt = strMeasure S dt ++ wrap (strMeasure NS dt)
    indexed : forall a. Nat -> List a -> List (Nat, a)
    indexed n xs = zip [1..n] xs

runtest : Nat -> IO ()
runtest n = run (pureLazy fef) n

rt : IO ()    
rt = runtest 3