Project

General

Profile

« Previous | Next » 

Revision b5b745fb

Added by Guillaume DAVY almost 3 years ago

Ada: First support for transition predicate generation.

View differences:

src/backends/Ada/ada_printer.ml
9 9

  
10 10
type printer = Format.formatter -> unit
11 11

  
12
type ada_var_decl = parameter_mode * printer * printer
12
type ada_with = (bool * (printer list) * (printer list)) option
13

  
14
type ada_var_decl = parameter_mode * printer * printer * ada_with
13 15

  
14 16
type ada_local_decl =
15 17
  | AdaLocalVar of ada_var_decl
......
17 19

  
18 20
type def_content =
19 21
  | AdaNoContent
20
  | AdaPackageContent of (Format.formatter -> unit)
22
  | AdaPackageContent of printer
23
  | AdaSimpleContent of printer
21 24
  | AdaVisibilityDefinition of visibility
22 25
  | AdaProcedureContent of ((ada_local_decl list list) * (printer list))
23 26
  | AdaRecord of ((ada_var_decl list) list)
......
48 51
                     | AdaPrivate          -> "private"
49 52
                     | AdaLimitedPrivate   -> "limited private")
50 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

  
51 69
let pp_group ~sep:sep pp_list fmt =
52 70
  assert(pp_list != []);
53 71
  fprintf fmt "@[%a@]"
......
63 81
    (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) pp_item_list
64 82
    (Utils.pp_final_char_if_non_empty ";@," pp_item_list)
65 83

  
84

  
85
let pp_ada_with fmt = function
86
  | None -> fprintf fmt ""
87
  | Some (ghost, pres, posts) ->
88
      assert(ghost || (pres != []) || (posts != []));
89
      let contract = pres@posts in
90
      let pp_ghost fmt = if not ghost then fprintf fmt "" else
91
        fprintf fmt " Ghost%t" (Utils.pp_final_char_if_non_empty ",@," contract)
92
      in
93
      let pp_aspect aspect fmt pps = if pps = [] then fprintf fmt "" else
94
        fprintf fmt "%s => %t" aspect (pp_group ~sep:"@,and " pps)
95
      in
96
      let pp_contract fmt = if contract = [] then fprintf fmt "" else
97
        let sep = if pres != [] && posts != [] then ",@," else "" in
98
        fprintf fmt "@,  @[<v>%a%s%a@]"
99
          (pp_aspect "Pre") pres
100
          sep
101
          (pp_aspect "Post") posts
102
      in
103
      fprintf fmt " with%t%t"
104
        pp_ghost
105
        pp_contract
106

  
66 107
(** Print instanciation of a generic type in a new statement.
67 108
   @param fmt the formater to print on
68 109
   @param id id of the polymorphic type
......
78 119
   @param fmt the formater to print on
79 120
   @param id the variable
80 121
**)
81
let pp_var_decl (mode, pp_name, pp_type) fmt =
82
  fprintf fmt "%t: %a%s%t"
122
let pp_var_decl (mode, pp_name, pp_type, with_statement) fmt =
123
  fprintf fmt "%t: %a%s%t%a"
83 124
    pp_name
84 125
    pp_parameter_mode mode
85 126
    (if mode = AdaNoMode then "" else " ")
86 127
    pp_type
128
    pp_ada_with with_statement
87 129

  
88 130
let apply_var_decl_lists var_list =
89 131
  List.map (fun l-> List.map pp_var_decl l) var_list
......
108 150
      fprintf fmt " is %a" pp_visibility visbility
109 151
  | AdaPackageContent pp_package ->
110 152
      fprintf fmt " is@,  @[<v>%t;@]@,end %t" pp_package pp_name
153
  | AdaSimpleContent pp_content ->
154
      fprintf fmt " is@,  @[<v 2>(%t)@]" pp_content
111 155
  | AdaProcedureContent (local_list, pp_instr_list) ->
112 156
      fprintf fmt " is@,%abegin@,%aend %t"
113
        pp_block (List.map (fun l -> pp_group ~sep:";@," (List.map pp_local l)) local_list)
157
        pp_block (List.map (fun l -> pp_group ~sep:";@;" (List.map pp_local l)) local_list)
114 158
        pp_block pp_instr_list
115 159
        pp_name
116 160
  | AdaRecord var_list ->
117 161
      assert(var_list != []);
118 162
      let pp_lists = apply_var_decl_lists var_list in
119 163
      fprintf fmt " is@,  @[<v>record@,  @[<v>%a@]@,end record@]"
120
        pp_block (List.map (pp_group ~sep:";@,") pp_lists)
164
        pp_block (List.map (pp_group ~sep:";@;") pp_lists)
121 165
  | AdaPackageInstanciation (pp_name, instanciations) ->
122 166
      fprintf fmt " is new %t%a"
123 167
        pp_name
124 168
        (pp_args ~sep:",@,") (List.map pp_generic_instanciation instanciations)
125
and pp_def fmt (pp_generics, kind_def, pp_name, args, pp_type_opt, content, pp_spec_opt) =
169
and pp_def fmt (pp_generics, kind_def, pp_name, args, pp_type_opt, content, pp_with_opt) =
126 170
  let pp_arg_lists = apply_var_decl_lists args in
127 171
  fprintf fmt "%a%a %t%a%a%a%a"
128 172
    pp_generic pp_generics
......
131 175
    (pp_args ~sep:";@,") (List.map (pp_group ~sep:";@,") pp_arg_lists)
132 176
    (pp_opt "return") pp_type_opt
133 177
    (pp_content pp_name) content
134
    (pp_opt   "with") pp_spec_opt
178
    pp_ada_with pp_with_opt
135 179
and pp_package_instanciation pp_name pp_base_name fmt instanciations =
136 180
  pp_def fmt ([], AdaPackageDecl, pp_name, [], None, (AdaPackageInstanciation (pp_base_name, instanciations)), None)
137 181

  
......
165 209
let pp_procedure pp_name args pp_with_opt fmt content =
166 210
  pp_def fmt ([], AdaProcedure, pp_name, args, None, content, pp_with_opt)
167 211

  
212
let pp_predicate pp_name args fmt content_opt =
213
  let rec quantify pp_content = function
214
    | [] -> pp_content
215
    | (pp_var, pp_type)::q -> fun fmt ->
216
      fprintf fmt "for some %t in %t => (@,  @[<v>%t@])" pp_var pp_type (quantify pp_content q)
217
  in
218
  let content, with_st = match content_opt with
219
    | Some (locals, booleans) -> AdaSimpleContent (quantify (fun fmt -> Utils.fprintf_list ~sep:"@;and " (fun fmt pp->pp fmt) fmt booleans) locals), None
220
    | None -> AdaNoContent, Some (true, [], [])
221
  in
222
  pp_def fmt ([], AdaFunction, pp_name, args, Some pp_boolean_type, content, with_st)
223

  
168 224

  
169 225

  
170 226

  
......
228 284
let pp_call fmt (pp_name, args) =
229 285
  fprintf fmt "%t%a"
230 286
    pp_name
231
    (pp_args ~sep:",@ ") (List.map (pp_group ~sep:",@ ") args)
287
    (pp_args ~sep:",@ ") (List.map (pp_group ~sep:",@,") args)
232 288

  
233 289

  
234
(*
235

  
236
(** Print a precondition in aspect
290
(** Print the complete name of variable.
291
   @param m the machine to check if it is memory
237 292
   @param fmt the formater to print on
238
   @param expr the expession to print as pre
293
   @param var the variable
239 294
**)
240
let pp_pre fmt expr =
241
  fprintf fmt "Pre => %a"
242
    pp_clean_ada_identifier expr
243

  
244
(** Print a postcondition in aspect
245
   @param fmt the formater to print on
246
   @param expr the expession to print as pre
247
**)
248
let pp_post fmt ident =
249
  fprintf fmt "Post => %a"
250
    pp_clean_ada_identifier ident
251

  
252
(** Print the declaration of a procedure with a contract
253
   @param pp_prototype the prototype printer
254
   @param fmt the formater to print on
255
   @param contract the contract for the function to declare
256
**)
257
let pp_contract guarantees fmt =
258
  fprintf fmt "@,  @[<v>Global => null%t%a@]"
259
    (Utils.pp_final_char_if_non_empty ",@," guarantees)
260
    (Utils.fprintf_list ~sep:",@," pp_post) guarantees
261

  
262
*)
263

  
264

  
265

  
295
let pp_access pp_state pp_var fmt =
296
  fprintf fmt "%t.%t" pp_state pp_var
266 297

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

  

Also available in: Unified diff