From 05013fb61dfa807f04e82ef92500f6b2d78e8aa3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 Aug 2016 21:36:44 -0700
Subject: [PATCH] feat(library/equations_compiler): add elim_match skeleton

---
 src/library/equations_compiler/CMakeLists.txt |  2 +-
 src/library/equations_compiler/compiler.cpp   |  7 ++-
 src/library/equations_compiler/elim_match.cpp | 48 +++++++++++++++++++
 src/library/equations_compiler/elim_match.h   | 13 +++++
 .../equations_compiler/init_module.cpp        |  3 ++
 tmp/bad2.lean                                 |  7 +++
 6 files changed, 78 insertions(+), 2 deletions(-)
 create mode 100644 src/library/equations_compiler/elim_match.cpp
 create mode 100644 src/library/equations_compiler/elim_match.h
 create mode 100644 tmp/bad2.lean

diff --git a/src/library/equations_compiler/CMakeLists.txt b/src/library/equations_compiler/CMakeLists.txt
index 5eb1586853..c380277d8b 100644
--- a/src/library/equations_compiler/CMakeLists.txt
+++ b/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)
diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index ac07e8c40d..f114473928 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/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();
 }
 
diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
new file mode 100644
index 0000000000..7d0c7014e8
--- /dev/null
+++ b/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() {
+}
+}
diff --git a/src/library/equations_compiler/elim_match.h b/src/library/equations_compiler/elim_match.h
new file mode 100644
index 0000000000..5107a1c11c
--- /dev/null
+++ b/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();
+}
diff --git a/src/library/equations_compiler/init_module.cpp b/src/library/equations_compiler/init_module.cpp
index b67ab08cfa..cc64e279ad 100644
--- a/src/library/equations_compiler/init_module.cpp
+++ b/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();
 }
diff --git a/tmp/bad2.lean b/tmp/bad2.lean
new file mode 100644
index 0000000000..a5485870e8
--- /dev/null
+++ b/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