From 2ad33a23dbffe9d64e3d27c7309cd599efcea1d3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Jul 2019 11:04:57 -0700
Subject: [PATCH] chore(runtime,library/init/lean): remove evalConst

---
 library/init/lean/default.lean   |  1 -
 library/init/lean/evalconst.lean | 40 --------------------------------
 src/runtime/object.cpp           | 36 ----------------------------
 src/runtime/object.h             |  9 -------
 src/stage0/CMakeLists.txt        |  2 +-
 src/stage0/init/lean/default.cpp |  5 +---
 6 files changed, 2 insertions(+), 91 deletions(-)
 delete mode 100644 library/init/lean/evalconst.lean

diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean
index 6a9516fc0b..68f4b74127 100644
--- a/library/init/lean/default.lean
+++ b/library/init/lean/default.lean
@@ -10,7 +10,6 @@ import init.lean.modifiers
 import init.lean.projfns
 import init.lean.runtime
 import init.lean.attributes
-import init.lean.evalconst
 import init.lean.parser
 import init.lean.reducibilityattrs
 import init.lean.elaborator
diff --git a/library/init/lean/evalconst.lean b/library/init/lean/evalconst.lean
deleted file mode 100644
index 17a80eef52..0000000000
--- a/library/init/lean/evalconst.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.io
-import init.data.array
-import init.lean.name
-
-namespace Lean
-
-/- We mark this primitive as `unsafe` because it assumes the table is
-   being accessed by a single thread. -/
-@[extern 2 "lean_modify_constant_table"]
-unsafe constant modifyConstTable (f : Array (Name × NonScalar) → Array (Name × NonScalar)) : IO Unit := default _
-
-/- We mark this primitive as `unsafe` because it assumes the table is
-   being accessed by a single thread. -/
-@[extern 1 "lean_get_constant_table"]
-unsafe constant getConstTable : IO (Array (Name × NonScalar)) := default _
-
-/- We mark this primitive as `unsafe` because it assumes the table is
-   being accessed by a single thread. We meet this requirement by invoking
-   it after we have initialized all modules.
-   See `src/init/init.cpp` -/
-@[export lean.sort_const_table_core]
-unsafe def sortConstTable : IO Unit :=
-modifyConstTable (fun cs => cs.qsort (fun e₁ e₂ => Name.quickLt e₁.1 e₂.1))
-
-/- We make this primitive as `unsafe` because it uses `unsafeCast`, and
-   the program may crash if the type provided by the user is incorrect.
-   It also assumes there are no threads trying to update the table concurrently. -/
-unsafe def evalConst (α : Type) [Inhabited α] (c : Name) : IO α :=
-do cs ← getConstTable;
-   match cs.binSearch (c, default _) (fun e₁ e₂ => Name.quickLt e₁.1 e₂.1) with
-   | some (_, v) => pure (unsafeCast v)
-   | none        => throw (IO.userError ("unknow constant '" ++ toString c ++ "'"))
-
-end Lean
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index f10ddd2d72..4a7eca13dc 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1795,41 +1795,6 @@ struct runtime_stats {
 runtime_stats g_runtime_stats;
 #endif
 
-// =======================================
-// Global constant table
-
-static object * g_decls = nullptr;
-
-/* Remark: this is ugly, it forces the Lean runtime to depend on the implementation of `Lean.Name`.
-   This may be an issue for standalone applications. */
-extern "C" object* lean_name_mk_string(obj_arg p, obj_arg s);
-
-obj_res mk_const_name(obj_arg p, char const * s) {
-    return lean_name_mk_string(p, mk_string(s));
-}
-
-/* Remark: we should improve this too. A standalone application implemented in Lean will seldom
-   need a table with all constants. This table is only used to implement `Lean.evalConst`
-   unsafe primitive. */
-void register_constant(obj_arg fn, obj_arg obj) {
-    object * p = alloc_cnstr(0, 2, 0);
-    cnstr_set(p, 0, fn);
-    cnstr_set(p, 1, obj);
-    g_decls = array_push(g_decls, p);
-}
-
-obj_res set_io_result(obj_arg r, obj_arg a);
-
-extern "C" obj_res lean_modify_constant_table(obj_arg f, obj_arg w) {
-    g_decls = apply_1(f, g_decls);
-    return w;
-}
-
-extern "C" obj_res lean_get_constant_table(obj_arg w) {
-    inc(g_decls);
-    return set_io_result(w, g_decls);
-}
-
 // =======================================
 // Module initialization
 
@@ -1838,7 +1803,6 @@ void initialize_object() {
     g_ext_classes_mutex = new mutex();
     g_array_empty       = alloc_array(0, 0);
     mark_persistent(g_array_empty);
-    g_decls             = alloc_array(0, 8192);
 }
 
 void finalize_object() {
diff --git a/src/runtime/object.h b/src/runtime/object.h
index 1b88a0f22b..04ab2e6a4a 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -1486,15 +1486,6 @@ obj_res io_ref_set(b_obj_arg, obj_arg, obj_arg);
 obj_res io_ref_reset(b_obj_arg, obj_arg);
 obj_res io_ref_swap(b_obj_arg, obj_arg, obj_arg);
 
-// =======================================
-// Global function table
-
-/* Create a Lean.Name for a constant */
-obj_res mk_const_name(obj_arg p, char const * s);
-inline obj_res mk_const_name(char const * s) { return mk_const_name(box(0), s); }
-void register_constant(obj_arg n, obj_arg obj);
-#define REGISTER_LEAN_FUNCTION(fn, arity, cls) ::lean::register_constant(fn, lean::alloc_closure(reinterpret_cast<void*>(cls), arity, 0))
-
 // =======================================
 // Module initialization/finalization
 void initialize_object();
diff --git a/src/stage0/CMakeLists.txt b/src/stage0/CMakeLists.txt
index 122c71ee89..086cb1e8f7 100644
--- a/src/stage0/CMakeLists.txt
+++ b/src/stage0/CMakeLists.txt
@@ -1 +1 @@
-add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/class.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/implementedbyattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specialize.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/basic.cpp ./init/lean/elaborator/command.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/namegenerator.cpp ./init/lean/options.cpp ./init/lean/parser/command.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/term.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/scopes.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/class.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/implementedbyattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specialize.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/basic.cpp ./init/lean/elaborator/command.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/namegenerator.cpp ./init/lean/options.cpp ./init/lean/parser/command.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/term.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/scopes.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
diff --git a/src/stage0/init/lean/default.cpp b/src/stage0/init/lean/default.cpp
index 415ee40e52..a96108428c 100644
--- a/src/stage0/init/lean/default.cpp
+++ b/src/stage0/init/lean/default.cpp
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.default
-// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.projfns init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default init.lean.eqncompiler.default init.lean.class
+// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.projfns init.lean.runtime init.lean.attributes init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default init.lean.eqncompiler.default init.lean.class
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -20,7 +20,6 @@ obj* initialize_init_lean_modifiers(obj*);
 obj* initialize_init_lean_projfns(obj*);
 obj* initialize_init_lean_runtime(obj*);
 obj* initialize_init_lean_attributes(obj*);
-obj* initialize_init_lean_evalconst(obj*);
 obj* initialize_init_lean_parser_default(obj*);
 obj* initialize_init_lean_reducibilityattrs(obj*);
 obj* initialize_init_lean_elaborator_default(obj*);
@@ -43,8 +42,6 @@ w = initialize_init_lean_runtime(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_attributes(w);
 if (io_result_is_error(w)) return w;
-w = initialize_init_lean_evalconst(w);
-if (io_result_is_error(w)) return w;
 w = initialize_init_lean_parser_default(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_reducibilityattrs(w);