| author | wenzelm | 
| Tue, 09 Sep 2008 16:29:34 +0200 | |
| changeset 28177 | 8c0335bc9336 | 
| parent 23510 | 4521fead5609 | 
| child 39353 | 7f11d833d65b | 
| permissions | -rw-r--r-- | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
1  | 
(* ========================================================================= *)  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
2  | 
(* A HEAP DATATYPE FOR ML *)  | 
| 23510 | 3  | 
(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)  | 
| 
23442
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
4  | 
(* ========================================================================= *)  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
5  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
6  | 
structure Heap :> Heap =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
struct  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
8  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
9  | 
(* Leftist heaps as in Purely Functional Data Structures, by Chris Okasaki *)  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
10  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
11  | 
datatype 'a node = E | T of int * 'a * 'a node * 'a node;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
12  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
13  | 
datatype 'a heap = Heap of ('a * 'a -> order) * int * 'a node;
 | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
14  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
15  | 
fun rank E = 0  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
16  | 
| rank (T (r,_,_,_)) = r;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
fun makeT (x,a,b) =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
19  | 
if rank a >= rank b then T (rank b + 1, x, a, b) else T (rank a + 1, x, b, a);  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
20  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
21  | 
fun merge cmp =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
22  | 
let  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
fun mrg (h,E) = h  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
24  | 
| mrg (E,h) = h  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
25  | 
| mrg (h1 as T (_,x,a1,b1), h2 as T (_,y,a2,b2)) =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
case cmp (x,y) of  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
GREATER => makeT (y, a2, mrg (h1,b2))  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
28  | 
| _ => makeT (x, a1, mrg (b1,h2))  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
in  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
30  | 
mrg  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
31  | 
end;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
32  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
33  | 
fun new cmp = Heap (cmp,0,E);  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
34  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
35  | 
fun add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (T (1,x,E,E), a));  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
36  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
37  | 
fun size (Heap (_, n, _)) = n;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
38  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
39  | 
fun null h = size h = 0;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
40  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
41  | 
fun top (Heap (_,_,E)) = raise Empty  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
42  | 
| top (Heap (_, _, T (_,x,_,_))) = x;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
43  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
44  | 
fun remove (Heap (_,_,E)) = raise Empty  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
45  | 
| remove (Heap (f, n, T (_,x,a,b))) = (x, Heap (f, n - 1, merge f (a,b)));  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
46  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
47  | 
fun app f =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
48  | 
let  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
49  | 
fun ap [] = ()  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
50  | 
| ap (E :: rest) = ap rest  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
51  | 
| ap (T (_,d,a,b) :: rest) = (f d; ap (a :: b :: rest))  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
52  | 
in  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
53  | 
fn Heap (_,_,a) => ap [a]  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
54  | 
end;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
55  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
56  | 
fun toList h =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
57  | 
if null h then []  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
58  | 
else  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
59  | 
let  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
60  | 
val (x,h) = remove h  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
61  | 
in  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
62  | 
x :: toList h  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
63  | 
end;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
64  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
65  | 
fun toStream h =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
66  | 
if null h then Stream.NIL  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
67  | 
else  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
68  | 
let  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
69  | 
val (x,h) = remove h  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
70  | 
in  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
71  | 
Stream.CONS (x, fn () => toStream h)  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
72  | 
end;  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
73  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
74  | 
fun toString h =  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
75  | 
"Heap[" ^ (if null h then "" else Int.toString (size h)) ^ "]";  | 
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
76  | 
|
| 
 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
 
wenzelm 
parents:  
diff
changeset
 | 
77  | 
end  |