|
1 (* Title: HOL/ex/Sketch_and_Explore.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 chapter \<open>Experimental commands \<^text>\<open>sketch\<close> and \<^text>\<open>explore\<close>\<close> |
|
6 |
|
7 theory Sketch_and_Explore |
|
8 imports Main \<comment> \<open>TODO: generalize existing sledgehammer functions to Pure\<close> |
|
9 keywords "sketch" "explore" :: diag |
|
10 begin |
|
11 |
|
12 ML \<open> |
|
13 fun split_clause t = |
|
14 let |
|
15 val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all t; |
|
16 val assms = Logic.strip_imp_prems horn; |
|
17 val concl = Logic.strip_imp_concl horn; |
|
18 in (fixes, assms, concl) end; |
|
19 |
|
20 fun maybe_quote ctxt = |
|
21 ATP_Util.maybe_quote (Thy_Header.get_keywords' ctxt); |
|
22 |
|
23 fun print_typ ctxt T = |
|
24 T |
|
25 |> Syntax.string_of_typ ctxt |
|
26 |> maybe_quote ctxt; |
|
27 |
|
28 fun print_term ctxt t = |
|
29 t |
|
30 |> singleton (Syntax.uncheck_terms ctxt) |
|
31 |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt |
|
32 \<comment> \<open>TODO pointless to annotate explicit fixes in term\<close> |
|
33 |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |
|
34 |> Sledgehammer_Util.simplify_spaces |
|
35 |> maybe_quote ctxt; |
|
36 |
|
37 fun print_isar_skeleton ctxt indent keyword (fixes, assms, concl) = |
|
38 let |
|
39 val (_, ctxt') = Variable.add_fixes (map fst fixes) ctxt; |
|
40 val prefix = replicate_string indent " "; |
|
41 \<comment> \<open>TODO consider pre-existing indentation -- how?\<close> |
|
42 val prefix_sep = "\n" ^ prefix ^ " and "; |
|
43 val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl; |
|
44 val if_s = if null assms then NONE |
|
45 else SOME (prefix ^ " if " ^ space_implode prefix_sep |
|
46 (map (print_term ctxt') assms)); |
|
47 val for_s = if null fixes then NONE |
|
48 else SOME (prefix ^ " for " ^ space_implode prefix_sep |
|
49 (map (fn (v, T) => v ^ " :: " ^ print_typ ctxt T) fixes)); |
|
50 val s = cat_lines ([show_s] @ map_filter I [if_s, for_s] @ |
|
51 [prefix ^ " " ^ (if is_none if_s then "" else "using that ") ^ "sorry"]); |
|
52 in |
|
53 s |
|
54 end; |
|
55 |
|
56 fun print_sketch ctxt method_text clauses = |
|
57 "proof" ^ method_text :: map (print_isar_skeleton ctxt 2 "show") clauses @ ["qed"]; |
|
58 |
|
59 fun print_exploration ctxt method_text [clause] = |
|
60 ["proof -", print_isar_skeleton ctxt 2 "have" clause, |
|
61 " then show ?thesis", " by" ^ method_text, "qed"] |
|
62 | print_exploration ctxt method_text (clause :: clauses) = |
|
63 "proof -" :: print_isar_skeleton ctxt 2 "have" clause |
|
64 :: map (print_isar_skeleton ctxt 2 "moreover have") clauses |
|
65 @ [" ultimately show ?thesis", " by" ^ method_text, "qed"]; |
|
66 |
|
67 fun coalesce_method_txt [] = "" |
|
68 | coalesce_method_txt [s] = s |
|
69 | coalesce_method_txt (s1 :: s2 :: ss) = |
|
70 if s1 = "(" orelse s1 = "[" |
|
71 orelse s2 = ")" orelse s2 = "]" orelse s2= ":" |
|
72 then s1 ^ coalesce_method_txt (s2 :: ss) |
|
73 else s1 ^ " " ^ coalesce_method_txt (s2 :: ss); |
|
74 |
|
75 fun print_proof_text_from_state print (some_method_ref : ((Method.text * Position.range) * Token.T list) option) state = |
|
76 let |
|
77 val state' = state |
|
78 |> Proof.proof (Option.map fst some_method_ref) |
|
79 |> Seq.the_result "" |
|
80 |
|
81 val { context = ctxt, facts = _, goal } = Proof.goal state'; |
|
82 |
|
83 val ctxt_print = fold (fn opt => Config.put opt false) |
|
84 [show_markup, Printer.show_type_emphasis, show_types, show_sorts, show_consts] ctxt |
|
85 |
|
86 val method_text = case some_method_ref of |
|
87 NONE => "" |
|
88 | SOME (_, toks) => " " ^ coalesce_method_txt (map Token.unparse toks); |
|
89 \<comment> \<open>TODO proper printing required\<close> |
|
90 val goal_props = Logic.strip_imp_prems (Thm.prop_of goal); |
|
91 val clauses = map split_clause goal_props; |
|
92 val lines = if null clauses then |
|
93 if is_none some_method_ref then [" .."] |
|
94 else [" by" ^ method_text] |
|
95 else print ctxt_print method_text clauses; |
|
96 val message = Active.sendback_markup_properties [] (cat_lines lines); |
|
97 in |
|
98 (state |> tap (fn _ => Output.information message)) |
|
99 end |
|
100 |
|
101 val sketch = print_proof_text_from_state print_sketch; |
|
102 |
|
103 fun explore method_ref = print_proof_text_from_state print_exploration (SOME method_ref); |
|
104 |
|
105 fun sketch_cmd some_method_text = |
|
106 Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of) |
|
107 |
|
108 fun explore_cmd method_text = |
|
109 Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of) |
|
110 |
|
111 val _ = |
|
112 Outer_Syntax.command \<^command_keyword>\<open>sketch\<close> |
|
113 "print sketch of Isar proof text after method application" |
|
114 (Scan.option (Scan.trace Method.parse) >> sketch_cmd); |
|
115 |
|
116 val _ = |
|
117 Outer_Syntax.command \<^command_keyword>\<open>explore\<close> |
|
118 "explore proof obligations after method application as Isar proof text" |
|
119 (Scan.trace Method.parse >> explore_cmd); |
|
120 \<close> |
|
121 |
|
122 end |