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