lustrec / src / tools / seal / seal_utils.ml @ a0c92fa8
History | View | Annotate | Download (3.17 KB)
1 |
open Lustre_types |
---|---|
2 |
open Utils |
3 |
|
4 |
let report = Log.report ~plugin:"seal" |
5 |
let seal_debug = ref false |
6 |
|
7 |
type 'boolexpr guard = 'boolexpr list |
8 |
type ('guard, 'elem) guarded_expr = 'guard * 'elem |
9 |
|
10 |
|
11 |
type element = IsInit | Expr of expr |
12 |
type elem_boolexpr = element * bool |
13 |
|
14 |
type elem_guarded_expr = (elem_boolexpr guard, element) guarded_expr |
15 |
type 'ge mdef_t = 'ge list |
16 |
|
17 |
(* |
18 |
type mdef_t = guarded_expr list |
19 |
*) |
20 |
|
21 |
let pp_elem fmt e = |
22 |
match e with |
23 |
| IsInit -> Format.fprintf fmt "init" |
24 |
| Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e |
25 |
|
26 |
let pp_guard_list pp_elem fmt gl = |
27 |
(fprintf_list ~sep:";@ " |
28 |
(fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) fmt gl |
29 |
|
30 |
let pp_guard_expr pp_elem fmt (gl,e) = |
31 |
Format.fprintf fmt "@[<v 2>@[%a@] ->@ @[<hov 2>%a@]@]" |
32 |
(pp_guard_list pp_elem) gl |
33 |
pp_elem e |
34 |
|
35 |
let pp_mdefs pp_elem fmt gel = fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel |
36 |
|
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 |
) |
45 |
|
46 |
let deelem e = match e with |
47 |
Expr e -> e |
48 |
| IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *) |
49 |
|
50 |
let is_eq_elem elem elem' = |
51 |
match elem, elem' with |
52 |
| IsInit, IsInit -> true |
53 |
| Expr e, Expr e' -> Corelang.is_eq_expr e e' |
54 |
| _ -> false |
55 |
|
56 |
let select_elem elem (gelem, _) = |
57 |
is_eq_elem elem gelem |
58 |
|
59 |
let pp_gl pp_expr = |
60 |
fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e) |
61 |
|
62 |
let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) |
63 |
|
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 |
|
82 |
let pp_all_defs = |
83 |
(Utils.fprintf_list ~sep:",@ " |
84 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" |
85 |
id |
86 |
(pp_mdefs pp_elem) gel)) |
87 |
module UpMap = |
88 |
struct |
89 |
include Map.Make ( |
90 |
struct |
91 |
type t = (ident * expr) list |
92 |
let compare l1 l2 = |
93 |
let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in |
94 |
compare (proj l1) (proj l2) |
95 |
end) |
96 |
let pp = pp_up Printers.pp_expr |
97 |
end |
98 |
|
99 |
module Guards = struct |
100 |
include Set.Make ( |
101 |
struct |
102 |
type t = (expr * bool) |
103 |
let compare l1 l2 = |
104 |
let proj (e,b) = e.expr_tag, b in |
105 |
compare (proj l1) (proj l2) |
106 |
end) |
107 |
let pp_short fmt s = pp_gl_short fmt (elements s) |
108 |
let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s) |
109 |
end |
110 |
|
111 |
|