Add support for define attribute :is_eq

NEWS.md

@@ -7,9 +7,11 @@ ethos 0.2.3 prerelease
 - Updates to the external plugin interface.
 - The identifier `Type` is no longer treated as a keyword in proofs and reference files.
 - The command `declare-sort` is now allowed in proof files.
+- Adds support for an attribute `:is_eq` to test whether a defined term is equal to another.
 - Fixes a bug where the character code point `\u{30000}` was incorrectly
   treated as a valid code point.
 
+
 ethos 0.2.2
 ===========
 

src/attr.cpp

@@ -17,6 +17,7 @@ std::ostream& operator<<(std::ostream& o, Attr a)
     case Attr::NONE: o << "NONE"; break;
     case Attr::IMPLICIT: o << "implicit"; break;
     case Attr::TYPE: o << "type"; break;
+    case Attr::IS_EQ: o << "is_eq"; break;
     case Attr::SORRY: o << "sorry"; break;
     case Attr::LIST: o << "list"; break;
     case Attr::PROOF_RULE: o << "proof_rule"; break;

src/attr.h

@@ -21,7 +21,9 @@ enum class Attr
   NONE = 0,
 
   IMPLICIT,
+  // inspecting define
   TYPE,
+  IS_EQ,
   // properties of rules
   SORRY,
 

src/expr_parser.cpp

@@ -64,6 +64,7 @@ ExprParser::ExprParser(Lexer& lex, State& state, bool isSignature)
     : d_lex(lex), d_state(state), d_isSignature(isSignature)
 {
   d_strToAttr[":implicit"] = Attr::IMPLICIT;
+  d_strToAttr[":is_eq"] = Attr::IS_EQ;
   d_strToAttr[":type"] = Attr::TYPE;
   d_strToAttr[":list"] = Attr::LIST;
   d_strToAttr[":left-assoc"] = Attr::LEFT_ASSOC;
@@ -1075,15 +1076,27 @@ void ExprParser::parseAttributeList(
         break;
       case Kind::LAMBDA:
       {
-        // only :type is available in define
+        Assert(!e.isNull());
         if (a==Attr::TYPE)
         {
-          Assert (!e.isNull());
           handled = true;
           val = parseExpr();
           // run type checking
           typeCheck(e, val);
         }
+        else if (a == Attr::IS_EQ)
+        {
+          handled = true;
+          val = parseExpr();
+          if (e != val)
+          {
+            std::stringstream msg;
+            msg << "Terms are not equal:" << std::endl;
+            msg << "Expression: " << e << std::endl;
+            msg << "Target expression: " << val << std::endl;
+            d_lex.parseError(msg.str());
+          }
+        }
       }
         break;
       default:

tests/CMakeLists.txt

@@ -123,6 +123,7 @@ set(ethos_test_file_list
     disamb-arith.eo
     opaque-inline.eo
     implicit-then-var.eo
+    is_eq.eo
     simple-reference.eo
     simple-quant-reference.eo
     simple-lra-reference.eo

tests/is_eq.eo

@@ -0,0 +1,3 @@
+
+(define test () (eo::add 1 1) :is_eq 2)
+