Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ 22fe1c93

History | View | Annotate | Download (12.4 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- *)
22
open Corelang
23
open LustreSpec
24
open Format
25
open Utils
26

    
27
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
28
   following the C convention for multiple lines macro *)
29
let pp_as_c_macro pp_fun fmt v =
30
  let (out, flush, newline, spaces) = pp_get_all_formatter_output_functions fmt () in
31
  let macro_newline () = (out "\\" 0 1; newline ()) in
32
  begin
33
    pp_set_all_formatter_output_functions fmt out flush macro_newline spaces;
34
    pp_fun fmt v;
35
    pp_set_all_formatter_output_functions fmt out flush newline spaces;
36
  end
37

    
38

    
39
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
40

    
41
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
42

    
43
let rec pp_const fmt c = 
44
  match c with
45
    | Const_int i -> pp_print_int fmt i
46
    | Const_real r -> pp_print_string fmt r
47
    | Const_float r -> pp_print_float fmt r
48
    | Const_tag  t -> pp_print_string fmt t
49
    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
50

    
51
and pp_var fmt id = fprintf fmt "%s: %a" id.var_id Types.print_ty id.var_type
52

    
53
and pp_expr fmt expr =
54
  match expr.expr_desc with
55
    | Expr_const c -> pp_const fmt c
56
    | Expr_ident id -> Format.fprintf fmt "%s" id
57
(*    | Expr_cst_array (c, e) -> fprintf fmt "%a^%a" pp_expr e pp_const c *)
58
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
59
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
60
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
61
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
62
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
63
    | Expr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_expr e1 pp_expr e2
64
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
65
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
66
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
67
    | Expr_merge (id, hl) -> 
68
      fprintf fmt "merge %s %a" id pp_handlers hl
69
    | Expr_appl (id, e, r) -> pp_app fmt id e r
70
    | Expr_uclock _
71
    | Expr_dclock _
72
    | Expr_phclock _ -> assert false
73

    
74
and pp_tuple fmt el =
75
 fprintf_list ~sep:"," pp_expr fmt el
76

    
77
and pp_handler fmt (t, h) =
78
 fprintf fmt "(%s -> %a)" t pp_expr h
79

    
80
and pp_handlers fmt hl =
81
 fprintf_list ~sep:" " pp_handler fmt hl
82

    
83
and pp_app fmt id e r =
84
  match r with
85
  | None ->
86
    (match id, e.expr_desc with
87
    | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
88
    | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
89
    | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
90
    | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
91
    | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
92
    | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
93
    | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
94
    | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
95
    | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
96
    | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
97
    | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
98
    | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
99
    | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
100
    | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
101
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
102
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
103
    | "not", _ -> fprintf fmt "(not %a)" pp_expr e
104
    | _ -> fprintf fmt "%s (%a)" id pp_expr e)
105
  | Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x 
106
	
107
let pp_node_eq fmt eq = 
108
  fprintf fmt "%a = %a;" 
109
    pp_eq_lhs eq.eq_lhs
110
    pp_expr eq.eq_rhs
111

    
112
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq 
113

    
114
let pp_node_args = fprintf_list ~sep:"; " pp_var 
115

    
116
let pp_var_type_dec fmt ty =
117
  let rec pp_var_type_dec_desc fmt tdesc =
118
  match tdesc with 
119
    | Tydec_any -> fprintf fmt "<any>"
120
    | Tydec_int -> fprintf fmt "int"
121
    | Tydec_real -> fprintf fmt "real"
122
    | Tydec_float -> fprintf fmt "float"
123
    | Tydec_bool -> fprintf fmt "bool"
124
    | Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
125
    | Tydec_const t -> fprintf fmt "%s" t
126
    | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
127
    | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
128
in pp_var_type_dec_desc fmt ty.ty_dec_desc
129

    
130
(* let rec pp_var_type fmt ty =  *)
131
(*   fprintf fmt "%a" (match ty.tdesc with  *)
132
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
133
(*     | Tint -> pp_print_string fmt "int" *)
134
(*     | Treal -> pp_print_string fmt "real" *)
135
(*     | Tbool -> pp_print_string fmt "bool" *)
136
(*     | Trat -> pp_print_string fmt "rat" *)
137
(*     | Tclock -> pp_print_string fmt "clock"  *)
138
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
139
(*   ) *)
140

    
141
let pp_node fmt nd = 
142
fprintf fmt "@[<v>node %s (%a) returns (%a)@ %a%alet@ @[<h 2>   @ @[%a@]@ @]@ tel@]@ "
143
  nd.node_id
144
  pp_node_args nd.node_inputs
145
  pp_node_args nd.node_outputs
146
  (fun fmt locals ->
147
  match locals with [] -> () | _ ->
148
    fprintf fmt "@[<v 4>var %a@]@ " 
149
      (fprintf_list ~sep:"@ " 
150
	 (fun fmt v -> fprintf fmt "%a;" pp_var v))
151
      locals
152
  ) nd.node_locals
153
  (fun fmt checks ->
154
  match checks with [] -> () | _ ->
155
    fprintf fmt "@[<v 4>check@ %a@]@ " 
156
      (fprintf_list ~sep:"@ " 
157
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
158
      checks
159
  ) nd.node_checks
160
  pp_node_eqs nd.node_eqs
161
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
162

    
163
let pp_imported_node fmt ind = 
164
  fprintf fmt "@[<v>node %s (%a) returns (%a) %t@]"
165
    ind.nodei_id
166
    pp_node_args ind.nodei_inputs
167
    pp_node_args ind.nodei_outputs
168
    (fun fmt -> if ind.nodei_stateless then Format.fprintf fmt "stateless") 
169

    
170
let pp_imported_fun fmt ind = 
171
  fprintf fmt "@[<v>function %s (%a) returns (%a)@]"
172
    ind.fun_id
173
    pp_node_args ind.fun_inputs
174
    pp_node_args ind.fun_outputs
175

    
176
let pp_decl fmt decl =
177
  match decl.top_decl_desc with
178
  | Node nd -> fprintf fmt "%a@ " pp_node nd
179
  | ImportedNode ind ->
180
    fprintf fmt "imported %a;@ " pp_imported_node ind
181
  | ImportedFun ind ->
182
    fprintf fmt "%a;@ " pp_imported_fun ind
183
  | Consts clist -> (
184
    fprintf fmt "const %a@ " 
185
      (fprintf_list ~sep:"@ " (fun fmt cdecl ->
186
	fprintf fmt "%s = %a;"
187
	  cdecl.const_id pp_const cdecl.const_value)) clist)
188
  | Include s -> fprintf fmt "include %s" s
189

    
190

    
191
let pp_prog fmt prog = 
192
  fprintf_list ~sep:"@ " pp_decl fmt prog
193

    
194
let pp_short_decl fmt decl =
195
  match decl.top_decl_desc with
196
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
197
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
198
  | ImportedFun ind -> fprintf fmt "function %s" ind.fun_id
199
  | Consts clist -> (
200
    fprintf fmt "const %a@ " 
201
      (fprintf_list ~sep:"@ " (fun fmt cdecl ->
202
	pp_print_string fmt cdecl.const_id)) clist)
203
  | Include s -> fprintf fmt "include %s" s
204

    
205

    
206

    
207
let pp_econst fmt c = 
208
  match c with
209
    | EConst_int i -> pp_print_int fmt i
210
    | EConst_real r -> pp_print_string fmt r
211
    | EConst_float r -> pp_print_float fmt r
212
    | EConst_bool b -> pp_print_bool fmt b
213
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
214

    
215
let rec pp_eexpr is_output fmt eexpr = 
216
  let pp_eexpr = pp_eexpr is_output in
217
  match eexpr.eexpr_desc with
218
    | EExpr_const c -> pp_econst fmt c
219
    | EExpr_ident id -> 
220
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
221
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
222
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
223
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
224
    | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2
225
    | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e
226
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
227
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
228
    | EExpr_merge (id, e1, e2) -> 
229
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
230
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
231
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
232
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
233

    
234

    
235
    | EExpr_whennot _
236
    | EExpr_uclock _
237
    | EExpr_dclock _
238
    | EExpr_phclock _ -> assert false
239
and pp_eapp is_output fmt id e r =
240
  let pp_eexpr = pp_eexpr is_output in
241
  match r with
242
  | None ->
243
    (match id, e.eexpr_desc with
244
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
245
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
246
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
247
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
248
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
249
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
250
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
251
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
252
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
253
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
254
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
255
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
256
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
257
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
258
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
259
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
260
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
261
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
262
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
263
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
264

    
265
  
266
let pp_ensures is_output fmt e =
267
  let pp_eexpr = pp_eexpr is_output in
268
  match e with
269
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e
270
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args
271
 
272
let pp_acsl_spec outputs fmt spec =
273
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
274
  let pp_eexpr = pp_eexpr is_output in
275
  fprintf fmt "@[<v 2>/*@@ ";
276
  fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
277
  fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
278
  fprintf fmt "@ ";
279
  (* fprintf fmt "assigns *self%t%a;@ "  *)
280
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
281
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
282
  fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
283
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
284
      name
285
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
286
      (fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
287
  ) fmt spec.behaviors;
288
  fprintf fmt "@]@ */@.";
289
  ()
290
(* Local Variables: *)
291
(* compile-command:"make -C .." *)
292
(* End: *)