Support for alf.as

src/kind.cpp

@@ -36,6 +36,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::NIL: o << "NIL"; break;
     case Kind::PROGRAM: o << "PROGRAM"; break;
     case Kind::COLLECT: o << "COLLECT"; break;
+    case Kind::AS: o << "AS"; break;
     // literals
     case Kind::BOOLEAN: o << "BOOLEAN"; break;
     case Kind::NUMERAL: o << "NUMERAL"; break;
@@ -97,6 +98,7 @@ std::string kindToTerm(Kind k)
     case Kind::APPLY: ss << "@"; break;
     case Kind::LAMBDA: ss << "lambda"; break;
     case Kind::PROGRAM: ss << "program"; break;
+    case Kind::AS: ss << "alf.as"; break;
     // operations on literals
     default:
       if (isLiteralOp(k))

src/kind.h

@@ -35,6 +35,7 @@ enum class Kind
   NIL,
   PROGRAM,
   COLLECT,
+  AS,
 
   // symbols
   PARAM,

src/state.cpp

@@ -78,6 +78,9 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("extract", Kind::EVAL_EXTRACT);
   bindBuiltinEval("find", Kind::EVAL_FIND);
 
+  // as
+  bindBuiltinEval("as", Kind::AS);
+
   d_nil = Expr(mkExprInternal(Kind::NIL, {}));
   bind("alf.nil", d_nil);
   // self is a distinguished parameter
@@ -807,12 +810,53 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
   else if (isLiteralOp(k))
   {
     // only if correct arity, else we will catch the type error
-    if (TypeChecker::checkArity(k, children.size()))
+    if (TypeChecker::checkArity(k, vchildren.size()))
     {
       // return the evaluation
       return d_tc.evaluateLiteralOp(k, vchildren);
     }
   }
+  else if (k==Kind::AS)
+  {
+    // if it has 2 children, process it, otherwise we make the bogus term
+    // below
+    if (vchildren.size()==2)
+    {
+      AppInfo* ai = getAppInfo(vchildren[0]);
+      Expr ret;
+      if (ai!=nullptr && !ai->d_overloads.empty())
+      {
+        size_t arity = 0;
+        Expr cur = children[1];
+        while (cur.getKind()!=Kind::FUNCTION_TYPE)
+        {
+          size_t nchild = cur.getNumChildren();
+          arity += nchild-1;
+          cur = cur[nchild-1];
+        }
+        // look up the overload
+        std::map<size_t, Expr>::iterator ito = ai->d_overloads.find(children.size()-1);
+        if (ito!=ai->d_overloads.end())
+        {
+          ret = ito->second;
+        }
+      }
+      else
+      {
+        ret = children[0];
+      }
+      if (!ret.isNull())
+      {
+        Expr tret = d_tc.getType(ret);
+        // must be matchable
+        Ctx ctx;
+        if (d_tc.match(tret.getValue(), vchildren[1], ctx))
+        {
+          return ret;
+        }
+      }
+    }
+  }
   return Expr(mkExprInternal(k, vchildren));
 }
 

src/type_checker.cpp

@@ -290,6 +290,16 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
       return Expr(ret);
     }
       break;
+    case Kind::AS:
+    {
+      // constructing an application of AS means the type was incorrect.
+      if (out)
+      {
+        (*out) << "Encountered bad type for alf.as";
+      }
+      return d_null;
+    }
+      break;
     default:
       // if a literal operator, consult auxiliary method
       if (isLiteralOp(k))

src/type_checker.h

@@ -77,12 +77,12 @@ class TypeChecker
    * operator does not evaluate.
    */
   Expr evaluateLiteralOp(Kind k, const std::vector<ExprValue*>& args);
- private:
   /**
    * Match expression a with b. If this returns true, then ctx is a substitution
    * that when applied to b gives a. The substitution
    */
   bool match(ExprValue* a, ExprValue* b, Ctx& ctx);
+ private:
   /** Same as above, but takes a cache of pairs we have already visited */
   bool match(ExprValue* a,
              ExprValue* b,

tests/CMakeLists.txt

@@ -102,6 +102,7 @@ set(alfc_test_file_list
     or-concat-false.smt3
     emptylist.smt3
     premise-list-empty.smt3
+    overloading-as.smt3
 )
 
 macro(alfc_test file)

tests/overloading-as.smt3

@@ -0,0 +1,8 @@
+(declare-sort Int 0)
+(declare-const - (-> Int Int Int))
+(declare-const - (-> Int Int))
+
+(declare-const ho_pred (-> (-> Int Int) Bool))
+
+
+(assume @p0 (ho_pred (alf.as - (-> Bool Int))))