Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_ads.ml @ c2db420f

History | View | Annotate | Download (9.56 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 "inv"
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_axiomatize_package_name fmt = fprintf  fmt "axiomatize"
39

    
40
  (** Print the expression function representing the transition predicate.
41
     @param fmt the formater to print on
42
     @param machine the machine
43
  **)
44
  let pp_init_predicate typed_submachines fmt (opt_spec_machine, m) =
45
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
46
    pp_predicate pp_init_name [[new_state]] true fmt None
47

    
48
  (** Print the expression function representing the transition predicate.
49
     @param fmt the formater to print on
50
     @param machine the machine
51
  **)
52
  let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
53
    let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in
54
    let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
55
    let inputs = build_pp_var_decl_step_input AdaIn None m in
56
    let outputs = build_pp_var_decl_step_output AdaIn None m in
57
    pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) true fmt None
58

    
59
  let pp_invariant_predicate typed_submachines fmt (opt_spec_machine, m) =
60
    pp_predicate pp_invariant_name [[build_pp_state_decl AdaIn None]] true fmt None
61

    
62
  (** Print a new statement instantiating a generic package.
63
     @param fmt the formater to print on
64
     @param substitutions the instanciation substitution
65
     @param machine the machine to instanciate
66
  **)
67
  let pp_new_package fmt (substitutions, machine) =
68
    let pp_name = pp_package_name machine in
69
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
70
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
71
    pp_package_instanciation pp_new_name pp_name fmt instanciations
72

    
73
  (** Remove duplicates from a list according to a given predicate.
74
     @param eq the predicate defining equality
75
     @param l the list to parse
76
  **)
77
  let remove_duplicates eq l =
78
    let aux l x = if List.exists (eq x) l then l else x::l in
79
    List.fold_left aux [] l
80

    
81

    
82
  (** Compare two typed machines.
83
  **)
84
  let eq_typed_machine (subst1, machine1) (subst2, machine2) =
85
    (String.equal machine1.mname.node_id machine2.mname.node_id) &&
86
    (List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
87

    
88

    
89
  (** Print the package declaration(ads) of a machine.
90
    It requires the list of all typed instance.
91
    A typed submachine is a (ident, typed_machine) with
92
      - ident: the name 
93
      - typed_machine: a (substitution, machine) with
94
        - machine: the submachine struct
95
        - substitution the instanciation of all its polymorphic types.
96
     @param fmt the formater to print on
97
     @param typed_submachines list of all typed submachines of this machine
98
     @param m the machine
99
  **)
100
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
101
    let typed_machines = snd (List.split typed_submachines) in
102
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
103
    
104
    let machines_to_import = List.map pp_package_name (snd (List.split typed_machines_set)) in
105

    
106
    let polymorphic_types = find_all_polymorphic_type m in
107
    
108
    let typed_machines_to_instanciate =
109
      List.filter (fun (l, _) -> l != []) typed_machines_set in
110

    
111
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
112

    
113
    let memories = match m_spec_opt with
114
      | None -> []
115
      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x)) m.mmemory
116
    in
117
    let ghost_private = memories in
118
    (* Commented since not used. Could be reinjected in the code 
119
    let vars_spec = match m_spec_opt with
120
      | None -> []
121
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, false, [], []))) (m_spec.mmemory)
122
    in *)
123
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
124
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
125
    let var_lists =
126
      (if states = [] then [] else [states]) @
127
      (if vars = [] then [] else [vars]) in
128
    
129
    let pp_ifstatefull fmt pp =
130
      if is_machine_statefull m then
131
        fprintf fmt "%t" pp
132
      else
133
        fprintf fmt ""
134
    in
135

    
136
    let pp_state_decl_and_reset fmt =
137
      let init fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_init_name, [[pp_state_name]]) in
138
      let contract = Some (false, false, [], [init]) in
139
      fprintf fmt "%t;@,@,%a;@,@,"
140
        (*Declare the state type*)
141
        (pp_type_decl pp_state_type AdaPrivate)
142
        
143
        (*Declare the reset procedure*)
144
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract) AdaNoContent
145
    in
146

    
147
    let pp_private_section fmt =
148
      fprintf fmt "@,private@,@,%a%t%a%t%a"
149
      (*Instantiate the polymorphic type that need to be instantiated*)
150
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
151
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
152
      
153
      (*Define the state type*)
154
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
155
        
156
      (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
157
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private
158
    in
159

    
160
    let pp_content fmt =
161
      let pp_contract_opt =
162
        let pp_var x fmt =
163
            pp_clean_ada_identifier fmt x
164
        in
165
        let guarantee_post_conditions = List.map pp_var guarantees in
166
        let state_pre_conditions, state_post_conditions =
167
          if is_machine_statefull m then
168
          begin
169
            let input = List.map pp_var_name m.mstep.step_inputs in
170
            let output = List.map pp_var_name m.mstep.step_outputs in
171
            let args =
172
              [[pp_old pp_state_name;pp_state_name]]
173
                @(if input!=[] then [input] else [])
174
                @(if output!=[] then [output] else [])
175
            in
176
            let transition fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_transition_name, args) in
177
            let invariant fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_invariant_name, [[pp_state_name]]) in
178
            [invariant], [transition;invariant]
179
          end
180
          else
181
            [], []
182
        in
183
        let post_conditions = state_post_conditions@guarantee_post_conditions in
184
        let pre_conditions = state_pre_conditions in
185
        if post_conditions = [] && pre_conditions = [] then
186
          None
187
        else
188
          Some (false, false, pre_conditions, post_conditions)
189
      in
190
      let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, false, [], []))) in
191
      let ghost_public = List.map pp_guarantee guarantees in
192
      fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%t"
193
        
194
        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_public
195
        (Utils.pp_final_char_if_non_empty ";@,@," ghost_public)
196
        
197
        pp_ifstatefull pp_state_decl_and_reset
198
        
199
        (*Declare the step procedure*)
200
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
201
        
202
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
203
        
204
        (pp_package (pp_axiomatize_package_name) [] false)
205
          (fun fmt -> fprintf fmt "pragma Annotate (GNATProve, External_Axiomatization);@,@,%a;@,%a;@,%a"
206
            (*Declare the init predicate*)
207
            (pp_init_predicate typed_submachines) (m_spec_opt, m)
208
            (*Declare the transition predicate*)
209
            (pp_transition_predicate typed_submachines) (m_spec_opt, m)
210
            (*Declare the invariant predicate*)
211
            (pp_invariant_predicate typed_submachines) (m_spec_opt, m)
212
          )
213
        
214
        (*Print the private section*)
215
        pp_private_section
216
    in
217
    
218
    let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
219
    let pp_generics = List.map pp_poly_type polymorphic_types in
220
    
221
    fprintf fmt "@[<v>%a%t%a;@]@."
222
      
223
      (* Include all the subinstance package*)
224
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
225
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
226
      
227
      (*Begin the package*)
228
      (pp_package (pp_package_name m) pp_generics false) pp_content
229

    
230
end