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