From 9e6e406f73202d8eb768f71f69b9f1d62e6ccff0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 Jun 2015 14:42:25 -0700
Subject: [PATCH] feat(frontends/lean): add '#compose' command for testing
 composition manager

---
 src/frontends/lean/builtin_cmds.cpp | 17 ++++++++++++++++-
 src/frontends/lean/token_table.cpp  |  2 +-
 tests/lean/comp1.lean               | 24 ++++++++++++++++++++++++
 tests/lean/comp1.lean.expected.out  | 14 ++++++++++++++
 4 files changed, 55 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/comp1.lean
 create mode 100644 tests/lean/comp1.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 0797e2f56..dbd19acb2 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/user_recursors.h"
 #include "library/pp_options.h"
+#include "library/composition_manager.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/rewrite_rule_set.h"
 #include "frontends/lean/util.h"
@@ -953,6 +954,20 @@ static environment init_hits_cmd(parser & p) {
     return module::declare_hits(p.env());
 }
 
+static environment compose_cmd(parser & p) {
+    name g = p.check_constant_next("invalid #compose command, constant expected");
+    name f = p.check_constant_next("invalid #compose command, constant expected");
+    optional<name> gf;
+    if (p.curr_is_token(get_arrow_tk())) {
+        p.next();
+        name id = p.check_id_next("invalid #compose command, identifier expected");
+        gf = get_namespace(p.env()) + id;
+    }
+    auto r = compose(p.env(), g, f, gf);
+    p.regular_stream() << ">> " << r.second << "\n";
+    return r.first;
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",          "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -976,7 +991,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#erase_cache",  "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#projections",  "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
     add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd));
-
+    add_cmd(r, cmd_info("#compose",      "(for debugging purposes)", compose_cmd));
     register_decl_cmds(r);
     register_inductive_cmd(r);
     register_structure_cmd(r);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 6a529b1d7..e92cb1fb5 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -120,7 +120,7 @@ void init_token_table(token_table & t) {
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
-         nullptr};
+         "#compose", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
diff --git a/tests/lean/comp1.lean b/tests/lean/comp1.lean
new file mode 100644
index 000000000..bef01c8e6
--- /dev/null
+++ b/tests/lean/comp1.lean
@@ -0,0 +1,24 @@
+import data.real data.vector data.list
+open nat int rat
+
+#compose int.of_nat nat.of_num → num_to_int
+#compose int.of_nat nat.of_num → num_to_int_2
+set_option pp.all true
+
+print num_to_int
+
+check num_to_int
+check num_to_int_2 -- Error
+
+constant to_list {A : Type} {n : nat} : vector A n → list A
+constant to_vector {A : Type} (l : list A) : vector A (list.length l)
+constant matrix.{l} : Type.{l} → nat → nat → Type.{l}
+constant to_matrix {A : Type} {n : nat} : vector A n → matrix A n 1
+
+#compose list.length to_list → vec_len
+#compose to_matrix to_vector → list_to_matrix
+#compose to_matrix to_vector → list_to_matrix_2
+
+print vec_len
+print list_to_matrix
+check list_to_matrix_2 -- Error
diff --git a/tests/lean/comp1.lean.expected.out b/tests/lean/comp1.lean.expected.out
new file mode 100644
index 000000000..5ad2653c7
--- /dev/null
+++ b/tests/lean/comp1.lean.expected.out
@@ -0,0 +1,14 @@
+>> num_to_int
+>> num_to_int
+definition num_to_int : num → int :=
+λ (n : num), int.of_nat (nat.of_num n)
+num_to_int : num → int
+comp1.lean:11:6: error: unknown identifier 'num_to_int_2'
+>> vec_len
+>> list_to_matrix
+>> list_to_matrix
+definition vec_len : Π {A : Type.{l_1}} {n : nat}, vector.{l_1} A n → nat :=
+λ {A : Type.{l_1}} {n : nat} (a : vector.{l_1} A n), @list.length.{l_1} A (@to_list.{l_1} A n a)
+definition list_to_matrix : Π {A : Type.{l_1}} (l : list.{l_1} A), matrix.{l_1} A (@list.length.{l_1} A l) (nat.of_num 1) :=
+λ {A : Type.{l_1}} (l : list.{l_1} A), @to_matrix.{l_1} A (@list.length.{l_1} A l) (@to_vector.{l_1} A l)
+comp1.lean:24:6: error: unknown identifier 'list_to_matrix_2'