Terms.java

package org.derive4j.exemple;

import java.lang.Boolean;
import java.lang.Integer;
import java.lang.Object;
import java.lang.Override;
import java.lang.String;
import java.lang.SuppressWarnings;
import java.util.Optional;
import java.util.function.Function;
import java.util.function.Supplier;

public final class Terms {
  @SuppressWarnings("rawtypes")
  private static final Term Zero = new Zero();

  private static final Term.Cases<Object, Optional<Term<Integer>>> predGetter = Terms.cases((id) -> Optional.empty(),
  (pred, id) -> Optional.of(pred),
  (succ, id) -> Optional.empty(),
  (a, id) -> Optional.empty(),
  (cond, then, otherwise) -> Optional.empty());

  private static final Term.Cases<Object, Optional<Term<Integer>>> succGetter = Terms.cases((id) -> Optional.empty(),
  (pred, id) -> Optional.empty(),
  (succ, id) -> Optional.of(succ),
  (a, id) -> Optional.empty(),
  (cond, then, otherwise) -> Optional.empty());

  private static final Term.Cases<Object, Optional<Term<Integer>>> aGetter = Terms.cases((id) -> Optional.empty(),
  (pred, id) -> Optional.empty(),
  (succ, id) -> Optional.empty(),
  (a, id) -> Optional.of(a),
  (cond, then, otherwise) -> Optional.empty());

  private static final Term.Cases<Object, Optional<Term<Boolean>>> condGetter = Terms.cases((id) -> Optional.empty(),
  (pred, id) -> Optional.empty(),
  (succ, id) -> Optional.empty(),
  (a, id) -> Optional.empty(),
  (cond, then, otherwise) -> Optional.of(cond));

  private static final Term.Cases<Object, Optional<Term<Object>>> thenGetter = Terms.cases((id) -> Optional.empty(),
  (pred, id) -> Optional.empty(),
  (succ, id) -> Optional.empty(),
  (a, id) -> Optional.empty(),
  (cond, then, otherwise) -> Optional.of(then));

  private static final Term.Cases<Object, Optional<Term<Object>>> otherwiseGetter = Terms.cases((id) -> Optional.empty(),
  (pred, id) -> Optional.empty(),
  (succ, id) -> Optional.empty(),
  (a, id) -> Optional.empty(),
  (cond, then, otherwise) -> Optional.of(otherwise));

  @SuppressWarnings("rawtypes")
  private static final TotalMatchBuilderZero<Object> totalMatchBuilderZero = new TotalMatchBuilderZero<Object>();

  private Terms() {
  }

  @SuppressWarnings("unchecked")
  public static Term<Integer> Zero() {
    return Zero;
  }

  public static Term<Integer> Succ(Term<Integer> pred) {
    return new Succ(pred);
  }

  public static Term<Integer> Pred(Term<Integer> succ) {
    return new Pred(succ);
  }

  public static Term<Boolean> IsZero(Term<Integer> a) {
    return new IsZero(a);
  }

  public static <T> Term<T> If(Term<Boolean> cond, Term<T> then, Term<T> otherwise) {
    return new If<>(cond, then, otherwise);
  }

  public static <T> Term<T> lazy(Supplier<Term<T>> term) {
    return new Lazy<>(term);
  }

  public static <T, X> Term.Cases<T, X> cases(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred, IsZeroMapper<T, X> IsZero, IfMapper<T, Term<T>, X> If) {
    return new LambdaCases<>(Zero, Succ, Pred, IsZero, If);
  }

  public static <T, X> Function<Term<T>, X> cata(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred, IsZeroMapper<T, X> IsZero, IfMapper<T, Supplier<X>, X> If) {
    Term.Cases<T, X> cata = new Object() {
      Term.Cases<T, X> cata = Terms.cases(
          Zero,
          Succ,
          Pred,
          IsZero,
          (cond, then, otherwise) -> If.If(cond, () -> then.match(this.cata), () -> otherwise.match(this.cata)));
      ;
    }.cata;
    return term -> term.match(cata);
  }

  @SuppressWarnings({"unchecked", "rawtypes"})
  public static <T> Optional<Term<Integer>> getPred(Term<T> term) {
    return (Optional<Term<Integer>>) term.match((Term.Cases) predGetter);
  }

  @SuppressWarnings({"unchecked", "rawtypes"})
  public static <T> Optional<Term<Integer>> getSucc(Term<T> term) {
    return (Optional<Term<Integer>>) term.match((Term.Cases) succGetter);
  }

  @SuppressWarnings({"unchecked", "rawtypes"})
  public static <T> Optional<Term<Integer>> getA(Term<T> term) {
    return (Optional<Term<Integer>>) term.match((Term.Cases) aGetter);
  }

  @SuppressWarnings({"unchecked", "rawtypes"})
  public static <T> Optional<Term<Boolean>> getCond(Term<T> term) {
    return (Optional<Term<Boolean>>) term.match((Term.Cases) condGetter);
  }

  @SuppressWarnings({"unchecked", "rawtypes"})
  public static <T> Optional<Term<T>> getThen(Term<T> term) {
    return (Optional<Term<T>>) term.match((Term.Cases) thenGetter);
  }

  @SuppressWarnings({"unchecked", "rawtypes"})
  public static <T> Optional<Term<T>> getOtherwise(Term<T> term) {
    return (Optional<Term<T>>) term.match((Term.Cases) otherwiseGetter);
  }

  public static <T> Function<Term<T>, Term<T>> setPred(Term<Integer> newPred) {
    return modPred(__ -> newPred);
  }

  @SuppressWarnings("unchecked")
  public static <T> Function<Term<T>, Term<T>> modPred(Function<Term<Integer>, Term<Integer>> predMod) {
    Term.Cases<T, Term<T>> cases = Terms.cases((id) -> (Term) Zero(),
        (pred, id) -> (Term) Succ(predMod.apply(pred)),
        (succ, id) -> (Term) Pred(succ),
        (a, id) -> (Term) IsZero(a),
        (cond, then, otherwise) -> If(cond, then, otherwise));
    return term -> term.match(cases);
  }

  public static <T> Function<Term<T>, Term<T>> setSucc(Term<Integer> newSucc) {
    return modSucc(__ -> newSucc);
  }

  @SuppressWarnings("unchecked")
  public static <T> Function<Term<T>, Term<T>> modSucc(Function<Term<Integer>, Term<Integer>> succMod) {
    Term.Cases<T, Term<T>> cases = Terms.cases((id) -> (Term) Zero(),
        (pred, id) -> (Term) Succ(pred),
        (succ, id) -> (Term) Pred(succMod.apply(succ)),
        (a, id) -> (Term) IsZero(a),
        (cond, then, otherwise) -> If(cond, then, otherwise));
    return term -> term.match(cases);
  }

  public static <T> Function<Term<T>, Term<T>> setA(Term<Integer> newA) {
    return modA(__ -> newA);
  }

  @SuppressWarnings("unchecked")
  public static <T> Function<Term<T>, Term<T>> modA(Function<Term<Integer>, Term<Integer>> aMod) {
    Term.Cases<T, Term<T>> cases = Terms.cases((id) -> (Term) Zero(),
        (pred, id) -> (Term) Succ(pred),
        (succ, id) -> (Term) Pred(succ),
        (a, id) -> (Term) IsZero(aMod.apply(a)),
        (cond, then, otherwise) -> If(cond, then, otherwise));
    return term -> term.match(cases);
  }

  public static <T> Function<Term<T>, Term<T>> setCond(Term<Boolean> newCond) {
    return modCond(__ -> newCond);
  }

  @SuppressWarnings("unchecked")
  public static <T> Function<Term<T>, Term<T>> modCond(Function<Term<Boolean>, Term<Boolean>> condMod) {
    Term.Cases<T, Term<T>> cases = Terms.cases((id) -> (Term) Zero(),
        (pred, id) -> (Term) Succ(pred),
        (succ, id) -> (Term) Pred(succ),
        (a, id) -> (Term) IsZero(a),
        (cond, then, otherwise) -> If(condMod.apply(cond), then, otherwise));
    return term -> term.match(cases);
  }

  public static <T> Function<Term<T>, Term<T>> setThen(Term<T> newThen) {
    return modThen(__ -> newThen);
  }

  @SuppressWarnings("unchecked")
  public static <T> Function<Term<T>, Term<T>> modThen(Function<Term<T>, Term<T>> thenMod) {
    Term.Cases<T, Term<T>> cases = Terms.cases((id) -> (Term) Zero(),
        (pred, id) -> (Term) Succ(pred),
        (succ, id) -> (Term) Pred(succ),
        (a, id) -> (Term) IsZero(a),
        (cond, then, otherwise) -> If(cond, thenMod.apply(then), otherwise));
    return term -> term.match(cases);
  }

  public static <T> Function<Term<T>, Term<T>> setOtherwise(Term<T> newOtherwise) {
    return modOtherwise(__ -> newOtherwise);
  }

  @SuppressWarnings("unchecked")
  public static <T> Function<Term<T>, Term<T>> modOtherwise(Function<Term<T>, Term<T>> otherwiseMod) {
    Term.Cases<T, Term<T>> cases = Terms.cases((id) -> (Term) Zero(),
        (pred, id) -> (Term) Succ(pred),
        (succ, id) -> (Term) Pred(succ),
        (a, id) -> (Term) IsZero(a),
        (cond, then, otherwise) -> If(cond, then, otherwiseMod.apply(otherwise)));
    return term -> term.match(cases);
  }

  @SuppressWarnings("unchecked")
  public static <T> TotalMatchBuilderZero<T> cases() {
    return (TotalMatchBuilderZero<T>) totalMatchBuilderZero;
  }

  private static final class Zero extends Term<Integer> {
    Zero() {
    }

    @Override
    public <X> X match(Term.Cases<Integer, X> cases) {
      return cases.Zero(t -> t);
    }

    @Override
    @SuppressWarnings("unchecked")
    public boolean equals(Object obj) {
      return (obj instanceof Term) && ((Term<Integer>) obj).match(Terms.cases((id) -> true,
          (pred, id) -> false,
          (succ, id) -> false,
          (a, id) -> false,
          (cond, then, otherwise) -> false));
    }

    @Override
    public int hashCode() {
      return 23;
    }

    @Override
    public String toString() {
      return "Zero()";
    }
  }

  private static final class Succ extends Term<Integer> {
    private final Term<Integer> pred;

    Succ(Term<Integer> pred) {
      this.pred = pred;
    }

    @Override
    public <X> X match(Term.Cases<Integer, X> cases) {
      return cases.Succ(this.pred, t -> t);
    }

    @Override
    @SuppressWarnings("unchecked")
    public boolean equals(Object obj) {
      return (obj instanceof Term) && ((Term<Integer>) obj).match(Terms.cases((id) -> false,
          (pred, id) -> this.pred.equals(pred),
          (succ, id) -> false,
          (a, id) -> false,
          (cond, then, otherwise) -> false));
    }

    @Override
    public int hashCode() {
      return 29 + this.pred.hashCode();
    }

    @Override
    public String toString() {
      return "Succ(" + this.pred + ")";
    }
  }

  private static final class Pred extends Term<Integer> {
    private final Term<Integer> succ;

    Pred(Term<Integer> succ) {
      this.succ = succ;
    }

    @Override
    public <X> X match(Term.Cases<Integer, X> cases) {
      return cases.Pred(this.succ, t -> t);
    }

    @Override
    @SuppressWarnings("unchecked")
    public boolean equals(Object obj) {
      return (obj instanceof Term) && ((Term<Integer>) obj).match(Terms.cases((id) -> false,
          (pred, id) -> false,
          (succ, id) -> this.succ.equals(succ),
          (a, id) -> false,
          (cond, then, otherwise) -> false));
    }

    @Override
    public int hashCode() {
      return 31 + this.succ.hashCode();
    }

    @Override
    public String toString() {
      return "Pred(" + this.succ + ")";
    }
  }

  private static final class IsZero extends Term<Boolean> {
    private final Term<Integer> a;

    IsZero(Term<Integer> a) {
      this.a = a;
    }

    @Override
    public <X> X match(Term.Cases<Boolean, X> cases) {
      return cases.IsZero(this.a, t -> t);
    }

    @Override
    @SuppressWarnings("unchecked")
    public boolean equals(Object obj) {
      return (obj instanceof Term) && ((Term<Boolean>) obj).match(Terms.cases((id) -> false,
          (pred, id) -> false,
          (succ, id) -> false,
          (a, id) -> this.a.equals(a),
          (cond, then, otherwise) -> false));
    }

    @Override
    public int hashCode() {
      return 37 + this.a.hashCode();
    }

    @Override
    public String toString() {
      return "IsZero(" + this.a + ")";
    }
  }

  private static final class If<T> extends Term<T> {
    private final Term<Boolean> cond;

    private final Term<T> then;

    private final Term<T> otherwise;

    If(Term<Boolean> cond, Term<T> then, Term<T> otherwise) {
      this.cond = cond;
      this.then = then;
      this.otherwise = otherwise;
    }

    @Override
    public <X> X match(Term.Cases<T, X> cases) {
      return cases.If(this.cond, this.then, this.otherwise);
    }

    @Override
    @SuppressWarnings("unchecked")
    public boolean equals(Object obj) {
      return (obj instanceof Term) && ((Term<T>) obj).match(Terms.cases((id) -> false,
          (pred, id) -> false,
          (succ, id) -> false,
          (a, id) -> false,
          (cond, then, otherwise) -> this.cond.equals(cond) && this.then.equals(then) && this.otherwise.equals(otherwise)));
    }

    @Override
    public int hashCode() {
      return ((41 + this.cond.hashCode()) * 41 + this.then.hashCode()) * 41 + this.otherwise.hashCode();
    }

    @Override
    public String toString() {
      return "If(" + this.cond + ", " + this.then + ", " + this.otherwise + ")";
    }
  }

  private static final class Lazy<T> extends Term<T> {
    private final Object lock = new Object();

    private Supplier<Term<T>> expression;

    private volatile Term<T> evaluation;

    Lazy(Supplier<Term<T>> term) {
      this.expression = term;
    }

    private Term<T> eval() {
      Term<T> _evaluation = this.evaluation;
      if (_evaluation == null) {
        synchronized (this.lock) {
          _evaluation = this.evaluation;
          if (_evaluation == null) {
            this.evaluation = _evaluation = expression.get();
            this.expression = null;
          }
        }
      }
      return _evaluation;
    }

    @Override
    public <X> X match(Term.Cases<T, X> cases) {
      return this.eval().match(cases);
    }

    @Override
    public boolean equals(Object obj) {
      return this.eval().equals(obj);
    }

    @Override
    public int hashCode() {
      return this.eval().hashCode();
    }

    @Override
    public String toString() {
      return this.eval().toString();
    }
  }

  public interface SuccMapper<T, X> {
    X Succ(Term<Integer> pred, Term.F<Integer, T> id);
  }

  public interface PredMapper<T, X> {
    X Pred(Term<Integer> succ, Term.F<Integer, T> id);
  }

  public interface IsZeroMapper<T, X> {
    X IsZero(Term<Integer> a, Term.F<Boolean, T> id);
  }

  public interface IfMapper<T, R, X> {
    X If(Term<Boolean> cond, R then, R otherwise);
  }

  private static final class LambdaCases<T, X> implements Term.Cases<T, X> {
    private final Function<Term.F<Integer, T>, X> Zero;

    private final SuccMapper<T, X> Succ;

    private final PredMapper<T, X> Pred;

    private final IsZeroMapper<T, X> IsZero;

    private final IfMapper<T, Term<T>, X> If;

    LambdaCases(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred, IsZeroMapper<T, X> IsZero, IfMapper<T, Term<T>, X> If) {
      this.Zero = Zero;
      this.Succ = Succ;
      this.Pred = Pred;
      this.IsZero = IsZero;
      this.If = If;
    }

    @Override
    public X Zero(Term.F<Integer, T> id) {
      return this.Zero.apply(id);
    }

    @Override
    public X Succ(Term<Integer> pred, Term.F<Integer, T> id) {
      return this.Succ.Succ(pred, id);
    }

    @Override
    public X Pred(Term<Integer> succ, Term.F<Integer, T> id) {
      return this.Pred.Pred(succ, id);
    }

    @Override
    public X IsZero(Term<Integer> a, Term.F<Boolean, T> id) {
      return this.IsZero.IsZero(a, id);
    }

    @Override
    public X If(Term<Boolean> cond, Term<T> then, Term<T> otherwise) {
      return this.If.If(cond, then, otherwise);
    }
  }

  public static final class TotalMatchBuilderZero<T> {
    private TotalMatchBuilderZero() {
    }

    public final <X> TotalMatchBuilderSucc<T, X> Zero(Function<Term.F<Integer, T>, X> Zero) {
      return new TotalMatchBuilderSucc<>(Zero);
    }

    public final <X> TotalMatchBuilderSucc<T, X> Zero(X x) {
      return this.Zero((id) -> x);
    }

    public final <X> PartialMatchBuilderPred<T, X> Succ(SuccMapper<T, X> Succ) {
      return new PartialMatchBuilderPred<>(null, Succ);
    }

    public final <X> PartialMatchBuilderPred<T, X> Succ(X x) {
      return this.Succ((pred, id) -> x);
    }

    public final <X> PartialMatchBuilderIsZero<T, X> Pred(PredMapper<T, X> Pred) {
      return new PartialMatchBuilderIsZero<>(null, null, Pred);
    }

    public final <X> PartialMatchBuilderIsZero<T, X> Pred(X x) {
      return this.Pred((succ, id) -> x);
    }

    public final <X> PartialMatchBuilderIf<T, X> IsZero(IsZeroMapper<T, X> IsZero) {
      return new PartialMatchBuilderIf<>(null, null, null, IsZero);
    }

    public final <X> PartialMatchBuilderIf<T, X> IsZero(X x) {
      return this.IsZero((a, id) -> x);
    }

    public final <X> PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(null, null, null, null, If);
    }

    public final <X> PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static final class TotalMatchBuilderSucc<T, X> extends PartialMatchBuilder<T, X> {
    private TotalMatchBuilderSucc(Function<Term.F<Integer, T>, X> Zero) {
      super(Zero, null, null, null, null);
    }

    public final TotalMatchBuilderPred<T, X> Succ(SuccMapper<T, X> Succ) {
      return new TotalMatchBuilderPred<>(super.Zero, Succ);
    }

    public final TotalMatchBuilderPred<T, X> Succ(X x) {
      return this.Succ((pred, id) -> x);
    }

    public final PartialMatchBuilderIsZero<T, X> Pred(PredMapper<T, X> Pred) {
      return new PartialMatchBuilderIsZero<>(super.Zero, null, Pred);
    }

    public final PartialMatchBuilderIsZero<T, X> Pred(X x) {
      return this.Pred((succ, id) -> x);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(IsZeroMapper<T, X> IsZero) {
      return new PartialMatchBuilderIf<>(super.Zero, null, null, IsZero);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(X x) {
      return this.IsZero((a, id) -> x);
    }

    public final PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(super.Zero, null, null, null, If);
    }

    public final PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static final class TotalMatchBuilderPred<T, X> extends PartialMatchBuilder<T, X> {
    private TotalMatchBuilderPred(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ) {
      super(Zero, Succ, null, null, null);
    }

    public final TotalMatchBuilderIsZero<T, X> Pred(PredMapper<T, X> Pred) {
      return new TotalMatchBuilderIsZero<>(super.Zero, super.Succ, Pred);
    }

    public final TotalMatchBuilderIsZero<T, X> Pred(X x) {
      return this.Pred((succ, id) -> x);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(IsZeroMapper<T, X> IsZero) {
      return new PartialMatchBuilderIf<>(super.Zero, super.Succ, null, IsZero);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(X x) {
      return this.IsZero((a, id) -> x);
    }

    public final PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(super.Zero, super.Succ, null, null, If);
    }

    public final PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static final class TotalMatchBuilderIsZero<T, X> extends PartialMatchBuilder<T, X> {
    private TotalMatchBuilderIsZero(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred) {
      super(Zero, Succ, Pred, null, null);
    }

    public final TotalMatchBuilderIf<T, X> IsZero(IsZeroMapper<T, X> IsZero) {
      return new TotalMatchBuilderIf<>(super.Zero, super.Succ, super.Pred, IsZero);
    }

    public final TotalMatchBuilderIf<T, X> IsZero(X x) {
      return this.IsZero((a, id) -> x);
    }

    public final PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(super.Zero, super.Succ, super.Pred, null, If);
    }

    public final PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static final class TotalMatchBuilderIf<T, X> extends PartialMatchBuilder<T, X> {
    private TotalMatchBuilderIf(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred, IsZeroMapper<T, X> IsZero) {
      super(Zero, Succ, Pred, IsZero, null);
    }

    public final Function<Term<T>, X> If(IfMapper<T, Term<T>, X> If) {
      Term.Cases<T, X> cases = Terms.cases(super.Zero, super.Succ, super.Pred, super.IsZero, If);
      return term -> term.match(cases);
    }

    public final Function<Term<T>, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static class PartialMatchBuilderSucc<T, X> extends PartialMatchBuilder<T, X> {
    private PartialMatchBuilderSucc(Function<Term.F<Integer, T>, X> Zero) {
      super(Zero, null, null, null, null);
    }

    public final PartialMatchBuilderPred<T, X> Succ(SuccMapper<T, X> Succ) {
      return new PartialMatchBuilderPred<>(super.Zero, Succ);
    }

    public final PartialMatchBuilderPred<T, X> Succ(X x) {
      return this.Succ((pred, id) -> x);
    }

    public final PartialMatchBuilderIsZero<T, X> Pred(PredMapper<T, X> Pred) {
      return new PartialMatchBuilderIsZero<>(super.Zero, null, Pred);
    }

    public final PartialMatchBuilderIsZero<T, X> Pred(X x) {
      return this.Pred((succ, id) -> x);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(IsZeroMapper<T, X> IsZero) {
      return new PartialMatchBuilderIf<>(super.Zero, null, null, IsZero);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(X x) {
      return this.IsZero((a, id) -> x);
    }

    public final PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(super.Zero, null, null, null, If);
    }

    public final PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static class PartialMatchBuilderPred<T, X> extends PartialMatchBuilder<T, X> {
    private PartialMatchBuilderPred(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ) {
      super(Zero, Succ, null, null, null);
    }

    public final PartialMatchBuilderIsZero<T, X> Pred(PredMapper<T, X> Pred) {
      return new PartialMatchBuilderIsZero<>(super.Zero, super.Succ, Pred);
    }

    public final PartialMatchBuilderIsZero<T, X> Pred(X x) {
      return this.Pred((succ, id) -> x);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(IsZeroMapper<T, X> IsZero) {
      return new PartialMatchBuilderIf<>(super.Zero, super.Succ, null, IsZero);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(X x) {
      return this.IsZero((a, id) -> x);
    }

    public final PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(super.Zero, super.Succ, null, null, If);
    }

    public final PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static class PartialMatchBuilderIsZero<T, X> extends PartialMatchBuilder<T, X> {
    private PartialMatchBuilderIsZero(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred) {
      super(Zero, Succ, Pred, null, null);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(IsZeroMapper<T, X> IsZero) {
      return new PartialMatchBuilderIf<>(super.Zero, super.Succ, super.Pred, IsZero);
    }

    public final PartialMatchBuilderIf<T, X> IsZero(X x) {
      return this.IsZero((a, id) -> x);
    }

    public final PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(super.Zero, super.Succ, super.Pred, null, If);
    }

    public final PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static class PartialMatchBuilderIf<T, X> extends PartialMatchBuilder<T, X> {
    private PartialMatchBuilderIf(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred, IsZeroMapper<T, X> IsZero) {
      super(Zero, Succ, Pred, IsZero, null);
    }

    public final PartialMatchBuilder<T, X> If(IfMapper<T, Term<T>, X> If) {
      return new PartialMatchBuilder<>(super.Zero, super.Succ, super.Pred, super.IsZero, If);
    }

    public final PartialMatchBuilder<T, X> If(X x) {
      return this.If((cond, then, otherwise) -> x);
    }
  }

  public static class PartialMatchBuilder<T, X> {
    private final Function<Term.F<Integer, T>, X> Zero;

    private final SuccMapper<T, X> Succ;

    private final PredMapper<T, X> Pred;

    private final IsZeroMapper<T, X> IsZero;

    private final IfMapper<T, Term<T>, X> If;

    private PartialMatchBuilder(Function<Term.F<Integer, T>, X> Zero, SuccMapper<T, X> Succ, PredMapper<T, X> Pred, IsZeroMapper<T, X> IsZero, IfMapper<T, Term<T>, X> If) {
      this.Zero = Zero;
      this.Succ = Succ;
      this.Pred = Pred;
      this.IsZero = IsZero;
      this.If = If;
    }

    public final Function<Term<T>, X> otherwise(Supplier<X> otherwise) {
      Term.Cases<T, X> cases = Terms.cases(this.Zero != null ? this.Zero : (id) -> otherwise.get(),
          this.Succ != null ? this.Succ : (pred, id) -> otherwise.get(),
          this.Pred != null ? this.Pred : (succ, id) -> otherwise.get(),
          this.IsZero != null ? this.IsZero : (a, id) -> otherwise.get(),
          this.If != null ? this.If : (cond, then, otherwise_) -> otherwise.get());
      return term -> term.match(cases);
    }

    public final Function<Term<T>, X> otherwise(X x) {
      return this.otherwise(() -> x);
    }

    public final Function<Term<T>, Optional<X>> otherwiseEmpty() {
      Term.Cases<T, Optional<X>> cases = Terms.cases((this.Zero != null) ? (id) -> Optional.of(this.Zero.apply(id))
          : (id) -> Optional.empty(),
          (this.Succ != null) ? (pred, id) -> Optional.of(this.Succ.Succ(pred, id))
          : (pred, id) -> Optional.empty(),
          (this.Pred != null) ? (succ, id) -> Optional.of(this.Pred.Pred(succ, id))
          : (succ, id) -> Optional.empty(),
          (this.IsZero != null) ? (a, id) -> Optional.of(this.IsZero.IsZero(a, id))
          : (a, id) -> Optional.empty(),
          (this.If != null) ? (cond, then, otherwise) -> Optional.of(this.If.If(cond, then, otherwise))
          : (cond, then, otherwise) -> Optional.empty());
      return term -> term.match(cases);
    }
  }
}