Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustre_types.ml @ 4f26dcf5

History | View | Annotate | Download (6.52 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_struct of (label * constant) list
56

    
57
type quantifier_type = Exists | Forall
58

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

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

    
76

    
77

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

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

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

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

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

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

    
127
type contract_desc = {
128
(* TODO: 
129
   local variables 
130
   rename: assume/guarantee
131
           in behavior mode (id, requires/ensures)
132
   import contract
133
*)
134
  
135
  requires: eexpr list;
136
  ensures: eexpr list;
137
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
138
  spec_loc: Location.t;
139
}
140

    
141
type offset =
142
| Index of Dimension.dim_expr
143
| Field of label
144

    
145
type assert_t =
146
    {
147
      assert_expr: expr;
148
      assert_loc: Location.t;
149
    }
150

    
151
type statement =
152
| Eq of eq
153
| Aut of automata_desc
154

    
155
and automata_desc =
156
  {aut_id : ident;
157
   aut_handlers: handler_desc list;
158
   aut_loc: Location.t}
159

    
160
and handler_desc =
161
  {hand_state: ident;
162
   hand_unless: (Location.t * expr * bool * ident) list;
163
   hand_until: (Location.t * expr * bool * ident) list;
164
   hand_locals: var_decl list;
165
   hand_stmts: statement list;
166
   hand_asserts: assert_t list;
167
   hand_annots: expr_annot list;
168
   hand_loc: Location.t}
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: contract_desc option;
184
     node_annot: expr_annot list;
185
    }
186

    
187
type imported_node_desc =
188
    {nodei_id: ident;
189
     mutable nodei_type: Types.type_expr;
190
     mutable nodei_clock: Clocks.clock_expr;
191
     nodei_inputs: var_decl list;
192
     nodei_outputs: var_decl list;
193
     nodei_stateless: bool;
194
     nodei_spec: contract_desc option;
195
     (* nodei_annot: expr_annot list; *)
196
     nodei_prototype: string option;
197
     nodei_in_lib: string list;
198
    }
199

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

    
207
type top_decl_desc =
208
| Node of node_desc
209
| Const of const_desc
210
| ImportedNode of imported_node_desc
211
| Open of bool * string (* the boolean set to true denotes a local
212
			   lusi vs a lusi installed at system level *)
213
| TypeDef of typedef_desc
214
| Contract of contract_desc
215
    
216
type top_decl =
217
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
218
     top_decl_owner: Location.filename; (* the module where it is defined *)
219
     top_decl_itf: bool;                (* header or source file ? *)
220
     top_decl_loc: Location.t}          (* the location where it is defined *)
221

    
222
type program = top_decl list
223

    
224
type dep_t = Dep of
225
    bool
226
  * ident
227
  * (top_decl list)
228
  * bool (* is stateful *)
229

    
230

    
231

    
232

    
233
(* Local Variables: *)
234
(* compile-command:"make -C .." *)
235
(* End: *)