--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/lazy_scan.ML Sat Oct 08 22:39:40 2005 +0200
@@ -0,0 +1,206 @@
+(* Title: HOL/Import/lazy_scan.ML
+ ID: $Id$
+ Author: Sebastian Skalberg, TU Muenchen
+
+Scanner combinators for lazy sequences.
+*)
+
+signature LAZY_SCAN =
+sig
+
+ exception SyntaxError
+
+ type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
+
+ val :-- : ('a,'b) scanner * ('b -> ('a,'c) scanner)
+ -> ('a,'b*'c) scanner
+ val -- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
+ val >> : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
+ val --| : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
+ val |-- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
+ val ^^ : ('a,string) scanner * ('a,string) scanner
+ -> ('a,string) scanner
+ val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
+ val one : ('a -> bool) -> ('a,'a) scanner
+ val succeed : 'b -> ('a,'b) scanner
+ val any : ('a -> bool) -> ('a,'a list) scanner
+ val any1 : ('a -> bool) -> ('a,'a list) scanner
+ val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
+ val option : ('a,'b) scanner -> ('a,'b option) scanner
+ val repeat : ('a,'b) scanner -> ('a,'b list) scanner
+ val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner
+ val ahead : ('a,'b) scanner -> ('a,'b) scanner
+ val unless : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner
+ val $$ : ''a -> (''a,''a) scanner
+ val !! : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
+ val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
+
+end
+
+structure LazyScan :> LAZY_SCAN =
+struct
+
+infix 7 |-- --|
+infix 5 :-- -- ^^
+infix 3 >>
+infix 0 ||
+
+exception SyntaxError
+exception Fail of string
+
+type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
+
+fun (sc1 :-- sc2) toks =
+ let
+ val (x,toks2) = sc1 toks
+ val (y,toks3) = sc2 x toks2
+ in
+ ((x,y),toks3)
+ end
+
+fun (sc1 -- sc2) toks =
+ let
+ val (x,toks2) = sc1 toks
+ val (y,toks3) = sc2 toks2
+ in
+ ((x,y),toks3)
+ end
+
+fun (sc >> f) toks =
+ let
+ val (x,toks2) = sc toks
+ in
+ (f x,toks2)
+ end
+
+fun (sc1 --| sc2) toks =
+ let
+ val (x,toks2) = sc1 toks
+ val (_,toks3) = sc2 toks2
+ in
+ (x,toks3)
+ end
+
+fun (sc1 |-- sc2) toks =
+ let
+ val (_,toks2) = sc1 toks
+ in
+ sc2 toks2
+ end
+
+fun (sc1 ^^ sc2) toks =
+ let
+ val (x,toks2) = sc1 toks
+ val (y,toks3) = sc2 toks2
+ in
+ (x^y,toks3)
+ end
+
+fun (sc1 || sc2) toks =
+ (sc1 toks)
+ handle SyntaxError => sc2 toks
+
+fun one p toks =
+ case LazySeq.getItem toks of
+ NONE => raise SyntaxError
+ | SOME(t,toks) => if p t
+ then (t,toks)
+ else raise SyntaxError
+
+fun succeed e toks = (e,toks)
+
+fun any p toks =
+ case LazySeq.getItem toks of
+ NONE => ([],toks)
+ | SOME(x,toks2) => if p x
+ then
+ let
+ val (xs,toks3) = any p toks2
+ in
+ (x::xs,toks3)
+ end
+ else ([],toks)
+
+fun any1 p toks =
+ let
+ val (x,toks2) = one p toks
+ val (xs,toks3) = any p toks2
+ in
+ (x::xs,toks3)
+ end
+
+fun optional sc def = sc || succeed def
+fun option sc = (sc >> SOME) || succeed NONE
+
+(*
+fun repeat sc =
+ let
+ fun R toks =
+ let
+ val (x,toks2) = sc toks
+ val (xs,toks3) = R toks2
+ in
+ (x::xs,toks3)
+ end
+ handle SyntaxError => ([],toks)
+ in
+ R
+ end
+*)
+
+(* A tail-recursive version of repeat. It is (ever so) slightly slower
+ * than the above, non-tail-recursive version (due to the garbage generation
+ * associated with the reversal of the list). However, this version will be
+ * able to process input where the former version must give up (due to stack
+ * overflow). The slowdown seems to be around the one percent mark.
+ *)
+fun repeat sc =
+ let
+ fun R xs toks =
+ case SOME (sc toks) handle SyntaxError => NONE of
+ SOME (x,toks2) => R (x::xs) toks2
+ | NONE => (List.rev xs,toks)
+ in
+ R []
+ end
+
+fun repeat1 sc toks =
+ let
+ val (x,toks2) = sc toks
+ val (xs,toks3) = repeat sc toks2
+ in
+ (x::xs,toks3)
+ end
+
+fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
+
+fun unless test sc toks =
+ let
+ val test_failed = (test toks;false) handle SyntaxError => true
+ in
+ if test_failed
+ then sc toks
+ else raise SyntaxError
+ end
+
+fun $$ arg = one (fn x => x = arg)
+
+fun !! f sc toks = (sc toks
+ handle SyntaxError => raise Fail (f toks))
+
+fun scan_full sc toks =
+ let
+ fun F toks =
+ if LazySeq.null toks
+ then NONE
+ else
+ let
+ val (x,toks') = sc toks
+ in
+ SOME(x,LazySeq.make (fn () => F toks'))
+ end
+ in
+ LazySeq.make (fn () => F toks)
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/lazy_seq.ML Sat Oct 08 22:39:40 2005 +0200
@@ -0,0 +1,543 @@
+(* Title: HOL/Import/lazy_seq.ML
+ ID: $Id$
+ Author: Sebastian Skalberg, TU Muenchen
+
+Alternative version of lazy sequences.
+*)
+
+signature LAZY_SEQ =
+sig
+
+ type 'a seq
+
+ (* From LIST *)
+
+ val null : 'a seq -> bool
+ val length : 'a seq -> int
+ val @ : 'a seq * 'a seq -> 'a seq
+ val hd : 'a seq -> 'a
+ val tl : 'a seq -> 'a seq
+ val last : 'a seq -> 'a
+ val getItem : 'a seq -> ('a * 'a seq) option
+ val nth : 'a seq * int -> 'a
+ val take : 'a seq * int -> 'a seq
+ val drop : 'a seq * int -> 'a seq
+ val rev : 'a seq -> 'a seq
+ val concat : 'a seq seq -> 'a seq
+ val revAppend : 'a seq * 'a seq -> 'a seq
+ val app : ('a -> unit) -> 'a seq -> unit
+ val map : ('a -> 'b) -> 'a seq -> 'b seq
+ val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
+ val find : ('a -> bool) -> 'a seq -> 'a option
+ val filter : ('a -> bool) -> 'a seq -> 'a seq
+ val partition : ('a -> bool)
+ -> 'a seq -> 'a seq * 'a seq
+ val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
+ val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
+ val exists : ('a -> bool) -> 'a seq -> bool
+ val all : ('a -> bool) -> 'a seq -> bool
+ val tabulate : int * (int -> 'a) -> 'a seq
+ val collate : ('a * 'a -> order)
+ -> 'a seq * 'a seq -> order
+
+ (* Miscellaneous *)
+
+ val cycle : ((unit ->'a seq) -> 'a seq) -> 'a seq
+ val iterates : ('a -> 'a) -> 'a -> 'a seq
+ val of_function: (unit -> 'a option) -> 'a seq
+ val of_string : string -> char seq
+ val of_instream: TextIO.instream -> char seq
+
+ (* From SEQ *)
+
+ val make: (unit -> ('a * 'a seq) option) -> 'a seq
+ val empty: 'a -> 'a seq
+ val cons: 'a * 'a seq -> 'a seq
+ val single: 'a -> 'a seq
+ val try: ('a -> 'b) -> 'a -> 'b seq
+ val chop: int * 'a seq -> 'a list * 'a seq
+ val list_of: 'a seq -> 'a list
+ val of_list: 'a list -> 'a seq
+ val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
+ val interleave: 'a seq * 'a seq -> 'a seq
+ val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
+ val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
+ val commute: 'a seq list -> 'a list seq
+ val succeed: 'a -> 'a seq
+ val fail: 'a -> 'b seq
+ val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
+ val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
+ val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
+ val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
+ val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
+ val TRY: ('a -> 'a seq) -> 'a -> 'a seq
+ val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
+ val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
+ val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
+ val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
+
+end
+
+structure LazySeq :> LAZY_SEQ =
+struct
+
+open Susp
+
+datatype 'a seq = Seq of ('a * 'a seq) option susp
+
+exception Empty
+
+fun getItem (Seq s) = force s
+fun make f = Seq (delay f)
+
+fun null s = isSome (getItem s)
+
+local
+ fun F n NONE = n
+ | F n (SOME(_,s)) = F (n+1) (getItem s)
+in
+fun length s = F 0 (getItem s)
+end
+
+fun s1 @ s2 =
+ let
+ fun F NONE = getItem s2
+ | F (SOME(x,s1')) = SOME(x,F' s1')
+ and F' s = make (fn () => F (getItem s))
+ in
+ F' s1
+ end
+
+local
+ fun F NONE = raise Empty
+ | F (SOME arg) = arg
+in
+fun hd s = #1 (F (getItem s))
+fun tl s = #2 (F (getItem s))
+end
+
+local
+ fun F x NONE = x
+ | F _ (SOME(x,s)) = F x (getItem s)
+ fun G NONE = raise Empty
+ | G (SOME(x,s)) = F x (getItem s)
+in
+fun last s = G (getItem s)
+end
+
+local
+ fun F NONE _ = raise Subscript
+ | F (SOME(x,_)) 0 = x
+ | F (SOME(_,s)) n = F (getItem s) (n-1)
+in
+fun nth(s,n) =
+ if n < 0
+ then raise Subscript
+ else F (getItem s) n
+end
+
+local
+ fun F NONE _ = raise Subscript
+ | F (SOME(x,s)) n = SOME(x,F' s (n-1))
+ and F' s 0 = Seq (value NONE)
+ | F' s n = make (fn () => F (getItem s) n)
+in
+fun take (s,n) =
+ if n < 0
+ then raise Subscript
+ else F' s n
+end
+
+local
+ fun F s 0 = s
+ | F NONE _ = raise Subscript
+ | F (SOME(_,s)) n = F (getItem s) (n-1)
+in
+fun drop (s,0) = s
+ | drop (s,n) =
+ if n < 0
+ then raise Subscript
+ else make (fn () => F (getItem s) n)
+end
+
+local
+ fun F s NONE = s
+ | F s (SOME(x,s')) = F (SOME(x, Seq (value s))) (getItem s')
+in
+fun rev s = make (fn () => F NONE (getItem s))
+end
+
+local
+ fun F s NONE = getItem s
+ | F s (SOME(x,s')) = F (Seq (value (SOME(x,s)))) (getItem s')
+in
+fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
+end
+
+local
+ fun F NONE = NONE
+ | F (SOME(s1,s2)) =
+ let
+ fun G NONE = F (getItem s2)
+ | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
+ in
+ G (getItem s1)
+ end
+in
+fun concat s = make (fn () => F (getItem s))
+end
+
+fun app f =
+ let
+ fun F NONE = ()
+ | F (SOME(x,s)) =
+ (f x;
+ F (getItem s))
+ in
+ F o getItem
+ end
+
+fun map f =
+ let
+ fun F NONE = NONE
+ | F (SOME(x,s)) = SOME(f x,F' s)
+ and F' s = make (fn() => F (getItem s))
+ in
+ F'
+ end
+
+fun mapPartial f =
+ let
+ fun F NONE = NONE
+ | F (SOME(x,s)) =
+ (case f x of
+ SOME y => SOME(y,F' s)
+ | NONE => F (getItem s))
+ and F' s = make (fn()=> F (getItem s))
+ in
+ F'
+ end
+
+fun find P =
+ let
+ fun F NONE = NONE
+ | F (SOME(x,s)) =
+ if P x
+ then SOME x
+ else F (getItem s)
+ in
+ F o getItem
+ end
+
+(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
+
+fun filter P =
+ let
+ fun F NONE = NONE
+ | F (SOME(x,s)) =
+ if P x
+ then SOME(x,F' s)
+ else F (getItem s)
+ and F' s = make (fn () => F (getItem s))
+ in
+ F'
+ end
+
+fun partition f s =
+ let
+ val s' = map (fn x => (x,f x)) s
+ in
+ (mapPartial (fn (x,true) => SOME x | _ => NONE) s',
+ mapPartial (fn (x,false) => SOME x | _ => NONE) s')
+ end
+
+fun exists P =
+ let
+ fun F NONE = false
+ | F (SOME(x,s)) = P x orelse F (getItem s)
+ in
+ F o getItem
+ end
+
+fun all P =
+ let
+ fun F NONE = true
+ | F (SOME(x,s)) = P x andalso F (getItem s)
+ in
+ F o getItem
+ end
+
+(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
+
+fun tabulate (n,f) =
+ let
+ fun F n = make (fn () => SOME(f n,F (n+1)))
+ in
+ F n
+ end
+
+fun collate c (s1,s2) =
+ let
+ fun F NONE _ = LESS
+ | F _ NONE = GREATER
+ | F (SOME(x,s1)) (SOME(y,s2)) =
+ (case c (x,y) of
+ LESS => LESS
+ | GREATER => GREATER
+ | EQUAL => F' s1 s2)
+ and F' s1 s2 = F (getItem s1) (getItem s2)
+ in
+ F' s1 s2
+ end
+
+fun empty _ = Seq (value NONE)
+fun single x = Seq(value (SOME(x,Seq (value NONE))))
+fun cons a = Seq(value (SOME a))
+
+fun cycle seqfn =
+ let
+ val knot = ref (Seq (value NONE))
+ in
+ knot := seqfn (fn () => !knot);
+ !knot
+ end
+
+fun iterates f =
+ let
+ fun F x = make (fn() => SOME(x,F (f x)))
+ in
+ F
+ end
+
+fun interleave (s1,s2) =
+ let
+ fun F NONE = getItem s2
+ | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
+ in
+ make (fn()=> F (getItem s1))
+ end
+
+(* val force_all = app ignore *)
+
+local
+ fun F NONE = ()
+ | F (SOME(x,s)) = F (getItem s)
+in
+fun force_all s = F (getItem s)
+end
+
+fun of_function f =
+ let
+ fun F () = case f () of
+ SOME x => SOME(x,make F)
+ | NONE => NONE
+ in
+ make F
+ end
+
+local
+ fun F [] = NONE
+ | F (x::xs) = SOME(x,F' xs)
+ and F' xs = make (fn () => F xs)
+in
+fun of_list xs = F' xs
+end
+
+val of_string = of_list o String.explode
+
+fun of_instream is =
+ let
+ val buffer : char list ref = ref []
+ fun get_input () =
+ case !buffer of
+ (c::cs) => (buffer:=cs;
+ SOME c)
+ | [] => (case String.explode (TextIO.input is) of
+ [] => NONE
+ | (c::cs) => (buffer := cs;
+ SOME c))
+ in
+ of_function get_input
+ end
+
+local
+ fun F k NONE = k []
+ | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
+in
+fun list_of s = F (fn x => x) (getItem s)
+end
+
+(* Adapted from seq.ML *)
+
+val succeed = single
+fun fail _ = Seq (value NONE)
+
+(* fun op THEN (f, g) x = flat (map g (f x)) *)
+
+fun op THEN (f, g) =
+ let
+ fun F NONE = NONE
+ | F (SOME(x,xs)) =
+ let
+ fun G NONE = F (getItem xs)
+ | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
+ in
+ G (getItem (g x))
+ end
+ in
+ fn x => make (fn () => F (getItem (f x)))
+ end
+
+fun op ORELSE (f, g) x =
+ make (fn () =>
+ case getItem (f x) of
+ NONE => getItem (g x)
+ | some => some)
+
+fun op APPEND (f, g) x =
+ let
+ fun copy s =
+ case getItem s of
+ NONE => getItem (g x)
+ | SOME(x,xs) => SOME(x,make (fn () => copy xs))
+ in
+ make (fn () => copy (f x))
+ end
+
+fun EVERY fs = foldr (op THEN) succeed fs
+fun FIRST fs = foldr (op ORELSE) fail fs
+
+fun TRY f x =
+ make (fn () =>
+ case getItem (f x) of
+ NONE => SOME(x,Seq (value NONE))
+ | some => some)
+
+fun REPEAT f =
+ let
+ fun rep qs x =
+ case getItem (f x) of
+ NONE => SOME(x, make (fn () => repq qs))
+ | SOME (x', q) => rep (q :: qs) x'
+ and repq [] = NONE
+ | repq (q :: qs) =
+ case getItem q of
+ NONE => repq qs
+ | SOME (x, q) => rep (q :: qs) x
+ in
+ fn x => make (fn () => rep [] x)
+ end
+
+fun REPEAT1 f = op THEN (f, REPEAT f);
+
+fun INTERVAL f i =
+ let
+ fun F j =
+ if i > j
+ then single
+ else op THEN (f j, F (j - 1))
+ in F end
+
+fun DETERM f x =
+ make (fn () =>
+ case getItem (f x) of
+ NONE => NONE
+ | SOME (x', _) => SOME(x',Seq (value NONE)))
+
+(*partial function as procedure*)
+fun try f x =
+ make (fn () =>
+ case Library.try f x of
+ SOME y => SOME(y,Seq (value NONE))
+ | NONE => NONE)
+
+(*functional to print a sequence, up to "count" elements;
+ the function prelem should print the element number and also the element*)
+fun print prelem count seq =
+ let
+ fun pr k xq =
+ if k > count
+ then ()
+ else
+ case getItem xq of
+ NONE => ()
+ | SOME (x, xq') =>
+ (prelem k x;
+ writeln "";
+ pr (k + 1) xq')
+ in
+ pr 1 seq
+ end
+
+(*accumulating a function over a sequence; this is lazy*)
+fun it_right f (xq, yq) =
+ let
+ fun its s =
+ make (fn () =>
+ case getItem s of
+ NONE => getItem yq
+ | SOME (a, s') => getItem(f (a, its s')))
+ in
+ its xq
+ end
+
+(*map over a sequence s1, append the sequence s2*)
+fun mapp f s1 s2 =
+ let
+ fun F NONE = getItem s2
+ | F (SOME(x,s1')) = SOME(f x,F' s1')
+ and F' s = make (fn () => F (getItem s))
+ in
+ F' s1
+ end
+
+(*turn a list of sequences into a sequence of lists*)
+local
+ fun F [] = SOME([],Seq (value NONE))
+ | F (xq :: xqs) =
+ case getItem xq of
+ NONE => NONE
+ | SOME (x, xq') =>
+ (case F xqs of
+ NONE => NONE
+ | SOME (xs, xsq) =>
+ let
+ fun G s =
+ make (fn () =>
+ case getItem s of
+ NONE => F (xq' :: xqs)
+ | SOME(ys,ysq) => SOME(x::ys,G ysq))
+ in
+ SOME (x :: xs, G xsq)
+ end)
+in
+fun commute xqs = make (fn () => F xqs)
+end
+
+(*the list of the first n elements, paired with rest of sequence;
+ if length of list is less than n, then sequence had less than n elements*)
+fun chop (n, xq) =
+ if n <= 0
+ then ([], xq)
+ else
+ case getItem xq of
+ NONE => ([], xq)
+ | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
+
+fun foldl f e s =
+ let
+ fun F k NONE = k e
+ | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
+ in
+ F (fn x => x) (getItem s)
+ end
+
+fun foldr f e s =
+ let
+ fun F e NONE = e
+ | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
+ in
+ F e (getItem s)
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/susp.ML Sat Oct 08 22:39:40 2005 +0200
@@ -0,0 +1,41 @@
+(* Title: HOL/Import/susp.ML
+ ID: $Id$
+ Author: Sebastian Skalberg, TU Muenchen
+
+Delayed evaluation.
+*)
+
+signature SUSP =
+sig
+
+type 'a susp
+
+val force : 'a susp -> 'a
+val delay : (unit -> 'a) -> 'a susp
+val value : 'a -> 'a susp
+
+end
+
+structure Susp :> SUSP =
+struct
+
+datatype 'a suspVal
+ = Value of 'a
+ | Delay of unit -> 'a
+
+type 'a susp = 'a suspVal ref
+
+fun force (ref (Value v)) = v
+ | force (r as ref (Delay f)) =
+ let
+ val v = f ()
+ in
+ r := Value v;
+ v
+ end
+
+fun delay f = ref (Delay f)
+
+fun value v = ref (Value v)
+
+end
--- a/src/Pure/General/ROOT.ML Sat Oct 08 22:39:39 2005 +0200
+++ b/src/Pure/General/ROOT.ML Sat Oct 08 22:39:40 2005 +0200
@@ -16,9 +16,6 @@
use "symbol.ML";
use "name_space.ML";
use "seq.ML";
-use "susp.ML";
-use "lazy_seq.ML";
-use "lazy_scan.ML";
use "position.ML";
use "path.ML";
use "url.ML";
--- a/src/Pure/General/lazy_scan.ML Sat Oct 08 22:39:39 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,206 +0,0 @@
-(* Title: Pure/General/lazy_scan.ML
- ID: $Id$
- Author: Sebastian Skalberg, TU Muenchen
-
-Scanner combinators for lazy sequences.
-*)
-
-signature LAZY_SCAN =
-sig
-
- exception SyntaxError
-
- type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
-
- val :-- : ('a,'b) scanner * ('b -> ('a,'c) scanner)
- -> ('a,'b*'c) scanner
- val -- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
- val >> : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
- val --| : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
- val |-- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
- val ^^ : ('a,string) scanner * ('a,string) scanner
- -> ('a,string) scanner
- val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
- val one : ('a -> bool) -> ('a,'a) scanner
- val succeed : 'b -> ('a,'b) scanner
- val any : ('a -> bool) -> ('a,'a list) scanner
- val any1 : ('a -> bool) -> ('a,'a list) scanner
- val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
- val option : ('a,'b) scanner -> ('a,'b option) scanner
- val repeat : ('a,'b) scanner -> ('a,'b list) scanner
- val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner
- val ahead : ('a,'b) scanner -> ('a,'b) scanner
- val unless : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner
- val $$ : ''a -> (''a,''a) scanner
- val !! : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
- val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
-
-end
-
-structure LazyScan :> LAZY_SCAN =
-struct
-
-infix 7 |-- --|
-infix 5 :-- -- ^^
-infix 3 >>
-infix 0 ||
-
-exception SyntaxError
-exception Fail of string
-
-type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
-
-fun (sc1 :-- sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 x toks2
- in
- ((x,y),toks3)
- end
-
-fun (sc1 -- sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 toks2
- in
- ((x,y),toks3)
- end
-
-fun (sc >> f) toks =
- let
- val (x,toks2) = sc toks
- in
- (f x,toks2)
- end
-
-fun (sc1 --| sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (_,toks3) = sc2 toks2
- in
- (x,toks3)
- end
-
-fun (sc1 |-- sc2) toks =
- let
- val (_,toks2) = sc1 toks
- in
- sc2 toks2
- end
-
-fun (sc1 ^^ sc2) toks =
- let
- val (x,toks2) = sc1 toks
- val (y,toks3) = sc2 toks2
- in
- (x^y,toks3)
- end
-
-fun (sc1 || sc2) toks =
- (sc1 toks)
- handle SyntaxError => sc2 toks
-
-fun one p toks =
- case LazySeq.getItem toks of
- NONE => raise SyntaxError
- | SOME(t,toks) => if p t
- then (t,toks)
- else raise SyntaxError
-
-fun succeed e toks = (e,toks)
-
-fun any p toks =
- case LazySeq.getItem toks of
- NONE => ([],toks)
- | SOME(x,toks2) => if p x
- then
- let
- val (xs,toks3) = any p toks2
- in
- (x::xs,toks3)
- end
- else ([],toks)
-
-fun any1 p toks =
- let
- val (x,toks2) = one p toks
- val (xs,toks3) = any p toks2
- in
- (x::xs,toks3)
- end
-
-fun optional sc def = sc || succeed def
-fun option sc = (sc >> SOME) || succeed NONE
-
-(*
-fun repeat sc =
- let
- fun R toks =
- let
- val (x,toks2) = sc toks
- val (xs,toks3) = R toks2
- in
- (x::xs,toks3)
- end
- handle SyntaxError => ([],toks)
- in
- R
- end
-*)
-
-(* A tail-recursive version of repeat. It is (ever so) slightly slower
- * than the above, non-tail-recursive version (due to the garbage generation
- * associated with the reversal of the list). However, this version will be
- * able to process input where the former version must give up (due to stack
- * overflow). The slowdown seems to be around the one percent mark.
- *)
-fun repeat sc =
- let
- fun R xs toks =
- case SOME (sc toks) handle SyntaxError => NONE of
- SOME (x,toks2) => R (x::xs) toks2
- | NONE => (List.rev xs,toks)
- in
- R []
- end
-
-fun repeat1 sc toks =
- let
- val (x,toks2) = sc toks
- val (xs,toks3) = repeat sc toks2
- in
- (x::xs,toks3)
- end
-
-fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
-
-fun unless test sc toks =
- let
- val test_failed = (test toks;false) handle SyntaxError => true
- in
- if test_failed
- then sc toks
- else raise SyntaxError
- end
-
-fun $$ arg = one (fn x => x = arg)
-
-fun !! f sc toks = (sc toks
- handle SyntaxError => raise Fail (f toks))
-
-fun scan_full sc toks =
- let
- fun F toks =
- if LazySeq.null toks
- then NONE
- else
- let
- val (x,toks') = sc toks
- in
- SOME(x,LazySeq.make (fn () => F toks'))
- end
- in
- LazySeq.make (fn () => F toks)
- end
-
-end
--- a/src/Pure/General/lazy_seq.ML Sat Oct 08 22:39:39 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,543 +0,0 @@
-(* Title: Pure/General/lazy_seq.ML
- ID: $Id$
- Author: Sebastian Skalberg, TU Muenchen
-
-Alternative version of lazy sequences.
-*)
-
-signature LAZY_SEQ =
-sig
-
- type 'a seq
-
- (* From LIST *)
-
- val null : 'a seq -> bool
- val length : 'a seq -> int
- val @ : 'a seq * 'a seq -> 'a seq
- val hd : 'a seq -> 'a
- val tl : 'a seq -> 'a seq
- val last : 'a seq -> 'a
- val getItem : 'a seq -> ('a * 'a seq) option
- val nth : 'a seq * int -> 'a
- val take : 'a seq * int -> 'a seq
- val drop : 'a seq * int -> 'a seq
- val rev : 'a seq -> 'a seq
- val concat : 'a seq seq -> 'a seq
- val revAppend : 'a seq * 'a seq -> 'a seq
- val app : ('a -> unit) -> 'a seq -> unit
- val map : ('a -> 'b) -> 'a seq -> 'b seq
- val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
- val find : ('a -> bool) -> 'a seq -> 'a option
- val filter : ('a -> bool) -> 'a seq -> 'a seq
- val partition : ('a -> bool)
- -> 'a seq -> 'a seq * 'a seq
- val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
- val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
- val exists : ('a -> bool) -> 'a seq -> bool
- val all : ('a -> bool) -> 'a seq -> bool
- val tabulate : int * (int -> 'a) -> 'a seq
- val collate : ('a * 'a -> order)
- -> 'a seq * 'a seq -> order
-
- (* Miscellaneous *)
-
- val cycle : ((unit ->'a seq) -> 'a seq) -> 'a seq
- val iterates : ('a -> 'a) -> 'a -> 'a seq
- val of_function: (unit -> 'a option) -> 'a seq
- val of_string : string -> char seq
- val of_instream: TextIO.instream -> char seq
-
- (* From SEQ *)
-
- val make: (unit -> ('a * 'a seq) option) -> 'a seq
- val empty: 'a -> 'a seq
- val cons: 'a * 'a seq -> 'a seq
- val single: 'a -> 'a seq
- val try: ('a -> 'b) -> 'a -> 'b seq
- val chop: int * 'a seq -> 'a list * 'a seq
- val list_of: 'a seq -> 'a list
- val of_list: 'a list -> 'a seq
- val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
- val interleave: 'a seq * 'a seq -> 'a seq
- val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
- val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
- val commute: 'a seq list -> 'a list seq
- val succeed: 'a -> 'a seq
- val fail: 'a -> 'b seq
- val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
- val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
- val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
- val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
- val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
- val TRY: ('a -> 'a seq) -> 'a -> 'a seq
- val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
- val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
- val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
- val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
-
-end
-
-structure LazySeq :> LAZY_SEQ =
-struct
-
-open Susp
-
-datatype 'a seq = Seq of ('a * 'a seq) option susp
-
-exception Empty
-
-fun getItem (Seq s) = force s
-fun make f = Seq (delay f)
-
-fun null s = isSome (getItem s)
-
-local
- fun F n NONE = n
- | F n (SOME(_,s)) = F (n+1) (getItem s)
-in
-fun length s = F 0 (getItem s)
-end
-
-fun s1 @ s2 =
- let
- fun F NONE = getItem s2
- | F (SOME(x,s1')) = SOME(x,F' s1')
- and F' s = make (fn () => F (getItem s))
- in
- F' s1
- end
-
-local
- fun F NONE = raise Empty
- | F (SOME arg) = arg
-in
-fun hd s = #1 (F (getItem s))
-fun tl s = #2 (F (getItem s))
-end
-
-local
- fun F x NONE = x
- | F _ (SOME(x,s)) = F x (getItem s)
- fun G NONE = raise Empty
- | G (SOME(x,s)) = F x (getItem s)
-in
-fun last s = G (getItem s)
-end
-
-local
- fun F NONE _ = raise Subscript
- | F (SOME(x,_)) 0 = x
- | F (SOME(_,s)) n = F (getItem s) (n-1)
-in
-fun nth(s,n) =
- if n < 0
- then raise Subscript
- else F (getItem s) n
-end
-
-local
- fun F NONE _ = raise Subscript
- | F (SOME(x,s)) n = SOME(x,F' s (n-1))
- and F' s 0 = Seq (value NONE)
- | F' s n = make (fn () => F (getItem s) n)
-in
-fun take (s,n) =
- if n < 0
- then raise Subscript
- else F' s n
-end
-
-local
- fun F s 0 = s
- | F NONE _ = raise Subscript
- | F (SOME(_,s)) n = F (getItem s) (n-1)
-in
-fun drop (s,0) = s
- | drop (s,n) =
- if n < 0
- then raise Subscript
- else make (fn () => F (getItem s) n)
-end
-
-local
- fun F s NONE = s
- | F s (SOME(x,s')) = F (SOME(x, Seq (value s))) (getItem s')
-in
-fun rev s = make (fn () => F NONE (getItem s))
-end
-
-local
- fun F s NONE = getItem s
- | F s (SOME(x,s')) = F (Seq (value (SOME(x,s)))) (getItem s')
-in
-fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
-end
-
-local
- fun F NONE = NONE
- | F (SOME(s1,s2)) =
- let
- fun G NONE = F (getItem s2)
- | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
- in
- G (getItem s1)
- end
-in
-fun concat s = make (fn () => F (getItem s))
-end
-
-fun app f =
- let
- fun F NONE = ()
- | F (SOME(x,s)) =
- (f x;
- F (getItem s))
- in
- F o getItem
- end
-
-fun map f =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) = SOME(f x,F' s)
- and F' s = make (fn() => F (getItem s))
- in
- F'
- end
-
-fun mapPartial f =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) =
- (case f x of
- SOME y => SOME(y,F' s)
- | NONE => F (getItem s))
- and F' s = make (fn()=> F (getItem s))
- in
- F'
- end
-
-fun find P =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) =
- if P x
- then SOME x
- else F (getItem s)
- in
- F o getItem
- end
-
-(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
-
-fun filter P =
- let
- fun F NONE = NONE
- | F (SOME(x,s)) =
- if P x
- then SOME(x,F' s)
- else F (getItem s)
- and F' s = make (fn () => F (getItem s))
- in
- F'
- end
-
-fun partition f s =
- let
- val s' = map (fn x => (x,f x)) s
- in
- (mapPartial (fn (x,true) => SOME x | _ => NONE) s',
- mapPartial (fn (x,false) => SOME x | _ => NONE) s')
- end
-
-fun exists P =
- let
- fun F NONE = false
- | F (SOME(x,s)) = P x orelse F (getItem s)
- in
- F o getItem
- end
-
-fun all P =
- let
- fun F NONE = true
- | F (SOME(x,s)) = P x andalso F (getItem s)
- in
- F o getItem
- end
-
-(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
-
-fun tabulate (n,f) =
- let
- fun F n = make (fn () => SOME(f n,F (n+1)))
- in
- F n
- end
-
-fun collate c (s1,s2) =
- let
- fun F NONE _ = LESS
- | F _ NONE = GREATER
- | F (SOME(x,s1)) (SOME(y,s2)) =
- (case c (x,y) of
- LESS => LESS
- | GREATER => GREATER
- | EQUAL => F' s1 s2)
- and F' s1 s2 = F (getItem s1) (getItem s2)
- in
- F' s1 s2
- end
-
-fun empty _ = Seq (value NONE)
-fun single x = Seq(value (SOME(x,Seq (value NONE))))
-fun cons a = Seq(value (SOME a))
-
-fun cycle seqfn =
- let
- val knot = ref (Seq (value NONE))
- in
- knot := seqfn (fn () => !knot);
- !knot
- end
-
-fun iterates f =
- let
- fun F x = make (fn() => SOME(x,F (f x)))
- in
- F
- end
-
-fun interleave (s1,s2) =
- let
- fun F NONE = getItem s2
- | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
- in
- make (fn()=> F (getItem s1))
- end
-
-(* val force_all = app ignore *)
-
-local
- fun F NONE = ()
- | F (SOME(x,s)) = F (getItem s)
-in
-fun force_all s = F (getItem s)
-end
-
-fun of_function f =
- let
- fun F () = case f () of
- SOME x => SOME(x,make F)
- | NONE => NONE
- in
- make F
- end
-
-local
- fun F [] = NONE
- | F (x::xs) = SOME(x,F' xs)
- and F' xs = make (fn () => F xs)
-in
-fun of_list xs = F' xs
-end
-
-val of_string = of_list o String.explode
-
-fun of_instream is =
- let
- val buffer : char list ref = ref []
- fun get_input () =
- case !buffer of
- (c::cs) => (buffer:=cs;
- SOME c)
- | [] => (case String.explode (TextIO.input is) of
- [] => NONE
- | (c::cs) => (buffer := cs;
- SOME c))
- in
- of_function get_input
- end
-
-local
- fun F k NONE = k []
- | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
-in
-fun list_of s = F (fn x => x) (getItem s)
-end
-
-(* Adapted from seq.ML *)
-
-val succeed = single
-fun fail _ = Seq (value NONE)
-
-(* fun op THEN (f, g) x = flat (map g (f x)) *)
-
-fun op THEN (f, g) =
- let
- fun F NONE = NONE
- | F (SOME(x,xs)) =
- let
- fun G NONE = F (getItem xs)
- | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
- in
- G (getItem (g x))
- end
- in
- fn x => make (fn () => F (getItem (f x)))
- end
-
-fun op ORELSE (f, g) x =
- make (fn () =>
- case getItem (f x) of
- NONE => getItem (g x)
- | some => some)
-
-fun op APPEND (f, g) x =
- let
- fun copy s =
- case getItem s of
- NONE => getItem (g x)
- | SOME(x,xs) => SOME(x,make (fn () => copy xs))
- in
- make (fn () => copy (f x))
- end
-
-fun EVERY fs = foldr THEN succeed fs
-fun FIRST fs = foldr ORELSE fail fs
-
-fun TRY f x =
- make (fn () =>
- case getItem (f x) of
- NONE => SOME(x,Seq (value NONE))
- | some => some)
-
-fun REPEAT f =
- let
- fun rep qs x =
- case getItem (f x) of
- NONE => SOME(x, make (fn () => repq qs))
- | SOME (x', q) => rep (q :: qs) x'
- and repq [] = NONE
- | repq (q :: qs) =
- case getItem q of
- NONE => repq qs
- | SOME (x, q) => rep (q :: qs) x
- in
- fn x => make (fn () => rep [] x)
- end
-
-fun REPEAT1 f = THEN (f, REPEAT f);
-
-fun INTERVAL f i =
- let
- fun F j =
- if i > j
- then single
- else op THEN (f j, F (j - 1))
- in F end
-
-fun DETERM f x =
- make (fn () =>
- case getItem (f x) of
- NONE => NONE
- | SOME (x', _) => SOME(x',Seq (value NONE)))
-
-(*partial function as procedure*)
-fun try f x =
- make (fn () =>
- case Library.try f x of
- SOME y => SOME(y,Seq (value NONE))
- | NONE => NONE)
-
-(*functional to print a sequence, up to "count" elements;
- the function prelem should print the element number and also the element*)
-fun print prelem count seq =
- let
- fun pr k xq =
- if k > count
- then ()
- else
- case getItem xq of
- NONE => ()
- | SOME (x, xq') =>
- (prelem k x;
- writeln "";
- pr (k + 1) xq')
- in
- pr 1 seq
- end
-
-(*accumulating a function over a sequence; this is lazy*)
-fun it_right f (xq, yq) =
- let
- fun its s =
- make (fn () =>
- case getItem s of
- NONE => getItem yq
- | SOME (a, s') => getItem(f (a, its s')))
- in
- its xq
- end
-
-(*map over a sequence s1, append the sequence s2*)
-fun mapp f s1 s2 =
- let
- fun F NONE = getItem s2
- | F (SOME(x,s1')) = SOME(f x,F' s1')
- and F' s = make (fn () => F (getItem s))
- in
- F' s1
- end
-
-(*turn a list of sequences into a sequence of lists*)
-local
- fun F [] = SOME([],Seq (value NONE))
- | F (xq :: xqs) =
- case getItem xq of
- NONE => NONE
- | SOME (x, xq') =>
- (case F xqs of
- NONE => NONE
- | SOME (xs, xsq) =>
- let
- fun G s =
- make (fn () =>
- case getItem s of
- NONE => F (xq' :: xqs)
- | SOME(ys,ysq) => SOME(x::ys,G ysq))
- in
- SOME (x :: xs, G xsq)
- end)
-in
-fun commute xqs = make (fn () => F xqs)
-end
-
-(*the list of the first n elements, paired with rest of sequence;
- if length of list is less than n, then sequence had less than n elements*)
-fun chop (n, xq) =
- if n <= 0
- then ([], xq)
- else
- case getItem xq of
- NONE => ([], xq)
- | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
-
-fun foldl f e s =
- let
- fun F k NONE = k e
- | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
- in
- F (fn x => x) (getItem s)
- end
-
-fun foldr f e s =
- let
- fun F e NONE = e
- | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
- in
- F e (getItem s)
- end
-
-end
--- a/src/Pure/General/susp.ML Sat Oct 08 22:39:39 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: Pure/General/susp.ML
- ID: $Id$
- Author: Sebastian Skalberg, TU Muenchen
-
-Delayed evaluation.
-*)
-
-signature SUSP =
-sig
-
-type 'a susp
-
-val force : 'a susp -> 'a
-val delay : (unit -> 'a) -> 'a susp
-val value : 'a -> 'a susp
-
-end
-
-structure Susp :> SUSP =
-struct
-
-datatype 'a suspVal
- = Value of 'a
- | Delay of unit -> 'a
-
-type 'a susp = 'a suspVal ref
-
-fun force (ref (Value v)) = v
- | force (r as ref (Delay f)) =
- let
- val v = f ()
- in
- r := Value v;
- v
- end
-
-fun delay f = ref (Delay f)
-
-fun value v = ref (Value v)
-
-end
--- a/src/Pure/IsaMakefile Sat Oct 08 22:39:39 2005 +0200
+++ b/src/Pure/IsaMakefile Sat Oct 08 22:39:40 2005 +0200
@@ -21,15 +21,15 @@
## Pure
-Pure: $(OUT)/Pure
+Pure: $(OUT)/Pure$(ML_SUFFIX)
-$(OUT)/Pure: CPure.thy General/ROOT.ML General/alist.ML \
+$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \
General/buffer.ML \
General/file.ML General/graph.ML General/heap.ML General/history.ML \
- General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML \
+ General/name_space.ML \
General/ord_list.ML General/output.ML General/path.ML \
General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
- General/source.ML General/stack.ML General/susp.ML General/symbol.ML \
+ General/source.ML General/stack.ML General/symbol.ML \
General/table.ML General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML \
IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML \
IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML \
@@ -44,7 +44,7 @@
Isar/proof_history.ML Isar/rule_cases.ML Isar/session.ML \
Isar/skip_proof.ML Isar/term_style.ML Isar/thy_header.ML \
Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML \
- ML-Systems/cpu-timer-gc.ML \
+ ML-Systems/cpu-timer-gc.ML ML-Systems/poplogml.ML \
ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML \
ML-Systems/polyml-posix.ML ML-Systems/smlnj-basis-compat.ML \
ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-ptreql.ML \
@@ -82,4 +82,4 @@
## clean
clean:
- @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz
+ @rm -f $(OUT)/Pure$(ML_SUFFIX) $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz