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

feat(api): expose lean_expr pretty printing function

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-23 09:09:17 -07:00
parent 3798493d99
commit b42e561bb1
3 changed files with 34 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/api/ios.cpp
View file

@ -7,6 +7,8 @@ Author: Leonardo de Moura
#include "frontends/lean/pp.h" #include "frontends/lean/pp.h"
#include "api/string.h" #include "api/string.h"
#include "api/exception.h" #include "api/exception.h"
#include "api/decl.h"
#include "api/lean_env.h"
#include "api/ios.h" #include "api/ios.h"
using namespace lean; // NOLINT using namespace lean; // NOLINT
@ -86,3 +88,16 @@ lean_bool lean_ios_reset_diagnostic(lean_ios ios, lean_exception * ex) {
to_io_state(ios)->set_diagnostic_channel(std::make_shared<string_output_channel>()); to_io_state(ios)->set_diagnostic_channel(std::make_shared<string_output_channel>());
LEAN_CATCH; LEAN_CATCH;
} }
lean_bool lean_expr_to_pp_string(lean_env env, lean_ios ios, lean_expr e, char const ** r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(env);
check_nonnull(ios);
check_nonnull(e);
options const & o = to_io_state_ref(ios).get_options();
formatter fmt = to_io_state_ref(ios).get_formatter_factory()(to_env_ref(env), o);
std::ostringstream out;
out << mk_pair(fmt(to_expr_ref(e)), o);
*r = mk_string(out.str());
LEAN_CATCH;
}

3
src/api/lean_ios.h
View file

@ -57,6 +57,9 @@ lean_bool lean_ios_reset_regular(lean_ios ios, lean_exception * ex);
\pre !lean_ios_is_std(ios) */ \pre !lean_ios_is_std(ios) */
lean_bool lean_ios_reset_diagnostic(lean_ios ios, lean_exception * ex); lean_bool lean_ios_reset_diagnostic(lean_ios ios, lean_exception * ex);
/** \brief Store in \c r a pretty printed representation of \c e */
lean_bool lean_expr_to_pp_string(lean_env env, lean_ios ios, lean_expr e, char const ** r, lean_exception * ex);
/*@}*/ /*@}*/
/*@}*/ /*@}*/

16
src/tests/shared/env.c
View file

@ -238,16 +238,32 @@ void test_import() {
lean_options o; lean_options o;
lean_ios ios; lean_ios ios;
lean_env new_env; lean_env new_env;
lean_decl nat_gcd_decl;
lean_name nat = mk_name("nat");
lean_name nat_gcd;
lean_expr nat_gcd_val;
char const * s;
check(lean_options_mk_empty(&o, &ex)); check(lean_options_mk_empty(&o, &ex));
check(lean_ios_mk_std(o, &ios, &ex)); check(lean_ios_mk_std(o, &ios, &ex));
check(lean_env_import(env, ios, ms, &new_env, &ex)); check(lean_env_import(env, ios, ms, &new_env, &ex));
check(lean_env_for_each_decl(new_env, print_decl_name_and_del, &ex)); check(lean_env_for_each_decl(new_env, print_decl_name_and_del, &ex));
check(lean_name_mk_str(nat, "gcd", &nat_gcd, &ex));
check(lean_env_get_decl(new_env, nat_gcd, &nat_gcd_decl, &ex));
check(lean_decl_get_value(nat_gcd_decl, &nat_gcd_val, &ex));
check(lean_expr_to_pp_string(new_env, ios, nat_gcd_val, &s, &ex));
printf("nat.gcd\n%s\n", s);
lean_env_del(env); lean_env_del(env);
lean_name_del(std); lean_name_del(std);
lean_list_name_del(ms); lean_list_name_del(ms);
lean_options_del(o); lean_options_del(o);
lean_ios_del(ios); lean_ios_del(ios);
lean_env_del(new_env); lean_env_del(new_env);
lean_name_del(nat);
lean_name_del(nat_gcd);
lean_decl_del(nat_gcd_decl);
lean_expr_del(nat_gcd_val);
lean_string_del(s);
} }
int main() { int main() {