/* Pairing heap

Reference:

- Chris Okasaki. Purely Functional Data Structures. Cambridge University Press 1999.
*/
module ck/heapck/heap

type multiway-treeck/heap/multiway-tree: V -> V<aa: V>
  Empck/heap/Emp: forall<a> multiway-tree<a>
  Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>{ value: aa: V; sub: liststd/core/types/list: V -> V<multiway-treeck/heap/multiway-tree: V -> V<aa: V>> }

/// Implementation notes of `pairing-heap`:
/// - The constructor should not take a comparison function as a field because
///   it is too slow. It is better to pass comparison functions or structs with
///   them to the operations as implicit parameters instead.

abstract type pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  PairingHeapck/heap/PairingHeap: forall<a> (tree : multiway-tree<a>) -> pairing-heap<a>{ treeck/heap/pairing-heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>: multiway-treeck/heap/multiway-tree: V -> V<aa: V> }

// Check whether a heap is empty
pub inline fun is-emptyck/heap/is-empty: forall<a> (h : pairing-heap<a>) -> bool(hh: pairing-heap<$163>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>)result: -> total bool: boolstd/core/types/bool: V
  match hh: pairing-heap<$163>.treeck/heap/pairing-heap/tree: (pairing-heap<$163>) -> multiway-tree<$163>
    Empck/heap/Emp: forall<a> multiway-tree<a> -> Truestd/core/types/True: bool
    _ -> Falsestd/core/types/False: bool

// Create an empty heap.
pub inline fun emptyck/heap/empty: forall<a> () -> pairing-heap<a>()result: -> total pairing-heap<208>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  PairingHeapck/heap/PairingHeap: forall<a> (tree : multiway-tree<a>) -> pairing-heap<a>(Empck/heap/Emp: forall<a> multiway-tree<a>)

// Create a heap with a single element.
pub inline fun singletonck/heap/singleton: forall<a> (v : a) -> pairing-heap<a>(vv: $213: aa: V)result: -> total pairing-heap<238>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  PairingHeapck/heap/PairingHeap: forall<a> (tree : multiway-tree<a>) -> pairing-heap<a>(Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $213, [std/core/types/Nil: forall<a> list<a>]std/core/types/Nil: forall<a> list<a>))

fun multiway-tree/meldck/heap/multiway-tree/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, @implicit/(<) : (a, a) -> bool) -> multiway-tree<a>(t1t1: multiway-tree<$243>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, t2t2: multiway-tree<$243>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, (@implicit/<)?(<): ($243, $243) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V)result: -> total multiway-tree<343>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>
  match t1t1: multiway-tree<$243>
    Empck/heap/Emp: forall<a> multiway-tree<a> -> t2t2: multiway-tree<$243>
    Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v1v1: $243, ss1ss1: list<multiway-tree<$243>>) ->
      match t2t2: multiway-tree<$243>
        Empck/heap/Emp: forall<a> multiway-tree<a> -> t1t1: multiway-tree<$243>
        Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v2v2: $243, ss2ss2: list<multiway-tree<$243>>) ->
          if v1v1: $243 <?(<): ($243, $243) -> bool v2v2: $243 then
            Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v1v1: $243, Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t2t2: multiway-tree<$243>, ss1ss1: list<multiway-tree<$243>>))
          else
            Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v2v2: $243, Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t1t1: multiway-tree<$243>, ss2ss2: list<multiway-tree<$243>>))

// Combine two heaps.
// Assume they use the same ordering function
pub inline fun meldck/heap/meld: forall<a> (h1 : pairing-heap<a>, h2 : pairing-heap<a>, @implicit/(<) : (a, a) -> bool) -> pairing-heap<a>(h1h1: pairing-heap<$348>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, h2h2: pairing-heap<$348>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, (@implicit/<)?(<): ($348, $348) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V)result: -> total pairing-heap<415>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  PairingHeapck/heap/PairingHeap: forall<a> (tree : multiway-tree<a>) -> pairing-heap<a>(meldck/heap/multiway-tree/meld: (t1 : multiway-tree<$348>, t2 : multiway-tree<$348>, @implicit/(<) : ($348, $348) -> bool) -> multiway-tree<$348>
?(<)=?(<)(h1h1: pairing-heap<$348>.treeck/heap/pairing-heap/tree: (pairing-heap<$348>) -> multiway-tree<$348>, h2h2: pairing-heap<$348>.treeck/heap/pairing-heap/tree: (pairing-heap<$348>) -> multiway-tree<$348>))

inline fun multiway-tree/addck/heap/multiway-tree/add: forall<a> (t : multiway-tree<a>, v : a, @implicit/(<) : (a, a) -> bool) -> multiway-tree<a>(tt: multiway-tree<$423>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, vv: $423: aa: V, (@implicit/<)?(<): ($423, $423) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V)result: -> total multiway-tree<479>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>
  meldck/heap/multiway-tree/meld: (t1 : multiway-tree<$423>, t2 : multiway-tree<$423>, @implicit/(<) : ($423, $423) -> bool) -> multiway-tree<$423>
?(<)=?(<)(tt: multiway-tree<$423>, Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $423, [std/core/types/Nil: forall<a> list<a>]std/core/types/Nil: forall<a> list<a>))

// Add a value to a heap
pub inline fun addck/heap/add: forall<a> (h : pairing-heap<a>, v : a, @implicit/(<) : (a, a) -> bool) -> pairing-heap<a>(hh: pairing-heap<$484>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, vv: $484: aa: V, (@implicit/<)?(<): ($484, $484) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V)result: -> total pairing-heap<544>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  PairingHeapck/heap/PairingHeap: forall<a> (tree : multiway-tree<a>) -> pairing-heap<a>(hh: pairing-heap<$484>.treeck/heap/pairing-heap/tree: (pairing-heap<$484>) -> multiway-tree<$484>.addck/heap/multiway-tree/add: (t : multiway-tree<$484>, v : $484, @implicit/(<) : ($484, $484) -> bool) -> multiway-tree<$484>
?(<)=?(<)(vv: $484))

// Return the minimum element of a heap
pub inline fun minck/heap/min: forall<a> (h : pairing-heap<a>) -> maybe<a>(hh: pairing-heap<$552>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>)result: -> total maybe<587>: maybestd/core/types/maybe: V -> V<aa: V>
  match hh: pairing-heap<$552>.treeck/heap/pairing-heap/tree: (pairing-heap<$552>) -> multiway-tree<$552>
    Empck/heap/Emp: forall<a> multiway-tree<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $552, _) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(vv: $552)

fun meld-pairsck/heap/meld-pairs: forall<a> (ts : list<multiway-tree<a>>, @implicit/(<) : (a, a) -> bool) -> multiway-tree<a>(tsts: list<multiway-tree<$592>>: liststd/core/types/list: V -> V<multiway-treeck/heap/multiway-tree: V -> V<aa: V>>, (@implicit/<)?(<): ($592, $592) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V)result: -> total multiway-tree<736>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>
  match tsts: list<multiway-tree<$592>>
    Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t1t1: multiway-tree<$592>, Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t2t2: multiway-tree<$592>, ts'ts': list<multiway-tree<$592>>)) -> meldck/heap/multiway-tree/meld: (t1 : multiway-tree<$592>, t2 : multiway-tree<$592>, @implicit/(<) : ($592, $592) -> bool) -> multiway-tree<$592>
?(<)=?(<)(meldck/heap/multiway-tree/meld: (t1 : multiway-tree<$592>, t2 : multiway-tree<$592>, @implicit/(<) : ($592, $592) -> bool) -> multiway-tree<$592>
?(<)=?(<)(t1t1: multiway-tree<$592>, t2t2: multiway-tree<$592>), ts'ts': list<multiway-tree<$592>>.meld-pairsck/heap/meld-pairs: (ts : list<multiway-tree<$592>>, @implicit/(<) : ($592, $592) -> bool) -> multiway-tree<$592>
?(<)=?(<))
    [std/core/types/Nil: forall<a> list<a>]std/core/types/Nil: forall<a> list<a> -> Empck/heap/Emp: forall<a> multiway-tree<a>
    [tstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>]std/core/types/Nil: forall<a> list<a> -> tt: multiway-tree<$592>

// Remove the minimum element from a heap.
// Do nothing if the given heap is empty
pub inline fun remove-minck/heap/remove-min: forall<a> (h : pairing-heap<a>, @implicit/(<) : (a, a) -> bool) -> pairing-heap<a>(hh: pairing-heap<$741>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, (@implicit/<)?(<): ($741, $741) -> bool: (aa: V, aa: V) -> boolstd/core/types/bool: V)result: -> total pairing-heap<810>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  match hh: pairing-heap<$741>.treeck/heap/pairing-heap/tree: (pairing-heap<$741>) -> multiway-tree<$741>
    Empck/heap/Emp: forall<a> multiway-tree<a> -> hh: pairing-heap<$741>
    Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(_, ssss: list<multiway-tree<$741>>) -> PairingHeapck/heap/PairingHeap: forall<a> (tree : multiway-tree<a>) -> pairing-heap<a>(ssss: list<multiway-tree<$741>>.meld-pairsck/heap/meld-pairs: (ts : list<multiway-tree<$741>>, @implicit/(<) : ($741, $741) -> bool) -> multiway-tree<$741>
?(<)=?(<))