Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / parserLustreSpec.mly @ 22fe1c93

History | View | Annotate | Download (5.86 KB)

1
%{
2
  open Utils
3
  open Corelang
4
  open LustreSpec
5
  
6
  let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x
7
  let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x
8
  let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x
9
  
10
  let mktyp x = mktyp (Location.symbol_rloc ()) x
11
  let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x
12
  let mkclock x = mkclock (Location.symbol_rloc ()) x
13

    
14
%}
15

    
16

    
17
%token <int> INT
18
%token <string> REAL
19
%token <float> FLOAT
20
%token <string> STRING
21
%token TRUE FALSE STATELESS ASSERT INCLUDE QUOTE
22
%token <string> IDENT
23
%token LPAR RPAR SCOL COL COMMA COLCOL
24
%token AMPERAMPER BARBAR NOT POWER
25
%token IF THEN ELSE
26
%token UCLOCK DCLOCK PHCLOCK TAIL
27
%token MERGE FBY WHEN WHENNOT EVERY
28
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
29
%token TINT TFLOAT TREAL TBOOL TCLOCK
30
%token RATE DUE
31
%token EQ LT GT LTE GTE NEQ
32
%token AND OR XOR IMPL
33
%token MULT DIV MOD
34
%token MINUS PLUS UMINUS
35
%token PRE ARROW
36
%token EOF
37
%token REQUIRES ENSURES OBSERVER
38
%token INVARIANT BEHAVIOR ASSUMES
39
%token EXISTS FORALL
40

    
41
%nonassoc prec_exists prec_forall
42
%nonassoc COMMA POWER
43
%left MERGE IF
44
%nonassoc ELSE
45
%right ARROW FBY
46
%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
47
%right COLCOL
48
%right IMPL
49
%left OR XOR BARBAR
50
%left AND AMPERAMPER
51
%left NOT
52
%nonassoc EQ LT GT LTE GTE NEQ
53
%left MINUS PLUS
54
%left MULT DIV MOD
55
%left PRE 
56
%nonassoc UMINUS
57

    
58
%start lustre_annot
59
%type <LustreSpec.expr_annot> lustre_annot
60

    
61
%start lustre_spec
62
%type <LustreSpec.node_annot> lustre_spec
63

    
64
%%
65

    
66
lustre_spec:
67
| contract EOF { $1 }
68

    
69
contract:
70
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; } }
71
 
72
requires:
73
{ [] }
74
| REQUIRES expr SCOL requires { $2::$4 }
75

    
76
ensures:
77
{ [] }
78
| ENSURES expr SCOL ensures { (EnsuresExpr $2) :: $4 }
79
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
80

    
81
behaviors:
82
{ [] }
83
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5)::$6 }
84

    
85
assumes:
86
{ [] }
87
| ASSUMES expr SCOL assumes { $2::$4 } 
88

    
89
tuple_expr:
90
| expr COMMA expr {[$3;$1]}
91
| tuple_expr COMMA expr {$3::$1}
92

    
93
expr:
94
| const {mkeexpr (EExpr_const $1)} 
95
| IDENT 
96
    {mkeexpr (EExpr_ident $1)}
97
| LPAR expr RPAR
98
    {$2}
99
| LPAR tuple_expr RPAR
100
    {mkeexpr (EExpr_tuple (List.rev $2))}
101
| expr ARROW expr 
102
    {mkeexpr (EExpr_arrow ($1,$3))}
103
| expr FBY expr 
104
    {mkeexpr (EExpr_fby ($1,$3))}
105
| expr COLCOL expr 
106
    {mkeexpr (EExpr_concat ($1,$3))} 
107
| TAIL LPAR expr RPAR
108
    {mkeexpr (EExpr_tail $3)}
109
| expr WHEN IDENT 
110
    {mkeexpr (EExpr_when ($1,$3))}
111
| expr WHENNOT IDENT
112
    {mkeexpr (EExpr_whennot ($1,$3))}
113
| MERGE LPAR IDENT COMMA expr COMMA expr RPAR
114
    {mkeexpr (EExpr_merge ($3,$5,$7))}
115
| IDENT LPAR expr RPAR
116
    {mkeexpr (EExpr_appl ($1, $3, None))}
117
| IDENT LPAR expr RPAR EVERY IDENT
118
    {mkeexpr (EExpr_appl ($1, $3, Some $6))}
119
| IDENT LPAR tuple_expr RPAR
120
    {mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))}
121
| IDENT LPAR tuple_expr RPAR EVERY IDENT
122
    {mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) }
123

    
124
/* Boolean expr */
125
| expr AND expr 
126
    {mkepredef_call "&&" [$1;$3]}
127
| expr AMPERAMPER expr 
128
    {mkepredef_call "&&" [$1;$3]}
129
| expr OR expr 
130
    {mkepredef_call "||" [$1;$3]}
131
| expr BARBAR expr 
132
    {mkepredef_call "||" [$1;$3]}
133
| expr XOR expr 
134
    {mkepredef_call "xor" [$1;$3]}
135
| NOT expr 
136
    {mkepredef_unary_call "not" $2}
137
| expr IMPL expr 
138
    {mkepredef_call "impl" [$1;$3]}
139

    
140
/* Comparison expr */
141
| expr EQ expr 
142
    {mkepredef_call "=" [$1;$3]}
143
| expr LT expr 
144
    {mkepredef_call "<" [$1;$3]}
145
| expr LTE expr 
146
    {mkepredef_call "<=" [$1;$3]}
147
| expr GT expr 
148
    {mkepredef_call ">" [$1;$3]}
149
| expr GTE  expr 
150
    {mkepredef_call ">=" [$1;$3]}
151
| expr NEQ expr 
152
    {mkepredef_call "!=" [$1;$3]}
153

    
154
/* Arithmetic expr */
155
| expr PLUS expr 
156
    {mkepredef_call "+" [$1;$3]}
157
| expr MINUS expr 
158
    {mkepredef_call "-" [$1;$3]}
159
| expr MULT expr 
160
    {mkepredef_call "*" [$1;$3]}
161
| expr DIV expr 
162
    {mkepredef_call "/" [$1;$3]}
163
| MINUS expr %prec UMINUS
164
    {mkepredef_unary_call "uminus" $2}
165
| expr MOD expr 
166
    {mkepredef_call "mod" [$1;$3]}
167

    
168
/* Temp op */
169
| PRE expr 
170
    {mkeexpr (EExpr_pre $2)}
171

    
172
/* If */
173
| IF expr THEN expr ELSE expr
174
    {mkepredef_call "ite" [$2;$4;$6]}
175

    
176
/* Quantifiers */
177
| EXISTS vdecl SCOL expr %prec prec_exists {mkeexpr (EExpr_exists ($2, $4))} 
178
| FORALL vdecl SCOL expr %prec prec_forall {mkeexpr (EExpr_forall ($2, $4))}
179

    
180
vdecl:
181
| ident_list COL typ clock 
182
    {List.map mkvar_decl (List.map (fun id -> (id, $3, $4, false)) $1)}
183
| CONST ident_list COL typ clock 
184
    {List.map mkvar_decl (List.map (fun id -> (id, $4, $5, true)) $2)}
185

    
186

    
187
ident_list:
188
  IDENT {[$1]}
189
| ident_list COMMA IDENT {$3::$1}
190

    
191

    
192
typ:
193
    {mktyp Tydec_any}
194
| TINT {mktyp Tydec_int}
195
| IDENT {
196
  try 
197
    mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1))
198
  with Not_found -> raise (Corelang.Unbound_type ((Tydec_const $1),Location.symbol_rloc()))
199
}
200
| TFLOAT {mktyp Tydec_float}
201
| TREAL {mktyp Tydec_real}
202
| TBOOL {mktyp Tydec_bool}
203
| TCLOCK {mktyp (Tydec_clock Tydec_bool) }
204
| typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)}
205
| typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try 
206
					match get_const $3 with Const_int i -> i with _ -> failwith "Const power error") $1)*)}
207

    
208
clock:
209
    {mkclock Ckdec_any}
210
| when_list
211
    {mkclock (Ckdec_bool (List.rev $1))}
212

    
213
when_cond:
214
    WHEN IDENT {($2, tag_true)}
215
| WHENNOT IDENT {($2, tag_false)}
216

    
217
when_list:
218
    when_cond {[$1]}
219
| when_list when_cond {$2::$1}
220

    
221

    
222
const:
223
| INT {EConst_int $1}
224
| REAL {EConst_real $1}
225
| FLOAT {EConst_float $1}
226
| TRUE {EConst_bool true}
227
| FALSE {EConst_bool false}
228
| STRING {EConst_string $1}
229

    
230
lustre_annot:
231
lustre_annot_list EOF { $1 }
232

    
233
lustre_annot_list:
234
  { [] } 
235
| kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 }
236
| IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 }
237
| INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
238
| OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 }
239

    
240
kwd:
241
DIV { [] }
242
| DIV IDENT kwd { $2::$3}