lustrec / src / lexerLustreSpec.mll @ 0038002e
History | View | Annotate | Download (3.44 KB)
1 |
{ |
---|---|
2 |
|
3 |
(* open ParserLustreSpec *) |
4 |
open Parser_lustre |
5 |
open Utils |
6 |
|
7 |
let str_buf = Buffer.create 1024 |
8 |
|
9 |
exception Error of Location.t |
10 |
|
11 |
(* As advised by Caml documentation. This way a single lexer rule is |
12 |
used to handle all the possible keywords. *) |
13 |
let keyword_table = |
14 |
create_hashtable 20 [ |
15 |
(* "true", TRUE; *) |
16 |
(* "false", FALSE; *) |
17 |
"stateless", STATELESS; |
18 |
"if", IF; |
19 |
"then", THEN; |
20 |
"else", ELSE; |
21 |
"merge", MERGE; |
22 |
"arrow", ARROW; |
23 |
"fby", FBY; |
24 |
"when", WHEN; |
25 |
"whennot", WHENNOT; |
26 |
"every", EVERY; |
27 |
"node", NODE; |
28 |
"let", LET; |
29 |
"tel", TEL; |
30 |
"returns", RETURNS; |
31 |
"var", VAR; |
32 |
"imported", IMPORTED; |
33 |
"wcet", WCET; |
34 |
"int", TINT; |
35 |
"bool", TBOOL; |
36 |
"float", TFLOAT; |
37 |
"real", TREAL; |
38 |
"clock", TCLOCK; |
39 |
"not", NOT; |
40 |
"tail", TAIL; |
41 |
"and", AND; |
42 |
"or", OR; |
43 |
"xor", OR; |
44 |
"mod", MOD; |
45 |
"pre", PRE; |
46 |
"div", DIV; |
47 |
"const", CONST; |
48 |
(* "include", INCLUDE; *) |
49 |
"assert", ASSERT; |
50 |
"ensures", ENSURES; |
51 |
"requires", REQUIRES; |
52 |
"observer", OBSERVER; |
53 |
"invariant", INVARIANT; |
54 |
"behavior", BEHAVIOR; |
55 |
"assumes", ASSUMES; |
56 |
"exists", EXISTS; |
57 |
"forall", FORALL; |
58 |
] |
59 |
|
60 |
} |
61 |
|
62 |
|
63 |
let newline = ('\010' | '\013' | "\013\010") |
64 |
let notnewline = [^ '\010' '\013'] |
65 |
let blank = [' ' '\009' '\012'] |
66 |
|
67 |
rule token = parse |
68 |
| "(*" |
69 |
{ comment_line 0 lexbuf } |
70 |
| "--" notnewline* (newline|eof) |
71 |
{ incr_line lexbuf; |
72 |
token lexbuf } |
73 |
| newline |
74 |
{ incr_line lexbuf; |
75 |
token lexbuf } |
76 |
| blank + |
77 |
{token lexbuf} |
78 |
| '-'? ['0'-'9'] ['0'-'9']* '.' ['0'-'9']* |
79 |
{FLOAT (float_of_string (Lexing.lexeme lexbuf))} |
80 |
| '-'? ['0'-'9']+ |
81 |
{INT (int_of_string (Lexing.lexeme lexbuf)) } |
82 |
| '-'? ['0'-'9']+ '.' ['0'-'9']+ ('E'|'e') ('+'|'-') ['0'-'9'] ['0'-'9'] as s {REAL s} |
83 |
(* | '/' (['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* '/')+ as s |
84 |
{IDENT s} |
85 |
*) |
86 |
| ['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* |
87 |
{let s = Lexing.lexeme lexbuf in |
88 |
try |
89 |
Hashtbl.find keyword_table s |
90 |
with Not_found -> |
91 |
IDENT s} |
92 |
| "->" {ARROW} |
93 |
| "=>" {IMPL} |
94 |
| "<=" {LTE} |
95 |
| ">=" {GTE} |
96 |
| "<>" {NEQ} |
97 |
| '<' {LT} |
98 |
| '>' {GT} |
99 |
| "!=" {NEQ} |
100 |
| '-' {MINUS} |
101 |
| '+' {PLUS} |
102 |
| '/' {DIV} |
103 |
| '*' {MULT} |
104 |
| '=' {EQ} |
105 |
| '(' {LPAR} |
106 |
| ')' {RPAR} |
107 |
| ';' {SCOL} |
108 |
| ':' {COL} |
109 |
| ',' {COMMA} |
110 |
| '=' {EQ} |
111 |
| '/' {DIV} |
112 |
| "&&" {AMPERAMPER} |
113 |
| "||" {BARBAR} |
114 |
| "::" {COLCOL} |
115 |
| "^" {POWER} |
116 |
| '"' { Buffer.clear str_buf; string_parse lexbuf } |
117 |
| eof { EOF } |
118 |
| _ { raise (Error (Location.curr lexbuf)) } |
119 |
and comment_line n = parse |
120 |
| eof |
121 |
{ raise (Error (Location.curr lexbuf)) } |
122 |
| "(*" |
123 |
{ comment_line (n+1) lexbuf } |
124 |
| "*)" |
125 |
{ if n > 0 then comment_line (n-1) lexbuf else token lexbuf } |
126 |
| newline |
127 |
{ incr_line lexbuf; |
128 |
comment_line n lexbuf } |
129 |
| _ { comment_line n lexbuf } |
130 |
and string_parse = parse |
131 |
| "\\\"" as s { Buffer.add_string str_buf s; string_parse lexbuf} |
132 |
| '"' { STRING (Buffer.contents str_buf) } |
133 |
| _ as c { Buffer.add_char str_buf c; string_parse lexbuf } |
134 |
|
135 |
{ |
136 |
|
137 |
let annot s = |
138 |
let lb = Lexing.from_string s in |
139 |
try |
140 |
Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lb |
141 |
with Parsing.Parse_error as _e -> ( |
142 |
Format.eprintf "Lexing error at position %a:@.unexpected token %s@.@?" |
143 |
(fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lb.Lexing.lex_curr_p |
144 |
(Lexing.lexeme lb); |
145 |
raise Parsing.Parse_error) |
146 |
|
147 |
|
148 |
let spec s = |
149 |
let lb = Lexing.from_string s in |
150 |
Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lb |
151 |
|
152 |
} |