1(* ========================================================================= *) 2(* A STORE FOR UNIT THEOREMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Units :> Units = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* A type of unit store. *) 13(* ------------------------------------------------------------------------- *) 14 15type unitThm = Literal.literal * Thm.thm; 16 17datatype units = Units of unitThm LiteralNet.literalNet; 18 19(* ------------------------------------------------------------------------- *) 20(* Basic operations. *) 21(* ------------------------------------------------------------------------- *) 22 23val empty = Units (LiteralNet.new {fifo = false}); 24 25fun size (Units net) = LiteralNet.size net; 26 27fun toString units = "U{" ^ Int.toString (size units) ^ "}"; 28 29val pp = Print.ppMap toString Print.ppString; 30 31(* ------------------------------------------------------------------------- *) 32(* Add units into the store. *) 33(* ------------------------------------------------------------------------- *) 34 35fun add (units as Units net) (uTh as (lit,th)) = 36 let 37 val net = LiteralNet.insert net (lit,uTh) 38 in 39 case total Literal.sym lit of 40 NONE => Units net 41 | SOME (lit' as (pol,_)) => 42 let 43 val th' = (if pol then Rule.symEq else Rule.symNeq) lit th 44 val net = LiteralNet.insert net (lit',(lit',th')) 45 in 46 Units net 47 end 48 end; 49 50val addList = List.foldl (fn (th,u) => add u th); 51 52(* ------------------------------------------------------------------------- *) 53(* Matching. *) 54(* ------------------------------------------------------------------------- *) 55 56fun match (Units net) lit = 57 let 58 fun check (uTh as (lit',_)) = 59 case total (Literal.match Subst.empty lit') lit of 60 NONE => NONE 61 | SOME sub => SOME (uTh,sub) 62 in 63 first check (LiteralNet.match net lit) 64 end; 65 66(* ------------------------------------------------------------------------- *) 67(* Reducing by repeated matching and resolution. *) 68(* ------------------------------------------------------------------------- *) 69 70fun reduce units = 71 let 72 fun red1 (lit,news_th) = 73 case total Literal.destIrrefl lit of 74 SOME tm => 75 let 76 val (news,th) = news_th 77 val th = Thm.resolve lit th (Thm.refl tm) 78 in 79 (news,th) 80 end 81 | NONE => 82 let 83 val lit' = Literal.negate lit 84 in 85 case match units lit' of 86 NONE => news_th 87 | SOME ((_,rth),sub) => 88 let 89 val (news,th) = news_th 90 val rth = Thm.subst sub rth 91 val th = Thm.resolve lit th rth 92 val new = LiteralSet.delete (Thm.clause rth) lit' 93 val news = LiteralSet.union new news 94 in 95 (news,th) 96 end 97 end 98 99 fun red (news,th) = 100 if LiteralSet.null news then th 101 else red (LiteralSet.foldl red1 (LiteralSet.empty,th) news) 102 in 103 fn th => Rule.removeSym (red (Thm.clause th, th)) 104 end; 105 106end 107