6 evaluate them. |
6 evaluate them. |
7 *) |
7 *) |
8 |
8 |
9 signature MASH_IMPORT = |
9 signature MASH_IMPORT = |
10 sig |
10 sig |
|
11 val import_and_evaluate_mash_suggestions : |
|
12 Proof.context -> theory -> string -> unit |
11 end; |
13 end; |
12 |
14 |
13 structure MaSh_Import : MASH_IMPORT = |
15 structure MaSh_Import : MASH_IMPORT = |
14 struct |
16 struct |
|
17 |
|
18 val unescape_meta = |
|
19 let |
|
20 fun un accum [] = String.implode (rev accum) |
|
21 | un accum (#"\\" :: d1 :: d2 :: d3 :: cs) = |
|
22 (case Int.fromString (String.implode [d1, d2, d3]) of |
|
23 SOME n => un (Char.chr n :: accum) cs |
|
24 | NONE => "" (* error *)) |
|
25 | un _ (#"\\" :: _) = "" (* error *) |
|
26 | un accum (c :: cs) = un (c :: accum) cs |
|
27 in un [] o String.explode end |
|
28 |
|
29 val of_fact_name = unescape_meta |
|
30 |
|
31 val freezeT = Type.legacy_freeze_type; |
|
32 |
|
33 fun freeze (t $ u) = freeze t $ freeze u |
|
34 | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) |
|
35 | freeze (Var ((s, _), T)) = Free (s, freezeT T) |
|
36 | freeze (Const (s, T)) = Const (s, freezeT T) |
|
37 | freeze (Free (s, T)) = Free (s, freezeT T) |
|
38 | freeze t = t |
|
39 |
|
40 val prover_name = ATP_Systems.spassN |
|
41 val max_relevant = 40 |
|
42 val slack_max_relevant = 2 * max_relevant |
|
43 val timeout = 2 |
|
44 |
|
45 fun import_and_evaluate_mash_suggestions ctxt thy file_name = |
|
46 let |
|
47 val params as {relevance_thresholds, ...} = |
|
48 Sledgehammer_Isar.default_params ctxt |
|
49 [("strict", "true"), |
|
50 ("slice", "false"), |
|
51 ("timeout", string_of_int timeout), |
|
52 ("preplay_timeout", "0"), |
|
53 ("minimize", "true")] |
|
54 val is_built_in_const = |
|
55 Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name |
|
56 val relevance_fudge = |
|
57 Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name |
|
58 val relevance_override = {add = [], del = [], only = false} |
|
59 val path = file_name |> Path.explode |
|
60 val lines = path |> File.read_lines |
|
61 val facts = non_tautological_facts_of thy |
|
62 val all_names = facts |> map (Thm.get_name_hint o snd) |
|
63 val i = 1 |
|
64 fun run_sh facts goal = |
|
65 let |
|
66 val facts = |
|
67 facts |> take max_relevant |
|
68 |> map Sledgehammer_Provers.Untranslated_Fact |
|
69 val problem = |
|
70 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1, |
|
71 facts = facts} |
|
72 val prover = |
|
73 Sledgehammer_Run.get_minimizing_prover ctxt |
|
74 Sledgehammer_Provers.Normal prover_name |
|
75 in prover params (K (K (K ""))) problem end |
|
76 fun meng_facts goal = |
|
77 let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i in |
|
78 Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
|
79 slack_max_relevant is_built_in_const relevance_fudge |
|
80 relevance_override [] hyp_ts concl_t |
|
81 end |
|
82 fun find_sugg facts sugg = |
|
83 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts |
|
84 fun sugg_facts facts = |
|
85 map_filter (find_sugg facts o of_fact_name) |
|
86 #> take slack_max_relevant |
|
87 #> map (apfst (apfst (fn name => name ()))) |
|
88 fun hybrid_facts fs1 fs2 = |
|
89 let |
|
90 val fact_eq = (op =) o pairself fst |
|
91 fun score_in f fs = |
|
92 case find_index (curry fact_eq f) fs of |
|
93 ~1 => length fs |
|
94 | j => j |
|
95 fun score_of f = score_in f fs1 + score_in f fs2 |
|
96 in |
|
97 union fact_eq fs1 fs2 |
|
98 |> map (`score_of) |
|
99 |> sort (int_ord o pairself fst) |
|
100 |> map snd |
|
101 |> take max_relevant |
|
102 end |
|
103 fun with_index facts s = |
|
104 (find_index (fn ((s', _), _) => s = s') facts + 1, s) |
|
105 fun index_string (j, s) = s ^ "@" ^ string_of_int j |
|
106 fun print_res label facts {outcome, run_time, used_facts, ...} = |
|
107 tracing (" " ^ label ^ ": " ^ |
|
108 (if is_none outcome then |
|
109 "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ |
|
110 space_implode " " |
|
111 (used_facts |> map (with_index facts o fst) |
|
112 |> sort (int_ord o pairself fst) |
|
113 |> map index_string) |
|
114 else |
|
115 "Failure: " ^ space_implode " " (map (fst o fst) facts) )) |
|
116 fun solve_goal name suggs = |
|
117 let |
|
118 val name = of_fact_name name |
|
119 val _ = tracing ("Goal: " ^ name) |
|
120 val th = |
|
121 case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of |
|
122 SOME (_, th) => th |
|
123 | NONE => error ("No fact called \"" ^ name ^ "\"") |
|
124 val deps = dependencies_of all_names th |
|
125 val goal = th |> prop_of |> freeze |> cterm_of thy |> Goal.init |
|
126 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
|
127 val deps_facts = sugg_facts facts deps |
|
128 val meng_facts = meng_facts goal facts |
|
129 val mash_facts = sugg_facts facts suggs |
|
130 val hybrid_facts = hybrid_facts meng_facts mash_facts |
|
131 val deps_res = run_sh deps_facts goal |
|
132 val meng_res = run_sh meng_facts goal |
|
133 val mash_res = run_sh mash_facts goal |
|
134 val hybrid_res = run_sh hybrid_facts goal |
|
135 in |
|
136 print_res "Dependencies" deps_facts deps_res; |
|
137 print_res "Meng & Paulson" meng_facts meng_res; |
|
138 print_res "MaSh" mash_facts mash_res; |
|
139 print_res "Hybrid" hybrid_facts hybrid_res |
|
140 end |
|
141 val explode_suggs = space_explode " " #> filter_out (curry (op =) "") |
|
142 fun do_line line = |
|
143 case space_explode ":" line of |
|
144 [goal_name, suggs] => solve_goal goal_name (explode_suggs suggs) |
|
145 | _ => () |
|
146 in List.app do_line lines end |
|
147 |
15 end; |
148 end; |