Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_utils.ml @ 03c767b1

History | View | Annotate | Download (2.78 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 "@[%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
                             
38
  
39
let deelem e =  match e with
40
    Expr e -> e
41
  | IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *)
42

    
43
let is_eq_elem elem elem' =
44
  match elem, elem' with
45
  | IsInit, IsInit -> true
46
  | Expr e, Expr e' -> e = e' (*
47
     Corelang.is_eq_expr e e' *)
48
  | _ -> false
49

    
50
let select_elem elem (gelem, _) =
51
  is_eq_elem elem gelem
52

    
53
let pp_gl pp_expr =
54
  fprintf_list ~sep:", " (fun fmt (e,b) -> Format.fprintf fmt "%s%a" (if b then "" else "NOT ") pp_expr e)
55
  
56
let pp_gl_short = pp_gl (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) 
57
let pp_up fmt up = List.iter (fun (id,e) -> Format.fprintf fmt "%s->%i; " id e.expr_tag) up 
58

    
59
let pp_sys fmt sw = List.iter (fun (gl,up) ->
60
                        match gl with
61
                        | None ->
62
                           pp_up fmt up
63
                        | Some gl ->
64
                           Format.fprintf fmt "[@[%a@]] -> (%a)@ "
65
                             Printers.pp_expr gl pp_up up) sw
66
                  
67
module UpMap =
68
  struct
69
    include Map.Make (
70
                struct
71
                  type t = (ident * expr) list
72
                  let compare l1 l2 =
73
                    let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in
74
                    compare (proj l1) (proj l2) 
75
                end)
76
    let pp = pp_up 
77
  end
78
    
79
module Guards = struct
80
  include Set.Make (
81
              struct
82
                type t = (expr * bool) 
83
                let compare l1 l2 =
84
                  let proj (e,b) = e.expr_tag, b in
85
                  compare (proj l1) (proj l2) 
86
              end)
87
  let pp_short fmt s = pp_gl_short fmt (elements s)
88
  let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s)
89
end
90
                  
91
                  
92