1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Backend for tracing apply statements. Useful for doing proof step dependency analysis. 8 * Provides an alternate refinement function which takes an additional stateful journaling operation. *) 9theory Apply_Trace 10imports 11 Main 12 "MLUtils" 13begin 14 15 16ML \<open> 17signature APPLY_TRACE = 18sig 19 val apply_results : 20 {silent_fail : bool} -> 21 (Proof.context -> thm -> ((string * int option) * term) list -> unit) -> 22 Method.text_range -> Proof.state -> Proof.state Seq.result Seq.seq 23 24 (* Lower level interface. *) 25 val can_clear : theory -> bool 26 val clear_deps : thm -> thm 27 val join_deps : thm -> thm -> thm 28 val used_facts : Proof.context -> thm -> ((string * int option) * term) list 29 val pretty_deps: bool -> (string * Position.T) option -> Proof.context -> thm -> 30 ((string * int option) * term) list -> Pretty.T 31end 32 33structure Apply_Trace : APPLY_TRACE = 34struct 35 36(*TODO: Add more robust oracle without hyp clearing *) 37fun thm_to_cterm keep_hyps thm = 38let 39 40 val thy = Thm.theory_of_thm thm 41 val pairs = Thm.tpairs_of thm 42 val ceqs = map (Thm.global_cterm_of thy o Logic.mk_equals) pairs 43 val hyps = Thm.chyps_of thm 44 val prop = Thm.cprop_of thm 45 val thm' = if keep_hyps then Drule.list_implies (hyps,prop) else prop 46 47in 48 Drule.list_implies (ceqs,thm') end 49 50 51val (_, clear_thm_deps') = 52 Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "count_cheat", thm_to_cterm false))); 53 54fun clear_deps thm = 55let 56 57 val thm' = try clear_thm_deps' thm 58 |> Option.map (fold (fn _ => fn t => (@{thm Pure.reflexive} RS t)) (Thm.tpairs_of thm)) 59 60in case thm' of SOME thm' => thm' | NONE => error "Can't clear deps here" end 61 62 63fun can_clear thy = Context.subthy(@{theory},thy) 64 65fun join_deps pre_thm post_thm = 66let 67 val pre_thm' = Thm.flexflex_rule NONE pre_thm |> Seq.hd 68 |> Thm.adjust_maxidx_thm (Thm.maxidx_of post_thm + 1) 69in 70 Conjunction.intr pre_thm' post_thm |> Conjunction.elim |> snd 71end 72 73fun get_ref_from_nm' nm = 74let 75 val exploded = space_explode "_" nm; 76 val base = List.take (exploded, (length exploded) - 1) |> space_implode "_" 77 val idx = List.last exploded |> Int.fromString; 78in if is_some idx andalso base <> "" then SOME (base, the idx) else NONE end 79 80fun get_ref_from_nm nm = Option.join (try get_ref_from_nm' nm); 81 82fun maybe_nth l = try (curry List.nth l) 83 84fun fact_from_derivation ctxt xnm = 85let 86 87 val facts = Proof_Context.facts_of ctxt; 88 (* TODO: Check that exported local fact is equivalent to external one *) 89 90 val idx_result = 91 let 92 val (name', idx) = get_ref_from_nm xnm |> the; 93 val entry = try (Facts.retrieve (Context.Proof ctxt) facts) (name', Position.none) |> the; 94 val thm = maybe_nth (#thms entry) (idx - 1) |> the; 95 in SOME (xnm, thm) end handle Option => NONE; 96 97 fun non_idx_result () = 98 let 99 val entry = try (Facts.retrieve (Context.Proof ctxt) facts) (xnm, Position.none) |> the; 100 val thm = try the_single (#thms entry) |> the; 101 in SOME (#name entry, thm) end handle Option => NONE; 102 103in 104 case idx_result of 105 SOME thm => SOME thm 106 | NONE => non_idx_result () 107end 108 109fun most_local_fact_of ctxt xnm = 110let 111 val local_name = try (fn xnm => Long_Name.explode xnm |> tl |> tl |> Long_Name.implode) xnm |> the; 112in SOME (fact_from_derivation ctxt local_name |> the) end handle Option => 113 fact_from_derivation ctxt xnm; 114 115fun thms_of (PBody {thms,...}) = thms 116 117fun proof_body_descend' f get_fact (ident, thm_node) deptab = let 118 val nm = Proofterm.thm_node_name thm_node 119 val body = Proofterm.thm_node_body thm_node 120in 121 (if not (f nm) then 122 (Inttab.update_new (ident, SOME (nm, get_fact nm |> the)) deptab handle Inttab.DUP _ => deptab) 123 else raise Option) handle Option => 124 ((fold (proof_body_descend' f get_fact) (thms_of (Future.join body)) 125 (Inttab.update_new (ident, NONE) deptab)) handle Inttab.DUP _ => deptab) 126end 127 128fun used_facts' f get_fact thm = 129 let 130 val body = thms_of (Thm.proof_body_of thm); 131 132 in fold (proof_body_descend' f get_fact) body Inttab.empty end 133 134fun used_pbody_facts ctxt thm = 135 let 136 val nm = Thm.get_name_hint thm; 137 val get_fact = most_local_fact_of ctxt; 138 in 139 used_facts' (fn nm' => nm' = "" orelse nm' = nm) get_fact thm 140 |> Inttab.dest |> map_filter snd |> map snd |> map (apsnd (Thm.prop_of)) 141 end 142 143fun raw_primitive_text f = Method.Basic (fn _ => ((K (fn (ctxt, thm) => Seq.make_results (Seq.single (ctxt, f thm)))))) 144 145 146(*Find local facts from new hyps*) 147fun used_local_facts ctxt thm = 148let 149 val hyps = Thm.hyps_of thm 150 val facts = Proof_Context.facts_of ctxt |> Facts.dest_static true [] 151 152 fun match_hyp hyp = 153 let 154 fun get (nm,thms) = 155 case (get_index (fn t => if (Thm.prop_of t) aconv hyp then SOME hyp else NONE) thms) 156 of SOME t => SOME (nm,t) 157 | NONE => NONE 158 159 160 in 161 get_first get facts 162 end 163 164in 165 map_filter match_hyp hyps end 166 167fun used_facts ctxt thm = 168 let 169 val used_from_pbody = used_pbody_facts ctxt thm |> map (fn (nm,t) => ((nm,NONE),t)) 170 val used_from_hyps = used_local_facts ctxt thm |> map (fn (nm,(i,t)) => ((nm,SOME i),t)) 171 in 172 (used_from_hyps @ used_from_pbody) 173 end 174 175(* Perform refinement step, and run the given stateful function 176 against computed dependencies afterwards. *) 177fun refine args f text state = 178let 179 180 val ctxt = Proof.context_of state 181 182 val thm = Proof.simple_goal state |> #goal 183 184 fun save_deps deps = f ctxt thm deps 185 186 187in 188 if (can_clear (Proof.theory_of state)) then 189 Proof.refine (Method.Combinator (Method.no_combinator_info,Method.Then, [raw_primitive_text (clear_deps),text, 190 raw_primitive_text (fn thm' => (save_deps (used_facts ctxt thm');join_deps thm thm'))])) state 191 else 192 (if (#silent_fail args) then (save_deps [];Proof.refine text state) else error "Apply_Trace theory must be imported to trace applies") 193end 194 195(* Boilerplate from Proof.ML *) 196 197 198fun method_error kind pos state = 199 Seq.single (Proof_Display.method_error kind pos (Proof.raw_goal state)); 200 201fun apply args f text = Proof.assert_backward #> refine args f text #> 202 Seq.maps_results (Proof.apply ((raw_primitive_text I),(Position.none, Position.none))); 203 204fun apply_results args f (text, range) = 205 Seq.APPEND (apply args f text, method_error "" (Position.range_position range)); 206 207 208structure Filter_Thms = Named_Thms 209( 210 val name = @{binding no_trace} 211 val description = "thms to be ignored from tracing" 212) 213 214(* Print out the found dependencies. *) 215fun pretty_deps only_names query ctxt thm deps = 216let 217 (* Remove duplicates. *) 218 val deps = sort_distinct (prod_ord (prod_ord string_ord (option_ord int_ord)) Term_Ord.term_ord) deps 219 220 (* Fetch canonical names and theorems. *) 221 val deps = map (fn (ident, term) => ThmExtras.adjust_thm_name ctxt ident term) deps 222 223 (* Remove "boring" theorems. *) 224 val deps = subtract (fn (a, ThmExtras.FoundName (_, thm)) => Thm.eq_thm (thm, a) 225 | _ => false) (Filter_Thms.get ctxt) deps 226 227 val deps = case query of SOME (raw_query,pos) => 228 let 229 val pos' = perhaps (try (Position.advance_offsets 1)) pos; 230 val q = Find_Theorems.read_query pos' raw_query; 231 val results = Find_Theorems.find_theorems_cmd ctxt (SOME thm) (SOME 1000000000) false q 232 |> snd 233 |> map ThmExtras.fact_ref_to_name; 234 235 (* Only consider theorems from our query. *) 236 237 val deps = inter (fn (ThmExtras.FoundName (nmidx,_), ThmExtras.FoundName (nmidx',_)) => nmidx = nmidx' 238 | _ => false) results deps 239 in deps end 240 | _ => deps 241 242in 243 if only_names then 244 Pretty.block 245 (Pretty.separate "" (map (ThmExtras.pretty_fact only_names ctxt) deps)) 246 else 247 (* Pretty-print resulting theorems. *) 248 Pretty.big_list "used theorems:" 249 (map (Pretty.item o single o ThmExtras.pretty_fact only_names ctxt) deps) 250 251end 252 253val _ = Context.>> (Context.map_theory Filter_Thms.setup) 254 255end 256\<close> 257 258end 259 260