feat(compiler/erase_irrelevant): eliminate subtype.tag, subtype.rec and subtype.elt_of

src/compiler/erase_irrelevant.cpp

@@ -39,13 +39,17 @@ class erase_irrelevant_fn : public compiler_step_visitor {
         return mk_app(fn, args.size() - nparams - 1 - nindices, args.data() + nparams + 1 + nindices);
     }
 
+    expr add_args(expr e, unsigned start_idx, buffer<expr> const & args) {
+        for (unsigned i = start_idx; i < args.size(); i++)
+            e = mk_app(e, args[i]);
+        return beta_reduce(e);
+    }
+
     /* Remove eq.rec applications since they are just "type-casting" operations. */
     expr visit_eq_rec(buffer<expr> & args) {
         lean_assert(args.size() >= 6);
         expr major = visit(args[3]);
-        for (unsigned i = 6; i < args.size(); i++)
-            args[i] = visit(args[i]);
-        return beta_reduce(mk_app(major, args.size() - 6, args.data() + 6));
+        return add_args(major, 6, args);
     }
 
     expr consume_lambdas(type_context::tmp_locals & locals, expr e) {
@@ -88,9 +92,30 @@ class erase_irrelevant_fn : public compiler_step_visitor {
         for (unsigned i = 0; i < c_data_sz; i++)
             r = mk_app(r, *g_neutral_expr); // add dummy proofs
         /* add remaining arguments */
-        for (unsigned i = nparams + nindices + 5; i < args.size(); i++)
-            r = mk_app(r, visit(args[i]));
-        return beta_reduce(r);
+        return add_args(r, nparams + nindices + 5, args);
+    }
+
+    /* Treat subtype.tag as the identity function */
+    virtual expr visit_subtype_tag(buffer<expr> const & args) {
+        lean_assert(args.size() >= 4);
+        expr r = visit(args[2]);
+        return add_args(r, 4, args);
+    }
+
+    /* Eliminate subtype.rec */
+    virtual expr visit_subtype_rec(buffer<expr> const & args) {
+        lean_assert(args.size() >= 5);
+        expr minor = visit(args[3]);
+        expr major = visit(args[4]);
+        expr r     = mk_app(minor, major, *g_neutral_expr);
+        return add_args(r, 5, args);
+    }
+
+    /* subtype.elt_of is also compiled as the identity function */
+    virtual expr visit_subtype_elt_of(buffer<expr> const & args) {
+        lean_assert(args.size() >= 3);
+        expr r = visit(args[2]);
+        return add_args(r, 3, args);
     }
 
     virtual expr visit_app(expr const & e) override {
@@ -106,6 +131,12 @@ class erase_irrelevant_fn : public compiler_step_visitor {
                 return visit_no_confusion(fn, args);
             } else if (n == get_eq_rec_name()) {
                 return visit_eq_rec(args);
+            } else if (n == get_subtype_tag_name()) {
+                return visit_subtype_tag(args);
+            } else if (n == get_subtype_rec_name()) {
+                return visit_subtype_rec(args);
+            } else if (n == get_subtype_elt_of_name()) {
+                return visit_subtype_elt_of(args);
             }
         }
         return compiler_step_visitor::visit_app(e);

src/library/constants.cpp

@@ -205,6 +205,9 @@ name const * g_sub = nullptr;
 name const * g_subsingleton = nullptr;
 name const * g_subsingleton_elim = nullptr;
 name const * g_subsingleton_helim = nullptr;
+name const * g_subtype_tag = nullptr;
+name const * g_subtype_elt_of = nullptr;
+name const * g_subtype_rec = nullptr;
 name const * g_tactic = nullptr;
 name const * g_tactic_all_goals = nullptr;
 name const * g_tactic_and_then = nullptr;
@@ -480,6 +483,9 @@ void initialize_constants() {
     g_subsingleton = new name{"subsingleton"};
     g_subsingleton_elim = new name{"subsingleton", "elim"};
     g_subsingleton_helim = new name{"subsingleton", "helim"};
+    g_subtype_tag = new name{"subtype", "tag"};
+    g_subtype_elt_of = new name{"subtype", "elt_of"};
+    g_subtype_rec = new name{"subtype", "rec"};
     g_tactic = new name{"tactic"};
     g_tactic_all_goals = new name{"tactic", "all_goals"};
     g_tactic_and_then = new name{"tactic", "and_then"};
@@ -756,6 +762,9 @@ void finalize_constants() {
     delete g_subsingleton;
     delete g_subsingleton_elim;
     delete g_subsingleton_helim;
+    delete g_subtype_tag;
+    delete g_subtype_elt_of;
+    delete g_subtype_rec;
     delete g_tactic;
     delete g_tactic_all_goals;
     delete g_tactic_and_then;
@@ -1031,6 +1040,9 @@ name const & get_sub_name() { return *g_sub; }
 name const & get_subsingleton_name() { return *g_subsingleton; }
 name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
 name const & get_subsingleton_helim_name() { return *g_subsingleton_helim; }
+name const & get_subtype_tag_name() { return *g_subtype_tag; }
+name const & get_subtype_elt_of_name() { return *g_subtype_elt_of; }
+name const & get_subtype_rec_name() { return *g_subtype_rec; }
 name const & get_tactic_name() { return *g_tactic; }
 name const & get_tactic_all_goals_name() { return *g_tactic_all_goals; }
 name const & get_tactic_and_then_name() { return *g_tactic_and_then; }

src/library/constants.h

@@ -207,6 +207,9 @@ name const & get_sub_name();
 name const & get_subsingleton_name();
 name const & get_subsingleton_elim_name();
 name const & get_subsingleton_helim_name();
+name const & get_subtype_tag_name();
+name const & get_subtype_elt_of_name();
+name const & get_subtype_rec_name();
 name const & get_tactic_name();
 name const & get_tactic_all_goals_name();
 name const & get_tactic_and_then_name();

src/library/constants.txt

@@ -200,6 +200,9 @@ sub
 subsingleton
 subsingleton.elim
 subsingleton.helim
+subtype.tag
+subtype.elt_of
+subtype.rec
 tactic
 tactic.all_goals
 tactic.and_then