1(* ========================================================================= *) 2(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Rule :> Rule = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* Variable names. *) 13(* ------------------------------------------------------------------------- *) 14 15val xVarName = Name.fromString "x"; 16val xVar = Term.Var xVarName; 17 18val yVarName = Name.fromString "y"; 19val yVar = Term.Var yVarName; 20 21val zVarName = Name.fromString "z"; 22val zVar = Term.Var zVarName; 23 24fun xIVarName i = Name.fromString ("x" ^ Int.toString i); 25fun xIVar i = Term.Var (xIVarName i); 26 27fun yIVarName i = Name.fromString ("y" ^ Int.toString i); 28fun yIVar i = Term.Var (yIVarName i); 29 30(* ------------------------------------------------------------------------- *) 31(* *) 32(* --------- reflexivity *) 33(* x = x *) 34(* ------------------------------------------------------------------------- *) 35 36fun reflexivityRule x = Thm.refl x; 37 38val reflexivity = reflexivityRule xVar; 39 40(* ------------------------------------------------------------------------- *) 41(* *) 42(* --------------------- symmetry *) 43(* ~(x = y) \/ y = x *) 44(* ------------------------------------------------------------------------- *) 45 46fun symmetryRule x y = 47 let 48 val reflTh = reflexivityRule x 49 val reflLit = Thm.destUnit reflTh 50 val eqTh = Thm.equality reflLit [0] y 51 in 52 Thm.resolve reflLit reflTh eqTh 53 end; 54 55val symmetry = symmetryRule xVar yVar; 56 57(* ------------------------------------------------------------------------- *) 58(* *) 59(* --------------------------------- transitivity *) 60(* ~(x = y) \/ ~(y = z) \/ x = z *) 61(* ------------------------------------------------------------------------- *) 62 63val transitivity = 64 let 65 val eqTh = Thm.equality (Literal.mkEq (yVar,zVar)) [0] xVar 66 in 67 Thm.resolve (Literal.mkEq (yVar,xVar)) symmetry eqTh 68 end; 69 70(* ------------------------------------------------------------------------- *) 71(* x = y \/ C *) 72(* -------------- symEq (x = y) *) 73(* y = x \/ C *) 74(* ------------------------------------------------------------------------- *) 75 76fun symEq lit th = 77 let 78 val (x,y) = Literal.destEq lit 79 in 80 if Term.equal x y then th 81 else 82 let 83 val sub = Subst.fromList [(xVarName,x),(yVarName,y)] 84 85 val symTh = Thm.subst sub symmetry 86 in 87 Thm.resolve lit th symTh 88 end 89 end; 90 91(* ------------------------------------------------------------------------- *) 92(* An equation consists of two terms (t,u) plus a theorem (stronger than) *) 93(* t = u \/ C. *) 94(* ------------------------------------------------------------------------- *) 95 96type equation = (Term.term * Term.term) * Thm.thm; 97 98fun ppEquation ((_,th) : equation) = Thm.pp th; 99 100val equationToString = Print.toString ppEquation; 101 102fun equationLiteral (t_u,th) = 103 let 104 val lit = Literal.mkEq t_u 105 in 106 if LiteralSet.member lit (Thm.clause th) then SOME lit else NONE 107 end; 108 109fun reflEqn t = ((t,t), Thm.refl t); 110 111fun symEqn (eqn as ((t,u), th)) = 112 if Term.equal t u then eqn 113 else 114 ((u,t), 115 case equationLiteral eqn of 116 SOME t_u => symEq t_u th 117 | NONE => th); 118 119fun transEqn (eqn1 as ((x,y), th1)) (eqn2 as ((_,z), th2)) = 120 if Term.equal x y then eqn2 121 else if Term.equal y z then eqn1 122 else if Term.equal x z then reflEqn x 123 else 124 ((x,z), 125 case equationLiteral eqn1 of 126 NONE => th1 127 | SOME x_y => 128 case equationLiteral eqn2 of 129 NONE => th2 130 | SOME y_z => 131 let 132 val sub = Subst.fromList [(xVarName,x),(yVarName,y),(zVarName,z)] 133 val th = Thm.subst sub transitivity 134 val th = Thm.resolve x_y th1 th 135 val th = Thm.resolve y_z th2 th 136 in 137 th 138 end); 139 140(*MetisDebug 141val transEqn = fn eqn1 => fn eqn2 => 142 transEqn eqn1 eqn2 143 handle Error err => 144 raise Error ("Rule.transEqn:\neqn1 = " ^ equationToString eqn1 ^ 145 "\neqn2 = " ^ equationToString eqn2 ^ "\n" ^ err); 146*) 147 148(* ------------------------------------------------------------------------- *) 149(* A conversion takes a term t and either: *) 150(* 1. Returns a term u together with a theorem (stronger than) t = u \/ C. *) 151(* 2. Raises an Error exception. *) 152(* ------------------------------------------------------------------------- *) 153 154type conv = Term.term -> Term.term * Thm.thm; 155 156fun allConv tm = (tm, Thm.refl tm); 157 158val noConv : conv = fn _ => raise Error "noConv"; 159 160(*MetisDebug 161fun traceConv s conv tm = 162 let 163 val res as (tm',th) = conv tm 164 val () = trace (s ^ ": " ^ Term.toString tm ^ " --> " ^ 165 Term.toString tm' ^ " " ^ Thm.toString th ^ "\n") 166 in 167 res 168 end 169 handle Error err => 170 (trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n"); 171 raise Error (s ^ ": " ^ err)); 172*) 173 174fun thenConvTrans tm (tm',th1) (tm'',th2) = 175 let 176 val eqn1 = ((tm,tm'),th1) 177 and eqn2 = ((tm',tm''),th2) 178 val (_,th) = transEqn eqn1 eqn2 179 in 180 (tm'',th) 181 end; 182 183fun thenConv conv1 conv2 tm = 184 let 185 val res1 as (tm',_) = conv1 tm 186 val res2 = conv2 tm' 187 in 188 thenConvTrans tm res1 res2 189 end; 190 191fun orelseConv (conv1 : conv) conv2 tm = conv1 tm handle Error _ => conv2 tm; 192 193fun tryConv conv = orelseConv conv allConv; 194 195fun changedConv conv tm = 196 let 197 val res as (tm',_) = conv tm 198 in 199 if tm = tm' then raise Error "changedConv" else res 200 end; 201 202fun repeatConv conv tm = tryConv (thenConv conv (repeatConv conv)) tm; 203 204fun firstConv [] _ = raise Error "firstConv" 205 | firstConv [conv] tm = conv tm 206 | firstConv (conv :: convs) tm = orelseConv conv (firstConv convs) tm; 207 208fun everyConv [] tm = allConv tm 209 | everyConv [conv] tm = conv tm 210 | everyConv (conv :: convs) tm = thenConv conv (everyConv convs) tm; 211 212fun rewrConv (eqn as ((x,y), eqTh)) path tm = 213 if Term.equal x y then allConv tm 214 else if List.null path then (y,eqTh) 215 else 216 let 217 val reflTh = Thm.refl tm 218 val reflLit = Thm.destUnit reflTh 219 val th = Thm.equality reflLit (1 :: path) y 220 val th = Thm.resolve reflLit reflTh th 221 val th = 222 case equationLiteral eqn of 223 NONE => th 224 | SOME x_y => Thm.resolve x_y eqTh th 225 val tm' = Term.replace tm (path,y) 226 in 227 (tm',th) 228 end; 229 230(*MetisDebug 231val rewrConv = fn eqn as ((x,y),eqTh) => fn path => fn tm => 232 rewrConv eqn path tm 233 handle Error err => 234 raise Error ("Rule.rewrConv:\nx = " ^ Term.toString x ^ 235 "\ny = " ^ Term.toString y ^ 236 "\neqTh = " ^ Thm.toString eqTh ^ 237 "\npath = " ^ Term.pathToString path ^ 238 "\ntm = " ^ Term.toString tm ^ "\n" ^ err); 239*) 240 241fun pathConv conv path tm = 242 let 243 val x = Term.subterm tm path 244 val (y,th) = conv x 245 in 246 rewrConv ((x,y),th) path tm 247 end; 248 249fun subtermConv conv i = pathConv conv [i]; 250 251fun subtermsConv _ (tm as Term.Var _) = allConv tm 252 | subtermsConv conv (tm as Term.Fn (_,a)) = 253 everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm; 254 255(* ------------------------------------------------------------------------- *) 256(* Applying a conversion to every subterm, with some traversal strategy. *) 257(* ------------------------------------------------------------------------- *) 258 259fun bottomUpConv conv tm = 260 thenConv (subtermsConv (bottomUpConv conv)) (repeatConv conv) tm; 261 262fun topDownConv conv tm = 263 thenConv (repeatConv conv) (subtermsConv (topDownConv conv)) tm; 264 265fun repeatTopDownConv conv = 266 let 267 fun f tm = thenConv (repeatConv conv) g tm 268 and g tm = thenConv (subtermsConv f) h tm 269 and h tm = tryConv (thenConv conv f) tm 270 in 271 f 272 end; 273 274(*MetisDebug 275val repeatTopDownConv = fn conv => fn tm => 276 repeatTopDownConv conv tm 277 handle Error err => raise Error ("repeatTopDownConv: " ^ err); 278*) 279 280(* ------------------------------------------------------------------------- *) 281(* A literule (bad pun) takes a literal L and either: *) 282(* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C. *) 283(* 2. Raises an Error exception. *) 284(* ------------------------------------------------------------------------- *) 285 286type literule = Literal.literal -> Literal.literal * Thm.thm; 287 288fun allLiterule lit = (lit, Thm.assume lit); 289 290val noLiterule : literule = fn _ => raise Error "noLiterule"; 291 292fun thenLiterule literule1 literule2 lit = 293 let 294 val res1 as (lit',th1) = literule1 lit 295 val res2 as (lit'',th2) = literule2 lit' 296 in 297 if Literal.equal lit lit' then res2 298 else if Literal.equal lit' lit'' then res1 299 else if Literal.equal lit lit'' then allLiterule lit 300 else 301 (lit'', 302 if not (Thm.member lit' th1) then th1 303 else if not (Thm.negateMember lit' th2) then th2 304 else Thm.resolve lit' th1 th2) 305 end; 306 307fun orelseLiterule (literule1 : literule) literule2 lit = 308 literule1 lit handle Error _ => literule2 lit; 309 310fun tryLiterule literule = orelseLiterule literule allLiterule; 311 312fun changedLiterule literule lit = 313 let 314 val res as (lit',_) = literule lit 315 in 316 if lit = lit' then raise Error "changedLiterule" else res 317 end; 318 319fun repeatLiterule literule lit = 320 tryLiterule (thenLiterule literule (repeatLiterule literule)) lit; 321 322fun firstLiterule [] _ = raise Error "firstLiterule" 323 | firstLiterule [literule] lit = literule lit 324 | firstLiterule (literule :: literules) lit = 325 orelseLiterule literule (firstLiterule literules) lit; 326 327fun everyLiterule [] lit = allLiterule lit 328 | everyLiterule [literule] lit = literule lit 329 | everyLiterule (literule :: literules) lit = 330 thenLiterule literule (everyLiterule literules) lit; 331 332fun rewrLiterule (eqn as ((x,y),eqTh)) path lit = 333 if Term.equal x y then allLiterule lit 334 else 335 let 336 val th = Thm.equality lit path y 337 val th = 338 case equationLiteral eqn of 339 NONE => th 340 | SOME x_y => Thm.resolve x_y eqTh th 341 val lit' = Literal.replace lit (path,y) 342 in 343 (lit',th) 344 end; 345 346(*MetisDebug 347val rewrLiterule = fn eqn => fn path => fn lit => 348 rewrLiterule eqn path lit 349 handle Error err => 350 raise Error ("Rule.rewrLiterule:\neqn = " ^ equationToString eqn ^ 351 "\npath = " ^ Term.pathToString path ^ 352 "\nlit = " ^ Literal.toString lit ^ "\n" ^ err); 353*) 354 355fun pathLiterule conv path lit = 356 let 357 val tm = Literal.subterm lit path 358 val (tm',th) = conv tm 359 in 360 rewrLiterule ((tm,tm'),th) path lit 361 end; 362 363fun argumentLiterule conv i = pathLiterule conv [i]; 364 365fun allArgumentsLiterule conv lit = 366 everyLiterule 367 (List.map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit; 368 369(* ------------------------------------------------------------------------- *) 370(* A rule takes one theorem and either deduces another or raises an Error *) 371(* exception. *) 372(* ------------------------------------------------------------------------- *) 373 374type rule = Thm.thm -> Thm.thm; 375 376val allRule : rule = fn th => th; 377 378val noRule : rule = fn _ => raise Error "noRule"; 379 380fun thenRule (rule1 : rule) (rule2 : rule) th = rule1 (rule2 th); 381 382fun orelseRule (rule1 : rule) rule2 th = rule1 th handle Error _ => rule2 th; 383 384fun tryRule rule = orelseRule rule allRule; 385 386fun changedRule rule th = 387 let 388 val th' = rule th 389 in 390 if not (LiteralSet.equal (Thm.clause th) (Thm.clause th')) then th' 391 else raise Error "changedRule" 392 end; 393 394fun repeatRule rule lit = tryRule (thenRule rule (repeatRule rule)) lit; 395 396fun firstRule [] _ = raise Error "firstRule" 397 | firstRule [rule] th = rule th 398 | firstRule (rule :: rules) th = orelseRule rule (firstRule rules) th; 399 400fun everyRule [] th = allRule th 401 | everyRule [rule] th = rule th 402 | everyRule (rule :: rules) th = thenRule rule (everyRule rules) th; 403 404fun literalRule literule lit th = 405 let 406 val (lit',litTh) = literule lit 407 in 408 if Literal.equal lit lit' then th 409 else if not (Thm.negateMember lit litTh) then litTh 410 else Thm.resolve lit th litTh 411 end; 412 413(*MetisDebug 414val literalRule = fn literule => fn lit => fn th => 415 literalRule literule lit th 416 handle Error err => 417 raise Error ("Rule.literalRule:\nlit = " ^ Literal.toString lit ^ 418 "\nth = " ^ Thm.toString th ^ "\n" ^ err); 419*) 420 421fun rewrRule eqTh lit path = literalRule (rewrLiterule eqTh path) lit; 422 423fun pathRule conv lit path = literalRule (pathLiterule conv path) lit; 424 425fun literalsRule literule = 426 let 427 fun f (lit,th) = 428 if Thm.member lit th then literalRule literule lit th else th 429 in 430 fn lits => fn th => LiteralSet.foldl f th lits 431 end; 432 433fun allLiteralsRule literule th = literalsRule literule (Thm.clause th) th; 434 435fun convRule conv = allLiteralsRule (allArgumentsLiterule conv); 436 437(* ------------------------------------------------------------------------- *) 438(* *) 439(* ---------------------------------------------- functionCongruence (f,n) *) 440(* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) 441(* f x0 ... x{n-1} = f y0 ... y{n-1} *) 442(* ------------------------------------------------------------------------- *) 443 444fun functionCongruence (f,n) = 445 let 446 val xs = List.tabulate (n,xIVar) 447 and ys = List.tabulate (n,yIVar) 448 449 fun cong ((i,yi),(th,lit)) = 450 let 451 val path = [1,i] 452 val th = Thm.resolve lit th (Thm.equality lit path yi) 453 val lit = Literal.replace lit (path,yi) 454 in 455 (th,lit) 456 end 457 458 val reflTh = Thm.refl (Term.Fn (f,xs)) 459 val reflLit = Thm.destUnit reflTh 460 in 461 fst (List.foldl cong (reflTh,reflLit) (enumerate ys)) 462 end; 463 464(* ------------------------------------------------------------------------- *) 465(* *) 466(* ---------------------------------------------- relationCongruence (R,n) *) 467(* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) 468(* ~R x0 ... x{n-1} \/ R y0 ... y{n-1} *) 469(* ------------------------------------------------------------------------- *) 470 471fun relationCongruence (R,n) = 472 let 473 val xs = List.tabulate (n,xIVar) 474 and ys = List.tabulate (n,yIVar) 475 476 fun cong ((i,yi),(th,lit)) = 477 let 478 val path = [i] 479 val th = Thm.resolve lit th (Thm.equality lit path yi) 480 val lit = Literal.replace lit (path,yi) 481 in 482 (th,lit) 483 end 484 485 val assumeLit = (false,(R,xs)) 486 val assumeTh = Thm.assume assumeLit 487 in 488 fst (List.foldl cong (assumeTh,assumeLit) (enumerate ys)) 489 end; 490 491(* ------------------------------------------------------------------------- *) 492(* ~(x = y) \/ C *) 493(* ----------------- symNeq ~(x = y) *) 494(* ~(y = x) \/ C *) 495(* ------------------------------------------------------------------------- *) 496 497fun symNeq lit th = 498 let 499 val (x,y) = Literal.destNeq lit 500 in 501 if Term.equal x y then th 502 else 503 let 504 val sub = Subst.fromList [(xVarName,y),(yVarName,x)] 505 val symTh = Thm.subst sub symmetry 506 in 507 Thm.resolve lit th symTh 508 end 509 end; 510 511(* ------------------------------------------------------------------------- *) 512(* sym (x = y) = symEq (x = y) /\ sym ~(x = y) = symNeq ~(x = y) *) 513(* ------------------------------------------------------------------------- *) 514 515fun sym (lit as (pol,_)) th = if pol then symEq lit th else symNeq lit th; 516 517(* ------------------------------------------------------------------------- *) 518(* ~(x = x) \/ C *) 519(* ----------------- removeIrrefl *) 520(* C *) 521(* *) 522(* where all irreflexive equalities. *) 523(* ------------------------------------------------------------------------- *) 524 525local 526 fun irrefl ((true,_),th) = th 527 | irrefl (lit as (false,atm), th) = 528 case total Atom.destRefl atm of 529 SOME x => Thm.resolve lit th (Thm.refl x) 530 | NONE => th; 531in 532 fun removeIrrefl th = LiteralSet.foldl irrefl th (Thm.clause th); 533end; 534 535(* ------------------------------------------------------------------------- *) 536(* x = y \/ y = x \/ C *) 537(* ----------------------- removeSym *) 538(* x = y \/ C *) 539(* *) 540(* where all duplicate copies of equalities and disequalities are removed. *) 541(* ------------------------------------------------------------------------- *) 542 543local 544 fun rem (lit as (pol,atm), eqs_th as (eqs,th)) = 545 case total Atom.sym atm of 546 NONE => eqs_th 547 | SOME atm' => 548 if LiteralSet.member lit eqs then 549 (eqs, if pol then symEq lit th else symNeq lit th) 550 else 551 (LiteralSet.add eqs (pol,atm'), th); 552in 553 fun removeSym th = 554 snd (LiteralSet.foldl rem (LiteralSet.empty,th) (Thm.clause th)); 555end; 556 557(* ------------------------------------------------------------------------- *) 558(* ~(v = t) \/ C *) 559(* ----------------- expandAbbrevs *) 560(* C[t/v] *) 561(* *) 562(* where t must not contain any occurrence of the variable v. *) 563(* ------------------------------------------------------------------------- *) 564 565local 566 fun expand lit = 567 let 568 val (x,y) = Literal.destNeq lit 569 val _ = Term.isTypedVar x orelse Term.isTypedVar y orelse 570 raise Error "Rule.expandAbbrevs: no vars" 571 val _ = not (Term.equal x y) orelse 572 raise Error "Rule.expandAbbrevs: equal vars" 573 in 574 Subst.unify Subst.empty x y 575 end; 576in 577 fun expandAbbrevs th = 578 case LiteralSet.firstl (total expand) (Thm.clause th) of 579 NONE => removeIrrefl th 580 | SOME sub => expandAbbrevs (Thm.subst sub th); 581end; 582 583(* ------------------------------------------------------------------------- *) 584(* simplify = isTautology + expandAbbrevs + removeSym *) 585(* ------------------------------------------------------------------------- *) 586 587fun simplify th = 588 if Thm.isTautology th then NONE 589 else 590 let 591 val th' = th 592 val th' = expandAbbrevs th' 593 val th' = removeSym th' 594 in 595 if Thm.equal th th' then SOME th else simplify th' 596 end; 597 598(* ------------------------------------------------------------------------- *) 599(* C *) 600(* -------- freshVars *) 601(* C[s] *) 602(* *) 603(* where s is a renaming substitution chosen so that all of the variables in *) 604(* C are replaced by fresh variables. *) 605(* ------------------------------------------------------------------------- *) 606 607fun freshVars th = Thm.subst (Subst.freshVars (Thm.freeVars th)) th; 608 609(* ------------------------------------------------------------------------- *) 610(* C *) 611(* ---------------------------- factor *) 612(* C_s_1, C_s_2, ..., C_s_n *) 613(* *) 614(* where each s_i is a substitution that factors C, meaning that the theorem *) 615(* *) 616(* C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C *) 617(* *) 618(* has fewer literals than C. *) 619(* *) 620(* Also, if s is any substitution that factors C, then one of the s_i will *) 621(* result in a theorem C_s_i that strictly subsumes the theorem C_s. *) 622(* ------------------------------------------------------------------------- *) 623 624local 625 datatype edge = 626 FactorEdge of Atom.atom * Atom.atom 627 | ReflEdge of Term.term * Term.term; 628 629 fun ppEdge (FactorEdge atm_atm') = Print.ppPair Atom.pp Atom.pp atm_atm' 630 | ppEdge (ReflEdge tm_tm') = Print.ppPair Term.pp Term.pp tm_tm'; 631 632 datatype joinStatus = 633 Joined 634 | Joinable of Subst.subst 635 | Apart; 636 637 fun joinEdge sub edge = 638 let 639 val result = 640 case edge of 641 FactorEdge (atm,atm') => total (Atom.unify sub atm) atm' 642 | ReflEdge (tm,tm') => total (Subst.unify sub tm) tm' 643 in 644 case result of 645 NONE => Apart 646 | SOME sub' => 647 if Portable.pointerEqual (sub,sub') then Joined else Joinable sub' 648 end; 649 650 fun updateApart sub = 651 let 652 fun update acc [] = SOME acc 653 | update acc (edge :: edges) = 654 case joinEdge sub edge of 655 Joined => NONE 656 | Joinable _ => update (edge :: acc) edges 657 | Apart => update acc edges 658 in 659 update [] 660 end; 661 662 fun addFactorEdge (pol,atm) ((pol',atm'),acc) = 663 if pol <> pol' then acc 664 else 665 let 666 val edge = FactorEdge (atm,atm') 667 in 668 case joinEdge Subst.empty edge of 669 Joined => raise Bug "addFactorEdge: joined" 670 | Joinable sub => (sub,edge) :: acc 671 | Apart => acc 672 end; 673 674 fun addReflEdge (false,_) acc = acc 675 | addReflEdge (true,atm) acc = 676 let 677 val edge = ReflEdge (Atom.destEq atm) 678 in 679 case joinEdge Subst.empty edge of 680 Joined => raise Bug "addRefl: joined" 681 | Joinable _ => edge :: acc 682 | Apart => acc 683 end; 684 685 fun addIrreflEdge (true,_) acc = acc 686 | addIrreflEdge (false,atm) acc = 687 let 688 val edge = ReflEdge (Atom.destEq atm) 689 in 690 case joinEdge Subst.empty edge of 691 Joined => raise Bug "addRefl: joined" 692 | Joinable sub => (sub,edge) :: acc 693 | Apart => acc 694 end; 695 696 fun init_edges acc _ [] = 697 let 698 fun init ((apart,sub,edge),(edges,acc)) = 699 (edge :: edges, (apart,sub,edges) :: acc) 700 in 701 snd (List.foldl init ([],[]) acc) 702 end 703 | init_edges acc apart ((sub,edge) :: sub_edges) = 704 let 705(*MetisDebug 706 val () = if not (Subst.null sub) then () 707 else raise Bug "Rule.factor.init_edges: empty subst" 708*) 709 val (acc,apart) = 710 case updateApart sub apart of 711 SOME apart' => ((apart',sub,edge) :: acc, edge :: apart) 712 | NONE => (acc,apart) 713 in 714 init_edges acc apart sub_edges 715 end; 716 717 fun mk_edges apart sub_edges [] = init_edges [] apart sub_edges 718 | mk_edges apart sub_edges (lit :: lits) = 719 let 720 val sub_edges = List.foldl (addFactorEdge lit) sub_edges lits 721 722 val (apart,sub_edges) = 723 case total Literal.sym lit of 724 NONE => (apart,sub_edges) 725 | SOME lit' => 726 let 727 val apart = addReflEdge lit apart 728 val sub_edges = addIrreflEdge lit sub_edges 729 val sub_edges = List.foldl (addFactorEdge lit') sub_edges lits 730 in 731 (apart,sub_edges) 732 end 733 in 734 mk_edges apart sub_edges lits 735 end; 736 737 fun fact acc [] = acc 738 | fact acc ((_,sub,[]) :: others) = fact (sub :: acc) others 739 | fact acc ((apart, sub, edge :: edges) :: others) = 740 let 741 val others = 742 case joinEdge sub edge of 743 Joinable sub' => 744 let 745 val others = (edge :: apart, sub, edges) :: others 746 in 747 case updateApart sub' apart of 748 NONE => others 749 | SOME apart' => (apart',sub',edges) :: others 750 end 751 | _ => (apart,sub,edges) :: others 752 in 753 fact acc others 754 end; 755in 756 fun factor' cl = 757 let 758(*MetisTrace6 759 val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl 760*) 761 val edges = mk_edges [] [] (LiteralSet.toList cl) 762(*MetisTrace6 763 val ppEdgesSize = Print.ppMap length Print.ppInt 764 val ppEdgel = Print.ppList ppEdge 765 val ppEdges = Print.ppList (Print.ppTriple ppEdgel Subst.pp ppEdgel) 766 val () = Print.trace ppEdgesSize "Rule.factor': |edges|" edges 767 val () = Print.trace ppEdges "Rule.factor': edges" edges 768*) 769 val result = fact [] edges 770(*MetisTrace6 771 val ppResult = Print.ppList Subst.pp 772 val () = Print.trace ppResult "Rule.factor': result" result 773*) 774 in 775 result 776 end; 777end; 778 779fun factor th = 780 let 781 fun fact sub = removeSym (Thm.subst sub th) 782 in 783 List.map fact (factor' (Thm.clause th)) 784 end; 785 786end 787