package frama-c

  1. Overview
  2. Docs

Source file partition.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

module type Elt =
sig
  type t
  val equal : t -> t -> bool
  val compare : t -> t -> int
end

module type Set =
sig
  type t
  type elt
  val singleton : elt -> t
  val iter : (elt -> unit) -> t -> unit
  val union : t -> t -> t
  val inter : t -> t -> t
end

module type Map =
sig
  type 'a t
  type key
  val empty : 'a t
  val is_empty : 'a t -> bool
  val find : key -> 'a t -> 'a
  val add : key -> 'a -> 'a t -> 'a t
  val remove : key -> 'a t -> 'a t
  val iter : (key -> 'a -> unit) -> 'a t -> unit
end

module Make(E : Elt)
    (S : Set with type elt = E.t)
    (M : Map with type key = E.t) =
struct

  type elt = E.t
  type set = S.t

  type t = {
    mutable dag : E.t M.t ;
    members : S.t M.t ;
    size : int ;
  }

  let empty = { size = 0 ; dag = M.empty ; members = M.empty }

  let rec lookup p a =
    try
      let a0 = M.find a p.dag in
      let a1 = lookup p a0 in
      p.dag <- M.add a a1 p.dag ; a1
    with Not_found -> a

  let equal t a b = E.equal (lookup t a) (lookup t b)
  let members p e =
    try M.find e p.members with Not_found -> S.singleton e

  let merge p a b =
    let a = lookup p a in
    let b = lookup p b in
    let cmp = E.compare a b in
    if cmp = 0 then p else
      let c = S.union (members p a) (members p b) in
      let size = succ p.size in
      if cmp < 0 then {
        size ; dag = M.add b a p.dag ;
        members = M.add a c (M.remove b p.members) ;
      } else {
        size ; dag = M.add a b p.dag ;
        members = M.add b c (M.remove a p.members) ;
      }

  let rec merge_with p e = function
    | [] -> p
    | e'::es -> merge_with (merge p e e') e es

  let merge_list p = function
    | [] -> p
    | e::es -> merge_with p e es

  let merge_set p s =
    let p = ref p in
    let w = ref None in
    S.iter
      (fun e ->
         match !w with
         | None -> w := Some e
         | Some u -> p := merge !p u e
      ) s ;
    !p

  let iter f p = M.iter f p.members
  let unstable_iter f p = M.iter f p.dag

  let map f p =
    let r = ref empty in
    M.iter (fun a b -> r := merge !r (f a) (f b)) p.dag ; !r

  let merge_dag p dag =
    let r = ref p in
    M.iter (fun a b -> r := merge !r a b) dag ; !r

  let union p q =
    if p.size < q.size
    then merge_dag q p.dag
    else merge_dag p q.dag

  let inter p q =
    let r = ref empty in
    M.iter (fun _ ca ->
        M.iter (fun _ cb ->
            r := merge_set !r (S.inter ca cb)
          ) q.members
      ) p.members ;
    !r

  let is_empty p = M.is_empty p.dag

end