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

feat(api): APIs for importing/exporting modules

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-23 08:30:55 -07:00
parent 5263ef4a74
commit 6f78304f31
3 changed files with 74 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/CMakeLists.txt
View file

@ -1,5 +1,5 @@
add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp univ.cpp
expr.cpp decl.cpp env.cpp ios.cpp)
expr.cpp decl.cpp env.cpp ios.cpp module.cpp)
FILE(GLOB LEAN_API_INCLUDE_FILES lean*.h)
install(FILES ${LEAN_API_INCLUDE_FILES} DESTINATION include)

36
src/api/lean_module.h Normal file
View file

@ -0,0 +1,36 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#ifndef _LEAN_MODULE_H
#define _LEAN_MODULE_H
#ifdef __cplusplus
extern "C" {
#endif
/**
\defgroup capi C API
*/
/*@{*/
/**
@name Module API
*/
/*@{*/
/** \brief Import the given modules (i.e., pre-compiled .olean files) */
lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, lean_env * r, lean_exception * ex);
/** \brief Export to the given file name the declarations added to the environment */
lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex);
/*@}*/
/*@}*/
#ifdef __cplusplus
};
#endif
#endif

37
src/api/module.cpp Normal file
View file

@ -0,0 +1,37 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/module.h"
#include "api/decl.h"
#include "api/string.h"
#include "api/exception.h"
#include "api/ios.h"
#include "api/lean_env.h"
#include "api/lean_module.h"
using namespace lean; // NOLINT
lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, lean_env * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(env);
check_nonnull(ios);
check_nonnull(modules);
buffer<module_name> ms;
for (name const & n : to_list_name_ref(modules)) {
ms.push_back(module_name(n));
}
environment new_env = import_modules(to_env_ref(env), std::string(), ms.size(), ms.data(),
1, true, to_io_state_ref(ios));
*r = of_env(new environment(new_env));
LEAN_CATCH;
}
lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex) {
LEAN_TRY;
check_nonnull(env);
std::ofstream out(fname, std::ofstream::binary);
export_module(out, to_env_ref(env));
LEAN_CATCH;
}