chore: update stage0

stage0/src/CMakeLists.txt

@@ -384,6 +384,7 @@ include_directories(${CMAKE_BINARY_DIR}/include)  # config.h etc., "public" head
 
 string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
 # These are used in lean.mk (and libleanrt) and passed through by stdlib.make
+# They are not embedded into `leanc` since they are build profile/machine specific
 string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
 if(CMAKE_OSX_DEPLOYMENT_TARGET)
   string(APPEND LEANC_OPTS " ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET}")

stage0/src/library/compiler/csimp.cpp

@@ -1149,8 +1149,8 @@ class csimp_fn {
         // Example: `fun {a} => ReaderT.pure`
         if (!is_join_point_def && !top) {
             expr new_e = eta_reduce(e);
-           // Remark: we should not eta-reduce auxiliary match applications.
-            if (is_app(new_e) && !is_constructor_app(env(), new_e) && !is_proj(new_e) && !is_matcher_app(env(), new_e) && !is_cases_on_app(env(), new_e) && !is_lc_unreachable_app(new_e))
+           // Remark: we should only keep result if it is not a term must be in eta-expanded form.
+            if (is_app(new_e) && !must_be_eta_expanded(env(), new_e))
                 return visit(new_e, true);
         }
         buffer<expr> binding_fvars;

stage0/src/library/compiler/util.cpp

@@ -749,6 +749,21 @@ expr lcnf_eta_expand(type_checker::state & st, local_ctx lctx, expr e) {
     }
 }
 
+bool is_quot_primitive_app(environment const & env, expr const & e) {
+  expr const & f = get_app_fn(e);
+  return is_constant(f) && is_quot_primitive(env, const_name(f));
+}
+
+bool must_be_eta_expanded(environment const & env, expr const & e) {
+  return
+    is_constructor_app(env, e) ||
+    is_proj(e) ||
+    is_matcher_app(env, e) ||
+    is_cases_on_app(env, e) ||
+    is_lc_unreachable_app(e) ||
+    is_quot_primitive_app(env, e);
+}
+
 void initialize_compiler_util() {
     g_neutral_expr        = new expr(mk_constant("_neutral"));
     mark_persistent(g_neutral_expr->raw());

stage0/src/library/compiler/util.h

@@ -209,6 +209,12 @@ inline bool is_matcher_app(environment const & env, expr const & e) {
   return is_constant(f) && is_matcher(env, const_name(f));
 }
 
+/*
+  Return true if the given expression must be in eta-expanded form during compilation.
+  Example: constructors, `casesOn` applications must always be in eta-expanded form.
+*/
+bool must_be_eta_expanded(environment const & env, expr const & e);
+
 void initialize_compiler_util();
 void finalize_compiler_util();
 }