Project

General

Profile

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

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

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

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

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

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

    
72
let pp_var_clock fmt id = Clocks.pp_suffix fmt id.var_clock
73

    
74
let pp_eq_lhs = pp_comma_list pp_print_string
75

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

    
85
let pp_vars fmt vars = pp_print_list ~pp_sep:pp_print_semicolon pp_var fmt vars
86

    
87
let pp_quantifiers fmt (q, vars) =
88
  match q with
89
  | Forall ->
90
    fprintf fmt "forall %a" pp_vars vars
91
  | Exists ->
92
    fprintf fmt "exists %a" pp_vars vars
93

    
94
let rec pp_struct_const_field fmt (label, c) =
95
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
96

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

    
122
let pp_annot_key fmt kwds =
123
  match kwds with
124
  | [] ->
125
    assert false
126
  | [ x ] ->
127
    pp_print_string fmt x
128
  | _ ->
129
    fprintf
130
      fmt
131
      "/%a/"
132
      (pp_print_list
133
         ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
134
         pp_print_string)
135
      kwds
136

    
137
let pp_kind2_when fmt (id, l) =
138
  if l = "true" then fprintf fmt "%s" id
139
  else if l = "false" then fprintf fmt "not(%s)" id
140
  else fprintf fmt "(%s=%s)" l id
141

    
142
let rec pp_expr fmt expr =
143
  (match expr.expr_annot with
144
  | None ->
145
    fprintf fmt "%t"
146
  | Some ann ->
147
    fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
148
    (fun fmt ->
149
      let pp fmt =
150
        match expr.expr_desc with
151
        | Expr_const c ->
152
          pp_const fmt c
153
        | Expr_ident id ->
154
          fprintf
155
            fmt
156
            "%s"
157
            (if !Options.kind2_print then kind2_protect id else id)
158
        | Expr_array a ->
159
          fprintf fmt "[%a]" pp_tuple a
160
        | Expr_access (a, d) ->
161
          fprintf fmt "%a[%a]" pp_expr a Dimension.pp d
162
        | Expr_power (a, d) ->
163
          fprintf fmt "(%a^%a)" pp_expr a Dimension.pp d
164
        | Expr_tuple el ->
165
          fprintf fmt "(%a)" pp_tuple el
166
        | Expr_ite (c, t, e) ->
167
          fprintf
168
            fmt
169
            "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
170
            pp_expr
171
            c
172
            pp_expr
173
            t
174
            pp_expr
175
            e
176
        | Expr_arrow (e1, e2) ->
177
          fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
178
        | Expr_fby (e1, e2) ->
179
          fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
180
        | Expr_pre e ->
181
          fprintf fmt "pre %a" pp_expr e
182
        | Expr_when (e, id, l) ->
183
          if !Options.kind2_print then
184
            fprintf fmt "%a when %a" pp_expr e pp_kind2_when (l, id)
185
          else fprintf fmt "%a when %s(%s)" pp_expr e l id
186
        | Expr_merge (id, hl) ->
187
          fprintf fmt "merge %s %a" id pp_handlers hl
188
        | Expr_appl (id, e, r) ->
189
          pp_app fmt id e r
190
      in
191
      if false (* extra debug *) then
192
        Format.fprintf fmt "%t: %a" pp Types.pp expr.expr_type
193
      else pp fmt)
194

    
195
and pp_tuple fmt el =
196
  pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ",") pp_expr fmt el
197

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

    
200
and pp_handlers fmt hl = pp_print_list pp_handler fmt hl
201

    
202
and pp_app fmt id e r =
203
  if !Options.kind2_print && not (List.mem id Basic_library.internal_funs) then
204
    (* We only translate calls to nodes in kind2. The other may be rejected by
205
       Kind2 *)
206
    (* Small local function to extract the first layer of when constructs *)
207
    let rec un_when_ed_expr e =
208
      match e.expr_desc with
209
      | Expr_when (e, i, l) ->
210
        Some (i, l), e
211
      | Expr_tuple el -> (
212
        let un_when_ed_el = List.map un_when_ed_expr el in
213
        if List.length un_when_ed_el < 1 then assert false;
214
        (* tuple should have at least one element*)
215
        let init_when = fst (List.hd un_when_ed_el) in
216
        let common_when =
217
          List.fold_left
218
            (fun accu (new_opt, _) ->
219
              match accu, new_opt with
220
              | Some c1, Some c2 ->
221
                if c1 = c2 then Some c1
222
                else assert false (* should not be clocked *)
223
              | None, None ->
224
                None
225
              | _ ->
226
                assert false
227
              (* If this is not even, there should be a clocking problem*))
228
            init_when
229
            (List.tl un_when_ed_el)
230
        in
231
        match common_when with
232
        | None ->
233
          None, e
234
        | Some _ ->
235
          ( common_when,
236
            { e with expr_desc = Expr_tuple (List.map snd un_when_ed_el) } ))
237
      | _ ->
238
        None, e
239
    in
240
    let when_expr, _ = un_when_ed_expr e in
241
    match r, when_expr with
242
    | None, None ->
243
      pp_call fmt id e
244
    | None, Some w ->
245
      fprintf fmt "(activate %s every (%a)) (%a)" id pp_kind2_when w pp_expr e
246
    | Some r, None ->
247
      fprintf fmt "(restart %s every (%a)) (%a)" id pp_expr r pp_expr e
248
    | Some r, Some w ->
249
      fprintf
250
        fmt
251
        "(activate %s every (%a) restart every (%a)) (%a)"
252
        id
253
        pp_kind2_when
254
        w
255
        pp_expr
256
        r
257
        pp_expr
258
        e
259
  else
260
    match r with
261
    | None ->
262
      pp_call fmt id e
263
    | Some c ->
264
      fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
265

    
266
and pp_call fmt id e =
267
  match id, e.expr_desc with
268
  | "+", Expr_tuple [ e1; e2 ] ->
269
    fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
270
  | "uminus", _ ->
271
    fprintf fmt "(- %a)" pp_expr e
272
  | "-", Expr_tuple [ e1; e2 ] ->
273
    fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
274
  | "*", Expr_tuple [ e1; e2 ] ->
275
    fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
276
  | "/", Expr_tuple [ e1; e2 ] ->
277
    fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
278
  | "mod", Expr_tuple [ e1; e2 ] ->
279
    fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
280
  | "&&", Expr_tuple [ e1; e2 ] ->
281
    fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
282
  | "||", Expr_tuple [ e1; e2 ] ->
283
    fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
284
  | "xor", Expr_tuple [ e1; e2 ] ->
285
    fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
286
  | "impl", Expr_tuple [ e1; e2 ] ->
287
    fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
288
  | "<", Expr_tuple [ e1; e2 ] ->
289
    fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
290
  | "<=", Expr_tuple [ e1; e2 ] ->
291
    fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
292
  | ">", Expr_tuple [ e1; e2 ] ->
293
    fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
294
  | ">=", Expr_tuple [ e1; e2 ] ->
295
    fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
296
  | "!=", Expr_tuple [ e1; e2 ] ->
297
    fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
298
  | "=", Expr_tuple [ e1; e2 ] ->
299
    fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
300
  | "not", _ ->
301
    fprintf fmt "(not %a)" pp_expr e
302
  | _, Expr_tuple _ ->
303
    fprintf fmt "%s %a" id pp_expr e
304
  | _ ->
305
    fprintf fmt "%s (%a)" id pp_expr e
306

    
307
and pp_eexpr fmt e =
308
  fprintf
309
    fmt
310
    "%a%t %a"
311
    (pp_print_list ~pp_sep:pp_print_semicolon pp_quantifiers)
312
    e.eexpr_quantifiers
313
    (fun fmt ->
314
      match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
315
    pp_expr
316
    e.eexpr_qfexpr
317

    
318
and pp_sf_value fmt e =
319
  fprintf
320
    fmt
321
    "%a"
322
    (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
323
    (* (fun fmt -> match e.eexpr_quantifiers *)
324
    (*             with [] -> () *)
325
    (*                | _ -> fprintf fmt ";") *)
326
    pp_expr
327
    e.eexpr_qfexpr
328

    
329
and pp_s_function fmt expr_ann =
330
  let pp_annot fmt (kwds, ee) =
331
    fprintf
332
      fmt
333
      " %t : %a"
334
      (fun fmt ->
335
        match kwds with
336
        | [] ->
337
          assert false
338
        | [ x ] ->
339
          pp_print_string fmt x
340
        | _ ->
341
          fprintf
342
            fmt
343
            "%a"
344
            (pp_print_list
345
               ~pp_sep:(fun fmt () -> pp_print_string fmt "/")
346
               pp_print_string)
347
            kwds)
348
      pp_sf_value
349
      ee
350
  in
351
  pp_print_list pp_annot fmt expr_ann.annots
352

    
353
and pp_expr_annot fmt expr_ann =
354
  let pp_annot fmt (kwds, ee) =
355
    fprintf fmt "(*!%a: %a; *)" pp_annot_key kwds pp_eexpr ee
356
  in
357
  pp_print_list pp_annot fmt expr_ann.annots
358

    
359
let pp_asserts fmt asserts =
360
  match asserts with
361
  | _ :: _ ->
362
    fprintf fmt "(* Asserts definitions *)@ ";
363
    pp_print_list
364
      (fun fmt assert_ ->
365
        let expr = assert_.assert_expr in
366
        fprintf fmt "assert %a;" pp_expr expr)
367
      fmt
368
      asserts
369
  | _ ->
370
    ()
371

    
372
(* let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const
373
   then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc
374
   Types.pp id.var_type Clocks.pp_ck_suffix id.var_clock *)
375
let pp_node_var fmt id =
376
  fprintf
377
    fmt
378
    "%s%s: %a%a"
379
    (if id.var_dec_const then "const " else "")
380
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
381
    pp_var_type
382
    id
383
    pp_var_clock
384
    id;
385
  match id.var_dec_value with
386
  | None ->
387
    ()
388
  | Some v ->
389
    fprintf fmt " = %a" pp_expr v
390

    
391
let pp_node_args = pp_print_list ~pp_sep:pp_print_semicolon pp_node_var
392

    
393
let pp_node_eq fmt eq =
394
  fprintf fmt "%a = %a;" pp_eq_lhs eq.eq_lhs pp_expr eq.eq_rhs
395

    
396
let pp_restart fmt restart =
397
  fprintf fmt "%s" (if restart then "restart" else "resume")
398

    
399
let pp_unless fmt (_, expr, restart, st) =
400
  fprintf fmt "unless %a %a %s" pp_expr expr pp_restart restart st
401

    
402
let pp_until fmt (_, expr, restart, st) =
403
  fprintf fmt "until %a %a %s" pp_expr expr pp_restart restart st
404

    
405
let rec pp_handler fmt handler =
406
  fprintf
407
    fmt
408
    "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
409
    handler.hand_state
410
    (pp_print_list pp_unless)
411
    handler.hand_unless
412
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
413
    (fun fmt locals ->
414
      match locals with
415
      | [] ->
416
        ()
417
      | _ ->
418
        fprintf
419
          fmt
420
          "@[<v 4>var %a@]@ "
421
          (pp_print_list ~pp_sep:pp_print_semicolon pp_node_var)
422
          locals)
423
    handler.hand_locals
424
    (pp_print_list pp_expr_annot)
425
    handler.hand_annots
426
    pp_node_stmts
427
    handler.hand_stmts
428
    pp_asserts
429
    handler.hand_asserts
430
    (pp_print_list pp_until)
431
    handler.hand_until
432

    
433
and pp_node_stmt fmt stmt =
434
  match stmt with Eq eq -> pp_node_eq fmt eq | Aut aut -> pp_node_aut fmt aut
435

    
436
and pp_node_stmts fmt stmts =
437
  pp_print_list
438
    ~pp_open_box:pp_open_vbox0
439
    ~pp_sep:pp_print_cut
440
    pp_node_stmt
441
    fmt
442
    stmts
443

    
444
and pp_node_aut fmt aut =
445
  fprintf
446
    fmt
447
    "@[<v 0>automaton %s@,%a@]"
448
    aut.aut_id
449
    (pp_print_list pp_handler)
450
    aut.aut_handlers
451

    
452
and pp_node_eqs fmt eqs = pp_print_list pp_node_eq fmt eqs
453

    
454
let pp_typedef fmt ty =
455
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
456

    
457
(* XXX: UNUSED *)
458
(* let pp_typedec fmt ty = fprintf fmt "type %s;" ty.tydec_id *)
459

    
460
(* let rec pp_var_type fmt ty =  *)
461
(*   fprintf fmt "%a" (match ty.tdesc with  *)
462
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
463
(*     | Tint -> pp_print_string fmt "int" *)
464
(*     | Treal -> pp_print_string fmt "real" *)
465
(*     | Tbool -> pp_print_string fmt "bool" *)
466
(*     | Trat -> pp_print_string fmt "rat" *)
467
(*     | Tclock -> pp_print_string fmt "clock"  *)
468
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
469
(*   ) *)
470

    
471
(* let pp_quantifiers fmt (q, vars) =
472
 *   match q with
473
 *     | Forall -> fprintf fmt "forall %a" pp_vars vars 
474
 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars *)
475

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

    
480
let pp_spec_eq fmt eq =
481
  fprintf
482
    fmt
483
    "var %a : %a = %a;"
484
    pp_eq_lhs
485
    eq.eq_lhs
486
    Types.pp_node_ty
487
    eq.eq_rhs.expr_type
488
    pp_expr
489
    eq.eq_rhs
490

    
491
let pp_spec_stmt fmt stmt =
492
  match stmt with Eq eq -> pp_spec_eq fmt eq | Aut _ -> assert false
493
(* Not supported yet *)
494

    
495
let pp_spec fmt spec =
496
  (* const are prefixed with const in pp_var and with nothing for regular
497
     variables. We adapt the call to produce the appropriate output. *)
498
  fprintf fmt "@[<v>%a%a%a%a%a%a@]"
499
    (pp_print_list
500
       (fun fmt v ->
501
          fprintf fmt "%a = %t;" pp_var v (fun fmt ->
502
              match v.var_dec_value with
503
              | None ->
504
                assert false
505
              | Some e ->
506
                pp_expr fmt e)))
507
    spec.consts
508

    
509
    (pp_print_list ~pp_prologue:pp_print_cut pp_spec_stmt) spec.stmts
510

    
511
    (pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "assume %a;" pp_eexpr))
512
    spec.assume
513

    
514
    (pp_print_list ~pp_prologue:pp_print_cut (fun fmt -> fprintf fmt "guarantee %a;" pp_eexpr))
515
    spec.guarantees
516

    
517
    (pp_print_list ~pp_prologue:pp_print_cut
518
       (fun fmt mode ->
519
          fprintf
520
            fmt
521
            "mode %s (@[<v 0>%a@ %a@]);"
522
            mode.mode_id
523
            (pp_print_list (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r))
524
            mode.require
525
            (pp_print_list (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r))
526
            mode.ensure))
527
    spec.modes
528

    
529
    (pp_print_list ~pp_prologue:pp_print_cut
530
       (fun fmt import ->
531
          fprintf
532
            fmt
533
            "import %s (%a) returns (%a);"
534
            import.import_nodeid
535
            pp_expr
536
            import.inputs
537
            pp_expr
538
            import.outputs))
539
    spec.imports
540

    
541
(* Project the contract node as a pure contract: local memories are pushed back
542
   in the contract definition. Should mainly be used to print it *)
543
let node_as_contract nd =
544
  match nd.node_spec with
545
  | None | Some (NodeSpec _) ->
546
    raise (Invalid_argument "Not a contract")
547
  | Some (Contract c) ->
548
    (* While a processed contract shall have no locals, sttms nor consts, an
549
       unprocessed one could. So we conservatively merge elements, to enable
550
       printing unprocessed contracts *)
551
    let consts, locals =
552
      List.partition (fun v -> v.var_dec_const) nd.node_locals
553
    in
554
    {
555
      c with
556
      consts = consts @ c.consts;
557
      locals = locals @ c.locals;
558
      stmts = nd.node_stmts @ c.stmts;
559
    }
560

    
561
(* Printing top contract as comments in regular output and as contract in kind2 *)
562
let pp_contract fmt nd =
563
  let c = node_as_contract nd in
564
  fprintf
565
    fmt
566
    "@[<v 2>%scontract %s(%a) returns (%a);@ "
567
    (if !Options.kind2_print then "" else "(*@")
568
    nd.node_id
569
    pp_node_args
570
    nd.node_inputs
571
    pp_node_args
572
    nd.node_outputs;
573
  fprintf fmt "@[<v 2>let@ ";
574
  pp_spec fmt c;
575
  fprintf fmt "@]@ tel@ @]%s@ " (if !Options.kind2_print then "" else "*)")
576

    
577
let pp_spec_as_comment fmt (inl, outl, spec) =
578
  match spec with
579
  | Contract c ->
580
    (* should have been processed by now *)
581
    fprintf fmt "@[<hov 2>(*@contract@ ";
582
    pp_spec fmt c;
583
    fprintf fmt "@]*)@ "
584
  | NodeSpec name ->
585
    (* Pushing stmts in contract. We update the original information with the
586
       computed one in nd. *)
587
    let pp_l = pp_comma_list pp_var_name in
588
    fprintf
589
      fmt
590
      "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ "
591
      name
592
      pp_l
593
      inl
594
      pp_l
595
      outl
596

    
597
let pp_node_vs_function fmt nd =
598
  fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")
599

    
600
let pp_node fmt nd =
601
  (* Prototype *)
602
  fprintf
603
    fmt
604
    "%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
605
    pp_node_vs_function
606
    nd
607
    nd.node_id
608
    pp_node_args
609
    nd.node_inputs
610
    pp_node_args
611
    nd.node_outputs;
612
  (* Contracts *)
613
  fprintf
614
    fmt
615
    "%a"
616
    (fun fmt s ->
617
      match s with
618
      | Some s ->
619
        pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s)
620
      | _ ->
621
        ())
622
    nd.node_spec
623
  (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@
624
     ") *);
625
  (* Locals *)
626
  fprintf
627
    fmt
628
    "%a"
629
    (fun fmt locals ->
630
      match locals with
631
      | [] ->
632
        ()
633
      | _ ->
634
        fprintf
635
          fmt
636
          "@[<v 4>var %a@]@ "
637
          (pp_print_list (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
638
          locals)
639
    nd.node_locals;
640
  (* Checks *)
641
  fprintf
642
    fmt
643
    "%a"
644
    (fun fmt checks ->
645
      match checks with
646
      | [] ->
647
        ()
648
      | _ ->
649
        fprintf
650
          fmt
651
          "@[<v 4>check@ %a@]@ "
652
          (pp_print_list (fun fmt d -> fprintf fmt "%a" Dimension.pp d))
653
          checks)
654
    nd.node_checks;
655
  (* Body *)
656
  fprintf fmt "@[<v 2>let@ ";
657
  (* Annotations *)
658
  fprintf fmt "%a" (pp_print_list pp_expr_annot) nd.node_annot;
659
  (* Statements *)
660
  fprintf fmt "%a" pp_node_stmts nd.node_stmts;
661
  (* Asserts *)
662
  fprintf fmt "%a" pp_asserts nd.node_asserts;
663
  (* closing boxes body (2) and node (1) *)
664
  fprintf fmt "@]@ tel"
665

    
666
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", "
667
  pp_print_string) (Scheduling.schedule_node nd)*)
668

    
669
let pp_node fmt nd =
670
  match nd.node_spec, nd.node_iscontract with
671
  | None, false | Some (NodeSpec _), false ->
672
    pp_node fmt nd
673
  | Some (Contract _), false ->
674
    pp_node fmt nd (* may happen early in the compil process *)
675
  | Some (Contract _), true ->
676
    pp_contract fmt nd
677
  | _ ->
678
    assert false
679

    
680
let pp_imported_node fmt ind =
681
  fprintf fmt "@[<v 0>";
682
  (* Prototype *)
683
  fprintf
684
    fmt
685
    "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
686
    (if ind.nodei_stateless then "function" else "node")
687
    ind.nodei_id
688
    pp_node_args
689
    ind.nodei_inputs
690
    pp_node_args
691
    ind.nodei_outputs;
692
  (* Contracts *)
693
  fprintf
694
    fmt
695
    "%a%t"
696
    (fun fmt s ->
697
      match s with
698
      | Some s ->
699
        pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s)
700
      | _ ->
701
        ())
702
    ind.nodei_spec
703
    (fun fmt ->
704
      match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
705
  fprintf fmt "@]@ "
706

    
707
let pp_const_decl fmt cdecl =
708
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
709

    
710
(* XXX: UNUSED *)
711
(* let pp_const_decl_list fmt clist =
712
 *   pp_print_list pp_const_decl fmt clist *)
713

    
714
let pp_decl fmt decl =
715
  match decl.top_decl_desc with
716
  | Node nd ->
717
    fprintf fmt "%a" pp_node nd
718
  | ImportedNode ind ->
719
    (* We do not print imported nodes *)
720
    fprintf fmt "(* imported %a; *)" pp_imported_node ind
721
  | Const c ->
722
    fprintf fmt "const %a" pp_const_decl c
723
  | Open (local, s) ->
724
    if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
725
  | Include s ->
726
    fprintf fmt "include \"%s\"" s
727
  | TypeDef tdef ->
728
    fprintf fmt "%a" pp_typedef tdef
729

    
730
let pp_prog pp_decl fmt prog =
731
  (* we first print types: the function SortProg.sort could do the job but ut
732
     introduces a cyclic dependance *)
733
  let open_decl, prog =
734
    List.partition
735
      (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false)
736
      prog
737
  in
738
  let type_decl, prog =
739
    List.partition
740
      (fun decl ->
741
        match decl.top_decl_desc with TypeDef _ -> true | _ -> false)
742
      prog
743
  in
744
  pp_print_list
745
    ~pp_open_box:pp_open_vbox0
746
    ~pp_sep:pp_print_cutcut
747
    pp_decl
748
    fmt
749
    (open_decl @ type_decl @ prog)
750

    
751
(* Gives a short overview of model content. Do not print all node content *)
752
let pp_short_decl fmt decl =
753
  match decl.top_decl_desc with
754
  | Node nd ->
755
    fprintf fmt "%a %s" pp_node_vs_function nd nd.node_id
756
  | ImportedNode ind ->
757
    fprintf fmt "imported node %s" ind.nodei_id
758
  | Const c ->
759
    fprintf fmt "const %a" pp_const_decl c
760
  | Include s ->
761
    fprintf fmt "include \"%s\"" s
762
  | Open (local, s) ->
763
    if local then fprintf fmt "#open \"%s\"" s
764
    else fprintf fmt "#open <%s>" s
765
  | TypeDef tdef ->
766
    fprintf fmt "type %s" tdef.tydef_id
767

    
768
let pp_prog_short = pp_prog pp_short_decl
769

    
770
let pp_prog = pp_prog pp_decl
771

    
772
let pp_lusi fmt decl =
773
  match decl.top_decl_desc with
774
  | ImportedNode ind ->
775
    fprintf fmt "%a;@ " pp_imported_node ind
776
  | Const c ->
777
    fprintf fmt "const %a@ " pp_const_decl c
778
  | Include s ->
779
    fprintf fmt "include \"%s\"" s
780
  | Open (local, s) ->
781
    if local then fprintf fmt "#open \"%s\"@ " s
782
    else fprintf fmt "#open <%s>@ " s
783
  | TypeDef tdef ->
784
    fprintf fmt "%a@ " pp_typedef tdef
785
  | Node _ ->
786
    assert false
787

    
788
let pp_lusi_header fmt basename prog =
789
  fprintf fmt "@[<v 0>";
790
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
791
  fprintf
792
    fmt
793
    "(* by Lustre-C compiler version %s, %a *)@ "
794
    Version.number
795
    pp_date
796
    (Unix.gmtime (Unix.time ()));
797
  fprintf
798
    fmt
799
    "(* Feel free to mask some of the definitions by removing them from this \
800
     file. *)@ @ ";
801
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
802
  fprintf fmt "@]@."
803

    
804
(* XXX: UNUSED *)
805
(* let pp_offset fmt offset =
806
 *   match offset with
807
 *   | Index i ->
808
 *     fprintf fmt "[%a]" Dimension.pp i
809
 *   | Field f ->
810
 *     fprintf fmt ".%s" f *)
811

    
812
let pp_node_list fmt prog =
813
  Format.fprintf
814
    fmt
815
    "@[<h 2>%a@]"
816
    (pp_print_list (fun fmt decl ->
817
         match decl.top_decl_desc with
818
         | Node nd ->
819
           Format.fprintf fmt "%s" nd.node_id
820
         | _ ->
821
           ()))
822
    prog
823

    
824
(* Local Variables: *)
825
(* compile-command:"make -C .." *)
826
(* End: *)
(70-70/99)