Project

General

Profile

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