Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ b38ffff3

History | View | Annotate | Download (14.2 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 Corelang
13
open LustreSpec
14
open Format
15
open Utils
16

    
17
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
18
   following the C convention for multiple lines macro *)
19
let pp_as_c_macro pp_fun fmt v =
20
  let (out, flush, newline, spaces) = pp_get_all_formatter_output_functions fmt () in
21
  let macro_newline () = (out "\\" 0 1; newline ()) in
22
  begin
23
    pp_set_all_formatter_output_functions fmt out flush macro_newline spaces;
24
    pp_fun fmt v;
25
    pp_set_all_formatter_output_functions fmt out flush newline spaces;
26
  end
27

    
28

    
29
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
30

    
31
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
32

    
33
let pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
34

    
35
let pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock
36

    
37
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
38

    
39
let pp_quantifiers fmt (q, vars) =
40
  match q with
41
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
42
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
43

    
44
(*
45
let pp_econst fmt c = 
46
  match c with
47
    | EConst_int i -> pp_print_int fmt i
48
    | EConst_real r -> pp_print_string fmt r
49
    | EConst_float r -> pp_print_float fmt r
50
    | EConst_tag  t -> pp_print_string fmt t
51
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
52

    
53

    
54
let rec pp_eexpr fmt eexpr = 
55
  match eexpr.eexpr_desc with
56
    | EExpr_const c -> pp_econst fmt c
57
    | EExpr_ident id -> pp_print_string fmt id
58
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
59
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
60
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
61
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
62
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
63
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
64
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
65
    | EExpr_merge (id, e1, e2) -> 
66
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
67
    | EExpr_appl (id, e, r) -> pp_eapp fmt id e r
68
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
69
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
70

    
71

    
72
    (* | EExpr_whennot _ *)
73
    (* | EExpr_uclock _ *)
74
    (* | EExpr_dclock _ *)
75
    (* | EExpr_phclock _ -> assert false *)
76
and pp_eapp fmt id e r =
77
  match r with
78
  | None ->
79
    (match id, e.eexpr_desc with
80
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
81
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
82
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
83
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
84
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
85
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
86
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
87
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
88
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
89
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
90
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
91
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
92
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
93
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
94
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
95
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
96
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
97
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
98
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
99
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
100
*)
101

    
102

    
103
let rec pp_struct_const_field fmt (label, c) =
104
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
105
and pp_const fmt c = 
106
  match c with
107
    | Const_int i -> pp_print_int fmt i
108
    | Const_real r -> pp_print_string fmt r
109
    | Const_float r -> pp_print_float fmt r
110
    | Const_tag  t -> pp_print_string fmt t
111
    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
112
    | Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
113
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
114

    
115

    
116
let rec pp_expr fmt expr =
117
  (match expr.expr_annot with 
118
  | None -> fprintf fmt "%t" 
119
  | Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann)
120
    (fun fmt -> 
121
      match expr.expr_desc with
122
    | Expr_const c -> pp_const fmt c
123
    | Expr_ident id -> Format.fprintf fmt "%s" id
124
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
125
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
126
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
127
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
128
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
129
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
130
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
131
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
132
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
133
    | Expr_merge (id, hl) -> 
134
      fprintf fmt "merge %s %a" id pp_handlers hl
135
    | Expr_appl (id, e, r) -> pp_app fmt id e r
136
    )
137
and pp_tuple fmt el =
138
 fprintf_list ~sep:"," pp_expr fmt el
139

    
140
and pp_handler fmt (t, h) =
141
 fprintf fmt "(%s -> %a)" t pp_expr h
142

    
143
and pp_handlers fmt hl =
144
 fprintf_list ~sep:" " pp_handler fmt hl
145

    
146
and pp_app fmt id e r =
147
  match r with
148
  | None ->
149
    (match id, e.expr_desc with
150
    | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
151
    | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
152
    | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
153
    | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
154
    | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
155
    | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
156
    | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
157
    | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
158
    | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
159
    | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
160
    | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
161
    | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
162
    | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
163
    | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
164
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
165
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
166
    | "not", _ -> fprintf fmt "(not %a)" pp_expr e
167
    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
168
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
169
)
170
  | Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x 
171

    
172

    
173

    
174
and pp_eexpr fmt e =
175
  fprintf fmt "%a%t %a"
176
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
177
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
178
    pp_expr e.eexpr_qfexpr
179

    
180

    
181
and pp_expr_annot fmt expr_ann =
182
  let pp_annot fmt (kwds, ee) =
183
    Format.fprintf fmt "(*! %t: %a *)"
184
      (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)
185
      pp_eexpr ee
186
  in
187
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
188
    
189
	
190
let pp_node_eq fmt eq = 
191
  fprintf fmt "%a = %a;" 
192
    pp_eq_lhs eq.eq_lhs
193
    pp_expr eq.eq_rhs
194

    
195
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq 
196

    
197

    
198
let pp_var_type_dec fmt ty =
199
  let rec pp_var_struct_type_field fmt (label, tdesc) =
200
    fprintf fmt "%a : %a" pp_var_type_dec_desc tdesc pp_print_string label
201
  and pp_var_type_dec_desc fmt tdesc =
202
  match tdesc with 
203
    | Tydec_any -> fprintf fmt "<any>"
204
    | Tydec_int -> fprintf fmt "int"
205
    | Tydec_real -> fprintf fmt "real"
206
    | Tydec_float -> fprintf fmt "float"
207
    | Tydec_bool -> fprintf fmt "bool"
208
    | Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
209
    | Tydec_const t -> fprintf fmt "%s" t
210
    | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
211
    | Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:"; " pp_var_struct_type_field) f_list
212
    | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
213
in pp_var_type_dec_desc fmt ty.ty_dec_desc
214

    
215
(* let rec pp_var_type fmt ty =  *)
216
(*   fprintf fmt "%a" (match ty.tdesc with  *)
217
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
218
(*     | Tint -> pp_print_string fmt "int" *)
219
(*     | Treal -> pp_print_string fmt "real" *)
220
(*     | Tbool -> pp_print_string fmt "bool" *)
221
(*     | Trat -> pp_print_string fmt "rat" *)
222
(*     | Tclock -> pp_print_string fmt "clock"  *)
223
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
224
(*   ) *)
225

    
226

    
227
let pp_spec fmt spec =
228
  fprintf fmt "@[<hov 2>(*@@ ";
229
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
230
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
231
  fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures, _) -> 
232
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
233
      name
234
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
235
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
236
  ) fmt spec.behaviors;
237
  fprintf fmt "@]*)";
238
  ()
239

    
240

    
241
let pp_asserts fmt asserts =
242
  match asserts with 
243
  | _::_ -> (
244
  fprintf fmt "(* Asserts definitions *)@ ";
245
  fprintf_list ~sep:"@ " (fun fmt assert_ -> 
246
    let expr = assert_.assert_expr in
247
    fprintf fmt "assert %a;" pp_expr expr 
248
  ) fmt asserts 
249
  )
250
  | _ -> ()
251
    
252
let pp_node fmt nd = 
253
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
254
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
255
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
256
  (if nd.node_dec_stateless then "function" else "node")
257
  nd.node_id
258
  pp_node_args nd.node_inputs
259
  pp_node_args nd.node_outputs
260
  (fun fmt locals ->
261
  match locals with [] -> () | _ ->
262
    fprintf fmt "@[<v 4>var %a@]@ " 
263
      (fprintf_list ~sep:"@ " 
264
	 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
265
      locals
266
  ) nd.node_locals
267
  (fun fmt checks ->
268
  match checks with [] -> () | _ ->
269
    fprintf fmt "@[<v 4>check@ %a@]@ " 
270
      (fprintf_list ~sep:"@ " 
271
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
272
      checks
273
  ) nd.node_checks
274
  (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
275
  pp_node_eqs nd.node_eqs
276
  pp_asserts nd.node_asserts
277
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
278

    
279
let pp_imported_node fmt ind = 
280
  fprintf fmt "@[<v>%s %s (%a) returns (%a) %t@]"
281
    (if ind.nodei_stateless then "function" else "node")
282
    ind.nodei_id
283
    pp_node_args ind.nodei_inputs
284
    pp_node_args ind.nodei_outputs
285
    (fun fmt -> if ind.nodei_stateless then Format.fprintf fmt "stateless") 
286

    
287
let pp_const_list fmt clist = 
288
  fprintf_list ~sep:"@ " (fun fmt cdecl ->
289
    fprintf fmt "%s = %a;"
290
      cdecl.const_id pp_const cdecl.const_value) fmt clist
291

    
292
let pp_decl fmt decl =
293
  match decl.top_decl_desc with
294
  | Node nd -> fprintf fmt "%a@ " pp_node nd
295
  | ImportedNode ind ->
296
    fprintf fmt "imported %a;@ " pp_imported_node ind
297
  | Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
298
  | Open (local, s) -> if local then fprintf fmt "open \"%s\"" s else fprintf fmt "open <%s>" s
299

    
300

    
301
let pp_prog fmt prog = 
302
  fprintf_list ~sep:"@ " pp_decl fmt prog
303

    
304
let pp_short_decl fmt decl =
305
  match decl.top_decl_desc with
306
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
307
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
308
  | Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
309
    | Open (local, s) -> if local then fprintf fmt "open \"%s\"" s else fprintf fmt "open <%s>" s
310

    
311
let pp_lusi fmt decl = 
312
  match decl.top_decl_desc with
313
  | Node nd ->  
314
    fprintf fmt 
315
      "@[<v>%s %s (%a) returns (%a);@ @]@ "
316
      (if Stateless.check_node decl then "function" else "node")
317
      nd.node_id
318
      pp_node_args nd.node_inputs
319
      pp_node_args nd.node_outputs
320
| Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
321
| ImportedNode _ | Open _ -> ()
322

    
323

    
324

    
325

    
326
let pp_lusi_header fmt filename prog =
327
  fprintf fmt "(* Generated Lustre Interface file from %s *)@." filename;
328
  fprintf fmt "(* generated by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));
329
  fprintf fmt "(* feel free to mask some of the nodes by removing them from this file. *)@.@.";
330
  List.iter (fprintf fmt "%a@." pp_lusi) prog    
331
  
332
(* Local Variables: *)
333
(* compile-command:"make -C .." *)
334
(* End: *)