A thunk based implementation of natural numbers in Java

Nat.java

package me.arrdem.ox;

import io.lacuna.bifurcan.IList;
import io.lacuna.bifurcan.Lists;
import kotlin.jvm.functions.Function0;
import org.jetbrains.annotations.NotNull;

import java.math.BigInteger;

public final class Nat implements Comparable<Nat> {
  private static IList<Function0<Nat>> FEL = (IList<Function0<Nat>>) Lists.EMPTY;

  private BigInteger value;
  private IList<Function0<Nat>> thunks;

  public static Nat ZERO = new Nat(BigInteger.ZERO, FEL);
  public static Nat ONE = new Nat(BigInteger.ONE, FEL);
  public static Nat TWO = new Nat(BigInteger.TWO, FEL);
  public static Nat TEN = new Nat(BigInteger.TEN, FEL);
  /**
   * FIXME (arrdem 2019-09-13)
   *   Is stepping by Long.MAX_VALUE reasonable here?
   */
  public static Nat INFINITY = new Nat(BigInteger.valueOf(Long.MAX_VALUE), FEL.addLast(() -> Nat.INFINITY));

  private Nat(BigInteger value, IList<Function0<Nat>> thunks) {
    assert value.compareTo(BigInteger.ZERO) >= 0;
    this.value = value;
    assert this.thunks != null;
    this.thunks = thunks;
  }

  public static Nat of(long value) {
    return new Nat(BigInteger.valueOf(value), Lists.EMPTY);
  }

  public static Nat of(BigInteger value) {
    return new Nat(value, Lists.EMPTY);
  }

  public static Nat of(long value, Function0<Nat> thunk) {
    return new Nat(BigInteger.valueOf(value), FEL.addLast(() -> {
      Object v = thunk.invoke();
      assert v instanceof Nat : "Contract violation! Thunk did not return nat!";
      return (Nat) v;
    }));
  }

  public static Nat of(BigInteger value, Function0<Nat> thunk) {
    return new Nat(value, FEL.addLast(() -> {
      Object v = thunk.invoke();
      assert v instanceof Nat : "Contract violation! Thunk did not return nat!";
      return (Nat) v;
    }));
  }

  public Nat succ() {
    return new Nat(BigInteger.ONE, FEL.addLast(() -> this));
  }

  public Nat add(int other) {
    if (other == 0) return this;
    else return new Nat(BigInteger.valueOf(other), FEL.addLast(() -> this));
  }

  public Nat add(long other) {
    return new Nat(BigInteger.valueOf(other), FEL.addLast(() -> this));
  }

  public Nat add(BigInteger other) {
    return new Nat(other, FEL.addLast(() -> this));
  }

  public Nat add(Nat other) {
    return new Nat(this.value.add(other.value), Lists.concat(this.thunks, other.thunks));
  }

  private boolean maybeStep() {
    if(this.thunks.size() > 0) {
      Function0<Nat> thunk = this.thunks.first();
      this.thunks = this.thunks.removeFirst();

      Nat next = thunk.invoke();
      if (next != null) {
        this.value = this.value.add(next.value);
        return true;
      }
    }
    return false;
  }

  public Nat decs() {
    return this.subtract(ONE);
  }

  public Nat subtract(int other) {
    return this.subtract(Nat.of(other));
  }

  public Nat subtract(long other) {
    return this.subtract(Nat.of(other));
  }

  public Nat subtract(BigInteger other) {
    return this.subtract(Nat.of(other));
  }

  /**
   * Subtraction is implemented by LAZILY evaluating both ths and other until either other has been
   * fully evaluated, or the subtrand has been reduced to zero.
   *
   * Note that this is LAZY subtraction, so it WILL loop given infinite structures.
   */
  public Nat subtract(Nat other) {
    while(true) {
      // If the other side is smaller and it can be stepped, step it.
      if(!other.thunks.equals(Lists.EMPTY) && other.value.compareTo(this.value) <= 0)
        other.maybeStep();

      // If our side is smaller and it can be stepped, step it
      else if (!this.thunks.equals(Lists.EMPTY) && this.value.compareTo(other.value) <= 0)
        this.maybeStep();

      // If we've grounded out and one side is fully evaluated, do the math.
      else if (this.thunks.equals(Lists.EMPTY) || other.thunks.equals(Lists.EMPTY)) {
        if (this.value.compareTo(other.value) > 0)
          return new Nat(this.value.subtract(other.value), this.thunks);
        else return ZERO;
      }
    }
  }

  public BigInteger get() {
    while(this.maybeStep()) {}
    return this.value;
  }

  /**
   *
   * @param other
   * @return -1 if this is less than other, 0 if equal, 1 if this is greater
   */
  @Override
  public int compareTo(@NotNull Nat other) {
    if(this == other || this.equals(other)) {
      return 0;
    }

    while(true) {
      // If the other side is smaller and it can be stepped, step it.
      if(!other.thunks.equals(Lists.EMPTY) && other.value.compareTo(this.value) <= 0)
        other.maybeStep();

      // If our side is smaller and it can be stepped, step it
      else if (!this.thunks.equals(Lists.EMPTY) && this.value.compareTo(other.value) <= 0)
        this.maybeStep();

      // We've exhausted this value, other has more AND is gt -> lt
      else if (this.thunks.equals(Lists.EMPTY) && !other.thunks.equals(Lists.EMPTY) && this.value.compareTo(other.value) < 0)
        return -1;

      // We've exhausted the other, and other's lt -> we're gt
      else if (!this.thunks.equals(Lists.EMPTY) && other.thunks.equals(Lists.EMPTY) && other.value.compareTo(this.value) < 0)
        return 1;

      // We've exhausted both
      return this.value.compareTo(other.value);
    }
  }

  public boolean equals(Object other) {
    if (this == other)
      return true;

    if (!(other instanceof Nat))
      return false;

    Nat o = (Nat) other;
    return this.compareTo(o) == 0;
  }

  public String toString() {
    return String.format("Nat<%s, more?=%s>", this.value.toString(10), !this.thunks.equals(Lists.EMPTY));
  }
}