src/Tools/Metis/src/Rule.sml

 (* ========================================================================= *)
 (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS                     *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License       *)
 (* ========================================================================= *)
 
 structure Rule :> Rule =
 struct
 
 open Useful;
 
 (* ------------------------------------------------------------------------- *)
+(* Variable names.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val xVarName = Name.fromString "x";
+val xVar = Term.Var xVarName;
+
+val yVarName = Name.fromString "y";
+val yVar = Term.Var yVarName;
+
+val zVarName = Name.fromString "z";
+val zVar = Term.Var zVarName;
+
+fun xIVarName i = Name.fromString ("x" ^ Int.toString i);
+fun xIVar i = Term.Var (xIVarName i);
+
+fun yIVarName i = Name.fromString ("y" ^ Int.toString i);
+fun yIVar i = Term.Var (yIVarName i);
+
+(* ------------------------------------------------------------------------- *)
 (*                                                                           *)
 (* --------- reflexivity                                                     *)
 (*   x = x                                                                   *)
 (* ------------------------------------------------------------------------- *)
 
-val reflexivity = Thm.refl (Term.Var "x");
+fun reflexivityRule x = Thm.refl x;
+
+val reflexivity = reflexivityRule xVar;
 
 (* ------------------------------------------------------------------------- *)
 (*                                                                           *)
 (* --------------------- symmetry                                            *)
 (*   ~(x = y) \/ y = x                                                       *)
 (* ------------------------------------------------------------------------- *)
 
-val symmetry =
-    let
-      val x = Term.Var "x"
-      and y = Term.Var "y"
-      val reflTh = reflexivity
+fun symmetryRule x y =
+    let
+      val reflTh = reflexivityRule x
       val reflLit = Thm.destUnit reflTh
       val eqTh = Thm.equality reflLit [0] y
     in
       Thm.resolve reflLit reflTh eqTh
     end;
 
+val symmetry = symmetryRule xVar yVar;
+
 (* ------------------------------------------------------------------------- *)
 (*                                                                           *)
 (* --------------------------------- transitivity                            *)
 (*   ~(x = y) \/ ~(y = z) \/ x = z                                           *)
 (* ------------------------------------------------------------------------- *)
 
 val transitivity =
     let
-      val x = Term.Var "x"
-      and y = Term.Var "y"
-      and z = Term.Var "z"
-      val eqTh = Thm.equality (Literal.mkEq (y,z)) [0] x
-    in
-      Thm.resolve (Literal.mkEq (y,x)) symmetry eqTh
+      val eqTh = Thm.equality (Literal.mkEq (yVar,zVar)) [0] xVar
+    in
+      Thm.resolve (Literal.mkEq (yVar,xVar)) symmetry eqTh
     end;
 
 (* ------------------------------------------------------------------------- *)
 (*   x = y \/ C                                                              *)
 (* -------------- symEq (x = y)                                              *)

 
 fun symEq lit th =
     let
       val (x,y) = Literal.destEq lit
     in
-      if x = y then th
+      if Term.equal x y then th
       else
         let
-          val sub = Subst.fromList [("x",x),("y",y)]
+          val sub = Subst.fromList [(xVarName,x),(yVarName,y)]
           val symTh = Thm.subst sub symmetry
         in
           Thm.resolve lit th symTh
         end
     end;

 (* t = u \/ C.                                                               *)
 (* ------------------------------------------------------------------------- *)
 
 type equation = (Term.term * Term.term) * Thm.thm;
 
-fun ppEquation pp (eqn as (_,th)) = Thm.pp pp th;
-
-fun equationToString x = Parser.toString ppEquation x;
+fun ppEquation (_,th) = Thm.pp th;
+
+val equationToString = Print.toString ppEquation;
 
 fun equationLiteral (t_u,th) =
     let
       val lit = Literal.mkEq t_u
     in

     end;
 
 fun reflEqn t = ((t,t), Thm.refl t);
 
 fun symEqn (eqn as ((t,u), th)) =
-    if t = u then eqn
+    if Term.equal t u then eqn
     else
       ((u,t),
        case equationLiteral eqn of
          SOME t_u => symEq t_u th
        | NONE => th);
 
 fun transEqn (eqn1 as ((x,y), th1)) (eqn2 as ((_,z), th2)) =
-    if x = y then eqn2
-    else if y = z then eqn1
-    else if x = z then reflEqn x
+    if Term.equal x y then eqn2
+    else if Term.equal y z then eqn1
+    else if Term.equal x z then reflEqn x
     else
       ((x,z),
        case equationLiteral eqn1 of
          NONE => th1
        | SOME x_y =>
          case equationLiteral eqn2 of
            NONE => th2
          | SOME y_z =>
            let
-             val sub = Subst.fromList [("x",x),("y",y),("z",z)]
+             val sub = Subst.fromList [(xVarName,x),(yVarName,y),(zVarName,z)]
              val th = Thm.subst sub transitivity
              val th = Thm.resolve x_y th1 th
              val th = Thm.resolve y_z th2 th
            in
              th
            end);
 
-(*DEBUG
+(*MetisDebug
 val transEqn = fn eqn1 => fn eqn2 =>
     transEqn eqn1 eqn2
     handle Error err =>
       raise Error ("Rule.transEqn:\neqn1 = " ^ equationToString eqn1 ^
                    "\neqn2 = " ^ equationToString eqn2 ^ "\n" ^ err);

       res
     end
     handle Error err =>
       (print (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n");
        raise Error (s ^ ": " ^ err));
-    
+
 fun thenConvTrans tm (tm',th1) (tm'',th2) =
     let
       val eqn1 = ((tm,tm'),th1)
       and eqn2 = ((tm',tm''),th2)
       val (_,th) = transEqn eqn1 eqn2

 fun everyConv [] tm = allConv tm
   | everyConv [conv] tm = conv tm
   | everyConv (conv :: convs) tm = thenConv conv (everyConv convs) tm;
 
 fun rewrConv (eqn as ((x,y), eqTh)) path tm =
-    if x = y then allConv tm
+    if Term.equal x y then allConv tm
     else if null path then (y,eqTh)
     else
       let
         val reflTh = Thm.refl tm
         val reflLit = Thm.destUnit reflTh

         val tm' = Term.replace tm (path,y)
       in
         (tm',th)
       end;
 
-(*DEBUG
+(*MetisDebug
 val rewrConv = fn eqn as ((x,y),eqTh) => fn path => fn tm =>
     rewrConv eqn path tm
     handle Error err =>
       raise Error ("Rule.rewrConv:\nx = " ^ Term.toString x ^
                    "\ny = " ^ Term.toString y ^

       and h tm = tryConv (thenConv conv f) tm
     in
       f
     end;
 
-(*DEBUG
+(*MetisDebug
 val repeatTopDownConv = fn conv => fn tm =>
     repeatTopDownConv conv tm
     handle Error err => raise Error ("repeatTopDownConv: " ^ err);
 *)
 

 fun thenLiterule literule1 literule2 lit =
     let
       val res1 as (lit',th1) = literule1 lit
       val res2 as (lit'',th2) = literule2 lit'
     in
-      if lit = lit' then res2
-      else if lit' = lit'' then res1
-      else if lit = lit'' then allLiterule lit
+      if Literal.equal lit lit' then res2
+      else if Literal.equal lit' lit'' then res1
+      else if Literal.equal lit lit'' then allLiterule lit
       else
         (lit'',
          if not (Thm.member lit' th1) then th1
          else if not (Thm.negateMember lit' th2) then th2
          else Thm.resolve lit' th1 th2)

   | everyLiterule [literule] lit = literule lit
   | everyLiterule (literule :: literules) lit =
     thenLiterule literule (everyLiterule literules) lit;
 
 fun rewrLiterule (eqn as ((x,y),eqTh)) path lit =
-    if x = y then allLiterule lit
+    if Term.equal x y then allLiterule lit
     else
       let
         val th = Thm.equality lit path y
         val th =
             case equationLiteral eqn of

         val lit' = Literal.replace lit (path,y)
       in
         (lit',th)
       end;
 
-(*DEBUG
+(*MetisDebug
 val rewrLiterule = fn eqn => fn path => fn lit =>
     rewrLiterule eqn path lit
     handle Error err =>
       raise Error ("Rule.rewrLiterule:\neqn = " ^ equationToString eqn ^
                    "\npath = " ^ Term.pathToString path ^

 
 fun literalRule literule lit th =
     let
       val (lit',litTh) = literule lit
     in
-      if lit = lit' then th
+      if Literal.equal lit lit' then th
       else if not (Thm.negateMember lit litTh) then litTh
       else Thm.resolve lit th litTh
     end;
 
-(*DEBUG
+(*MetisDebug
 val literalRule = fn literule => fn lit => fn th =>
     literalRule literule lit th
     handle Error err =>
       raise Error ("Rule.literalRule:\nlit = " ^ Literal.toString lit ^
                    "\nth = " ^ Thm.toString th ^ "\n" ^ err);

     end;
 
 fun allLiteralsRule literule th = literalsRule literule (Thm.clause th) th;
 
 fun convRule conv = allLiteralsRule (allArgumentsLiterule conv);
-  
+
 (* ------------------------------------------------------------------------- *)
 (*                                                                           *)
 (* ---------------------------------------------- functionCongruence (f,n)   *)
 (*   ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/                              *)
 (*   f x0 ... x{n-1} = f y0 ... y{n-1}                                       *)
 (* ------------------------------------------------------------------------- *)
 
 fun functionCongruence (f,n) =
     let
-      val xs = List.tabulate (n, fn i => Term.Var ("x" ^ Int.toString i))
-      and ys = List.tabulate (n, fn i => Term.Var ("y" ^ Int.toString i))
+      val xs = List.tabulate (n,xIVar)
+      and ys = List.tabulate (n,yIVar)
 
       fun cong ((i,yi),(th,lit)) =
           let
             val path = [1,i]
             val th = Thm.resolve lit th (Thm.equality lit path yi)

 (*   ~R x0 ... x{n-1} \/ R y0 ... y{n-1}                                     *)
 (* ------------------------------------------------------------------------- *)
 
 fun relationCongruence (R,n) =
     let
-      val xs = List.tabulate (n, fn i => Term.Var ("x" ^ Int.toString i))
-      and ys = List.tabulate (n, fn i => Term.Var ("y" ^ Int.toString i))
+      val xs = List.tabulate (n,xIVar)
+      and ys = List.tabulate (n,yIVar)
 
       fun cong ((i,yi),(th,lit)) =
           let
             val path = [i]
             val th = Thm.resolve lit th (Thm.equality lit path yi)

 
 fun symNeq lit th =
     let
       val (x,y) = Literal.destNeq lit
     in
-      if x = y then th
+      if Term.equal x y then th
       else
         let
-          val sub = Subst.fromList [("x",y),("y",x)]
+          val sub = Subst.fromList [(xVarName,y),(yVarName,x)]
           val symTh = Thm.subst sub symmetry
         in
           Thm.resolve lit th symTh
         end
     end;

 
 local
   fun expand lit =
       let
         val (x,y) = Literal.destNeq lit
-      in
-        if (Term.isTypedVar x orelse Term.isTypedVar y) andalso x <> y then
-          Subst.unify Subst.empty x y
-        else raise Error "expand"
+        val _ = Term.isTypedVar x orelse Term.isTypedVar y orelse
+                raise Error "Rule.expandAbbrevs: no vars"
+        val _ = not (Term.equal x y) orelse
+                raise Error "Rule.expandAbbrevs: equal vars"
+      in
+        Subst.unify Subst.empty x y
       end;
 in
   fun expandAbbrevs th =
       case LiteralSet.firstl (total expand) (Thm.clause th) of
         NONE => removeIrrefl th

 local
   datatype edge =
       FactorEdge of Atom.atom * Atom.atom
     | ReflEdge of Term.term * Term.term;
 
-  fun ppEdge p (FactorEdge atm_atm') = Parser.ppPair Atom.pp Atom.pp p atm_atm'
-    | ppEdge p (ReflEdge tm_tm') = Parser.ppPair Term.pp Term.pp p tm_tm';
+  fun ppEdge (FactorEdge atm_atm') = Print.ppPair Atom.pp Atom.pp atm_atm'
+    | ppEdge (ReflEdge tm_tm') = Print.ppPair Term.pp Term.pp tm_tm';
 
   datatype joinStatus =
       Joined
     | Joinable of Subst.subst
     | Apart;

       in
         snd (List.foldl init ([],[]) acc)
       end
     | init_edges acc apart ((sub,edge) :: sub_edges) =
       let
-(*DEBUG
+(*MetisDebug
         val () = if not (Subst.null sub) then ()
                  else raise Bug "Rule.factor.init_edges: empty subst"
 *)
         val (acc,apart) =
             case updateApart sub apart of

         fact acc others
       end;
 in
   fun factor' cl =
       let
-(*TRACE6
-        val () = Parser.ppTrace LiteralSet.pp "Rule.factor': cl" cl
+(*MetisTrace6
+        val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl
 *)
         val edges = mk_edges [] [] (LiteralSet.toList cl)
-(*TRACE6
-        val ppEdgesSize = Parser.ppMap length Parser.ppInt
-        val ppEdgel = Parser.ppList ppEdge
-        val ppEdges = Parser.ppList (Parser.ppTriple ppEdgel Subst.pp ppEdgel)
-        val () = Parser.ppTrace ppEdgesSize "Rule.factor': |edges|" edges
-        val () = Parser.ppTrace ppEdges "Rule.factor': edges" edges
+(*MetisTrace6
+        val ppEdgesSize = Print.ppMap length Print.ppInt
+        val ppEdgel = Print.ppList ppEdge
+        val ppEdges = Print.ppList (Print.ppTriple ppEdgel Subst.pp ppEdgel)
+        val () = Print.trace ppEdgesSize "Rule.factor': |edges|" edges
+        val () = Print.trace ppEdges "Rule.factor': edges" edges
 *)
         val result = fact [] edges
-(*TRACE6
-        val ppResult = Parser.ppList Subst.pp
-        val () = Parser.ppTrace ppResult "Rule.factor': result" result
+(*MetisTrace6
+        val ppResult = Print.ppList Subst.pp
+        val () = Print.trace ppResult "Rule.factor': result" result
 *)
       in
         result
       end;
 end;