Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_printer.ml @ 173a2a8f

History | View | Annotate | Download (11.3 KB)

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 * (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, pres, posts) ->
90
      assert(ghost || (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" (Utils.pp_final_char_if_non_empty ",@," contract)
94
      in
95
      let pp_aspect aspect fmt pps = if pps = [] then fprintf fmt "" else
96
        fprintf fmt "%s => %t" aspect (pp_and pps)
97
      in
98
      let pp_contract fmt = if contract = [] then fprintf fmt "" else
99
        let sep fmt = if pres != [] && posts != [] then fprintf fmt ",@," else fprintf fmt "" in
100
        fprintf fmt "@,  @[<v>%a%t%a@]"
101
          (pp_aspect "Pre") pres
102
          sep
103
          (pp_aspect "Post") posts
104
      in
105
      fprintf fmt " with%t%t"
106
        pp_ghost
107
        pp_contract
108

    
109
(** Print instanciation of a generic type in a new statement.
110
   @param fmt the formater to print on
111
   @param id id of the polymorphic type
112
   @param typ the new type
113
**)
114
let pp_generic_instanciation (pp_name, pp_type) fmt =
115
  fprintf fmt "%t => %t" pp_name pp_type
116

    
117
(** Print a variable declaration with mode
118
   @param mode input/output mode of the parameter
119
   @param pp_name a format printer wich print the variable name
120
   @param pp_type a format printer wich print the variable type
121
   @param fmt the formater to print on
122
   @param id the variable
123
**)
124
let pp_var_decl (mode, pp_name, pp_type, with_statement) fmt =
125
  fprintf fmt "%t: %a%s%t%a"
126
    pp_name
127
    pp_parameter_mode mode
128
    (if mode = AdaNoMode then "" else " ")
129
    pp_type
130
    pp_ada_with with_statement
131

    
132
let apply_var_decl_lists var_list =
133
  List.map (fun l-> List.map pp_var_decl l) var_list
134

    
135
let pp_generic fmt = function
136
    | [] -> fprintf fmt ""
137
    | l -> fprintf fmt "generic@,%a" pp_block l
138

    
139
let pp_opt intro fmt = function
140
  | None -> fprintf fmt ""
141
  | Some pp -> fprintf fmt " %s %t" intro pp
142

    
143
let rec pp_local local fmt =
144
  match local with
145
    | AdaLocalVar var -> pp_var_decl var fmt
146
    | AdaLocalPackage (pp_name, pp_base_name, instanciations) ->
147
        pp_package_instanciation pp_name pp_base_name fmt instanciations
148
and pp_content pp_name fmt = function
149
  | AdaNoContent ->
150
      fprintf fmt ""
151
  | AdaVisibilityDefinition visbility ->
152
      fprintf fmt " is %a" pp_visibility visbility
153
  | AdaPackageContent pp_package ->
154
      fprintf fmt " is@,  @[<v>%t;@]@,end %t" pp_package pp_name
155
  | AdaSimpleContent pp_content ->
156
      fprintf fmt " is@,  @[<v 2>(%t)@]" pp_content
157
  | AdaProcedureContent (local_list, pp_instr_list) ->
158
      fprintf fmt " is@,%abegin@,%aend %t"
159
        pp_block (List.map (fun l -> pp_group ~sep:";@;" (List.map pp_local l)) local_list)
160
        pp_block pp_instr_list
161
        pp_name
162
  | AdaRecord var_list ->
163
      assert(var_list != []);
164
      let pp_lists = apply_var_decl_lists var_list in
165
      fprintf fmt " is@,  @[<v>record@,  @[<v>%a@]@,end record@]"
166
        pp_block (List.map (pp_group ~sep:";@;") pp_lists)
167
  | AdaPackageInstanciation (pp_name, instanciations) ->
168
      fprintf fmt " is new %t%a"
169
        pp_name
170
        (pp_args ~sep:",@,") (List.map pp_generic_instanciation instanciations)
171
and pp_def fmt (pp_generics, kind_def, pp_name, args, pp_type_opt, content, pp_with_opt) =
172
  let pp_arg_lists = apply_var_decl_lists args in
173
  fprintf fmt "%a%a %t%a%a%a%a"
174
    pp_generic pp_generics
175
    pp_kind_def kind_def
176
    pp_name
177
    (pp_args ~sep:";@,") (List.map (pp_group ~sep:";@,") pp_arg_lists)
178
    (pp_opt "return") pp_type_opt
179
    (pp_content pp_name) content
180
    pp_ada_with pp_with_opt
181
and pp_package_instanciation pp_name pp_base_name fmt instanciations =
182
  pp_def fmt ([], AdaPackageDecl, pp_name, [], None, (AdaPackageInstanciation (pp_base_name, instanciations)), None)
183

    
184
let pp_adastring pp_content fmt =
185
  fprintf fmt "\"%t\"" pp_content
186

    
187
(** Print the ada package introduction sentence it can be used for body and
188
declaration. Boolean parameter body should be true if it is a body delcaration.
189
   @param fmt the formater to print on
190
   @param fmt the formater to print on
191
   @param machine the machine
192
**)
193
let pp_package pp_name pp_generics body fmt pp_content =
194
  let kind = if body then AdaPackageBody else AdaPackageDecl in
195
  pp_def fmt (pp_generics, kind, pp_name, [], None, (AdaPackageContent pp_content), None)
196

    
197
(** Print a new statement instantiating a generic package.
198
   @param fmt the formater to print on
199
   @param substitutions the instanciation substitution
200
   @param machine the machine to instanciate
201
**)
202

    
203
(** Print a type declaration
204
   @param fmt the formater to print on
205
   @param pp_name a format printer which print the type name
206
   @param pp_value a format printer which print the type definition
207
**)
208
let pp_type_decl pp_name visibility fmt =
209
  let v = match visibility with
210
    | AdaNoVisibility -> AdaNoContent
211
    | _ -> AdaVisibilityDefinition visibility
212
  in
213
  pp_def fmt ([], AdaType, pp_name, [], None, v, None)
214

    
215
let pp_record pp_name fmt var_lists =
216
  pp_def fmt ([], AdaType, pp_name, [], None, AdaRecord var_lists, None)
217

    
218
let pp_procedure pp_name args pp_with_opt fmt content =
219
  pp_def fmt ([], AdaProcedure, pp_name, args, None, content, pp_with_opt)
220

    
221
let pp_predicate pp_name args fmt content_opt =
222
  let content, with_st = match content_opt with
223
    | Some content -> AdaSimpleContent content, None
224
    | None -> AdaNoContent, Some (true, [], [])
225
  in
226
  pp_def fmt ([], AdaFunction, pp_name, args, Some pp_boolean_type, content, with_st)
227

    
228
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
229
    underscore and must not contain a double underscore
230
   @param var name to be cleaned*)
231
let pp_clean_ada_identifier fmt name =
232
  let reserved_words = ["abort"; "else"; "new"; "return"; "boolean"; "integer";
233
                        "abs"; "elsif"; "not"; "reverse"; "abstract"; "end";
234
                        "null"; "accept"; "entry"; "select"; "access";
235
                        "exception"; "of"; "separate"; "aliased"; "exit";
236
                        "or"; "some"; "all"; "others"; "subtype"; "and";
237
                        "for"; "out"; "synchronized"; "array"; "function";
238
                        "overriding"; "at"; "tagged"; "generic"; "package";
239
                        "task"; "begin"; "goto"; "pragma"; "terminate";
240
                        "body"; "private"; "then"; "if"; "procedure"; "type";
241
                        "case"; "in"; "protected"; "constant"; "interface";
242
                        "until"; "is"; "raise"; "use"; "declare"; "	range";
243
                        "delay"; "limited"; "record"; "when"; "delta"; "loop";
244
                        "rem"; "while"; "digits"; "renames"; "with"; "do";
245
                        "mod"; "requeue"; "xor"; "float"] in
246
  let base_size = String.length name in
247
  assert(base_size > 0);
248
  let rec remove_double_underscore s = function
249
    | i when i == String.length s - 1 -> s
250
    | i when String.get s i == '_' && String.get s (i+1) == '_' ->
251
        remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
252
    | i -> remove_double_underscore s (i+1)
253
  in
254
  let name = if String.get name (base_size-1) == '_' then name^"ada" else name in
255
  let name = remove_double_underscore name 0 in
256
  let prefix = if String.length name != base_size
257
                  || String.get name 0 == '_' 
258
                  || List.exists (String.equal (String.lowercase_ascii name)) reserved_words then
259
                  "ada"
260
               else
261
                  ""
262
  in
263
  fprintf fmt "%s%s" prefix name
264

    
265
(** Print the access of an item from an other package.
266
   @param fmt the formater to print on
267
   @param package the package to use
268
   @param item the item which is accessed
269
**)
270
let pp_package_access (pp_package, pp_item) fmt =
271
  fprintf fmt "%t.%t" pp_package pp_item
272

    
273
let pp_with visibility fmt pp_pakage_name =
274
  fprintf fmt "%a with %t" pp_visibility visibility pp_pakage_name
275

    
276
(** Print a one line comment with the final new line character to avoid
277
      commenting anything else.
278
   @param fmt the formater to print on
279
   @param s the comment without newline character
280
**)
281
let pp_oneline_comment fmt s =
282
  assert (not (String.contains s '\n'));
283
  fprintf fmt "-- %s@," s
284

    
285
let pp_call fmt (pp_name, args) =
286
  fprintf fmt "%t%a"
287
    pp_name
288
    (pp_args ~sep:",@ ") (List.map (pp_group ~sep:",@,") args)
289

    
290

    
291
(** Print the complete name of variable.
292
   @param m the machine to check if it is memory
293
   @param fmt the formater to print on
294
   @param var the variable
295
**)
296
let pp_access pp_state pp_var fmt =
297
  fprintf fmt "%t.%t" pp_state pp_var
298

    
299
let pp_old pp fmt = fprintf fmt "%t'Old" pp
300