Add ToPlaceholders TermTransformer

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;

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;
       }
 

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);

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>>;
@@ -123,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);
@@ -371,4 +376,4 @@ void HOL::getMatrixAndPrefSorts(TermList t, TermList& matrix, TermStack& sorts)
     t = t.lambdaBody();
   }
   matrix = t;
-}
+}

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.
  */
@@ -68,7 +70,7 @@ 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 {

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;

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) {

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:

Kernel/HOL/TermShifter.hpp

@@ -31,13 +31,13 @@ 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
 {
 public:
   explicit TermShifter(int shiftBy)
-    : TermTransformer(false),
+    : TermTransformer(/*transformSorts=*/false),
       _shiftBy(shiftBy) {}
 
   // positive value -> shift up

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(Options::FunctionExtensionality funcExtMode)
+      : TermTransformer(/*transformSorts=*/false),
+        _nextIsPrefix(false),
+        _topLevel(true),
+        _mode(funcExtMode) {}
+
+TermList ToPlaceholders::replace(TermList term, std::optional<Options::FunctionExtensionality> funcExtMode) {
+  auto toPlaceholders = ToPlaceholders(funcExtMode.value_or(env.options->functionExtensionality()));
+
+  if (auto transformed = toPlaceholders.transformSubterm(term); transformed != term)
+    return transformed;
+
+  toPlaceholders._topLevel = false;
+  return toPlaceholders.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;
+}

Kernel/HOL/ToPlaceholders.hpp

@@ -0,0 +1,55 @@
+/*
+ * 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"
+
+#include <optional>
+
+using namespace Kernel;
+
+/**
+* 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:
+  static TermList replace(TermList term, std::optional<Shell::Options::FunctionExtensionality> funcExtMode = std::nullopt);
+  TermList transformSubterm(TermList t) override;
+
+  void onTermEntry(Term* t) override {
+    if (t->isApplication())
+      _nextIsPrefix = true;
+  }
+
+  void onTermExit(Term* t) override {
+    _nextIsPrefix = false;
+  }
+
+private:
+  explicit ToPlaceholders(Shell::Options::FunctionExtensionality funcExtMode);
+  bool _nextIsPrefix;
+  bool _topLevel;
+  Shell::Options::FunctionExtensionality _mode;
+};
+
+#endif // __ToPlaceholders__

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;
 }
 

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));