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

feat(library/compiler/compiler): add option compiler.extract_closed

Browse source 
It is useful when using `unsafeIO`
This commit is contained in:
Leonardo de Moura 2019-07-10 11:08:34 -07:00
parent 228ddd5fdc
commit 17cc34def5
3 changed files with 26 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/io.lean
View file

@ -45,9 +45,14 @@ id
abbrev IO : Type → Type := EIO IO.Error
@[inline]
unsafe def unsafeIO {α : Type} (fn : IO α) : Option α :=
section
/- After we inline `EState.run'`, the closed term `((), ())` is generated, where the second `()`
represents the "initial world". We don't want to cache this closed term. So, we disable
the "extract closed terms" optimization. -/
set_option compiler.extract_closed false
@[inline] unsafe def unsafeIO {α : Type} (fn : IO α) : Option α :=
fn.run' ()
end
@[extern 4 "lean_io_timeit"]
constant timeit {α : Type} (msg : @& String) (fn : IO α) : IO α := default _

6
library/init/lean/environment.lean
View file

@ -309,6 +309,11 @@ def CPPExtensionState := NonScalar
instance CPPExtensionState.inhabited : Inhabited CPPExtensionState := inferInstanceAs (Inhabited NonScalar)
section
/- It is not safe to use "extract closed term" optimization in the following code because of `unsafeIO`.
If `compiler.extract_closed` is set to true, then the compiler will cache the result of
`exts ← envExtensionsRef.get` during initialization which is incorrect. -/
set_option compiler.extract_closed false
@[export lean.register_extension_core]
unsafe def registerCPPExtension (initial : CPPExtensionState) : Option Nat :=
unsafeIO (do ext ← registerEnvExtension initial; pure ext.idx)
@ -320,6 +325,7 @@ unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).setState env s
@[export lean.get_extension_core]
unsafe def getCPPExtensionState (env : Environment) (idx : Nat) : Option CPPExtensionState :=
unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).getState env)
end
/- Legacy support for Modification objects -/

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

@ -31,10 +31,10 @@ Author: Leonardo de Moura
namespace lean {
static name * g_codegen = nullptr;
static name * g_extract_closed = nullptr;
bool is_codegen_enabled(options const & opts) {
return opts.get_bool(*g_codegen, true);
}
bool is_codegen_enabled(options const & opts) { return opts.get_bool(*g_codegen, true); }
bool is_extract_closed_enabled(options const & opts) { return opts.get_bool(*g_extract_closed, true); }
static name get_real_name(name const & n) {
if (optional<name> new_n = is_unsafe_rec_name(n))
@ -222,10 +222,12 @@ environment compile(environment const & env, options const & opts, names cs) {
trace_compiler(name({"compiler", "simp"}), ds);
new_env = cache_stage2(new_env, ds);
trace_compiler(name({"compiler", "stage2"}), ds);
std::tie(new_env, ds) = extract_closed(new_env, ds);
ds = apply(elim_dead_let, ds);
ds = apply(esimp, new_env, ds);
trace_compiler(name({"compiler", "extract_closed"}), ds);
if (is_extract_closed_enabled(opts)) {
std::tie(new_env, ds) = extract_closed(new_env, ds);
ds = apply(elim_dead_let, ds);
ds = apply(esimp, new_env, ds);
trace_compiler(name({"compiler", "extract_closed"}), ds);
}
new_env = cache_new_stage2(new_env, ds);
ds = apply(esimp, new_env, ds);
trace_compiler(name({"compiler", "simp"}), ds);
@ -260,9 +262,10 @@ extern "C" object * lean_add_and_compile(object * env, object * opts, object * d
}
void initialize_compiler() {
g_codegen = new name("codegen");
g_codegen = new name("codegen");
g_extract_closed = new name{"compiler", "extract_closed"};
register_bool_option(*g_codegen, true, "(compiler) enable/disable code generation");
register_bool_option(*g_extract_closed, true, "(compiler) enable/disable closed term caching");
register_trace_class("compiler");
register_trace_class({"compiler", "input"});
register_trace_class({"compiler", "eta_expand"});
@ -302,5 +305,6 @@ void initialize_compiler() {
void finalize_compiler() {
delete g_codegen;
delete g_extract_closed;
}
}