michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Move elaborator to lean default frontend. It is getting too specific

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-01 18:16:26 -07:00
parent 42be7a4989
commit e8c09015ad
13 changed files with 79 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/CMakeLists.txt
View file

@ -1,2 +1,3 @@
add_library(lean_frontend lean_frontend.cpp lean_operator_info.cpp lean_scanner.cpp lean_parser.cpp lean_pp.cpp lean_notation.cpp)
add_library(lean_frontend lean_frontend.cpp lean_operator_info.cpp lean_scanner.cpp lean_parser.cpp lean_pp.cpp
lean_notation.cpp lean_elaborator.cpp lean_elaborator_exception.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

15
src/library/elaborator.cpp → src/frontends/lean/lean_elaborator.cpp
View file

@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <deque>
#include "elaborator.h"
#include "normalize.h"
#include "metavar.h"
#include "printer.h"
@ -17,7 +16,9 @@ Author: Leonardo de Moura
#include "replace.h"
#include "expr_pair.h"
#include "flet.h"
#include "elaborator_exception.h"
#include "lean_frontend.h"
#include "lean_elaborator.h"
#include "lean_elaborator_exception.h"
namespace lean {
static name g_choice_name(name(name(name(0u), "library"), "choice"));
@ -78,6 +79,7 @@ class elaborator::imp {
typedef std::deque<constraint> constraint_queue;
typedef std::vector<metavar_info> metavars;
frontend const & m_frontend;
environment const & m_env;
name_set const * m_available_defs;
elaborator const * m_owner;
@ -626,10 +628,11 @@ class elaborator::imp {
}
public:
imp(environment const & env, name_set const * defs):
m_env(env),
imp(frontend const & fe, name_set const * defs):
m_frontend(fe),
m_env(fe.get_environment()),
m_available_defs(defs),
m_normalizer(env) {
m_normalizer(m_env) {
m_interrupted = false;
m_owner = nullptr;
}
@ -713,7 +716,7 @@ public:
return r;
}
};
elaborator::elaborator(environment const & env):m_ptr(new imp(env, nullptr)) {}
elaborator::elaborator(frontend const & fe):m_ptr(new imp(fe, nullptr)) {}
elaborator::~elaborator() {}
expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, *this); }
expr const & elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); }

3
src/library/elaborator.h → src/frontends/lean/lean_elaborator.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "formatter.h"
namespace lean {
class frontend;
/**
\brief Expression elaborator, it is responsible for "filling" holes
in terms left by the user. This is the main module resposible for computing
@ -20,7 +21,7 @@ class elaborator {
std::shared_ptr<imp> m_ptr;
static void print(imp * ptr);
public:
explicit elaborator(environment const & env);
explicit elaborator(frontend const & fe);
~elaborator();
expr operator()(expr const & e);

32
src/frontends/lean/lean_elaborator_exception.cpp Normal file
View file

@ -0,0 +1,32 @@
/*
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 "lean_elaborator_exception.h"
#include "lean_elaborator.h"
namespace lean {
format pp(formatter fmt, elaborator_exception const & ex, options const & opts) {
unsigned indent = get_pp_indent(opts);
format expr_f = fmt(ex.get_context(), ex.get_expr(), false, opts);
format elb_f = ex.get_elaborator().pp(fmt, opts);
return format({format(ex.what()), space(), format("at term"),
nest(indent, compose(line(), expr_f)),
line(), format("Elaborator state"),
nest(indent, compose(line(), elb_f))});
}
regular const & operator<<(regular const & out, elaborator_exception const & ex) {
options const & opts = out.m_state.get_options();
out.m_state.get_regular_channel().get_stream() << mk_pair(pp(out.m_state.get_formatter(), ex, opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex) {
options const & opts = out.m_state.get_options();
out.m_state.get_diagnostic_channel().get_stream() << mk_pair(pp(out.m_state.get_formatter(), ex, opts), opts);
return out;
}
}

7
src/library/elaborator_exception.h → src/frontends/lean/lean_elaborator_exception.h
View file

@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "elaborator.h"
#include "lean_elaborator.h"
#include "kernel_exception.h"
#include "state.h"
namespace lean {
/**
@ -53,4 +54,8 @@ public:
unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s):elaborator_exception(elb, ctx, s) {}
virtual char const * what() const noexcept { return "type mismatch during term elaboration"; }
};
format pp(formatter fmt, elaborator_exception const & ex, options const & opts);
regular const & operator<<(regular const & out, elaborator_exception const & ex);
diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex);
}

4
src/frontends/lean/lean_parser.cpp
View file

@ -18,10 +18,10 @@ Author: Leonardo de Moura
#include "expr_maps.h"
#include "sstream.h"
#include "kernel_exception.h"
#include "elaborator_exception.h"
#include "metavar.h"
#include "elaborator.h"
#include "lean_frontend.h"
#include "lean_elaborator.h"
#include "lean_elaborator_exception.h"
#include "lean_parser.h"
#include "lean_scanner.h"
#include "lean_notation.h"

2
src/library/CMakeLists.txt
View file

@ -1,4 +1,4 @@
add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
state.cpp metavar.cpp elaborator.cpp update_expr.cpp)
state.cpp metavar.cpp update_expr.cpp)
target_link_libraries(library ${LEAN_LIBS})

12
src/library/formatter.cpp
View file

@ -8,8 +8,6 @@ Author: Leonardo de Moura
#include "formatter.h"
#include "printer.h"
#include "kernel_exception.h"
#include "elaborator_exception.h"
#include "elaborator.h"
namespace lean {
class simple_formatter_cell : public formatter_cell {
@ -79,14 +77,4 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
return format(ex.what());
}
}
format formatter::operator()(elaborator_exception const & ex, options const & opts) {
unsigned indent = get_pp_indent(opts);
format expr_f = operator()(ex.get_context(), ex.get_expr(), false, opts);
format elb_f = ex.get_elaborator().pp(*this, opts);
return format({format(ex.what()), space(), format("at term"),
nest(indent, compose(line(), expr_f)),
line(), format("Elaborator state"),
nest(indent, compose(line(), elb_f))});
}
}

3
src/library/formatter.h
View file

@ -38,7 +38,6 @@ public:
virtual void set_interrupt(bool flag) {}
};
class kernel_exception;
class elaborator_exception;
class formatter {
std::shared_ptr<formatter_cell> m_cell;
public:
@ -51,8 +50,6 @@ public:
format operator()(environment const & env, options const & opts = options()) { return (*m_cell)(env, opts); }
/** \brief Pretty print a kernel exception using the this formatter */
format operator()(kernel_exception const & ex, options const & opts = options());
/** \brief Pretty print a elaborator exception using the this formatter */
format operator()(elaborator_exception const & ex, options const & opts = options());
void set_interrupt(bool flag) { m_cell->set_interrupt(flag); }
};

12
src/library/state.h
View file

@ -102,18 +102,6 @@ inline diagnostic const & operator<<(diagnostic const & out, kernel_exception co
return out;
}
inline regular const & operator<<(regular const & out, elaborator_exception const & ex) {
options const & opts = out.m_state.get_options();
out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(ex, opts), opts);
return out;
}
inline diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex) {
options const & opts = out.m_state.get_options();
out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(ex, opts), opts);
return out;
}
template<typename T>
inline regular const & operator<<(regular const & out, T const & t) {
out.m_state.get_regular_channel().get_stream() << t;

3
src/tests/frontends/lean/CMakeLists.txt
View file

@ -10,3 +10,6 @@ add_test(lean_parser ${CMAKE_CURRENT_BINARY_DIR}/lean_parser)
add_executable(lean_pp lean_pp.cpp)
target_link_libraries(lean_pp ${EXTRA_LIBS})
add_test(lean_pp ${CMAKE_CURRENT_BINARY_DIR}/lean_pp)
add_executable(implicit_args implicit_args.cpp)
target_link_libraries(implicit_args ${EXTRA_LIBS})
add_test(implicit_args ${CMAKE_CURRENT_BINARY_DIR}/implicit_args)

43
src/tests/library/implicit_args.cpp → src/tests/frontends/lean/implicit_args.cpp
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#include "test.h"
#include "metavar.h"
#include "elaborator.h"
#include "free_vars.h"
#include "printer.h"
#include "occurs.h"
@ -15,16 +14,18 @@ Author: Leonardo de Moura
#include "basic_thms.h"
#include "type_check.h"
#include "kernel_exception.h"
#include "elaborator_exception.h"
#include "lean_frontend.h"
#include "lean_elaborator.h"
#include "lean_elaborator_exception.h"
using namespace lean;
expr elaborate(expr const & e, environment const & env) {
expr elaborate(expr const & e, frontend const & env) {
elaborator elb(env);
return elb(e);
}
// Check elaborator success
static void success(expr const & e, expr const & expected, environment const & env) {
static void success(expr const & e, expr const & expected, frontend const & env) {
std::cout << "\n" << e << "\n------>\n";
try {
std::cout << elaborate(e, env) << "\n";
@ -50,7 +51,7 @@ static void success(expr const & e, expr const & expected, environment const & e
}
// Check elaborator failure
static void fails(expr const & e, environment const & env) {
static void fails(expr const & e, frontend const & env) {
try {
expr new_e = elaborate(e, env);
std::cout << "new_e: " << new_e << std::endl;
@ -60,7 +61,7 @@ static void fails(expr const & e, environment const & env) {
}
// Check elaborator partial success (i.e., result still contain some metavariables */
static void unsolved(expr const & e, environment const & env) {
static void unsolved(expr const & e, frontend const & env) {
std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n";
lean_assert(has_metavar(elaborate(e, env)));
}
@ -68,7 +69,7 @@ static void unsolved(expr const & e, environment const & env) {
#define _ mk_placholder()
static void tst1() {
environment env;
frontend env;
expr A = Const("A");
expr B = Const("B");
expr F = Const("F");
@ -87,7 +88,7 @@ static void tst1() {
}
static void tst2() {
environment env = mk_toplevel();
frontend env;
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
@ -111,7 +112,7 @@ static void tst2() {
}
static void tst3() {
environment env = mk_toplevel();
frontend env;
expr Nat = Const("Nat");
env.add_var("Nat", Type());
env.add_var("vec", Nat >> Type());
@ -141,7 +142,7 @@ static void tst3() {
}
static void tst4() {
environment env;
frontend env;
expr Nat = Const("Nat");
env.add_var("Nat", Type());
expr R = Const("R");
@ -163,7 +164,7 @@ static void tst4() {
}
static void tst5() {
environment env;
frontend env;
expr A = Const("A");
expr B = Const("B");
expr a = Const("a");
@ -179,7 +180,7 @@ static void tst5() {
}
static void tst6() {
environment env;
frontend env;
expr lst = Const("list");
expr nil = Const("nil");
expr cons = Const("cons");
@ -198,14 +199,14 @@ static void tst6() {
}
static void tst7() {
environment env;
frontend env;
expr x = Const("x");
expr omega = mk_app(Fun({x,_}, x(x)), Fun({x,_}, x(x)));
fails(omega, env);
}
static void tst8() {
environment env;
frontend env;
expr B = Const("B");
expr A = Const("A");
expr x = Const("x");
@ -226,7 +227,7 @@ static void tst8() {
}
static void tst9() {
environment env = mk_toplevel();
frontend env;
expr A = Const("A");
expr B = Const("B");
expr f = Const("f");
@ -265,7 +266,7 @@ static void tst9() {
}
static void tst10() {
environment env = mk_toplevel();
frontend env;
expr A = Const("A");
expr B = Const("B");
expr C = Const("C");
@ -290,7 +291,7 @@ static void tst10() {
static void tst11() {
environment env = mk_toplevel();
frontend env;
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
@ -310,7 +311,7 @@ static void tst11() {
Fun({{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3))),
env);
environment env2 = mk_toplevel();
frontend env2;
success(Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3))),
Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
@ -325,7 +326,7 @@ static void tst11() {
}
void tst12() {
environment env;
frontend env;
expr A = Const("A");
expr B = Const("B");
expr a = Const("a");
@ -338,7 +339,7 @@ void tst12() {
}
void tst13() {
environment env = mk_toplevel();
frontend env;
expr A = Const("A");
expr h = Const("h");
expr f = Const("f");
@ -350,7 +351,7 @@ void tst13() {
}
void tst14() {
environment env = mk_toplevel();
frontend env;
expr R = Const("R");
expr A = Const("A");
expr r = Const("r");

3
src/tests/library/CMakeLists.txt
View file

@ -1,6 +1,3 @@
add_executable(implicit_args implicit_args.cpp)
target_link_libraries(implicit_args ${EXTRA_LIBS})
add_test(implicit_args ${CMAKE_CURRENT_BINARY_DIR}/implicit_args)
add_executable(metavar metavar.cpp)
target_link_libraries(metavar ${EXTRA_LIBS})
add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)