@@ -0,0 +1,230 @@
1+-- ---------------------------------------------------------------- [ Perf.idr ]
2+-- Module : 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.
8+module Effect.Perf
9+
10+import System
11+
12+import Effects
13+import Effect.Default
14+
15+%access public
16+
17+-- ---------------------------------------------------- [ Timer Data Structure ]
18+
19+||| A Simple timer.
20+record Timer where
21+ constructor MkTimer
22+ desc : String
23+ start : Integer
24+ stop : Integer
25+ splits : List (Integer, Maybe String)
26+
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)]
33+ ]
34+ where
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]
38+
39+ displaySplits : List (Integer, Maybe String) -> String
40+ displaySplits Nil = ""
41+ displaySplits ss = "\n" ++ unlines (map displaySplit $ reverse ss)
42+
43+
44+defaultTimer : String -> Timer
45+defaultTimer n = MkTimer n 0 0 Nil
46+
47+-- ---------------------------------------------------------------- [ Resource ]
48+
49+||| Performance Metrics to keep during program lifetime.
50+record PMetrics where
51+ constructor MkPMetrics
52+ canPerf : Bool
53+ livePerf : Bool
54+ counters : List (String, Nat)
55+ timers : List (String, Timer)
56+ stime : Integer
57+ stamps : List (String, Integer)
58+
59+
60+instance Default PMetrics where
61+ default = MkPMetrics False False Nil Nil 0 Nil
62+
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]
69+ where
70+ displayMarker : Show a => Pair String a -> String
71+ displayMarker (d,v) = unwords [show v, "\t<==\t", show d]
72+
73+-- ------------------------------------------------------- [ Utility functions ]
74+
75+incCounter' : String -> PMetrics -> PMetrics
76+incCounter' x st = record {counters = cs} st
77+ where
78+ cs : List (String, Nat)
79+ cs = map (\(y,c) => if x == y then (y,S c) else (y,c)) (counters st)
80+
81+
82+data TOpt = START | STOP | SPLIT
83+
84+displayTimerOpt : TOpt -> String
85+displayTimerOpt START = "Starting"
86+displayTimerOpt STOP = "Stopping"
87+displayTimerOpt SPLIT = "Splitting"
88+
89+timerStuff' : TOpt -> Integer -> String -> Maybe String -> PMetrics -> PMetrics
90+timerStuff' opt val x msg st = record {timers = ts} st
91+ where
92+ doThing : (String,Timer) -> (String,Timer)
93+ doThing (y,t) =
94+ if not (x == y)
95+ then (y, t)
96+ else case opt of
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
100+
101+ ts : List (String, Timer)
102+ ts = map doThing (timers st)
103+
104+
105+perfLog : PMetrics -> String -> IO ()
106+perfLog res msg =
107+ if livePerf res
108+ then putStrLn $ unwords ["PERF:", msg]
109+ else return ()
110+
111+-- ------------------------------------------------------- [ Effect Definition ]
112+
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)
121+
122+-- ---------------------------------------------------------- [ Handler for IO ]
123+
124+instance Handler Perf IO where
125+ handle res (TurnOn b) k = do
126+ v <- time
127+ let res' = record {canPerf = True, livePerf = b, stime = v} res
128+ perfLog res' $ unwords [ "Turning on Perf with at", show v]
129+ k () (res')
130+
131+ handle res (GetMetrics) k = k res res
132+
133+ handle res (MkCounter n) k = do
134+ if not (canPerf res)
135+ then k () res
136+ else do
137+ let res' = record {counters = (n,Z) :: counters res} res
138+ perfLog res' $ unwords ["Creating counter:", show n]
139+ k () (res')
140+
141+ handle res (IncCounter n) k = do
142+ if not (canPerf res)
143+ then k () res
144+ else do
145+ let res' = incCounter' n res
146+ perfLog res' $ unwords ["Incriminating counter:", show n]
147+ k () (res')
148+
149+ handle res (MkStopWatch n) k = do
150+ if not (canPerf res)
151+ then k () res
152+ else do
153+ let res' = record {timers = (n, defaultTimer n) :: timers res} res
154+ perfLog res' $ unwords ["Creating Timer:", show n]
155+ k () (res')
156+
157+ handle res (TimerStuff opt n msg) k = do
158+ v <- time
159+ if not (canPerf res)
160+ then k () res
161+ else do
162+ let res' = timerStuff' opt v n msg res
163+ perfLog res' $ unwords [displayTimerOpt opt, "timer", show n, "at", show v, fromMaybe "" msg]
164+ k () (res')
165+
166+ handle res (Timestamp s) k = do
167+ v <- time
168+ let stamp = v - (stime res)
169+ if not (canPerf res)
170+ then k () res
171+ else do
172+ let res' = record {stamps = (s,stamp) :: stamps res} res
173+ perfLog res' $ unlines [ "Creating Timestamp:"
174+ , "\tTIMESTAMP:", show v
175+ , "\tMESSAGE:", show s]
176+ k () (res')
177+
178+-- ------------------------------------------------------- [ Effect Descriptor ]
179+
180+PERF : EFFECT
181+PERF = MkEff PMetrics Perf
182+
183+-- --------------------------------------------------------------------- [ API ]
184+
185+||| Turn on performance metrics.
186+collectPMetricsOnly : Eff () [PERF]
187+collectPMetricsOnly = call $ TurnOn False
188+
189+collectPMetrics : Bool -> Eff () [PERF]
190+collectPMetrics b = call $ TurnOn b
191+
192+||| Turn on performance metrics and show during operation
193+collectPMetricsAndShow : Eff () [PERF]
194+collectPMetricsAndShow = call $ TurnOn True
195+
196+||| Return gatheres metrics
197+getPerfMetrics : Eff PMetrics [PERF]
198+getPerfMetrics = call $ GetMetrics
199+
200+||| Create a counter
201+mkCounter : String -> Eff () [PERF]
202+mkCounter n = call $ MkCounter n
203+
204+||| Increment the counter
205+incCounter : String -> Eff () [PERF]
206+incCounter n = call $ IncCounter n
207+
208+mkTimer : String -> Eff () [PERF]
209+mkTimer n = call $ MkStopWatch n
210+
211+||| Stop a timer
212+stopTimer : String -> Eff () [PERF]
213+stopTimer n = call $ TimerStuff STOP n Nothing
214+
215+||| Start a timer
216+startTimer : String -> Eff () [PERF]
217+startTimer n = call $ TimerStuff START n Nothing
218+
219+||| Split a timer
220+splitTimer : String -> Eff () [PERF]
221+splitTimer n = call $ TimerStuff SPLIT n Nothing
222+
223+splitTimerMsg : String -> String -> Eff () [PERF]
224+splitTimerMsg n msg = call $ TimerStuff SPLIT n (Just msg)
225+
226+||| Create a time stamp.
227+timestamp : String -> Eff () [PERF]
228+timestamp msg = call $ Timestamp msg
229+
230+-- --------------------------------------------------------------------- [ EOF ]