Revision 05f85b44
Added by Guillaume DAVY almost 6 years ago
src/backends/Ada/ada_printer.ml | ||
---|---|---|
9 | 9 |
|
10 | 10 |
type printer = Format.formatter -> unit |
11 | 11 |
|
12 |
type ada_with = (bool * (printer list) * (printer list)) option |
|
12 |
type ada_with = (bool * bool * (printer list) * (printer list)) option
|
|
13 | 13 |
|
14 | 14 |
type ada_var_decl = parameter_mode * printer * printer * ada_with |
15 | 15 |
|
... | ... | |
86 | 86 |
|
87 | 87 |
let pp_ada_with fmt = function |
88 | 88 |
| None -> fprintf fmt "" |
89 |
| Some (ghost, pres, posts) -> |
|
90 |
assert(ghost || (pres != []) || (posts != [])); |
|
89 |
| Some (ghost, import, pres, posts) ->
|
|
90 |
assert(ghost || import || (pres != []) || (posts != []));
|
|
91 | 91 |
let contract = pres@posts in |
92 | 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) |
|
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) |
|
94 | 97 |
in |
95 | 98 |
let pp_aspect aspect fmt pps = if pps = [] then fprintf fmt "" else |
96 | 99 |
fprintf fmt "%s => %t" aspect (pp_and pps) |
... | ... | |
102 | 105 |
sep |
103 | 106 |
(pp_aspect "Post") posts |
104 | 107 |
in |
105 |
fprintf fmt " with%t%t" |
|
108 |
fprintf fmt " with%t%t%t"
|
|
106 | 109 |
pp_ghost |
110 |
pp_import |
|
107 | 111 |
pp_contract |
108 | 112 |
|
109 | 113 |
(** Print instanciation of a generic type in a new statement. |
... | ... | |
218 | 222 |
let pp_procedure pp_name args pp_with_opt fmt content = |
219 | 223 |
pp_def fmt ([], AdaProcedure, pp_name, args, None, content, pp_with_opt) |
220 | 224 |
|
221 |
let pp_predicate pp_name args fmt content_opt = |
|
225 |
let pp_predicate pp_name args imported fmt content_opt =
|
|
222 | 226 |
let content, with_st = match content_opt with |
223 | 227 |
| Some content -> AdaSimpleContent content, None |
224 |
| None -> AdaNoContent, Some (true, [], []) |
|
228 |
| None -> AdaNoContent, Some (true, imported, [], [])
|
|
225 | 229 |
in |
226 | 230 |
pp_def fmt ([], AdaFunction, pp_name, args, Some pp_boolean_type, content, with_st) |
227 | 231 |
|
Also available in: Unified diff
Ada: Start cleaning Ada to prepare for why beckend