Implement experimental :match-conclusion for rules

When defining a rule, one can use :match-conclusion instead of
:conclusion.  If this is used, the conclusion must be given in
the step.  To achieve this, define-rule with a
`:match-conclusion T` adds an additional argument `Quote T` to
the start of the argument list, and sets the conclusion to
`Proof T`.  The `step` command detects rules annotated with
`:match-conclusion` and hands the conclusion to the rule as
the first argument.

Hence, this feature doesn't change functional semantic of rules,
it is just syntactic sugar for `step`.

src/attr.cpp

@@ -13,6 +13,10 @@ std::ostream& operator<<(std::ostream& o, Attr a)
     case Attr::SYNTAX: o << "SYNTAX"; break;
     case Attr::REQUIRES: o << "REQUIRES"; break;
     case Attr::PREMISE_LIST: o << "PREMISE_LIST"; break;
+    case Attr::MATCH_CONCLUSION: o << "MATCH_CONCLUSION"; break;
+    case Attr::PREMISE_LIST_MATCH_CONCLUSION:
+      o << "PREMISE_LIST_MATCH_CONCLUSION";
+      break;
     case Attr::PROGRAM: o << "PROGRAM"; break;
     case Attr::ORACLE: o << "ORACLE"; break;
     case Attr::RIGHT_ASSOC: o << "RIGHT_ASSOC"; break;

src/attr.h

@@ -11,7 +11,7 @@ namespace alfc {
 enum class Attr
 {
   NONE = 0,
-  
+
   VAR,
   IMPLICIT,
   REQUIRES,
@@ -21,9 +21,11 @@ enum class Attr
   SYNTAX,
   PROGRAM,
   ORACLE,
-  
+
   // indicate how to construct proof rule steps
   PREMISE_LIST,
+  MATCH_CONCLUSION,
+  PREMISE_LIST_MATCH_CONCLUSION,  // It is possible to have both
 
   // indicate how to construct apps of function symbols
   RIGHT_ASSOC,
@@ -37,7 +39,7 @@ enum class Attr
   DATATYPE,
   DATATYPE_CONSTRUCTOR,
   CODATATYPE,
-  
+
   // internal
   CLOSURE
 };

src/cmd_parser.cpp

@@ -284,6 +284,7 @@ bool CmdParser::parseNextCommand()
       std::vector<Expr> args;
       std::vector<Expr> reqs;
       Expr conc;
+      bool matchConclusion = false;
       if (tok==Token::DECLARE_RULE)
       {
         // parse premises, optionally
@@ -320,10 +321,12 @@ bool CmdParser::parseNextCommand()
           keyword = d_eparser.parseKeyword();
         }
         // parse conclusion
-        if (keyword!="conclusion")
+        if (keyword != "conclusion" && keyword != "match-conclusion")
         {
-          d_lex.parseError("Expected conclusion in declare-rule");
+          d_lex.parseError(
+              "Expected conclusion or match-conclusion in declare-rule");
         }
+        matchConclusion = (keyword == "match-conclusion");
         conc = d_eparser.parseExpr();
       }
       else
@@ -343,6 +346,11 @@ bool CmdParser::parseNextCommand()
         Expr pet = d_state.mkProofType(e);
         argTypes.push_back(pet);
       }
+      if (matchConclusion)
+      {
+        Expr et = d_state.mkQuoteType(conc);
+        argTypes.push_back(et);
+      }
       for (Expr& e : args)
       {
         Expr et = d_state.mkQuoteType(e);
@@ -370,7 +378,23 @@ bool CmdParser::parseNextCommand()
       d_eparser.bind(name, rule);
       if (!plCons.isNull())
       {
-        d_state.markConstructorKind(rule, Attr::PREMISE_LIST, plCons);
+        if (matchConclusion)
+        {
+          d_state.markConstructorKind(
+              rule, Attr::PREMISE_LIST_MATCH_CONCLUSION, plCons);
+        }
+        else
+        {
+          d_state.markConstructorKind(rule, Attr::PREMISE_LIST, plCons);
+        }
+      }
+      else
+      {
+        if (matchConclusion)
+        {
+          d_state.markConstructorKind(
+              rule, Attr::MATCH_CONCLUSION, d_state.mkNil());
+        }
       }
     }
     break;
@@ -696,6 +720,18 @@ bool CmdParser::parseNextCommand()
       }
       // premises before arguments
       children.insert(children.end(), premises.begin(), premises.end());
+      if (d_state.matchesConclusion(rule.getValue()))
+      {
+        Trace("step") << "Matches conclusion " << ruleName << std::endl;
+        if (proven.isNull())
+        {
+          std::stringstream ss;
+          ss << "The proof rule " << ruleName
+             << " expects an explicit conclusion.";
+          d_lex.parseError(ss.str());
+        }
+        children.push_back(proven);
+      }
       for (const Expr& e : args)
       {
         children.push_back(e);

src/expr_parser.cpp

@@ -1197,6 +1197,7 @@ bool ExprParser::processAttributeMap(const AttrMap& attrs, Attr& ck, Expr& cons)
         case Attr::LIST:
         case Attr::SYNTAX:
         case Attr::PREMISE_LIST:
+        case Attr::PREMISE_LIST_MATCH_CONCLUSION:
         case Attr::LEFT_ASSOC:
         case Attr::RIGHT_ASSOC:
         case Attr::LEFT_ASSOC_NIL:

src/state.cpp

@@ -1032,12 +1032,22 @@ Expr State::getProofRule(const std::string& name) const
   return d_null;
 }
 
+bool State::matchesConclusion(const ExprValue* rule)
+{
+  AppInfo* ainfo = getAppInfo(rule);
+  return (ainfo != nullptr
+          && (ainfo->d_attrCons == Attr::MATCH_CONCLUSION
+              || ainfo->d_attrCons == Attr::PREMISE_LIST_MATCH_CONCLUSION));
+}
+
 bool State::getActualPremises(const ExprValue* rule,
                               std::vector<Expr>& given,
                               std::vector<Expr>& actual)
 {
   AppInfo* ainfo = getAppInfo(rule);
-  if (ainfo!=nullptr && ainfo->d_attrCons==Attr::PREMISE_LIST)
+  if (ainfo != nullptr
+      && (ainfo->d_attrCons == Attr::PREMISE_LIST
+          || ainfo->d_attrCons == Attr::PREMISE_LIST_MATCH_CONCLUSION))
   {
     Expr plCons = ainfo->d_attrConsTerm;
     if (!plCons.isNull())

src/state.h

@@ -121,6 +121,8 @@ class State
   Expr getVar(const std::string& name) const;
   /** Get the proof rule with the given name or nullptr if it does not exist */
   Expr getProofRule(const std::string& name) const;
+  /** Returns true if e is a rule that matches on the conclusion */
+  bool matchesConclusion(const ExprValue* rule);
   /** Get actual premises */
   bool getActualPremises(const ExprValue* ev,
                          std::vector<Expr>& given,

tests/CMakeLists.txt

@@ -58,6 +58,7 @@ set(alfc_test_file_list
     nat-type.smt3
     use-match.smt3
     match-simple.smt3
+    match_conclusion.smt3
     and-intro-old.smt3
     strings-rules-test.smt3
     ite-compile-test.smt3

tests/match_conclusion.smt3

@@ -0,0 +1,12 @@
+(include "Builtin-theory.smt3")
+
+(declare-rule match1 ((F1 Bool) (F2 Bool))
+    :match-conclusion (and F1 F2)
+)
+
+(declare-const c1 Bool)
+(declare-const c2 Bool)
+(step test1 (and c1 c2) :rule match1)
+
+; This fails as expected:
+; (step test2 :rule match1)