aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/heap.ml
blob: 47718bf3e7576a0789c8e4c39bd9503fbc62e525 (plain)
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

(*s Heaps *)

module type Ordered = sig
  type t
  val compare : t -> t -> int
end

module type S =sig
  
  (* Type of functional heaps *)
  type t

  (* Type of elements *)
  type elt
    
  (* The empty heap *)
  val empty : t
    
  (* [add x h] returns a new heap containing the elements of [h], plus [x];
     complexity $O(log(n))$ *)
  val add : elt -> t -> t
    
  (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
     when [h] is empty; complexity $O(1)$ *)
  val maximum : t -> elt
    
  (* [remove h] returns a new heap containing the elements of [h], except
     the maximum of [h]; raises [EmptyHeap] when [h] is empty; 
     complexity $O(log(n))$ *) 
  val remove : t -> t
    
  (* usual iterators and combinators; elements are presented in
     arbitrary order *)
  val iter : (elt -> unit) -> t -> unit
    
  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
    
end

exception EmptyHeap

(*s Functional implementation *)

module Functional(X : Ordered) = struct

  (* Heaps are encoded as complete binary trees, i.e., binary trees
     which are full expect, may be, on the bottom level where it is filled 
     from the left. 
     These trees also enjoy the heap property, namely the value of any node 
     is greater or equal than those of its left and right subtrees.

     There are 4 kinds of complete binary trees, denoted by 4 constructors:
     [FFF] for a full binary tree (and thus 2 full subtrees);
     [PPF] for a partial tree with a partial left subtree and a full
     right subtree;
     [PFF] for a partial tree with a full left subtree and a full right subtree
     (but of different heights);
     and [PFP] for a partial tree with a full left subtree and a partial
     right subtree. *)

  type t = 
    | Empty
    | FFF of t * X.t * t (* full    (full,    full) *)
    | PPF of t * X.t * t (* partial (partial, full) *)
    | PFF of t * X.t * t (* partial (full,    full) *)
    | PFP of t * X.t * t (* partial (full,    partial) *)

  type elt = X.t

  let empty = Empty
 
  (* smart constructors for insertion *)
  let p_f l x r = match l with
    | Empty | FFF _ -> PFF (l, x, r)
    | _ -> PPF (l, x, r)

  let pf_ l x = function
    | Empty | FFF _ as r -> FFF (l, x, r)
    | r -> PFP (l, x, r)

  let rec add x = function
    | Empty -> 
	FFF (Empty, x, Empty)
    (* insertion to the left *)
    | FFF (l, y, r) | PPF (l, y, r) ->
	if X.compare x y > 0 then p_f (add y l) x r else p_f (add x l) y r
    (* insertion to the right *)
    | PFF (l, y, r) | PFP (l, y, r) ->
	if X.compare x y > 0 then pf_ l x (add y r) else pf_ l y (add x r)

  let maximum = function
    | Empty -> raise EmptyHeap
    | FFF (_, x, _) | PPF (_, x, _) | PFF (_, x, _) | PFP (_, x, _) -> x

  (* smart constructors for removal; note that they are different
     from the ones for insertion! *)
  let p_f l x r = match l with
    | Empty | FFF _ -> FFF (l, x, r)
    | _ -> PPF (l, x, r)

  let pf_ l x = function
    | Empty | FFF _ as r -> PFF (l, x, r)
    | r -> PFP (l, x, r)

  let rec remove = function
    | Empty -> 
	raise EmptyHeap
    | FFF (Empty, _, Empty) -> 
	Empty
    | PFF (l, _, Empty) ->
	l
    (* remove on the left *)
    | PPF (l, x, r) | PFF (l, x, r) ->
        let xl = maximum l in
	let xr = maximum r in
	let l' = remove l in
	if X.compare xl xr >= 0 then 
	  p_f l' xl r 
	else 
	  p_f l' xr (add xl (remove r))
    (* remove on the right *)
    | FFF (l, x, r) | PFP (l, x, r) ->
        let xl = maximum l in
	let xr = maximum r in
	let r' = remove r in
	if X.compare xl xr > 0 then 
	  pf_ (add xr (remove l)) xl r'
	else 
	  pf_ l xr r'

  let rec iter f = function
    | Empty -> 
	()
    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
	iter f l; f x; iter f r

  let rec fold f h x0 = match h with
    | Empty -> 
	x0
    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
	fold f l (fold f r (f x x0))

end