chore(tests/frontends/lean): remove tests for old parser
This commit is contained in:
Leonardo de Moura
parent
bdd2a53d6a
commit
87b5fd70af
6 changed files with 0 additions and 693 deletions
|
|
@ -451,7 +451,6 @@ endfunction()
|
|||
add_subdirectory(tests/util)
|
||||
add_subdirectory(tests/kernel)
|
||||
add_subdirectory(tests/library)
|
||||
add_subdirectory(tests/frontends/lean)
|
||||
add_subdirectory(tests/shell)
|
||||
|
||||
# Include style check
|
||||
|
|
|
|||
|
|
@ -1,9 +0,0 @@
|
|||
add_executable(lean_scanner scanner.cpp ${LEAN_OBJS})
|
||||
target_link_libraries(lean_scanner ${EXTRA_LIBS})
|
||||
add_exec_test(lean_scanner "lean_scanner")
|
||||
# add_executable(lean_parser parser.cpp)
|
||||
# target_link_libraries(lean_parser ${ALL_LIBS})
|
||||
# add_exec_test(lean_parser "lean_parser")
|
||||
# # add_executable(lean_pp pp.cpp)
|
||||
# target_link_libraries(lean_pp ${ALL_LIBS})
|
||||
# add_exec_test(lean_pp "lean_pp")
|
||||
|
|
@ -1,225 +0,0 @@
|
|||
/*
|
||||
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/kernel.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "library/printer.h"
|
||||
#include "library/bin_op.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "frontends/lean/frontend.h"
|
||||
#include "frontends/lean/operator_info.h"
|
||||
#include "frontends/lean/pp.h"
|
||||
#include "frontends/lua/register_modules.h"
|
||||
using namespace lean;
|
||||
|
||||
static void tst1() {
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
env->add_uvar_cnstr("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);
|
||||
formatter fmt = mk_pp_formatter(env);
|
||||
context c;
|
||||
c = extend(c, "x", Prop);
|
||||
c = extend(c, "y", Prop);
|
||||
c = extend(c, "x", Prop, Var(1));
|
||||
c = extend(c, "x", Prop, Var(2));
|
||||
c = extend(c, "z", Prop, Var(1));
|
||||
c = extend(c, "x", Prop, Var(4));
|
||||
std::cout << fmt(c) << "\n";
|
||||
}
|
||||
|
||||
static void tst5() {
|
||||
std::cout << "=================\n";
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
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"; }
|
||||
virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
|
||||
};
|
||||
|
||||
static void tst6() {
|
||||
std::cout << "=================\n";
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
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);
|
||||
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);
|
||||
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);
|
||||
lean_assert(!env->has_children());
|
||||
{
|
||||
environment c = env->mk_child();
|
||||
lean_assert(env->has_children());
|
||||
}
|
||||
lean_assert(!env->has_children());
|
||||
env->add_uvar_cnstr("l", level()+1);
|
||||
lean_assert(env->get_uvar("l") == level("l"));
|
||||
try { env->get_uvar("l2"); lean_unreachable(); }
|
||||
catch (exception &) {}
|
||||
env->add_definition("x", Prop, 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);
|
||||
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);
|
||||
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();
|
||||
register_modules();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
tst4();
|
||||
tst5();
|
||||
tst6();
|
||||
tst7();
|
||||
tst8();
|
||||
tst9();
|
||||
tst10();
|
||||
tst11();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
@ -1,118 +0,0 @@
|
|||
/*
|
||||
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 <sstream>
|
||||
#include <memory>
|
||||
#include "util/test.h"
|
||||
#include "util/exception.h"
|
||||
#include "util/numerics/mpq.h"
|
||||
#include "kernel/kernel.h"
|
||||
#include "library/printer.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "library/arith/arith.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/frontend.h"
|
||||
#include "frontends/lean/pp.h"
|
||||
#include "frontends/lua/register_modules.h"
|
||||
using namespace lean;
|
||||
|
||||
static void parse(environment const & env, io_state const & ios, char const * str) {
|
||||
environment child = env->mk_child();
|
||||
io_state ios_copy = ios;
|
||||
std::istringstream in(str);
|
||||
if (parse_commands(child, ios_copy, in, "[string]")) {
|
||||
formatter fmt = mk_pp_formatter(env);
|
||||
std::for_each(child->begin_local_objects(),
|
||||
child->end_local_objects(),
|
||||
[&](object const & obj) {
|
||||
std::cout << fmt(obj) << "\n";
|
||||
std::cout << obj << "\n";
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
static void parse_error(environment const & env, io_state const & ios, char const * str) {
|
||||
try {
|
||||
parse(env, ios, str);
|
||||
lean_unreachable();
|
||||
} catch (exception & ex) {
|
||||
std::cout << "expected error: " << ex.what() << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
static void tst1() {
|
||||
environment env; io_state ios = init_test_frontend(env);
|
||||
parse(env, ios, "variable x : Prop variable y : Prop axiom H : x && y || x -> x");
|
||||
parse(env, ios, "eval true && true");
|
||||
parse(env, ios, "print true && false eval true && false");
|
||||
parse(env, ios, "infixl 35 & : and print true & false & false eval true & false");
|
||||
parse(env, ios, "notation 100 if _ then _ fi : implies print if true then false fi");
|
||||
parse(env, ios, "print forall (A : Type), A -> A");
|
||||
parse(env, ios, "check forall (A : Type), A -> A");
|
||||
}
|
||||
|
||||
static void check(environment const & env, io_state & ios, char const * str, expr const & expected) {
|
||||
std::istringstream in(str);
|
||||
try {
|
||||
expr got = parse_expr(env, ios, in, "[string]");
|
||||
lean_assert(expected == got);
|
||||
} catch (exception &) {
|
||||
lean_unreachable();
|
||||
}
|
||||
}
|
||||
|
||||
static void tst2() {
|
||||
environment env; io_state ios = init_test_frontend(env);
|
||||
env->add_var("x", Prop);
|
||||
env->add_var("y", Prop);
|
||||
env->add_var("z", Prop);
|
||||
expr x = Const("x"); expr y = Const("y"); expr z = Const("z");
|
||||
check(env, ios, "x && y", And(x, y));
|
||||
check(env, ios, "x && y || z", Or(And(x, y), z));
|
||||
check(env, ios, "x || y && z", Or(x, And(y, z)));
|
||||
check(env, ios, "x || y || x && z", Or(x, Or(y, And(x, z))));
|
||||
check(env, ios, "x || y || x && z -> x && y", mk_arrow(Or(x, Or(y, And(x, z))), And(x, y)));
|
||||
check(env, ios, "x ∨ y ∨ x ∧ z → x ∧ y", mk_arrow(Or(x, Or(y, And(x, z))), And(x, y)));
|
||||
check(env, ios, "x→y→z→x", mk_arrow(x, mk_arrow(y, mk_arrow(z, x))));
|
||||
check(env, ios, "x->y->z->x", mk_arrow(x, mk_arrow(y, mk_arrow(z, x))));
|
||||
check(env, ios, "x->(y->z)->x", mk_arrow(x, mk_arrow(mk_arrow(y, z), x)));
|
||||
}
|
||||
|
||||
static void tst3() {
|
||||
environment env; io_state ios = init_test_frontend(env);
|
||||
parse(env, ios, "help");
|
||||
parse(env, ios, "help options");
|
||||
parse_error(env, ios, "help print");
|
||||
check(env, ios, "10.3", mk_real_value(mpq(103, 10)));
|
||||
parse(env, ios, "variable f : Real -> Real. check f 10.3.");
|
||||
parse(env, ios, "variable g : (Type 1) -> Type. check g Type");
|
||||
parse_error(env, ios, "check fun .");
|
||||
parse_error(env, ios, "definition foo .");
|
||||
parse_error(env, ios, "check a");
|
||||
parse_error(env, ios, "check U");
|
||||
parse(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 ; 20.1 ].");
|
||||
parse_error(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 | 20.1 ].");
|
||||
parse_error(env, ios, "set_option pp::indent true");
|
||||
parse(env, ios, "set_option pp::indent 10");
|
||||
parse_error(env, ios, "set_option pp::colors foo");
|
||||
parse_error(env, ios, "set_option pp::colors \"foo\"");
|
||||
parse(env, ios, "set_option pp::colors true");
|
||||
parse_error(env, ios, "notation 10 : Int::add");
|
||||
parse_error(env, ios, "notation 10 _ : Int::add");
|
||||
parse(env, ios, "notation 10 _ ++ _ : Int::add. eval 10 ++ 20.");
|
||||
parse(env, ios, "notation 10 _ -+ : Int::neg. eval 10 -+");
|
||||
parse(env, ios, "notation 30 -+ _ : Int::neg. eval -+ 10");
|
||||
parse_error(env, ios, "10 + 30");
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
register_modules();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
@ -1,117 +0,0 @@
|
|||
/*
|
||||
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 "util/test.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/kernel.h"
|
||||
#include "library/printer.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "frontends/lean/frontend.h"
|
||||
#include "frontends/lean/pp.h"
|
||||
#include "frontends/lua/register_modules.h"
|
||||
using namespace lean;
|
||||
|
||||
static expr mk_shared_expr(unsigned depth) {
|
||||
expr f = Const("f");
|
||||
expr a = Const("a");
|
||||
expr r = a;
|
||||
for (unsigned i = 0; i < depth; i++)
|
||||
r = f(r, r);
|
||||
return r;
|
||||
}
|
||||
|
||||
static void tst1() {
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
formatter fmt = mk_pp_formatter(env);
|
||||
std::cout << "Basic printer\n";
|
||||
std::cout << mk_shared_expr(10) << std::endl;
|
||||
std::cout << "----------------------------\nPretty printer\n";
|
||||
std::cout << fmt(mk_shared_expr(10)) << std::endl;
|
||||
}
|
||||
|
||||
static void tst2() {
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
formatter fmt = mk_pp_formatter(env);
|
||||
expr a = Const("a");
|
||||
expr t = Fun({a, Type()}, mk_shared_expr(10));
|
||||
expr g = Const("g");
|
||||
std::cout << fmt(g(t, t, t)) << std::endl;
|
||||
formatter fmt2 = mk_pp_formatter(env);
|
||||
std::cout << fmt2(g(t, t, t), options({"lean", "pp", "alias_min_weight"}, 100)) << std::endl;
|
||||
}
|
||||
|
||||
static void tst3() {
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
formatter fmt = mk_pp_formatter(env);
|
||||
expr g = Const("g");
|
||||
expr a = Const("\u03BA");
|
||||
expr b = Const("\u03C1");
|
||||
expr c = Const("\u03BD");
|
||||
expr d = Const(name("\u03BD", 1u));
|
||||
expr t = g(a, mk_shared_expr(5));
|
||||
std::cout << "----------------\n";
|
||||
std::cout << fmt(t) << "\n----------------\n";
|
||||
std::cout << fmt(g(b, t)) << "\n----------------\n";
|
||||
std::cout << fmt(g(c, b, t)) << "\n----------------\n";
|
||||
std::cout << fmt(g(d, c, b, t)) << "\n";
|
||||
}
|
||||
|
||||
static void tst4() {
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
io_state const & s1 = ios;
|
||||
io_state s2 = ios;
|
||||
regular(s1) << And(Const("a"), Const("b")) << "\n";
|
||||
regular(ios) << And(Const("a"), Const("b")) << "\n";
|
||||
diagnostic(ios) << And(Const("a"), Const("b")) << "\n";
|
||||
ios.set_option(name{"lean", "pp", "notation"}, false);
|
||||
regular(ios) << And(Const("a"), Const("b")) << "\n";
|
||||
regular(s1) << And(Const("a"), Const("b")) << "\n";
|
||||
regular(s2) << And(Const("a"), Const("b")) << "\n";
|
||||
}
|
||||
|
||||
static void tst5() {
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
std::shared_ptr<string_output_channel> out(std::make_shared<string_output_channel>());
|
||||
ios.set_regular_channel(out);
|
||||
ios.set_option(name{"pp", "unicode"}, true);
|
||||
ios.set_option(name{"lean", "pp", "notation"}, true);
|
||||
regular(ios) << And(Const("a"), Const("b"));
|
||||
lean_assert(out->str() == "a ∧ b");
|
||||
ios.set_option(name{"lean", "pp", "notation"}, false);
|
||||
regular(ios) << " " << And(Const("a"), Const("b"));
|
||||
lean_assert(out->str() == "a ∧ b and a b");
|
||||
}
|
||||
|
||||
static expr mk_deep(unsigned depth) {
|
||||
if (depth == 0)
|
||||
return Const("a");
|
||||
else
|
||||
return Const("f")(mk_deep(depth - 1));
|
||||
}
|
||||
|
||||
static void tst6() {
|
||||
environment env; io_state ios = init_frontend(env);
|
||||
std::shared_ptr<string_output_channel> out(std::make_shared<string_output_channel>());
|
||||
ios.set_regular_channel(out);
|
||||
expr t = mk_deep(10);
|
||||
ios.set_option(name{"lean", "pp", "max_depth"}, 5);
|
||||
ios.set_option(name{"pp", "colors"}, false);
|
||||
ios.set_option(name{"pp", "unicode"}, false);
|
||||
regular(ios) << t;
|
||||
lean_assert(out->str() == "f (f (f (f (f (...)))))");
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
register_modules();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
tst4();
|
||||
tst5();
|
||||
tst6();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
@ -1,223 +0,0 @@
|
|||
/*
|
||||
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 <sstream>
|
||||
#include <string>
|
||||
#include "runtime/exception.h"
|
||||
#include "util/test.h"
|
||||
#include "util/escaped.h"
|
||||
#include "frontends/lean/scanner.h"
|
||||
#include "frontends/lean/parser_config.h"
|
||||
#include "init/init.h"
|
||||
using namespace lean;
|
||||
|
||||
#define tk token_kind
|
||||
|
||||
static void scan(char const * str, environment const & env = environment()) {
|
||||
std::istringstream in(str);
|
||||
scanner s(in, "[string]");
|
||||
while (true) {
|
||||
tk k = s.scan(env);
|
||||
if (k == tk::Eof)
|
||||
break;
|
||||
if (k == tk::Identifier)
|
||||
std::cout << "id[" << s.get_name_val() << "]";
|
||||
else if (k == tk::CommandKeyword)
|
||||
std::cout << "cmd[" << s.get_token_info().value() << "]";
|
||||
else if (k == tk::Keyword)
|
||||
std::cout << "tk[" << s.get_token_info().value() << "]";
|
||||
else if (k == tk::Decimal || k == tk::Numeral)
|
||||
std::cout << "n[" << s.get_num_val() << "]";
|
||||
else if (k == tk::String)
|
||||
std::cout << "[\"" << escaped(s.get_str_val().c_str()) << "\"]";
|
||||
std::cout << ":" << s.get_pos() << ":" << s.get_line() << " ";
|
||||
}
|
||||
std::cout << "\n";
|
||||
}
|
||||
|
||||
static void scan_success(char const * str, environment const & env = environment()) {
|
||||
try {
|
||||
scan(str, env);
|
||||
} catch (exception & ex) {
|
||||
std::cout << "ERROR: " << ex.what() << "\n";
|
||||
lean_unreachable();
|
||||
}
|
||||
}
|
||||
|
||||
static void scan_error(char const * str) {
|
||||
try {
|
||||
scan(str);
|
||||
lean_unreachable();
|
||||
} catch (exception & ex) {
|
||||
std::cout << "expected error: " << ex.what() << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
static void check(char const * str, std::initializer_list<tk> const & l,
|
||||
environment const & env = environment()) {
|
||||
try {
|
||||
auto it = l.begin();
|
||||
std::istringstream in(str);
|
||||
scanner s(in, "[string]");
|
||||
while (true) {
|
||||
tk k = s.scan(env);
|
||||
if (k == tk::Eof) {
|
||||
lean_assert(it == l.end());
|
||||
return;
|
||||
}
|
||||
lean_assert(it != l.end());
|
||||
lean_assert_eq(k, *it);
|
||||
++it;
|
||||
}
|
||||
} catch (exception & ex) {
|
||||
std::cout << "ERROR: " << ex.what() << "\n";
|
||||
lean_unreachable();
|
||||
}
|
||||
}
|
||||
|
||||
static void check_name(char const * str, name const & expected, environment const & env = environment()) {
|
||||
std::istringstream in(str);
|
||||
scanner s(in, "[string]");
|
||||
tk k = s.scan(env);
|
||||
lean_assert(k == tk::Identifier);
|
||||
lean_assert(s.get_name_val() == expected);
|
||||
lean_assert(s.scan(env) == tk::Eof);
|
||||
}
|
||||
|
||||
static void check_keyword(char const * str, name const & expected, environment const & env = environment()) {
|
||||
std::istringstream in(str);
|
||||
scanner s(in, "[string]");
|
||||
tk k = s.scan(env);
|
||||
lean_assert(k == tk::Keyword);
|
||||
lean_assert(s.get_token_info().value() == expected);
|
||||
lean_assert(s.scan(env) == tk::Eof);
|
||||
}
|
||||
|
||||
static void tst1() {
|
||||
environment env;
|
||||
token_table s = get_token_table(env);
|
||||
env = add_token(env, "+", 0);
|
||||
env = add_token(env, "=", 0);
|
||||
scan_success("a..a");
|
||||
check("Type.{0}", {tk::Keyword, tk::Keyword, tk::Numeral, tk::Keyword});
|
||||
env = add_token(env, "ab+cde", 0);
|
||||
env = add_token(env, "+cd", 0);
|
||||
scan_success("ab+cd", env);
|
||||
check("ab+cd", {tk::Identifier, tk::Keyword}, env);
|
||||
scan_success("ab+cde", env);
|
||||
check("ab+cde", {tk::Keyword}, env);
|
||||
scan_success("Type.{0}");
|
||||
scan_success("0.a a");
|
||||
scan_success("0.");
|
||||
scan_success("0..");
|
||||
scan_success("fun");
|
||||
scan_success("..");
|
||||
scan_success("....");
|
||||
scan_success("....\n..");
|
||||
scan_success("a", env);
|
||||
scan_success("a. b.c..");
|
||||
scan_success(".. ..");
|
||||
scan_success("....\n..");
|
||||
scan_success("fun(x: forall A : Type, A -> A), x+1 = 2.0 λvalue.foo. . . a", env);
|
||||
}
|
||||
|
||||
static void tst2() {
|
||||
scan("x.name");
|
||||
scan("x.foo");
|
||||
check("x.name", {tk::Identifier});
|
||||
check("fun (x : Prop), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Identifier,
|
||||
tk::Keyword, tk::Keyword, tk::Identifier});
|
||||
check_name("x10", name("x10"));
|
||||
// check_name("x.10", name(name("x"), 10));
|
||||
check_name("x.bla", name({"x", "bla"}));
|
||||
|
||||
scan_error("***");
|
||||
environment env;
|
||||
token_table s = mk_default_token_table();
|
||||
env = add_token(env, "***", 0);
|
||||
check_keyword("***", "***", env);
|
||||
env = add_token(env, "+", 0);
|
||||
check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
|
||||
check("-- testing", {});
|
||||
check("/- testing -/", {});
|
||||
check("/- /- testing\n -/ -/", {});
|
||||
check(" 2.31 ", {tk::Decimal});
|
||||
check("2.31", {tk::Decimal});
|
||||
check(" 333 22", {tk::Numeral, tk::Numeral});
|
||||
check("int -> int", {tk::Identifier, tk::Keyword, tk::Identifier});
|
||||
check("int->int", {tk::Identifier, tk::Keyword, tk::Identifier});
|
||||
check_keyword("->", "->");
|
||||
env = add_token(env, "-+->", 0);
|
||||
check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
|
||||
check("x := 10", {tk::Identifier, tk::Keyword, tk::Numeral});
|
||||
check("{x}", {tk::Keyword, tk::Identifier, tk::Keyword});
|
||||
check("λ ∀ →", {tk::Keyword, tk::Keyword, tk::Keyword});
|
||||
check_keyword("λ", "fun");
|
||||
scan("theorem a : Prop axiom b : Int");
|
||||
check("theorem a : Prop axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier,
|
||||
tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier});
|
||||
scan("foo \"ttk\\\"\" : Int");
|
||||
check("foo \"ttk\\\"\" : Int", {tk::Identifier, tk::String, tk::Keyword, tk::Identifier});
|
||||
scan_error("\"foo");
|
||||
scan("2.13 1.2 0.5");
|
||||
}
|
||||
|
||||
static void tst3() {
|
||||
scan_error("\"\\");
|
||||
scan_error("\"\\a");
|
||||
scan("\"\naaa\"");
|
||||
scan_error("foo.* 01");
|
||||
scan("10.0.");
|
||||
scan("{ } . forall exists let in ∀ := _");
|
||||
}
|
||||
|
||||
static void tst4(unsigned N) {
|
||||
std::string big;
|
||||
for (unsigned i = 0; i < N; i++)
|
||||
big += "aaa ";
|
||||
std::istringstream in(big);
|
||||
environment env;
|
||||
scanner s(in, "[string]");
|
||||
unsigned i = 0;
|
||||
while (true) {
|
||||
tk k = s.scan(env);
|
||||
if (k == tk::Eof)
|
||||
break;
|
||||
i++;
|
||||
}
|
||||
std::cout << i << "\n";
|
||||
}
|
||||
|
||||
static void tst_id_escape() {
|
||||
check_name("«a»", name("a"));
|
||||
check_name("«a».b", name({"a", "b"}));
|
||||
check_name("a.«b»", name({"a", "b"}));
|
||||
check_name("a.«b».c", name({"a", "b", "c"}));
|
||||
|
||||
check_name("«a.b».c", name({"a.b", "c"}));
|
||||
check_name("«a b».c", name({"a b", "c"}));
|
||||
check_name("«a🍏b».c", name({"a🍏b", "c"}));
|
||||
|
||||
check_name("a«b»", "ab");
|
||||
check_name("«a»b", "ab");
|
||||
|
||||
scan_error("«");
|
||||
scan_error("«a");
|
||||
scan_error("«a\nb»");
|
||||
scan_error("a.«");
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
initialize();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
tst4(100000);
|
||||
tst_id_escape();
|
||||
finalize();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue