1 (* Title: Pure/Isar/isar.ML |
|
2 Author: Makarius |
|
3 |
|
4 The global Isabelle/Isar state and main read-eval-print loop. |
|
5 *) |
|
6 |
|
7 signature ISAR = |
|
8 sig |
|
9 val init: unit -> unit |
|
10 val exn: unit -> (exn * string) option |
|
11 val state: unit -> Toplevel.state |
|
12 val context: unit -> Proof.context |
|
13 val goal: unit -> thm |
|
14 val print: unit -> unit |
|
15 val >> : Toplevel.transition -> bool |
|
16 val >>> : Toplevel.transition list -> unit |
|
17 val linear_undo: int -> unit |
|
18 val undo: int -> unit |
|
19 val kill: unit -> unit |
|
20 val kill_proof: unit -> unit |
|
21 val crashes: exn list ref |
|
22 val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit |
|
23 val loop: unit -> unit |
|
24 val main: unit -> unit |
|
25 |
|
26 type id = string |
|
27 val no_id: id |
|
28 val create_command: Toplevel.transition -> id |
|
29 val insert_command: id -> id -> unit |
|
30 val remove_command: id -> unit |
|
31 end; |
|
32 |
|
33 structure Isar: ISAR = |
|
34 struct |
|
35 |
|
36 |
|
37 (** TTY model -- SINGLE-THREADED! **) |
|
38 |
|
39 (* the global state *) |
|
40 |
|
41 type history = (Toplevel.state * Toplevel.transition) list; |
|
42 (*previous state, state transition -- regular commands only*) |
|
43 |
|
44 local |
|
45 val global_history = ref ([]: history); |
|
46 val global_state = ref Toplevel.toplevel; |
|
47 val global_exn = ref (NONE: (exn * string) option); |
|
48 in |
|
49 |
|
50 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () => |
|
51 let |
|
52 fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE) |
|
53 | edit n (st, hist) = edit (n - 1) (f st hist); |
|
54 in edit count (! global_state, ! global_history) end); |
|
55 |
|
56 fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state); |
|
57 fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state); |
|
58 |
|
59 fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn); |
|
60 fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn); |
|
61 |
|
62 end; |
|
63 |
|
64 |
|
65 fun init () = edit_history 1 (K (K (Toplevel.toplevel, []))); |
|
66 |
|
67 fun context () = Toplevel.context_of (state ()) |
|
68 handle Toplevel.UNDEF => error "Unknown context"; |
|
69 |
|
70 fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ())))) |
|
71 handle Toplevel.UNDEF => error "No goal present"; |
|
72 |
|
73 fun print () = Toplevel.print_state false (state ()); |
|
74 |
|
75 |
|
76 (* history navigation *) |
|
77 |
|
78 local |
|
79 |
|
80 fun find_and_undo _ [] = error "Undo history exhausted" |
|
81 | find_and_undo which ((prev, tr) :: hist) = |
|
82 ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ()); |
|
83 if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist); |
|
84 |
|
85 in |
|
86 |
|
87 fun linear_undo n = edit_history n (K (find_and_undo (K true))); |
|
88 |
|
89 fun undo n = edit_history n (fn st => fn hist => |
|
90 find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist); |
|
91 |
|
92 fun kill () = edit_history 1 (fn st => fn hist => |
|
93 find_and_undo |
|
94 (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist); |
|
95 |
|
96 fun kill_proof () = edit_history 1 (fn st => fn hist => |
|
97 if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist |
|
98 else raise Toplevel.UNDEF); |
|
99 |
|
100 end; |
|
101 |
|
102 |
|
103 (* interactive state transformations *) |
|
104 |
|
105 fun op >> tr = |
|
106 (case Toplevel.transition true tr (state ()) of |
|
107 NONE => false |
|
108 | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true) |
|
109 | SOME (st', NONE) => |
|
110 let |
|
111 val name = Toplevel.name_of tr; |
|
112 val _ = if OuterKeyword.is_theory_begin name then init () else (); |
|
113 val _ = |
|
114 if OuterKeyword.is_regular name |
|
115 then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else (); |
|
116 in true end); |
|
117 |
|
118 fun op >>> [] = () |
|
119 | op >>> (tr :: trs) = if op >> tr then op >>> trs else (); |
|
120 |
|
121 |
|
122 (* toplevel loop *) |
|
123 |
|
124 val crashes = ref ([]: exn list); |
|
125 |
|
126 local |
|
127 |
|
128 fun raw_loop secure src = |
|
129 let |
|
130 fun check_secure () = |
|
131 (if secure then warning "Secure loop -- cannot exit to ML" else (); secure); |
|
132 in |
|
133 (case Source.get_single (Source.set_prompt Source.default_prompt src) of |
|
134 NONE => if secure then quit () else () |
|
135 | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) |
|
136 handle exn => |
|
137 (Output.error_msg (Toplevel.exn_message exn) |
|
138 handle crash => |
|
139 (CRITICAL (fn () => change crashes (cons crash)); |
|
140 warning "Recovering from Isar toplevel crash -- see also Isar.crashes"); |
|
141 raw_loop secure src) |
|
142 end; |
|
143 |
|
144 in |
|
145 |
|
146 fun toplevel_loop {init = do_init, welcome, sync, secure} = |
|
147 (Context.set_thread_data NONE; |
|
148 if do_init then init () else (); (* FIXME init editor model *) |
|
149 if welcome then writeln (Session.welcome ()) else (); |
|
150 uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ()); |
|
151 |
|
152 end; |
|
153 |
|
154 fun loop () = |
|
155 toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; |
|
156 |
|
157 fun main () = |
|
158 toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()}; |
|
159 |
|
160 |
|
161 |
|
162 (** individual toplevel commands **) |
|
163 |
|
164 (* unique identification *) |
|
165 |
|
166 type id = string; |
|
167 val no_id : id = ""; |
|
168 |
|
169 |
|
170 (* command category *) |
|
171 |
|
172 datatype category = Empty | Theory | Proof | Diag | Control; |
|
173 |
|
174 fun category_of tr = |
|
175 let val name = Toplevel.name_of tr in |
|
176 if name = "" then Empty |
|
177 else if OuterKeyword.is_theory name then Theory |
|
178 else if OuterKeyword.is_proof name then Proof |
|
179 else if OuterKeyword.is_diag name then Diag |
|
180 else Control |
|
181 end; |
|
182 |
|
183 val is_theory = fn Theory => true | _ => false; |
|
184 val is_proper = fn Theory => true | Proof => true | _ => false; |
|
185 val is_regular = fn Control => false | _ => true; |
|
186 |
|
187 |
|
188 (* command status *) |
|
189 |
|
190 datatype status = |
|
191 Unprocessed | |
|
192 Running | |
|
193 Failed of exn * string | |
|
194 Finished of Toplevel.state; |
|
195 |
|
196 fun status_markup Unprocessed = Markup.unprocessed |
|
197 | status_markup Running = (Markup.runningN, []) |
|
198 | status_markup (Failed _) = Markup.failed |
|
199 | status_markup (Finished _) = Markup.finished; |
|
200 |
|
201 fun run int tr state = |
|
202 (case Toplevel.transition int tr state of |
|
203 NONE => NONE |
|
204 | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err)) |
|
205 | SOME (state', NONE) => SOME (Finished state')); |
|
206 |
|
207 |
|
208 (* datatype command *) |
|
209 |
|
210 datatype command = Command of |
|
211 {category: category, |
|
212 transition: Toplevel.transition, |
|
213 status: status}; |
|
214 |
|
215 fun make_command (category, transition, status) = |
|
216 Command {category = category, transition = transition, status = status}; |
|
217 |
|
218 val empty_command = |
|
219 make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel); |
|
220 |
|
221 fun map_command f (Command {category, transition, status}) = |
|
222 make_command (f (category, transition, status)); |
|
223 |
|
224 fun map_status f = map_command (fn (category, transition, status) => |
|
225 (category, transition, f status)); |
|
226 |
|
227 |
|
228 (* global collection of identified commands *) |
|
229 |
|
230 fun err_dup id = sys_error ("Duplicate command " ^ quote id); |
|
231 fun err_undef id = sys_error ("Unknown command " ^ quote id); |
|
232 |
|
233 local val global_commands = ref (Graph.empty: command Graph.T) in |
|
234 |
|
235 fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f) |
|
236 handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad; |
|
237 |
|
238 fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands); |
|
239 |
|
240 end; |
|
241 |
|
242 fun add_edge (id1, id2) = |
|
243 if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2); |
|
244 |
|
245 |
|
246 fun init_commands () = change_commands (K Graph.empty); |
|
247 |
|
248 fun the_command id = |
|
249 let val Command cmd = |
|
250 if id = no_id then empty_command |
|
251 else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad) |
|
252 in cmd end; |
|
253 |
|
254 fun prev_command id = |
|
255 if id = no_id then no_id |
|
256 else |
|
257 (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of |
|
258 [] => no_id |
|
259 | [prev] => prev |
|
260 | _ => sys_error ("Non-linear command dependency " ^ quote id)); |
|
261 |
|
262 fun next_commands id = |
|
263 if id = no_id then [] |
|
264 else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad; |
|
265 |
|
266 fun descendant_commands ids = |
|
267 Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids)) |
|
268 handle Graph.UNDEF bad => err_undef bad; |
|
269 |
|
270 |
|
271 (* maintain status *) |
|
272 |
|
273 fun report_status markup id = Toplevel.status (#transition (the_command id)) markup; |
|
274 |
|
275 fun update_status status id = change_commands (Graph.map_node id (map_status (K status))); |
|
276 |
|
277 fun report_update_status status id = |
|
278 change_commands (Graph.map_node id (map_status (fn old_status => |
|
279 let val markup = status_markup status |
|
280 in if markup <> status_markup old_status then report_status markup id else (); status end))); |
|
281 |
|
282 |
|
283 (* create and dispose commands *) |
|
284 |
|
285 fun create_command raw_tr = |
|
286 let |
|
287 val (id, tr) = |
|
288 (case Toplevel.get_id raw_tr of |
|
289 SOME id => (id, raw_tr) |
|
290 | NONE => |
|
291 let val id = |
|
292 if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string () |
|
293 else "isabelle:" ^ serial_string () |
|
294 in (id, Toplevel.put_id id raw_tr) end); |
|
295 |
|
296 val cmd = make_command (category_of tr, tr, Unprocessed); |
|
297 val _ = change_commands (Graph.new_node (id, cmd)); |
|
298 in id end; |
|
299 |
|
300 fun dispose_commands ids = |
|
301 let |
|
302 val desc = descendant_commands ids; |
|
303 val _ = List.app (report_status Markup.disposed) desc; |
|
304 val _ = change_commands (Graph.del_nodes desc); |
|
305 in () end; |
|
306 |
|
307 |
|
308 (* final state *) |
|
309 |
|
310 fun the_state id = |
|
311 (case the_command id of |
|
312 {status = Finished state, ...} => state |
|
313 | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition)); |
|
314 |
|
315 |
|
316 |
|
317 (** editor model **) |
|
318 |
|
319 (* run commands *) |
|
320 |
|
321 fun try_run id = |
|
322 (case try the_state (prev_command id) of |
|
323 NONE => () |
|
324 | SOME state => |
|
325 (case run true (#transition (the_command id)) state of |
|
326 NONE => () |
|
327 | SOME status => report_update_status status id)); |
|
328 |
|
329 fun rerun_commands ids = |
|
330 (List.app (report_update_status Unprocessed) ids; List.app try_run ids); |
|
331 |
|
332 |
|
333 (* modify document *) |
|
334 |
|
335 fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () => |
|
336 let |
|
337 val nexts = next_commands prev; |
|
338 val _ = change_commands |
|
339 (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #> |
|
340 fold (fn next => Graph.add_edge (id, next)) nexts); |
|
341 in descendant_commands [id] end) |> rerun_commands; |
|
342 |
|
343 fun remove_command id = NAMED_CRITICAL "Isar" (fn () => |
|
344 let |
|
345 val prev = prev_command id; |
|
346 val nexts = next_commands id; |
|
347 val _ = change_commands |
|
348 (fold (fn next => Graph.del_edge (id, next)) nexts #> |
|
349 fold (fn next => add_edge (prev, next)) nexts); |
|
350 in descendant_commands nexts end) |> rerun_commands; |
|
351 |
|
352 |
|
353 (* concrete syntax *) |
|
354 |
|
355 local |
|
356 |
|
357 structure P = OuterParse; |
|
358 val op >> = Scan.>>; |
|
359 |
|
360 in |
|
361 |
|
362 val _ = |
|
363 OuterSyntax.internal_command "Isar.command" |
|
364 (P.string -- P.string >> (fn (id, text) => |
|
365 Toplevel.imperative (fn () => |
|
366 ignore (create_command (OuterSyntax.prepare_command (Position.id id) text))))); |
|
367 |
|
368 val _ = |
|
369 OuterSyntax.internal_command "Isar.insert" |
|
370 (P.string -- P.string >> (fn (prev, id) => |
|
371 Toplevel.imperative (fn () => insert_command prev id))); |
|
372 |
|
373 val _ = |
|
374 OuterSyntax.internal_command "Isar.remove" |
|
375 (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id))); |
|
376 |
|
377 end; |
|
378 |
|
379 end; |
|