83 lines
3.4 KiB
C++
83 lines
3.4 KiB
C++
/*
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include <vector>
|
|
#include <memory>
|
|
#include <string>
|
|
#include "runtime/sstream.h"
|
|
#include "util/io.h"
|
|
#include "library/scoped_ext.h"
|
|
|
|
namespace lean {
|
|
typedef std::tuple<push_scope_fn, pop_scope_fn> entry;
|
|
typedef std::vector<entry> scoped_exts;
|
|
static scoped_exts * g_exts = nullptr;
|
|
static scoped_exts & get_exts() { return *g_exts; }
|
|
|
|
void register_scoped_ext(push_scope_fn push, pop_scope_fn pop) {
|
|
get_exts().emplace_back(push, pop);
|
|
}
|
|
|
|
object* get_namespace_core(object* env);
|
|
object* get_namespaces_core(object* env);
|
|
object* get_scope_header_core(object* env);
|
|
uint8 in_section_core(object* env);
|
|
uint8 is_namespace_core(object* env, object * n);
|
|
uint8 has_open_scopes_core(object* env);
|
|
uint8 in_section_core(object* env);
|
|
object* get_scope_header_core(object* env);
|
|
object* to_valid_namespace_core(object* env, object * n);
|
|
object* register_namespace_core(object* env, object * n);
|
|
object* push_scope_core(object* env, object* header, uint8 isNamespace, object* w);
|
|
object* pop_scope_core(object* env, object* w);
|
|
|
|
name get_scope_header(environment const & env) { return name(get_scope_header_core(env.to_obj_arg())); }
|
|
name get_namespace(environment const & env) { return name(get_namespace_core(env.to_obj_arg())); }
|
|
names get_namespaces(environment const & env) { return names(get_namespaces_core(env.to_obj_arg())); }
|
|
bool in_section(environment const & env) { return in_section_core(env.to_obj_arg()); }
|
|
bool is_namespace(environment const & env, name const & n) { return is_namespace_core(env.to_obj_arg(), n.to_obj_arg()); }
|
|
optional<name> to_valid_namespace_name(environment const & env, name const & n) {
|
|
return to_optional<name>(to_valid_namespace_core(env.to_obj_arg(), n.to_obj_arg()));
|
|
}
|
|
environment add_namespace(environment const & env, name const & n) { return environment(register_namespace_core(env.to_obj_arg(), n.to_obj_arg())); }
|
|
bool has_open_scopes(environment const & env) { return has_open_scopes_core(env.to_obj_arg()); }
|
|
environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
|
|
environment r = get_io_result<environment>(push_scope_core(env.to_obj_arg(), n.to_obj_arg(), k == scope_kind::Namespace, io_mk_world()));
|
|
for (auto const & t : get_exts()) {
|
|
r = std::get<0>(t)(r, ios, k);
|
|
}
|
|
return r;
|
|
}
|
|
environment pop_scope_core(environment const & env, io_state const & ios) {
|
|
scope_kind k = in_section_core(env.to_obj_arg()) ? scope_kind::Section : scope_kind::Namespace;
|
|
environment r = get_io_result<environment>(pop_scope_core(env.to_obj_arg(), io_mk_world()));
|
|
for (auto const & t : get_exts()) {
|
|
r = std::get<1>(t)(r, ios, k);
|
|
}
|
|
return r;
|
|
}
|
|
environment pop_scope(environment const & env, io_state const & ios, name const & n) {
|
|
// TODO(Leo) this kind of check should be performed in the new frontend
|
|
if (!has_open_scopes(env))
|
|
throw exception("invalid end of scope, there are no open namespaces/sections");
|
|
if (n != get_scope_header(env))
|
|
throw exception("invalid end of scope, begin/end mismatch");
|
|
return pop_scope_core(env, ios);
|
|
}
|
|
|
|
// temporary HACK
|
|
environment set_namespace(environment const & env, name const & /* ns */) {
|
|
return env;
|
|
}
|
|
|
|
void initialize_scoped_ext() {
|
|
g_exts = new scoped_exts();
|
|
}
|
|
|
|
void finalize_scoped_ext() {
|
|
delete g_exts;
|
|
}
|
|
}
|