From 5bdce6336afe1c92a70f6e54ceabf110fac9d2a6 Mon Sep 17 00:00:00 2001
From: Matthias Hetzenberger <mhetzenberger@gmail.com>
Date: Fri, 10 Oct 2025 16:43:05 +0200
Subject: [PATCH 1/6] Implement ToPlaceholders to replace higher-order subterms
 with a placeholder constant

# Conflicts:
#	Kernel/HOL/Create.cpp
#	Kernel/HOL/HOL.hpp
---
 Kernel/HOL/Convert.cpp                        | 10 +---
 Kernel/HOL/Create.cpp                         | 30 +++++++++++
 Kernel/HOL/HOL.cpp                            |  5 ++
 Kernel/HOL/HOL.hpp                            | 19 ++++---
 Kernel/HOL/ToPlaceholders.cpp                 | 50 +++++++++++++++++++
 Kernel/HOL/ToPlaceholders.hpp                 | 49 ++++++++++++++++++
 Kernel/Signature.cpp                          | 13 +++--
 Kernel/Signature.hpp                          |  4 +-
 Kernel/Term.cpp                               | 42 +++++++++-------
 Kernel/Term.hpp                               | 17 ++++---
 Test/HOLUtils.cpp                             |  7 +--
 Test/HOLUtils.hpp                             |  2 +-
 ...taReduction.cpp => tHOL_BetaReduction.cpp} |  0
 ...EtaReduction.cpp => tHOL_EtaReduction.cpp} |  2 +-
 UnitTests/HOL/tHOL_Printing.cpp               | 23 +++++++++
 ...mReplacer.cpp => tHOL_SubtermReplacer.cpp} |  0
 ...{tTermShifter.cpp => tHOL_TermShifter.cpp} |  0
 UnitTests/HOL/tHOL_ToPlaceholders.cpp         | 26 ++++++++++
 cmake/sources.cmake                           | 11 ++--
 19 files changed, 250 insertions(+), 60 deletions(-)
 create mode 100644 Kernel/HOL/ToPlaceholders.cpp
 create mode 100644 Kernel/HOL/ToPlaceholders.hpp
 rename UnitTests/HOL/{tBetaReduction.cpp => tHOL_BetaReduction.cpp} (100%)
 rename UnitTests/HOL/{tEtaReduction.cpp => tHOL_EtaReduction.cpp} (97%)
 rename UnitTests/HOL/{tSubtermReplacer.cpp => tHOL_SubtermReplacer.cpp} (100%)
 rename UnitTests/HOL/{tTermShifter.cpp => tHOL_TermShifter.cpp} (100%)
 create mode 100644 UnitTests/HOL/tHOL_ToPlaceholders.cpp

diff --git a/Kernel/HOL/Convert.cpp b/Kernel/HOL/Convert.cpp
index 0f4d32f42..ec9f4a580 100644
--- a/Kernel/HOL/Convert.cpp
+++ b/Kernel/HOL/Convert.cpp
@@ -20,12 +20,6 @@
 using IndexSortPair = std::pair<int, TermList>;
 using VarToIndexMap = std::unordered_map<unsigned, IndexSortPair>;
 
-static TermList sortOf(TermList t) {
-  ASS(t.isTerm())
-
-  return SortHelper::getResultSort(t.term());
-}
-
 static TermList termToNameless(TermList term, const VarToIndexMap& map);
 static TermList formulaToNameless(Formula *formula, const VarToIndexMap& map);
 
@@ -40,7 +34,7 @@ static TermList toNamelessAux(VList* vars, SList* sorts, TermList body, TermList
     vars->tail() == nullptr ? termToNameless(body, newMap)
                             : toNamelessAux(vars->tail(), sorts->tail(), body, bodySort, newMap);
 
-  bodySort = converted.isVar() ? bodySort : sortOf(converted);
+  bodySort = converted.isVar() ? bodySort : converted.resultSort();
   return HOL::create::namelessLambda(sorts->head(), bodySort, converted);
 }
 
@@ -68,7 +62,7 @@ static TermList termToNameless(TermList term, const VarToIndexMap& map) {
         const auto vars = sd->getLambdaVars();
 
         const auto eliminated = toNamelessAux(vars, sorts, sd->getLambdaExp(), sd->getLambdaExpSort(), map);
-        ASS_REP2(eliminated.isVar() || sortOf(eliminated) == sd->getSort(), t->toString(), eliminated.toString())
+        ASS_REP2(eliminated.isVar() || eliminated.resultSort() == sd->getSort(), t->toString(), eliminated.toString())
         return eliminated;
       }
 
diff --git a/Kernel/HOL/Create.cpp b/Kernel/HOL/Create.cpp
index 7be33b0d3..a201abdc2 100644
--- a/Kernel/HOL/Create.cpp
+++ b/Kernel/HOL/Create.cpp
@@ -62,6 +62,36 @@ TermList HOL::create::app(TermList head, const TermStack& terms) {
   return app(SortHelper::getResultSort(head.term()), head, terms);
 }
 
+TermList HOL::create::equality(TermList sort) {
+  static const auto eqProxy = env.signature->getEqualityProxy();
+
+  return TermList(Term::create1(eqProxy, sort));
+}
+
+TermList HOL::create::neg() {
+  static const auto term = TermList(Term::createConstant(env.signature->getNotProxy()));
+
+  return term;
+}
+
+TermList HOL::create::pi(TermList sort) {
+  static const auto piProxy = env.signature->getPiSigmaProxy("vPI");
+
+  return TermList(Term::create1(piProxy, sort));
+}
+
+TermList HOL::create::sigma(TermList sort) {
+  static const auto sigmaProxy = env.signature->getPiSigmaProxy("vSIGMA");
+
+  return TermList(Term::create1(sigmaProxy, sort));
+}
+
+TermList HOL::create::placeholder(TermList sort) {
+  static const auto placeholder = env.signature->getPlaceholder();
+
+  return TermList(Term::create1(placeholder, sort));
+}
+
 Term* HOL::create::lambda(unsigned numArgs, const unsigned* vars, const TermList* varSorts, TypedTermList body, TermList* resultExprSort) {
   auto s = new (0, sizeof(Term::SpecialTermData)) Term;
   s->makeSymbol(Term::toNormalFunctor(SpecialFunctor::LAMBDA), 0);
diff --git a/Kernel/HOL/HOL.cpp b/Kernel/HOL/HOL.cpp
index f9ce3f66f..5a18366e8 100644
--- a/Kernel/HOL/HOL.cpp
+++ b/Kernel/HOL/HOL.cpp
@@ -13,6 +13,7 @@
 
 #include "Kernel/HOL/HOL.hpp"
 
+#include "ToPlaceholders.hpp"
 #include "Kernel/Formula.hpp"
 
 using IndexVarStack = Stack<std::pair<unsigned, unsigned>>;
@@ -371,4 +372,8 @@ void HOL::getMatrixAndPrefSorts(TermList t, TermList& matrix, TermStack& sorts)
     t = t.lambdaBody();
   }
   matrix = t;
+}
+
+TermList HOL::toPlaceholders(TermList term) {
+  return ToPlaceholders().replace(term);
 }
\ No newline at end of file
diff --git a/Kernel/HOL/HOL.hpp b/Kernel/HOL/HOL.hpp
index 240262064..0c05630a4 100644
--- a/Kernel/HOL/HOL.hpp
+++ b/Kernel/HOL/HOL.hpp
@@ -24,7 +24,7 @@
 namespace HOL {
 
 using Kernel::Term;
-
+  
 inline bool isTrue(TermList term) {
   return term.isTerm() && env.signature->isFoolConstantSymbol(true, term.term()->functor());
 }
@@ -62,13 +62,15 @@ inline bool canHeadReduce(const TermList& head, const TermStack& args) {
   return head.isLambdaTerm() && args.isNonEmpty();
 }
 
+TermList toPlaceholders(TermList term);
+
 } // namespace HOL
 
 namespace HOL::create {
   TermList app(TermList sort, TermList head, TermList arg);
   TermList app(TermList head, TermList arg);
   TermList app(TermList s1, TermList s2, TermList arg1, TermList arg2, bool shared = true);
-  TermList app(TermList sort, TermList head, const TermStack& terms); // todo const termstack
+  TermList app(TermList sort, TermList head, const TermStack& terms);
   TermList app(TermList head, const TermStack& terms);
 
   inline TermList app2(TermList sort, TermList head, TermList arg1, TermList arg2) {
@@ -78,13 +80,14 @@ namespace HOL::create {
   inline TermList app2(TermList head, TermList arg1, TermList arg2) {
     ASS(head.isTerm())
 
-    return app2(Kernel::SortHelper::getResultSort(head.term()), head, arg1, arg2);
+    return app2(head.resultSort(), head, arg1, arg2);
   }
 
-  inline TermList equality(TermList sort) { return TermList(Term::create1(env.signature->getEqualityProxy(), sort)); }
-  inline TermList neg() { return TermList(Term::createConstant(env.signature->getNotProxy())); }
-  inline TermList pi(TermList sort) { return TermList(Term::create1(env.signature->getPiSigmaProxy("vPI"), sort)); }
-  inline TermList sigma(TermList sort) { return TermList(Term::create1(env.signature->getPiSigmaProxy("vSIGMA"), sort)); }
+  TermList equality(TermList sort);
+  TermList neg();
+  TermList pi(TermList sort);
+  TermList sigma(TermList sort);
+  TermList placeholder(TermList sort);
 
   Term* lambda(unsigned numArgs, const unsigned* vars, const TermList* varSorts, TypedTermList body, TermList* resultExprSort = nullptr);
 
@@ -93,6 +96,8 @@ namespace HOL::create {
 
   TermList surroundWithLambdas(TermList t, TermStack& sorts, bool fromTop = false);
   TermList surroundWithLambdas(TermList t, TermStack& sorts, TermList sort, bool fromTop = false);
+
+  TermList placeholder(TermList sort);
 } // namespace HOL::create
 
 namespace HOL::convert {
diff --git a/Kernel/HOL/ToPlaceholders.cpp b/Kernel/HOL/ToPlaceholders.cpp
new file mode 100644
index 000000000..a544fef02
--- /dev/null
+++ b/Kernel/HOL/ToPlaceholders.cpp
@@ -0,0 +1,50 @@
+ /*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+/**
+ * @file ToPlaceholders.cpp
+ */
+
+#include "Kernel/HOL/ToPlaceholders.hpp"
+#include "Kernel/HOL/HOL.hpp"
+
+ToPlaceholders::ToPlaceholders()
+      : TermTransformer(false),
+        _nextIsPrefix(false),
+        _topLevel(true),
+        _mode(env.options->functionExtensionality()) {}
+
+TermList ToPlaceholders::replace(TermList term) {
+  TermList transformed = transformSubterm(term);
+
+  if (transformed != term)
+    return transformed;
+
+  _topLevel = false;
+  return transform(term);
+}
+
+TermList ToPlaceholders::transformSubterm(TermList t) {
+  if (_nextIsPrefix || t.isVar())
+    return t;
+
+  // Not expecting any unreduced redexes here
+  ASS(!t.head().isLambdaTerm())
+
+  auto sort = SortHelper::getResultSort(t.term());
+  if (t.isLambdaTerm() || t.head().isVar())
+    return HOL::create::placeholder(sort);
+
+  if (_mode == Options::FunctionExtensionality::ABSTRACTION) {
+    if (sort.isArrowSort() || sort.isVar() || (sort.isBoolSort() && !_topLevel)) {
+      return HOL::create::placeholder(sort);
+    }
+  }
+  return t;
+}
diff --git a/Kernel/HOL/ToPlaceholders.hpp b/Kernel/HOL/ToPlaceholders.hpp
new file mode 100644
index 000000000..7a5ca3629
--- /dev/null
+++ b/Kernel/HOL/ToPlaceholders.hpp
@@ -0,0 +1,49 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+/**
+ * @file ToPlaceholders.hpp
+ */
+
+#ifndef __ToPlaceholders__
+#define __ToPlaceholders__
+
+
+#include "Kernel/TermTransformer.hpp"
+#include "Shell/Options.hpp"
+
+using namespace Kernel;
+
+// replaces higher-order subterms (subterms with variable heads e.g., X a b &
+// lambda terms) with a special polymorphic constant we call a "placeholder".
+// Depending on the mode functional and Boolean subterms may also be replaced
+class ToPlaceholders : public TermTransformer
+{
+public:
+  ToPlaceholders();
+
+  TermList replace(TermList term);
+  TermList transformSubterm(TermList t) override;
+
+  void onTermEntry(Term* t) override {
+    if (t->isApplication())
+      _nextIsPrefix = true;
+  }
+
+  void onTermExit(Term* t) override {
+    _nextIsPrefix = false;
+  }
+
+private:
+  bool _nextIsPrefix;
+  bool _topLevel;
+  Shell::Options::FunctionExtensionality _mode;
+};
+
+#endif // __ToPlaceholders__
diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
index a23e966a8..570cbde6a 100644
--- a/Kernel/Signature.cpp
+++ b/Kernel/Signature.cpp
@@ -583,7 +583,7 @@ unsigned Signature::getDiff() {
     auto alpha = TermList(0, false);
     auto beta = TermList(1, false);
     auto alphaBeta = AtomicSort::arrowSort(alpha, beta);
-    auto result = AtomicSort::arrowSort(alphaBeta, alphaBeta, alpha);
+    auto result = AtomicSort::arrowSort({alphaBeta, alphaBeta, alpha});
     auto sym = getFunction(diff);
     sym->setType(OperatorType::getConstantsType(result, 2));
   }
@@ -654,12 +654,13 @@ unsigned Signature::getChoice() {
 }
 
 unsigned Signature::getDeBruijnIndex(int index) {
+  ASS(index >= 0)
+
   bool added = false;
   unsigned fun = addFunction("db" + Int::toString(index), 1, added);
   if (added) {
-    auto alpha = TermList(0, false);
     auto sym = getFunction(fun);
-    sym->setType(OperatorType::getConstantsType(alpha, 1));
+    sym->setType(OperatorType::getConstantsType(TermList::var(0), 1));
     sym->setDeBruijnIndex(index);
   }
   return fun;
@@ -669,11 +670,9 @@ unsigned Signature::getPlaceholder() {
   if (_placeholderFun != UINT_MAX)
     return _placeholderFun;
 
-  unsigned fun = addFreshFunction(1,"ph");
+  unsigned fun = addFreshFunction(1, "ph");
   _placeholderFun = fun;
-  auto alpha = TermList(0, false);
-  auto sym = getFunction(fun);
-  sym->setType(OperatorType::getConstantsType(alpha, 1));
+  getFunction(fun)->setType(OperatorType::getConstantsType(TermList::var(0), 1));
   return fun;
 }
 
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index 66c67f4a7..264c491a9 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -915,7 +915,7 @@ class Signature
     unsigned eqProxy = addFunction("vEQ",1, added);
     if(added){
       TermList tv = TermList(0, false);
-      TermList result = AtomicSort::arrowSort(tv, tv, AtomicSort::boolSort());
+      TermList result = AtomicSort::arrowSort({tv, tv, AtomicSort::boolSort()});
       Symbol * sym = getFunction(eqProxy);
       sym->setType(OperatorType::getConstantsType(result, 1));
       sym->setProxy(Proxy::EQUALS);
@@ -938,7 +938,7 @@ class Signature
     unsigned proxy = addFunction(name, 0, added);
     if (added) {
       auto bs = AtomicSort::boolSort();
-      auto result = AtomicSort::arrowSort(bs, bs, bs);
+      auto result = AtomicSort::arrowSort({bs, bs, bs});
       auto sym = getFunction(proxy);
       sym->setType(OperatorType::getConstantsType(result));
       sym->setProxy(convert(name));
diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp
index 9f503a217..8387fca55 100644
--- a/Kernel/Term.cpp
+++ b/Kernel/Term.cpp
@@ -182,24 +182,28 @@ TermList TermList::head() const {
   return trm;
 }
 
-std::pair<TermList, TermList> TermList::asPair() {
+std::pair<TermList, TermList> TermList::asPair() const {
   ASS(isArrowSort())
 
   return {domain(), result()};
 }
 
-TermList TermList::domain() {
+TermList TermList::domain() const {
   ASS(isArrowSort())
 
   return *term()->nthArgument(0);
 }
 
-TermList TermList::result() {
+TermList TermList::result() const {
   ASS(isArrowSort())
 
   return *term()->nthArgument(1);
 }
 
+TermList TermList::resultSort() const {
+  return SortHelper::getResultSort(term());
+}
+
 TermList TermList::replaceSubterm(TermList what, TermList by, bool liftFreeIndices) const {
   return SubtermReplacer(what, by, liftFreeIndices).replace(*this);
 }
@@ -306,28 +310,24 @@ unsigned TermList::weight() const
   return isVar() ? 1 : term()->weight();
 }
 
-bool TermList::isArrowSort()
-{
+bool TermList::isArrowSort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isArrowSort();
+         static_cast<const AtomicSort*>(term())->isArrowSort();
 }
 
-bool TermList::isBoolSort()
-{
+bool TermList::isBoolSort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isBoolSort();
+         static_cast<const AtomicSort*>(term())->isBoolSort();
 }
 
-bool TermList::isArraySort()
-{
+bool TermList::isArraySort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isArraySort();
+         static_cast<const AtomicSort*>(term())->isArraySort();
 }
 
-bool TermList::isTupleSort()
-{
+bool TermList::isTupleSort() const {
   return !isVar() && term()->isSort() &&
-         static_cast<AtomicSort*>(term())->isTupleSort();
+         static_cast<const AtomicSort*>(term())->isTupleSort();
 }
 
 bool AtomicSort::isArrowSort() const {
@@ -1305,10 +1305,6 @@ TermList AtomicSort::arrowSort(TermList s1, TermList s2) {
   return TermList(create2(arrow, s1, s2));
 }
 
-TermList AtomicSort::arrowSort(TermList s1, TermList s2, TermList s3) {
-  return arrowSort(s1, arrowSort(s2, s3));
-}
-
 TermList AtomicSort::arrowSort(unsigned size, const TermList* types, TermList range) {
   ASS(size > 0)
 
@@ -1319,6 +1315,14 @@ TermList AtomicSort::arrowSort(unsigned size, const TermList* types, TermList ra
   return res;
 }
 
+TermList AtomicSort::arrowSort(const std::initializer_list<TermList>& types) {
+  const auto size = types.size();
+  ASS(size >= 2)
+
+  const TermList* data = std::data(types);
+  return arrowSort(size - 1, data, data[size - 1]);
+}
+
 TermList AtomicSort::arrowSort(const TermStack & domSorts, TermList range) {
   TermList res = range;
   for (auto domSort : domSorts)
diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp
index 052fea53d..fdbb7b3ff 100644
--- a/Kernel/Term.hpp
+++ b/Kernel/Term.hpp
@@ -274,10 +274,10 @@ class TermList {
   /** if not var, the inner term must be shared */
   unsigned weight() const;
   /** returns true if this termList is wrapping a higher-order "arrow" sort */
-  bool isArrowSort();
-  bool isBoolSort();
-  bool isArraySort();
-  bool isTupleSort();
+  bool isArrowSort() const;
+  bool isBoolSort() const;
+  bool isArraySort() const;
+  bool isTupleSort() const;
   bool containsSubterm(TermList v) const;
   bool containsAllVariablesOf(TermList t) const;
   bool ground() const;
@@ -295,9 +295,10 @@ class TermList {
   TermList rhs() const;
   TermList lambdaBody() const;
   TermList head() const;
-  std::pair<TermList, TermList> asPair();
-  TermList domain();
-  TermList result();
+  std::pair<TermList, TermList> asPair() const;
+  TermList domain() const;
+  TermList result() const;
+  TermList resultSort() const;
   TermList replaceSubterm(TermList what, TermList by, bool liftFreeIndices = false) const;
   /* End higher-order terms */
 
@@ -1049,8 +1050,8 @@ class AtomicSort
   
   static TermList arrowSort(const TermStack& domSorts, TermList range);
   static TermList arrowSort(TermList s1, TermList s2);
-  static TermList arrowSort(TermList s1, TermList s2, TermList s3);
   static TermList arrowSort(unsigned size, const TermList* types, TermList range);
+  static TermList arrowSort(const std::initializer_list<TermList>& types);
   static TermList arraySort(TermList indexSort, TermList innerSort);
   static TermList tupleSort(unsigned arity, TermList* sorts);
   static TermList defaultSort();
diff --git a/Test/HOLUtils.cpp b/Test/HOLUtils.cpp
index 89518d68f..bc4305b31 100644
--- a/Test/HOLUtils.cpp
+++ b/Test/HOLUtils.cpp
@@ -83,9 +83,10 @@ Defs::Defs() {
   fSrt = TermList(AtomicSort::arrowSort(srt, srt));
   a = mkConst("a", srt);
   f = mkConst("f", fSrt);
-  f2 = mkConst("f2", AtomicSort::arrowSort(srt, AtomicSort::arrowSort(srt, srt)));
-  f3 = mkConst("f3", AtomicSort::arrowSort(srt, AtomicSort::arrowSort(srt, AtomicSort::arrowSort(srt, srt))));
-  g = mkConst("g", AtomicSort::arrowSort(AtomicSort::arrowSort(srt, srt), srt));
+  f2 = mkConst("f2", AtomicSort::arrowSort({srt, srt, srt}));
+  f3 = mkConst("f3", AtomicSort::arrowSort({srt, srt, srt, srt}));
+  g = mkConst("g", AtomicSort::arrowSort(fSrt, srt));
+  h = mkConst("h", AtomicSort::arrowSort({fSrt, srt, srt}));
 }
 
 Defs* Defs::_instance = nullptr;
diff --git a/Test/HOLUtils.hpp b/Test/HOLUtils.hpp
index c5cd0aa4f..9f2dc1f85 100644
--- a/Test/HOLUtils.hpp
+++ b/Test/HOLUtils.hpp
@@ -51,7 +51,7 @@ class Defs {
   static Defs* instance();
 
   TermList srt, fSrt;
-  TypedTermList a, f, f2, f3, g;
+  TypedTermList a, f, f2, f3, g, h;
 };
 
 TypedTermList x(unsigned idx, std::optional<TermList> sort = std::nullopt);
diff --git a/UnitTests/HOL/tBetaReduction.cpp b/UnitTests/HOL/tHOL_BetaReduction.cpp
similarity index 100%
rename from UnitTests/HOL/tBetaReduction.cpp
rename to UnitTests/HOL/tHOL_BetaReduction.cpp
diff --git a/UnitTests/HOL/tEtaReduction.cpp b/UnitTests/HOL/tHOL_EtaReduction.cpp
similarity index 97%
rename from UnitTests/HOL/tEtaReduction.cpp
rename to UnitTests/HOL/tHOL_EtaReduction.cpp
index c10476eb9..03efc2452 100644
--- a/UnitTests/HOL/tEtaReduction.cpp
+++ b/UnitTests/HOL/tHOL_EtaReduction.cpp
@@ -51,7 +51,7 @@ HOL_TEST_FUN(eta_reduction_2) {
 }
 
 HOL_TEST_FUN(eta_reduction_3) {
-  auto v0 = x(0, AtomicSort::arrowSort(D.srt, D.srt, D.srt));
+  auto v0 = x(0, AtomicSort::arrowSort({D.srt, D.srt, D.srt}));
   auto term = toNameless(lam({v0, x(1), x(2)}, app({v0, x(1), x(2)})));
   auto expected = toNameless(lam(v0, v0));
 
diff --git a/UnitTests/HOL/tHOL_Printing.cpp b/UnitTests/HOL/tHOL_Printing.cpp
index c3821bcf6..4118485a3 100644
--- a/UnitTests/HOL/tHOL_Printing.cpp
+++ b/UnitTests/HOL/tHOL_Printing.cpp
@@ -118,3 +118,26 @@ HOL_TEST_FUN(hol_print_2) {
       {TPTP,       "(^[Y0 : srt > srt]: ((^[Y1 : srt]: (Y1))))" }}
   );
 }
+
+HOL_TEST_FUN(hol_print_3) {
+  runTest(
+    D.f3.sort(),
+    { {RAW,    "(srt > (srt > (srt > srt)))" },
+      {PRETTY, "(srt → srt → srt → srt)" },
+      {TPTP,   "(srt > srt > srt > srt)"} }
+  );
+
+  runTest(
+    D.g.sort(),
+    { {RAW,    "((srt > srt) > srt)" },
+      {PRETTY, "((srt → srt) → srt)" },
+      {TPTP,   "((srt > srt) > srt)"} }
+  );
+
+  runTest(
+    D.h.sort(),
+    { {RAW,    "((srt > srt) > (srt > srt))" },
+      {PRETTY, "((srt → srt) → srt → srt)" },
+      {TPTP,   "((srt > srt) > srt > srt)"} }
+  );
+}
\ No newline at end of file
diff --git a/UnitTests/HOL/tSubtermReplacer.cpp b/UnitTests/HOL/tHOL_SubtermReplacer.cpp
similarity index 100%
rename from UnitTests/HOL/tSubtermReplacer.cpp
rename to UnitTests/HOL/tHOL_SubtermReplacer.cpp
diff --git a/UnitTests/HOL/tTermShifter.cpp b/UnitTests/HOL/tHOL_TermShifter.cpp
similarity index 100%
rename from UnitTests/HOL/tTermShifter.cpp
rename to UnitTests/HOL/tHOL_TermShifter.cpp
diff --git a/UnitTests/HOL/tHOL_ToPlaceholders.cpp b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
new file mode 100644
index 000000000..a6323ad20
--- /dev/null
+++ b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
@@ -0,0 +1,26 @@
+/*
+ * This file is part of the source code of the software program
+ * Vampire. It is protected by applicable
+ * copyright laws.
+ *
+ * This source code is distributed under the licence found here
+ * https://vprover.github.io/license.html
+ * and in the source directory
+ */
+
+#include "Kernel/HOL/HOL.hpp"
+#include "Test/HOLUtils.hpp"
+#include "Test/UnitTesting.hpp"
+
+using namespace Test::HOL;
+
+HOL_TEST_FUN(to_placeholders_1) {
+  auto term = app({D.h, D.f, app(x(1, D.fSrt), x(2))});
+  ASS_EQ(term.sort(), D.srt)
+  ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
+         "(h @ f @ (X1 @ X2))")
+  ASS_EQ(termListToString(term, Options::HPrinting::RAW),
+         "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),vAPP(srt,srt,X1,X2))")
+
+  std::cout << HOL::toPlaceholders(term) << std::endl;
+}
\ No newline at end of file
diff --git a/cmake/sources.cmake b/cmake/sources.cmake
index 5fb082254..640e33c19 100644
--- a/cmake/sources.cmake
+++ b/cmake/sources.cmake
@@ -84,10 +84,11 @@ set(UNIT_TESTS
     UnitTests/tTimeTrace.cpp
     UnitTests/tUnificationWithAbstraction.cpp
     UnitTests/HOL/tHOL_Printing.cpp
-    UnitTests/HOL/tBetaReduction.cpp
-    UnitTests/HOL/tEtaReduction.cpp
-    UnitTests/HOL/tTermShifter.cpp
-    UnitTests/HOL/tSubtermReplacer.cpp
+    UnitTests/HOL/tHOL_BetaReduction.cpp
+    UnitTests/HOL/tHOL_EtaReduction.cpp
+    UnitTests/HOL/tHOL_TermShifter.cpp
+    UnitTests/HOL/tHOL_SubtermReplacer.cpp
+    UnitTests/HOL/tHOL_ToPlaceholders.cpp
 )
 
 ################################################################
@@ -462,6 +463,8 @@ set(SOURCES
     Kernel/HOL/EtaNormaliser.hpp
     Kernel/HOL/SubtermReplacer.cpp
     Kernel/HOL/SubtermReplacer.hpp
+    Kernel/HOL/ToPlaceholders.cpp
+    Kernel/HOL/ToPlaceholders.hpp
     Lib/Allocator.cpp
     Lib/Allocator.hpp
     Lib/Array.hpp

From 43d670f9299d9f7044cf0e61663042d241f18239 Mon Sep 17 00:00:00 2001
From: Matthias Hetzenberger <mhetzenberger@gmail.com>
Date: Thu, 16 Oct 2025 17:59:25 +0200
Subject: [PATCH 2/6] Add more ToPlaceholder test and fix printing issue of
 placeholder constant

---
 Kernel/HOL/HOL.cpp                    |  8 ++++--
 Kernel/HOL/HOL.hpp                    |  4 ++-
 Kernel/HOL/SubtermReplacer.hpp        |  2 +-
 Kernel/HOL/TermShifter.hpp            |  2 +-
 Kernel/HOL/ToPlaceholders.cpp         |  4 +--
 Kernel/HOL/ToPlaceholders.hpp         | 15 +++++++++---
 Kernel/Term.cpp                       |  8 ++++++
 Kernel/Term.hpp                       |  2 ++
 UnitTests/HOL/tHOL_ToPlaceholders.cpp | 35 +++++++++++++++++++++++----
 9 files changed, 64 insertions(+), 16 deletions(-)

diff --git a/Kernel/HOL/HOL.cpp b/Kernel/HOL/HOL.cpp
index 5a18366e8..9d896b1ac 100644
--- a/Kernel/HOL/HOL.cpp
+++ b/Kernel/HOL/HOL.cpp
@@ -124,6 +124,10 @@ static std::string toStringAux(const Term& term, bool topLevel, IndexVarStack& s
     return res;
   }
 
+  if (term.isPlaceholder()) {
+    return term.functionName() + "⟨" + term.nthArgument(0)->toString(true) + "⟩";
+  }
+
   if (term.isLambdaTerm()) {
     unsigned v = st.size() ? st.top().second + 1 : 0;
     std::string bvar = (pretty ? "y" : "Y") + Int::toString(v);
@@ -374,6 +378,6 @@ void HOL::getMatrixAndPrefSorts(TermList t, TermList& matrix, TermStack& sorts)
   matrix = t;
 }
 
-TermList HOL::toPlaceholders(TermList term) {
-  return ToPlaceholders().replace(term);
+TermList HOL::toPlaceholders(TermList term, std::optional<Options::FunctionExtensionality> funcExtMode) {
+  return ToPlaceholders(funcExtMode).replace(term);
 }
\ No newline at end of file
diff --git a/Kernel/HOL/HOL.hpp b/Kernel/HOL/HOL.hpp
index 0c05630a4..527b4eae6 100644
--- a/Kernel/HOL/HOL.hpp
+++ b/Kernel/HOL/HOL.hpp
@@ -18,6 +18,8 @@
 #include "Kernel/TypedTermList.hpp"
 #include "Lib/Environment.hpp"
 
+#include <optional>
+
 /**
  * This namespace contains several helper functions to deal with higher-order terms.
  */
@@ -62,7 +64,7 @@ inline bool canHeadReduce(const TermList& head, const TermStack& args) {
   return head.isLambdaTerm() && args.isNonEmpty();
 }
 
-TermList toPlaceholders(TermList term);
+TermList toPlaceholders(TermList term, std::optional<Options::FunctionExtensionality> funcExtMode = std::nullopt);
 
 } // namespace HOL
 
diff --git a/Kernel/HOL/SubtermReplacer.hpp b/Kernel/HOL/SubtermReplacer.hpp
index 2798aaa44..10e185fbf 100644
--- a/Kernel/HOL/SubtermReplacer.hpp
+++ b/Kernel/HOL/SubtermReplacer.hpp
@@ -24,7 +24,7 @@ using namespace Kernel;
  * In contrast to EqHelper::replace free de Bruijn indices of the new subterm can be automatically
  * lifted in order to avoid name capture.
  *
- * See also tSubtermReplacer.cpp for accompanying unit tests of this class.
+ * See also tHOL_SubtermReplacer.cpp for accompanying unit tests of this class.
  */
 class SubtermReplacer : public TermTransformer {
 public:
diff --git a/Kernel/HOL/TermShifter.hpp b/Kernel/HOL/TermShifter.hpp
index 8607ceb1a..a5463ffb5 100644
--- a/Kernel/HOL/TermShifter.hpp
+++ b/Kernel/HOL/TermShifter.hpp
@@ -31,7 +31,7 @@ using namespace Kernel;
  * Example:
  * TermTransformer::shift(t, 2) ~> { "(λ. f db_0) db_2", Option<unsigned>(0) }
  *
- * See also tTermShifter.cpp for accompanying unit tests of this class.
+ * See also tHOL_TermShifter.cpp for accompanying unit tests of this class.
  */
 class TermShifter : public TermTransformer
 {
diff --git a/Kernel/HOL/ToPlaceholders.cpp b/Kernel/HOL/ToPlaceholders.cpp
index a544fef02..a76b6248e 100644
--- a/Kernel/HOL/ToPlaceholders.cpp
+++ b/Kernel/HOL/ToPlaceholders.cpp
@@ -14,11 +14,11 @@
 #include "Kernel/HOL/ToPlaceholders.hpp"
 #include "Kernel/HOL/HOL.hpp"
 
-ToPlaceholders::ToPlaceholders()
+ToPlaceholders::ToPlaceholders(std::optional<Options::FunctionExtensionality> funcExtMode)
       : TermTransformer(false),
         _nextIsPrefix(false),
         _topLevel(true),
-        _mode(env.options->functionExtensionality()) {}
+        _mode(funcExtMode.value_or(env.options->functionExtensionality())) {}
 
 TermList ToPlaceholders::replace(TermList term) {
   TermList transformed = transformSubterm(term);
diff --git a/Kernel/HOL/ToPlaceholders.hpp b/Kernel/HOL/ToPlaceholders.hpp
index 7a5ca3629..820a050fd 100644
--- a/Kernel/HOL/ToPlaceholders.hpp
+++ b/Kernel/HOL/ToPlaceholders.hpp
@@ -18,15 +18,22 @@
 #include "Kernel/TermTransformer.hpp"
 #include "Shell/Options.hpp"
 
+#include <optional>
+
 using namespace Kernel;
 
-// replaces higher-order subterms (subterms with variable heads e.g., X a b &
-// lambda terms) with a special polymorphic constant we call a "placeholder".
-// Depending on the mode functional and Boolean subterms may also be replaced
+/**
+* Replaces higher-order subterms (subterms with variable heads e.g., X a b and
+* lambda terms) with a special polymorphic constant we call a "placeholder".
+*
+* If the value of the FunctionExtensionality option is ABSTRACTION, functional and Boolean subterms are also be replaced
+*
+* See also tHOL_ToPlaceholders.cpp for accompanying unit tests of this class.
+*/
 class ToPlaceholders : public TermTransformer
 {
 public:
-  ToPlaceholders();
+  explicit ToPlaceholders(std::optional<Shell::Options::FunctionExtensionality> funcExtMode);
 
   TermList replace(TermList term);
   TermList transformSubterm(TermList t) override;
diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp
index 8387fca55..75640dc01 100644
--- a/Kernel/Term.cpp
+++ b/Kernel/Term.cpp
@@ -143,6 +143,10 @@ bool TermList::isChoice() const {
   return !isVar() && term()->isChoice();
 }
 
+bool TermList::isPlaceholder() const {
+  return !isVar() && term()->isPlaceholder();
+}
+
 Option<unsigned> TermList::deBruijnIndex() const {
   if (isVar())
     return {};
@@ -941,6 +945,10 @@ bool Term::isChoice() const {
   return !isSort() && !isLiteral() && !isSpecial() && env.signature->isChoiceFun(_functor);
 }
 
+bool Term::isPlaceholder() const {
+  return !isSort() && !isLiteral() && !isSpecial() && env.signature->isPlaceholder(_functor);
+}
+
 Option<unsigned> Term::deBruijnIndex() const {
   if (isSort() || isLiteral() || isSpecial())
     return {};
diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp
index fdbb7b3ff..9428802e0 100644
--- a/Kernel/Term.hpp
+++ b/Kernel/Term.hpp
@@ -289,6 +289,7 @@ class TermList {
   bool isRedex() const;
   bool isProxy(Proxy proxy) const;
   bool isChoice() const;
+  bool isPlaceholder() const;
 
   Option<unsigned> deBruijnIndex() const;
   TermList lhs() const;
@@ -787,6 +788,7 @@ class alignas(8) Term
   bool isRedex() const;
   bool isProxy(Proxy proxy) const;
   bool isChoice() const;
+  bool isPlaceholder() const;
 
   TermList lambdaBody() const {
     ASS(isLambdaTerm())
diff --git a/UnitTests/HOL/tHOL_ToPlaceholders.cpp b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
index a6323ad20..770adf85f 100644
--- a/UnitTests/HOL/tHOL_ToPlaceholders.cpp
+++ b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
@@ -14,13 +14,38 @@
 
 using namespace Test::HOL;
 
+TypedTermList ph(TermList sort) {
+  return {HOL::create::placeholder(sort), sort};
+}
+
 HOL_TEST_FUN(to_placeholders_1) {
   auto term = app({D.h, D.f, app(x(1, D.fSrt), x(2))});
   ASS_EQ(term.sort(), D.srt)
-  ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
-         "(h @ f @ (X1 @ X2))")
-  ASS_EQ(termListToString(term, Options::HPrinting::RAW),
-         "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),vAPP(srt,srt,X1,X2))")
 
-  std::cout << HOL::toPlaceholders(term) << std::endl;
+  ASS_EQ(
+    termListToString(term, Options::HPrinting::TPTP),
+    "(h @ f @ (X1 @ X2))"
+  )
+
+  ASS_EQ(
+    termListToString(term, Options::HPrinting::RAW),
+    "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),vAPP(srt,srt,X1,X2))"
+  )
+
+  ASS_EQ(
+    HOL::toPlaceholders(term),
+    app({D.h, ph(D.fSrt), ph(D.srt)})
+  )
+
+  ASS_EQ(
+    HOL::toPlaceholders(term, Options::FunctionExtensionality::OFF),
+    app({D.h, D.f, ph(D.srt)})
+  )
+}
+
+HOL_TEST_FUN(to_placeholders_2) {
+  ASS_EQ(
+    HOL::toPlaceholders(app({D.h, LAM(D.srt, db(0)), D.a})),
+    app({D.h, ph(D.fSrt), D.a})
+  )
 }
\ No newline at end of file

From d2a45d529affbaedcf9447eb51d006a926b64ae3 Mon Sep 17 00:00:00 2001
From: Matthias Hetzenberger <mhetzenberger@gmail.com>
Date: Fri, 23 Jan 2026 11:09:03 +0100
Subject: [PATCH 3/6] Strengthen ToPlaceholders unit tests

---
 Kernel/HOL/ToPlaceholders.cpp         |  2 +-
 UnitTests/HOL/tHOL_ToPlaceholders.cpp | 31 +++++++++++++++------------
 2 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/Kernel/HOL/ToPlaceholders.cpp b/Kernel/HOL/ToPlaceholders.cpp
index a76b6248e..d159aa6ea 100644
--- a/Kernel/HOL/ToPlaceholders.cpp
+++ b/Kernel/HOL/ToPlaceholders.cpp
@@ -1,4 +1,4 @@
- /*
+/*
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.
diff --git a/UnitTests/HOL/tHOL_ToPlaceholders.cpp b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
index 770adf85f..790b27b89 100644
--- a/UnitTests/HOL/tHOL_ToPlaceholders.cpp
+++ b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
@@ -32,20 +32,23 @@ HOL_TEST_FUN(to_placeholders_1) {
     "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),vAPP(srt,srt,X1,X2))"
   )
 
-  ASS_EQ(
-    HOL::toPlaceholders(term),
-    app({D.h, ph(D.fSrt), ph(D.srt)})
-  )
-
-  ASS_EQ(
-    HOL::toPlaceholders(term, Options::FunctionExtensionality::OFF),
-    app({D.h, D.f, ph(D.srt)})
-  )
+  auto res = HOL::toPlaceholders(term);
+  ASS_EQ(res, app({D.h, ph(D.fSrt), ph(D.srt)}))
+  ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ ph0⟨srt⟩)")
+  ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,ph0(srt > srt)),ph0(srt))")
+
+  // With the setting FunctionExtensionality::OFF, the result of toPlaceholders(h @ f @ (x1 @ x2))
+  // is h @ f @ ☐ as the functional subterm f is not replaced by a placeholder.
+  res = HOL::toPlaceholders(term, Options::FunctionExtensionality::OFF);
+  ASS_EQ(res, app({D.h, D.f, ph(D.srt)}))
+  ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ f @ ph0⟨srt⟩)")
+  ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),ph0(srt))")
 }
 
 HOL_TEST_FUN(to_placeholders_2) {
-  ASS_EQ(
-    HOL::toPlaceholders(app({D.h, LAM(D.srt, db(0)), D.a})),
-    app({D.h, ph(D.fSrt), D.a})
-  )
-}
\ No newline at end of file
+  const auto res = HOL::toPlaceholders(app({D.h, LAM(D.srt, db(0)), D.a}));
+
+  ASS_EQ(res, app({D.h, ph(D.fSrt), D.a}))
+  ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ a)")
+  ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,ph0(srt > srt)),a)")
+}

From 973149d2866a0afe2961e76e992e6a124381a411 Mon Sep 17 00:00:00 2001
From: Matthias Hetzenberger <mhetzenberger@gmail.com>
Date: Mon, 26 Jan 2026 18:00:03 +0100
Subject: [PATCH 4/6] Add 'transformSorts' comment to TermTransformer
 constructor invocations

---
 Kernel/HOL/BetaNormaliser.hpp  | 2 +-
 Kernel/HOL/HOL.hpp             | 2 +-
 Kernel/HOL/RedexReducer.hpp    | 2 +-
 Kernel/HOL/SubtermReplacer.cpp | 2 +-
 Kernel/HOL/TermShifter.hpp     | 2 +-
 Kernel/HOL/ToPlaceholders.cpp  | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Kernel/HOL/BetaNormaliser.hpp b/Kernel/HOL/BetaNormaliser.hpp
index 90b486ed7..b7f0e0962 100644
--- a/Kernel/HOL/BetaNormaliser.hpp
+++ b/Kernel/HOL/BetaNormaliser.hpp
@@ -26,7 +26,7 @@ using namespace Kernel;
 class BetaNormaliser : public TermTransformer {
   unsigned reductions = 0;
 public:
-  BetaNormaliser() : TermTransformer(false) {}
+  BetaNormaliser() : TermTransformer(/*transformSorts=*/false) {}
 
   unsigned getReductions() const {
     return reductions;
diff --git a/Kernel/HOL/HOL.hpp b/Kernel/HOL/HOL.hpp
index 527b4eae6..311dca0d3 100644
--- a/Kernel/HOL/HOL.hpp
+++ b/Kernel/HOL/HOL.hpp
@@ -26,7 +26,7 @@
 namespace HOL {
 
 using Kernel::Term;
-  
+
 inline bool isTrue(TermList term) {
   return term.isTerm() && env.signature->isFoolConstantSymbol(true, term.term()->functor());
 }
diff --git a/Kernel/HOL/RedexReducer.hpp b/Kernel/HOL/RedexReducer.hpp
index 86a91ca9d..669bd23db 100644
--- a/Kernel/HOL/RedexReducer.hpp
+++ b/Kernel/HOL/RedexReducer.hpp
@@ -20,7 +20,7 @@ using namespace Kernel;
 
 class RedexReducer : public TermTransformer {
 public:
-  RedexReducer() : TermTransformer(false) {}
+  RedexReducer() : TermTransformer(/*transformSorts=*/false) {}
 
   TermList reduce(TermList head, TermStack& args);
   TermList transformSubterm(TermList t) override;
diff --git a/Kernel/HOL/SubtermReplacer.cpp b/Kernel/HOL/SubtermReplacer.cpp
index 500613cd7..d9399d710 100644
--- a/Kernel/HOL/SubtermReplacer.cpp
+++ b/Kernel/HOL/SubtermReplacer.cpp
@@ -16,7 +16,7 @@
 #include "TermShifter.hpp"
 
 SubtermReplacer::SubtermReplacer(TermList what, TermList by, bool liftFree)
-      : TermTransformer(false),
+      : TermTransformer(/*transformSorts=*/false),
         _what(what),
         _by(by),
         _liftFreeIndices(liftFree) {
diff --git a/Kernel/HOL/TermShifter.hpp b/Kernel/HOL/TermShifter.hpp
index a5463ffb5..627c58c35 100644
--- a/Kernel/HOL/TermShifter.hpp
+++ b/Kernel/HOL/TermShifter.hpp
@@ -37,7 +37,7 @@ class TermShifter : public TermTransformer
 {
 public:
   explicit TermShifter(int shiftBy)
-    : TermTransformer(false),
+    : TermTransformer(/*transformSorts=*/false),
       _shiftBy(shiftBy) {}
 
   // positive value -> shift up
diff --git a/Kernel/HOL/ToPlaceholders.cpp b/Kernel/HOL/ToPlaceholders.cpp
index d159aa6ea..80922c329 100644
--- a/Kernel/HOL/ToPlaceholders.cpp
+++ b/Kernel/HOL/ToPlaceholders.cpp
@@ -15,7 +15,7 @@
 #include "Kernel/HOL/HOL.hpp"
 
 ToPlaceholders::ToPlaceholders(std::optional<Options::FunctionExtensionality> funcExtMode)
-      : TermTransformer(false),
+      : TermTransformer(/*transformSorts=*/false),
         _nextIsPrefix(false),
         _topLevel(true),
         _mode(funcExtMode.value_or(env.options->functionExtensionality())) {}

From ddaffdc1360068be1c112385c8db576a2725ef7f Mon Sep 17 00:00:00 2001
From: Matthias Hetzenberger <mhetzenberger@gmail.com>
Date: Mon, 26 Jan 2026 18:22:08 +0100
Subject: [PATCH 5/6] Make ToPlaceholders::replace static to prevent accidental
 reuse

---
 Kernel/HOL/HOL.cpp                    |  4 ----
 Kernel/HOL/HOL.hpp                    |  2 --
 Kernel/HOL/ToPlaceholders.cpp         | 14 +++++++-------
 Kernel/HOL/ToPlaceholders.hpp         |  5 ++---
 UnitTests/HOL/tHOL_ToPlaceholders.cpp |  7 ++++---
 5 files changed, 13 insertions(+), 19 deletions(-)

diff --git a/Kernel/HOL/HOL.cpp b/Kernel/HOL/HOL.cpp
index 9d896b1ac..c0a2a0a20 100644
--- a/Kernel/HOL/HOL.cpp
+++ b/Kernel/HOL/HOL.cpp
@@ -377,7 +377,3 @@ void HOL::getMatrixAndPrefSorts(TermList t, TermList& matrix, TermStack& sorts)
   }
   matrix = t;
 }
-
-TermList HOL::toPlaceholders(TermList term, std::optional<Options::FunctionExtensionality> funcExtMode) {
-  return ToPlaceholders(funcExtMode).replace(term);
-}
\ No newline at end of file
diff --git a/Kernel/HOL/HOL.hpp b/Kernel/HOL/HOL.hpp
index 311dca0d3..808753bab 100644
--- a/Kernel/HOL/HOL.hpp
+++ b/Kernel/HOL/HOL.hpp
@@ -64,8 +64,6 @@ inline bool canHeadReduce(const TermList& head, const TermStack& args) {
   return head.isLambdaTerm() && args.isNonEmpty();
 }
 
-TermList toPlaceholders(TermList term, std::optional<Options::FunctionExtensionality> funcExtMode = std::nullopt);
-
 } // namespace HOL
 
 namespace HOL::create {
diff --git a/Kernel/HOL/ToPlaceholders.cpp b/Kernel/HOL/ToPlaceholders.cpp
index 80922c329..592c7fbb8 100644
--- a/Kernel/HOL/ToPlaceholders.cpp
+++ b/Kernel/HOL/ToPlaceholders.cpp
@@ -14,20 +14,20 @@
 #include "Kernel/HOL/ToPlaceholders.hpp"
 #include "Kernel/HOL/HOL.hpp"
 
-ToPlaceholders::ToPlaceholders(std::optional<Options::FunctionExtensionality> funcExtMode)
+ToPlaceholders::ToPlaceholders(Options::FunctionExtensionality funcExtMode)
       : TermTransformer(/*transformSorts=*/false),
         _nextIsPrefix(false),
         _topLevel(true),
-        _mode(funcExtMode.value_or(env.options->functionExtensionality())) {}
+        _mode(funcExtMode) {}
 
-TermList ToPlaceholders::replace(TermList term) {
-  TermList transformed = transformSubterm(term);
+TermList ToPlaceholders::replace(TermList term, std::optional<Options::FunctionExtensionality> funcExtMode) {
+  auto toPlaceholders = ToPlaceholders(funcExtMode.value_or(env.options->functionExtensionality()));
 
-  if (transformed != term)
+  if (auto transformed = toPlaceholders.transformSubterm(term); transformed != term)
     return transformed;
 
-  _topLevel = false;
-  return transform(term);
+  toPlaceholders._topLevel = false;
+  return toPlaceholders.transform(term);
 }
 
 TermList ToPlaceholders::transformSubterm(TermList t) {
diff --git a/Kernel/HOL/ToPlaceholders.hpp b/Kernel/HOL/ToPlaceholders.hpp
index 820a050fd..eb6f06ba3 100644
--- a/Kernel/HOL/ToPlaceholders.hpp
+++ b/Kernel/HOL/ToPlaceholders.hpp
@@ -33,9 +33,7 @@ using namespace Kernel;
 class ToPlaceholders : public TermTransformer
 {
 public:
-  explicit ToPlaceholders(std::optional<Shell::Options::FunctionExtensionality> funcExtMode);
-
-  TermList replace(TermList term);
+  static TermList replace(TermList term, std::optional<Shell::Options::FunctionExtensionality> funcExtMode = std::nullopt);
   TermList transformSubterm(TermList t) override;
 
   void onTermEntry(Term* t) override {
@@ -48,6 +46,7 @@ class ToPlaceholders : public TermTransformer
   }
 
 private:
+  explicit ToPlaceholders(Shell::Options::FunctionExtensionality funcExtMode);
   bool _nextIsPrefix;
   bool _topLevel;
   Shell::Options::FunctionExtensionality _mode;
diff --git a/UnitTests/HOL/tHOL_ToPlaceholders.cpp b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
index 790b27b89..3148fb225 100644
--- a/UnitTests/HOL/tHOL_ToPlaceholders.cpp
+++ b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
@@ -9,6 +9,7 @@
  */
 
 #include "Kernel/HOL/HOL.hpp"
+#include "Kernel/HOL/ToPlaceholders.hpp"
 #include "Test/HOLUtils.hpp"
 #include "Test/UnitTesting.hpp"
 
@@ -32,21 +33,21 @@ HOL_TEST_FUN(to_placeholders_1) {
     "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),vAPP(srt,srt,X1,X2))"
   )
 
-  auto res = HOL::toPlaceholders(term);
+  auto res = ToPlaceholders::replace(term);
   ASS_EQ(res, app({D.h, ph(D.fSrt), ph(D.srt)}))
   ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ ph0⟨srt⟩)")
   ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,ph0(srt > srt)),ph0(srt))")
 
   // With the setting FunctionExtensionality::OFF, the result of toPlaceholders(h @ f @ (x1 @ x2))
   // is h @ f @ ☐ as the functional subterm f is not replaced by a placeholder.
-  res = HOL::toPlaceholders(term, Options::FunctionExtensionality::OFF);
+  res = ToPlaceholders::replace(term, Options::FunctionExtensionality::OFF);
   ASS_EQ(res, app({D.h, D.f, ph(D.srt)}))
   ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ f @ ph0⟨srt⟩)")
   ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),ph0(srt))")
 }
 
 HOL_TEST_FUN(to_placeholders_2) {
-  const auto res = HOL::toPlaceholders(app({D.h, LAM(D.srt, db(0)), D.a}));
+  const auto res = ToPlaceholders::replace(app({D.h, LAM(D.srt, db(0)), D.a}));
 
   ASS_EQ(res, app({D.h, ph(D.fSrt), D.a}))
   ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ a)")

From 8b4088362a59391a6bda726bdbc44d9872b9d6d0 Mon Sep 17 00:00:00 2001
From: Matthias Hetzenberger <mhetzenberger@gmail.com>
Date: Mon, 26 Jan 2026 19:27:26 +0100
Subject: [PATCH 6/6] Convert HOLUtils::app function to use variadic template
 arguments

---
 Test/HOLUtils.cpp                     | 24 ------------------------
 Test/HOLUtils.hpp                     | 18 ++++++++++++++++--
 UnitTests/HOL/tHOL_BetaReduction.cpp  |  4 ++--
 UnitTests/HOL/tHOL_EtaReduction.cpp   | 12 ++++++------
 UnitTests/HOL/tHOL_ToPlaceholders.cpp | 10 +++++-----
 5 files changed, 29 insertions(+), 39 deletions(-)

diff --git a/Test/HOLUtils.cpp b/Test/HOLUtils.cpp
index bc4305b31..90fc1a858 100644
--- a/Test/HOLUtils.cpp
+++ b/Test/HOLUtils.cpp
@@ -44,30 +44,6 @@ TypedTermList lam(std::initializer_list<TypedTermList> typedVars, TypedTermList
   return {TermList(term), sort};
 }
 
-TypedTermList app(TypedTermList lhs, TypedTermList rhs) {
-  ASS(lhs.sort().isArrowSort())
-
-  auto [domain, result] = lhs.sort().asPair();
-
-  ASS(domain == rhs.sort())
-
-  return {::HOL::create::app(domain, result, lhs, rhs), result};
-}
-
-TypedTermList app(const std::initializer_list<TypedTermList>& terms) {
-  const auto size = terms.size();
-
-  ASS(size > 0)
-  auto a = std::data(terms);
-  TypedTermList res = a[0];
-
-  for (std::size_t i = 0; i + 1 < size; ++i) {
-    res = app(res, a[i+1]);
-  }
-
-  return res;
-}
-
 static TermList mkAtomicSort(const std::string& name) {
   return TermList(AtomicSort::createConstant(name));
 }
diff --git a/Test/HOLUtils.hpp b/Test/HOLUtils.hpp
index 9f2dc1f85..4d55fd6c4 100644
--- a/Test/HOLUtils.hpp
+++ b/Test/HOLUtils.hpp
@@ -16,6 +16,7 @@
 
 #include "Kernel/Term.hpp"
 #include "Kernel/TypedTermList.hpp"
+#include "Kernel/HOL/HOL.hpp"
 #include "Shell/Options.hpp"
 
 #include <optional>
@@ -41,8 +42,21 @@ inline TypedTermList lam(TypedTermList var, TypedTermList body) {
   return lam({var}, body);
 }
 
-TypedTermList app(TypedTermList lhs, TypedTermList rhs);
-TypedTermList app(const std::initializer_list<TypedTermList>& terms);
+template <class T, class ...Ts>
+TypedTermList app(TypedTermList arg1, T arg2, Ts... args) {
+  ASS(arg1.sort().isArrowSort())
+
+  auto [domain, result] = arg1.sort().asPair();
+
+  ASS(domain == arg2.sort())
+
+  TypedTermList t = {::HOL::create::app(domain, result, arg1, arg2), result};
+
+  if constexpr (sizeof...(args) == 0)
+    return t;
+  else
+    return app(t, args...);
+}
 
 class Defs {
   static Defs* _instance;
diff --git a/UnitTests/HOL/tHOL_BetaReduction.cpp b/UnitTests/HOL/tHOL_BetaReduction.cpp
index 70a164013..a2e4a85f0 100644
--- a/UnitTests/HOL/tHOL_BetaReduction.cpp
+++ b/UnitTests/HOL/tHOL_BetaReduction.cpp
@@ -24,7 +24,7 @@ HOL_TEST_FUN(beta_reduction_1) {
   unsigned reds;
   for (const auto term : testTerms) {
     auto reduced = betaNF(
-      toNameless(app(id(), {term, D.srt})), &reds
+      toNameless(app(id(), TypedTermList(term, D.srt))), &reds
     );
 
     ASS_EQ(reds, 1)
@@ -46,7 +46,7 @@ HOL_TEST_FUN(beta_reduction_2) {
     for (const auto term2 : testTerms) {
       auto constFn = lam(x(0), {term1, D.srt});
       auto reduced = betaNF(
-        toNameless(app(constFn, {term2, D.srt})), &reds
+        toNameless(app(constFn, TypedTermList(term2, D.srt))), &reds
       );
 
       ASS_EQ(reds, 1)
diff --git a/UnitTests/HOL/tHOL_EtaReduction.cpp b/UnitTests/HOL/tHOL_EtaReduction.cpp
index 03efc2452..dfd80554f 100644
--- a/UnitTests/HOL/tHOL_EtaReduction.cpp
+++ b/UnitTests/HOL/tHOL_EtaReduction.cpp
@@ -20,21 +20,21 @@ HOL_TEST_FUN(eta_reduction_1) {
   ASS_EQ(D.a, toNameless(D.a))
   ASS_EQ(etaNF(D.a), D.a)
 
-  auto term = toNameless(lam(x(0), app({D.f, x(0)})));
+  auto term = toNameless(lam(x(0), app(D.f, x(0))));
   ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
          "(^[Y0 : srt]: (f @ Y0))")
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
          "vLAM(srt,srt,vAPP(srt,srt,f,db0(srt)))")
   ASS_EQ(etaNF(term), D.f)
 
-  term = toNameless(lam({x(0), x(1)}, app({D.f2, x(0), x(1)})));
+  term = toNameless(lam({x(0), x(1)}, app(D.f2, x(0), x(1))));
   ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
          "(^[Y0 : srt]: ((^[Y1 : srt]: (f2 @ Y0 @ Y1))))")
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
          "vLAM(srt,srt > srt,vLAM(srt,srt,vAPP(srt,srt,vAPP(srt,srt > srt,f2,db1(srt)),db0(srt))))")
   ASS_EQ(etaNF(term), D.f2)
 
-  term = toNameless(lam({x(0), x(1), x(2)}, app({D.f3, x(0), x(1), x(2)})));
+  term = toNameless(lam({x(0), x(1), x(2)}, app(D.f3, x(0), x(1), x(2))));
   ASS_EQ(termListToString(term, Options::HPrinting::TPTP),
          "(^[Y0 : srt]: ((^[Y1 : srt]: ((^[Y2 : srt]: (f3 @ Y0 @ Y1 @ Y2))))))")
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
@@ -43,7 +43,7 @@ HOL_TEST_FUN(eta_reduction_1) {
 }
 
 HOL_TEST_FUN(eta_reduction_2) {
-  auto term = toNameless(lam({x(0), x(1), x(2)}, app({D.f3, x(0), x(2), x(1)})));
+  auto term = toNameless(lam({x(0), x(1), x(2)}, app(D.f3, x(0), x(2), x(1))));
 
   ASS_EQ(termListToString(term, Options::HPrinting::RAW),
          "vLAM(srt,srt > (srt > srt),vLAM(srt,srt > srt,vLAM(srt,srt,vAPP(srt,srt,vAPP(srt,srt > srt,vAPP(srt,srt > (srt > srt),f3,db2(srt)),db0(srt)),db1(srt)))))");
@@ -52,7 +52,7 @@ HOL_TEST_FUN(eta_reduction_2) {
 
 HOL_TEST_FUN(eta_reduction_3) {
   auto v0 = x(0, AtomicSort::arrowSort({D.srt, D.srt, D.srt}));
-  auto term = toNameless(lam({v0, x(1), x(2)}, app({v0, x(1), x(2)})));
+  auto term = toNameless(lam({v0, x(1), x(2)}, app(v0, x(1), x(2))));
   auto expected = toNameless(lam(v0, v0));
 
   ASS_EQ(expected, HOL::create::namelessLambda(v0.sort(), v0.sort(), HOL::getDeBruijnIndex(0, v0.sort())))
@@ -60,7 +60,7 @@ HOL_TEST_FUN(eta_reduction_3) {
 }
 
 HOL_TEST_FUN(eta_reduction_4) {
-  auto term = toNameless(lam(x(0), app({D.f2, x(0), x(0)})));
+  auto term = toNameless(lam(x(0), app(D.f2, x(0), x(0))));
 
   ASS_EQ(etaNF(term), term)
 }
diff --git a/UnitTests/HOL/tHOL_ToPlaceholders.cpp b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
index 3148fb225..0b2567fde 100644
--- a/UnitTests/HOL/tHOL_ToPlaceholders.cpp
+++ b/UnitTests/HOL/tHOL_ToPlaceholders.cpp
@@ -20,7 +20,7 @@ TypedTermList ph(TermList sort) {
 }
 
 HOL_TEST_FUN(to_placeholders_1) {
-  auto term = app({D.h, D.f, app(x(1, D.fSrt), x(2))});
+  auto term = app(D.h, D.f, app(x(1, D.fSrt), x(2)));
   ASS_EQ(term.sort(), D.srt)
 
   ASS_EQ(
@@ -34,22 +34,22 @@ HOL_TEST_FUN(to_placeholders_1) {
   )
 
   auto res = ToPlaceholders::replace(term);
-  ASS_EQ(res, app({D.h, ph(D.fSrt), ph(D.srt)}))
+  ASS_EQ(res, app(D.h, ph(D.fSrt), ph(D.srt)))
   ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ ph0⟨srt⟩)")
   ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,ph0(srt > srt)),ph0(srt))")
 
   // With the setting FunctionExtensionality::OFF, the result of toPlaceholders(h @ f @ (x1 @ x2))
   // is h @ f @ ☐ as the functional subterm f is not replaced by a placeholder.
   res = ToPlaceholders::replace(term, Options::FunctionExtensionality::OFF);
-  ASS_EQ(res, app({D.h, D.f, ph(D.srt)}))
+  ASS_EQ(res, app(D.h, D.f, ph(D.srt)))
   ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ f @ ph0⟨srt⟩)")
   ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,f),ph0(srt))")
 }
 
 HOL_TEST_FUN(to_placeholders_2) {
-  const auto res = ToPlaceholders::replace(app({D.h, LAM(D.srt, db(0)), D.a}));
+  const auto res = ToPlaceholders::replace(app(D.h, LAM(D.srt, db(0)), D.a));
 
-  ASS_EQ(res, app({D.h, ph(D.fSrt), D.a}))
+  ASS_EQ(res, app(D.h, ph(D.fSrt), D.a))
   ASS_EQ(termListToString(res, Options::HPrinting::TPTP), "(h @ ph0⟨srt > srt⟩ @ a)")
   ASS_EQ(termListToString(res, Options::HPrinting::RAW), "vAPP(srt,srt,vAPP(srt > srt,srt > srt,h,ph0(srt > srt)),a)")
 }