Project

General

Profile

Download (11.7 KB) Statistics
| Branch: | Tag: | Revision:
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
(12-12/17)