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