Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_ads.ml @ 173a2a8f

History | View | Annotate | Download (16.1 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Format
13

    
14
open Machine_code_types
15
open Lustre_types
16
open Corelang
17
open Machine_code_common
18

    
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
22
open Ada_backend_common
23

    
24

    
25

    
26
(** Functions printing the .ads file **)
27
module Main =
28
struct
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*)
31

    
32
  let suffixOld = "_old"
33
  let suffixNew = "_new"
34
  let pp_invariant_name fmt = fprintf fmt "invariant"
35
  let pp_transition_name fmt = fprintf fmt "transition"
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"
40

    
41

    
42

    
43
  (** Printing function for basic assignement [var := value].
44

    
45
      @param fmt the formater to print on
46
      @param var_name the name of the variable
47
      @param value the value to be assigned
48
   **)
49
  let pp_local_eq env fmt var value =
50
    fprintf fmt "%t = %a"
51
      (pp_var_name var)
52
      (pp_value env) value
53

    
54
  (** Printing function for basic assignement [var := value].
55

    
56
      @param fmt the formater to print on
57
      @param var_name the name of the variable
58
      @param value the value to be assigned
59
   **)
60
  let pp_state_eq env fmt var value =
61
    fprintf fmt "%t = %a"
62
      (pp_access (pp_state_name_predicate suffixNew) (pp_var_name var))
63
      (pp_value env) value
64

    
65
  (** Printing function for instruction. See
66
      {!type:Machine_code_types.instr_t} for more details on
67
      machine types.
68

    
69
      @param typed_submachines list of all typed machine instances of this machine
70
      @param machine the current machine
71
      @param fmt the formater to print on
72
      @param instr the instruction to print
73
   **)
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

    
122

    
123

    
124

    
125

    
126

    
127

    
128

    
129

    
130

    
131

    
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
144

    
145

    
146

    
147

    
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

    
162

    
163

    
164
  (** Print the expression function representing the transition predicate.
165
     @param fmt the formater to print on
166
     @param machine the machine
167
  **)
168
  let pp_transition_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
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
172
    let inputs = build_pp_var_decl_step_input AdaIn None m in
173
    let outputs = build_pp_var_decl_step_output AdaIn None m in
174
    let instrs = push_if_in_expr m.mstep.step_instrs in
175
    let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in
176
    let locals = List.map (fun x-> (pp_var_name x, fun fmt -> pp_var_type fmt x)) m.mstep.step_locals in
177
    pp_predicate_special pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content))
178

    
179
  let build_pp_past mode with_st i = (mode, pp_past_name (i+1), pp_state_type , with_st)
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
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
220

    
221

    
222

    
223

    
224
  (** Print a new statement instantiating a generic package.
225
     @param fmt the formater to print on
226
     @param substitutions the instanciation substitution
227
     @param machine the machine to instanciate
228
  **)
229
  let pp_new_package fmt (substitutions, machine) =
230
    let pp_name = pp_package_name machine in
231
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine 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
233
    pp_package_instanciation pp_new_name pp_name fmt instanciations
234

    
235
  (** Remove duplicates from a list according to a given predicate.
236
     @param eq the predicate defining equality
237
     @param l the list to parse
238
  **)
239
  let remove_duplicates eq l =
240
    let aux l x = if List.exists (eq x) l then l else x::l in
241
    List.fold_left aux [] l
242

    
243

    
244
  (** Compare two typed machines.
245
  **)
246
  let eq_typed_machine (subst1, machine1) (subst2, machine2) =
247
    (String.equal machine1.mname.node_id machine2.mname.node_id) &&
248
    (List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
249

    
250

    
251
  (** Print the package declaration(ads) of a machine.
252
    It requires the list of all typed instance.
253
    A typed submachine is a (ident, typed_machine) with
254
      - ident: the name 
255
      - typed_machine: a (substitution, machine) with
256
        - machine: the submachine struct
257
        - substitution the instanciation of all its polymorphic types.
258
     @param fmt the formater to print on
259
     @param typed_submachines list of all typed submachines of this machine
260
     @param m the machine
261
  **)
262
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees, past_size), m)) =
263
    let typed_machines = snd (List.split typed_submachines) in
264
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
265
    
266
    let machines_to_import = List.map pp_package_name (snd (List.split typed_machines_set)) in
267

    
268
    let polymorphic_types = find_all_polymorphic_type m in
269
    
270
    let typed_machines_to_instanciate =
271
      (*List.filter (fun (l, _) -> l != [])*) typed_machines_set in
272

    
273
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
274

    
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
278
    in
279
    let ghost_private = memories in
280
    
281
    let vars_spec = match m_spec_opt with
282
      | None -> []
283
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, [], []))) (m_spec.mmemory)
284
    in
285
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
286
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
287
    let var_lists =
288
      (if states = [] then [] else [states]) @
289
      (if vars = [] then [] else [vars]) in
290
    
291
    let pp_ifstatefull fmt pp =
292
      if is_machine_statefull m then
293
        fprintf fmt "%t" pp
294
      else
295
        fprintf fmt ""
296
    in
297

    
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"
311
      (*Instantiate the polymorphic type that need to be instantiated*)
312
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
313
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
314
      
315
      (*Define the state type*)
316
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
317
        
318
      (*Declare the init predicate*)
319
      (pp_init_predicate false typed_submachines) (m_spec_opt, m)
320
        
321
      (*Declare the transition predicate*)
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
329
    in
330

    
331
    let pp_content fmt =
332
      let pp_contract_opt =
333
        let pp_var x fmt =
334
            pp_clean_ada_identifier fmt x
335
        in
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
            [], []
356
        in
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)
363
      in
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
        
372
        pp_ifstatefull pp_state_decl_and_reset
373
        
374
        (*Declare the step procedure*)
375
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
376
        
377
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
378
        
379
        (*Declare the init predicate*)
380
        (pp_init_predicate true typed_submachines) (m_spec_opt, m)
381
        
382
        (*Declare the transition predicate*)
383
        (pp_transition_predicate true typed_submachines) (m_spec_opt, m)
384
        
385
        (*Declare the transition predicate*)
386
        (pp_invariant_predicate true typed_submachines) (past_size, m_spec_opt, m)
387
        
388
        (*Print the private section*)
389
        pp_private_section
390
    in
391
    
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
394
    
395
    fprintf fmt "@[<v>%a%t%a;@]@."
396
      
397
      (* Include all the subinstance package*)
398
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
399
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
400
      
401
      (*Begin the package*)
402
      (pp_package (pp_package_name m) pp_generics false) pp_content
403

    
404
end