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