--- a/src/Tools/Metis/metis.ML Wed Sep 15 20:07:41 2010 +0200
+++ b/src/Tools/Metis/metis.ML Wed Sep 15 22:20:10 2010 +0200
@@ -1494,357 +1494,6 @@
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: 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 ****)
(* ========================================================================= *)