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