Revision a0c92fa8
Added by Pierre-Loïc Garoche over 2 years ago
| src/tools/seal/seal_utils.ml | ||
|---|---|---|
| 28 | 28 |
(fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl |
| 29 | 29 |
|
| 30 | 30 |
let pp_guard_expr pp_elem fmt (gl,e) = |
| 31 |
Format.fprintf fmt "@[%a@] -> @[<hov 2>%a@]"
|
|
| 31 |
Format.fprintf fmt "@[<v 2>@[%a@] ->@ @[<hov 2>%a@]@]"
|
|
| 32 | 32 |
(pp_guard_list pp_elem) gl |
| 33 | 33 |
pp_elem e |
| 34 | 34 |
|
| 35 | 35 |
let pp_mdefs pp_elem fmt gel = fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel |
| 36 | 36 |
|
| 37 |
|
|
| 37 |
let pp_assign_map pp_elem = |
|
| 38 |
fprintf_list ~sep:"@ " |
|
| 39 |
(fun fmt (m, mdefs) -> |
|
| 40 |
Format.fprintf fmt |
|
| 41 |
"%s -> @[<v 0>[%a@] ]@ " |
|
| 42 |
m |
|
| 43 |
(pp_mdefs pp_elem) mdefs |
|
| 44 |
) |
|
| 38 | 45 |
|
| 39 | 46 |
let deelem e = match e with |
| 40 | 47 |
Expr e -> e |
| ... | ... | |
| 53 | 60 |
fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e) |
| 54 | 61 |
|
| 55 | 62 |
let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) |
| 56 |
let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up |
|
| 57 | 63 |
|
| 58 |
let pp_sys fmt sw = List.iter (fun (gl,up) -> |
|
| 59 |
match gl with |
|
| 60 |
| None -> |
|
| 61 |
pp_up fmt up |
|
| 62 |
| Some gl -> |
|
| 63 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
|
| 64 |
Printers.pp_expr gl pp_up up) sw |
|
| 64 |
let pp_up pp_elem fmt up = |
|
| 65 |
fprintf_list ~sep:"@ " |
|
| 66 |
(fun fmt (id,e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e) |
|
| 67 |
fmt |
|
| 68 |
up |
|
| 69 |
|
|
| 70 |
let pp_sys pp_elem fmt sw = |
|
| 71 |
fprintf_list ~sep:"@ " |
|
| 72 |
(fun fmt (gl,up) -> |
|
| 73 |
match gl with |
|
| 74 |
| None -> |
|
| 75 |
(pp_up pp_elem) fmt up |
|
| 76 |
| Some gl -> |
|
| 77 |
Format.fprintf fmt "@[<v 2>[@[%a@]]:@ %a@]" |
|
| 78 |
Printers.pp_expr gl (pp_up pp_elem) up) |
|
| 79 |
fmt |
|
| 80 |
sw |
|
| 81 |
|
|
| 65 | 82 |
let pp_all_defs = |
| 66 | 83 |
(Utils.fprintf_list ~sep:",@ " |
| 67 | 84 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" |
| ... | ... | |
| 76 | 93 |
let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in |
| 77 | 94 |
compare (proj l1) (proj l2) |
| 78 | 95 |
end) |
| 79 |
let pp = pp_up |
|
| 96 |
let pp = pp_up Printers.pp_expr
|
|
| 80 | 97 |
end |
| 81 | 98 |
|
| 82 | 99 |
module Guards = struct |
Also available in: Unified diff
printing nodes + more progress on seal export