From 007838166ca082168b9992c54486ffdc2e00c84b Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 29 Feb 2024 19:08:16 -0600
Subject: [PATCH] Support alf.conclusion

---
 src/cmd_parser.cpp  | 19 +++++++++++++++----
 src/expr_parser.cpp |  5 +++++
 src/state.cpp       |  7 +++++++
 src/state.h         |  3 +++
 4 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp
index 08ffe627..e0813d57 100644
--- a/src/cmd_parser.cpp
+++ b/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());
         }
diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
index c85e25fc..7420419e 100644
--- a/src/expr_parser.cpp
+++ b/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;
diff --git a/src/state.cpp b/src/state.cpp
index 1006d7e1..d4d81ec5 100644
--- a/src/state.cpp
+++ b/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;
diff --git a/src/state.h b/src/state.h
index 63d3058a..2f922873 100644
--- a/src/state.h
+++ b/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 */