max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/compiler/extname): add validation

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-06 13:24:42 -08:00
parent a8e2e535a2
commit b85f4aac88
1 changed files with 26 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/library/compiler/extname.cpp
View file

@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/attribute_manager.h"
#include "library/constants.h"
namespace lean {
struct extname_attr_data : public attr_data {
name m_id;
@ -32,16 +34,38 @@ optional<name> get_extname_for(environment const & env, name const & n) {
}
}
/* Return true iff type is `list string -> io uint32` */
bool is_main_fn_type(expr const & type) {
if (!is_arrow(type)) return false;
expr d = binding_domain(type);
expr r = binding_body(type);
return
is_app(r) &&
is_constant(app_fn(r), get_io_name()) &&
is_constant(app_arg(r), get_uint32_name()) &&
is_app(d) &&
is_constant(app_fn(d), get_list_name()) &&
is_constant(app_arg(d), get_string_name());
}
void initialize_extname() {
register_system_attribute(extname_attr("extname", "name to be used by code generators",
[](environment const & env, io_state const &, name const & n, unsigned, bool persistent) {
if (!persistent) throw exception("invalid [extname] attribute, must be persistent");
if (n.is_anonymous()) throw exception("invalid [extname] attribute, argument is missing");
name it = n;
auto const & data = *get_extname_attr().get(env, n);
name it = data.m_id;
if (it.is_anonymous()) throw exception("invalid [extname] attribute, argument is missing");
while (!it.is_anonymous()) {
if (!it.is_string()) throw exception("invalid [extname] attribute, identifier cannot be numeric");
it = it.get_prefix();
}
constant_info cinfo = env.get(n);
if (!cinfo.is_definition()) {
throw exception("invalid '[extname]' use, only definitions can be use this attribute");
}
if (data.m_id == "main" && !is_main_fn_type(cinfo.get_type())) {
throw exception("invalid [extname main] attribute, `main` function must have type `list string -> io uint32`");
}
return env;
}));
}