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