Project

General

Profile

« Previous | Next » 

Revision 173a2a8f

Added by Guillaume DAVY almost 3 years ago

Ada: Lot of specification is exported in Ada. We use ghost code to store all states,
we generate the transition pridicate but also the invariant. But two problems, occured.
The first one is a visibility problem for the record which is private but must be
public for ghost variable which have to be public for specifaction. The second
problem is that the approache requires existential quantification for inputs and
locals. It works for integers and boolean but not for floats. Some complex
solution could be found like writing an iterator for floats, expanding all
local variable and store all the required inputs in ghost variable.

View differences:

src/backends/Ada/ada_backend.ml
112 112
            | [] -> None
113 113
            | _ -> Some machine_spec
114 114
        in
115
        None, [] (*(opt_machine_spec, guarantees)*)
115
        (opt_machine_spec, guarantees, 4)
116 116
      end
117
    | _ -> None, []
117
    | _ -> None, [], 0
118 118

  
119 119
(** Main function of the Ada backend. It calls all the subfunction creating all
120 120
the file and fill them with Ada code representing the machines list given.
src/backends/Ada/ada_backend_adb.ml
124 124
     @param fmt the formater to print on
125 125
     @param machine the machine
126 126
  **)
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt) =
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
128 128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129 129
      | MLocalAssign (ident, value) -> 
130 130
          { instr_desc = MStateAssign (ident, value);
131 131
            lustre_eq= instr.lustre_eq }
132 132
      | x -> instr
133 133
    in
134
    let spec_instrs = match m_spec_opt with
135
      | None -> []
136
      | Some m_spec -> List.map transform_local_to_state_assign m_spec.mstep.step_instrs
134
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
135
      | None -> [], []
136
      | Some m_spec ->
137
          List.map (build_pp_var_decl_local (Some (true, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
138
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
137 139
    in
138 140
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
139 141
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
140
    let content = AdaProcedureContent ((if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
142
    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
141 143
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
142 144

  
143 145
  (** Print the definition of the reset procedure from a machine.
......
146 148
     @param fmt the formater to print on
147 149
     @param machine the machine
148 150
  **)
149
  let pp_reset_definition env typed_submachines fmt m =
151
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
150 152
    let build_assign = function var ->
151 153
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
152 154
    in
153
    let assigns = List.map build_assign m.mmemory in
155
    let env, memory = match m_spec_opt with
156
      | None -> env, m.mmemory
157
      | Some m_spec ->
158
          env,
159
          (m.mmemory)
160
    in
161
    let assigns = List.map build_assign memory in
154 162
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
155 163
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
156 164

  
......
164 172
     @param typed_submachines list of all typed machine instances of this machine
165 173
     @param m the machine
166 174
  **)
167
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
175
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees, past_size), machine)) =
168 176
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
169 177
    let pp_reset fmt =
170 178
      if is_machine_statefull machine then
171
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) machine
179
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
172 180
      else
173 181
        fprintf fmt ""
174 182
    in
......
188 196
        pp_reset
189 197
        
190 198
        (*Define the step procedure*)
191
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine)
199
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
192 200
    in
193 201
    fprintf fmt "%a%t%a;@."
194 202
      
195 203
      (* Include all the required packages*)
196
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) packages
204
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
197 205
      (Utils.pp_final_char_if_non_empty ";@,@," packages)
198 206
      
199 207
      (*Print package*)
src/backends/Ada/ada_backend_ads.ml
21 21
open Ada_printer
22 22
open Ada_backend_common
23 23

  
24

  
25

  
24 26
(** Functions printing the .ads file **)
25 27
module Main =
26 28
struct
27 29

  
30
  let rec init f = function i when i < 0 -> [] | i -> (f i)::(init f (i-1)) (*should be replaced by the init of list from ocaml std lib*)
28 31

  
29 32
  let suffixOld = "_old"
30 33
  let suffixNew = "_new"
34
  let pp_invariant_name fmt = fprintf fmt "invariant"
31 35
  let pp_transition_name fmt = fprintf fmt "transition"
32
  let pp_state_name_transition suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
33

  
36
  let pp_init_name fmt = fprintf fmt "init"
37
  let pp_state_name_predicate suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
38
  let pp_name_generic fmt = fprintf fmt "name"
39
  let pp_type_generic fmt = fprintf fmt "string"
34 40

  
35 41

  
36 42

  
......
53 59
   **)
54 60
  let pp_state_eq env fmt var value =
55 61
    fprintf fmt "%t = %a"
56
      (pp_access (pp_state_name_transition suffixNew) (pp_var_name var))
62
      (pp_access (pp_state_name_predicate suffixNew) (pp_var_name var))
57 63
      (pp_value env) value
58 64

  
59 65
  (** Printing function for instruction. See
......
65 71
      @param fmt the formater to print on
66 72
      @param instr the instruction to print
67 73
   **)
68
  let rec pp_machine_instr typed_submachines env instr fmt =
69
    let pp_instr = pp_machine_instr typed_submachines env in
70
    let pp_state suffix i fmt = fprintf fmt "%t.%s" (pp_state_name_transition suffix) i in
71
    match get_instr_desc instr with
72
      (* no reset *)
73
      | MNoReset _ -> ()
74
      (* reset  *)
75
      | MReset i when List.mem_assoc i typed_submachines ->
76
          let (substitution, submachine) = get_instance i typed_submachines in
77
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
78
          let args = if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [] in
79
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
80
      | MLocalAssign (ident, value) ->
81
          pp_local_eq env fmt ident value
82
      | MStateAssign (ident, value) ->
83
          pp_state_eq env fmt ident value
84
      | MStep ([i0], i, vl) when is_builtin_fun i ->
85
          let value = mk_val (Fun (i, vl)) i0.var_type in
86
          if List.mem_assoc i0.var_id env then
87
            pp_state_eq env fmt i0 value
88
          else
89
            pp_local_eq env fmt i0 value
90
          
91
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
92
          let (substitution, submachine) = get_instance i typed_submachines in
93
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
94
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
95
          let output = List.map pp_var_name il in
96
          let args =
97
            (if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [])
98
              @(if input!=[] then [input] else [])
99
              @(if output!=[] then [output] else [])
100
          in
101
          fprintf fmt "(%a)" pp_call (pp_package_access (pp_package, pp_transition_name), args)
102
      | MComment s -> ()
103
      | _ -> assert false
74
  let pp_machine_instr typed_submachines env (pps, assigned) instr =
75
    let pp_state suffix i fmt = fprintf fmt "%t.%s" (pp_state_name_predicate suffix) i in
76
    let fresh x l = not (List.exists (fun y -> String.equal x.var_id y.var_id) l) in
77
    let pp, newvals =
78
      match get_instr_desc instr with
79
        (* no reset *)
80
        | MNoReset _ -> ((fun fmt -> ()), [])
81
        (* reset  *)
82
        | MReset i when List.mem_assoc i typed_submachines ->
83
            let (substitution, submachine) = get_instance i typed_submachines in
84
            let pp_package = pp_package_name_with_polymorphic substitution submachine in
85
            let args = if is_machine_statefull submachine then [[pp_state suffixNew i]] else [] in
86
            ((fun fmt -> pp_call fmt (pp_package_access (pp_package, pp_init_name), args)),
87
            [])
88
        | MLocalAssign (ident, value) ->
89
            assert(fresh ident assigned);
90
            ((fun fmt -> pp_local_eq env fmt ident value),
91
            [ident])
92
        | MStateAssign (ident, value) ->
93
            assert(fresh ident assigned);
94
            ((fun fmt -> pp_state_eq env fmt ident value),
95
            [ident])
96
        | MStep ([i0], i, vl) when is_builtin_fun i ->
97
            assert(fresh i0 assigned);
98
            let value = mk_val (Fun (i, vl)) i0.var_type in
99
            ((fun fmt -> (if List.mem_assoc i0.var_id env then
100
              pp_state_eq env fmt i0 value
101
            else
102
              pp_local_eq env fmt i0 value)),
103
            [i0])
104
        | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
105
            assert(List.for_all (fun x -> fresh x assigned) il);
106
            let (substitution, submachine) = get_instance i typed_submachines in
107
            let pp_package = pp_package_name_with_polymorphic substitution submachine in
108
            let input = List.map (fun x fmt -> pp_value env fmt x) vl in
109
            let output = List.map pp_var_name il in
110
            let args =
111
              (if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [])
112
                @(if input!=[] then [input] else [])
113
                @(if output!=[] then [output] else [])
114
            in
115
            ((fun fmt -> fprintf fmt "(%a)" pp_call (pp_package_access (pp_package, pp_transition_name), args)),
116
            il)
117
        | MComment s -> ((fun fmt -> ()), [])
118
        | _ -> assert false
119
      in
120
      (pp::pps, newvals@assigned)
121

  
104 122

  
105 123

  
106 124

  
......
112 130

  
113 131

  
114 132

  
133
let pp_predicate_special pp_name args fmt content_opt =
134
  let rec quantify pp_content = function
135
    | [] -> pp_content
136
    | (pp_var, pp_type)::q -> fun fmt ->
137
      fprintf fmt "for some %t in %t => (@,  @[<v>%t@])" pp_var pp_type (quantify pp_content q)
138
  in
139
  let content = match content_opt with
140
    | Some (locals, booleans) -> Some (quantify (fun fmt -> Utils.fprintf_list ~sep:"@,and " (fun fmt pp->pp fmt) fmt booleans) locals)
141
    | None -> None
142
  in
143
  pp_predicate pp_name args fmt content
115 144

  
116 145

  
117 146

  
118 147

  
119 148

  
149
  (** Print the expression function representing the transition predicate.
150
     @param fmt the formater to print on
151
     @param machine the machine
152
  **)
153
  let pp_init_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
154
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
155
    let env = [] in
156
    let instrs = push_if_in_expr m.minit in
157
    let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in
158
    pp_predicate_special pp_init_name ([[new_state]]) fmt (if prototype then None else Some ([], content))
159
    
160

  
161

  
120 162

  
121 163

  
122 164
  (** Print the expression function representing the transition predicate.
......
124 166
     @param machine the machine
125 167
  **)
126 168
  let pp_transition_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
127
    let old_state = (AdaIn, pp_state_name_transition suffixOld, pp_state_type, None) in
128
    let new_state = (AdaIn, pp_state_name_transition suffixNew, pp_state_type, None) in
129
    let env = List.map (fun x -> x.var_id, pp_state_name_transition suffixOld) m.mmemory in
169
    let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in
170
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
171
    let env = List.map (fun x -> x.var_id, pp_state_name_predicate suffixOld) m.mmemory in
130 172
    let inputs = build_pp_var_decl_step_input AdaIn None m in
131 173
    let outputs = build_pp_var_decl_step_output AdaIn None m in
132 174
    let instrs = push_if_in_expr m.mstep.step_instrs in
133
    let content = List.map (pp_machine_instr typed_submachines env) instrs in
175
    let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in
134 176
    let locals = List.map (fun x-> (pp_var_name x, fun fmt -> pp_var_type fmt x)) m.mstep.step_locals in
135
    pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content))
136
    
137

  
138

  
139

  
140

  
141

  
177
    pp_predicate_special pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content))
142 178

  
179
  let build_pp_past mode with_st i = (mode, pp_past_name (i+1), pp_state_type , with_st)
143 180

  
181
  let pp_invariant_predicate prototype typed_submachines fmt (past_size, opt_spec_machine, m) =
182
    let pp_state nbr = if nbr = 0 then pp_state_name else pp_past_name nbr in
183
    if past_size < 1 then fprintf fmt "" else
184
    begin
185
      let pp_var x fmt =
186
          pp_clean_ada_identifier fmt x
187
      in
188
      let input = List.map pp_var_name m.mstep.step_inputs in
189
      let output = List.map pp_var_name m.mstep.step_outputs in
190
      let args =
191
        [[pp_old pp_state_name;pp_state_name]]
192
          @(if input!=[] then [input] else [])
193
          @(if output!=[] then [output] else [])
194
      in
195
      let transition fmt = pp_call fmt (pp_transition_name, args) in
144 196

  
197
      let pp_append_nbr pp nbr fmt = fprintf fmt "%t_%i" pp nbr in
198
      let pp_transition nbr fmt =
199
        assert(is_machine_statefull m);
200
        let args =
201
          [[pp_past_name (nbr+1);pp_state nbr]]
202
            @(if input!=[] then [input] else [])
203
            @(if output!=[] then [output] else [])
204
        in
205
        pp_call fmt (pp_transition_name, args)
206
      in
207
      let build_chain nbr =
208
        assert (nbr > 0);
209
        pp_and (init pp_transition nbr)
210
      in
211
      let pp_init nbr fmt = pp_call fmt (pp_init_name, [[pp_state nbr]]) in
212
      let rec build_initial nbr = pp_and (match nbr with
213
        | 0 -> [pp_init 0]
214
        | i when i > 0 -> [pp_init i;build_chain i]
215
        | _ -> assert false)
216
      in
217
      let content = pp_or ((build_chain (past_size-1))::(init build_initial (past_size-1))) in
218
      fprintf fmt ";@,@,%a" (pp_predicate pp_invariant_name [init (build_pp_past AdaIn None) (past_size-1);[build_pp_state_decl AdaIn None]]) (if prototype then None else Some content)
219
    end
145 220

  
146 221

  
147 222

  
......
154 229
  let pp_new_package fmt (substitutions, machine) =
155 230
    let pp_name = pp_package_name machine in
156 231
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
157
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
232
    let instanciations = ((pp_name_generic, pp_adastring pp_name))::(List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions) in
158 233
    pp_package_instanciation pp_new_name pp_name fmt instanciations
159 234

  
160 235
  (** Remove duplicates from a list according to a given predicate.
......
184 259
     @param typed_submachines list of all typed submachines of this machine
185 260
     @param m the machine
186 261
  **)
187
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
262
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees, past_size), m)) =
188 263
    let typed_machines = snd (List.split typed_submachines) in
189 264
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
190 265
    
......
193 268
    let polymorphic_types = find_all_polymorphic_type m in
194 269
    
195 270
    let typed_machines_to_instanciate =
196
      List.filter (fun (l, _) -> l != []) typed_machines_set in
271
      (*List.filter (fun (l, _) -> l != [])*) typed_machines_set in
197 272

  
198 273
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
199 274

  
200
    let pp_state_decl_and_reset fmt = fprintf fmt "%t;@,@,%a;@,@,"
201
      (*Declare the state type*)
202
      (pp_type_decl pp_state_type AdaPrivate)
203
      (*Declare the reset procedure*)
204
      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None) AdaNoContent
275
    let memories = match m_spec_opt with
276
      | None -> []
277
      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, [], [])) x)) m.mmemory
205 278
    in
279
    let ghost_private = memories in
206 280
    
207 281
    let vars_spec = match m_spec_opt with
208 282
      | None -> []
209
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode None) m_spec.mstep.step_locals
283
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, [], []))) (m_spec.mmemory)
210 284
    in
211 285
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
212 286
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
213 287
    let var_lists =
214 288
      (if states = [] then [] else [states]) @
215
      (if vars = [] then [] else [vars])@
216
      (if vars_spec = [] then [] else [vars_spec]) in
289
      (if vars = [] then [] else [vars]) in
217 290
    
218 291
    let pp_ifstatefull fmt pp =
219 292
      if is_machine_statefull m then
......
222 295
        fprintf fmt ""
223 296
    in
224 297

  
225
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,@,%a"
298
    let pp_state_decl_and_reset fmt =
299
      let init fmt = pp_call fmt (pp_init_name, [[pp_state_name]]) in
300
      let contract = Some (false, [], [init]) in
301
      fprintf fmt "%t;@,@,%a;@,@,"
302
        (*Declare the state type*)
303
        (pp_type_decl pp_state_type AdaPrivate)
304
        
305
        (*Declare the reset procedure*)
306
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract) AdaNoContent
307
    in
308

  
309
    let pp_private_section fmt =
310
      fprintf fmt "@,private@,@,%a%t%a;@,@,%a;@,@,%a%a%t%a"
226 311
      (*Instantiate the polymorphic type that need to be instantiated*)
227 312
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
228 313
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
314
      
229 315
      (*Define the state type*)
230 316
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
231 317
        
318
      (*Declare the init predicate*)
319
      (pp_init_predicate false typed_submachines) (m_spec_opt, m)
320
        
232 321
      (*Declare the transition predicate*)
233 322
      (pp_transition_predicate false typed_submachines) (m_spec_opt, m)
323
        
324
      (*Declare the transition predicate*)
325
      (pp_invariant_predicate false typed_submachines) (past_size, m_spec_opt, m)
326
        
327
      (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
328
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private
234 329
    in
235 330

  
236 331
    let pp_content fmt =
237 332
      let pp_contract_opt =
238
        let ghost_memory = match m_spec_opt with
239
          | None -> []
240
          | Some m_spec -> m_spec.mstep.step_locals
241
        in
242 333
        let pp_var x fmt =
243
          if List.exists (fun var -> var.var_id == x) ghost_memory then
244
            pp_access pp_state_name (fun fmt -> pp_clean_ada_identifier fmt x) fmt
245
          else
246 334
            pp_clean_ada_identifier fmt x
247 335
        in
248
        let input = List.map pp_var_name m.mstep.step_inputs in
249
        let output = List.map pp_var_name m.mstep.step_outputs in
250
        let args =
251
          (if is_machine_statefull m then [[pp_old pp_state_name;pp_state_name]] else [])
252
            @(if input!=[] then [input] else [])
253
            @(if output!=[] then [output] else [])
336
        let guarantee_post_conditions = List.map pp_var guarantees in
337
        let state_pre_conditions, state_post_conditions =
338
          if is_machine_statefull m then
339
          begin
340
            let input = List.map pp_var_name m.mstep.step_inputs in
341
            let output = List.map pp_var_name m.mstep.step_outputs in
342
            let args =
343
              [[pp_old pp_state_name;pp_state_name]]
344
                @(if input!=[] then [input] else [])
345
                @(if output!=[] then [output] else [])
346
            in
347
            let transition fmt = pp_call fmt (pp_transition_name, args) in
348
            let invariant fmt = pp_call fmt (pp_invariant_name, [init (fun i->pp_past_name (i+1)) (past_size-1);[pp_state_name]]) in
349
            if past_size > 0 then
350
              [invariant], [transition;invariant]
351
            else
352
              [], [transition]
353
          end
354
          else
355
            [], []
254 356
        in
255
        let transition fmt = pp_call fmt (pp_transition_name, args) in
256
        match guarantees with
257
          | [] -> Some (false, [], [transition])
258
          | _ ->  Some (false, [], transition::(List.map pp_var guarantees))
357
        let post_conditions = state_post_conditions@guarantee_post_conditions in
358
        let pre_conditions = state_pre_conditions in
359
        if post_conditions = [] && pre_conditions = [] then
360
          None
361
        else
362
          Some (false, pre_conditions, post_conditions)
259 363
      in
260
      fprintf fmt "%a%a%a@,@,%a;%t" (* %a;@, *)
364
      let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, [], []))) in
365
      let pasts = List.map pp_var_decl (init (build_pp_past AdaNoMode (Some (true, [], []))) (past_size-1)) in
366
      let ghost_public = pasts@(List.map pp_guarantee guarantees) in
367
      fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%a%a;%t"
368
        
369
        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_public
370
        (Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
371
        
261 372
        pp_ifstatefull pp_state_decl_and_reset
262 373
        
263 374
        (*Declare the step procedure*)
......
265 376
        
266 377
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
267 378
        
379
        (*Declare the init predicate*)
380
        (pp_init_predicate true typed_submachines) (m_spec_opt, m)
381
        
268 382
        (*Declare the transition predicate*)
269 383
        (pp_transition_predicate true typed_submachines) (m_spec_opt, m)
270 384
        
385
        (*Declare the transition predicate*)
386
        (pp_invariant_predicate true typed_submachines) (past_size, m_spec_opt, m)
387
        
271 388
        (*Print the private section*)
272 389
        pp_private_section
273 390
    in
274 391
    
275
    let pp_poly_types id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
276
    let pp_generics = List.map pp_poly_types polymorphic_types in
392
    let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
393
    let pp_generics = (pp_var_decl (AdaNoMode, pp_name_generic, pp_type_generic , None))::(List.map pp_poly_type polymorphic_types) in
277 394
    
278 395
    fprintf fmt "@[<v>%a%t%a;@]@."
279 396
      
280 397
      (* Include all the subinstance package*)
281
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) machines_to_import
398
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
282 399
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
283 400
      
284 401
      (*Begin the package*)
src/backends/Ada/ada_backend_common.ml
42 42
**)
43 43
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
44 44

  
45
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
46

  
45 47

  
46 48

  
47 49

  
......
153 155
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
154 156
            polymorphic_types substituion);
155 157
  let instantiated_types = snd (List.split substitution) in
156
  fprintf fmt "%t%t%a"
158
  fprintf fmt "%t_inst%t%a"
157 159
    (pp_package_name machine)
158 160
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
159 161
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
src/backends/Ada/ada_backend_common.mli
13 13
val pp_step_procedure_name : printer
14 14
val pp_main_procedure_name : printer
15 15
val pp_polymorphic_type : int -> printer
16
val pp_past_name : int -> printer
16 17

  
17 18
val is_builtin_fun : string -> bool
18 19
val ada_supported_funs : (string*(string*string)) list
......
35 36
val build_pp_arg_step : machine_t -> (ada_var_decl list list)
36 37
val build_pp_arg_reset : machine_t -> (ada_var_decl list list)
37 38
val build_pp_state_decl_from_subinstance : parameter_mode -> ada_with -> (string * ((int * Types.type_expr) list * Machine_code_types.machine_t)) -> ada_var_decl
39
val build_pp_state_decl : parameter_mode -> ada_with -> ada_var_decl
38 40

  
39 41
val pp_machine_filename : string -> formatter -> machine_t -> unit
40 42
val pp_main_filename : formatter -> machine_t -> unit
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*)
src/backends/Ada/ada_printer.mli
37 37
val pp_access :  printer -> printer -> formatter -> unit
38 38
val pp_call : formatter -> (printer*(printer list list)) -> unit
39 39
val pp_old : printer -> printer
40
val pp_adastring : printer -> printer
41

  
42
val pp_or : (printer list) -> printer
43
val pp_and : (printer list) -> printer
40 44

  
41 45
(* declaration printer *)
42 46
val pp_package : printer -> printer list -> bool -> formatter -> printer -> unit
......
44 48
val pp_type_decl : printer -> visibility -> printer
45 49
val pp_record : printer -> formatter -> ada_var_decl list list -> unit
46 50
val pp_procedure : printer -> (ada_var_decl list list) -> ada_with -> formatter -> def_content -> unit
47
val pp_predicate : printer -> (ada_var_decl list list) -> formatter -> ((((printer*printer) list)*(printer list)) option) -> unit
48

  
51
val pp_predicate : printer -> (ada_var_decl list list) -> formatter -> (printer option) -> unit
49 52
(* Local function :
50 53

  
51 54
val pp_parameter_mode : formatter -> parameter_mode -> unit
src/backends/Ada/misc_lustre_function.ml
271 271
              }
272 272
            in
273 273
            let mkval_var id = {
274
                              value_desc   = Var id;
275
                              value_type   = id.var_type;
276
                              value_annot  = None
277
                            }
274
              value_desc   = Var id;
275
              value_type   = id.var_type;
276
              value_annot  = None
277
            }
278 278
            in
279 279
            let rec find_split s1 id1 accu = function
280 280
              | [] -> [], accu, mkval_var id1

Also available in: Unified diff