feat: add options preserve_data and zeta to apply_beta

leanprover · Aug 5, 2024 · e9ad746 · e9ad746
1 parent 486d98f
commit e9ad746
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 15 deletions.
diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
@@ -165,22 +165,38 @@ bool is_head_beta(expr const & t) {
     return is_app(t) && is_lambda(get_app_fn(t));
 }
 
-expr apply_beta(expr f, unsigned num_args, expr const * args) {
-    if (num_args == 0) {
-        return f;
-    } else if (!is_lambda(f)) {
-        return mk_rev_app(f, num_args, args);
-    } else {
-        unsigned m = 1;
-        while (is_lambda(binding_body(f)) && m < num_args) {
-            f = binding_body(f);
-            m++;
+static expr apply_beta_rec(expr e, unsigned i, unsigned num_rev_args, expr const * rev_args, bool preserve_data, bool zeta) {
+    if (is_lambda(e)) {
+        if (i + 1 < num_rev_args) {
+            return apply_beta_rec(binding_body(e), i+1, num_rev_args, rev_args, preserve_data, zeta);
+        } else {
+            return instantiate(binding_body(e), num_rev_args, rev_args);
+        }
+    } else if (is_let(e)) {
+        if (zeta && i < num_rev_args) {
+            return apply_beta_rec(instantiate(let_body(e), let_value(e)), i, num_rev_args, rev_args, preserve_data, zeta);
+        } else {
+            unsigned n = num_rev_args - i;
+            return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
+        }
+    } else if (is_mdata(e)) {
+        if (preserve_data) {
+            unsigned n = num_rev_args - i;
+            return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
+        } else {
+            return apply_beta_rec(mdata_expr(e), i, num_rev_args, rev_args, preserve_data, zeta);
         }
-        lean_assert(m <= num_args);
-        return mk_rev_app(instantiate(binding_body(f), m, args + (num_args - m)), num_args - m, args);
+    } else {
+        unsigned n = num_rev_args - i;
+        return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
     }
 }
 
+expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args, bool preserve_data, bool zeta) {
+    if (num_rev_args == 0) return f;
+    return apply_beta_rec(f, 0, num_rev_args, rev_args, preserve_data, zeta);
+}
+
 expr head_beta_reduce(expr const & t) {
     if (!is_head_beta(t)) {
         return t;

diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h
@@ -24,7 +24,7 @@ inline expr instantiate_rev(expr const & e, buffer<expr> const & s) {
     return instantiate_rev(e, s.size(), s.data());
 }
 
-expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args);
+expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args, bool preserve_data = true, bool zeta = false);
 bool is_head_beta(expr const & t);
 expr head_beta_reduce(expr const & t);
 /* If `e` is of the form `(fun x, t) a` return `head_beta_const_fn(t)` if `t` does not depend on `x`,

diff --git a/src/kernel/instantiate_mvars.cpp b/src/kernel/instantiate_mvars.cpp
@@ -215,8 +215,16 @@ class instantiate_mvars_fn {
             args.push_back(visit(app_arg(e)));
             return visit_args_and_beta(f_new, app_fn(e), args);
         } else {
-            // TODO (zeta := true)
-            return apply_beta(f_new, args.size(), args.data());
+            /*
+            Some of the arguments in `args` are irrelevant after we beta
+            reduce. Also, it may be a bug to not instantiate them, since they
+            may depend on free variables that are not in the context (see
+            issue #4375). So we pass `useZeta := true` to ensure that they are
+            instantiated.
+            */
+            bool preserve_data = false;
+            bool zeta = true;
+            return apply_beta(f_new, args.size(), args.data(), preserve_data, zeta);
         }
     }