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

feat(library/compiler): allow main function to also have type io uint32

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-13 16:29:10 -08:00
parent 06bb9b7ea8
commit 19e111c2ff
3 changed files with 32 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/library/compiler/compiler.cpp
View file

@ -109,18 +109,25 @@ bool is_main_fn(environment const & env, name const & n) {
return false;
}
/* Return true iff type is `list string -> io uint32` */
/* Return true iff type is `list string -> io uint32` or `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());
if (is_arrow(type)) {
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());
} else if (is_app(type)) {
return
is_constant(app_fn(type), get_io_name()) &&
is_constant(app_arg(type), get_uint32_name());
} else {
return false;
}
}
environment compile(environment const & env, options const & opts, names const & cs) {

21
src/library/compiler/emit_cpp.cpp
View file

@ -916,7 +916,8 @@ static bool uses_lean_namespace(environment const & env) {
}
static void emit_main_fn(std::ostream & out, environment const & env, module_name const & m, comp_decl const & d) {
if (get_num_nested_lambdas(d.snd()) != 2) {
unsigned arity = get_num_nested_lambdas(d.snd());
if (arity != 2 && arity != 1) {
throw exception("invalid main function, incorrect arity when generating code");
}
bool uses_lean_api = uses_lean_namespace(env);
@ -928,13 +929,17 @@ static void emit_main_fn(std::ostream & out, environment const & env, module_nam
else
out << "lean::initialize_runtime_module();\n";
out << "initialize_" << mangle(m, false) << "();\n";
out << "obj* in = lean::box(0);\n";
out << "int i = argc;\n";
out << "while (i > 1) {\n i--;\n";
out << " obj* n = lean::alloc_cnstr(1,2,0); lean::cnstr_set(n, 0, lean::mk_string(argv[i])); lean::cnstr_set(n, 1, in);\n";
out << " in = n;\n";
out << "}\n";
out << "obj * r = " << g_lean_main << "(in, lean::box(0));\n";
if (arity == 2) {
out << "obj* in = lean::box(0);\n";
out << "int i = argc;\n";
out << "while (i > 1) {\n i--;\n";
out << " obj* n = lean::alloc_cnstr(1,2,0); lean::cnstr_set(n, 0, lean::mk_string(argv[i])); lean::cnstr_set(n, 1, in);\n";
out << " in = n;\n";
out << "}\n";
out << "obj * r = " << g_lean_main << "(in, lean::box(0));\n";
} else {
out << "obj * r = " << g_lean_main << "(lean::box(0));\n";
}
out << "int ret = lean::unbox(lean::cnstr_get(r, 0));\n";
out << "lean::dec(r);\n";
out << "return ret;\n";

2
tests/compiler/expr.lean
View file

@ -1,7 +1,7 @@
import init.lean.expr
open lean
def main (xs : list string) : io uint32 :=
def main : io uint32 :=
let e := expr.app (expr.const `f []) (expr.const `a []) in
io.println' e.dbg_to_string *>
io.println' ("hash: " ++ to_string e.hash) *>