(* 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";
open "queue_h";

(*$E-*) (* turn off sharing for heaps. *)
datatype 'a mheap = MH_empty
       | MH_branch of 'a ref * 'a mheap ref * 'a mheap ref;
(*$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).
 *)

exception MkList;
exception Dump;
exception PopMin;
exception PopMins;
exception FindMin;

fun mheap less =
    let val mhr = ref MH_empty
	fun up (w, mhr as ref MH_empty) =
	    mhr := MH_branch (ref w, ref MH_empty, ref MH_empty)
	  | up (w, ref (MH_branch (vr as ref v, pr as ref p, qr as ref q))) =
	    (pr := q;
	     qr := p;
	     if less (w, v)
		 then (vr := w;
		       up (v, pr))
	     else up (w, pr))
	fun removeleft (mhr as ref (MH_branch (ref w, ref MH_empty, _))) =
	    (mhr := MH_empty;
	     w)
	  | removeleft (ref (MH_branch (_, pr, qr as ref q))) =
	    (qr := !pr;
	     pr := q;
	     removeleft qr)
	fun siftdown (x, MH_branch (wr, ref MH_empty, _)) =
	    wr := x
	  | siftdown (x, MH_branch (wr,
				    ref (MH_branch (yr as ref y, ...)),
				    ref MH_empty)) =
	    if less (x, y)
		then wr := x
	    else (wr := y;
		  yr := x)
	  | siftdown (x, MH_branch (wr,
				    ref (p as MH_branch (ref y,
							 ...)),
				    ref (q as MH_branch (ref z,
							 ...)))) =
	    if less (x, y) andalso less (x, z)
		then wr := x
	    else if less (y, z)
		then (wr := y;
		      siftdown (x, p))
	    else (wr := z;
		  siftdown (x, q))
	fun deletemin (ref MH_empty) = raise MHeapEmptyEvt
	  | deletemin (mhr as ref (MH_branch (ref w, ref MH_empty, ref q))) =
	    mhr := q
	  | deletemin (ref (mh as MH_branch (_, pr, qr as ref q))) =
	    let val x = removeleft pr
	    in
		qr := !pr;
		pr := q;
		siftdown (x, mh)
	    end

	val tx = table ()
	val txget = t_get tx
	val txput = t_put tx
	val txrem = t_remove tx

	fun mklist acc =
	    case !mhr of
		MH_empty => acc
	      | MH_branch (ref xa, ...) =>
		(deletemin mhr;
		 case txget xa of
		     SOME (xas) =>
		     mklist ([(xa, xb) | xb in list #mklist xas ()] @  acc)
		   | _ => raise MkList)
	fun dump (MH_empty, acc) = acc
	  | dump (MH_branch (ref xa, ref l, ref r), acc) =
	    dump (l, dump (r, [xb | xb in list (case txget xa of
						    SOME (xas) => #mklist xas ()
						  | _ => raise Dump)] @ acc))
	fun iter f =
	    (t_iter tx (fn (xa, xas) =>
			   (iterate
			      f (xa, xb)
			    | xb in list #mklist xas ()
			    end;
			      false));
	     ())
    in
	|[ insert = (fn (xa, xb) =>
			(case txget xa of
			     SOME xas => #push xas xb
			   | _ => let val q = queue ()
				  in
				      #push q xb;
				      txput (xa, q);
				      up (xa, mhr)
				  end)),
	   findmin = (fn () =>
			 case !mhr of
			     MH_empty => raise MHeapEmptyEvt
			   | MH_branch (ref xa, ...) =>
			     (case txget xa of
				  SOME (xas) => (xa, #top xas ())
				| _ => raise FindMin)),
	   popmin = (fn () =>
			case !mhr of
			    MH_empty => raise MHeapEmptyEvt
			  | MH_branch (ref xa, ...) =>
			    (case txget xa of
				 SOME xas =>
				 let val xb = #pop xas ()
				 in
				     if #empty xas ()
					 then (deletemin mhr; txrem xa)
				     else ();
					 (xa, xb)
				 end
			       | _ => raise PopMin)),
	   cvt_to_revlist = (fn () => mklist nil before t_reset tx),
	   empty = (fn () =>
		       case !mhr of
			   MH_empty => true
			 | _ => false),
	   dump_list = (fn () => dump (!mhr, nil)),
	   iter = iter
	   ]|
    end;
