feat(library/equations_compiler): add elim_match skeleton

src/library/equations_compiler/CMakeLists.txt

@@ -1,6 +1,6 @@
 add_library(equations_compiler OBJECT
   equations.cpp util.cpp pack_domain.cpp
   structural_rec.cpp unbounded_rec.cpp
-  compiler.cpp init_module.cpp
+  elim_match.cpp compiler.cpp init_module.cpp
 #LEGACY
   old_compiler.cpp old_goal.cpp old_inversion.cpp)

src/library/equations_compiler/compiler.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/pack_domain.h"
 #include "library/equations_compiler/structural_rec.h"
 #include "library/equations_compiler/unbounded_rec.h"
+#include "library/equations_compiler/elim_match.h"
 
 namespace lean {
 #define trace_compiler(Code) lean_trace("eqn_compiler", scope_trace_env _scope1(ctx->env(), ctx); Code)
@@ -25,11 +26,15 @@ expr compile_equations(environment const & env, options const & opts, metavar_co
 
     // test structural_rec
     unsigned arg_idx;
-    try_structural_rec(ctx.get(), eqns, arg_idx);
+    optional<expr> eqns1 = try_structural_rec(ctx.get(), eqns, arg_idx);
+    if (eqns1) {
+        elim_match(ctx.get(), eqns);
+    }
 
     // test unbounded_rec
     unbounded_rec(ctx.get(), eqns);
 
+
     lean_unreachable();
 }
 

src/library/equations_compiler/elim_match.cpp

@@ -0,0 +1,48 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/trace.h"
+#include "library/equations_compiler/equations.h"
+#include "library/equations_compiler/util.h"
+
+namespace lean {
+#define trace_match(Code) lean_trace(name({"eqn_compiler", "elim_match"}), scope_trace_env _scope1(m_ctx.env(), m_ctx); Code)
+
+struct elim_match_fn {
+    type_context & m_ctx;
+    elim_match_fn(type_context & ctx):m_ctx(ctx) {}
+
+    struct equation {
+        list<expr> m_vars;
+        list<expr> m_patterns;
+        expr       m_rhs;
+    };
+
+    struct program {
+        /* Variables that still need to be matched/processed */
+        list<expr> m_var_stack;
+        list<expr> m_equations;
+    };
+
+
+    pair<expr, environment> operator()(expr const & e) {
+        unpack_eqns ues(m_ctx, e);
+        lean_assert(ues.get_num_fns() == 1);
+
+        lean_unreachable();
+    }
+};
+
+pair<expr, environment> elim_match(type_context & ctx, expr const & eqns) {
+    return elim_match_fn(ctx)(eqns);
+}
+
+void initialize_elim_match() {
+    register_trace_class({"eqn_compiler", "elim_match"});
+}
+void finalize_elim_match() {
+}
+}

src/library/equations_compiler/elim_match.h

@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/type_context.h"
+namespace lean {
+pair<expr, environment> elim_match(type_context & ctx, expr const & eqns);
+void initialize_elim_match();
+void finalize_elim_match();
+}

src/library/equations_compiler/init_module.cpp

@@ -6,17 +6,20 @@ Author: Leonardo de Moura
 */
 #include "library/equations_compiler/equations.h"
 #include "library/equations_compiler/structural_rec.h"
+#include "library/equations_compiler/elim_match.h"
 #include "library/equations_compiler/compiler.h"
 
 namespace lean{
 void initialize_equations_compiler_module() {
     initialize_equations();
     initialize_structural_rec();
+    initialize_elim_match();
     initialize_compiler();
 }
 
 void finalize_equations_compiler_module() {
     finalize_compiler();
+    finalize_elim_match();
     finalize_structural_rec();
     finalize_equations();
 }

tmp/bad2.lean

@@ -0,0 +1,7 @@
+inductive imf (f : nat → nat) : nat → Type
+| mk1 : ∀ (a : nat), imf (f a)
+| mk2 : imf (f 0 + 1)
+
+definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat \ x > b} →nat
+| ⌞f a⌟     (imf.mk1 ⌞f⌟ a) x := a
+| ⌞f 0 + 1⌟ (imf.mk2 ⌞f⌟)   x := subtype.elt_of x