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