More

src/attr.cpp

@@ -45,23 +45,34 @@ std::ostream& operator<<(std::ostream& o, Attr a)
   return o;
 }
 
-bool isNAryAttr(Attr a)
+bool isNAryNilAttr(Attr a)
 {
   switch (a)
   {
-    case Attr::LEFT_ASSOC:
-    case Attr::RIGHT_ASSOC:
     case Attr::LEFT_ASSOC_NIL:
     case Attr::RIGHT_ASSOC_NIL:
     case Attr::LEFT_ASSOC_NIL_COLLAPSE:
     case Attr::RIGHT_ASSOC_NIL_COLLAPSE:
+      return true;
+    default:
+      break;
+  }
+  return false;
+}
+
+bool isNAryAttr(Attr a)
+{
+  switch (a)
+  {
+    case Attr::LEFT_ASSOC:
+    case Attr::RIGHT_ASSOC:
     case Attr::CHAINABLE:
     case Attr::PAIRWISE:
       return true;
     default:
       break;
   }
-  return false;
+  return isNAryNilAttr(a);
 }
 
 bool isConstructorKindAttr(Attr a)

src/attr.h

@@ -59,7 +59,11 @@ enum class Attr
 };
 
 /**
- * Is the Attr indicate that any number of children can be passed to the given
+ * Does the Attr indicate a nil terminated n-ary kind?
+ */
+bool isNAryNilAttr(Attr a);
+/**
+ * Does the Attr indicate that any number of children can be passed to the given
  * operator?
  */
 bool isNAryAttr(Attr a);

src/expr_parser.cpp

@@ -1145,6 +1145,8 @@ void ExprParser::parseAttributeList(Kind k, Expr& e, AttrMap& attrs, bool& pushe
             break;
           case Attr::RIGHT_ASSOC_NIL:
           case Attr::LEFT_ASSOC_NIL:
+          case Attr::RIGHT_ASSOC_NIL_COLLAPSE:
+          case Attr::LEFT_ASSOC_NIL_COLLAPSE:
           case Attr::CHAINABLE:
           case Attr::PAIRWISE:
           case Attr::BINDER:

src/state.cpp

@@ -1246,7 +1246,7 @@ bool State::getActualPremises(const ExprValue* rule,
         // the nil terminator if applied to empty list
         AppInfo* aic = getAppInfo(plCons.getValue());
         Attr ck = aic->d_attrCons;
-        if (ck==Attr::RIGHT_ASSOC_NIL || ck==Attr::LEFT_ASSOC_NIL)
+        if (isNAryNilAttr(ck))
         {
           ap = aic->d_attrConsTerm;
         }

src/type_checker.cpp

@@ -1235,12 +1235,12 @@ Expr TypeChecker::evaluateLiteralOpInternal(
     return d_null;
   }
   Attr ck = ac->d_attrCons;
-  if (ck!=Attr::RIGHT_ASSOC_NIL && ck!=Attr::LEFT_ASSOC_NIL)
+  if (!isNAryNilAttr(ck))
   {
     // not an associative operator
     return d_null;
   }
-  bool isLeft = (ck==Attr::LEFT_ASSOC_NIL);
+  bool isLeft = (ck==Attr::LEFT_ASSOC_NIL || ck==Attr::LEFT_ASSOC_NIL_COLLAPSE);
   Trace("type_checker_debug") << "EVALUATE-LIT (list) " << k << " " << isLeft << " " << args << std::endl;
   // infer the nil expression, which depends on the type of args[1]
   std::vector<Expr> eargs;

tests/CMakeLists.txt

@@ -126,6 +126,7 @@ set(ethos_test_file_list
     simple-reference.eo
     simple-quant-reference.eo
     simple-lra-reference.eo
+    rare-example-collapse.eo
 )
 
 if(ENABLE_ORACLES)

tests/rare-example.eo

@@ -11,24 +11,9 @@
   :conclusion (= (or xs true ys) true)
 )
 
-(program elim_singleton_list_rhs ((T Type) (f (-> T T T)) (t T) (s T :list))
-  ((-> T T T) T) T
-  (
-  ((elim_singleton_list_rhs f (f t s)) (eo::ite (eo::is_eq s (eo::nil f)) t (f t s)))
-  ((elim_singleton_list_rhs f t)       t)
-  )
-)
-(program elim_singleton_list_lhs ((T Type) (f (-> T T T)) (t T :list) (s T))
-  ((-> T T T) T) T
-  (
-  ((elim_singleton_list_lhs f (f t s)) (eo::ite (eo::is_eq t (eo::nil f)) s (f t s)))
-  ((elim_singleton_list_lhs f s)       s)
-  )
-)
-
 (declare-rule bool-or-false ((xs Bool :list) (ys Bool :list))
   :args (xs ys)
-  :conclusion (= (or xs false ys) (elim_singleton_list_rhs or (eo::list_concat or xs ys)))
+  :conclusion (= (or xs false ys) (eo::list_collapse or (or xs ys)))
 )
 
 (step @p0 (= (or a b true c) true) :rule bool-or-true :args ((or a b) (or c)))
@@ -41,7 +26,7 @@
 
 (declare-rule bool-and-true ((xs Bool :list) (ys Bool :list))
   :args (xs ys)
-  :conclusion (= (and xs true ys) (elim_singleton_list_lhs and (eo::list_concat and xs ys)))
+  :conclusion (= (and xs true ys) (eo::list_collapse and (and xs ys)))
 )
 
 (declare-rule bool-and-false ((xs Bool :list) (ys Bool :list))