Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_common.ml @ 3de9f6e4

History | View | Annotate | Download (27.2 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 functions common to the ada backend **)
12

    
13
(* Misc pretty print functions *)
14

    
15

    
16
(** Print a cleaned an identifier for ada exportation : Ada names must not start by an
17
    underscore and must not contain a double underscore
18
   @param var name to be cleaned*)
19
let pp_clean_ada_identifier fmt name =
20
  let reserved_words = ["abort"; "else"; "new"; "return";
21
                        "abs"; "elsif"; "not"; "reverse"; "abstract"; "end";
22
                        "null"; "accept"; "entry"; "select"; "access";
23
                        "exception"; "of"; "separate"; "aliased"; "exit";
24
                        "or"; "some"; "all"; "others"; "subtype"; "and";
25
                        "for"; "out"; "synchronized"; "array"; "function";
26
                        "overriding"; "at"; "tagged"; "generic"; "package";
27
                        "task"; "begin"; "goto"; "pragma"; "terminate";
28
                        "body"; "private"; "then"; "if"; "procedure"; "type";
29
                        "case"; "in"; "protected"; "constant"; "interface";
30
                        "until"; "is"; "raise"; "use"; "declare"; "	range";
31
                        "delay"; "limited"; "record"; "when"; "delta"; "loop";
32
                        "rem"; "while"; "digits"; "renames"; "with"; "do";
33
                        "mod"; "requeue"; "xor"] in
34
  let base_size = String.length name in
35
  assert(base_size > 0);
36
  let rec remove_double_underscore s = function
37
    | i when i == String.length s - 1 -> s
38
    | i when String.get s i == '_' && String.get s (i+1) == '_' ->
39
        remove_double_underscore (sprintf "%s%s" (String.sub s 0 i) (String.sub s (i+1) (String.length s-i-1))) i
40
    | i -> remove_double_underscore s (i+1)
41
  in
42
  let name = if String.get name (base_size-1) == '_' then name^"ada" else name in
43
  let name = remove_double_underscore name 0 in
44
  let prefix = if String.length name != base_size
45
                  || String.get name 0 == '_' 
46
                  || List.exists (String.equal (String.lowercase_ascii name)) reserved_words then
47
                  "ada"
48
               else
49
                  ""
50
  in
51
  fprintf fmt "%s%s" prefix name
52

    
53
(** Encapsulate a pretty print function to lower case its result when applied
54
   @param pp the pretty print function
55
   @param fmt the formatter
56
   @param arg the argument of the pp function
57
**)
58
let pp_lowercase pp fmt =
59
  let str = asprintf "%t" pp in
60
  fprintf fmt "%s" (String. lowercase_ascii str)
61

    
62
(** Print a filename by lowercasing the base and appending an extension.
63
   @param extension the extension to append to the package name
64
   @param fmt the formatter
65
   @param pp_name the file base name printer
66
**)
67
let pp_filename extension fmt pp_name =
68
  fprintf fmt "%t.%s"
69
    (pp_lowercase pp_name)
70
    extension
71

    
72

    
73
(* Package pretty print functions *)
74

    
75
(** Print the name of the arrow package.
76
   @param fmt the formater to print on
77
**)
78
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
79

    
80
(** Print the name of a package associated to a node.
81
   @param fmt the formater to print on
82
   @param machine the machine
83
**)
84
let pp_package_name_from_node fmt node =
85
  if String.equal Arrow.arrow_id node.node_id then
86
      fprintf fmt "%t" pp_arrow_package_name
87
  else
88
      fprintf fmt "%a" pp_clean_ada_identifier node.node_id
89

    
90
(** Print the name of a package associated to a machine.
91
   @param fmt the formater to print on
92
   @param machine the machine
93
**)
94
let pp_package_name fmt machine =
95
  pp_package_name_from_node fmt machine.mname
96

    
97
(** Print the ada package introduction sentence it can be used for body and
98
declaration. Boolean parameter body should be true if it is a body delcaration.
99
   @param fmt the formater to print on
100
   @param fmt the formater to print on
101
   @param machine the machine
102
**)
103
let pp_begin_package body fmt machine =
104
  fprintf fmt "package %s%a is"
105
    (if body then "body " else "")
106
    pp_package_name machine
107

    
108
(** Print the ada package conclusion sentence.
109
   @param fmt the formater to print on
110
   @param machine the machine
111
**)
112
let pp_end_package fmt machine =
113
  fprintf fmt "end %a" pp_package_name machine
114

    
115
(** Print the access of an item from an other package.
116
   @param fmt the formater to print on
117
   @param package the package to use
118
   @param item the item which is accessed
119
**)
120
let pp_package_access fmt (package, item) =
121
  fprintf fmt "%t.%t" package item
122

    
123
(** Print the name of the main procedure.
124
   @param fmt the formater to print on
125
**)
126
let pp_main_procedure_name fmt =
127
  fprintf fmt "ada_main"
128

    
129
(** Print a with statement to include a package.
130
   @param fmt the formater to print on
131
   @param pp_pakage_name the package name printer
132
**)
133
let pp_private_with fmt pp_pakage_name =
134
  fprintf fmt "private with %t" pp_pakage_name
135

    
136
(** Print a with statement to include a machine.
137
   @param fmt the formater to print on
138
   @param machine the machine
139
**)
140
let pp_with_machine fmt machine =
141
  fprintf fmt "private with %a" pp_package_name machine
142

    
143
(** Extract a node from an instance.
144
   @param instance the instance
145
**)
146
let extract_node instance =
147
  let (_, (node, _)) = instance in
148
  match node.top_decl_desc with
149
    | Node nd         -> nd
150
    | _ -> assert false (*TODO*)
151

    
152
(** Extract from a machine list the one corresponding to the given instance.
153
      assume that the machine is in the list.
154
   @param machines list of all machines
155
   @param instance instance of a machine
156
   @return the machine corresponding to hte given instance
157
**)
158
let get_machine machines instance =
159
    let id = (extract_node instance).node_id in
160
    try
161
      List.find (function m -> m.mname.node_id=id) machines
162
    with
163
      Not_found -> assert false
164

    
165

    
166
(* Type pretty print functions *)
167

    
168
(** Print a type declaration
169
   @param fmt the formater to print on
170
   @param pp_name a format printer which print the type name
171
   @param pp_value a format printer which print the type definition
172
**)
173
let pp_type_decl fmt (pp_name, pp_definition) =
174
  fprintf fmt "type %t is %t" pp_name pp_definition
175

    
176
(** Print a limited private type declaration
177
   @param fmt the formater to print on
178
   @param pp_name a format printer which print the type name
179
**)
180
let pp_private_limited_type_decl fmt pp_name =
181
  let pp_definition fmt = fprintf fmt "limited private" in
182
  pp_type_decl fmt (pp_name, pp_definition)
183

    
184
(** Print the type of the state variable.
185
   @param fmt the formater to print on
186
**)
187
let pp_state_type fmt =
188
  (* Type and variable names live in the same environement in Ada so name of
189
     this type and of the associated parameter : pp_state_name must be
190
     different *)
191
  fprintf fmt "TState"
192

    
193
(** Print the integer type name.
194
   @param fmt the formater to print on
195
**)
196
let pp_integer_type fmt = fprintf fmt "Integer"
197

    
198
(** Print the float type name.
199
   @param fmt the formater to print on
200
**)
201
let pp_float_type fmt = fprintf fmt "Float"
202

    
203
(** Print the boolean type name.
204
   @param fmt the formater to print on
205
**)
206
let pp_boolean_type fmt = fprintf fmt "Boolean"
207

    
208
(** Print the type of a polymorphic type.
209
   @param fmt the formater to print on
210
   @param id the id of the polymorphic type
211
**)
212
let pp_polymorphic_type fmt id =
213
  fprintf fmt "T_%i" id
214

    
215
(** Print a type.
216
   @param fmt the formater to print on
217
   @param type the type
218
**)
219
let pp_type fmt typ = 
220
  (match (Types.repr typ).Types.tdesc with
221
    | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
222
    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
223
    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
224
    | Types.Tunivar _                -> pp_polymorphic_type fmt typ.tid
225
    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
226
    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
227
    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
228
    | Types.Tarrow _                 -> eprintf "Tarrow@."; assert false (*TODO*)
229
    | Types.Ttuple l                 -> eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; assert false (*TODO*)
230
    | Types.Tenum _                  -> eprintf "Tenum@.";  assert false (*TODO*)
231
    | Types.Tstruct _                -> eprintf "Tstruct@.";assert false (*TODO*)
232
    | Types.Tarray _                 -> eprintf "Tarray@."; assert false (*TODO*)
233
    | Types.Tstatic _                -> eprintf "Tstatic@.";assert false (*TODO*)
234
    | Types.Tlink _                  -> eprintf "Tlink@.";  assert false (*TODO*)
235
    | Types.Tvar _                   -> eprintf "Tvar@.";   assert false (*TODO*)
236
    | _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false (*TODO*)
237
  )
238

    
239

    
240
(** Test if two types are the same.
241
   @param typ1 the first type
242
   @param typ2 the second type
243
**)
244
let pp_eq_type typ1 typ2 = 
245
  let get_basic typ = match (Types.repr typ).Types.tdesc with
246
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
247
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
248
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
249
    | _ -> assert false (*TODO*)
250
  in
251
  get_basic typ1 = get_basic typ2
252

    
253

    
254
(** Print the type of a variable.
255
   @param fmt the formater to print on
256
   @param id the variable
257
**)
258
let pp_var_type fmt id = 
259
  pp_type fmt id.var_type
260

    
261
(** Extract all the inputs and outputs.
262
   @param machine the machine
263
   @return a list of all the var_decl of a macine
264
**)
265
let get_all_vars_machine m =
266
  m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic
267

    
268
(** Check if a type is polymorphic.
269
   @param typ the type
270
   @return true if its polymorphic
271
**)
272
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar
273

    
274
(** Find all polymorphic type : Types.Tunivar in a machine.
275
   @param machine the machine
276
   @return a list of id corresponding to polymorphic type
277
**)
278
let find_all_polymorphic_type m =
279
  let vars = get_all_vars_machine m in
280
  let extract id = id.var_type.tid in
281
  let polymorphic_type_vars =
282
    List.filter (function x-> is_Tunivar x.var_type) vars in
283
  List.sort_uniq (-) (List.map extract polymorphic_type_vars)
284

    
285
(** Print a package name with polymorphic types specified.
286
   @param substitution correspondance between polymorphic type id and their instantiation
287
   @param fmt the formater to print on
288
   @param machine the machine
289
**)
290
let pp_package_name_with_polymorphic substitution fmt machine =
291
  let polymorphic_types = find_all_polymorphic_type machine in
292
  assert(List.length polymorphic_types = List.length substitution);
293
  let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
294
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
295
            polymorphic_types substituion);
296
  let instantiated_types = snd (List.split substitution) in
297
  fprintf fmt "%a%t%a"
298
    pp_package_name machine
299
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
300
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
301

    
302

    
303
(* Variable pretty print functions *)
304

    
305
(** Represent the possible mode for a type of a procedure parameter **)
306
type parameter_mode = NoMode | In | Out | InOut
307

    
308
(** Print a parameter_mode.
309
   @param fmt the formater to print on
310
   @param mode the modifier
311
**)
312
let pp_parameter_mode fmt mode =
313
  fprintf fmt "%s" (match mode with
314
                     | NoMode -> ""
315
                     | In     -> "in"
316
                     | Out    -> "out"
317
                     | InOut  -> "in out")
318

    
319
(** Print the name of the state variable.
320
   @param fmt the formater to print on
321
**)
322
let pp_state_name fmt =
323
  fprintf fmt "state"
324

    
325

    
326
(** Print the name of a variable.
327
   @param fmt the formater to print on
328
   @param id the variable
329
**)
330
let pp_var_name fmt id =
331
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
332

    
333
(** Print the complete name of variable.
334
   @param m the machine to check if it is memory
335
   @param fmt the formater to print on
336
   @param var the variable
337
**)
338
let pp_access_var m fmt var =
339
  if is_memory m var then
340
    fprintf fmt "%t.%a" pp_state_name pp_var_name var
341
  else
342
    pp_var_name fmt var
343

    
344
(** Print a variable declaration
345
   @param mode input/output mode of the parameter
346
   @param pp_name a format printer wich print the variable name
347
   @param pp_type a format printer wich print the variable type
348
   @param fmt the formater to print on
349
   @param id the variable
350
**)
351
let pp_var_decl fmt (mode, pp_name, pp_type) =
352
  fprintf fmt "%t: %a%s%t"
353
    pp_name
354
    pp_parameter_mode mode
355
    (if mode = NoMode then "" else " ")
356
    pp_type
357

    
358
(** Print variable declaration for machine variable
359
   @param mode input/output mode of the parameter
360
   @param fmt the formater to print on
361
   @param id the variable
362
**)
363
let pp_machine_var_decl mode fmt id =
364
  let pp_name = function fmt -> pp_var_name fmt id in
365
  let pp_type = function fmt -> pp_var_type fmt id in
366
  pp_var_decl fmt (mode, pp_name, pp_type)
367

    
368
(** Print variable declaration for a local state variable
369
   @param fmt the formater to print on
370
   @param mode input/output mode of the parameter
371
**)
372
let pp_state_var_decl fmt mode =
373
  let pp_name = pp_state_name in
374
  let pp_type = pp_state_type in
375
  pp_var_decl fmt (mode, pp_name, pp_type)
376

    
377
(** Print the declaration of a state element of a machine.
378
   @param substitution correspondance between polymorphic type id and their instantiation
379
   @param name name of the variable
380
   @param fmt the formater to print on
381
   @param machine the machine
382
**)
383
let pp_node_state_decl substitution name fmt machine =
384
  let pp_package fmt = pp_package_name_with_polymorphic substitution fmt machine in
385
  let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
386
  let pp_name fmt = pp_clean_ada_identifier fmt name in
387
  pp_var_decl fmt (NoMode, pp_name, pp_type)
388

    
389

    
390
(* Prototype pretty print functions *)
391

    
392
(** Print the name of the reset procedure **)
393
let pp_reset_procedure_name fmt = fprintf fmt "reset"
394

    
395
(** Print the name of the step procedure **)
396
let pp_step_procedure_name fmt = fprintf fmt "step"
397

    
398
(** Print the name of the init procedure **)
399
let pp_init_procedure_name fmt = fprintf fmt "init"
400

    
401
(** Print the name of the clear procedure **)
402
let pp_clear_procedure_name fmt = fprintf fmt "clear"
403

    
404
(** Print the prototype of a procedure with non input/outputs
405
   @param fmt the formater to print on
406
   @param name the name of the procedure
407
**)
408
let pp_simple_prototype pp_name fmt =
409
  fprintf fmt "procedure %t" pp_name
410

    
411
(** Print the prototype of a machine procedure. The first parameter is always
412
the state, state_modifier specify the modifier applying to it. The next
413
parameters are inputs and the last parameters are the outputs.
414
   @param state_mode the input/output mode for the state parameter
415
   @param input list of the input parameter of the procedure
416
   @param output list of the output parameter of the procedure
417
   @param fmt the formater to print on
418
   @param name the name of the procedure
419
**)
420
let pp_base_prototype state_mode input output fmt pp_name =
421
  fprintf fmt "procedure %t(@[<v>%a%t@[%a@]%t@[%a@])@]"
422
    pp_name
423
    pp_state_var_decl state_mode
424
    (Utils.pp_final_char_if_non_empty ";@," input)
425
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl In)) input
426
    (Utils.pp_final_char_if_non_empty ";@," output)
427
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl Out)) output
428

    
429
(** Print the prototype of the step procedure of a machine.
430
   @param m the machine
431
   @param fmt the formater to print on
432
   @param pp_name name function printer
433
**)
434
let pp_step_prototype m fmt =
435
  pp_base_prototype InOut m.mstep.step_inputs m.mstep.step_outputs fmt pp_step_procedure_name
436

    
437
(** Print the prototype of the reset procedure of a machine.
438
   @param m the machine
439
   @param fmt the formater to print on
440
   @param pp_name name function printer
441
**)
442
let pp_reset_prototype m fmt =
443
  pp_base_prototype InOut m.mstatic [] fmt pp_reset_procedure_name
444

    
445
(** Print the prototype of the init procedure of a machine.
446
   @param m the machine
447
   @param fmt the formater to print on
448
   @param pp_name name function printer
449
**)
450
let pp_init_prototype m fmt =
451
  pp_base_prototype Out m.mstatic [] fmt pp_init_procedure_name
452

    
453
(** Print the prototype of the clear procedure of a machine.
454
   @param m the machine
455
   @param fmt the formater to print on
456
   @param pp_name name function printer
457
**)
458
let pp_clear_prototype m fmt =
459
  pp_base_prototype InOut m.mstatic [] fmt pp_clear_procedure_name
460

    
461
(** Print a one line comment with the final new line character to avoid
462
      commenting anything else.
463
   @param fmt the formater to print on
464
   @param s the comment without newline character
465
**)
466
let pp_oneline_comment fmt s =
467
  assert (not (String.contains s '\n'));
468
  fprintf fmt "-- %s@," s
469

    
470
(* Functions which computes the substitution for polymorphic type *)
471
(** Find a submachine step call in a list of instructions.
472
    @param ident submachine instance ident
473
    @param instr_list List of instruction sto search
474
    @return a list of pair containing input types and output types for each step call found
475
**)
476
let rec find_submachine_step_call ident instr_list =
477
  let search_instr instruction = 
478
    match instruction.instr_desc with
479
      | MStep (il, i, vl) when String.equal i ident -> [
480
        (List.map (function x-> x.value_type) vl,
481
            List.map (function x-> x.var_type) il)]
482
      | MBranch (_, l) -> List.flatten
483
          (List.map (function x, y -> find_submachine_step_call ident y) l)
484
      | _ -> []
485
  in
486
  List.flatten (List.map search_instr instr_list)
487

    
488
(** Check that two types are the same.
489
   @param t1 a type
490
   @param t2 an other type
491
   @param return true if the two types are Tbasic or Tunivar and equal
492
**)
493
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
494
  match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
495
    | Types.Tbasic x, Types.Tbasic y -> x = y
496
    | Types.Tunivar,  Types.Tunivar  -> t1.tid = t2.tid
497
    | Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
498
    | _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
499
    | Types.Tstatic (_, t), _ -> check_type_equal t t2
500
    | _, Types.Tstatic (_, t) -> check_type_equal t1 t
501
    | _ -> eprintf "ERROR: %a | %a" pp_type t1 pp_type t2; assert false (* TODO *)
502

    
503
(** Extend a substitution to unify the two given types. Only the
504
  first type can be polymorphic.
505
    @param subsitution the base substitution
506
    @param type_poly the type which can be polymorphic
507
    @param typ the type to match type_poly with
508
**)
509
let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) =
510
  assert(not (is_Tunivar typ));
511
  (* If type_poly is polymorphic *)
512
  if is_Tunivar type_poly then
513
    (* If a subsitution exists for it *)
514
    if List.mem_assoc type_poly.tid substituion then
515
    begin
516
      (* We check that the type corresponding to type_poly in the subsitution
517
         match typ *)
518
      (try
519
        assert(check_type_equal (List.assoc type_poly.tid substituion) typ)
520
      with
521
        Not_found -> assert false);
522
      (* We return the original substituion, it is already correct *)
523
      substituion
524
    end
525
    (* If type_poly is not in the subsitution *)
526
    else
527
      (* We add it to the substituion *)
528
      (type_poly.tid, typ)::substituion
529
  (* iftype_poly is not polymorphic *)
530
  else
531
  begin
532
    (* We check that type_poly and typ are the same *)
533
    assert(check_type_equal type_poly typ);
534
    (* We return the original substituion, it is already correct *)
535
    substituion
536
  end
537

    
538
(** Check that two calls are equal. A call is
539
  a pair of list of types, the inputs and the outputs.
540
   @param calls a list of pair of list of types
541
   @param return true if the two pairs are equal
542
**)
543
let check_call_equal (i1, o1) (i2, o2) =
544
  (List.for_all2 check_type_equal i1 i2)
545
    && (List.for_all2 check_type_equal i1 i2)
546

    
547
(** Check that all the elements of list of calls are equal to one.
548
  A call is a pair of list of types, the inputs and the outputs.
549
   @param call a pair of list of types
550
   @param calls a list of pair of list of types
551
   @param return true if all the elements are equal
552
**)
553
let check_calls call calls =
554
  List.for_all (check_call_equal call) calls
555

    
556
(** Extract from a subinstance that can have polymorphic type the instantiation
557
    of all its polymorphic type instanciation for a given machine. It searches
558
    the step calls and extract a substitution for all polymorphic type from
559
    it.
560
   @param machine the machine which instantiate the subinstance
561
   @param ident the identifier of the instance which permits to find the step call
562
   @param submachine the machine corresponding to the subinstance
563
   @return the correspondance between polymorphic type id and their instantiation
564
**)
565
let get_substitution machine ident submachine =
566
  (* extract the calls to submachines from the machine *)
567
  let calls = find_submachine_step_call ident machine.mstep.step_instrs in
568
  (* extract the first call  *)
569
  let call = match calls with
570
              (* assume that there is always one call to a subinstance *)
571
              | []    -> assert(false)
572
              | h::t  -> h in
573
  (* assume that all the calls to a subinstance are using the same type *)
574
  assert(check_calls call calls);
575
  (* make a list of all types from input and output vars *)
576
  let call_types = (fst call)@(snd call) in
577
  (* extract all the input and output vars from the submachine *)
578
  let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in
579
  (* keep only the type of vars *)
580
  let machine_types = List.map (function x-> x.var_type) machine_vars in
581
  (* assume that there is the same numer of input and output in the submachine
582
      and the call *)
583
  assert (List.length machine_types = List.length call_types);
584
  (* Unify the two lists of types *)
585
  let substitution = List.fold_left unification [] (List.combine machine_types call_types) in
586
  (* Assume that our substitution match all the possible
587
       polymorphic type of the node *)
588
  let polymorphic_types = find_all_polymorphic_type submachine in
589
  assert (List.length polymorphic_types = List.length substitution);
590
  (try
591
    assert (List.for_all (fun x -> List.mem_assoc x substitution) polymorphic_types)
592
  with
593
    Not_found -> assert false);
594
  substitution
595

    
596

    
597
(* Procedure pretty print functions *)
598

    
599
(** Print the definition of a procedure
600
   @param pp_name the procedure name printer
601
   @param pp_prototype the prototype printer
602
   @param pp_instr local var printer
603
   @param pp_instr instruction printer
604
   @param fmt the formater to print on
605
   @param locals locals var list
606
   @param instrs instructions list
607
**)
608
let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals, instrs) =
609
  fprintf fmt "@[<v>%t is%t@[<v>%a%t@]@,begin@,  @[<v>%a%t@]@,end %t@]"
610
    pp_prototype
611
    (Utils.pp_final_char_if_non_empty "@,  " locals)
612
    (Utils.fprintf_list ~sep:";@," pp_local) locals
613
    (Utils.pp_final_char_if_non_empty ";" locals)
614
    (Utils.fprintf_list ~sep:";@," pp_instr) instrs
615
    (Utils.pp_final_char_if_non_empty ";" instrs)
616
    pp_name
617

    
618

    
619
(* Expression print functions *)
620

    
621
  (* Printing functions for basic operations and expressions *)
622
  (* TODO: refactor code -> use let rec and for basic pretty printing
623
     function *)
624
  (** Printing function for Ada tags, mainly booleans.
625

    
626
      @param fmt the formater to use
627
      @param t the tag to print
628
   **)
629
  let pp_ada_tag fmt t =
630
    pp_print_string fmt
631
      (if t = tag_true then "True" else if t = tag_false then "False" else t)
632

    
633
  (** Printing function for machine type constants. For the moment,
634
      arrays are not supported.
635

    
636
      @param fmt the formater to use
637
      @param c the constant to print
638
   **)
639
  let pp_ada_const fmt c =
640
    match c with
641
    | Const_int i                     -> pp_print_int fmt i
642
    | Const_real (c, e, s)            -> pp_print_string fmt s
643
    | Const_tag t                     -> pp_ada_tag fmt t
644
    | Const_string _ | Const_modeid _ ->
645
      (Format.eprintf
646
         "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
647
       assert false)
648
    | _                               ->
649
      raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
650
      support this constant")
651

    
652
  (** Printing function for expressions [v1 modulo v2]. Depends
653
      on option [integer_div_euclidean] to choose between mathematical
654
      modulo or remainder ([rem] in Ada).
655

    
656
      @param pp_value pretty printer for values
657
      @param v1 the first value in the expression
658
      @param v2 the second value in the expression
659
      @param fmt the formater to print on
660
   **)
661
  let pp_mod pp_value v1 v2 fmt =
662
    if !Options.integer_div_euclidean then
663
      (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
664
      Format.fprintf fmt
665
        "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
666
        pp_value v1 pp_value v2
667
        pp_value v1 pp_value v2
668
        pp_value v2
669
    else (* Ada behavior for rem *)
670
      Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
671

    
672
  (** Printing function for expressions [v1 div v2]. Depends on
673
      option [integer_div_euclidean] to choose between mathematic
674
      division or Ada division.
675

    
676
      @param pp_value pretty printer for values
677
      @param v1 the first value in the expression
678
      @param v2 the second value in the expression
679
      @param fmt the formater to print in
680
   **)
681
  let pp_div pp_value v1 v2 fmt =
682
    if !Options.integer_div_euclidean then
683
      (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
684
      Format.fprintf fmt "(%a - %t) / %a"
685
        pp_value v1
686
        (pp_mod pp_value v1 v2)
687
        pp_value v2
688
    else (* Ada behavior for / *)
689
      Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
690

    
691
  (** Printing function for basic lib functions.
692

    
693
      @param pp_value pretty printer for values
694
      @param i a string representing the function
695
      @param fmt the formater to print on
696
      @param vl the list of operands
697
   **)
698
  let pp_basic_lib_fun pp_value ident fmt vl =
699
    match ident, vl with
700
    | "uminus", [v]    ->
701
      Format.fprintf fmt "(- %a)" pp_value v
702
    | "not", [v]       ->
703
      Format.fprintf fmt "(not %a)" pp_value v
704
    | "impl", [v1; v2] ->
705
      Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
706
    | "=", [v1; v2]    ->
707
      Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
708
    | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
709
    | "equi", [v1; v2] ->
710
      Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
711
    | "xor", [v1; v2]  ->
712
      Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
713
    | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
714
    | "&&", [v1; v2]    ->
715
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
716
    | "||", [v1; v2]    ->
717
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
718
    | "!=", [v1; v2]    ->
719
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
720
    | op, [v1; v2]     ->
721
      Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
722
    | fun_name, _      ->
723
      (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
724

    
725
  (** Printing function for values.
726

    
727
      @param m the machine to know the state variable
728
      @param fmt the formater to use
729
      @param value the value to print. Should be a
730
             {!type:Machine_code_types.value_t} value
731
   **)
732
  let rec pp_value m fmt value =
733
    match value.value_desc with
734
    | Cst c             -> pp_ada_const fmt c
735
    | Var var      -> pp_access_var m fmt var
736
    | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value m) f_ident fmt vl
737
    | _                 ->
738
      raise (Ada_not_supported
739
               "unsupported: Ada_backend.adb.pp_value does not support this value type")