perf(frontends/lean): add notation #[...]

The new notation should be use to input long sequences.
Closes #1755

doc/changes.md

@@ -43,6 +43,10 @@ master branch (aka work in progress branch)
 
 * `induction e` now also works on non-variable `e`. Unlike `ginduction`, it will not introduce equalities relating `e` to the inductive cases.
 
+* Add notation `#[a, b, c, d]` for `bin_tree.node (bin_tree.node (bin_tree.leaf a) (bin_tree.leaf b)) (bin_tree.node (bin_tree.leaf c) (bin_tree.leaf d))`.
+  There is a coercion from `bin_tree` to `list`. The new notation allows to input long sequences efficiently.
+  It also prevents system stack overflows.
+
 *Changes*
 
 * We now have two type classes for converting to string: `has_to_string` and `has_repr`.

library/init/core.lean

@@ -520,6 +520,23 @@ def K {α : Type u₁} {β : Type u₂} (a : α) (b : β) := a
 def S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
 end combinator
 
+/-- Auxiliary datatype for #[ ... ] notation.
+    #[1, 2, 3, 4] is notation for
+
+    bin_tree.node
+      (bin_tree.node (bin_tree.leaf 1) (bin_tree.leaf 2))
+      (bin_tree.node (bin_tree.leaf 3) (bin_tree.leaf 4))
+
+    We use this notation to input long sequences without exhausting the system stack space.
+    Later, we define a coercion from `bin_tree` into `list`.
+-/
+inductive bin_tree (α : Type u)
+| empty {}       : bin_tree
+| leaf (val : α) : bin_tree
+| node (left right : bin_tree) : bin_tree
+
+attribute [elab_simple] bin_tree.node bin_tree.leaf
+
 /- Basic unification hints -/
 @[unify] def add_succ_defeq_succ_add_hint (x y z : nat) : unification_hint :=
 { pattern     := x + nat.succ y ≟ nat.succ z,

library/init/data/list/basic.lean

@@ -332,3 +332,13 @@ infix ` <:+ `:50 := is_suffix
 infix ` <:+: `:50 := is_infix
 
 end list
+
+namespace bin_tree
+private def to_list_aux : bin_tree α → list α → list α
+| empty      as := as
+| (leaf a)   as := a::as
+| (node l r) as := to_list_aux l (to_list_aux r as)
+
+def to_list (t : bin_tree α) : list α :=
+to_list_aux t []
+end bin_tree

library/init/data/list/instances.lean

@@ -60,6 +60,9 @@ namespace list
 
 variables {α β : Type u} (p : α → Prop) [decidable_pred p]
 
+instance bin_tree_to_list : has_coe (bin_tree α) (list α) :=
+⟨bin_tree.to_list⟩
+
 lemma mem_bind_iff {b : β} {l : list α} {f : α → list β} : b ∈ l >>= f ↔ ∃ a ∈ l, b ∈ f a :=
 iff.trans mem_join_iff
   ⟨λ ⟨l', h1, h2⟩, let ⟨a, al, fa⟩ := exists_of_mem_map h1 in ⟨a, al, fa.symm ▸ h2⟩,

src/frontends/lean/builtin_exprs.cpp

@@ -978,6 +978,37 @@ static expr parse_hole(parser_state & p, unsigned, expr const *, pos_info const
     return r;
 }
 
+
+static expr mk_bin_tree(parser & p, buffer<expr> const & args, unsigned start, unsigned end, pos_info const & pos) {
+    lean_assert(start < end);
+    lean_assert(end <= args.size());
+    if (end == start+1)
+        return p.save_pos(mk_app(p.save_pos(mk_constant(get_bin_tree_leaf_name()), pos), args[start]), pos);
+    unsigned mid = (start + end)/2;
+    expr left  = mk_bin_tree(p, args, start, mid, pos);
+    expr right = mk_bin_tree(p, args, mid, end, pos);
+    return p.save_pos(mk_app(p.save_pos(mk_constant(get_bin_tree_node_name()), pos),
+                             left, right),
+                      pos);
+}
+
+
+static expr parse_bin_tree(parser_state & p, unsigned, expr const *, pos_info const & pos) {
+    buffer<expr> es;
+    while (!p.curr_is_token(get_rbracket_tk())) {
+        es.push_back(p.parse_expr());
+        if (!p.curr_is_token(get_comma_tk()))
+            break;
+        p.next();
+    }
+    p.check_token_next(get_rbracket_tk(), "invalid `#[...]`, `]` expected");
+    if (es.empty()) {
+        return p.save_pos(mk_constant(get_bin_tree_empty_name()), pos);
+    } else {
+        return mk_bin_tree(p, es, 0, es.size(), pos);
+    }
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -1002,6 +1033,7 @@ parse_table init_nud_table() {
     r = r.add({transition("`[", mk_ext_action(parse_interactive_tactic_block))}, x0);
     r = r.add({transition("`", mk_ext_action(parse_quoted_name))}, x0);
     r = r.add({transition("%%", mk_ext_action(parse_antiquote_expr))}, x0);
+    r = r.add({transition("#[", mk_ext_action(parse_bin_tree))}, x0);
     r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);
     r = r.add({transition("()", mk_ext_action(parse_unit))}, x0);
     r = r.add({transition("(::)", mk_ext_action(parse_lambda_cons))}, x0);

src/frontends/lean/token_table.cpp

@@ -86,7 +86,7 @@ void init_token_table(token_table & t) {
          {"```(", g_max_prec}, {"`[", g_max_prec}, {"`", g_max_prec},
          {"%%", g_max_prec}, {"()", g_max_prec}, {"(::)", g_max_prec}, {")", 0}, {"'", 0},
          {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
-         {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
+         {"[", g_max_prec}, {"#[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
          {"{!", g_max_prec}, {"!}", 0},
          {"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
          {"(:", g_max_prec}, {":)", 0}, {".(", g_max_prec}, {"._", g_max_prec},

src/library/constants.cpp

@@ -20,6 +20,9 @@ name const * g_and_cases_on = nullptr;
 name const * g_auto_param = nullptr;
 name const * g_bit0 = nullptr;
 name const * g_bit1 = nullptr;
+name const * g_bin_tree_empty = nullptr;
+name const * g_bin_tree_leaf = nullptr;
+name const * g_bin_tree_node = nullptr;
 name const * g_bool = nullptr;
 name const * g_bool_ff = nullptr;
 name const * g_bool_tt = nullptr;
@@ -394,6 +397,9 @@ void initialize_constants() {
     g_auto_param = new name{"auto_param"};
     g_bit0 = new name{"bit0"};
     g_bit1 = new name{"bit1"};
+    g_bin_tree_empty = new name{"bin_tree", "empty"};
+    g_bin_tree_leaf = new name{"bin_tree", "leaf"};
+    g_bin_tree_node = new name{"bin_tree", "node"};
     g_bool = new name{"bool"};
     g_bool_ff = new name{"bool", "ff"};
     g_bool_tt = new name{"bool", "tt"};
@@ -769,6 +775,9 @@ void finalize_constants() {
     delete g_auto_param;
     delete g_bit0;
     delete g_bit1;
+    delete g_bin_tree_empty;
+    delete g_bin_tree_leaf;
+    delete g_bin_tree_node;
     delete g_bool;
     delete g_bool_ff;
     delete g_bool_tt;
@@ -1143,6 +1152,9 @@ name const & get_and_cases_on_name() { return *g_and_cases_on; }
 name const & get_auto_param_name() { return *g_auto_param; }
 name const & get_bit0_name() { return *g_bit0; }
 name const & get_bit1_name() { return *g_bit1; }
+name const & get_bin_tree_empty_name() { return *g_bin_tree_empty; }
+name const & get_bin_tree_leaf_name() { return *g_bin_tree_leaf; }
+name const & get_bin_tree_node_name() { return *g_bin_tree_node; }
 name const & get_bool_name() { return *g_bool; }
 name const & get_bool_ff_name() { return *g_bool_ff; }
 name const & get_bool_tt_name() { return *g_bool_tt; }

src/library/constants.h

@@ -22,6 +22,9 @@ name const & get_and_cases_on_name();
 name const & get_auto_param_name();
 name const & get_bit0_name();
 name const & get_bit1_name();
+name const & get_bin_tree_empty_name();
+name const & get_bin_tree_leaf_name();
+name const & get_bin_tree_node_name();
 name const & get_bool_name();
 name const & get_bool_ff_name();
 name const & get_bool_tt_name();

src/library/constants.txt

@@ -15,6 +15,9 @@ and.cases_on
 auto_param
 bit0
 bit1
+bin_tree.empty
+bin_tree.leaf
+bin_tree.node
 bool
 bool.ff
 bool.tt

tests/lean/run/check_constants.lean

@@ -20,6 +20,9 @@ run_cmd script_check_id `and.cases_on
 run_cmd script_check_id `auto_param
 run_cmd script_check_id `bit0
 run_cmd script_check_id `bit1
+run_cmd script_check_id `bin_tree.empty
+run_cmd script_check_id `bin_tree.leaf
+run_cmd script_check_id `bin_tree.node
 run_cmd script_check_id `bool
 run_cmd script_check_id `bool.ff
 run_cmd script_check_id `bool.tt

tests/lean/run/lst64.lean

@@ -0,0 +1,74 @@
+def mylist : list ℕ :=
+#[
+ 0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
+]