Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustre_types.ml @ df94cd73

History | View | Annotate | Download (7.11 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
type ident = Utils.ident
13
type rat = Utils.rat
14
type tag = Utils.tag
15
type label = Utils.ident
16

    
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
  (* | Tydec_float *)
26
  | Tydec_bool
27
  | Tydec_clock of type_dec_desc
28
  | Tydec_const of ident
29
  | Tydec_enum of ident list
30
  | Tydec_struct of (ident * type_dec_desc) list
31
  | Tydec_array of Dimension.dim_expr * type_dec_desc
32

    
33
type typedec_desc =
34
    {tydec_id: ident}
35

    
36
type typedef_desc =
37
    {tydef_id: ident;
38
     tydef_desc: type_dec_desc}
39

    
40
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
  | Ckdec_bool of (ident * ident) list
47

    
48

    
49
type constant =
50
  | Const_int of int
51
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
52
  | Const_array of constant list
53
  | Const_tag of label
54
  | Const_string of string (* used only for annotations *)
55
  | Const_modeid of string (* used only for annotations *)
56
  | Const_struct of (label * constant) list
57

    
58
type quantifier_type = Exists | Forall
59

    
60
type var_decl =
61
    {var_id: ident;
62
     var_orig:bool;
63
     var_dec_type: type_dec;
64
     var_dec_clock: clock_dec;
65
     var_dec_const: bool;
66
     var_dec_value: expr option;
67
     mutable var_parent_nodeid: ident option;
68
     mutable var_type: Types.type_expr;
69
     mutable var_clock: Clocks.clock_expr;
70
     var_loc: Location.t}
71

    
72
(** The core language and its ast. Every element of the ast contains its
73
    location in the program text. The type and clock of an ast element
74
    is mutable (and initialized to dummy values). This avoids to have to
75
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
76

    
77

    
78

    
79
(* The tag of an expression is a unique identifier used to distinguish
80
   different instances of the same node *)
81
and expr =
82
    {expr_tag: tag;
83
     expr_desc: expr_desc;
84
     mutable expr_type: Types.type_expr;
85
     mutable expr_clock: Clocks.clock_expr;
86
     mutable expr_delay: Delay.delay_expr;
87
     mutable expr_annot: expr_annot option;
88
     expr_loc: Location.t}
89

    
90
and expr_desc =
91
  | Expr_const of constant
92
  | Expr_ident of ident
93
  | Expr_tuple of expr list
94
  | Expr_ite   of expr * expr * expr
95
  | Expr_arrow of expr * expr
96
  | Expr_fby of expr * expr
97
  | Expr_array of expr list
98
  | Expr_access of expr * Dimension.dim_expr
99
  | Expr_power of expr * Dimension.dim_expr
100
  | Expr_pre of expr
101
  | Expr_when of expr * ident * label
102
  | Expr_merge of ident * (label * expr) list
103
  | Expr_appl of call_t
104

    
105
and call_t = ident * expr * expr option
106
     (* The third part denotes the boolean condition for resetting *)
107

    
108
and eq =
109
    {eq_lhs: ident list;
110
     eq_rhs: expr;
111
     eq_loc: Location.t}
112

    
113
  (* The tag of an expression is a unique identifier used to distinguish
114
     different instances of the same node *)
115
and  eexpr =
116
    {eexpr_tag: tag;
117
     eexpr_qfexpr: expr;
118
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
119
     eexpr_name: string option;
120
     mutable eexpr_type: Types.type_expr;
121
     mutable eexpr_clock: Clocks.clock_expr;
122
     (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
123
     eexpr_loc: Location.t}
124

    
125
and expr_annot =
126
 {annots: (string list * eexpr) list;
127
  annot_loc: Location.t}
128

    
129
type contract_mode =
130
  {
131
    mode_id: ident;
132
    require: eexpr list;
133
    ensure: eexpr list;
134
    mode_loc: Location.t
135
  }
136

    
137
type contract_import =
138
  { import_nodeid: ident;
139
    inputs: expr;
140
    outputs: expr;
141
    import_loc: Location.t }
142
    
143

    
144

    
145
type offset =
146
| Index of Dimension.dim_expr
147
| Field of label
148

    
149
type assert_t =
150
    {
151
      assert_expr: expr;
152
      assert_loc: Location.t;
153
    }
154

    
155
type statement =
156
| Eq of eq
157
| Aut of automata_desc
158

    
159
and automata_desc =
160
  {aut_id : ident;
161
   aut_handlers: handler_desc list;
162
   aut_loc: Location.t}
163

    
164
and handler_desc =
165
  {hand_state: ident;
166
   hand_unless: (Location.t * expr * bool * ident) list;
167
   hand_until: (Location.t * expr * bool * ident) list;
168
   hand_locals: var_decl list;
169
   hand_stmts: statement list;
170
   hand_asserts: assert_t list;
171
   hand_annots: expr_annot list;
172
   hand_loc: Location.t}
173

    
174
type contract_desc = 
175
  {
176
    consts: var_decl list;
177
    locals: var_decl list;
178
    stmts: statement list;
179
    assume: eexpr list;
180
    guarantees: eexpr list;
181
    modes: contract_mode list;
182
    imports: contract_import list; 
183
    spec_loc: Location.t;
184
  }
185

    
186
type node_spec_t = Contract of contract_desc
187
                 | NodeSpec of ident
188

    
189
type node_desc =
190
    {node_id: ident;
191
     mutable node_type: Types.type_expr;
192
     mutable node_clock: Clocks.clock_expr;
193
     node_inputs: var_decl list;
194
     node_outputs: var_decl list;
195
     node_locals: var_decl list;
196
     mutable node_gencalls: expr list;
197
     mutable node_checks: Dimension.dim_expr list;
198
     node_asserts: assert_t list;
199
     node_stmts: statement list;
200
     mutable node_dec_stateless: bool;
201
     mutable node_stateless: bool option;
202
     node_spec: node_spec_t option;
203
     node_annot: expr_annot list;
204
     node_iscontract: bool;
205
    }
206

    
207
type imported_node_desc =
208
    {nodei_id: ident;
209
     mutable nodei_type: Types.type_expr;
210
     mutable nodei_clock: Clocks.clock_expr;
211
     nodei_inputs: var_decl list;
212
     nodei_outputs: var_decl list;
213
     nodei_stateless: bool;
214
     nodei_spec: node_spec_t option;
215
     (* nodei_annot: expr_annot list; *)
216
     nodei_prototype: string option;
217
     nodei_in_lib: string list;
218
    }
219

    
220
type const_desc =
221
    {const_id: ident;
222
     const_loc: Location.t;
223
     const_value: constant;
224
     mutable const_type: Types.type_expr;
225
    }
226

    
227
  
228
type top_decl_desc =
229
  | Node of node_desc
230
  | Const of const_desc
231
  | ImportedNode of imported_node_desc
232
  | Open of bool * string (* the boolean set to true denotes a local
233
			   lusi vs a lusi installed at system level *)
234
  | Include of string (* the boolean set to true denotes a local
235
			   lus vs a lus installed at system level *)
236
  | TypeDef of typedef_desc
237
    
238
type top_decl =
239
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
240
     top_decl_owner: Location.filename; (* the module where it is defined *)
241
     top_decl_itf: bool;                (* header or source file ? *)
242
     top_decl_loc: Location.t}          (* the location where it is defined *)
243

    
244
type program_t = top_decl list
245

    
246
type dep_t = {
247
    local: bool;
248
    name: ident;
249
    content: program_t;
250
    is_stateful: bool
251
  }
252

    
253
type spec_types =
254
  | LocalContract of contract_desc
255
  | TopContract of top_decl list
256

    
257

    
258

    
259
(* Local Variables: *)
260
(* compile-command:"make -C .." *)
261
(* End: *)