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