src/Pure/Thy/parse.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/parse
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    Dezember 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 parser combinators.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
Adapted from Larry Paulson's ML for the Working Programmer.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
(*Global infix declarations for the parsing primitives*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
infix 5 -- --$$ $$--;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
infix 3 >>;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
infix 0 ||;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
signature PARSE = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
type token
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
val $$     : string -> 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
             (token * int) list -> string * (token * int)list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
val id     : (token * int) list -> string * (token * int)list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
val nat    : (token * int) list -> string * (token * int)list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
val stg    : (token * int) list -> string * (token * int)list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val txt    : (token * int) list -> string * (token * int)list 
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
    28
val typevar: (token * int) list -> string * (token * int)list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val >>     : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val ||     : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val --     : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
             'a -> ('b * 'd) * 'e
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val $$--   : string * ((token * int)list -> 'b * 'c) -> 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
             (token * int) list -> 'b * 'c
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
val --$$   : ( 'a -> 'b * (token * int)list ) * string -> 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
             'a -> 'b * (token * int)list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val !!     : ((token * int) list -> 'a * (token * int) list ) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
             -> (token * int) list -> 'a * (token * int) list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val empty  : 'a -> 'b list * 'a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val list_of: ((token * int)list -> 'b * (token * int)list ) -> 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
             (token * int)list  -> 'b list * (token * int)list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
val list_of1: ((token * int)list -> 'b * (token * int)list ) -> 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
             (token * int)list  -> 'b list * (token * int)list 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val reader : ((token * int) list -> 'a * ('b * int) list )
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
              -> string list -> 'a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
functor ParseFUN (Lex: LEXICAL): PARSE =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
type token = Lex.token;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
datatype synerr = Line of string * string * int | EOF of string;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
exception SynError of synerr;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
fun synerr(Line(s1, s2, n)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
      error("Syntax error on line " ^ (string_of_int n) ^ ": " ^ s1 ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
            " expected and " ^ s2 ^ " was found")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
  | synerr(EOF(s)) = error("Syntax error on last line: " ^ s ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
                           " expected and end-of-file was found"); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
fun string_of_token (Lex.Key b) = b
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  | string_of_token (Lex.Id b)  = b
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
  | string_of_token (Lex.Nat b) = b
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  | string_of_token (Lex.Txt b) = b
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
    72
  | string_of_token (Lex.Stg b) = b
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
    73
  | string_of_token (Lex.TypVar b) = b;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
fun line_err x = raise SynError(Line x);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
fun eof_err s =  raise SynError(EOF s);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
fun $$a ((Lex.Key b,n) :: toks) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
           if a = b then (a,toks) else line_err(a,b,n) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
  | $$a ((t,n) :: toks) = line_err (a,string_of_token t, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  | $$a _ = eof_err a;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
fun id ((Lex.Id b,n) :: toks) = (b, toks)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  | id ((t,n) :: toks) = line_err ("identifier", string_of_token t, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  | id _ = eof_err "identifier";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
fun nat ((Lex.Nat b,n) :: toks) = (b, toks)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
  | nat ((t,n) :: toks) = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
	line_err ("natural number", string_of_token t, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
  | nat _ = eof_err "natural number";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
fun stg ((Lex.Stg b,n) :: toks) = (b, toks)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
  | stg ((t,n) :: toks) = line_err("string", string_of_token t, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  | stg _ = eof_err"string";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
fun txt ((Lex.Txt b,n) :: toks) = (b, toks)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
  | txt ((t,n) :: toks) = line_err ("ML text", string_of_token t, n)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
  | txt _ = eof_err "ML text";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
213
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   104
fun typevar ((Lex.TypVar b,n) :: toks) = (b, toks)
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   105
  | typevar ((t,n)::toks) = line_err("type variable",string_of_token t,n)
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   106
  | typevar _ = eof_err "type variable";
42f2b8a3581f added lexical class of type variables
nipkow
parents: 0
diff changeset
   107
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
fun ( ph >> f) toks = let val (x, toks2) = ph toks in (f x, toks2) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
fun (ph1 || ph2) toks = ph1 toks handle SynError _ => ph2 toks;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
fun (ph1 -- ph2) toks =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
    let val (x, toks2) = ph1 toks
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
        val (y, toks3) = ph2 toks2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    in ((x,y), toks3) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
fun (a $$-- ph)  =  $$a -- ph >> #2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
fun (ph --$$ a)  =  ph -- $$a >> #1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
fun !! ph toks = ph toks handle SynError s => synerr s;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
fun empty toks = ([], toks);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
fun repeat ph toks  = (   ph -- repeat ph >> (op::)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
                       || empty ) toks; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
fun repeat1 ph  =  ph -- repeat ph >> (op::);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
fun list_of1 ph =  ph -- repeat("," $$-- !! ph) >> (op::);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
fun list_of ph  =  list_of1 ph || empty;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
fun reader ph a = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
       ( case ph (Lex.scan a) of 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
                (x,  []) => x
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
              | (_,(_, n)::_) => error
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
                ("Syntax error on line " ^ (string_of_int n) ^ ": " ^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
                 "Extra characters in phrase")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
       );
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
end;