Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parsers / lexer_lustre.mll @ 04a188ec

History | View | Annotate | Download (6.16 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
{
13
open Parser_lustre
14
open Utils
15

    
16
(* As advised by Caml documentation. This way a single lexer rule is
17
   used to handle all the possible keywords. *)
18
let keyword_table =
19
  create_hashtable 20 [
20
  "function", FUNCTION;
21
  "struct", STRUCT;
22
  "enum", ENUM;
23
  "automaton", AUTOMATON;
24
  "state", STATE;
25
  "until", UNTIL;
26
  "unless", UNLESS;
27
  "resume", RESUME;
28
  "restart", RESTART;
29
  "if", IF;
30
  "then", THEN;
31
  "else", ELSE;
32
  "merge", MERGE;
33
  "arrow", ARROW;
34
  "fby", FBY;
35
  "when", WHEN;
36
  "whenot", WHENNOT;
37
  "every", EVERY;
38
  "node", NODE;
39
  "let", LET;
40
  "tel", TEL;
41
  "returns", RETURNS;
42
  "var", VAR;
43
  "imported", IMPORTED;
44
  "import", IMPORT;
45
  "type", TYPE;
46
  "int", TINT;
47
  "bool", TBOOL;
48
  (* "float", TFLOAT; *)
49
  "real", TREAL;
50
  "clock", TCLOCK;
51
  "not", NOT;
52
  "true", TRUE;
53
  "false", FALSE;
54
  "and", AND;
55
  "or", OR;
56
  "xor", XOR;
57
  "mod", MOD;
58
  "pre", PRE;
59
  "div", DIV;
60
  "const", CONST;
61
  "assert", ASSERT;
62
  "contract", CONTRACT;
63
  "lib", LIB;
64
  "prototype", PROTOTYPE;
65
  "ensure", ENSURE;
66
  "require", REQUIRE;
67
  (* "observer", OBSERVER; *)
68
  "invariant", INVARIANT;
69
  "mode", MODE;
70
  "assume", ASSUME;
71
  "contract", CONTRACT;
72
  "guarantee", GUARANTEES;
73
  "exists", EXISTS;
74
  "forall", FORALL;
75
 
76
  "c_code", CCODE; (* not sure how it is used *)
77
  "matlab", MATLAB; (* same as above *)
78
]
79

    
80

    
81
(* Buffer for parsing specification/annotation *)
82
let buf = Buffer.create 1024
83

    
84
let make_annot lexbuf s =
85
  let orig_loc = Location.curr lexbuf in
86
  try
87
    Location.push_loc orig_loc;	
88
    let ann = LexerLustreSpec.annot s in
89
    Location.pop_loc ();
90
    ANNOT ann
91
  with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift orig_loc loc, Parse.Annot_error s))
92

    
93
let make_spec orig_loc lexbuf s = 
94
  try
95
    Location.push_loc orig_loc;	
96
    let ns = LexerLustreSpec.spec s in
97
    Location.pop_loc ();
98
    NODESPEC ns
99
  with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift orig_loc loc, Parse.Node_spec_error s))
100

    
101
}
102

    
103
let newline = ('\010' | '\013' | "\013\010")
104
let notnewline = [^ '\010' '\013']
105
let blank = [' ' '\009' '\012']
106

    
107
rule token = parse
108
| "--@" { Buffer.clear buf;
109
          let loc = Location.curr lexbuf in
110
	  spec_singleline loc lexbuf }
111
| "(*@" { Buffer.clear buf; 
112
	  let loc = Location.curr lexbuf in
113
	  spec_multiline loc 0 lexbuf }
114
| "--!" { Buffer.clear buf; 
115
	  annot_singleline lexbuf }
116
| "(*!" { Buffer.clear buf; 
117
	  annot_multiline 0 lexbuf }
118
| "(*"
119
    { comment 0 lexbuf }
120
| "--" [^ '!' '@'] notnewline* (newline|eof)
121
    { incr_line lexbuf;
122
      token lexbuf }
123
| newline
124
    { incr_line lexbuf;
125
      token lexbuf }
126
| blank +
127
    {token lexbuf}
128
| ((['0'-'9']+ as l)  '.' (['0'-'9']* as r) ('E'|'e') (('+'|'-')? ['0'-'9']+ as exp)) as s
129
    {REAL (Real.create (l^r) (String.length r + -1 * int_of_string exp) s)}
130
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r)) as s
131
    {REAL (Real.create (l^r) (String.length r) s)}
132
| ['0'-'9']+ 
133
    {INT (int_of_string (Lexing.lexeme lexbuf)) }
134
| "tel." {TEL}
135
| "tel;" {TEL}
136
| "#open" { OPEN }
137
| "include" { INCLUDE }
138
| ['_' 'a'-'z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']*
139
    {let s = Lexing.lexeme lexbuf in
140
    try
141
      Hashtbl.find keyword_table s
142
    with Not_found ->
143
      IDENT s}
144
| ['A'-'Z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']*
145
    {let s = Lexing.lexeme lexbuf in
146
    try
147
      Hashtbl.find keyword_table s
148
    with Not_found ->
149
      UIDENT s}     
150
| "->" {ARROW}
151
| "=>" {IMPL}
152
| "<=" {LTE}
153
| ">=" {GTE}
154
| "<>" {NEQ}
155
| '<' {LT}
156
| '>' {GT}
157
| "!=" {NEQ}
158
| '-' {MINUS}
159
| '+' {PLUS}
160
| '/' {DIV}
161
| '*' {MULT}
162
| '=' {EQ}
163
| '(' {LPAR}
164
| ')' {RPAR}
165
| '[' {LBRACKET}
166
| ']' {RBRACKET}
167
| '{' {LCUR}
168
| '}' {RCUR}
169
| ';' {SCOL}
170
| ':' {COL}
171
| ',' {COMMA}
172
| '=' {EQ}
173
| "&&" {AMPERAMPER}
174
| "||" {BARBAR}
175
| "::" {COLCOL}
176
| "^" {POWER}
177
| '"' {QUOTE}
178
| '.' {POINT}
179
| eof { EOF }
180
| _ { raise (Parse.Error (Location.curr lexbuf, Parse.Undefined_token (Lexing.lexeme lexbuf))) }
181

    
182
and comment n = parse
183
| eof
184
    { raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_comment)) }
185
| "(*"
186
    { comment (n+1) lexbuf }
187
| "*)"
188
    { if n > 0 then comment (n-1) lexbuf else token lexbuf }
189
| newline
190
    { incr_line lexbuf;
191
      comment n lexbuf }
192
| _ { comment n lexbuf }
193

    
194
and annot_singleline = parse
195
  | eof { make_annot lexbuf (Buffer.contents buf) }
196
  | newline { incr_line lexbuf; make_annot lexbuf (Buffer.contents buf) }
197
  | _ as c { Buffer.add_char buf c; annot_singleline lexbuf }
198

    
199
and annot_multiline n = parse
200
  | eof { raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_annot)) }
201
  | "*)" as s { 
202
    if n > 0 then 
203
      (Buffer.add_string buf s; annot_multiline (n-1) lexbuf) 
204
    else 
205
      make_annot lexbuf (Buffer.contents buf) }
206
  | "(*" as s { Buffer.add_string buf s; annot_multiline (n+1) lexbuf }
207
  | newline as s { incr_line lexbuf; Buffer.add_string buf s; annot_multiline n lexbuf }
208
  | _ as c { Buffer.add_char buf c; annot_multiline n lexbuf }
209

    
210
and spec_singleline loc = parse
211
  | eof { make_spec loc lexbuf (Buffer.contents buf) }
212
  | newline { incr_line lexbuf; make_spec loc lexbuf (Buffer.contents buf) }
213
  | _ as c { Buffer.add_char buf c; spec_singleline loc lexbuf }
214

    
215
and spec_multiline loc n = parse
216
  | eof { raise (Parse.Error (Location.curr lexbuf, Parse.Unfinished_node_spec)) }
217
  | "*)" as s { if n > 0 then 
218
      (Buffer.add_string buf s; spec_multiline loc (n-1) lexbuf) 
219
    else 
220
      make_spec loc lexbuf (Buffer.contents buf) }
221
  | "(*" as s { Buffer.add_string buf s; spec_multiline loc (n+1) lexbuf }
222
  | newline as s { incr_line lexbuf; Buffer.add_string buf s; spec_multiline loc n lexbuf }
223
  | _ as c { Buffer.add_char buf c; spec_multiline loc n lexbuf }
224