Project

General

Profile

« Previous | Next » 

Revision 230b168e

Added by Guillaume DAVY almost 3 years ago

Ada: Refactor Ada Backend to reduce redundancy, make it more modular and
more simple.

View differences:

src/backends/Ada/ada_backend_ads.ml
16 16
open Corelang
17 17
open Machine_code_common
18 18

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

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

  
25
  (** Print the declaration of a state element of a subinstance of a machine.
26
     @param machine the machine
27
     @param fmt the formater to print on
28
     @param substitution correspondance between polymorphic type id and their instantiation
29
     @param ident the identifier of the subinstance
30
     @param submachine the submachine of the subinstance
31
  **)
32
  let pp_machine_subinstance_state_decl fmt (ident, (substitution, submachine)) =
33
    pp_node_state_decl substitution ident fmt submachine
34

  
35
  (** Print the state record for a machine.
36
     @param fmt the formater to print on
37
     @param var_list list of all state var
38
     @param typed_instances list typed instances
39
  **)
40
  let pp_state_record_definition fmt (var_list, typed_instances) =
41
    fprintf fmt "@,  @[<v>record@,  @[<v>%a%t%t%a%t@]@,end record@]"
42
      (Utils.fprintf_list ~sep:";@;" pp_machine_subinstance_state_decl)
43
      typed_instances
44
      (Utils.pp_final_char_if_non_empty ";" typed_instances)
45
      (fun fmt -> if var_list!=[] && typed_instances!= [] then fprintf fmt "@,@," else fprintf fmt "")
46
      (Utils.fprintf_list ~sep:";@;" (pp_machine_var_decl NoMode))
47
      var_list
48
      (Utils.pp_final_char_if_non_empty ";" var_list)
49

  
50
  (** Print the declaration for polymorphic types.
51
     @param fmt the formater to print on
52
     @param polymorphic_types all the types to print
53
  **)
54
  let pp_generic fmt polymorphic_types =
55
    let pp_polymorphic_types =
56
      List.map (fun id fmt -> pp_polymorphic_type fmt id) polymorphic_types in
57
    if polymorphic_types != [] then
58
        fprintf fmt "generic@,  @[<v>%a;@]@,"
59
          (Utils.fprintf_list ~sep:";@," pp_private_type_decl)
60
          pp_polymorphic_types
61
    else
62
      fprintf fmt ""
63

  
64
  (** Print instanciation of a generic type in a new statement.
65
     @param fmt the formater to print on
66
     @param id id of the polymorphic type
67
     @param typ the new type
68
  **)
69
  let pp_generic_instanciation fmt (id, typ) =
70
    fprintf fmt "%a => %a" pp_polymorphic_type id pp_type typ
71

  
72 28
  (** Print a new statement instantiating a generic package.
73 29
     @param fmt the formater to print on
74 30
     @param substitutions the instanciation substitution
75 31
     @param machine the machine to instanciate
76 32
  **)
77 33
  let pp_new_package fmt (substitutions, machine) =
78
    fprintf fmt "package %a is new %a @[<v>(%a)@]"
79
      (pp_package_name_with_polymorphic substitutions) machine
80
      pp_package_name machine
81
      (Utils.fprintf_list ~sep:",@," pp_generic_instanciation) substitutions
82

  
83
  let pp_eexpr fmt eexpr = fprintf fmt "true"
34
    let pp_name = pp_package_name machine in
35
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
36
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
37
    pp_package_instanciation pp_new_name pp_name fmt instanciations
84 38

  
85 39
  (** Print a precondition in aspect
86 40
     @param fmt the formater to print on
......
88 42
  **)
89 43
  let pp_pre fmt expr =
90 44
    fprintf fmt "Pre => %a"
91
      pp_eexpr expr
45
      pp_clean_ada_identifier expr
92 46

  
93 47
  (** Print a postcondition in aspect
94 48
     @param fmt the formater to print on
95 49
     @param expr the expession to print as pre
96 50
  **)
97
  let pp_post fmt expr =
51
  let pp_post fmt ident =
98 52
    fprintf fmt "Post => %a"
99
      pp_eexpr expr
53
      pp_clean_ada_identifier ident
100 54

  
101 55
  (** Print the declaration of a procedure with a contract
102 56
     @param pp_prototype the prototype printer
103 57
     @param fmt the formater to print on
104 58
     @param contract the contract for the function to declare
105 59
  **)
106
  let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
107
    match opt_contract with
108
      | None -> pp_prototype fmt
109
      | Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)
110
      | Some (Contract contract) ->
111
          fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"
112
            pp_prototype
113
            (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
114
            (Utils.pp_final_char_if_non_empty ",@," contract.assume)
115
            (Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees
116

  
117
  (** Print the prototype with a contract of the reset procedure from a machine.
60
  let pp_contract guarantees fmt =
61
    fprintf fmt "@,  @[<v>Global => null%t%a@]"
62
      (Utils.pp_final_char_if_non_empty ",@," guarantees)
63
      (Utils.fprintf_list ~sep:",@," pp_post) guarantees
64

  
65
(*
66
  let pp_transition_name fmt = fprintf fmt "transition"
67
  let pp_state_name_transition suffix fmt = fprintf fmt "%t_%s" pp_state_name suffix
68

  
69
  (** Printing function for basic assignement [var_name := value].
70

  
71
      @param fmt the formater to print on
72
      @param var_name the name of the variable
73
      @param value the value to be assigned
74
   **)
75
  let pp_basic_assign m fmt var_name value =
76
    fprintf fmt "%a = %a"
77
      (pp_access_var m) var_name
78
      (pp_value m) value
79

  
80

  
81
  (** Printing function for instruction. See
82
      {!type:Machine_code_types.instr_t} for more details on
83
      machine types.
84

  
85
      @param typed_submachines list of all typed machine instances of this machine
86
      @param machine the current machine
87
      @param fmt the formater to print on
88
      @param instr the instruction to print
89
   **)
90
  let rec pp_machine_instr typed_submachines machine instr fmt =
91
    let pp_instr = pp_machine_instr typed_submachines machine in
92
    (* Print args for a step call *)
93
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
94
    let pp_args vl il fmt =
95
      fprintf fmt "@[%a@]%t@[%a@]"
96
        (Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl
97
        (Utils.pp_final_char_if_non_empty ",@," il)
98
        (Utils.fprintf_list ~sep:",@ " pp_var_name) il
99
    in
100
    (* Print a when branch of a case *)
101
    let pp_when (cond, instrs) fmt =
102
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
103
    in
104
    (* Print a case *)
105
    let pp_case fmt (g, hl) =
106
      fprintf fmt "case %a is@,%aend case"
107
        (pp_value machine) g
108
        pp_block (List.map pp_when hl)
109
    in
110
    (* Print a if *)
111
    (* If neg is true the we must test for the negation of the condition. It
112
       first check that we don't have a negation and a else case, if so it
113
       inverses the two branch and remove the negation doing a recursive
114
       call. *)
115
    let rec pp_if neg fmt (g, instrs1, instrs2) =
116
      match neg, instrs2 with
117
        | true, Some x -> pp_if false fmt (g, x, Some instrs1)
118
        | _ ->
119
          let pp_cond =
120
            if neg then
121
              fun fmt x -> fprintf fmt "! (%a)" (pp_value machine) x
122
            else
123
              pp_value machine
124
          in
125
          let pp_else = match instrs2 with
126
            | None -> fun fmt -> fprintf fmt ""
127
            | Some i2 -> fun fmt ->
128
                fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
129
          in
130
          fprintf fmt "if %a then@,%a%tend if"
131
            pp_cond g
132
            pp_block (List.map pp_instr instrs1)
133
            pp_else
134
    in
135
    match get_instr_desc instr with
136
      (* no reset *)
137
      | MNoReset _ -> ()
138
      (* reset  *)
139
      | MReset i when List.mem_assoc i typed_submachines ->
140
          let (substitution, submachine) = get_instance i typed_submachines in
141
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
142
          pp_call fmt (pp_package_access (pp_package, pp_name), [pp_state i])
143
      | MLocalAssign (ident, value) ->
144
          pp_basic_assign machine fmt ident value
145
      | MStateAssign (ident, value) ->
146
          pp_basic_assign machine fmt ident value
147
      | MStep ([i0], i, vl) when is_builtin_fun i ->
148
          let value = mk_val (Fun (i, vl)) i0.var_type in
149
          pp_basic_assign machine fmt i0 value
150
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
151
          let (substitution, submachine) = get_instance i typed_submachines in
152
          pp_package_call
153
            pp_step_procedure_name
154
            fmt
155
            (substitution, submachine, pp_state i, Some (pp_args vl il))
156
      | MBranch (_, []) -> assert false
157
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
158
          let neg = c1=tag_false in
159
          let other = match tl with
160
            | []         -> None
161
            | [(c2, i2)] -> Some i2
162
            | _          -> assert false
163
          in
164
          pp_if neg fmt (g, i1, other)
165
      | MBranch (g, hl) -> pp_case fmt (g, hl)
166
      | MComment s  ->
167
          let lines = String.split_on_char '\n' s in
168
          fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
169
      | _ -> assert false
170

  
171
  (** Print the expression function representing the transition predicate.
118 172
     @param fmt the formater to print on
119 173
     @param machine the machine
120 174
  **)
121
  let pp_step_prototype_contract fmt m =
122
    pp_procedure_prototype_contract
123
      (pp_step_prototype m)
124
      fmt
125
      m.mspec
126
       
175
  let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
176
    let spec_instrs = match opt_spec_machine with
177
      | None -> []
178
      | Some m -> m.mstep.step_instrs
179
    in
180
    fprintf fmt "function %t (%a; %a) return Boolean is (@,  @[<v>%a@,@]) with Ghost"
181
      pp_transition_name
182
      pp_var_decl_mode (In, pp_state_name_transition "old", pp_state_type)
183
      pp_var_decl_mode (In, pp_state_name_transition "new", pp_state_type)
184
      (Utils.fprintf_list ~sep:" and@," (pp_machine_instr typed_submachines m)) (m.mstep.step_instrs@spec_instrs)*)
127 185
    
128 186
  (** Remove duplicates from a list according to a given predicate.
129 187
     @param eq the predicate defining equality
......
152 210
     @param typed_submachines list of all typed submachines of this machine
153 211
     @param m the machine
154 212
  **)
155
  let pp_file fmt (typed_submachines, m) =
213
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), m)) =
156 214
    let typed_machines = snd (List.split typed_submachines) in
157 215
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
158 216
    
159
    let machines_to_import = snd (List.split typed_machines_set) in
217
    let machines_to_import = List.map pp_package_name (snd (List.split typed_machines_set)) in
160 218

  
161 219
    let polymorphic_types = find_all_polymorphic_type m in
162 220
    
......
164 222
      List.filter (fun (l, _) -> l != []) typed_machines_set in
165 223

  
166 224
    let typed_instances = List.filter is_submachine_statefull typed_submachines in
167
    
168
    let pp_record fmt =
169
      pp_state_record_definition fmt (m.mmemory, typed_instances) in
170 225

  
171
    let pp_state_decl_and_reset fmt = fprintf fmt "%a;@,@,%t;@,@,"
226
    let pp_state_decl_and_reset fmt = fprintf fmt "%t;@,@,%a;@,@,"
172 227
      (*Declare the state type*)
173
      pp_private_limited_type_decl pp_state_type
228
      (pp_type_decl pp_state_type AdaLimitedPrivate)
174 229
      (*Declare the reset procedure*)
175
      (pp_reset_prototype m)
230
      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None) AdaNoContent
176 231
    in
177 232

  
178
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,"
233
    let vars = List.map (build_pp_var_decl AdaNoMode) m.mmemory in
234
    let states = List.map build_pp_state_decl_from_subinstance typed_instances in
235
    let var_lists = (if vars = [] then [] else [vars])@(if states = [] then [] else [states]) in
236

  
237
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a"
179 238
      (*Instantiate the polymorphic type that need to be instantiated*)
180 239
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
181 240
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
182 241
      (*Define the state type*)
183
      pp_type_decl (pp_state_type, pp_record)
242
      (pp_record pp_state_type) var_lists
184 243
    in
185 244
    
186 245
    let pp_ifstatefull fmt pp =
......
189 248
      else
190 249
        fprintf fmt ""
191 250
    in
251

  
252
    let pp_content fmt =
253
      let pp_contract_opt = match guarantees with
254
                              | [] -> None
255
                              | _ ->  Some (pp_contract guarantees) in
256
      fprintf fmt "%a%a;@,%a" (* %a;@, *)
257
        pp_ifstatefull pp_state_decl_and_reset
258
        
259
        (*Declare the transition predicate*)
260
        (* pp_transition_predicate typed_submachines) (opt_spec_machine, m) *)
261
        
262
        (*Declare the step procedure*)
263
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
264
        
265
        (*Print the private section*)
266
        pp_ifstatefull pp_private_section
267
    in
192 268
    
193
    fprintf fmt "@[<v>%a%t%a%a@,  @[<v>@,%a%a;@,%a@]@,%a;@.@]"
269
    let pp_poly_types id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
270
    let pp_generics = List.map pp_poly_types polymorphic_types in
271
    
272
    fprintf fmt "@[<v>%a%t%a;@]@."
194 273
      
195 274
      (* Include all the subinstance package*)
196
      (Utils.fprintf_list ~sep:";@," pp_with_machine) machines_to_import
275
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) machines_to_import
197 276
      (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
198 277
      
199
      pp_generic polymorphic_types
200
      
201 278
      (*Begin the package*)
202
      (pp_begin_package false) m
203

  
204
      pp_ifstatefull pp_state_decl_and_reset
205
      
206
      (*Declare the step procedure*)
207
      pp_step_prototype_contract m
208
      
209
      (*Print the private section*)
210
      pp_ifstatefull pp_private_section
211
      
212
      (*End the package*)
213
      pp_end_package m
279
      (pp_package (pp_package_name m) pp_generics false) pp_content
214 280

  
215 281
end

Also available in: Unified diff