author | wenzelm |
Fri, 21 Apr 2017 15:26:24 +0200 | |
changeset 65534 | b6250ee6ce79 |
parent 63806 | c54a53ef1873 |
child 67147 | dea94b1aabc3 |
permissions | -rw-r--r-- |
54730 | 1 |
(* Title: Pure/Tools/simplifier_trace.ML |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
2 |
Author: Lars Hupel |
54730 | 3 |
|
4 |
Interactive Simplifier trace. |
|
5 |
*) |
|
6 |
||
7 |
signature SIMPLIFIER_TRACE = |
|
8 |
sig |
|
62983
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
9 |
val disable: Proof.context -> Proof.context |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
10 |
val add_term_breakpoint: term -> Context.generic -> Context.generic |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
11 |
val add_thm_breakpoint: thm -> Context.generic -> Context.generic |
54730 | 12 |
end |
13 |
||
14 |
structure Simplifier_Trace: SIMPLIFIER_TRACE = |
|
15 |
struct |
|
16 |
||
55552 | 17 |
(** context data **) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
18 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
19 |
datatype mode = Disabled | Normal | Full |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
20 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
21 |
fun merge_modes Disabled m = m |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
22 |
| merge_modes Normal Full = Full |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
23 |
| merge_modes Normal _ = Normal |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
24 |
| merge_modes Full _ = Full |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
25 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
26 |
val empty_breakpoints = |
55560 | 27 |
(Item_Net.init (op aconv) single, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
28 |
Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
29 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
30 |
fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
31 |
(Item_Net.merge (term_bs1, term_bs2), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
32 |
Item_Net.merge (thm_bs1, thm_bs2)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
33 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
34 |
structure Data = Generic_Data |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
35 |
( |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
36 |
type T = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
37 |
{max_depth: int, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
38 |
mode: mode, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
39 |
interactive: bool, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
40 |
memory: bool, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
41 |
parent: int, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
42 |
breakpoints: term Item_Net.T * rrule Item_Net.T} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
43 |
val empty = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
44 |
{max_depth = 10, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
45 |
mode = Disabled, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
46 |
interactive = false, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
47 |
memory = true, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
48 |
parent = 0, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
49 |
breakpoints = empty_breakpoints} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
50 |
val extend = I |
55552 | 51 |
fun merge |
52 |
({max_depth = max_depth1, mode = mode1, interactive = interactive1, |
|
53 |
memory = memory1, breakpoints = breakpoints1, ...}: T, |
|
54 |
{max_depth = max_depth2, mode = mode2, interactive = interactive2, |
|
55 |
memory = memory2, breakpoints = breakpoints2, ...}: T) = |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
56 |
{max_depth = Int.max (max_depth1, max_depth2), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
57 |
mode = merge_modes mode1 mode2, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
58 |
interactive = interactive1 orelse interactive2, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
59 |
memory = memory1 andalso memory2, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
60 |
parent = 0, |
55335 | 61 |
breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
62 |
) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
63 |
|
57592 | 64 |
val get_data = Data.get o Context.Proof |
65 |
val put_data = Context.proof_map o Data.put |
|
66 |
||
62983
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
67 |
val disable = |
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
68 |
Config.put simp_trace false #> |
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
69 |
(Context.proof_map o Data.map) |
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
70 |
(fn {max_depth, mode = _, interactive, parent, memory, breakpoints} => |
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
71 |
{max_depth = max_depth, mode = Disabled, interactive = interactive, parent = parent, |
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
72 |
memory = memory, breakpoints = breakpoints}); |
ba9072b303a2
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
wenzelm
parents:
62505
diff
changeset
|
73 |
|
57592 | 74 |
val get_breakpoints = #breakpoints o get_data |
75 |
||
76 |
fun map_breakpoints f = |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
77 |
Data.map |
57592 | 78 |
(fn {max_depth, mode, interactive, parent, memory, breakpoints} => |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
79 |
{max_depth = max_depth, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
80 |
mode = mode, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
81 |
interactive = interactive, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
82 |
memory = memory, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
83 |
parent = parent, |
57592 | 84 |
breakpoints = f breakpoints}) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
85 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
86 |
fun add_term_breakpoint term = |
57592 | 87 |
map_breakpoints (apfst (Item_Net.update term)) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
88 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
89 |
fun add_thm_breakpoint thm context = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
90 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
91 |
val rrules = mk_rrules (Context.proof_of context) [thm] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
92 |
in |
57592 | 93 |
map_breakpoints (apsnd (fold Item_Net.update rrules)) context |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
94 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
95 |
|
57592 | 96 |
fun check_breakpoint (term, rrule) ctxt = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
97 |
let |
57592 | 98 |
val thy = Proof_Context.theory_of ctxt |
99 |
val (term_bs, thm_bs) = get_breakpoints ctxt |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
100 |
|
57592 | 101 |
val term_matches = |
102 |
filter (fn pat => Pattern.matches thy (pat, term)) |
|
103 |
(Item_Net.retrieve_matching term_bs term) |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
104 |
|
57592 | 105 |
val thm_matches = |
106 |
exists (eq_rrule o pair rrule) |
|
107 |
(Item_Net.retrieve_matching thm_bs (Thm.full_prop_of (#thm rrule))) |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
108 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
109 |
(term_matches, thm_matches) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
110 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
111 |
|
55552 | 112 |
|
113 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
114 |
(** config and attributes **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
115 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
116 |
fun config raw_mode interactive max_depth memory = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
117 |
let |
55552 | 118 |
val mode = |
119 |
(case raw_mode of |
|
120 |
"normal" => Normal |
|
121 |
| "full" => Full |
|
122 |
| _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)) |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
123 |
|
55946 | 124 |
val update = Data.map (fn {parent, breakpoints, ...} => |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
125 |
{max_depth = max_depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
126 |
mode = mode, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
127 |
interactive = interactive, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
128 |
memory = memory, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
129 |
parent = parent, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
130 |
breakpoints = breakpoints}) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
131 |
in Thm.declaration_attribute (K update) end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
132 |
|
57041
aceaca232177
consolidate "break_thm" and "break_term" attributes into "simp_break";
Lars Hupel <lars.hupel@mytum.de>
parents:
56333
diff
changeset
|
133 |
fun breakpoint terms = |
aceaca232177
consolidate "break_thm" and "break_term" attributes into "simp_break";
Lars Hupel <lars.hupel@mytum.de>
parents:
56333
diff
changeset
|
134 |
Thm.declaration_attribute (fn thm => add_thm_breakpoint thm o fold add_term_breakpoint terms) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
135 |
|
55552 | 136 |
|
137 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
138 |
(** tracing state **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
139 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
140 |
val futures = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
141 |
Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
142 |
|
55552 | 143 |
|
144 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
145 |
(** markup **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
146 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
147 |
fun output_result (id, data) = |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
55946
diff
changeset
|
148 |
Output.result (Markup.serial_properties id) [data] |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
149 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
150 |
val parentN = "parent" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
151 |
val textN = "text" |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
152 |
val memoryN = "memory" |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
153 |
val successN = "success" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
154 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
155 |
type payload = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
156 |
{props: Properties.T, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
157 |
pretty: Pretty.T} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
158 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
159 |
fun empty_payload () : payload = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
160 |
{props = [], pretty = Pretty.str ""} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
161 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
162 |
fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
163 |
let |
57592 | 164 |
val {mode, interactive, memory, parent, ...} = get_data ctxt |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
165 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
166 |
val eligible = |
55552 | 167 |
(case mode of |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
168 |
Disabled => false |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
169 |
| Normal => triggered |
55552 | 170 |
| Full => true) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
171 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
172 |
val markup' = |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
173 |
if markup = Markup.simp_trace_stepN andalso not interactive |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
174 |
then Markup.simp_trace_logN |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
175 |
else markup |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
176 |
in |
55946 | 177 |
if not eligible then NONE |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
178 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
179 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
180 |
val {props = more_props, pretty} = payload () |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
181 |
val props = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
182 |
[(textN, text), |
63806 | 183 |
(memoryN, Value.print_bool memory), |
184 |
(parentN, Value.print_int parent)] |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
185 |
val data = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
186 |
Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty]) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
187 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
188 |
SOME (serial (), data) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
189 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
190 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
191 |
|
55552 | 192 |
|
193 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
194 |
(** tracing output **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
195 |
|
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57592
diff
changeset
|
196 |
fun see_panel () = |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57592
diff
changeset
|
197 |
let |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57592
diff
changeset
|
198 |
val ((bg1, bg2), en) = |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57592
diff
changeset
|
199 |
YXML.output_markup_elem |
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57592
diff
changeset
|
200 |
(Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []}) |
57596
3a1b1bda702f
refer to Simplifier Trace panel on first invocation;
wenzelm
parents:
57594
diff
changeset
|
201 |
in "See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en end |
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57592
diff
changeset
|
202 |
|
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
57592
diff
changeset
|
203 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
204 |
fun send_request (result_id, content) = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
205 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
206 |
fun break () = |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
55946
diff
changeset
|
207 |
(Output.protocol_message (Markup.simp_trace_cancel result_id) []; |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
208 |
Synchronized.change futures (Inttab.delete_safe result_id)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
209 |
val promise = Future.promise break : string future |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
210 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
211 |
Synchronized.change futures (Inttab.update_new (result_id, promise)); |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
212 |
output_result (result_id, content); |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
213 |
promise |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
214 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
215 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
216 |
|
55335 | 217 |
type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule} |
218 |
||
219 |
fun step ({term, thm, unconditional, ctxt, rrule}: data) = |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
220 |
let |
57592 | 221 |
val (matching_terms, thm_triggered) = check_breakpoint (term, rrule) ctxt |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
222 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
223 |
val {name, ...} = rrule |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
224 |
val term_triggered = not (null matching_terms) |
54730 | 225 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
226 |
val text = |
55552 | 227 |
if unconditional then "Apply rewrite rule?" |
228 |
else "Apply conditional rewrite rule?" |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
229 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
230 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
231 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
232 |
(* FIXME pretty printing via Proof_Context.pretty_fact *) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
233 |
val pretty_thm = Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
234 |
[Pretty.str ("Instance of " ^ name ^ ":"), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
235 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
236 |
Syntax.pretty_term ctxt (Thm.prop_of thm)] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
237 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
238 |
val pretty_term = Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
239 |
[Pretty.str "Trying to rewrite:", |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
240 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
241 |
Syntax.pretty_term ctxt term] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
242 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
243 |
val pretty_matchings = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
244 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
245 |
val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
246 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
247 |
if not (null matching_terms) then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
248 |
[Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] |
55552 | 249 |
else [] |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
250 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
251 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
252 |
val pretty = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
253 |
Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
254 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
255 |
{props = [], pretty = pretty} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
256 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
257 |
|
57592 | 258 |
val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
259 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
260 |
fun mk_promise result = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
261 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
262 |
val result_id = #1 result |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
263 |
|
57592 | 264 |
fun put mode' interactive' = put_data |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
265 |
{max_depth = max_depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
266 |
mode = mode', |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
267 |
interactive = interactive', |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
268 |
memory = memory, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
269 |
parent = result_id, |
57592 | 270 |
breakpoints = breakpoints} ctxt |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
271 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
272 |
fun to_response "skip" = NONE |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
273 |
| to_response "continue" = SOME (put mode true) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
274 |
| to_response "continue_trace" = SOME (put Full true) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
275 |
| to_response "continue_passive" = SOME (put mode false) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
276 |
| to_response "continue_disable" = SOME (put Disabled false) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
277 |
| to_response _ = raise Fail "Simplifier_Trace.step: invalid message" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
278 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
279 |
if not interactive then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
280 |
(output_result result; Future.value (SOME (put mode false))) |
55552 | 281 |
else Future.map to_response (send_request result) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
282 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
283 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
284 |
in |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
285 |
(case mk_generic_result Markup.simp_trace_stepN text |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
286 |
(thm_triggered orelse term_triggered) payload ctxt of |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
287 |
NONE => Future.value (SOME ctxt) |
55552 | 288 |
| SOME res => mk_promise res) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
289 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
290 |
|
55946 | 291 |
fun recurse text depth term ctxt = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
292 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
293 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
294 |
{props = [], |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
295 |
pretty = Syntax.pretty_term ctxt term} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
296 |
|
57592 | 297 |
val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
298 |
|
57592 | 299 |
fun put result_id = put_data |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
300 |
{max_depth = max_depth, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
301 |
mode = if depth >= max_depth then Disabled else mode, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
302 |
interactive = interactive, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
303 |
memory = memory, |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
304 |
parent = result_id, |
57592 | 305 |
breakpoints = breakpoints} ctxt |
306 |
in |
|
307 |
(case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of |
|
308 |
NONE => put 0 |
|
57596
3a1b1bda702f
refer to Simplifier Trace panel on first invocation;
wenzelm
parents:
57594
diff
changeset
|
309 |
| SOME res => |
3a1b1bda702f
refer to Simplifier Trace panel on first invocation;
wenzelm
parents:
57594
diff
changeset
|
310 |
(if depth = 1 then writeln (see_panel ()) else (); |
3a1b1bda702f
refer to Simplifier Trace panel on first invocation;
wenzelm
parents:
57594
diff
changeset
|
311 |
output_result res; |
3a1b1bda702f
refer to Simplifier Trace panel on first invocation;
wenzelm
parents:
57594
diff
changeset
|
312 |
put (#1 res))) |
57592 | 313 |
end |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
314 |
|
55335 | 315 |
fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
316 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
317 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
318 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
319 |
val {name, ...} = rrule |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
320 |
val pretty_thm = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
321 |
(* FIXME pretty printing via Proof_Context.pretty_fact *) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
322 |
Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
323 |
[Pretty.str ("In an instance of " ^ name ^ ":"), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
324 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
325 |
Syntax.pretty_term ctxt (Thm.prop_of thm)] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
326 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
327 |
val pretty_term = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
328 |
Pretty.block |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
329 |
[Pretty.str "Was trying to rewrite:", |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
330 |
Pretty.brk 1, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
331 |
Syntax.pretty_term ctxt term] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
332 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
333 |
val pretty = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
334 |
Pretty.chunks [pretty_thm, pretty_term] |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
335 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
336 |
{props = [(successN, "false")], pretty = pretty} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
337 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
338 |
|
57592 | 339 |
val {interactive, ...} = get_data ctxt |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
340 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
341 |
fun mk_promise result = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
342 |
let |
55552 | 343 |
fun to_response "exit" = false |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
344 |
| to_response "redo" = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
345 |
(Option.app output_result |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
346 |
(mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt'); |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
347 |
true) |
55552 | 348 |
| to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message" |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
349 |
in |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
350 |
if not interactive then |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
351 |
(output_result result; Future.value false) |
55552 | 352 |
else Future.map to_response (send_request result) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
353 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
354 |
in |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
355 |
(case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
356 |
NONE => Future.value false |
55552 | 357 |
| SOME res => mk_promise res) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
358 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
359 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
360 |
fun indicate_success thm ctxt = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
361 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
362 |
fun payload () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
363 |
{props = [(successN, "true")], |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
364 |
pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
365 |
in |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
366 |
Option.app output_result |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
367 |
(mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
368 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
369 |
|
55552 | 370 |
|
371 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
372 |
(** setup **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
373 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
374 |
fun simp_apply args ctxt cont = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
375 |
let |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
376 |
val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
377 |
val data = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
378 |
{term = term, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
379 |
unconditional = unconditional, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
380 |
ctxt = ctxt, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
381 |
thm = thm, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
382 |
rrule = rrule} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
383 |
in |
55552 | 384 |
(case Future.join (step data) of |
385 |
NONE => NONE |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
386 |
| SOME ctxt' => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
387 |
let val res = cont ctxt' in |
55552 | 388 |
(case res of |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
389 |
NONE => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
390 |
if Future.join (indicate_failure data ctxt') then |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
391 |
simp_apply args ctxt cont |
55552 | 392 |
else NONE |
393 |
| SOME (thm, _) => (indicate_success thm ctxt'; res)) |
|
394 |
end) |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
395 |
end |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
396 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
397 |
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" |
54730 | 398 |
|
399 |
val _ = Theory.setup |
|
54731
384ac33802b0
clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
wenzelm
parents:
54730
diff
changeset
|
400 |
(Simplifier.set_trace_ops |
55946 | 401 |
{trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
402 |
trace_apply = simp_apply}) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
403 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
404 |
val _ = |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
405 |
Isabelle_Process.protocol_command "Simplifier_Trace.reply" |
60747 | 406 |
(fn [serial_string, reply] => |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
407 |
let |
63806 | 408 |
val serial = Value.parse_int serial_string |
60747 | 409 |
val result = |
410 |
Synchronized.change_result futures |
|
411 |
(fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab)) |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
412 |
in |
60747 | 413 |
(case result of |
414 |
SOME promise => Future.fulfill promise reply |
|
415 |
| NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *) |
|
62505 | 416 |
end handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
417 |
|
55552 | 418 |
|
419 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
420 |
(** attributes **) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
421 |
|
55560 | 422 |
val mode_parser = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
423 |
Scan.optional |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
424 |
(Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full")) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
425 |
"normal" |
54730 | 426 |
|
55560 | 427 |
val interactive_parser = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
428 |
Scan.optional (Args.$$$ "interactive" >> K true) false |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
429 |
|
55560 | 430 |
val memory_parser = |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
431 |
Scan.optional (Args.$$$ "no_memory" >> K false) true |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
432 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
433 |
val depth_parser = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
434 |
Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10 |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
435 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
436 |
val config_parser = |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
437 |
(interactive_parser -- mode_parser -- depth_parser -- memory_parser) >> |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
438 |
(fn (((interactive, mode), depth), memory) => config mode interactive depth memory) |
54730 | 439 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
440 |
val _ = Theory.setup |
57041
aceaca232177
consolidate "break_thm" and "break_term" attributes into "simp_break";
Lars Hupel <lars.hupel@mytum.de>
parents:
56333
diff
changeset
|
441 |
(Attrib.setup @{binding simp_break} |
aceaca232177
consolidate "break_thm" and "break_term" attributes into "simp_break";
Lars Hupel <lars.hupel@mytum.de>
parents:
56333
diff
changeset
|
442 |
(Scan.repeat Args.term_pattern >> breakpoint) |
aceaca232177
consolidate "break_thm" and "break_term" attributes into "simp_break";
Lars Hupel <lars.hupel@mytum.de>
parents:
56333
diff
changeset
|
443 |
"declaration of a simplifier breakpoint" #> |
57591
8c095aef6769
clarified "simp_trace_new" and corresponding isar-ref section;
wenzelm
parents:
57041
diff
changeset
|
444 |
Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
445 |
"simplifier trace configuration") |
54730 | 446 |
|
447 |
end |