1
2
3(******************************************************************************
4Simple lexer for PSL/Sugar properties
5(based on examples/lexyacc in mosml distribution)
6 ******************************************************************************)
7
8
9{
10 open Lexing Parser;
11
12 exception LexicalError of string * int * int (* (message, loc1, loc2) *)
13
14 fun lexerError lexbuf s =
15     raise LexicalError (s, getLexemeStart lexbuf, getLexemeEnd lexbuf);
16
17 val commentStart = ref 0;  (* Start of outermost comment being scanned *)
18
19 fun commentNotClosed lexbuf =
20     raise LexicalError ("Comment not terminated",
21                         !commentStart, getLexemeEnd lexbuf);
22
23 val commentDepth = ref 0;  (* Current comment nesting *)
24
25 (* Scan keywords as identifiers and use this function to distinguish them. *)
26 (* If the set of keywords is large, use an auxiliary hashtable.            *)
27
28 fun keyword s =
29     case s of
30         "A"            => A
31       | "AF"           => AF
32       | "AG"           => AG
33       | "AX"           => AX
34       | "abort"        => ABORT
35       | "always"       => ALWAYS
36       | "before"       => BEFORE
37       | "E"            => E
38       | "EF"           => EF
39       | "EG"           => EG
40       | "EX"           => EX
41       | "forall"       => FORALL
42       | "G"            => G
43       | "inf"          => INF
44       | "never"        => NEVER
45       | "next"         => NEXT
46       | "U"            => U
47       | "X"            => X
48       | "abort"        => ABORT
49       | "until"        => UNTIL
50       | "W"            => W
51       | "whilenot"     => WHILENOT
52       | "within"       => WITHIN
53       | _              => Name s;
54
55 }
56
57rule Token = parse
58    "(*"                { commentStart := getLexemeStart lexbuf;
59                          commentDepth := 1;
60                          SkipComment lexbuf; Token lexbuf }
61  | `@`                 { AT }
62  | `;`                 { SEMICOLON }
63  | "[*"                { LBRKTSTAR }
64  | "[="                { LBRKTEQ }
65  | "[->"               { LBRKTLEFTARROW }
66  | "[*]"               { LBRKTSTARRBRKT }
67  | "[+]"               { LBRKTPLUSRBRKT }
68  | `,`                 { COMMA }
69  | `:`                 { COLON }
70  | `|`                 { BAR }
71  | "||"                { BARBAR }
72  | `&`                 { AMPERSAND }
73  | "&&"                { AMPERSANDAMPERSAND }
74  | "->"                { LEFTARROW }
75  | "<->"               { LEFTRIGHTARROW }
76  | "|->"               { BARLEFTARROW }
77  | "|=>"               { BAREQLEFTARROW }
78  | "|="                { BAREQUAL }
79  | `!`                 { EXCLAIM }
80  | `*`                 { STAR }
81  | `(`                 { LPAR }
82  | `)`                 { RPAR }
83  | `[`                 { LBRKT }
84  | `]`                 { RBRKT }
85  | `{`                 { LBRACE }
86  | `}`                 { RBRACE }
87  | "before!"           { BEFOREX }
88  | "before!_"          { BEFOREXU }
89  | "before_"           { BEFOREU }
90  | "whilenot!_"        { WHILENOTXU }
91  | "eventually!"       { EVENTUALLYX }
92  | "next!"             { NEXTX }
93  | "next_a"            { NEXTA }
94  | "next_a!"           { NEXTAX }
95  | "next_e"            { NEXTE }
96  | "next_e!"           { NEXTEX }
97  | "next_event"        { NEXTEVENT }
98  | "next_event!"       { NEXTEVENTX }
99  | "next_event_a!"     { NEXTEVENTAX }
100  | "next_event_e!"     { NEXTEVENTEX }
101  | "until!"            { UNTILX }
102  | "until!_"           { UNTILXU }
103  | "until_"            { UNTILU }
104  | "whilenot!"         { WHILENOTX }
105  | "whilenot!_"        { WHILENOTXU }
106  | "whilenot_"         { WHILENOTU }
107  | "within!"           { WITHINX }
108  | "within!_"          { WITHINXU }
109  | "within_"           { WITHINU }
110  | "X!"                { XX }
111  | eof                 { EOF }
112  | [` ` `\t` `\n` `\r`]{ Token lexbuf }
113  | [`0`-`9`]+          { case Int.fromString (getLexeme lexbuf) of
114                             NONE   => lexerError lexbuf "internal error"
115                           | SOME i => Number i}
116  | [`_``a`-`z``A`-`Z`][`_``a`-`z``A`-`Z``0`-`9`]*
117                        { keyword (getLexeme lexbuf) }
118
119  | _                   { lexerError lexbuf "Illegal symbol in input" }
120
121and SkipComment = parse
122    "*)"                { commentDepth := !commentDepth - 1;
123                          if !commentDepth = 0 then ()
124                          else SkipComment lexbuf }
125   | "(*"               { commentDepth := !commentDepth + 1;
126                          SkipComment lexbuf }
127   | (eof | `\^Z`)      { commentNotClosed lexbuf }
128   | _                  { SkipComment lexbuf }
129;
130