From c0ff9967af2e0dc79b00eedc113bebba6543d628 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 Sep 2016 16:12:22 -0700
Subject: [PATCH] feat(frontends/lean): add basic notation for collections

---
 library/init/default.lean               |   2 +-
 library/init/subtype.lean               |  18 ++--
 src/frontends/lean/CMakeLists.txt       |   3 +-
 src/frontends/lean/brackets.cpp         | 130 ++++++++++++++++++++++++
 src/frontends/lean/brackets.h           |  11 ++
 src/frontends/lean/builtin_exprs.cpp    |   2 +
 src/frontends/lean/pp.cpp               |  62 +++++++++++
 src/frontends/lean/pp.h                 |   2 +
 src/frontends/lean/token_table.cpp      |   2 +-
 src/frontends/lean/tokens.cpp           |  12 +++
 src/frontends/lean/tokens.h             |   3 +
 src/frontends/lean/tokens.txt           |   3 +
 src/library/constants.cpp               |  16 +++
 src/library/constants.h                 |   4 +
 src/library/constants.txt               |   4 +
 tests/lean/pattern_pp.lean              |  13 ---
 tests/lean/pattern_pp.lean.expected.out |   3 -
 tests/lean/print_ax1.lean.expected.out  |   2 +-
 tests/lean/print_ax2.lean.expected.out  |   2 +-
 tests/lean/print_ax3.lean.expected.out  |   2 +-
 tests/lean/run/curly_notation.lean      |  12 +++
 tests/lean/run/pattern2.lean            |  18 ----
 tests/lean/run/pattern3.lean            |   7 --
 tests/lean/run/print_no_pattern.lean    |   1 -
 tests/lean/subpp.lean.expected.out      |   2 +-
 25 files changed, 277 insertions(+), 59 deletions(-)
 create mode 100644 src/frontends/lean/brackets.cpp
 create mode 100644 src/frontends/lean/brackets.h
 delete mode 100644 tests/lean/pattern_pp.lean
 delete mode 100644 tests/lean/pattern_pp.lean.expected.out
 create mode 100644 tests/lean/run/curly_notation.lean
 delete mode 100644 tests/lean/run/pattern2.lean
 delete mode 100644 tests/lean/run/pattern3.lean
 delete mode 100644 tests/lean/run/print_no_pattern.lean

diff --git a/library/init/default.lean b/library/init/default.lean
index df9b1fc5f9..1813b34d46 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -9,7 +9,7 @@ import init.relation init.nat init.prod init.sum init.combinator
 import init.bool init.unit init.num init.sigma init.setoid init.quot
 import init.funext init.function init.subtype init.classical
 import init.monad init.option init.state init.fin init.list init.char init.string init.to_string
-import init.monad_combinators
+import init.monad_combinators init.set
 import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
 import init.wf init.nat_div init.meta init.instances
 import init.wf_k init.sigma_lex
diff --git a/library/init/subtype.lean b/library/init/subtype.lean
index 6bd3b6e6b4..89e632ddf5 100644
--- a/library/init/subtype.lean
+++ b/library/init/subtype.lean
@@ -9,30 +9,28 @@ open decidable
 
 universe variables u
 
-structure subtype {A : Type u} (P : A → Prop) :=
-tag :: (elt_of : A) (has_property : P elt_of)
-
-notation `{` binder ` \ `:0 r:(scoped:1 P, subtype P) `}` := r
+structure subtype {A : Type u} (p : A → Prop) :=
+tag :: (elt_of : A) (has_property : p elt_of)
 
 namespace subtype
 
-  definition exists_of_subtype {A : Type u} {P : A → Prop} : { x \ P x } → ∃ x, P x
+  definition exists_of_subtype {A : Type u} {p : A → Prop} : { x \ p x } → ∃ x, p x
   | ⟨a, h⟩ := ⟨a, h⟩
 
-  variables {A : Type u} {P : A → Prop}
+  variables {A : Type u} {p : A → Prop}
 
-  theorem tag_irrelevant {a : A} (h1 h2 : P a) : tag a h1 = tag a h2 :=
+  theorem tag_irrelevant {a : A} (h1 h2 : p a) : tag a h1 = tag a h2 :=
   rfl
 
-  protected theorem eq : ∀ {a1 a2 : {x \ P x}}, elt_of a1 = elt_of a2 → a1 = a2
+  protected theorem eq : ∀ {a1 a2 : {x \ p x}}, elt_of a1 = elt_of a2 → a1 = a2
   | ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
 
 end subtype
 
 open subtype
 
-variables {A : Type u} {P : A → Prop}
+variables {A : Type u} {p : A → Prop}
 
 attribute [instance]
-protected definition subtype.is_inhabited {a : A} (h : P a) : inhabited {x \ P x} :=
+protected definition subtype.is_inhabited {a : A} (h : p a) : inhabited {x \ p x} :=
 ⟨⟨a, h⟩⟩
diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index f5757cde81..caffde5211 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -6,4 +6,5 @@ inductive_cmds.cpp dependencies.cpp
 pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
 opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp
-match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp)
+match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
+brackets.cpp)
diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp
new file mode 100644
index 0000000000..b4cba07eab
--- /dev/null
+++ b/src/frontends/lean/brackets.cpp
@@ -0,0 +1,130 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/abstract.h"
+#include "library/constants.h"
+#include "library/placeholder.h"
+#include "frontends/lean/parser.h"
+#include "frontends/lean/util.h"
+#include "frontends/lean/tokens.h"
+
+namespace lean {
+/* Parse rest of the subtype expression prefix '{' id ':' expr '\' ... */
+static expr parse_subtype(parser & p, pos_info const & pos, expr const & local) {
+    parser::local_scope scope(p);
+    p.add_local(local);
+    expr pred    = p.parse_expr();
+    p.check_token_next(get_rcurly_tk(), "invalid subtype, '}' expected");
+    pred         = p.save_pos(Fun(local, pred), pos);
+    expr subtype = p.save_pos(mk_constant(get_subtype_name()), pos);
+    return p.mk_app(subtype, pred, pos);
+}
+
+/* Create empty collection for '{' '}' */
+static expr mk_empty_collection(parser & p, pos_info const & pos) {
+    return p.save_pos(mk_constant(get_empty_col_name()), pos);
+}
+
+/* Create singletoncollection for '{' expr '}' */
+static expr mk_singleton(parser & p, pos_info const & pos, expr const & e) {
+    return p.mk_app(p.save_pos(mk_constant(get_singleton_name()), pos), e, pos);
+}
+
+/* Parse rest of the insertable '{' expr ... */
+static expr parse_insertable(parser & p, pos_info const & pos, expr const & e) {
+    lean_assert(p.curr_is_token(get_comma_tk()));
+    expr r = mk_singleton(p, pos, e);
+    while (p.curr_is_token(get_comma_tk())) {
+        auto ins_pos = p.pos();
+        p.next();
+        expr e2 = p.parse_expr();
+        expr insert = p.save_pos(mk_constant(get_insert_name()), ins_pos);
+        r = p.rec_save_pos(mk_app(insert, e2, r), ins_pos);
+    }
+    p.check_token_next(get_rcurly_tk(), "invalid explicit finite collection, '}' expected");
+    return r;
+}
+
+/* Parse rest of the qualified structure instance prefix '{' S '.' ... */
+static expr parse_qualified_structure_instance(parser & p, pos_info const & pos, name const & S) {
+    throw parser_error("qualified strucuture instance was not implemented yet", pos);
+}
+
+/* Parse rest of the structure instance prefix '{' fname ... */
+static expr parse_structure_instance(parser & p, pos_info const & pos, name const & fname) {
+    throw parser_error("strucuture instance was not implemented yet", pos);
+}
+
+/* Parse rest of the structure instance update '{' expr 'with' ... */
+static expr parse_structure_instance_update(parser & p, pos_info const & pos, expr const & e) {
+    throw parser_error("strucuture instance update was not implemented yet", pos);
+}
+
+/* Parse rest of the monadic comprehension expression '{' expr '|' ... */
+static expr parse_monadic_comprehension(parser & p, pos_info const & pos, expr const & e) {
+    throw parser_error("monadic comprehension was not implemented yet", pos);
+}
+
+/* Parse rest of the sep expression '{' id '∈' ... */
+static expr parse_sep(parser & p, pos_info const & pos, name const & id) {
+    throw parser_error("sep was not implemented yet", pos);
+}
+
+expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & pos) {
+    expr e;
+    if (p.curr_is_token(get_rcurly_tk())) {
+        p.next();
+        return mk_empty_collection(p, pos);
+    } else if (p.curr_is_identifier()) {
+        auto id_pos = p.pos();
+        name id     = p.get_name_val();
+        p.next();
+        if (p.curr_is_token(get_backslash_tk())) {
+            expr type  = p.save_pos(mk_expr_placeholder(), id_pos);
+            expr local = p.save_pos(mk_local(id, type), id_pos);
+            p.next();
+            return parse_subtype(p, pos, local);
+        } else if (p.curr_is_token(get_colon_tk())) {
+            p.next();
+            expr type  = p.parse_expr();
+            expr local = p.save_pos(mk_local(id, type), id_pos);
+            p.check_token_next(get_backslash_tk(), "invalid subtype, '\' expected");
+            return parse_subtype(p, pos, local);
+        } else if (p.curr_is_token(get_period_tk())) {
+            p.next();
+            return parse_qualified_structure_instance(p, pos, id);
+        } else if (p.curr_is_token(get_assign_tk()) || p.curr_is_token(get_fieldarrow_tk())) {
+            return parse_structure_instance(p, pos, id);
+        } else if (p.curr_is_token(get_membership_tk())) {
+            p.next();
+            return parse_sep(p, pos, id);
+        } else {
+            expr left = p.id_to_expr(id, id_pos);
+            unsigned rbp = 0;
+            while (rbp < p.curr_lbp()) {
+                left = p.parse_led(left);
+            }
+            e = left;
+        }
+    } else {
+        e = p.parse_expr();
+    }
+
+    if (p.curr_is_token(get_comma_tk())) {
+        return parse_insertable(p, pos, e);
+    } else if (p.curr_is_token(get_rcurly_tk())) {
+        return parse_insertable(p, pos, e);
+    } else if (p.curr_is_token(get_with_tk())) {
+        p.next();
+        return parse_structure_instance_update(p, pos, e);
+    } else if (p.curr_is_token(get_bar_tk())) {
+        p.next();
+        return parse_monadic_comprehension(p, pos, e);
+    } else {
+        throw parser_error("invalid '{' expression, ',', '}', 'with', `\\` or `|` expected", p.pos());
+    }
+}
+}
diff --git a/src/frontends/lean/brackets.h b/src/frontends/lean/brackets.h
new file mode 100644
index 0000000000..e1fd2dce34
--- /dev/null
+++ b/src/frontends/lean/brackets.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "frontends/lean/parser.h"
+namespace lean {
+expr parse_curly_bracket(parser & p, unsigned, expr const * args, pos_info const & pos);
+}
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index b0a4a59029..fb2f082a33 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/decl_util.h"
+#include "frontends/lean/brackets.h"
 
 #ifndef LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE
 #define LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE true
@@ -750,6 +751,7 @@ parse_table init_nud_table() {
     r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
     r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0);
     r = r.add({transition("⟨", mk_ext_action(parse_constructor))}, x0);
+    r = r.add({transition("{", mk_ext_action(parse_curly_bracket))}, x0);
     r = r.add({transition("`(", mk_ext_action(parse_quoted_expr))}, x0);
     r = r.add({transition("`", mk_ext_action(parse_quoted_name))}, x0);
     r = r.add({transition("%%", mk_ext_action(parse_antiquote_expr))}, x0);
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index aac741d5e8..e3bf1e2d38 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1456,6 +1456,60 @@ auto pretty_fn::pp_proof_type(expr const & t) -> result {
     return result(group(nest(1, li + pp(t).fmt() + ri)));
 }
 
+static bool is_subtype(expr const & e) {
+    return
+        is_constant(get_app_fn(e), get_subtype_name()) &&
+        get_app_num_args(e) == 2 &&
+        is_lambda(app_arg(e));
+}
+
+auto pretty_fn::pp_subtype(expr const & e) -> result {
+    lean_assert(is_subtype(e));
+    expr pred = app_arg(e);
+    lean_assert(is_lambda(pred));
+    auto p     = binding_body_fresh(pred, true);
+    expr body  = p.first;
+    expr local = p.second;
+    format r   = bracket("{", format(local_pp_name(local)) + space() + format("\\") + space() + pp_child(body, 0).fmt(), "}");
+    return result(r);
+}
+
+static bool is_singleton(expr const & e) {
+    return
+        is_constant(get_app_fn(e), get_singleton_name()) &&
+        get_app_num_args(e) == 4;
+}
+
+static bool is_insert(expr const & e) {
+    return
+        is_constant(get_app_fn(e), get_insert_name()) &&
+        get_app_num_args(e) == 5;
+}
+
+/* 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)) {
+        elems.push_back(app_arg(e));
+        return true;
+    } else if (is_insert(e) && is_explicit_collection(app_arg(e), elems)) {
+        elems.push_back(app_arg(app_fn(e)));
+        return true;
+    } else {
+        return false;
+    }
+}
+
+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());
+    }
+    r = group(bracket("{", r, "}"));
+    return result(r);
+}
+
 auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     check_system("pretty printer");
     if ((m_depth >= m_max_depth ||
@@ -1481,6 +1535,14 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     if (auto r = pp_notation(e))
         return *r;
 
+    if (m_notation) {
+        if (is_subtype(e))
+            return pp_subtype(e);
+        buffer<expr> elems;
+        if (is_explicit_collection(e, elems))
+            return pp_explicit_collection(elems);
+    }
+
     if (is_placeholder(e))  return result(*g_placeholder_fmt);
     if (is_show(e))         return pp_show(e);
     if (is_have(e))         return pp_have(e);
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 053b8ccc01..817005f45a 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -114,6 +114,8 @@ private:
     result pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hide = false);
     result pp_child_core(expr const & e, unsigned bp, bool ignore_hide = false);
     result pp_child(expr const & e, unsigned bp, bool ignore_hide = false);
+    result pp_subtype(expr const & e);
+    result pp_explicit_collection(buffer<expr> const & elems);
     result pp_var(expr const & e);
     result pp_sort(expr const & e);
     result pp_const(expr const & e, optional<unsigned> const & num_ref_univs = optional<unsigned>());
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 2fa6cae184..e0af4fb34f 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -87,7 +87,7 @@ void init_token_table(token_table & t) {
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type*", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
-         {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
+         {"\\", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
          {"@@", g_max_prec}, {"@", g_max_prec},
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 3123f9bf30..9e5f63e247 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -6,6 +6,8 @@ namespace lean{
 static name const * g_aliases_tk = nullptr;
 static name const * g_period_tk = nullptr;
 static name const * g_backtick_tk = nullptr;
+static name const * g_backslash_tk = nullptr;
+static name const * g_fieldarrow_tk = nullptr;
 static name const * g_placeholder_tk = nullptr;
 static name const * g_colon_tk = nullptr;
 static name const * g_semicolon_tk = nullptr;
@@ -36,6 +38,7 @@ static name const * g_slash_tk = nullptr;
 static name const * g_plus_tk = nullptr;
 static name const * g_star_tk = nullptr;
 static name const * g_turnstile_tk = nullptr;
+static name const * g_membership_tk = nullptr;
 static name const * g_explicit_tk = nullptr;
 static name const * g_partial_explicit_tk = nullptr;
 static name const * g_max_tk = nullptr;
@@ -124,6 +127,8 @@ void initialize_tokens() {
     g_aliases_tk = new name{"aliases"};
     g_period_tk = new name{"."};
     g_backtick_tk = new name{"`"};
+    g_backslash_tk = new name{"\\"};
+    g_fieldarrow_tk = new name{"~>"};
     g_placeholder_tk = new name{"_"};
     g_colon_tk = new name{":"};
     g_semicolon_tk = new name{";"};
@@ -154,6 +159,7 @@ void initialize_tokens() {
     g_plus_tk = new name{"+"};
     g_star_tk = new name{"*"};
     g_turnstile_tk = new name{"⊢"};
+    g_membership_tk = new name{"∈"};
     g_explicit_tk = new name{"@"};
     g_partial_explicit_tk = new name{"@@"};
     g_max_tk = new name{"max"};
@@ -243,6 +249,8 @@ void finalize_tokens() {
     delete g_aliases_tk;
     delete g_period_tk;
     delete g_backtick_tk;
+    delete g_backslash_tk;
+    delete g_fieldarrow_tk;
     delete g_placeholder_tk;
     delete g_colon_tk;
     delete g_semicolon_tk;
@@ -273,6 +281,7 @@ void finalize_tokens() {
     delete g_plus_tk;
     delete g_star_tk;
     delete g_turnstile_tk;
+    delete g_membership_tk;
     delete g_explicit_tk;
     delete g_partial_explicit_tk;
     delete g_max_tk;
@@ -361,6 +370,8 @@ void finalize_tokens() {
 name const & get_aliases_tk() { return *g_aliases_tk; }
 name const & get_period_tk() { return *g_period_tk; }
 name const & get_backtick_tk() { return *g_backtick_tk; }
+name const & get_backslash_tk() { return *g_backslash_tk; }
+name const & get_fieldarrow_tk() { return *g_fieldarrow_tk; }
 name const & get_placeholder_tk() { return *g_placeholder_tk; }
 name const & get_colon_tk() { return *g_colon_tk; }
 name const & get_semicolon_tk() { return *g_semicolon_tk; }
@@ -391,6 +402,7 @@ name const & get_slash_tk() { return *g_slash_tk; }
 name const & get_plus_tk() { return *g_plus_tk; }
 name const & get_star_tk() { return *g_star_tk; }
 name const & get_turnstile_tk() { return *g_turnstile_tk; }
+name const & get_membership_tk() { return *g_membership_tk; }
 name const & get_explicit_tk() { return *g_explicit_tk; }
 name const & get_partial_explicit_tk() { return *g_partial_explicit_tk; }
 name const & get_max_tk() { return *g_max_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 3730f71b5a..983cefa24b 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -8,6 +8,8 @@ void finalize_tokens();
 name const & get_aliases_tk();
 name const & get_period_tk();
 name const & get_backtick_tk();
+name const & get_backslash_tk();
+name const & get_fieldarrow_tk();
 name const & get_placeholder_tk();
 name const & get_colon_tk();
 name const & get_semicolon_tk();
@@ -38,6 +40,7 @@ name const & get_slash_tk();
 name const & get_plus_tk();
 name const & get_star_tk();
 name const & get_turnstile_tk();
+name const & get_membership_tk();
 name const & get_explicit_tk();
 name const & get_partial_explicit_tk();
 name const & get_max_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index ea03231d77..47a30ab02f 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -1,6 +1,8 @@
 aliases      aliases
 period       .
 backtick     `
+backslash    \\
+fieldarrow   ~>
 placeholder  _
 colon        :
 semicolon    ;
@@ -31,6 +33,7 @@ slash        /
 plus         +
 star         *
 turnstile    ⊢
+membership   ∈
 explicit     @
 partial_explicit @@
 max          max
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 0ed75a5669..f54288a329 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -52,6 +52,7 @@ name const * g_div = nullptr;
 name const * g_id = nullptr;
 name const * g_empty = nullptr;
 name const * g_empty_rec = nullptr;
+name const * g_empty_col = nullptr;
 name const * g_Exists = nullptr;
 name const * g_eq = nullptr;
 name const * g_eq_drec = nullptr;
@@ -119,6 +120,7 @@ name const * g_implies = nullptr;
 name const * g_implies_of_if_neg = nullptr;
 name const * g_implies_of_if_pos = nullptr;
 name const * g_implies_resolve = nullptr;
+name const * g_insert = nullptr;
 name const * g_int = nullptr;
 name const * g_int_of_nat = nullptr;
 name const * g_int_has_zero = nullptr;
@@ -309,6 +311,7 @@ name const * g_simplifier_congr_bin_op = nullptr;
 name const * g_simplifier_congr_bin_arg1 = nullptr;
 name const * g_simplifier_congr_bin_arg2 = nullptr;
 name const * g_simplifier_congr_bin_args = nullptr;
+name const * g_singleton = nullptr;
 name const * g_sizeof = nullptr;
 name const * g_smt_array = nullptr;
 name const * g_smt_select = nullptr;
@@ -323,6 +326,7 @@ name const * g_sub = nullptr;
 name const * g_subsingleton = nullptr;
 name const * g_subsingleton_elim = nullptr;
 name const * g_subsingleton_helim = nullptr;
+name const * g_subtype = nullptr;
 name const * g_subtype_tag = nullptr;
 name const * g_subtype_elt_of = nullptr;
 name const * g_subtype_rec = nullptr;
@@ -405,6 +409,7 @@ void initialize_constants() {
     g_id = new name{"id"};
     g_empty = new name{"empty"};
     g_empty_rec = new name{"empty", "rec"};
+    g_empty_col = new name{"empty_col"};
     g_Exists = new name{"Exists"};
     g_eq = new name{"eq"};
     g_eq_drec = new name{"eq", "drec"};
@@ -472,6 +477,7 @@ void initialize_constants() {
     g_implies_of_if_neg = new name{"implies_of_if_neg"};
     g_implies_of_if_pos = new name{"implies_of_if_pos"};
     g_implies_resolve = new name{"implies", "resolve"};
+    g_insert = new name{"insert"};
     g_int = new name{"int"};
     g_int_of_nat = new name{"int", "of_nat"};
     g_int_has_zero = new name{"int_has_zero"};
@@ -662,6 +668,7 @@ void initialize_constants() {
     g_simplifier_congr_bin_arg1 = new name{"simplifier", "congr_bin_arg1"};
     g_simplifier_congr_bin_arg2 = new name{"simplifier", "congr_bin_arg2"};
     g_simplifier_congr_bin_args = new name{"simplifier", "congr_bin_args"};
+    g_singleton = new name{"singleton"};
     g_sizeof = new name{"sizeof"};
     g_smt_array = new name{"smt", "array"};
     g_smt_select = new name{"smt", "select"};
@@ -676,6 +683,7 @@ void initialize_constants() {
     g_subsingleton = new name{"subsingleton"};
     g_subsingleton_elim = new name{"subsingleton", "elim"};
     g_subsingleton_helim = new name{"subsingleton", "helim"};
+    g_subtype = new name{"subtype"};
     g_subtype_tag = new name{"subtype", "tag"};
     g_subtype_elt_of = new name{"subtype", "elt_of"};
     g_subtype_rec = new name{"subtype", "rec"};
@@ -759,6 +767,7 @@ void finalize_constants() {
     delete g_id;
     delete g_empty;
     delete g_empty_rec;
+    delete g_empty_col;
     delete g_Exists;
     delete g_eq;
     delete g_eq_drec;
@@ -826,6 +835,7 @@ void finalize_constants() {
     delete g_implies_of_if_neg;
     delete g_implies_of_if_pos;
     delete g_implies_resolve;
+    delete g_insert;
     delete g_int;
     delete g_int_of_nat;
     delete g_int_has_zero;
@@ -1016,6 +1026,7 @@ void finalize_constants() {
     delete g_simplifier_congr_bin_arg1;
     delete g_simplifier_congr_bin_arg2;
     delete g_simplifier_congr_bin_args;
+    delete g_singleton;
     delete g_sizeof;
     delete g_smt_array;
     delete g_smt_select;
@@ -1030,6 +1041,7 @@ void finalize_constants() {
     delete g_subsingleton;
     delete g_subsingleton_elim;
     delete g_subsingleton_helim;
+    delete g_subtype;
     delete g_subtype_tag;
     delete g_subtype_elt_of;
     delete g_subtype_rec;
@@ -1112,6 +1124,7 @@ name const & get_div_name() { return *g_div; }
 name const & get_id_name() { return *g_id; }
 name const & get_empty_name() { return *g_empty; }
 name const & get_empty_rec_name() { return *g_empty_rec; }
+name const & get_empty_col_name() { return *g_empty_col; }
 name const & get_Exists_name() { return *g_Exists; }
 name const & get_eq_name() { return *g_eq; }
 name const & get_eq_drec_name() { return *g_eq_drec; }
@@ -1179,6 +1192,7 @@ name const & get_implies_name() { return *g_implies; }
 name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; }
 name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; }
 name const & get_implies_resolve_name() { return *g_implies_resolve; }
+name const & get_insert_name() { return *g_insert; }
 name const & get_int_name() { return *g_int; }
 name const & get_int_of_nat_name() { return *g_int_of_nat; }
 name const & get_int_has_zero_name() { return *g_int_has_zero; }
@@ -1369,6 +1383,7 @@ name const & get_simplifier_congr_bin_op_name() { return *g_simplifier_congr_bin
 name const & get_simplifier_congr_bin_arg1_name() { return *g_simplifier_congr_bin_arg1; }
 name const & get_simplifier_congr_bin_arg2_name() { return *g_simplifier_congr_bin_arg2; }
 name const & get_simplifier_congr_bin_args_name() { return *g_simplifier_congr_bin_args; }
+name const & get_singleton_name() { return *g_singleton; }
 name const & get_sizeof_name() { return *g_sizeof; }
 name const & get_smt_array_name() { return *g_smt_array; }
 name const & get_smt_select_name() { return *g_smt_select; }
@@ -1383,6 +1398,7 @@ name const & get_sub_name() { return *g_sub; }
 name const & get_subsingleton_name() { return *g_subsingleton; }
 name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
 name const & get_subsingleton_helim_name() { return *g_subsingleton_helim; }
+name const & get_subtype_name() { return *g_subtype; }
 name const & get_subtype_tag_name() { return *g_subtype_tag; }
 name const & get_subtype_elt_of_name() { return *g_subtype_elt_of; }
 name const & get_subtype_rec_name() { return *g_subtype_rec; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 81fabde712..45b15b70cc 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -54,6 +54,7 @@ name const & get_div_name();
 name const & get_id_name();
 name const & get_empty_name();
 name const & get_empty_rec_name();
+name const & get_empty_col_name();
 name const & get_Exists_name();
 name const & get_eq_name();
 name const & get_eq_drec_name();
@@ -121,6 +122,7 @@ name const & get_implies_name();
 name const & get_implies_of_if_neg_name();
 name const & get_implies_of_if_pos_name();
 name const & get_implies_resolve_name();
+name const & get_insert_name();
 name const & get_int_name();
 name const & get_int_of_nat_name();
 name const & get_int_has_zero_name();
@@ -311,6 +313,7 @@ name const & get_simplifier_congr_bin_op_name();
 name const & get_simplifier_congr_bin_arg1_name();
 name const & get_simplifier_congr_bin_arg2_name();
 name const & get_simplifier_congr_bin_args_name();
+name const & get_singleton_name();
 name const & get_sizeof_name();
 name const & get_smt_array_name();
 name const & get_smt_select_name();
@@ -325,6 +328,7 @@ name const & get_sub_name();
 name const & get_subsingleton_name();
 name const & get_subsingleton_elim_name();
 name const & get_subsingleton_helim_name();
+name const & get_subtype_name();
 name const & get_subtype_tag_name();
 name const & get_subtype_elt_of_name();
 name const & get_subtype_rec_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index c12e6a9a32..c4b1a7eea1 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -47,6 +47,7 @@ div
 id
 empty
 empty.rec
+empty_col
 Exists
 eq
 eq.drec
@@ -114,6 +115,7 @@ implies
 implies_of_if_neg
 implies_of_if_pos
 implies.resolve
+insert
 int
 int.of_nat
 int_has_zero
@@ -304,6 +306,7 @@ simplifier.congr_bin_op
 simplifier.congr_bin_arg1
 simplifier.congr_bin_arg2
 simplifier.congr_bin_args
+singleton
 sizeof
 smt.array
 smt.select
@@ -318,6 +321,7 @@ sub
 subsingleton
 subsingleton.elim
 subsingleton.helim
+subtype
 subtype.tag
 subtype.elt_of
 subtype.rec
diff --git a/tests/lean/pattern_pp.lean b/tests/lean/pattern_pp.lean
deleted file mode 100644
index 64977ca896..0000000000
--- a/tests/lean/pattern_pp.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-noncomputable definition Sum : nat → (nat → nat) → nat := sorry
-attribute [forward]
-definition Sum_weird (f g h : nat → nat) (n : nat) : (Sum n (λ x, f (g (h x)))) = 1 := sorry
-print Sum_weird
-
-/-
-attribute [forward]
-definition Sum_weird : ∀ (f g h : nat → nat) (n : nat), eq (Sum n (λ (x : nat), f (g (h x)))) 1 :=
-λ (f g h : nat → nat) (n : nat), sorry
-(multi-)patterns:
-?M_1 : nat → nat, ?M_2 : nat → nat, ?M_3 : nat → nat, ?M_4 : nat
-{Sum ?M_4 (λ (x : nat), ?M_1)}
--/
diff --git a/tests/lean/pattern_pp.lean.expected.out b/tests/lean/pattern_pp.lean.expected.out
deleted file mode 100644
index 6884cd4083..0000000000
--- a/tests/lean/pattern_pp.lean.expected.out
+++ /dev/null
@@ -1,3 +0,0 @@
-attribute [forward]
-definition Sum_weird : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 :=
-λ (f g h : ℕ → ℕ) (n : ℕ), sorry
diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out
index d908942421..04b757a8ef 100644
--- a/tests/lean/print_ax1.lean.expected.out
+++ b/tests/lean/print_ax1.lean.expected.out
@@ -1,3 +1,3 @@
 quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
-classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x : A \ Exists P → P x}
+classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index d908942421..04b757a8ef 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,3 +1,3 @@
 quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
-classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x : A \ Exists P → P x}
+classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out
index 1238f47ae7..bd14ec3c7b 100644
--- a/tests/lean/print_ax3.lean.expected.out
+++ b/tests/lean/print_ax3.lean.expected.out
@@ -1,7 +1,7 @@
 no axioms
 ------
 quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
-classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x : A \ Exists P → P x}
+classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
 ------
 theorem foo3 : 0 = 0 :=
diff --git a/tests/lean/run/curly_notation.lean b/tests/lean/run/curly_notation.lean
new file mode 100644
index 0000000000..1e2d676077
--- /dev/null
+++ b/tests/lean/run/curly_notation.lean
@@ -0,0 +1,12 @@
+check ({1, 2, 3} : set nat)
+check ({1} : set nat)
+check ({} : set nat)
+
+definition s1 : set nat := {1, 2+3, 3, 4}
+print s1
+
+definition s2 : set char := {'a', 'b', 'c'}
+print s2
+
+definition s3 : set string := {"hello", "world"}
+print s3
diff --git a/tests/lean/run/pattern2.lean b/tests/lean/run/pattern2.lean
deleted file mode 100644
index ea790db874..0000000000
--- a/tests/lean/run/pattern2.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-constant f : nat → nat → nat
-constant g : nat → nat → nat
-attribute g [no_pattern]
-
-namespace foo
-
-attribute [forward]
-definition lemma1 {a b : nat} : f a b = g a b :=
-sorry
-
-end foo
-
-print foo.lemma1
-open foo
-print foo.lemma1
-attribute foo.lemma1 [forward]
-
-print foo.lemma1
diff --git a/tests/lean/run/pattern3.lean b/tests/lean/run/pattern3.lean
deleted file mode 100644
index e239df3860..0000000000
--- a/tests/lean/run/pattern3.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-constant Sum : (nat → nat) → nat → nat
-
-attribute [forward]
-lemma l1 (f : nat → nat) : Sum f 0 = 0 :=
-sorry
-
-print l1
diff --git a/tests/lean/run/print_no_pattern.lean b/tests/lean/run/print_no_pattern.lean
deleted file mode 100644
index ac4db0ff78..0000000000
--- a/tests/lean/run/print_no_pattern.lean
+++ /dev/null
@@ -1 +0,0 @@
-print [no_pattern]
diff --git a/tests/lean/subpp.lean.expected.out b/tests/lean/subpp.lean.expected.out
index e754354b5c..8361435712 100644
--- a/tests/lean/subpp.lean.expected.out
+++ b/tests/lean/subpp.lean.expected.out
@@ -1 +1 @@
-{x : ℕ \ x > 0} : Type
+{x \ x > 0} : Type