Revision 52cfee34 src/parser_lustre.mly
src/parser_lustre.mly | ||
---|---|---|
51 | 51 |
| ImportedNode _, _ -> |
52 | 52 |
Hashtbl.add hashtbl name value |
53 | 53 |
| Node _ , _ -> |
54 |
raise (Corelang.Error (Corelang.Already_bound_symbol msg, Location.symbol_rloc ()))
|
|
54 |
raise (Corelang.Error (Location.symbol_rloc (), Corelang.Already_bound_symbol msg))
|
|
55 | 55 |
| _ -> assert false |
56 | 56 |
with |
57 | 57 |
Not_found -> |
... | ... | |
59 | 59 |
|
60 | 60 |
let add_symbol msg hashtbl name value = |
61 | 61 |
if Hashtbl.mem hashtbl name |
62 |
then raise (Corelang.Error (Corelang.Already_bound_symbol msg, Location.symbol_rloc ()))
|
|
62 |
then raise (Corelang.Error (Location.symbol_rloc (), Corelang.Already_bound_symbol msg))
|
|
63 | 63 |
else Hashtbl.add hashtbl name value |
64 | 64 |
|
65 | 65 |
let check_symbol msg hashtbl name = |
66 | 66 |
if not (Hashtbl.mem hashtbl name) |
67 |
then raise (Corelang.Error (Corelang.Unbound_symbol msg, Location.symbol_rloc ()))
|
|
67 |
then raise (Corelang.Error (Location.symbol_rloc (), Corelang.Unbound_symbol msg))
|
|
68 | 68 |
else () |
69 | 69 |
|
70 | 70 |
%} |
... | ... | |
143 | 143 |
top_decl_header {(fun own -> [$1 own]) } |
144 | 144 |
| top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) } |
145 | 145 |
|
146 |
state_annot: |
|
147 |
FUNCTION { true } |
|
148 |
| NODE { false } |
|
146 | 149 |
|
147 | 150 |
top_decl_header: |
148 |
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL |
|
149 |
{let nd = mktop_decl (ImportedNode |
|
150 |
{nodei_id = $2; |
|
151 |
nodei_type = Types.new_var (); |
|
152 |
nodei_clock = Clocks.new_var true; |
|
153 |
nodei_inputs = List.rev $4; |
|
154 |
nodei_outputs = List.rev $9; |
|
155 |
nodei_stateless = $12; |
|
156 |
nodei_spec = None}) |
|
157 |
in |
|
158 |
(fun own -> add_node own ("node " ^ $2) node_table $2 nd; nd) } |
|
159 |
|
|
160 |
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL |
|
151 |
nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL |
|
161 | 152 |
{let nd = mktop_decl (ImportedNode |
162 | 153 |
{nodei_id = $3; |
163 | 154 |
nodei_type = Types.new_var (); |
164 | 155 |
nodei_clock = Clocks.new_var true; |
165 | 156 |
nodei_inputs = List.rev $5; |
166 | 157 |
nodei_outputs = List.rev $10; |
167 |
nodei_stateless = $13;
|
|
168 |
nodei_spec = Some $1})
|
|
158 |
nodei_stateless = $2;
|
|
159 |
nodei_spec = $1}) |
|
169 | 160 |
in |
170 | 161 |
(fun own -> add_node own ("node " ^ $3) node_table $3 nd; nd) } |
171 | 162 |
|
172 |
| FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL |
|
173 |
{let nd = mktop_decl (ImportedNode |
|
174 |
{nodei_id = $2; |
|
175 |
nodei_type = Types.new_var (); |
|
176 |
nodei_clock = Clocks.new_var true; |
|
177 |
nodei_inputs = List.rev $4; |
|
178 |
nodei_outputs = List.rev $9; |
|
179 |
nodei_stateless = true; |
|
180 |
nodei_spec = None}) |
|
181 |
in |
|
182 |
(fun own -> add_node own ("function " ^ $2) node_table $2 nd; nd) } |
|
183 |
|
|
184 |
| nodespec_list FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL |
|
185 |
{let nd = mktop_decl (ImportedNode |
|
186 |
{nodei_id = $3; |
|
187 |
nodei_type = Types.new_var (); |
|
188 |
nodei_clock = Clocks.new_var true; |
|
189 |
nodei_inputs = List.rev $5; |
|
190 |
nodei_outputs = List.rev $10; |
|
191 |
nodei_stateless = true; |
|
192 |
nodei_spec = Some $1}) |
|
193 |
in |
|
194 |
(fun own -> add_node own ("function " ^ $3) node_table $3 nd; nd) } |
|
195 |
|
|
196 | 163 |
top_decl: |
197 | 164 |
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) } |
198 |
|
|
199 |
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
200 |
{let eqs, asserts, annots = $15 in |
|
201 |
let nd = mktop_decl (Node |
|
202 |
{node_id = $2; |
|
203 |
node_type = Types.new_var (); |
|
204 |
node_clock = Clocks.new_var true; |
|
205 |
node_inputs = List.rev $4; |
|
206 |
node_outputs = List.rev $9; |
|
207 |
node_locals = List.rev $13; |
|
208 |
node_gencalls = []; |
|
209 |
node_checks = []; |
|
210 |
node_asserts = asserts; |
|
211 |
node_eqs = eqs; |
|
212 |
node_spec = None; |
|
213 |
node_annot = match annots with [] -> None | _ -> Some annots}) |
|
214 |
in |
|
215 |
add_node true ("node " ^ $2) node_table $2 nd; nd} |
|
216 |
|
|
217 |
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
165 |
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
218 | 166 |
{let eqs, asserts, annots = $16 in |
219 | 167 |
let nd = mktop_decl (Node |
220 | 168 |
{node_id = $3; |
... | ... | |
227 | 175 |
node_checks = []; |
228 | 176 |
node_asserts = asserts; |
229 | 177 |
node_eqs = eqs; |
230 |
node_spec = Some $1; |
|
178 |
node_dec_stateless = $2; |
|
179 |
node_stateless = None; |
|
180 |
node_spec = $1; |
|
231 | 181 |
node_annot = match annots with [] -> None | _ -> Some annots}) |
232 | 182 |
in |
233 | 183 |
add_node true ("node " ^ $3) node_table $3 nd; nd} |
234 | 184 |
|
235 | 185 |
nodespec_list: |
236 |
NODESPEC { $1 } |
|
237 |
| NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 } |
|
238 |
|
|
239 |
stateless_opt: |
|
240 |
{ false } |
|
241 |
| STATELESS {true} |
|
186 |
{ None } |
|
187 |
| NODESPEC nodespec_list { (function None -> (fun s1 -> Some s1) | Some s2 -> (fun s1 -> Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 } |
|
242 | 188 |
|
243 | 189 |
typ_def_list: |
244 | 190 |
/* empty */ {} |
Also available in: Unified diff