Remove deprecated kind

cvc5 · Jun 5, 2024 · 3da9738 · 3da9738
1 parent 3aab53b
commit 3da9738
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 24 deletions.
diff --git a/src/kind.cpp b/src/kind.cpp
@@ -34,7 +34,6 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::VARIABLE: o << "VARIABLE"; break;
     case Kind::ORACLE: o << "ORACLE"; break;
     case Kind::TUPLE: o << "TUPLE"; break;
-    case Kind::NULL_EXPR: o << "NIL"; break;
     case Kind::PROGRAM: o << "PROGRAM"; break;
     case Kind::AS: o << "AS"; break;
     case Kind::PARAMETERIZED: o << "PARAMETERIZED"; break;
@@ -101,7 +100,6 @@ std::string kindToTerm(Kind k)
     case Kind::ABSTRACT_TYPE: ss << "?"; break;
     case Kind::BOOL_TYPE: ss << "Bool"; break;
     case Kind::QUOTE_TYPE: ss << "Quote"; break;
-    case Kind::NULL_EXPR: ss << "alf.nil"; break;
     case Kind::TUPLE: ss << "alf.tuple"; break;
     // terms
     case Kind::APPLY: ss << "_"; break;

diff --git a/src/kind.h b/src/kind.h
@@ -33,7 +33,6 @@ enum class Kind
   APPLY,
   LAMBDA,
   TUPLE,
-  NULL_EXPR,
   PROGRAM,
   AS,
   PARAMETERIZED,

diff --git a/src/state.cpp b/src/state.cpp
@@ -89,7 +89,6 @@ State::State(Options& opts, Stats& stats)
   // as
   bindBuiltinEval("as", Kind::AS);
 
-  d_nullExpr = Expr(mkExprInternal(Kind::NULL_EXPR, {}));
   // we do not export alf.null
   // for now, alf.? is (undocumented) syntax for abstract type
   bind("alf.?", mkAbstractType());
@@ -503,11 +502,6 @@ Expr State::mkConclusion()
   return d_conclusion;
 }
 
-Expr State::mkNil()
-{
-  return d_nullExpr;
-}
-
 Expr State::mkPair(const Expr& t1, const Expr& t2)
 {
   return Expr(mkExprInternal(Kind::TUPLE, {t1.getValue(), t2.getValue()}));
@@ -626,8 +620,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
             std::vector<ExprValue*> cc{hd, nullptr, nullptr};
             size_t nextIndex = isLeft ? 2 : 1;
             size_t prevIndex = isLeft ? 1 : 2;
-            // note the nil element is always treated as a list
-            if (curr->getKind()!=Kind::NULL_EXPR && isNil)
+            if (isNil)
             {
               if (getConstructorKind(curr) != Attr::LIST)
               {

diff --git a/src/state.h b/src/state.h
@@ -109,8 +109,6 @@ class State
   Expr mkRequires(const std::vector<Expr>& args, const Expr& ret);
   /** (alf.requires <arg1> <arg2> <type>) */
   Expr mkRequires(const Expr& a1, const Expr& a2, const Expr& ret);
-  /** alf.nil */
-  Expr mkNil();
   /** */
   Expr mkSelf();
   /** Make the conclusion variable */
@@ -194,7 +192,6 @@ class State
   Expr d_false;
   Expr d_self;
   Expr d_conclusion;
-  Expr d_nullExpr;
   Expr d_fail;
   /** Get base operator */
   const ExprValue* getBaseOperator(const ExprValue * v) const;

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -134,9 +134,6 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
   // check arities
   switch(k)
   {
-    case Kind::NULL_EXPR:
-      ret = (nargs==0);
-      break;
     case Kind::EVAL_IS_EQ:
     case Kind::EVAL_VAR:
     case Kind::EVAL_INT_DIV:
@@ -227,13 +224,6 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
       Assert(!ret.isNull());
       return d_state.mkFunctionType(args, ret);
     }
-    case Kind::NULL_EXPR:
-      if (!checkArity(k, e->getNumChildren(), out))
-      {
-        return d_null;
-      }
-      // nil is its own type
-      return Expr(e);
     case Kind::TYPE:
     case Kind::ABSTRACT_TYPE:
     case Kind::BOOL_TYPE:
-Original file line number
+Diff line change
@@ Expand Up / @@ -33,7 +33,6 @@ enum class Kind @@
       APPLY,
       LAMBDA,
       TUPLE,
-      NULL_EXPR,
       PROGRAM,
       AS,
       PARAMETERIZED,
@@ Expand Down @@