# Theory Statistics

```section ‹Collecting Statistics about Algorithms›
theory Statistics
imports Main
begin

text ‹
This theory contains an infrastructure to collect statistics about
algorithms by instrumenting the formalization with dummy constants that
get translated to functions that update the statistics as a side-effect.
›

code_printing
(* HACK: code_modules seem to be sorted alphabetically when written to SML.
However, other code_modules will depend on this, so we put an A in front
of the name to get this first. *)
code_module AStatistics ⇀ (SML) ‹
structure Statistics : sig
type stat_entry = string * (unit -> bool) * (unit -> string)

val register_stat : stat_entry -> unit
val get_active_stats : unit -> (string * string) list
val pretty_stats : (string * string) list -> string

end = struct
type stat_entry = string * (unit -> bool) * (unit -> string)
val stats : stat_entry list Unsynchronized.ref = Unsynchronized.ref []

fun register_stat e = stats := e :: !stats

fun get_active_stats () = let
fun flt [] = []
| flt ((n,a,s)::l) = if a () then (n,s ()) :: flt l else flt l

in flt (!stats)
end

fun pretty_stats [] = ""
| pretty_stats ((n,s)::l) = "=== " ^ n ^ " ===\n" ^ s ^ "\n" ^ pretty_stats l
end

(* Argh! Functors not compatible with ML_val command!
functor Timer () : sig
val reset : unit -> unit
val start : unit -> unit
val stop : unit -> unit
val set : Time.time -> unit
val get : unit -> Time.time
val pretty : unit -> string
end = struct

open Time;

val time : Time.time Unsynchronized.ref = Unsynchronized.ref Time.zeroTime
val running : bool Unsynchronized.ref = Unsynchronized.ref false
val start_time : Time.time Unsynchronized.ref = Unsynchronized.ref Time.zeroTime

fun reset () = (
time := Time.zeroTime;
running := false;
start_time := Time.zeroTime
)

fun start () =
if !running then
()
else (
running := true;
start_time := Time.now ()
)

fun this_runs_time () =
if !running then
Time.now () - !start_time
else
Time.zeroTime

fun stop () = (
time := !time + this_runs_time ();
running := false
)

fun get () = !time + this_runs_time ()
fun set t = time := t - this_runs_time ()

fun pretty () = Time.toString (!time) ^ "s"
end
*)

›
code_reserved SML Statistics Timer

end
```