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