feat(frontends/lean/builtin_cmds): add 'print prefix' command

This commit is contained in:
Leonardo de Moura 2014-11-04 08:40:32 -08:00
parent 3454e70017
commit d58c3e498d
3 changed files with 43 additions and 12 deletions

View file

@ -73,6 +73,23 @@ static void print_axioms(parser & p) {
p.regular_stream() << "no axioms" << endl; p.regular_stream() << "no axioms" << endl;
} }
static void print_prefix(parser & p) {
name prefix = p.check_id_next("invalid 'print prefix' command, identifier expected");
environment const & env = p.env();
buffer<declaration> to_print;
env.for_each_declaration([&](declaration const & d) {
if (is_prefix_of(prefix, d.get_name())) {
to_print.push_back(d);
}
});
std::sort(to_print.begin(), to_print.end(), [](declaration const & d1, declaration const & d2) { return d1.get_name() < d2.get_name(); });
for (declaration const & d : to_print) {
p.regular_stream() << d.get_name() << " : " << d.get_type() << endl;
}
if (to_print.empty())
p.regular_stream() << "no declaration starting with prefix '" << prefix << "'" << endl;
}
environment print_cmd(parser & p) { environment print_cmd(parser & p) {
if (p.curr() == scanner::token_kind::String) { if (p.curr() == scanner::token_kind::String) {
p.regular_stream() << p.get_str_val() << endl; p.regular_stream() << p.get_str_val() << endl;
@ -112,6 +129,9 @@ environment print_cmd(parser & p) {
for (name const & c : classes) { for (name const & c : classes) {
p.regular_stream() << c << " : " << env.get(c).get_type() << endl; p.regular_stream() << c << " : " << env.get(c).get_type() << endl;
} }
} else if (p.curr_is_token_or_id(get_prefix_tk())) {
p.next();
print_prefix(p);
} else if (p.curr_is_token_or_id(get_coercions_tk())) { } else if (p.curr_is_token_or_id(get_coercions_tk())) {
p.next(); p.next();
optional<name> C; optional<name> C;

View file

@ -75,6 +75,8 @@ end
structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
print prefix algebra.comm_monoid
structure Semigroup := structure Semigroup :=
mk :: (carrier : Type) (struct : semigroup carrier) mk :: (carrier : Type) (struct : semigroup carrier)
@ -107,15 +109,15 @@ section examples
theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) := theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
calc calc
a * (b * c) * d = a * b * c * d : {symm !mul_assoc} a * (b * c) * d = a * b * c * d : mul_assoc
... = a * b * (c * d) : !mul_assoc ... = a * b * (c * d) : mul_assoc
theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) := theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
calc calc
a * (b * c) * d = a * b * c * d : {symm !mul_assoc} a * (b * c) * d = a * b * c * d : mul_assoc
... = a * b * (c * d) : !mul_assoc ... = a * b * (c * d) : mul_assoc
-- for test4b to work, we need instances at the level of the bundled structures as well -- for test4b to work, we need instances at the level of the bundled structures as well
definition Monoid_Semigroup [coercion] (M : Monoid) : Semigroup := definition Monoid_Semigroup [coercion] (M : Monoid) : Semigroup :=
@ -126,21 +128,21 @@ test1 a b c d
theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) := theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc calc
a * 1 * b * c = a * b * c : {!mul_right_id} a * 1 * b * c = a * b * c : mul_right_id
... = a * (b * c) : !mul_assoc ... = a * (b * c) : mul_assoc
theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) := theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc calc
a * 1 * b * c = a * b * c : {!mul_right_id} a * 1 * b * c = a * b * c : mul_right_id
... = a * (b * c) : !mul_assoc ... = a * (b * c) : mul_assoc
theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) := theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
calc calc
a * 1 * b * c = a * b * c : {!mul_right_id} a * 1 * b * c = a * b * c : mul_right_id
... = a * (b * c) : !mul_assoc ... = a * (b * c) : mul_assoc
theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) := theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc calc
a * 1 * b * c = a * b * c : {!mul_right_id} a * 1 * b * c = a * b * c : mul_right_id
... = a * (b * c) : !mul_assoc ... = a * (b * c) : mul_assoc
end examples end examples

View file

@ -0,0 +1,9 @@
import logic data.unit
structure point (A : Type) (B : Type) :=
mk :: (x : A) (y : B)
structure point2 (A : Type) (B : Type) extends point A B :=
make
print prefix point2