Project

General

Profile

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
124
(** Return a default ada constant for a given type. @param cst_typ the constant
125
    type **)
126
let default_ada_cst t =
127
  let open Types in
128
  if is_bool_type t then
129
    Const_tag tag_false
130
  else if is_int_type t then
131
    Const_int 0
132
  else if is_real_type t then
133
    Const_real Real.zero
134
  else
135
    assert false
136

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

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

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

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

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

    
184
(* Expression print functions *)
185

    
186
(* Printing functions for basic operations and expressions *)
187
(* TODO: refactor code -> use let rec and for basic pretty printing function *)
188

    
189
(** Printing function for Ada tags, mainly booleans.
190

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

    
196
(** Printing function for machine type constants. For the moment, arrays are not
197
    supported.
198

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

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

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

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

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

    
252
(** Printing function for basic lib functions.
253

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

    
296
(** Printing function for values.
297

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

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

    
321
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
322

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

    
335
(** Print variable declaration for a local state variable @param fmt the
336
    formater to print on @param mode input/output mode of the parameter **)
337
let build_pp_state_decl mode with_statement =
338
  mode, pp_state_name, pp_state_type, with_statement
339

    
340
let build_pp_var_decl mode with_statement var =
341
  let pp_name = function fmt -> pp_var_name var fmt in
342
  let pp_type = function fmt -> pp_var_type fmt var in
343
  mode, pp_name, pp_type, with_statement
344

    
345
let build_pp_var_decl_local with_statement var =
346
  AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
347

    
348
let build_pp_var_decl_step_input mode with_statement m =
349
  if m.mstep.step_inputs = [] then []
350
  else [ List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs ]
351

    
352
let build_pp_var_decl_step_output mode with_statement m =
353
  if m.mstep.step_outputs = [] then []
354
  else [ List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs ]
355

    
356
let build_pp_var_decl_static mode with_statement m =
357
  if m.mstatic = [] then []
358
  else [ List.map (build_pp_var_decl mode with_statement) m.mstatic ]
359

    
360
let build_pp_arg_step m =
361
  (if is_machine_statefull m then [ [ build_pp_state_decl AdaInOut None ] ]
362
  else [])
363
  @ build_pp_var_decl_step_input AdaIn None m
364
  @ build_pp_var_decl_step_output AdaOut None m
365

    
366
let build_pp_arg_reset m =
367
  (if is_machine_statefull m then [ [ build_pp_state_decl AdaOut None ] ]
368
  else [])
369
  @ build_pp_var_decl_static AdaIn None m
370

    
371
(* let build_pp_arg_transition m =
372
 *   (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
373
 *     @ (build_pp_var_decl_step_input AdaIn None m)
374
 *     @ (build_pp_var_decl_step_output AdaOut None m) *)
(8-8/17)