~thon/thon

ref: fd82ecc4851b6e941a5aabb6c1747c1580f94fa1 thon/parse/thon.lex -rw-r--r-- 3.2 KiB
fd82ecc4Evan Bergeron Add no-op elaboration 10 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
structure A = Ast
structure Tokens = Tokens

exception UnbalancedComments

type pos = int
type svalue = Tokens.svalue
type ('a,'b) token = ('a,'b) Tokens.token
type lexresult= (svalue,pos) token

val pos = ref 0

local val commentLevel = ref 0 in

  (* Thank you to Kaustuv Chaudhuri, Frank Pfenning, Anand
   * Subramanian, and/or Taegyun Kim for these enterComment,
   * exitComment functions and their usages.
   *)
  fun enterComment yypos =
    (commentLevel := !commentLevel + 1)

  fun exitComment () =
    (commentLevel := !commentLevel - 1;
    !commentLevel = 0)

  fun eof () =
      (if (!commentLevel > 0)
       then raise UnbalancedComments
       else ();
       Tokens.EOF(!pos,!pos))
end

fun error (e,l : int,_) = TextIO.output (TextIO.stdOut, String.concat[
        "line ", (Int.toString l), ": ", e, "\n"
      ])

%%
%header (functor ThonLexFn(structure Tokens: Thon_TOKENS));
%s COMMENT;
alpha=[A-Za-z];
id=[A-Za-z_\']*;
digit=[0-9];
ws = [\ \t];
%%
<INITIAL> \n       => (pos := (!pos) + 1; lex());
<INITIAL> {ws}+    => (lex());
<INITIAL> "Z"      => (Tokens.ZERO(!pos,!pos));
<INITIAL> "S"      => (Tokens.SUCC(!pos,!pos));
<INITIAL> "\\"     => (Tokens.LAM(!pos,!pos));
<INITIAL> "let"    => (Tokens.LET(!pos,!pos));
<INITIAL> "fix"    => (Tokens.FIX(!pos,!pos));
<INITIAL> "ifz"    => (Tokens.IFZ(!pos,!pos));
<INITIAL> "fun"    => (Tokens.FUN(!pos,!pos));
<INITIAL> "->"     => (Tokens.SARROW(!pos,!pos));
<INITIAL> "nat"    => (Tokens.NAT(!pos,!pos));
<INITIAL> "rec"    => (Tokens.REC(!pos,!pos));
<INITIAL> "go"     => (Tokens.GO(!pos,!pos));
<INITIAL> "poly"   => (Tokens.POLY(!pos,!pos));
<INITIAL> "left"   => (Tokens.LEFT(!pos,!pos));
<INITIAL> "right"  => (Tokens.RIGHT(!pos,!pos));
<INITIAL> "fst"    => (Tokens.FST(!pos,!pos));
<INITIAL> "snd"    => (Tokens.SND(!pos,!pos));
<INITIAL> "all"    => (Tokens.ALL(!pos,!pos));
<INITIAL> "some"   => (Tokens.SOME(!pos,!pos));
<INITIAL> "unit"   => (Tokens.UNIT(!pos,!pos));
<INITIAL> "fold"   => (Tokens.FOLD(!pos,!pos));
<INITIAL> "unfold" => (Tokens.UNFOLD(!pos,!pos));
<INITIAL> "with"   => (Tokens.WITH(!pos,!pos));
<INITIAL> "impl"   => (Tokens.IMPL(!pos,!pos));
<INITIAL> "use"    => (Tokens.USE(!pos,!pos));
<INITIAL> "case"   => (Tokens.CASE(!pos,!pos));
<INITIAL> "as"     => (Tokens.AS(!pos,!pos));
<INITIAL> "in"     => (Tokens.IN(!pos,!pos));
<INITIAL> "of"     => (Tokens.OF(!pos,!pos));
<INITIAL> "u"      => (Tokens.TYPEREC(!pos,!pos));
<INITIAL> "."      => (Tokens.DOT(!pos,!pos));
<INITIAL> ":"      => (Tokens.COLON(!pos,!pos));
<INITIAL> ","      => (Tokens.COMMA(!pos,!pos));
<INITIAL> "*"      => (Tokens.STAR(!pos,!pos));
<INITIAL> "="      => (Tokens.EQ(!pos,!pos));
<INITIAL> "("      => (Tokens.LPAREN(!pos,!pos));
<INITIAL> ")"      => (Tokens.RPAREN(!pos,!pos));
<INITIAL> "|"      => (Tokens.PIPE(!pos,!pos));
<INITIAL> {digit}+ => (Tokens.IDX (valOf (Int.fromString yytext), !pos, !pos));
<INITIAL> {id}     => (Tokens.ID(yytext, !pos, !pos));

<INITIAL> "(*"        => (YYBEGIN COMMENT; enterComment yypos; lex());
<INITIAL> "*)"        => (raise UnbalancedComments);

<COMMENT> "(*"        => (enterComment yypos; lex());
<COMMENT> "*)"        => (if exitComment () then YYBEGIN INITIAL else ();lex());
<COMMENT> \n          => (lex());
<COMMENT> .           => (lex());