Idris2Doc : Profile.Types

Profile.Types

(source)
Reexports
import public Data.DPair
import public Data.Nat
import public Data.Vect
import public System.Clock
Definitions
data Format : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Table : Format
  
Details : Format
record Pos : Type
  A strictly positive natural number.

  Totality: total
  Visibility: public export
  Constructor: 
MkPos : (val : Nat) -> {auto 0 _ : IsSucc val} -> Pos

  Projections:
  
0 .prf : ({rec:0} : Pos) -> IsSucc (val {rec:0})
  
.val : Pos -> Nat

  Hints:
  
Eq Pos
  
Ord Pos
.val : Pos -> Nat
  Totality: total
  Visibility: public export
val : Pos -> Nat
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : Pos) -> IsSucc (val {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : Pos) -> IsSucc (val {rec:0})
  Totality: total
  Visibility: public export
fromInteger : (n : Integer) -> {auto 0 _ : IsSucc (cast n)} -> Pos
  Totality: total
  Visibility: public export
record Benchmarkable : Type -> Type
  A benchmarkable computation, which can fail with error `err`.

  Totality: total
  Visibility: public export
  Constructor: 
MkBenchmarkable : (Pos -> IO environment) -> (Pos -> environment -> IO ()) -> (environment -> Pos -> IO (Either err result)) -> Bool -> Benchmarkable err

  Projections:
  
.allocEnv : ({rec:0} : Benchmarkable err) -> Pos -> IO (environment {rec:0})
  Allocates an environment for running the benchmark
  the given number of times.
  
.cleanEnv : ({rec:0} : Benchmarkable err) -> Pos -> environment {rec:0} -> IO ()
  Cleanup the environment after running the benchmark
  the given number of times.
  
.cpuOnly : Benchmarkable err -> Bool
  True, if this is a pure computation and we are only interested
  in the time spent on the CPU.
  
0 .environment : Benchmarkable err -> Type
  
0 .result : Benchmarkable err -> Type
  
.runRepeatedly : ({rec:0} : Benchmarkable err) -> environment {rec:0} -> Pos -> IO (Either err (result {rec:0}))
  Run a benchmurk in the given environment for
  the given number of times.
0 .environment : Benchmarkable err -> Type
  Totality: total
  Visibility: public export
0 environment : Benchmarkable err -> Type
  Totality: total
  Visibility: public export
0 .result : Benchmarkable err -> Type
  Totality: total
  Visibility: public export
0 result : Benchmarkable err -> Type
  Totality: total
  Visibility: public export
.allocEnv : ({rec:0} : Benchmarkable err) -> Pos -> IO (environment {rec:0})
  Allocates an environment for running the benchmark
  the given number of times.

  Totality: total
  Visibility: public export
allocEnv : ({rec:0} : Benchmarkable err) -> Pos -> IO (environment {rec:0})
  Allocates an environment for running the benchmark
  the given number of times.

  Totality: total
  Visibility: public export
.cleanEnv : ({rec:0} : Benchmarkable err) -> Pos -> environment {rec:0} -> IO ()
  Cleanup the environment after running the benchmark
  the given number of times.

  Totality: total
  Visibility: public export
cleanEnv : ({rec:0} : Benchmarkable err) -> Pos -> environment {rec:0} -> IO ()
  Cleanup the environment after running the benchmark
  the given number of times.

  Totality: total
  Visibility: public export
.runRepeatedly : ({rec:0} : Benchmarkable err) -> environment {rec:0} -> Pos -> IO (Either err (result {rec:0}))
  Run a benchmurk in the given environment for
  the given number of times.

  Totality: total
  Visibility: public export
runRepeatedly : ({rec:0} : Benchmarkable err) -> environment {rec:0} -> Pos -> IO (Either err (result {rec:0}))
  Run a benchmurk in the given environment for
  the given number of times.

  Totality: total
  Visibility: public export
.cpuOnly : Benchmarkable err -> Bool
  True, if this is a pure computation and we are only interested
  in the time spent on the CPU.

  Totality: total
  Visibility: public export
cpuOnly : Benchmarkable err -> Bool
  True, if this is a pure computation and we are only interested
  in the time spent on the CPU.

  Totality: total
  Visibility: public export
repeatedly : Pos -> IO (Either err ()) -> IO (Either err ())
  Tail-recursively runs an IO action the given number
  of times or until it returns `False`, signaling a
  failure.

  Totality: total
  Visibility: export
singleIO : IO () -> Benchmarkable Void
  Totality: total
  Visibility: export
repeatedlyPure : Pos -> (() -> Either err a) -> Either err a
  Totality: total
  Visibility: export
singlePure : (() -> Either err a) -> Benchmarkable err
  Totality: total
  Visibility: export
basic : (a -> b) -> a -> Benchmarkable Void
  Totality: total
  Visibility: export
data Benchmark : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Single : String -> Benchmarkable err -> Benchmark err
  
Group : String -> List (Benchmark err) -> Benchmark err
addPrefix : String -> String -> String
  Totality: total
  Visibility: export
record SUnit : Type
  Totality: total
  Visibility: public export
  Constructor: 
U : Integer -> Integer -> SUnit

  Projections:
  
.atto : SUnit -> Integer
  
.run : SUnit -> Integer

  Hints:
  
Eq (Scalar u)
  
Ord (Scalar u)
.atto : SUnit -> Integer
  Totality: total
  Visibility: public export
atto : SUnit -> Integer
  Totality: total
  Visibility: public export
.run : SUnit -> Integer
  Totality: total
  Visibility: public export
run : SUnit -> Integer
  Totality: total
  Visibility: public export
times : SUnit -> SUnit -> SUnit
  Totality: total
  Visibility: public export
div : SUnit -> SUnit -> SUnit
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 9
record Scalar : SUnit -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkScalar : Integer -> Scalar u

  Projection: 
.val : Scalar u -> Integer

  Hints:
  
Eq (Scalar u)
  
Ord (Scalar u)
.val : Scalar u -> Integer
  Totality: total
  Visibility: public export
val : Scalar u -> Integer
  Totality: total
  Visibility: public export
fromInteger : Integer -> Scalar u
  Totality: total
  Visibility: public export
0 AttoSeconds : Type
  Totality: total
  Visibility: public export
0 AttoSecondsPerRun : Type
  Totality: total
  Visibility: public export
0 Runs : Type
  Totality: total
  Visibility: public export
plus : Scalar u -> Scalar u -> Scalar u
  Totality: total
  Visibility: public export
minus : Scalar u -> Scalar u -> Scalar u
  Totality: total
  Visibility: public export
scalarSum : Foldable t => t (Scalar u) -> Scalar u
  Totality: total
  Visibility: public export
mult : Scalar u1 -> Scalar u2 -> Scalar (times u1 u2)
  Totality: total
  Visibility: public export
div : Scalar u1 -> Scalar u2 -> Scalar (u1 `div` u2)
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 9
posLength : Vect (S n) a -> Scalar (U 0 0)
  Totality: total
  Visibility: public export
fromFemtoSeconds : Integer -> AttoSeconds
  Totality: total
  Visibility: public export
fromPicoSeconds : Integer -> AttoSeconds
  Totality: total
  Visibility: public export
fromNanoSeconds : Integer -> AttoSeconds
  Totality: total
  Visibility: public export
fromMicroSeconds : Integer -> AttoSeconds
  Totality: total
  Visibility: public export
fromMilliSeconds : Integer -> AttoSeconds
  Totality: total
  Visibility: public export
fromSeconds : Integer -> AttoSeconds
  Totality: total
  Visibility: public export
fromClock : Clock Duration -> AttoSeconds
  Totality: total
  Visibility: public export
timeDelta : Clock t -> Clock t -> AttoSeconds
  Totality: total
  Visibility: export
toFloat : Scalar u -> Double
  Totality: total
  Visibility: export
record Measured : Type
  A collection of measurements made while benchmarking

  Totality: total
  Visibility: public export
  Constructor: 
MkMeasured : Runs -> Bool -> Clock Monotonic -> Clock Monotonic -> AttoSeconds -> AttoSecondsPerRun -> AttoSeconds -> AttoSecondsPerRun -> Measured

  Projections:
  
.avrgCPU : Measured -> AttoSecondsPerRun
  Average CPU time elapsed per iteration
  
.avrgTime : Measured -> AttoSecondsPerRun
  Average wall clock time elapsed per iteration
  
.cpuOnly : Measured -> Bool
  True, if we are interested only in the CPU time
  
.cpuTime : Measured -> AttoSeconds
  Total CPU time elapsed
  
.iterations : Measured -> Runs
  Number of iterations
  
.startTime : Measured -> Clock Monotonic
  Wall clock time when starting the measurement
  
.stopTime : Measured -> Clock Monotonic
  Wall clock time when stopping the measurement
  
.totalTime : Measured -> AttoSeconds
  Total wall clock time elapsed in atto seconds
.iterations : Measured -> Runs
  Number of iterations

  Totality: total
  Visibility: public export
iterations : Measured -> Runs
  Number of iterations

  Totality: total
  Visibility: public export
.cpuOnly : Measured -> Bool
  True, if we are interested only in the CPU time

  Totality: total
  Visibility: public export
cpuOnly : Measured -> Bool
  True, if we are interested only in the CPU time

  Totality: total
  Visibility: public export
.startTime : Measured -> Clock Monotonic
  Wall clock time when starting the measurement

  Totality: total
  Visibility: public export
startTime : Measured -> Clock Monotonic
  Wall clock time when starting the measurement

  Totality: total
  Visibility: public export
.stopTime : Measured -> Clock Monotonic
  Wall clock time when stopping the measurement

  Totality: total
  Visibility: public export
stopTime : Measured -> Clock Monotonic
  Wall clock time when stopping the measurement

  Totality: total
  Visibility: public export
.totalTime : Measured -> AttoSeconds
  Total wall clock time elapsed in atto seconds

  Totality: total
  Visibility: public export
totalTime : Measured -> AttoSeconds
  Total wall clock time elapsed in atto seconds

  Totality: total
  Visibility: public export
.avrgTime : Measured -> AttoSecondsPerRun
  Average wall clock time elapsed per iteration

  Totality: total
  Visibility: public export
avrgTime : Measured -> AttoSecondsPerRun
  Average wall clock time elapsed per iteration

  Totality: total
  Visibility: public export
.cpuTime : Measured -> AttoSeconds
  Total CPU time elapsed

  Totality: total
  Visibility: public export
cpuTime : Measured -> AttoSeconds
  Total CPU time elapsed

  Totality: total
  Visibility: public export
.avrgCPU : Measured -> AttoSecondsPerRun
  Average CPU time elapsed per iteration

  Totality: total
  Visibility: public export
avrgCPU : Measured -> AttoSecondsPerRun
  Average CPU time elapsed per iteration

  Totality: total
  Visibility: public export
tot : Measured -> AttoSeconds
  Totality: total
  Visibility: export
avrg : Measured -> AttoSecondsPerRun
  Totality: total
  Visibility: export
record Result : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkResult : String -> List Measured -> Result

  Projections:
  
.name : Result -> String
  
.runs : Result -> List Measured
.name : Result -> String
  Totality: total
  Visibility: public export
name : Result -> String
  Totality: total
  Visibility: public export
.runs : Result -> List Measured
  Totality: total
  Visibility: public export
runs : Result -> List Measured
  Totality: total
  Visibility: public export