feat(frontends/lean): add '#compose' command for testing composition manager

This commit is contained in:
Leonardo de Moura 2015-06-17 14:42:25 -07:00
parent c59e1f49db
commit 9e6e406f73
4 changed files with 55 additions and 2 deletions

View file

@ -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);

View file

@ -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"},

24
tests/lean/comp1.lean Normal file
View file

@ -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

View file

@ -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'