Project

General

Profile

Download (7.96 KB) Statistics
| Branch: | Tag: | Revision:
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
  "guarantee", GUARANTEES;
72
  "exists", EXISTS;
73
  "forall", FORALL;
74
 
75
  "c_code", CCODE; (* not sure how it is used *)
76
  "matlab", MATLAB; (* same as above *)
77
]
78

    
79

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

    
83
  type error =
84
    | Undefined_token of string
85
    | Unfinished_comment
86
    | Unfinished_annot
87
    | Unfinished_node_spec
88
    | Annot_error of string
89
    | Node_spec_error of string
90

    
91
  exception Error of Location.t * error
92

    
93
let pp_error fmt =
94
  let open Format in
95
  function
96
  | Undefined_token s ->
97
    fprintf fmt "Undefined token '%s'." s
98
  | Unfinished_comment ->
99
    fprintf fmt "Unfinished comment."
100
  | Unfinished_annot ->
101
    fprintf fmt "Unfinished annotation."
102
  | Unfinished_node_spec ->
103
    fprintf fmt "Unfinished node specification."
104
  | Annot_error s ->
105
    fprintf fmt "Ill-formed annotation '%s'." s
106
  | Node_spec_error s ->
107
    fprintf fmt "Ill-formed node specification '%s'." s
108

    
109
let error_with loc err =
110
  raise (Error (loc, err))
111

    
112
let error lexbuf =
113
  error_with (Location.curr lexbuf)
114

    
115
let newline token lexbuf =
116
  Location.Lex.newline lexbuf;
117
  token lexbuf
118

    
119
let make_annot orig_loc s =
120
  let lexbuf = Lexing.from_string s in
121
  let f = Location.filename_of_loc orig_loc in
122
  ANNOT (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
123
        Parser_lustre.lustre_annot Parse.Inc.lustre_annot)
124

    
125
let make_spec orig_loc s =
126
  let lexbuf = Lexing.from_string s in
127
  let f = Location.filename_of_loc orig_loc in
128
  NODESPEC (Parse.parse (module LexerLustreSpec) ~orig_loc f s lexbuf
129
        Parser_lustre.lustre_spec Parse.Inc.lustre_spec)
130
}
131

    
132
let newline = ('\010' | '\013' | "\013\010")
133
let notnewline = [^ '\010' '\013']
134
let blank = [' ' '\009' '\012']
135

    
136
rule token = parse
137
| "--@" { Buffer.clear buf;
138
          let loc = Location.curr lexbuf in
139
          extra_singleline (make_spec loc) lexbuf }
140
| "(*@" { Buffer.clear buf; 
141
          let loc = Location.curr lexbuf in
142
          extra_multiline (make_spec loc) Unfinished_node_spec 0 lexbuf }
143
| "--!" { Buffer.clear buf;
144
          let loc = Location.curr lexbuf in
145
          extra_singleline (make_annot loc) lexbuf }
146
| "(*!" { Buffer.clear buf;
147
          let loc = Location.curr lexbuf in
148
          extra_multiline (make_annot loc) Unfinished_annot 0 lexbuf }
149
| "(*"  { comment 0 lexbuf }
150
| "--" [^ '!' '@'] notnewline* (newline|eof)
151
    { newline token lexbuf }
152
| newline { newline token lexbuf }
153
| blank + { token lexbuf }
154
| ((['0'-'9']+ as l)  '.' (['0'-'9']* as r) ('E'|'e') (('+'|'-')? ['0'-'9']+ as exp)) as s
155
    {REAL (Real.create (l^r) (String.length r + -1 * int_of_string exp) s)}
156
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r)) as s
157
    {REAL (Real.create (l^r) (String.length r) s)}
158
| ['0'-'9']+ 
159
    {INT (int_of_string (Lexing.lexeme lexbuf)) }
160
| "tel." {TEL}
161
| "tel;" {TEL}
162
| "#open" { OPEN }
163
| "include" { INCLUDE }
164
| ['_' 'a'-'z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']* as s
165
    { try Hashtbl.find keyword_table s with Not_found -> IDENT s }
166
| ['A'-'Z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']* as s
167
    { try Hashtbl.find keyword_table s with Not_found -> UIDENT s }
168
| "->" {ARROW}
169
| "=>" {IMPL}
170
| "<=" {LTE}
171
| ">=" {GTE}
172
| "<>" {NEQ}
173
| '<' {LT}
174
| '>' {GT}
175
| "!=" {NEQ}
176
| '-' {MINUS}
177
| '+' {PLUS}
178
| '/' {DIV}
179
| '*' {MULT}
180
| '=' {EQ}
181
| '(' {LPAR}
182
| ')' {RPAR}
183
| '[' {LBRACKET}
184
| ']' {RBRACKET}
185
| '{' {LCUR}
186
| '}' {RCUR}
187
| ';' {SCOL}
188
| ':' {COL}
189
| ',' {COMMA}
190
| '=' {EQ}
191
| "&&" {AMPERAMPER}
192
| "||" {BARBAR}
193
| "::" {COLCOL}
194
| "^" {POWER}
195
| '"' {QUOTE}
196
| '.' {POINT}
197
| eof { EOF }
198
| _ { error lexbuf (Undefined_token (Lexing.lexeme lexbuf)) }
199

    
200
and comment n = parse
201
  | eof     { error lexbuf Unfinished_comment }
202
  | "(*"    { comment (n+1) lexbuf }
203
  | "*)"    { if n > 0 then comment (n-1) lexbuf else token lexbuf }
204
  | newline { newline (comment n) lexbuf }
205
  | _       { comment n lexbuf }
206

    
207
and extra_singleline extra = parse
208
  | eof     { extra (Buffer.contents buf) }
209
  | newline { newline (fun _ -> extra (Buffer.contents buf)) lexbuf }
210
  | _ as c  { Buffer.add_char buf c; extra_singleline extra lexbuf }
211

    
212
and extra_multiline extra err n = parse
213
  | eof          { error lexbuf err }
214
  | "*)" as s    { if n > 0 then begin
215
                     Buffer.add_string buf s;
216
                     extra_multiline extra err (n-1) lexbuf
217
                   end else
218
                     extra (Buffer.contents buf) }
219
  | "(*" as s    { Buffer.add_string buf s;
220
                   extra_multiline extra err (n+1) lexbuf }
221
  | newline as s { newline (fun lexbuf ->
222
                     Buffer.add_string buf s;
223
                     extra_multiline extra err n lexbuf) lexbuf }
224
  | _ as c       { Buffer.add_char buf c; extra_multiline extra err n lexbuf }
225

    
226
(* and annot_singleline loc = parse
227
 *   | eof     { make_annot loc (Buffer.contents buf) }
228
 *   | newline { newline (fun _ -> make_annot loc (Buffer.contents buf)) lexbuf }
229
 *   | _ as c  { Buffer.add_char buf c; annot_singleline loc lexbuf }
230
 *
231
 * and annot_multiline loc n = parse
232
 *   | eof          { error lexbuf Unfinished_annot }
233
 *   | "*\)" as s    { if n > 0 then
234
 *                      (Buffer.add_string buf s; annot_multiline (n-1) lexbuf)
235
 *                    else
236
 *                      make_annot (Buffer.contents buf) lexbuf }
237
 *   | "(\*" as s    { Buffer.add_string buf s; annot_multiline (n+1) lexbuf }
238
 *   | newline as s { newline (fun lexbuf ->
239
 *         Buffer.add_string buf s; annot_multiline n lexbuf) lexbuf }
240
 *   | _ as c       { Buffer.add_char buf c; annot_multiline n lexbuf }
241
 *
242
 * and spec_singleline loc = parse
243
 *   | eof     { make_spec loc (Buffer.contents buf) }
244
 *   | newline { newline (fun _ -> make_spec loc (Buffer.contents buf)) lexbuf }
245
 *   | _ as c  { Buffer.add_char buf c; spec_singleline loc lexbuf }
246
 *
247
 * and spec_multiline loc n = parse
248
 *   | eof          { error lexbuf Unfinished_node_spec }
249
 *   | "*\)" as s    { if n > 0 then
250
 *                      (Buffer.add_string buf s; spec_multiline loc (n-1) lexbuf)
251
 *                    else
252
 *                      make_spec loc (Buffer.contents buf) }
253
 *   | "(\*" as s    { Buffer.add_string buf s; spec_multiline loc (n+1) lexbuf }
254
 *   | newline as s { newline (fun lexbuf ->
255
 *         Buffer.add_string buf s; spec_multiline loc n lexbuf) lexbuf }
256
 *   | _ as c       { Buffer.add_char buf c; spec_multiline loc n lexbuf } *)
(3-3/8)