src/Tools/Metis/src/Units.sml

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Units.sml	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,106 @@
+(* ========================================================================= *)
+(* A STORE FOR UNIT THEOREMS                                                 *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Units :> Units =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of unit store.                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+type unitThm = Literal.literal * Thm.thm;
+
+datatype units = Units of unitThm LiteralNet.literalNet;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val empty = Units (LiteralNet.new {fifo = false});
+
+fun size (Units net) = LiteralNet.size net;
+
+fun toString units = "U{" ^ Int.toString (size units) ^ "}";
+
+val pp = Parser.ppMap toString Parser.ppString;
+
+(* ------------------------------------------------------------------------- *)
+(* Add units into the store.                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun add (units as Units net) (uTh as (lit,th)) =
+    let
+      val net = LiteralNet.insert net (lit,uTh)
+    in
+      case total Literal.sym lit of
+        NONE => Units net
+      | SOME (lit' as (pol,_)) =>
+        let
+          val th' = (if pol then Rule.symEq else Rule.symNeq) lit th
+          val net = LiteralNet.insert net (lit',(lit',th'))
+        in
+          Units net
+        end
+    end;
+
+val addList = foldl (fn (th,u) => add u th);
+
+(* ------------------------------------------------------------------------- *)
+(* Matching.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun match (Units net) lit =
+    let
+      fun check (uTh as (lit',_)) =
+          case total (Literal.match Subst.empty lit') lit of
+            NONE => NONE
+          | SOME sub => SOME (uTh,sub)
+    in
+      first check (LiteralNet.match net lit)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Reducing by repeated matching and resolution.                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun reduce units =
+    let
+      fun red1 (lit,news_th) =
+          case total Literal.destIrrefl lit of
+            SOME tm =>
+            let
+              val (news,th) = news_th
+              val th = Thm.resolve lit th (Thm.refl tm)
+            in
+              (news,th)
+            end
+          | NONE =>
+            let
+              val lit' = Literal.negate lit
+            in
+              case match units lit' of
+                NONE => news_th
+              | SOME ((_,rth),sub) =>
+                let
+                  val (news,th) = news_th
+                  val rth = Thm.subst sub rth
+                  val th = Thm.resolve lit th rth
+                  val new = LiteralSet.delete (Thm.clause rth) lit'
+                  val news = LiteralSet.union new news
+                in
+                  (news,th)
+                end
+            end
+
+      fun red (news,th) =
+          if LiteralSet.null news then th
+          else red (LiteralSet.foldl red1 (LiteralSet.empty,th) news)
+    in
+      fn th => Rule.removeSym (red (Thm.clause th, th))
+    end;
+
+end