Overload alf.nil instead of using alf.nil_of

cvc5 · Apr 5, 2024 · 33e9ecf · 33e9ecf
1 parent 55cf265
commit 33e9ecf
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 13 deletions.
diff --git a/src/kind.cpp b/src/kind.cpp
@@ -56,7 +56,6 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     // lists
     case Kind::EVAL_NIL: o << "EVAL_NIL";break;
     case Kind::EVAL_CONS: o << "EVAL_CONS"; break;
-    case Kind::EVAL_NIL_OF: o << "EVAL_NIL_OF"; break;
     // boolean
     case Kind::EVAL_NOT: o << "EVAL_NOT"; break;
     case Kind::EVAL_AND: o << "EVAL_AND"; break;
@@ -120,7 +119,6 @@ std::string kindToTerm(Kind k)
         // lists
         case Kind::EVAL_NIL: ss << "nil"; break;
         case Kind::EVAL_CONS: ss << "cons"; break;
-        case Kind::EVAL_NIL_OF: ss << "nil_of"; break;
         // boolean
         case Kind::EVAL_NOT: ss << "not"; break;
         case Kind::EVAL_AND: ss << "and"; break;
@@ -199,7 +197,6 @@ bool isLiteralOp(Kind k)
     // lists
     case Kind::EVAL_NIL:
     case Kind::EVAL_CONS:
-    case Kind::EVAL_NIL_OF:
     // boolean
     case Kind::EVAL_NOT:
     case Kind::EVAL_AND:
@@ -233,7 +230,6 @@ bool isListLiteralOp(Kind k)
   {
     case Kind::EVAL_NIL:
     case Kind::EVAL_CONS:
-    case Kind::EVAL_NIL_OF:
     case Kind::EVAL_CONCAT:
     case Kind::EVAL_EXTRACT:
     case Kind::EVAL_FIND:

diff --git a/src/kind.h b/src/kind.h
@@ -66,9 +66,6 @@ enum class Kind
   // lists
   EVAL_NIL,
   EVAL_CONS,
-  // internal only, (alf.nil_of f t1 ... tn) is the nil terminator of f
-  // applied to t1 ... tn.
-  EVAL_NIL_OF,
   // boolean
   EVAL_NOT,
   EVAL_AND,

diff --git a/src/state.cpp b/src/state.cpp
@@ -643,10 +643,10 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
                 {
                   // if we failed to infer a nil terminator (likely due to
                   // a non-ground parameter), then we insert a placeholder
-                  // (alf.nil_of f t1 ... tn), which if t1...tn are non-ground
+                  // (alf.nil f t1 ... tn), which if t1...tn are non-ground
                   // will evaluate to the proper nil terminator when
                   // instantiated.
-                  curr = mkExprInternal(Kind::EVAL_NIL_OF, vchildren);
+                  curr = mkExprInternal(Kind::EVAL_NIL, vchildren);
                 }
                 else
                 {

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -187,10 +187,9 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_TO_INT:
     case Kind::EVAL_TO_RAT:
     case Kind::EVAL_TO_STRING:
-    case Kind::EVAL_NIL:
       ret = (nargs==1);
       break;
-    case Kind::EVAL_NIL_OF:
+    case Kind::EVAL_NIL:
       ret = (nargs>=1);
       break;
     case Kind::EVAL_REQUIRES:
@@ -1201,7 +1200,6 @@ Expr TypeChecker::evaluateLiteralOpInternal(
   switch (k)
   {
     case Kind::EVAL_NIL:
-    case Kind::EVAL_NIL_OF:
     {
       return nilExpr;
     }
@@ -1447,7 +1445,7 @@ bool TypeChecker::computedParameterizedInternal(AppInfo* ai,
           {
             // If the parameter is non-ground, we also wait to construct;
             // if the nil terminator is used, it will be replaced by a
-            // placeholder involving alf.nil_of.
+            // placeholder involving alf.nil.
             return false;
           }
           args.emplace_back(cv);