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