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