-
Notifications
You must be signed in to change notification settings - Fork 0
/
AutoLevity_Base.thy
559 lines (439 loc) · 18.4 KB
/
AutoLevity_Base.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory AutoLevity_Base
imports Main Apply_Trace
keywords "levity_tag" :: thy_decl
begin
ML \<open>
fun is_simp (_: Proof.context) (_: thm) = true
\<close>
ML \<open>
val is_simp_installed = is_some (
try (ML_Context.eval ML_Compiler.flags Position.none)
(ML_Lex.read_text ("val is_simp = Raw_Simplifier.is_simp", Position.none )));
\<close>
ML\<open>
(* Describing a ordering on Position.T. Optionally we compare absolute document position, or
just line numbers. Somewhat complicated by the fact that jEdit positions don't have line or
file identifiers. *)
fun pos_ord use_offset (pos1, pos2) =
let
fun get_offset pos = if use_offset then Position.offset_of pos else SOME 0;
fun get_props pos =
(SOME (Position.file_of pos |> the,
(Position.line_of pos |> the,
get_offset pos |> the)), NONE)
handle Option => (NONE, Position.parse_id pos)
val props1 = get_props pos1;
val props2 = get_props pos2;
in prod_ord
(option_ord (prod_ord string_ord (prod_ord int_ord int_ord)))
(option_ord (int_ord))
(props1, props2) end
structure Postab = Table(type key = Position.T val ord = (pos_ord false));
structure Postab_strict = Table(type key = Position.T val ord = (pos_ord true));
signature AUTOLEVITY_BASE =
sig
type extras = {levity_tag : string option, subgoals : int}
val get_transactions : unit -> ((string * extras) Postab_strict.table * string list Postab_strict.table) Symtab.table;
val get_applys : unit -> ((string * string list) list) Postab_strict.table Symtab.table;
val add_attribute_test: string -> (Proof.context -> thm -> bool) -> theory -> theory;
val attribs_of: Proof.context -> thm -> string list;
val used_facts: Proof.context option -> thm -> (string * thm) list;
val used_facts_attribs: Proof.context -> thm -> (string * string list) list;
(*
Returns the proof body form of the prop proved by a theorem.
Unfortunately, proof bodies don't contain terms in the same form as what you'd get
from things like `Thm.full_prop_of`: the proof body terms have sort constraints
pulled out as separate assumptions, rather than as annotations on the types of
terms.
It's easier for our dependency-tracking purposes to treat this transformed
term as the 'canonical' form of a theorem, since it's always available as the
top-level prop of a theorem's proof body.
*)
val proof_body_prop_of: thm -> term;
(*
Get every (named) term that was proved in the proof body of the given thm.
The returned terms are in proof body form.
*)
val used_named_props_of: thm -> (string * term) list;
(*
Distinguish whether the thm name "foo_3" refers to foo(3) or foo_3 by comparing
against the given term. Assumes the term is in proof body form.
The provided context should match the context used to extract the (name, prop) pair
(that is, it should match the context used to extract the thm passed into
`proof_body_prop_of` or `used_named_props_of`).
Returns SOME ("foo", SOME 3) if the answer is 'it refers to foo(3)'.
Returns SOME ("foo_3", NONE) if the answer is 'it refers to foo_3'.
Returns NONE if the answer is 'it doesn't seem to refer to anything.'
*)
val disambiguate_indices: Proof.context -> string * term -> (string * int option) option;
(* Install toplevel hook for tracking command positions. *)
val setup_command_hook: {trace_apply : bool} -> theory -> theory;
(* Used to trace the dependencies of all apply statements.
They are set up by setup_command_hook if the appropriate hooks in the "Proof"
module exist. *)
val pre_apply_hook: Proof.context -> Method.text -> thm -> thm;
val post_apply_hook: Proof.context -> Method.text -> thm -> thm -> thm;
end;
structure AutoLevity_Base : AUTOLEVITY_BASE =
struct
val applys = Synchronized.var "applys"
(Symtab.empty : (((string * string list) list) Postab_strict.table) Symtab.table)
fun get_applys () = Synchronized.value applys;
type extras = {levity_tag : string option, subgoals : int}
val transactions = Synchronized.var "hook"
(Symtab.empty : ((string * extras) Postab_strict.table * ((string list) Postab_strict.table)) Symtab.table);
fun get_transactions () =
Synchronized.value transactions;
structure Data = Theory_Data
(
type T = (bool *
string option *
(Proof.context -> thm -> bool) Symtab.table); (* command_hook * levity tag * attribute tests *)
val empty = (false, NONE, Symtab.empty);
val extend = I;
fun merge (((b1, _, tab), (b2, _, tab')) : T * T) = (b1 orelse b2, NONE, Symtab.merge (fn _ => true) (tab, tab'));
);
val set_command_hook_flag = Data.map (@{apply 3(1)} (fn _ => true));
val get_command_hook_flag = #1 o Data.get
fun set_levity_tag tag = Data.map (@{apply 3(2)} (fn _ => tag));
val get_levity_tag = #2 o Data.get
fun update_attrib_tab f = Data.map (@{apply 3(3)} f);
fun add_attribute_test nm f =
let
val f' = (fn ctxt => fn thm => the_default false (try (f ctxt) thm))
in update_attrib_tab (Symtab.update_new (nm,f')) end;
val get_attribute_tests = Symtab.dest o #3 o Data.get;
(* Internal fact names get the naming scheme "foo_3" to indicate the third
member of the multi-thm "foo". We need to do some work to guess if
such a fact refers to an indexed multi-thm or a real fact named "foo_3" *)
fun base_and_index nm =
let
val exploded = space_explode "_" nm;
val base =
(exploded, (length exploded) - 1)
|> try (List.take #> space_implode "_")
|> Option.mapPartial (Option.filter (fn nm => nm <> ""))
val idx = exploded |> try (List.last #> Int.fromString) |> Option.join;
in
case (base, idx) of
(SOME base, SOME idx) => SOME (base, idx)
| _ => NONE
end
fun maybe_nth idx xs = idx |> try (curry List.nth xs)
fun fact_from_derivation ctxt prop xnm =
let
val facts = Proof_Context.facts_of ctxt;
(* TODO: Check that exported local fact is equivalent to external one *)
fun check_prop thm = Thm.full_prop_of thm = prop
fun entry (name, idx) =
(name, Position.none)
|> try (Facts.retrieve (Context.Proof ctxt) facts)
|> Option.mapPartial (#thms #> maybe_nth (idx - 1))
|> Option.mapPartial (Option.filter check_prop)
|> Option.map (pair name)
val idx_result = (base_and_index xnm) |> Option.mapPartial entry
val non_idx_result = (xnm, 1) |> entry
val _ =
if is_some idx_result andalso is_some non_idx_result
then warning (
"Levity: found two possible results for name " ^ quote xnm ^ " with the same prop:\n" ^
(@{make_string} (the idx_result)) ^ ",\nand\n" ^
(@{make_string} (the non_idx_result)) ^ ".\nUsing the first one.")
else ()
in
merge_options (idx_result, non_idx_result)
end
(* Local facts (from locales) aren't marked in proof bodies, we only
see their external variants. We guess the local name from the external one
(i.e. "Theory_Name.Locale_Name.foo" -> "foo")
This is needed to perform localized attribute tests (e.g.. is this locale assumption marked as simp?) *)
fun most_local_fact_of ctxt xnm prop =
let
val local_name = xnm |> try (Long_Name.explode #> tl #> tl #> Long_Name.implode)
val local_result = local_name |> Option.mapPartial (fact_from_derivation ctxt prop)
fun global_result () = fact_from_derivation ctxt prop xnm
in
if is_some local_result then local_result else global_result ()
end
fun thms_of (PBody {thms,...}) = thms
(* We recursively descend into the proof body to find dependent facts.
We skip over empty derivations or facts that we fail to find, but recurse
into their dependents. This ensures that an attempt to re-build the proof dependencies
graph will result in a connected graph. *)
fun proof_body_deps
(filter_name: string -> bool)
(get_fact: string -> term -> (string * thm) option)
(thm_ident, thm_node)
(tab: (string * thm) option Inttab.table) =
let
val name = Proofterm.thm_node_name thm_node
val body = Proofterm.thm_node_body thm_node
val prop = Proofterm.thm_node_prop thm_node
val result = if filter_name name then NONE else get_fact name prop
val is_new_result = not (Inttab.defined tab thm_ident)
val insert = if is_new_result then Inttab.update (thm_ident, result) else I
val descend =
if is_new_result andalso is_none result
then fold (proof_body_deps filter_name get_fact) (thms_of (Future.join body))
else I
in
tab |> insert |> descend
end
fun used_facts opt_ctxt thm =
let
val nm = Thm.get_name_hint thm;
val get_fact =
case opt_ctxt of
SOME ctxt => most_local_fact_of ctxt
| NONE => fn name => fn _ => (SOME (name, Drule.dummy_thm));
val body = thms_of (Thm.proof_body_of thm);
fun filter_name nm' = nm' = "" orelse nm' = nm;
in
fold (proof_body_deps filter_name get_fact) body Inttab.empty
|> Inttab.dest |> map_filter snd
end
fun attribs_of ctxt =
let
val tests = get_attribute_tests (Proof_Context.theory_of ctxt)
|> map (apsnd (fn test => test ctxt));
in (fn t => map_filter (fn (testnm, test) => if test t then SOME testnm else NONE) tests) end;
fun used_facts_attribs ctxt thm =
let
val fact_nms = used_facts (SOME ctxt) thm;
val attribs_of = attribs_of ctxt;
in map (apsnd attribs_of) fact_nms end
local
fun app3 f g h x = (f x, g x, h x);
datatype ('a, 'b) Either =
Left of 'a
| Right of 'b;
local
fun partition_map_foldr f (x, (ls, rs)) =
case f x of
Left l => (l :: ls, rs)
| Right r => (ls, r :: rs);
in
fun partition_map f = List.foldr (partition_map_foldr f) ([], []);
end
(*
Extracts the bits we care about from a thm_node: the name, the prop,
and (the next steps of) the proof.
*)
val thm_node_dest =
app3
Proofterm.thm_node_name
Proofterm.thm_node_prop
(Proofterm.thm_node_body #> Future.join);
(*
Partitioning function for thm_node data. We want to insert any named props,
then recursively find the named props used by any unnamed intermediate/anonymous props.
*)
fun insert_or_descend (name, prop, proof) =
if name = "" then Right proof else Left (name, prop);
(*
Extracts the next layer of proof data from a proof step.
*)
val next_level = thms_of #> List.map (snd #> thm_node_dest);
(*
Secretly used as a set, using `()` as the values.
*)
structure NamePropTab = Table(
type key = string * term;
val ord = prod_ord fast_string_ord Term_Ord.fast_term_ord);
val insert_all = List.foldr (fn (k, tab) => NamePropTab.update (k, ()) tab)
(*
Proofterm.fold_body_thms unconditionally recursively descends into the proof body,
so instead of only getting the topmost named props we'd get _all_ of them. Here
we do a more controlled recursion.
*)
fun used_props_foldr (proof, named_props) =
let
val (to_insert, child_proofs) =
proof |> next_level |> partition_map insert_or_descend;
val thms = insert_all named_props to_insert;
in
List.foldr used_props_foldr thms child_proofs
end;
(*
Extracts the outermost proof step of a thm (which is just "the proof of the prop of the thm").
*)
val initial_proof =
Thm.proof_body_of
#> thms_of
#> List.hd
#> snd
#> Proofterm.thm_node_body
#> Future.join;
in
fun used_named_props_of thm =
let val used_props = used_props_foldr (initial_proof thm, NamePropTab.empty);
in used_props |> NamePropTab.keys
end;
end
val proof_body_prop_of =
Thm.proof_body_of
#> thms_of
#> List.hd
#> snd
#> Proofterm.thm_node_prop
local
fun thm_matches prop thm = proof_body_prop_of thm = prop
fun entry ctxt prop (name, idx) =
name
|> try (Proof_Context.get_thms ctxt)
|> Option.mapPartial (maybe_nth (idx - 1))
|> Option.mapPartial (Option.filter (thm_matches prop))
|> Option.map (K (name, SOME idx))
fun warn_if_ambiguous
name
(idx_result: (string * int option) option)
(non_idx_result: (string * int option) option) =
if is_some idx_result andalso is_some non_idx_result
then warning (
"Levity: found two possible results for name " ^ quote name ^ " with the same prop:\n" ^
(@{make_string} (the idx_result)) ^ ",\nand\n" ^
(@{make_string} (the non_idx_result)) ^ ".\nUsing the first one.")
else ()
in
fun disambiguate_indices ctxt (name, prop) =
let
val entry = entry ctxt prop
val idx_result = (base_and_index name) |> Option.mapPartial entry
val non_idx_result = (name, 1) |> entry |> Option.map (apsnd (K NONE))
val _ = warn_if_ambiguous name idx_result non_idx_result
in
merge_options (idx_result, non_idx_result)
end
end
(* We identify "apply" applications by the document position of their corresponding method.
We can only get a document position out of "real" methods, so internal methods
(i.e. Method.Basic) won't have a position.*)
fun get_pos_of_text' (Method.Source src) = SOME (snd (Token.name_of_src src))
| get_pos_of_text' (Method.Combinator (_, _, texts)) = get_first get_pos_of_text' texts
| get_pos_of_text' _ = NONE
(* We only want to apply our hooks in batch mode, so we test if our position has a line number
(in jEdit it will only have an id number) *)
fun get_pos_of_text text = case get_pos_of_text' text of
SOME pos => if is_some (Position.line_of pos) then SOME pos else NONE
| NONE => NONE
(* Clear the theorem dependencies using the apply_trace oracle, then
pick up the new ones after the apply step is finished. *)
fun pre_apply_hook ctxt text thm =
case get_pos_of_text text of NONE => thm
| SOME _ =>
if Apply_Trace.can_clear (Proof_Context.theory_of ctxt)
then Apply_Trace.clear_deps thm
else thm;
val post_apply_hook = (fn ctxt => fn text => fn pre_thm => fn post_thm =>
case get_pos_of_text text of NONE => post_thm
| SOME pos => if Apply_Trace.can_clear (Proof_Context.theory_of ctxt) then
(let
val thy_nm = Context.theory_name (Thm.theory_of_thm post_thm);
val used_facts = the_default [] (try (used_facts_attribs ctxt) post_thm);
val _ =
Synchronized.change applys
(Symtab.map_default
(thy_nm, Postab_strict.empty) (Postab_strict.update (pos, used_facts)))
(* We want to keep our old theorem dependencies around, so we put them back into
the goal thm when we are done *)
val post_thm' = post_thm
|> Apply_Trace.join_deps pre_thm
in post_thm' end)
else post_thm)
(* The Proof hooks need to be patched in to track apply dependencies, but the rest of levity
can work without them. Here we graciously fail if the hook interface is missing *)
fun setup_pre_apply_hook () =
try (ML_Context.eval ML_Compiler.flags Position.none)
(ML_Lex.read_text ("Proof.set_pre_apply_hook AutoLevity_Base.pre_apply_hook", Position.none));
fun setup_post_apply_hook () =
try (ML_Context.eval ML_Compiler.flags Position.none)
(ML_Lex.read_text ("Proof.set_post_apply_hook AutoLevity_Base.post_apply_hook", Position.none));
(* This command is treated specially by AutoLevity_Theory_Report. The command executed directly
after this one will be tagged with the given tag *)
val _ =
Outer_Syntax.command @{command_keyword levity_tag} "tag for levity"
(Parse.string >> (fn str =>
Toplevel.local_theory NONE NONE
(Local_Theory.raw_theory (set_levity_tag (SOME str)))))
fun get_subgoals' state =
let
val proof_state = Toplevel.proof_of state;
val {goal, ...} = Proof.raw_goal proof_state;
in Thm.nprems_of goal end
fun get_subgoals state = the_default ~1 (try get_subgoals' state);
fun setup_toplevel_command_hook () =
Toplevel.add_hook (fn transition => fn start_state => fn end_state =>
let val name = Toplevel.name_of transition
val pos = Toplevel.pos_of transition;
val thy = Toplevel.theory_of start_state;
val thynm = Context.theory_name thy;
val end_thy = Toplevel.theory_of end_state;
in
if name = "clear_deps" orelse name = "dummy_apply" orelse Position.line_of pos = NONE then () else
(let
val levity_input = if name = "levity_tag" then get_levity_tag end_thy else NONE;
val subgoals = get_subgoals start_state;
val entry = {levity_tag = levity_input, subgoals = subgoals}
val _ =
Synchronized.change transactions
(Symtab.map_default (thynm, (Postab_strict.empty, Postab_strict.empty))
(apfst (Postab_strict.update (pos, (name, entry)))))
in () end) handle e => if Exn.is_interrupt e then Exn.reraise e else
Synchronized.change transactions
(Symtab.map_default (thynm, (Postab_strict.empty, Postab_strict.empty))
(apsnd (Postab_strict.map_default (pos, []) (cons (@{make_string} e)))))
end)
fun setup_attrib_tests theory = if not (is_simp_installed) then
error "Missing interface into Raw_Simplifier. Can't trace apply statements with unpatched isabelle."
else
let
(* FIXME: mk_rews not exported any more in Raw_Simplifier
fun is_first_cong ctxt thm =
let
val simpset = dest_ss (Raw_Simplifier.simpset_of ctxt);
val congs = #congs simpset;
val cong_thm = #mk_cong (#mk_rews simpset) ctxt thm;
in
case (find_first (fn (_, thm') => Thm.eq_thm_prop (cong_thm, thm')) congs) of
SOME (nm, _) =>
Thm.eq_thm_prop (find_first (fn (nm', _) => nm' = nm) congs |> the |> snd, cong_thm)
| NONE => false
end
*)
fun is_classical proj ctxt thm =
let
val intros = proj (Classical.claset_of ctxt |> Classical.rep_cs);
val results = Item_Net.retrieve intros (Thm.full_prop_of thm);
in exists (fn (thm', _, _) => Thm.eq_thm_prop (thm',thm)) results end
in
theory
|> add_attribute_test "simp" is_simp
(* |> add_attribute_test "cong" is_first_cong FIXME: see above *)
|> add_attribute_test "intro" (is_classical #unsafeIs)
|> add_attribute_test "intro!" (is_classical #safeIs)
|> add_attribute_test "elim" (is_classical #unsafeEs)
|> add_attribute_test "elim!" (is_classical #safeEs)
|> add_attribute_test "dest" (fn ctxt => fn thm => is_classical #unsafeEs ctxt (Tactic.make_elim thm))
|> add_attribute_test "dest!" (fn ctxt => fn thm => is_classical #safeEs ctxt (Tactic.make_elim thm))
end
fun setup_command_hook {trace_apply, ...} theory =
if get_command_hook_flag theory then theory else
let
val _ = if trace_apply then
(the (setup_pre_apply_hook ());
the (setup_post_apply_hook ()))
handle Option => error "Missing interface into Proof module. Can't trace apply statements with unpatched isabelle"
else ()
val _ = setup_toplevel_command_hook ();
val theory' = theory
|> trace_apply ? setup_attrib_tests
|> set_command_hook_flag
in theory' end;
end
\<close>
end