perf: add missing std::moves to save refcounting

Author: eric-wieser

src/kernel/equiv_manager.cpp

@@ -14,7 +14,7 @@ auto equiv_manager::mk_node() -> node_ref {
     node n;
     n.m_parent = r;
     n.m_rank   = 0;
-    m_nodes.push_back(n);
+    m_nodes.push_back(std::move(n));
     return r;
 }
 

src/kernel/instantiate_mvars.cpp

@@ -78,7 +78,7 @@ class instantiate_lmvars_fn {
                         after we update `mctx`. This is necessary because `m_cache`
                         may contain references to its subterms.
                         */
-                        m_saved.push_back(a);
+                        m_saved.push_back(std::move(a));
                         assign_lmvar(m_mctx, mvar_id(l), a_new);
                     }
                     return a_new;
@@ -169,7 +169,7 @@ class instantiate_mvars_fn {
         } else {
             expr a(r.get_val());
             if (!has_mvar(a) || m_already_normalized.contains(mid)) {
-                return optional<expr>(a);
+                return optional<expr>(std::move(a));
             } else {
                 m_already_normalized.insert(mid);
                 expr a_new = visit(a);
@@ -179,10 +179,10 @@ class instantiate_mvars_fn {
                     after we update `mctx`. This is necessary because `m_cache`
                     may contain references to its subterms.
                     */
-                    m_saved.push_back(a);
+                    m_saved.push_back(std::move(a));
                     assign_mvar(m_mctx, mid, a_new);
                 }
-                return optional<expr>(a_new);
+                return optional<expr>(std::move(a_new));
             }
         }
     }

src/kernel/type_checker.cpp

@@ -120,7 +120,7 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
     while (is_lambda(e)) {
         expr d    = instantiate_rev(binding_domain(e), fvars.size(), fvars.data());
         expr fvar = m_lctx.mk_local_decl(m_st->m_ngen, binding_name(e), d, binding_info(e));
-        fvars.push_back(fvar);
+        fvars.push_back(std::move(fvar));
         if (!infer_only) {
             ensure_sort_core(infer_type_core(d, infer_only), d);
         }

src/library/constructions/cases_on.cpp

@@ -64,7 +64,7 @@ declaration mk_cases_on(environment const & env, name const & n) {
     while (is_pi(rec_type)) {
         expr local = lctx.mk_local_decl(ngen, binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type));
         rec_type   = instantiate(binding_body(rec_type), local);
-        rec_fvars.push_back(local);
+        rec_fvars.push_back(std::move(local));
     }
     /* Remark `rec_fvars` free variables represent the recursor:
        - Type parameters `As` (size == `num_params`)
@@ -137,7 +137,7 @@ declaration mk_cases_on(environment const & env, name const & n) {
                 } else {
                     expr new_local = lctx.mk_local_decl(ngen, binding_name(minor_type), mk_pi_unit(curr_type, unit),
                                                         binding_info(minor_type));
-                    minor_params.push_back(new_local);
+                    minor_params.push_back(std::move(new_local));
                 }
             } else {
                 minor_params.push_back(local);

src/library/print.cpp

@@ -207,7 +207,7 @@ struct print_expr_fn {
         if (!is_nil(ls)) {
             out() << ".{";
             bool first = true;
-            for (auto l : ls) {
+            for (auto const & l : ls) {
                 if (first) first = false; else out() << ", ";
                 out() << l;
             }