(* Heaps (as in heapsort).
   Copyright (C) 2003 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "heap_h";

(*$E-*) (* turn off sharing for heaps. *)
datatype 'a heap = EmptyHeap | BranchHeap of 'a * 'a heap * 'a heap
(*$E+*)

(* The invariant on heaps is as follows:
 either it is EmptyHeap (empty), or its root node contains the
 least element of the heap, and the two successors are again heaps.
 Furthermore, heaps are balanced, and last rows can only be of the
 form:
 branch(empty,empty) ... branch(empty, empty) empty ... empty
 (more or less).
 *)

infix 4 less;

fun mheap (op less) =
    let fun up (w, EmptyHeap) = BranchHeap (w, EmptyHeap, EmptyHeap)
	  | up (w, b as BranchHeap (v, p, q)) =
	    if w less v
		then BranchHeap (w, up (v, q), p)
	    else if w=v
		then b
	    else BranchHeap (v, up (w, q), p)
	fun removeleft (BranchHeap (w,EmptyHeap,_)) = (w,EmptyHeap)
	  | removeleft (BranchHeap (w,p,q)) =
	    let val (x,p') = removeleft p
	    in
		(x, BranchHeap (w,q,p'))
	    end
	fun siftdown (x,EmptyHeap,_) = BranchHeap (x,EmptyHeap,EmptyHeap)
	  | siftdown (x, p as BranchHeap (y,_,_), EmptyHeap) =
	    if x less y
		then BranchHeap (x,p,EmptyHeap)
	    else BranchHeap (y, BranchHeap (x,EmptyHeap,EmptyHeap), EmptyHeap)
	  | siftdown (x, p as BranchHeap (y,p1,q1), q as BranchHeap (z,p2,q2)) =
	    if x less y andalso x less z
		then BranchHeap (x,p,q)
	    else if y less z
		then BranchHeap (y, siftdown (x,p1,q1), q)
	    else BranchHeap (z, p, siftdown (x,p2,q2))
	fun deletemin EmptyHeap = raise MHeapEmptyEvt
	  | deletemin (BranchHeap (w,EmptyHeap,q)) = q
	  | deletemin (BranchHeap (w,p,q)) =
	    let val (x,p') = removeleft p
	    in
		siftdown (x,q,p')
	    end
	fun mklist (EmptyHeap, acc) = acc
	  | mklist (p as BranchHeap (w,...), acc) =
	    mklist (deletemin p, w::acc)
	fun dump (EmptyHeap, acc) = acc
	  | dump (BranchHeap (w, p, q), acc) =
	    dump (p, dump (q, w::acc))

	val the_heap = ref EmptyHeap
    in
	|[insert = (fn x => the_heap := up (x, !the_heap)),
	   findmin = (fn () =>
			 case !the_heap of
			     BranchHeap (w,...) => w
			   | _ => raise MHeapEmptyEvt),
	   popmin = (fn () =>
			case !the_heap of
			    BranchHeap (w, ...) =>
			    (the_heap := deletemin (!the_heap);
			     w)
			  | _ => raise MHeapEmptyEvt),
	   cvt_to_revlist = (fn () => mklist (!the_heap, nil) before the_heap := EmptyHeap),
	   empty = (fn () => case !the_heap of
				 EmptyHeap => true
			       | _ => false),
	   dump_list = (fn () => dump (!the_heap, nil))
	   ]|
    end;
