Project

General

Profile

Download (13.6 KB) Statistics
| Branch: | Tag: | Revision:
1
open Format
2
open Machine_code_types
3
open Lustre_types
4
open Machine_code_common
5
open Ada_printer
6
open Misc_printer
7
open Misc_lustre_function
8

    
9
exception Ada_not_supported of string
10
(** Exception for unsupported features in Ada backend **)
11

    
12
(** Print the name of the state variable. @param fmt the formater to print on **)
13
let pp_state_name fmt = fprintf fmt "state"
14

    
15
(** Print the type of the state variable. @param fmt the formater to print on **)
16
let pp_state_type fmt = fprintf fmt "TState"
17

    
18
(** Print the name of the reset procedure @param fmt the formater to print on **)
19
let pp_reset_procedure_name fmt = fprintf fmt "reset"
20

    
21
(** Print the name of the step procedure @param fmt the formater to print on **)
22
let pp_step_procedure_name fmt = fprintf fmt "step"
23

    
24
(** Print the name of the main procedure. @param fmt the formater to print on **)
25
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
26

    
27
(** Print the name of the arrow package. @param fmt the formater to print on **)
28
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
29

    
30
(** Print the type of a polymorphic type. @param fmt the formater to print on
31
    @param id the id of the polymorphic type **)
32
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
33

    
34
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
35

    
36
(*TODO Check all this function with unit test, improve this system and add
37
  support for : "cbrt", "erf", "log10", "pow", "atan2". *)
38
let ada_supported_funs =
39
  [
40
    "sqrt", ("Ada.Numerics.Elementary_Functions", "Sqrt");
41
    "log", ("Ada.Numerics.Elementary_Functions", "Log");
42
    "exp", ("Ada.Numerics.Elementary_Functions", "Exp");
43
    "pow", ("Ada.Numerics.Elementary_Functions", "**");
44
    "sin", ("Ada.Numerics.Elementary_Functions", "Sin");
45
    "cos", ("Ada.Numerics.Elementary_Functions", "Cos");
46
    "tan", ("Ada.Numerics.Elementary_Functions", "Tan");
47
    "asin", ("Ada.Numerics.Elementary_Functions", "Arcsin");
48
    "acos", ("Ada.Numerics.Elementary_Functions", "Arccos");
49
    "atan", ("Ada.Numerics.Elementary_Functions", "Arctan");
50
    "sinh", ("Ada.Numerics.Elementary_Functions", "Sinh");
51
    "cosh", ("Ada.Numerics.Elementary_Functions", "Cosh");
52
    "tanh", ("Ada.Numerics.Elementary_Functions", "Tanh");
53
    "asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh");
54
    "acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh");
55
    "atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh");
56
    "ceil", ("", "Float'Ceiling");
57
    "floor", ("", "Float'Floor");
58
    "fmod", ("", "Float'Remainder");
59
    "round", ("", "Float'Rounding");
60
    "trunc", ("", "Float'Truncation");
61
    "fabs", ("", "abs");
62
  ]
63

    
64
let is_builtin_fun ident =
65
  List.mem ident Basic_library.internal_funs
66
  || List.mem_assoc ident ada_supported_funs
67

    
68
(** Print the name of a package associated to a machine. @param fmt the formater
69
    to print on @param machine the machine **)
70
let pp_package_name machine fmt =
71
  if is_arrow machine then fprintf fmt "%t" pp_arrow_package_name
72
  else fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
73

    
74
(** Print a type. @param fmt the formater to print on @param type the type **)
75
let pp_type fmt typ =
76
  match (Types.repr typ).Types.tdesc with
77
  | Types.Tbasic Types.Basic.Tint ->
78
    pp_integer_type fmt
79
  | Types.Tbasic Types.Basic.Treal ->
80
    pp_float_type fmt
81
  | Types.Tbasic Types.Basic.Tbool ->
82
    pp_boolean_type fmt
83
  | Types.Tunivar ->
84
    pp_polymorphic_type typ.Types.tid fmt
85
  | Types.Tbasic _ ->
86
    eprintf "Tbasic@.";
87
    assert false (*TODO*)
88
  | Types.Tconst _ ->
89
    eprintf "Tconst@.";
90
    assert false (*TODO*)
91
  | Types.Tclock _ ->
92
    eprintf "Tclock@.";
93
    assert false (*TODO*)
94
  | Types.Tarrow _ ->
95
    eprintf "Tarrow@.";
96
    assert false (*TODO*)
97
  | Types.Ttuple l ->
98
    eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l;
99
    assert false (*TODO*)
100
  | Types.Tenum _ ->
101
    eprintf "Tenum@.";
102
    assert false (*TODO*)
103
  | Types.Tstruct _ ->
104
    eprintf "Tstruct@.";
105
    assert false (*TODO*)
106
  | Types.Tarray _ ->
107
    eprintf "Tarray@.";
108
    assert false (*TODO*)
109
  | Types.Tstatic _ ->
110
    eprintf "Tstatic@.";
111
    assert false (*TODO*)
112
  | Types.Tlink _ ->
113
    eprintf "Tlink@.";
114
    assert false (*TODO*)
115
  | Types.Tvar ->
116
    eprintf "Tvar@.";
117
    assert false
118
(*TODO*)
119
(*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
120

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

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

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

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

    
164
(** Print the name of a variable. @param fmt the formater to print on @param id
165
    the variable **)
166
let pp_var_name id fmt = fprintf fmt "%a" pp_clean_ada_identifier id.var_id
167

    
168
(** Print the complete name of variable. @param m the machine to check if it is
169
    memory @param fmt the formater to print on @param var the variable **)
170
let pp_var env fmt var =
171
  match List.assoc_opt var.var_id env with
172
  | None ->
173
    pp_var_name var fmt
174
  | Some pp_state ->
175
    pp_access pp_state (pp_var_name var) fmt
176

    
177
(* Expression print functions *)
178

    
179
(* Printing functions for basic operations and expressions *)
180
(* TODO: refactor code -> use let rec and for basic pretty printing function *)
181

    
182
(** Printing function for Ada tags, mainly booleans.
183

    
184
    @param fmt the formater to use @param t the tag to print **)
185
let pp_ada_tag fmt t =
186
  pp_print_string fmt
187
    (if t = tag_true then "True" else if t = tag_false then "False" else t)
188

    
189
(** Printing function for machine type constants. For the moment, arrays are not
190
    supported.
191

    
192
    @param fmt the formater to use @param c the constant to print **)
193
let pp_ada_const fmt c =
194
  match c with
195
  | Const_int i ->
196
    pp_print_int fmt i
197
  | Const_real r ->
198
    Real.pp_ada fmt r
199
  | Const_tag t ->
200
    pp_ada_tag fmt t
201
  | Const_string _ | Const_modeid _ ->
202
    Format.eprintf
203
      "internal error: Ada_backend_adb.pp_ada_const cannot print string or \
204
       modeid.";
205
    assert false
206
  | _ ->
207
    raise
208
      (Ada_not_supported
209
         "unsupported: Ada_backend_adb.pp_ada_const does not\n\
210
         \    support this constant")
211

    
212
(** Printing function for expressions [v1 modulo v2]. Depends on option
213
    [integer_div_euclidean] to choose between mathematical modulo or remainder
214
    ([rem] in Ada).
215

    
216
    @param pp_value pretty printer for values @param v1 the first value in the
217
    expression @param v2 the second value in the expression @param fmt the
218
    formater to print on **)
219
let pp_mod pp_value v1 v2 fmt =
220
  if !Options.integer_div_euclidean then
221
    (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
222
    Format.fprintf fmt
223
      "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))" pp_value v1
224
      pp_value v2 pp_value v1 pp_value v2 pp_value v2
225
  else
226
    (* Ada behavior for rem *)
227
    Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
228

    
229
(** Printing function for expressions [v1 div v2]. Depends on option
230
    [integer_div_euclidean] to choose between mathematic division or Ada
231
    division.
232

    
233
    @param pp_value pretty printer for values @param v1 the first value in the
234
    expression @param v2 the second value in the expression @param fmt the
235
    formater to print in **)
236
let pp_div pp_value v1 v2 fmt =
237
  if !Options.integer_div_euclidean then
238
    (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
239
    Format.fprintf fmt "(%a - %t) / %a" pp_value v1 (pp_mod pp_value v1 v2)
240
      pp_value v2
241
  else
242
    (* Ada behavior for / *)
243
    Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
244

    
245
(** Printing function for basic lib functions.
246

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

    
289
(** Printing function for values.
290

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

    
308
(** Print the filename of a machine package. @param extension the extension to
309
    append to the package name @param fmt the formatter @param machine the
310
    machine corresponding to the package **)
311
let pp_machine_filename extension fmt machine =
312
  pp_filename extension fmt (pp_package_name machine)
313

    
314
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
315

    
316
(** Print the declaration of a state element of a subinstance of a machine.
317
    @param machine the machine @param fmt the formater to print on @param
318
    substitution correspondance between polymorphic type id and their
319
    instantiation @param ident the identifier of the subinstance @param
320
    submachine the submachine of the subinstance **)
321
let build_pp_state_decl_from_subinstance mode with_statement
322
    (name, (substitution, machine)) =
323
  let pp_package = pp_package_name_with_polymorphic substitution machine in
324
  let pp_type = pp_package_access (pp_package, pp_state_type) in
325
  let pp_name fmt = pp_clean_ada_identifier fmt name in
326
  mode, pp_name, pp_type, with_statement
327

    
328
(** Print variable declaration for a local state variable @param fmt the
329
    formater to print on @param mode input/output mode of the parameter **)
330
let build_pp_state_decl mode with_statement =
331
  mode, pp_state_name, pp_state_type, with_statement
332

    
333
let build_pp_var_decl mode with_statement var =
334
  let pp_name = function fmt -> pp_var_name var fmt in
335
  let pp_type = function fmt -> pp_var_type fmt var in
336
  mode, pp_name, pp_type, with_statement
337

    
338
let build_pp_var_decl_local with_statement var =
339
  AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
340

    
341
let build_pp_var_decl_step_input mode with_statement m =
342
  if m.mstep.step_inputs = [] then []
343
  else [ List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs ]
344

    
345
let build_pp_var_decl_step_output mode with_statement m =
346
  if m.mstep.step_outputs = [] then []
347
  else [ List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs ]
348

    
349
let build_pp_var_decl_static mode with_statement m =
350
  if m.mstatic = [] then []
351
  else [ List.map (build_pp_var_decl mode with_statement) m.mstatic ]
352

    
353
let build_pp_arg_step m =
354
  (if is_machine_statefull m then [ [ build_pp_state_decl AdaInOut None ] ]
355
  else [])
356
  @ build_pp_var_decl_step_input AdaIn None m
357
  @ build_pp_var_decl_step_output AdaOut None m
358

    
359
let build_pp_arg_reset m =
360
  (if is_machine_statefull m then [ [ build_pp_state_decl AdaOut None ] ]
361
  else [])
362
  @ build_pp_var_decl_static AdaIn None m
363

    
364
(* let build_pp_arg_transition m =
365
 *   (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
366
 *     @ (build_pp_var_decl_step_input AdaIn None m)
367
 *     @ (build_pp_var_decl_step_output AdaOut None m) *)
(5-5/11)