22 -> int list list * (string * locality) list vector |
22 -> int list list * (string * locality) list vector |
23 val apply_on_subgoal : int -> int -> string |
23 val apply_on_subgoal : int -> int -> string |
24 val command_call : string -> string list -> string |
24 val command_call : string -> string list -> string |
25 val try_command_line : string -> string -> string |
25 val try_command_line : string -> string -> string |
26 val minimize_line : ('a list -> string) -> 'a list -> string |
26 val minimize_line : ('a list -> string) -> 'a list -> string |
27 val metis_proof_text : metis_params -> text_result |
27 val split_used_facts : |
|
28 (string * locality) list |
|
29 -> (string * locality) list * (string * locality) list |
28 val isar_proof_text : isar_params -> metis_params -> text_result |
30 val isar_proof_text : isar_params -> metis_params -> text_result |
29 val proof_text : bool -> isar_params -> metis_params -> text_result |
31 val proof_text : bool -> isar_params -> metis_params -> text_result |
30 end; |
32 end; |
31 |
33 |
32 structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = |
34 structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = |
157 | add_fact _ _ = I |
159 | add_fact _ _ = I |
158 |
160 |
159 fun used_facts_in_tstplike_proof fact_names = |
161 fun used_facts_in_tstplike_proof fact_names = |
160 atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names) |
162 atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names) |
161 |
163 |
162 fun used_facts fact_names = |
164 val split_used_facts = |
163 used_facts_in_tstplike_proof fact_names |
165 List.partition (curry (op =) Chained o snd) |
164 #> List.partition (curry (op =) Chained o snd) |
|
165 #> pairself (sort_distinct (string_ord o pairself fst)) |
166 #> pairself (sort_distinct (string_ord o pairself fst)) |
166 |
167 |
167 fun metis_proof_text (banner, full_types, minimize_command, |
168 fun metis_proof_text (banner, full_types, minimize_command, |
168 tstplike_proof, fact_names, goal, i) = |
169 tstplike_proof, fact_names, goal, i) = |
169 let |
170 let |
170 val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof |
171 val (chained_lemmas, other_lemmas) = |
|
172 split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof) |
171 val n = Logic.count_prems (prop_of goal) |
173 val n = Logic.count_prems (prop_of goal) |
172 in |
174 in |
173 (metis_line banner full_types i n (map fst other_lemmas) ^ |
175 (metis_line banner full_types i n (map fst other_lemmas) ^ |
174 minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), |
176 minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), |
175 other_lemmas @ chained_lemmas) |
177 other_lemmas @ chained_lemmas) |
910 do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ |
912 do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ |
911 (if n <> 1 then "next" else "qed") |
913 (if n <> 1 then "next" else "qed") |
912 in do_proof end |
914 in do_proof end |
913 |
915 |
914 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
916 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
915 (other_params as (_, full_types, _, tstplike_proof, |
917 (metis_params as (_, full_types, _, tstplike_proof, |
916 fact_names, goal, i)) = |
918 fact_names, goal, i)) = |
917 let |
919 let |
918 val (params, hyp_ts, concl_t) = strip_subgoal goal i |
920 val (params, hyp_ts, concl_t) = strip_subgoal goal i |
919 val frees = fold Term.add_frees (concl_t :: hyp_ts) [] |
921 val frees = fold Term.add_frees (concl_t :: hyp_ts) [] |
920 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] |
922 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] |
921 val n = Logic.count_prems (prop_of goal) |
923 val n = Logic.count_prems (prop_of goal) |
922 val (one_line_proof, lemma_names) = metis_proof_text other_params |
924 val (one_line_proof, lemma_names) = metis_proof_text metis_params |
923 fun isar_proof_for () = |
925 fun isar_proof_for () = |
924 case isar_proof_from_tstplike_proof pool ctxt full_types tfrees |
926 case isar_proof_from_tstplike_proof pool ctxt full_types tfrees |
925 isar_shrink_factor tstplike_proof conjecture_shape fact_names |
927 isar_shrink_factor tstplike_proof conjecture_shape fact_names |
926 params frees |
928 params frees |
927 |> redirect_proof hyp_ts concl_t |
929 |> redirect_proof hyp_ts concl_t |
938 else |
940 else |
939 try isar_proof_for () |
941 try isar_proof_for () |
940 |> the_default "\nWarning: The Isar proof construction failed." |
942 |> the_default "\nWarning: The Isar proof construction failed." |
941 in (one_line_proof ^ isar_proof, lemma_names) end |
943 in (one_line_proof ^ isar_proof, lemma_names) end |
942 |
944 |
943 fun proof_text isar_proof isar_params other_params = |
945 fun proof_text isar_proof isar_params metis_params = |
944 (if isar_proof then isar_proof_text isar_params else metis_proof_text) |
946 (if isar_proof then isar_proof_text isar_params else metis_proof_text) |
945 other_params |
947 metis_params |
946 |
948 |
947 end; |
949 end; |