feat(frontends/lean/elaborator): default parameter prototype

See #1340

library/init/core.lean

@@ -81,6 +81,10 @@ reserve infixl `; `:1
 
 universe variables u v
 
+/- gadget for optional parameter support -/
+@[reducible] def opt_param (α : Type u) (default : α) : Type u :=
+α
+
 inductive poly_unit : Type u
 | star : poly_unit
 

src/frontends/lean/elaborator.cpp

@@ -1014,6 +1014,14 @@ struct elaborator::first_pass_info {
     buffer<unsigned> new_instances_size;
 };
 
+static optional<expr> is_optional_param(expr const & e) {
+    if (is_app_of(e, get_opt_param_name(), 2)) {
+        return some_expr(app_arg(e));
+    } else {
+        return none_expr();
+    }
+}
+
 /* Check if fn args resulting type matches the expected type, and fill
    first_pass_info & info with information collected in this first pass.
    Return true iff the types match.
@@ -1032,7 +1040,7 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
     while (is_pi(type)) {
         binder_info const & bi = binding_info(type);
         expr const & d = binding_domain(type);
-        if (bi.is_strict_implicit() && i == args.size())
+        if (bi.is_strict_implicit() && i == args.size() && !is_optional_param(d))
             break;
         expr new_arg;
         if (!is_explicit(bi)) {
@@ -1052,6 +1060,8 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
             info.args_mvars.push_back(new_arg);
             info.new_args_size.push_back(info.new_args.size());
             info.new_instances_size.push_back(info.new_instances.size());
+        } else if (auto def_value = is_optional_param(d)) {
+            new_arg = *def_value;
         } else {
             break;
         }
@@ -1149,7 +1159,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
             binder_info const & bi = binding_info(type);
             expr const & d = binding_domain(type);
             expr new_arg;
-            if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size())
+            if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size() && !is_optional_param(d))
                 break;
             if ((amask == arg_mask::Default && !is_explicit(bi)) ||
                 (amask == arg_mask::InstHoExplicit && !is_explicit(bi) && !bi.is_inst_implicit() && !is_pi(d))) {
@@ -1184,6 +1194,8 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
                     throw elaborator_exception(ref, msg);
                 }
                 i++;
+            } else if (auto def_value = is_optional_param(d)) {
+                new_arg = *def_value;
             } else {
                 break;
             }

src/library/constants.cpp

@@ -317,6 +317,7 @@ name const * g_one_mul = nullptr;
 name const * g_option = nullptr;
 name const * g_option_none = nullptr;
 name const * g_option_some = nullptr;
+name const * g_opt_param = nullptr;
 name const * g_or = nullptr;
 name const * g_or_elim = nullptr;
 name const * g_or_intro_left = nullptr;
@@ -781,6 +782,7 @@ void initialize_constants() {
     g_option = new name{"option"};
     g_option_none = new name{"option", "none"};
     g_option_some = new name{"option", "some"};
+    g_opt_param = new name{"opt_param"};
     g_or = new name{"or"};
     g_or_elim = new name{"or", "elim"};
     g_or_intro_left = new name{"or", "intro_left"};
@@ -1246,6 +1248,7 @@ void finalize_constants() {
     delete g_option;
     delete g_option_none;
     delete g_option_some;
+    delete g_opt_param;
     delete g_or;
     delete g_or_elim;
     delete g_or_intro_left;
@@ -1710,6 +1713,7 @@ name const & get_one_mul_name() { return *g_one_mul; }
 name const & get_option_name() { return *g_option; }
 name const & get_option_none_name() { return *g_option_none; }
 name const & get_option_some_name() { return *g_option_some; }
+name const & get_opt_param_name() { return *g_opt_param; }
 name const & get_or_name() { return *g_or; }
 name const & get_or_elim_name() { return *g_or_elim; }
 name const & get_or_intro_left_name() { return *g_or_intro_left; }

src/library/constants.h

@@ -319,6 +319,7 @@ name const & get_one_mul_name();
 name const & get_option_name();
 name const & get_option_none_name();
 name const & get_option_some_name();
+name const & get_opt_param_name();
 name const & get_or_name();
 name const & get_or_elim_name();
 name const & get_or_intro_left_name();

src/library/constants.txt

@@ -312,6 +312,7 @@ one_mul
 option
 option.none
 option.some
+opt_param
 or
 or.elim
 or.intro_left

tests/lean/run/default_param.lean

@@ -0,0 +1,65 @@
+universe variable u
+
+def f (a : nat) (o : opt_param nat 5) :=
+a + o
+
+example : f 1 = f 1 5 :=
+rfl
+
+check f 1
+
+structure config :=
+(v1   := 10)
+(v2   := 20)
+(flag := tt)
+(ps   := ["hello", "world"])
+
+def g (a : nat) (c : opt_param config {}) : nat :=
+if c^.flag then a + c^.v1 else a + c^.v2
+
+example : g 1 = 11 :=
+rfl
+
+example : g 1 {flag := ff} = 21 :=
+rfl
+
+example : g 1 {v1 := 100} = 101 :=
+rfl
+
+def h (a : nat) (c : opt_param config {v1 := a}) : nat :=
+g a c
+
+example : h 2 = 4 :=
+rfl
+
+example : h 3 = 6 :=
+rfl
+
+example : h 2 {flag := ff} = 22 :=
+rfl
+
+def boo (a : nat) (b : opt_param nat a) (c : opt_param bool ff) (d : opt_param config {v2 := b, flag := c}) :=
+g a d
+
+check boo 2
+
+example : boo 2 = 4 :=
+rfl
+
+example : boo 2 20 = 22 :=
+rfl
+
+example : boo 2 0 tt = 12 :=
+rfl
+
+open tactic
+set_option pp.all true
+
+meta def check_expr (p : pexpr) (t : expr) : tactic unit :=
+do e ← to_expr p, guard (t = e)
+
+run_command do
+  e ← to_expr `(boo 2),
+  check_expr `(boo 2 (2:nat) ff {v1 := config.v1._default, v2 := 2, flag := ff, ps := config.ps._default}) e,
+  e ← to_expr `(f 1),
+  check_expr `(f 1 (5:nat)) e