Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / printers.ml @ 70df2f87

History | View | Annotate | Download (11.3 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 22fe1c93 ploc
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 (out, flush, newline, spaces) = pp_get_all_formatter_output_functions fmt () in
20
  let macro_newline () = (out "\\" 0 1; newline ()) in
21
  begin
22
    pp_set_all_formatter_output_functions fmt out flush macro_newline spaces;
23
    pp_fun fmt v;
24
    pp_set_all_formatter_output_functions fmt out flush newline spaces;
25
  end
26
27
28
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
29
30
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
31
32 af5af1e8 ploc
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
33
34
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
35
36
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
37
38
let pp_quantifiers fmt (q, vars) =
39
  match q with
40
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
41
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
42
43 12af4908 xthirioux
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 22fe1c93 ploc
  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 12af4908 xthirioux
    | Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
53 01c7d5e1 ploc
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
54 22fe1c93 ploc
55
56 af5af1e8 ploc
let rec pp_expr fmt expr =
57
  (match expr.expr_annot with 
58
  | None -> fprintf fmt "%t" 
59
  | Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann)
60
    (fun fmt -> 
61
      match expr.expr_desc with
62 22fe1c93 ploc
    | Expr_const c -> pp_const fmt c
63
    | Expr_ident id -> Format.fprintf fmt "%s" id
64
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
65
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
66
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
67
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
68
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
69 e2380d4d ploc
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
70 22fe1c93 ploc
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
71
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
72
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
73
    | Expr_merge (id, hl) -> 
74
      fprintf fmt "merge %s %a" id pp_handlers hl
75
    | Expr_appl (id, e, r) -> pp_app fmt id e r
76 af5af1e8 ploc
    )
77 22fe1c93 ploc
and pp_tuple fmt el =
78
 fprintf_list ~sep:"," pp_expr fmt el
79
80
and pp_handler fmt (t, h) =
81
 fprintf fmt "(%s -> %a)" t pp_expr h
82
83
and pp_handlers fmt hl =
84
 fprintf_list ~sep:" " pp_handler fmt hl
85
86
and pp_app fmt id e r =
87
  match r with
88 70df2f87 xthirioux
  | None -> pp_call fmt id e
89
  | Some (x, l) -> fprintf fmt "%t every %s(%s)" (fun fmt -> pp_call fmt id e) l x 
90
91
and pp_call fmt id e =
92
  match id, e.expr_desc with
93
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
94
  | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
95
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
96
  | "*", 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
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
99
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
100
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
101
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
102
  | "impl", 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
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
106
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
107
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
108
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
109
  | "not", _ -> fprintf fmt "(not %a)" pp_expr e
110
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
111
  | _ -> fprintf fmt "%s (%a)" id pp_expr e
112 af5af1e8 ploc
113
and pp_eexpr fmt e =
114
  fprintf fmt "%a%t %a"
115
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
116
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
117
    pp_expr e.eexpr_qfexpr
118
119
120
and pp_expr_annot fmt expr_ann =
121
  let pp_annot fmt (kwds, ee) =
122
    Format.fprintf fmt "(*! %t: %a *)"
123
      (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)
124
      pp_eexpr ee
125
  in
126
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
127
    
128 22fe1c93 ploc
	
129
let pp_node_eq fmt eq = 
130
  fprintf fmt "%a = %a;" 
131
    pp_eq_lhs eq.eq_lhs
132
    pp_expr eq.eq_rhs
133
134 b1655a21 xthirioux
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq
135 22fe1c93 ploc
136 b1655a21 xthirioux
let rec pp_var_struct_type_field fmt (label, tdesc) =
137
  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
138
and pp_var_type_dec_desc fmt tdesc =
139
  match tdesc with 
140
  | Tydec_any -> fprintf fmt "<any>"
141
  | Tydec_int -> fprintf fmt "int"
142
  | Tydec_real -> fprintf fmt "real"
143
  | Tydec_float -> fprintf fmt "float"
144
  | Tydec_bool -> fprintf fmt "bool"
145
  | Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
146
  | Tydec_const t -> fprintf fmt "%s" t
147
  | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
148
  | Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:" " pp_var_struct_type_field) f_list
149
  | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
150 22fe1c93 ploc
151
let pp_var_type_dec fmt ty =
152 b1655a21 xthirioux
  pp_var_type_dec_desc fmt ty.ty_dec_desc
153
154 ef34b4ae xthirioux
let pp_typedef fmt ty =
155
  fprintf fmt "type %s = %a;@ " ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
156
157
let pp_typedec fmt ty =
158
  fprintf fmt "type %s;@ " ty.tydec_id
159 22fe1c93 ploc
160
(* let rec pp_var_type fmt ty =  *)
161
(*   fprintf fmt "%a" (match ty.tdesc with  *)
162
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
163
(*     | Tint -> pp_print_string fmt "int" *)
164
(*     | Treal -> pp_print_string fmt "real" *)
165
(*     | Tbool -> pp_print_string fmt "bool" *)
166
(*     | Trat -> pp_print_string fmt "rat" *)
167
(*     | Tclock -> pp_print_string fmt "clock"  *)
168
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
169
(*   ) *)
170
171 e2380d4d ploc
172
let pp_spec fmt spec =
173
  fprintf fmt "@[<hov 2>(*@@ ";
174 01c7d5e1 ploc
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
175
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
176
  fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures, _) -> 
177 e2380d4d ploc
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
178
      name
179
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
180 01c7d5e1 ploc
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
181 e2380d4d ploc
  ) fmt spec.behaviors;
182
  fprintf fmt "@]*)";
183
  ()
184
185 af5af1e8 ploc
186
let pp_asserts fmt asserts =
187
  match asserts with 
188
  | _::_ -> (
189
  fprintf fmt "(* Asserts definitions *)@ ";
190
  fprintf_list ~sep:"@ " (fun fmt assert_ -> 
191
    let expr = assert_.assert_expr in
192
    fprintf fmt "assert %a;" pp_expr expr 
193
  ) fmt asserts 
194
  )
195
  | _ -> ()
196
    
197 22fe1c93 ploc
let pp_node fmt nd = 
198 af5af1e8 ploc
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
199 e2380d4d ploc
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
200 52cfee34 xthirioux
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
201
  (if nd.node_dec_stateless then "function" else "node")
202 22fe1c93 ploc
  nd.node_id
203
  pp_node_args nd.node_inputs
204
  pp_node_args nd.node_outputs
205
  (fun fmt locals ->
206
  match locals with [] -> () | _ ->
207
    fprintf fmt "@[<v 4>var %a@]@ " 
208
      (fprintf_list ~sep:"@ " 
209 7291cb80 xthirioux
	 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
210 22fe1c93 ploc
      locals
211
  ) nd.node_locals
212
  (fun fmt checks ->
213
  match checks with [] -> () | _ ->
214
    fprintf fmt "@[<v 4>check@ %a@]@ " 
215
      (fprintf_list ~sep:"@ " 
216
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
217
      checks
218
  ) nd.node_checks
219 af5af1e8 ploc
  (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
220 22fe1c93 ploc
  pp_node_eqs nd.node_eqs
221 af5af1e8 ploc
  pp_asserts nd.node_asserts
222 22fe1c93 ploc
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
223
224
let pp_imported_node fmt ind = 
225 ef34b4ae xthirioux
  fprintf fmt "@[<v>%s %s (%a) returns (%a)@]"
226 52cfee34 xthirioux
    (if ind.nodei_stateless then "function" else "node")
227 22fe1c93 ploc
    ind.nodei_id
228
    pp_node_args ind.nodei_inputs
229
    pp_node_args ind.nodei_outputs
230
231 ef34b4ae xthirioux
let pp_const_decl fmt cdecl =
232
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
233
234
let pp_const_decl_list fmt clist = 
235
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
236 54ae8ac7 ploc
237 22fe1c93 ploc
let pp_decl fmt decl =
238
  match decl.top_decl_desc with
239
  | Node nd -> fprintf fmt "%a@ " pp_node nd
240
  | ImportedNode ind ->
241
    fprintf fmt "imported %a;@ " pp_imported_node ind
242 ef34b4ae xthirioux
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
243
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
244
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
245 22fe1c93 ploc
246
let pp_prog fmt prog = 
247
  fprintf_list ~sep:"@ " pp_decl fmt prog
248
249
let pp_short_decl fmt decl =
250
  match decl.top_decl_desc with
251
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
252
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
253 ef34b4ae xthirioux
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
254
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
255
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
256 22fe1c93 ploc
257 5c1184ad ploc
let pp_lusi fmt decl = 
258
  match decl.top_decl_desc with
259 ef34b4ae xthirioux
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
260
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
261
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
262
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
263
  | Node _ -> assert false
264
265
let pp_lusi_header fmt basename prog =
266
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@." basename;
267 b1655a21 xthirioux
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));
268
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@.@.";
269 5c1184ad ploc
  List.iter (fprintf fmt "%a@." pp_lusi) prog    
270
  
271 22fe1c93 ploc
(* Local Variables: *)
272
(* compile-command:"make -C .." *)
273
(* End: *)