author | Lars Hupel <lars.hupel@mytum.de> |
Thu, 06 Mar 2014 17:55:39 +0100 | |
changeset 55946 | 5163ed3a38f5 |
parent 55611 | 8ae36527c2a6 |
child 56333 | 38f1422ef473 |
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 = |
55560 | 26 |
(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
|
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 |
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
|
38 |
interactive: bool, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
39 |
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
|
40 |
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
|
41 |
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
|
42 |
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
|
43 |
{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
|
44 |
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
|
45 |
interactive = false, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
val extend = I |
55552 | 50 |
fun merge |
51 |
({max_depth = max_depth1, mode = mode1, interactive = interactive1, |
|
52 |
memory = memory1, breakpoints = breakpoints1, ...}: T, |
|
53 |
{max_depth = max_depth2, mode = mode2, interactive = interactive2, |
|
54 |
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
|
55 |
{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
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
parent = 0, |
55335 | 60 |
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
|
61 |
) |
885500f4aa6a
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 |
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
|
64 |
Data.map |
55946 | 65 |
(fn {max_depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} => |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
66 |
{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
|
67 |
mode = mode, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
68 |
interactive = interactive, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
69 |
memory = memory, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
70 |
parent = parent, |
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
71 |
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
|
72 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
73 |
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
|
74 |
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
|
75 |
|
885500f4aa6a
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 |
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
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
|
82 |
|
885500f4aa6a
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 |
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
|
84 |
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
|
85 |
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
|
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 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
|
88 |
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
|
89 |
|
885500f4aa6a
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 |
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
|
91 |
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
|
92 |
(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
|
93 |
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
|
94 |
(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
|
95 |
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
|
96 |
|
55552 | 97 |
|
98 |
||
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
|
99 |
(** 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
|
100 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
101 |
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
|
102 |
let |
55552 | 103 |
val mode = |
104 |
(case raw_mode of |
|
105 |
"normal" => Normal |
|
106 |
| "full" => Full |
|
107 |
| _ => 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
|
108 |
|
55946 | 109 |
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
|
110 |
{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
|
111 |
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
|
112 |
interactive = interactive, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
113 |
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
|
114 |
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
|
115 |
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
|
116 |
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
|
117 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
118 |
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
|
119 |
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
|
120 |
|
885500f4aa6a
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 |
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
|
122 |
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
|
123 |
|
55552 | 124 |
|
125 |
||
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
|
126 |
(** 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
|
127 |
|
885500f4aa6a
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 |
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
|
129 |
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
|
130 |
|
55552 | 131 |
|
132 |
||
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
|
133 |
(** 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
|
134 |
|
885500f4aa6a
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 |
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
|
136 |
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
|
137 |
|
885500f4aa6a
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 |
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
|
139 |
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
|
140 |
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
|
141 |
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
|
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 |
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
|
144 |
{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
|
145 |
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
|
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 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
|
148 |
{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
|
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 |
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
|
151 |
let |
55946 | 152 |
val {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
|
153 |
|
885500f4aa6a
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 |
val eligible = |
55552 | 155 |
(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
|
156 |
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
|
157 |
| Normal => triggered |
55552 | 158 |
| 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
|
159 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
160 |
val markup' = |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
161 |
if markup = Markup.simp_trace_stepN andalso not interactive |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
162 |
then Markup.simp_trace_logN |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
163 |
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
|
164 |
in |
55946 | 165 |
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
|
166 |
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
|
167 |
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
|
168 |
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
|
169 |
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
|
170 |
[(textN, text), |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
171 |
(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
|
172 |
(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
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
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
|
179 |
|
55552 | 180 |
|
181 |
||
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
|
182 |
(** 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
|
183 |
|
885500f4aa6a
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 |
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
|
185 |
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
|
186 |
fun break () = |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
187 |
(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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
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
|
193 |
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
|
194 |
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
|
195 |
|
885500f4aa6a
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 |
|
55335 | 197 |
type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule} |
198 |
||
199 |
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
|
200 |
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
|
201 |
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
|
202 |
|
885500f4aa6a
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 {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
|
204 |
val term_triggered = not (null matching_terms) |
54730 | 205 |
|
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
|
206 |
val text = |
55552 | 207 |
if unconditional then "Apply rewrite rule?" |
208 |
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
|
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 |
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
|
211 |
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
|
212 |
(* 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
|
213 |
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
|
214 |
[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
|
215 |
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
|
216 |
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
|
217 |
|
885500f4aa6a
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 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
|
219 |
[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
|
220 |
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
|
221 |
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
|
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 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
|
224 |
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
|
225 |
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
|
226 |
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
|
227 |
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
|
228 |
[Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] |
55552 | 229 |
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
|
230 |
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
|
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 = |
885500f4aa6a
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.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
|
234 |
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
|
235 |
{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
|
236 |
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
|
237 |
|
55946 | 238 |
val {max_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
|
239 |
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
|
240 |
|
885500f4aa6a
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 |
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
|
242 |
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
|
243 |
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
|
244 |
|
885500f4aa6a
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 |
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
|
246 |
{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
|
247 |
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
|
248 |
interactive = interactive', |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
249 |
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
|
250 |
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
|
251 |
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
|
252 |
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
|
253 |
|
885500f4aa6a
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 |
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
|
255 |
| 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
|
256 |
| 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
|
257 |
| 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
|
258 |
| 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
|
259 |
| 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
|
260 |
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
|
261 |
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
|
262 |
(output_result result; Future.value (SOME (put mode false))) |
55552 | 263 |
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
|
264 |
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
|
265 |
|
885500f4aa6a
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 |
in |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
267 |
(case mk_generic_result Markup.simp_trace_stepN text |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
268 |
(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
|
269 |
NONE => Future.value (SOME ctxt) |
55552 | 270 |
| 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
|
271 |
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
|
272 |
|
55946 | 273 |
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
|
274 |
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
|
275 |
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
|
276 |
{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
|
277 |
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
|
278 |
|
55946 | 279 |
val {max_depth, mode, interactive, memory, breakpoints, ...} = |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
280 |
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
|
281 |
|
885500f4aa6a
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 |
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
|
283 |
{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
|
284 |
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
|
285 |
interactive = interactive, |
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
286 |
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
|
287 |
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
|
288 |
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
|
289 |
|
885500f4aa6a
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 |
val context' = |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
291 |
(case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of |
55552 | 292 |
NONE => put 0 |
293 |
| 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
|
294 |
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
|
295 |
|
55335 | 296 |
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
|
297 |
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
|
298 |
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
|
299 |
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
|
300 |
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
|
301 |
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
|
302 |
(* 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
|
303 |
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
|
304 |
[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
|
305 |
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
|
306 |
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
|
307 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
54731
diff
changeset
|
308 |
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
|
309 |
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
|
310 |
[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
|
311 |
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
|
312 |
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
|
313 |
|
885500f4aa6a
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 |
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
|
315 |
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
|
316 |
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
|
317 |
{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
|
318 |
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
|
319 |
|
885500f4aa6a
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 {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
|
321 |
|
885500f4aa6a
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 |
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
|
323 |
let |
55552 | 324 |
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
|
325 |
| 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
|
326 |
(Option.app output_result |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
327 |
(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
|
328 |
true) |
55552 | 329 |
| 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
|
330 |
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
|
331 |
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
|
332 |
(output_result result; Future.value false) |
55552 | 333 |
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
|
334 |
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
|
335 |
in |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
336 |
(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
|
337 |
NONE => Future.value false |
55552 | 338 |
| 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
|
339 |
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
|
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 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
|
342 |
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
|
343 |
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
|
344 |
{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
|
345 |
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
|
346 |
in |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
347 |
Option.app output_result |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
348 |
(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
|
349 |
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
|
350 |
|
55552 | 351 |
|
352 |
||
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 |
(** 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
|
354 |
|
55390
36550a4eac5e
"no_memory" option for the simplifier trace to bypass memoization
Lars Hupel <lars.hupel@mytum.de>
parents:
55335
diff
changeset
|
355 |
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
|
356 |
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
|
357 |
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
|
358 |
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
|
359 |
{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
|
360 |
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
|
361 |
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
|
362 |
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
|
363 |
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
|
364 |
in |
55552 | 365 |
(case Future.join (step data) of |
366 |
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
|
367 |
| 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
|
368 |
let val res = cont ctxt' in |
55552 | 369 |
(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
|
370 |
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
|
371 |
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
|
372 |
simp_apply args ctxt cont |
55552 | 373 |
else NONE |
374 |
| SOME (thm, _) => (indicate_success thm ctxt'; res)) |
|
375 |
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
|
376 |
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
|
377 |
|
885500f4aa6a
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 |
val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" |
54730 | 379 |
|
380 |
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
|
381 |
(Simplifier.set_trace_ops |
55946 | 382 |
{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
|
383 |
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
|
384 |
|
885500f4aa6a
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 |
val _ = |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55552
diff
changeset
|
386 |
Isabelle_Process.protocol_command "Simplifier_Trace.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
|
387 |
(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
|
388 |
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
|
389 |
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
|
390 |
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
|
391 |
(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
|
392 |
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
|
393 |
| 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
|
394 |
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
|
395 |
(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
|
396 |
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
|
397 |
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
|
398 |
|
55552 | 399 |
|
400 |
||
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 |
(** 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
|
402 |
|
55560 | 403 |
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
|
404 |
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
|
405 |
(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
|
406 |
"normal" |
54730 | 407 |
|
55560 | 408 |
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
|
409 |
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
|
410 |
|
55560 | 411 |
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
|
412 |
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
|
413 |
|
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
|
414 |
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
|
415 |
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
|
416 |
|
885500f4aa6a
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 |
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
|
418 |
(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
|
419 |
(fn (((interactive, mode), depth), memory) => config mode interactive depth memory) |
54730 | 420 |
|
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
|
421 |
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
|
422 |
(Attrib.setup @{binding break_term} |
55560 | 423 |
(Scan.repeat1 Args.term_pattern >> term_breakpoint) |
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
|
424 |
"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
|
425 |
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
|
426 |
(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
|
427 |
"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
|
428 |
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
|
429 |
"simplifier trace configuration") |
54730 | 430 |
|
431 |
end |