source: extracted/untrusted/pmap.ml @ 2755

Last change on this file since 2755 was 2738, checked in by sacerdot, 7 years ago

Porting the graph colouring stuff from the untrusted prototype to the extracted
code.

File size: 3.1 KB
Line 
1(* Copied from OCaml's Map to make it polymorphic *)
2
3    type ('k,'a) map =
4        Empty
5      | Node of ('k,'a) map * 'k * 'a * ('k,'a) map * int
6
7    let empty = Empty
8
9    let height = function
10        Empty -> 0
11      | Node(_,_,_,_,h) -> h
12
13    let rec find x = function
14        Empty ->
15          raise Not_found
16      | Node(l, v, d, r, _) ->
17          let c = compare x v in
18          if c = 0 then d
19          else find x (if c < 0 then l else r)
20
21    let create l x d r =
22      let hl = height l and hr = height r in
23      Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
24
25    let bal l x d r =
26      let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in
27      let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in
28      if hl > hr + 2 then begin
29        match l with
30          Empty -> invalid_arg "Map.bal"
31        | Node(ll, lv, ld, lr, _) ->
32            if height ll >= height lr then
33              create ll lv ld (create lr x d r)
34            else begin
35              match lr with
36                Empty -> invalid_arg "Map.bal"
37              | Node(lrl, lrv, lrd, lrr, _)->
38                  create (create ll lv ld lrl) lrv lrd (create lrr x d r)
39            end
40      end else if hr > hl + 2 then begin
41        match r with
42          Empty -> invalid_arg "Map.bal"
43        | Node(rl, rv, rd, rr, _) ->
44            if height rr >= height rl then
45              create (create l x d rl) rv rd rr
46            else begin
47              match rl with
48                Empty -> invalid_arg "Map.bal"
49              | Node(rll, rlv, rld, rlr, _) ->
50                  create (create l x d rll) rlv rld (create rlr rv rd rr)
51            end
52      end else
53        Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
54
55    let rec add x data = function
56        Empty ->
57          Node(Empty, x, data, Empty, 1)
58      | Node(l, v, d, r, h) ->
59          let c = compare x v in
60          if c = 0 then
61            Node(l, x, data, r, h)
62          else if c < 0 then
63            bal (add x data l) v d r
64          else
65            bal l v d (add x data r)
66
67    let rec min_binding = function
68        Empty -> raise Not_found
69      | Node(Empty, x, d, r, _) -> (x, d)
70      | Node(l, x, d, r, _) -> min_binding l
71
72    let rec remove_min_binding = function
73        Empty -> invalid_arg "Map.remove_min_elt"
74      | Node(Empty, x, d, r, _) -> r
75      | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
76
77    let merge t1 t2 =
78      match (t1, t2) with
79        (Empty, t) -> t
80      | (t, Empty) -> t
81      | (_, _) ->
82          let (x, d) = min_binding t2 in
83          bal t1 x d (remove_min_binding t2)
84
85    let rec remove x = function
86        Empty ->
87          Empty
88      | Node(l, v, d, r, h) ->
89          let c = compare x v in
90          if c = 0 then
91            merge l r
92          else if c < 0 then
93            bal (remove x l) v d r
94          else
95            bal l v d (remove x r)
96
97    let rec fold f m accu =
98      match m with
99        Empty -> accu
100      | Node(l, v, d, r, _) ->
101          fold f r (f v d (fold f l accu))
102
103(* Copied from atom.ml *)
104
105let restrict p m =
106    fold (fun x d m ->
107      if p x then
108        add x d m
109      else
110        m
111    ) m empty
Note: See TracBrowser for help on using the repository browser.