Project

General

Profile

Download (2.71 KB) Statistics
| Branch: | Tag: | Revision:
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
(5-5/6)