1
|
open Utils
|
2
|
open Format
|
3
|
|
4
|
(** Represent the possible mode for a type of a procedure parameter **)
|
5
|
type parameter_mode = AdaNoMode | AdaIn | AdaOut | AdaInOut
|
6
|
|
7
|
type kind_def =
|
8
|
| AdaType
|
9
|
| AdaProcedure
|
10
|
| AdaFunction
|
11
|
| AdaPackageDecl
|
12
|
| AdaPackageBody
|
13
|
|
14
|
type visibility = AdaNoVisibility | AdaPrivate | AdaLimitedPrivate
|
15
|
|
16
|
type printer = Format.formatter -> unit
|
17
|
|
18
|
type ada_with = (bool * bool * printer list * printer list) option
|
19
|
|
20
|
type ada_var_decl = parameter_mode * printer * printer * ada_with
|
21
|
|
22
|
type ada_local_decl =
|
23
|
| AdaLocalVar of ada_var_decl
|
24
|
| AdaLocalPackage of (printer * printer * (printer * printer) list)
|
25
|
|
26
|
type def_content =
|
27
|
| AdaNoContent
|
28
|
| AdaPackageContent of printer
|
29
|
| AdaSimpleContent of printer
|
30
|
| AdaVisibilityDefinition of visibility
|
31
|
| AdaProcedureContent of (ada_local_decl list list * printer list)
|
32
|
| AdaRecord of ada_var_decl list list
|
33
|
| AdaPackageInstanciation of (printer * (printer * printer) list)
|
34
|
|
35
|
(** Print a parameter_mode. @param fmt the formater to print on @param mode the
|
36
|
modifier **)
|
37
|
let pp_parameter_mode fmt mode =
|
38
|
fprintf fmt "%s"
|
39
|
(match mode with
|
40
|
| AdaNoMode ->
|
41
|
""
|
42
|
| AdaIn ->
|
43
|
"in"
|
44
|
| AdaOut ->
|
45
|
"out"
|
46
|
| AdaInOut ->
|
47
|
"in out")
|
48
|
|
49
|
let pp_kind_def fmt kind_def =
|
50
|
fprintf fmt "%s"
|
51
|
(match kind_def with
|
52
|
| AdaType ->
|
53
|
"type"
|
54
|
| AdaProcedure ->
|
55
|
"procedure"
|
56
|
| AdaFunction ->
|
57
|
"function"
|
58
|
| AdaPackageDecl ->
|
59
|
"package"
|
60
|
| AdaPackageBody ->
|
61
|
"package body")
|
62
|
|
63
|
let pp_visibility fmt visibility =
|
64
|
fprintf fmt "%s"
|
65
|
(match visibility with
|
66
|
| AdaNoVisibility ->
|
67
|
""
|
68
|
| AdaPrivate ->
|
69
|
"private"
|
70
|
| AdaLimitedPrivate ->
|
71
|
"limited private")
|
72
|
|
73
|
(** Print the integer type name. @param fmt the formater to print on **)
|
74
|
let pp_integer_type fmt = fprintf fmt "Integer"
|
75
|
|
76
|
(** Print the float type name. @param fmt the formater to print on **)
|
77
|
let pp_float_type fmt = fprintf fmt "Float"
|
78
|
|
79
|
(** Print the boolean type name. @param fmt the formater to print on **)
|
80
|
let pp_boolean_type fmt = fprintf fmt "Boolean"
|
81
|
|
82
|
let pp_group ~pp_sep pp_list fmt =
|
83
|
assert (pp_list != []);
|
84
|
fprintf fmt "@[%a@]" (pp_print_list ~pp_sep (fun fmt pp -> pp fmt)) pp_list
|
85
|
|
86
|
let pp_args ~pp_sep fmt = function
|
87
|
| [] ->
|
88
|
fprintf fmt ""
|
89
|
| args ->
|
90
|
fprintf fmt " (@[<v>%a)@]"
|
91
|
(pp_print_list ~pp_sep (fun fmt pp -> pp fmt))
|
92
|
args
|
93
|
|
94
|
let pp_block fmt pp_item_list =
|
95
|
pp_print_list
|
96
|
~pp_open_box:pp_open_vbox0
|
97
|
~pp_prologue:(fun fmt () -> pp_print_string fmt " ")
|
98
|
~pp_epilogue:pp_print_semicolon
|
99
|
~pp_sep:pp_print_semicolon (fun fmt pp -> pp fmt)
|
100
|
fmt
|
101
|
pp_item_list
|
102
|
|
103
|
let pp_and l fmt =
|
104
|
fprintf fmt "(%t)" (pp_group ~pp_sep:(fun fmt () -> fprintf fmt "@ and then ") l)
|
105
|
|
106
|
let pp_or l fmt =
|
107
|
fprintf fmt "(%t)" (pp_group ~pp_sep:(fun fmt () -> fprintf fmt "@ or ") l)
|
108
|
|
109
|
let pp_ada_with fmt = function
|
110
|
| None ->
|
111
|
fprintf fmt ""
|
112
|
| Some (ghost, import, pres, posts) ->
|
113
|
assert (ghost || import || pres != [] || posts != []);
|
114
|
let contract = pres @ posts in
|
115
|
let pp_ghost fmt =
|
116
|
if not ghost then fprintf fmt ""
|
117
|
else
|
118
|
fprintf fmt " Ghost%t" (fun fmt ->
|
119
|
if contract != [] || import then fprintf fmt ",@,"
|
120
|
else fprintf fmt "")
|
121
|
in
|
122
|
let pp_import fmt =
|
123
|
if not import then fprintf fmt ""
|
124
|
else
|
125
|
fprintf fmt " Import%a"
|
126
|
(if contract = [] then pp_print_nothing else pp_print_comma) ()
|
127
|
in
|
128
|
let pp_aspect aspect fmt pps =
|
129
|
if pps = [] then fprintf fmt ""
|
130
|
else fprintf fmt "%s => %t" aspect (pp_and pps)
|
131
|
in
|
132
|
let pp_contract fmt =
|
133
|
if contract = [] then fprintf fmt ""
|
134
|
else
|
135
|
let sep fmt =
|
136
|
if pres != [] && posts != [] then fprintf fmt ",@,"
|
137
|
else fprintf fmt ""
|
138
|
in
|
139
|
fprintf fmt "@, @[<v>%a%t%a@]" (pp_aspect "Pre") pres sep
|
140
|
(pp_aspect "Post") posts
|
141
|
in
|
142
|
fprintf fmt " with%t%t%t" pp_ghost pp_import pp_contract
|
143
|
|
144
|
(** Print instanciation of a generic type in a new statement. @param fmt the
|
145
|
formater to print on @param id id of the polymorphic type @param typ the new
|
146
|
type **)
|
147
|
let pp_generic_instanciation (pp_name, pp_type) fmt =
|
148
|
fprintf fmt "%t => %t" pp_name pp_type
|
149
|
|
150
|
(** Print a variable declaration with mode @param mode input/output mode of the
|
151
|
parameter @param pp_name a format printer wich print the variable name
|
152
|
@param pp_type a format printer wich print the variable type @param fmt the
|
153
|
formater to print on @param id the variable **)
|
154
|
let pp_var_decl (mode, pp_name, pp_type, with_statement) fmt =
|
155
|
fprintf fmt "%t: %a%s%t%a" pp_name pp_parameter_mode mode
|
156
|
(if mode = AdaNoMode then "" else " ")
|
157
|
pp_type pp_ada_with with_statement
|
158
|
|
159
|
let apply_var_decl_lists var_list =
|
160
|
List.map (fun l -> List.map pp_var_decl l) var_list
|
161
|
|
162
|
let pp_generic fmt = function
|
163
|
| [] ->
|
164
|
fprintf fmt ""
|
165
|
| l ->
|
166
|
fprintf fmt "generic@,%a" pp_block l
|
167
|
|
168
|
let pp_opt intro fmt = function
|
169
|
| None ->
|
170
|
fprintf fmt ""
|
171
|
| Some pp ->
|
172
|
fprintf fmt " %s %t" intro pp
|
173
|
|
174
|
let rec pp_local local fmt =
|
175
|
match local with
|
176
|
| AdaLocalVar var ->
|
177
|
pp_var_decl var fmt
|
178
|
| AdaLocalPackage (pp_name, pp_base_name, instanciations) ->
|
179
|
pp_package_instanciation pp_name pp_base_name fmt instanciations
|
180
|
|
181
|
and pp_content pp_name fmt = function
|
182
|
| AdaNoContent ->
|
183
|
fprintf fmt ""
|
184
|
| AdaVisibilityDefinition visbility ->
|
185
|
fprintf fmt " is %a" pp_visibility visbility
|
186
|
| AdaPackageContent pp_package ->
|
187
|
fprintf fmt " is@, @[<v>%t;@]@,end %t" pp_package pp_name
|
188
|
| AdaSimpleContent pp_content ->
|
189
|
fprintf fmt " is@, @[<v 2>(%t)@]" pp_content
|
190
|
| AdaProcedureContent (local_list, pp_instr_list) ->
|
191
|
fprintf fmt " is@,%abegin@,%aend %t" pp_block
|
192
|
(List.map (fun l -> pp_group ~pp_sep:pp_print_semicolon (List.map pp_local l)) local_list)
|
193
|
pp_block pp_instr_list pp_name
|
194
|
| AdaRecord var_list ->
|
195
|
assert (var_list != []);
|
196
|
let pp_lists = apply_var_decl_lists var_list in
|
197
|
fprintf fmt " is@, @[<v>record@, @[<v>%a@]@,end record@]" pp_block
|
198
|
(List.map (pp_group ~pp_sep:pp_print_semicolon) pp_lists)
|
199
|
| AdaPackageInstanciation (pp_name, instanciations) ->
|
200
|
fprintf fmt " is new %t%a" pp_name (pp_args ~pp_sep:pp_print_comma)
|
201
|
(List.map pp_generic_instanciation instanciations)
|
202
|
|
203
|
and pp_def fmt
|
204
|
(pp_generics, kind_def, pp_name, args, pp_type_opt, content, pp_with_opt) =
|
205
|
let pp_arg_lists = apply_var_decl_lists args in
|
206
|
fprintf fmt "%a%a %t%a%a%a%a" pp_generic pp_generics pp_kind_def kind_def
|
207
|
pp_name (pp_args ~pp_sep:pp_print_semicolon)
|
208
|
(List.map (pp_group ~pp_sep:pp_print_semicolon) pp_arg_lists)
|
209
|
(pp_opt "return") pp_type_opt (pp_content pp_name) content pp_ada_with
|
210
|
pp_with_opt
|
211
|
|
212
|
and pp_package_instanciation pp_name pp_base_name fmt instanciations =
|
213
|
pp_def fmt
|
214
|
( [],
|
215
|
AdaPackageDecl,
|
216
|
pp_name,
|
217
|
[],
|
218
|
None,
|
219
|
AdaPackageInstanciation (pp_base_name, instanciations),
|
220
|
None )
|
221
|
|
222
|
let pp_adastring pp_content fmt = fprintf fmt "\"%t\"" pp_content
|
223
|
|
224
|
(** Print the ada package introduction sentence it can be used for body and
|
225
|
declaration. Boolean parameter body should be true if it is a body
|
226
|
delcaration. @param fmt the formater to print on @param fmt the formater to
|
227
|
print on @param machine the machine **)
|
228
|
let pp_package pp_name pp_generics body fmt pp_content =
|
229
|
let kind = if body then AdaPackageBody else AdaPackageDecl in
|
230
|
pp_def fmt
|
231
|
(pp_generics, kind, pp_name, [], None, AdaPackageContent pp_content, None)
|
232
|
|
233
|
(** Print a new statement instantiating a generic package. @param fmt the
|
234
|
formater to print on @param substitutions the instanciation substitution
|
235
|
@param machine the machine to instanciate **)
|
236
|
|
237
|
(** Print a type declaration @param fmt the formater to print on @param pp_name
|
238
|
a format printer which print the type name @param pp_value a format printer
|
239
|
which print the type definition **)
|
240
|
let pp_type_decl pp_name visibility fmt =
|
241
|
let v =
|
242
|
match visibility with
|
243
|
| AdaNoVisibility ->
|
244
|
AdaNoContent
|
245
|
| _ ->
|
246
|
AdaVisibilityDefinition visibility
|
247
|
in
|
248
|
pp_def fmt ([], AdaType, pp_name, [], None, v, None)
|
249
|
|
250
|
let pp_record pp_name fmt var_lists =
|
251
|
pp_def fmt ([], AdaType, pp_name, [], None, AdaRecord var_lists, None)
|
252
|
|
253
|
let pp_procedure pp_name args pp_with_opt fmt content =
|
254
|
pp_def fmt ([], AdaProcedure, pp_name, args, None, content, pp_with_opt)
|
255
|
|
256
|
let pp_predicate pp_name args imported fmt content_opt =
|
257
|
let content, with_st =
|
258
|
match content_opt with
|
259
|
| Some content ->
|
260
|
AdaSimpleContent content, None
|
261
|
| None ->
|
262
|
AdaNoContent, Some (true, imported, [], [])
|
263
|
in
|
264
|
pp_def fmt
|
265
|
([], AdaFunction, pp_name, args, Some pp_boolean_type, content, with_st)
|
266
|
|
267
|
(** Print a cleaned an identifier for ada exportation : Ada names must not start
|
268
|
by an underscore and must not contain a double underscore @param var name to
|
269
|
be cleaned*)
|
270
|
let pp_clean_ada_identifier fmt name =
|
271
|
let reserved_words =
|
272
|
[
|
273
|
"abort";
|
274
|
"else";
|
275
|
"new";
|
276
|
"return";
|
277
|
"boolean";
|
278
|
"integer";
|
279
|
"abs";
|
280
|
"elsif";
|
281
|
"not";
|
282
|
"reverse";
|
283
|
"abstract";
|
284
|
"end";
|
285
|
"null";
|
286
|
"accept";
|
287
|
"entry";
|
288
|
"select";
|
289
|
"access";
|
290
|
"exception";
|
291
|
"of";
|
292
|
"separate";
|
293
|
"aliased";
|
294
|
"exit";
|
295
|
"or";
|
296
|
"some";
|
297
|
"all";
|
298
|
"others";
|
299
|
"subtype";
|
300
|
"and";
|
301
|
"for";
|
302
|
"out";
|
303
|
"synchronized";
|
304
|
"array";
|
305
|
"function";
|
306
|
"overriding";
|
307
|
"at";
|
308
|
"tagged";
|
309
|
"generic";
|
310
|
"package";
|
311
|
"task";
|
312
|
"begin";
|
313
|
"goto";
|
314
|
"pragma";
|
315
|
"terminate";
|
316
|
"body";
|
317
|
"private";
|
318
|
"then";
|
319
|
"if";
|
320
|
"procedure";
|
321
|
"type";
|
322
|
"case";
|
323
|
"in";
|
324
|
"protected";
|
325
|
"constant";
|
326
|
"interface";
|
327
|
"until";
|
328
|
"is";
|
329
|
"raise";
|
330
|
"use";
|
331
|
"declare";
|
332
|
"\trange";
|
333
|
"delay";
|
334
|
"limited";
|
335
|
"record";
|
336
|
"when";
|
337
|
"delta";
|
338
|
"loop";
|
339
|
"rem";
|
340
|
"while";
|
341
|
"digits";
|
342
|
"renames";
|
343
|
"with";
|
344
|
"do";
|
345
|
"mod";
|
346
|
"requeue";
|
347
|
"xor";
|
348
|
"float";
|
349
|
]
|
350
|
in
|
351
|
let base_size = String.length name in
|
352
|
assert (base_size > 0);
|
353
|
let rec remove_double_underscore s = function
|
354
|
| i when i == String.length s - 1 ->
|
355
|
s
|
356
|
| i when String.get s i == '_' && String.get s (i + 1) == '_' ->
|
357
|
remove_double_underscore
|
358
|
(sprintf "%s%s" (String.sub s 0 i)
|
359
|
(String.sub s (i + 1) (String.length s - i - 1)))
|
360
|
i
|
361
|
| i ->
|
362
|
remove_double_underscore s (i + 1)
|
363
|
in
|
364
|
let name =
|
365
|
if String.get name (base_size - 1) == '_' then name ^ "ada" else name
|
366
|
in
|
367
|
let name = remove_double_underscore name 0 in
|
368
|
let prefix =
|
369
|
if
|
370
|
String.length name != base_size
|
371
|
|| String.get name 0 == '_'
|
372
|
|| List.exists (String.equal (String.lowercase_ascii name)) reserved_words
|
373
|
then "ada"
|
374
|
else ""
|
375
|
in
|
376
|
fprintf fmt "%s%s" prefix name
|
377
|
|
378
|
(** Print the access of an item from an other package. @param fmt the formater
|
379
|
to print on @param package the package to use @param item the item which is
|
380
|
accessed **)
|
381
|
let pp_package_access (pp_package, pp_item) fmt =
|
382
|
fprintf fmt "%t.%t" pp_package pp_item
|
383
|
|
384
|
let pp_with visibility fmt pp_pakage_name =
|
385
|
fprintf fmt "%a with %t" pp_visibility visibility pp_pakage_name
|
386
|
|
387
|
(** Print a one line comment with the final new line character to avoid
|
388
|
commenting anything else. @param fmt the formater to print on @param s the
|
389
|
comment without newline character **)
|
390
|
let pp_oneline_comment fmt s =
|
391
|
assert (not (String.contains s '\n'));
|
392
|
fprintf fmt "-- %s@," s
|
393
|
|
394
|
let pp_call fmt (pp_name, args) =
|
395
|
fprintf fmt "%t%a" pp_name (pp_args ~pp_sep:pp_print_comma)
|
396
|
(List.map (pp_group ~pp_sep:pp_print_comma) args)
|
397
|
|
398
|
(** Print the complete name of variable. @param m the machine to check if it is
|
399
|
memory @param fmt the formater to print on @param var the variable **)
|
400
|
let pp_access pp_state pp_var fmt = fprintf fmt "%t.%t" pp_state pp_var
|
401
|
|
402
|
let pp_old pp fmt = fprintf fmt "%t'Old" pp
|