Heap.cpp

#include <functional>
#include <iostream>
#include <memory>
#include <optional>
#include <variant>

template <typename T> struct Thunk {
  std::variant<T, std::function<T()>> contents;

  Thunk(const T &val) : contents{val} {}
  Thunk(std::function<T()> fn) : contents(fn) {}

  auto force() -> T & {
    struct visitor {
      Thunk &self;

      T &operator()(T &a) { return a; }
      T &operator()(std::function<T()> &a) {
        self.contents = {a()};
        return self.force();
      }
    };

    return std::visit(visitor{*this}, contents);
  }
};

struct HeapNode;
using OHeapNode = std::shared_ptr<HeapNode>;

struct HeapNode {
  int val;
  Thunk<OHeapNode> merged_children;
  OHeapNode odd;

  HeapNode(int a, Thunk<OHeapNode> b, OHeapNode c)
      : val(a), merged_children(b), odd(c) {}

  static auto make_empty() -> OHeapNode {
    return std::shared_ptr<HeapNode>(nullptr);
  }

  static auto make_singleton(int x) -> OHeapNode {
    return std::make_shared<HeapNode>(x, Thunk(make_empty()), make_empty());
  }

  static auto merge(OHeapNode left, OHeapNode right) -> OHeapNode {
    if (!left)
      return right;
    if (!right)
      return left;

    if (left->val < right->val) {
      return left->link(std::move(right));
    } else {
      return right->link(std::move(left));
    }
  }

  auto link(OHeapNode other) -> OHeapNode {
    if (!odd)
      return std::make_shared<HeapNode>(val, merged_children, other);

    return std::make_shared<HeapNode>(val, Thunk<OHeapNode>{[=]() {
                                        return merge(merge(odd, other),
                                                     merged_children.force());
                                      }},
                                      std::shared_ptr<HeapNode>(nullptr));
  }
};

struct Heap {
  OHeapNode root = nullptr;

  void insert(int x) {
    root = HeapNode::merge(root, HeapNode::make_singleton(x));
  }

  auto min() -> std::optional<int> {
    if (root)
      return {root->val};
    else
      return std::nullopt;
  }

  auto remove_min() {
    if (root) {
      root = HeapNode::merge(root->merged_children.force(), root->odd);
    }
  }
};

int main() {
  auto heap = Heap();

  heap.insert(3);
  heap.insert(5);
  heap.insert(2);

  std::cout << *heap.min() << '\n';
  heap.remove_min();
  std::cout << *heap.min() << '\n';
  heap.remove_min();
  auto w = heap;
  heap.insert(1);
  std::cout << *heap.min() << '\n';
  heap.remove_min();
  std::cout << *heap.min() << '\n';
  heap.remove_min();

  heap = std::move(w);
  std::cout << *heap.min() << '\n';
  heap.remove_min();
}

heap.lean

inductive Heap (a : Type)
  | empty
  | node (val : a) (merged_children : Thunk (Heap a)) (odd : Heap a)

syntax (priority := high) "??" term : term
macro_rules
  | `(?? $a) => `(Thunk.mk fun _ => $a)

mutual
  partial def Heap.merge [Ord a] : Heap a -> Heap a -> Heap a
    | .empty, r => r
    | l, .empty => l
    | l@(.node x _ _), r@(.node y _ _) =>
      match compare x y with
      | .lt => link l r
      | _ => link r l

  partial def link [Ord a] : Heap a -> Heap a -> Heap a
    | .empty, r => r
    | .node x m .empty, r => .node x m r
    | .node x m o, r => .node x (?? o.merge r |>.merge m.get) .empty
end

def Heap.min : Heap a -> Option a
  | .empty => none
  | .node x _ _ => x

def Heap.removeMin [Ord a] : Heap a -> Heap a
  | .empty => .empty
  | .node _ m o => m.get.merge o