Project

General

Profile

Download (6.8 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
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

    
12
open Utils
13

    
14
type label = ident
15

    
16
type type_dec = { ty_dec_desc : type_dec_desc; ty_dec_loc : Location.t }
17

    
18
and type_dec_desc =
19
  | Tydec_any
20
  | Tydec_int
21
  | Tydec_real
22
  (* | Tydec_float *)
23
  | Tydec_bool
24
  | Tydec_clock of type_dec_desc
25
  | Tydec_const of ident
26
  | Tydec_enum of ident list
27
  | Tydec_struct of (ident * type_dec_desc) list
28
  | Tydec_array of Dimension.t * type_dec_desc
29

    
30
type typedec_desc = { tydec_id : ident }
31

    
32
type typedef_desc = { tydef_id : ident; tydef_desc : type_dec_desc }
33

    
34
type clock_dec = { ck_dec_desc : clock_dec_desc; ck_dec_loc : Location.t }
35

    
36
and clock_dec_desc = Ckdec_any | Ckdec_bool of (ident * ident) list
37

    
38
type constant =
39
  | Const_int of int
40
  | Const_real of Real.t
41
  | Const_array of constant list
42
  | Const_tag of label
43
  | Const_string of string
44
  (* used only for annotations *)
45
  | Const_modeid of string
46
  (* used only for annotations *)
47
  | Const_struct of (label * constant) list
48

    
49
type quantifier_type = Exists | Forall
50

    
51
type var_decl = {
52
  var_id : ident;
53
  var_orig : bool;
54
  var_dec_type : type_dec;
55
  var_dec_clock : clock_dec;
56
  var_dec_const : bool;
57
  var_dec_value : expr option;
58
  mutable var_parent_nodeid : ident option;
59
  mutable var_type : Types.t;
60
  mutable var_clock : Clocks.t;
61
  var_loc : Location.t;
62
  var_is_contract: bool;
63
}
64
(* The tag of an expression is a unique identifier used to distinguish different
65
   instances of the same node *)
66

    
67
(** The core language and its ast. Every element of the ast contains its
68
    location in the program text. The type and clock of an ast element is
69
    mutable (and initialized to dummy values). This avoids to have to duplicate
70
    ast structures (e.g. ast, typed_ast, clocked_ast). *)
71

    
72
and expr = {
73
  expr_tag : tag;
74
  expr_desc : expr_desc;
75
  mutable expr_type : Types.t;
76
  mutable expr_clock : Clocks.t;
77
  mutable expr_delay : Delay.t;
78
  mutable expr_annot : expr_annot option;
79
  expr_loc : Location.t;
80
}
81

    
82
and expr_desc =
83
  | Expr_const of constant
84
  | Expr_ident of ident
85
  | Expr_tuple of expr list
86
  | Expr_ite of expr * expr * expr
87
  | Expr_arrow of expr * expr
88
  | Expr_fby of expr * expr
89
  | Expr_array of expr list
90
  | Expr_access of expr * Dimension.t
91
  | Expr_power of expr * Dimension.t
92
  | Expr_pre of expr
93
  | Expr_when of expr * ident * label
94
  | Expr_merge of ident * (label * expr) list
95
  | Expr_appl of call_t
96

    
97
and call_t = ident * expr * expr option
98
(* The third part denotes the boolean condition for resetting *)
99

    
100
and eq = { eq_lhs : ident list; eq_rhs : expr; eq_loc : Location.t }
101

    
102
(* The tag of an expression is a unique identifier used to distinguish different
103
   instances of the same node *)
104
and eexpr = {
105
  eexpr_tag : tag;
106
  eexpr_qfexpr : expr;
107
  eexpr_quantifiers : (quantifier_type * var_decl list) list;
108
  eexpr_name : string option;
109
  mutable eexpr_type : Types.t;
110
  mutable eexpr_clock : Clocks.t;
111
  (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
112
  eexpr_loc : Location.t;
113
}
114

    
115
and expr_annot = { annots : (string list * eexpr) list; annot_loc : Location.t }
116

    
117
type contract_mode = {
118
  mode_id : ident;
119
  require : eexpr list;
120
  ensure : eexpr list;
121
  mode_loc : Location.t;
122
}
123

    
124
type contract_import = {
125
  import_nodeid : ident;
126
  inputs : expr;
127
  outputs : expr;
128
  import_loc : Location.t;
129
}
130

    
131
type offset = Index of Dimension.t | Field of label
132

    
133
type assert_t = { assert_expr : expr; assert_loc : Location.t }
134

    
135
type statement = Eq of eq | Aut of automata_desc
136

    
137
and automata_desc = {
138
  aut_id : ident;
139
  aut_handlers : handler_desc list;
140
  aut_loc : Location.t;
141
}
142

    
143
and handler_desc = {
144
  hand_state : ident;
145
  hand_unless : (Location.t * expr * bool * ident) list;
146
  hand_until : (Location.t * expr * bool * ident) list;
147
  hand_locals : var_decl list;
148
  hand_stmts : statement list;
149
  hand_asserts : assert_t list;
150
  hand_annots : expr_annot list;
151
  hand_loc : Location.t;
152
}
153

    
154
type proof_annotation = Kinduction of int
155

    
156
type contract_desc = {
157
  consts : var_decl list;
158
  locals : var_decl list;
159
  stmts : statement list;
160
  assume : eexpr list;
161
  guarantees : eexpr list;
162
  modes : contract_mode list;
163
  imports : contract_import list;
164
  spec_loc : Location.t;
165
  proof : proof_annotation option
166
}
167

    
168
type 'a node_spec_t = Contract of 'a | NodeSpec of ident
169

    
170
type node_desc = {
171
  node_id : ident;
172
  mutable node_type : Types.t;
173
  mutable node_clock : Clocks.t;
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.t 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 : contract_desc 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.t;
191
  mutable nodei_clock : Clocks.t;
192
  nodei_inputs : var_decl list;
193
  nodei_outputs : var_decl list;
194
  nodei_stateless : bool;
195
  nodei_spec : contract_desc node_spec_t option;
196
  (* nodei_annot: expr_annot list; *)
197
  nodei_prototype : string option;
198
  nodei_in_lib : string list;
199
  nodei_iscontract : bool;
200
}
201

    
202
type const_desc = {
203
  const_id : ident;
204
  const_loc : Location.t;
205
  const_value : constant;
206
  mutable const_type : Types.t;
207
}
208

    
209
type top_decl_desc =
210
  | Node of node_desc
211
  | Const of const_desc
212
  | ImportedNode of imported_node_desc
213
  | Open of bool * string
214
  (* the boolean set to true denotes a local lusi vs a lusi installed at system
215
     level *)
216
  | Include of string
217
  (* the boolean set to true denotes a local lus vs a lus installed at system
218
     level *)
219
  | TypeDef of typedef_desc
220

    
221
type top_decl = {
222
  top_decl_desc : top_decl_desc;
223
  (* description of the symbol *)
224
  top_decl_owner : Location.filename;
225
  (* the module where it is defined *)
226
  top_decl_itf : bool;
227
  (* header or source file ? *)
228
  top_decl_loc : Location.t;
229
}
230
(* the location where it is defined *)
231

    
232
type program_t = top_decl list
233

    
234
type dep_t = {
235
  local : bool;
236
  name : ident;
237
  content : program_t;
238
  is_stateful : bool;
239
}
240

    
241
type spec_types =
242
  | LocalContract of contract_desc
243
  | TopContract of top_decl list
244

    
245
let tag_true = "true"
246

    
247
let tag_false = "false"
248

    
249
(* Local Variables: *)
250
(* compile-command:"make -C .." *)
251
(* End: *)
(43-43/99)