--- a/src/Tools/Metis/README Wed Sep 15 20:47:14 2010 +0200
+++ b/src/Tools/Metis/README Wed Sep 15 22:24:35 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.
--- a/src/Tools/Metis/metis.ML Wed Sep 15 20:47:14 2010 +0200
+++ b/src/Tools/Metis/metis.ML Wed Sep 15 22:24:35 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 ****)
(* ========================================================================= *)