35 lines
1.2 KiB
C++
35 lines
1.2 KiB
C++
/*
|
|
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Jared Roesch
|
|
*/
|
|
#pragma once
|
|
#include <string>
|
|
#include "kernel/environment.h"
|
|
|
|
namespace lean {
|
|
void initialize_install_path();
|
|
std::string get_install_path();
|
|
|
|
struct extern_fn {
|
|
bool m_in_lean_namespace;
|
|
name m_name;
|
|
unsigned m_arity;
|
|
extern_fn(bool in_lean_namespace, name n, unsigned arity) :
|
|
m_in_lean_namespace(in_lean_namespace), m_name(n), m_arity(arity) {}
|
|
};
|
|
|
|
optional<extern_fn> get_builtin(name const & n);
|
|
|
|
enum native_compiler_mode { JIT, AOT };
|
|
void native_compile(environment const & env, buffer<pair<name, expr>> & procs, native_compiler_mode & mode);
|
|
void native_compile_binary(environment const & env, declaration const & d);
|
|
void native_compile_module(environment const & env, buffer<declaration> decls);
|
|
void native_compile_module(environment const & env);
|
|
// void native_aot_compile(environment const & env, config & conf, declaration const & main);
|
|
// void native_compile_file(environment const & env, config & conf, declaration const & main);
|
|
environment set_native_module_path(environment & env, name const & n);
|
|
void initialize_native_compiler();
|
|
void finalize_native_compiler();
|
|
}
|