1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 * 10 * Base of autolevity. 11 * Needs to be installed to track command start/end locations 12 *) 13 14theory AutoLevity_Base 15imports Main Apply_Trace 16keywords "levity_tag" :: thy_decl 17begin 18 19 20ML \<open> 21fun is_simp (_: Proof.context) (_: thm) = true 22\<close> 23 24ML \<open> 25val is_simp_installed = is_some ( 26 try (ML_Context.eval ML_Compiler.flags @{here}) 27 (ML_Lex.read_pos @{here} "val is_simp = Raw_Simplifier.is_simp")); 28\<close> 29 30ML\<open> 31(* Describing a ordering on Position.T. Optionally we compare absolute document position, or 32 just line numbers. Somewhat complicated by the fact that jEdit positions don't have line or 33 file identifiers. *) 34 35fun pos_ord use_offset (pos1, pos2) = 36 let 37 fun get_offset pos = if use_offset then Position.offset_of pos else SOME 0; 38 39 fun get_props pos = 40 (SOME (Position.file_of pos |> the, 41 (Position.line_of pos |> the, 42 get_offset pos |> the)), NONE) 43 handle Option => (NONE, Position.parse_id pos) 44 45 val props1 = get_props pos1; 46 val props2 = get_props pos2; 47 48 in prod_ord 49 (option_ord (prod_ord string_ord (prod_ord int_ord int_ord))) 50 (option_ord (int_ord)) 51 (props1, props2) end 52 53structure Postab = Table(type key = Position.T val ord = (pos_ord false)); 54structure Postab_strict = Table(type key = Position.T val ord = (pos_ord true)); 55 56 57signature AUTOLEVITY_BASE = 58sig 59type extras = {levity_tag : string option, subgoals : int} 60 61 62 63val get_transactions : unit -> ((string * extras) Postab_strict.table * string list Postab_strict.table) Symtab.table; 64 65val get_applys : unit -> ((string * string list) list) Postab_strict.table Symtab.table; 66 67val add_attribute_test: string -> (Proof.context -> thm -> bool) -> theory -> theory; 68 69val attribs_of: Proof.context -> thm -> string list; 70 71val used_facts: Proof.context option -> thm -> (string * thm) list; 72val used_facts_attribs: Proof.context -> thm -> (string * string list) list; 73 74(* Install toplevel hook for tracking command positions. *) 75 76val setup_command_hook: {trace_apply : bool} -> theory -> theory; 77 78(* Used to trace the dependencies of all apply statements. 79 They are set up by setup_command_hook if the appropriate hooks in the "Proof" 80 module exist. *) 81 82val pre_apply_hook: Proof.context -> Method.text -> thm -> thm; 83val post_apply_hook: Proof.context -> Method.text -> thm -> thm -> thm; 84 85 86end; 87 88 89 90 91structure AutoLevity_Base : AUTOLEVITY_BASE = 92struct 93 94val applys = Synchronized.var "applys" 95 (Symtab.empty : (((string * string list) list) Postab_strict.table) Symtab.table) 96 97fun get_applys () = Synchronized.value applys; 98 99type extras = {levity_tag : string option, subgoals : int} 100 101 102val transactions = Synchronized.var "hook" 103 (Symtab.empty : ((string * extras) Postab_strict.table * ((string list) Postab_strict.table)) Symtab.table); 104 105fun get_transactions () = 106 Synchronized.value transactions; 107 108 109structure Data = Theory_Data 110 ( 111 type T = (bool * 112 string option * 113 (Proof.context -> thm -> bool) Symtab.table); (* command_hook * levity tag * attribute tests *) 114 val empty = (false, NONE, Symtab.empty); 115 val extend = I; 116 fun merge (((b1, _, tab), (b2, _, tab')) : T * T) = (b1 orelse b2, NONE, Symtab.merge (fn _ => true) (tab, tab')); 117 ); 118 119val set_command_hook_flag = Data.map (@{apply 3(1)} (fn _ => true)); 120val get_command_hook_flag = #1 o Data.get 121 122fun set_levity_tag tag = Data.map (@{apply 3(2)} (fn _ => tag)); 123val get_levity_tag = #2 o Data.get 124 125fun update_attrib_tab f = Data.map (@{apply 3(3)} f); 126 127 128fun add_attribute_test nm f = 129let 130 val f' = (fn ctxt => fn thm => the_default false (try (f ctxt) thm)) 131in update_attrib_tab (Symtab.update_new (nm,f')) end; 132 133val get_attribute_tests = Symtab.dest o #3 o Data.get; 134 135(* Internal fact names get the naming scheme "foo_3" to indicate the third 136 member of the multi-thm "foo". We need to do some work to guess if 137 such a fact refers to an indexed multi-thm or a real fact named "foo_3" *) 138 139fun base_and_index nm = 140let 141 val exploded = space_explode "_" nm; 142 val base = 143 (exploded, (length exploded) - 1) 144 |> try (List.take #> space_implode "_") 145 |> Option.mapPartial (Option.filter (fn nm => nm <> "")) 146 val idx = exploded |> try (List.last #> Int.fromString) |> Option.join; 147in 148 case (base, idx) of 149 (SOME base, SOME idx) => SOME (base, idx) 150 | _ => NONE 151end 152 153 154fun fact_from_derivation ctxt prop xnm = 155let 156 val facts = Proof_Context.facts_of ctxt; 157 (* TODO: Check that exported local fact is equivalent to external one *) 158 159 fun maybe_nth idx xs = idx |> try (curry List.nth xs) 160 161 fun check_prop thm = Thm.full_prop_of thm = prop 162 163 fun entry (name, idx) = 164 (name, Position.none) 165 |> try (Facts.retrieve (Context.Proof ctxt) facts) 166 |> Option.mapPartial (#thms #> maybe_nth (idx - 1)) 167 |> Option.mapPartial (Option.filter check_prop) 168 |> Option.map (pair name) 169 170 val idx_result = (base_and_index xnm) |> Option.mapPartial entry 171 val non_idx_result = (xnm, 1) |> entry 172 173 val _ = 174 if is_some idx_result andalso is_some non_idx_result 175 then warning ( 176 "Levity: found two possible results for name " ^ quote xnm ^ " with the same prop:\n" ^ 177 (@{make_string} (the idx_result)) ^ ",\nand\n" ^ 178 (@{make_string} (the non_idx_result)) ^ ".\nUsing the first one.") 179 else () 180in 181 merge_options (idx_result, non_idx_result) 182end 183 184 185(* Local facts (from locales) aren't marked in proof bodies, we only 186 see their external variants. We guess the local name from the external one 187 (i.e. "Theory_Name.Locale_Name.foo" -> "foo") 188 189 This is needed to perform localized attribute tests (e.g.. is this locale assumption marked as simp?) *) 190 191(* TODO: extend_locale breaks this naming scheme by adding the "chunk" qualifier. This can 192 probably just be handled as a special case *) 193 194fun most_local_fact_of ctxt xnm prop = 195let 196 val local_name = xnm |> try (Long_Name.explode #> tl #> tl #> Long_Name.implode) 197 val local_result = local_name |> Option.mapPartial (fact_from_derivation ctxt prop) 198 fun global_result () = fact_from_derivation ctxt prop xnm 199in 200 if is_some local_result then local_result else global_result () 201end 202 203(* We recursively descend into the proof body to find dependent facts. 204 We skip over empty derivations or facts that we fail to find, but recurse 205 into their dependents. This ensures that an attempt to re-build the proof dependencies 206 graph will result in a connected graph. *) 207 208fun thms_of (PBody {thms,...}) = thms 209 210fun proof_body_deps 211 (filter_name: string -> bool) 212 (get_fact: string -> term -> (string * thm) option) 213 (thm_ident, thm_node) 214 (tab: (string * thm) option Inttab.table) = 215let 216 val name = Proofterm.thm_node_name thm_node 217 val body = Proofterm.thm_node_body thm_node 218 val prop = Proofterm.thm_node_prop thm_node 219 val result = if filter_name name then NONE else get_fact name prop 220 val is_new_result = not (Inttab.defined tab thm_ident) 221 val insert = if is_new_result then Inttab.update (thm_ident, result) else I 222 val descend = 223 if is_new_result andalso is_none result 224 then fold (proof_body_deps filter_name get_fact) (thms_of (Future.join body)) 225 else I 226in 227 tab |> insert |> descend 228end 229 230fun used_facts opt_ctxt thm = 231let 232 val nm = Thm.get_name_hint thm; 233 val get_fact = 234 case opt_ctxt of 235 SOME ctxt => most_local_fact_of ctxt 236 | NONE => fn name => fn _ => (SOME (name, Drule.dummy_thm)); 237 val body = thms_of (Thm.proof_body_of thm); 238 fun filter_name nm' = nm' = "" orelse nm' = nm; 239in 240 fold (proof_body_deps filter_name get_fact) body Inttab.empty 241 |> Inttab.dest |> map_filter snd 242end 243 244fun attribs_of ctxt = 245let 246 val tests = get_attribute_tests (Proof_Context.theory_of ctxt) 247 |> map (apsnd (fn test => test ctxt)); 248 249in (fn t => map_filter (fn (testnm, test) => if test t then SOME testnm else NONE) tests) end; 250 251fun used_facts_attribs ctxt thm = 252let 253 val fact_nms = used_facts (SOME ctxt) thm; 254 255 val attribs_of = attribs_of ctxt; 256 257in map (apsnd attribs_of) fact_nms end 258 259(* We identify "apply" applications by the document position of their corresponding method. 260 We can only get a document position out of "real" methods, so internal methods 261 (i.e. Method.Basic) won't have a position.*) 262 263fun get_pos_of_text' (Method.Source src) = SOME (snd (Token.name_of_src src)) 264 | get_pos_of_text' (Method.Combinator (_, _, texts)) = get_first get_pos_of_text' texts 265 | get_pos_of_text' _ = NONE 266 267(* We only want to apply our hooks in batch mode, so we test if our position has a line number 268 (in jEdit it will only have an id number) *) 269 270fun get_pos_of_text text = case get_pos_of_text' text of 271 SOME pos => if is_some (Position.line_of pos) then SOME pos else NONE 272 | NONE => NONE 273 274(* Clear the theorem dependencies using the apply_trace oracle, then 275 pick up the new ones after the apply step is finished. *) 276 277fun pre_apply_hook ctxt text thm = 278 case get_pos_of_text text of NONE => thm 279 | SOME _ => 280 if Apply_Trace.can_clear (Proof_Context.theory_of ctxt) 281 then Apply_Trace.clear_deps thm 282 else thm; 283 284 285val post_apply_hook = (fn ctxt => fn text => fn pre_thm => fn post_thm => 286 case get_pos_of_text text of NONE => post_thm 287 | SOME pos => if Apply_Trace.can_clear (Proof_Context.theory_of ctxt) then 288 (let 289 val thy_nm = Context.theory_name (Thm.theory_of_thm post_thm); 290 291 val used_facts = the_default [] (try (used_facts_attribs ctxt) post_thm); 292 val _ = 293 Synchronized.change applys 294 (Symtab.map_default 295 (thy_nm, Postab_strict.empty) (Postab_strict.update (pos, used_facts))) 296 297 (* We want to keep our old theorem dependencies around, so we put them back into 298 the goal thm when we are done *) 299 300 val post_thm' = post_thm 301 |> Apply_Trace.join_deps pre_thm 302 303 in post_thm' end) 304 else post_thm) 305 306(* The Proof hooks need to be patched in to track apply dependencies, but the rest of levity 307 can work without them. Here we graciously fail if the hook interface is missing *) 308 309fun setup_pre_apply_hook () = 310 try (ML_Context.eval ML_Compiler.flags @{here}) 311 (ML_Lex.read_pos @{here} "Proof.set_pre_apply_hook AutoLevity_Base.pre_apply_hook"); 312 313fun setup_post_apply_hook () = 314 try (ML_Context.eval ML_Compiler.flags @{here}) 315 (ML_Lex.read_pos @{here} "Proof.set_post_apply_hook AutoLevity_Base.post_apply_hook"); 316 317(* This command is treated specially by AutoLevity_Theory_Report. The command executed directly 318 after this one will be tagged with the given tag *) 319 320val _ = 321 Outer_Syntax.command @{command_keyword levity_tag} "tag for levity" 322 (Parse.string >> (fn str => 323 Toplevel.local_theory NONE NONE 324 (Local_Theory.raw_theory (set_levity_tag (SOME str))))) 325 326fun get_subgoals' state = 327let 328 val proof_state = Toplevel.proof_of state; 329 val {goal, ...} = Proof.raw_goal proof_state; 330in Thm.nprems_of goal end 331 332fun get_subgoals state = the_default ~1 (try get_subgoals' state); 333 334fun setup_toplevel_command_hook () = 335Toplevel.add_hook (fn transition => fn start_state => fn end_state => 336 let val name = Toplevel.name_of transition 337 val pos = Toplevel.pos_of transition; 338 val thy = Toplevel.theory_of start_state; 339 val thynm = Context.theory_name thy; 340 val end_thy = Toplevel.theory_of end_state; 341 in 342 if name = "clear_deps" orelse name = "dummy_apply" orelse Position.line_of pos = NONE then () else 343 (let 344 345 val levity_input = if name = "levity_tag" then get_levity_tag end_thy else NONE; 346 347 val subgoals = get_subgoals start_state; 348 349 val entry = {levity_tag = levity_input, subgoals = subgoals} 350 351 val _ = 352 Synchronized.change transactions 353 (Symtab.map_default (thynm, (Postab_strict.empty, Postab_strict.empty)) 354 (apfst (Postab_strict.update (pos, (name, entry))))) 355 in () end) handle e => if Exn.is_interrupt e then Exn.reraise e else 356 Synchronized.change transactions 357 (Symtab.map_default (thynm, (Postab_strict.empty, Postab_strict.empty)) 358 (apsnd (Postab_strict.map_default (pos, []) (cons (@{make_string} e))))) 359 end) 360 361fun setup_attrib_tests theory = if not (is_simp_installed) then 362error "Missing interface into Raw_Simplifier. Can't trace apply statements with unpatched isabelle." 363else 364let 365 fun is_first_cong ctxt thm = 366 let 367 val simpset = Raw_Simplifier.internal_ss (Raw_Simplifier.simpset_of ctxt); 368 val (congs, _) = #congs simpset; 369 val cong_thm = #mk_cong (#mk_rews simpset) ctxt thm; 370 in 371 case (find_first (fn (_, thm') => Thm.eq_thm_prop (cong_thm, thm')) congs) of 372 SOME (nm, _) => 373 Thm.eq_thm_prop (find_first (fn (nm', _) => nm' = nm) congs |> the |> snd, cong_thm) 374 | NONE => false 375 end 376 377 fun is_classical proj ctxt thm = 378 let 379 val intros = proj (Classical.claset_of ctxt |> Classical.rep_cs); 380 val results = Item_Net.retrieve intros (Thm.full_prop_of thm); 381 in exists (fn (thm', _, _) => Thm.eq_thm_prop (thm',thm)) results end 382in 383 theory 384|> add_attribute_test "simp" is_simp 385|> add_attribute_test "cong" is_first_cong 386|> add_attribute_test "intro" (is_classical #unsafeIs) 387|> add_attribute_test "intro!" (is_classical #safeIs) 388|> add_attribute_test "elim" (is_classical #unsafeEs) 389|> add_attribute_test "elim!" (is_classical #safeEs) 390|> add_attribute_test "dest" (fn ctxt => fn thm => is_classical #unsafeEs ctxt (Tactic.make_elim thm)) 391|> add_attribute_test "dest!" (fn ctxt => fn thm => is_classical #safeEs ctxt (Tactic.make_elim thm)) 392end 393 394 395fun setup_command_hook {trace_apply, ...} theory = 396if get_command_hook_flag theory then theory else 397let 398 val _ = if trace_apply then 399 (the (setup_pre_apply_hook ()); 400 the (setup_post_apply_hook ())) 401 handle Option => error "Missing interface into Proof module. Can't trace apply statements with unpatched isabelle" 402 else () 403 404 val _ = setup_toplevel_command_hook (); 405 406 val theory' = theory 407 |> trace_apply ? setup_attrib_tests 408 |> set_command_hook_flag 409 410in theory' end; 411 412 413end 414\<close> 415 416end 417