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

refactor(library/state): rename Lean state object to io_state

Browse source 
The idea is to make it clear that io_state is distinguish it from proof_state, and from leanlua_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-21 15:51:29 -08:00
parent 680ec8abba
commit 5346b67651
24 changed files with 202 additions and 201 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/bindings/lua/CMakeLists.txt
View file

@ -2,6 +2,6 @@ add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
lref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp
local_context.cpp expr.cpp context.cpp object.cpp environment.cpp
formatter.cpp justification.cpp metavar_env.cpp type_inferer.cpp
state.cpp leanlua_state.cpp frontend_lean.cpp)
io_state.cpp leanlua_state.cpp frontend_lean.cpp)
target_link_libraries(lua ${LEAN_LIBS})

14
src/bindings/lua/formatter.cpp
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
#include "bindings/lua/context.h"
#include "bindings/lua/environment.h"
#include "bindings/lua/object.h"
#include "bindings/lua/state.h"
#include "bindings/lua/io_state.h"
namespace lean {
DECL_UDATA(formatter)
@ -67,9 +67,9 @@ static char g_formatter_key;
static formatter g_simple_formatter = mk_simple_formatter();
formatter get_global_formatter(lua_State * L) {
state * S = get_state(L);
if (S != nullptr) {
return S->get_formatter();
io_state * io = get_io_state(L);
if (io != nullptr) {
return io->get_formatter();
} else {
lua_pushlightuserdata(L, static_cast<void *>(&g_formatter_key));
lua_gettable(L, LUA_REGISTRYINDEX);
@ -85,9 +85,9 @@ formatter get_global_formatter(lua_State * L) {
}
void set_global_formatter(lua_State * L, formatter const & fmt) {
state * S = get_state(L);
if (S != nullptr) {
S->set_formatter(fmt);
io_state * io = get_io_state(L);
if (io != nullptr) {
io->set_formatter(fmt);
} else {
lua_pushlightuserdata(L, static_cast<void *>(&g_formatter_key));
push_formatter(L, fmt);

34
src/bindings/lua/frontend_lean.cpp
View file

@ -6,19 +6,19 @@ Author: Leonardo de Moura
*/
#include <sstream>
#include <lua.hpp>
#include "library/state.h"
#include "library/io_state.h"
#include "frontends/lean/parser.h"
#include "bindings/lua/util.h"
#include "bindings/lua/expr.h"
#include "bindings/lua/environment.h"
#include "bindings/lua/options.h"
#include "bindings/lua/formatter.h"
#include "bindings/lua/state.h"
#include "bindings/lua/io_state.h"
#include "bindings/lua/leanlua_state.h"
namespace lean {
/** \see parse_lean_expr */
static int parse_lean_expr_core(lua_State * L, ro_environment const & env, state & st) {
static int parse_lean_expr_core(lua_State * L, ro_environment const & env, io_state & st) {
char const * src = luaL_checkstring(L, 1);
std::istringstream in(src);
leanlua_state S = to_leanlua_state(L);
@ -28,12 +28,12 @@ static int parse_lean_expr_core(lua_State * L, ro_environment const & env, state
/** \see parse_lean_expr */
static int parse_lean_expr_core(lua_State * L, ro_environment const & env) {
state * st = get_state(L);
if (st == nullptr) {
state st(get_global_options(L), get_global_formatter(L));
return parse_lean_expr_core(L, env, st);
io_state * io = get_io_state(L);
if (io == nullptr) {
io_state s(get_global_options(L), get_global_formatter(L));
return parse_lean_expr_core(L, env, s);
} else {
return parse_lean_expr_core(L, env, *st);
return parse_lean_expr_core(L, env, *io);
}
}
@ -67,14 +67,14 @@ static int parse_lean_expr(lua_State * L) {
} else {
options opts = to_options(L, 3);
formatter fmt = nargs == 3 ? get_global_formatter(L) : to_formatter(L, 4);
state st(opts, fmt);
io_state st(opts, fmt);
return parse_lean_expr_core(L, env, st);
}
}
}
/** \see parse_lean_cmds */
static void parse_lean_cmds_core(lua_State * L, rw_environment & env, state & st) {
static void parse_lean_cmds_core(lua_State * L, rw_environment & env, io_state & st) {
char const * src = luaL_checkstring(L, 1);
std::istringstream in(src);
leanlua_state S = to_leanlua_state(L);
@ -83,13 +83,13 @@ static void parse_lean_cmds_core(lua_State * L, rw_environment & env, state & st
/** \see parse_lean_cmds */
static void parse_lean_cmds_core(lua_State * L, rw_environment & env) {
state * st = get_state(L);
if (st == nullptr) {
state st(get_global_options(L), get_global_formatter(L));
parse_lean_cmds_core(L, env, st);
set_global_options(L, st.get_options());
io_state * io = get_io_state(L);
if (io == nullptr) {
io_state s(get_global_options(L), get_global_formatter(L));
parse_lean_cmds_core(L, env, s);
set_global_options(L, s.get_options());
} else {
parse_lean_cmds_core(L, env, *st);
parse_lean_cmds_core(L, env, *io);
}
}
@ -113,7 +113,7 @@ static int parse_lean_cmds(lua_State * L) {
} else {
options opts = to_options(L, 3);
formatter fmt = nargs == 3 ? get_global_formatter(L) : to_formatter(L, 4);
state st(opts, fmt);
io_state st(opts, fmt);
parse_lean_cmds_core(L, env, st);
push_options(L, st.get_options());
return 1;

12
src/bindings/lua/state.cpp → src/bindings/lua/io_state.cpp
View file

@ -5,33 +5,33 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <lua.hpp>
#include "library/state.h"
#include "bindings/lua/state.h"
#include "library/io_state.h"
#include "bindings/lua/io_state.h"
namespace lean {
static char g_set_state_key;
set_state::set_state(lua_State * L, state & st) {
set_io_state::set_io_state(lua_State * L, io_state & st) {
m_state = L;
lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
lua_pushlightuserdata(m_state, &st);
lua_settable(m_state, LUA_REGISTRYINDEX);
}
set_state::~set_state() {
set_io_state::~set_io_state() {
lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
lua_pushnil(m_state);
lua_settable(m_state, LUA_REGISTRYINDEX);
}
state * get_state(lua_State * L) {
io_state * get_io_state(lua_State * L) {
lua_pushlightuserdata(L, static_cast<void *>(&g_set_state_key));
lua_gettable(L, LUA_REGISTRYINDEX);
if (!lua_islightuserdata(L, -1)) {
lua_pop(L, 1);
return nullptr;
} else {
state * r = static_cast<state*>(lua_touserdata(L, -1));
io_state * r = static_cast<io_state*>(lua_touserdata(L, -1));
lua_pop(L, 1);
return r;
}

12
src/bindings/lua/state.h → src/bindings/lua/io_state.h
View file

@ -6,22 +6,22 @@ Author: Leonardo de Moura
*/
#pragma once
#include <lua.hpp>
#include "library/state.h"
#include "library/io_state.h"
namespace lean {
/**
\brief Auxiliary class for temporarily setting the Lua registry of a Lua state
with a Lean state object.
with a Lean io_state object.
*/
class set_state {
class set_io_state {
lua_State * m_state;
public:
set_state(lua_State * L, state & st);
~set_state();
set_io_state(lua_State * L, io_state & st);
~set_io_state();
};
/**
\brief Return the Lean state object associated with the given Lua state.
Return nullptr is there is none.
*/
state * get_state(lua_State * L);
io_state * get_io_state(lua_State * L);
}

24
src/bindings/lua/leanlua_state.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "util/memory.h"
#include "util/buffer.h"
#include "util/interrupt.h"
#include "library/state.h"
#include "library/io_state.h"
#include "bindings/lua/leanlua_state.h"
#include "bindings/lua/util.h"
#include "bindings/lua/name.h"
@ -33,7 +33,7 @@ Author: Leonardo de Moura
#include "bindings/lua/environment.h"
#include "bindings/lua/justification.h"
#include "bindings/lua/metavar_env.h"
#include "bindings/lua/state.h"
#include "bindings/lua/io_state.h"
#include "bindings/lua/type_inferer.h"
#include "bindings/lua/frontend_lean.h"
#include "bindings/lua/lean.lua"
@ -208,8 +208,8 @@ struct leanlua_state::imp {
::lean::dostring(m_state, str);
}
void dostring(char const * str, environment & env, state & st) {
set_state set1(m_state, st);
void dostring(char const * str, environment & env, io_state & st) {
set_io_state set1(m_state, st);
set_environment set2(m_state, env);
dostring(str);
}
@ -239,7 +239,7 @@ void leanlua_state::dostring(char const * str) {
m_ptr->dostring(str);
}
void leanlua_state::dostring(char const * str, environment & env, state & st) {
void leanlua_state::dostring(char const * str, environment & env, io_state & st) {
m_ptr->dostring(str, env, st);
}
@ -247,7 +247,7 @@ static std::mutex g_print_mutex;
/** \brief Thread safe version of print function */
static int print(lua_State * L) {
state * S = get_state(L);
io_state * io = get_io_state(L);
int n = lua_gettop(L);
int i;
lua_getglobal(L, "tostring");
@ -262,19 +262,19 @@ static int print(lua_State * L) {
if (s == NULL)
throw exception("'to_string' must return a string to 'print'");
if (i > 1) {
if (S)
regular(*S) << "\t";
if (io)
regular(*io) << "\t";
else
std::cout << "\t";
}
if (S)
regular(*S) << s;
if (io)
regular(*io) << s;
else
std::cout << s;
lua_pop(L, 1);
}
if (S)
regular(*S) << endl;
if (io)
regular(*io) << endl;
else
std::cout << std::endl;
return 0;

4
src/bindings/lua/leanlua_state.h
View file

@ -12,7 +12,7 @@ Author: Leonardo de Moura
namespace lean {
class environment;
class state;
class io_state;
/**
\brief Wrapper for lua_State objects which contains all Lean bindings.
*/
@ -49,7 +49,7 @@ public:
The registry can be accessed by \str by invoking the function <tt>env()</tt>.
The script \c str should not store a reference to the environment \c env.
*/
virtual void dostring(char const * str, environment & env, state & st);
virtual void dostring(char const * str, environment & env, io_state & st);
};
/**
\brief Return a reference to the leanlua_state object that is wrapping \c L.

6
src/bindings/lua/options.cpp
View file

@ -13,7 +13,7 @@ Author: Leonardo de Moura
#include "util/sexpr/option_declarations.h"
#include "bindings/lua/util.h"
#include "bindings/lua/name.h"
#include "bindings/lua/state.h"
#include "bindings/lua/io_state.h"
namespace lean {
DECL_UDATA(options)
@ -139,7 +139,7 @@ static int options_update(lua_State * L) {
static char g_options_key;
options get_global_options(lua_State * L) {
state * S = get_state(L);
io_state * S = get_io_state(L);
if (S != nullptr) {
return S->get_options();
} else {
@ -154,7 +154,7 @@ options get_global_options(lua_State * L) {
}
void set_global_options(lua_State * L, options const & o) {
state * S = get_state(L);
io_state * S = get_io_state(L);
if (S != nullptr) {
S->set_options(o);
} else {

6
src/frontends/lean/frontend.cpp
View file

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "util/exception.h"
#include "kernel/environment.h"
#include "library/expr_pair.h"
#include "library/state.h"
#include "library/io_state.h"
#include "library/all/all.h"
#include "frontends/lean/operator_info.h"
#include "frontends/lean/coercion.h"
@ -181,7 +181,7 @@ struct lean_extension : public environment::extension {
2) It is a real conflict, and report the issue in the
diagnostic channel, and override the existing operator (aka notation).
*/
void add_op(operator_info new_op, expr const & d, bool led, environment & env, state & st) {
void add_op(operator_info new_op, expr const & d, bool led, environment & env, io_state & st) {
name const & opn = new_op.get_op_name();
operator_info old_op = find_op(opn, led);
if (!old_op) {
@ -365,7 +365,7 @@ frontend::frontend() {
init_builtin_notation(*this);
m_state.set_formatter(mk_pp_formatter(*this));
}
frontend::frontend(environment const & env, state const & s):m_env(env), m_state(s) {
frontend::frontend(environment const & env, io_state const & s):m_env(env), m_state(s) {
import_all(m_env);
init_builtin_notation(*this);
}

14
src/frontends/lean/frontend.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include <memory>
#include <vector>
#include "kernel/environment.h"
#include "library/state.h"
#include "library/io_state.h"
#include "library/expr_pair.h"
#include "frontends/lean/operator_info.h"
@ -22,10 +22,10 @@ namespace lean {
*/
class frontend {
environment m_env;
state m_state;
io_state m_state;
public:
frontend();
frontend(environment const & env, state const & s);
frontend(environment const & env, io_state const & s);
frontend mk_child() const { return frontend(m_env.mk_child(), m_state); }
bool has_children() const { return m_env.has_children(); }
@ -179,10 +179,10 @@ public:
@name State management.
*/
/*@{*/
state const & get_state() const { return m_state; }
operator state const &() const { return m_state; }
state & get_state() { return m_state; }
operator state &() { return m_state; }
io_state const & get_state() const { return m_state; }
operator io_state const &() const { return m_state; }
io_state & get_state() { return m_state; }
operator io_state &() { return m_state; }
options get_options() const { return m_state.get_options(); }
void set_options(options const & opts) { return m_state.set_options(opts); }
template<typename T> void set_option(name const & n, T const & v) { m_state.set_option(n, v); }

6
src/frontends/lean/parser.cpp
View file

@ -29,7 +29,7 @@ Author: Leonardo de Moura
#include "kernel/expr_maps.h"
#include "kernel/printer.h"
#include "library/arith/arith.h"
#include "library/state.h"
#include "library/io_state.h"
#include "library/placeholder.h"
#include "library/script_evaluator.h"
#include "library/elaborator/elaborator_exception.h"
@ -1735,7 +1735,7 @@ bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S, bool
return parser(fe, in, S, use_exceptions, interactive)();
}
bool parse_commands(environment const & env, state & st, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
frontend f(env, st);
bool r = parse_commands(f, in, S, use_exceptions, interactive);
st = f.get_state();
@ -1746,7 +1746,7 @@ expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S, bool use
return parser(fe, in, S, use_exceptions).parse_expr();
}
expr parse_expr(environment const & env, state & st, std::istream & in, script_evaluator * S, bool use_exceptions) {
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_evaluator * S, bool use_exceptions) {
frontend f(env, st);
expr r = parse_expr(f, in, S, use_exceptions);
st = f.get_state();

6
src/frontends/lean/parser.h
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
namespace lean {
class script_evaluator;
class frontend;
class state;
class io_state;
class environment;
/** \brief Functional object for parsing commands and expressions */
class parser {
@ -39,7 +39,7 @@ public:
};
bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
bool parse_commands(environment const & env, state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
expr parse_expr(environment const & env, state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
}

2
src/library/CMakeLists.txt
View file

@ -1,5 +1,5 @@
add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
context_to_lambda.cpp state.cpp update_expr.cpp type_inferer.cpp
context_to_lambda.cpp io_state.cpp update_expr.cpp type_inferer.cpp
placeholder.cpp expr_lt.cpp script_evaluator.cpp)
target_link_libraries(library ${LEAN_LIBS})

97
src/library/io_state.cpp Normal file
View file

@ -0,0 +1,97 @@
/*
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 "kernel/kernel_exception.h"
#include "library/io_state.h"
namespace lean {
io_state::io_state():
m_formatter(mk_simple_formatter()),
m_regular_channel(new stdout_channel()),
m_diagnostic_channel(new stderr_channel()) {
}
io_state::io_state(options const & opts, formatter const & fmt):
m_options(opts),
m_formatter(fmt),
m_regular_channel(new stdout_channel()),
m_diagnostic_channel(new stderr_channel()) {
}
io_state::~io_state() {}
void io_state::set_regular_channel(std::shared_ptr<output_channel> const & out) {
if (out)
m_regular_channel = out;
}
void io_state::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) {
if (out)
m_diagnostic_channel = out;
}
void io_state::set_options(options const & opts) {
m_options = opts;
}
void io_state::set_formatter(formatter const & f) {
m_formatter = f;
}
void regular::flush() {
m_io_state.get_regular_channel().get_stream().flush();
}
void diagnostic::flush() {
m_io_state.get_diagnostic_channel().get_stream().flush();
}
regular const & operator<<(regular const & out, endl_class) {
out.m_io_state.get_regular_channel().get_stream() << std::endl;
return out;
}
diagnostic const & operator<<(diagnostic const & out, endl_class) {
out.m_io_state.get_diagnostic_channel().get_stream() << std::endl;
return out;
}
regular const & operator<<(regular const & out, expr const & e) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_regular_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(e, opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, expr const & e) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(e, opts), opts);
return out;
}
regular const & operator<<(regular const & out, object const & obj) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_regular_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(obj, opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, object const & obj) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(obj, opts), opts);
return out;
}
regular const & operator<<(regular const & out, kernel_exception const & ex) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_regular_channel().get_stream() << mk_pair(ex.pp(out.m_io_state.get_formatter(), opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, kernel_exception const & ex) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(ex.pp(out.m_io_state.get_formatter(), opts), opts);
return out;
}
}

28
src/library/state.h → src/library/io_state.h
View file

@ -17,15 +17,15 @@ namespace lean {
3- Output results
4- Produce formatted output
*/
class state {
class io_state {
options m_options;
formatter m_formatter;
std::shared_ptr<output_channel> m_regular_channel;
std::shared_ptr<output_channel> m_diagnostic_channel;
public:
state();
state(options const & opts, formatter const & fmt);
~state();
io_state();
io_state(options const & opts, formatter const & fmt);
~io_state();
options get_options() const { return m_options; }
formatter get_formatter() const { return m_formatter; }
@ -42,22 +42,22 @@ public:
};
/**
\brief Wrapper for the state object that provides access to the
state's regular channel
\brief Wrapper for the io_state object that provides access to the
io_state's regular channel
*/
struct regular {
state const & m_state;
regular(state const & s):m_state(s) {}
io_state const & m_io_state;
regular(io_state const & s):m_io_state(s) {}
void flush();
};
/**
\brief Wrapper for the state object that provides access to the
state's diagnostic channel
\brief Wrapper for the io_state object that provides access to the
io_state's diagnostic channel
*/
struct diagnostic {
state const & m_state;
diagnostic(state const & s):m_state(s) {}
io_state const & m_io_state;
diagnostic(io_state const & s):m_io_state(s) {}
void flush();
};
@ -78,13 +78,13 @@ diagnostic const & operator<<(diagnostic const & out, kernel_exception const & e
template<typename T>
inline regular const & operator<<(regular const & out, T const & t) {
out.m_state.get_regular_channel().get_stream() << t;
out.m_io_state.get_regular_channel().get_stream() << t;
return out;
}
template<typename T>
inline diagnostic const & operator<<(diagnostic const & out, T const & t) {
out.m_state.get_diagnostic_channel().get_stream() << t;
out.m_io_state.get_diagnostic_channel().get_stream() << t;
return out;
}
}

4
src/library/script_evaluator.h
View file

@ -9,7 +9,7 @@ Author: Leonardo de Moura
namespace lean {
class environment;
class state;
class io_state;
/**
\brief Abstract base class for script code evaluators.
These evaluators are used to execute user-supplied code embedded in frontend files (.e.g., .lean, .smt2, etc).
@ -19,7 +19,7 @@ class script_evaluator {
public:
virtual ~script_evaluator() {}
virtual void dostring(char const * str) = 0;
virtual void dostring(char const * str, environment & env, state & st) = 0;
virtual void dostring(char const * str, environment & env, io_state & st) = 0;
};
/**

97
src/library/state.cpp
View file

@ -1,97 +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 "kernel/kernel_exception.h"
#include "library/state.h"
namespace lean {
state::state():
m_formatter(mk_simple_formatter()),
m_regular_channel(new stdout_channel()),
m_diagnostic_channel(new stderr_channel()) {
}
state::state(options const & opts, formatter const & fmt):
m_options(opts),
m_formatter(fmt),
m_regular_channel(new stdout_channel()),
m_diagnostic_channel(new stderr_channel()) {
}
state::~state() {}
void state::set_regular_channel(std::shared_ptr<output_channel> const & out) {
if (out)
m_regular_channel = out;
}
void state::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) {
if (out)
m_diagnostic_channel = out;
}
void state::set_options(options const & opts) {
m_options = opts;
}
void state::set_formatter(formatter const & f) {
m_formatter = f;
}
void regular::flush() {
m_state.get_regular_channel().get_stream().flush();
}
void diagnostic::flush() {
m_state.get_diagnostic_channel().get_stream().flush();
}
regular const & operator<<(regular const & out, endl_class) {
out.m_state.get_regular_channel().get_stream() << std::endl;
return out;
}
diagnostic const & operator<<(diagnostic const & out, endl_class) {
out.m_state.get_diagnostic_channel().get_stream() << std::endl;
return out;
}
regular const & operator<<(regular const & out, expr const & e) {
options const & opts = out.m_state.get_options();
out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, expr const & e) {
options const & opts = out.m_state.get_options();
out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
return out;
}
regular const & operator<<(regular const & out, object const & obj) {
options const & opts = out.m_state.get_options();
out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(obj, opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, object const & obj) {
options const & opts = out.m_state.get_options();
out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(obj, opts), opts);
return out;
}
regular const & operator<<(regular const & out, kernel_exception const & ex) {
options const & opts = out.m_state.get_options();
out.m_state.get_regular_channel().get_stream() << mk_pair(ex.pp(out.m_state.get_formatter(), opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, kernel_exception const & ex) {
options const & opts = out.m_state.get_options();
out.m_state.get_diagnostic_channel().get_stream() << mk_pair(ex.pp(out.m_state.get_formatter(), opts), opts);
return out;
}
}

12
src/library/tactic/tactic.cpp
View file

@ -23,7 +23,7 @@ void tactic_result::request_interrupt() {
::lean::request_interrupt();
}
proof_state_ref tactic_result::next(environment const & env, state const & s) {
proof_state_ref tactic_result::next(environment const & env, io_state const & s) {
try {
return next_core(env, s);
} catch (interrupted &) {
@ -68,7 +68,7 @@ public:
public:
result(tactic_result_ref && r1, tactic const & t2):m_r1(std::move(r1)), m_t2(t2) {}
virtual proof_state_ref next_core(environment const & env, state const & s) {
virtual proof_state_ref next_core(environment const & env, io_state const & s) {
if (m_r2) {
proof_state_ref s2 = m_r2->next(env, s);
if (s2)
@ -95,12 +95,12 @@ public:
tactic then(tactic const & t1, tactic const & t2) { return tactic(new then_tactic(t1, t2)); }
tactic id_tactic() { return mk_tactic([](environment const &, state const &, proof_state const & s) -> proof_state { return s; }); }
tactic id_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { return s; }); }
tactic fail_tactic() { return mk_tactic([](environment const &, state const &, proof_state const &) -> proof_state { throw tactic_exception("failed"); }); }
tactic fail_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const &) -> proof_state { throw tactic_exception("failed"); }); }
tactic now_tactic() {
return mk_tactic([](environment const &, state const &, proof_state const & s) -> proof_state {
return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
if (!empty(s.get_goals()))
throw tactic_exception("nowtac failed");
return s;
@ -108,7 +108,7 @@ tactic now_tactic() {
}
tactic assumption_tactic() {
return mk_tactic([](environment const &, state const &, proof_state const & s) -> proof_state {
return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
list<std::pair<name, expr>> proofs;
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
expr const & c = g.get_conclusion();

8
src/library/tactic/tactic.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include <algorithm>
#include <memory>
#include <mutex>
#include "library/state.h"
#include "library/io_state.h"
#include "library/tactic/proof_state.h"
namespace lean {
@ -27,11 +27,11 @@ protected:
}
virtual void interrupt();
void propagate_interrupt(tactic_result_ref & r) { if (r) r->interrupt(); }
virtual proof_state_ref next_core(environment const & env, state const & s) = 0;
virtual proof_state_ref next_core(environment const & env, io_state const & s) = 0;
public:
tactic_result():m_interrupted(false) {}
void request_interrupt();
proof_state_ref next(environment const & env, state const & s);
proof_state_ref next(environment const & env, io_state const & s);
virtual ~tactic_result();
};
@ -73,7 +73,7 @@ public:
m_cell->inc_ref();
}
virtual ~result() { if (m_cell) m_cell->dec_ref(); }
virtual proof_state_ref next_core(environment const & env, state const & io) {
virtual proof_state_ref next_core(environment const & env, io_state const & io) {
if (m_cell) {
proof_state_ref r(new proof_state(m_cell->m_f(env, io, m_in)));
m_cell = nullptr;

1
src/library/tactic/tactic_exception.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "util/exception.h"
namespace lean {

4
src/tests/frontends/lean/pp.cpp
View file

@ -59,8 +59,8 @@ static void tst3() {
static void tst4() {
frontend f;
state const & s1 = f.get_state();
state s2 = f.get_state();
io_state const & s1 = f.get_state();
io_state s2 = f.get_state();
regular(s1) << And(Const("a"), Const("b")) << "\n";
regular(f) << And(Const("a"), Const("b")) << "\n";
diagnostic(f) << And(Const("a"), Const("b")) << "\n";

4
src/tests/kernel/metavar.cpp
View file

@ -19,7 +19,7 @@ Author: Leonardo de Moura
#include "kernel/printer.h"
#include "kernel/kernel_exception.h"
#include "library/placeholder.h"
#include "library/state.h"
#include "library/io_state.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
using namespace lean;
@ -477,7 +477,7 @@ static void tst23() {
std::cout << checker.infer_type(F1, context(), &menv, up) << "\n";
} catch (kernel_exception & ex) {
formatter fmt = mk_simple_formatter();
state st(options(), fmt);
io_state st(options(), fmt);
regular(st) << ex << "\n";
}
std::cout << up << "\n";

4
src/tests/kernel/type_checker.cpp
View file

@ -23,7 +23,7 @@ Author: Leonardo de Moura
#include "library/basic_thms.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
#include "library/state.h"
#include "library/io_state.h"
using namespace lean;
expr c(char const * n) { return mk_constant(n); }
@ -263,7 +263,7 @@ static void tst14() {
expr F = f(a);
type_checker checker(env);
formatter fmt = mk_simple_formatter();
state st(options(), fmt);
io_state st(options(), fmt);
try {
std::cout << checker.infer_type(F) << "\n";
} catch (kernel_exception & ex) {

2
src/tests/library/rewriter/rewriter.cpp
View file

@ -9,7 +9,7 @@ Author: Soonho Kong
#include "kernel/context.h"
#include "kernel/expr.h"
#include "kernel/printer.h"
#include "library/state.h"
#include "library/io_state.h"
#include "library/all/all.h"
#include "library/arith/arith.h"
#include "library/arith/nat.h"