From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 10 Jan 2022 22:53:40 +0000 (-0600)
Subject: Fix internal type error when printing lambdas with more than one variable in LFSC... 
X-Git-Tag: cvc5-1.0.0~573
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0218a7f4b0fc0b6b6c066cb675fa55ff34992a1;p=cvc5.git

Fix internal type error when printing lambdas with more than one variable in LFSC (#7909)
---

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 5af1c2b7e..148c5d9e7 100644
--- 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 fefe24d91..07eed996c 100644
--- 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