Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ e8250987

History | View | Annotate | Download (17.5 KB)

1 a2d97a3e ploc
(********************************************************************)
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 8446bf03 ploc
open Lustre_types
13 22fe1c93 ploc
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 04a63d25 xthirioux
  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 22fe1c93 ploc
  begin
26 04a63d25 xthirioux
    pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
27 22fe1c93 ploc
    pp_fun fmt v;
28 04a63d25 xthirioux
    pp_set_formatter_out_functions fmt formatter_out_funs;
29 22fe1c93 ploc
  end
30
31 74ca6b61 ploc
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 ec433d69 xthirioux
  | Tydec_int -> fprintf fmt "int"
37 04a63d25 xthirioux
  | Tydec_real -> fprintf fmt "real"
38 74ca6b61 ploc
  (* | Tydec_float -> fprintf fmt "float" *)
39 ec433d69 xthirioux
  | Tydec_bool -> fprintf fmt "bool"
40 74ca6b61 ploc
  | 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 22fe1c93 ploc
49
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
50 74ca6b61 ploc
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 9f0f88dd ploc
  
57 22fe1c93 ploc
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
58
59 74ca6b61 ploc
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 af5af1e8 ploc
65
let pp_quantifiers fmt (q, vars) =
66
  match q with
67
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
68
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
69
70 12af4908 xthirioux
let rec pp_struct_const_field fmt (label, c) =
71
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
72
and pp_const fmt c = 
73 22fe1c93 ploc
  match c with
74
    | Const_int i -> pp_print_int fmt i
75 04a63d25 xthirioux
    | Const_real (c, e, s) -> pp_print_string fmt s (*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 *)
76
    (* | Const_float r -> pp_print_float fmt r *)
77 22fe1c93 ploc
    | Const_tag  t -> pp_print_string fmt t
78 34d3f022 ploc
    | Const_array ca -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
79
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
80
81
    (* used only for annotations *)
82 01c7d5e1 ploc
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
83 34d3f022 ploc
    | Const_modeid s -> pp_print_string fmt ("\"" ^ s ^ "\"")
84 22fe1c93 ploc
85
86 66359a5e ploc
let pp_annot_key fmt kwds =
87
  match kwds with
88
  | [] -> assert false
89 34d3f022 ploc
  | [x] -> pp_print_string fmt x
90
  | _ -> fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
91 66359a5e ploc
92 af5af1e8 ploc
let rec pp_expr fmt expr =
93
  (match expr.expr_annot with 
94
  | None -> fprintf fmt "%t" 
95 521e2a6b ploc
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
96 af5af1e8 ploc
    (fun fmt -> 
97
      match expr.expr_desc with
98 22fe1c93 ploc
    | Expr_const c -> pp_const fmt c
99 521e2a6b ploc
    | Expr_ident id -> fprintf fmt "%s" id
100 22fe1c93 ploc
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
101
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
102
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
103
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
104 521e2a6b ploc
    | 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
105 e2380d4d ploc
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
106 22fe1c93 ploc
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
107
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
108
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
109
    | Expr_merge (id, hl) -> 
110
      fprintf fmt "merge %s %a" id pp_handlers hl
111
    | Expr_appl (id, e, r) -> pp_app fmt id e r
112 af5af1e8 ploc
    )
113 22fe1c93 ploc
and pp_tuple fmt el =
114
 fprintf_list ~sep:"," pp_expr fmt el
115
116
and pp_handler fmt (t, h) =
117
 fprintf fmt "(%s -> %a)" t pp_expr h
118
119
and pp_handlers fmt hl =
120
 fprintf_list ~sep:" " pp_handler fmt hl
121
122
and pp_app fmt id e r =
123
  match r with
124 70df2f87 xthirioux
  | None -> pp_call fmt id e
125 54d032f5 xthirioux
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
126 70df2f87 xthirioux
127
and pp_call fmt id e =
128
  match id, e.expr_desc with
129
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
130
  | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
131
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
132
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
133
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
134
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
135
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
136
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
137
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
138
  | "impl", 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
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
141
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
142
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
143 2ae3ef3f ploc
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
144 70df2f87 xthirioux
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
145
  | "not", _ -> fprintf fmt "(not %a)" pp_expr e
146
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
147
  | _ -> fprintf fmt "%s (%a)" id pp_expr e
148 af5af1e8 ploc
149
and pp_eexpr fmt e =
150
  fprintf fmt "%a%t %a"
151
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
152
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
153
    pp_expr e.eexpr_qfexpr
154
155 1b57e111 Teme
and  pp_sf_value fmt e =
156
   fprintf fmt "%a"
157
     (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
158
     (* (fun fmt -> match e.eexpr_quantifiers *)
159
     (*             with [] -> () *)
160
     (*                | _ -> fprintf fmt ";") *)
161
     pp_expr e.eexpr_qfexpr
162
163
and pp_s_function fmt expr_ann =
164
  let pp_annot fmt (kwds, ee) =
165 34d3f022 ploc
    fprintf fmt " %t : %a"
166 1b57e111 Teme
                   (fun fmt -> match kwds with
167
                               | [] -> assert false
168 34d3f022 ploc
                               | [x] -> pp_print_string fmt x
169
                               | _ -> fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)
170 1b57e111 Teme
                   pp_sf_value ee
171
  in
172
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
173 af5af1e8 ploc
174
and pp_expr_annot fmt expr_ann =
175
  let pp_annot fmt (kwds, ee) =
176 34d3f022 ploc
    fprintf fmt "(*! %a: %a; *)"
177 66359a5e ploc
      pp_annot_key kwds
178 af5af1e8 ploc
      pp_eexpr ee
179
  in
180
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
181 27e5a70d ploc
182
183
let pp_asserts fmt asserts =
184
  match asserts with 
185
  | _::_ -> (
186
    fprintf fmt "(* Asserts definitions *)@ ";
187
    fprintf_list ~sep:"@ " (fun fmt assert_ -> 
188
      let expr = assert_.assert_expr in
189
      fprintf fmt "assert %a;" pp_expr expr 
190
    ) fmt asserts 
191
  )
192
  | _ -> ()
193
194 ec433d69 xthirioux
(*
195
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
196
*)
197
let pp_node_var fmt id =
198
  begin
199 74ca6b61 ploc
    fprintf fmt "%s%s: %a%a"
200
      (if id.var_dec_const then "const " else "")
201
      id.var_id
202
      pp_var_type id
203
      pp_var_clock id;
204 ec433d69 xthirioux
    match id.var_dec_value with
205
    | None -> () 
206
    | Some v -> fprintf fmt " = %a" pp_expr v
207
  end 
208
209 27e5a70d ploc
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var 
210 ec433d69 xthirioux
211 22fe1c93 ploc
let pp_node_eq fmt eq = 
212
  fprintf fmt "%a = %a;" 
213
    pp_eq_lhs eq.eq_lhs
214
    pp_expr eq.eq_rhs
215
216 b08ffca7 xthirioux
let pp_restart fmt restart =
217 34d3f022 ploc
  fprintf fmt "%s" (if restart then "restart" else "resume")
218 b08ffca7 xthirioux
219
let pp_unless fmt (_, expr, restart, st) =
220 34d3f022 ploc
  fprintf fmt "unless %a %a %s"
221 b08ffca7 xthirioux
    pp_expr expr
222
    pp_restart restart
223
    st
224
225
let pp_until fmt (_, expr, restart, st) =
226 34d3f022 ploc
  fprintf fmt "until %a %a %s"
227 b08ffca7 xthirioux
    pp_expr expr
228
    pp_restart restart
229
    st
230
231
let rec pp_handler fmt handler =
232 34d3f022 ploc
  fprintf fmt "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
233 b08ffca7 xthirioux
    handler.hand_state
234 27e5a70d ploc
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
235
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
236 b08ffca7 xthirioux
    (fun fmt locals ->
237
      match locals with [] -> () | _ ->
238 34d3f022 ploc
	fprintf fmt "@[<v 4>var %a@]@ " 
239 b08ffca7 xthirioux
	  (Utils.fprintf_list ~sep:"@ " 
240 34d3f022 ploc
	     (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
241 b08ffca7 xthirioux
	  locals)
242
    handler.hand_locals
243 27e5a70d ploc
    (fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots
244 b08ffca7 xthirioux
    pp_node_stmts handler.hand_stmts
245 27e5a70d ploc
    pp_asserts handler.hand_asserts
246 54d032f5 xthirioux
    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
247 b08ffca7 xthirioux
248
and pp_node_stmt fmt stmt =
249
  match stmt with
250
  | Eq eq -> pp_node_eq fmt eq
251
  | Aut aut -> pp_node_aut fmt aut
252
253
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
254
255
and pp_node_aut fmt aut =
256 34d3f022 ploc
  fprintf fmt "@[<v 0>automaton %s@,%a@]"
257 b08ffca7 xthirioux
    aut.aut_id
258
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
259
260
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
261 22fe1c93 ploc
262 ef34b4ae xthirioux
let pp_typedef fmt ty =
263 94cf0fc5 ploc
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
264 ef34b4ae xthirioux
265
let pp_typedec fmt ty =
266 94cf0fc5 ploc
  fprintf fmt "type %s;" ty.tydec_id
267 22fe1c93 ploc
268
(* let rec pp_var_type fmt ty =  *)
269
(*   fprintf fmt "%a" (match ty.tdesc with  *)
270
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
271
(*     | Tint -> pp_print_string fmt "int" *)
272
(*     | Treal -> pp_print_string fmt "real" *)
273
(*     | Tbool -> pp_print_string fmt "bool" *)
274
(*     | Trat -> pp_print_string fmt "rat" *)
275
(*     | Tclock -> pp_print_string fmt "clock"  *)
276
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
277
(*   ) *)
278
279 e2380d4d ploc
280 949b2e1e ploc
281
let pp_quantifiers fmt (q, vars) =
282
  match q with
283
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
284
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
285
286
let pp_eexpr fmt e =
287
  fprintf fmt "%a%t %a"
288
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
289
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
290
    pp_expr e.eexpr_qfexpr
291
292 217837e2 ploc
    
293
let pp_spec_eq fmt eq = 
294
  fprintf fmt "var %a : %a = %a;" 
295
    pp_eq_lhs eq.eq_lhs
296
    Types.print_node_ty eq.eq_rhs.expr_type
297
    pp_expr eq.eq_rhs
298
  
299
let pp_spec_stmt fmt stmt =
300
  match stmt with
301
  | Eq eq -> pp_spec_eq fmt eq
302
  | Aut aut -> assert false (* Not supported yet *)
303
             
304
  
305 e2380d4d ploc
let pp_spec fmt spec =
306 778c80fd ploc
  (* const are prefixed with const in pp_var and with nothing for regular
307
     variables. We adapt the call to produce the appropriate output. *)
308 217837e2 ploc
    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
309
    fprintf fmt "const %a = %t;"
310 778c80fd ploc
      pp_var v
311 217837e2 ploc
      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
312
    ) fmt spec.consts;
313
  
314
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
315
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
316
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
317
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
318 778c80fd ploc
    fprintf fmt "mode %s (@[@ %a@ %a@]);" 
319
      mode.mode_id
320 217837e2 ploc
      (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
321
      (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
322 778c80fd ploc
  ) fmt spec.modes;
323 217837e2 ploc
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
324 778c80fd ploc
    fprintf fmt "import %s (%a) returns (%a);" 
325
      import.import_nodeid
326
      (fprintf_list ~sep:"@ " pp_expr) import.inputs
327
      (fprintf_list ~sep:"@ " pp_expr) import.outputs
328 217837e2 ploc
  ) fmt spec.imports
329 e2380d4d ploc
330 217837e2 ploc
let pp_spec_as_comment fmt spec =
331
  fprintf fmt "@[<hov 2>(*@@ ";
332
  pp_spec fmt spec;
333
  fprintf fmt "@]*)@ "
334 af5af1e8 ploc
    
335 bc3139b0 ploc
let pp_node fmt nd =
336
  fprintf fmt "@[<v 0>";
337
  (* Prototype *)
338
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
339
    (if nd.node_dec_stateless then "function" else "node")
340
    nd.node_id
341
    pp_node_args nd.node_inputs
342
    pp_node_args nd.node_outputs;
343
  (* Contracts *)
344
  fprintf fmt "%a%t"
345 217837e2 ploc
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) nd.node_spec
346 bc3139b0 ploc
    (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ");
347
  (* Locals *)
348
  fprintf fmt "%a" (fun fmt locals ->
349
      match locals with [] -> () | _ ->
350
                                    fprintf fmt "@[<v 4>var %a@]@ " 
351
                                      (fprintf_list ~sep:"@ " 
352
	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
353
                                      locals
354
    ) nd.node_locals;
355
  (* Checks *)
356
  fprintf fmt "%a"
357
    (fun fmt checks ->
358
      match checks with [] -> () | _ ->
359
                                    fprintf fmt "@[<v 4>check@ %a@]@ " 
360
                                      (fprintf_list ~sep:"@ " 
361
	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
362
                                      checks
363
    ) nd.node_checks;
364
  (* Body *)
365
  fprintf fmt "let@[<h 2>   @ @[<v>";
366
  (* Annotations *)
367
  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
368
  (* Statements *)
369
  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;
370
  (* Asserts *)    
371
  fprintf fmt "%a" pp_asserts nd.node_asserts;
372
  (* closing boxes body (2)  and node (1) *) 
373
  fprintf fmt "@]@]@ tel@]@ "
374
375
376 22fe1c93 ploc
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
377
378
let pp_imported_node fmt ind = 
379 217837e2 ploc
  fprintf fmt "@[<v 0>";
380
  (* Prototype *)
381
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
382 52cfee34 xthirioux
    (if ind.nodei_stateless then "function" else "node")
383 22fe1c93 ploc
    ind.nodei_id
384
    pp_node_args ind.nodei_inputs
385 217837e2 ploc
    pp_node_args ind.nodei_outputs;
386
  (* Contracts *)
387
  fprintf fmt "%a%t"
388
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) ind.nodei_spec
389
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
390
  fprintf fmt "@]@ "
391
  
392 22fe1c93 ploc
393 ef34b4ae xthirioux
let pp_const_decl fmt cdecl =
394
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
395
396
let pp_const_decl_list fmt clist = 
397
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
398 54ae8ac7 ploc
399 34d3f022 ploc
400
  
401 22fe1c93 ploc
let pp_decl fmt decl =
402
  match decl.top_decl_desc with
403 94cf0fc5 ploc
  | Node nd -> fprintf fmt "%a" pp_node nd
404 22fe1c93 ploc
  | ImportedNode ind ->
405 34d3f022 ploc
     fprintf fmt "imported %a;" pp_imported_node ind
406 94cf0fc5 ploc
  | Const c -> fprintf fmt "const %a" pp_const_decl c
407
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
408 19a1e66b ploc
  | Include s -> fprintf fmt "include \"%s\"" s
409 94cf0fc5 ploc
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
410 34d3f022 ploc
  
411 753d4562 ploc
let pp_prog fmt prog =
412 333e3a25 ploc
  (* we first print types: the function SortProg.sort could do the job but ut
413
     introduces a cyclic dependance *)
414 a879351b ploc
415
  let open_decl, prog =
416
    List.partition (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false) prog
417
  in
418
  let type_decl, prog =
419 753d4562 ploc
    List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
420
  in
421 a879351b ploc
  fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (open_decl@type_decl@prog)
422 22fe1c93 ploc
423 34d3f022 ploc
(* Gives a short overview of model content. Do not print all node content *)
424 22fe1c93 ploc
let pp_short_decl fmt decl =
425
  match decl.top_decl_desc with
426
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
427
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
428 ef34b4ae xthirioux
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
429 19a1e66b ploc
  | Include s -> fprintf fmt "include \"%s\"" s
430 ef34b4ae xthirioux
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
431
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
432 0d54d8a8 ploc
  
433 5c1184ad ploc
let pp_lusi fmt decl = 
434
  match decl.top_decl_desc with
435 ef34b4ae xthirioux
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
436
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
437 19a1e66b ploc
  | Include s -> fprintf fmt "include \"%s\"" s
438 ef34b4ae xthirioux
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
439
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
440
  | Node _ -> assert false
441 34d3f022 ploc
                
442 ef34b4ae xthirioux
let pp_lusi_header fmt basename prog =
443 521e2a6b ploc
  fprintf fmt "@[<v 0>";
444
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
445
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
446
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
447
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
448 c4fb63af ploc
  fprintf fmt "@]@."
449 d7b73fed xthirioux
450
let pp_offset fmt offset =
451
  match offset with
452
  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
453
  | Field f -> fprintf fmt ".%s" f
454
455 22fe1c93 ploc
(* Local Variables: *)
456
(* compile-command:"make -C .." *)
457
(* End: *)