equal
deleted
inserted
replaced
7 |
7 |
8 signature SLEDGEHAMMER_COMPRESS = |
8 signature SLEDGEHAMMER_COMPRESS = |
9 sig |
9 sig |
10 type isar_proof = Sledgehammer_Proof.isar_proof |
10 type isar_proof = Sledgehammer_Proof.isar_proof |
11 type preplay_time = Sledgehammer_Preplay.preplay_time |
11 type preplay_time = Sledgehammer_Preplay.preplay_time |
12 val compress_proof : |
12 val compress_and_preplay_proof : |
13 bool -> Proof.context -> string -> string -> bool -> Time.time option |
13 bool -> Proof.context -> string -> string -> bool -> Time.time option |
14 -> real -> isar_proof -> isar_proof * (bool * preplay_time) |
14 -> real -> isar_proof -> isar_proof * (bool * preplay_time) |
15 end |
15 end |
16 |
16 |
17 structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS = |
17 structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS = |
44 end |
44 end |
45 fun pop_max tab = pop tab (the (Inttab.max_key tab)) |
45 fun pop_max tab = pop tab (the (Inttab.max_key tab)) |
46 fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab |
46 fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab |
47 |
47 |
48 (* Main function for compresing proofs *) |
48 (* Main function for compresing proofs *) |
49 fun compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout |
49 fun compress_and_preplay_proof debug ctxt type_enc lam_trans preplay |
50 isar_compress proof = |
50 preplay_timeout isar_compress proof = |
51 let |
51 let |
52 (* 60 seconds seems like a good interpreation of "no timeout" *) |
52 (* 60 seconds seems like a good interpreation of "no timeout" *) |
53 val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) |
53 val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) |
54 |
54 |
55 (* handle metis preplay fail *) |
55 (* handle metis preplay fail *) |