Theory HOL-Eisbach.Eisbach_Tools
1
6
7theory Eisbach_Tools
8imports Eisbach
9begin
10
11ML ‹
12local
13
14fun trace_method parser print =
15 Scan.lift (Args.mode "dummy") -- parser >>
16 (fn (dummy, x) => fn ctxt => SIMPLE_METHOD (fn st =>
17 (if dummy orelse not (Method.detect_closure_state st)
18 then tracing (print ctxt x) else ();
19 all_tac st)));
20
21fun setup_trace_method binding parser print =
22 Method.setup binding
23 (trace_method parser (fn ctxt => fn x => Binding.name_of binding ^ ": " ^ print ctxt x))
24 "";
25
26in
27
28val _ =
29 Theory.setup
30 (setup_trace_method \<^binding>‹print_fact›
31 (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms)
32 (fn ctxt => fn (tok, thms) =>
33
34 Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #>
35 setup_trace_method \<^binding>‹print_term›
36 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
37 (fn ctxt => fn (tok, t) =>
38
39 Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #>
40 setup_trace_method \<^binding>‹print_type›
41 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.typ)
42 (fn ctxt => fn (tok, t) =>
43
44 Token.unparse tok ^ ": " ^ Syntax.string_of_typ ctxt t));
45
46end
47›
48
49ML ‹
50 fun try_map v seq =
51 (case try Seq.pull seq of
52 SOME (SOME (x, seq')) => Seq.make (fn () => SOME(x, try_map v seq'))
53 | SOME NONE => Seq.empty
54 | NONE => v);
55›
56
57method_setup catch = ‹
58 Method.text_closure -- Method.text_closure >>
59 (fn (text, text') => fn ctxt => fn using => fn st =>
60 let
61 val method = Method.evaluate_runtime text ctxt using;
62 val backup_results = Method.evaluate_runtime text' ctxt using st;
63 in
64 (case try method st of
65 SOME seq => try_map backup_results seq
66 | NONE => backup_results)
67 end)
68›
69
70ML ‹
71 fun uncurry_rule thm = Conjunction.uncurry_balanced (Thm.nprems_of thm) thm;
72 fun curry_rule thm =
73 if Thm.no_prems thm then thm
74 else
75 let val conjs = Logic.dest_conjunctions (Thm.major_prem_of thm);
76 in Conjunction.curry_balanced (length conjs) thm end;
77›
78
79attribute_setup uncurry = ‹Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))›
80attribute_setup curry = ‹Scan.succeed (Thm.rule_attribute [] (K curry_rule))›
81
82end
83