1 |
a2d97a3e
|
ploc
|
(********************************************************************)
|
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 |
66359a5e
|
ploc
|
|
12 |
22fe1c93
|
ploc
|
type ident = Utils.ident
|
13 |
|
|
type rat = Utils.rat
|
14 |
|
|
type tag = Utils.tag
|
15 |
af5af1e8
|
ploc
|
type label = Utils.ident
|
16 |
22fe1c93
|
ploc
|
|
17 |
|
|
type type_dec =
|
18 |
|
|
{ty_dec_desc: type_dec_desc;
|
19 |
|
|
ty_dec_loc: Location.t}
|
20 |
|
|
|
21 |
|
|
and type_dec_desc =
|
22 |
|
|
| Tydec_any
|
23 |
|
|
| Tydec_int
|
24 |
|
|
| Tydec_real
|
25 |
04a63d25
|
xthirioux
|
(* | Tydec_float *)
|
26 |
22fe1c93
|
ploc
|
| Tydec_bool
|
27 |
|
|
| Tydec_clock of type_dec_desc
|
28 |
|
|
| Tydec_const of ident
|
29 |
|
|
| Tydec_enum of ident list
|
30 |
6a6abd76
|
xthirioux
|
| Tydec_struct of (ident * type_dec_desc) list
|
31 |
22fe1c93
|
ploc
|
| Tydec_array of Dimension.dim_expr * type_dec_desc
|
32 |
|
|
|
33 |
ef34b4ae
|
xthirioux
|
type typedec_desc =
|
34 |
|
|
{tydec_id: ident}
|
35 |
|
|
|
36 |
|
|
type typedef_desc =
|
37 |
|
|
{tydef_id: ident;
|
38 |
|
|
tydef_desc: type_dec_desc}
|
39 |
b1655a21
|
xthirioux
|
|
40 |
22fe1c93
|
ploc
|
type clock_dec =
|
41 |
|
|
{ck_dec_desc: clock_dec_desc;
|
42 |
|
|
ck_dec_loc: Location.t}
|
43 |
|
|
|
44 |
|
|
and clock_dec_desc =
|
45 |
|
|
| Ckdec_any
|
46 |
04396cc7
|
Christophe Garion
|
| Ckdec_bool of (ident * ident) list
|
47 |
45f0f48d
|
xthirioux
|
|
48 |
22fe1c93
|
ploc
|
|
49 |
ec433d69
|
xthirioux
|
type constant =
|
50 |
|
|
| Const_int of int
|
51 |
04a63d25
|
xthirioux
|
| Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
|
52 |
ec433d69
|
xthirioux
|
| Const_array of constant list
|
53 |
|
|
| Const_tag of label
|
54 |
|
|
| Const_string of string (* used only for annotations *)
|
55 |
|
|
| Const_struct of (label * constant) list
|
56 |
|
|
|
57 |
|
|
type quantifier_type = Exists | Forall
|
58 |
|
|
|
59 |
04396cc7
|
Christophe Garion
|
type var_decl =
|
60 |
22fe1c93
|
ploc
|
{var_id: ident;
|
61 |
54d032f5
|
xthirioux
|
var_orig:bool;
|
62 |
22fe1c93
|
ploc
|
var_dec_type: type_dec;
|
63 |
|
|
var_dec_clock: clock_dec;
|
64 |
|
|
var_dec_const: bool;
|
65 |
ec433d69
|
xthirioux
|
var_dec_value: expr option;
|
66 |
66359a5e
|
ploc
|
mutable var_parent_nodeid: ident option;
|
67 |
22fe1c93
|
ploc
|
mutable var_type: Types.type_expr;
|
68 |
|
|
mutable var_clock: Clocks.clock_expr;
|
69 |
|
|
var_loc: Location.t}
|
70 |
|
|
|
71 |
01c7d5e1
|
ploc
|
(** The core language and its ast. Every element of the ast contains its
|
72 |
|
|
location in the program text. The type and clock of an ast element
|
73 |
|
|
is mutable (and initialized to dummy values). This avoids to have to
|
74 |
|
|
duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
|
75 |
|
|
|
76 |
|
|
|
77 |
|
|
|
78 |
22fe1c93
|
ploc
|
(* The tag of an expression is a unique identifier used to distinguish
|
79 |
|
|
different instances of the same node *)
|
80 |
ec433d69
|
xthirioux
|
and expr =
|
81 |
01c7d5e1
|
ploc
|
{expr_tag: tag;
|
82 |
|
|
expr_desc: expr_desc;
|
83 |
|
|
mutable expr_type: Types.type_expr;
|
84 |
|
|
mutable expr_clock: Clocks.clock_expr;
|
85 |
|
|
mutable expr_delay: Delay.delay_expr;
|
86 |
|
|
mutable expr_annot: expr_annot option;
|
87 |
|
|
expr_loc: Location.t}
|
88 |
|
|
|
89 |
|
|
and expr_desc =
|
90 |
|
|
| Expr_const of constant
|
91 |
|
|
| Expr_ident of ident
|
92 |
|
|
| Expr_tuple of expr list
|
93 |
|
|
| Expr_ite of expr * expr * expr
|
94 |
|
|
| Expr_arrow of expr * expr
|
95 |
|
|
| Expr_fby of expr * expr
|
96 |
|
|
| Expr_array of expr list
|
97 |
|
|
| Expr_access of expr * Dimension.dim_expr
|
98 |
|
|
| Expr_power of expr * Dimension.dim_expr
|
99 |
|
|
| Expr_pre of expr
|
100 |
|
|
| Expr_when of expr * ident * label
|
101 |
|
|
| Expr_merge of ident * (label * expr) list
|
102 |
|
|
| Expr_appl of call_t
|
103 |
ef34b4ae
|
xthirioux
|
|
104 |
04396cc7
|
Christophe Garion
|
and call_t = ident * expr * expr option
|
105 |
54d032f5
|
xthirioux
|
(* The third part denotes the boolean condition for resetting *)
|
106 |
ef34b4ae
|
xthirioux
|
|
107 |
|
|
and eq =
|
108 |
|
|
{eq_lhs: ident list;
|
109 |
|
|
eq_rhs: expr;
|
110 |
|
|
eq_loc: Location.t}
|
111 |
|
|
|
112 |
01c7d5e1
|
ploc
|
(* The tag of an expression is a unique identifier used to distinguish
|
113 |
|
|
different instances of the same node *)
|
114 |
ef34b4ae
|
xthirioux
|
and eexpr =
|
115 |
22fe1c93
|
ploc
|
{eexpr_tag: tag;
|
116 |
01c7d5e1
|
ploc
|
eexpr_qfexpr: expr;
|
117 |
|
|
eexpr_quantifiers: (quantifier_type * var_decl list) list;
|
118 |
22fe1c93
|
ploc
|
mutable eexpr_type: Types.type_expr;
|
119 |
|
|
mutable eexpr_clock: Clocks.clock_expr;
|
120 |
01c7d5e1
|
ploc
|
mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
|
121 |
22fe1c93
|
ploc
|
eexpr_loc: Location.t}
|
122 |
|
|
|
123 |
ef34b4ae
|
xthirioux
|
and expr_annot =
|
124 |
|
|
{annots: (string list * eexpr) list;
|
125 |
|
|
annot_loc: Location.t}
|
126 |
22fe1c93
|
ploc
|
|
127 |
|
|
type node_annot = {
|
128 |
|
|
requires: eexpr list;
|
129 |
01c7d5e1
|
ploc
|
ensures: eexpr list;
|
130 |
|
|
behaviors: (string * eexpr list * eexpr list * Location.t) list;
|
131 |
|
|
spec_loc: Location.t;
|
132 |
22fe1c93
|
ploc
|
}
|
133 |
2d179f5b
|
xthirioux
|
|
134 |
|
|
type offset =
|
135 |
|
|
| Index of Dimension.dim_expr
|
136 |
|
|
| Field of label
|
137 |
|
|
|
138 |
04396cc7
|
Christophe Garion
|
type assert_t =
|
139 |
01c7d5e1
|
ploc
|
{
|
140 |
|
|
assert_expr: expr;
|
141 |
af5af1e8
|
ploc
|
assert_loc: Location.t;
|
142 |
b08ffca7
|
xthirioux
|
}
|
143 |
|
|
|
144 |
|
|
type statement =
|
145 |
|
|
| Eq of eq
|
146 |
|
|
| Aut of automata_desc
|
147 |
01c7d5e1
|
ploc
|
|
148 |
b08ffca7
|
xthirioux
|
and automata_desc =
|
149 |
ef34b4ae
|
xthirioux
|
{aut_id : ident;
|
150 |
|
|
aut_handlers: handler_desc list;
|
151 |
|
|
aut_loc: Location.t}
|
152 |
|
|
|
153 |
|
|
and handler_desc =
|
154 |
|
|
{hand_state: ident;
|
155 |
2822cf55
|
xthirioux
|
hand_unless: (Location.t * expr * bool * ident) list;
|
156 |
|
|
hand_until: (Location.t * expr * bool * ident) list;
|
157 |
ef34b4ae
|
xthirioux
|
hand_locals: var_decl list;
|
158 |
b08ffca7
|
xthirioux
|
hand_stmts: statement list;
|
159 |
2822cf55
|
xthirioux
|
hand_asserts: assert_t list;
|
160 |
|
|
hand_annots: expr_annot list;
|
161 |
ef34b4ae
|
xthirioux
|
hand_loc: Location.t}
|
162 |
|
|
|
163 |
01c7d5e1
|
ploc
|
type node_desc =
|
164 |
|
|
{node_id: ident;
|
165 |
|
|
mutable node_type: Types.type_expr;
|
166 |
|
|
mutable node_clock: Clocks.clock_expr;
|
167 |
|
|
node_inputs: var_decl list;
|
168 |
|
|
node_outputs: var_decl list;
|
169 |
|
|
node_locals: var_decl list;
|
170 |
|
|
mutable node_gencalls: expr list;
|
171 |
|
|
mutable node_checks: Dimension.dim_expr list;
|
172 |
04396cc7
|
Christophe Garion
|
node_asserts: assert_t list;
|
173 |
b08ffca7
|
xthirioux
|
node_stmts: statement list;
|
174 |
01c7d5e1
|
ploc
|
mutable node_dec_stateless: bool;
|
175 |
|
|
mutable node_stateless: bool option;
|
176 |
|
|
node_spec: node_annot option;
|
177 |
|
|
node_annot: expr_annot list;
|
178 |
|
|
}
|
179 |
|
|
|
180 |
|
|
type imported_node_desc =
|
181 |
|
|
{nodei_id: ident;
|
182 |
|
|
mutable nodei_type: Types.type_expr;
|
183 |
|
|
mutable nodei_clock: Clocks.clock_expr;
|
184 |
|
|
nodei_inputs: var_decl list;
|
185 |
|
|
nodei_outputs: var_decl list;
|
186 |
|
|
nodei_stateless: bool;
|
187 |
|
|
nodei_spec: node_annot option;
|
188 |
66359a5e
|
ploc
|
(* nodei_annot: expr_annot list; *)
|
189 |
01c7d5e1
|
ploc
|
nodei_prototype: string option;
|
190 |
04a63d25
|
xthirioux
|
nodei_in_lib: string list;
|
191 |
01c7d5e1
|
ploc
|
}
|
192 |
|
|
|
193 |
04396cc7
|
Christophe Garion
|
type const_desc =
|
194 |
|
|
{const_id: ident;
|
195 |
|
|
const_loc: Location.t;
|
196 |
|
|
const_value: constant;
|
197 |
01c7d5e1
|
ploc
|
mutable const_type: Types.type_expr;
|
198 |
|
|
}
|
199 |
|
|
|
200 |
|
|
type top_decl_desc =
|
201 |
|
|
| Node of node_desc
|
202 |
ef34b4ae
|
xthirioux
|
| Const of const_desc
|
203 |
01c7d5e1
|
ploc
|
| ImportedNode of imported_node_desc
|
204 |
04396cc7
|
Christophe Garion
|
| Open of bool * string (* the boolean set to true denotes a local
|
205 |
01c7d5e1
|
ploc
|
lusi vs a lusi installed at system level *)
|
206 |
ef34b4ae
|
xthirioux
|
| TypeDef of typedef_desc
|
207 |
01c7d5e1
|
ploc
|
|
208 |
|
|
type top_decl =
|
209 |
ef34b4ae
|
xthirioux
|
{top_decl_desc: top_decl_desc; (* description of the symbol *)
|
210 |
|
|
top_decl_owner: Location.filename; (* the module where it is defined *)
|
211 |
|
|
top_decl_itf: bool; (* header or source file ? *)
|
212 |
|
|
top_decl_loc: Location.t} (* the location where it is defined *)
|
213 |
01c7d5e1
|
ploc
|
|
214 |
|
|
type program = top_decl list
|
215 |
|
|
|
216 |
04396cc7
|
Christophe Garion
|
type dep_t = Dep of
|
217 |
|
|
bool
|
218 |
58a463e7
|
ploc
|
* ident
|
219 |
04396cc7
|
Christophe Garion
|
* (top_decl list)
|
220 |
58a463e7
|
ploc
|
* bool (* is stateful *)
|
221 |
|
|
|
222 |
04a63d25
|
xthirioux
|
|
223 |
|
|
|
224 |
|
|
|
225 |
22fe1c93
|
ploc
|
(* Local Variables: *)
|
226 |
|
|
(* compile-command:"make -C .." *)
|
227 |
|
|
(* End: *)
|