Setup test and bench harness
This commit is contained in:
parent
0257c9fde7
commit
31515dc82d
|
@ -19,6 +19,7 @@ depends = contrib
|
||||||
modules = PrimeSieve
|
modules = PrimeSieve
|
||||||
, PrimeSieve.Util
|
, PrimeSieve.Util
|
||||||
, PrimeSieve.Trivial
|
, PrimeSieve.Trivial
|
||||||
|
, PrimeSieve.Simple
|
||||||
|
|
||||||
-- main file (i.e. file to load at REPL)
|
-- main file (i.e. file to load at REPL)
|
||||||
main = PrimeSieve
|
main = PrimeSieve
|
||||||
|
|
|
@ -1,4 +1,230 @@
|
||||||
module PrimeSieve
|
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} <<args>>"
|
||||||
|
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 : 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}"
|
||||||
|
|
|
@ -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
|
|
@ -7,6 +7,7 @@ import PrimeSieve.Util
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
||| Test if a number is prime via trial division
|
||| Test if a number is prime via trial division
|
||||||
|
export
|
||||||
isPrime : (Integral t, Ord t, Num t, Range t) => t -> Bool
|
isPrime : (Integral t, Ord t, Num t, Range t) => t -> Bool
|
||||||
isPrime x =
|
isPrime x =
|
||||||
let trial_divisors = [2..((isqrt x) + 1)]
|
let trial_divisors = [2..((isqrt x) + 1)]
|
||||||
|
@ -22,6 +23,7 @@ isPrime x =
|
||||||
else isPrime' xs x
|
else isPrime' xs x
|
||||||
|
|
||||||
||| A stream of primes, generated by testing via trial division
|
||| A stream of primes, generated by testing via trial division
|
||||||
|
export
|
||||||
primes : (Integral t, Ord t, Num t, Range t) => Stream t
|
primes : (Integral t, Ord t, Num t, Range t) => Stream t
|
||||||
primes =
|
primes =
|
||||||
let naturals : Stream t = iterate (+1) 1
|
let naturals : Stream t = iterate (+1) 1
|
||||||
|
@ -37,6 +39,7 @@ primes =
|
||||||
else next_prime (assert_smaller orig ys)
|
else next_prime (assert_smaller orig ys)
|
||||||
|
|
||||||
||| All the primes up until the given limit
|
||| All the primes up until the given limit
|
||||||
|
export
|
||||||
primesUntil : (Integral t, Ord t, Num t, Range t) => (limit : t) -> List t
|
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
|
-- We assert_total here as the list of primes is infinite and strictly increasing, so this
|
||||||
-- Will always terminate in finite time
|
-- Will always terminate in finite time
|
||||||
|
|
Loading…
Reference in New Issue