Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ a0c92fa8

History | View | Annotate | Download (22.6 KB)

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 Format
14
open Utils
15

    
16
let kind2_language_cst =
17
  [ "initial" ]
18
  
19
let kind2_protect id =
20
  if List.mem id kind2_language_cst then
21
    "_KIND2_PROTECT_" ^ id
22
  else
23
    id
24
  
25
   
26
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
27
   following the C convention for multiple lines macro *)
28
let pp_as_c_macro pp_fun fmt v =
29
  let formatter_out_funs = pp_get_formatter_out_functions fmt () in
30
  let macro_newline () =
31
    begin
32
      formatter_out_funs.out_string "\\" 0 1;
33
      formatter_out_funs.out_newline ()
34
    end in
35
  begin
36
    pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
37
    pp_fun fmt v;
38
    pp_set_formatter_out_functions fmt formatter_out_funs;
39
  end
40

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

    
56
let pp_var_type_dec fmt ty =
57
  pp_var_type_dec_desc fmt ty.ty_dec_desc
58

    
59
let pp_var_name fmt id =
60
  fprintf fmt "%s" (if !Options.kind2_print then kind2_protect id.var_id else id.var_id) 
61

    
62
let pp_var_type fmt id =
63
  if !Options.print_dec_types then
64
    pp_var_type_dec fmt id.var_dec_type
65
  else
66
    Types.print_node_ty fmt id.var_type
67
let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock
68
  
69
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
70

    
71
let pp_var fmt id =
72
  fprintf fmt "%s%s: %a"
73
    (if id.var_dec_const then "const " else "")
74
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
75
    pp_var_type id
76

    
77
let pp_vars fmt vars =
78
  fprintf_list ~sep:"; " pp_var fmt vars
79
  
80
let pp_quantifiers fmt (q, vars) =
81
  match q with
82
    | Forall -> fprintf fmt "forall %a" pp_vars vars 
83
    | Exists -> fprintf fmt "exists %a" pp_vars vars 
84

    
85
let rec pp_struct_const_field fmt (label, c) =
86
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
87
and pp_const fmt c = 
88
  match c with
89
    | Const_int i -> pp_print_int fmt i
90
    | Const_real r -> Real.pp fmt r
91
    (*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt "%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)
92
    (* | Const_float r -> pp_print_float fmt r *)
93
    | Const_tag  t -> pp_print_string fmt t
94
    | Const_array ca -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
95
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
96

    
97
    (* used only for annotations *)
98
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
99
    | Const_modeid s -> pp_print_string fmt ("\"" ^ s ^ "\"")
100

    
101

    
102
let pp_annot_key fmt kwds =
103
  match kwds with
104
  | [] -> assert false
105
  | [x] -> pp_print_string fmt x
106
  | _ -> fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
107

    
108
let pp_kind2_when fmt (id, l) =
109
  if l = "true" then 
110
    fprintf fmt "%s" id
111
  else if l = "false" then
112
    fprintf fmt "not(%s)" id
113
  else
114
    fprintf fmt "(%s=%s)" l id
115
       
116
  
117
let rec pp_expr fmt expr =
118
  (match expr.expr_annot with 
119
   | None -> fprintf fmt "%t" 
120
   | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
121
    (fun fmt ->
122
      let pp fmt = 
123
      match expr.expr_desc with
124
      | Expr_const c -> pp_const fmt c
125
      | Expr_ident id ->
126
         fprintf fmt "%s"
127
           (if !Options.kind2_print then kind2_protect id else id)
128

    
129
      | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
130
      | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
131
      | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
132
      | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
133
      | Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_expr c pp_expr t pp_expr e
134
      | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
135
      | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
136
      | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
137
      | Expr_when (e, id, l) ->
138
         if !Options.kind2_print then
139
           fprintf fmt "%a when %a" pp_expr e pp_kind2_when (l, id)
140
         else
141
           fprintf fmt "%a when %s(%s)" pp_expr e l id
142
      | Expr_merge (id, hl) -> 
143
         fprintf fmt "merge %s %a" id pp_handlers hl
144
      | Expr_appl (id, e, r) -> pp_app fmt id e r
145
      in
146
      if false (* extra debug *)
147
      then
148
        Format.fprintf fmt "%t: %a" pp Types.print_ty expr.expr_type 
149
      else
150
        pp fmt
151
    )
152
and pp_tuple fmt el =
153
  fprintf_list ~sep:"," pp_expr fmt el
154

    
155
and pp_handler fmt (t, h) =
156
  fprintf fmt "(%s -> %a)" t pp_expr h
157

    
158
and pp_handlers fmt hl =
159
  fprintf_list ~sep:" " pp_handler fmt hl
160

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

    
218
  else (
219
    match r with
220
    | None -> pp_call fmt id e
221
    | Some c ->
222
       fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
223
  )
224
  
225
and pp_call fmt id e =
226
  match id, e.expr_desc with
227
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
228
  | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
229
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
230
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
231
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
232
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
233
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
234
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
235
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
236
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
237
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
238
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
239
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
240
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
241
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
242
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
243
  | "not", _ -> fprintf fmt "(not %a)" pp_expr e
244
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
245
  | _ -> fprintf fmt "%s (%a)" id pp_expr e
246

    
247
and pp_eexpr fmt e =
248
  fprintf fmt "%a%t %a"
249
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
250
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
251
    pp_expr e.eexpr_qfexpr
252

    
253
and  pp_sf_value fmt e =
254
  fprintf fmt "%a"
255
    (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
256
    (* (fun fmt -> match e.eexpr_quantifiers *)
257
    (*             with [] -> () *)
258
    (*                | _ -> fprintf fmt ";") *)
259
    pp_expr e.eexpr_qfexpr
260

    
261
and pp_s_function fmt expr_ann =
262
  let pp_annot fmt (kwds, ee) =
263
    fprintf fmt " %t : %a"
264
      (fun fmt -> match kwds with
265
                  | [] -> assert false
266
                  | [x] -> pp_print_string fmt x
267
                  | _ -> fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)
268
      pp_sf_value ee
269
  in
270
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
271

    
272
and pp_expr_annot fmt expr_ann =
273
  let pp_annot fmt (kwds, ee) =
274
    fprintf fmt "(*!%a: %a; *)"
275
      pp_annot_key kwds
276
      pp_eexpr ee
277
  in
278
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
279
 
280

    
281
let pp_asserts fmt asserts =
282
  match asserts with 
283
  | _::_ -> (
284
    fprintf fmt "(* Asserts definitions *)@ ";
285
    fprintf_list ~sep:"@ " (fun fmt assert_ -> 
286
      let expr = assert_.assert_expr in
287
      fprintf fmt "assert %a;" pp_expr expr 
288
    ) fmt asserts 
289
  )
290
  | _ -> ()
291

    
292
(*
293
let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock
294
*)
295
let pp_node_var fmt id =
296
  begin
297
    fprintf fmt "%s%s: %a%a"
298
      (if id.var_dec_const then "const " else "")
299
      (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
300
      pp_var_type id
301
      pp_var_clock id;
302
    match id.var_dec_value with
303
    | None -> () 
304
    | Some v -> fprintf fmt " = %a" pp_expr v
305
  end 
306

    
307
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var 
308

    
309
let pp_node_eq fmt eq = 
310
  fprintf fmt "%a = %a;" 
311
    pp_eq_lhs eq.eq_lhs
312
    pp_expr eq.eq_rhs
313

    
314
let pp_restart fmt restart =
315
  fprintf fmt "%s" (if restart then "restart" else "resume")
316

    
317
let pp_unless fmt (_, expr, restart, st) =
318
  fprintf fmt "unless %a %a %s"
319
    pp_expr expr
320
    pp_restart restart
321
    st
322

    
323
let pp_until fmt (_, expr, restart, st) =
324
  fprintf fmt "until %a %a %s"
325
    pp_expr expr
326
    pp_restart restart
327
    st
328

    
329
let rec pp_handler fmt handler =
330
  fprintf fmt "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
331
    handler.hand_state
332
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
333
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
334
    (fun fmt locals ->
335
      match locals with [] -> () | _ ->
336
	fprintf fmt "@[<v 4>var %a@]@ " 
337
	  (Utils.fprintf_list ~sep:"@ " 
338
	     (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
339
	  locals)
340
    handler.hand_locals
341
    (fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots
342
    pp_node_stmts handler.hand_stmts
343
    pp_asserts handler.hand_asserts
344
    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
345

    
346
and pp_node_stmt fmt stmt =
347
  match stmt with
348
  | Eq eq -> pp_node_eq fmt eq
349
  | Aut aut -> pp_node_aut fmt aut
350

    
351
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
352

    
353
and pp_node_aut fmt aut =
354
  fprintf fmt "@[<v 0>automaton %s@,%a@]"
355
    aut.aut_id
356
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
357

    
358
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
359

    
360
let pp_typedef fmt ty =
361
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
362

    
363
let pp_typedec fmt ty =
364
  fprintf fmt "type %s;" ty.tydec_id
365

    
366
(* let rec pp_var_type fmt ty =  *)
367
(*   fprintf fmt "%a" (match ty.tdesc with  *)
368
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
369
(*     | Tint -> pp_print_string fmt "int" *)
370
(*     | Treal -> pp_print_string fmt "real" *)
371
(*     | Tbool -> pp_print_string fmt "bool" *)
372
(*     | Trat -> pp_print_string fmt "rat" *)
373
(*     | Tclock -> pp_print_string fmt "clock"  *)
374
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
375
(*   ) *)
376

    
377

    
378

    
379
(* let pp_quantifiers fmt (q, vars) =
380
 *   match q with
381
 *     | Forall -> fprintf fmt "forall %a" pp_vars vars 
382
 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars  *)
383

    
384
(*let pp_eexpr fmt e =
385
  fprintf fmt "%a%t %a"
386
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
387
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
388
    pp_expr e.eexpr_qfexpr
389
 *)
390
    
391
let pp_spec_eq fmt eq = 
392
  fprintf fmt "var %a : %a = %a;" 
393
    pp_eq_lhs eq.eq_lhs
394
    Types.print_node_ty eq.eq_rhs.expr_type
395
    pp_expr eq.eq_rhs
396
  
397
let pp_spec_stmt fmt stmt =
398
  match stmt with
399
  | Eq eq -> pp_spec_eq fmt eq
400
  | Aut aut -> assert false (* Not supported yet *)
401
             
402
  
403
let pp_spec fmt spec =
404
  (* const are prefixed with const in pp_var and with nothing for regular
405
     variables. We adapt the call to produce the appropriate output. *)
406
    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
407
    fprintf fmt "%a = %t;"
408
      pp_var v
409
      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
410
    ) fmt spec.consts;
411
  
412
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
413
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
414
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r) fmt spec.guarantees;
415
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
416
    fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" 
417
      mode.mode_id
418
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
419
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
420
  ) fmt spec.modes;
421
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
422
    fprintf fmt "import %s (%a) returns (%a);" 
423
      import.import_nodeid
424
      pp_expr import.inputs
425
      pp_expr import.outputs
426
  ) fmt spec.imports
427

    
428
(* Project the contract node as a pure contract: local memories are pushed back in the contract definition. Should mainly be used to print it *) 
429
let node_as_contract nd =
430
  match nd.node_spec with
431
  | None | Some (NodeSpec _) -> raise (Invalid_argument "Not a contract")
432
  | Some (Contract c) -> (
433
    (* While a processed contract shall have no locals, sttms nor
434
       consts, an unprocessed one could. So we conservatively merge
435
       elements, to enable printing unprocessed contracts *)
436
    let consts, locals = List.partition(fun v -> v.var_dec_const) nd.node_locals in
437
    { c with
438
      consts = consts @ c.consts;
439
      locals = locals @ c.locals;
440
      stmts = nd.node_stmts @ c.stmts;
441
    }
442
  )
443

    
444
(* Printing top contract as comments in regular output and as contract
445
   in kind2 *)
446
let pp_contract fmt nd =    
447
   let c = node_as_contract nd in
448
  fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "
449
    (if !Options.kind2_print then "" else "(*@")
450
    nd.node_id
451
    pp_node_args nd.node_inputs
452
    pp_node_args nd.node_outputs;
453
  fprintf fmt "@[<v 2>let@ ";
454
  pp_spec fmt c;
455
  fprintf fmt "@]@ tel@ @]%s@ "
456
  (if !Options.kind2_print then "" else "*)")
457
    
458
let pp_spec_as_comment fmt (inl, outl, spec) =
459
  match spec with
460
  | Contract c -> (* should have been processed by now *)
461
     fprintf fmt "@[<hov 2>(*@contract@ ";
462
     pp_spec fmt c;
463
     fprintf fmt "@]*)@ "
464
     
465
  | NodeSpec name -> (* Pushing stmts in contract. We update the
466
                      original information with the computed one in
467
                      nd. *)
468
     let pp_l = fprintf_list ~sep:"," pp_var_name in
469
     fprintf fmt "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ "
470
       name
471
       pp_l inl
472
       pp_l outl
473
     
474
              
475
let pp_node fmt nd =
476
  fprintf fmt "@[<v 0>";
477
  (* Prototype *)
478
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
479
    (if nd.node_dec_stateless then "function" else "node")
480
    nd.node_id
481
    pp_node_args nd.node_inputs
482
    pp_node_args nd.node_outputs;
483
  (* Contracts *)
484
  fprintf fmt "%a"
485
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s) | _ -> ()) nd.node_spec
486
    (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ") *);
487
  (* Locals *)
488
  fprintf fmt "%a" (fun fmt locals ->
489
      match locals with [] -> () | _ ->
490
                                    fprintf fmt "@[<v 4>var %a@]@ " 
491
                                      (fprintf_list ~sep:"@ " 
492
	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
493
                                      locals
494
    ) nd.node_locals;
495
  (* Checks *)
496
  fprintf fmt "%a"
497
    (fun fmt checks ->
498
      match checks with [] -> () | _ ->
499
                                    fprintf fmt "@[<v 4>check@ %a@]@ " 
500
                                      (fprintf_list ~sep:"@ " 
501
	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
502
                                      checks
503
    ) nd.node_checks;
504
  (* Body *)
505
  fprintf fmt "let@[<h 2>   @ @[<v>";
506
  (* Annotations *)
507
  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
508
  (* Statements *)
509
  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;
510
  (* Asserts *)    
511
  fprintf fmt "%a" pp_asserts nd.node_asserts;
512
  (* closing boxes body (2)  and node (1) *) 
513
  fprintf fmt "@]@]@ tel@]@ "
514

    
515

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

    
518
let pp_node fmt nd =
519
  match nd.node_spec, nd.node_iscontract with
520
  | None, false
521
    | Some (NodeSpec _), false 
522
    -> pp_node fmt nd
523
  | Some (Contract _), false -> pp_node fmt nd (* may happen early in the compil process *)
524
  | Some (Contract _), true -> pp_contract fmt nd 
525
  | _ -> assert false
526
     
527
let pp_imported_node fmt ind = 
528
  fprintf fmt "@[<v 0>";
529
  (* Prototype *)
530
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
531
    (if ind.nodei_stateless then "function" else "node")
532
    ind.nodei_id
533
    pp_node_args ind.nodei_inputs
534
    pp_node_args ind.nodei_outputs;
535
  (* Contracts *)
536
  fprintf fmt "%a%t"
537
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s) | _ -> ()) ind.nodei_spec
538
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
539
  fprintf fmt "@]@ "
540
  
541

    
542
let pp_const_decl fmt cdecl =
543
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
544

    
545
let pp_const_decl_list fmt clist = 
546
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
547

    
548

    
549
  
550
let pp_decl fmt decl =
551
  match decl.top_decl_desc with
552
  | Node nd -> fprintf fmt "%a" pp_node nd
553
  | ImportedNode ind -> (* We do not print imported nodes *)
554
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
555
  | Const c -> fprintf fmt "const %a" pp_const_decl c
556
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
557
  | Include s -> fprintf fmt "include \"%s\"" s
558
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
559
  
560
let pp_prog fmt prog =
561
  (* we first print types: the function SortProg.sort could do the job but ut
562
     introduces a cyclic dependance *)
563

    
564
  let open_decl, prog =
565
    List.partition (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false) prog
566
  in
567
  let type_decl, prog =
568
    List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
569
  in
570
  fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (open_decl@type_decl@prog)
571

    
572
(* Gives a short overview of model content. Do not print all node content *)
573
let pp_short_decl fmt decl =
574
  match decl.top_decl_desc with
575
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
576
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
577
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
578
  | Include s -> fprintf fmt "include \"%s\"" s
579
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
580
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
581
  
582
let pp_lusi fmt decl = 
583
  match decl.top_decl_desc with
584
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
585
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
586
  | Include s -> fprintf fmt "include \"%s\"" s
587
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
588
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
589
  | Node _ -> assert false
590
                
591
let pp_lusi_header fmt basename prog =
592
  fprintf fmt "@[<v 0>";
593
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
594
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
595
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
596
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
597
  fprintf fmt "@]@."
598

    
599
let pp_offset fmt offset =
600
  match offset with
601
  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
602
  | Field f -> fprintf fmt ".%s" f
603

    
604
let pp_node_list fmt prog =
605
  Format.fprintf fmt "@[<h 2>%a@]"
606
    (fprintf_list
607
       ~sep:"@ "
608
       (fun fmt decl ->
609
         match decl.top_decl_desc with
610
         | Node nd -> Format.fprintf fmt "%s" nd.node_id
611
         | _ -> ()
612
    ))
613
    prog
614
    
615
(* Local Variables: *)
616
(* compile-command:"make -C .." *)
617
(* End: *)