# HG changeset patch # User blanchet # Date 1284582010 -7200 # Node ID 3e41c9d297691ac877814300783d8d6dfaec5c96 # Parent f5320aba6750a72793c91ddf098adff22848d5bd make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; instead, query the original "Makefile" diff -r f5320aba6750 -r 3e41c9d29769 src/Tools/Metis/FILES --- a/src/Tools/Metis/FILES Wed Sep 15 20:07:41 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -Random.sig Random.sml -Portable.sig PortablePolyml.sml -Useful.sig Useful.sml -Lazy.sig Lazy.sml -Stream.sig Stream.sml -Ordered.sig Ordered.sml -Map.sig Map.sml -KeyMap.sig KeyMap.sml -Set.sig Set.sml -ElementSet.sig ElementSet.sml -Sharing.sig Sharing.sml -Heap.sig Heap.sml -Print.sig Print.sml -Parse.sig Parse.sml -Name.sig Name.sml -NameArity.sig NameArity.sml -Term.sig Term.sml -Subst.sig Subst.sml -Atom.sig Atom.sml -Formula.sig Formula.sml -Literal.sig Literal.sml -Thm.sig Thm.sml -Proof.sig Proof.sml -Rule.sig Rule.sml -Normalize.sig Normalize.sml -Model.sig Model.sml -Problem.sig Problem.sml -TermNet.sig TermNet.sml -AtomNet.sig AtomNet.sml -LiteralNet.sig LiteralNet.sml -Subsume.sig Subsume.sml -KnuthBendixOrder.sig KnuthBendixOrder.sml -Rewrite.sig Rewrite.sml -Units.sig Units.sml -Clause.sig Clause.sml -Active.sig Active.sml -Waiting.sig Waiting.sml -Resolution.sig Resolution.sml diff -r f5320aba6750 -r 3e41c9d29769 src/Tools/Metis/Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Metis/Makefile Wed Sep 15 22:20:10 2010 +0200 @@ -0,0 +1,230 @@ +############################################################################### +# METIS MAKEFILE +# Copyright (c) 2001 Joe Hurd, distributed under the GNU GPL version 2 +############################################################################### + +.SUFFIXES: + +############################################################################### +# The default action. +############################################################################### + +.PHONY: default +default: mosml + +############################################################################### +# 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/*.o + +.PHONY: clean +clean: + @echo + @echo '********************' + @echo '* Clean everything *' + @echo '********************' + @echo + rm -f $(TEMP) + $(MAKE) -C test $@ + +############################################################################### +# Testing. +############################################################################### + +.PHONY: test +test: + $(MAKE) -C test + +############################################################################### +# Source files. +############################################################################### + +SRC = \ + src/Useful.sig src/Useful.sml \ + src/Lazy.sig src/Lazy.sml \ + src/Ordered.sig src/Ordered.sml \ + src/Map.sig src/Map.sml \ + src/KeyMap.sig src/KeyMap.sml \ + src/Set.sig src/Set.sml \ + src/ElementSet.sig src/ElementSet.sml \ + src/Sharing.sig src/Sharing.sml \ + src/Stream.sig src/Stream.sml \ + src/Heap.sig src/Heap.sml \ + src/Print.sig src/Print.sml \ + src/Parse.sig src/Parse.sml \ + src/Name.sig src/Name.sml \ + src/NameArity.sig src/NameArity.sml \ + src/Term.sig src/Term.sml \ + src/Subst.sig src/Subst.sml \ + src/Atom.sig src/Atom.sml \ + src/Formula.sig src/Formula.sml \ + src/Literal.sig src/Literal.sml \ + src/Thm.sig src/Thm.sml \ + src/Proof.sig src/Proof.sml \ + src/Rule.sig src/Rule.sml \ + src/Normalize.sig src/Normalize.sml \ + src/Model.sig src/Model.sml \ + src/Problem.sig src/Problem.sml \ + src/TermNet.sig src/TermNet.sml \ + src/AtomNet.sig src/AtomNet.sml \ + src/LiteralNet.sig src/LiteralNet.sml \ + src/Subsume.sig src/Subsume.sml \ + src/KnuthBendixOrder.sig src/KnuthBendixOrder.sml \ + src/Rewrite.sig src/Rewrite.sml \ + src/Units.sig src/Units.sml \ + src/Clause.sig src/Clause.sml \ + src/Active.sig src/Active.sml \ + src/Waiting.sig src/Waiting.sml \ + src/Resolution.sig src/Resolution.sml \ + src/Tptp.sig src/Tptp.sml \ + src/Options.sig src/Options.sml + +EXTRA_SRC = \ + src/problems.sml + +############################################################################### +# The ML preprocessor. +############################################################################### + +MLPP = scripts/mlpp + +MLPP_OPTS = + +############################################################################### +# Building using Moscow ML. +############################################################################### + +MOSMLC = mosmlc -toplevel -q + +MOSML_SRC = \ + src/Portable.sig src/PortableMosml.sml \ + $(SRC) + +MOSML_TARGETS = \ + bin/mosml/problems2tptp \ + bin/mosml/metis + +include bin/mosml/Makefile.src + +.PHONY: mosml-info +mosml-info: + @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 + +MLTON_TARGETS = \ + bin/mlton/selftest \ + bin/mlton/problems2tptp \ + $(METIS) + +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 = + +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) + +bin/polyml/%: bin/polyml/%.o + @echo + @echo '*****************************' + @echo '* Compile a Poly/ML program *' + @echo '*****************************' + @echo + @echo $@ + cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) -lpolymain -lpolyml + @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. +############################################################################## + +include Makefile.dev + +Makefile.dev: + echo > $@ diff -r f5320aba6750 -r 3e41c9d29769 src/Tools/Metis/Makefile.FILES --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Metis/Makefile.FILES Wed Sep 15 22:20:10 2010 +0200 @@ -0,0 +1,10 @@ +include Makefile +bin/mosml/Makefile.src: + mkdir -p `dirname $@` + echo > $@ +refresh_FILES: + echo $(POLYML_SRC) | \ + sed "s/src\///g" | \ + sed "s/ Tptp\.s[a-z][a-z]//g" | \ + sed "s/ Options\.s[a-z][a-z]//g" \ + > FILES diff -r f5320aba6750 -r 3e41c9d29769 src/Tools/Metis/README --- a/src/Tools/Metis/README Wed Sep 15 20:07:41 2010 +0200 +++ b/src/Tools/Metis/README Wed Sep 15 22:20:10 2010 +0200 @@ -5,11 +5,12 @@ unfortunately somewhat involved and frustrating, and hopefully temporary. - 1. The directories "src/" and "script/" were initially copied from - Joe Hurd's Metis package. (His "script/" directory has many files - in it, but we only need "mlpp".) The package that was used when - these notes where written was an unnumbered version of Metis, more - recent than 2.2 and dated 19 July 2010. + 1. The file "Makefile" and the directory "src/" and "script/" were + initially copied from Joe Hurd's Metis package. (His "script/" + directory has many files in it, but we only need "mlpp".) The + package that was used when these notes where written was an + unnumbered version of Metis, more recent than 2.2 and dated 19 + July 2010. 2. The license in each source file will probably not be something we can use in Isabelle. Lawrence C. Paulson's command @@ -20,8 +21,9 @@ 2010 email to Gerwin Klein, Joe 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 Isabelle BSD license. + I hereby give permission to the Isabelle team to release Metis + as part of Isabelle, with the Metis code covered under the + Isabelle BSD license. 3. Some modifications have to be done manually to the source files. Some of these are necessary so that the sources compile at all @@ -44,16 +46,16 @@ 4. Isabelle itself only cares about "metis.ML", which is generated from the files in "src/" by the script "make_metis". The script - relies on "src/", "scripts/", and a hand-crafted "FILES" file - listing all the files needed to be included in "metis.ML". The - "FILES" file should be updated to reflect the contents of "src/", - although a few files in "src/" are not necessary. Also, the order - of the file names in "FILES" matters; X must appear before Y if Y - depends on X. + relies on "Makefile", "src/", and "scripts/", as well as a special + file "Makefile.FILES" used to determine all the files needed to be + included in "metis.ML". 5. The output of "make_metis" should then work as is with Isabelle, but there are of course no guarantees. The script "make_metis" has - a few evil regex hacks that could go wrong. + a few evil regex hacks that could go wrong. It also produces a + few temporary files ("FILES", "Makefile.dev", and + "bin/mosml/Makefile.src") as side-effects; you can safely ignore + them or delete them. 6. Once you have successfully regenerated "metis.ML", build all of Isabelle and keep an eye on the time taken by Metis. diff -r f5320aba6750 -r 3e41c9d29769 src/Tools/Metis/make_metis --- a/src/Tools/Metis/make_metis Wed Sep 15 20:07:41 2010 +0200 +++ b/src/Tools/Metis/make_metis Wed Sep 15 22:20:10 2010 +0200 @@ -8,6 +8,8 @@ THIS=$(cd "$(dirname "$0")"; echo $PWD) +make -f Makefile.FILES refresh_FILES + ( cat < 'a stream) - -(* If you're wondering how to create an infinite stream: *) -(* val stream4 = let fun s4 () = Metis_Stream.Cons (4,s4) in s4 () end; *) - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream constructors. *) -(* ------------------------------------------------------------------------- *) - -val repeat : 'a -> 'a stream - -val count : int -> int stream - -val funpows : ('a -> 'a) -> 'a -> 'a stream - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream versions of standard list operations: these should all terminate. *) -(* ------------------------------------------------------------------------- *) - -val cons : 'a -> (unit -> 'a stream) -> 'a stream - -val null : 'a stream -> bool - -val hd : 'a stream -> 'a (* raises Empty *) - -val tl : 'a stream -> 'a stream (* raises Empty *) - -val hdTl : 'a stream -> 'a * 'a stream (* raises Empty *) - -val singleton : 'a -> 'a stream - -val append : 'a stream -> (unit -> 'a stream) -> 'a stream - -val map : ('a -> 'b) -> 'a stream -> 'b stream - -val maps : - ('a -> 's -> 'b * 's) -> ('s -> 'b stream) -> 's -> 'a stream -> 'b stream - -val zipwith : ('a -> 'b -> 'c) -> 'a stream -> 'b stream -> 'c stream - -val zip : 'a stream -> 'b stream -> ('a * 'b) stream - -val take : int -> 'a stream -> 'a stream (* raises Subscript *) - -val drop : int -> 'a stream -> 'a stream (* raises Subscript *) - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream versions of standard list operations: these might not terminate. *) -(* ------------------------------------------------------------------------- *) - -val length : 'a stream -> int - -val exists : ('a -> bool) -> 'a stream -> bool - -val all : ('a -> bool) -> 'a stream -> bool - -val filter : ('a -> bool) -> 'a stream -> 'a stream - -val foldl : ('a * 's -> 's) -> 's -> 'a stream -> 's - -val concat : 'a stream stream -> 'a stream - -val mapPartial : ('a -> 'b option) -> 'a stream -> 'b stream - -val mapsPartial : - ('a -> 's -> 'b option * 's) -> ('s -> 'b stream) -> 's -> - 'a stream -> 'b stream - -val mapConcat : ('a -> 'b stream) -> 'a stream -> 'b stream - -val mapsConcat : - ('a -> 's -> 'b stream * 's) -> ('s -> 'b stream) -> 's -> - 'a stream -> 'b stream - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream operations. *) -(* ------------------------------------------------------------------------- *) - -val memoize : 'a stream -> 'a stream - -val listConcat : 'a list stream -> 'a stream - -val concatList : 'a stream list -> 'a stream - -val toList : 'a stream -> 'a list - -val fromList : 'a list -> 'a stream - -val toString : char stream -> string - -val fromString : string -> char stream - -val toTextFile : {filename : string} -> string stream -> unit - -val fromTextFile : {filename : string} -> string stream (* line by line *) - -end - -(**** Original file: Stream.sml ****) - -(* ========================================================================= *) -(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *) -(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) -(* ========================================================================= *) - -structure Metis_Stream :> Metis_Stream = -struct - -open Metis_Useful; (* MODIFIED by Jasmin Blanchette *) - -val K = Metis_Useful.K; - -val pair = Metis_Useful.pair; - -val funpow = Metis_Useful.funpow; - -(* ------------------------------------------------------------------------- *) -(* The stream type. *) -(* ------------------------------------------------------------------------- *) - -datatype 'a stream = - Nil - | Cons of 'a * (unit -> 'a stream); - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream constructors. *) -(* ------------------------------------------------------------------------- *) - -fun repeat x = let fun rep () = Cons (x,rep) in rep () end; - -fun count n = Cons (n, fn () => count (n + 1)); - -fun funpows f x = Cons (x, fn () => funpows f (f x)); - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream versions of standard list operations: these should all terminate. *) -(* ------------------------------------------------------------------------- *) - -fun cons h t = Cons (h,t); - -fun null Nil = true - | null (Cons _) = false; - -fun hd Nil = raise Empty - | hd (Cons (h,_)) = h; - -fun tl Nil = raise Empty - | tl (Cons (_,t)) = t (); - -fun hdTl s = (hd s, tl s); - -fun singleton s = Cons (s, K Nil); - -fun append Nil s = s () - | append (Cons (h,t)) s = Cons (h, fn () => append (t ()) s); - -fun map f = - let - fun m Nil = Nil - | m (Cons (h,t)) = Cons (f h, m o t) - in - m - end; - -fun maps f g = - let - fun mm s Nil = g s - | mm s (Cons (x,xs)) = - let - val (y,s') = f x s - in - Cons (y, mm s' o xs) - end - in - mm - end; - -fun zipwith f = - let - fun z Nil _ = Nil - | z _ Nil = Nil - | z (Cons (x,xs)) (Cons (y,ys)) = - Cons (f x y, fn () => z (xs ()) (ys ())) - in - z - end; - -fun zip s t = zipwith pair s t; - -fun take 0 _ = Nil - | take n Nil = raise Subscript - | take 1 (Cons (x,_)) = Cons (x, K Nil) - | take n (Cons (x,xs)) = Cons (x, fn () => take (n - 1) (xs ())); - -fun drop n s = funpow n tl s handle Empty => raise Subscript; - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream versions of standard list operations: these might not terminate. *) -(* ------------------------------------------------------------------------- *) - -local - fun len n Nil = n - | len n (Cons (_,t)) = len (n + 1) (t ()); -in - fun length s = len 0 s; -end; - -fun exists pred = - let - fun f Nil = false - | f (Cons (h,t)) = pred h orelse f (t ()) - in - f - end; - -fun all pred = not o exists (not o pred); - -fun filter p Nil = Nil - | filter p (Cons (x,xs)) = - if p x then Cons (x, fn () => filter p (xs ())) else filter p (xs ()); - -fun foldl f = - let - fun fold b Nil = b - | fold b (Cons (h,t)) = fold (f (h,b)) (t ()) - in - fold - end; - -fun concat Nil = Nil - | concat (Cons (Nil, ss)) = concat (ss ()) - | concat (Cons (Cons (x, xs), ss)) = - Cons (x, fn () => concat (Cons (xs (), ss))); - -fun mapPartial f = - let - fun mp Nil = Nil - | mp (Cons (h,t)) = - case f h of - NONE => mp (t ()) - | SOME h' => Cons (h', fn () => mp (t ())) - in - mp - end; - -fun mapsPartial f g = - let - fun mp s Nil = g s - | mp s (Cons (h,t)) = - let - val (h,s) = f h s - in - case h of - NONE => mp s (t ()) - | SOME h => Cons (h, fn () => mp s (t ())) - end - in - mp - end; - -fun mapConcat f = - let - fun mc Nil = Nil - | mc (Cons (h,t)) = append (f h) (fn () => mc (t ())) - in - mc - end; - -fun mapsConcat f g = - let - fun mc s Nil = g s - | mc s (Cons (h,t)) = - let - val (l,s) = f h s - in - append l (fn () => mc s (t ())) - end - in - mc - end; - -(* ------------------------------------------------------------------------- *) -(* Metis_Stream operations. *) -(* ------------------------------------------------------------------------- *) - -fun memoize Nil = Nil - | memoize (Cons (h,t)) = Cons (h, Metis_Lazy.memoize (fn () => memoize (t ()))); - -fun concatList [] = Nil - | concatList (h :: t) = append h (fn () => concatList t); - -local - fun toLst res Nil = rev res - | toLst res (Cons (x, xs)) = toLst (x :: res) (xs ()); -in - fun toList s = toLst [] s; -end; - -fun fromList [] = Nil - | fromList (x :: xs) = Cons (x, fn () => fromList xs); - -fun listConcat s = concat (map fromList s); - -fun toString s = implode (toList s); - -fun fromString s = fromList (explode s); - -fun toTextFile {filename = f} s = - let - val (h,close) = - if f = "-" then (TextIO.stdOut, K ()) - else (TextIO.openOut f, TextIO.closeOut) - - fun toFile Nil = () - | toFile (Cons (x,y)) = (TextIO.output (h,x); toFile (y ())) - - val () = toFile s - in - close h - end; - -fun fromTextFile {filename = f} = - let - val (h,close) = - if f = "-" then (TextIO.stdIn, K ()) - else (TextIO.openIn f, TextIO.closeIn) - - fun strm () = - case TextIO.inputLine h of - NONE => (close h; Nil) - | SOME s => Cons (s,strm) - in - memoize (strm ()) - end; - -end - (**** Original file: Ordered.sig ****) (* ========================================================================= *) @@ -6415,6 +6064,357 @@ end +(**** Original file: Stream.sig ****) + +(* ========================================================================= *) +(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *) +(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) +(* ========================================================================= *) + +signature Metis_Stream = +sig + +(* ------------------------------------------------------------------------- *) +(* The stream type. *) +(* ------------------------------------------------------------------------- *) + +datatype 'a stream = Nil | Cons of 'a * (unit -> 'a stream) + +(* If you're wondering how to create an infinite stream: *) +(* val stream4 = let fun s4 () = Metis_Stream.Cons (4,s4) in s4 () end; *) + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream constructors. *) +(* ------------------------------------------------------------------------- *) + +val repeat : 'a -> 'a stream + +val count : int -> int stream + +val funpows : ('a -> 'a) -> 'a -> 'a stream + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream versions of standard list operations: these should all terminate. *) +(* ------------------------------------------------------------------------- *) + +val cons : 'a -> (unit -> 'a stream) -> 'a stream + +val null : 'a stream -> bool + +val hd : 'a stream -> 'a (* raises Empty *) + +val tl : 'a stream -> 'a stream (* raises Empty *) + +val hdTl : 'a stream -> 'a * 'a stream (* raises Empty *) + +val singleton : 'a -> 'a stream + +val append : 'a stream -> (unit -> 'a stream) -> 'a stream + +val map : ('a -> 'b) -> 'a stream -> 'b stream + +val maps : + ('a -> 's -> 'b * 's) -> ('s -> 'b stream) -> 's -> 'a stream -> 'b stream + +val zipwith : ('a -> 'b -> 'c) -> 'a stream -> 'b stream -> 'c stream + +val zip : 'a stream -> 'b stream -> ('a * 'b) stream + +val take : int -> 'a stream -> 'a stream (* raises Subscript *) + +val drop : int -> 'a stream -> 'a stream (* raises Subscript *) + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream versions of standard list operations: these might not terminate. *) +(* ------------------------------------------------------------------------- *) + +val length : 'a stream -> int + +val exists : ('a -> bool) -> 'a stream -> bool + +val all : ('a -> bool) -> 'a stream -> bool + +val filter : ('a -> bool) -> 'a stream -> 'a stream + +val foldl : ('a * 's -> 's) -> 's -> 'a stream -> 's + +val concat : 'a stream stream -> 'a stream + +val mapPartial : ('a -> 'b option) -> 'a stream -> 'b stream + +val mapsPartial : + ('a -> 's -> 'b option * 's) -> ('s -> 'b stream) -> 's -> + 'a stream -> 'b stream + +val mapConcat : ('a -> 'b stream) -> 'a stream -> 'b stream + +val mapsConcat : + ('a -> 's -> 'b stream * 's) -> ('s -> 'b stream) -> 's -> + 'a stream -> 'b stream + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream operations. *) +(* ------------------------------------------------------------------------- *) + +val memoize : 'a stream -> 'a stream + +val listConcat : 'a list stream -> 'a stream + +val concatList : 'a stream list -> 'a stream + +val toList : 'a stream -> 'a list + +val fromList : 'a list -> 'a stream + +val toString : char stream -> string + +val fromString : string -> char stream + +val toTextFile : {filename : string} -> string stream -> unit + +val fromTextFile : {filename : string} -> string stream (* line by line *) + +end + +(**** Original file: Stream.sml ****) + +(* ========================================================================= *) +(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *) +(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) +(* ========================================================================= *) + +structure Metis_Stream :> Metis_Stream = +struct + +open Metis_Useful; (* MODIFIED by Jasmin Blanchette *) + +val K = Metis_Useful.K; + +val pair = Metis_Useful.pair; + +val funpow = Metis_Useful.funpow; + +(* ------------------------------------------------------------------------- *) +(* The stream type. *) +(* ------------------------------------------------------------------------- *) + +datatype 'a stream = + Nil + | Cons of 'a * (unit -> 'a stream); + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream constructors. *) +(* ------------------------------------------------------------------------- *) + +fun repeat x = let fun rep () = Cons (x,rep) in rep () end; + +fun count n = Cons (n, fn () => count (n + 1)); + +fun funpows f x = Cons (x, fn () => funpows f (f x)); + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream versions of standard list operations: these should all terminate. *) +(* ------------------------------------------------------------------------- *) + +fun cons h t = Cons (h,t); + +fun null Nil = true + | null (Cons _) = false; + +fun hd Nil = raise Empty + | hd (Cons (h,_)) = h; + +fun tl Nil = raise Empty + | tl (Cons (_,t)) = t (); + +fun hdTl s = (hd s, tl s); + +fun singleton s = Cons (s, K Nil); + +fun append Nil s = s () + | append (Cons (h,t)) s = Cons (h, fn () => append (t ()) s); + +fun map f = + let + fun m Nil = Nil + | m (Cons (h,t)) = Cons (f h, m o t) + in + m + end; + +fun maps f g = + let + fun mm s Nil = g s + | mm s (Cons (x,xs)) = + let + val (y,s') = f x s + in + Cons (y, mm s' o xs) + end + in + mm + end; + +fun zipwith f = + let + fun z Nil _ = Nil + | z _ Nil = Nil + | z (Cons (x,xs)) (Cons (y,ys)) = + Cons (f x y, fn () => z (xs ()) (ys ())) + in + z + end; + +fun zip s t = zipwith pair s t; + +fun take 0 _ = Nil + | take n Nil = raise Subscript + | take 1 (Cons (x,_)) = Cons (x, K Nil) + | take n (Cons (x,xs)) = Cons (x, fn () => take (n - 1) (xs ())); + +fun drop n s = funpow n tl s handle Empty => raise Subscript; + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream versions of standard list operations: these might not terminate. *) +(* ------------------------------------------------------------------------- *) + +local + fun len n Nil = n + | len n (Cons (_,t)) = len (n + 1) (t ()); +in + fun length s = len 0 s; +end; + +fun exists pred = + let + fun f Nil = false + | f (Cons (h,t)) = pred h orelse f (t ()) + in + f + end; + +fun all pred = not o exists (not o pred); + +fun filter p Nil = Nil + | filter p (Cons (x,xs)) = + if p x then Cons (x, fn () => filter p (xs ())) else filter p (xs ()); + +fun foldl f = + let + fun fold b Nil = b + | fold b (Cons (h,t)) = fold (f (h,b)) (t ()) + in + fold + end; + +fun concat Nil = Nil + | concat (Cons (Nil, ss)) = concat (ss ()) + | concat (Cons (Cons (x, xs), ss)) = + Cons (x, fn () => concat (Cons (xs (), ss))); + +fun mapPartial f = + let + fun mp Nil = Nil + | mp (Cons (h,t)) = + case f h of + NONE => mp (t ()) + | SOME h' => Cons (h', fn () => mp (t ())) + in + mp + end; + +fun mapsPartial f g = + let + fun mp s Nil = g s + | mp s (Cons (h,t)) = + let + val (h,s) = f h s + in + case h of + NONE => mp s (t ()) + | SOME h => Cons (h, fn () => mp s (t ())) + end + in + mp + end; + +fun mapConcat f = + let + fun mc Nil = Nil + | mc (Cons (h,t)) = append (f h) (fn () => mc (t ())) + in + mc + end; + +fun mapsConcat f g = + let + fun mc s Nil = g s + | mc s (Cons (h,t)) = + let + val (l,s) = f h s + in + append l (fn () => mc s (t ())) + end + in + mc + end; + +(* ------------------------------------------------------------------------- *) +(* Metis_Stream operations. *) +(* ------------------------------------------------------------------------- *) + +fun memoize Nil = Nil + | memoize (Cons (h,t)) = Cons (h, Metis_Lazy.memoize (fn () => memoize (t ()))); + +fun concatList [] = Nil + | concatList (h :: t) = append h (fn () => concatList t); + +local + fun toLst res Nil = rev res + | toLst res (Cons (x, xs)) = toLst (x :: res) (xs ()); +in + fun toList s = toLst [] s; +end; + +fun fromList [] = Nil + | fromList (x :: xs) = Cons (x, fn () => fromList xs); + +fun listConcat s = concat (map fromList s); + +fun toString s = implode (toList s); + +fun fromString s = fromList (explode s); + +fun toTextFile {filename = f} s = + let + val (h,close) = + if f = "-" then (TextIO.stdOut, K ()) + else (TextIO.openOut f, TextIO.closeOut) + + fun toFile Nil = () + | toFile (Cons (x,y)) = (TextIO.output (h,x); toFile (y ())) + + val () = toFile s + in + close h + end; + +fun fromTextFile {filename = f} = + let + val (h,close) = + if f = "-" then (TextIO.stdIn, K ()) + else (TextIO.openIn f, TextIO.closeIn) + + fun strm () = + case TextIO.inputLine h of + NONE => (close h; Nil) + | SOME s => Cons (s,strm) + in + memoize (strm ()) + end; + +end + (**** Original file: Heap.sig ****) (* ========================================================================= *)