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