Project

General

Profile

Download (22.7 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Lustre_types
13
open Utils
14
open Format
15

    
16
let kind2_language_cst = [ "initial" ]
17

    
18
let kind2_protect id =
19
  if List.mem id kind2_language_cst then "_KIND2_PROTECT_" ^ id else id
20

    
21
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
22
   following the C convention for multiple lines macro *)
23
let pp_as_c_macro pp_fun fmt v =
24
  let formatter_out_funs = pp_get_formatter_out_functions fmt () in
25
  let macro_newline () =
26
    formatter_out_funs.out_string "\\" 0 1;
27
    formatter_out_funs.out_newline ()
28
  in
29
  pp_set_formatter_out_functions fmt
30
    { formatter_out_funs with out_newline = macro_newline };
31
  pp_fun fmt v;
32
  pp_set_formatter_out_functions fmt formatter_out_funs
33

    
34
let rec pp_var_struct_type_field fmt (label, tdesc) =
35
  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
36

    
37
and pp_var_type_dec_desc fmt tdesc =
38
  match tdesc with
39
  | Tydec_any ->
40
    fprintf fmt "<any>"
41
  | Tydec_int ->
42
    fprintf fmt "int"
43
  | Tydec_real ->
44
    fprintf fmt "real"
45
  (* | Tydec_float -> fprintf fmt "float" *)
46
  | Tydec_bool ->
47
    fprintf fmt "bool"
48
  | Tydec_clock t ->
49
    fprintf fmt "%a clock" pp_var_type_dec_desc t
50
  | Tydec_const t ->
51
    fprintf fmt "%s" t
52
  | Tydec_enum id_list ->
53
    fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
54
  | Tydec_struct f_list ->
55
    fprintf fmt "struct {%a }"
56
      (fprintf_list ~sep:" " pp_var_struct_type_field)
57
      f_list
58
  | Tydec_array (s, t) ->
59
    fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
60

    
61
let pp_var_type_dec fmt ty = pp_var_type_dec_desc fmt ty.ty_dec_desc
62

    
63
let pp_var_name fmt id =
64
  fprintf fmt "%s"
65
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
66

    
67
let pp_var_type fmt id =
68
  if !Options.print_dec_types then pp_var_type_dec fmt id.var_dec_type
69
  else Types.print_node_ty fmt id.var_type
70

    
71
let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock
72

    
73
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
74

    
75
let pp_var fmt id =
76
  fprintf fmt "%s%s: %a"
77
    (if id.var_dec_const then "const " else "")
78
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
79
    pp_var_type id
80

    
81
let pp_vars fmt vars = fprintf_list ~sep:"; " pp_var fmt vars
82

    
83
let pp_quantifiers fmt (q, vars) =
84
  match q with
85
  | Forall ->
86
    fprintf fmt "forall %a" pp_vars vars
87
  | Exists ->
88
    fprintf fmt "exists %a" pp_vars vars
89

    
90
let rec pp_struct_const_field fmt (label, c) =
91
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
92

    
93
and pp_const fmt c =
94
  match c with
95
  | Const_int i ->
96
    pp_print_int fmt i
97
  | Const_real r ->
98
    Real.pp fmt r
99
  (*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt
100
    "%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)
101
  (* | Const_float r -> pp_print_float fmt r *)
102
  | Const_tag t ->
103
    pp_print_string fmt t
104
  | Const_array ca ->
105
    fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
106
  | Const_struct fl ->
107
    fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
108
  (* used only for annotations *)
109
  | Const_string s ->
110
    pp_print_string fmt ("\"" ^ s ^ "\"")
111
  | Const_modeid s ->
112
    pp_print_string fmt ("\"" ^ s ^ "\"")
113

    
114
let pp_annot_key fmt kwds =
115
  match kwds with
116
  | [] ->
117
    assert false
118
  | [ x ] ->
119
    pp_print_string fmt x
120
  | _ ->
121
    fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
122

    
123
let pp_kind2_when fmt (id, l) =
124
  if l = "true" then fprintf fmt "%s" id
125
  else if l = "false" then fprintf fmt "not(%s)" id
126
  else fprintf fmt "(%s=%s)" l id
127

    
128
let rec pp_expr fmt expr =
129
  (match expr.expr_annot with
130
  | None ->
131
    fprintf fmt "%t"
132
  | Some ann ->
133
    fprintf fmt "@[(%a %t)@]" pp_expr_annot ann) (fun fmt ->
134
      let pp fmt =
135
        match expr.expr_desc with
136
        | Expr_const c ->
137
          pp_const fmt c
138
        | Expr_ident id ->
139
          fprintf fmt "%s"
140
            (if !Options.kind2_print then kind2_protect id else id)
141
        | Expr_array a ->
142
          fprintf fmt "[%a]" pp_tuple a
143
        | Expr_access (a, d) ->
144
          fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
145
        | Expr_power (a, d) ->
146
          fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
147
        | Expr_tuple el ->
148
          fprintf fmt "(%a)" pp_tuple el
149
        | Expr_ite (c, t, e) ->
150
          fprintf fmt
151
            "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
152
            pp_expr c pp_expr t pp_expr e
153
        | Expr_arrow (e1, e2) ->
154
          fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
155
        | Expr_fby (e1, e2) ->
156
          fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
157
        | Expr_pre e ->
158
          fprintf fmt "pre %a" pp_expr e
159
        | Expr_when (e, id, l) ->
160
          if !Options.kind2_print then
161
            fprintf fmt "%a when %a" pp_expr e pp_kind2_when (l, id)
162
          else fprintf fmt "%a when %s(%s)" pp_expr e l id
163
        | Expr_merge (id, hl) ->
164
          fprintf fmt "merge %s %a" id pp_handlers hl
165
        | Expr_appl (id, e, r) ->
166
          pp_app fmt id e r
167
      in
168
      if false (* extra debug *) then
169
        Format.fprintf fmt "%t: %a" pp Types.print_ty expr.expr_type
170
      else pp fmt)
171

    
172
and pp_tuple fmt el = fprintf_list ~sep:"," pp_expr fmt el
173

    
174
and pp_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_expr h
175

    
176
and pp_handlers fmt hl = fprintf_list ~sep:" " pp_handler fmt hl
177

    
178
and pp_app fmt id e r =
179
  if !Options.kind2_print && not (List.mem id Basic_library.internal_funs) then
180
    (* We only translate calls to nodes in kind2. The other may be rejected by
181
       Kind2 *)
182
    (* Small local function to extract the first layer of when constructs *)
183
    let rec un_when_ed_expr e =
184
      match e.expr_desc with
185
      | Expr_when (e, i, l) ->
186
        Some (i, l), e
187
      | Expr_tuple el -> (
188
        let un_when_ed_el = List.map un_when_ed_expr el in
189
        if List.length un_when_ed_el < 1 then assert false;
190
        (* tuple should have at least one element*)
191
        let init_when = fst (List.hd un_when_ed_el) in
192
        let common_when =
193
          List.fold_left
194
            (fun accu (new_opt, _) ->
195
              match accu, new_opt with
196
              | Some c1, Some c2 ->
197
                if c1 = c2 then Some c1
198
                else assert false (* should not be clocked *)
199
              | None, None ->
200
                None
201
              | _ ->
202
                assert false
203
              (* If this is not even, there should be a clocking problem*))
204
            init_when (List.tl un_when_ed_el)
205
        in
206
        match common_when with
207
        | None ->
208
          None, e
209
        | Some _ ->
210
          ( common_when,
211
            { e with expr_desc = Expr_tuple (List.map snd un_when_ed_el) } ))
212
      | _ ->
213
        None, e
214
    in
215
    let when_expr, _ = un_when_ed_expr e in
216
    match r, when_expr with
217
    | None, None ->
218
      pp_call fmt id e
219
    | None, Some w ->
220
      fprintf fmt "(activate %s every (%a)) (%a)" id pp_kind2_when w pp_expr e
221
    | Some r, None ->
222
      fprintf fmt "(restart %s every (%a)) (%a)" id pp_expr r pp_expr e
223
    | Some r, Some w ->
224
      fprintf fmt "(activate %s every (%a) restart every (%a)) (%a)" id
225
        pp_kind2_when w pp_expr r pp_expr e
226
  else
227
    match r with
228
    | None ->
229
      pp_call fmt id e
230
    | Some c ->
231
      fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
232

    
233
and pp_call fmt id e =
234
  match id, e.expr_desc with
235
  | "+", Expr_tuple [ e1; e2 ] ->
236
    fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
237
  | "uminus", _ ->
238
    fprintf fmt "(- %a)" pp_expr e
239
  | "-", Expr_tuple [ e1; e2 ] ->
240
    fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
241
  | "*", Expr_tuple [ e1; e2 ] ->
242
    fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
243
  | "/", Expr_tuple [ e1; e2 ] ->
244
    fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
245
  | "mod", Expr_tuple [ e1; e2 ] ->
246
    fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
247
  | "&&", Expr_tuple [ e1; e2 ] ->
248
    fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
249
  | "||", Expr_tuple [ e1; e2 ] ->
250
    fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
251
  | "xor", Expr_tuple [ e1; e2 ] ->
252
    fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
253
  | "impl", Expr_tuple [ e1; e2 ] ->
254
    fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
255
  | "<", Expr_tuple [ e1; e2 ] ->
256
    fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
257
  | "<=", Expr_tuple [ e1; e2 ] ->
258
    fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
259
  | ">", Expr_tuple [ e1; e2 ] ->
260
    fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
261
  | ">=", Expr_tuple [ e1; e2 ] ->
262
    fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
263
  | "!=", Expr_tuple [ e1; e2 ] ->
264
    fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
265
  | "=", Expr_tuple [ e1; e2 ] ->
266
    fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
267
  | "not", _ ->
268
    fprintf fmt "(not %a)" pp_expr e
269
  | _, Expr_tuple _ ->
270
    fprintf fmt "%s %a" id pp_expr e
271
  | _ ->
272
    fprintf fmt "%s (%a)" id pp_expr e
273

    
274
and pp_eexpr fmt e =
275
  fprintf fmt "%a%t %a"
276
    (Utils.fprintf_list ~sep:"; " pp_quantifiers)
277
    e.eexpr_quantifiers
278
    (fun fmt ->
279
      match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
280
    pp_expr e.eexpr_qfexpr
281

    
282
and pp_sf_value fmt e =
283
  fprintf fmt "%a"
284
    (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
285
    (* (fun fmt -> match e.eexpr_quantifiers *)
286
    (*             with [] -> () *)
287
    (*                | _ -> fprintf fmt ";") *)
288
    pp_expr e.eexpr_qfexpr
289

    
290
and pp_s_function fmt expr_ann =
291
  let pp_annot fmt (kwds, ee) =
292
    fprintf fmt " %t : %a"
293
      (fun fmt ->
294
        match kwds with
295
        | [] ->
296
          assert false
297
        | [ x ] ->
298
          pp_print_string fmt x
299
        | _ ->
300
          fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)
301
      pp_sf_value ee
302
  in
303
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
304

    
305
and pp_expr_annot fmt expr_ann =
306
  let pp_annot fmt (kwds, ee) =
307
    fprintf fmt "(*!%a: %a; *)" pp_annot_key kwds pp_eexpr ee
308
  in
309
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
310

    
311
let pp_asserts fmt asserts =
312
  match asserts with
313
  | _ :: _ ->
314
    fprintf fmt "(* Asserts definitions *)@ ";
315
    fprintf_list ~sep:"@ "
316
      (fun fmt assert_ ->
317
        let expr = assert_.assert_expr in
318
        fprintf fmt "assert %a;" pp_expr expr)
319
      fmt asserts
320
  | _ ->
321
    ()
322

    
323
(* let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const
324
   then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc
325
   Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock *)
326
let pp_node_var fmt id =
327
  fprintf fmt "%s%s: %a%a"
328
    (if id.var_dec_const then "const " else "")
329
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
330
    pp_var_type id pp_var_clock id;
331
  match id.var_dec_value with
332
  | None ->
333
    ()
334
  | Some v ->
335
    fprintf fmt " = %a" pp_expr v
336

    
337
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var
338

    
339
let pp_node_eq fmt eq =
340
  fprintf fmt "%a = %a;" pp_eq_lhs eq.eq_lhs pp_expr eq.eq_rhs
341

    
342
let pp_restart fmt restart =
343
  fprintf fmt "%s" (if restart then "restart" else "resume")
344

    
345
let pp_unless fmt (_, expr, restart, st) =
346
  fprintf fmt "unless %a %a %s" pp_expr expr pp_restart restart st
347

    
348
let pp_until fmt (_, expr, restart, st) =
349
  fprintf fmt "until %a %a %s" pp_expr expr pp_restart restart st
350

    
351
let rec pp_handler fmt handler =
352
  fprintf fmt "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
353
    handler.hand_state
354
    (Utils.fprintf_list ~sep:"@ " pp_unless)
355
    handler.hand_unless
356
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
357
    (fun fmt locals ->
358
      match locals with
359
      | [] ->
360
        ()
361
      | _ ->
362
        fprintf fmt "@[<v 4>var %a@]@ "
363
          (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
364
               fprintf fmt "%a;" pp_node_var v))
365
          locals)
366
    handler.hand_locals
367
    (fprintf_list ~sep:"@ " pp_expr_annot)
368
    handler.hand_annots pp_node_stmts handler.hand_stmts pp_asserts
369
    handler.hand_asserts
370
    (Utils.fprintf_list ~sep:"@," pp_until)
371
    handler.hand_until
372

    
373
and pp_node_stmt fmt stmt =
374
  match stmt with Eq eq -> pp_node_eq fmt eq | Aut aut -> pp_node_aut fmt aut
375

    
376
and pp_node_stmts fmt stmts =
377
  pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cut pp_node_stmt fmt
378
    stmts
379

    
380
and pp_node_aut fmt aut =
381
  fprintf fmt "@[<v 0>automaton %s@,%a@]" aut.aut_id
382
    (Utils.fprintf_list ~sep:"@ " pp_handler)
383
    aut.aut_handlers
384

    
385
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
386

    
387
let pp_typedef fmt ty =
388
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
389

    
390
let pp_typedec fmt ty = fprintf fmt "type %s;" ty.tydec_id
391

    
392
(* let rec pp_var_type fmt ty =  *)
393
(*   fprintf fmt "%a" (match ty.tdesc with  *)
394
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
395
(*     | Tint -> pp_print_string fmt "int" *)
396
(*     | Treal -> pp_print_string fmt "real" *)
397
(*     | Tbool -> pp_print_string fmt "bool" *)
398
(*     | Trat -> pp_print_string fmt "rat" *)
399
(*     | Tclock -> pp_print_string fmt "clock"  *)
400
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
401
(*   ) *)
402

    
403
(* let pp_quantifiers fmt (q, vars) =
404
 *   match q with
405
 *     | Forall -> fprintf fmt "forall %a" pp_vars vars 
406
 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars *)
407

    
408
(*let pp_eexpr fmt e = fprintf fmt "%a%t %a" (Utils.fprintf_list ~sep:"; "
409
  pp_quantifiers) e.eexpr_quantifiers (fun fmt -> match e.eexpr_quantifiers with
410
  [] -> () | _ -> fprintf fmt ";") pp_expr e.eexpr_qfexpr *)
411

    
412
let pp_spec_eq fmt eq =
413
  fprintf fmt "var %a : %a = %a;" pp_eq_lhs eq.eq_lhs Types.print_node_ty
414
    eq.eq_rhs.expr_type pp_expr eq.eq_rhs
415

    
416
let pp_spec_stmt fmt stmt =
417
  match stmt with Eq eq -> pp_spec_eq fmt eq | Aut _ -> assert false
418
(* Not supported yet *)
419

    
420
let pp_spec fmt spec =
421
  (* const are prefixed with const in pp_var and with nothing for regular
422
     variables. We adapt the call to produce the appropriate output. *)
423
  fprintf_list ~eol:"@, " ~sep:"@, "
424
    (fun fmt v ->
425
      fprintf fmt "%a = %t;" pp_var v (fun fmt ->
426
          match v.var_dec_value with
427
          | None ->
428
            assert false
429
          | Some e ->
430
            pp_expr fmt e))
431
    fmt spec.consts;
432

    
433
  fprintf_list ~eol:"@, " ~sep:"@, "
434
    (fun fmt s -> pp_spec_stmt fmt s)
435
    fmt spec.stmts;
436
  fprintf_list ~eol:"@, " ~sep:"@, "
437
    (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r)
438
    fmt spec.assume;
439
  fprintf_list ~eol:"@, " ~sep:"@, "
440
    (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r)
441
    fmt spec.guarantees;
442
  fprintf_list ~eol:"@, " ~sep:"@, "
443
    (fun fmt mode ->
444
      fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" mode.mode_id
445
        (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r ->
446
             fprintf fmt "require %a;" pp_eexpr r))
447
        mode.require
448
        (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r ->
449
             fprintf fmt "ensure %a;" pp_eexpr r))
450
        mode.ensure)
451
    fmt spec.modes;
452
  fprintf_list ~eol:"@, " ~sep:"@, "
453
    (fun fmt import ->
454
      fprintf fmt "import %s (%a) returns (%a);" import.import_nodeid pp_expr
455
        import.inputs pp_expr import.outputs)
456
    fmt spec.imports
457

    
458
(* Project the contract node as a pure contract: local memories are pushed back
459
   in the contract definition. Should mainly be used to print it *)
460
let node_as_contract nd =
461
  match nd.node_spec with
462
  | None | Some (NodeSpec _) ->
463
    raise (Invalid_argument "Not a contract")
464
  | Some (Contract c) ->
465
    (* While a processed contract shall have no locals, sttms nor consts, an
466
       unprocessed one could. So we conservatively merge elements, to enable
467
       printing unprocessed contracts *)
468
    let consts, locals =
469
      List.partition (fun v -> v.var_dec_const) nd.node_locals
470
    in
471
    {
472
      c with
473
      consts = consts @ c.consts;
474
      locals = locals @ c.locals;
475
      stmts = nd.node_stmts @ c.stmts;
476
    }
477

    
478
(* Printing top contract as comments in regular output and as contract in kind2 *)
479
let pp_contract fmt nd =
480
  let c = node_as_contract nd in
481
  fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "
482
    (if !Options.kind2_print then "" else "(*@")
483
    nd.node_id pp_node_args nd.node_inputs pp_node_args nd.node_outputs;
484
  fprintf fmt "@[<v 2>let@ ";
485
  pp_spec fmt c;
486
  fprintf fmt "@]@ tel@ @]%s@ " (if !Options.kind2_print then "" else "*)")
487

    
488
let pp_spec_as_comment fmt (inl, outl, spec) =
489
  match spec with
490
  | Contract c ->
491
    (* should have been processed by now *)
492
    fprintf fmt "@[<hov 2>(*@contract@ ";
493
    pp_spec fmt c;
494
    fprintf fmt "@]*)@ "
495
  | NodeSpec name ->
496
    (* Pushing stmts in contract. We update the original information with the
497
       computed one in nd. *)
498
    let pp_l = fprintf_list ~sep:"," pp_var_name in
499
    fprintf fmt "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ " name
500
      pp_l inl pp_l outl
501

    
502
let pp_node_vs_function fmt nd =
503
  fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")
504

    
505
let pp_node fmt nd =
506
  (* Prototype *)
507
  fprintf fmt "%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
508
    pp_node_vs_function nd nd.node_id pp_node_args nd.node_inputs pp_node_args
509
    nd.node_outputs;
510
  (* Contracts *)
511
  fprintf fmt "%a"
512
    (fun fmt s ->
513
      match s with
514
      | Some s ->
515
        pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s)
516
      | _ ->
517
        ())
518
    nd.node_spec
519
  (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@
520
     ") *);
521
  (* Locals *)
522
  fprintf fmt "%a"
523
    (fun fmt locals ->
524
      match locals with
525
      | [] ->
526
        ()
527
      | _ ->
528
        fprintf fmt "@[<v 4>var %a@]@ "
529
          (fprintf_list ~sep:"@ " (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
530
          locals)
531
    nd.node_locals;
532
  (* Checks *)
533
  fprintf fmt "%a"
534
    (fun fmt checks ->
535
      match checks with
536
      | [] ->
537
        ()
538
      | _ ->
539
        fprintf fmt "@[<v 4>check@ %a@]@ "
540
          (fprintf_list ~sep:"@ " (fun fmt d ->
541
               fprintf fmt "%a" Dimension.pp_dimension d))
542
          checks)
543
    nd.node_checks;
544
  (* Body *)
545
  fprintf fmt "@[<v 2>let@ ";
546
  (* Annotations *)
547
  fprintf fmt "%a" (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
548
  (* Statements *)
549
  fprintf fmt "%a" pp_node_stmts nd.node_stmts;
550
  (* Asserts *)
551
  fprintf fmt "%a" pp_asserts nd.node_asserts;
552
  (* closing boxes body (2) and node (1) *)
553
  fprintf fmt "@]@ tel"
554

    
555
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", "
556
  pp_print_string) (Scheduling.schedule_node nd)*)
557

    
558
let pp_node fmt nd =
559
  match nd.node_spec, nd.node_iscontract with
560
  | None, false | Some (NodeSpec _), false ->
561
    pp_node fmt nd
562
  | Some (Contract _), false ->
563
    pp_node fmt nd (* may happen early in the compil process *)
564
  | Some (Contract _), true ->
565
    pp_contract fmt nd
566
  | _ ->
567
    assert false
568

    
569
let pp_imported_node fmt ind =
570
  fprintf fmt "@[<v 0>";
571
  (* Prototype *)
572
  fprintf fmt "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
573
    (if ind.nodei_stateless then "function" else "node")
574
    ind.nodei_id pp_node_args ind.nodei_inputs pp_node_args ind.nodei_outputs;
575
  (* Contracts *)
576
  fprintf fmt "%a%t"
577
    (fun fmt s ->
578
      match s with
579
      | Some s ->
580
        pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s)
581
      | _ ->
582
        ())
583
    ind.nodei_spec
584
    (fun fmt ->
585
      match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
586
  fprintf fmt "@]@ "
587

    
588
let pp_const_decl fmt cdecl =
589
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
590

    
591
let pp_const_decl_list fmt clist =
592
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
593

    
594
let pp_decl fmt decl =
595
  match decl.top_decl_desc with
596
  | Node nd ->
597
    fprintf fmt "%a" pp_node nd
598
  | ImportedNode ind ->
599
    (* We do not print imported nodes *)
600
    fprintf fmt "(* imported %a; *)" pp_imported_node ind
601
  | Const c ->
602
    fprintf fmt "const %a" pp_const_decl c
603
  | Open (local, s) ->
604
    if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
605
  | Include s ->
606
    fprintf fmt "include \"%s\"" s
607
  | TypeDef tdef ->
608
    fprintf fmt "%a" pp_typedef tdef
609

    
610
let pp_prog pp_decl fmt prog =
611
  (* we first print types: the function SortProg.sort could do the job but ut
612
     introduces a cyclic dependance *)
613
  let open_decl, prog =
614
    List.partition
615
      (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false)
616
      prog
617
  in
618
  let type_decl, prog =
619
    List.partition
620
      (fun decl ->
621
        match decl.top_decl_desc with TypeDef _ -> true | _ -> false)
622
      prog
623
  in
624
  pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut pp_decl fmt
625
    (open_decl @ type_decl @ prog)
626

    
627
(* Gives a short overview of model content. Do not print all node content *)
628
let pp_short_decl fmt decl =
629
  match decl.top_decl_desc with
630
  | Node nd ->
631
    fprintf fmt "%a %s@ " pp_node_vs_function nd nd.node_id
632
  | ImportedNode ind ->
633
    fprintf fmt "imported node %s" ind.nodei_id
634
  | Const c ->
635
    fprintf fmt "const %a@ " pp_const_decl c
636
  | Include s ->
637
    fprintf fmt "include \"%s\"" s
638
  | Open (local, s) ->
639
    if local then fprintf fmt "#open \"%s\"@ " s
640
    else fprintf fmt "#open <%s>@ " s
641
  | TypeDef tdef ->
642
    fprintf fmt "type %s;@ " tdef.tydef_id
643

    
644
let pp_prog_short = pp_prog pp_short_decl
645

    
646
let pp_prog = pp_prog pp_decl
647

    
648
let pp_lusi fmt decl =
649
  match decl.top_decl_desc with
650
  | ImportedNode ind ->
651
    fprintf fmt "%a;@ " pp_imported_node ind
652
  | Const c ->
653
    fprintf fmt "const %a@ " pp_const_decl c
654
  | Include s ->
655
    fprintf fmt "include \"%s\"" s
656
  | Open (local, s) ->
657
    if local then fprintf fmt "#open \"%s\"@ " s
658
    else fprintf fmt "#open <%s>@ " s
659
  | TypeDef tdef ->
660
    fprintf fmt "%a@ " pp_typedef tdef
661
  | Node _ ->
662
    assert false
663

    
664
let pp_lusi_header fmt basename prog =
665
  fprintf fmt "@[<v 0>";
666
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
667
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number
668
    pp_date
669
    (Unix.gmtime (Unix.time ()));
670
  fprintf fmt
671
    "(* Feel free to mask some of the definitions by removing them from this \
672
     file. *)@ @ ";
673
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
674
  fprintf fmt "@]@."
675

    
676
let pp_offset fmt offset =
677
  match offset with
678
  | Index i ->
679
    fprintf fmt "[%a]" Dimension.pp_dimension i
680
  | Field f ->
681
    fprintf fmt ".%s" f
682

    
683
let pp_node_list fmt prog =
684
  Format.fprintf fmt "@[<h 2>%a@]"
685
    (fprintf_list ~sep:"@ " (fun fmt decl ->
686
         match decl.top_decl_desc with
687
         | Node nd ->
688
           Format.fprintf fmt "%s" nd.node_id
689
         | _ ->
690
           ()))
691
    prog
692

    
693
(* Local Variables: *)
694
(* compile-command:"make -C .." *)
695
(* End: *)
(50-50/66)