1(* this is an -*- sml-lex -*- file *)
2structure Tokens = Tokens
3type pos = int
4
5type svalue = Tokens.svalue
6type ('a,'b) token = ('a,'b)Tokens.token
7type lexresult = (svalue,pos) token
8
9val pos = ref 1
10fun eof _ = Tokens.EOF(!pos,!pos)
11type arg = string list ref
12
13%%
14%header (functor HOLsexpLexFun(structure Tokens : HOLsexp_TOKENS));
15%full
16%s string comment quotedsymbol;
17%arg (stringbuffer : string list ref);
18digit=[0-9];
19integer={digit}+;
20space = [\ \t];
21%%
22<INITIAL>";" => (YYBEGIN comment; continue());
23<INITIAL>"(" => (Tokens.LPAREN(!pos, !pos));
24<INITIAL>")" => (Tokens.RPAREN(!pos, !pos));
25<INITIAL>{space}+ => (continue());
26<INITIAL>"\n" => (continue());
27<INITIAL>[-+]?{integer} =>
28   (Tokens.NUMBER(valOf (Int.fromString yytext), !pos, !pos));
29<INITIAL>"'" => (Tokens.QUOTE(!pos,!pos));
30<INITIAL>"." => (Tokens.DOT(!pos,!pos));
31<INITIAL>"|" => (YYBEGIN quotedsymbol; stringbuffer := []; continue());
32<INITIAL>[-%+*_A-Za-z0-9]+ => (Tokens.SYMBOL(yytext, !pos, !pos));
33<INITIAL>"\"" => (YYBEGIN string; stringbuffer := []; continue());
34<INITIAL>. => (raise Fail ("Unexpected: "^yytext));
35
36<quotedsymbol>"|" => (YYBEGIN INITIAL;
37                      Tokens.SYMBOL(String.concat (List.rev(!stringbuffer)),
38                                    !pos, !pos));
39<quotedsymbol>"\\|" => (stringbuffer := "|" :: !stringbuffer; continue());
40<quotedsymbol>"\\n" => (stringbuffer := "\n" :: !stringbuffer; continue());
41<quotedsymbol>[^\\|]+ => (stringbuffer := yytext :: !stringbuffer; continue());
42<quotedsymbol>\n => (raise Fail "Newline inside |-quoted-symbol");
43
44<string>"\"" => (YYBEGIN INITIAL;
45                 Tokens.STRING(String.concat (List.rev(!stringbuffer)),
46                               !pos, !pos));
47<string>"\\\"" => (stringbuffer := "\"" :: !stringbuffer; continue());
48<string>"\\a" => (stringbuffer := "\a" :: !stringbuffer; continue());
49<string>"\\b" => (stringbuffer := "\b" :: !stringbuffer; continue());
50<string>"\\f" => (stringbuffer := "\f" :: !stringbuffer; continue());
51<string>"\\n" => (stringbuffer := "\n" :: !stringbuffer; continue());
52<string>"\\r" => (stringbuffer := "\r" :: !stringbuffer; continue());
53<string>"\\t" => (stringbuffer := "\t" :: !stringbuffer; continue());
54<string>[^\"\\]+ => (stringbuffer := yytext :: !stringbuffer; continue());
55<string>\n => (raise Fail "Newline inside string literal");
56<string>"\\"[0-9][0-9][0-9] => (
57  let
58    val code = valOf (Int.fromString (String.substring(yytext, 1, 3)))
59  in
60    stringbuffer := str (Char.chr code) :: !stringbuffer; continue()
61  end
62);
63<string>"\\^" [\064-\095] => (
64  let
65    val code = Char.ord (String.sub(yytext, 2)) - 64
66  in
67    stringbuffer := str (Char.chr code) :: !stringbuffer ; continue()
68  end
69);
70<string>"\\\\" => (stringbuffer := "\\" :: !stringbuffer; continue());
71<string>"\\" . => (raise Fail ("Can't cope with escaping "^yytext^
72                               " inside string literal"));
73<string>. => (raise Fail ("Can't cope with character "^yytext^
74                          " inside string literal"));
75
76<comment>\n => (YYBEGIN INITIAL; continue());
77<comment>. => (continue());
78