From 5b04e6f0b29be4f376ab1f306529bf8a22111bd5 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 14 Dec 2011 22:44:58 +0000
Subject: [PATCH] minor fixes to printing and parsing of CVC-language defined
 functions and lambdas; resolves bug 294

---
 src/expr/expr_template.cpp      |  1 +
 src/parser/cvc/Cvc.g            |  4 +++-
 src/printer/cvc/cvc_printer.cpp | 18 +++++++++++-------
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 29aa1a737..3c376f632 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -206,6 +206,7 @@ Expr Expr::getOperator() const {
 Type Expr::getType(bool check) const throw (TypeCheckingException) {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  CheckArgument(!d_node->isNull(), this, "Can't get type of null expression!");
   return d_exprManager->getType(*this, check);
 }
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2d659cfe3..9f0c2cddb 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -897,6 +897,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
           }
         }
       } else {
+        // f is not null-- meaning this is a definition not a declaration
         if(!topLevel) {
           // must be top-level; doesn't make sense to write something
           // like e.g. FORALL(x:INT = 4): [...]
@@ -908,8 +909,9 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
             i != i_end;
             ++i) {
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
+          Expr func = EXPR_MANAGER->mkVar(*i, f.getType());
           PARSER_STATE->defineFunction(*i, f);
-          Command* decl = new DefineFunctionCommand(*i, Expr(), f);
+          Command* decl = new DefineFunctionCommand(*i, func, f);
           seq->addCommand(decl);
         }
       }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 0d47c9c6c..8d76a7332 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -484,15 +484,19 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
   Expr func = c->getFunction();
   const vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
-  out << func << " : " << func.getType() << " = LAMBDA(";
-  vector<Expr>::const_iterator i = formals.begin();
-  while(i != formals.end()) {
-    out << (*i) << ":" << (*i).getType();
-    if(++i != formals.end()) {
-      out << ", ";
+  out << func << " : " << func.getType() << " = ";
+  if(formals.size() > 0) {
+    out << "LAMBDA(";
+    vector<Expr>::const_iterator i = formals.begin();
+    while(i != formals.end()) {
+      out << (*i) << ":" << (*i).getType();
+      if(++i != formals.end()) {
+        out << ", ";
+      }
     }
+    out << "): ";
   }
-  out << "): " << formula << ";";
+  out << formula << ";";
 }
 
 static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
-- 
2.30.2