Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

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