220 lines
7.5 KiB
C++
220 lines
7.5 KiB
C++
/*
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include <vector>
|
|
#include "util/test.h"
|
|
#include "kernel/environment.h"
|
|
#include "kernel/kernel_exception.h"
|
|
#include "kernel/builtin.h"
|
|
#include "kernel/abstract.h"
|
|
#include "kernel/printer.h"
|
|
#include "frontends/lean/frontend.h"
|
|
#include "frontends/lean/operator_info.h"
|
|
#include "frontends/lean/pp.h"
|
|
using namespace lean;
|
|
|
|
static void tst1() {
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
env->add_uvar("tst");
|
|
environment c = env->mk_child();
|
|
lean_assert(c->get_uvar("tst") == env->get_uvar("tst"));
|
|
lean_assert(env->has_children());
|
|
}
|
|
|
|
static void tst2() {
|
|
operator_info op1 = infixl(name("and"), 10);
|
|
operator_info op2 = infixr(name("implies"), 20);
|
|
lean_assert(op1.get_precedence() == 10);
|
|
lean_assert(op1.get_fixity() == fixity::Infixl);
|
|
op1.add_expr(mk_and_fn());
|
|
operator_info op3 = infixl(name("+"), 10);
|
|
op3.add_expr(Const(name{"Int", "plus"}));
|
|
op3.add_expr(Const(name{"Real", "plus"}));
|
|
std::cout << op3.get_denotations() << "\n";
|
|
lean_assert(length(op3.get_denotations()) == 2);
|
|
operator_info op4 = op3.copy();
|
|
op4.add_expr(Const(name{"Complex", "plus"}));
|
|
std::cout << op4.get_denotations() << "\n";
|
|
lean_assert(length(op3.get_denotations()) == 2);
|
|
lean_assert(length(op4.get_denotations()) == 3);
|
|
lean_assert(op4.get_fixity() == fixity::Infixl);
|
|
lean_assert(op4.get_op_name() == op3.get_op_name());
|
|
lean_assert(prefix("tst", 20).get_fixity() == fixity::Prefix);
|
|
lean_assert(postfix("!", 20).get_fixity() == fixity::Postfix);
|
|
lean_assert(length(mixfixl({"if", "then", "else"}, 10).get_op_name_parts()) == 3);
|
|
lean_assert(mixfixc({"if", "then", "else", "endif"}, 10).get_fixity() == fixity::Mixfixc);
|
|
std::cout << mixfixc({"if", "then", "else", "endif"}, 10).get_op_name_parts() << "\n";
|
|
std::cout << op4 << "\n";
|
|
std::cout << op2 << "\n";
|
|
std::cout << mixfixc({"if", "then", "else", "endif"}, 10) << "\n";
|
|
}
|
|
|
|
static void tst3() {
|
|
environment env;
|
|
std::cout << "====================\n";
|
|
std::cout << env << "\n";
|
|
}
|
|
|
|
static void tst4() {
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
formatter fmt = mk_pp_formatter(env);
|
|
context c;
|
|
c = extend(c, "x", Bool);
|
|
c = extend(c, "y", Bool);
|
|
c = extend(c, "x", Bool, Var(1));
|
|
c = extend(c, "x", Bool, Var(2));
|
|
c = extend(c, "z", Bool, Var(1));
|
|
c = extend(c, "x", Bool, Var(4));
|
|
std::cout << fmt(c) << "\n";
|
|
}
|
|
|
|
static void tst5() {
|
|
std::cout << "=================\n";
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
formatter fmt = mk_pp_formatter(env);
|
|
env->add_var("A", Type());
|
|
env->add_var("x", Const("A"));
|
|
optional<object> obj = env->find_object("x");
|
|
lean_assert(obj);
|
|
lean_assert(obj->get_name() == "x");
|
|
std::cout << fmt(*obj) << "\n";
|
|
optional<object> obj2 = env->find_object("y");
|
|
lean_assert(!obj2);
|
|
try {
|
|
env->get_object("y");
|
|
lean_unreachable();
|
|
} catch (unknown_name_exception & ex) {
|
|
std::cout << ex.what() << " " << ex.get_name() << "\n";
|
|
}
|
|
}
|
|
|
|
class alien_cell : public neutral_object_cell {
|
|
unsigned m_data[128];
|
|
public:
|
|
alien_cell() {}
|
|
unsigned & get_data(unsigned i) { return m_data[i]; }
|
|
virtual char const * keyword() const { return "alien"; }
|
|
};
|
|
|
|
static void tst6() {
|
|
std::cout << "=================\n";
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
env->add_neutral_object(new alien_cell());
|
|
formatter fmt = mk_pp_formatter(env);
|
|
std::cout << fmt(env) << "\n";
|
|
}
|
|
|
|
static void tst7() {
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
formatter fmt = mk_pp_formatter(env);
|
|
std::cout << fmt(And(Const("x"), Const("y"))) << "\n";
|
|
}
|
|
|
|
static void tst8() {
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
formatter fmt = mk_pp_formatter(env);
|
|
add_infixl(env, ios, "<-$->", 10, mk_refl_fn());
|
|
std::cout << fmt(*(env->find_object("Trivial"))) << "\n";
|
|
}
|
|
|
|
static void tst9() {
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
lean_assert(!env->has_children());
|
|
{
|
|
environment c = env->mk_child();
|
|
lean_assert(env->has_children());
|
|
}
|
|
lean_assert(!env->has_children());
|
|
env->add_uvar("l", level()+1);
|
|
lean_assert(env->get_uvar("l") == level("l"));
|
|
try { env->get_uvar("l2"); lean_unreachable(); }
|
|
catch (exception &) {}
|
|
env->add_definition("x", Bool, True);
|
|
object const & obj = env->get_object("x");
|
|
lean_assert(obj.get_name() == "x");
|
|
lean_assert(is_bool(obj.get_type()));
|
|
lean_assert(obj.get_value() == True);
|
|
try { env->get_object("y"); lean_unreachable(); }
|
|
catch (exception &) {}
|
|
lean_assert(!env->find_object("y"));
|
|
env->add_definition("y", False);
|
|
lean_assert(is_bool(env->find_object("y")->get_type()));
|
|
lean_assert(env->has_object("y"));
|
|
lean_assert(!env->has_object("z"));
|
|
bool found = false;
|
|
std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) { if (obj.has_name() && obj.get_name() == "y") found = true; });
|
|
lean_assert(found);
|
|
add_postfix(env, ios, "!", 10, Const("factorial"));
|
|
name parts[] = {"if", "then", "else"};
|
|
add_mixfixl(env, ios, 3, parts, 10, Const("if"));
|
|
}
|
|
|
|
static void tst10() {
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
formatter fmt = mk_pp_formatter(env);
|
|
expr x = Const("xxxxxxxxxxxx");
|
|
expr y = Const("y");
|
|
expr z = Const("foo");
|
|
expr e = Let({{x, True}, {y, And({x, x, x, x, x, x, x, x})}, {z, And(x, y)}}, Or({x, x, x, x, x, x, x, x, x, z, z, z, z, z, z, z}));
|
|
std::cout << e << "\n";
|
|
std::cout << fmt(e) << "\n";
|
|
}
|
|
|
|
static void tst11() {
|
|
environment env; io_state ios; init_frontend(env, ios);
|
|
expr A = Const("A");
|
|
env->add_var("g", Pi({A, Type()}, A >> (A >> A)));
|
|
lean_assert(!has_implicit_arguments(env, "g"));
|
|
mark_implicit_arguments(env, "g", {true, false, false});
|
|
lean_assert(has_implicit_arguments(env, "g"))
|
|
name gexp = get_explicit_version(env, "g");
|
|
lean_assert(env->find_object(gexp));
|
|
lean_assert(env->find_object("g")->get_type() == env->find_object(gexp)->get_type());
|
|
lean_assert(get_implicit_arguments(env, "g") == std::vector<bool>({true})); // the trailing "false" marks are removed
|
|
try {
|
|
mark_implicit_arguments(env, "g", {true, false, false});
|
|
lean_unreachable();
|
|
} catch (exception & ex) {
|
|
std::cout << "Expected error: " << ex.what() << std::endl;
|
|
}
|
|
env->add_var("s", Pi({A, Type()}, A >> (A >> A)));
|
|
try {
|
|
mark_implicit_arguments(env, "s", {true, true, true, true});
|
|
lean_unreachable();
|
|
} catch (exception & ex) {
|
|
std::cout << "Expected error: " << ex.what() << std::endl;
|
|
}
|
|
env->add_var(name("@h"), Pi({A, Type()}, A >> (A >> A)));
|
|
env->add_var("h", Pi({A, Type()}, A >> (A >> A)));
|
|
try {
|
|
mark_implicit_arguments(env, "h", {true, false, false});
|
|
lean_unreachable();
|
|
} catch (exception & ex) {
|
|
std::cout << "Expected error: " << ex.what() << std::endl;
|
|
}
|
|
try {
|
|
mark_implicit_arguments(env, "u", {true, false});
|
|
lean_unreachable();
|
|
} catch (exception & ex) {
|
|
std::cout << "Expected error: " << ex.what() << std::endl;
|
|
}
|
|
}
|
|
|
|
int main() {
|
|
save_stack_info();
|
|
tst1();
|
|
tst2();
|
|
tst3();
|
|
tst4();
|
|
tst5();
|
|
tst6();
|
|
tst7();
|
|
tst8();
|
|
tst9();
|
|
tst10();
|
|
tst11();
|
|
return has_violations() ? 1 : 0;
|
|
}
|