Revision 27e5a70d src/printers.ml
| src/printers.ml | ||
|---|---|---|
| 158 | 158 |
pp_eexpr ee |
| 159 | 159 |
in |
| 160 | 160 |
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots |
| 161 |
|
|
| 161 |
|
|
| 162 |
|
|
| 163 |
let pp_asserts fmt asserts = |
|
| 164 |
match asserts with |
|
| 165 |
| _::_ -> ( |
|
| 166 |
fprintf fmt "(* Asserts definitions *)@ "; |
|
| 167 |
fprintf_list ~sep:"@ " (fun fmt assert_ -> |
|
| 168 |
let expr = assert_.assert_expr in |
|
| 169 |
fprintf fmt "assert %a;" pp_expr expr |
|
| 170 |
) fmt asserts |
|
| 171 |
) |
|
| 172 |
| _ -> () |
|
| 173 |
|
|
| 162 | 174 |
(* |
| 163 | 175 |
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 |
| 164 | 176 |
*) |
| ... | ... | |
| 170 | 182 |
| Some v -> fprintf fmt " = %a" pp_expr v |
| 171 | 183 |
end |
| 172 | 184 |
|
| 173 |
let pp_node_args = fprintf_list ~sep:"; " pp_node_var |
|
| 185 |
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var
|
|
| 174 | 186 |
|
| 175 | 187 |
let pp_node_eq fmt eq = |
| 176 | 188 |
fprintf fmt "%a = %a;" |
| ... | ... | |
| 181 | 193 |
Format.fprintf fmt "%s" (if restart then "restart" else "resume") |
| 182 | 194 |
|
| 183 | 195 |
let pp_unless fmt (_, expr, restart, st) = |
| 184 |
Format.fprintf fmt "unless %a %a %s@ "
|
|
| 196 |
Format.fprintf fmt "unless %a %a %s" |
|
| 185 | 197 |
pp_expr expr |
| 186 | 198 |
pp_restart restart |
| 187 | 199 |
st |
| 188 | 200 |
|
| 189 | 201 |
let pp_until fmt (_, expr, restart, st) = |
| 190 |
Format.fprintf fmt "until %a %a %s@ "
|
|
| 202 |
Format.fprintf fmt "until %a %a %s" |
|
| 191 | 203 |
pp_expr expr |
| 192 | 204 |
pp_restart restart |
| 193 | 205 |
st |
| 194 | 206 |
|
| 195 | 207 |
let rec pp_handler fmt handler = |
| 196 |
Format.fprintf fmt "state %s ->@ @[<v 2> %a%alet@,@[<v 2> %a@]@,tel%a@]"
|
|
| 208 |
Format.fprintf fmt "state %s:@ @[<v 2> %a%t%alet@,@[<v 2> %a@ %a@ %a@]@,tel@ %a@]"
|
|
| 197 | 209 |
handler.hand_state |
| 198 |
(Utils.fprintf_list ~sep:"@," pp_unless) handler.hand_unless |
|
| 210 |
(Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless |
|
| 211 |
(fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ") |
|
| 199 | 212 |
(fun fmt locals -> |
| 200 | 213 |
match locals with [] -> () | _ -> |
| 201 | 214 |
Format.fprintf fmt "@[<v 4>var %a@]@ " |
| ... | ... | |
| 203 | 216 |
(fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v)) |
| 204 | 217 |
locals) |
| 205 | 218 |
handler.hand_locals |
| 219 |
(fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots |
|
| 206 | 220 |
pp_node_stmts handler.hand_stmts |
| 221 |
pp_asserts handler.hand_asserts |
|
| 207 | 222 |
(Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until |
| 208 | 223 |
|
| 209 | 224 |
and pp_node_stmt fmt stmt = |
| ... | ... | |
| 269 | 284 |
fprintf fmt "@]*)"; |
| 270 | 285 |
() |
| 271 | 286 |
|
| 272 |
|
|
| 273 |
let pp_asserts fmt asserts = |
|
| 274 |
match asserts with |
|
| 275 |
| _::_ -> ( |
|
| 276 |
fprintf fmt "(* Asserts definitions *)@ "; |
|
| 277 |
fprintf_list ~sep:"@ " (fun fmt assert_ -> |
|
| 278 |
let expr = assert_.assert_expr in |
|
| 279 |
fprintf fmt "assert %a;" pp_expr expr |
|
| 280 |
) fmt asserts |
|
| 281 |
) |
|
| 282 |
| _ -> () |
|
| 283 | 287 |
|
| 284 | 288 |
let pp_node fmt nd = |
| 285 |
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@ %a%alet@[<h 2> @ @[<v>%a@ %a@ %a@]@]@ tel@]@ "
|
|
| 289 |
fprintf fmt "@[<v 0>%a%t%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ %a%alet@[<h 2> @ @[<v>%a@ %a@ %a@]@]@ tel@]@ "
|
|
| 286 | 290 |
(fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec |
| 287 | 291 |
(fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@ ") |
| 288 | 292 |
(if nd.node_dec_stateless then "function" else "node") |
Also available in: Unified diff