Project

General

Profile

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