src/Pure/General/lazy_scan.ML
author wenzelm
Wed, 09 Jun 2004 18:52:42 +0200
changeset 14898 a25550451b51
parent 14278 ae499452700a
child 15531 08c8dad8e399
permissions -rw-r--r--
Url.File;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     1
(* $Id$ *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     3
signature LAZY_SCAN =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     4
sig
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     5
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     6
    exception SyntaxError
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     7
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     8
    type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     9
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    10
    val :--      : ('a,'b) scanner * ('b -> ('a,'c) scanner)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    11
		   -> ('a,'b*'c) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    12
    val --       : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    13
    val >>       : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    14
    val --|      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    15
    val |--      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    16
    val ^^       : ('a,string) scanner * ('a,string) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    17
		   -> ('a,string) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    18
    val ||       : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    19
    val one      : ('a -> bool) -> ('a,'a) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    20
    val succeed  : 'b -> ('a,'b) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    21
    val any      : ('a -> bool) -> ('a,'a list) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    22
    val any1     : ('a -> bool) -> ('a,'a list) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    23
    val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    24
    val option   : ('a,'b) scanner -> ('a,'b option) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    25
    val repeat   : ('a,'b) scanner -> ('a,'b list) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    26
    val repeat1  : ('a,'b) scanner -> ('a,'b list) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    27
    val ahead    : ('a,'b) scanner -> ('a,'b) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    28
    val unless   : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    29
    val $$       : ''a -> (''a,''a) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    30
    val !!       : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    31
    val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    32
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    33
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    34
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    35
structure LazyScan :> LAZY_SCAN =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    36
struct
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    37
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    38
infix 7 |-- --|
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    39
infix 5 :-- -- ^^
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    40
infix 3 >>
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    41
infix 0 ||
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    42
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    43
exception SyntaxError
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    44
exception Fail of string
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    45
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    46
type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    47
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    48
fun (sc1 :-- sc2) toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    49
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    50
	val (x,toks2) = sc1 toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    51
	val (y,toks3) = sc2 x toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    52
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    53
	((x,y),toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    54
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    55
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    56
fun (sc1 -- sc2) toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    57
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    58
	val (x,toks2) = sc1 toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    59
	val (y,toks3) = sc2 toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    60
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    61
	((x,y),toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    62
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    63
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    64
fun (sc >> f) toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    65
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    66
	val (x,toks2) = sc toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    67
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    68
	(f x,toks2)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    69
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    70
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    71
fun (sc1 --| sc2) toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    72
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    73
	val (x,toks2) = sc1 toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    74
	val (_,toks3) = sc2 toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    75
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    76
	(x,toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    77
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    78
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    79
fun (sc1 |-- sc2) toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    80
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    81
	val (_,toks2) = sc1 toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    82
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    83
	sc2 toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    84
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    85
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    86
fun (sc1 ^^ sc2) toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    87
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    88
	val (x,toks2) = sc1 toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    89
	val (y,toks3) = sc2 toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    90
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    91
	(x^y,toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    92
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    93
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    94
fun (sc1 || sc2) toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    95
    (sc1 toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    96
    handle SyntaxError => sc2 toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    97
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    98
fun one p toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    99
    case LazySeq.getItem toks of
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   100
	None => raise SyntaxError
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   101
      | Some(t,toks) => if p t
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   102
			then (t,toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   103
			else raise SyntaxError
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   104
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   105
fun succeed e toks = (e,toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   106
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   107
fun any p toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   108
    case LazySeq.getItem toks of
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   109
	None =>  ([],toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   110
      | Some(x,toks2) => if p x
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   111
			 then
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   112
			     let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   113
				 val (xs,toks3) = any p toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   114
			     in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   115
				 (x::xs,toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   116
			     end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   117
			 else ([],toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   118
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   119
fun any1 p toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   120
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   121
	val (x,toks2) = one p toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   122
	val (xs,toks3) = any p toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   123
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   124
	(x::xs,toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   125
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   126
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   127
fun optional sc def =  sc || succeed def
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   128
fun option sc = (sc >> Some) || succeed None
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   129
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   130
(*
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   131
fun repeat sc =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   132
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   133
	fun R toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   134
	    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   135
		val (x,toks2) = sc toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   136
		val (xs,toks3) = R toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   137
	    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   138
		(x::xs,toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   139
	    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   140
	    handle SyntaxError => ([],toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   141
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   142
	R
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   143
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   144
*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   145
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   146
(* A tail-recursive version of repeat.  It is (ever so) slightly slower
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   147
 * than the above, non-tail-recursive version (due to the garbage generation
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   148
 * associated with the reversal of the list).  However,  this version will be
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   149
 * able to process input where the former version must give up (due to stack
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   150
 * overflow).  The slowdown seems to be around the one percent mark.
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   151
 *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   152
fun repeat sc =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   153
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   154
	fun R xs toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   155
	    case Some (sc toks) handle SyntaxError => None of
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   156
		Some (x,toks2) => R (x::xs) toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   157
	      | None => (List.rev xs,toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   158
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   159
	R []
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   160
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   161
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   162
fun repeat1 sc toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   163
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   164
	val (x,toks2) = sc toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   165
	val (xs,toks3) = repeat sc toks2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   166
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   167
	(x::xs,toks3)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   168
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   169
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   170
fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   171
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   172
fun unless test sc toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   173
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   174
	val test_failed = (test toks;false) handle SyntaxError => true
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   175
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   176
	if test_failed
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   177
	then sc toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   178
	else raise SyntaxError
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   179
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   180
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   181
fun $$ arg = one (fn x => x = arg)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   182
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   183
fun !! f sc toks = (sc toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   184
		    handle SyntaxError => raise Fail (f toks))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   185
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   186
fun scan_full sc toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   187
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   188
	fun F toks =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   189
	    if LazySeq.null toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   190
	    then None
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   191
	    else
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   192
		let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   193
		    val (x,toks') = sc toks
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   194
		in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   195
		    Some(x,LazySeq.make (fn () => F toks'))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   196
		end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   197
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   198
	LazySeq.make (fn () => F toks)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   199
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   200
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   201
end