Project

General

Profile

« Previous | Next » 

Revision 3dfb5cd8

Added by LĂ©lio Brun over 3 years ago

rewrite a bit the menhir parser

View differences:

src/parsers/dune
7 7
;  (libraries lustre_types corelang automata))
8 8

  
9 9
(menhir
10
 (modules parser_lustre))
10
 (modules parser_lustre)
11
 (flags --explain))
11 12

  
12 13
(ocamllex lexerLustreSpec lexer_lustre)
src/parsers/lexerLustreSpec.mll
41 41
  "returns", RETURNS;
42 42
  "var", VAR;
43 43
  "import", IMPORT;
44
  "imported", IMPORTED;
44
  (* "imported", IMPORTED; *)
45 45
  "int", TINT;
46 46
  "bool", TBOOL;
47 47
  (* "float", TFLOAT; *)
src/parsers/lexer_lustre.mll
40 40
  "tel", TEL;
41 41
  "returns", RETURNS;
42 42
  "var", VAR;
43
  "imported", IMPORTED;
43
  (* "imported", IMPORTED; *)
44 44
  "import", IMPORT;
45 45
  "type", TYPE;
46 46
  "int", TINT;
......
90 90
    ANNOT ann
91 91
  with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift orig_loc loc, Parse.Annot_error s))
92 92

  
93
let make_spec orig_loc lexbuf s = 
93
let make_spec orig_loc s =
94 94
  try
95 95
    Location.push_loc orig_loc;	
96 96
    let ns = LexerLustreSpec.spec s in
......
208 208
  | _ as c { Buffer.add_char buf c; annot_multiline n lexbuf }
209 209

  
210 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) }
211
  | eof { make_spec loc (Buffer.contents buf) }
212
  | newline { incr_line lexbuf; make_spec loc (Buffer.contents buf) }
213 213
  | _ as c { Buffer.add_char buf c; spec_singleline loc lexbuf }
214 214

  
215 215
and spec_multiline loc n = parse
......
217 217
  | "*)" as s { if n > 0 then 
218 218
      (Buffer.add_string buf s; spec_multiline loc (n-1) lexbuf) 
219 219
    else 
220
      make_spec loc lexbuf (Buffer.contents buf) }
220
      make_spec loc (Buffer.contents buf) }
221 221
  | "(*" as s { Buffer.add_string buf s; spec_multiline loc (n+1) lexbuf }
222 222
  | newline as s { incr_line lexbuf; Buffer.add_string buf s; spec_multiline loc n lexbuf }
223 223
  | _ as c { Buffer.add_char buf c; spec_multiline loc n lexbuf }
src/parsers/parser_lustre.mly
14 14
open Lustre_types
15 15
open Corelang
16 16
open Dimension
17
open Parse
18 17

  
19 18
   
20 19
let get_loc () = Location.symbol_rloc ()
21 20

  
22 21
let mkident x = x, get_loc ()
23
let mktyp x = mktyp (get_loc ()) x
24
let mkclock x = mkclock (get_loc ()) x
22
let mktyp = mktyp (get_loc ())
23
let mkotyp x = match x with Some t -> Some (mktyp t) | None -> None
24
let mkclock = mkclock (get_loc ())
25 25
let mkvar_decl x loc = mkvar_decl loc ~orig:true x
26
let mkexpr x = mkexpr (get_loc ()) x
27
let mkeexpr x = mkeexpr (get_loc ()) x 
28
let mkeq x = mkeq (get_loc ()) x
29
let mkassert x = mkassert (get_loc ()) x
30
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x
31
let mkpredef_call x = mkpredef_call (get_loc ()) x
32
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
33

  
34
let mkdim_int i = mkdim_int (get_loc ()) i
35
let mkdim_bool b = mkdim_bool (get_loc ()) b
36
let mkdim_ident id = mkdim_ident (get_loc ()) id
37
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
38
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
39

  
40
let mkannots annots = { annots = annots; annot_loc = get_loc () }
26
let mkexpr = mkexpr (get_loc ())
27
let mkeexpr = mkeexpr (get_loc ())
28
let mkeq = mkeq (get_loc ())
29
let mkassert = mkassert (get_loc ())
30
let mktop_decl = mktop_decl (get_loc ()) (Location.get_module ())
31
let mkpredef_call = mkpredef_call (get_loc ())
32
let mkpredef_call_b f x1 x2 = mkpredef_call f [x1; x2]
33
let mkpredef_call_u f x = mkpredef_call f [x]
34

  
35
let mkdim_int = mkdim_int (get_loc ())
36
(* let mkdim_bool b = mkdim_bool (get_loc ()) b *)
37
let mkdim_ident = mkdim_ident (get_loc ())
38
let mkdim_appl = mkdim_appl (get_loc ())
39
let mkdim_appl_b f x1 x2 = mkdim_appl f [x1; x2]
40
let mkdim_appl_u f x = mkdim_appl f [x]
41
let mkdim_ite = mkdim_ite (get_loc ())
42

  
43
let mkarraytype = List.fold_left (fun t d -> Tydec_array (d, t))
44

  
45
let mkvdecls const typ clock expr =
46
  List.map (fun (id, loc) ->
47
      mkvar_decl (id,
48
                  mktyp (match typ with Some t -> t | None -> Tydec_any),
49
                  (match clock with Some ck -> ck | None -> mkclock Ckdec_any),
50
                  const, expr, None) loc)
51

  
52
(* let mkannots annots = { annots = annots; annot_loc = get_loc () } *)
41 53

  
42 54
let node_stack : ident list ref = ref []
43
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack
44
let push_node nd =  node_stack:= nd :: !node_stack
55
(* let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack *)
56
let push_node nd = node_stack := nd :: !node_stack; nd
45 57
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
46 58
let get_current_node () = try List.hd !node_stack with _ -> assert false
47 59

  
48 60
let rec fby expr n init =
49
  if n<=1 then
61
  if n <= 1 then
50 62
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
51 63
  else
52
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
64
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n - 1) init))))
53 65

  
54 66
 
55 67
%}
......
69 81
%token AMPERAMPER BARBAR NOT POWER
70 82
%token IF THEN ELSE
71 83
%token MERGE FBY WHEN WHENNOT EVERY
72
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST
84
%token NODE LET TEL RETURNS VAR TYPE CONST
73 85
%token STRUCT ENUM
74 86
%token TINT TREAL TBOOL TCLOCK
75 87
%token EQ LT GT LTE GTE NEQ
76 88
%token AND OR XOR IMPL
77 89
%token MULT DIV MOD
78
%token MINUS PLUS UMINUS
90
%token MINUS PLUS 
79 91
%token PRE ARROW
80 92
%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT
81 93
%token INVARIANT MODE CCODE MATLAB
......
83 95
%token PROTOTYPE LIB
84 96
%token EOF
85 97

  
86
%nonassoc prec_exists prec_forall
87
%nonassoc COMMA
98
%nonassoc p_string
99
%nonassoc p_vdecl
100
%left SCOL
88 101
%nonassoc EVERY
89
%left MERGE IF
90 102
%nonassoc ELSE
91 103
%right ARROW FBY
92 104
%left WHEN WHENNOT 
93
%right COLCOL
94 105
%right IMPL
95 106
%left OR XOR BARBAR
96 107
%left AND AMPERAMPER
97 108
%left NOT
98
%nonassoc INT
99 109
%nonassoc EQ LT GT LTE GTE NEQ
100 110
%left MINUS PLUS
101 111
%left MULT DIV MOD
102
%left UMINUS
112
%left p_uminus
103 113
%left POWER
104
%left PRE LAST
114
%left PRE
105 115
%nonassoc RBRACKET
106 116
%nonassoc LBRACKET
107 117

  
108
%start prog
109
%type <Lustre_types.top_decl list> prog
118
%start <Lustre_types.top_decl list> prog
110 119

  
111
%start header
112
%type <Lustre_types.top_decl list> header
120
%start <Lustre_types.top_decl list> header
113 121

  
114
%start lustre_annot
115
%type <Lustre_types.expr_annot> lustre_annot
122
%start <Lustre_types.expr_annot> lustre_annot
116 123

  
117
%start lustre_spec
118
%type <Lustre_types.spec_types> lustre_spec
124
%start <Lustre_types.spec_types> lustre_spec
119 125

  
120
%start signed_const
121
%type <Lustre_types.constant> signed_const
122

  
123
%start expr
124
%type <Lustre_types.expr> expr
125

  
126
%start stmt_list
127
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
128

  
129
%start vdecl_list
130
%type <Lustre_types.var_decl list> vdecl_list
131 126
%%
132 127

  
128
ident:
129
| x=UIDENT { x }
130
| x=IDENT  { x }
133 131

  
134 132
module_ident:
135
  UIDENT { $1 }
136
| IDENT  { $1 }
133
| m=ident { m }
137 134

  
138 135
file_ident:
139
module_ident { $1 } 
140
| module_ident POINT file_ident { $1 ^ "." ^ $3 } 
136
| m=module_ident                    { m }
137
| m=module_ident POINT f=file_ident { m ^ "." ^ f }
141 138

  
142 139
path_ident:
143
POINT DIV path_ident { "./" ^ $3 }
144
| file_ident DIV path_ident { $1 ^ "/" ^ $3 }
145
| DIV path_ident { "/" ^ $2 }
146
| file_ident { $1 }
140
| POINT DIV p=path_ident        { "./" ^ p }
141
| f=file_ident DIV p=path_ident { f ^ "/" ^ p }
142
| DIV p=path_ident              { "/" ^ p }
143
| f=file_ident                  { f }
147 144

  
148 145
tag_bool:
149
  | TRUE    { tag_true }
150
  | FALSE   { tag_false }
146
| TRUE  { tag_true }
147
| FALSE { tag_false }
151 148

  
152 149
tag_ident:
153
  UIDENT  { $1 }
154
  | tag_bool { $1 }
150
| t=UIDENT   { t }
151
| t=tag_bool { t }
155 152

  
156 153
node_ident:
157
  UIDENT { $1 }
158
| IDENT  { $1 }
154
| n=ident { n }
159 155

  
160 156
node_ident_decl:
161
 node_ident { push_node $1; $1 }
157
| n=node_ident { push_node n }
162 158

  
163 159
vdecl_ident:
164
  UIDENT { mkident $1 }
165
| IDENT  { mkident $1 }
160
| x=ident { mkident x }
166 161

  
167 162
const_ident:
168
  UIDENT { $1 }
169
| IDENT  { $1 }
163
| c=ident { c }
170 164

  
171 165
type_ident:
172
  IDENT { $1 }
166
| t=IDENT { t }
173 167

  
174 168
prog:
175
 prefix_prog top_decl_list EOF { $1 @ (List.rev $2) }
176

  
177
prefix_prog:
178
    { [] }
179
  | open_lusi prefix_prog { $1 :: $2 }
180
  | typ_def prefix_prog   { ($1 false (* not a header *)) :: $2 }
181

  
182
prefix_header:
183
    { [] }
184
  | open_lusi prefix_header { $1 :: $2 }
185
  | typ_def prefix_header   { ($1 true (* is a header *)) :: $2 }
169
| p=prefix ds=flatten(top_decl*) EOF { List.map ((|>) false) p @ ds }
186 170

  
187 171
header:
188
 prefix_header top_decl_header_list EOF { $1 @ (List.rev $2) }
172
| p=prefix ds=flatten(top_decl_header*) EOF { List.map ((|>) true) p @ ds }
189 173

  
174
prefix:
175
|                      { [] }
176
| o=open_lusi p=prefix { (fun _ -> o) :: p }
177
| td=typ_def p=prefix  { (fun is_header -> td is_header) :: p }
190 178

  
191 179
open_lusi:
192
  | OPEN QUOTE path_ident QUOTE { mktop_decl false (Open (true, $3)) }
193
  | INCLUDE QUOTE path_ident QUOTE { mktop_decl false (Include ($3)) }
194
  | OPEN LT path_ident GT { mktop_decl false (Open (false, $3))  }
195

  
196
top_decl_list:
197
   {[]}
198
| top_decl_list top_decl {$2@$1}
199

  
200

  
201
top_decl_header_list:
202
   { [] }
203
| top_decl_header_list top_decl_header { $2@$1 }
180
| OPEN QUOTE p=path_ident QUOTE    { mktop_decl false (Open (true, p)) }
181
| INCLUDE QUOTE p=path_ident QUOTE { mktop_decl false (Include p) }
182
| OPEN LT p=path_ident GT          { mktop_decl false (Open (false, p))  }
204 183

  
205 184
state_annot:
206
  FUNCTION { true }
207
| NODE { false }
185
| FUNCTION { true }
186
| NODE     { false }
208 187

  
209 188
top_decl_header:
210
| CONST cdecl_list { List.rev ($2 true) }
211
| 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
212
    {
213
      let inputs = List.rev $5 in
214
      let outputs = List.rev $10 in
215
      let nd = mktop_decl true (ImportedNode
216
				 {nodei_id = $3;
217
				  nodei_type = Types.new_var ();
218
				  nodei_clock = Clocks.new_var true;
219
				  nodei_inputs = inputs;
220
				  nodei_outputs = outputs;
221
				  nodei_stateless = $2;
222
				  nodei_spec = $1;
223
				  nodei_prototype = $13;
224
				  nodei_in_lib = $14;})
225
     in
226
     pop_node ();
227
     [nd] } 
228
| top_contract { [$1] }
229

  
230

  
231
prototype_opt:
232
 { None }
233
| PROTOTYPE node_ident { Some $2}
234

  
235
in_lib_list:
236
{ [] }
237
| LIB module_ident in_lib_list { $2::$3 } 
189
| CONST ds=cdecl+ SCOL
190
  { List.map ((|>) true) ds }
191
| nodei_spec=nodespecs nodei_stateless=state_annot nodei_id=node_ident_decl
192
  LPAR nodei_inputs=vdecl_list SCOL? RPAR
193
  RETURNS LPAR nodei_outputs=vdecl_list SCOL? RPAR
194
  nodei_prototype=preceded(PROTOTYPE, node_ident)?
195
  nodei_in_lib=preceded(LIB, module_ident)* SCOL
196
  { let nd = mktop_decl true (ImportedNode {
197
                                  nodei_id;
198
                                  nodei_type = Types.new_var ();
199
                                  nodei_clock = Clocks.new_var true;
200
                                  nodei_inputs;
201
                                  nodei_outputs;
202
                                  nodei_stateless;
203
                                  nodei_spec;
204
                                  nodei_prototype;
205
                                  nodei_in_lib
206
               })
207
    in
208
    pop_node ();
209
    [nd]
210
  }
211
| c=top_contract
212
  { [c] }
238 213

  
239 214
top_decl:
240
| CONST cdecl_list { List.rev ($2 false) }
241
| 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 
242
    {
243
     let stmts, asserts, annots = $16 in
244
      (* Declaring eqs annots *)
245
      List.iter (fun ann -> 
246
	List.iter (fun (key, _) -> 
247
	  Annotations.add_node_ann $2 key
248
	) ann.annots
249
      ) annots;
250
      (* Building the node *)
251
      let inputs = List.rev $4 in
252
      let outputs = List.rev $9 in
253
     let nd = mktop_decl false (Node
254
				  {node_id = $2;
255
				   node_type = Types.new_var ();
256
				   node_clock = Clocks.new_var true;
257
				   node_inputs = inputs;
258
				   node_outputs = outputs;
259
				   node_locals = List.rev $14;
260
				   node_gencalls = [];
261
				   node_checks = [];
262
				   node_asserts = asserts; 
263
				   node_stmts = stmts;
264
				   node_dec_stateless = $1;
265
				   node_stateless = None;
266
				   node_spec = $13;
267
				   node_annot = annots;
268
				   node_iscontract = false;
269
			       })
270
     in
271
     pop_node ();
272
     (*add_node $3 nd;*) [nd] }
273

  
274

  
275
| NODESPEC
276
    { match $1 with
277
      | LocalContract c -> assert false
278
      | TopContract c   -> c
279
			 
280
    }
215
| CONST ds=cdecl+ SCOL
216
  { List.map ((|>) false) ds }
217
| node_dec_stateless=state_annot node_id=node_ident_decl
218
  LPAR node_inputs=vdecl_list SCOL? RPAR
219
  RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?
220
  node_spec=nodespecs
221
  node_locals=locals LET content=stmt_list TEL
222
  { let node_stmts, node_asserts, node_annot = content in
223
    (* Declaring eqs annots *)
224
    List.iter (fun ann ->
225
        List.iter (fun (key, _) ->
226
            Annotations.add_node_ann node_id key)
227
          ann.annots)
228
      node_annot;
229
    (* Building the node *)
230
    let nd = mktop_decl false (Node
231
                                 {node_id;
232
                                  node_type = Types.new_var ();
233
                                  node_clock = Clocks.new_var true;
234
                                  node_inputs;
235
                                  node_outputs;
236
                                  node_locals;
237
                                  node_gencalls = [];
238
                                  node_checks = [];
239
                                  node_asserts;
240
                                  node_stmts;
241
                                  node_dec_stateless;
242
                                  node_stateless = None;
243
                                  node_spec;
244
                                  node_annot;
245
                                  node_iscontract = false;
246
               })
247
    in
248
    pop_node ();
249
    (*add_node $3 nd;*)
250
    [nd]
251
  }
252
| s=NODESPEC
253
  { match s with
254
    | LocalContract _ -> assert false
255
    | TopContract c   -> c
256
  }
281 257

  
282 258
nodespecs:
283
nodespec_list {
284
  match $1 with
285
  | None -> None 
286
  | Some c -> Some (Contract c)
287
}
259
| ss=nodespec_list
260
  { match ss with
261
    | None   -> None
262
    | Some c -> Some (Contract c)
263
  }
288 264

  
289 265
nodespec_list:
290
 { None }
291
  | NODESPEC nodespec_list {
292
	       let extract x = match x with LocalContract c -> c | _ -> assert false in
293
	       let s1 = extract $1 in
294
	       match $2 with
295
	       | None -> Some s1
296
	       | Some s2 -> Some (merge_contracts s1 s2) }
297

  
298
typ_def_list:
299
    /* empty */             { (fun itf -> []) }
300
| typ_def typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($2 itf)) }
266
| { None }
267
| s=NODESPEC ss=nodespec_list
268
  { let extract x = match x with LocalContract c -> c | _ -> assert false in
269
    let s1 = extract s in
270
    match ss with
271
    | None -> Some s1
272
    | Some s2 -> Some (merge_contracts s1 s2)
273
  }
301 274

  
302 275
typ_def:
303
  TYPE type_ident EQ typ_def_rhs SCOL { (fun itf ->
304
			       let typ = mktop_decl itf (TypeDef { tydef_id = $2;
305
								   tydef_desc = $4
306
							})
307
			       in (*add_type itf $2 typ;*) typ) }
276
| TYPE tydef_id=type_ident EQ tydef_desc=typ_def_rhs SCOL
277
  { fun itf ->
278
    let typ = mktop_decl itf (TypeDef { tydef_id; tydef_desc }) in
279
    (*add_type itf $2 typ;*)
280
    typ
281
  }
308 282

  
309 283
typ_def_rhs:
310
  typeconst                   { $1 }
311
| ENUM LCUR tag_list RCUR     { Tydec_enum (List.rev $3) }
312
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
284
| t=typeconst
285
  { t }
286
| ENUM LCUR ts=separated_nonempty_list(COMMA, UIDENT) RCUR
287
  { Tydec_enum ts }
288
| STRUCT LCUR fs=separated_list(SCOL, separated_pair(IDENT, COL, typeconst)) RCUR
289
  { Tydec_struct fs }
313 290

  
314
array_typ_decl:
315
 %prec POWER                { fun typ -> typ }
316
 | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
291
%inline array_typ_decl:
292
|                          { [] }
293
| ds=preceded(POWER, dim)+ { ds }
317 294

  
318 295
typeconst:
319
  TINT array_typ_decl   { $2 Tydec_int }
320
| TBOOL array_typ_decl  { $2 Tydec_bool  }
321
| TREAL array_typ_decl  { $2 Tydec_real  }
322
/* | TFLOAT array_typ_decl { $2 Tydec_float } */
323
| type_ident array_typ_decl  { $2 (Tydec_const $1) }
324
| TBOOL TCLOCK          { Tydec_clock Tydec_bool }
325
| IDENT TCLOCK          { Tydec_clock (Tydec_const $1) }
326

  
327
tag_list:
328
  UIDENT                { $1 :: [] }
329
| tag_list COMMA UIDENT { $3 :: $1 }
330
      
331
field_list:                           { [] }
332
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
333
      
296
| TINT ds=array_typ_decl         { mkarraytype Tydec_int ds }
297
| TBOOL ds=array_typ_decl        { mkarraytype Tydec_bool ds }
298
| TREAL ds=array_typ_decl        { mkarraytype Tydec_real ds }
299
/* | TFLOAT ds=array_typ_decl { mkarraytype Tydec_float ds } */
300
| t=type_ident ds=array_typ_decl { mkarraytype (Tydec_const t) ds }
301
| TBOOL TCLOCK                   { Tydec_clock Tydec_bool }
302
| t=IDENT TCLOCK                 { Tydec_clock (Tydec_const t) }
303

  
334 304
stmt_list:
335
  { [], [], [] }
336
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
337
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
338
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
339
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
305
| { [], [], [] }
306
| e=eq ss=stmt_list
307
  { let eql, assertl, annotl = ss in
308
    Eq e :: eql, assertl, annotl
309
  }
310
| a=assert_ ss=stmt_list
311
  { let eql, assertl, annotl = ss in
312
    eql, a :: assertl, annotl
313
  }
314
| a=ANNOT ss=stmt_list
315
  { let eql, assertl, annotl = ss in
316
    eql, assertl, a :: annotl
317
  }
318
| a=automaton ss=stmt_list
319
  { let eql, assertl, annotl = ss in
320
    Aut a :: eql, assertl, annotl
321
  }
340 322

  
341 323
automaton:
342
 AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
343

  
344
handler_list:
345
     { [] }
346
| handler handler_list { $1::$2 }
324
| AUTOMATON t=type_ident hs=handler* { Automata.mkautomata (get_loc ()) t hs }
347 325

  
348 326
handler:
349
 STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
350

  
351
unless_list:
352
    { [] }
353
| unless unless_list { $1::$2 }
354

  
355
until_list:
356
    { [] }
357
| until until_list { $1::$2 }
327
| STATE x=UIDENT COL ul=unless* l=locals LET ss=stmt_list TEL ut=until*
328
  { Automata.mkhandler (get_loc ()) x ul ut l ss }
358 329

  
359 330
unless:
360
  UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
361
| UNLESS expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
331
| UNLESS e=expr RESTART s=UIDENT { get_loc (), e, true, s  }
332
| UNLESS e=expr RESUME s=UIDENT  { get_loc (), e, false, s }
362 333

  
363 334
until:
364
  UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4)  }
365
| UNTIL expr RESUME UIDENT  { (get_loc (), $2, false, $4) }
335
| UNTIL e=expr RESTART s=UIDENT { get_loc (), e, true, s }
336
| UNTIL e=expr RESUME s=UIDENT  { get_loc (), e, false, s }
366 337

  
367 338
assert_:
368
| ASSERT expr SCOL {mkassert ($2)}
339
| ASSERT e=expr SCOL { mkassert e }
369 340

  
370 341
eq:
371
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
372
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
342
| xs=pattern EQ e=expr SCOL {mkeq (List.map fst xs, e)}
373 343

  
374
lustre_spec:
375
| top_contracts EOF     { TopContract $1 }
376
| contract_content EOF { LocalContract $1}
344
%inline pattern:
345
| xs=ident_list           { xs }
346
| LPAR xs=ident_list RPAR { xs }
377 347

  
378
top_contracts:
379
| top_contract { [$1] }
380
| top_contract top_contracts { $1::$2 }
348
lustre_spec:
349
| cs=top_contract+ EOF   { TopContract cs }
350
| c=contract_content EOF { LocalContract c }
381 351

  
382 352
top_contract:
383
| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL 
384
    {
385
      let nd = mktop_decl true (Node
386
				 {node_id = $2;
387
				  node_type = Types.new_var ();
388
				  node_clock = Clocks.new_var true;
389
				  node_inputs = List.rev $4;
390
				  node_outputs = List.rev $9;
391
				  node_locals = []; (* will be filled later *)
392
				  node_gencalls = [];
393
				  node_checks = [];
394
				  node_asserts = [];
395
				  node_stmts = []; (* will be filled later *)
396
				  node_dec_stateless = false;
397
				  (* By default we assume contracts as stateful *)
398
				  node_stateless = None;
399
				  node_spec = Some (Contract $14);
400
				  node_annot = [];
401
				  node_iscontract = true;
402
				 }
403
			       )
404
     in
405
     pop_node ();
406
     (*add_imported_node $3 nd;*)
407
     nd }
353
| CONTRACT node_id=node_ident_decl
354
  LPAR node_inputs=vdecl_list SCOL? RPAR
355
  RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?
356
  LET cc=contract_content TEL
357
  { let nd = mktop_decl true (Node {
358
                                  node_id;
359
                                  node_type = Types.new_var ();
360
                                  node_clock = Clocks.new_var true;
361
                                  node_inputs;
362
                                  node_outputs;
363
                                  node_locals = []; (* will be filled later *)
364
                                  node_gencalls = [];
365
                                  node_checks = [];
366
                                  node_asserts = [];
367
                                  node_stmts = []; (* will be filled later *)
368
                                  node_dec_stateless = false;
369
                                  (* By default we assume contracts as stateful *)
370
                                  node_stateless = None;
371
                                  node_spec = Some (Contract cc);
372
                                  node_annot = [];
373
                                  node_iscontract = true;
374
                                }
375
               )
376
    in
377
    pop_node ();
378
    (*add_imported_node $3 nd;*)
379
    nd
380
  }
408 381

  
409 382
contract_content:
410
{ empty_contract }
411
| CONTRACT contract_content { $2 }
412
| CONST IDENT EQ expr SCOL contract_content
413
    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
414
| CONST IDENT COL typeconst EQ expr SCOL contract_content
415
    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
416
| VAR IDENT COL typeconst EQ expr SCOL contract_content
417
    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
418
| ASSUME qexpr SCOL contract_content
419
    { merge_contracts (mk_contract_assume $2) $4 }
420
| ASSUME STRING qexpr SCOL contract_content
421
    { merge_contracts (mk_contract_assume ~name:$2 $3) $5 }
422
| GUARANTEES qexpr SCOL contract_content	
423
    { merge_contracts (mk_contract_guarantees $2) $4 }
424
| GUARANTEES STRING qexpr SCOL contract_content	
425
    { merge_contracts (mk_contract_guarantees ~name:$2 $3) $5 }
426
| MODE IDENT LPAR mode_content RPAR SCOL contract_content
427
	{ merge_contracts (
428
	  let r, e = $4 in 
429
	  mk_contract_mode $2 r e (get_loc())) $7 }	
430
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content
431
    { merge_contracts (mk_contract_import $2  (mkexpr (Expr_tuple (List.rev $4)))  (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
432
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content
433
    { merge_contracts (mk_contract_import $2  $4  (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
434
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
435
    { merge_contracts (mk_contract_import $2  (mkexpr (Expr_tuple (List.rev $4)))  $8 (get_loc())) $11 }
436
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
437
    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }
383
| { empty_contract }
384
| CONTRACT cc=contract_content
385
  { cc }
386
| CONST x=IDENT COL t=typeconst? EQ e=expr SCOL cc=contract_content
387
  { merge_contracts (mk_contract_var x true (mkotyp t) e (get_loc())) cc }
388
| VAR x=IDENT COL t=typeconst EQ e=expr SCOL cc=contract_content
389
  { merge_contracts (mk_contract_var x false (Some (mktyp t)) e (get_loc())) cc }
390
| ASSUME x=ioption(STRING) e=qexpr SCOL cc=contract_content
391
  { merge_contracts (mk_contract_assume x e) cc }
392
| GUARANTEES x=ioption(STRING) e=qexpr SCOL cc=contract_content
393
  { merge_contracts (mk_contract_guarantees x e) cc }
394
| MODE x=IDENT LPAR mc=mode_content RPAR SCOL cc=contract_content
395
  { merge_contracts (
396
        let r, e = mc in
397
        mk_contract_mode x r e (get_loc())) cc
398
  }
399
| IMPORT x=IDENT LPAR xs=expr_or_tuple RPAR RETURNS LPAR ys=expr_or_tuple RPAR
400
  SCOL cc=contract_content
401
  { merge_contracts (mk_contract_import x xs ys (get_loc())) cc }
402

  
403
%inline expr_or_tuple:
404
| e=expr                     { e }
405
| e=expr COMMA es=array_expr { mkexpr (Expr_tuple (e :: es)) }
438 406

  
439 407
mode_content:
440
{ [], [] }
441
| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e }
442
| REQUIRE STRING qexpr SCOL mode_content { let (r,e) = $5 in {$3 with eexpr_name = Some $2}::r, e }
443
| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e }
444
| ENSURE STRING qexpr SCOL mode_content { let (r,e) = $5 in r, {$3 with eexpr_name = Some $2}::e }
445

  
446
/* WARNING: UNUSED RULES */
447
tuple_qexpr:
448
| qexpr COMMA qexpr {[$3;$1]}
449
| tuple_qexpr COMMA qexpr {$3::$1}
408
| { [], [] }
409
| REQUIRE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
410
  { let (r, e) = mc in
411
    { qe with eexpr_name } :: r, e }
412
| ENSURE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
413
  { let (r, e) = mc in
414
    r, { qe with eexpr_name } :: e }
415

  
416
(* /* WARNING: UNUSED RULES */
417
 * tuple_qexpr:
418
 * | qexpr COMMA qexpr {[$3;$1]}
419
 * | tuple_qexpr COMMA qexpr {$3::$1} *)
450 420

  
451 421
qexpr:
452
| expr { mkeexpr $1 }
422
| e=expr                      { mkeexpr e }
453 423
  /* Quantifiers */
454
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
455
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
424
| EXISTS x=vdecl SCOL e=qexpr { extend_eexpr [Exists, x] e }
425
| FORALL x=vdecl SCOL e=qexpr { extend_eexpr [Forall, x] e }
456 426

  
457

  
458
tuple_expr:
459
    expr COMMA expr {[$3;$1]}
460
| tuple_expr COMMA expr {$3::$1}
427
(* %inline tuple_expr:
428
 * | e=expr COMMA es=array_expr { e :: es } *)
461 429

  
462 430
// Same as tuple expr but accepting lists with single element
463
array_expr:
464
  expr {[$1]}
465
| expr COMMA array_expr {$1::$3}
466

  
467
dim_list:
468
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
469
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
431
%inline array_expr:
432
| es=separated_nonempty_list(COMMA, expr) { es }
470 433

  
471 434
expr:
472 435
/* constants */
473
  INT {mkexpr (Expr_const (Const_int $1))}
474
| REAL {mkexpr (Expr_const (Const_real $1))}
475
| STRING {mkexpr (Expr_const (Const_string $1))}
476
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))} 
477
    
478
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
436
| c=INT                   { mkexpr (Expr_const (Const_int c)) }
437
| c=REAL                  { mkexpr (Expr_const (Const_real c)) }
438
| c=STRING %prec p_string { mkexpr (Expr_const (Const_string c)) }
439
| COLCOL c=IDENT          { mkexpr (Expr_const (Const_modeid c)) }
440
/* | c=FLOAT { mkexpr (Expr_const (Const_float c)) }*/
441

  
479 442
/* Idents or type enum tags */
480
| IDENT { mkexpr (Expr_ident $1) }
481
| UIDENT { mkexpr (Expr_ident $1) (* TODO we will differenciate enum constants from variables later *) }
482
| tag_bool {
483
	(* on sept 2014, X chenged the Const to 
484
	mkexpr (Expr_ident $1)
485
	reverted back to const on july 2019 *)
486
	mkexpr (Expr_const (Const_tag $1)) }
487
| LPAR ANNOT expr RPAR
488
    {update_expr_annot (get_current_node ()) $3 $2}
489
| LPAR expr RPAR
490
    {$2}
491
| LPAR tuple_expr RPAR
492
    {mkexpr (Expr_tuple (List.rev $2))}
443
| x=IDENT    { mkexpr (Expr_ident x) }
444
| x=UIDENT   { mkexpr (Expr_ident x) (* TODO we will differenciate enum constants from variables later *) }
445
| t=tag_bool { mkexpr (Expr_const (Const_tag t)) } (* on sept 2014, X changed the Const to
446
                                                      mkexpr (Expr_ident $1)
447
                                                      reverted back to const on july 2019 *)
448
| LPAR a=ANNOT e=expr RPAR  { update_expr_annot (get_current_node ()) e a }
449
| LPAR e=expr_or_tuple RPAR { e }
493 450

  
494 451
/* Array expressions */
495
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
496
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
497
| expr LBRACKET dim_list { $3 $1 }
452
| LBRACKET es=array_expr RBRACKET
453
  { mkexpr (Expr_array es) }
454
| e=expr POWER d=dim
455
  { mkexpr (Expr_power (e, d)) }
456
| e=expr ds=delimited(LBRACKET, dim, RBRACKET)+
457
  { List.fold_left (fun base d -> mkexpr (Expr_access (base, d))) e ds }
498 458

  
499 459
/* Temporal operators */
500
| PRE expr 
501
    {mkexpr (Expr_pre $2)}
502
| expr ARROW expr 
503
    {mkexpr (Expr_arrow ($1,$3))}
504
| expr FBY expr 
505
    {(*mkexpr (Expr_fby ($1,$3))*)
506
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
507
| expr WHEN vdecl_ident
508
    {mkexpr (Expr_when ($1,fst $3,tag_true))}
509
| expr WHENNOT vdecl_ident
510
    {mkexpr (Expr_when ($1,fst $3,tag_false))}
511
| expr WHEN tag_ident LPAR vdecl_ident RPAR
512
    {mkexpr (Expr_when ($1, fst $5, $3))}
513
| MERGE vdecl_ident handler_expr_list
514
    {mkexpr (Expr_merge (fst $2,$3))}
460
| PRE e=expr
461
  { mkexpr (Expr_pre e) }
462
| e1=expr ARROW e2=expr
463
  { mkexpr (Expr_arrow (e1, e2)) }
464
| e1=expr FBY e2=expr
465
  { mkexpr (Expr_arrow (e1, mkexpr (Expr_pre e2))) }
466
| e=expr WHEN x=vdecl_ident
467
  { mkexpr (Expr_when (e, fst x, tag_true)) }
468
| e=expr WHENNOT x=vdecl_ident
469
  { mkexpr (Expr_when (e, fst x, tag_false)) }
470
| e=expr WHEN t=tag_ident LPAR x=vdecl_ident RPAR
471
  { mkexpr (Expr_when (e, fst x, t)) }
472
| MERGE x=vdecl_ident
473
  hs=delimited(LPAR, separated_pair(tag_ident, ARROW, expr), RPAR)*
474
  { mkexpr (Expr_merge (fst x, hs)) }
515 475

  
516 476
/* Applications */
517
| node_ident LPAR expr RPAR
518
    {mkexpr (Expr_appl ($1, $3, None))}
519
| node_ident LPAR expr RPAR EVERY expr
520
    {mkexpr (Expr_appl ($1, $3, Some $6))}
521
| node_ident LPAR tuple_expr RPAR
522
    {
523
      let id=$1 in
524
      let args=List.rev $3 in
525
      match id, args with
526
      | "fbyn", [expr;n;init] ->
527
	let n = match n.expr_desc with
528
	  | Expr_const (Const_int n) -> n
529
	  | _ -> assert false
530
	in
531
	fby expr n init
532
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
533
    }
534
| node_ident LPAR tuple_expr RPAR EVERY expr
535
    {
536
      let id=$1 in
537
      let args=List.rev $3 in
538
      let clock=$6 in
539
      if id="fby" then
540
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
541
      else
542
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 
543
    }
477
| f=node_ident LPAR es=expr_or_tuple RPAR r=preceded(EVERY, expr)?
478
  { match f, es.expr_desc, r with
479
    | "fbyn", Expr_tuple [expr; n; init], None ->
480
       let n = match n.expr_desc with
481
         | Expr_const (Const_int n) -> n
482
         | _ -> assert false
483
       in
484
       fby expr n init
485
    | "fbyn", _ , Some _ ->
486
       assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
487
    | _ -> mkexpr (Expr_appl (f, es, r))
488
  }
544 489

  
545 490
/* Boolean expr */
546
| expr AND expr 
547
    {mkpredef_call "&&" [$1;$3]}
548
| expr AMPERAMPER expr 
549
    {mkpredef_call "&&" [$1;$3]}
550
| expr OR expr 
551
    {mkpredef_call "||" [$1;$3]}
552
| expr BARBAR expr 
553
    {mkpredef_call "||" [$1;$3]}
554
| expr XOR expr 
555
    {mkpredef_call "xor" [$1;$3]}
556
| NOT expr 
557
    {mkpredef_call "not" [$2]}
558
| expr IMPL expr 
559
    {mkpredef_call "impl" [$1;$3]}
491
| e1=expr AND e2=expr         { mkpredef_call_b "&&" e1 e2 }
492
| e1=expr AMPERAMPER e2=expr  { mkpredef_call_b "&&" e1 e2 }
493
| e1=expr OR e2=expr          { mkpredef_call_b "||" e1 e2 }
494
| e1=expr BARBAR e2=expr      { mkpredef_call_b "||" e1 e2 }
495
| e1=expr XOR e2=expr         { mkpredef_call_b "xor" e1 e2 }
496
| NOT e=expr                  { mkpredef_call_u "not" e }
497
| e1=expr IMPL e2=expr        { mkpredef_call_b "impl" e1 e2 }
560 498

  
561 499
/* Comparison expr */
562
| expr EQ expr 
563
    {mkpredef_call "=" [$1;$3]}
564
| expr LT expr 
565
    {mkpredef_call "<" [$1;$3]}
566
| expr LTE expr 
567
    {mkpredef_call "<=" [$1;$3]}
568
| expr GT expr 
569
    {mkpredef_call ">" [$1;$3]}
570
| expr GTE  expr 
571
    {mkpredef_call ">=" [$1;$3]}
572
| expr NEQ expr 
573
    {mkpredef_call "!=" [$1;$3]}
500
| e1=expr EQ e2=expr          { mkpredef_call_b "=" e1 e2 }
501
| e1=expr LT e2=expr          { mkpredef_call_b "<" e1 e2 }
502
| e1=expr LTE e2=expr         { mkpredef_call_b "<=" e1 e2 }
503
| e1=expr GT e2=expr          { mkpredef_call_b ">" e1 e2 }
504
| e1=expr GTE e2=expr         { mkpredef_call_b ">=" e1 e2 }
505
| e1=expr NEQ e2=expr         { mkpredef_call_b "!=" e1 e2 }
574 506

  
575 507
/* Arithmetic expr */
576
| expr PLUS expr 
577
    {mkpredef_call "+" [$1;$3]}
578
| expr MINUS expr 
579
    {mkpredef_call "-" [$1;$3]}
580
| expr MULT expr 
581
    {mkpredef_call "*" [$1;$3]}
582
| expr DIV expr 
583
    {mkpredef_call "/" [$1;$3]}
584
| MINUS expr %prec UMINUS
585
  {mkpredef_call "uminus" [$2]}
586
| expr MOD expr 
587
    {mkpredef_call "mod" [$1;$3]}
508
| e1=expr PLUS e2=expr        { mkpredef_call_b "+" e1 e2 }
509
| e1=expr MINUS e2=expr       { mkpredef_call_b "-" e1 e2 }
510
| e1=expr MULT e2=expr        { mkpredef_call_b "*" e1 e2 }
511
| e1=expr DIV e2=expr         { mkpredef_call_b "/" e1 e2 }
512
| MINUS e=expr %prec p_uminus { mkpredef_call_u "uminus" e }
513
| e1=expr MOD e2=expr         { mkpredef_call_b "mod" e1 e2 }
588 514

  
589 515
/* If */
590
| IF expr THEN expr ELSE expr
591
    {mkexpr (Expr_ite ($2, $4, $6))}
592

  
593
handler_expr_list:
594
   { [] }
595
| handler_expr handler_expr_list { $1 :: $2 }
596

  
597
handler_expr:
598
 LPAR tag_ident ARROW expr RPAR { ($2, $4) }
599

  
600
signed_const_array:
601
| signed_const { [$1] }
602
| signed_const COMMA signed_const_array { $1 :: $3 }
603

  
604
signed_const_struct:
605
| IDENT EQ signed_const { [ ($1, $3) ] }
606
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
516
| IF e=expr THEN t=expr ELSE f=expr { mkexpr (Expr_ite (e, t, f)) }
607 517

  
608 518
signed_const:
609
  INT {Const_int $1}
610
| REAL {Const_real $1}
611
/* | FLOAT {Const_float $1} */
612
| tag_ident {Const_tag $1}
613
| MINUS INT {Const_int (-1 * $2)}
614
| MINUS REAL {Const_real (Real.uminus $2)}
615
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
616
| LCUR signed_const_struct RCUR { Const_struct $2 }
617
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
519
| c=INT
520
  { Const_int c }
521
| c=REAL
522
  { Const_real c }
523
/* | c=FLOAT { Const_float c } */
524
| t=tag_ident { Const_tag t }
525
| MINUS c=INT
526
  { Const_int (-1 * c) }
527
| MINUS c=REAL
528
  { Const_real (Real.uminus c) }
529
/* | MINUS c=FLOAT { Const_float (-1. *. c) } */
530
| LCUR
531
  cs=separated_nonempty_list(COMMA, separated_pair(IDENT, EQ, signed_const))
532
  RCUR
533
  { Const_struct cs }
534
| LBRACKET cs=separated_nonempty_list(COMMA, signed_const) RBRACKET
535
  { Const_array cs }
618 536

  
619 537
dim:
620
   INT { mkdim_int $1 }
621
| LPAR dim RPAR { $2 }
622
| UIDENT { mkdim_ident $1 }
623
| IDENT { mkdim_ident $1 }
624
| dim AND dim 
625
    {mkdim_appl "&&" [$1;$3]}
626
| dim AMPERAMPER dim 
627
    {mkdim_appl "&&" [$1;$3]}
628
| dim OR dim 
629
    {mkdim_appl "||" [$1;$3]}
630
| dim BARBAR dim 
631
    {mkdim_appl "||" [$1;$3]}
632
| dim XOR dim 
633
    {mkdim_appl "xor" [$1;$3]}
634
| NOT dim 
635
    {mkdim_appl "not" [$2]}
636
| dim IMPL dim 
637
    {mkdim_appl "impl" [$1;$3]}
538
| i=INT                      { mkdim_int i }
539
| LPAR d=dim RPAR            { d }
540
| x=ident                    { mkdim_ident x }
541
| d1=dim AND d2=dim          { mkdim_appl_b "&&" d1 d2 }
542
| d1=dim AMPERAMPER d2=dim   { mkdim_appl_b "&&" d1 d2 }
543
| d1=dim OR d2=dim           { mkdim_appl_b "||" d1 d2 }
544
| d1=dim BARBAR d2=dim       { mkdim_appl_b "||" d1 d2 }
545
| d1=dim XOR d2=dim          { mkdim_appl_b "xor" d1 d2 }
546
| NOT d=dim                  { mkdim_appl_u "not" d }
547
| d1=dim IMPL d2=dim         { mkdim_appl_b "impl" d1 d2 }
638 548

  
639 549
/* Comparison dim */
640
| dim EQ dim 
641
    {mkdim_appl "=" [$1;$3]}
642
| dim LT dim 
643
    {mkdim_appl "<" [$1;$3]}
644
| dim LTE dim 
645
    {mkdim_appl "<=" [$1;$3]}
646
| dim GT dim 
647
    {mkdim_appl ">" [$1;$3]}
648
| dim GTE  dim 
649
    {mkdim_appl ">=" [$1;$3]}
650
| dim NEQ dim 
651
    {mkdim_appl "!=" [$1;$3]}
550
| d1=dim EQ d2=dim           { mkdim_appl_b "=" d1 d2 }
551
| d1=dim LT d2=dim           { mkdim_appl_b "<" d1 d2 }
552
| d1=dim LTE d2=dim          { mkdim_appl_b "<=" d1 d2 }
553
| d1=dim GT d2=dim           { mkdim_appl_b ">" d1 d2 }
554
| d1=dim GTE  d2=dim         { mkdim_appl_b ">=" d1 d2 }
555
| d1=dim NEQ d2=dim          { mkdim_appl_b "!=" d1 d2 }
652 556

  
653 557
/* Arithmetic dim */
654
| dim PLUS dim 
655
    {mkdim_appl "+" [$1;$3]}
656
| dim MINUS dim 
657
    {mkdim_appl "-" [$1;$3]}
658
| dim MULT dim 
659
    {mkdim_appl "*" [$1;$3]}
660
| dim DIV dim 
661
    {mkdim_appl "/" [$1;$3]}
662
| MINUS dim %prec UMINUS
663
  {mkdim_appl "uminus" [$2]}
664
| dim MOD dim 
665
    {mkdim_appl "mod" [$1;$3]}
558
| d1=dim PLUS d2=dim         { mkdim_appl_b "+" d1 d2 }
559
| d1=dim MINUS d2=dim        { mkdim_appl_b "-" d1 d2 }
560
| d1=dim MULT d2=dim         { mkdim_appl_b "*" d1 d2 }
561
| d1=dim DIV d2=dim          { mkdim_appl_b "/" d1 d2 }
562
| MINUS d=dim %prec p_uminus { mkdim_appl_u "uminus" d }
563
| d1=dim MOD d2=dim          { mkdim_appl_b "mod" d1 d2 }
564

  
666 565
/* If */
667
| IF dim THEN dim ELSE dim
668
    {mkdim_ite $2 $4 $6}
566
| IF d=dim THEN t=dim ELSE f=dim { mkdim_ite d t f }
669 567

  
670
locals:
671
  {[]}
672
| VAR local_vdecl_list SCOL {$2}
568
%inline locals:
569
| xs=loption(preceded(VAR, flatten(separated_nonempty_list(SCOL, local_vdecl))))
570
  { xs }
673 571

  
674 572
vdecl_list:
675
  vdecl {$1}
676
| vdecl_list SCOL vdecl {$3 @ $1}
573
| d=vdecl %prec p_vdecl { d }
574
| d=vdecl SCOL ds=vdecl_list { d @ ds }
677 575

  
678 576
vdecl:
679
  ident_list COL typeconst clock 
680
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
681
| CONST ident_list /* static parameters don't have clocks */
682
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }
683
| CONST ident_list COL typeconst /* static parameters don't have clocks */
684
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }
685

  
686
local_vdecl_list:
687
  local_vdecl {$1}
688
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
577
| xs=ident_list COL t=typeconst c=clock?
578
  { mkvdecls false (Some t) c None xs }
579
| CONST xs=ident_list t=preceded(COL, typeconst)?
580
  /* static parameters don't have clocks */
581
  { mkvdecls true t None None xs }
689 582

  
690 583
local_vdecl:
691
/* Useless no ?*/    ident_list
692
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }
693
| ident_list COL typeconst clock 
694
    { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
695
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
696
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }
697
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
698
    { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }
699

  
700
cdecl_list:
701
  cdecl SCOL { (fun itf -> [$1 itf]) }
702
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
584
| xs=ident_list /* Useless no ?*/
585
  { mkvdecls false None None None xs }
586
| xs=ident_list COL t=typeconst c=clock?
587
  { mkvdecls false (Some t) c None xs }
588
| CONST x=vdecl_ident t=preceded(COL, typeconst)? EQ e=expr
589
  /* static parameters don't have clocks */
590
  { mkvdecls true t None (Some e) [x] }
703 591

  
704 592
cdecl:
705
    const_ident EQ signed_const {
706
      (fun itf -> 
707
       let c = mktop_decl itf (Const {
708
				   const_id = $1;
709
				   const_loc = get_loc ();
710
				   const_type = Types.new_var ();
711
				   const_value = $3})
712
       in
713
       (*add_const itf $1 c;*) c)
714
    }
715

  
716
clock:
717
    {mkclock Ckdec_any}
718
| when_list
719
    {mkclock (Ckdec_bool (List.rev $1))}
593
| x=const_ident EQ c=signed_const
594
  { fun itf ->
595
    let c = mktop_decl itf (Const {
596
                                const_id = x;
597
                                const_loc = get_loc ();
598
                                const_type = Types.new_var ();
599
                                const_value = c
600
              })
601
    in
602
    (*add_const itf $1 c;*)
603
    c
604
  }
605

  
606
%inline clock:
607
| l=when_cond+ { mkclock (Ckdec_bool l) }
720 608

  
721 609
when_cond:
722
  WHEN IDENT {($2, tag_true)}
723
| WHENNOT IDENT {($2, tag_false)}
724
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
725

  
726
when_list:
727
    when_cond {[$1]}
728
| when_list when_cond {$2::$1}
729

  
730
ident_list:
731
  vdecl_ident {[$1]}
732
| ident_list COMMA vdecl_ident {$3::$1}
733

  
734
SCOL_opt:
735
    SCOL {} | {}
610
| WHEN x=IDENT                       { x, tag_true }
611
| WHENNOT x=IDENT                    { x, tag_false }
612
| WHEN t=tag_ident LPAR x=IDENT RPAR { x, t }
736 613

  
614
%inline ident_list:
615
| ds=separated_nonempty_list(COMMA, vdecl_ident) { ds }
737 616

  
738 617
lustre_annot:
739
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
618
| lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
740 619

  
741 620
lustre_annot_list:
742 621
  { [] } 
svnignore
1
*.cmx
2
*.cmo
3
*.cmi
4
*.annot
5
*.tgz
6
*.output
7
lexer.ml
8
parser.mli
9
parser.ml
10
preludec.opt
11
preludec
12
prelude-*

Also available in: Unified diff