--- a/src/Tools/Metis/Makefile Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/Makefile Wed Jun 08 08:47:43 2011 +0200
@@ -22,7 +22,7 @@
$(MLTON_TARGETS) \
bin/mlton/*.sml bin/mlton/*.mlb \
$(POLYML_TARGETS) \
- bin/polyml/*.sml bin/polyml/*.o
+ bin/polyml/*.sml bin/polyml/*.log bin/polyml/*.o
.PHONY: clean
clean:
@@ -138,10 +138,12 @@
METIS = bin/mlton/metis
+PROBLEMS2TPTP = bin/mlton/problems2tptp
+
MLTON_TARGETS = \
bin/mlton/selftest \
- bin/mlton/problems2tptp \
- $(METIS)
+ $(METIS) \
+ $(PROBLEMS2TPTP)
bin/mlton/%.sml: $(MLTON_SRC) src/%.sml
@$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@
@@ -202,7 +204,8 @@
@echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@
bin/polyml/%.o: bin/polyml/%.sml
- cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS)
+ 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
--- a/src/Tools/Metis/README Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/README Wed Jun 08 08:47:43 2011 +0200
@@ -4,9 +4,9 @@
for Metis with the latest Metis package.
1. The files "Makefile" and "script/mlpp" and the directory "src/"
- were initially copied from Joe Hurd's official Metis package. The
- package that was used when these notes where written was Metis 2.3
- (29 Dec. 2010).
+ 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 (31 May 2011).
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
@@ -20,13 +20,6 @@
3. Some modifications might have to be done manually to the source
files. The ultimate way to track them down is to use Mercurial.
- The command
-
- hg diff -r90c7c97f0c21: src
-
- should do the trick. You might need to specify a different
- revision number if somebody updated the Metis sources without
- updating these instructions; consult the history in case of doubt.
4. Isabelle itself cares only about "metis.ML", which is generated
from the files in "src/" by the script "make_metis". The script
@@ -53,4 +46,4 @@
Good luck!
Jasmin Blanchette
- 23 March 2011
+ 8 June 2011
--- a/src/Tools/Metis/metis.ML Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/metis.ML Wed Jun 08 08:47:43 2011 +0200
@@ -5417,6 +5417,14 @@
val disjoint : set -> set -> bool
(* ------------------------------------------------------------------------- *)
+(* Closing under an operation. *)
+(* ------------------------------------------------------------------------- *)
+
+val closedAdd : (element -> set) -> set -> set -> set
+
+val close : (element -> set) -> set -> set
+
+(* ------------------------------------------------------------------------- *)
(* Converting to and from lists. *)
(* ------------------------------------------------------------------------- *)
@@ -5467,8 +5475,11 @@
(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
-functor Metis_ElementSet (KM : Metis_KeyMap) :> Metis_ElementSet
-where type element = KM.key and type 'a map = 'a KM.map =
+functor Metis_ElementSet (
+ KM : Metis_KeyMap
+) :> Metis_ElementSet
+where type element = KM.key
+and type 'a map = 'a KM.map =
struct
(* ------------------------------------------------------------------------- *)
@@ -5759,6 +5770,25 @@
fun disjoint (Metis_Set m1) (Metis_Set m2) = KM.disjointDomain m1 m2;
(* ------------------------------------------------------------------------- *)
+(* Closing under an operation. *)
+(* ------------------------------------------------------------------------- *)
+
+fun closedAdd f =
+ let
+ fun adds acc set = foldl check acc set
+
+ and check (elt,acc) =
+ if member elt acc then acc
+ else expand (add acc elt) elt
+
+ and expand acc elt = adds acc (f elt)
+ in
+ adds
+ end;
+
+fun close f = closedAdd f empty;
+
+(* ------------------------------------------------------------------------- *)
(* Converting to and from lists. *)
(* ------------------------------------------------------------------------- *)
@@ -6653,6 +6683,8 @@
val toString : 'a pp -> 'a -> string
+val toLine : 'a pp -> 'a -> string
+
val toStream : 'a pp -> 'a -> string Metis_Stream.stream
val trace : 'a pp -> string -> 'a -> unit
@@ -7828,17 +7860,13 @@
val lineLength = Unsynchronized.ref initialLineLength;
-fun toStream ppA a =
- Metis_Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
- (execute {lineLength = !lineLength} (ppA a));
-
local
fun inc {indent,line} acc = line :: nSpaces indent :: acc;
fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
in
- fun toString ppA a =
- case execute {lineLength = !lineLength} (ppA a) of
+ fun toLines len ppA a =
+ case execute {lineLength = len} (ppA a) of
Metis_Stream.Nil => ""
| Metis_Stream.Cons (h,t) =>
let
@@ -7848,6 +7876,14 @@
end;
end;
+fun toString ppA a = toLines (!lineLength) ppA a;
+
+fun toLine ppA a = toLines 100000 ppA a;
+
+fun toStream ppA a =
+ Metis_Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
+ (execute {lineLength = !lineLength} (ppA a));
+
local
val sep = mkStringSize " =";
in
--- a/src/Tools/Metis/src/ElementSet.sig Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/src/ElementSet.sig Wed Jun 08 08:47:43 2011 +0200
@@ -131,6 +131,14 @@
val disjoint : set -> set -> bool
(* ------------------------------------------------------------------------- *)
+(* Closing under an operation. *)
+(* ------------------------------------------------------------------------- *)
+
+val closedAdd : (element -> set) -> set -> set -> set
+
+val close : (element -> set) -> set -> set
+
+(* ------------------------------------------------------------------------- *)
(* Converting to and from lists. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/ElementSet.sml Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/src/ElementSet.sml Wed Jun 08 08:47:43 2011 +0200
@@ -3,8 +3,11 @@
(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
-functor ElementSet (KM : KeyMap) :> ElementSet
-where type element = KM.key and type 'a map = 'a KM.map =
+functor ElementSet (
+ KM : KeyMap
+) :> ElementSet
+where type element = KM.key
+and type 'a map = 'a KM.map =
struct
(* ------------------------------------------------------------------------- *)
@@ -295,6 +298,25 @@
fun disjoint (Set m1) (Set m2) = KM.disjointDomain m1 m2;
(* ------------------------------------------------------------------------- *)
+(* Closing under an operation. *)
+(* ------------------------------------------------------------------------- *)
+
+fun closedAdd f =
+ let
+ fun adds acc set = foldl check acc set
+
+ and check (elt,acc) =
+ if member elt acc then acc
+ else expand (add acc elt) elt
+
+ and expand acc elt = adds acc (f elt)
+ in
+ adds
+ end;
+
+fun close f = closedAdd f empty;
+
+(* ------------------------------------------------------------------------- *)
(* Converting to and from lists. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Print.sig Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/src/Print.sig Wed Jun 08 08:47:43 2011 +0200
@@ -167,6 +167,8 @@
val toString : 'a pp -> 'a -> string
+val toLine : 'a pp -> 'a -> string
+
val toStream : 'a pp -> 'a -> string Stream.stream
val trace : 'a pp -> string -> 'a -> unit
--- a/src/Tools/Metis/src/Print.sml Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/src/Print.sml Wed Jun 08 08:47:43 2011 +0200
@@ -1165,17 +1165,13 @@
val lineLength = ref initialLineLength;
-fun toStream ppA a =
- Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
- (execute {lineLength = !lineLength} (ppA a));
-
local
fun inc {indent,line} acc = line :: nSpaces indent :: acc;
fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
in
- fun toString ppA a =
- case execute {lineLength = !lineLength} (ppA a) of
+ fun toLines len ppA a =
+ case execute {lineLength = len} (ppA a) of
Stream.Nil => ""
| Stream.Cons (h,t) =>
let
@@ -1185,6 +1181,14 @@
end;
end;
+fun toString ppA a = toLines (!lineLength) ppA a;
+
+fun toLine ppA a = toLines 100000 ppA a;
+
+fun toStream ppA a =
+ Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
+ (execute {lineLength = !lineLength} (ppA a));
+
local
val sep = mkStringSize " =";
in
--- a/src/Tools/Metis/src/metis.sml Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/src/metis.sml Wed Jun 08 08:47:43 2011 +0200
@@ -13,7 +13,7 @@
val VERSION = "2.3";
-val versionString = PROGRAM^" "^VERSION^" (release 20101229)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20110531)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)