author | wenzelm |
Tue, 18 Feb 2014 17:26:13 +0100 | |
changeset 55552 | e4907b74a347 |
parent 55390 | 36550a4eac5e |
child 55553 | 99409ccbe04a |
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 |
|
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
|
9 |
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
|
10 |
val add_thm_breakpoint: thm -> Context.generic -> Context.generic |
54730 | 11 |
end |
12 |
||
13 |
structure Simplifier_Trace: SIMPLIFIER_TRACE = |
|
14 |
struct |
|
15 |
||
55552 | 16 |
(** 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
|
17 |
|
885500f4aa6a
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 |
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
|
19 |
|
885500f4aa6a
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 |
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
|
21 |
| 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
|
22 |
| 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
|
23 |
| 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
|
24 |
|
885500f4aa6a
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 |
val 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
|
26 |
(Item_Net.init (op =) single (* FIXME equality on 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
|
27 |
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
|
28 |
|
885500f4aa6a
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 |
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
|
30 |
(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
|
31 |
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
|
32 |
|
885500f4aa6a
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 |
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
|
34 |
( |
885500f4aa6a
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 |
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
|
36 |
{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
|
37 |
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 |
depth = 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
|
46 |
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
|
47 |
interactive = false, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
48 |
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
|
49 |
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
|
50 |
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
|
51 |
val extend = I |
55552 | 52 |
fun merge |
53 |
({max_depth = max_depth1, mode = mode1, interactive = interactive1, |
|
54 |
memory = memory1, breakpoints = breakpoints1, ...}: T, |
|
55 |
{max_depth = max_depth2, mode = mode2, interactive = interactive2, |
|
56 |
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
|
57 |
{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
|
58 |
depth = 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
|
59 |
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
|
60 |
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
|
61 |
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
|
62 |
parent = 0, |
55335 | 63 |
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
|
64 |
) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
65 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
66 |
fun map_breakpoints f_term f_thm = |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
67 |
Data.map |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
68 |
(fn {max_depth, depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} => |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
69 |
{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
|
70 |
depth = depth, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
71 |
mode = mode, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
72 |
interactive = interactive, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
73 |
memory = memory, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
74 |
parent = parent, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
75 |
breakpoints = (f_term term_bs, f_thm thm_bs)}) |
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
|
76 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
77 |
fun add_term_breakpoint 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
|
78 |
map_breakpoints (Item_Net.update term) I |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
79 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
map_breakpoints I (fold Item_Net.update rrules) 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
|
85 |
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
|
86 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
87 |
fun is_breakpoint (term, rrule) 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
|
88 |
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
|
89 |
val {breakpoints, ...} = Data.get 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 |
|
885500f4aa6a
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 |
fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, 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
|
92 |
val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) 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
|
93 |
|
885500f4aa6a
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 |
val {thm = thm, ...} = 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
|
95 |
val thm_matches = exists (eq_rrule o pair 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
|
96 |
(Item_Net.retrieve_matching (snd breakpoints) (Thm.full_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
|
97 |
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
|
98 |
(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
|
99 |
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
|
100 |
|
55552 | 101 |
|
102 |
||
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
|
103 |
(** 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
|
104 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
105 |
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
|
106 |
let |
55552 | 107 |
val mode = |
108 |
(case raw_mode of |
|
109 |
"normal" => Normal |
|
110 |
| "full" => Full |
|
111 |
| _ => 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
|
112 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
113 |
val update = Data.map (fn {depth, parent, 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
|
114 |
{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
|
115 |
depth = 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
|
116 |
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
|
117 |
interactive = interactive, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
118 |
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
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
|
885500f4aa6a
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 |
fun term_breakpoint 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
|
124 |
Thm.declaration_attribute (K (fold add_term_breakpoint 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
|
125 |
|
885500f4aa6a
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 |
val thm_breakpoint = |
885500f4aa6a
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 |
Thm.declaration_attribute add_thm_breakpoint |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
128 |
|
55552 | 129 |
|
130 |
||
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
|
131 |
(** 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
|
132 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
133 |
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
|
134 |
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
|
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 |
(** 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
|
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 |
fun output_result (id, 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
|
141 |
Output.result (Markup.serial_properties id) 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
|
142 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
143 |
val serialN = "serial" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
144 |
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
|
145 |
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
|
146 |
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
|
147 |
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
|
148 |
|
885500f4aa6a
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 |
val logN = "simp_trace_log" |
885500f4aa6a
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 stepN = "simp_trace_step" |
885500f4aa6a
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 recurseN = "simp_trace_recurse" |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
152 |
val hintN = "simp_trace_hint" |
885500f4aa6a
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 ignoreN = "simp_trace_ignore" |
885500f4aa6a
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 |
val cancelN = "simp_trace_cancel" |
885500f4aa6a
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 |
|
885500f4aa6a
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 |
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
|
158 |
{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
|
159 |
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
|
160 |
|
885500f4aa6a
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 |
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
|
162 |
{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
|
163 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
164 |
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
|
165 |
let |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
166 |
val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof 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
|
167 |
|
885500f4aa6a
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 |
val eligible = |
55552 | 169 |
(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
|
170 |
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
|
171 |
| Normal => triggered |
55552 | 172 |
| 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
|
173 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
174 |
val markup' = if markup = stepN andalso not interactive then logN else 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
|
175 |
in |
55552 | 176 |
if not eligible orelse depth > max_depth 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
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
[(textN, text), |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
182 |
(memoryN, Markup.print_bool 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
|
183 |
(parentN, Markup.print_int 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
|
184 |
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
|
185 |
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
|
186 |
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
|
187 |
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
|
188 |
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
|
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 |
|
55552 | 191 |
|
192 |
||
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
|
193 |
(** 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
|
194 |
|
885500f4aa6a
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 |
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
|
196 |
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
|
197 |
fun break () = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
198 |
(Output.protocol_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
|
199 |
[(Markup.functionN, cancelN), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
200 |
(serialN, Markup.print_int 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
|
201 |
""; |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
202 |
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
|
203 |
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
|
204 |
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
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
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
|
209 |
|
885500f4aa6a
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 |
|
55335 | 211 |
type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule} |
212 |
||
213 |
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
|
214 |
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
|
215 |
val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof 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
|
216 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
217 |
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
|
218 |
val term_triggered = not (null matching_terms) |
54730 | 219 |
|
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 |
val text = |
55552 | 221 |
if unconditional then "Apply rewrite rule?" |
222 |
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
|
223 |
|
885500f4aa6a
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 |
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
|
225 |
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
|
226 |
(* 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
|
227 |
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
|
228 |
[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
|
229 |
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
|
230 |
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
|
231 |
|
885500f4aa6a
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 |
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
|
233 |
[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
|
234 |
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
|
235 |
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
|
236 |
|
885500f4aa6a
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 |
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
|
238 |
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
|
239 |
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
|
240 |
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
|
241 |
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
|
242 |
[Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] |
55552 | 243 |
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
|
244 |
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
|
245 |
|
885500f4aa6a
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 |
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
|
247 |
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
|
248 |
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
|
249 |
{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
|
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 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
252 |
val {max_depth, depth, mode, interactive, memory, 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
|
253 |
Data.get (Context.Proof 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
|
254 |
|
885500f4aa6a
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 |
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
|
256 |
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
|
257 |
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
|
258 |
|
885500f4aa6a
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 |
fun put mode' interactive' = Data.put |
885500f4aa6a
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 |
{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
|
261 |
depth = 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
|
262 |
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
|
263 |
interactive = interactive', |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
264 |
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
|
265 |
parent = 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
|
266 |
breakpoints = breakpoints} (Context.Proof 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
|
267 |
Context.the_proof |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
268 |
|
885500f4aa6a
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 |
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
|
270 |
| 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
|
271 |
| 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
|
272 |
| 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
|
273 |
| 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
|
274 |
| 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
|
275 |
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
|
276 |
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
|
277 |
(output_result result; Future.value (SOME (put mode false))) |
55552 | 278 |
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
|
279 |
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
|
280 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
281 |
in |
55552 | 282 |
(case mk_generic_result stepN text (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
|
283 |
NONE => Future.value (SOME ctxt) |
55552 | 284 |
| 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
|
285 |
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
|
286 |
|
885500f4aa6a
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 |
fun recurse text term 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
|
288 |
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
|
289 |
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
|
290 |
{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
|
291 |
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
|
292 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
293 |
val {max_depth, depth, mode, interactive, memory, breakpoints, ...} = |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
294 |
Data.get (Context.Proof 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
|
295 |
|
885500f4aa6a
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 |
fun put result_id = Data.put |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
297 |
{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
|
298 |
depth = depth + 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
|
299 |
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
|
300 |
interactive = interactive, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
301 |
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
|
302 |
parent = 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
|
303 |
breakpoints = breakpoints} (Context.Proof 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
|
304 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
305 |
val context' = |
55552 | 306 |
(case mk_generic_result recurseN text true payload ctxt of |
307 |
NONE => put 0 |
|
308 |
| SOME res => (output_result res; put (#1 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
|
309 |
in Context.the_proof context' 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
|
310 |
|
55335 | 311 |
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
|
312 |
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
|
313 |
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
|
314 |
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
|
315 |
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
|
316 |
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
|
317 |
(* 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
|
318 |
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
|
319 |
[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
|
320 |
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
|
321 |
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
|
322 |
|
885500f4aa6a
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 |
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
|
324 |
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
|
325 |
[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
|
326 |
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
|
327 |
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
|
328 |
|
885500f4aa6a
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 |
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
|
330 |
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
|
331 |
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
|
332 |
{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
|
333 |
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
|
334 |
|
885500f4aa6a
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 |
val {interactive, ...} = Data.get (Context.Proof 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
|
336 |
val {parent, ...} = Data.get (Context.Proof 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
|
337 |
|
885500f4aa6a
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 |
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
|
339 |
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
|
340 |
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
|
341 |
|
55552 | 342 |
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
|
343 |
| 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
|
344 |
(Option.app output_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
|
345 |
(mk_generic_result ignoreN "Ignore" true empty_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
|
346 |
true) |
55552 | 347 |
| 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
|
348 |
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
|
349 |
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
|
350 |
(output_result result; Future.value false) |
55552 | 351 |
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
|
352 |
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
|
353 |
in |
55552 | 354 |
(case mk_generic_result 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
|
355 |
NONE => Future.value false |
55552 | 356 |
| 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
|
357 |
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
|
358 |
|
885500f4aa6a
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 |
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
|
360 |
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
|
361 |
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
|
362 |
{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
|
363 |
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
|
364 |
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
|
365 |
Option.app output_result (mk_generic_result hintN "Successfully rewrote" true 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
|
366 |
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
|
367 |
|
55552 | 368 |
|
369 |
||
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
|
370 |
(** 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
|
371 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
372 |
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
|
373 |
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
|
374 |
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
|
375 |
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
|
376 |
{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
|
377 |
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
|
378 |
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
|
379 |
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
|
380 |
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
|
381 |
in |
55552 | 382 |
(case Future.join (step data) of |
383 |
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
|
384 |
| 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
|
385 |
let val res = cont ctxt' in |
55552 | 386 |
(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
|
387 |
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
|
388 |
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
|
389 |
simp_apply args ctxt cont |
55552 | 390 |
else NONE |
391 |
| SOME (thm, _) => (indicate_success thm ctxt'; res)) |
|
392 |
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
|
393 |
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
|
394 |
|
885500f4aa6a
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 |
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" |
54730 | 396 |
|
397 |
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
|
398 |
(Simplifier.set_trace_ops |
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
|
399 |
{trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
400 |
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
|
401 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
402 |
val _ = |
885500f4aa6a
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 |
Isabelle_Process.protocol_command "Document.simp_trace_reply" |
885500f4aa6a
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 |
(fn [s, r] => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
405 |
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
|
406 |
val serial = Markup.parse_int s |
885500f4aa6a
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 |
fun lookup_delete tab = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
408 |
(Inttab.lookup tab serial, Inttab.delete_safe serial tab) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
409 |
fun apply_result (SOME promise) = Future.fulfill promise r |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
410 |
| apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
411 |
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
|
412 |
(Synchronized.change_result futures lookup_delete |> apply_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
|
413 |
handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
414 |
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
|
415 |
|
55552 | 416 |
|
417 |
||
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
|
418 |
(** 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
|
419 |
|
885500f4aa6a
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 |
val pat_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
|
421 |
Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic |
54730 | 422 |
|
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 |
val mode_parser: string 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
|
424 |
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
|
425 |
(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
|
426 |
"normal" |
54730 | 427 |
|
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 |
val interactive_parser: bool 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
|
429 |
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
|
430 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
431 |
val memory_parser: bool parser = |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
432 |
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
|
433 |
|
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
|
434 |
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
|
435 |
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
|
436 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
437 |
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
|
438 |
(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
|
439 |
(fn (((interactive, mode), depth), memory) => config mode interactive depth memory) |
54730 | 440 |
|
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
|
441 |
val _ = Theory.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
|
442 |
(Attrib.setup @{binding break_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
|
443 |
((Scan.repeat1 pat_parser) >> term_breakpoint) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
444 |
"declaration of a term breakpoint" #> |
885500f4aa6a
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 |
Attrib.setup @{binding break_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
|
446 |
(Scan.succeed thm_breakpoint) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
447 |
"declaration of a theorem breakpoint" #> |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
448 |
Attrib.setup @{binding simplifier_trace} (Scan.lift config_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
|
449 |
"simplifier trace configuration") |
54730 | 450 |
|
451 |
end |