@@ -0,0 +1,230 @@
1+-- ---------------------------------------------------------------- [ Perf.idr ]
3+-- Copyright : (c) Jan de Muijnck-Hughes
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| A naive performance effect for gathering data about the
7+||| performance of effectful programmes.
17+-- ---------------------------------------------------- [ Timer Data Structure ]
25+ splits : List (Integer, Maybe String)
27+displayTimer : Timer -> String
28+displayTimer (MkTimer d a z bcd) = unlines
29+ [ unwords ["Timer:", d]
30+ , unwords ["\tStart:\t", show a, (displaySplits bcd)]
31+ , unwords ["\tStop:\t", show z]
32+ , unwords ["\tDifference:\t", show (z - a)]
35+ displaySplit : (Integer, Maybe String) -> String
36+ displaySplit (v, Nothing) = with List unwords ["\tSplit:\t",show v]
37+ displaySplit (v, Just msg) = with List unwords ["\tSplit:\t",show v, show msg]
39+ displaySplits : List (Integer, Maybe String) -> String
40+ displaySplits Nil = ""
41+ displaySplits ss = "\n" ++ unlines (map displaySplit $ reverse ss)
44+defaultTimer : String -> Timer
45+defaultTimer n = MkTimer n 0 0 Nil
47+-- ---------------------------------------------------------------- [ Resource ]
49+||| Performance Metrics to keep during program lifetime.
51+ constructor MkPMetrics
54+ counters : List (String, Nat)
55+ timers : List (String, Timer)
57+ stamps : List (String, Integer)
60+instance Default PMetrics where
61+ default = MkPMetrics False False Nil Nil 0 Nil
63+displayPerfMetrics : PMetrics -> String
64+displayPerfMetrics (MkPMetrics c l cs ts _ ss) =
65+ unlines [ "Perf Data:"
66+ , unlines $ map displayMarker cs
67+ , unlines $ map (\(x,y) => displayTimer y) ts
68+ , unlines $ map displayMarker ss]
70+ displayMarker : Show a => Pair String a -> String
71+ displayMarker (d,v) = unwords [show v, "\t<==\t", show d]
73+-- ------------------------------------------------------- [ Utility functions ]
75+incCounter' : String -> PMetrics -> PMetrics
76+incCounter' x st = record {counters = cs} st
78+ cs : List (String, Nat)
79+ cs = map (\(y,c) => if x == y then (y,S c) else (y,c)) (counters st)
82+data TOpt = START | STOP | SPLIT
84+displayTimerOpt : TOpt -> String
85+displayTimerOpt START = "Starting"
86+displayTimerOpt STOP = "Stopping"
87+displayTimerOpt SPLIT = "Splitting"
89+timerStuff' : TOpt -> Integer -> String -> Maybe String -> PMetrics -> PMetrics
90+timerStuff' opt val x msg st = record {timers = ts} st
92+ doThing : (String,Timer) -> (String,Timer)
97+ START => MkPair y $ record {start = val} t
98+ STOP => MkPair y $ record {stop = val} t
99+ SPLIT => MkPair y $ record {splits = (val, msg) :: splits t} t
101+ ts : List (String, Timer)
102+ ts = map doThing (timers st)
105+perfLog : PMetrics -> String -> IO ()
108+ then putStrLn $ unwords ["PERF:", msg]
111+-- ------------------------------------------------------- [ Effect Definition ]
113+data Perf : Effect where
114+ GetMetrics : sig Perf (PMetrics) (PMetrics)
115+ TurnOn : Bool -> sig Perf () (PMetrics) (PMetrics)
116+ MkCounter : String -> sig Perf () (PMetrics) (PMetrics)
117+ IncCounter : String -> sig Perf () (PMetrics) (PMetrics)
118+ Timestamp : String -> sig Perf () (PMetrics) (PMetrics)
119+ MkStopWatch : String -> sig Perf () (PMetrics) (PMetrics)
120+ TimerStuff : TOpt -> String -> Maybe String -> sig Perf () (PMetrics) (PMetrics)
122+-- ---------------------------------------------------------- [ Handler for IO ]
124+instance Handler Perf IO where
125+ handle res (TurnOn b) k = do
127+ let res' = record {canPerf = True, livePerf = b, stime = v} res
128+ perfLog res' $ unwords [ "Turning on Perf with at", show v]
131+ handle res (GetMetrics) k = k res res
133+ handle res (MkCounter n) k = do
134+ if not (canPerf res)
137+ let res' = record {counters = (n,Z) :: counters res} res
138+ perfLog res' $ unwords ["Creating counter:", show n]
141+ handle res (IncCounter n) k = do
142+ if not (canPerf res)
145+ let res' = incCounter' n res
146+ perfLog res' $ unwords ["Incriminating counter:", show n]
149+ handle res (MkStopWatch n) k = do
150+ if not (canPerf res)
153+ let res' = record {timers = (n, defaultTimer n) :: timers res} res
154+ perfLog res' $ unwords ["Creating Timer:", show n]
157+ handle res (TimerStuff opt n msg) k = do
159+ if not (canPerf res)
162+ let res' = timerStuff' opt v n msg res
163+ perfLog res' $ unwords [displayTimerOpt opt, "timer", show n, "at", show v, fromMaybe "" msg]
166+ handle res (Timestamp s) k = do
168+ let stamp = v - (stime res)
169+ if not (canPerf res)
172+ let res' = record {stamps = (s,stamp) :: stamps res} res
173+ perfLog res' $ unlines [ "Creating Timestamp:"
174+ , "\tTIMESTAMP:", show v
175+ , "\tMESSAGE:", show s]
178+-- ------------------------------------------------------- [ Effect Descriptor ]
181+PERF = MkEff PMetrics Perf
183+-- --------------------------------------------------------------------- [ API ]
185+||| Turn on performance metrics.
186+collectPMetricsOnly : Eff () [PERF]
187+collectPMetricsOnly = call $ TurnOn False
189+collectPMetrics : Bool -> Eff () [PERF]
190+collectPMetrics b = call $ TurnOn b
192+||| Turn on performance metrics and show during operation
193+collectPMetricsAndShow : Eff () [PERF]
194+collectPMetricsAndShow = call $ TurnOn True
196+||| Return gatheres metrics
197+getPerfMetrics : Eff PMetrics [PERF]
198+getPerfMetrics = call $ GetMetrics
201+mkCounter : String -> Eff () [PERF]
202+mkCounter n = call $ MkCounter n
204+||| Increment the counter
205+incCounter : String -> Eff () [PERF]
206+incCounter n = call $ IncCounter n
208+mkTimer : String -> Eff () [PERF]
209+mkTimer n = call $ MkStopWatch n
212+stopTimer : String -> Eff () [PERF]
213+stopTimer n = call $ TimerStuff STOP n Nothing
216+startTimer : String -> Eff () [PERF]
217+startTimer n = call $ TimerStuff START n Nothing
220+splitTimer : String -> Eff () [PERF]
221+splitTimer n = call $ TimerStuff SPLIT n Nothing
223+splitTimerMsg : String -> String -> Eff () [PERF]
224+splitTimerMsg n msg = call $ TimerStuff SPLIT n (Just msg)
226+||| Create a time stamp.
227+timestamp : String -> Eff () [PERF]
228+timestamp msg = call $ Timestamp msg
230+-- --------------------------------------------------------------------- [ EOF ]