Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustre_types.ml @ 5fccce23

History | View | Annotate | Download (6.75 KB)

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 66359a5e ploc
  
12 22fe1c93 ploc
type ident = Utils.ident
13
type rat = Utils.rat
14
type tag = Utils.tag
15 af5af1e8 ploc
type label = Utils.ident
16 22fe1c93 ploc
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 04a63d25 xthirioux
  (* | Tydec_float *)
26 22fe1c93 ploc
  | Tydec_bool
27
  | Tydec_clock of type_dec_desc
28
  | Tydec_const of ident
29
  | Tydec_enum of ident list
30 6a6abd76 xthirioux
  | Tydec_struct of (ident * type_dec_desc) list
31 22fe1c93 ploc
  | Tydec_array of Dimension.dim_expr * type_dec_desc
32
33 ef34b4ae xthirioux
type typedec_desc =
34
    {tydec_id: ident}
35
36
type typedef_desc =
37
    {tydef_id: ident;
38
     tydef_desc: type_dec_desc}
39 b1655a21 xthirioux
40 22fe1c93 ploc
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 04396cc7 Christophe Garion
  | Ckdec_bool of (ident * ident) list
47 45f0f48d xthirioux
48 22fe1c93 ploc
49 ec433d69 xthirioux
type constant =
50
  | Const_int of int
51 04a63d25 xthirioux
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
52 ec433d69 xthirioux
  | Const_array of constant list
53
  | Const_tag of label
54
  | Const_string of string (* used only for annotations *)
55 778c80fd ploc
  | Const_modeid of string (* used only for annotations *)
56 ec433d69 xthirioux
  | Const_struct of (label * constant) list
57
58
type quantifier_type = Exists | Forall
59
60 04396cc7 Christophe Garion
type var_decl =
61 22fe1c93 ploc
    {var_id: ident;
62 54d032f5 xthirioux
     var_orig:bool;
63 22fe1c93 ploc
     var_dec_type: type_dec;
64
     var_dec_clock: clock_dec;
65
     var_dec_const: bool;
66 ec433d69 xthirioux
     var_dec_value: expr option;
67 66359a5e ploc
     mutable var_parent_nodeid: ident option;
68 22fe1c93 ploc
     mutable var_type: Types.type_expr;
69
     mutable var_clock: Clocks.clock_expr;
70
     var_loc: Location.t}
71
72 01c7d5e1 ploc
(** 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 22fe1c93 ploc
(* The tag of an expression is a unique identifier used to distinguish
80
   different instances of the same node *)
81 ec433d69 xthirioux
and expr =
82 01c7d5e1 ploc
    {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 ef34b4ae xthirioux
105 04396cc7 Christophe Garion
and call_t = ident * expr * expr option
106 54d032f5 xthirioux
     (* The third part denotes the boolean condition for resetting *)
107 ef34b4ae xthirioux
108
and eq =
109
    {eq_lhs: ident list;
110
     eq_rhs: expr;
111
     eq_loc: Location.t}
112
113 01c7d5e1 ploc
  (* The tag of an expression is a unique identifier used to distinguish
114
     different instances of the same node *)
115 ef34b4ae xthirioux
and  eexpr =
116 22fe1c93 ploc
    {eexpr_tag: tag;
117 01c7d5e1 ploc
     eexpr_qfexpr: expr;
118
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
119 22fe1c93 ploc
     mutable eexpr_type: Types.type_expr;
120
     mutable eexpr_clock: Clocks.clock_expr;
121 01c7d5e1 ploc
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
122 22fe1c93 ploc
     eexpr_loc: Location.t}
123
124 ef34b4ae xthirioux
and expr_annot =
125
 {annots: (string list * eexpr) list;
126
  annot_loc: Location.t}
127 22fe1c93 ploc
128 778c80fd ploc
type contract_mode =
129
  { mode_id: ident; require: eexpr list; ensure: eexpr list; mode_loc: Location.t}
130
131
type contract_import =
132
  { import_nodeid: ident; inputs: expr list; outputs: expr list; import_loc: Location.t }
133
    
134 2d179f5b xthirioux
135 0d54d8a8 ploc
136 2d179f5b xthirioux
type offset =
137
| Index of Dimension.dim_expr
138
| Field of label
139
140 04396cc7 Christophe Garion
type assert_t =
141 01c7d5e1 ploc
    {
142
      assert_expr: expr;
143 af5af1e8 ploc
      assert_loc: Location.t;
144 b08ffca7 xthirioux
    }
145
146
type statement =
147
| Eq of eq
148
| Aut of automata_desc
149 01c7d5e1 ploc
150 b08ffca7 xthirioux
and automata_desc =
151 ef34b4ae xthirioux
  {aut_id : ident;
152
   aut_handlers: handler_desc list;
153
   aut_loc: Location.t}
154
155
and handler_desc =
156
  {hand_state: ident;
157 2822cf55 xthirioux
   hand_unless: (Location.t * expr * bool * ident) list;
158
   hand_until: (Location.t * expr * bool * ident) list;
159 ef34b4ae xthirioux
   hand_locals: var_decl list;
160 b08ffca7 xthirioux
   hand_stmts: statement list;
161 2822cf55 xthirioux
   hand_asserts: assert_t list;
162
   hand_annots: expr_annot list;
163 ef34b4ae xthirioux
   hand_loc: Location.t}
164
165 f9f06e7d ploc
type contract_desc = 
166
  {
167
    consts: var_decl list;
168
    locals: var_decl list;
169
    stmts: statement list;
170
    assume: eexpr list;
171
    guarantees: eexpr list;
172
    modes: contract_mode list;
173
    imports: contract_import list; 
174
    spec_loc: Location.t;
175
  }
176
177 01c7d5e1 ploc
type node_desc =
178
    {node_id: ident;
179
     mutable node_type: Types.type_expr;
180
     mutable node_clock: Clocks.clock_expr;
181
     node_inputs: var_decl list;
182
     node_outputs: var_decl list;
183
     node_locals: var_decl list;
184
     mutable node_gencalls: expr list;
185
     mutable node_checks: Dimension.dim_expr list;
186 04396cc7 Christophe Garion
     node_asserts: assert_t list;
187 b08ffca7 xthirioux
     node_stmts: statement list;
188 01c7d5e1 ploc
     mutable node_dec_stateless: bool;
189
     mutable node_stateless: bool option;
190 4f26dcf5 ploc
     node_spec: contract_desc option;
191 01c7d5e1 ploc
     node_annot: expr_annot list;
192
    }
193
194
type imported_node_desc =
195
    {nodei_id: ident;
196
     mutable nodei_type: Types.type_expr;
197
     mutable nodei_clock: Clocks.clock_expr;
198
     nodei_inputs: var_decl list;
199
     nodei_outputs: var_decl list;
200
     nodei_stateless: bool;
201 4f26dcf5 ploc
     nodei_spec: contract_desc option;
202 66359a5e ploc
     (* nodei_annot: expr_annot list; *)
203 01c7d5e1 ploc
     nodei_prototype: string option;
204 04a63d25 xthirioux
     nodei_in_lib: string list;
205 01c7d5e1 ploc
    }
206
207 04396cc7 Christophe Garion
type const_desc =
208
    {const_id: ident;
209
     const_loc: Location.t;
210
     const_value: constant;
211 01c7d5e1 ploc
     mutable const_type: Types.type_expr;
212
    }
213
214 0d54d8a8 ploc
  
215 01c7d5e1 ploc
type top_decl_desc =
216
| Node of node_desc
217 ef34b4ae xthirioux
| Const of const_desc
218 01c7d5e1 ploc
| ImportedNode of imported_node_desc
219 04396cc7 Christophe Garion
| Open of bool * string (* the boolean set to true denotes a local
220 01c7d5e1 ploc
			   lusi vs a lusi installed at system level *)
221 ef34b4ae xthirioux
| TypeDef of typedef_desc
222 4f26dcf5 ploc
    
223 01c7d5e1 ploc
type top_decl =
224 ef34b4ae xthirioux
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
225
     top_decl_owner: Location.filename; (* the module where it is defined *)
226
     top_decl_itf: bool;                (* header or source file ? *)
227
     top_decl_loc: Location.t}          (* the location where it is defined *)
228 01c7d5e1 ploc
229 ad4774b0 ploc
type program_t = top_decl list
230 01c7d5e1 ploc
231 5fccce23 ploc
type dep_t = {
232
    local: bool;
233
    name: ident;
234
    content: program_t;
235
    is_stateful: bool
236
  }
237 04a63d25 xthirioux
238
239
240 22fe1c93 ploc
(* Local Variables: *)
241
(* compile-command:"make -C .." *)
242
(* End: *)