Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/backends/Ada/ada_backend_ads.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13

  
14 13
open Machine_code_types
15 14
open Lustre_types
16

  
17 15
open Misc_lustre_function
18 16
open Ada_printer
19 17
open Ada_backend_common
20 18

  
21

  
22

  
23 19
(** Functions printing the .ads file **)
24
module Main =
25
struct
26

  
27
  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*)
20
module Main = struct
21
  let rec init f = function i when i < 0 -> [] | i -> f i :: init f (i - 1)
22
  (*should be replaced by the init of list from ocaml std lib*)
28 23

  
29 24
  let suffixOld = "_old"
25

  
30 26
  let suffixNew = "_new"
27

  
31 28
  let pp_invariant_name fmt = fprintf fmt "inv"
29

  
32 30
  let pp_transition_name fmt = fprintf fmt "transition"
31

  
33 32
  let pp_init_name fmt = fprintf fmt "init"
34
  let pp_state_name_predicate suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
35
  let pp_axiomatize_package_name fmt = fprintf  fmt "axiomatize"
33

  
34
  let pp_state_name_predicate suffix fmt =
35
    fprintf fmt "%t%s" pp_state_name suffix
36

  
37
  let pp_axiomatize_package_name fmt = fprintf fmt "axiomatize"
36 38

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

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

  
55 62
  let pp_invariant_predicate fmt () =
56
    pp_predicate pp_invariant_name [[build_pp_state_decl AdaIn None]] true fmt None
63
    pp_predicate pp_invariant_name
64
      [ [ build_pp_state_decl AdaIn None ] ]
65
      true fmt None
57 66

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

  
69
  (** Remove duplicates from a list according to a given predicate.
70
     @param eq the predicate defining equality
71
     @param l the list to parse
72
  **)
80
  (** Remove duplicates from a list according to a given predicate. @param eq
81
      the predicate defining equality @param l the list to parse **)
73 82
  let remove_duplicates eq l =
74
    let aux l x = if List.exists (eq x) l then l else x::l in
83
    let aux l x = if List.exists (eq x) l then l else x :: l in
75 84
    List.fold_left aux [] l
76 85

  
77

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

  
84

  
85
  (** Print the package declaration(ads) of a machine.
86
    It requires the list of all typed instance.
87
    A typed submachine is a (ident, typed_machine) with
88
      - ident: the name 
89
      - typed_machine: a (substitution, machine) with
90
        - machine: the submachine struct
91
        - substitution the instanciation of all its polymorphic types.
92
     @param fmt the formater to print on
93
     @param typed_submachines list of all typed submachines of this machine
94
     @param m the machine
95
  **)
88
    String.equal machine1.mname.node_id machine2.mname.node_id
89
    && List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2
90

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

  
104
    let machines_to_import =
105
      List.map pp_package_name (snd (List.split typed_machines_set))
106
    in
101 107

  
102 108
    let polymorphic_types = find_all_polymorphic_type m in
103
    
109

  
104 110
    let typed_machines_to_instanciate =
105
      List.filter (fun (l, _) -> l != []) typed_machines_set in
111
      List.filter (fun (l, _) -> l != []) typed_machines_set
112
    in
106 113

  
107
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
114
    let typed_instances =
115
      List.filter is_submachine_statefull typed_submachines
116
    in
108 117

  
109
    let memories = match m_spec_opt with
110
      | None -> []
111
      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x)) m.mmemory
118
    let memories =
119
      match m_spec_opt with
120
      | None ->
121
        []
122
      | Some m ->
123
        List.map
124
          (fun x ->
125
            pp_var_decl
126
              (build_pp_var_decl AdaNoMode (Some (true, false, [], [])) x))
127
          m.mmemory
112 128
    in
113 129
    let ghost_private = memories in
114
    (* Commented since not used. Could be reinjected in the code 
115
    let vars_spec = match m_spec_opt with
116
      | None -> []
117
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, false, [], []))) (m_spec.mmemory)
118
    in *)
130
    (* Commented since not used. Could be reinjected in the code let vars_spec =
131
       match m_spec_opt with | None -> [] | Some m_spec -> List.map
132
       (build_pp_var_decl AdaNoMode (Some (true, false, [], [])))
133
       (m_spec.mmemory) in *)
119 134
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
120
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
135
    let states =
136
      List.map
137
        (build_pp_state_decl_from_subinstance AdaNoMode None)
138
        typed_instances
139
    in
121 140
    let var_lists =
122
      (if states = [] then [] else [states]) @
123
      (if vars = [] then [] else [vars]) in
124
    
141
      (if states = [] then [] else [ states ])
142
      @ if vars = [] then [] else [ vars ]
143
    in
144

  
125 145
    let pp_ifstatefull fmt pp =
126
      if is_machine_statefull m then
127
        fprintf fmt "%t" pp
128
      else
129
        fprintf fmt ""
146
      if is_machine_statefull m then fprintf fmt "%t" pp else fprintf fmt ""
130 147
    in
131 148

  
132 149
    let pp_state_decl_and_reset fmt =
133
      let init fmt = pp_call fmt (pp_access pp_axiomatize_package_name pp_init_name, [[pp_state_name]]) in
134
      let contract = Some (false, false, [], [init]) in
150
      let init fmt =
151
        pp_call fmt
152
          ( pp_access pp_axiomatize_package_name pp_init_name,
153
            [ [ pp_state_name ] ] )
154
      in
155
      let contract = Some (false, false, [], [ init ]) in
135 156
      fprintf fmt "%t;@,@,%a;@,@,"
136 157
        (*Declare the state type*)
137 158
        (pp_type_decl pp_state_type AdaPrivate)
138
        
139 159
        (*Declare the reset procedure*)
140
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract) AdaNoContent
160
        (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) contract)
161
        AdaNoContent
141 162
    in
142 163

  
143 164
    let pp_private_section fmt =
144 165
      fprintf fmt "@,private@,@,%a%t%a%t%a"
145
      (*Instantiate the polymorphic type that need to be instantiated*)
146
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
147
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
148
      
149
      (*Define the state type*)
150
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
151
        
152
      (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
153
      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) ghost_private
166
        (*Instantiate the polymorphic type that need to be instantiated*)
167
        (Utils.fprintf_list ~sep:";@," pp_new_package)
168
        typed_machines_to_instanciate
169
        (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
170
        (*Define the state type*)
171
        pp_ifstatefull
172
        (fun fmt -> pp_record pp_state_type fmt var_lists)
173
        (Utils.pp_final_char_if_non_empty ";@,@," ghost_private)
174
        (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt))
175
        ghost_private
154 176
    in
155 177

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

  
213 246
    let pp_poly_type id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
214 247
    let pp_generics = List.map pp_poly_type polymorphic_types in
215
    
248

  
216 249
    fprintf fmt "@[<v>%a%t%a;@]@."
217
      
218 250
      (* Include all the subinstance package*)
219
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility)) machines_to_import
251
      (Utils.fprintf_list ~sep:";@," (pp_with AdaNoVisibility))
252
      machines_to_import
220 253
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
221
      
222 254
      (*Begin the package*)
223
      (pp_package (pp_package_name m) pp_generics false) pp_content
224

  
255
      (pp_package (pp_package_name m) pp_generics false)
256
      pp_content
225 257
end

Also available in: Unified diff