1(*===========================================================================*) 2(* FILE : simpLib.sml *) 3(* DESCRIPTION : A programmable, contextual, conditional simplifier *) 4(* *) 5(* AUTHOR : Donald Syme *) 6(* Based loosely on original HOL rewriting by *) 7(* Larry Paulson et al, *) 8(* and not-so-loosely on the Isabelle simplifier. *) 9(*===========================================================================*) 10 11structure simpLib :> simpLib = 12struct 13 14infix oo; 15 16open HolKernel boolLib liteLib Trace Cond_rewr Travrules Traverse Ho_Net 17 18local open markerTheory in end; 19 20fun ERR x = STRUCT_ERR "simpLib" x ; 21fun WRAP_ERR x = STRUCT_WRAP "simpLib" x; 22 23fun option_cases f e (SOME x) = f x 24 | option_cases f e NONE = e; 25 26fun f oo g = fn x => flatten (map f (g x)); 27 28(*---------------------------------------------------------------------------*) 29(* Representation of conversions manipulated by the simplifier. *) 30(*---------------------------------------------------------------------------*) 31 32type convdata = {name : string, 33 key : (term list * term) option, 34 trace : int, 35 conv : (term list -> term -> thm) -> term list -> conv}; 36 37type stdconvdata = { name: string, 38 pats: term list, 39 conv: conv} 40 41(*---------------------------------------------------------------------------*) 42(* Make a rewrite rule into a conversion. *) 43(*---------------------------------------------------------------------------*) 44 45(* boolean argument to c is whether or not the rewrite is bounded *) 46fun appconv (c,UNBOUNDED) solver stk tm = c false solver stk tm 47 | appconv (c,BOUNDED r) solver stk tm = if !r = 0 then failwith "exceeded rewrite bound" 48 else c true solver stk tm before 49 Portable.dec r 50 51fun mk_rewr_convdata (thm,tag) = let 52 val th = SPEC_ALL thm 53in 54 SOME {name = "<rewrite>", 55 key = SOME (free_varsl (hyp th), lhs(#2 (strip_imp(concl th)))), 56 trace = 100, (* no need to provide extra tracing here; 57 COND_REWR_CONV provides enough tracing itself *) 58 conv = appconv (COND_REWR_CONV th, tag)} before 59 trace(2, LZ_TEXT(fn () => "New rewrite: " ^ thm_to_string th)) 60 handle HOL_ERR _ => 61 (trace (2, LZ_TEXT(fn () => 62 thm_to_string th ^ 63 " dropped (conversion to rewrite failed)")); 64 NONE) 65end 66 67(*---------------------------------------------------------------------------*) 68(* Composable simpset fragments *) 69(*---------------------------------------------------------------------------*) 70 71type relsimpdata = {refl: thm, trans:thm, weakenings:thm list, 72 subsets : thm list, rewrs : thm list} 73 74datatype ssfrag = SSFRAG_CON of { 75 name : string option, 76 convs : convdata list, 77 rewrs : thm list, 78 ac : (thm * thm) list, 79 filter : (controlled_thm -> controlled_thm list) option, 80 dprocs : Traverse.reducer list, 81 congs : thm list, 82 relsimps : relsimpdata list 83} 84 85fun SSFRAG {name,convs,rewrs,ac,filter,dprocs,congs} = 86 SSFRAG_CON {name = name, convs = convs, rewrs = rewrs, ac = ac, 87 filter = filter, dprocs = dprocs, congs = congs, 88 relsimps = []} 89 90(*---------------------------------------------------------------------------*) 91(* Operation on ssfrag values *) 92(*---------------------------------------------------------------------------*) 93 94fun name_ss s (SSFRAG_CON {convs,rewrs,filter,ac,dprocs,congs,relsimps,...}) = 95 SSFRAG_CON {name=SOME s, convs=convs,rewrs=rewrs,filter=filter, 96 ac=ac,dprocs=dprocs,congs=congs, relsimps = relsimps}; 97 98fun rewrites rewrs = 99 SSFRAG_CON {name=NONE, relsimps = [], 100 convs=[],rewrs=rewrs,filter=NONE,ac=[],dprocs=[],congs=[]}; 101 102fun dproc_ss dproc = 103 SSFRAG_CON {name=NONE, relsimps = [], 104 convs=[],rewrs=[],filter=NONE,ac=[],dprocs=[dproc],congs=[]}; 105 106fun ac_ss aclist = 107 SSFRAG_CON {name=NONE, relsimps = [], 108 convs=[],rewrs=[],filter=NONE,ac=aclist,dprocs=[],congs=[]}; 109 110fun conv_ss conv = 111 SSFRAG_CON {name=NONE, relsimps = [], 112 convs=[conv],rewrs=[],filter=NONE,ac=[],dprocs=[],congs=[]}; 113 114fun relsimp_ss rsdata = 115 SSFRAG_CON {name = NONE, relsimps = [rsdata], 116 convs=[],rewrs=[],filter=NONE,ac=[],dprocs=[],congs=[]}; 117 118fun D (SSFRAG_CON s) = s; 119fun frag_rewrites ssf = #rewrs (D ssf) 120 121 122fun merge_names list = 123 itlist (fn (SOME x) => 124 (fn NONE => SOME x 125 | SOME y => SOME (x^", "^y)) 126 | NONE => 127 (fn NONE => NONE 128 | SOME y => SOME y)) 129 list NONE; 130 131(*---------------------------------------------------------------------------*) 132(* Possibly need to suppress duplicates in the merge? *) 133(*---------------------------------------------------------------------------*) 134 135fun merge_ss (s:ssfrag list) = 136 SSFRAG_CON 137 { name = merge_names (map (#name o D) s), 138 convs = flatten (map (#convs o D) s), 139 rewrs = flatten (map (#rewrs o D) s), 140 filter = SOME (end_foldr (op oo) (mapfilter (the o #filter o D) s)) 141 handle HOL_ERR _ => NONE, 142 ac = flatten (map (#ac o D) s), 143 dprocs = flatten (map (#dprocs o D) s), 144 congs = flatten (map (#congs o D) s), 145 relsimps = flatten (map (#relsimps o D) s) 146 } 147 148fun named_rewrites name = (name_ss name) o rewrites; 149fun named_merge_ss name = (name_ss name) o merge_ss; 150 151fun std_conv_ss {name,conv,pats} = 152 let 153 fun cnv k = conv_ss {conv = K (K conv), trace = 2, name = name, key = k} 154 in 155 if null pats then 156 cnv NONE 157 else 158 merge_ss (map (fn p => cnv (SOME([],p))) pats) 159 end 160 161fun ssfrag_name (SSFRAG_CON s) = Option.valOf (#name s); 162 163fun partition_ssfrags names ssdata = 164 List.partition 165 (fn SSFRAG_CON s => 166 case #name s 167 of SOME name => Lib.mem name names 168 | NONE => false) ssdata 169 170(*---------------------------------------------------------------------------*) 171(* Simpsets and basic operations on them. Simpsets contain enough *) 172(* information to spark off term traversal quickly and efficiently. In *) 173(* theory the net need not be stored (and the code would look neater if it *) 174(* wasn't), but in practice it has to be. *) 175(* --------------------------------------------------------------------------*) 176 177type net = ((term list -> term -> thm) -> term list -> conv) Ho_Net.net; 178 179datatype simpset = 180 SS of {mk_rewrs : (controlled_thm -> controlled_thm list), 181 ssfrags : ssfrag list, 182 initial_net : net, 183 dprocs : reducer list, 184 travrules : travrules, 185 limit : int option} 186 187 val empty_ss = SS {mk_rewrs=fn x => [x], 188 ssfrags = [], limit = NONE, 189 initial_net=empty, 190 dprocs=[],travrules=EQ_tr}; 191 192 fun ssfrags_of (SS x) = #ssfrags x; 193 194 (* --------------------------------------------------------------------- 195 * USER_CONV wraps a bit of tracing around a user conversion. 196 * 197 * net_add_convs (internal function) adds conversions to the 198 * initial context net. 199 * ---------------------------------------------------------------------*) 200 201 fun USER_CONV {name,key,trace=trace_level,conv} = 202 let val trace_string1 = "trying "^name^" on" 203 val trace_string2 = name^" ineffectual" 204 val trace_string3 = name^" left term unchanged" 205 val trace_string4 = name^" raised an unusual exception (ignored)" 206 in fn solver => fn stack => fn tm => 207 let val _ = trace(trace_level+2,REDUCE(trace_string1,tm)) 208 val thm = conv solver stack tm 209 in 210 trace(trace_level,PRODUCE(tm,name,thm)); 211 thm 212 end 213 handle e as HOL_ERR _ => 214 (trace (trace_level+2,TEXT trace_string2); raise e) 215 | e as Conv.UNCHANGED => 216 (trace (trace_level+2,TEXT trace_string3); raise e) 217 | e => (trace (trace_level, TEXT trace_string4); raise e) 218 end; 219 220 val any = mk_var("x",Type.alpha); 221 222 fun net_add_conv (data as {name,key,trace,conv}:convdata) = 223 enter (option_cases #1 [] key, 224 option_cases #2 any key, 225 USER_CONV data); 226 227(* itlist is like foldr, so that theorems get added to the context starting 228 from the end of the list *) 229 fun net_add_convs net convs = itlist net_add_conv convs net; 230 231 232 fun mk_ac p A = 233 let val (a,b,c) = Drule.MK_AC_LCOMM p 234 in (a, UNBOUNDED)::(b, UNBOUNDED)::(c,UNBOUNDED)::A 235 end handle HOL_ERR _ => A; 236 237 fun ac_rewrites aclist = Lib.itlist mk_ac aclist []; 238 239 fun same_frag (SSFRAG_CON{name=SOME n1, ...}) 240 (SSFRAG_CON{name=SOME n2, ...}) = n1=n2 241 | same_frag other wise = false; 242 243 fun ssfrag_names_of ss = 244 ss |> ssfrags_of 245 |> Lib.mapfilter ssfrag_name 246 |> Lib.mk_set 247 248 fun limit n (SS {mk_rewrs,ssfrags,travrules,initial_net,dprocs,limit}) = 249 SS {mk_rewrs = mk_rewrs, ssfrags = ssfrags, travrules = travrules, 250 initial_net = initial_net, dprocs = dprocs, limit = SOME n} 251 252 fun unlimit (SS {mk_rewrs,ssfrags,travrules,initial_net,dprocs,limit}) = 253 SS {mk_rewrs = mk_rewrs, ssfrags = ssfrags, travrules = travrules, 254 initial_net = initial_net, dprocs = dprocs, limit = NONE} 255 256 fun wk_mk_travrules (rels, congs) = let 257 fun cong2proc th = let 258 open Opening Travrules 259 fun mk_refl (x as {Rinst=rel,arg= t}) = let 260 val PREORDER(_,_,refl) = find_relation rel rels 261 in 262 refl x 263 end 264 in 265 CONGPROC mk_refl th 266 end 267 in 268 TRAVRULES {relations = rels, 269 congprocs = [], 270 weakenprocs = map cong2proc congs} 271 end 272 273 fun add_weakener (rels,congs,dp) simpset = let 274 val SS {mk_rewrs,ssfrags,travrules,initial_net,dprocs,limit} = simpset 275 in 276 SS {mk_rewrs = mk_rewrs, ssfrags = ssfrags, 277 travrules = merge_travrules [travrules, wk_mk_travrules(rels,congs)], 278 initial_net = initial_net, dprocs = dprocs @ [dp], limit = limit} 279 end 280 281(* ---------------------------------------------------------------------- 282 add_relsimp : {trans,refl,weakenings,subsets} -> simpset -> simpset 283 284 trans and refl are the transitivity and reflexivity theorems for the 285 relation. weakenings are theorems for turning (at least) equality goals 286 into goals over the new relation. subsets are theorems that help the 287 munger: they say that certain forms imply rules for the relation. For 288 example, if using RTC R as the relation, then RTC_R, which states 289 !x y. R x y ==> RTC R x y 290 is a good subset theorem 291 ---------------------------------------------------------------------- *) 292 293 fun dest_binop t = let 294 val (fx,y) = dest_comb t 295 val (f,x) = dest_comb fx 296 in 297 (f,x,y) 298 end 299 300 fun vperm(tm1,tm2) = 301 case (dest_term tm1, dest_term tm2) of 302 (VAR v1,VAR v2) => (snd v1 = snd v2) 303 | (LAMB t1,LAMB t2) => vperm(snd t1, snd t2) 304 | (COMB t1,COMB t2) => vperm(fst t1,fst t2) andalso vperm(snd t1,snd t2) 305 | (x,y) => (x = y) 306 307 fun is_var_perm(tm1,tm2) = 308 vperm(tm1,tm2) andalso set_eq (free_vars tm1) (free_vars tm2) 309 310 datatype munge_action = TH of thm | POP 311 312 fun munge base subsets asms (thlistlist, n) = let 313 val munge = munge base subsets 314 val isbase = can (match_term base) 315 in 316 case thlistlist of 317 [] => n 318 | [] :: rest => munge asms (rest, n) 319 | (TH th :: ths) :: rest => let 320 in 321 case CONJUNCTS (SPEC_ALL th) of 322 [] => raise Fail "munge: Can't happen" 323 | [th] => let 324 open Net 325 in 326 if is_imp (concl th) then 327 munge (#1 (dest_imp (concl th)) :: asms) 328 ((TH (UNDISCH th)::POP::ths)::rest, n) 329 else 330 case total dest_binop (concl th) of 331 SOME (R,from,to) => let 332 fun foldthis (t,th) = DISCH t th 333 fun insert (t,th0) n = let 334 val (th,bound) = dest_tagged_rewrite th0 335 val looksloopy = aconv from to orelse 336 (is_var_perm (from,to) andalso 337 case bound of UNBOUNDED => true 338 | _ => false) 339 in 340 if looksloopy then n 341 else 342 Net.insert (t, (bound, List.foldl foldthis th asms)) n 343 end 344 345 in 346 if isbase R then 347 munge asms (ths :: rest, insert (mk_comb(R,from),th) n) 348 else 349 case List.find (fn (t,_) => aconv R t) subsets of 350 NONE => munge asms (ths :: rest, n) 351 | SOME (_, sub_th) => let 352 val new_th = MATCH_MP sub_th th 353 in 354 munge asms ((TH new_th :: ths) :: rest, n) 355 end 356 end 357 | NONE => munge asms (ths :: rest, n) 358 end 359 | thlist => munge asms (map TH thlist :: ths :: rest, n) 360 end 361 | (POP :: ths) :: rest => munge (tl asms) (ths::rest, n) 362 end 363 364 fun po_rel (Travrules.PREORDER(r,_,_)) = r 365 366 fun mk_reducer rel_t subsets initial_rewrites = let 367 exception redExn of (control * thm) Net.net 368 fun munge_subset_th th = let 369 val (_, impn) = strip_forall (concl th) 370 val (a, _) = dest_imp impn 371 val (f, _, _) = dest_binop a 372 in 373 (f, th) 374 end 375 val subsets = map munge_subset_th subsets 376 fun addcontext (ctxt, thms) = let 377 val n = case ctxt of redExn n => n 378 | _ => raise ERR ("mk_reducer.addcontext", 379 "Wrong sort of ctxt") 380 val n' = munge rel_t subsets [] ([map TH thms], n) 381 in 382 redExn n' 383 end 384 val initial_ctxt = addcontext (redExn Net.empty, initial_rewrites) 385 fun applythm solver t (bound, th) = let 386 val _ = 387 trace(7, LZ_TEXT (fn () => "Attempting rewrite: "^thm_to_string th)) 388 fun dec() = case bound of 389 BOUNDED r => 390 let val n = !r in 391 if n > 0 then r := n - 1 392 else raise ERR ("mk_reducer.applythm", 393 "Bound exceeded on rwt.") 394 end 395 | UNBOUNDED => () 396 val matched = PART_MATCH (rator o #2 o strip_imp) th t 397 open Trace 398 fun do_sideconds th = 399 if is_imp (concl th) then let 400 val (h,c) = dest_imp (concl th) 401 val _ = trace(3,SIDECOND_ATTEMPT h) 402 val scond = solver h 403 val _ = trace(2,SIDECOND_SOLVED scond) 404 in 405 do_sideconds (MP th scond) 406 end 407 else (dec(); trace(2,REWRITING(t,th)); th) 408 in 409 do_sideconds matched 410 end 411 412 fun mk_icomb(f, x) = let 413 val (f_domty, _) = dom_rng (type_of f) 414 val xty = type_of x 415 val theta = match_type f_domty xty 416 in 417 mk_comb(Term.inst theta f, x) 418 end 419 420 fun apply {solver,conv,context,stack,relation = (relation,_)} t = let 421 val _ = can (match_term rel_t) relation orelse 422 raise ERR ("mk_reducer.apply", "Wrong relation") 423 val n = case context of redExn n => n 424 | _ => raise ERR ("apply", "Wrong sort of ctxt") 425 val lookup_t = mk_icomb(relation,t) 426 val _ = trace(7, LZ_TEXT(fn () => "Looking up "^term_to_string lookup_t)) 427 val matches = Net.match lookup_t n 428 val _ = trace(7, LZ_TEXT(fn () => "Found "^Int.toString (length matches)^ 429 " matches")) 430 in 431 tryfind (applythm (solver stack) lookup_t) matches 432 end 433 in 434 Traverse.REDUCER {name = SOME ("reducer for "^term_to_string rel_t), 435 addcontext = addcontext, 436 apply = apply, 437 initial = initial_ctxt} 438 end 439 440 val equality_po = let 441 open Travrules 442 val TRAVRULES {relations,...} = EQ_tr 443 in 444 hd relations 445 end 446 447 fun rsd_rel {refl,trans,weakenings,subsets,rewrs} = 448 #1 (dest_binop (#2 (strip_forall (concl refl)))) 449 fun rsd_po {refl,trans,weakenings,subsets,rewrs} = 450 Travrules.mk_preorder(trans,refl) 451 452 fun rsd_travrules (rsd as {refl,trans,weakenings,subsets,rewrs}) = 453 wk_mk_travrules([rsd_po rsd, equality_po], weakenings) 454 455 fun rsd_reducer rsd = 456 mk_reducer (rsd_rel rsd) (#subsets rsd) (#rewrs rsd) 457 458 459 fun add_relsimp (rsd as {refl,trans,weakenings,subsets,rewrs}) ss = let 460 val rel_t = rsd_rel rsd 461 val rel_po = rsd_po rsd 462 val reducer = mk_reducer rel_t subsets rewrs 463 in 464 add_weakener ([rel_po, equality_po], weakenings, reducer) ss 465 end 466 467 fun op++(SS sset, f as SSFRAG_CON ssf) = let 468 val {mk_rewrs=mk_rewrs',ssfrags,travrules,initial_net,dprocs=dprocs',limit}= 469 sset 470 val {convs,rewrs,filter,ac,dprocs,congs,relsimps,...} = ssf 471 val mk_rewrs = case filter of 472 SOME f => f oo mk_rewrs' 473 | _ => mk_rewrs' 474 val crewrs = map dest_tagged_rewrite rewrs 475 val rewrs' = flatten (map mk_rewrs (ac_rewrites ac@crewrs)) 476 val newconvdata = convs @ List.mapPartial mk_rewr_convdata rewrs' 477 val net = net_add_convs initial_net newconvdata 478 fun travrel (TRAVRULES{relations,...}) = relations 479 val sset_rels = travrel travrules 480 (* give the existing dprocs the rewrs as additional context - 481 assume the provided dprocs in the frag have already been 482 primed *) 483 val relreducers = map rsd_reducer relsimps 484 val new_dprocs = map (Traverse.addctxt rewrs) dprocs' @ dprocs @ relreducers 485 486 val reltravs = map rsd_travrules relsimps 487 val relrels = List.concat (map travrel reltravs) 488 val relations = sset_rels @ relrels 489 in 490 SS { 491 mk_rewrs = mk_rewrs, 492 ssfrags = f :: ssfrags, 493 initial_net = net, 494 limit = limit, 495 dprocs = new_dprocs, 496 travrules = merge_travrules 497 (travrules::mk_travrules relations congs::reltravs) 498 } 499 end 500 501val mk_simpset = foldl (fn (f,ss) => ss ++ f) empty_ss 502 503fun remove_ssfrags ss names = 504 ss |> ssfrags_of 505 |> partition_ssfrags names 506 |> snd |> List.rev 507 |> mk_simpset 508 509local 510 val lhs_of_thm = boolSyntax.lhs o snd o boolSyntax.strip_forall o Thm.concl 511 fun term_of_thm th = 512 case (Lib.total lhs_of_thm th, Thm.hyp th) of 513 (SOME tm, []) => tm 514 | _ => boolSyntax.T 515 fun match_eq tm1 tm2 = 516 Lib.can (Term.match_term tm1) tm2 andalso Lib.can (Term.match_term tm2) tm1 517 fun exists_match l thm = List.exists (match_eq (term_of_thm thm)) l 518 fun remove_theorems_from_frag f 519 (SSFRAG_CON { name, convs, rewrs, ac, filter, dprocs, congs, relsimps}) = 520 SSFRAG_CON 521 { name = name, 522 convs = convs, 523 rewrs = List.mapPartial (f false) rewrs, 524 ac = let val ok = Option.isSome o (f true) in 525 List.filter (fn (th1, th2) => ok th1 andalso ok th2) ac 526 end, 527 filter = filter, 528 dprocs = dprocs, 529 congs = congs, 530 relsimps = relsimps 531 } 532in 533 fun remove_theorems avoids (SS {mk_rewrs, ssfrags, ...}) = 534 let 535 fun thm_to_thms thm = 536 List.map fst (mk_rewrs (thm, BoundedRewrites.BOUNDED (ref 1))) 537 val part = List.partition (exists_match avoids) 538 fun f ac thm = 539 let 540 val (l, r) = part (if ac then [thm] else thm_to_thms thm) 541 in 542 if List.null l then SOME thm else Lib.total Drule.LIST_CONJ r 543 end 544 in 545 mk_simpset (List.rev (List.map (remove_theorems_from_frag f) ssfrags)) 546 end 547end 548 549(*---------------------------------------------------------------------------*) 550(* SIMP_QCONV : simpset -> thm list -> conv *) 551(*---------------------------------------------------------------------------*) 552 553 exception CONVNET of net; 554 555 fun rewriter_for_ss (SS{mk_rewrs,travrules,initial_net,...}) = let 556 fun addcontext (context,thms) = let 557 val net = (raise context) handle CONVNET net => net 558 val cthms = map dest_tagged_rewrite thms 559 val new_rwts = flatten (map mk_rewrs cthms) 560 in 561 CONVNET (net_add_convs net (List.mapPartial mk_rewr_convdata new_rwts)) 562 end 563 fun apply {solver,conv,context,stack,relation} tm = let 564 val net = (raise context) handle CONVNET net => net 565 in 566 tryfind (fn conv' => conv' solver stack tm) (lookup tm net) 567 end 568 in REDUCER {name=SOME"rewriter_for_ss", 569 addcontext=addcontext, apply=apply, 570 initial=CONVNET initial_net} 571 end; 572 573 fun traversedata_for_ss (ss as (SS ssdata)) = 574 {rewriters=[rewriter_for_ss ss], 575 dprocs= #dprocs ssdata, 576 relation= boolSyntax.equality, 577 travrules= #travrules ssdata, 578 limit = #limit ssdata}; 579 580 fun SIMP_QCONV ss = TRAVERSE (traversedata_for_ss ss); 581 582val Cong = markerLib.Cong 583val AC = markerLib.AC; 584 585local open markerSyntax markerLib 586 fun is_AC thm = same_const(fst(strip_comb(concl thm))) AC_tm 587 fun is_Cong thm = same_const(fst(strip_comb(concl thm))) Cong_tm 588 589 fun process_tags ss thl = 590 let val (Congs,rst) = Lib.partition is_Cong thl 591 val (ACs,rst') = Lib.partition is_AC rst 592 in 593 if null Congs andalso null ACs then (ss,thl) 594 else ((ss ++ SSFRAG_CON{name=SOME"Cong and/or AC", relsimps = [], 595 ac=map unAC ACs, congs=map unCong Congs, 596 convs=[],rewrs=[],filter=NONE,dprocs=[]}), rst') 597 end 598in 599fun SIMP_CONV ss l tm = 600 let val (ss', l') = process_tags ss l 601 in TRY_CONV (SIMP_QCONV ss' l') tm 602 end; 603 604fun SIMP_PROVE ss l t = 605 let val (ss', l') = process_tags ss l 606 in EQT_ELIM (SIMP_QCONV ss' l' t) 607 end; 608 609infix &&; 610 611fun (ss && thl) = 612 let val (ss',thl') = process_tags ss thl 613 in ss' ++ rewrites thl' 614 end; 615 616end; 617 618(*---------------------------------------------------------------------------*) 619(* SIMP_TAC : simpset -> thm list -> tactic *) 620(* ASM_SIMP_TAC : simpset -> thm list -> tactic *) 621(* FULL_SIMP_TAC : simpset -> thm list -> tactic *) 622(* *) 623(* FAILURE CONDITIONS *) 624(* *) 625(* These tactics never fail, though they may diverge. *) 626(* --------------------------------------------------------------------------*) 627 628 629fun SIMP_RULE ss l = CONV_RULE (SIMP_CONV ss l) 630 631fun ASM_SIMP_RULE ss l th = SIMP_RULE ss (l@map ASSUME (hyp th)) th; 632 633fun SIMP_TAC ss l = markerLib.ABBRS_THEN (CONV_TAC o SIMP_CONV ss) l; 634val simp_tac = SIMP_TAC 635 636fun ASM_SIMP_TAC ss = 637 markerLib.ABBRS_THEN 638 (fn thl => fn gl as (asl,_) => 639 SIMP_TAC ss (markerLib.LLABEL_RESOLVE thl asl) gl); 640val asm_simp_tac = ASM_SIMP_TAC 641 642local 643 (* differs only in that it doesn't call OPPOSITE_TAC or DISCARD_TAC *) 644 fun caa_tac th = FIRST [CONTR_TAC th, ACCEPT_TAC th, ASSUME_TAC th] 645 val STRIP_ASSUME_TAC' = REPEAT_TCL STRIP_THM_THEN caa_tac 646 fun drop r = 647 fn n => 648 POP_ASSUM_LIST 649 (fn l => 650 MAP_EVERY ASSUME_TAC 651 (Lib.with_exn (r o List.take) (l, List.length l - n) 652 (Feedback.mk_HOL_ERR "simpLib" "drop" "Bad cut off number"))) 653 fun GEN_FULL_SIMP_TAC (drop, r) tac = 654 fn ss => fn thms => 655 let 656 fun simp_asm (t, l') = SIMP_RULE ss (l' @ thms) t :: l' 657 fun f asms = MAP_EVERY tac (List.foldl simp_asm [] (r asms)) 658 THEN drop (List.length asms) 659 in 660 markerLib.ABBRS_THEN 661 (fn l => ASSUM_LIST f THEN ASM_SIMP_TAC ss l) thms 662 end 663 val full_tac = GEN_FULL_SIMP_TAC (drop List.rev, Lib.I) 664 val rev_full_tac = GEN_FULL_SIMP_TAC (drop Lib.I, List.rev) 665in 666 val FULL_SIMP_TAC = full_tac STRIP_ASSUME_TAC' 667 val full_simp_tac = FULL_SIMP_TAC 668 val REV_FULL_SIMP_TAC = rev_full_tac STRIP_ASSUME_TAC' 669 val rev_full_simp_tac = REV_FULL_SIMP_TAC 670 val NO_STRIP_FULL_SIMP_TAC = full_tac caa_tac 671 val NO_STRIP_REV_FULL_SIMP_TAC = rev_full_tac caa_tac 672end 673 674fun track f x = 675 let val _ = (used_rewrites := []) 676 val res = Lib.with_flag(track_rewrites,true) f x 677 in used_rewrites := rev (!used_rewrites) 678 ; res 679 end; 680 681(* ---------------------------------------------------------------------- 682 creating per-type ssdata values 683 ---------------------------------------------------------------------- *) 684 685fun type_ssfrag ty = let 686 val {Thy,Tyop,...} = dest_thy_type ty 687 val tyname = Thy^"$"^Tyop 688 val {rewrs, convs} = TypeBase.simpls_of ty 689in 690 SSFRAG_CON {name=SOME ("Datatype "^tyname), relsimps = [], 691 convs = convs, rewrs = rewrs, filter = NONE, 692 dprocs = [], ac = [], congs = []} 693end 694 695 696(*---------------------------------------------------------------------------*) 697(* Pretty printers for ssfrags and simpsets *) 698(*---------------------------------------------------------------------------*) 699 700val CONSISTENT = Portable.CONSISTENT 701val INCONSISTENT = Portable.INCONSISTENT; 702 703fun dest_reducer (Traverse.REDUCER x) = x; 704 705fun merge_names list = 706 itlist (fn (SOME x) => 707 (fn NONE => SOME x 708 | SOME y => SOME (x^", "^y)) 709 | NONE => 710 (fn NONE => NONE 711 | SOME y => SOME y)) 712 list NONE; 713 714fun dest_convdata {name,key as SOME(_,tm),trace,conv} = (name,SOME tm) 715 | dest_convdata {name,...} = (name,NONE); 716 717fun pp_ssfrag (SSFRAG_CON {name,convs,rewrs,ac,dprocs,congs,...}) = 718 let open Portable smpp 719 val name = (case name of SOME s => s | NONE => "<anonymous>") 720 val convs = map dest_convdata convs 721 val dps = case merge_names (map (#name o dest_reducer) dprocs) 722 of NONE => [] 723 | SOME n => [n] 724 val pp_term = lift (Parse.term_pp_with_delimiters Hol_pp.pp_term) 725 val pp_thm = lift pp_thm 726 fun pp_thm_pair (th1,th2) = 727 block CONSISTENT 0 (pp_thm th1 >> add_break(2,0) >> pp_thm th2) 728 fun pp_conv_info (n,SOME tm) = 729 block CONSISTENT 0 ( 730 add_string (n^", keyed on pattern") >> add_break(2,0) >> pp_term tm 731 ) 732 | pp_conv_info (n,NONE) = add_string n 733 val nl2 = add_newline >> add_newline 734 fun vspace l = if null l then nothing else nl2 735 fun vblock(header, ob_pr, obs) = 736 if null obs then nothing 737 else 738 block CONSISTENT 3 ( 739 add_string (header^":") >> 740 add_newline >> 741 pr_list ob_pr add_newline obs 742 ) >> add_break(1,0) 743 in 744 block CONSISTENT 0 ( 745 add_string ("Simplification set: "^name) >> add_newline >> 746 vblock("Conversions",pp_conv_info,convs) >> 747 vblock("Decision procedures",add_string,dps) >> 748 vblock("Congruence rules",pp_thm,congs) >> 749 vblock("AC rewrites",pp_thm_pair,ac) >> 750 vblock("Rewrite rules",pp_thm,rewrs) 751 ) 752 end 753 754fun pp_simpset ss = 755 let 756 open Portable smpp 757 in 758 Parse.mlower (pr_list pp_ssfrag add_newline (rev (ssfrags_of ss))) 759 end; 760 761val pp_ssfrag = Parse.mlower o pp_ssfrag 762 763end (* struct *) 764