1structure Cache :> Cache = 2struct 3 4open HolKernel liteLib Trace Abbrev boolSyntax boolLib 5 6 7type key = term 8type hypinfo = {hyps : term HOLset.set, thms : term HOLset.set} 9type data = (hypinfo * thm option) list 10 11type table = (key, data) Redblackmap.dict 12val empty_table = Redblackmap.mkDict Term.compare : table 13 14type cache = table Sref.t 15fun c_insert c (k,v) = Sref.update c (fn t => Redblackmap.insert(t,k,v)) 16fun cvalue (c:cache) = Sref.value c 17fun new_cache() : cache = Sref.new empty_table 18 19val empty_hypinfo = {hyps = empty_tmset, thms = empty_tmset} 20fun hypinfo_addth (th, {hyps,thms}) = 21 {hyps = HOLset.union(hyps, hypset th), thms = HOLset.add(thms, concl th)} 22val all_hyps = List.foldl hypinfo_addth empty_hypinfo 23 24infix <<; (* A subsetof B *) 25fun {hyps=h1,thms=ths1} << {hyps=h2,thms=ths2} = 26 HOLset.isSubset(h1,h2) andalso HOLset.isSubset(ths1, ths2) 27val _ = op<< : hypinfo * hypinfo -> bool 28fun hypinfo_list {hyps,thms} = HOLset.foldl op:: (HOLset.listItems hyps) thms 29fun hypinfo_isEmpty ({hyps,thms}:hypinfo) = 30 HOLset.isEmpty hyps andalso HOLset.isEmpty thms 31 32exception NOT_FOUND 33exception FIRST 34fun first p [] = raise FIRST 35 | first p (h::t) = if p h then h else first p t 36 37fun CACHE (filt,conv) = let 38 val cache = new_cache() 39 fun cache_proc thms tm = let 40 val _ = if (filt tm) then () 41 else failwith "CACHE_CCONV: not applicable" 42 val prevs = Redblackmap.find (cvalue cache, tm) 43 handle Redblackmap.NotFound => [] 44 val curr = all_hyps thms 45 fun ok (prev,SOME thm) = prev << curr 46 | ok (prev,NONE) = curr << prev 47 in 48 (case snd (first ok prevs) of 49 SOME x => (trace(1,PRODUCE(tm,"cache hit!",x)); x) 50 | NONE => failwith "cache hit was failure") 51 handle FIRST => let 52 val thm = conv thms tm 53 handle e as (HOL_ERR _) => 54 (trace(2, 55 REDUCE("Inserting failed ctxt", 56 if hypinfo_isEmpty curr then tm 57 else 58 mk_imp(list_mk_conj (hypinfo_list curr), 59 tm))) ; 60 c_insert cache (tm, (curr,NONE)::prevs); 61 raise e) 62 in 63 (trace(2,PRODUCE(tm, "Inserting into cache:", thm)); 64 c_insert cache (tm,(curr,SOME thm)::prevs); 65 thm) 66 end 67 end 68in 69 (cache_proc, cache) 70end 71 72fun clear_cache cache = (Sref.update cache (fn c => empty_table)) 73 74fun cache_values (cache : cache) = let 75 val items = Redblackmap.listItems (cvalue cache) 76 fun tolist (set, thmopt) = (hypinfo_list set, thmopt) 77 fun ToList (k, stlist) = (k, map tolist stlist) 78in 79 map ToList items 80end 81 82 83(* ---------------------------------------------------------------------- 84 RCACHE 85 86 Cached decision procedures have always recorded both the successes 87 and the failures of the underlying d.p. With failures recorded, 88 the system will not repeatedly try (and fail) to solve the same 89 goal. However, the underlying decision procedures are 90 context-aware, and the context as well the goal attempted is 91 stored in the cache. 92 93 If a success is stored with context C, and the context of the 94 latest attempt is a superset of C, then the cache's stored 95 information can be accepted. Conversely, if there is a failure 96 stored in the cache, and a new attempt is made to prove the same 97 goal, with a smaller context, then the cache's verdict can be 98 accepted immediately. On the other hand, if this means that the 99 latest attempt has a larger context, and what's stored is a 100 failure, then a fresh call to the underlying decision procedure is 101 called for. 102 103 However, if the context in the latest attempt is only larger 104 because of the addition of irrelevant new assumptions (those that 105 do not mention any variables from the underlying goal), then they 106 shouldn't make any difference, and trying the goal again with this 107 bigger context will just result in a slower failure. That is, 108 unless the new assumptions introduce a contradiction with other 109 irrelevants bits of the assumptions. 110 111 The RCACHE code does a connected components analysis to split 112 problems up, and the sub-problems are tried (and cached!) 113 independently. 114 115 ---------------------------------------------------------------------- *) 116 117fun ccs G vs = let 118 (* G is a Binarymap from terms to term sets, with the set representing 119 the adjacent nodes in the graph. The graph is undirected so 120 there will be two entries for each link. 121 vs is a list of all the terms in G. *) 122 fun recurse acc visited v = let 123 (* v is already in acc and visited *) 124 val neighbours = Binarymap.find (G, v) 125 handle Binarymap.NotFound => empty_tmset 126 fun visit_neighbour(n, (acc, visited)) = 127 if HOLset.member(visited, n) then (acc, visited) 128 else recurse (n::acc) (HOLset.add(visited, n)) n 129 in 130 HOLset.foldl visit_neighbour (acc, visited) neighbours 131 end 132 fun find_component visited v = (* v is not in visited *) 133 recurse [v] (HOLset.add(visited, v)) v 134 fun find_component_acc(v, (acc,visited)) = 135 if HOLset.member (visited, v) then (acc,visited) 136 else let 137 val (vcomp, visited') = find_component visited v 138 in 139 (vcomp::acc, visited') 140 end 141in 142 List.foldl find_component_acc ([], empty_tmset) vs 143end 144 145fun make_links fvs_of (t, G) = let 146 val fvs = fvs_of t 147 fun mk_link1 t1 t2 G = let 148 val newset = 149 case Binarymap.peek(G, t1) of 150 NONE => HOLset.singleton Term.compare t2 151 | SOME s => HOLset.add(s, t2) 152 in 153 Binarymap.insert(G, t1, newset) 154 end 155 fun mk_link t1 t2 G = mk_link1 t1 t2 (mk_link1 t2 t1 G) 156 fun mk_links [] G = G 157 | mk_links [_] G = G 158 | mk_links (x::y::rest) G = mk_link x y (mk_links (y::rest) G) 159 fun enter_domain x G = 160 case Binarymap.peek (G, x) of 161 NONE => Binarymap.insert(G, x, HOLset.empty Term.compare) 162 | SOME _ => G 163in 164 case fvs of 165 [x] => enter_domain x G 166 | _ => mk_links fvs G 167end 168 169(* Creates a graph. Each node is a term where two terms are linked (by 170 the transitive closure of the adjacency relation) if each appears 171 in a term from tmlist. The function parameter fvs_of calculates 172 which sub-terms should be inserted into the graph. 173 174 The "idea" is that only free variables are linked, but the 175 specified fvs_of function may additionally cause other sorts of 176 sub-terms to be treated as variables. 177 178 The implementation (see make_links) just creates a linear sub-graph 179 for each element of tmlist. In other words, if a term gives rise 180 to n subterms, the K_n subgraph is not inserted, only a connected 181 linear graph of those n subterms. The later connected components 182 analysis will realise that all of these sub-terms are part of the 183 same component anyway. 184*) 185fun build_graph fvs_of tmlist = 186 List.foldl (make_links fvs_of) (Binarymap.mkDict Term.compare) tmlist 187 188(* given a list of list of variables; build a map where all the variables 189 in the same list point to the same updatable reference cell *) 190val build_var_to_group_map = let 191 fun foldthis (tlist, acc) = let 192 val r = ref (empty_hypinfo, [] : thm list) 193 in 194 List.foldl (fn (t, acc) => Binarymap.insert(acc, t, r)) acc tlist 195 end 196in 197 List.foldl foldthis (Binarymap.mkDict Term.compare) 198end 199 200 201fun thmlistrefcmp(r1, r2) = 202 if r1 = r2 then EQUAL 203 else Term.compare (concl (hd (!r1)), concl (hd (!r2))) 204 205type context = hypinfo * thm list 206 (* terms are the union of all the theorems hypotheses *) 207datatype result = proved_it of thm 208 | possible_ctxts of context list 209fun mk_goal t = let 210 val ty = type_of t 211in 212 mk_eq(t, if ty = bool then T else mk_arb ty) 213end 214 215fun consider_false_context_cache table original_goal (ctxtlist:context list) = 216 let 217 val cache_F = Redblackmap.find (table, boolSyntax.F) 218 handle Redblackmap.NotFound => [] 219 fun recurse acc ctxts = 220 case ctxts of 221 [] => possible_ctxts acc 222 | (c as (hyps, thlist))::cs => let 223 fun ok (cached, SOME _) = cached << hyps 224 | ok (cached, NONE) = hyps << cached 225 in 226 case List.find ok cache_F of 227 NONE => recurse (c::acc) cs 228 | SOME (_, NONE) => recurse acc cs 229 | SOME (_, SOME th) => 230 (trace(1,PRODUCE(original_goal, 231 "cache hit for contradiction", th)); 232 proved_it (CCONTR (mk_goal original_goal) (EQT_ELIM th))) 233 end 234 in 235 recurse [] ctxtlist 236 end 237 238fun prove_false_context (conv:thm list -> conv) (cache:cache) (ctxtlist:context list) original_goal = let 239 fun recurse clist = 240 case clist of 241 [] => raise mk_HOL_ERR "Cache" "RCACHE" 242 "No (more) possibly false contexts" 243 | (hyps,thms)::cs => let 244 val oldval = Redblackmap.find (cvalue cache, F) 245 handle Redblackmap.NotFound => [] 246 val conjs = list_mk_conj (map concl thms) 247 in 248 case Lib.total (conv thms) boolSyntax.F of 249 SOME th => let 250 val newth = CCONTR (mk_goal original_goal) (EQT_ELIM th) 251 in 252 trace(2,PRODUCE(conjs, "Inserting into cache:", th)); 253 c_insert cache (F, (hyps, SOME th) :: oldval); 254 newth 255 end 256 | NONE => ( 257 trace(2, REDUCE("Inserting failed contradictory context", conjs)); 258 c_insert cache (F, (hyps, NONE)::oldval); 259 recurse cs 260 ) 261 end 262in 263 recurse ctxtlist 264end 265 266fun RCACHE (dpfvs, check, conv) = let 267 val cache = new_cache() 268 fun build_up_ctxt mp th = let 269 val c = concl th 270 in 271 case dpfvs c of 272 [] => () 273 | (v::_) => let 274 val r = Binarymap.find(mp,v) 275 val (oldhyps, oldthms) = !r 276 in 277 r := (hypinfo_addth(th, oldhyps), th::oldthms) 278 end 279 end 280 fun decider ctxt t = let 281 val _ = if check t then () 282 else raise mk_HOL_ERR "Cache" "RCACHE" "not applicable" 283 val prevs = Redblackmap.find (cvalue cache, t) handle NotFound => [] 284 val curr = all_hyps ctxt 285 fun oksome (prev, SOME thm) = prev << curr 286 | oksome (_, NONE) = false 287 in 288 case List.find oksome prevs of 289 SOME (_, SOME x) => (trace(1,PRODUCE(t, "cache hit!", x)); x) 290 | SOME (_, NONE) => raise Fail "RCACHE: Invariant failure" 291 | NONE => let 292 (* do connected component analysis to test for false *) 293 fun foldthis (th, (ctxt_ts, ground_ths)) = let 294 val c = concl th 295 in 296 if null (dpfvs c) then (ctxt_ts, th::ground_ths) 297 else (c::ctxt_ts, ground_ths) 298 end 299 val (ctxt_ts,ground_ctxt_ths) = 300 List.foldl foldthis ([], []) ctxt 301 val G = build_graph dpfvs (t::ctxt_ts) 302 (* G a map from v to v's neighbours *) 303 val vs = Binarymap.foldl (fn (k,v,acc) => k::acc) [] G 304 val (comps, _) = ccs G vs 305 (* a list of lists of variables *) 306 val group_map = build_var_to_group_map comps 307 val _ = app (build_up_ctxt group_map) ctxt 308 (* group map is a map from variables to all the 309 ctxts (theorems) that are in that variable's component *) 310 311 (* now extract the ctxt relevant for the goal statement *) 312 val (group_map', glstmtref) = 313 case dpfvs t of 314 [] => (group_map, ref (empty_hypinfo, [])) 315 | (glvar::_) => Binarymap.remove(group_map, glvar) 316 317 (* and the remaining contexts, ensuring there are no 318 duplicate copies *) 319 fun foldthis (k, v, acc as (setlist, seenreflist)) = 320 if mem v seenreflist then acc 321 else (!v::setlist, v::seenreflist) 322 val (divided_clist0, _) = 323 Binarymap.foldl foldthis ([], [glstmtref]) group_map' 324 325 (* fold in every ground hypothesis as a separate context, entire 326 unto itself *) 327 val divided_clist = 328 divided_clist0 @ 329 map (fn th => (hypinfo_addth(th, empty_hypinfo), [th])) 330 ground_ctxt_ths 331 332 val (glhyps, thmlist) = !glstmtref 333 fun oknone (prev, NONE) = glhyps << prev 334 | oknone _ = false 335 in 336 case List.find oknone prevs of 337 NONE => let 338 (* nothing cached, but should still try cache for proving 339 false from the context *) 340 in 341 case consider_false_context_cache (cvalue cache) t divided_clist 342 of 343 proved_it th => th 344 | possible_ctxts cs => let 345 (* cs is the list of things worth trying to prove, but 346 in this situation should first try conv on the original 347 goal because there's nothing in the cache about it *) 348 in 349 case Lib.total (conv thmlist) t of 350 SOME th => let 351 in 352 trace(2,PRODUCE(t,"Inserting into cache:", th)); 353 c_insert cache (t, (glhyps,SOME th)::prevs); 354 th 355 end 356 | NONE => let 357 in 358 trace(2, REDUCE("Inserting failure to prove", 359 if hypinfo_isEmpty glhyps then t 360 else mk_imp(list_mk_conj 361 (map concl thmlist), t))); 362 c_insert cache (t, (glhyps, NONE)::prevs); 363 prove_false_context conv cache cs t 364 end 365 end 366 end 367 | SOME (_, NONE) => let 368 (* with the relevant context, our goal doesn't resolve one 369 way or the other. However, it's possible that part of the 370 rest of the context goes to false *) 371 in 372 case consider_false_context_cache (cvalue cache) t divided_clist of 373 proved_it th => th 374 | possible_ctxts cs => prove_false_context conv cache cs t 375 end 376 | SOME _ => raise Fail "RCACHE: invariant failure the second" 377 end 378 end 379in 380 (decider,cache) 381end 382 383end (* struct *) 384