Project

General

Profile

Revision 173a2a8f

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