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