src/Pure/Thy/scan.ML
author paulson
Tue, 22 Jul 1997 11:14:18 +0200
changeset 3538 ed9de44032e0
parent 213 42f2b8a3581f
permissions -rw-r--r--
Removal of the tactical STATE
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	Pure/Thy/scan
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Sonia Mahjoub / Tobias Nipkow
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  TU Muenchen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
     6
    modified    December 1993 by Max Breitling (Type-variables added)
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
     7
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
The scanner. Adapted from Larry Paulson's ML for the Working Programmer.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
signature LEXICAL =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
datatype token = Id  of string 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
               | Key of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
               | Nat of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
               | Stg of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
               | Txt of string
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
    20
               | TypVar of string
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val scan : string list -> (token * int) list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
signature KEYWORD = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val alphas  : string list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val symbols : string list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
functor LexicalFUN (Keyword: KEYWORD): LEXICAL = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
datatype token = Id  of string 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
               | Key of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
               | Nat of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
               | Stg of string
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
    42
               | Txt of string
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
    43
               | TypVar of string;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
fun lexerr(n,s) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
    error("Lexical error on line " ^ (string_of_int n) ^ ": " ^ s);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
    49
val specials = explode"!{}@#$%^&*()+-=[]:\";,./?`_~<>|\\";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
fun is_symbol c = "_" = c orelse "'" = c;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
fun alphanum (id, c::cs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
       if is_letter c orelse is_digit c orelse is_symbol c
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
       then alphanum (id ^ c , cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
       else (id , c :: cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  | alphanum (id ,[]) = (id ,[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
fun numeric (nat, c::cs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
      if is_digit c 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
      then numeric (nat^c, cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
      else (nat, c::cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  | numeric (nat, []) = (nat,[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
fun tokenof (a, n) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
      if a mem Keyword.alphas
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
      then (Key a, n) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
      else (Id a, n);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
fun symbolic (sy, c::cs) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
       if (sy mem Keyword.symbols) andalso 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
          not((sy^c) mem Keyword.symbols) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
          orelse not (c mem specials)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
       then (sy, c::cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
       else symbolic(sy^c, cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  | symbolic (sy, []) = (sy, []);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
fun stringerr(n) = lexerr(n, "No matching quote found on this line");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
fun is_control_chr ([],_,n) = stringerr(n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  | is_control_chr (c::cs,s,n) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
          let val m = ord c
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
          in if (m >= 64 andalso m <= 95)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
             then (cs, s^c, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
             else stringerr(n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
          end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
fun is_3_dgt (c1::c2::cs, c,n) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
          let val s = c^c1^c2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
          in  if (s >= "000" andalso s <= "255")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
              then (cs, s)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
              else stringerr(n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
          end 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  | is_3_dgt (_,_,n) = stringerr(n); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
fun is_imprt_seq ([],_,n) = stringerr(n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  | is_imprt_seq ((c::cs),s,n) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
          if c = "\\" then (cs,s^"\\",n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
          else if c = "\n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
               then is_imprt_seq (cs,s^"\n",n+1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
          else if (c = "\t") orelse (c = " ")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
               then is_imprt_seq (cs,s^c,n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
          else stringerr(n);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
fun is_escape_seq ([],_,n) = stringerr(n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
  | is_escape_seq ((c::cs),s,n) =  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
          if c = "\\" then (cs,s^"\\",n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
          else if c = "\n" 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
               then is_imprt_seq (cs,s^"\n",n+1) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
          else if (c = "\t") orelse (c = " ")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
               then is_imprt_seq (cs,s^c,n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
          else if c = "^" 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
               then is_control_chr (cs,s^"^",n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
          else if ("0" <= c andalso c <= "2") 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
               then let val (cs',s') = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
                            is_3_dgt(cs,c,n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
                    in (cs',s^s',n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
                    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
          else stringerr(n);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
fun string (_,[],_,n) = stringerr(n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
  | string (toks, c::cs, s, n) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
       if c  = "\"" then ((Stg s, n)::toks , cs, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
       else if c = "\\" 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
            then  let val (cs',s',n') = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
                          is_escape_seq (cs, s^"\\",n) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
                  in string (toks,cs',s',n') end 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
       else string (toks,cs,s^c,n);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
fun comment ((c1::c2::cs), n) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
      if c1 = "*" andalso c2 = ")" then (cs,n) else
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
      if c1 = "\n" then comment((c2::cs), n+1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
      else comment((c2::cs), n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
  | comment (_, n) = lexerr(n, "Missing end of comment");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
fun scanning (toks , [], n) = rev toks
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
  | scanning (toks , c :: cs, n) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
       if is_letter c 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
       then let val (id , cs2) = alphanum (c , cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
            in if id = "ML"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
               then let val text = implode cs2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
                    in  scanning ((Txt text,n) :: toks , [], n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
                    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
               else scanning (tokenof(id,n) :: toks , cs2, n) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
            end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
       else if is_digit c 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
            then let val (nat , cs2) = numeric(c , cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
                 in scanning ((Nat nat,n) :: toks , cs2, n) end
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   151
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   152
       else if c = "'" andalso is_letter(hd cs)
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   153
            then let val (var, cs2) = alphanum (hd cs, tl cs)
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   154
                 in scanning((TypVar (c^var),n) :: toks, cs2, n) end
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   155
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
       else if c mem specials
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
            then if c = "\""
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
                 then let val (toks', cs', n') = string (toks, cs, "", n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
                      in scanning (toks', cs', n') end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
                 else let val (sy , cs2) = symbolic (c , cs)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
                      in if sy = "(*"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
                         then let val (cs3,n2) = comment(cs2,n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
                              in scanning (toks , cs3, n2) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
                         else scanning ((Key sy,n) :: toks, cs2, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
                      end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
       else if c = "\n" then scanning (toks, cs, n+1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
       else if c = " " orelse c = "\t" then scanning (toks , cs, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
       else lexerr(n,"Illegal character " ^ c);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
fun scan a = scanning ([] , a, 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
end;