Revision ca7ff3f7
Added by Lélio Brun 8 months ago
| src/tools/seal/seal_utils.ml | ||
|---|---|---|
| 1 | 1 |
open Lustre_types |
| 2 | 2 |
open Utils |
| 3 |
|
|
| 3 |
|
|
| 4 | 4 |
let report = Log.report ~plugin:"seal" |
| 5 |
|
|
| 5 | 6 |
let seal_debug = ref false |
| 6 | 7 |
|
| 7 |
type 'boolexpr guard = 'boolexpr list |
|
| 8 |
type ('guard, 'elem) guarded_expr = 'guard * 'elem
|
|
| 8 |
type 'boolexpr guard = 'boolexpr list |
|
| 9 |
|
|
| 10 |
type ('guard, 'elem) guarded_expr = 'guard * 'elem
|
|
| 9 | 11 |
|
| 10 |
|
|
| 11 | 12 |
type element = IsInit | Expr of expr |
| 13 |
|
|
| 12 | 14 |
type elem_boolexpr = element * bool |
| 13 | 15 |
|
| 14 | 16 |
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 |
|
|
| 17 |
|
|
| 18 |
type 'ge mdef_t = 'ge list |
|
| 19 |
|
|
| 20 |
(* type mdef_t = guarded_expr list *) |
|
| 21 |
|
|
| 21 | 22 |
let pp_elem fmt e = |
| 22 | 23 |
match e with |
| 23 |
| IsInit -> Format.fprintf fmt "init" |
|
| 24 |
| Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e |
|
| 24 |
| IsInit -> |
|
| 25 |
Format.fprintf fmt "init" |
|
| 26 |
| Expr e -> |
|
| 27 |
Format.fprintf fmt "%a" Printers.pp_expr e |
|
| 25 | 28 |
|
| 26 | 29 |
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 |
|
| 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
|
|
| 34 | 37 |
|
| 35 |
let pp_mdefs pp_elem fmt gel = fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel |
|
| 38 |
let pp_mdefs pp_elem fmt gel = |
|
| 39 |
fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel |
|
| 36 | 40 |
|
| 37 | 41 |
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! *) |
|
| 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! *) |
|
| 49 | 47 |
|
| 50 | 48 |
let is_eq_elem elem elem' = |
| 51 | 49 |
match elem, elem' with |
| 52 |
| IsInit, IsInit -> true |
|
| 53 |
| Expr e, Expr e' -> Corelang.is_eq_expr e e' |
|
| 54 |
| _ -> false |
|
| 50 |
| IsInit, IsInit -> |
|
| 51 |
true |
|
| 52 |
| Expr e, Expr e' -> |
|
| 53 |
Corelang.is_eq_expr e e' |
|
| 54 |
| _ -> |
|
| 55 |
false |
|
| 55 | 56 |
|
| 56 |
let select_elem elem (gelem, _) = |
|
| 57 |
is_eq_elem elem gelem |
|
| 57 |
let select_elem elem (gelem, _) = is_eq_elem elem gelem |
|
| 58 | 58 |
|
| 59 | 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) |
|
| 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) |
|
| 63 | 65 |
|
| 64 | 66 |
let pp_up pp_elem fmt up = |
| 65 | 67 |
fprintf_list ~sep:"@ " |
| 66 |
(fun fmt (id,e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e) |
|
| 67 |
fmt |
|
| 68 |
up |
|
| 68 |
(fun fmt (id, e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e) |
|
| 69 |
fmt up |
|
| 69 | 70 |
|
| 70 | 71 |
let pp_sys pp_elem fmt sw = |
| 71 | 72 |
fprintf_list ~sep:"@ " |
| 72 |
(fun fmt (gl,up) -> |
|
| 73 |
(fun fmt (gl, up) ->
|
|
| 73 | 74 |
match gl with |
| 74 | 75 |
| None -> |
| 75 |
(pp_up pp_elem) fmt up
|
|
| 76 |
(pp_up pp_elem) fmt up |
|
| 76 | 77 |
| 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 |
|
|
| 78 |
Format.fprintf fmt "@[<v 2>[@[%a@]]:@ %a@]" Printers.pp_expr gl |
|
| 79 |
(pp_up pp_elem) up) |
|
| 80 |
fmt sw |
|
| 81 |
|
|
| 82 | 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 |
|
|
| 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 |
|
|
| 99 | 98 |
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) |
|
| 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 | 107 |
let pp_short fmt s = pp_gl_short fmt (elements s) |
| 108 |
|
|
| 108 | 109 |
let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s) |
| 109 | 110 |
end |
| 110 |
|
|
| 111 |
|
|
Also available in: Unified diff
reformatting