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