# HG changeset patch # User desharna # Date 1594287556 -7200 # Node ID 913162a47d9fedff5262e1f6d084cbda43416283 # Parent a7e6ac2dfa58c431d9d8348c6719063ddb6a14d5 Update Metis to 2.4 diff -r a7e6ac2dfa58 -r 913162a47d9f CONTRIBUTORS --- a/CONTRIBUTORS Wed Jul 08 16:35:23 2020 +0200 +++ b/CONTRIBUTORS Thu Jul 09 11:39:16 2020 +0200 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* July 2020: Martin Desharnais + Integration of Metis 2.4. + * June 2020: Makarius Wenzel System option pide_session is enabled by default, notably for standard "isabelle build" to invoke Scala from ML. diff -r a7e6ac2dfa58 -r 913162a47d9f NEWS --- a/NEWS Wed Jul 08 16:35:23 2020 +0200 +++ b/NEWS Thu Jul 09 11:39:16 2020 +0200 @@ -48,6 +48,10 @@ * For the natural numbers, Sup {} = 0. +* Updated the Metis prover underlying the "metis" proof method to + version 2.4 (release 20180810). The new version fixes one soundness + defect and two incompleteness defects. Very slight INCOMPATIBILITY. + * Library theory "Bit_Operations" with generic bit operations. * Session HOL-Word: Type word is restricted to bit strings consisting diff -r a7e6ac2dfa58 -r 913162a47d9f src/HOL/Algebra/Polynomial_Divisibility.thy --- a/src/HOL/Algebra/Polynomial_Divisibility.thy Wed Jul 08 16:35:23 2020 +0200 +++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Thu Jul 09 11:39:16 2020 +0200 @@ -950,7 +950,7 @@ from \degree p = 1\ have "length p = Suc (Suc 0)" by simp then obtain a b where p: "p = [ a, b ]" - by (metis length_0_conv length_Suc_conv) + by (metis length_0_conv length_Cons nat.inject neq_Nil_conv) with \p \ carrier (K[X])\ show ?thesis using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b] subfield.subfield_Units[OF assms(1)] diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/Makefile --- a/src/Tools/Metis/Makefile Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/Makefile Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ ############################################################################### # METIS MAKEFILE -# Copyright (c) 2001 Joe Hurd, distributed under the BSD License +# Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License ############################################################################### .SUFFIXES: @@ -10,26 +10,27 @@ ############################################################################### .PHONY: default -default: mosml +default: + @if command -v mlton > /dev/null ; then $(MAKE) mlton ; else if command -v polyc > /dev/null ; then $(MAKE) polyml ; else if command -v mosmlc > /dev/null ; then $(MAKE) mosml ; else echo "ERROR: No ML found on path: install either MLton, Poly/ML or Moscow ML." ; exit 1 ; fi ; fi ; fi ############################################################################### # Cleaning temporary files. ############################################################################### TEMP = \ - $(MOSML_TARGETS) \ - bin/mosml/*.sml bin/mosml/*.ui bin/mosml/*.uo bin/mosml/a.out \ $(MLTON_TARGETS) \ bin/mlton/*.sml bin/mlton/*.mlb \ $(POLYML_TARGETS) \ - bin/polyml/*.sml bin/polyml/*.log bin/polyml/*.o + bin/polyml/*.sml bin/polyml/*.log \ + $(MOSML_TARGETS) \ + bin/mosml/*.sml bin/mosml/*.ui bin/mosml/*.uo bin/mosml/a.out .PHONY: clean clean: @echo - @echo '********************' - @echo '* Clean everything *' - @echo '********************' + @echo '+------------------+' + @echo '| Clean everything |' + @echo '+------------------+' @echo rm -f $(TEMP) $(MAKE) -C test $@ @@ -98,6 +99,97 @@ MLPP_OPTS = ############################################################################### +# Building using MLton. +############################################################################### + +MLTON = mlton + +MLTON_OPTS = -runtime 'ram-slop 0.4' + +MLTON_SRC = \ + src/Portable.sig src/PortableMlton.sml \ + $(SRC) + +MLTON_TARGETS = \ + bin/mlton/selftest \ + bin/mlton/metis \ + bin/mlton/problems2tptp + +bin/mlton/%.sml: $(MLTON_SRC) src/%.sml + @$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@ + +bin/mlton/%.mlb: bin/mlton/%.sml + echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@ + +bin/mlton/%: bin/mlton/%.mlb + @echo + @echo '+-------------------------+' + @echo '| Compile a MLton program |' + @echo '+-------------------------+' + @echo + @echo $@ + cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<) + @echo + +.PHONY: mlton-info +mlton-info: + @echo + @echo '+-----------------------------------+' + @echo '| Build and test the MLton programs |' + @echo '+-----------------------------------+' + @echo + +.PHONY: mlton +mlton: mlton-info $(MLTON_TARGETS) + $(MAKE) -C test mlton + +############################################################################### +# Building using Poly/ML. +############################################################################### + +POLYML = polyc + +POLYML_OPTS = + +POLYML_SRC = \ + src/Random.sig src/Random.sml \ + src/Portable.sig src/PortablePolyml.sml \ + $(SRC) + +POLYML_TARGETS = \ + bin/polyml/selftest \ + bin/polyml/problems2tptp \ + bin/polyml/metis + +bin/polyml/%.sml: src/%.sml $(POLYML_SRC) + @$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@ + @echo 'fun main () = let' >> $@ + @$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@ + @echo "in () end handle e => (TextIO.output (TextIO.stdErr, \"FATAL EXCEPTION:\\\\n\"^ exnMessage e); OS.Process.exit OS.Process.failure);" >> $@ + +bin/polyml/%: bin/polyml/%.sml + @echo + @echo '+---------------------------+' + @echo '| Compile a Poly/ML program |' + @echo '+---------------------------+' + @echo + @echo $@ + cd bin/polyml && $(POLYML) $(POLYML_OPTS) -o $(notdir $@) $(notdir $<) + @echo + +.PHONY: polyml-info +polyml-info: + @echo + @echo '+-------------------------------------+' + @echo '| Build and test the Poly/ML programs |' + @echo '+-------------------------------------+' + @echo + +.PHONY: polyml +polyml: polyml-info $(POLYML_TARGETS) + $(MAKE) -C test polyml + +############################################################################### # Building using Moscow ML. ############################################################################### @@ -116,120 +208,15 @@ .PHONY: mosml-info mosml-info: @echo - @echo '*****************************************' - @echo '* Build and test the Moscow ML programs *' - @echo '*****************************************' + @echo '+---------------------------------------+' + @echo '| Build and test the Moscow ML programs |' + @echo '+---------------------------------------+' @echo .PHONY: mosml mosml: mosml-info $(MOSML_OBJ) $(MOSML_TARGETS) test ############################################################################### -# Building using MLton. -############################################################################### - -MLTON = mlton - -MLTON_OPTS = -runtime 'ram-slop 0.4' - -MLTON_SRC = \ - src/Portable.sig src/PortableMlton.sml \ - $(SRC) - -METIS = bin/mlton/metis - -PROBLEMS2TPTP = bin/mlton/problems2tptp - -MLTON_TARGETS = \ - bin/mlton/selftest \ - $(METIS) \ - $(PROBLEMS2TPTP) - -bin/mlton/%.sml: $(MLTON_SRC) src/%.sml - @$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@ - -bin/mlton/%.mlb: bin/mlton/%.sml - echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@ - -bin/mlton/%: bin/mlton/%.mlb - @echo - @echo '***************************' - @echo '* Compile a MLton program *' - @echo '***************************' - @echo - @echo $@ - cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<) - @echo - -.PHONY: mlton-info -mlton-info: - @echo - @echo '*************************************' - @echo '* Build and test the MLton programs *' - @echo '*************************************' - @echo - -.PHONY: mlton -mlton: mlton-info $(MLTON_TARGETS) - $(MAKE) -C test mlton - -############################################################################### -# Building using Poly/ML. -############################################################################### - -POLYML = poly - -POLYML_OPTS = - -ifeq ($(shell uname), Darwin) - POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx -else - POLYML_LINK_OPTS = -lpolymain -lpolyml -endif - -POLYML_SRC = \ - src/Random.sig src/Random.sml \ - src/Portable.sig src/PortablePolyml.sml \ - $(SRC) - -POLYML_TARGETS = \ - bin/polyml/selftest \ - bin/polyml/problems2tptp \ - bin/polyml/metis - -bin/polyml/%.sml: src/%.sml $(POLYML_SRC) - @$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@ - @echo 'fun main () = let' >> $@ - @$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@ - @echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@ - -bin/polyml/%.o: bin/polyml/%.sml - cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS) > $(basename $(notdir $<)).log - @if test $@ -nt $< ; then echo 'compiled $@' ; else cat bin/polyml/$(basename $(notdir $<)).log ; exit 1 ; fi - -bin/polyml/%: bin/polyml/%.o - @echo - @echo '*****************************' - @echo '* Compile a Poly/ML program *' - @echo '*****************************' - @echo - @echo $@ - cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS) - @echo - -.PHONY: polyml-info -polyml-info: - @echo - @echo '***************************************' - @echo '* Build and test the Poly/ML programs *' - @echo '***************************************' - @echo - -.PHONY: polyml -polyml: polyml-info $(POLYML_TARGETS) - $(MAKE) -C test polyml - -############################################################################### # Development. ############################################################################## diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/README --- a/src/Tools/Metis/README Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/README Thu Jul 09 11:39:16 2020 +0200 @@ -4,15 +4,16 @@ for Metis with the latest Metis package. 1. The files "Makefile" and "script/mlpp" and the directory "src/" - must reflect the corresponding files in Joe Hurd's official Metis - package. The package that was used when these notes where written - was Metis 2.3 (release 20110926). + must reflect the corresponding files in Joe Leslie-Hurd's official + Metis package. The package that was used when these notes where + written was Metis 2.3 (release 20110926). The package was later + updated to Metis 2.4 (release 20180810). 2. The license in each source file will probably not be something we can use in Isabelle. The "fix_metis_license" script can be run to replace all occurrences of "MIT license" with "BSD License". In a - 13 Sept. 2010 email to Gerwin Klein, Joe Hurd, the sole copyright - holder of Metis, wrote: + 13 Sept. 2010 email to Gerwin Klein, Joe Leslie-Hurd, the sole + copyright holder of Metis, wrote: I hereby give permission to the Isabelle team to release Metis as part of Isabelle, with the Metis code covered under the @@ -46,5 +47,11 @@ Good luck! + Jasmin Blanchette 1 December 2011 + +Updated by + + Martin Desharnais + 9 July 2020 diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/make_metis --- a/src/Tools/Metis/make_metis Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/make_metis Thu Jul 09 11:39:16 2020 +0200 @@ -14,8 +14,8 @@ cat < 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 = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/scripts/mlpp --- a/src/Tools/Metis/scripts/mlpp Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/scripts/mlpp Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ #!/usr/bin/perl -# Copyright (c) 2006 Joe Hurd, distributed under the BSD License +# Copyright (c) 2006 Joe Leslie-Hurd, distributed under the BSD License use strict; use warnings; @@ -72,19 +72,7 @@ my $text = shift @_; if ($opt_c eq "mosml") { - $text =~ s/Array\.copy/Array_copy/g; - $text =~ s/Array\.foldli/Array_foldli/g; - $text =~ s/Array\.foldri/Array_foldri/g; - $text =~ s/Array\.modifyi/Array_modifyi/g; - $text =~ s/OS\.Process\.isSuccess/OS_Process_isSuccess/g; - $text =~ s/PP\.ppstream/ppstream/g; - $text =~ s/String\.concatWith/String_concatWith/g; - $text =~ s/String\.isSubstring/String_isSubstring/g; - $text =~ s/String\.isSuffix/String_isSuffix/g; - $text =~ s/Substring\.full/Substring_full/g; - $text =~ s/TextIO\.inputLine/TextIO_inputLine/g; - $text =~ s/Vector\.foldli/Vector_foldli/g; - $text =~ s/Vector\.mapi/Vector_mapi/g; + $text =~ s/Real\.isFinite/Real_isFinite/g; } print STDOUT $text; @@ -300,7 +288,7 @@ =head1 AUTHORS -Joe Hurd +Joe Leslie-Hurd =head1 SEE ALSO diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Active.sig --- a/src/Tools/Metis/src/Active.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Active.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Active = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Active.sml --- a/src/Tools/Metis/src/Active.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Active.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Active :> Active = @@ -152,9 +152,9 @@ let fun simp cl = case Clause.simplify cl of - NONE => true + NONE => true (* tautology case *) | SOME cl => - Subsume.isStrictlySubsumed subsume (Clause.literals cl) orelse + Subsume.isSubsumed subsume (Clause.literals cl) orelse let val cl' = cl val cl' = Clause.reduce reduce cl' @@ -394,9 +394,11 @@ (*MetisDebug val simplify = fn simp => fn units => fn rewr => fn subs => fn cl => let - fun traceCl s = Print.trace Clause.pp ("Active.simplify: " ^ s) + val ppClOpt = Print.ppOption Clause.pp + fun trace pp s = Print.trace pp ("Active.simplify: " ^ s) + val traceCl = trace Clause.pp + val traceClOpt = trace ppClOpt (*MetisTrace4 - val ppClOpt = Print.ppOption Clause.pp val () = traceCl "cl" cl *) val cl' = simplify simp units rewr subs cl @@ -416,8 +418,14 @@ NONE => () | SOME (e,f) => let + val () = Print.trace Rewrite.pp "Active.simplify: rewr" rewr + val () = Print.trace Units.pp "Active.simplify: units" units + val () = Print.trace Subsume.pp "Active.simplify: subs" subs val () = traceCl "cl" cl val () = traceCl "cl'" cl' + val () = traceClOpt "simplify cl'" (Clause.simplify cl') + val () = traceCl "rewrite cl'" (Clause.rewrite rewr cl') + val () = traceCl "reduce cl'" (Clause.reduce units cl') val () = f () in raise @@ -816,34 +824,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; + | SOME cl' => + if 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 - fun factor1 (cl, active_subsume_acc as (active,subsume,_)) = + and factor1 cl active_subsume_acc = + let + val cls = sort_utilitywise (cl :: 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 :: 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 diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Atom.sig --- a/src/Tools/Metis/src/Atom.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Atom.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Atom = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Atom.sml --- a/src/Tools/Metis/src/Atom.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Atom.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Atom :> Atom = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/AtomNet.sig --- a/src/Tools/Metis/src/AtomNet.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/AtomNet.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 AtomNet = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/AtomNet.sml --- a/src/Tools/Metis/src/AtomNet.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/AtomNet.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 AtomNet :> AtomNet = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Clause.sig --- a/src/Tools/Metis/src/Clause.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Clause.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Clause = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Clause.sml --- a/src/Tools/Metis/src/Clause.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Clause.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Clause :> Clause = @@ -218,38 +218,43 @@ fun reduce units (Clause {parameters,id,thm}) = Clause {parameters = parameters, id = id, thm = Units.reduce units thm}; -fun rewrite rewr (cl as Clause {parameters,id,thm}) = - let - fun simp th = - let - val {ordering,...} = parameters - val cmp = KnuthBendixOrder.compare ordering - in - Rewrite.rewriteIdRule rewr cmp id th - end +local + fun simp rewr (parm : parameters) id th = + let + val {ordering,...} = parm + val cmp = KnuthBendixOrder.compare ordering + in + Rewrite.rewriteIdRule rewr cmp id th + end; +in + fun rewrite rewr cl = + let + val Clause {parameters = parm, id, thm = th} = cl (*MetisTrace4 - val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr - val () = Print.trace Print.ppInt "Clause.rewrite: id" id - val () = Print.trace pp "Clause.rewrite: cl" cl + val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr + val () = Print.trace Print.ppInt "Clause.rewrite: id" id + val () = Print.trace pp "Clause.rewrite: cl" cl *) - val thm = - case Rewrite.peek rewr id of - NONE => simp thm - | SOME ((_,thm),_) => if Rewrite.isReduced rewr then thm else simp thm + val th = + case Rewrite.peek rewr id of + NONE => simp rewr parm id th + | SOME ((_,th),_) => + if Rewrite.isReduced rewr then th else simp rewr parm id th - val result = Clause {parameters = parameters, id = id, thm = thm} + val result = Clause {parameters = parm, id = id, thm = th} (*MetisTrace4 - val () = Print.trace pp "Clause.rewrite: result" result + val () = Print.trace pp "Clause.rewrite: result" result *) - in - result - end + in + result + end (*MetisDebug - handle Error err => raise Error ("Clause.rewrite:\n" ^ err); + handle Error err => raise Error ("Clause.rewrite:\n" ^ err); *) +end; (* ------------------------------------------------------------------------- *) (* Inference rules: these generate new clause ids. *) diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/ElementSet.sig --- a/src/Tools/Metis/src/ElementSet.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/ElementSet.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 ElementSet = @@ -135,9 +135,11 @@ val disjoint : set -> set -> bool (* ------------------------------------------------------------------------- *) -(* Closing under an operation. *) +(* Pointwise operations. *) (* ------------------------------------------------------------------------- *) +val lift : (element -> set) -> set -> set + val closedAdd : (element -> set) -> set -> set -> set val close : (element -> set) -> set -> set @@ -165,6 +167,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. *) (* ------------------------------------------------------------------------- *) diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/ElementSet.sml --- a/src/Tools/Metis/src/ElementSet.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/ElementSet.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 ElementSet ( @@ -302,9 +302,16 @@ fun disjoint (Set m1) (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 fun adds acc set = foldl check acc set @@ -336,6 +343,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 + 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 Useful.Bug "ElementSet.preOrder: missing roots" + + val () = + if preOrdered children l then () + else raise Useful.Bug "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 Useful.Bug "ElementSet.postOrder: missing roots" + + val () = + if postOrdered children l then () + else raise Useful.Bug "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 Useful.Bug "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 Useful.Bug "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 Useful.Bug "ElementSet.preOrderSCC: missing roots" + + val () = + if preOrderedSCC children result then () + else raise Useful.Bug "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 Useful.Bug "ElementSet.postOrderSCC: missing roots" + + val () = + if postOrderedSCC children result then () + else raise Useful.Bug "ElementSet.postOrderSCC: bad ordering" +*) + in + result + end; +end; + +(* ------------------------------------------------------------------------- *) (* Pretty-printing. *) (* ------------------------------------------------------------------------- *) diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Formula.sig --- a/src/Tools/Metis/src/Formula.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Formula.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Formula = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Formula.sml --- a/src/Tools/Metis/src/Formula.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Formula.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Formula :> Formula = @@ -572,7 +572,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)]; diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Heap.sig --- a/src/Tools/Metis/src/Heap.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Heap.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Heap = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Heap.sml --- a/src/Tools/Metis/src/Heap.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Heap.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Heap :> Heap = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/KeyMap.sig --- a/src/Tools/Metis/src/KeyMap.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/KeyMap.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 KeyMap = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/KeyMap.sml --- a/src/Tools/Metis/src/KeyMap.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/KeyMap.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 KeyMap (Key : Ordered) :> KeyMap where type key = Key.t = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/KnuthBendixOrder.sig --- a/src/Tools/Metis/src/KnuthBendixOrder.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/KnuthBendixOrder.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 KnuthBendixOrder = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/KnuthBendixOrder.sml --- a/src/Tools/Metis/src/KnuthBendixOrder.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 KnuthBendixOrder :> KnuthBendixOrder = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Lazy.sig --- a/src/Tools/Metis/src/Lazy.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Lazy.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Lazy = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Lazy.sml --- a/src/Tools/Metis/src/Lazy.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Lazy.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Lazy :> Lazy = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Literal.sig --- a/src/Tools/Metis/src/Literal.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Literal.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Literal = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Literal.sml --- a/src/Tools/Metis/src/Literal.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Literal.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Literal :> Literal = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/LiteralNet.sig --- a/src/Tools/Metis/src/LiteralNet.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/LiteralNet.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 LiteralNet = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/LiteralNet.sml --- a/src/Tools/Metis/src/LiteralNet.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/LiteralNet.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 LiteralNet :> LiteralNet = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Map.sig --- a/src/Tools/Metis/src/Map.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Map.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Map = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Map.sml --- a/src/Tools/Metis/src/Map.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Map.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Map :> Map = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Model.sig --- a/src/Tools/Metis/src/Model.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Model.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Model = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Model.sml --- a/src/Tools/Metis/src/Model.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Model.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Model :> Model = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Name.sig --- a/src/Tools/Metis/src/Name.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Name.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* NAMES *) -(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Name = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Name.sml --- a/src/Tools/Metis/src/Name.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Name.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* NAMES *) -(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Name :> Name = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/NameArity.sig --- a/src/Tools/Metis/src/NameArity.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/NameArity.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 NameArity = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/NameArity.sml --- a/src/Tools/Metis/src/NameArity.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/NameArity.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 NameArity :> NameArity = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Normalize.sig --- a/src/Tools/Metis/src/Normalize.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Normalize.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* NORMALIZING FORMULAS *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Normalize = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Normalize.sml --- a/src/Tools/Metis/src/Normalize.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Normalize.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* NORMALIZING FORMULAS *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Normalize :> Normalize = @@ -648,14 +648,24 @@ | Literal (_,lit) => Literal.toFormula lit | And (_,_,s) => Formula.listMkConj (Set.transform form s) | Or (_,_,s) => Formula.listMkDisj (Set.transform form s) - | Xor (_,_,p,s) => - let - val s = if p then negateLastElt s else s - in - Formula.listMkEquiv (Set.transform form s) - end + | Xor (_,_,p,s) => xorForm p s | Exists (_,_,n,f) => Formula.listMkExists (NameSet.toList n, form f) - | Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f); + | Forall (_,_,n,f) => Formula.listMkForall (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 Set.size s mod 2 = 0 then not p else p + val s = if p then s else negateLastElt s + in + Formula.listMkEquiv (Set.transform form s) + end; in val toFormula = form; end; diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Options.sig --- a/src/Tools/Metis/src/Options.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Options.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* PROCESSING COMMAND LINE OPTIONS *) -(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Options = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Options.sml --- a/src/Tools/Metis/src/Options.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Options.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* PROCESSING COMMAND LINE OPTIONS *) -(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Options :> Options = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Ordered.sig --- a/src/Tools/Metis/src/Ordered.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Ordered.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* ORDERED TYPES *) -(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Ordered = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Ordered.sml --- a/src/Tools/Metis/src/Ordered.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Ordered.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* ORDERED TYPES *) -(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure IntOrdered = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Parse.sig --- a/src/Tools/Metis/src/Parse.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Parse.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* PARSING *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Parse = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Parse.sml --- a/src/Tools/Metis/src/Parse.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Parse.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* PARSING *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Parse :> Parse = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Portable.sig --- a/src/Tools/Metis/src/Portable.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Portable.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Portable = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/PortableMlton.sml --- a/src/Tools/Metis/src/PortableMlton.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/PortableMlton.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* MLTON SPECIFIC FUNCTIONS *) -(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Portable :> Portable = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/PortableMosml.sml --- a/src/Tools/Metis/src/PortableMosml.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/PortableMosml.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* MOSCOW ML SPECIFIC FUNCTIONS *) -(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Portable :> Portable = @@ -85,99 +85,4 @@ (* Ad-hoc upgrading of the Moscow ML basis library. *) (* ------------------------------------------------------------------------- *) -fun Array_copy {src,dst,di} = - let - open Array - in - copy {src = src, si = 0, len = NONE, dst = dst, di = di} - end; - -fun Array_foldli f b v = - let - open Array - in - foldli f b (v,0,NONE) - end; - -fun Array_foldri f b v = - let - open Array - in - foldri f b (v,0,NONE) - end; - -fun Array_modifyi f a = - let - open Array - in - modifyi f (a,0,NONE) - end; - -fun OS_Process_isSuccess s = s = OS.Process.success; - -fun String_concatWith s = - let - fun add (x,l) = s :: x :: l - in - fn [] => "" - | x :: xs => - let - val xs = List.foldl add [] (List.rev xs) - in - String.concat (x :: xs) - end - end; - -fun String_isSubstring p s = - let - val sizeP = size p - and sizeS = size s - in - if sizeP > sizeS then false - else if sizeP = sizeS then p = s - else - let - fun check i = String.substring (s,i,sizeP) = p - - fun checkn i = check i orelse (i > 0 andalso checkn (i - 1)) - in - checkn (sizeS - sizeP) - end - end; - -fun String_isSuffix p s = - let - val sizeP = size p - and sizeS = size s - in - sizeP <= sizeS andalso - String.extract (s, sizeS - sizeP, NONE) = p - end; - -fun Substring_full s = - let - open Substring - in - all s - end; - -fun TextIO_inputLine h = - let - open TextIO - in - case inputLine h of "" => NONE | s => SOME s - end; - -fun Vector_foldli f b v = - let - open Vector - in - foldli f b (v,0,NONE) - end; - -fun Vector_mapi f v = - let - open Vector - in - mapi f (v,0,NONE) - end; +fun Real_isFinite (_ : real) = true; diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/PortablePolyml.sml --- a/src/Tools/Metis/src/PortablePolyml.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/PortablePolyml.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* POLY/ML SPECIFIC FUNCTIONS *) -(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Portable :> Portable = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Print.sig --- a/src/Tools/Metis/src/Print.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Print.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* PRETTY-PRINTING *) -(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Print = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Print.sml --- a/src/Tools/Metis/src/Print.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Print.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* PRETTY-PRINTING *) -(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Print :> Print = @@ -1548,11 +1548,16 @@ toStreamWithLineLength len ppA a end; -local - val sep = mkWord " ="; -in - fun trace ppX nameX x = - 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 => Useful.trace (toString ppNameX x ^ "\n") + end; end diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Problem.sig --- a/src/Tools/Metis/src/Problem.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Problem.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* CNF PROBLEMS *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Problem = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Problem.sml --- a/src/Tools/Metis/src/Problem.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Problem.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* CNF PROBLEMS *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Problem :> Problem = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Proof.sig --- a/src/Tools/Metis/src/Proof.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Proof.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Proof = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Proof.sml --- a/src/Tools/Metis/src/Proof.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Proof.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Proof :> Proof = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Resolution.sig --- a/src/Tools/Metis/src/Resolution.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Resolution.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Resolution = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Resolution.sml --- a/src/Tools/Metis/src/Resolution.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Resolution.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Resolution :> Resolution = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Rewrite.sig --- a/src/Tools/Metis/src/Rewrite.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Rewrite.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Rewrite = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Rewrite.sml --- a/src/Tools/Metis/src/Rewrite.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Rewrite.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Rewrite :> Rewrite = @@ -219,7 +219,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 @@ -289,34 +289,35 @@ end end; -datatype neqConvs = NeqConvs of Rule.conv LiteralMap.map; +datatype neqConvs = NeqConvs of Rule.conv list; -val neqConvsEmpty = NeqConvs (LiteralMap.new ()); +val neqConvsEmpty = NeqConvs []; -fun neqConvsNull (NeqConvs m) = LiteralMap.null m; +fun neqConvsNull (NeqConvs l) = List.null l; -fun neqConvsAdd order (neq as NeqConvs m) lit = +fun neqConvsAdd order (neq as NeqConvs l) lit = case total (mkNeqConv order) lit of - NONE => NONE - | SOME conv => SOME (NeqConvs (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, LiteralSet.add lits lit) + fun add (lit,neq) = neqConvsAdd order neq lit in - LiteralSet.foldl add (neqConvsEmpty,LiteralSet.empty) + LiteralSet.foldl add neqConvsEmpty end; -fun neqConvsDelete (NeqConvs m) lit = NeqConvs (LiteralMap.delete m lit); +fun buildNeqConvs order lits = + let + fun add (lit,(neq,neqs)) = (neqConvsAdd order neq lit, (lit,neq) :: neqs) + in + snd (LiteralSet.foldl add (neqConvsEmpty,[]) lits) + end; -fun neqConvsToConv (NeqConvs m) = - Rule.firstConv (LiteralMap.foldr (fn (_,c,l) => c :: l) [] m); +fun neqConvsToConv (NeqConvs l) = Rule.firstConv l; -fun neqConvsFoldl f b (NeqConvs m) = - LiteralMap.foldl (fn (l,_,z) => f (l,z)) b m; +fun neqConvsUnion (NeqConvs l1) (NeqConvs l2) = + NeqConvs (List.revAppend (l1,l2)); fun neqConvsRewrIdLiterule order known redexes id neq = if IntMap.null known andalso neqConvsNull neq then Rule.allLiterule @@ -332,7 +333,7 @@ fun rewriteIdEqn' order known redexes id (eqn as (l_r,th)) = let - val (neq,_) = mkNeqConvs order (Thm.clause th) + val neq = mkNeqConvs order (Thm.clause th) val literule = neqConvsRewrIdLiterule order known redexes id neq val (strongEqn,lit) = case Rule.equationLiteral eqn of @@ -355,40 +356,39 @@ let val mk_literule = neqConvsRewrIdLiterule order known redexes id - fun rewr_neq_lit (lit, acc as (changed,neq,lits,th)) = + fun rewr_neq_lit ((lit,rneq),(changed,lneq,lits,th)) = let - val neq = neqConvsDelete neq lit + val neq = neqConvsUnion lneq rneq val (lit',litTh) = mk_literule neq lit + val lneq = neqConvsAdd order lneq lit' + val lits = LiteralSet.add lits lit' in - if Literal.equal lit lit' then acc - else - let - val th = Thm.resolve lit th litTh - in - case neqConvsAdd order neq lit' of - SOME neq => (true,neq,lits,th) - | NONE => (changed, neq, LiteralSet.add lits lit', th) - end + if Literal.equal lit lit' then (changed,lneq,lits,th) + else (true, lneq, lits, Thm.resolve lit th litTh) end - fun rewr_neq_lits neq lits th = + fun rewr_neq_lits lits th = let + val neqs = buildNeqConvs order lits + + val neq = neqConvsEmpty + val lits = LiteralSet.empty + val (changed,neq,lits,th) = - neqConvsFoldl rewr_neq_lit (false,neq,lits,th) neq + List.foldl rewr_neq_lit (false,neq,lits,th) neqs in - if changed then rewr_neq_lits neq lits th - else (neq,lits,th) + if changed then rewr_neq_lits lits th else (neq,th) end - val (neq,lits) = mkNeqConvs order lits + val (neq,lits) = LiteralSet.partition Literal.isNeq lits - val (neq,lits,th) = rewr_neq_lits neq lits th + val (neq,th) = rewr_neq_lits neq th val rewr_literule = mk_literule neq fun rewr_lit (lit,th) = - if Thm.member lit th then Rule.literalRule rewr_literule lit th - else th + if not (Thm.member lit th) then th + else Rule.literalRule rewr_literule lit th in LiteralSet.foldl rewr_lit th lits end; @@ -406,12 +406,12 @@ (*MetisTrace6 val () = Print.trace Thm.pp "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 "Rewrite.rewriteIdRule': should be normalized" in result end - handle Error err => raise Error ("Rewrite.rewriteIdRule:\n" ^ err); + handle Error err => raise Error ("Rewrite.rewriteIdRule':\n" ^ err); *) fun rewrIdConv (Rewrite {known,redexes,...}) order = @@ -433,6 +433,30 @@ fun rewriteIdRule (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 Thm.equal th' result then () + else + let + fun trace p s = Print.trace p ("Rewrite.rewriteIdRule: "^s) + val () = trace pp "rewr" rewr + val () = trace Thm.pp "th" th + val () = trace Thm.pp "result" result + val () = trace Thm.pp "th'" th' + in + raise Bug "Rewrite.rewriteIdRule: should be idempotent" + end + in + result + end + handle Error err => raise Error ("Rewrite.rewriteIdRule:\n" ^ err); +*) + fun rewriteRule rewrite order = rewriteIdRule rewrite order ~1; (* ------------------------------------------------------------------------- *) diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Rule.sig --- a/src/Tools/Metis/src/Rule.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Rule.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Rule = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Rule.sml --- a/src/Tools/Metis/src/Rule.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Rule.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Rule :> Rule = @@ -778,7 +778,7 @@ fun factor th = let - fun fact sub = removeSym (Thm.subst sub th) + fun fact sub = removeIrrefl (removeSym (Thm.subst sub th)) in List.map fact (factor' (Thm.clause th)) end; diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Set.sig --- a/src/Tools/Metis/src/Set.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Set.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Set = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Set.sml --- a/src/Tools/Metis/src/Set.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Set.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Set :> Set = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Sharing.sig --- a/src/Tools/Metis/src/Sharing.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Sharing.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Sharing = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Sharing.sml --- a/src/Tools/Metis/src/Sharing.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Sharing.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Sharing :> Sharing = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Stream.sig --- a/src/Tools/Metis/src/Stream.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Stream.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Stream = @@ -56,6 +56,8 @@ val drop : int -> 'a stream -> 'a stream (* raises Subscript *) +val unfold : ('b -> ('a * 'b) option) -> 'b -> 'a stream + (* ------------------------------------------------------------------------- *) (* Stream versions of standard list operations: these might not terminate. *) (* ------------------------------------------------------------------------- *) @@ -88,6 +90,8 @@ (* Stream operations. *) (* ------------------------------------------------------------------------- *) +val primes : int stream + val memoize : 'a stream -> 'a stream val listConcat : 'a list stream -> 'a stream diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Stream.sml --- a/src/Tools/Metis/src/Stream.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Stream.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Stream :> Stream = @@ -92,6 +92,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; + (* ------------------------------------------------------------------------- *) (* Stream versions of standard list operations: these might not terminate. *) (* ------------------------------------------------------------------------- *) @@ -181,6 +191,13 @@ (* Stream operations. *) (* ------------------------------------------------------------------------- *) +val primes = + let + fun next s = SOME (Useful.nextSieve s) + in + unfold next Useful.initSieve + end; + fun memoize Nil = Nil | memoize (Cons (h,t)) = Cons (h, Lazy.memoize (fn () => memoize (t ()))); diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Subst.sig --- a/src/Tools/Metis/src/Subst.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Subst.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Subst = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Subst.sml --- a/src/Tools/Metis/src/Subst.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Subst.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Subst :> Subst = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Subsume.sig --- a/src/Tools/Metis/src/Subsume.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Subsume.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Subsume = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Subsume.sml --- a/src/Tools/Metis/src/Subsume.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Subsume.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Subsume :> Subsume = @@ -97,7 +97,7 @@ fun size (Subsume {empty, unit, nonunit = {clauses,...}}) = length empty + LiteralNet.size unit + IntMap.size clauses; - + fun insert (Subsume {empty,unit,nonunit}) (cl',a) = case sortClause cl' of [] => diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Term.sig --- a/src/Tools/Metis/src/Term.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Term.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Term = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Term.sml --- a/src/Tools/Metis/src/Term.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Term.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Term :> Term = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/TermNet.sig --- a/src/Tools/Metis/src/TermNet.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/TermNet.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 TermNet = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/TermNet.sml --- a/src/Tools/Metis/src/TermNet.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/TermNet.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 TermNet :> TermNet = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Thm.sig --- a/src/Tools/Metis/src/Thm.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Thm.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Thm = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Thm.sml --- a/src/Tools/Metis/src/Thm.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Thm.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Thm :> Thm = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Tptp.sig --- a/src/Tools/Metis/src/Tptp.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Tptp.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* THE TPTP PROBLEM FILE FORMAT *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) signature Tptp = @@ -103,13 +103,23 @@ | FofFormulaBody of Formula.formula (* ------------------------------------------------------------------------- *) +(* Extra TPTP inferences. *) +(* ------------------------------------------------------------------------- *) + +datatype inference = + StripInference + | NegateInference + +val nameInference : inference -> string + +(* ------------------------------------------------------------------------- *) (* TPTP formula sources. *) (* ------------------------------------------------------------------------- *) datatype formulaSource = NoFormulaSource | StripFormulaSource of - {inference : string, + {inference : inference, parents : formulaName list} | NormalizeFormulaSource of {inference : Normalize.inference, diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Tptp.sml --- a/src/Tools/Metis/src/Tptp.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Tptp.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* THE TPTP PROBLEM FILE FORMAT *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) structure Tptp :> Tptp = @@ -886,13 +886,26 @@ | FofFormulaBody fm => ppFof mapping (Formula.generalize fm); (* ------------------------------------------------------------------------- *) +(* Extra TPTP inferences. *) +(* ------------------------------------------------------------------------- *) + +datatype inference = + StripInference + | NegateInference; + +fun nameInference inf = + case inf of + StripInference => "strip" + | NegateInference => "negate"; + +(* ------------------------------------------------------------------------- *) (* TPTP formula sources. *) (* ------------------------------------------------------------------------- *) datatype formulaSource = NoFormulaSource | StripFormulaSource of - {inference : string, + {inference : inference, parents : formulaName list} | NormalizeFormulaSource of {inference : Normalize.inference, @@ -983,8 +996,6 @@ val GEN_INFERENCE = "inference" and GEN_INTRODUCED = "introduced"; - fun nameStrip inf = inf; - fun ppStrip mapping inf = Print.skip; fun nameNormalize inf = @@ -1075,7 +1086,7 @@ let val gen = GEN_INFERENCE - val name = nameStrip inference + val name = nameInference inference in Print.inconsistentBlock (size gen + 1) [Print.ppString gen, @@ -1315,7 +1326,7 @@ (fn ((),((),s)) => "$$" ^ s); val nameParser = - (stringParser || numberParser || quoteParser) >> FormulaName; + (lowerParser || numberParser || quoteParser) >> FormulaName; val roleParser = lowerParser >> fromStringRole; @@ -2043,46 +2054,79 @@ end; local - datatype blockComment = - OutsideBlockComment + datatype comment = + NoComment + | EnteringLineComment + | InsideLineComment | EnteringBlockComment | InsideBlockComment - | LeavingBlockComment; - - fun stripLineComments acc strm = + | LeavingBlockComment + | InsideSingleQuoteComment + | EscapedSingleQuoteComment; + + fun stripInitialLineComments acc strm = case strm of Stream.Nil => (List.rev acc, Stream.Nil) | Stream.Cons (line,rest) => case total destLineComment line of - SOME s => stripLineComments (s :: acc) (rest ()) - | NONE => (List.rev acc, Stream.filter (not o isLineComment) strm); - - fun advanceBlockComment c state = + SOME s => stripInitialLineComments (s :: acc) (rest ()) + | NONE => (List.rev acc, strm); + + fun advanceComment c state = case state of - OutsideBlockComment => - if c = #"/" then (Stream.Nil, EnteringBlockComment) - else (Stream.singleton c, OutsideBlockComment) + NoComment => + (case c of + #"\n" => (Stream.Nil, EnteringLineComment) + | #"/" => (Stream.Nil, EnteringBlockComment) + | #"'" => (Stream.singleton #"'", InsideSingleQuoteComment) + | _ => (Stream.singleton c, NoComment)) + | EnteringLineComment => + (case c of + #"%" => (Stream.singleton #"\n", InsideLineComment) + | #"\n" => (Stream.singleton #"\n", EnteringLineComment) + | #"/" => (Stream.singleton #"\n", EnteringBlockComment) + | #"'" => (Stream.fromList [#"\n",#"'"], InsideSingleQuoteComment) + | _ => (Stream.fromList [#"\n",c], NoComment)) + | InsideLineComment => + (case c of + #"\n" => (Stream.Nil, EnteringLineComment) + | _ => (Stream.Nil, InsideLineComment)) | EnteringBlockComment => - if c = #"*" then (Stream.Nil, InsideBlockComment) - else if c = #"/" then (Stream.singleton #"/", EnteringBlockComment) - else (Stream.fromList [#"/",c], OutsideBlockComment) + (case c of + #"*" => (Stream.Nil, InsideBlockComment) + | #"\n" => (Stream.singleton #"/", EnteringLineComment) + | #"/" => (Stream.singleton #"/", EnteringBlockComment) + | #"'" => (Stream.fromList [#"/",#"'"], InsideSingleQuoteComment) + | _ => (Stream.fromList [#"/",c], NoComment)) | InsideBlockComment => - if c = #"*" then (Stream.Nil, LeavingBlockComment) - else (Stream.Nil, InsideBlockComment) + (case c of + #"*" => (Stream.Nil, LeavingBlockComment) + | _ => (Stream.Nil, InsideBlockComment)) | LeavingBlockComment => - if c = #"/" then (Stream.Nil, OutsideBlockComment) - else if c = #"*" then (Stream.Nil, LeavingBlockComment) - else (Stream.Nil, InsideBlockComment); - - fun eofBlockComment state = + (case c of + #"/" => (Stream.Nil, NoComment) + | #"*" => (Stream.Nil, LeavingBlockComment) + | _ => (Stream.Nil, InsideBlockComment)) + | InsideSingleQuoteComment => + (case c of + #"'" => (Stream.singleton #"'", NoComment) + | #"\\" => (Stream.singleton #"\\", EscapedSingleQuoteComment) + | _ => (Stream.singleton c, InsideSingleQuoteComment)) + | EscapedSingleQuoteComment => + (Stream.singleton c, InsideSingleQuoteComment); + + fun eofComment state = case state of - OutsideBlockComment => Stream.Nil + NoComment => Stream.Nil + | EnteringLineComment => Stream.singleton #"\n" + | InsideLineComment => Stream.Nil | EnteringBlockComment => Stream.singleton #"/" - | _ => raise Error "EOF inside a block comment"; - - val stripBlockComments = - Stream.mapsConcat advanceBlockComment eofBlockComment - OutsideBlockComment; + | InsideBlockComment => raise Error "EOF inside a block comment" + | LeavingBlockComment => raise Error "EOF inside a block comment" + | InsideSingleQuoteComment => raise Error "EOF inside a single quote" + | EscapedSingleQuoteComment => raise Error "EOF inside a single quote"; + + val stripComments = Stream.mapsConcat advanceComment eofComment NoComment; in fun read {mapping,filename} = let @@ -2095,11 +2139,11 @@ (let (* The character stream *) - val (comments,chars) = stripLineComments [] chars + val (comments,chars) = stripInitialLineComments [] chars val chars = Parse.everything Parse.any chars - val chars = stripBlockComments chars + val chars = stripComments chars (* The declaration stream *) @@ -2347,7 +2391,7 @@ val source = StripFormulaSource - {inference = "strip", + {inference = StripInference, parents = pars} val formula = @@ -2487,7 +2531,7 @@ let val source = StripFormulaSource - {inference = "negate", + {inference = NegateInference, parents = [name]} val prefix = "negate_" ^ Int.toString number ^ "_" diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Units.sig --- a/src/Tools/Metis/src/Units.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Units.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Units = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Units.sml --- a/src/Tools/Metis/src/Units.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Units.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Units :> Units = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Useful.sig --- a/src/Tools/Metis/src/Useful.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Useful.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Useful = @@ -203,6 +203,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 diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Useful.sml --- a/src/Tools/Metis/src/Useful.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Useful.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Useful :> Useful = @@ -474,33 +474,99 @@ end; 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 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; + fun inc s = + let + val (_,s) = incSieve s + in + s + end; in - fun primes n = - if n <= 0 then [] - else calcPrimes true [2] 3 (n - 1); + fun primesUpTo m = + if m <= 1 then [] + else primesSieve (funpow (m - 1) inc initSieve); +end; - fun primesUpTo n = - if n < 2 then [] - else calcPrimes false [2] 3 (n - 2); -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. *) @@ -847,7 +913,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) diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Waiting.sig --- a/src/Tools/Metis/src/Waiting.sig Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Waiting.sig Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Waiting = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/Waiting.sml --- a/src/Tools/Metis/src/Waiting.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/Waiting.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* 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 Waiting :> Waiting = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/metis.sml --- a/src/Tools/Metis/src/metis.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/metis.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* METIS FIRST ORDER PROVER *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) open Useful; @@ -11,9 +11,9 @@ val PROGRAM = "metis"; -val VERSION = "2.3"; +val VERSION = "2.4"; -val versionString = PROGRAM^" "^VERSION^" (release 20110926)"^"\n"; +val versionString = PROGRAM^" "^VERSION^" (release 20180810)"^"\n"; (* ------------------------------------------------------------------------- *) (* Program options. *) @@ -157,7 +157,7 @@ local fun display_sep () = if notshowing_any () then () - else TextIO.print (nChars #"-" (!Print.lineLength) ^ "\n"); + else TextIO.print (nChars #"%" (!Print.lineLength) ^ "\n"); fun display_name filename = if notshowing "name" then () @@ -204,7 +204,7 @@ local fun display_proof_start filename = - TextIO.print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n"); + TextIO.print ("\n% SZS output start CNFRefutation for " ^ filename ^ "\n"); fun display_proof_body problem proofs = let @@ -235,7 +235,7 @@ end; fun display_proof_end filename = - TextIO.print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n"); + TextIO.print ("% SZS output end CNFRefutation for " ^ filename ^ "\n\n"); in fun display_proof filename problem proofs = if notshowing "proof" then () @@ -291,7 +291,7 @@ fun display_status filename status = if notshowing "status" then () else - TextIO.print ("SZS status " ^ Tptp.toStringStatus status ^ + TextIO.print ("% SZS status " ^ Tptp.toStringStatus status ^ " for " ^ filename ^ "\n"); fun display_problem filename cls = diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/problems.sml --- a/src/Tools/Metis/src/problems.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/problems.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) (* ========================================================================= *) @@ -218,7 +218,7 @@ {name = "SPLIT_NOT_IFF", comments = ["A way to split a goal that looks like ~(p <=> q)"], goal = ` -~(p <=> q) <=> (p ==> ~q) /\ (q ==> ~p)`}, +~(p <=> q) <=> (p ==> ~q) /\ (~q ==> p)`}, (* ------------------------------------------------------------------------- *) (* Monadic Predicate Logic. *) diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/problems2tptp.sml --- a/src/Tools/Metis/src/problems2tptp.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/problems2tptp.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *) -(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) open Useful; diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/src/selftest.sml --- a/src/Tools/Metis/src/selftest.sml Wed Jul 08 16:35:23 2020 +0200 +++ b/src/Tools/Metis/src/selftest.sml Thu Jul 09 11:39:16 2020 +0200 @@ -1,6 +1,6 @@ (* ========================================================================= *) (* METIS TESTS *) -(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) +(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) @@ -65,6 +65,7 @@ and pvFm = printval Formula.pp and pvFms = printval (Print.ppList Formula.pp) and pvThm = printval Thm.pp +and pvThms = printval (Print.ppList Thm.pp) and pvEqn : Rule.equation -> Rule.equation = printval (Print.ppMap snd Thm.pp) and pvNet = printval (LiteralNet.pp Print.ppInt) and pvRw = printval Rewrite.pp @@ -483,6 +484,27 @@ val ax = pvThm (AX [`~(a = b)`, `~(b = c)`, `~(c = d)`, `a = d`]); val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax); +(* Bug discovered by Michael Farber *) + +val eqns = [Q`f $x = c`]; +val ax = pvThm (AX [`~(f $y = g a b)`,`p (g a b)`]); +val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax); + +val eqns = [Q`even (numeral c) = d`, + Q`f (numeral c) $x = $x`]; +val ax = pvThm + (AX [`~(even (numeral c) = even $y)`, + `p (even (f (numeral c) $y))`]); +val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax); + +val eqns = [Q`even (numeral c) = d`, + Q`f (numeral c) $x = $x`, + Q`g a b = numeral c`]; +val ax = pvThm + (AX [`~(even (numeral c) = even $y)`, + `p (even (f (g a b) $y))`]); +val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax); + (* ------------------------------------------------------------------------- *) val () = SAY "Unit cache"; (* ------------------------------------------------------------------------- *) @@ -500,6 +522,11 @@ val _ = pvFm (nnf (F`p /\ ~p`)); val _ = pvFm (nnf (F`(!x. P x) ==> ((?y. Q y) <=> (?z. P z /\ Q z))`)); val _ = pvFm (nnf (F`~(~(p <=> q) <=> r) <=> ~(p <=> ~(q <=> r))`)); +val _ = pvFm (nnf (F`~((((p <=> q) <=> r) /\ (q <=> r)) ==> p)`)); +val _ = pvFm (nnf (F`p <=> q`)); +val _ = pvFm (nnf (F`p <=> q <=> r`)); +val _ = pvFm (nnf (F`p <=> q <=> r <=> s`)); +val _ = pvFm (nnf (F`p <=> q <=> r <=> s <=> t`)); (* ------------------------------------------------------------------------- *) val () = SAY "Conjunctive normal form"; @@ -1064,6 +1091,27 @@ `$y <= exp $x`]); val _ = pvLits (Clause.largestLiterals cl); +(* Bug discovered by Michael Farber *) + +local + fun activeFactor th = + let + val (_,{axioms,conjecture}) = + Active.new Active.default {axioms = [], conjecture = [th]} + in + List.map Clause.thm (axioms @ conjecture) + end; +in + val th = pvThm (AX[`c4 (c5 (c6 c7 c8) $y) $z = c3`, + `c4 (c5 (c6 c7 c8) $t) $u = c3`]); + val _ = pvThms (activeFactor th); + + val th = pvThm (AX[`~(c4 (c5 (c6 c7 c8) c28) c29 = c4 (c5 (c6 c7 c8) c28) $x)`, + `c4 (c5 (c6 c7 c8) $y) $z = c3`, + `c4 (c5 (c6 c7 c8) $t) $u = c3`]); + val _ = pvThms (activeFactor th); +end; + (* ------------------------------------------------------------------------- *) val () = SAY "Syntax checking the problem sets"; (* ------------------------------------------------------------------------- *)