246 |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) |
246 |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of) |
247 |> simplify_spaces |
247 |> simplify_spaces |
248 |> maybe_quote), |
248 |> maybe_quote), |
249 ctxt |> Variable.auto_fixes term) |
249 ctxt |> Variable.auto_fixes term) |
250 |
250 |
251 fun with_facts none _ [] [] = none |
251 fun using_facts [] [] = "" |
252 | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss)) |
252 | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss)) |
253 |
|
254 val using_facts = with_facts "" (enclose "using " " ") |
|
255 |
|
256 fun maybe_paren s = s |> String.isSubstring " " s ? enclose "(" ")" |
|
257 fun by_facts meth ls ss = |
|
258 "by " ^ with_facts (maybe_paren meth) (enclose ("(" ^ meth ^ " ") ")") ls ss |
|
259 |
253 |
260 fun is_direct_method (Metis_Method _) = true |
254 fun is_direct_method (Metis_Method _) = true |
261 | is_direct_method Meson_Method = true |
255 | is_direct_method Meson_Method = true |
262 | is_direct_method SMT2_Method = true |
256 | is_direct_method SMT2_Method = true |
|
257 | is_direct_method Simp_Method = true |
263 | is_direct_method _ = false |
258 | is_direct_method _ = false |
264 |
259 |
265 (* Local facts are always passed via "using", which affects "meson" and "metis". This is |
260 (* Local facts are always passed via "using", which affects "meson" and "metis". This is |
266 arguably stylistically superior, because it emphasises the structure of the proof. It is also |
261 arguably stylistically superior, because it emphasises the structure of the proof. It is also |
267 more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" |
262 more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" |
268 and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) |
263 and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) |
269 fun of_method ls ss meth = |
264 fun of_method ls ss meth = |
270 let val direct = is_direct_method meth in |
265 let val direct = is_direct_method meth in |
271 using_facts ls (if direct then [] else ss) ^ |
266 using_facts ls (if direct then [] else ss) ^ |
272 by_facts (string_of_proof_method meth) [] (if direct then ss else []) |
267 "by " ^ string_of_proof_method (if direct then ss else []) meth |
273 end |
268 end |
274 |
269 |
275 fun of_free (s, T) = |
270 fun of_free (s, T) = |
276 maybe_quote s ^ " :: " ^ |
271 maybe_quote s ^ " :: " ^ |
277 maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) |
272 maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) |