Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ 94cf0fc5

History | View | Annotate | Download (14.7 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 LustreSpec
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_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
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
  match c with
74
    | Const_int i -> pp_print_int fmt i
75
    | 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
    | Const_tag  t -> pp_print_string fmt t
78
    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
79
    | Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
80
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
81

    
82

    
83
let rec pp_expr fmt expr =
84
  (match expr.expr_annot with 
85
  | None -> fprintf fmt "%t" 
86
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
87
    (fun fmt -> 
88
      match expr.expr_desc with
89
    | Expr_const c -> pp_const fmt c
90
    | Expr_ident id -> fprintf fmt "%s" id
91
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
92
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
93
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
94
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
95
    | 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
96
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
97
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
98
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
99
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
100
    | Expr_merge (id, hl) -> 
101
      fprintf fmt "merge %s %a" id pp_handlers hl
102
    | Expr_appl (id, e, r) -> pp_app fmt id e r
103
    )
104
and pp_tuple fmt el =
105
 fprintf_list ~sep:"," pp_expr fmt el
106

    
107
and pp_handler fmt (t, h) =
108
 fprintf fmt "(%s -> %a)" t pp_expr h
109

    
110
and pp_handlers fmt hl =
111
 fprintf_list ~sep:" " pp_handler fmt hl
112

    
113
and pp_app fmt id e r =
114
  match r with
115
  | None -> pp_call fmt id e
116
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
117

    
118
and pp_call fmt id e =
119
  match id, e.expr_desc with
120
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
121
  | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
122
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
123
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
124
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
125
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
126
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
127
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
128
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
129
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
130
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
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
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
135
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
136
  | "not", _ -> fprintf fmt "(not %a)" pp_expr e
137
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
138
  | _ -> fprintf fmt "%s (%a)" id pp_expr e
139

    
140
and pp_eexpr fmt e =
141
  fprintf fmt "%a%t %a"
142
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
143
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
144
    pp_expr e.eexpr_qfexpr
145

    
146
and  pp_sf_value fmt e =
147
   fprintf fmt "%a"
148
     (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
149
     (* (fun fmt -> match e.eexpr_quantifiers *)
150
     (*             with [] -> () *)
151
     (*                | _ -> fprintf fmt ";") *)
152
     pp_expr e.eexpr_qfexpr
153

    
154
and pp_s_function fmt expr_ann =
155
  let pp_annot fmt (kwds, ee) =
156
    Format.fprintf fmt " %t : %a"
157
                   (fun fmt -> match kwds with
158
                               | [] -> assert false
159
                               | [x] -> Format.pp_print_string fmt x
160
                               | _ -> Format.fprintf fmt "%a" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
161
                   pp_sf_value ee
162
  in
163
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
164

    
165
and pp_expr_annot fmt expr_ann =
166
  let pp_annot fmt (kwds, ee) =
167
    Format.fprintf fmt "(*! %t: %a; *)"
168
      (fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
169
      pp_eexpr ee
170
  in
171
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
172

    
173

    
174
let pp_asserts fmt asserts =
175
  match asserts with 
176
  | _::_ -> (
177
    fprintf fmt "(* Asserts definitions *)@ ";
178
    fprintf_list ~sep:"@ " (fun fmt assert_ -> 
179
      let expr = assert_.assert_expr in
180
      fprintf fmt "assert %a;" pp_expr expr 
181
    ) fmt asserts 
182
  )
183
  | _ -> ()
184

    
185
(*
186
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
187
*)
188
let pp_node_var fmt id =
189
  begin
190
    fprintf fmt "%s%s: %a%a"
191
      (if id.var_dec_const then "const " else "")
192
      id.var_id
193
      pp_var_type id
194
      pp_var_clock id;
195
    match id.var_dec_value with
196
    | None -> () 
197
    | Some v -> fprintf fmt " = %a" pp_expr v
198
  end 
199

    
200
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var 
201

    
202
let pp_node_eq fmt eq = 
203
  fprintf fmt "%a = %a;" 
204
    pp_eq_lhs eq.eq_lhs
205
    pp_expr eq.eq_rhs
206

    
207
let pp_restart fmt restart =
208
  Format.fprintf fmt "%s" (if restart then "restart" else "resume")
209

    
210
let pp_unless fmt (_, expr, restart, st) =
211
  Format.fprintf fmt "unless %a %a %s"
212
    pp_expr expr
213
    pp_restart restart
214
    st
215

    
216
let pp_until fmt (_, expr, restart, st) =
217
  Format.fprintf fmt "until %a %a %s"
218
    pp_expr expr
219
    pp_restart restart
220
    st
221

    
222
let rec pp_handler fmt handler =
223
  Format.fprintf fmt "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
224
    handler.hand_state
225
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
226
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
227
    (fun fmt locals ->
228
      match locals with [] -> () | _ ->
229
	Format.fprintf fmt "@[<v 4>var %a@]@ " 
230
	  (Utils.fprintf_list ~sep:"@ " 
231
	     (fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v))
232
	  locals)
233
    handler.hand_locals
234
    (fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots
235
    pp_node_stmts handler.hand_stmts
236
    pp_asserts handler.hand_asserts
237
    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
238

    
239
and pp_node_stmt fmt stmt =
240
  match stmt with
241
  | Eq eq -> pp_node_eq fmt eq
242
  | Aut aut -> pp_node_aut fmt aut
243

    
244
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
245

    
246
and pp_node_aut fmt aut =
247
  Format.fprintf fmt "@[<v 0>automaton %s@,%a@]"
248
    aut.aut_id
249
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
250

    
251
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
252

    
253
let pp_typedef fmt ty =
254
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
255

    
256
let pp_typedec fmt ty =
257
  fprintf fmt "type %s;" ty.tydec_id
258

    
259
(* let rec pp_var_type fmt ty =  *)
260
(*   fprintf fmt "%a" (match ty.tdesc with  *)
261
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
262
(*     | Tint -> pp_print_string fmt "int" *)
263
(*     | Treal -> pp_print_string fmt "real" *)
264
(*     | Tbool -> pp_print_string fmt "bool" *)
265
(*     | Trat -> pp_print_string fmt "rat" *)
266
(*     | Tclock -> pp_print_string fmt "clock"  *)
267
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
268
(*   ) *)
269

    
270

    
271
let pp_spec fmt spec =
272
  fprintf fmt "@[<hov 2>(*@@ ";
273
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
274
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
275
  fprintf_list ~sep:"@," (fun fmt (name, assumes, ensures, _) -> 
276
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
277
      name
278
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
279
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
280
  ) fmt spec.behaviors;
281
  fprintf fmt "@]*)";
282
  ()
283

    
284
    
285
let pp_node fmt nd = 
286
fprintf fmt "@[<v 0>%a%t%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ %a%alet@[<h 2>   @ @[<v>%a@ %a@ %a@]@]@ tel@]@ "
287
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
288
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@ ")
289
  (if nd.node_dec_stateless then "function" else "node")
290
  nd.node_id
291
  pp_node_args nd.node_inputs
292
  pp_node_args nd.node_outputs
293
  (fun fmt locals ->
294
  match locals with [] -> () | _ ->
295
    fprintf fmt "@[<v 4>var %a@]@ " 
296
      (fprintf_list ~sep:"@ " 
297
	 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
298
      locals
299
  ) nd.node_locals
300
  (fun fmt checks ->
301
  match checks with [] -> () | _ ->
302
    fprintf fmt "@[<v 4>check@ %a@]@ " 
303
      (fprintf_list ~sep:"@ " 
304
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
305
      checks
306
  ) nd.node_checks
307
  (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
308
  pp_node_stmts nd.node_stmts
309
  pp_asserts nd.node_asserts
310
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
311

    
312
let pp_imported_node fmt ind = 
313
  fprintf fmt "@[<v>%s %s (%a) returns (%a)@]"
314
    (if ind.nodei_stateless then "function" else "node")
315
    ind.nodei_id
316
    pp_node_args ind.nodei_inputs
317
    pp_node_args ind.nodei_outputs
318

    
319
let pp_const_decl fmt cdecl =
320
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
321

    
322
let pp_const_decl_list fmt clist = 
323
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
324

    
325
let pp_decl fmt decl =
326
  match decl.top_decl_desc with
327
  | Node nd -> fprintf fmt "%a" pp_node nd
328
  | ImportedNode ind ->
329
    fprintf fmt "imported %a;" pp_imported_node ind
330
  | Const c -> fprintf fmt "const %a" pp_const_decl c
331
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
332
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
333

    
334
let pp_prog fmt prog =
335
  (* we first print types: the function SortProg.sort could do the job but ut
336
     introduces a cyclic dependance *)
337
  let type_decl, others =
338
    List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
339
  in
340
  fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (type_decl@others)
341

    
342
let pp_short_decl fmt decl =
343
  match decl.top_decl_desc with
344
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
345
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
346
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
347
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
348
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
349

    
350
let pp_lusi fmt decl = 
351
  match decl.top_decl_desc with
352
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
353
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
354
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
355
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
356
  | Node _ -> assert false
357

    
358
let pp_lusi_header fmt basename prog =
359
  fprintf fmt "@[<v 0>";
360
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
361
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
362
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
363
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
364
  fprintf fmt "@]@."
365

    
366
let pp_offset fmt offset =
367
  match offset with
368
  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
369
  | Field f -> fprintf fmt ".%s" f
370

    
371
(* Local Variables: *)
372
(* compile-command:"make -C .." *)
373
(* End: *)