Project

General

Profile

« Previous | Next » 

Revision 05f85b44

Added by Guillaume DAVY almost 6 years ago

Ada: Start cleaning Ada to prepare for why beckend

View differences:

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