Project

General

Profile

Revision f4cba4b8 src/parsers/parser_lustre.mly

View differences:

src/parsers/parser_lustre.mly
49 49
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
50 50
  else
51 51
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
52
  
52

  
53
 
53 54
%}
54 55

  
55 56
%token <int> INT
......
62 63
%token <string> UIDENT
63 64
%token TRUE FALSE
64 65
%token <Lustre_types.expr_annot> ANNOT
65
%token <Lustre_types.contract_desc> NODESPEC
66
%token <Lustre_types.spec_types> NODESPEC
66 67
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
67 68
%token AMPERAMPER BARBAR NOT POWER
68 69
%token IF THEN ELSE
......
113 114
%type <Lustre_types.expr_annot> lustre_annot
114 115

  
115 116
%start lustre_spec
116
%type <Lustre_types.contract_desc> lustre_spec
117
%type <Lustre_types.spec_types> lustre_spec
117 118

  
118 119
%start signed_const
119 120
%type <Lustre_types.constant> signed_const
......
203 204

  
204 205
top_decl_header:
205 206
| CONST cdecl_list { List.rev ($2 true) }
206
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_list SCOL
207
    {let nd = mktop_decl true (ImportedNode
207
| nodespecs state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR  prototype_opt in_lib_list SCOL
208
    {
209
      let inputs = List.rev $5 in
210
      let outputs = List.rev $10 in
211
      let nd = mktop_decl true (ImportedNode
208 212
				 {nodei_id = $3;
209 213
				  nodei_type = Types.new_var ();
210 214
				  nodei_clock = Clocks.new_var true;
211
				  nodei_inputs = List.rev $5;
212
				  nodei_outputs = List.rev $10;
215
				  nodei_inputs = inputs;
216
				  nodei_outputs = outputs;
213 217
				  nodei_stateless = $2;
214 218
				  nodei_spec = $1;
215 219
				  nodei_prototype = $13;
216 220
				  nodei_in_lib = $14;})
217 221
     in
218
     (*add_imported_node $3 nd;*) [nd] } 
219
| CONTRACT node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL 
220
    {let nd = mktop_decl true (ImportedNode
221
				 {nodei_id = $2;
222
				  nodei_type = Types.new_var ();
223
				  nodei_clock = Clocks.new_var true;
224
				  nodei_inputs = List.rev $4;
225
				  nodei_outputs = List.rev $9;
226
				  nodei_stateless = false (* By default we assume contracts as stateful *);
227
				  nodei_spec = Some $14;
228
				  nodei_prototype = None;
229
				  nodei_in_lib = [];})
230
     in
231
     (*add_imported_node $3 nd;*) [nd] }
222
     pop_node ();
223
     [nd] } 
224
| top_contract { [$1] }
225

  
232 226

  
233 227
prototype_opt:
234 228
 { None }
......
240 234

  
241 235
top_decl:
242 236
| CONST cdecl_list { List.rev ($2 false) }
243
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespec_list locals LET stmt_list TEL 
237
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespecs locals LET stmt_list TEL 
244 238
    {
245 239
     let stmts, asserts, annots = $16 in
246 240
      (* Declaring eqs annots *)
......
249 243
	  Annotations.add_node_ann $2 key
250 244
	) ann.annots
251 245
      ) annots;
252
     (* Building the node *)
246
      (* Building the node *)
247
      let inputs = List.rev $4 in
248
      let outputs = List.rev $9 in
253 249
     let nd = mktop_decl false (Node
254 250
				  {node_id = $2;
255 251
				   node_type = Types.new_var ();
256 252
				   node_clock = Clocks.new_var true;
257
				   node_inputs = List.rev $4;
258
				   node_outputs = List.rev $9;
253
				   node_inputs = inputs;
254
				   node_outputs = outputs;
259 255
				   node_locals = List.rev $14;
260 256
				   node_gencalls = [];
261 257
				   node_checks = [];
......
264 260
				   node_dec_stateless = $1;
265 261
				   node_stateless = None;
266 262
				   node_spec = $13;
267
				   node_annot = annots})
263
				   node_annot = annots;
264
				   node_iscontract = false;
265
			       })
268 266
     in
269 267
     pop_node ();
270 268
     (*add_node $3 nd;*) [nd] }
271 269

  
272
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL
273
    {let nd = mktop_decl true (ImportedNode
274
				 {nodei_id = $3;
275
				  nodei_type = Types.new_var ();
276
				  nodei_clock = Clocks.new_var true;
277
				  nodei_inputs = List.rev $5;
278
				  nodei_outputs = List.rev $10;
279
				  nodei_stateless = $1;
280
				  nodei_spec = Some $15;
281
				  nodei_prototype = None;
282
				  nodei_in_lib = [];})
283
     in
284
     pop_node ();
285
     (*add_imported_node $3 nd;*) [nd] } 
286
| state_annot IMPORTED node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
287
    {let nd = mktop_decl true (ImportedNode
288
				 {nodei_id = $3;
289
				  nodei_type = Types.new_var ();
290
				  nodei_clock = Clocks.new_var true;
291
				  nodei_inputs = List.rev $5;
292
				  nodei_outputs = List.rev $10;
293
				  nodei_stateless = $1;
294
				  nodei_spec = None;
295
				  nodei_prototype = None;
296
				  nodei_in_lib = [];})
297
     in
298
     pop_node ();
299
     (*add_imported_node $3 nd;*) [nd] } 
270

  
271
| NODESPEC
272
    { match $1 with
273
      | LocalContract c -> assert false
274
      | TopContract c   -> c
275
			 
276
    }
277

  
278
nodespecs:
279
nodespec_list {
280
  match $1 with
281
  | None -> None 
282
  | Some c -> Some (Contract c)
283
}
300 284

  
301 285
nodespec_list:
302 286
 { None }
303
| NODESPEC nodespec_list { 
304
  (function 
305
  | None    -> (fun s1 -> Some s1) 
306
  | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
287
  | NODESPEC nodespec_list {
288
	       let extract x = match x with LocalContract c -> c | _ -> assert false in
289
	       let s1 = extract $1 in
290
	       match $2 with
291
	       | None -> Some s1
292
	       | Some s2 -> Some (merge_contracts s1 s2) }
307 293

  
308 294
typ_def_list:
309 295
    /* empty */             { (fun itf -> []) }
......
382 368
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
383 369

  
384 370
lustre_spec:
385
| contract EOF { $1 }
371
| top_contracts EOF     { TopContract $1 }
372
| contract_content EOF { LocalContract $1}
373

  
374
top_contracts:
375
| top_contract { [$1] }
376
| top_contract top_contracts { $1::$2 }
377

  
378
top_contract:
379
| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL 
380
    {
381
      let nd = mktop_decl true (Node
382
				 {node_id = $2;
383
				  node_type = Types.new_var ();
384
				  node_clock = Clocks.new_var true;
385
				  node_inputs = List.rev $4;
386
				  node_outputs = List.rev $9;
387
				  node_locals = []; (* will be filled later *)
388
				  node_gencalls = [];
389
				  node_checks = [];
390
				  node_asserts = [];
391
				  node_stmts = []; (* will be filled later *)
392
				  node_dec_stateless = false;
393
				  (* By default we assume contracts as stateful *)
394
				  node_stateless = None;
395
				  node_spec = Some (Contract $14);
396
				  node_annot = [];
397
				  node_iscontract = true;
398
				 }
399
			       )
400
     in
401
     pop_node ();
402
     (*add_imported_node $3 nd;*)
403
     nd }
386 404

  
387
contract:
405
contract_content:
388 406
{ empty_contract }
389
| CONTRACT contract { $2 }
390
| CONST IDENT EQ expr SCOL contract
407
| CONTRACT contract_content { $2 }
408
| CONST IDENT EQ expr SCOL contract_content
391 409
    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
392
| CONST IDENT COL typeconst EQ expr SCOL contract
410
| CONST IDENT COL typeconst EQ expr SCOL contract_content
393 411
    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
394
| VAR IDENT COL typeconst EQ expr SCOL contract
412
| VAR IDENT COL typeconst EQ expr SCOL contract_content
395 413
    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
396
| ASSUME qexpr SCOL contract
414
| ASSUME qexpr SCOL contract_content
397 415
    { merge_contracts (mk_contract_assume $2) $4 }
398
| GUARANTEES qexpr SCOL contract	
416
| GUARANTEES qexpr SCOL contract_content	
399 417
    { merge_contracts (mk_contract_guarantees $2) $4 }
400
| MODE IDENT LPAR mode_content RPAR SCOL contract
418
| MODE IDENT LPAR mode_content RPAR SCOL contract_content
401 419
	{ merge_contracts (
402 420
	  let r, e = $4 in 
403 421
	  mk_contract_mode $2 r e (get_loc())) $7 }	
404
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract
422
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
405 423
    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }
406 424

  
407 425
mode_content:

Also available in: Unified diff