Project

General

Profile

Download (2.71 KB) Statistics
| Branch: | Tag: | Revision:
1 a703ed0c ploc
open Lustre_types
2
open Utils
3 ca7ff3f7 Lélio Brun
4 a742719e ploc
let report = Log.report ~plugin:"seal"
5 ca7ff3f7 Lélio Brun
6 03c767b1 ploc
let seal_debug = ref false
7 a703ed0c ploc
8 ca7ff3f7 Lélio Brun
type 'boolexpr guard = 'boolexpr list
9
10
type ('guard, 'elem) guarded_expr = 'guard * 'elem
11 03c767b1 ploc
12
type element = IsInit | Expr of expr
13 ca7ff3f7 Lélio Brun
14 03c767b1 ploc
type elem_boolexpr = element * bool
15
16
type elem_guarded_expr = (elem_boolexpr guard, element) guarded_expr
17 ca7ff3f7 Lélio Brun
18
type 'ge mdef_t = 'ge list
19
20
(* type mdef_t = guarded_expr list *)
21
22 03c767b1 ploc
let pp_elem fmt e =
23
  match e with
24 ca7ff3f7 Lélio Brun
  | IsInit ->
25
    Format.fprintf fmt "init"
26
  | Expr e ->
27
    Format.fprintf fmt "%a" Printers.pp_expr e
28 03c767b1 ploc
29
let pp_guard_list pp_elem fmt gl =
30 ca7ff3f7 Lélio Brun
  (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 03c767b1 ploc
38 ca7ff3f7 Lélio Brun
let pp_mdefs pp_elem fmt gel =
39
  fprintf_list ~sep:"@ " (pp_guard_expr pp_elem) fmt gel
40 03c767b1 ploc
41 a0c92fa8 ploc
let pp_assign_map pp_elem =
42 ca7ff3f7 Lélio Brun
  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 03c767b1 ploc
48
let is_eq_elem elem elem' =
49
  match elem, elem' with
50 ca7ff3f7 Lélio Brun
  | IsInit, IsInit ->
51
    true
52
  | Expr e, Expr e' ->
53
    Corelang.is_eq_expr e e'
54
  | _ ->
55
    false
56 03c767b1 ploc
57 ca7ff3f7 Lélio Brun
let select_elem elem (gelem, _) = is_eq_elem elem gelem
58 03c767b1 ploc
59
let pp_gl pp_expr =
60 ca7ff3f7 Lélio Brun
  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 03c767b1 ploc
66 a0c92fa8 ploc
let pp_up pp_elem fmt up =
67
  fprintf_list ~sep:"@ "
68 ca7ff3f7 Lélio Brun
    (fun fmt (id, e) -> Format.fprintf fmt "%s == %a;@ " id pp_elem e)
69
    fmt up
70 a0c92fa8 ploc
71
let pp_sys pp_elem fmt sw =
72
  fprintf_list ~sep:"@ "
73 ca7ff3f7 Lélio Brun
    (fun fmt (gl, up) ->
74 a0c92fa8 ploc
      match gl with
75
      | None ->
76 ca7ff3f7 Lélio Brun
        (pp_up pp_elem) fmt up
77 a0c92fa8 ploc
      | Some gl ->
78 ca7ff3f7 Lélio Brun
        Format.fprintf fmt "@[<v 2>[@[%a@]]:@ %a@]" Printers.pp_expr gl
79
          (pp_up pp_elem) up)
80
    fmt sw
81
82 ae08b9fc ploc
let pp_all_defs =
83 ca7ff3f7 Lélio Brun
  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 03c767b1 ploc
module Guards = struct
99 ca7ff3f7 Lélio Brun
  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 03c767b1 ploc
  let pp_short fmt s = pp_gl_short fmt (elements s)
108 ca7ff3f7 Lélio Brun
109 03c767b1 ploc
  let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s)
110
end