Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ fbcd3ad1

History | View | Annotate | Download (19.4 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
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
17
   following the C convention for multiple lines macro *)
18
let pp_as_c_macro pp_fun fmt v =
19
  let formatter_out_funs = pp_get_formatter_out_functions fmt () in
20
  let macro_newline () =
21
    begin
22
      formatter_out_funs.out_string "\\" 0 1;
23
      formatter_out_funs.out_newline ()
24
    end in
25
  begin
26
    pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
27
    pp_fun fmt v;
28
    pp_set_formatter_out_functions fmt formatter_out_funs;
29
  end
30

    
31
let rec pp_var_struct_type_field fmt (label, tdesc) =
32
  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
33
and pp_var_type_dec_desc fmt tdesc =
34
  match tdesc with 
35
  | Tydec_any -> fprintf fmt "<any>"
36
  | Tydec_int -> fprintf fmt "int"
37
  | Tydec_real -> fprintf fmt "real"
38
  (* | Tydec_float -> fprintf fmt "float" *)
39
  | Tydec_bool -> fprintf fmt "bool"
40
  | Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
41
  | Tydec_const t -> fprintf fmt "%s" t
42
  | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
43
  | Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:" " pp_var_struct_type_field) f_list
44
  | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
45

    
46
let pp_var_type_dec fmt ty =
47
  pp_var_type_dec_desc fmt ty.ty_dec_desc
48

    
49
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
50
let pp_var_type fmt id =
51
  if !Options.print_dec_types then
52
    pp_var_type_dec fmt id.var_dec_type
53
  else
54
    Types.print_node_ty fmt id.var_type
55
let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock
56
  
57
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
58

    
59
let pp_var fmt id =
60
  fprintf fmt "%s%s: %a"
61
    (if id.var_dec_const then "const " else "")
62
    id.var_id
63
    pp_var_type id
64

    
65
let pp_vars fmt vars =
66
  fprintf_list ~sep:"; " pp_var fmt vars
67
  
68
let pp_quantifiers fmt (q, vars) =
69
  match q with
70
    | Forall -> fprintf fmt "forall %a" pp_vars vars 
71
    | Exists -> fprintf fmt "exists %a" pp_vars vars 
72

    
73
let rec pp_struct_const_field fmt (label, c) =
74
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
75
and pp_const fmt c = 
76
  match c with
77
    | Const_int i -> pp_print_int fmt i
78
    | Const_real (c, e, s) -> fprintf fmt "%s%s"
79
                                s
80
                                (if String.get s (-1 + String.length s) = '.' then "0" else "")
81
    (*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 *)
82
    (* | Const_float r -> pp_print_float fmt r *)
83
    | Const_tag  t -> pp_print_string fmt t
84
    | Const_array ca -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
85
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
86

    
87
    (* used only for annotations *)
88
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
89
    | Const_modeid s -> pp_print_string fmt ("\"" ^ s ^ "\"")
90

    
91

    
92
let pp_annot_key fmt kwds =
93
  match kwds with
94
  | [] -> assert false
95
  | [x] -> pp_print_string fmt x
96
  | _ -> fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
97

    
98
let rec pp_expr fmt expr =
99
  (match expr.expr_annot with 
100
  | None -> fprintf fmt "%t" 
101
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
102
    (fun fmt -> 
103
      match expr.expr_desc with
104
    | Expr_const c -> pp_const fmt c
105
    | Expr_ident id -> fprintf fmt "%s" id
106
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
107
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
108
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
109
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
110
    | 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
111
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
112
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
113
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
114
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
115
    | Expr_merge (id, hl) -> 
116
      fprintf fmt "merge %s %a" id pp_handlers hl
117
    | Expr_appl (id, e, r) -> pp_app fmt id e r
118
    )
119
and pp_tuple fmt el =
120
 fprintf_list ~sep:"," pp_expr fmt el
121

    
122
and pp_handler fmt (t, h) =
123
 fprintf fmt "(%s -> %a)" t pp_expr h
124

    
125
and pp_handlers fmt hl =
126
 fprintf_list ~sep:" " pp_handler fmt hl
127

    
128
and pp_app fmt id e r =
129
  match r with
130
  | None -> pp_call fmt id e
131
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
132

    
133
and pp_call fmt id e =
134
  match id, e.expr_desc with
135
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
136
  | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
137
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
138
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
139
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
140
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
141
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
142
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
143
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
144
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
145
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
146
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
147
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
148
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
149
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
150
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
151
  | "not", _ -> fprintf fmt "(not %a)" pp_expr e
152
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
153
  | _ -> fprintf fmt "%s (%a)" id pp_expr e
154

    
155
and pp_eexpr fmt e =
156
  fprintf fmt "%a%t %a"
157
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
158
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
159
    pp_expr e.eexpr_qfexpr
160

    
161
and  pp_sf_value fmt e =
162
   fprintf fmt "%a"
163
     (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
164
     (* (fun fmt -> match e.eexpr_quantifiers *)
165
     (*             with [] -> () *)
166
     (*                | _ -> fprintf fmt ";") *)
167
     pp_expr e.eexpr_qfexpr
168

    
169
and pp_s_function fmt expr_ann =
170
  let pp_annot fmt (kwds, ee) =
171
    fprintf fmt " %t : %a"
172
                   (fun fmt -> match kwds with
173
                               | [] -> assert false
174
                               | [x] -> pp_print_string fmt x
175
                               | _ -> fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)
176
                   pp_sf_value ee
177
  in
178
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
179

    
180
and pp_expr_annot fmt expr_ann =
181
  let pp_annot fmt (kwds, ee) =
182
    fprintf fmt "(*!%a: %a; *)"
183
      pp_annot_key kwds
184
      pp_eexpr ee
185
  in
186
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
187

    
188

    
189
let pp_asserts fmt asserts =
190
  match asserts with 
191
  | _::_ -> (
192
    fprintf fmt "(* Asserts definitions *)@ ";
193
    fprintf_list ~sep:"@ " (fun fmt assert_ -> 
194
      let expr = assert_.assert_expr in
195
      fprintf fmt "assert %a;" pp_expr expr 
196
    ) fmt asserts 
197
  )
198
  | _ -> ()
199

    
200
(*
201
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
202
*)
203
let pp_node_var fmt id =
204
  begin
205
    fprintf fmt "%s%s: %a%a"
206
      (if id.var_dec_const then "const " else "")
207
      id.var_id
208
      pp_var_type id
209
      pp_var_clock id;
210
    match id.var_dec_value with
211
    | None -> () 
212
    | Some v -> fprintf fmt " = %a" pp_expr v
213
  end 
214

    
215
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var 
216

    
217
let pp_node_eq fmt eq = 
218
  fprintf fmt "%a = %a;" 
219
    pp_eq_lhs eq.eq_lhs
220
    pp_expr eq.eq_rhs
221

    
222
let pp_restart fmt restart =
223
  fprintf fmt "%s" (if restart then "restart" else "resume")
224

    
225
let pp_unless fmt (_, expr, restart, st) =
226
  fprintf fmt "unless %a %a %s"
227
    pp_expr expr
228
    pp_restart restart
229
    st
230

    
231
let pp_until fmt (_, expr, restart, st) =
232
  fprintf fmt "until %a %a %s"
233
    pp_expr expr
234
    pp_restart restart
235
    st
236

    
237
let rec pp_handler fmt handler =
238
  fprintf fmt "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
239
    handler.hand_state
240
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
241
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
242
    (fun fmt locals ->
243
      match locals with [] -> () | _ ->
244
	fprintf fmt "@[<v 4>var %a@]@ " 
245
	  (Utils.fprintf_list ~sep:"@ " 
246
	     (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
247
	  locals)
248
    handler.hand_locals
249
    (fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots
250
    pp_node_stmts handler.hand_stmts
251
    pp_asserts handler.hand_asserts
252
    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
253

    
254
and pp_node_stmt fmt stmt =
255
  match stmt with
256
  | Eq eq -> pp_node_eq fmt eq
257
  | Aut aut -> pp_node_aut fmt aut
258

    
259
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
260

    
261
and pp_node_aut fmt aut =
262
  fprintf fmt "@[<v 0>automaton %s@,%a@]"
263
    aut.aut_id
264
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
265

    
266
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
267

    
268
let pp_typedef fmt ty =
269
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
270

    
271
let pp_typedec fmt ty =
272
  fprintf fmt "type %s;" ty.tydec_id
273

    
274
(* let rec pp_var_type fmt ty =  *)
275
(*   fprintf fmt "%a" (match ty.tdesc with  *)
276
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
277
(*     | Tint -> pp_print_string fmt "int" *)
278
(*     | Treal -> pp_print_string fmt "real" *)
279
(*     | Tbool -> pp_print_string fmt "bool" *)
280
(*     | Trat -> pp_print_string fmt "rat" *)
281
(*     | Tclock -> pp_print_string fmt "clock"  *)
282
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
283
(*   ) *)
284

    
285

    
286

    
287
(* let pp_quantifiers fmt (q, vars) =
288
 *   match q with
289
 *     | Forall -> fprintf fmt "forall %a" pp_vars vars 
290
 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars  *)
291

    
292
(*let pp_eexpr fmt e =
293
  fprintf fmt "%a%t %a"
294
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
295
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
296
    pp_expr e.eexpr_qfexpr
297
 *)
298
    
299
let pp_spec_eq fmt eq = 
300
  fprintf fmt "var %a : %a = %a;" 
301
    pp_eq_lhs eq.eq_lhs
302
    Types.print_node_ty eq.eq_rhs.expr_type
303
    pp_expr eq.eq_rhs
304
  
305
let pp_spec_stmt fmt stmt =
306
  match stmt with
307
  | Eq eq -> pp_spec_eq fmt eq
308
  | Aut aut -> assert false (* Not supported yet *)
309
             
310
  
311
let pp_spec fmt spec =
312
  (* const are prefixed with const in pp_var and with nothing for regular
313
     variables. We adapt the call to produce the appropriate output. *)
314
    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
315
    fprintf fmt "%a = %t;"
316
      pp_var v
317
      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
318
    ) fmt spec.consts;
319
  
320
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
321
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
322
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r) fmt spec.guarantees;
323
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
324
    fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" 
325
      mode.mode_id
326
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
327
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
328
  ) fmt spec.modes;
329
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
330
    fprintf fmt "import %s (%a) returns (%a);" 
331
      import.import_nodeid
332
      pp_expr import.inputs
333
      pp_expr import.outputs
334
  ) fmt spec.imports
335

    
336
(* Project the contract node as a pure contract: local memories are pushed back in the contract definition. Should mainly be used to print it *) 
337
let node_as_contract nd =
338
  match nd.node_spec with
339
  | None | Some (NodeSpec _) -> raise (Invalid_argument "Not a contract")
340
  | Some (Contract c) -> (
341
    (* While a processed contract shall have no locals, sttms nor
342
       consts, an unprocessed one could. So we conservatively merge
343
       elements, to enable printing unprocessed contracts *)
344
    let consts, locals = List.partition(fun v -> v.var_dec_const) nd.node_locals in
345
    { c with
346
      consts = consts @ c.consts;
347
      locals = locals @ c.locals;
348
      stmts = nd.node_stmts @ c.stmts;
349
    }
350
  )
351
  
352
let pp_contract fmt nd =    
353
  
354
  let c = node_as_contract nd in
355
  fprintf fmt "@[<v 2>(*@contract %s(%a) returns (%a);@ "
356
    nd.node_id
357
    pp_node_args nd.node_inputs
358
    pp_node_args nd.node_outputs;
359
  fprintf fmt "@[<v 2>let@ ";
360
  pp_spec fmt c;
361
  fprintf fmt "@]@ tel@ @]*)@ "        
362
    
363
let pp_spec_as_comment fmt (inl, outl, spec) =
364
  match spec with
365
  | Contract c -> (* should have been processed by now *)
366
     fprintf fmt "@[<hov 2>(*@contract@ ";
367
     pp_spec fmt c;
368
     fprintf fmt "@]*)@ "
369
     
370
  | NodeSpec name -> (* Pushing stmts in contract. We update the
371
                      original information with the computed one in
372
                      nd. *)
373
     let pp_l = fprintf_list ~sep:"," pp_var_name in
374
     fprintf fmt "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ "
375
       name
376
       pp_l inl
377
       pp_l outl
378
     
379
              
380
let pp_node fmt nd =
381
  fprintf fmt "@[<v 0>";
382
  (* Prototype *)
383
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
384
    (if nd.node_dec_stateless then "function" else "node")
385
    nd.node_id
386
    pp_node_args nd.node_inputs
387
    pp_node_args nd.node_outputs;
388
  (* Contracts *)
389
  fprintf fmt "%a"
390
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s) | _ -> ()) nd.node_spec
391
    (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ") *);
392
  (* Locals *)
393
  fprintf fmt "%a" (fun fmt locals ->
394
      match locals with [] -> () | _ ->
395
                                    fprintf fmt "@[<v 4>var %a@]@ " 
396
                                      (fprintf_list ~sep:"@ " 
397
	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
398
                                      locals
399
    ) nd.node_locals;
400
  (* Checks *)
401
  fprintf fmt "%a"
402
    (fun fmt checks ->
403
      match checks with [] -> () | _ ->
404
                                    fprintf fmt "@[<v 4>check@ %a@]@ " 
405
                                      (fprintf_list ~sep:"@ " 
406
	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
407
                                      checks
408
    ) nd.node_checks;
409
  (* Body *)
410
  fprintf fmt "let@[<h 2>   @ @[<v>";
411
  (* Annotations *)
412
  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
413
  (* Statements *)
414
  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;
415
  (* Asserts *)    
416
  fprintf fmt "%a" pp_asserts nd.node_asserts;
417
  (* closing boxes body (2)  and node (1) *) 
418
  fprintf fmt "@]@]@ tel@]@ "
419

    
420

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

    
423
let pp_node fmt nd =
424
  match nd.node_spec, nd.node_iscontract with
425
  | None, false
426
    | Some (NodeSpec _), false 
427
    -> pp_node fmt nd
428
  | Some (Contract _), false -> pp_node fmt nd (* may happen early in the compil process *)
429
  | Some (Contract _), true -> pp_contract fmt nd 
430
  | _ -> assert false
431
     
432
let pp_imported_node fmt ind = 
433
  fprintf fmt "@[<v 0>";
434
  (* Prototype *)
435
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
436
    (if ind.nodei_stateless then "function" else "node")
437
    ind.nodei_id
438
    pp_node_args ind.nodei_inputs
439
    pp_node_args ind.nodei_outputs;
440
  (* Contracts *)
441
  fprintf fmt "%a%t"
442
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s) | _ -> ()) ind.nodei_spec
443
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
444
  fprintf fmt "@]@ "
445
  
446

    
447
let pp_const_decl fmt cdecl =
448
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
449

    
450
let pp_const_decl_list fmt clist = 
451
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
452

    
453

    
454
  
455
let pp_decl fmt decl =
456
  match decl.top_decl_desc with
457
  | Node nd -> fprintf fmt "%a" pp_node nd
458
  | ImportedNode ind -> (* We do not print imported nodes *)
459
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
460
  | Const c -> fprintf fmt "const %a" pp_const_decl c
461
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
462
  | Include s -> fprintf fmt "include \"%s\"" s
463
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
464
  
465
let pp_prog fmt prog =
466
  (* we first print types: the function SortProg.sort could do the job but ut
467
     introduces a cyclic dependance *)
468

    
469
  let open_decl, prog =
470
    List.partition (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false) prog
471
  in
472
  let type_decl, prog =
473
    List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
474
  in
475
  fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (open_decl@type_decl@prog)
476

    
477
(* Gives a short overview of model content. Do not print all node content *)
478
let pp_short_decl fmt decl =
479
  match decl.top_decl_desc with
480
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
481
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
482
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
483
  | Include s -> fprintf fmt "include \"%s\"" s
484
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
485
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
486
  
487
let pp_lusi fmt decl = 
488
  match decl.top_decl_desc with
489
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
490
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
491
  | Include s -> fprintf fmt "include \"%s\"" s
492
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
493
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
494
  | Node _ -> assert false
495
                
496
let pp_lusi_header fmt basename prog =
497
  fprintf fmt "@[<v 0>";
498
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
499
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
500
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
501
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
502
  fprintf fmt "@]@."
503

    
504
let pp_offset fmt offset =
505
  match offset with
506
  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
507
  | Field f -> fprintf fmt ".%s" f
508

    
509
(* Local Variables: *)
510
(* compile-command:"make -C .." *)
511
(* End: *)