lustrec / src / lustre_types.ml @ 8446bf03
History  View  Annotate  Download (6.35 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 node_annot = { 
128 
requires: eexpr list; 
129 
ensures: eexpr list; 
130 
behaviors: (string * eexpr list * eexpr list * Location.t) list; 
131 
spec_loc: Location.t; 
132 
} 
133  
134 
type offset = 
135 
 Index of Dimension.dim_expr 
136 
 Field of label 
137  
138 
type assert_t = 
139 
{ 
140 
assert_expr: expr; 
141 
assert_loc: Location.t; 
142 
} 
143  
144 
type statement = 
145 
 Eq of eq 
146 
 Aut of automata_desc 
147  
148 
and automata_desc = 
149 
{aut_id : ident; 
150 
aut_handlers: handler_desc list; 
151 
aut_loc: Location.t} 
152  
153 
and handler_desc = 
154 
{hand_state: ident; 
155 
hand_unless: (Location.t * expr * bool * ident) list; 
156 
hand_until: (Location.t * expr * bool * ident) list; 
157 
hand_locals: var_decl list; 
158 
hand_stmts: statement list; 
159 
hand_asserts: assert_t list; 
160 
hand_annots: expr_annot list; 
161 
hand_loc: Location.t} 
162  
163 
type node_desc = 
164 
{node_id: ident; 
165 
mutable node_type: Types.type_expr; 
166 
mutable node_clock: Clocks.clock_expr; 
167 
node_inputs: var_decl list; 
168 
node_outputs: var_decl list; 
169 
node_locals: var_decl list; 
170 
mutable node_gencalls: expr list; 
171 
mutable node_checks: Dimension.dim_expr list; 
172 
node_asserts: assert_t list; 
173 
node_stmts: statement list; 
174 
mutable node_dec_stateless: bool; 
175 
mutable node_stateless: bool option; 
176 
node_spec: node_annot option; 
177 
node_annot: expr_annot list; 
178 
} 
179  
180 
type imported_node_desc = 
181 
{nodei_id: ident; 
182 
mutable nodei_type: Types.type_expr; 
183 
mutable nodei_clock: Clocks.clock_expr; 
184 
nodei_inputs: var_decl list; 
185 
nodei_outputs: var_decl list; 
186 
nodei_stateless: bool; 
187 
nodei_spec: node_annot option; 
188 
(* nodei_annot: expr_annot list; *) 
189 
nodei_prototype: string option; 
190 
nodei_in_lib: string list; 
191 
} 
192  
193 
type const_desc = 
194 
{const_id: ident; 
195 
const_loc: Location.t; 
196 
const_value: constant; 
197 
mutable const_type: Types.type_expr; 
198 
} 
199  
200 
type top_decl_desc = 
201 
 Node of node_desc 
202 
 Const of const_desc 
203 
 ImportedNode of imported_node_desc 
204 
 Open of bool * string (* the boolean set to true denotes a local 
205 
lusi vs a lusi installed at system level *) 
206 
 TypeDef of typedef_desc 
207  
208 
type top_decl = 
209 
{top_decl_desc: top_decl_desc; (* description of the symbol *) 
210 
top_decl_owner: Location.filename; (* the module where it is defined *) 
211 
top_decl_itf: bool; (* header or source file ? *) 
212 
top_decl_loc: Location.t} (* the location where it is defined *) 
213  
214 
type program = top_decl list 
215  
216 
type dep_t = Dep of 
217 
bool 
218 
* ident 
219 
* (top_decl list) 
220 
* bool (* is stateful *) 
221  
222  
223  
224  
225 
(* Local Variables: *) 
226 
(* compilecommand:"make C .." *) 
227 
(* End: *) 