refactor(library/init): simplify has_emptyc type class

library/init/core.lean

@@ -217,7 +217,7 @@ class has_ssubset  (A : Type u) := (ssubset : A → A → Prop)
 /- Type classes has_emptyc and has_insert are
    used to implement polymorphic notation for collections.
    Example: {a, b, c}. -/
-class has_emptyc   (A : Type u) (C : Type u → Type v) := (emptyc : C A)
+class has_emptyc   (A : Type u) := (emptyc : A)
 class has_insert   (A : Type u) (C : Type u → Type v) := (insert : A → C A → C A)
 /- Type class used to implement the notation { a ∈ c | p a } -/
 class has_sep (A : Type u) (C : Type u → Type v) :=
@@ -261,10 +261,10 @@ def insert {A : Type u} {C : Type u → Type v} [has_insert A C] : A → C A →
 has_insert.insert
 
 /- The empty collection -/
-def emptyc {A : Type u} {C : Type u → Type v} [has_emptyc A C] : C A :=
-has_emptyc.emptyc A C
+def emptyc {A : Type u} [has_emptyc A] : A :=
+has_emptyc.emptyc A
 
-def singleton {A : Type u} {C : Type u → Type v} [has_emptyc A C] [has_insert A C] (a : A) : C A :=
+def singleton {A : Type u} {C : Type u → Type v} [has_emptyc (C A)] [has_insert A C] (a : A) : C A :=
 insert a emptyc
 
 def sep {A : Type u} {C : Type u → Type v} [has_sep A C] : (A → Prop) → C A → C A :=

library/init/list.lean

@@ -45,7 +45,7 @@ def concat : list A → A → list A
 | []     a := [a]
 | (b::l) a := b :: concat l a
 
-instance : has_emptyc A list :=
+instance : has_emptyc (list A) :=
 ⟨list.nil⟩
 
 protected def insert [decidable_eq A] (a : A) (l : list A) : list A :=

library/init/set.lean

@@ -34,7 +34,7 @@ protected def sep (p : A → Prop) (s : set A) : set A :=
 instance : has_sep A set :=
 ⟨set.sep⟩
 
-instance : has_emptyc A set :=
+instance : has_emptyc (set A) :=
 ⟨λ a, false⟩
 
 protected def insert (a : A) (s : set A) : set A :=

src/frontends/lean/pp.cpp

@@ -1474,6 +1474,12 @@ auto pretty_fn::pp_subtype(expr const & e) -> result {
     return result(r);
 }
 
+static bool is_emptyc(expr const & e) {
+    return
+        is_constant(get_app_fn(e), get_emptyc_name()) &&
+        get_app_num_args(e) == 2;
+}
+
 static bool is_singleton(expr const & e) {
     return
         is_constant(get_app_fn(e), get_singleton_name()) &&
@@ -1489,7 +1495,9 @@ static bool is_insert(expr const & e) {
 /* Return true iff 'e' encodes a nonempty finite collection,
    and stores its elements at elems. */
 static bool is_explicit_collection(expr const & e, buffer<expr> & elems) {
-    if (is_singleton(e)) {
+    if (is_emptyc(e)) {
+        return true;
+    } else if (is_singleton(e)) {
         elems.push_back(app_arg(e));
         return true;
     } else if (is_insert(e) && is_explicit_collection(app_arg(e), elems)) {
@@ -1501,13 +1509,16 @@ static bool is_explicit_collection(expr const & e, buffer<expr> & elems) {
 }
 
 auto pretty_fn::pp_explicit_collection(buffer<expr> const & elems) -> result {
-    lean_assert(!elems.empty());
-    format r = pp_child(elems[0], 0).fmt();
-    for (unsigned i = 1; i < elems.size(); i++) {
-        r += nest(m_indent, comma() + line() + pp_child(elems[i], 0).fmt());
+    if (elems.empty()) {
+        return result(format(m_unicode ? "∅" : "{}"));
+    } else {
+        format r = pp_child(elems[0], 0).fmt();
+        for (unsigned i = 1; i < elems.size(); i++) {
+            r += nest(m_indent, comma() + line() + pp_child(elems[i], 0).fmt());
+        }
+        r = group(bracket("{", r, "}"));
+        return result(r);
     }
-    r = group(bracket("{", r, "}"));
-    return result(r);
 }
 
 bool is_set_of(expr const & e) {

tests/lean/struct_class.lean.expected.out

@@ -11,7 +11,7 @@ has_coe_to_fun : Type u → Type (max u (v+1))
 has_coe_to_sort : Type u → Type (max u (v+1))
 has_div : Type u → Type (max 1 u)
 has_dvd : Type u → Type (max 1 u)
-has_emptyc : Type u → (Type u → Type v) → Type (max 1 v)
+has_emptyc : Type u → Type (max 1 u)
 has_insert : Type u → (Type u → Type v) → Type (max 1 (imax u v))
 has_inter : Type u → Type (max 1 u)
 has_inv : Type u → Type (max 1 u)
@@ -57,7 +57,7 @@ has_coe_to_fun : Type u → Type (max u (v+1))
 has_coe_to_sort : Type u → Type (max u (v+1))
 has_div : Type u → Type (max 1 u)
 has_dvd : Type u → Type (max 1 u)
-has_emptyc : Type u → (Type u → Type v) → Type (max 1 v)
+has_emptyc : Type u → Type (max 1 u)
 has_insert : Type u → (Type u → Type v) → Type (max 1 (imax u v))
 has_inter : Type u → Type (max 1 u)
 has_inv : Type u → Type (max 1 u)