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