11 val simplify_spaces : string -> string |
11 val simplify_spaces : string -> string |
12 val parse_bool_option : bool -> string -> string -> bool option |
12 val parse_bool_option : bool -> string -> string -> bool option |
13 val parse_time_option : string -> string -> Time.time option |
13 val parse_time_option : string -> string -> Time.time option |
14 val subgoal_count : Proof.state -> int |
14 val subgoal_count : Proof.state -> int |
15 val reserved_isar_keyword_table : unit -> unit Symtab.table |
15 val reserved_isar_keyword_table : unit -> unit Symtab.table |
16 val thms_in_proof : string list option -> thm -> string list |
16 val thms_in_proof : unit Symtab.table option -> thm -> string list |
17 end; |
17 end; |
18 |
18 |
19 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
19 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
20 struct |
20 struct |
21 |
21 |
61 fixes that seem to be missing over there; or maybe the two code portions are |
61 fixes that seem to be missing over there; or maybe the two code portions are |
62 not doing the same? *) |
62 not doing the same? *) |
63 fun fold_body_thms thm_name f = |
63 fun fold_body_thms thm_name f = |
64 let |
64 let |
65 fun app n (PBody {thms, ...}) = |
65 fun app n (PBody {thms, ...}) = |
66 thms |> fold (fn (_, (name, prop, body)) => fn x => |
66 thms |> fold (fn (_, (name, _, body)) => fn accum => |
67 let |
67 let |
68 val body' = Future.join body |
68 (* The second disjunct caters for the uncommon case where the proved |
69 val n' = |
69 theorem occurs in its own proof (e.g., |
70 n + (if name = "" orelse |
70 "Transitive_Closure.trancl_into_trancl"). *) |
71 (* uncommon case where the proved theorem occurs twice |
71 val no_name = (name = "" orelse (n = 1 andalso name = thm_name)) |
72 (e.g., "Transitive_Closure.trancl_into_trancl") *) |
72 val accum = |
73 (n = 1 andalso name = thm_name) then |
73 accum |> (if n = 1 andalso not no_name then f name else I) |
74 0 |
74 val n = n + (if no_name then 0 else 1) |
75 else |
75 in accum |> (if n <= 1 then app n (Future.join body) else I) end) |
76 1) |
|
77 val x' = x |> n' <= 1 ? app n' body' |
|
78 in (x' |> n = 1 ? f (name, prop, body')) end) |
|
79 in fold (app 0) end |
76 in fold (app 0) end |
80 |
77 |
81 fun thms_in_proof all_names th = |
78 fun thms_in_proof all_names th = |
82 let |
79 let |
83 val is_name_ok = |
80 val collect = |
84 case all_names of |
81 case all_names of |
85 SOME names => member (op =) names |
82 SOME names => (fn s => Symtab.defined names s ? insert (op =) s) |
86 | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s)) |
83 | NONE => insert (op =) |
87 fun collect (s, _, _) = is_name_ok s ? insert (op =) s |
|
88 val names = |
84 val names = |
89 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
85 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] |
90 in names end |
86 in names end |
91 |
87 |
92 end; |
88 end; |