# HG changeset patch # User blanchet # Date 1307515663 -7200 # Node ID 3535f16d97145c40bc37f4891fc68cc85bead9c8 # Parent c0eaa8b9bff5965087de2dec8b0622623cad9506 new Metis version diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/Makefile --- 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 diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/README --- 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 diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/metis.ML --- 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 diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/src/ElementSet.sig --- 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. *) (* ------------------------------------------------------------------------- *) diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/src/ElementSet.sml --- 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. *) (* ------------------------------------------------------------------------- *) diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/src/Print.sig --- 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 diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/src/Print.sml --- 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 diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/src/metis.sml --- 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. *)