package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file mergeset.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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Merging Set Functor                                                --- *)
(* -------------------------------------------------------------------------- *)

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

module Make(E : Elt) =
struct

  module Lset = Listset.Make(E)

  type elt = E.t

  type t = E.t list Intmap.t

  let _nonempty = function [] -> None | l -> Some l

  let is_empty es =
    try
      Intmap.iteri (fun _ s -> if s <> [] then raise Exit) es ;
      true
    with Exit -> false
  let empty = Intmap.empty

  let add e m =
    let h = E.hash e in
    let w = try Lset.add e (Intmap.find h m) with Not_found -> [e] in
    Intmap.add h w m

  let singleton e =
    let h = E.hash e in
    Intmap.add h [e] Intmap.empty

  let mem e m =
    try Lset.mem e (Intmap.find (E.hash e) m)
    with Not_found -> false

  let elements m =
    Intmap.fold (fun w xs -> List.merge E.compare w xs) m []

  let iter_sorted f m =
    List.iter f (elements m)

  let fold_sorted f m a =
    List.fold_left (fun acc x -> f x acc) a (elements m)

  (* good sharing *)
  let filter f m =
    Intmap.mapq (fun _ l -> _nonempty (Lset.filter f l)) m

  (* good sharing *)
  let remove k m =
    let h = E.hash k in
    Intmap.change (fun _h k -> function
        | None -> None
        | Some old -> _nonempty (Lset.remove k old)) h k m
  (* good sharing *)
  let partition f =
    Intmap.partition_split (fun _k w ->
        let u,v = Lset.partition f w in
        (_nonempty u), (_nonempty v))

  exception BREAK

  let iter f = Intmap.iter (Lset.iter f)
  let fold f = Intmap.fold (Lset.fold f)

  let for_all f m =
    try iter (fun x -> if not (f x) then raise BREAK) m ; true
    with BREAK -> false

  let exists f m =
    try iter (fun x -> if f x then raise BREAK) m ; false
    with BREAK -> true

  (* good sharing *)
  let diff = Intmap.diffq (fun _h a b ->
      match Lset.diff a b with
      | [] -> None
      | l -> Some l
    )

  (* good sharing *)
  let union = Intmap.union (fun _h -> Lset.union)

  (* good sharing *)
  let inter = Intmap.inter (fun _h -> Lset.inter)

  (* good sharing *)
  let subset = Intmap.subset (fun _h -> Lset.subset)

  let intersect m1 m2 =
    try
      Intmap.iter2
        (fun _h xs ys ->
           match xs , ys with
           | None , _ | _ , None -> ()
           | Some w1 , Some w2 -> if Lset.intersect w1 w2 then raise Exit
        ) m1 m2 ; false
    with Exit -> true

  let equal = Intmap.equal Lset.equal
  let compare = Intmap.compare Lset.compare

  let of_list l = List.fold_left (fun acc e -> add e acc) empty l
end