/* Pairing heap

Reference:

- Chris Okasaki. Purely Functional Data Structures. Cambridge University Press 1999.

Warning: this implementation is slow
*/
module 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>{ valuevalue: 5: aa: V; subsub: list<multiway-tree<5>>: liststd/core/list: V -> V<multiway-treeck/heap/multiway-tree: V -> V<aa: V>> }

warning: Type pairing-heap may be better declared as a value type for efficiency (e.g. 'value type/struct'),
or declared as a reference type to suppress this warning (e.g. 'ref type/struct')abstract type pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>{ treetree: multiway-tree<11>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>; compcomp: (11, 11) -> order: (aa: V, aa: V) -> orderstd/core/types/order: 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<$165>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): boolstd/core/types/bool: V
  match hh: pairing-heap<$165>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>
    Empck/heap/Emp: forall<a> multiway-tree<a> -> Truestd/core/types/True: bool
    _ -> Falsestd/core/types/False: bool

// Create an empty heap.
// `comp` determines the order of elements in the heap
pub inline fun emptyck/heap/empty: forall<a> (comp : (a, a) -> order) -> pairing-heap<a>(compcomp: ($152, $152) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(Empck/heap/Emp: forall<a> multiway-tree<a>, compcomp: ($152, $152) -> order)

// Create a heap with a single element.
// `comp` determines the order of elements in the heap
pub inline fun singletonck/heap/singleton: forall<a> (v : a, comp : (a, a) -> order) -> pairing-heap<a>(vv: $203: aa: V, compcomp: ($203, $203) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $203, [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a>), compcomp: ($203, $203) -> order)

fun meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(t1t1: multiway-tree<$222>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, t2t2: multiway-tree<$222>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, compcomp: ($222, $222) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): multiway-treeck/heap/multiway-tree: V -> V<aa: V>
  match t1t1: multiway-tree<$222>
    Empck/heap/Emp: forall<a> multiway-tree<a> -> t2t2: multiway-tree<$222>
    Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v1v1: $222, ss1ss1: list<multiway-tree<$222>>) ->
      match t2t2: multiway-tree<$222>
        Empck/heap/Emp: forall<a> multiway-tree<a> -> t1t1: multiway-tree<$222>
        Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v2v2: $222, ss2ss2: list<multiway-tree<$222>>) ->
          if compcomp: ($222, $222) -> order(v1v1: $222, v2v2: $222).is-ltstd/core/types/is-lt: (order : order) -> bool then
            Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v1v1: $222, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t2t2: multiway-tree<$222>, ss1ss1: list<multiway-tree<$222>>))
          else
            Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v2v2: $222, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t1t1: multiway-tree<$222>, ss2ss2: list<multiway-tree<$222>>))

// Combine two heaps.
// Assume they use the same ordering function
pub inline fun meldck/heap/meld.1: forall<a> (h1 : pairing-heap<a>, h2 : pairing-heap<a>) -> pairing-heap<a>(h1h1: pairing-heap<$271>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, h2h2: pairing-heap<$271>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(h1h1: pairing-heap<$271>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>, h2h2: pairing-heap<$271>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>, h1h1: pairing-heap<$271>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order)), h1h1: pairing-heap<$271>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order))

fun insertck/heap/insert: forall<a> (t : multiway-tree<a>, v : a, comp : (a, a) -> order) -> multiway-tree<a>(tt: multiway-tree<$420>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, vv: $420: aa: V, compcomp: ($420, $420) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): multiway-treeck/heap/multiway-tree: V -> V<aa: V>
  match tt: multiway-tree<$420>
    Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(aa: $420, ssss: list<multiway-tree<$420>>) ->
      if compcomp: ($420, $420) -> order(vv: $420, aa: $420).is-ltstd/core/types/is-lt: (order : order) -> bool then
        Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $420, [std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>tt: multiway-tree<$420>]std/core/Nil: forall<a> list<a>)
      else
        Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(aa: $420, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $420, [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a>), ssss: list<multiway-tree<$420>>))
    Empck/heap/Emp: forall<a> multiway-tree<a> -> Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $420, [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a>)

// Add a value to a heap
pub inline fun insertck/heap/insert.1: forall<a> (h : pairing-heap<a>, v : a) -> pairing-heap<a>(hh: pairing-heap<$472>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, vv: $472: aa: V): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(hh: pairing-heap<$472>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>.insertck/heap/insert: forall<a> (t : multiway-tree<a>, v : a, comp : (a, a) -> order) -> multiway-tree<a>(vv: $472, hh: pairing-heap<$472>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order)), hh: pairing-heap<$472>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order))

// Return the minimum element of a heap
pub inline fun minck/heap/min: forall<a> (h : pairing-heap<a>) -> maybe<a>(hh: pairing-heap<$181>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): maybestd/core/types/maybe: V -> V<aa: V>
  match hh: pairing-heap<$181>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>
    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: $181, _) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(vv: $181)

fun meld-pairsck/heap/meld-pairs: forall<a> (ts : list<multiway-tree<a>>, comp : (a, a) -> order) -> multiway-tree<a>(tsts: list<multiway-tree<$326>>: liststd/core/list: V -> V<multiway-treeck/heap/multiway-tree: V -> V<aa: V>>, compcomp: ($326, $326) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): multiway-treeck/heap/multiway-tree: V -> V<aa: V>
  match tsts: list<multiway-tree<$326>>
    Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t1t1: multiway-tree<$326>, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t2t2: multiway-tree<$326>, ts'ts': list<multiway-tree<$326>>)) -> meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(t1t1: multiway-tree<$326>, t2t2: multiway-tree<$326>, compcomp: ($326, $326) -> order), ts'ts': list<multiway-tree<$326>>.meld-pairsck/heap/meld-pairs: forall<a> (ts : list<multiway-tree<a>>, comp : (a, a) -> order) -> multiway-tree<a>(compcomp: ($326, $326) -> order), compcomp: ($326, $326) -> order)
    [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a> -> Empck/heap/Emp: forall<a> multiway-tree<a>
    [tstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>]std/core/Nil: forall<a> list<a> -> tt: multiway-tree<$326>

// Remove the minimum element from a heap.
// Do nothing if the given heap is empty
pub inline fun erase-minck/heap/erase-min: forall<a> (h : pairing-heap<a>) -> pairing-heap<a>(hh: pairing-heap<$384>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
  match hh: pairing-heap<$384>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>
    Empck/heap/Emp: forall<a> multiway-tree<a> -> hh: pairing-heap<$384>
    Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(_, ssss: list<multiway-tree<$384>>) -> Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(ssss: list<multiway-tree<$384>>.meld-pairsck/heap/meld-pairs: forall<a> (ts : list<multiway-tree<a>>, comp : (a, a) -> order) -> multiway-tree<a>(hh: pairing-heap<$384>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order)), hh: pairing-heap<$384>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order))