Project

General

Profile

Download (14 KB) Statistics
| Branch: | Tag: | Revision:
1
open Format
2

    
3
open Machine_code_types
4
open Lustre_types
5
open Machine_code_common
6

    
7
open Ada_printer
8
open Misc_printer
9
open Misc_lustre_function
10

    
11
(** Exception for unsupported features in Ada backend **)
12
exception Ada_not_supported of string
13

    
14
(** Print the name of the state variable.
15
   @param fmt the formater to print on
16
**)
17
let pp_state_name fmt = fprintf fmt "state"
18

    
19
(** Print the type of the state variable.
20
   @param fmt the formater to print on
21
**)
22
let pp_state_type fmt = fprintf fmt "TState"
23

    
24
 (** Print the name of the reset procedure
25
   @param fmt the formater to print on
26
**)
27
let pp_reset_procedure_name fmt = fprintf fmt "reset"
28

    
29
 (** Print the name of the step procedure
30
   @param fmt the formater to print on
31
**)
32
let pp_step_procedure_name fmt = fprintf fmt "step"
33

    
34
 (** Print the name of the main procedure.
35
   @param fmt the formater to print on
36
**)
37
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
38

    
39
 (** Print the name of the arrow package.
40
   @param fmt the formater to print on
41
**)
42
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
43

    
44
 (** Print the type of a polymorphic type.
45
   @param fmt the formater to print on
46
   @param id the id of the polymorphic type
47
**)
48
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
49

    
50
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
51

    
52

    
53

    
54

    
55

    
56

    
57

    
58

    
59

    
60
(*TODO Check all this function with unit test, improve this system and
61
   add support for : "cbrt", "erf", "log10", "pow", "atan2".
62
*)
63
let ada_supported_funs =
64
  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));
65
   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));
66
   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));
67
   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));
68
   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));
69
   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));
70
   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));
71
   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));
72
   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));
73
   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));
74
   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));
75
   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));
76
   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));
77
   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
78
   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
79
   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
80
   
81
   ("ceil",  ("", "Float'Ceiling"));
82
   ("floor", ("", "Float'Floor"));
83
   ("fmod",  ("", "Float'Remainder"));
84
   ("round", ("", "Float'Rounding"));
85
   ("trunc", ("", "Float'Truncation"));
86

    
87
   ("fabs", ("", "abs"));]
88

    
89
let is_builtin_fun ident =
90
  List.mem ident Basic_library.internal_funs ||
91
    List.mem_assoc ident ada_supported_funs
92

    
93
(** Print the name of a package associated to a machine.
94
   @param fmt the formater to print on
95
   @param machine the machine
96
**)
97
let pp_package_name machine fmt =
98
  if is_arrow machine then
99
      fprintf fmt "%t" pp_arrow_package_name
100
  else
101
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
102

    
103
(** Print a type.
104
   @param fmt the formater to print on
105
   @param type the type
106
**)
107
let pp_type fmt typ = 
108
  (match (Types.repr typ).Types.tdesc with
109
    | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
110
    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
111
    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
112
    | Types.Tunivar                  -> pp_polymorphic_type typ.Types.tid fmt
113
    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
114
    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
115
    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
116
    | Types.Tarrow _                 -> eprintf "Tarrow@."; assert false (*TODO*)
117
    | Types.Ttuple l                 -> eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; assert false (*TODO*)
118
    | Types.Tenum _                  -> eprintf "Tenum@.";  assert false (*TODO*)
119
    | Types.Tstruct _                -> eprintf "Tstruct@.";assert false (*TODO*)
120
    | Types.Tarray _                 -> eprintf "Tarray@."; assert false (*TODO*)
121
    | Types.Tstatic _                -> eprintf "Tstatic@.";assert false (*TODO*)
122
    | Types.Tlink _                  -> eprintf "Tlink@.";  assert false (*TODO*)
123
    | Types.Tvar                     -> eprintf "Tvar@.";   assert false (*TODO*)
124
    (*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
125
  )
126

    
127
(** Return a default ada constant for a given type.
128
   @param cst_typ the constant type
129
**)
130
let default_ada_cst cst_typ = match cst_typ with
131
  | Types.Basic.Tint  -> Const_int 0
132
  | Types.Basic.Treal -> Const_real Real.zero
133
  | Types.Basic.Tbool -> Const_tag tag_false
134
  | _ -> assert false
135

    
136
(** Make a default value from a given type.
137
   @param typ the type
138
**)
139
let mk_default_value typ =
140
  match (Types.repr typ).Types.tdesc with
141
    | Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ
142
    | _                              -> assert false (*TODO*)
143

    
144
(** Print the type of a variable.
145
   @param fmt the formater to print on
146
   @param id the variable
147
**)
148
let pp_var_type fmt id = 
149
  pp_type fmt id.var_type
150

    
151
(** Print a package name with polymorphic types specified.
152
   @param substitution correspondance between polymorphic type id and their instantiation
153
   @param fmt the formater to print on
154
   @param machine the machine
155
**)
156
let pp_package_name_with_polymorphic substitution machine fmt =
157
  let polymorphic_types = find_all_polymorphic_type machine in
158
  assert(List.length polymorphic_types = List.length substitution);
159
  let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
160
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
161
            polymorphic_types substituion);
162
  let instantiated_types = snd (List.split substitution) in
163
  fprintf fmt "%t%t%a"
164
    (pp_package_name machine)
165
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
166
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
167

    
168
(** Print the name of a variable.
169
   @param fmt the formater to print on
170
   @param id the variable
171
**)
172
let pp_var_name id fmt =
173
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
174

    
175
(** Print the complete name of variable.
176
   @param m the machine to check if it is memory
177
   @param fmt the formater to print on
178
   @param var the variable
179
**)
180
let pp_var env fmt var =
181
  match List.assoc_opt var.var_id env with
182
    | None -> pp_var_name var fmt
183
    | Some pp_state -> pp_access pp_state (pp_var_name var) fmt
184

    
185
(* Expression print functions *)
186

    
187
(* Printing functions for basic operations and expressions *)
188
(* TODO: refactor code -> use let rec and for basic pretty printing
189
   function *)
190
(** Printing function for Ada tags, mainly booleans.
191

    
192
    @param fmt the formater to use
193
    @param t the tag to print
194
 **)
195
let pp_ada_tag fmt t =
196
  pp_print_string fmt
197
    (if t = tag_true then "True" else if t = tag_false then "False" else t)
198

    
199
(** Printing function for machine type constants. For the moment,
200
    arrays are not supported.
201

    
202
    @param fmt the formater to use
203
    @param c the constant to print
204
 **)
205
let pp_ada_const fmt c =
206
  match c with
207
  | Const_int i                     -> pp_print_int fmt i
208
  | Const_real r                    -> Real.pp_ada fmt r
209
  | Const_tag t                     -> pp_ada_tag fmt t
210
  | Const_string _ | Const_modeid _ ->
211
    (Format.eprintf
212
       "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
213
     assert false)
214
  | _                               ->
215
    raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
216
    support this constant")
217

    
218
(** Printing function for expressions [v1 modulo v2]. Depends
219
    on option [integer_div_euclidean] to choose between mathematical
220
    modulo or remainder ([rem] in Ada).
221

    
222
    @param pp_value pretty printer for values
223
    @param v1 the first value in the expression
224
    @param v2 the second value in the expression
225
    @param fmt the formater to print on
226
 **)
227
let pp_mod pp_value v1 v2 fmt =
228
  if !Options.integer_div_euclidean then
229
    (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
230
    Format.fprintf fmt
231
      "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
232
      pp_value v1 pp_value v2
233
      pp_value v1 pp_value v2
234
      pp_value v2
235
  else (* Ada behavior for rem *)
236
    Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
237

    
238
(** Printing function for expressions [v1 div v2]. Depends on
239
    option [integer_div_euclidean] to choose between mathematic
240
    division or Ada division.
241

    
242
    @param pp_value pretty printer for values
243
    @param v1 the first value in the expression
244
    @param v2 the second value in the expression
245
    @param fmt the formater to print in
246
 **)
247
let pp_div pp_value v1 v2 fmt =
248
  if !Options.integer_div_euclidean then
249
    (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
250
    Format.fprintf fmt "(%a - %t) / %a"
251
      pp_value v1
252
      (pp_mod pp_value v1 v2)
253
      pp_value v2
254
  else (* Ada behavior for / *)
255
    Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
256

    
257
(** Printing function for basic lib functions.
258

    
259
    @param pp_value pretty printer for values
260
    @param i a string representing the function
261
    @param fmt the formater to print on
262
    @param vl the list of operands
263
 **)
264
let pp_basic_lib_fun pp_value ident fmt vl =
265
  match ident, vl with
266
  | "uminus", [v]    ->
267
    Format.fprintf fmt "(- %a)" pp_value v
268
  | "not", [v]       ->
269
    Format.fprintf fmt "(not %a)" pp_value v
270
  | "impl", [v1; v2] ->
271
    Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
272
  | "=", [v1; v2]    ->
273
    Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
274
  | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
275
  | "equi", [v1; v2] ->
276
    Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
277
  | "xor", [v1; v2]  ->
278
    Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
279
  | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
280
  | "&&", [v1; v2]    ->
281
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
282
  | "||", [v1; v2]    ->
283
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
284
  | "!=", [v1; v2]    ->
285
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
286
  | "ite", [v1; v2; v3]    ->
287
    Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3
288
  | op, [v1; v2]     ->
289
    Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
290
  | _, [v1] when  List.mem_assoc ident ada_supported_funs ->
291
    let pkg, name = try List.assoc ident ada_supported_funs
292
      with Not_found -> assert false in
293
    let pkg = pkg^(if String.equal pkg "" then "" else ".") in
294
      Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1
295
  | fun_name, _      ->
296
    (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
297

    
298
(** Printing function for values.
299

    
300
    @param m the machine to know the state variable
301
    @param fmt the formater to use
302
    @param value the value to print. Should be a
303
           {!type:Machine_code_types.value_t} value
304
 **)
305
let rec pp_value env fmt value =
306
  match value.value_desc with
307
  | Cst c             -> pp_ada_const fmt c
308
  | Var var      -> pp_var env fmt var (* Find better to test if it is memory or not *)
309
  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl
310
  | _                 ->
311
    raise (Ada_not_supported
312
             "unsupported: Ada_backend.adb.pp_value does not support this value type")
313

    
314

    
315
(** Print the filename of a machine package.
316
   @param extension the extension to append to the package name
317
   @param fmt the formatter
318
   @param machine the machine corresponding to the package
319
**)
320
let pp_machine_filename extension fmt machine =
321
  pp_filename extension fmt (pp_package_name machine)
322

    
323
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
324

    
325

    
326
(** Print the declaration of a state element of a subinstance of a machine.
327
   @param machine the machine
328
   @param fmt the formater to print on
329
   @param substitution correspondance between polymorphic type id and their instantiation
330
   @param ident the identifier of the subinstance
331
   @param submachine the submachine of the subinstance
332
**)
333
let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) =
334
  let pp_package = pp_package_name_with_polymorphic substitution machine in
335
  let pp_type = pp_package_access (pp_package, pp_state_type) in
336
  let pp_name fmt = pp_clean_ada_identifier fmt name in
337
  (mode, pp_name, pp_type, with_statement)
338

    
339
(** Print variable declaration for a local state variable
340
   @param fmt the formater to print on
341
   @param mode input/output mode of the parameter
342
**)
343
let build_pp_state_decl mode with_statement =
344
  (mode, pp_state_name, pp_state_type, with_statement)
345

    
346
let build_pp_var_decl mode with_statement var =
347
  let pp_name = function fmt -> pp_var_name var fmt in
348
  let pp_type = function fmt -> pp_var_type fmt var in
349
  (mode, pp_name, pp_type, with_statement)
350

    
351
let build_pp_var_decl_local with_statement var =
352
  AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
353

    
354
let build_pp_var_decl_step_input mode with_statement m =
355
  if m.mstep.step_inputs=[] then [] else
356
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]
357

    
358
let build_pp_var_decl_step_output mode with_statement m =
359
  if m.mstep.step_outputs=[] then [] else
360
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]
361

    
362
let build_pp_var_decl_static mode with_statement m =
363
  if m.mstatic=[] then [] else
364
    [List.map (build_pp_var_decl mode with_statement) m.mstatic]
365

    
366
let build_pp_arg_step m =
367
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
368
    @ (build_pp_var_decl_step_input AdaIn None m)
369
    @ (build_pp_var_decl_step_output AdaOut None m)
370

    
371
let build_pp_arg_reset m =
372
  (if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])
373
    @ (build_pp_var_decl_static AdaIn None m)
374

    
375

    
376
(* let build_pp_arg_transition m =
377
 *   (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
378
 *     @ (build_pp_var_decl_step_input AdaIn None m)
379
 *     @ (build_pp_var_decl_step_output AdaOut None m) *)
(5-5/11)