Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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