1
|
open Format
|
2
|
|
3
|
open Machine_code_types
|
4
|
open Lustre_types
|
5
|
open Corelang
|
6
|
open Machine_code_common
|
7
|
|
8
|
(** All the pretty print functions common to the ada backend **)
|
9
|
|
10
|
|
11
|
(* Misc pretty print functions *)
|
12
|
|
13
|
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
|
14
|
underscore and must not contain a double underscore
|
15
|
@param var name to be cleaned*)
|
16
|
let pp_clean_ada_identifier fmt name =
|
17
|
let base_size = String.length name in
|
18
|
assert(base_size > 0);
|
19
|
let rec remove_double_underscore s = function
|
20
|
| i when i == String.length s - 1 -> s
|
21
|
| i when String.get s i == '_' && String.get s (i+1) == '_' ->
|
22
|
remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
|
23
|
| i -> remove_double_underscore s (i+1)
|
24
|
in
|
25
|
let name = remove_double_underscore name 0 in
|
26
|
let prefix = if String.length name != base_size
|
27
|
|| String.get name 0 == '_' then
|
28
|
"ada"
|
29
|
else
|
30
|
""
|
31
|
in
|
32
|
fprintf fmt "%s%s" prefix name
|
33
|
|
34
|
(** Encapsulate a pretty print function to lower case its result when applied
|
35
|
@param pp the pretty print function
|
36
|
@param fmt the formatter
|
37
|
@param arg the argument of the pp function
|
38
|
**)
|
39
|
let pp_lowercase pp fmt =
|
40
|
let str = asprintf "%t" pp in
|
41
|
fprintf fmt "%s" (String. lowercase_ascii str)
|
42
|
|
43
|
(** Print a filename by lowercasing the base and appending an extension.
|
44
|
@param extension the extension to append to the package name
|
45
|
@param fmt the formatter
|
46
|
@param pp_name the file base name printer
|
47
|
**)
|
48
|
let pp_filename extension fmt pp_name =
|
49
|
fprintf fmt "%t.%s"
|
50
|
(pp_lowercase pp_name)
|
51
|
extension
|
52
|
|
53
|
|
54
|
(* Package pretty print functions *)
|
55
|
|
56
|
(** Print the name of the arrow package.
|
57
|
@param fmt the formater to print on
|
58
|
**)
|
59
|
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
|
60
|
|
61
|
(** Print the name of a package associated to a node.
|
62
|
@param fmt the formater to print on
|
63
|
@param machine the machine
|
64
|
**)
|
65
|
let pp_package_name fmt machine =
|
66
|
if String.equal Arrow.arrow_id machine.mname.node_id then
|
67
|
fprintf fmt "%t" pp_arrow_package_name
|
68
|
else
|
69
|
fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
|
70
|
|
71
|
(** Print the ada package introduction sentence it can be used for body and
|
72
|
declaration. Boolean parameter body should be true if it is a body delcaration.
|
73
|
@param fmt the formater to print on
|
74
|
@param fmt the formater to print on
|
75
|
@param machine the machine
|
76
|
**)
|
77
|
let pp_begin_package body fmt machine =
|
78
|
fprintf fmt "package %s%a is"
|
79
|
(if body then "body " else "")
|
80
|
pp_package_name machine
|
81
|
|
82
|
(** Print the ada package conclusion sentence.
|
83
|
@param fmt the formater to print on
|
84
|
@param machine the machine
|
85
|
**)
|
86
|
let pp_end_package fmt machine =
|
87
|
fprintf fmt "end %a" pp_package_name machine
|
88
|
|
89
|
(** Print the access of an item from an other package.
|
90
|
@param fmt the formater to print on
|
91
|
@param package the package to use
|
92
|
@param item the item which is accessed
|
93
|
**)
|
94
|
let pp_package_access fmt (package, item) =
|
95
|
fprintf fmt "%t.%t" package item
|
96
|
|
97
|
(** Print the name of the main procedure.
|
98
|
@param fmt the formater to print on
|
99
|
**)
|
100
|
let pp_main_procedure_name fmt =
|
101
|
fprintf fmt "main"
|
102
|
|
103
|
(** Extract a node from an instance.
|
104
|
@param instance the instance
|
105
|
**)
|
106
|
let extract_node instance =
|
107
|
let (_, (node, _)) = instance in
|
108
|
match node.top_decl_desc with
|
109
|
| Node nd -> nd
|
110
|
| _ -> assert false (*TODO*)
|
111
|
|
112
|
(** Print a with statement to include a machine.
|
113
|
@param fmt the formater to print on
|
114
|
@param machine the machine
|
115
|
**)
|
116
|
let pp_with_machine fmt machine =
|
117
|
fprintf fmt "private with %a" pp_package_name machine
|
118
|
|
119
|
|
120
|
(* Type pretty print functions *)
|
121
|
|
122
|
(** Print a type declaration
|
123
|
@param fmt the formater to print on
|
124
|
@param pp_name a format printer which print the type name
|
125
|
@param pp_value a format printer which print the type definition
|
126
|
**)
|
127
|
let pp_type_decl fmt (pp_name, pp_definition) =
|
128
|
fprintf fmt "type %t is %t" pp_name pp_definition
|
129
|
|
130
|
(** Print a limited private type declaration
|
131
|
@param fmt the formater to print on
|
132
|
@param pp_name a format printer which print the type name
|
133
|
**)
|
134
|
let pp_private_limited_type_decl fmt pp_name =
|
135
|
let pp_definition fmt = fprintf fmt "limited private" in
|
136
|
pp_type_decl fmt (pp_name, pp_definition)
|
137
|
|
138
|
(** Print the type of the state variable.
|
139
|
@param fmt the formater to print on
|
140
|
**)
|
141
|
let pp_state_type fmt =
|
142
|
(* Type and variable names live in the same environement in Ada so name of
|
143
|
this type and of the associated parameter : pp_state_name must be
|
144
|
different *)
|
145
|
fprintf fmt "TState"
|
146
|
|
147
|
(** Print the integer type name.
|
148
|
@param fmt the formater to print on
|
149
|
**)
|
150
|
let pp_integer_type fmt = fprintf fmt "Integer"
|
151
|
|
152
|
(** Print the float type name.
|
153
|
@param fmt the formater to print on
|
154
|
**)
|
155
|
let pp_float_type fmt = fprintf fmt "Float"
|
156
|
|
157
|
(** Print the boolean type name.
|
158
|
@param fmt the formater to print on
|
159
|
**)
|
160
|
let pp_boolean_type fmt = fprintf fmt "Boolean"
|
161
|
|
162
|
(** Print the type of a polymorphic type.
|
163
|
@param fmt the formater to print on
|
164
|
@param id the id of the polymorphic type
|
165
|
**)
|
166
|
let pp_polymorphic_type fmt id =
|
167
|
fprintf fmt "T_%i" id
|
168
|
|
169
|
(** Print a type.
|
170
|
@param fmt the formater to print on
|
171
|
@param type the type
|
172
|
**)
|
173
|
let pp_type fmt typ =
|
174
|
(match (Types.repr typ).Types.tdesc with
|
175
|
| Types.Tbasic Types.Basic.Tint -> pp_integer_type fmt
|
176
|
| Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
|
177
|
| Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
|
178
|
| Types.Tunivar -> pp_polymorphic_type fmt typ.tid
|
179
|
| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false (*TODO*)
|
180
|
)
|
181
|
|
182
|
(** Print the type of a variable.
|
183
|
@param fmt the formater to print on
|
184
|
@param id the variable
|
185
|
**)
|
186
|
let pp_var_type fmt id =
|
187
|
pp_type fmt id.var_type
|
188
|
|
189
|
(** Extract all the inputs and outputs.
|
190
|
@param machine the machine
|
191
|
@return a list of all the var_decl of a macine
|
192
|
**)
|
193
|
let get_all_vars_machine m =
|
194
|
m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic
|
195
|
|
196
|
(** Check if a type is polymorphic.
|
197
|
@param typ the type
|
198
|
@return true if its polymorphic
|
199
|
**)
|
200
|
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar
|
201
|
|
202
|
(** Find all polymorphic type : Types.Tunivar in a machine.
|
203
|
@param machine the machine
|
204
|
@return a list of id corresponding to polymorphic type
|
205
|
**)
|
206
|
let find_all_polymorphic_type m =
|
207
|
let vars = get_all_vars_machine m in
|
208
|
let extract id = id.var_type.tid in
|
209
|
let polymorphic_type_vars =
|
210
|
List.filter (function x-> is_Tunivar x.var_type) vars in
|
211
|
List.sort_uniq (-) (List.map extract polymorphic_type_vars)
|
212
|
|
213
|
(** Print a package name with polymorphic types specified.
|
214
|
@param substitution correspondance between polymorphic type id and their instantiation
|
215
|
@param fmt the formater to print on
|
216
|
@param machine the machine
|
217
|
**)
|
218
|
let pp_package_name_with_polymorphic substitution fmt machine =
|
219
|
let polymorphic_types = find_all_polymorphic_type machine in
|
220
|
assert(List.length polymorphic_types = List.length substitution);
|
221
|
let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
|
222
|
assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
|
223
|
polymorphic_types substituion);
|
224
|
let instantiated_types = snd (List.split substitution) in
|
225
|
fprintf fmt "%a%t%a"
|
226
|
pp_package_name machine
|
227
|
(Utils.pp_final_char_if_non_empty "_" instantiated_types)
|
228
|
(Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
|
229
|
|
230
|
|
231
|
(* Variable pretty print functions *)
|
232
|
|
233
|
(** Represent the possible mode for a type of a procedure parameter **)
|
234
|
type parameter_mode = NoMode | In | Out | InOut
|
235
|
|
236
|
(** Print a parameter_mode.
|
237
|
@param fmt the formater to print on
|
238
|
@param mode the modifier
|
239
|
**)
|
240
|
let pp_parameter_mode fmt mode =
|
241
|
fprintf fmt "%s" (match mode with
|
242
|
| NoMode -> ""
|
243
|
| In -> "in"
|
244
|
| Out -> "out"
|
245
|
| InOut -> "in out")
|
246
|
|
247
|
(** Print the name of the state variable.
|
248
|
@param fmt the formater to print on
|
249
|
**)
|
250
|
let pp_state_name fmt =
|
251
|
fprintf fmt "state"
|
252
|
|
253
|
|
254
|
(** Print the name of a variable.
|
255
|
@param fmt the formater to print on
|
256
|
@param id the variable
|
257
|
**)
|
258
|
let pp_var_name fmt id =
|
259
|
fprintf fmt "%a" pp_clean_ada_identifier id.var_id
|
260
|
|
261
|
(** Print a variable declaration
|
262
|
@param mode input/output mode of the parameter
|
263
|
@param pp_name a format printer wich print the variable name
|
264
|
@param pp_type a format printer wich print the variable type
|
265
|
@param fmt the formater to print on
|
266
|
@param id the variable
|
267
|
**)
|
268
|
let pp_var_decl fmt (mode, pp_name, pp_type) =
|
269
|
fprintf fmt "%t: %a%s%t"
|
270
|
pp_name
|
271
|
pp_parameter_mode mode
|
272
|
(if mode = NoMode then "" else " ")
|
273
|
pp_type
|
274
|
|
275
|
(** Print variable declaration for machine variable
|
276
|
@param mode input/output mode of the parameter
|
277
|
@param fmt the formater to print on
|
278
|
@param id the variable
|
279
|
**)
|
280
|
let pp_machine_var_decl mode fmt id =
|
281
|
let pp_name = function fmt -> pp_var_name fmt id in
|
282
|
let pp_type = function fmt -> pp_var_type fmt id in
|
283
|
pp_var_decl fmt (mode, pp_name, pp_type)
|
284
|
|
285
|
(** Print variable declaration for a local state variable
|
286
|
@param fmt the formater to print on
|
287
|
@param mode input/output mode of the parameter
|
288
|
**)
|
289
|
let pp_state_var_decl fmt mode =
|
290
|
let pp_name = pp_state_name in
|
291
|
let pp_type = pp_state_type in
|
292
|
pp_var_decl fmt (mode, pp_name, pp_type)
|
293
|
|
294
|
(** Print the declaration of a state element of a machine.
|
295
|
@param substitution correspondance between polymorphic type id and their instantiation
|
296
|
@param name name of the variable
|
297
|
@param fmt the formater to print on
|
298
|
@param machine the machine
|
299
|
**)
|
300
|
let pp_node_state_decl substitution name fmt machine =
|
301
|
let pp_package fmt = pp_package_name_with_polymorphic substitution fmt machine in
|
302
|
let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
|
303
|
let pp_name fmt = pp_clean_ada_identifier fmt name in
|
304
|
pp_var_decl fmt (NoMode, pp_name, pp_type)
|
305
|
|
306
|
|
307
|
(* Prototype pretty print functions *)
|
308
|
|
309
|
(** Print the reset of the init procedure **)
|
310
|
let pp_reset_procedure_name fmt = fprintf fmt "reset"
|
311
|
|
312
|
(** Print the step of the init procedure **)
|
313
|
let pp_step_procedure_name fmt = fprintf fmt "step"
|
314
|
|
315
|
(** Print the name of the init procedure **)
|
316
|
let pp_init_procedure_name fmt = fprintf fmt "init"
|
317
|
|
318
|
(** Print the clear of the init procedure **)
|
319
|
let pp_clear_procedure_name fmt = fprintf fmt "clear"
|
320
|
|
321
|
(** Print the prototype of a procedure with non input/outputs
|
322
|
@param fmt the formater to print on
|
323
|
@param name the name of the procedure
|
324
|
**)
|
325
|
let pp_simple_prototype pp_name fmt =
|
326
|
fprintf fmt "procedure %t" pp_name
|
327
|
|
328
|
(** Print the prototype of a machine procedure. The first parameter is always
|
329
|
the state, state_modifier specify the modifier applying to it. The next
|
330
|
parameters are inputs and the last parameters are the outputs.
|
331
|
@param state_mode the input/output mode for the state parameter
|
332
|
@param input list of the input parameter of the procedure
|
333
|
@param output list of the output parameter of the procedure
|
334
|
@param fmt the formater to print on
|
335
|
@param name the name of the procedure
|
336
|
**)
|
337
|
let pp_base_prototype state_mode input output fmt pp_name =
|
338
|
fprintf fmt "procedure %t(@[<v>%a%t@[%a@]%t@[%a@])@]"
|
339
|
pp_name
|
340
|
pp_state_var_decl state_mode
|
341
|
(Utils.pp_final_char_if_non_empty ";@," input)
|
342
|
(Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl In)) input
|
343
|
(Utils.pp_final_char_if_non_empty ";@," output)
|
344
|
(Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl Out)) output
|
345
|
|
346
|
(** Print the prototype of the step procedure of a machine.
|
347
|
@param m the machine
|
348
|
@param fmt the formater to print on
|
349
|
@param pp_name name function printer
|
350
|
**)
|
351
|
let pp_step_prototype m fmt =
|
352
|
pp_base_prototype InOut m.mstep.step_inputs m.mstep.step_outputs fmt pp_step_procedure_name
|
353
|
|
354
|
(** Print the prototype of the reset procedure of a machine.
|
355
|
@param m the machine
|
356
|
@param fmt the formater to print on
|
357
|
@param pp_name name function printer
|
358
|
**)
|
359
|
let pp_reset_prototype m fmt =
|
360
|
pp_base_prototype InOut m.mstatic [] fmt pp_reset_procedure_name
|
361
|
|
362
|
(** Print the prototype of the init procedure of a machine.
|
363
|
@param m the machine
|
364
|
@param fmt the formater to print on
|
365
|
@param pp_name name function printer
|
366
|
**)
|
367
|
let pp_init_prototype m fmt =
|
368
|
pp_base_prototype Out m.mstatic [] fmt pp_init_procedure_name
|
369
|
|
370
|
(** Print the prototype of the clear procedure of a machine.
|
371
|
@param m the machine
|
372
|
@param fmt the formater to print on
|
373
|
@param pp_name name function printer
|
374
|
**)
|
375
|
let pp_clear_prototype m fmt =
|
376
|
pp_base_prototype InOut m.mstatic [] fmt pp_clear_procedure_name
|
377
|
|
378
|
|
379
|
(* Procedure pretty print functions *)
|
380
|
|
381
|
(** Print the definition of a procedure
|
382
|
@param pp_name the procedure name printer
|
383
|
@param pp_prototype the prototype printer
|
384
|
@param pp_instr local var printer
|
385
|
@param pp_instr instruction printer
|
386
|
@param fmt the formater to print on
|
387
|
@param locals locals var list
|
388
|
@param instrs instructions list
|
389
|
**)
|
390
|
let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals, instrs) =
|
391
|
fprintf fmt "@[<v>%t is%t@[<v>%a%t@]@,begin@, @[<v>%a%t@]@,end %t@]"
|
392
|
pp_prototype
|
393
|
(Utils.pp_final_char_if_non_empty "@, " locals)
|
394
|
(Utils.fprintf_list ~sep:";@," pp_local) locals
|
395
|
(Utils.pp_final_char_if_non_empty ";" locals)
|
396
|
(Utils.fprintf_list ~sep:";@," pp_instr) instrs
|
397
|
(Utils.pp_final_char_if_non_empty ";" instrs)
|
398
|
pp_name
|
399
|
|