Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / lib / lustre_types.ml @ 9b0432bc

History | View | Annotate | Download (7.54 KB)

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

    
13
type ident = Utils.ident
14
[@@deriving show]
15
type rat = Utils.rat
16
[@@deriving show]
17
type tag = Utils.tag
18
[@@deriving show]
19
type label = Utils.ident
20
[@@deriving show]
21

    
22
type type_dec =
23
    {ty_dec_desc: type_dec_desc;
24
     ty_dec_loc: Location.t}
25

    
26
and type_dec_desc =
27
  | Tydec_any
28
  | Tydec_int
29
  | Tydec_real
30
  (* | Tydec_float *)
31
  | Tydec_bool
32
  | Tydec_clock of type_dec_desc
33
  | Tydec_const of ident
34
  | Tydec_enum of ident list
35
  | Tydec_struct of (ident * type_dec_desc) list
36
  | Tydec_array of Dimension.dim_expr * type_dec_desc
37
[@@deriving show]
38

    
39
type typedec_desc =
40
    {tydec_id: ident}
41
 [@@deriving show]
42

    
43
type typedef_desc =
44
    {tydef_id: ident;
45
     tydef_desc: type_dec_desc}
46
 [@@deriving show]
47

    
48
type clock_dec =
49
    {ck_dec_desc: clock_dec_desc;
50
     ck_dec_loc: Location.t}
51

    
52
and clock_dec_desc =
53
  | Ckdec_any
54
  | Ckdec_bool of (ident * ident) list
55
 [@@deriving show]
56

    
57
type constant =
58
  | Const_int of int
59
  | Const_real of Real.t
60
  | Const_array of constant list
61
  | Const_tag of label
62
  | Const_string of string (* used only for annotations *)
63
  | Const_modeid of string (* used only for annotations *)
64
  | Const_struct of (label * constant) list
65
 [@@deriving show]
66

    
67
type quantifier_type = Exists | Forall
68
[@@deriving show]
69

    
70
type var_decl =
71
    {var_id: ident;
72
     var_orig:bool;
73
     var_dec_type: type_dec;
74
     var_dec_clock: clock_dec;
75
     var_dec_const: bool;
76
     var_dec_value: expr option;
77
     mutable var_parent_nodeid: ident option;
78
     mutable var_type: Types.type_expr;
79
     mutable var_clock: Clocks.clock_expr;
80
     var_loc: Location.t}
81

    
82
(** The core language and its ast. Every element of the ast contains its
83
    location in the program text. The type and clock of an ast element
84
    is mutable (and initialized to dummy values). This avoids to have to
85
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
86

    
87

    
88

    
89
(* The tag of an expression is a unique identifier used to distinguish
90
   different instances of the same node *)
91
and expr =
92
    {expr_tag: tag;
93
     expr_desc: expr_desc;
94
     mutable expr_type: Types.type_expr;
95
     mutable expr_clock: Clocks.clock_expr;
96
     mutable expr_delay: Delay.delay_expr;
97
     mutable expr_annot: expr_annot option;
98
     expr_loc: Location.t}
99

    
100
and expr_desc =
101
  | Expr_const of constant
102
  | Expr_ident of ident
103
  | Expr_tuple of expr list
104
  | Expr_ite   of expr * expr * expr
105
  | Expr_arrow of expr * expr
106
  | Expr_fby of expr * expr
107
  | Expr_array of expr list
108
  | Expr_access of expr * Dimension.dim_expr
109
  | Expr_power of expr * Dimension.dim_expr
110
  | Expr_pre of expr
111
  | Expr_when of expr * ident * label
112
  | Expr_merge of ident * (label * expr) list
113
  | Expr_appl of call_t
114

    
115
and call_t = ident * expr * expr option
116
     (* The third part denotes the boolean condition for resetting *)
117

    
118
and eq =
119
    {eq_lhs: ident list;
120
     eq_rhs: expr;
121
     eq_loc: Location.t}
122

    
123
  (* The tag of an expression is a unique identifier used to distinguish
124
     different instances of the same node *)
125
and  eexpr =
126
    {eexpr_tag: tag;
127
     eexpr_qfexpr: expr;
128
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
129
     eexpr_name: string option;
130
     mutable eexpr_type: Types.type_expr;
131
     mutable eexpr_clock: Clocks.clock_expr;
132
     (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
133
     eexpr_loc: Location.t}
134

    
135
and expr_annot =
136
 {annots: (string list * eexpr) list;
137
  annot_loc: Location.t}
138
[@@deriving show]
139

    
140
type contract_mode =
141
  {
142
    mode_id: ident;
143
    require: eexpr list;
144
    ensure: eexpr list;
145
    mode_loc: Location.t
146
  }
147
 [@@deriving show]
148

    
149
type contract_import =
150
  { import_nodeid: ident;
151
    inputs: expr;
152
    outputs: expr;
153
    import_loc: Location.t }
154
  [@@deriving show]  
155

    
156

    
157
type offset =
158
| Index of Dimension.dim_expr
159
| Field of label
160
 [@@deriving show]
161

    
162
type assert_t =
163
    {
164
      assert_expr: expr;
165
      assert_loc: Location.t;
166
    }
167
[@@deriving show]
168

    
169
type statement =
170
| Eq of eq
171
| Aut of automata_desc
172

    
173
and automata_desc =
174
  {aut_id : ident;
175
   aut_handlers: handler_desc list;
176
   aut_loc: Location.t}
177

    
178
and handler_desc =
179
  {hand_state: ident;
180
   hand_unless: (Location.t * expr * bool * ident) list;
181
   hand_until: (Location.t * expr * bool * ident) list;
182
   hand_locals: var_decl list;
183
   hand_stmts: statement list;
184
   hand_asserts: assert_t list;
185
   hand_annots: expr_annot list;
186
   hand_loc: Location.t}
187
[@@deriving show]
188

    
189
type contract_desc = 
190
  {
191
    consts: var_decl list;
192
    locals: var_decl list;
193
    stmts: statement list;
194
    assume: eexpr list;
195
    guarantees: eexpr list;
196
    modes: contract_mode list;
197
    imports: contract_import list; 
198
    spec_loc: Location.t;
199
  }
200
[@@deriving show]
201

    
202
type node_spec_t = Contract of contract_desc
203
                 | NodeSpec of ident
204
[@@deriving show]
205

    
206
type node_desc =
207
    {node_id: ident;
208
     mutable node_type: Types.type_expr;
209
     mutable node_clock: Clocks.clock_expr;
210
     node_inputs: var_decl list;
211
     node_outputs: var_decl list;
212
     node_locals: var_decl list;
213
     mutable node_gencalls: expr list;
214
     mutable node_checks: Dimension.dim_expr list;
215
     node_asserts: assert_t list;
216
     node_stmts: statement list;
217
     mutable node_dec_stateless: bool;
218
     mutable node_stateless: bool option;
219
     node_spec: node_spec_t option;
220
     node_annot: expr_annot list;
221
     node_iscontract: bool;
222
    }
223
[@@deriving show]
224

    
225
type imported_node_desc =
226
    {nodei_id: ident;
227
     mutable nodei_type: Types.type_expr;
228
     mutable nodei_clock: Clocks.clock_expr;
229
     nodei_inputs: var_decl list;
230
     nodei_outputs: var_decl list;
231
     nodei_stateless: bool;
232
     nodei_spec: node_spec_t option;
233
     (* nodei_annot: expr_annot list; *)
234
     nodei_prototype: string option;
235
     nodei_in_lib: string list;
236
    }
237
[@@deriving show]
238

    
239
type const_desc =
240
    {const_id: ident;
241
     const_loc: Location.t;
242
     const_value: constant;
243
     mutable const_type: Types.type_expr;
244
    }
245
[@@deriving show]
246

    
247
  
248
type top_decl_desc =
249
  | Node of node_desc
250
  | Const of const_desc
251
  | ImportedNode of imported_node_desc
252
  | Open of bool * string (* the boolean set to true denotes a local
253
			   lusi vs a lusi installed at system level *)
254
  | Include of string (* the boolean set to true denotes a local
255
			   lus vs a lus installed at system level *)
256
  | TypeDef of typedef_desc
257
[@@deriving show]   
258

    
259
type top_decl =
260
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
261
     top_decl_owner: Location.filename; (* the module where it is defined *)
262
     top_decl_itf: bool;                (* header or source file ? *)
263
     top_decl_loc: Location.t}          (* the location where it is defined *)
264
[@@deriving show]
265

    
266
type program_t = top_decl list
267
[@@deriving show]
268

    
269
type dep_t = {
270
    local: bool;
271
    name: ident;
272
    content: program_t;
273
    is_stateful: bool
274
  }
275
[@@deriving show]
276

    
277
type spec_types =
278
  | LocalContract of contract_desc
279
  | TopContract of top_decl list
280
[@@deriving show]
281

    
282
let tag_true = "true"
283
let tag_false = "false"
284

    
285

    
286
(* Local Variables: *)
287
(* compile-command:"make -C .." *)
288
(* End: *)