Project

General

Profile

Revision 173a2a8f src/backends/Ada/ada_printer.ml

View differences:

src/backends/Ada/ada_printer.ml
81 81
    (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) pp_item_list
82 82
    (Utils.pp_final_char_if_non_empty ";@," pp_item_list)
83 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)
84 86

  
85 87
let pp_ada_with fmt = function
86 88
  | None -> fprintf fmt ""
......
91 93
        fprintf fmt " Ghost%t" (Utils.pp_final_char_if_non_empty ",@," contract)
92 94
      in
93 95
      let pp_aspect aspect fmt pps = if pps = [] then fprintf fmt "" else
94
        fprintf fmt "%s => %t" aspect (pp_group ~sep:"@,and " pps)
96
        fprintf fmt "%s => %t" aspect (pp_and pps)
95 97
      in
96 98
      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
        let sep fmt = if pres != [] && posts != [] then fprintf fmt ",@," else fprintf fmt "" in
100
        fprintf fmt "@,  @[<v>%a%t%a@]"
99 101
          (pp_aspect "Pre") pres
100 102
          sep
101 103
          (pp_aspect "Post") posts
......
179 181
and pp_package_instanciation pp_name pp_base_name fmt instanciations =
180 182
  pp_def fmt ([], AdaPackageDecl, pp_name, [], None, (AdaPackageInstanciation (pp_base_name, instanciations)), None)
181 183

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

  
182 187
(** Print the ada package introduction sentence it can be used for body and
183 188
declaration. Boolean parameter body should be true if it is a body delcaration.
184 189
   @param fmt the formater to print on
......
201 206
   @param pp_value a format printer which print the type definition
202 207
**)
203 208
let pp_type_decl pp_name visibility fmt =
204
  pp_def fmt ([], AdaType, pp_name, [], None, AdaVisibilityDefinition visibility, None)
209
  let v = match visibility with
210
    | AdaNoVisibility -> AdaNoContent
211
    | _ -> AdaVisibilityDefinition visibility
212
  in
213
  pp_def fmt ([], AdaType, pp_name, [], None, v, None)
205 214

  
206 215
let pp_record pp_name fmt var_lists =
207 216
  pp_def fmt ([], AdaType, pp_name, [], None, AdaRecord var_lists, None)
......
210 219
  pp_def fmt ([], AdaProcedure, pp_name, args, None, content, pp_with_opt)
211 220

  
212 221
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 222
  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
223
    | Some content -> AdaSimpleContent content, None
220 224
    | None -> AdaNoContent, Some (true, [], [])
221 225
  in
222 226
  pp_def fmt ([], AdaFunction, pp_name, args, Some pp_boolean_type, content, with_st)
223 227

  
224

  
225

  
226

  
227 228
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
228 229
    underscore and must not contain a double underscore
229 230
   @param var name to be cleaned*)

Also available in: Unified diff