From 31515dc82d9bf08240824ff4c33bfb245dc36b0f Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 23 Jun 2023 07:02:00 -0400 Subject: [PATCH] Setup test and bench harness --- PrimeSieve.ipkg | 1 + src/PrimeSieve.idr | 228 ++++++++++++++++++++++++++++++++++++- src/PrimeSieve/Simple.idr | 9 ++ src/PrimeSieve/Trivial.idr | 3 + 4 files changed, 240 insertions(+), 1 deletion(-) create mode 100644 src/PrimeSieve/Simple.idr diff --git a/PrimeSieve.ipkg b/PrimeSieve.ipkg index 49f2d53..cc5cea7 100644 --- a/PrimeSieve.ipkg +++ b/PrimeSieve.ipkg @@ -19,6 +19,7 @@ depends = contrib modules = PrimeSieve , PrimeSieve.Util , PrimeSieve.Trivial + , PrimeSieve.Simple -- main file (i.e. file to load at REPL) main = PrimeSieve diff --git a/src/PrimeSieve.idr b/src/PrimeSieve.idr index 773c114..b55e314 100644 --- a/src/PrimeSieve.idr +++ b/src/PrimeSieve.idr @@ -1,4 +1,230 @@ module PrimeSieve +import System.Clock +import Data.String + +import Collie + +import PrimeSieve.Trivial as Trivial +import PrimeSieve.Simple as Simple + +primeSieve : Command "primesieve" +primeSieve = MkCommand + { description = """ + """ + , subcommands = + [ "--help" ::= basic "Print this help text." none + , "bench-trivial" ::= basic "Benchmark the trivial generator" none + , "bench-simple" ::= basic "Benchmark the simple sieve" none + , "test-simple" ::= basic "test the simple sieve against trivial generation" none + , "test-trivial" ::= basic "test the trival generation against trivial generation" none + ] + , modifiers = [] + , arguments = none } + +{nm : String} -> {cmd : Command nm} -> Show (ParseTreeT f g cmd) where + show (Here x) = "\{nm} <>" + show (There pos parsedSub) = "\{nm} \{show parsedSub}" + +interface PrimeGen where + constructor MkPrimeGen + primesUntil : (Integral t, Ord t, Num t, Range t) => (limit : t) -> List t + primes : (Integral t, Ord t, Num t, Range t) => Maybe (Stream t) + + +%noinline +call : (a -> b) -> a -> IO b +call f x = fromPrim $ \w => MkIORes (f x) w + +displayTime : Clock t -> String +displayTime x = + let (secs, ns) = (seconds x, nanoseconds x) + mins = secs `div` 60 + secs = secs `mod` 60 + nanos = ns `mod` 1_000 + ns = ns `div` 1_000 + micros = ns `mod` 1_000 + millis = ns `div` 1_000 + in """ + \{padLeft 3 ' ' (show mins)}m \ + \{padLeft 3 ' ' (show secs)}s \ + \{padLeft 3 ' ' (show millis)}ms \ + \{padLeft 3 ' ' (show micros)}μs \ + \{padLeft 3 ' '(show nanos)}ns + """ + +timeToDouble : Clock t -> Double +timeToDouble x = + let (secs, ns) = (seconds x, nanoseconds x) + ns_double : Double = fromInteger ns + secs_double = (fromInteger secs) + in secs_double + (ns_double / 1000000000.0) + +record Timed a where + constructor MkTimed + result : a + desc : String + runCount : Nat + runsNonZero : NonZero runCount + runs : Vect runCount (Clock Duration) + +%name Timed timed, timed2, timed3 + +(.min) : Timed a -> Clock Duration +(.min) (MkTimed result desc runCount runsNonZero runs) = minVect' runs + where + minVect : (Ord b) => (xs : Vect n b) -> b -> b + minVect [] x = x + minVect (y :: xs) x = + if y < x + then minVect xs y + else minVect xs x + minVect' : (Ord b) => {n : Nat} -> (xs : Vect n b) -> {auto prf : NonZero n} -> b + minVect' {prf} [] impossible + minVect' (x :: xs) = minVect xs x + +(.max) : Timed a -> Clock Duration +(.max) (MkTimed result desc runCount runsNonZero runs) = maxVect' runs + where + maxVect : (Ord b) => (xs : Vect n b) -> b -> b + maxVect [] x = x + maxVect (y :: xs) x = + if y > x + then maxVect xs y + else maxVect xs x + maxVect' : (Ord b) => {n : Nat} -> (xs : Vect n b) -> {auto prf : NonZero n} -> b + maxVect' {prf} [] impossible + maxVect' (x :: xs) = maxVect xs x + +(.avg) : Timed a -> Clock Duration +(.avg) (MkTimed result desc runCount runsNonZero runs) = avgVect runCount runs + where + totalVect : (xs : Vect n (Clock Duration)) -> (acc : (Integer, Integer)) -> (Integer, Integer) + totalVect [] acc = acc + totalVect (x :: xs) (sec_total, ns_total) = + let (sec, ns) = (seconds x, nanoseconds x) + in totalVect xs (sec_total + sec, ns_total + ns) + avgVect : (count : Nat) -> (xs : Vect count (Clock Duration)) -> Clock Duration + avgVect 0 xs = makeDuration 0 0 + avgVect count@(S count') xs = + let (sec, ns) = totalVect xs (0,0) + t = ((sec * 1_000_000_000) + ns) `div` (natToInteger count) + in makeDuration 0 t + +Show (Timed a) where + show t = """ + \{t.desc} \ + min: \{displayTime t.min} \ + avg: \{displayTime t.avg} \ + max: \{displayTime t.max} + """ + +mergeTimed : (x : Timed a) -> (y : Timed a) -> Timed a +mergeTimed (MkTimed result desc 0 runsNonZero runs) (MkTimed x str k y xs) impossible +mergeTimed (MkTimed result desc (S j) runsNonZero runs) (MkTimed x str k y xs) = + MkTimed x str ((S j) + k) SIsNonZero (runs ++ xs) + +timeIO : (prev : Maybe (Timed a)) + -> (action : IO a) + -> (case prev of + Nothing => (desc : String) -> IO (Timed a) + (Just _) => IO (Timed a)) +timeIO Nothing action = + (\desc => + do start <- clockTime Monotonic + result <- action + end <- clockTime Monotonic + let time = timeDifference end start + pure (MkTimed result desc 1 SIsNonZero [time])) +timeIO (Just timed) action = do + single <- timeIO Nothing action timed.desc + pure (mergeTimed timed single) + +runTimes : (times : Nat) -> {auto prf : NonZero times} -> (desc : String) -> (action : IO a) -> IO (Timed a) +runTimes 0 desc action impossible +runTimes (S times') desc action = do + timed <- timeIO Nothing action desc + runTimes' times' timed action + where + runTimes' : Nat -> (acc : Timed a) -> IO a -> IO (Timed a) + runTimes' 0 acc x = pure acc + runTimes' (S k) acc x = do + timed <- timeIO (Just acc) x + runTimes' k timed x + +||| Benchmark a PrimeGen +benchmark : PrimeGen -> IO () +benchmark x = do + putStrLn "Benching primesUntil method\n" + benchUntil 100 + benchUntil 1_000 + benchUntil 10_000 + benchUntil 100_000 + where + benchUntil : (limit : Bits64) -> IO () + benchUntil limit = + do putStrLn " Benchmarking primes up to \{show limit} (100 times):" + time <- runTimes + 100 + "Primes <= \{padLeft 6 ' ' (show limit)}" + ((call PrimeSieve.primesUntil) limit) + putStrLn " \{show time}" + let primesPerSec = 1.0 / (timeToDouble time.avg) + putStrLn + " Avg \{show primesPerSec} primes/s (\{show (length time.result)} primes)\n" + +||| Test a PrimeGen against the default +test : PrimeGen -> IO () +test item = do + putStrLn "Testing primesUntil method\n" + tryUntil 10 + tryUntil 100 + tryUntil 1_000 + tryUntil 10_000 + tryUntil 100_000 + putStrLn "" + let stream : Maybe (Stream Bits64) = PrimeSieve.primes + case stream of + Nothing => exitSuccess + (Just x) => do + tryStream 10 x + tryStream 100 x + tryStream 1_000 x + tryStream 10_000 x + where + fail : Show t => List t -> List t -> IO () + fail expected got = do + putStrLn "fail\n" + putStrLn "Expected: \{show expected}" + putStrLn "Got: \{show got}" + exitFailure + tryCompare : (Show t, Eq t) => List t -> List t -> IO () + tryCompare xs ys = + if xs == ys + then putStrLn "pass" + else fail xs ys + tryUntil : Bits64 -> IO () + tryUntil k = do + putStr " Testing up to \{show k}: " + let trivial : List Bits64 = Trivial.primesUntil k + let sample : List Bits64 = PrimeSieve.primesUntil k + tryCompare trivial sample + tryStream : Nat -> Stream Bits64 -> IO () + tryStream k stream = do + putStr " Testing up to \{show k}: " + let trivial = take k Trivial.primes + let sample = take k stream + tryCompare trivial sample + + main : IO () -main = putStrLn "Hello!" +main = do + Right cmdParse <- primeSieve.parseArgs + | Left err => putStrLn "Error: \{err}" + case fst (lookup cmdParse) of + "bench-trivial" => benchmark (MkPrimeGen Trivial.primesUntil (Just Trivial.primes)) + "bench-simple" => benchmark (MkPrimeGen Simple.primesUntil Nothing) + "test-trivial" => test (MkPrimeGen Trivial.primesUntil (Just Trivial.primes)) + "test-simple" => test (MkPrimeGen Simple.primesUntil Nothing) + "--help" => putStrLn "Usage: \n\{primeSieve.usage}" + _ => putStrLn "Parse as \{show cmdParse}" diff --git a/src/PrimeSieve/Simple.idr b/src/PrimeSieve/Simple.idr new file mode 100644 index 0000000..2c121ba --- /dev/null +++ b/src/PrimeSieve/Simple.idr @@ -0,0 +1,9 @@ +module PrimeSieve.Simple + +||| Use a basic, unoptimized sieve to generate the primes up to a specific number +export +primesUntil : (Integral t, Ord t, Num t, Range t) => (limit : t) -> List t + +||| A stream of primes, Generated by a lazily extending sieve +export +primes : (Integral t, Ord t, Num t, Range t) => Stream t diff --git a/src/PrimeSieve/Trivial.idr b/src/PrimeSieve/Trivial.idr index 4ce6447..bceaba6 100644 --- a/src/PrimeSieve/Trivial.idr +++ b/src/PrimeSieve/Trivial.idr @@ -7,6 +7,7 @@ import PrimeSieve.Util %default total ||| Test if a number is prime via trial division +export isPrime : (Integral t, Ord t, Num t, Range t) => t -> Bool isPrime x = let trial_divisors = [2..((isqrt x) + 1)] @@ -22,6 +23,7 @@ isPrime x = else isPrime' xs x ||| A stream of primes, generated by testing via trial division +export primes : (Integral t, Ord t, Num t, Range t) => Stream t primes = let naturals : Stream t = iterate (+1) 1 @@ -37,6 +39,7 @@ primes = else next_prime (assert_smaller orig ys) ||| All the primes up until the given limit +export primesUntil : (Integral t, Ord t, Num t, Range t) => (limit : t) -> List t -- We assert_total here as the list of primes is infinite and strictly increasing, so this -- Will always terminate in finite time