Parsing THF and adding several regressions (#3131)

1 files changed, 22 insertions, 1 deletions

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index c4efe5e09..694369429 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -121,7 +121,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer, std::vector< pANT
   // Same thing as the predefined PUSHSTREAM(in);
   lexer->pushCharStream(lexer,in);
   // restart it
-  //lexer->rec->state->tokenStartCharIndex	= -10;
+  //lexer->rec->state->tokenStartCharIndex  = -10;
   //lexer->emit(lexer);
 
   // Note that the input stream is not closed when it EOFs, I don't bother
@@ -301,6 +301,27 @@ void Tptp::makeApplication(Expr& expr, std::string& name,
   }
 }
 
+void Tptp::mkLambdaWrapper(Expr& expr, Type argType)
+{
+  std::vector<Expr> lvars;
+  std::vector<Type> domainTypes =
+      (static_cast<FunctionType>(argType)).getArgTypes();
+  for (unsigned i = 0, size = domainTypes.size(); i < size; ++i)
+  {
+    // the introduced variable is internal (not parsable)
+    std::stringstream ss;
+    ss << "_lvar_" << i;
+    Expr v = getExprManager()->mkBoundVar(ss.str(), domainTypes[i]);
+    lvars.push_back(v);
+  }
+  // apply body of lambda to variables
+  Expr wrapper = getExprManager()->mkExpr(
+      kind::LAMBDA,
+      getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars),
+      getExprManager()->mkExpr(expr, lvars));
+
+  expr = wrapper;
+}
 
 Expr Tptp::getAssertionExpr(FormulaRole fr, Expr expr) {
   switch (fr) {