900 val nclosed = ref 0 |
900 val nclosed = ref 0 |
901 and ntried = ref 1; |
901 and ntried = ref 1; |
902 |
902 |
903 fun printStats (b, start, tacs) = |
903 fun printStats (b, start, tacs) = |
904 if b then |
904 if b then |
905 writeln (endTiming start ^ " for search. Closed: " |
905 writeln (end_timing start ^ " for search. Closed: " |
906 ^ Int.toString (!nclosed) ^ |
906 ^ Int.toString (!nclosed) ^ |
907 " tried: " ^ Int.toString (!ntried) ^ |
907 " tried: " ^ Int.toString (!ntried) ^ |
908 " tactics: " ^ Int.toString (length tacs)) |
908 " tactics: " ^ Int.toString (length tacs)) |
909 else (); |
909 else (); |
910 |
910 |
1251 val {sign,...} = rep_thm st |
1251 val {sign,...} = rep_thm st |
1252 val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) |
1252 val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) |
1253 val hyps = strip_imp_prems skoprem |
1253 val hyps = strip_imp_prems skoprem |
1254 and concl = strip_imp_concl skoprem |
1254 and concl = strip_imp_concl skoprem |
1255 fun cont (tacs,_,choices) = |
1255 fun cont (tacs,_,choices) = |
1256 let val start = startTiming() |
1256 let val start = start_timing () |
1257 in |
1257 in |
1258 case Seq.pull(EVERY' (rev tacs) i st) of |
1258 case Seq.pull(EVERY' (rev tacs) i st) of |
1259 NONE => (writeln ("PROOF FAILED for depth " ^ |
1259 NONE => (writeln ("PROOF FAILED for depth " ^ |
1260 Int.toString lim); |
1260 Int.toString lim); |
1261 if !trace then error "************************\n" |
1261 if !trace then error "************************\n" |
1262 else (); |
1262 else (); |
1263 backtrack choices) |
1263 backtrack choices) |
1264 | cell => (if (!trace orelse !stats) |
1264 | cell => (if (!trace orelse !stats) |
1265 then writeln (endTiming start ^ " for reconstruction") |
1265 then writeln (end_timing start ^ " for reconstruction") |
1266 else (); |
1266 else (); |
1267 Seq.make(fn()=> cell)) |
1267 Seq.make(fn()=> cell)) |
1268 end |
1268 end |
1269 in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) |
1269 in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) |
1270 end |
1270 end |
1271 handle PROVE => Seq.empty; |
1271 handle PROVE => Seq.empty; |
1272 |
1272 |
1273 (*Public version with fixed depth*) |
1273 (*Public version with fixed depth*) |
1274 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st; |
1274 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st; |
1275 |
1275 |
1276 val depth_limit = ref 20; |
1276 val depth_limit = ref 20; |
1277 |
1277 |
1278 fun blast_tac cs i st = |
1278 fun blast_tac cs i st = |
1279 ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i |
1279 ((DEEPEN (1, !depth_limit) (timing_depth_tac (start_timing ()) cs) 0) i |
1280 THEN flexflex_tac) st |
1280 THEN flexflex_tac) st |
1281 handle TRANS s => |
1281 handle TRANS s => |
1282 ((if !trace then warning ("blast: " ^ s) else ()); |
1282 ((if !trace then warning ("blast: " ^ s) else ()); |
1283 Seq.empty); |
1283 Seq.empty); |
1284 |
1284 |
1294 val {sign,...} = rep_thm st |
1294 val {sign,...} = rep_thm st |
1295 val skoprem = (initialize (theory_of_thm st); |
1295 val skoprem = (initialize (theory_of_thm st); |
1296 fromSubgoal (List.nth(prems_of st, i-1))) |
1296 fromSubgoal (List.nth(prems_of st, i-1))) |
1297 val hyps = strip_imp_prems skoprem |
1297 val hyps = strip_imp_prems skoprem |
1298 and concl = strip_imp_concl skoprem |
1298 and concl = strip_imp_concl skoprem |
1299 in timeap prove (sign, startTiming(), cs, |
1299 in timeap prove (sign, start_timing (), cs, |
1300 [initBranch (mkGoal concl :: hyps, lim)], I) |
1300 [initBranch (mkGoal concl :: hyps, lim)], I) |
1301 end |
1301 end |
1302 handle Subscript => error("There is no subgoal " ^ Int.toString i); |
1302 handle Subscript => error("There is no subgoal " ^ Int.toString i); |
1303 |
1303 |
1304 fun Trygl lim i = trygl (Data.claset()) lim i; |
1304 fun Trygl lim i = trygl (Data.claset()) lim i; |