Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ 01c7d5e1

History | View | Annotate | Download (10.7 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_struct_const_field fmt (label, c) =
44
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
45
and pp_const fmt c = 
46
  match c with
47
    | Const_int i -> pp_print_int fmt i
48
    | Const_real r -> pp_print_string fmt r
49
    | Const_float r -> pp_print_float fmt r
50
    | Const_tag  t -> pp_print_string fmt t
51
    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
52
    | Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
53
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
54

    
55
and 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
56

    
57
and 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
58

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

    
76
and pp_tuple fmt el =
77
 fprintf_list ~sep:"," pp_expr fmt el
78

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

    
82
and pp_handlers fmt hl =
83
 fprintf_list ~sep:" " pp_handler fmt hl
84

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

    
116
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq 
117

    
118
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
119

    
120
let pp_var_type_dec fmt ty =
121
  let rec pp_var_struct_type_field fmt (label, tdesc) =
122
    fprintf fmt "%a : %a" pp_var_type_dec_desc tdesc pp_print_string label
123
  and pp_var_type_dec_desc fmt tdesc =
124
  match tdesc with 
125
    | Tydec_any -> fprintf fmt "<any>"
126
    | Tydec_int -> fprintf fmt "int"
127
    | Tydec_real -> fprintf fmt "real"
128
    | Tydec_float -> fprintf fmt "float"
129
    | Tydec_bool -> fprintf fmt "bool"
130
    | Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
131
    | Tydec_const t -> fprintf fmt "%s" t
132
    | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
133
    | Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:"; " pp_var_struct_type_field) f_list
134
    | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
135
in pp_var_type_dec_desc fmt ty.ty_dec_desc
136

    
137
(* let rec pp_var_type fmt ty =  *)
138
(*   fprintf fmt "%a" (match ty.tdesc with  *)
139
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
140
(*     | Tint -> pp_print_string fmt "int" *)
141
(*     | Treal -> pp_print_string fmt "real" *)
142
(*     | Tbool -> pp_print_string fmt "bool" *)
143
(*     | Trat -> pp_print_string fmt "rat" *)
144
(*     | Tclock -> pp_print_string fmt "clock"  *)
145
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
146
(*   ) *)
147

    
148

    
149

    
150
let pp_quantifiers fmt (q, vars) =
151
  match q with
152
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
153
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
154

    
155
let 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
let pp_spec fmt spec =
162
  fprintf fmt "@[<hov 2>(*@@ ";
163
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
164
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
165
  fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures, _) -> 
166
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
167
      name
168
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
169
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
170
  ) fmt spec.behaviors;
171
  fprintf fmt "@]*)";
172
  ()
173

    
174
let pp_node fmt nd = 
175
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@]@ @]@.tel@]@."
176
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
177
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
178
  (if nd.node_dec_stateless then "function" else "node")
179
  nd.node_id
180
  pp_node_args nd.node_inputs
181
  pp_node_args nd.node_outputs
182
  (fun fmt locals ->
183
  match locals with [] -> () | _ ->
184
    fprintf fmt "@[<v 4>var %a@]@ " 
185
      (fprintf_list ~sep:"@ " 
186
	 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
187
      locals
188
  ) nd.node_locals
189
  (fun fmt checks ->
190
  match checks with [] -> () | _ ->
191
    fprintf fmt "@[<v 4>check@ %a@]@ " 
192
      (fprintf_list ~sep:"@ " 
193
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
194
      checks
195
  ) nd.node_checks
196
  pp_node_eqs nd.node_eqs
197
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
198

    
199
let pp_imported_node fmt ind = 
200
  fprintf fmt "@[<v>%s %s (%a) returns (%a) %t@]"
201
    (if ind.nodei_stateless then "function" else "node")
202
    ind.nodei_id
203
    pp_node_args ind.nodei_inputs
204
    pp_node_args ind.nodei_outputs
205
    (fun fmt -> if ind.nodei_stateless then Format.fprintf fmt "stateless") 
206

    
207
let pp_const_list fmt clist = 
208
  fprintf_list ~sep:"@ " (fun fmt cdecl ->
209
    fprintf fmt "%s = %a;"
210
      cdecl.const_id pp_const cdecl.const_value) fmt clist
211

    
212
let pp_decl fmt decl =
213
  match decl.top_decl_desc with
214
  | Node nd -> fprintf fmt "%a@ " pp_node nd
215
  | ImportedNode ind ->
216
    fprintf fmt "imported %a;@ " pp_imported_node ind
217
  | Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
218
  | Open (local, s) -> if local then fprintf fmt "open \"%s\"" s else fprintf fmt "open <%s>" s
219

    
220

    
221
let pp_prog fmt prog = 
222
  fprintf_list ~sep:"@ " pp_decl fmt prog
223

    
224
let pp_short_decl fmt decl =
225
  match decl.top_decl_desc with
226
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
227
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
228
  | Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
229
    | Open (local, s) -> if local then fprintf fmt "open \"%s\"" s else fprintf fmt "open <%s>" s
230

    
231
let pp_lusi fmt decl = 
232
  match decl.top_decl_desc with
233
  | Node nd ->  
234
    fprintf fmt 
235
      "@[<v>%s %s (%a) returns (%a);@ @]@ "
236
      (if Stateless.check_node decl then "function" else "node")
237
      nd.node_id
238
      pp_node_args nd.node_inputs
239
      pp_node_args nd.node_outputs
240
| Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
241
| ImportedNode _ | Open _ -> ()
242

    
243

    
244

    
245

    
246
let pp_lusi_header fmt filename prog =
247
  fprintf fmt "(* Generated Lustre Interface file from %s *)@." filename;
248
  fprintf fmt "(* generated by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));
249
  fprintf fmt "(* feel free to mask some of the nodes by removing them from this file. *)@.@.";
250
  List.iter (fprintf fmt "%a@." pp_lusi) prog    
251
  
252
(* Local Variables: *)
253
(* compile-command:"make -C .." *)
254
(* End: *)