--- a/src/Tools/Metis/metis.ML Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/metis.ML Thu Jul 09 11:39:16 2020 +0200
@@ -1,7 +1,7 @@
(*
This file was generated by the "make_metis" script. The BSD License is used
- with Joe Hurd's kind permission. Extract from a September 13, 2010 email
- written by Joe Hurd:
+ with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010
+ email written by him:
I hereby give permission to the Isabelle team to release Metis as part
of Isabelle, with the Metis code covered under the Isabelle BSD
@@ -93,7 +93,7 @@
(* ========================================================================= *)
(* ML COMPILER SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Portable =
@@ -174,7 +174,7 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Useful =
@@ -377,6 +377,20 @@
val gcd : int -> int -> int
+(* Primes *)
+
+type sieve
+
+val initSieve : sieve
+
+val maxSieve : sieve -> int
+
+val primesSieve : sieve -> int list
+
+val incSieve : sieve -> bool * sieve
+
+val nextSieve : sieve -> int * sieve
+
val primes : int -> int list
val primesUpTo : int -> int list
@@ -507,7 +521,7 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Useful :> Metis_Useful =
@@ -981,33 +995,99 @@
end;
end;
-local
- fun calcPrimes mode ps i n =
- if n = 0 then ps
- else if List.exists (fn p => divides p i) ps then
- let
- val i = i + 1
- and n = if mode then n else n - 1
- in
- calcPrimes mode ps i n
- end
- else
- let
- val ps = ps @ [i]
- and i = i + 1
- and n = n - 1
- in
- calcPrimes mode ps i n
- end;
-in
- fun primes n =
- if n <= 0 then []
- else calcPrimes true [2] 3 (n - 1);
-
- fun primesUpTo n =
- if n < 2 then []
- else calcPrimes false [2] 3 (n - 2);
-end;
+(* Primes *)
+
+datatype sieve =
+ Sieve of
+ {max : int,
+ primes : (int * (int * int)) list};
+
+val initSieve =
+ let
+ val n = 1
+ and ps = []
+ in
+ Sieve
+ {max = n,
+ primes = ps}
+ end;
+
+fun maxSieve (Sieve {max = n, ...}) = n;
+
+fun primesSieve (Sieve {primes = ps, ...}) = List.map fst ps;
+
+fun incSieve sieve =
+ let
+ val n = maxSieve sieve + 1
+
+ fun add i ps =
+ case ps of
+ [] => (true,[(n,(0,0))])
+ | (p,(k,j)) :: ps =>
+ let
+ val k = (k + i) mod p
+
+ val j = j + i
+ in
+ if k = 0 then (false, (p,(k,j)) :: ps)
+ else
+ let
+ val (b,ps) = add j ps
+ in
+ (b, (p,(k,0)) :: ps)
+ end
+ end
+
+ val Sieve {primes = ps, ...} = sieve
+
+ val (b,ps) = add 1 ps
+
+ val sieve =
+ Sieve
+ {max = n,
+ primes = ps}
+ in
+ (b,sieve)
+ end;
+
+fun nextSieve sieve =
+ let
+ val (b,sieve) = incSieve sieve
+ in
+ if b then (maxSieve sieve, sieve)
+ else nextSieve sieve
+ end;
+
+local
+ fun inc s =
+ let
+ val (_,s) = incSieve s
+ in
+ s
+ end;
+in
+ fun primesUpTo m =
+ if m <= 1 then []
+ else primesSieve (funpow (m - 1) inc initSieve);
+end;
+
+val primes =
+ let
+ fun next s n =
+ if n <= 0 then []
+ else
+ let
+ val (p,s) = nextSieve s
+
+ val n = n - 1
+
+ val ps = next s n
+ in
+ p :: ps
+ end
+ in
+ next initSieve
+ end;
(* ------------------------------------------------------------------------- *)
(* Strings. *)
@@ -1354,7 +1434,9 @@
fun timed f a =
let
val tmr = Timer.startCPUTimer ()
+
val res = f a
+
val {usr,sys,...} = Timer.checkCPUTimer tmr
in
(Time.toReal usr + Time.toReal sys, res)
@@ -1388,7 +1470,7 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Lazy =
@@ -1410,7 +1492,7 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Lazy :> Metis_Lazy =
@@ -1451,7 +1533,7 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Ordered =
@@ -1487,7 +1569,7 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_IntOrdered =
@@ -1513,7 +1595,7 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Map =
@@ -1706,7 +1788,7 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Map :> Metis_Map =
@@ -3136,7 +3218,7 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_KeyMap =
@@ -3339,7 +3421,7 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
functor Metis_KeyMap (Key : Metis_Ordered) :> Metis_KeyMap where type key = Key.t =
@@ -4786,7 +4868,7 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Set =
@@ -4958,7 +5040,7 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Set :> Metis_Set =
@@ -5292,7 +5374,7 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_ElementSet =
@@ -5427,8 +5509,10 @@
val disjoint : set -> set -> bool
(* ------------------------------------------------------------------------- *)
-(* Closing under an operation. *)
-(* ------------------------------------------------------------------------- *)
+(* Pointwise operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val lift : (element -> set) -> set -> set
val closedAdd : (element -> set) -> set -> set -> set
@@ -5457,6 +5541,34 @@
val domain : 'a map -> set
(* ------------------------------------------------------------------------- *)
+(* Depth-first search. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ordering =
+ Linear of element list
+ | Cycle of element list
+
+val preOrder : (element -> set) -> set -> ordering
+
+val postOrder : (element -> set) -> set -> ordering
+
+val preOrdered : (element -> set) -> element list -> bool
+
+val postOrdered : (element -> set) -> element list -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Strongly connected components. *)
+(* ------------------------------------------------------------------------- *)
+
+val preOrderSCC : (element -> set) -> set -> set list
+
+val postOrderSCC : (element -> set) -> set -> set list
+
+val preOrderedSCC : (element -> set) -> set list -> bool
+
+val postOrderedSCC : (element -> set) -> set list -> bool
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing. *)
(* ------------------------------------------------------------------------- *)
@@ -5482,7 +5594,7 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
functor Metis_ElementSet (
@@ -5784,8 +5896,15 @@
fun disjoint (Metis_Set m1) (Metis_Set m2) = KM.disjointDomain m1 m2;
(* ------------------------------------------------------------------------- *)
-(* Closing under an operation. *)
-(* ------------------------------------------------------------------------- *)
+(* Pointwise operations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun lift f =
+ let
+ fun inc (elt,set) = union set (f elt)
+ in
+ foldl inc empty
+ end;
fun closedAdd f =
let
@@ -5818,6 +5937,324 @@
fun fromList elts = addList empty elts;
(* ------------------------------------------------------------------------- *)
+(* Depth-first search. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ordering =
+ Linear of element list
+ | Cycle of element list;
+
+fun postOrdered children =
+ let
+ fun check acc elts =
+ case elts of
+ [] => true
+ | elt :: elts =>
+ not (member elt acc) andalso
+ let
+ val acc = closedAdd children acc (singleton elt)
+ in
+ check acc elts
+ end
+ in
+ check empty
+ end;
+
+fun preOrdered children elts = postOrdered children (List.rev elts);
+
+local
+ fun takeStackset elt =
+ let
+ fun notElement (e,_,_) = not (equalElement e elt)
+ in
+ Metis_Useful.takeWhile notElement
+ end;
+
+ fun consElement ((e,_,_),el) = e :: el;
+
+ fun depthFirstSearch children =
+ let
+ fun traverse (dealt,dealtset) (stack,stackset) work =
+ case work of
+ [] =>
+ (case stack of
+ [] => Linear dealt
+ | (elt,work,stackset) :: stack =>
+ let
+ val dealt = elt :: dealt
+
+ val dealtset = add dealtset elt
+ in
+ traverse (dealt,dealtset) (stack,stackset) work
+ end)
+ | elt :: work =>
+ if member elt dealtset then
+ traverse (dealt,dealtset) (stack,stackset) work
+ else if member elt stackset then
+ let
+ val cycle = takeStackset elt stack
+
+ val cycle = elt :: List.foldl consElement [elt] cycle
+ in
+ Cycle cycle
+ end
+ else
+ let
+ val stack = (elt,work,stackset) :: stack
+
+ val stackset = add stackset elt
+
+ val work = toList (children elt)
+ in
+ traverse (dealt,dealtset) (stack,stackset) work
+ end
+
+ val dealt = []
+ and dealtset = empty
+ and stack = []
+ and stackset = empty
+ in
+ traverse (dealt,dealtset) (stack,stackset)
+ end;
+in
+ fun preOrder children roots =
+ let
+ val result = depthFirstSearch children (toList roots)
+
+(*BasicDebug
+ val () =
+ case result of
+ Cycle _ => ()
+ | Linear l =>
+ let
+ val () =
+ if subset roots (fromList l) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrder: missing roots"
+
+ val () =
+ if preOrdered children l then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrder: bad ordering"
+ in
+ ()
+ end
+*)
+ in
+ result
+ end;
+
+ fun postOrder children roots =
+ case depthFirstSearch children (toList roots) of
+ Linear l =>
+ let
+ val l = List.rev l
+
+(*BasicDebug
+ val () =
+ if subset roots (fromList l) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrder: missing roots"
+
+ val () =
+ if postOrdered children l then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrder: bad ordering"
+*)
+ in
+ Linear l
+ end
+ | cycle => cycle;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Strongly connected components. *)
+(* ------------------------------------------------------------------------- *)
+
+fun postOrderedSCC children =
+ let
+ fun check acc eltsl =
+ case eltsl of
+ [] => true
+ | elts :: eltsl =>
+ not (null elts) andalso
+ disjoint elts acc andalso
+ let
+ fun addElt elt = closedAdd children acc (singleton elt)
+
+ val (root,elts) = deletePick elts
+
+ fun checkElt elt = member root (addElt elt)
+ in
+ all checkElt elts andalso
+ let
+ val acc = addElt root
+ in
+ subset elts acc andalso
+ check acc eltsl
+ end
+ end
+ in
+ check empty
+ end;
+
+fun preOrderedSCC children eltsl = postOrderedSCC children (List.rev eltsl);
+
+(* An implementation of Tarjan's algorithm: *)
+
+(* http://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm *)
+
+local
+ datatype stackSCC = StackSCC of set * (element * set) list;
+
+ val emptyStack = StackSCC (empty,[]);
+
+ fun pushStack (StackSCC (elts,eltl)) elt =
+ StackSCC (add elts elt, (elt,elts) :: eltl);
+
+ fun inStack elt (StackSCC (elts,_)) = member elt elts;
+
+ fun popStack root =
+ let
+ fun pop scc eltl =
+ case eltl of
+ [] => raise Metis_Useful.Bug "Metis_ElementSet.popStack"
+ | (elt,elts) :: eltl =>
+ let
+ val scc = add scc elt
+ in
+ if equalElement elt root then (scc, StackSCC (elts,eltl))
+ else pop scc eltl
+ end
+ in
+ fn sccs => fn StackSCC (_,eltl) =>
+ let
+ val (scc,stack) = pop empty eltl
+ in
+ (scc :: sccs, stack)
+ end
+ end;
+
+ fun getIndex indices e : int =
+ case KM.peek indices e of
+ SOME i => i
+ | NONE => raise Metis_Useful.Bug "Metis_ElementSet.getIndex";
+
+ fun isRoot indices lows e = getIndex indices e = getIndex lows e;
+
+ fun reduceIndex indices (e,i) =
+ let
+ val j = getIndex indices e
+ in
+ if j <= i then indices else KM.insert indices (e,i)
+ end;
+
+ fun tarjan children =
+ let
+ fun dfsVertex sccs callstack index indices lows stack elt =
+ let
+ val indices = KM.insert indices (elt,index)
+ and lows = KM.insert lows (elt,index)
+
+ val index = index + 1
+
+ val stack = pushStack stack elt
+
+ val chil = toList (children elt)
+ in
+ dfsSuccessors sccs callstack index indices lows stack elt chil
+ end
+
+ and dfsSuccessors sccs callstack index indices lows stack elt chil =
+ case chil of
+ [] =>
+ let
+ val (sccs,stack) =
+ if isRoot indices lows elt then popStack elt sccs stack
+ else (sccs,stack)
+ in
+ case callstack of
+ [] => (sccs,index,indices,lows)
+ | (p,elts) :: callstack =>
+ let
+ val lows = reduceIndex lows (p, getIndex lows elt)
+ in
+ dfsSuccessors sccs callstack index indices lows stack p elts
+ end
+ end
+ | c :: chil =>
+ case KM.peek indices c of
+ NONE =>
+ let
+ val callstack = (elt,chil) :: callstack
+ in
+ dfsVertex sccs callstack index indices lows stack c
+ end
+ | SOME cind =>
+ let
+ val lows =
+ if inStack c stack then reduceIndex lows (elt,cind)
+ else lows
+ in
+ dfsSuccessors sccs callstack index indices lows stack elt chil
+ end
+
+ fun dfsRoots sccs index indices lows elts =
+ case elts of
+ [] => sccs
+ | elt :: elts =>
+ if KM.inDomain elt indices then
+ dfsRoots sccs index indices lows elts
+ else
+ let
+ val callstack = []
+
+ val (sccs,index,indices,lows) =
+ dfsVertex sccs callstack index indices lows emptyStack elt
+ in
+ dfsRoots sccs index indices lows elts
+ end
+
+ val sccs = []
+ and index = 0
+ and indices = KM.new ()
+ and lows = KM.new ()
+ in
+ dfsRoots sccs index indices lows
+ end;
+in
+ fun preOrderSCC children roots =
+ let
+ val result = tarjan children (toList roots)
+
+(*BasicDebug
+ val () =
+ if subset roots (unionList result) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrderSCC: missing roots"
+
+ val () =
+ if preOrderedSCC children result then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrderSCC: bad ordering"
+*)
+ in
+ result
+ end;
+
+ fun postOrderSCC children roots =
+ let
+ val result = List.rev (tarjan children (toList roots))
+
+(*BasicDebug
+ val () =
+ if subset roots (unionList result) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrderSCC: missing roots"
+
+ val () =
+ if postOrderedSCC children result then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrderSCC: bad ordering"
+*)
+ in
+ result
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing. *)
(* ------------------------------------------------------------------------- *)
@@ -5858,7 +6295,7 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Sharing =
@@ -5906,7 +6343,7 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Sharing :> Metis_Sharing =
@@ -6067,7 +6504,7 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Stream =
@@ -6123,6 +6560,8 @@
val drop : int -> 'a stream -> 'a stream (* raises Subscript *)
+val unfold : ('b -> ('a * 'b) option) -> 'b -> 'a stream
+
(* ------------------------------------------------------------------------- *)
(* Metis_Stream versions of standard list operations: these might not terminate. *)
(* ------------------------------------------------------------------------- *)
@@ -6155,6 +6594,8 @@
(* Metis_Stream operations. *)
(* ------------------------------------------------------------------------- *)
+val primes : int stream
+
val memoize : 'a stream -> 'a stream
val listConcat : 'a list stream -> 'a stream
@@ -6179,7 +6620,7 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Stream :> Metis_Stream =
@@ -6271,6 +6712,16 @@
fun drop n s = funpow n tl s handle Empty => raise Subscript;
+fun unfold f =
+ let
+ fun next b () =
+ case f b of
+ NONE => Nil
+ | SOME (a,b) => Cons (a, next b)
+ in
+ fn b => next b ()
+ end;
+
(* ------------------------------------------------------------------------- *)
(* Metis_Stream versions of standard list operations: these might not terminate. *)
(* ------------------------------------------------------------------------- *)
@@ -6360,6 +6811,13 @@
(* Metis_Stream operations. *)
(* ------------------------------------------------------------------------- *)
+val primes =
+ let
+ fun next s = SOME (Metis_Useful.nextSieve s)
+ in
+ unfold next Metis_Useful.initSieve
+ end;
+
fun memoize Nil = Nil
| memoize (Cons (h,t)) = Cons (h, Metis_Lazy.memoize (fn () => memoize (t ())));
@@ -6416,7 +6874,7 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Heap =
@@ -6450,7 +6908,7 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Heap :> Metis_Heap =
@@ -6530,7 +6988,7 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Print =
@@ -6737,7 +7195,7 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Print :> Metis_Print =
@@ -8285,12 +8743,17 @@
toStreamWithLineLength len ppA a
end;
-local
- val sep = mkWord " =";
-in
- fun trace ppX nameX x =
- Metis_Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
-end;
+fun trace ppX nameX =
+ let
+ fun ppNameX x =
+ consistentBlock 2
+ [ppString nameX,
+ ppString " =",
+ break,
+ ppX x]
+ in
+ fn x => Metis_Useful.trace (toString ppNameX x ^ "\n")
+ end;
end
@@ -8298,7 +8761,7 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Parse =
@@ -8415,7 +8878,7 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Parse :> Metis_Parse =
@@ -8689,7 +9152,7 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Name =
@@ -8737,7 +9200,7 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Name :> Metis_Name =
@@ -8837,7 +9300,7 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_NameArity =
@@ -8887,7 +9350,7 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_NameArity :> Metis_NameArity =
@@ -8982,7 +9445,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Term =
@@ -9172,7 +9635,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Term :> Metis_Term =
@@ -9913,7 +10376,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Subst =
@@ -10035,7 +10498,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Subst :> Metis_Subst =
@@ -10287,7 +10750,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Atom =
@@ -10431,7 +10894,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Atom :> Metis_Atom =
@@ -10682,7 +11145,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Formula =
@@ -10882,7 +11345,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Formula :> Metis_Formula =
@@ -11454,7 +11917,7 @@
split asms false f1 @ split (Not f1 :: asms) false f2
| (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
| (false, Iff (f1,f2)) =>
- split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
+ split (f1 :: asms) false f2 @ split (Not f2 :: asms) true f1
| (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
(* Unsplittables *)
| _ => [add_asms asms (if pol then fm else Not fm)];
@@ -11486,7 +11949,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Literal =
@@ -11654,7 +12117,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Literal :> Metis_Literal =
@@ -11950,7 +12413,7 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Thm =
@@ -12101,7 +12564,7 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Thm :> Metis_Thm =
@@ -12318,7 +12781,7 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Proof =
@@ -12382,7 +12845,7 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Proof :> Metis_Proof =
@@ -12836,7 +13299,7 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Rule =
@@ -13113,7 +13576,7 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Rule :> Metis_Rule =
@@ -13891,7 +14354,7 @@
fun factor th =
let
- fun fact sub = removeSym (Metis_Thm.subst sub th)
+ fun fact sub = removeIrrefl (removeSym (Metis_Thm.subst sub th))
in
List.map fact (factor' (Metis_Thm.clause th))
end;
@@ -13902,7 +14365,7 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Normalize =
@@ -13960,7 +14423,7 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Normalize :> Metis_Normalize =
@@ -14608,14 +15071,24 @@
| Metis_Literal (_,lit) => Metis_Literal.toFormula lit
| And (_,_,s) => Metis_Formula.listMkConj (Metis_Set.transform form s)
| Or (_,_,s) => Metis_Formula.listMkDisj (Metis_Set.transform form s)
- | Xor (_,_,p,s) =>
- let
- val s = if p then negateLastElt s else s
- in
- Metis_Formula.listMkEquiv (Metis_Set.transform form s)
- end
+ | Xor (_,_,p,s) => xorForm p s
| Exists (_,_,n,f) => Metis_Formula.listMkExists (Metis_NameSet.toList n, form f)
- | Forall (_,_,n,f) => Metis_Formula.listMkForall (Metis_NameSet.toList n, form f);
+ | Forall (_,_,n,f) => Metis_Formula.listMkForall (Metis_NameSet.toList n, form f)
+
+ (* To convert a Xor set to an Iff list we need to know *)
+ (* whether the size of the set is even or odd: *)
+ (* *)
+ (* b XOR a = b <=> ~a *)
+ (* c XOR b XOR a = c <=> b <=> a *)
+ (* d XOR c XOR b XOR a = d <=> c <=> b <=> ~a *)
+ (* e XOR d XOR c XOR b XOR a = e <=> d <=> c <=> b <=> a *)
+ and xorForm p s =
+ let
+ val p = if Metis_Set.size s mod 2 = 0 then not p else p
+ val s = if p then s else negateLastElt s
+ in
+ Metis_Formula.listMkEquiv (Metis_Set.transform form s)
+ end;
in
val toFormula = form;
end;
@@ -15351,7 +15824,7 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Model =
@@ -15631,7 +16104,7 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Model :> Metis_Model =
@@ -16912,7 +17385,7 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Problem =
@@ -16978,7 +17451,7 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Problem :> Metis_Problem =
@@ -17141,7 +17614,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_TermNet =
@@ -17194,7 +17667,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_TermNet :> Metis_TermNet =
@@ -17652,7 +18125,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_AtomNet =
@@ -17703,7 +18176,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_AtomNet :> Metis_AtomNet =
@@ -17765,7 +18238,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_LiteralNet =
@@ -17818,7 +18291,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_LiteralNet :> Metis_LiteralNet =
@@ -17895,7 +18368,7 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Subsume =
@@ -17949,7 +18422,7 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Subsume :> Metis_Subsume =
@@ -18046,7 +18519,7 @@
fun size (Metis_Subsume {empty, unit, nonunit = {clauses,...}}) =
length empty + Metis_LiteralNet.size unit + Metis_IntMap.size clauses;
-
+
fun insert (Metis_Subsume {empty,unit,nonunit}) (cl',a) =
case sortClause cl' of
[] =>
@@ -18286,7 +18759,7 @@
(* ========================================================================= *)
(* THE KNUTH-BENDIX TERM ORDERING *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_KnuthBendixOrder =
@@ -18311,7 +18784,7 @@
(* ========================================================================= *)
(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_KnuthBendixOrder :> Metis_KnuthBendixOrder =
@@ -18513,7 +18986,7 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Rewrite =
@@ -18615,7 +19088,7 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Rewrite :> Metis_Rewrite =
@@ -18834,7 +19307,7 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Rewriting (the order must be a refinement of the rewrite order). *)
+(* Rewriting (the supplied order must be a refinement of the rewrite order). *)
(* ------------------------------------------------------------------------- *)
local
@@ -18904,34 +19377,35 @@
end
end;
-datatype neqConvs = NeqConvs of Metis_Rule.conv Metis_LiteralMap.map;
-
-val neqConvsEmpty = NeqConvs (Metis_LiteralMap.new ());
-
-fun neqConvsNull (NeqConvs m) = Metis_LiteralMap.null m;
-
-fun neqConvsAdd order (neq as NeqConvs m) lit =
+datatype neqConvs = NeqConvs of Metis_Rule.conv list;
+
+val neqConvsEmpty = NeqConvs [];
+
+fun neqConvsNull (NeqConvs l) = List.null l;
+
+fun neqConvsAdd order (neq as NeqConvs l) lit =
case total (mkNeqConv order) lit of
- NONE => NONE
- | SOME conv => SOME (NeqConvs (Metis_LiteralMap.insert m (lit,conv)));
+ NONE => neq
+ | SOME conv => NeqConvs (conv :: l);
fun mkNeqConvs order =
let
- fun add (lit,(neq,lits)) =
- case neqConvsAdd order neq lit of
- SOME neq => (neq,lits)
- | NONE => (neq, Metis_LiteralSet.add lits lit)
- in
- Metis_LiteralSet.foldl add (neqConvsEmpty,Metis_LiteralSet.empty)
- end;
-
-fun neqConvsDelete (NeqConvs m) lit = NeqConvs (Metis_LiteralMap.delete m lit);
-
-fun neqConvsToConv (NeqConvs m) =
- Metis_Rule.firstConv (Metis_LiteralMap.foldr (fn (_,c,l) => c :: l) [] m);
-
-fun neqConvsFoldl f b (NeqConvs m) =
- Metis_LiteralMap.foldl (fn (l,_,z) => f (l,z)) b m;
+ fun add (lit,neq) = neqConvsAdd order neq lit
+ in
+ Metis_LiteralSet.foldl add neqConvsEmpty
+ end;
+
+fun buildNeqConvs order lits =
+ let
+ fun add (lit,(neq,neqs)) = (neqConvsAdd order neq lit, (lit,neq) :: neqs)
+ in
+ snd (Metis_LiteralSet.foldl add (neqConvsEmpty,[]) lits)
+ end;
+
+fun neqConvsToConv (NeqConvs l) = Metis_Rule.firstConv l;
+
+fun neqConvsUnion (NeqConvs l1) (NeqConvs l2) =
+ NeqConvs (List.revAppend (l1,l2));
fun neqConvsRewrIdLiterule order known redexes id neq =
if Metis_IntMap.null known andalso neqConvsNull neq then Metis_Rule.allLiterule
@@ -18947,7 +19421,7 @@
fun rewriteIdEqn' order known redexes id (eqn as (l_r,th)) =
let
- val (neq,_) = mkNeqConvs order (Metis_Thm.clause th)
+ val neq = mkNeqConvs order (Metis_Thm.clause th)
val literule = neqConvsRewrIdLiterule order known redexes id neq
val (strongEqn,lit) =
case Metis_Rule.equationLiteral eqn of
@@ -18970,40 +19444,39 @@
let
val mk_literule = neqConvsRewrIdLiterule order known redexes id
- fun rewr_neq_lit (lit, acc as (changed,neq,lits,th)) =
- let
- val neq = neqConvsDelete neq lit
+ fun rewr_neq_lit ((lit,rneq),(changed,lneq,lits,th)) =
+ let
+ val neq = neqConvsUnion lneq rneq
val (lit',litTh) = mk_literule neq lit
- in
- if Metis_Literal.equal lit lit' then acc
- else
- let
- val th = Metis_Thm.resolve lit th litTh
- in
- case neqConvsAdd order neq lit' of
- SOME neq => (true,neq,lits,th)
- | NONE => (changed, neq, Metis_LiteralSet.add lits lit', th)
- end
- end
-
- fun rewr_neq_lits neq lits th =
- let
+ val lneq = neqConvsAdd order lneq lit'
+ val lits = Metis_LiteralSet.add lits lit'
+ in
+ if Metis_Literal.equal lit lit' then (changed,lneq,lits,th)
+ else (true, lneq, lits, Metis_Thm.resolve lit th litTh)
+ end
+
+ fun rewr_neq_lits lits th =
+ let
+ val neqs = buildNeqConvs order lits
+
+ val neq = neqConvsEmpty
+ val lits = Metis_LiteralSet.empty
+
val (changed,neq,lits,th) =
- neqConvsFoldl rewr_neq_lit (false,neq,lits,th) neq
- in
- if changed then rewr_neq_lits neq lits th
- else (neq,lits,th)
- end
-
- val (neq,lits) = mkNeqConvs order lits
-
- val (neq,lits,th) = rewr_neq_lits neq lits th
+ List.foldl rewr_neq_lit (false,neq,lits,th) neqs
+ in
+ if changed then rewr_neq_lits lits th else (neq,th)
+ end
+
+ val (neq,lits) = Metis_LiteralSet.partition Metis_Literal.isNeq lits
+
+ val (neq,th) = rewr_neq_lits neq th
val rewr_literule = mk_literule neq
fun rewr_lit (lit,th) =
- if Metis_Thm.member lit th then Metis_Rule.literalRule rewr_literule lit th
- else th
+ if not (Metis_Thm.member lit th) then th
+ else Metis_Rule.literalRule rewr_literule lit th
in
Metis_LiteralSet.foldl rewr_lit th lits
end;
@@ -19021,12 +19494,12 @@
(*MetisTrace6
val () = Metis_Print.trace Metis_Thm.pp "Metis_Rewrite.rewriteIdRule': result" result
*)
- val _ = not (thmReducible order known id result) orelse
- raise Bug "rewriteIdRule: should be normalized"
+ val () = if not (thmReducible order known id result) then ()
+ else raise Bug "Metis_Rewrite.rewriteIdRule': should be normalized"
in
result
end
- handle Error err => raise Error ("Metis_Rewrite.rewriteIdRule:\n" ^ err);
+ handle Error err => raise Error ("Metis_Rewrite.rewriteIdRule':\n" ^ err);
*)
fun rewrIdConv (Metis_Rewrite {known,redexes,...}) order =
@@ -19048,6 +19521,30 @@
fun rewriteIdRule (Metis_Rewrite {known,redexes,...}) order =
rewriteIdRule' order known redexes;
+(*MetisDebug
+val rewriteIdRule = fn rewr => fn order => fn id => fn th =>
+ let
+ val result = rewriteIdRule rewr order id th
+
+ val th' = rewriteIdRule rewr order id result
+
+ val () = if Metis_Thm.equal th' result then ()
+ else
+ let
+ fun trace p s = Metis_Print.trace p ("Metis_Rewrite.rewriteIdRule: "^s)
+ val () = trace pp "rewr" rewr
+ val () = trace Metis_Thm.pp "th" th
+ val () = trace Metis_Thm.pp "result" result
+ val () = trace Metis_Thm.pp "th'" th'
+ in
+ raise Bug "Metis_Rewrite.rewriteIdRule: should be idempotent"
+ end
+ in
+ result
+ end
+ handle Error err => raise Error ("Metis_Rewrite.rewriteIdRule:\n" ^ err);
+*)
+
fun rewriteRule rewrite order = rewriteIdRule rewrite order ~1;
(* ------------------------------------------------------------------------- *)
@@ -19303,7 +19800,7 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Units =
@@ -19355,7 +19852,7 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Units :> Metis_Units =
@@ -19464,7 +19961,7 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Clause =
@@ -19574,7 +20071,7 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Clause :> Metis_Clause =
@@ -19792,38 +20289,43 @@
fun reduce units (Metis_Clause {parameters,id,thm}) =
Metis_Clause {parameters = parameters, id = id, thm = Metis_Units.reduce units thm};
-fun rewrite rewr (cl as Metis_Clause {parameters,id,thm}) =
- let
- fun simp th =
- let
- val {ordering,...} = parameters
- val cmp = Metis_KnuthBendixOrder.compare ordering
- in
- Metis_Rewrite.rewriteIdRule rewr cmp id th
- end
+local
+ fun simp rewr (parm : parameters) id th =
+ let
+ val {ordering,...} = parm
+ val cmp = Metis_KnuthBendixOrder.compare ordering
+ in
+ Metis_Rewrite.rewriteIdRule rewr cmp id th
+ end;
+in
+ fun rewrite rewr cl =
+ let
+ val Metis_Clause {parameters = parm, id, thm = th} = cl
(*MetisTrace4
- val () = Metis_Print.trace Metis_Rewrite.pp "Metis_Clause.rewrite: rewr" rewr
- val () = Metis_Print.trace Metis_Print.ppInt "Metis_Clause.rewrite: id" id
- val () = Metis_Print.trace pp "Metis_Clause.rewrite: cl" cl
-*)
-
- val thm =
- case Metis_Rewrite.peek rewr id of
- NONE => simp thm
- | SOME ((_,thm),_) => if Metis_Rewrite.isReduced rewr then thm else simp thm
-
- val result = Metis_Clause {parameters = parameters, id = id, thm = thm}
+ val () = Metis_Print.trace Metis_Rewrite.pp "Metis_Clause.rewrite: rewr" rewr
+ val () = Metis_Print.trace Metis_Print.ppInt "Metis_Clause.rewrite: id" id
+ val () = Metis_Print.trace pp "Metis_Clause.rewrite: cl" cl
+*)
+
+ val th =
+ case Metis_Rewrite.peek rewr id of
+ NONE => simp rewr parm id th
+ | SOME ((_,th),_) =>
+ if Metis_Rewrite.isReduced rewr then th else simp rewr parm id th
+
+ val result = Metis_Clause {parameters = parm, id = id, thm = th}
(*MetisTrace4
- val () = Metis_Print.trace pp "Metis_Clause.rewrite: result" result
-*)
- in
- result
- end
+ val () = Metis_Print.trace pp "Metis_Clause.rewrite: result" result
+*)
+ in
+ result
+ end
(*MetisDebug
- handle Error err => raise Error ("Metis_Clause.rewrite:\n" ^ err);
-*)
+ handle Error err => raise Error ("Metis_Clause.rewrite:\n" ^ err);
+*)
+end;
(* ------------------------------------------------------------------------- *)
(* Inference rules: these generate new clause ids. *)
@@ -19946,7 +20448,7 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Active =
@@ -20004,7 +20506,7 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Active :> Metis_Active =
@@ -20156,9 +20658,9 @@
let
fun simp cl =
case Metis_Clause.simplify cl of
- NONE => true
+ NONE => true (* tautology case *)
| SOME cl =>
- Metis_Subsume.isStrictlySubsumed subsume (Metis_Clause.literals cl) orelse
+ Metis_Subsume.isSubsumed subsume (Metis_Clause.literals cl) orelse
let
val cl' = cl
val cl' = Metis_Clause.reduce reduce cl'
@@ -20398,9 +20900,11 @@
(*MetisDebug
val simplify = fn simp => fn units => fn rewr => fn subs => fn cl =>
let
- fun traceCl s = Metis_Print.trace Metis_Clause.pp ("Metis_Active.simplify: " ^ s)
+ val ppClOpt = Metis_Print.ppOption Metis_Clause.pp
+ fun trace pp s = Metis_Print.trace pp ("Metis_Active.simplify: " ^ s)
+ val traceCl = trace Metis_Clause.pp
+ val traceClOpt = trace ppClOpt
(*MetisTrace4
- val ppClOpt = Metis_Print.ppOption Metis_Clause.pp
val () = traceCl "cl" cl
*)
val cl' = simplify simp units rewr subs cl
@@ -20420,8 +20924,14 @@
NONE => ()
| SOME (e,f) =>
let
+ val () = Metis_Print.trace Metis_Rewrite.pp "Metis_Active.simplify: rewr" rewr
+ val () = Metis_Print.trace Metis_Units.pp "Metis_Active.simplify: units" units
+ val () = Metis_Print.trace Metis_Subsume.pp "Metis_Active.simplify: subs" subs
val () = traceCl "cl" cl
val () = traceCl "cl'" cl'
+ val () = traceClOpt "simplify cl'" (Metis_Clause.simplify cl')
+ val () = traceCl "rewrite cl'" (Metis_Clause.rewrite rewr cl')
+ val () = traceCl "reduce cl'" (Metis_Clause.reduce units cl')
val () = f ()
in
raise
@@ -20820,34 +21330,42 @@
sortMap utility Int.compare
end;
- fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) =
+ fun post_factor (cl, active_subsume_acc as (active,subsume,acc)) =
case postfactor_simplify active subsume cl of
NONE => active_subsume_acc
- | SOME cl =>
- let
- val active = addFactorClause active cl
- and subsume = addSubsume subsume cl
- and acc = cl :: acc
- in
- (active,subsume,acc)
- end;
-
- fun factor1 (cl, active_subsume_acc as (active,subsume,_)) =
+ | SOME cl' =>
+ if Metis_Clause.equalThms cl' cl then
+ let
+ val active = addFactorClause active cl
+ and subsume = addSubsume subsume cl
+ and acc = cl :: acc
+ in
+ (active,subsume,acc)
+ end
+ else
+ (* If the clause was changed in the post-factor simplification *)
+ (* step, then it may have altered the set of largest literals *)
+ (* in the clause. The safest thing to do is to factor again. *)
+ factor1 cl' active_subsume_acc
+
+ and factor1 cl active_subsume_acc =
+ let
+ val cls = sort_utilitywise (cl :: Metis_Clause.factor cl)
+ in
+ List.foldl post_factor active_subsume_acc cls
+ end;
+
+ fun pre_factor (cl, active_subsume_acc as (active,subsume,_)) =
case prefactor_simplify active subsume cl of
NONE => active_subsume_acc
- | SOME cl =>
- let
- val cls = sort_utilitywise (cl :: Metis_Clause.factor cl)
- in
- List.foldl factor_add active_subsume_acc cls
- end;
+ | SOME cl => factor1 cl active_subsume_acc;
fun factor' active acc [] = (active, List.rev acc)
| factor' active acc cls =
let
val cls = sort_utilitywise cls
val subsume = getSubsume active
- val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls
+ val (active,_,acc) = List.foldl pre_factor (active,subsume,acc) cls
val (active,cls) = extract_rewritables active
in
factor' active acc cls
@@ -20919,7 +21437,7 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Waiting =
@@ -20999,7 +21517,7 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Waiting :> Metis_Waiting =
@@ -21293,7 +21811,7 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Resolution =
@@ -21347,7 +21865,7 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Resolution :> Metis_Resolution =