1(* ========================================================================= *) 2(* A STORE IN WHICH TO CACHE UNIT THEOREMS *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6structure mlibUnits :> mlibUnits = 7struct 8 9open mlibUseful mlibTerm mlibThm mlibMatch; 10 11structure N = mlibLiteralnet; local open mlibLiteralnet in end; 12 13val |<>| = mlibSubst.|<>|; 14val formula_subst = mlibSubst.formula_subst; 15 16(* ------------------------------------------------------------------------- *) 17(* Auxiliary functions. *) 18(* ------------------------------------------------------------------------- *) 19 20fun lift_options f = 21 let 22 fun g res [] = SOME (rev res) 23 | g res (x :: xs) = case f x of SOME y => g (y :: res) xs | NONE => NONE 24 in 25 g [] 26 end; 27 28fun psym lit = 29 let 30 val (s, (x,y)) = (I ## dest_eq) (dest_literal lit) 31 val () = assert (x <> y) (Error "psym: refl") 32 in 33 mk_literal (s, mk_eq (y,x)) 34 end; 35 36(* ------------------------------------------------------------------------- *) 37(* Operations on the raw unit cache. *) 38(* ------------------------------------------------------------------------- *) 39 40type uns = thm N.literalnet; 41 42val uempty : uns = N.empty {fifo = false}; 43 44fun usubsumes uns lit = 45 List.find (fn t => can (match_literals (dest_unit t)) lit) 46 (N.match uns lit); 47 48fun ucontr uns th = 49 let 50 val th = FRESH_VARS th 51 val lit = negate (dest_unit th) 52 fun check t = (unify_literals |<>| (dest_unit t) lit, t) 53 in 54 case first (total check) (N.unify uns lit) of NONE => NONE 55 | SOME (s,t) => SOME (RESOLVE (formula_subst s lit) (INST s t) (INST s th)) 56 end; 57 58fun uadd th uns = 59 let 60 val l = dest_unit th 61 in 62 if Option.isSome (usubsumes uns l) then uns else 63 (case total psym l of NONE => I | SOME l' => N.insert (l' |-> SYM l th)) 64 (N.insert (l |-> th) uns) 65 end; 66 67fun uprove uns = 68 let 69 fun pr lit = 70 Option.map (fn th => INST (match_literals (dest_unit th) lit) th) 71 (usubsumes uns lit) 72 in 73 lift_options pr 74 end; 75 76fun udemod uns = 77 let 78 fun demod (lit,th) = 79 case uprove uns [negate lit] of NONE => th 80 | SOME [dth] => RESOLVE lit th dth 81 | SOME _ => raise Bug "unit_demod: corrupt" 82 in 83 fn th => foldl demod th (clause th) 84 end; 85 86(* ------------------------------------------------------------------------- *) 87(* The user interface. *) 88(* ------------------------------------------------------------------------- *) 89 90type units = (thm,uns) sum; 91 92val empty : units = INR uempty; 93 94fun subsumes (INL th) = K (SOME th) 95 | subsumes (INR uns) = usubsumes uns; 96 97fun contr (INL th) _ = SOME th 98 | contr (INR uns) th = 99 if is_contradiction th then SOME th 100 else Option.mapPartial (ucontr uns) (total UNIT_SQUASH th); 101 102fun prove (INL th) lits = SOME (map (fn lit => CONTR lit th) lits) 103 | prove (INR uns) lits = uprove uns lits; 104 105fun demod (INL th) _ = th 106 | demod (INR uns) th = 107 let 108 val th = udemod uns th 109 in 110 case first (fn lit => uprove uns [lit]) (clause th) of 111 SOME [th] => th 112 | _ => th 113 end; 114 115fun info ((INL _) : units) = "*" 116 | info (INR uns) = int_to_string (N.size uns); 117 118val pp_units = pp_map info pp_string; 119 120(* Adding a theorem involves squashing it to a unit, if possible. *) 121 122fun add _ (U as INL _) = U 123 | add th (U as INR uns) = 124 if is_contradiction th then INL th else 125 case total UNIT_SQUASH th of NONE => U 126 | SOME th => (case ucontr uns th of SOME c => INL c 127 | NONE => INR (uadd th uns)); 128 129val addl = C (foldl (uncurry add)); 130 131end 132