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