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