Project

General

Profile

Revision bc3139b0

View differences:

src/printers.ml
317 317
  ()
318 318

  
319 319
    
320
let pp_node fmt nd = 
321
fprintf fmt "@[<v 0>%a%t%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ %a%alet@[<h 2>   @ @[<v>%a@ %a@ %a@]@]@ tel@]@ "
322
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
323
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ")
324
  (if nd.node_dec_stateless then "function" else "node")
325
  nd.node_id
326
  pp_node_args nd.node_inputs
327
  pp_node_args nd.node_outputs
328
  (fun fmt locals ->
329
  match locals with [] -> () | _ ->
330
    fprintf fmt "@[<v 4>var %a@]@ " 
331
      (fprintf_list ~sep:"@ " 
332
	 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
333
      locals
334
  ) nd.node_locals
335
  (fun fmt checks ->
336
  match checks with [] -> () | _ ->
337
    fprintf fmt "@[<v 4>check@ %a@]@ " 
338
      (fprintf_list ~sep:"@ " 
339
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
340
      checks
341
  ) nd.node_checks
342
  (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
343
  pp_node_stmts nd.node_stmts
344
  pp_asserts nd.node_asserts
320
let pp_node fmt nd =
321
  fprintf fmt "@[<v 0>";
322
  (* Prototype *)
323
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
324
    (if nd.node_dec_stateless then "function" else "node")
325
    nd.node_id
326
    pp_node_args nd.node_inputs
327
    pp_node_args nd.node_outputs;
328
  (* Contracts *)
329
  fprintf fmt "%a%t"
330
    (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
331
    (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ");
332
  (* Locals *)
333
  fprintf fmt "%a" (fun fmt locals ->
334
      match locals with [] -> () | _ ->
335
                                    fprintf fmt "@[<v 4>var %a@]@ " 
336
                                      (fprintf_list ~sep:"@ " 
337
	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
338
                                      locals
339
    ) nd.node_locals;
340
  (* Checks *)
341
  fprintf fmt "%a"
342
    (fun fmt checks ->
343
      match checks with [] -> () | _ ->
344
                                    fprintf fmt "@[<v 4>check@ %a@]@ " 
345
                                      (fprintf_list ~sep:"@ " 
346
	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
347
                                      checks
348
    ) nd.node_checks;
349
  (* Body *)
350
  fprintf fmt "let@[<h 2>   @ @[<v>";
351
  (* Annotations *)
352
  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
353
  (* Statements *)
354
  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;
355
  (* Asserts *)    
356
  fprintf fmt "%a" pp_asserts nd.node_asserts;
357
  (* closing boxes body (2)  and node (1) *) 
358
  fprintf fmt "@]@]@ tel@]@ "
359

  
360

  
345 361
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
346 362

  
347 363
let pp_imported_node fmt ind = 

Also available in: Unified diff