Project

General

Profile

Download (26.2 KB) Statistics
| Branch: | Tag: | Revision:
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
   @param machines list of all machines
154
   @param instance instance of a machine
155
   @return the machine corresponding to hte given instance
156
**)
157
let get_machine machines instance =
158
    let id = (extract_node instance).node_id in
159
    List.find  (function m -> m.mname.node_id=id) machines
160

    
161

    
162
(* Type pretty print functions *)
163

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

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

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

    
189
(** Print the integer type name.
190
   @param fmt the formater to print on
191
**)
192
let pp_integer_type fmt = fprintf fmt "Integer"
193

    
194
(** Print the float type name.
195
   @param fmt the formater to print on
196
**)
197
let pp_float_type fmt = fprintf fmt "Float"
198

    
199
(** Print the boolean type name.
200
   @param fmt the formater to print on
201
**)
202
let pp_boolean_type fmt = fprintf fmt "Boolean"
203

    
204
(** Print the type of a polymorphic type.
205
   @param fmt the formater to print on
206
   @param id the id of the polymorphic type
207
**)
208
let pp_polymorphic_type fmt id =
209
  fprintf fmt "T_%i" id
210

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

    
234
(** Print the type of a variable.
235
   @param fmt the formater to print on
236
   @param id the variable
237
**)
238
let pp_var_type fmt id = 
239
  pp_type fmt id.var_type
240

    
241
(** Extract all the inputs and outputs.
242
   @param machine the machine
243
   @return a list of all the var_decl of a macine
244
**)
245
let get_all_vars_machine m =
246
  m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic
247

    
248
(** Check if a type is polymorphic.
249
   @param typ the type
250
   @return true if its polymorphic
251
**)
252
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar
253

    
254
(** Find all polymorphic type : Types.Tunivar in a machine.
255
   @param machine the machine
256
   @return a list of id corresponding to polymorphic type
257
**)
258
let find_all_polymorphic_type m =
259
  let vars = get_all_vars_machine m in
260
  let extract id = id.var_type.tid in
261
  let polymorphic_type_vars =
262
    List.filter (function x-> is_Tunivar x.var_type) vars in
263
  List.sort_uniq (-) (List.map extract polymorphic_type_vars)
264

    
265
(** Print a package name with polymorphic types specified.
266
   @param substitution correspondance between polymorphic type id and their instantiation
267
   @param fmt the formater to print on
268
   @param machine the machine
269
**)
270
let pp_package_name_with_polymorphic substitution fmt machine =
271
  let polymorphic_types = find_all_polymorphic_type machine in
272
  assert(List.length polymorphic_types = List.length substitution);
273
  let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
274
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
275
            polymorphic_types substituion);
276
  let instantiated_types = snd (List.split substitution) in
277
  fprintf fmt "%a%t%a"
278
    pp_package_name machine
279
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
280
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
281

    
282

    
283
(* Variable pretty print functions *)
284

    
285
(** Represent the possible mode for a type of a procedure parameter **)
286
type parameter_mode = NoMode | In | Out | InOut
287

    
288
(** Print a parameter_mode.
289
   @param fmt the formater to print on
290
   @param mode the modifier
291
**)
292
let pp_parameter_mode fmt mode =
293
  fprintf fmt "%s" (match mode with
294
                     | NoMode -> ""
295
                     | In     -> "in"
296
                     | Out    -> "out"
297
                     | InOut  -> "in out")
298

    
299
(** Print the name of the state variable.
300
   @param fmt the formater to print on
301
**)
302
let pp_state_name fmt =
303
  fprintf fmt "state"
304

    
305

    
306
(** Print the name of a variable.
307
   @param fmt the formater to print on
308
   @param id the variable
309
**)
310
let pp_var_name fmt id =
311
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
312

    
313
(** Print the complete name of variable.
314
   @param m the machine to check if it is memory
315
   @param fmt the formater to print on
316
   @param var the variable
317
**)
318
let pp_access_var m fmt var =
319
  if is_memory m var then
320
    fprintf fmt "%t.%a" pp_state_name pp_var_name var
321
  else
322
    pp_var_name fmt var
323

    
324
(** Print a variable declaration
325
   @param mode input/output mode of the parameter
326
   @param pp_name a format printer wich print the variable name
327
   @param pp_type a format printer wich print the variable type
328
   @param fmt the formater to print on
329
   @param id the variable
330
**)
331
let pp_var_decl fmt (mode, pp_name, pp_type) =
332
  fprintf fmt "%t: %a%s%t"
333
    pp_name
334
    pp_parameter_mode mode
335
    (if mode = NoMode then "" else " ")
336
    pp_type
337

    
338
(** Print variable declaration for machine variable
339
   @param mode input/output mode of the parameter
340
   @param fmt the formater to print on
341
   @param id the variable
342
**)
343
let pp_machine_var_decl mode fmt id =
344
  let pp_name = function fmt -> pp_var_name fmt id in
345
  let pp_type = function fmt -> pp_var_type fmt id in
346
  pp_var_decl fmt (mode, pp_name, pp_type)
347

    
348
(** Print variable declaration for a local state variable
349
   @param fmt the formater to print on
350
   @param mode input/output mode of the parameter
351
**)
352
let pp_state_var_decl fmt mode =
353
  let pp_name = pp_state_name in
354
  let pp_type = pp_state_type in
355
  pp_var_decl fmt (mode, pp_name, pp_type)
356

    
357
(** Print the declaration of a state element of a machine.
358
   @param substitution correspondance between polymorphic type id and their instantiation
359
   @param name name of the variable
360
   @param fmt the formater to print on
361
   @param machine the machine
362
**)
363
let pp_node_state_decl substitution name fmt machine =
364
  let pp_package fmt = pp_package_name_with_polymorphic substitution fmt machine in
365
  let pp_type fmt = pp_package_access fmt (pp_package, pp_state_type) in
366
  let pp_name fmt = pp_clean_ada_identifier fmt name in
367
  pp_var_decl fmt (NoMode, pp_name, pp_type)
368

    
369

    
370
(* Prototype pretty print functions *)
371

    
372
(** Print the name of the reset procedure **)
373
let pp_reset_procedure_name fmt = fprintf fmt "reset"
374

    
375
(** Print the name of the step procedure **)
376
let pp_step_procedure_name fmt = fprintf fmt "step"
377

    
378
(** Print the name of the init procedure **)
379
let pp_init_procedure_name fmt = fprintf fmt "init"
380

    
381
(** Print the name of the clear procedure **)
382
let pp_clear_procedure_name fmt = fprintf fmt "clear"
383

    
384
(** Print the prototype of a procedure with non input/outputs
385
   @param fmt the formater to print on
386
   @param name the name of the procedure
387
**)
388
let pp_simple_prototype pp_name fmt =
389
  fprintf fmt "procedure %t" pp_name
390

    
391
(** Print the prototype of a machine procedure. The first parameter is always
392
the state, state_modifier specify the modifier applying to it. The next
393
parameters are inputs and the last parameters are the outputs.
394
   @param state_mode the input/output mode for the state parameter
395
   @param input list of the input parameter of the procedure
396
   @param output list of the output parameter of the procedure
397
   @param fmt the formater to print on
398
   @param name the name of the procedure
399
**)
400
let pp_base_prototype state_mode input output fmt pp_name =
401
  fprintf fmt "procedure %t(@[<v>%a%t@[%a@]%t@[%a@])@]"
402
    pp_name
403
    pp_state_var_decl state_mode
404
    (Utils.pp_final_char_if_non_empty ";@," input)
405
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl In)) input
406
    (Utils.pp_final_char_if_non_empty ";@," output)
407
    (Utils.fprintf_list ~sep:";@ " (pp_machine_var_decl Out)) output
408

    
409
(** Print the prototype of the step procedure of a machine.
410
   @param m the machine
411
   @param fmt the formater to print on
412
   @param pp_name name function printer
413
**)
414
let pp_step_prototype m fmt =
415
  pp_base_prototype InOut m.mstep.step_inputs m.mstep.step_outputs fmt pp_step_procedure_name
416

    
417
(** Print the prototype of the reset procedure of a machine.
418
   @param m the machine
419
   @param fmt the formater to print on
420
   @param pp_name name function printer
421
**)
422
let pp_reset_prototype m fmt =
423
  pp_base_prototype InOut m.mstatic [] fmt pp_reset_procedure_name
424

    
425
(** Print the prototype of the init procedure of a machine.
426
   @param m the machine
427
   @param fmt the formater to print on
428
   @param pp_name name function printer
429
**)
430
let pp_init_prototype m fmt =
431
  pp_base_prototype Out m.mstatic [] fmt pp_init_procedure_name
432

    
433
(** Print the prototype of the clear procedure of a machine.
434
   @param m the machine
435
   @param fmt the formater to print on
436
   @param pp_name name function printer
437
**)
438
let pp_clear_prototype m fmt =
439
  pp_base_prototype InOut m.mstatic [] fmt pp_clear_procedure_name
440

    
441

    
442
(* Functions which computes the substitution for polymorphic type *)
443
(** Find a submachine step call in a list of instructions.
444
    @param ident submachine instance ident
445
    @param instr_list List of instruction sto search
446
    @return a list of pair containing input types and output types for each step call found
447
**)
448
let rec find_submachine_step_call ident instr_list =
449
  let search_instr instruction = 
450
    match instruction.instr_desc with
451
      | MStep (il, i, vl) when String.equal i ident -> [
452
        (List.map (function x-> x.value_type) vl,
453
            List.map (function x-> x.var_type) il)]
454
      | MBranch (_, l) -> List.flatten
455
          (List.map (function x, y -> find_submachine_step_call ident y) l)
456
      | _ -> []
457
  in
458
  List.flatten (List.map search_instr instr_list)
459

    
460
(** Check that two types are the same.
461
   @param t1 a type
462
   @param t2 an other type
463
   @param return true if the two types are Tbasic or Tunivar and equal
464
**)
465
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
466
  match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
467
    | Types.Tbasic x, Types.Tbasic y -> x = y
468
    | Types.Tunivar,  Types.Tunivar  -> t1.tid = t2.tid
469
    | Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
470
    | _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
471
    | Types.Tstatic (_, t), _ -> check_type_equal t t2
472
    | _, Types.Tstatic (_, t) -> check_type_equal t1 t
473
    | _ -> eprintf "ERROR: %a | %a" pp_type t1 pp_type t2; assert false (* TODO *)
474

    
475
(** Extend a substitution to unify the two given types. Only the
476
  first type can be polymorphic.
477
    @param subsitution the base substitution
478
    @param type_poly the type which can be polymorphic
479
    @param typ the type to match type_poly with
480
**)
481
let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) =
482
  assert(not (is_Tunivar typ));
483
  (* If type_poly is polymorphic *)
484
  if is_Tunivar type_poly then
485
    (* If a subsitution exists for it *)
486
    if List.mem_assoc type_poly.tid substituion then
487
    begin
488
      (* We check that the type corresponding to type_poly in the subsitution
489
         match typ *)
490
      assert(check_type_equal (List.assoc type_poly.tid substituion) typ);
491
      (* We return the original substituion, it is already correct *)
492
      substituion
493
    end
494
    (* If type_poly is not in the subsitution *)
495
    else
496
      (* We add it to the substituion *)
497
      (type_poly.tid, typ)::substituion
498
  (* iftype_poly is not polymorphic *)
499
  else
500
  begin
501
    (* We check that type_poly and typ are the same *)
502
    assert(check_type_equal type_poly typ);
503
    (* We return the original substituion, it is already correct *)
504
    substituion
505
  end
506

    
507
(** Check that two calls are equal. A call is
508
  a pair of list of types, the inputs and the outputs.
509
   @param calls a list of pair of list of types
510
   @param return true if the two pairs are equal
511
**)
512
let check_call_equal (i1, o1) (i2, o2) =
513
  (List.for_all2 check_type_equal i1 i2)
514
    && (List.for_all2 check_type_equal i1 i2)
515

    
516
(** Check that all the elements of list of calls are equal to one.
517
  A call is a pair of list of types, the inputs and the outputs.
518
   @param call a pair of list of types
519
   @param calls a list of pair of list of types
520
   @param return true if all the elements are equal
521
**)
522
let check_calls call calls =
523
  List.for_all (check_call_equal call) calls
524

    
525
(** Extract from a subinstance that can have polymorphic type the instantiation
526
    of all its polymorphic type instanciation for a given machine. It searches
527
    the step calls and extract a substitution for all polymorphic type from
528
    it.
529
   @param machine the machine which instantiate the subinstance
530
   @param ident the identifier of the instance which permits to find the step call
531
   @param submachine the machine corresponding to the subinstance
532
   @return the correspondance between polymorphic type id and their instantiation
533
**)
534
let get_substitution machine ident submachine =
535
  (* extract the calls to submachines from the machine *)
536
  let calls = find_submachine_step_call ident machine.mstep.step_instrs in
537
  (* extract the first call  *)
538
  let call = match calls with
539
              (* assume that there is always one call to a subinstance *)
540
              | []    -> assert(false)
541
              | h::t  -> h in
542
  (* assume that all the calls to a subinstance are using the same type *)
543
  assert(check_calls call calls);
544
  (* make a list of all types from input and output vars *)
545
  let call_types = (fst call)@(snd call) in
546
  (* extract all the input and output vars from the submachine *)
547
  let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in
548
  (* keep only the type of vars *)
549
  let machine_types = List.map (function x-> x.var_type) machine_vars in
550
  (* assume that there is the same numer of input and output in the submachine
551
      and the call *)
552
  assert (List.length machine_types = List.length call_types);
553
  (* Unify the two lists of types *)
554
  let substitution = List.fold_left unification [] (List.combine machine_types call_types) in
555
  (* Assume that our substitution match all the possible
556
       polymorphic type of the node *)
557
  let polymorphic_types = find_all_polymorphic_type submachine in
558
  assert (List.length polymorphic_types = List.length substitution);
559
  assert (List.for_all (function x->List.mem_assoc x substitution) polymorphic_types);
560
  substitution
561

    
562

    
563
(* Procedure pretty print functions *)
564

    
565
(** Print the definition of a procedure
566
   @param pp_name the procedure name printer
567
   @param pp_prototype the prototype printer
568
   @param pp_instr local var printer
569
   @param pp_instr instruction printer
570
   @param fmt the formater to print on
571
   @param locals locals var list
572
   @param instrs instructions list
573
**)
574
let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals, instrs) =
575
  fprintf fmt "@[<v>%t is%t@[<v>%a%t@]@,begin@,  @[<v>%a%t@]@,end %t@]"
576
    pp_prototype
577
    (Utils.pp_final_char_if_non_empty "@,  " locals)
578
    (Utils.fprintf_list ~sep:";@," pp_local) locals
579
    (Utils.pp_final_char_if_non_empty ";" locals)
580
    (Utils.fprintf_list ~sep:";@," pp_instr) instrs
581
    (Utils.pp_final_char_if_non_empty ";" instrs)
582
    pp_name
583

    
584

    
585
(* Expression print functions *)
586

    
587
  (* Printing functions for basic operations and expressions *)
588
  (* TODO: refactor code -> use let rec and for basic pretty printing
589
     function *)
590
  (** Printing function for Ada tags, mainly booleans.
591

    
592
      @param fmt the formater to use
593
      @param t the tag to print
594
   **)
595
  let pp_ada_tag fmt t =
596
    pp_print_string fmt
597
      (if t = tag_true then "True" else if t = tag_false then "False" else t)
598

    
599
  (** Printing function for machine type constants. For the moment,
600
      arrays are not supported.
601

    
602
      @param fmt the formater to use
603
      @param c the constant to print
604
   **)
605
  let pp_ada_const fmt c =
606
    match c with
607
    | Const_int i                     -> pp_print_int fmt i
608
    | Const_real (c, e, s)            -> pp_print_string fmt s
609
    | Const_tag t                     -> pp_ada_tag fmt t
610
    | Const_string _ | Const_modeid _ ->
611
      (Format.eprintf
612
         "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
613
       assert false)
614
    | _                               ->
615
      raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
616
      support this constant")
617

    
618
  (** Printing function for expressions [v1 modulo v2]. Depends
619
      on option [integer_div_euclidean] to choose between mathematical
620
      modulo or remainder ([rem] in Ada).
621

    
622
      @param pp_value pretty printer for values
623
      @param v1 the first value in the expression
624
      @param v2 the second value in the expression
625
      @param fmt the formater to print on
626
   **)
627
  let pp_mod pp_value v1 v2 fmt =
628
    if !Options.integer_div_euclidean then
629
      (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
630
      Format.fprintf fmt
631
        "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
632
        pp_value v1 pp_value v2
633
        pp_value v1 pp_value v2
634
        pp_value v2
635
    else (* Ada behavior for rem *)
636
      Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
637

    
638
  (** Printing function for expressions [v1 div v2]. Depends on
639
      option [integer_div_euclidean] to choose between mathematic
640
      division or Ada division.
641

    
642
      @param pp_value pretty printer for values
643
      @param v1 the first value in the expression
644
      @param v2 the second value in the expression
645
      @param fmt the formater to print in
646
   **)
647
  let pp_div pp_value v1 v2 fmt =
648
    if !Options.integer_div_euclidean then
649
      (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
650
      Format.fprintf fmt "(%a - %t) / %a"
651
        pp_value v1
652
        (pp_mod pp_value v1 v2)
653
        pp_value v2
654
    else (* Ada behavior for / *)
655
      Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
656

    
657
  (** Printing function for basic lib functions.
658

    
659
      @param pp_value pretty printer for values
660
      @param i a string representing the function
661
      @param fmt the formater to print on
662
      @param vl the list of operands
663
   **)
664
  let pp_basic_lib_fun pp_value ident fmt vl =
665
    match ident, vl with
666
    | "uminus", [v]    ->
667
      Format.fprintf fmt "(- %a)" pp_value v
668
    | "not", [v]       ->
669
      Format.fprintf fmt "(not %a)" pp_value v
670
    | "impl", [v1; v2] ->
671
      Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
672
    | "=", [v1; v2]    ->
673
      Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
674
    | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
675
    | "equi", [v1; v2] ->
676
      Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
677
    | "xor", [v1; v2]  ->
678
      Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
679
    | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
680
    | "&&", [v1; v2]    ->
681
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
682
    | "||", [v1; v2]    ->
683
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
684
    | "!=", [v1; v2]    ->
685
      Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
686
    | op, [v1; v2]     ->
687
      Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
688
    | fun_name, _      ->
689
      (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
690

    
691
  (** Printing function for values.
692

    
693
      @param m the machine to know the state variable
694
      @param fmt the formater to use
695
      @param value the value to print. Should be a
696
             {!type:Machine_code_types.value_t} value
697
   **)
698
  let rec pp_value m fmt value =
699
    match value.value_desc with
700
    | Cst c             -> pp_ada_const fmt c
701
    | Var var      -> pp_access_var m fmt var
702
    | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value m) f_ident fmt vl
703
    | _                 ->
704
      raise (Ada_not_supported
705
               "unsupported: Ada_backend.adb.pp_value does not support this value type")
(5-5/6)