1structure Count :> Count =
2struct
3
4(*---------------------------------------------------------------------------*
5 * Support for monitoring how many theorems (and of what kind) are proved    *
6 * in a session. The numbers returned are not "secure", since the counter    *
7 * manipulation routines are visible to all.                                 *
8 *---------------------------------------------------------------------------*)
9
10val counting = ref false
11fun counting_thms b = counting := b
12val inc = Portable.inc
13
14datatype rule =
15   Abs
16 | Alpha
17 | ApTerm
18 | ApThm
19 | Assume
20 | Axiom
21 | Beta
22 | Ccontr
23 | Choose
24 | Conj
25 | Conjunct1
26 | Conjunct2
27 | Definition
28 | Disch
29 | Disj1
30 | Disj2
31 | DisjCases
32 | Disk
33 | EqImpRule
34 | EqMp
35 | Exists
36 | Gen
37 | GenAbs
38 | Inst
39 | InstType
40 | MkComb
41 | Mp
42 | NotElim
43 | NotIntro
44 | Oracle
45 | Refl
46 | Spec
47 | Subst
48 | Sym
49 | Trans
50
51val count =
52   {ABS = ref 0,
53    ALPHA = ref 0,
54    AP_TERM = ref 0,
55    AP_THM = ref 0,
56    ASSUME = ref 0,
57    AXIOM = ref 0,
58    BETA_CONV = ref 0,
59    CCONTR = ref 0,
60    CHOOSE = ref 0,
61    CONJ = ref 0,
62    CONJUNCT1 = ref 0,
63    CONJUNCT2 = ref 0,
64    DEFINITION = ref 0,
65    DISCH = ref 0,
66    DISJ1 = ref 0,
67    DISJ2 = ref 0,
68    DISJ_CASES = ref 0,
69    EQ_IMP_RULE = ref 0,
70    EQ_MP = ref 0,
71    EXISTS = ref 0,
72    FROM_DISK = ref 0,
73    GEN = ref 0,
74    GEN_ABS = ref 0,
75    INST = ref 0,
76    INST_TYPE = ref 0,
77    MK_COMB = ref 0,
78    MP = ref 0,
79    NOT_ELIM = ref 0,
80    NOT_INTRO = ref 0,
81    ORACLE = ref 0,
82    REFL = ref 0,
83    SPEC = ref 0,
84    SUBST = ref 0,
85    SYM = ref 0,
86    TOTAL = ref 0,
87    TRANS = ref 0}
88
89fun inc_count R =
90  if !counting
91  then inc ((case R of
92               Assume     => #ASSUME
93             | Abs        => #ABS
94             | Alpha      => #ALPHA
95             | ApTerm     => #AP_TERM
96             | ApThm      => #AP_THM
97             | Axiom      => #AXIOM
98             | Beta       => #BETA_CONV
99             | Ccontr     => #CCONTR
100             | Choose     => #CHOOSE
101             | Conj       => #CONJ
102             | Conjunct1  => #CONJUNCT1
103             | Conjunct2  => #CONJUNCT2
104             | Definition => #DEFINITION
105             | Disch      => #DISCH
106             | Disj1      => #DISJ1
107             | Disj2      => #DISJ2
108             | DisjCases  => #DISJ_CASES
109             | Disk       => #FROM_DISK
110             | EqImpRule  => #EQ_IMP_RULE
111             | EqMp       => #EQ_MP
112             | Exists     => #EXISTS
113             | Gen        => #GEN
114             | GenAbs     => #GEN_ABS
115             | Inst       => #INST
116             | InstType   => #INST_TYPE
117             | MkComb     => #MK_COMB
118             | Mp         => #MP
119             | NotElim    => #NOT_ELIM
120             | NotIntro   => #NOT_INTRO
121             | Oracle     => #ORACLE
122             | Refl       => #REFL
123             | Spec       => #SPEC
124             | Subst      => #SUBST
125             | Sym        => #SYM
126             | Trans      => #TRANS) count)
127  else ()
128
129local
130   val l = [#ABS, #ALPHA, #AP_TERM, #AP_THM, #ASSUME, #BETA_CONV, #CCONTR,
131            #CHOOSE, #CONJ, #CONJUNCT1, #CONJUNCT2, #DISCH, #DISJ1, #DISJ2,
132            #DISJ_CASES, #EQ_IMP_RULE, #EQ_MP, #EXISTS, #GEN, #GEN_ABS, #INST,
133            #INST_TYPE, #MK_COMB, #MP, #NOT_ELIM, #NOT_INTRO, #REFL, #SPEC,
134            #SUBST, #SYM, #TRANS]
135in
136   fun reset_thm_count () =
137      List.app (fn f => f count := 0)
138        (l @ [#AXIOM, #DEFINITION, #FROM_DISK, #ORACLE])
139   fun prims () = List.foldl (fn (f, c) => !(f count) + c) 0 l
140end
141
142fun axioms ()    = !(#AXIOM count)
143fun defns ()     = !(#DEFINITION count)
144fun from_disk () = !(#FROM_DISK count)
145fun oracles ()   = !(#ORACLE count)
146
147fun total () = axioms () + defns () + from_disk () + oracles () + prims ()
148
149fun thm_count () =
150   {ABS         = !(#ABS count),
151    ALPHA       = !(#ALPHA count),
152    AP_TERM     = !(#AP_TERM count),
153    AP_THM      = !(#AP_THM count),
154    ASSUME      = !(#ASSUME count),
155    BETA_CONV   = !(#BETA_CONV count),
156    CCONTR      = !(#CCONTR count),
157    CHOOSE      = !(#CHOOSE count),
158    CONJ        = !(#CONJ count),
159    CONJUNCT1   = !(#CONJUNCT1 count),
160    CONJUNCT2   = !(#CONJUNCT2 count),
161    DISCH       = !(#DISCH count),
162    DISJ1       = !(#DISJ1 count),
163    DISJ2       = !(#DISJ2 count),
164    DISJ_CASES  = !(#DISJ_CASES count),
165    EQ_IMP_RULE = !(#EQ_IMP_RULE count),
166    EQ_MP       = !(#EQ_MP count),
167    EXISTS      = !(#EXISTS count),
168    GEN         = !(#GEN count),
169    GEN_ABS     = !(#GEN_ABS count),
170    INST        = !(#INST count),
171    INST_TYPE   = !(#INST_TYPE count),
172    MK_COMB     = !(#MK_COMB count),
173    MP          = !(#MP count),
174    NOT_ELIM    = !(#NOT_ELIM count),
175    NOT_INTRO   = !(#NOT_INTRO count),
176    REFL        = !(#REFL count),
177    SPEC        = !(#SPEC count),
178    SUBST       = !(#SUBST count),
179    SYM         = !(#SYM count),
180    TRANS       = !(#TRANS count),
181    axiom       = !(#AXIOM count),
182    definition  = !(#DEFINITION count),
183    from_disk   = !(#FROM_DISK count),
184    oracle      = !(#ORACLE count),
185    total       = total ()}
186
187type meter = {axioms: int, defns: int, disk: int, oracles: int, prims: int}
188
189fun mk_meter () =
190   (counting_thms true;
191    {axioms = axioms (),
192     defns = defns (),
193     disk = from_disk (),
194     oracles = oracles (),
195     prims = prims ()})
196
197fun read {axioms = a0, defns = d0, disk = f0, oracles = or0, prims = p0} =
198   let
199      val {axioms, defns, disk, oracles, prims} = mk_meter ()
200   in
201      {axioms = axioms-a0,
202       defns = defns-d0,
203       disk = disk-f0,
204       oracles = oracles-or0,
205       prims = prims-p0}
206   end
207
208local
209   fun isay (s, i) = Lib.say (s ^ ": " ^ Lib.int_to_string i)
210in
211   fun report {axioms, defns, disk, oracles, prims} =
212     (List.app isay
213         [("Axioms", axioms),
214          (", Defs", defns),
215          (", Disk", disk),
216          (", Orcl", oracles),
217          (", Prims", prims),
218          ("; Total", axioms + defns + disk + oracles + prims)]
219      ; Lib.say "\n")
220end
221
222fun apply f x =
223   let
224      val m = mk_meter ()
225      val res = Lib.time f x handle e => (report (read m); raise e)
226   in
227      report (read m); res
228   end
229
230end
231