1
|
open Format
|
2
|
|
3
|
open Machine_code_types
|
4
|
open Lustre_types
|
5
|
open Corelang
|
6
|
open Machine_code_common
|
7
|
|
8
|
open Ada_printer
|
9
|
open Misc_printer
|
10
|
open Misc_lustre_function
|
11
|
|
12
|
(** Exception for unsupported features in Ada backend **)
|
13
|
exception Ada_not_supported of string
|
14
|
|
15
|
(** Print the name of the state variable.
|
16
|
@param fmt the formater to print on
|
17
|
**)
|
18
|
let pp_state_name fmt = fprintf fmt "state"
|
19
|
(** Print the type of the state variable.
|
20
|
@param fmt the formater to print on
|
21
|
**)
|
22
|
let pp_state_type fmt = fprintf fmt "TState"
|
23
|
(** Print the name of the reset procedure
|
24
|
@param fmt the formater to print on
|
25
|
**)
|
26
|
let pp_reset_procedure_name fmt = fprintf fmt "reset"
|
27
|
(** Print the name of the step procedure
|
28
|
@param fmt the formater to print on
|
29
|
**)
|
30
|
let pp_step_procedure_name fmt = fprintf fmt "step"
|
31
|
(** Print the name of the main procedure.
|
32
|
@param fmt the formater to print on
|
33
|
**)
|
34
|
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
|
35
|
(** Print the name of the arrow package.
|
36
|
@param fmt the formater to print on
|
37
|
**)
|
38
|
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
|
39
|
(** Print the type of a polymorphic type.
|
40
|
@param fmt the formater to print on
|
41
|
@param id the id of the polymorphic type
|
42
|
**)
|
43
|
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
|
44
|
|
45
|
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
|
46
|
|
47
|
|
48
|
|
49
|
|
50
|
|
51
|
|
52
|
|
53
|
|
54
|
|
55
|
(*TODO Check all this function with unit test, improve this system and
|
56
|
add support for : "cbrt", "erf", "log10", "pow", "atan2".
|
57
|
*)
|
58
|
let ada_supported_funs =
|
59
|
[("sqrt", ("Ada.Numerics.Elementary_Functions", "Sqrt"));
|
60
|
("log", ("Ada.Numerics.Elementary_Functions", "Log"));
|
61
|
("exp", ("Ada.Numerics.Elementary_Functions", "Exp"));
|
62
|
("pow", ("Ada.Numerics.Elementary_Functions", "**"));
|
63
|
("sin", ("Ada.Numerics.Elementary_Functions", "Sin"));
|
64
|
("cos", ("Ada.Numerics.Elementary_Functions", "Cos"));
|
65
|
("tan", ("Ada.Numerics.Elementary_Functions", "Tan"));
|
66
|
("asin", ("Ada.Numerics.Elementary_Functions", "Arcsin"));
|
67
|
("acos", ("Ada.Numerics.Elementary_Functions", "Arccos"));
|
68
|
("atan", ("Ada.Numerics.Elementary_Functions", "Arctan"));
|
69
|
("sinh", ("Ada.Numerics.Elementary_Functions", "Sinh"));
|
70
|
("cosh", ("Ada.Numerics.Elementary_Functions", "Cosh"));
|
71
|
("tanh", ("Ada.Numerics.Elementary_Functions", "Tanh"));
|
72
|
("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
|
73
|
("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
|
74
|
("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
|
75
|
|
76
|
("ceil", ("", "Float'Ceiling"));
|
77
|
("floor", ("", "Float'Floor"));
|
78
|
("fmod", ("", "Float'Remainder"));
|
79
|
("round", ("", "Float'Rounding"));
|
80
|
("trunc", ("", "Float'Truncation"));
|
81
|
|
82
|
("fabs", ("", "abs"));]
|
83
|
|
84
|
let is_builtin_fun ident =
|
85
|
List.mem ident Basic_library.internal_funs ||
|
86
|
List.mem_assoc ident ada_supported_funs
|
87
|
|
88
|
(** Print the name of a package associated to a machine.
|
89
|
@param fmt the formater to print on
|
90
|
@param machine the machine
|
91
|
**)
|
92
|
let pp_package_name machine fmt =
|
93
|
if is_arrow machine then
|
94
|
fprintf fmt "%t" pp_arrow_package_name
|
95
|
else
|
96
|
fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
|
97
|
|
98
|
(** Print a type.
|
99
|
@param fmt the formater to print on
|
100
|
@param type the type
|
101
|
**)
|
102
|
let pp_type fmt typ =
|
103
|
(match (Types.repr typ).Types.tdesc with
|
104
|
| Types.Tbasic Types.Basic.Tint -> pp_integer_type fmt
|
105
|
| Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
|
106
|
| Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
|
107
|
| Types.Tunivar -> pp_polymorphic_type typ.Types.tid fmt
|
108
|
| Types.Tbasic _ -> eprintf "Tbasic@."; assert false (*TODO*)
|
109
|
| Types.Tconst _ -> eprintf "Tconst@."; assert false (*TODO*)
|
110
|
| Types.Tclock _ -> eprintf "Tclock@."; assert false (*TODO*)
|
111
|
| Types.Tarrow _ -> eprintf "Tarrow@."; assert false (*TODO*)
|
112
|
| Types.Ttuple l -> eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; assert false (*TODO*)
|
113
|
| Types.Tenum _ -> eprintf "Tenum@."; assert false (*TODO*)
|
114
|
| Types.Tstruct _ -> eprintf "Tstruct@.";assert false (*TODO*)
|
115
|
| Types.Tarray _ -> eprintf "Tarray@."; assert false (*TODO*)
|
116
|
| Types.Tstatic _ -> eprintf "Tstatic@.";assert false (*TODO*)
|
117
|
| Types.Tlink _ -> eprintf "Tlink@."; assert false (*TODO*)
|
118
|
| Types.Tvar -> eprintf "Tvar@."; assert false (*TODO*)
|
119
|
(*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
|
120
|
)
|
121
|
|
122
|
(** Return a default ada constant for a given type.
|
123
|
@param cst_typ the constant type
|
124
|
**)
|
125
|
let default_ada_cst cst_typ = match cst_typ with
|
126
|
| Types.Basic.Tint -> Const_int 0
|
127
|
| Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0")
|
128
|
| Types.Basic.Tbool -> Const_tag tag_false
|
129
|
| _ -> assert false
|
130
|
|
131
|
(** Make a default value from a given type.
|
132
|
@param typ the type
|
133
|
**)
|
134
|
let mk_default_value typ =
|
135
|
match (Types.repr typ).Types.tdesc with
|
136
|
| Types.Tbasic t -> mk_val (Cst (default_ada_cst t)) typ
|
137
|
| _ -> assert false (*TODO*)
|
138
|
|
139
|
(** Print the type of a variable.
|
140
|
@param fmt the formater to print on
|
141
|
@param id the variable
|
142
|
**)
|
143
|
let pp_var_type fmt id =
|
144
|
pp_type fmt id.var_type
|
145
|
|
146
|
(** Print a package name with polymorphic types specified.
|
147
|
@param substitution correspondance between polymorphic type id and their instantiation
|
148
|
@param fmt the formater to print on
|
149
|
@param machine the machine
|
150
|
**)
|
151
|
let pp_package_name_with_polymorphic substitution machine fmt =
|
152
|
let polymorphic_types = find_all_polymorphic_type machine in
|
153
|
assert(List.length polymorphic_types = List.length substitution);
|
154
|
let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
|
155
|
assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
|
156
|
polymorphic_types substituion);
|
157
|
let instantiated_types = snd (List.split substitution) in
|
158
|
fprintf fmt "%t%t%a"
|
159
|
(pp_package_name machine)
|
160
|
(Utils.pp_final_char_if_non_empty "_" instantiated_types)
|
161
|
(Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
|
162
|
|
163
|
(** Print the name of a variable.
|
164
|
@param fmt the formater to print on
|
165
|
@param id the variable
|
166
|
**)
|
167
|
let pp_var_name id fmt =
|
168
|
fprintf fmt "%a" pp_clean_ada_identifier id.var_id
|
169
|
|
170
|
(** Print the complete name of variable.
|
171
|
@param m the machine to check if it is memory
|
172
|
@param fmt the formater to print on
|
173
|
@param var the variable
|
174
|
**)
|
175
|
let pp_var env fmt var =
|
176
|
match List.assoc_opt var.var_id env with
|
177
|
| None -> pp_var_name var fmt
|
178
|
| Some pp_state -> pp_access pp_state (pp_var_name var) fmt
|
179
|
|
180
|
(* Expression print functions *)
|
181
|
|
182
|
(* Printing functions for basic operations and expressions *)
|
183
|
(* TODO: refactor code -> use let rec and for basic pretty printing
|
184
|
function *)
|
185
|
(** Printing function for Ada tags, mainly booleans.
|
186
|
|
187
|
@param fmt the formater to use
|
188
|
@param t the tag to print
|
189
|
**)
|
190
|
let pp_ada_tag fmt t =
|
191
|
pp_print_string fmt
|
192
|
(if t = tag_true then "True" else if t = tag_false then "False" else t)
|
193
|
|
194
|
(** Printing function for machine type constants. For the moment,
|
195
|
arrays are not supported.
|
196
|
|
197
|
@param fmt the formater to use
|
198
|
@param c the constant to print
|
199
|
**)
|
200
|
let pp_ada_const fmt c =
|
201
|
match c with
|
202
|
| Const_int i -> pp_print_int fmt i
|
203
|
| Const_real (c, e, s) ->
|
204
|
fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
|
205
|
| Const_tag t -> pp_ada_tag fmt t
|
206
|
| Const_string _ | Const_modeid _ ->
|
207
|
(Format.eprintf
|
208
|
"internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
|
209
|
assert false)
|
210
|
| _ ->
|
211
|
raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
|
212
|
support this constant")
|
213
|
|
214
|
(** Printing function for expressions [v1 modulo v2]. Depends
|
215
|
on option [integer_div_euclidean] to choose between mathematical
|
216
|
modulo or remainder ([rem] in Ada).
|
217
|
|
218
|
@param pp_value pretty printer for values
|
219
|
@param v1 the first value in the expression
|
220
|
@param v2 the second value in the expression
|
221
|
@param fmt the formater to print on
|
222
|
**)
|
223
|
let pp_mod pp_value v1 v2 fmt =
|
224
|
if !Options.integer_div_euclidean then
|
225
|
(* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
|
226
|
Format.fprintf fmt
|
227
|
"((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
|
228
|
pp_value v1 pp_value v2
|
229
|
pp_value v1 pp_value v2
|
230
|
pp_value v2
|
231
|
else (* Ada behavior for rem *)
|
232
|
Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
|
233
|
|
234
|
(** Printing function for expressions [v1 div v2]. Depends on
|
235
|
option [integer_div_euclidean] to choose between mathematic
|
236
|
division or Ada division.
|
237
|
|
238
|
@param pp_value pretty printer for values
|
239
|
@param v1 the first value in the expression
|
240
|
@param v2 the second value in the expression
|
241
|
@param fmt the formater to print in
|
242
|
**)
|
243
|
let pp_div pp_value v1 v2 fmt =
|
244
|
if !Options.integer_div_euclidean then
|
245
|
(* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
|
246
|
Format.fprintf fmt "(%a - %t) / %a"
|
247
|
pp_value v1
|
248
|
(pp_mod pp_value v1 v2)
|
249
|
pp_value v2
|
250
|
else (* Ada behavior for / *)
|
251
|
Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
|
252
|
|
253
|
(** Printing function for basic lib functions.
|
254
|
|
255
|
@param pp_value pretty printer for values
|
256
|
@param i a string representing the function
|
257
|
@param fmt the formater to print on
|
258
|
@param vl the list of operands
|
259
|
**)
|
260
|
let pp_basic_lib_fun pp_value ident fmt vl =
|
261
|
match ident, vl with
|
262
|
| "uminus", [v] ->
|
263
|
Format.fprintf fmt "(- %a)" pp_value v
|
264
|
| "not", [v] ->
|
265
|
Format.fprintf fmt "(not %a)" pp_value v
|
266
|
| "impl", [v1; v2] ->
|
267
|
Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
|
268
|
| "=", [v1; v2] ->
|
269
|
Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
|
270
|
| "mod", [v1; v2] -> pp_mod pp_value v1 v2 fmt
|
271
|
| "equi", [v1; v2] ->
|
272
|
Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
|
273
|
| "xor", [v1; v2] ->
|
274
|
Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
|
275
|
| "/", [v1; v2] -> pp_div pp_value v1 v2 fmt
|
276
|
| "&&", [v1; v2] ->
|
277
|
Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
|
278
|
| "||", [v1; v2] ->
|
279
|
Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
|
280
|
| "!=", [v1; v2] ->
|
281
|
Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
|
282
|
| "ite", [v1; v2; v3] ->
|
283
|
Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3
|
284
|
| op, [v1; v2] ->
|
285
|
Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
|
286
|
| op, [v1] when List.mem_assoc ident ada_supported_funs ->
|
287
|
let pkg, name = try List.assoc ident ada_supported_funs
|
288
|
with Not_found -> assert false in
|
289
|
let pkg = pkg^(if String.equal pkg "" then "" else ".") in
|
290
|
Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1
|
291
|
| fun_name, _ ->
|
292
|
(Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
|
293
|
|
294
|
(** Printing function for values.
|
295
|
|
296
|
@param m the machine to know the state variable
|
297
|
@param fmt the formater to use
|
298
|
@param value the value to print. Should be a
|
299
|
{!type:Machine_code_types.value_t} value
|
300
|
**)
|
301
|
let rec pp_value env fmt value =
|
302
|
match value.value_desc with
|
303
|
| Cst c -> pp_ada_const fmt c
|
304
|
| Var var -> pp_var env fmt var (* Find better to test if it is memory or not *)
|
305
|
| Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl
|
306
|
| _ ->
|
307
|
raise (Ada_not_supported
|
308
|
"unsupported: Ada_backend.adb.pp_value does not support this value type")
|
309
|
|
310
|
|
311
|
(** Print the filename of a machine package.
|
312
|
@param extension the extension to append to the package name
|
313
|
@param fmt the formatter
|
314
|
@param machine the machine corresponding to the package
|
315
|
**)
|
316
|
let pp_machine_filename extension fmt machine =
|
317
|
pp_filename extension fmt (pp_package_name machine)
|
318
|
|
319
|
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
|
320
|
|
321
|
|
322
|
(** Print the declaration of a state element of a subinstance of a machine.
|
323
|
@param machine the machine
|
324
|
@param fmt the formater to print on
|
325
|
@param substitution correspondance between polymorphic type id and their instantiation
|
326
|
@param ident the identifier of the subinstance
|
327
|
@param submachine the submachine of the subinstance
|
328
|
**)
|
329
|
let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) =
|
330
|
let pp_package = pp_package_name_with_polymorphic substitution machine in
|
331
|
let pp_type = pp_package_access (pp_package, pp_state_type) in
|
332
|
let pp_name fmt = pp_clean_ada_identifier fmt name in
|
333
|
(mode, pp_name, pp_type, with_statement)
|
334
|
|
335
|
(** Print variable declaration for a local state variable
|
336
|
@param fmt the formater to print on
|
337
|
@param mode input/output mode of the parameter
|
338
|
**)
|
339
|
let build_pp_state_decl mode with_statement =
|
340
|
(mode, pp_state_name, pp_state_type, with_statement)
|
341
|
|
342
|
let build_pp_var_decl mode with_statement var =
|
343
|
let pp_name = function fmt -> pp_var_name var fmt in
|
344
|
let pp_type = function fmt -> pp_var_type fmt var in
|
345
|
(mode, pp_name, pp_type, with_statement)
|
346
|
|
347
|
let build_pp_var_decl_local with_statement var =
|
348
|
AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
|
349
|
|
350
|
let build_pp_var_decl_step_input mode with_statement m =
|
351
|
if m.mstep.step_inputs=[] then [] else
|
352
|
[List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]
|
353
|
|
354
|
let build_pp_var_decl_step_output mode with_statement m =
|
355
|
if m.mstep.step_outputs=[] then [] else
|
356
|
[List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]
|
357
|
|
358
|
let build_pp_var_decl_static mode with_statement m =
|
359
|
if m.mstatic=[] then [] else
|
360
|
[List.map (build_pp_var_decl mode with_statement) m.mstatic]
|
361
|
|
362
|
let build_pp_arg_step m =
|
363
|
(if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
|
364
|
@ (build_pp_var_decl_step_input AdaIn None m)
|
365
|
@ (build_pp_var_decl_step_output AdaOut None m)
|
366
|
|
367
|
let build_pp_arg_reset m =
|
368
|
(if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])
|
369
|
@ (build_pp_var_decl_static AdaIn None m)
|
370
|
|
371
|
|
372
|
let build_pp_arg_transition m =
|
373
|
(if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
|
374
|
@ (build_pp_var_decl_step_input AdaIn None m)
|
375
|
@ (build_pp_var_decl_step_output AdaOut None m)
|
376
|
|