Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_common.ml @ 826063db

History | View | Annotate | Download (32.4 KB)

1
open Format
2

    
3
open Machine_code_types
4
open Lustre_types
5
open Corelang
6
open Machine_code_common
7

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

    
11
(** All the pretty print and aux functions common to the ada backend **)
12

    
13
(* Misc pretty print functions *)
14

    
15
let is_machine_statefull m = not m.mname.node_dec_stateless
16

    
17
(*TODO Check all this function with unit test, improve this system and
18
   add support for : "cbrt", "erf", "log10", "pow", "atan2".
19
*)
20
let ada_supported_funs =
21
  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));
22
   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));
23
   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));
24
   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));
25
   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));
26
   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));
27
   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));
28
   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));
29
   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));
30
   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));
31
   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));
32
   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));
33
   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));
34
   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
35
   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
36
   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
37
   
38
   ("ceil",  ("", "Float'Ceiling"));
39
   ("floor", ("", "Float'Floor"));
40
   ("fmod",  ("", "Float'Remainder"));
41
   ("round", ("", "Float'Rounding"));
42
   ("trunc", ("", "Float'Truncation"));
43

    
44
   ("fabs", ("", "abs"));]
45

    
46
let is_builtin_fun ident =
47
  List.mem ident Basic_library.internal_funs ||
48
    List.mem_assoc ident ada_supported_funs
49

    
50
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
51
    underscore and must not contain a double underscore
52
   @param var name to be cleaned*)
53
let pp_clean_ada_identifier fmt name =
54
  let reserved_words = ["abort"; "else"; "new"; "return"; "boolean"; "integer";
55
                        "abs"; "elsif"; "not"; "reverse"; "abstract"; "end";
56
                        "null"; "accept"; "entry"; "select"; "access";
57
                        "exception"; "of"; "separate"; "aliased"; "exit";
58
                        "or"; "some"; "all"; "others"; "subtype"; "and";
59
                        "for"; "out"; "synchronized"; "array"; "function";
60
                        "overriding"; "at"; "tagged"; "generic"; "package";
61
                        "task"; "begin"; "goto"; "pragma"; "terminate";
62
                        "body"; "private"; "then"; "if"; "procedure"; "type";
63
                        "case"; "in"; "protected"; "constant"; "interface";
64
                        "until"; "is"; "raise"; "use"; "declare"; "	range";
65
                        "delay"; "limited"; "record"; "when"; "delta"; "loop";
66
                        "rem"; "while"; "digits"; "renames"; "with"; "do";
67
                        "mod"; "requeue"; "xor"; "float"] in
68
  let base_size = String.length name in
69
  assert(base_size > 0);
70
  let rec remove_double_underscore s = function
71
    | i when i == String.length s - 1 -> s
72
    | i when String.get s i == '_' && String.get s (i+1) == '_' ->
73
        remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
74
    | i -> remove_double_underscore s (i+1)
75
  in
76
  let name = if String.get name (base_size-1) == '_' then name^"ada" else name in
77
  let name = remove_double_underscore name 0 in
78
  let prefix = if String.length name != base_size
79
                  || String.get name 0 == '_' 
80
                  || List.exists (String.equal (String.lowercase_ascii name)) reserved_words then
81
                  "ada"
82
               else
83
                  ""
84
  in
85
  fprintf fmt "%s%s" prefix name
86

    
87
(** Encapsulate a pretty print function to lower case its result when applied
88
   @param pp the pretty print function
89
   @param fmt the formatter
90
   @param arg the argument of the pp function
91
**)
92
let pp_lowercase pp fmt =
93
  let str = asprintf "%t" pp in
94
  fprintf fmt "%s" (String. lowercase_ascii str)
95

    
96
(** Print a filename by lowercasing the base and appending an extension.
97
   @param extension the extension to append to the package name
98
   @param fmt the formatter
99
   @param pp_name the file base name printer
100
**)
101
let pp_filename extension fmt pp_name =
102
  fprintf fmt "%t.%s"
103
    (pp_lowercase pp_name)
104
    extension
105

    
106

    
107
(* Package pretty print functions *)
108

    
109
(** Return true if its the arrow machine
110
   @param machine the machine to test
111
*)
112
let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id
113

    
114
(** Print the name of the arrow package.
115
   @param fmt the formater to print on
116
**)
117
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
118

    
119
(** Print the name of a package associated to a machine.
120
   @param fmt the formater to print on
121
   @param machine the machine
122
**)
123
let pp_package_name fmt machine =
124
  if is_arrow machine then
125
      fprintf fmt "%t" pp_arrow_package_name
126
  else
127
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
128

    
129
(** Print the ada package introduction sentence it can be used for body and
130
declaration. Boolean parameter body should be true if it is a body delcaration.
131
   @param fmt the formater to print on
132
   @param fmt the formater to print on
133
   @param machine the machine
134
**)
135
let pp_begin_package body fmt machine =
136
  fprintf fmt "package %s%a is"
137
    (if body then "body " else "")
138
    pp_package_name machine
139

    
140
(** Print the ada package conclusion sentence.
141
   @param fmt the formater to print on
142
   @param machine the machine
143
**)
144
let pp_end_package fmt machine =
145
  fprintf fmt "end %a" pp_package_name machine
146

    
147
(** Print the access of an item from an other package.
148
   @param fmt the formater to print on
149
   @param package the package to use
150
   @param item the item which is accessed
151
**)
152
let pp_package_access fmt (package, item) =
153
  fprintf fmt "%t.%t" package item
154

    
155
(** Print the name of the main procedure.
156
   @param fmt the formater to print on
157
**)
158
let pp_main_procedure_name fmt =
159
  fprintf fmt "ada_main"
160

    
161
(** Print a with statement to include a package.
162
   @param fmt the formater to print on
163
   @param pp_pakage_name the package name printer
164
**)
165
let pp_private_with fmt pp_pakage_name =
166
  fprintf fmt "private with %t" pp_pakage_name
167

    
168
(** Print a with statement to include a package.
169
   @param fmt the formater to print on
170
   @param name the package name
171
**)
172
let pp_with fmt name =
173
  fprintf fmt "with %s" name
174

    
175
(** Print a with statement to include a machine.
176
   @param fmt the formater to print on
177
   @param machine the machine
178
**)
179
let pp_with_machine fmt machine =
180
  fprintf fmt "private with %a" pp_package_name machine
181

    
182
(** Extract a node from an instance.
183
   @param instance the instance
184
**)
185
let extract_node instance =
186
  let (_, (node, _)) = instance in
187
  match node.top_decl_desc with
188
    | Node nd         -> nd
189
    | _ -> assert false (*TODO*)
190

    
191
(** Extract from a machine list the one corresponding to the given instance.
192
      assume that the machine is in the list.
193
   @param machines list of all machines
194
   @param instance instance of a machine
195
   @return the machine corresponding to hte given instance
196
**)
197
let get_machine machines instance =
198
    let id = (extract_node instance).node_id in
199
    try
200
      List.find (function m -> m.mname.node_id=id) machines
201
    with
202
      Not_found -> assert false (*TODO*)
203

    
204

    
205
(* Type pretty print functions *)
206

    
207
(** Print a type declaration
208
   @param fmt the formater to print on
209
   @param pp_name a format printer which print the type name
210
   @param pp_value a format printer which print the type definition
211
**)
212
let pp_type_decl fmt (pp_name, pp_definition) =
213
  fprintf fmt "type %t is %t" pp_name pp_definition
214

    
215
(** Print a private type declaration
216
   @param fmt the formater to print on
217
   @param pp_name a format printer which print the type name
218
**)
219
let pp_private_type_decl fmt pp_name =
220
  let pp_definition fmt = fprintf fmt "private" in
221
  pp_type_decl fmt (pp_name, pp_definition)
222

    
223
(** Print a limited private type declaration
224
   @param fmt the formater to print on
225
   @param pp_name a format printer which print the type name
226
**)
227
let pp_private_limited_type_decl fmt pp_name =
228
  let pp_definition fmt = fprintf fmt "limited private" in
229
  pp_type_decl fmt (pp_name, pp_definition)
230

    
231
(** Print the type of the state variable.
232
   @param fmt the formater to print on
233
**)
234
let pp_state_type fmt =
235
  (* Type and variable names live in the same environement in Ada so name of
236
     this type and of the associated parameter : pp_state_name must be
237
     different *)
238
  fprintf fmt "TState"
239

    
240
(** Print the integer type name.
241
   @param fmt the formater to print on
242
**)
243
let pp_integer_type fmt = fprintf fmt "Integer"
244

    
245
(** Print the float type name.
246
   @param fmt the formater to print on
247
**)
248
let pp_float_type fmt = fprintf fmt "Float"
249

    
250
(** Print the boolean type name.
251
   @param fmt the formater to print on
252
**)
253
let pp_boolean_type fmt = fprintf fmt "Boolean"
254

    
255
(** Print the type of a polymorphic type.
256
   @param fmt the formater to print on
257
   @param id the id of the polymorphic type
258
**)
259
let pp_polymorphic_type fmt id =
260
  fprintf fmt "T_%i" id
261

    
262
(** Print a type.
263
   @param fmt the formater to print on
264
   @param type the type
265
**)
266
let pp_type fmt typ = 
267
  (match (Types.repr typ).Types.tdesc with
268
    | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
269
    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
270
    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
271
    | Types.Tunivar                  -> pp_polymorphic_type fmt typ.Types.tid
272
    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
273
    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
274
    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
275
    | Types.Tarrow _                 -> eprintf "Tarrow@."; assert false (*TODO*)
276
    | Types.Ttuple l                 -> eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; assert false (*TODO*)
277
    | Types.Tenum _                  -> eprintf "Tenum@.";  assert false (*TODO*)
278
    | Types.Tstruct _                -> eprintf "Tstruct@.";assert false (*TODO*)
279
    | Types.Tarray _                 -> eprintf "Tarray@."; assert false (*TODO*)
280
    | Types.Tstatic _                -> eprintf "Tstatic@.";assert false (*TODO*)
281
    | Types.Tlink _                  -> eprintf "Tlink@.";  assert false (*TODO*)
282
    | Types.Tvar                     -> eprintf "Tvar@.";   assert false (*TODO*)
283
    (*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
284
  )
285

    
286
(** Return a default ada constant for a given type.
287
   @param cst_typ the constant type
288
**)
289
let default_ada_cst cst_typ = match cst_typ with
290
  | Types.Basic.Tint  -> Const_int 0
291
  | Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0")
292
  | Types.Basic.Tbool -> Const_tag tag_false
293

    
294
(** Make a default value from a given type.
295
   @param typ the type
296
**)
297
let mk_default_value typ =
298
  match (Types.repr typ).Types.tdesc with
299
    | Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ
300
    | _                              -> assert false (*TODO*)
301

    
302
(** Test if two types are the same.
303
   @param typ1 the first type
304
   @param typ2 the second type
305
**)
306
let pp_eq_type typ1 typ2 = 
307
  let get_basic typ = match (Types.repr typ).Types.tdesc with
308
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
309
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
310
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
311
    | _ -> assert false (*TODO*)
312
  in
313
  get_basic typ1 = get_basic typ2
314

    
315

    
316
(** Print the type of a variable.
317
   @param fmt the formater to print on
318
   @param id the variable
319
**)
320
let pp_var_type fmt id = 
321
  pp_type fmt id.var_type
322

    
323
(** Extract all the inputs and outputs.
324
   @param machine the machine
325
   @return a list of all the var_decl of a macine
326
**)
327
let get_all_vars_machine m =
328
  m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic
329

    
330
(** Check if a type is polymorphic.
331
   @param typ the type
332
   @return true if its polymorphic
333
**)
334
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar
335

    
336
(** Find all polymorphic type : Types.Tunivar in a machine.
337
   @param machine the machine
338
   @return a list of id corresponding to polymorphic type
339
**)
340
let find_all_polymorphic_type m =
341
  let vars = get_all_vars_machine m in
342
  let extract id = id.var_type.tid in
343
  let polymorphic_type_vars =
344
    List.filter (function x-> is_Tunivar x.var_type) vars in
345
  List.sort_uniq (-) (List.map extract polymorphic_type_vars)
346

    
347
(** Print a package name with polymorphic types specified.
348
   @param substitution correspondance between polymorphic type id and their instantiation
349
   @param fmt the formater to print on
350
   @param machine the machine
351
**)
352
let pp_package_name_with_polymorphic substitution fmt machine =
353
  let polymorphic_types = find_all_polymorphic_type machine in
354
  assert(List.length polymorphic_types = List.length substitution);
355
  let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
356
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
357
            polymorphic_types substituion);
358
  let instantiated_types = snd (List.split substitution) in
359
  fprintf fmt "%a%t%a"
360
    pp_package_name machine
361
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
362
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
363

    
364

    
365
(* Variable pretty print functions *)
366

    
367
(** Represent the possible mode for a type of a procedure parameter **)
368
type parameter_mode = NoMode | In | Out | InOut
369

    
370
(** Print a parameter_mode.
371
   @param fmt the formater to print on
372
   @param mode the modifier
373
**)
374
let pp_parameter_mode fmt mode =
375
  fprintf fmt "%s" (match mode with
376
                     | NoMode -> ""
377
                     | In     -> "in"
378
                     | Out    -> "out"
379
                     | InOut  -> "in out")
380

    
381
(** Print the name of the state variable.
382
   @param fmt the formater to print on
383
**)
384
let pp_state_name fmt =
385
  fprintf fmt "state"
386

    
387

    
388
(** Print the name of a variable.
389
   @param fmt the formater to print on
390
   @param id the variable
391
**)
392
let pp_var_name fmt id =
393
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
394

    
395
(** Print the complete name of variable.
396
   @param m the machine to check if it is memory
397
   @param fmt the formater to print on
398
   @param var the variable
399
**)
400
let pp_access_var m fmt var =
401
  if is_memory m var then
402
    fprintf fmt "%t.%a" pp_state_name pp_var_name var
403
  else
404
    pp_var_name fmt var
405

    
406
(** Print a variable declaration
407
   @param mode input/output mode of the parameter
408
   @param pp_name a format printer wich print the variable name
409
   @param pp_type a format printer wich print the variable type
410
   @param fmt the formater to print on
411
   @param id the variable
412
**)
413
let pp_var_decl fmt (mode, pp_name, pp_type) =
414
  fprintf fmt "%t: %a%s%t"
415
    pp_name
416
    pp_parameter_mode mode
417
    (if mode = NoMode then "" else " ")
418
    pp_type
419

    
420
(** Print variable declaration for machine variable
421
   @param mode input/output mode of the parameter
422
   @param fmt the formater to print on
423
   @param id the variable
424
**)
425
let pp_machine_var_decl mode fmt id =
426
  let pp_name = function fmt -> pp_var_name fmt id in
427
  let pp_type = function fmt -> pp_var_type fmt id in
428
  pp_var_decl fmt (mode, pp_name, pp_type)
429

    
430
(** Print variable declaration for a local state variable
431
   @param fmt the formater to print on
432
   @param mode input/output mode of the parameter
433
**)
434
let pp_state_var_decl fmt mode =
435
  let pp_name = pp_state_name in
436
  let pp_type = pp_state_type in
437
  pp_var_decl fmt (mode, pp_name, pp_type)
438

    
439
(** Print the declaration of a state element of a machine.
440
   @param substitution correspondance between polymorphic type id and their instantiation
441
   @param name name of the variable
442
   @param fmt the formater to print on
443
   @param machine the machine
444
**)
445
let pp_node_state_decl substitution name fmt machine =
446
  let pp_package fmt = pp_package_name_with_polymorphic substitution fmt machine in
447
  let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
448
  let pp_name fmt = pp_clean_ada_identifier fmt name in
449
  pp_var_decl fmt (NoMode, pp_name, pp_type)
450

    
451

    
452
(* Prototype pretty print functions *)
453

    
454
(** Print the name of the reset procedure **)
455
let pp_reset_procedure_name fmt = fprintf fmt "reset"
456

    
457
(** Print the name of the step procedure **)
458
let pp_step_procedure_name fmt = fprintf fmt "step"
459

    
460
(** Print the name of the init procedure **)
461
let pp_init_procedure_name fmt = fprintf fmt "init"
462

    
463
(** Print the name of the clear procedure **)
464
let pp_clear_procedure_name fmt = fprintf fmt "clear"
465

    
466
(** Print the prototype of a procedure with non input/outputs
467
   @param fmt the formater to print on
468
   @param name the name of the procedure
469
**)
470
let pp_simple_prototype pp_name fmt =
471
  fprintf fmt "procedure %t" pp_name
472

    
473
(** Print the prototype of a machine procedure. The first parameter is always
474
the state, state_modifier specify the modifier applying to it. The next
475
parameters are inputs and the last parameters are the outputs.
476
   @param state_mode_opt None if no state parameter required and some input/output mode for it else
477
   @param input list of the input parameter of the procedure
478
   @param output list of the output parameter of the procedure
479
   @param fmt the formater to print on
480
   @param name the name of the procedure
481
**)
482
let pp_base_prototype state_mode_opt input output fmt pp_name =
483
  let pp_var_decl_state fmt = match state_mode_opt with
484
    | None -> fprintf fmt ""
485
    | Some state_mode -> fprintf fmt "%a" pp_state_var_decl state_mode
486
  in
487
  fprintf fmt "procedure %t(@[<v>%t%t@[%a@]%t@[%a@])@]"
488
    pp_name
489
    pp_var_decl_state
490
    (fun fmt -> if state_mode_opt != None && input!=[] then
491
      fprintf fmt ";@," else fprintf fmt "")
492
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl In)) input
493
    (fun fmt -> if (state_mode_opt != None || input!=[]) && output != [] then
494
      fprintf fmt ";@," else fprintf fmt "")
495
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl Out)) output
496

    
497
(** Print the prototype of the step procedure of a machine.
498
   @param m the machine
499
   @param fmt the formater to print on
500
   @param pp_name name function printer
501
**)
502
let pp_step_prototype m fmt =
503
  let state_mode = if is_machine_statefull m then Some InOut else None in
504
  pp_base_prototype state_mode m.mstep.step_inputs m.mstep.step_outputs fmt pp_step_procedure_name
505

    
506
(** Print the prototype of the reset procedure of a machine.
507
   @param m the machine
508
   @param fmt the formater to print on
509
   @param pp_name name function printer
510
**)
511
let pp_reset_prototype m fmt =
512
  let state_mode = if is_machine_statefull m then Some Out else None in
513
  pp_base_prototype state_mode m.mstatic [] fmt pp_reset_procedure_name
514

    
515
(** Print the prototype of the init procedure of a machine.
516
   @param m the machine
517
   @param fmt the formater to print on
518
   @param pp_name name function printer
519
**)
520
let pp_init_prototype m fmt =
521
  let state_mode = if is_machine_statefull m then Some Out else None in
522
  pp_base_prototype state_mode m.mstatic [] fmt pp_init_procedure_name
523

    
524
(** Print the prototype of the clear procedure of a machine.
525
   @param m the machine
526
   @param fmt the formater to print on
527
   @param pp_name name function printer
528
**)
529
let pp_clear_prototype m fmt =
530
  let state_mode = if is_machine_statefull m then Some InOut else None in
531
  pp_base_prototype state_mode m.mstatic [] fmt pp_clear_procedure_name
532

    
533
(** Print a one line comment with the final new line character to avoid
534
      commenting anything else.
535
   @param fmt the formater to print on
536
   @param s the comment without newline character
537
**)
538
let pp_oneline_comment fmt s =
539
  assert (not (String.contains s '\n'));
540
  fprintf fmt "-- %s@," s
541

    
542

    
543
(* Functions which computes the substitution for polymorphic type *)
544

    
545
(** Check if a submachine is statefull.
546
    @param submachine a submachine
547
    @return true if the submachine is statefull
548
**)
549
let is_submachine_statefull submachine =
550
    not (snd (snd submachine)).mname.node_dec_stateless
551

    
552
(** Find a submachine step call in a list of instructions.
553
    @param ident submachine instance ident
554
    @param instr_list List of instruction sto search
555
    @return a list of pair containing input types and output types for each step call found
556
**)
557
let rec find_submachine_step_call ident instr_list =
558
  let search_instr instruction = 
559
    match instruction.instr_desc with
560
      | MStep (il, i, vl) when String.equal i ident -> [
561
        (List.map (function x-> x.value_type) vl,
562
            List.map (function x-> x.var_type) il)]
563
      | MBranch (_, l) -> List.flatten
564
          (List.map (function x, y -> find_submachine_step_call ident y) l)
565
      | _ -> []
566
  in
567
  List.flatten (List.map search_instr instr_list)
568

    
569
(** Check that two types are the same.
570
   @param t1 a type
571
   @param t2 an other type
572
   @param return true if the two types are Tbasic or Tunivar and equal
573
**)
574
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
575
  match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
576
    | Types.Tbasic x, Types.Tbasic y -> x = y
577
    | Types.Tunivar,  Types.Tunivar  -> t1.tid = t2.tid
578
    | Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
579
    | _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
580
    | Types.Tstatic (_, t), _ -> check_type_equal t t2
581
    | _, Types.Tstatic (_, t) -> check_type_equal t1 t
582
    | _ -> eprintf "ERROR: %a | %a" pp_type t1 pp_type t2; assert false (* TODO *)
583

    
584
(** Extend a substitution to unify the two given types. Only the
585
  first type can be polymorphic.
586
    @param subsitution the base substitution
587
    @param type_poly the type which can be polymorphic
588
    @param typ the type to match type_poly with
589
**)
590
let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) =
591
  assert(not (is_Tunivar typ));
592
  (* If type_poly is polymorphic *)
593
  if is_Tunivar type_poly then
594
    (* If a subsitution exists for it *)
595
    if List.mem_assoc type_poly.tid substituion then
596
    begin
597
      (* We check that the type corresponding to type_poly in the subsitution
598
         match typ *)
599
      (try
600
        assert(check_type_equal (List.assoc type_poly.tid substituion) typ)
601
      with
602
        Not_found -> assert false);
603
      (* We return the original substituion, it is already correct *)
604
      substituion
605
    end
606
    (* If type_poly is not in the subsitution *)
607
    else
608
      (* We add it to the substituion *)
609
      (type_poly.tid, typ)::substituion
610
  (* iftype_poly is not polymorphic *)
611
  else
612
  begin
613
    (* We check that type_poly and typ are the same *)
614
    assert(check_type_equal type_poly typ);
615
    (* We return the original substituion, it is already correct *)
616
    substituion
617
  end
618

    
619
(** Check that two calls are equal. A call is
620
  a pair of list of types, the inputs and the outputs.
621
   @param calls a list of pair of list of types
622
   @param return true if the two pairs are equal
623
**)
624
let check_call_equal (i1, o1) (i2, o2) =
625
  (List.for_all2 check_type_equal i1 i2)
626
    && (List.for_all2 check_type_equal i1 i2)
627

    
628
(** Check that all the elements of list of calls are equal to one.
629
  A call is a pair of list of types, the inputs and the outputs.
630
   @param call a pair of list of types
631
   @param calls a list of pair of list of types
632
   @param return true if all the elements are equal
633
**)
634
let check_calls call calls =
635
  List.for_all (check_call_equal call) calls
636

    
637
(** Extract from a subinstance that can have polymorphic type the instantiation
638
    of all its polymorphic type instanciation for a given machine. It searches
639
    the step calls and extract a substitution for all polymorphic type from
640
    it.
641
   @param machine the machine which instantiate the subinstance
642
   @param ident the identifier of the instance which permits to find the step call
643
   @param submachine the machine corresponding to the subinstance
644
   @return the correspondance between polymorphic type id and their instantiation
645
**)
646
let get_substitution machine ident submachine =
647
  (* extract the calls to submachines from the machine *)
648
  let calls = find_submachine_step_call ident machine.mstep.step_instrs in
649
  (* extract the first call  *)
650
  let call = match calls with
651
              (* assume that there is always one call to a subinstance *)
652
              | []    -> assert(false)
653
              | h::t  -> h in
654
  (* assume that all the calls to a subinstance are using the same type *)
655
  assert(check_calls call calls);
656
  (* make a list of all types from input and output vars *)
657
  let call_types = (fst call)@(snd call) in
658
  (* extract all the input and output vars from the submachine *)
659
  let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in
660
  (* keep only the type of vars *)
661
  let machine_types = List.map (function x-> x.var_type) machine_vars in
662
  (* assume that there is the same numer of input and output in the submachine
663
      and the call *)
664
  assert (List.length machine_types = List.length call_types);
665
  (* Unify the two lists of types *)
666
  let substitution = List.fold_left unification [] (List.combine machine_types call_types) in
667
  (* Assume that our substitution match all the possible
668
       polymorphic type of the node *)
669
  let polymorphic_types = find_all_polymorphic_type submachine in
670
  assert (List.length polymorphic_types = List.length substitution);
671
  (try
672
    assert (List.for_all (fun x -> List.mem_assoc x substitution) polymorphic_types)
673
  with
674
    Not_found -> assert false);
675
  substitution
676

    
677

    
678
(* Procedure pretty print functions *)
679

    
680
let pp_block pp_item fmt items =
681
  fprintf fmt "  @[<v>%a%t@]@,"
682
    (Utils.fprintf_list ~sep:";@," pp_item) items
683
    (Utils.pp_final_char_if_non_empty ";" items)
684

    
685
(** Print the definition of a procedure
686
   @param pp_name the procedure name printer
687
   @param pp_prototype the prototype printer
688
   @param pp_instr local var printer
689
   @param pp_instr instruction printer
690
   @param fmt the formater to print on
691
   @param locals locals var list
692
   @param instrs instructions list
693
**)
694
let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals, instrs) =
695
  fprintf fmt "@[<v>%t is@,%abegin@,%aend %t@]"
696
    pp_prototype
697
    (pp_block pp_local) locals
698
    (pp_block pp_instr) instrs
699
    pp_name
700

    
701

    
702
(* Expression print functions *)
703

    
704
  (* Printing functions for basic operations and expressions *)
705
  (* TODO: refactor code -> use let rec and for basic pretty printing
706
     function *)
707
  (** Printing function for Ada tags, mainly booleans.
708

    
709
      @param fmt the formater to use
710
      @param t the tag to print
711
   **)
712
  let pp_ada_tag fmt t =
713
    pp_print_string fmt
714
      (if t = tag_true then "True" else if t = tag_false then "False" else t)
715

    
716
  (** Printing function for machine type constants. For the moment,
717
      arrays are not supported.
718

    
719
      @param fmt the formater to use
720
      @param c the constant to print
721
   **)
722
  let pp_ada_const fmt c =
723
    match c with
724
    | Const_int i                     -> pp_print_int fmt i
725
    | Const_real (c, e, s)            ->
726
        fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
727
    | Const_tag t                     -> pp_ada_tag fmt t
728
    | Const_string _ | Const_modeid _ ->
729
      (Format.eprintf
730
         "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
731
       assert false)
732
    | _                               ->
733
      raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
734
      support this constant")
735

    
736
  (** Printing function for expressions [v1 modulo v2]. Depends
737
      on option [integer_div_euclidean] to choose between mathematical
738
      modulo or remainder ([rem] in Ada).
739

    
740
      @param pp_value pretty printer for values
741
      @param v1 the first value in the expression
742
      @param v2 the second value in the expression
743
      @param fmt the formater to print on
744
   **)
745
  let pp_mod pp_value v1 v2 fmt =
746
    if !Options.integer_div_euclidean then
747
      (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
748
      Format.fprintf fmt
749
        "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
750
        pp_value v1 pp_value v2
751
        pp_value v1 pp_value v2
752
        pp_value v2
753
    else (* Ada behavior for rem *)
754
      Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
755

    
756
  (** Printing function for expressions [v1 div v2]. Depends on
757
      option [integer_div_euclidean] to choose between mathematic
758
      division or Ada division.
759

    
760
      @param pp_value pretty printer for values
761
      @param v1 the first value in the expression
762
      @param v2 the second value in the expression
763
      @param fmt the formater to print in
764
   **)
765
  let pp_div pp_value v1 v2 fmt =
766
    if !Options.integer_div_euclidean then
767
      (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
768
      Format.fprintf fmt "(%a - %t) / %a"
769
        pp_value v1
770
        (pp_mod pp_value v1 v2)
771
        pp_value v2
772
    else (* Ada behavior for / *)
773
      Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
774

    
775
  (** Printing function for basic lib functions.
776

    
777
      @param pp_value pretty printer for values
778
      @param i a string representing the function
779
      @param fmt the formater to print on
780
      @param vl the list of operands
781
   **)
782
  let pp_basic_lib_fun pp_value ident fmt vl =
783
    match ident, vl with
784
    | "uminus", [v]    ->
785
      Format.fprintf fmt "(- %a)" pp_value v
786
    | "not", [v]       ->
787
      Format.fprintf fmt "(not %a)" pp_value v
788
    | "impl", [v1; v2] ->
789
      Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
790
    | "=", [v1; v2]    ->
791
      Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
792
    | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
793
    | "equi", [v1; v2] ->
794
      Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
795
    | "xor", [v1; v2]  ->
796
      Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
797
    | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
798
    | "&&", [v1; v2]    ->
799
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
800
    | "||", [v1; v2]    ->
801
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
802
    | "!=", [v1; v2]    ->
803
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
804
    | op, [v1; v2]     ->
805
      Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
806
    | op, [v1] when  List.mem_assoc ident ada_supported_funs ->
807
      let pkg, name = try List.assoc ident ada_supported_funs
808
        with Not_found -> assert false in
809
      let pkg = pkg^(if String.equal pkg "" then "" else ".") in
810
        Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1
811
    | fun_name, _      ->
812
      (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
813

    
814
  (** Printing function for values.
815

    
816
      @param m the machine to know the state variable
817
      @param fmt the formater to use
818
      @param value the value to print. Should be a
819
             {!type:Machine_code_types.value_t} value
820
   **)
821
  let rec pp_value m fmt value =
822
    match value.value_desc with
823
    | Cst c             -> pp_ada_const fmt c
824
    | Var var      -> pp_access_var m fmt var
825
    | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value m) f_ident fmt vl
826
    | _                 ->
827
      raise (Ada_not_supported
828
               "unsupported: Ada_backend.adb.pp_value does not support this value type")
829

    
830

    
831
(** Print the filename of a machine package.
832
   @param extension the extension to append to the package name
833
   @param fmt the formatter
834
   @param machine the machine corresponding to the package
835
**)
836
let pp_machine_filename extension fmt machine =
837
  pp_filename extension fmt (function fmt -> pp_package_name fmt machine)
838

    
839
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
840

    
841
(** Extract from a machine the instance corresponding to the identifier,
842
      assume that the identifier exists in the instances of the machine.
843

    
844
   @param identifier the instance identifier
845
   @param machine a machine
846
   @return the instance of machine.minstances corresponding to identifier
847
**)
848
let get_instance identifier typed_submachines =
849
  try
850
    List.assoc identifier typed_submachines
851
  with Not_found -> assert false
852

    
853
(** Printing a call to a package function
854

    
855
    @param typed_submachines list of all typed machine instances of this machine
856
    @param pp_name printer for the function name
857
    @param fmt the formater to use
858
    @param identifier the instance identifier
859
    @param pp_args_opt optional printer for other arguments
860
 **)
861
let pp_package_call pp_name fmt (substitution, submachine, pp_state, pp_args_opt) =
862
  let statefull = is_machine_statefull submachine in
863
  let pp_opt fmt = function
864
      | Some pp_args when statefull -> fprintf fmt ",@,%t" pp_args
865
      | Some pp_args -> pp_args fmt
866
      | None -> fprintf fmt ""
867
  in
868
  let pp_state fmt =
869
    if statefull then
870
      pp_state fmt
871
    else
872
      fprintf fmt ""
873
  in
874
  fprintf fmt "%a.%t(@[<v>%t%a@])"
875
    (pp_package_name_with_polymorphic substitution) submachine
876
    pp_name
877
    pp_state
878
    pp_opt pp_args_opt
879