Support alf.conclusion

src/cmd_parser.cpp

@@ -734,21 +734,32 @@ bool CmdParser::parseNextCommand()
       {
         concType = d_eparser.typeCheck(rule);
       }
-      // ensure proof type, note this is where "proof checking" happens.
+      // if we specified a conclusion, we will possibly evaluate the type
+      // under the substitution `alf.conclusion -> proven`. We only do this
+      // if we did not already match what was proven.
+      if (!proven.isNull())
+      {
+        if (concType.getKind()!=Kind::PROOF_TYPE || concType[0]!=proven)
+        {
+          Ctx cctx;
+          cctx[d_state.mkConclusion().getValue()] = proven.getValue();
+          concType = d_state.getTypeChecker().evaluate(concType.getValue(), cctx);
+        }
+      }
       if (concType.getKind() != Kind::PROOF_TYPE)
       {
+        // ensure proof type, note this is where "proof checking" happens.
         std::stringstream ss;
         ss << "Non-proof conclusion for step, got " << concType;
         d_lex.parseError(ss.str());
       }
       if (!proven.isNull())
       {
-        const Expr& actual = concType[0];
-        if (actual!=proven)
+        if (concType[0]!=proven)
         {
           std::stringstream ss;
           ss << "Unexpected conclusion for step " << ruleName << ":" << std::endl;
-          ss << "    Proves: " << actual << std::endl;
+          ss << "    Proves: " << concType << std::endl;
           ss << "  Expected: " << proven;
           d_lex.parseError(ss.str());
         }

src/expr_parser.cpp

@@ -1227,6 +1227,11 @@ void ExprParser::ensureBound(const Expr& e, const std::vector<Expr>& bvs)
   {
     if (std::find(bvs.begin(), bvs.end(), v)==bvs.end())
     {
+      // ignore distinguished variables
+      if (v==d_state.mkConclusion() || v==d_state.mkSelf())
+      {
+        continue;
+      }
       std::stringstream msg;
       msg << "Unexpected free parameter in expression:" << std::endl;
       msg << "      Expression: " << e << std::endl;

src/state.cpp

@@ -86,6 +86,8 @@ State::State(Options& opts, Stats& stats)
   // self is a distinguished parameter
   d_self = Expr(mkSymbolInternal(Kind::PARAM, "alf.self", mkAbstractType()));
   bind("alf.self", d_self);
+  d_conclusion = Expr(mkSymbolInternal(Kind::PARAM, "alf.conclusion", mkBoolType()));
+  bind("alf.conclusion", d_conclusion);
 
   // note we don't allow parsing (Proof ...), (Quote ...), or (quote ...).
 
@@ -574,6 +576,11 @@ Expr State::mkSelf()
   return d_self;
 }
 
+Expr State::mkConclusion()
+{
+  return d_conclusion;
+}
+
 Expr State::mkNil()
 {
   return d_nil;

src/state.h

@@ -109,6 +109,8 @@ class State
   Expr mkNil();
   /** */
   Expr mkSelf();
+  /** Make the conclusion variable */
+  Expr mkConclusion();
   /** Make pair */
   Expr mkPair(const Expr& t1, const Expr& t2);
   /** */
@@ -175,6 +177,7 @@ class State
   Expr d_true;
   Expr d_false;
   Expr d_self;
+  Expr d_conclusion;
   Expr d_nil;
   Expr d_fail;
   /** Get the constructor kind for symbol v */