52 |
52 |
53 val liness' = Ctr_Sugar_Util.transpose (map pad liness0) |
53 val liness' = Ctr_Sugar_Util.transpose (map pad liness0) |
54 |
54 |
55 val css = clasimpset_rule_table_of ctxt |
55 val css = clasimpset_rule_table_of ctxt |
56 val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css |
56 val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css |
57 val name_tabs = build_name_tables (nickname_of_thm ctxt) facts |
57 val name_tabs = build_name_tables nickname_of_thm facts |
58 |
58 |
59 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
59 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
60 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
60 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
61 val str_of_method = enclose " " ": " |
61 val str_of_method = enclose " " ": " |
62 |
62 |
88 val name = |
88 val name = |
89 (case names |> filter (curry (op <>) "") |> distinct (op =) of |
89 (case names |> filter (curry (op <>) "") |> distinct (op =) of |
90 [name] => name |
90 [name] => name |
91 | names => error ("Input files out of sync: facts " ^ commas (map quote names) ^ ".")) |
91 | names => error ("Input files out of sync: facts " ^ commas (map quote names) ^ ".")) |
92 val th = |
92 val th = |
93 case find_first (fn (_, th) => nickname_of_thm ctxt th = name) facts of |
93 case find_first (fn (_, th) => nickname_of_thm th = name) facts of |
94 SOME (_, th) => th |
94 SOME (_, th) => th |
95 | NONE => error ("No fact called \"" ^ name ^ "\".") |
95 | NONE => error ("No fact called \"" ^ name ^ "\".") |
96 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
96 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
97 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt |
97 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt |
98 val isar_deps = these (isar_dependencies_of ctxt name_tabs th) |
98 val isar_deps = these (isar_dependencies_of name_tabs th) |
99 val suggss = isar_deps :: suggss0 |
99 val suggss = isar_deps :: suggss0 |
100 val facts = facts |> filter (fn (_, th') => thm_less (th', th)) |
100 val facts = facts |> filter (fn (_, th') => thm_less (th', th)) |
101 |
101 |
102 (* adapted from "mirabelle_sledgehammer.ML" *) |
102 (* adapted from "mirabelle_sledgehammer.ML" *) |
103 fun set_file_name method (SOME dir) = |
103 fun set_file_name method (SOME dir) = |
114 if null facts then |
114 if null facts then |
115 (str_of_method method ^ "Skipped", 0) |
115 (str_of_method method ^ "Skipped", 0) |
116 else |
116 else |
117 let |
117 let |
118 fun nickify ((_, stature), th) = |
118 fun nickify ((_, stature), th) = |
119 ((K (encode_str (nickname_of_thm ctxt th)), stature), th) |
119 ((K (encode_str (nickname_of_thm th)), stature), th) |
120 |
120 |
121 val facts = |
121 val facts = |
122 suggs |
122 suggs |
123 |> find_suggested_facts ctxt facts |
123 |> find_suggested_facts ctxt facts |
124 |> map (fact_of_raw_fact #> nickify) |
124 |> map (fact_of_raw_fact #> nickify) |