Project

General

Profile

Revision 86ae18b7 src/printers.ml

View differences:

src/printers.ml
52 52

  
53 53
let pp_quantifiers fmt (q, vars) =
54 54
  match q with
55
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
56
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
55
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars
56
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars
57 57

  
58 58
let rec pp_struct_const_field fmt (label, c) =
59 59
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
60
and pp_const fmt c = 
60
and pp_const fmt c =
61 61
  match c with
62 62
    | Const_int i -> pp_print_int fmt i
63 63
    | 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 *)
......
69 69

  
70 70

  
71 71
let rec pp_expr fmt expr =
72
  (match expr.expr_annot with 
73
  | None -> fprintf fmt "%t" 
72
  (match expr.expr_annot with
73
  | None -> fprintf fmt "%t"
74 74
  | Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann)
75
    (fun fmt -> 
75
    (fun fmt ->
76 76
      match expr.expr_desc with
77 77
    | Expr_const c -> pp_const fmt c
78 78
    | Expr_ident id -> Format.fprintf fmt "%s" id
......
85 85
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
86 86
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
87 87
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
88
    | Expr_merge (id, hl) -> 
88
    | Expr_merge (id, hl) ->
89 89
      fprintf fmt "merge %s %a" id pp_handlers hl
90 90
    | Expr_appl (id, e, r) -> pp_app fmt id e r
91 91
    )
......
101 101
and pp_app fmt id e r =
102 102
  match r with
103 103
  | None -> pp_call fmt id e
104
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
104
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
105 105

  
106 106
and pp_call fmt id e =
107 107
  match id, e.expr_desc with
......
131 131
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
132 132
    pp_expr e.eexpr_qfexpr
133 133

  
134
and  pp_sf_value fmt e =
135
   fprintf fmt "%a"
136
     (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
137
     (* (fun fmt -> match e.eexpr_quantifiers *)
138
     (*             with [] -> () *)
139
     (*                | _ -> fprintf fmt ";") *)
140
     pp_expr e.eexpr_qfexpr
141

  
142
and pp_s_function fmt expr_ann =
143
  let pp_annot fmt (kwds, ee) =
144
    Format.fprintf fmt " %t : %a"
145
                   (fun fmt -> match kwds with
146
                               | [] -> assert false
147
                               | [x] -> Format.pp_print_string fmt x
148
                               | _ -> Format.fprintf fmt "%a" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
149
                   pp_sf_value ee
150
  in
151
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
134 152

  
135 153
and pp_expr_annot fmt expr_ann =
136 154
  let pp_annot fmt (kwds, ee) =
......
139 157
      pp_eexpr ee
140 158
  in
141 159
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
142
    
160

  
143 161
(*
144 162
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
145 163
*)
......
147 165
  begin
148 166
    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;
149 167
    match id.var_dec_value with
150
    | None -> () 
168
    | None -> ()
151 169
    | Some v -> fprintf fmt " = %a" pp_expr v
152
  end 
170
  end
153 171

  
154
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
172
let pp_node_args = fprintf_list ~sep:"; " pp_node_var
155 173

  
156
let pp_node_eq fmt eq = 
157
  fprintf fmt "%a = %a;" 
174
let pp_node_eq fmt eq =
175
  fprintf fmt "%a = %a;"
158 176
    pp_eq_lhs eq.eq_lhs
159 177
    pp_expr eq.eq_rhs
160 178

  
......
179 197
    (Utils.fprintf_list ~sep:"@," pp_unless) handler.hand_unless
180 198
    (fun fmt locals ->
181 199
      match locals with [] -> () | _ ->
182
	Format.fprintf fmt "@[<v 4>var %a@]@ " 
183
	  (Utils.fprintf_list ~sep:"@ " 
200
	Format.fprintf fmt "@[<v 4>var %a@]@ "
201
	  (Utils.fprintf_list ~sep:"@ "
184 202
	     (fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v))
185 203
	  locals)
186 204
    handler.hand_locals
......
204 222
let rec pp_var_struct_type_field fmt (label, tdesc) =
205 223
  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
206 224
and pp_var_type_dec_desc fmt tdesc =
207
  match tdesc with 
225
  match tdesc with
208 226
  | Tydec_any -> fprintf fmt "<any>"
209 227
  | Tydec_int -> fprintf fmt "int"
210 228
  | Tydec_real -> fprintf fmt "real"
......
241 259
  fprintf fmt "@[<hov 2>(*@@ ";
242 260
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
243 261
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
244
  fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures, _) -> 
245
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
262
  fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures, _) ->
263
    fprintf fmt "behavior %s:@[@ %a@ %a@]"
246 264
      name
247 265
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
248 266
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
......
252 270

  
253 271

  
254 272
let pp_asserts fmt asserts =
255
  match asserts with 
273
  match asserts with
256 274
  | _::_ -> (
257 275
  fprintf fmt "(* Asserts definitions *)@ ";
258
  fprintf_list ~sep:"@ " (fun fmt assert_ -> 
276
  fprintf_list ~sep:"@ " (fun fmt assert_ ->
259 277
    let expr = assert_.assert_expr in
260
    fprintf fmt "assert %a;" pp_expr expr 
261
  ) fmt asserts 
278
    fprintf fmt "assert %a;" pp_expr expr
279
  ) fmt asserts
262 280
  )
263 281
  | _ -> ()
264
    
265
let pp_node fmt nd = 
282

  
283
let pp_node fmt nd =
266 284
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
267 285
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
268 286
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
......
272 290
  pp_node_args nd.node_outputs
273 291
  (fun fmt locals ->
274 292
  match locals with [] -> () | _ ->
275
    fprintf fmt "@[<v 4>var %a@]@ " 
276
      (fprintf_list ~sep:"@ " 
293
    fprintf fmt "@[<v 4>var %a@]@ "
294
      (fprintf_list ~sep:"@ "
277 295
	 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
278 296
      locals
279 297
  ) nd.node_locals
280 298
  (fun fmt checks ->
281 299
  match checks with [] -> () | _ ->
282
    fprintf fmt "@[<v 4>check@ %a@]@ " 
283
      (fprintf_list ~sep:"@ " 
300
    fprintf fmt "@[<v 4>check@ %a@]@ "
301
      (fprintf_list ~sep:"@ "
284 302
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
285 303
      checks
286 304
  ) nd.node_checks
......
289 307
  pp_asserts nd.node_asserts
290 308
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
291 309

  
292
let pp_imported_node fmt ind = 
310
let pp_imported_node fmt ind =
293 311
  fprintf fmt "@[<v>%s %s (%a) returns (%a)@]"
294 312
    (if ind.nodei_stateless then "function" else "node")
295 313
    ind.nodei_id
......
299 317
let pp_const_decl fmt cdecl =
300 318
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
301 319

  
302
let pp_const_decl_list fmt clist = 
320
let pp_const_decl_list fmt clist =
303 321
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
304 322

  
305 323
let pp_decl fmt decl =
......
311 329
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
312 330
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
313 331

  
314
let pp_prog fmt prog = 
332
let pp_prog fmt prog =
315 333
  fprintf_list ~sep:"@ " pp_decl fmt prog
316 334

  
317 335
let pp_short_decl fmt decl =
......
322 340
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
323 341
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
324 342

  
325
let pp_lusi fmt decl = 
343
let pp_lusi fmt decl =
326 344
  match decl.top_decl_desc with
327 345
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
328 346
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
......
334 352
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@." basename;
335 353
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));
336 354
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@.@.";
337
  List.iter (fprintf fmt "%a@." pp_lusi) prog    
355
  List.iter (fprintf fmt "%a@." pp_lusi) prog
338 356

  
339 357
let pp_offset fmt offset =
340 358
  match offset with

Also available in: Unified diff