Fix internal type error when printing lambdas with more than one variable in LFSC...

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 5af1c2b7e347cd8bcef90aa7e858be8bbafff909..148c5d9e78a71aad31da1751e755881e5bc12822 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -325,11 +325,13 @@ Node LfscNodeConverter::postConvert(Node n)
     // SEXPR to do this, which avoids the need for indexed operators.
     Node ret = n[1];
     Node cop = getOperatorOfClosure(n, true);
+    Node pcop = getOperatorOfClosure(n, true, true);
     for (size_t i = 0, nchild = n[0].getNumChildren(); i < nchild; i++)
     {
       size_t ii = (nchild - 1) - i;
       Node v = n[0][ii];
-      Node vop = getOperatorOfBoundVar(cop, v);
+      // use the partial operator for variables beyond the first
+      Node vop = getOperatorOfBoundVar(ii == 0 ? cop : pcop, v);
       ret = nm->mkNode(APPLY_UF, vop, ret);
     }
     // notice that intentionally we drop annotations here
@@ -993,10 +995,13 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
   return getSymbolInternal(k, ftype, opName.str());
 }
 
-Node LfscNodeConverter::getOperatorOfClosure(Node q, bool macroApply)
+Node LfscNodeConverter::getOperatorOfClosure(Node q,
+                                             bool macroApply,
+                                             bool isPartial)
 {
   NodeManager* nm = NodeManager::currentNM();
-  TypeNode bodyType = nm->mkFunctionType(q[1].getType(), q.getType());
+  TypeNode retType = isPartial ? q[1].getType() : q.getType();
+  TypeNode bodyType = nm->mkFunctionType(q[1].getType(), retType);
   // We permit non-flat function types here
   // intType is used here for variable indices
   TypeNode intType = nm->integerType();

diff --git a/src/proof/lfsc/lfsc_node_converter.h b/src/proof/lfsc/lfsc_node_converter.h
index fefe24d918ad7ddbad1ab6b8658abb98fe850168..07eed996c9fe813f9c4e57e391d942ffca6bc271 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.h
+++ b/src/proof/lfsc/lfsc_node_converter.h
@@ -64,8 +64,20 @@ class LfscNodeConverter : public NodeConverter
    * Get closure operator. In the above example, this method returns the
    * uninterpreted function whose name is "forall" and is used to construct
    * higher-order operators for each bound variable in the closure.
+   *
+   * To ensure typing is correct on converted terms, lambdas require further
+   * care on inner variables. For example:
+   *   (lambda ((x Int) (y Int) (z Int)) 0)
+   * is printed as:
+   *   (apply (lambda N1 Int) (apply (lambda N2 Int) (apply (lambda N3 Int) 0)))
+   * The inner two lambda operators we give type
+   *   (-> Sort Int Int Int)
+   * We call these "partial". Then, the outer lambda is given type:
+   *   (-> Sort Int Int (-> Int Int Int Int))
    */
-  Node getOperatorOfClosure(Node q, bool macroApply = false);
+  Node getOperatorOfClosure(Node q,
+                            bool macroApply = false,
+                            bool isPartial = false);
   /**
    * Get closure operator, where cop is the term returned by
    * getOperatorOfClosure(q), where q is the closures to which v