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