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