--- /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