From 16f7bef88f52dafefcb4e8beb5ef3a025e06dfc4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Oct 2020 09:05:51 -0700 Subject: [PATCH] chore: remove old frontend leftovers --- src/Init/System/IO.lean | 4 --- src/Lean/Attributes.lean | 3 -- src/Lean/Elab/Quotation.lean | 10 ------- src/Lean/Environment.lean | 26 ----------------- src/Lean/Server/Snapshots.lean | 1 - src/kernel/environment.cpp | 51 ---------------------------------- src/kernel/environment.h | 17 ------------ 7 files changed, 112 deletions(-) diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 19950b836f..da41c5b8da 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -480,8 +480,4 @@ instance {α : Type} [HasEval α] : HasEval (IO α) := @[noinline, nospecialize] def runEval {α : Type u} [HasEval α] (a : Unit → α) : IO (String × Except IO.Error Unit) := IO.FS.withIsolatedStreams (HasEval.eval a false) --- TODO: delete aux function old frontend -def runEvalOld {α : Type u} [HasEval α] (a : α) : IO (String × Except IO.Error Unit) := - runEval (fun _ => a) - end Lean diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 063990fa0a..4a0041e535 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -31,9 +31,6 @@ instance : MonadResolveName AttrM := { getOpenDecls := do pure (← read).openDecls } --- TODO: after we delete the old frontend, we should use `EIO` with a richer exception kind at AttributeImpl. --- We must perform a similar modification at `PersistentEnvExtension` - structure AttributeImplCore := (name : Name) (descr : String) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 2188b43306..65eea3e84c 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -10,16 +10,6 @@ import Lean.Syntax import Lean.ResolveName import Lean.Elab.Term -/- TODO - -Quotations are currently integrated hackily into the old frontend. This implies the following restrictions: -* quotations have to fit in a single line, because that's how the old scanner works :) -* `open` commands are not respected (but `export`, `namespace` are) -* antiquotation terms have to be trivial (locals, consts (w/ projections), and apps, basically) - -After removing the old frontend, quotations in this and other files should be cleaned up. --/ - namespace Lean.Elab.Term.Quotation open Lean.Syntax (isQuot isAntiquot) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 78e7f568fa..1d1b5c5662 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -209,32 +209,6 @@ unsafe def imp : EnvExtensionInterface := { mkInitialExtStates := mkInitialExtStates } -/- Auxiliary code for supporting old frontend. It will be deleted -/ -namespace OldFrontend -/- 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] -unsafe def registerCPPExtension (initial : EnvExtensionState) : Option Nat := - Except.toOption $ unsafeIO do - let ext ← registerExt (pure initial) - pure ext.idx - -@[export lean_set_extension] -unsafe def setCPPExtensionState (env : Environment) (idx : Nat) (s : EnvExtensionState) : Option Environment := - Except.toOption $ unsafeIO do - let exts ← envExtensionsRef.get - pure $ setState (exts.get! idx) env s - -@[export lean_get_extension] -unsafe def getCPPExtensionState (env : Environment) (idx : Nat) : Option EnvExtensionState := - Except.toOption $ unsafeIO do - let exts ← envExtensionsRef.get - pure $ getState (exts.get! idx) env - -end OldFrontend - end EnvExtensionInterfaceUnsafe @[implementedBy EnvExtensionInterfaceUnsafe.imp] diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index bbc9c346f2..1f8310f7c3 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -15,7 +15,6 @@ each command. Importantly, we allow (re)starting compilation from any snapshot/position in the file for interactive editing purposes. -/ namespace Lean -namespace Elab end Elab -- Hack for old frontend namespace Server namespace Snapshots diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 2824b94a52..c50bae03c8 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -243,56 +243,6 @@ extern "C" object * lean_add_decl(object * env, object * decl) { }); } -static void env_ext_finalizer(void * ext) { - delete static_cast(ext); -} - -static void env_ext_foreach(void * /* ext */, b_obj_arg /* fn */) { - /* The foreach combinator is used by `mark_mt` when marking values as "multi-threaded". - Moreover, it is invoked even when we don't use threads because of global - IO.Ref is considered to be "multi-threaded". - - So, we just ignore this issue for now. - This is not critical since eventually all environment extensions will be implemented in Lean, - and we will be able to delete this code. - */ -} - -static external_object_class * g_env_ext_class = nullptr; - -static environment_extension const & to_env_ext(b_obj_arg o) { - lean_assert(external_class(o) == g_env_ext_class); - return *static_cast(external_data(o)); -} - -static obj_res to_object(environment_extension * ext) { - return alloc_external(g_env_ext_class, ext); -} - -unsigned environment::register_extension(environment_extension * initial) { - object * r = lean_register_extension(to_object(initial)); - if (is_scalar(r)) { throw exception("error creating empty environment"); } - unsigned idx = unbox(cnstr_get(r, 0)); - dec(r); - return idx; -} - -environment_extension const & environment::get_extension(unsigned id) const { - object * r = lean_get_extension(to_obj_arg(), box(id)); - if (is_scalar(r)) { throw exception("invalid extension id"); } - object * ext = cnstr_get(r, 0); - dec(r); - return to_env_ext(ext); -} - -environment environment::update(unsigned id, environment_extension * ext) const { - object * r = lean_set_extension(to_obj_arg(), box(id), to_object(ext)); - if (is_scalar(r)) { throw exception("invalid extension id"); } - environment env(cnstr_get(r, 0), true); - dec(r); - return env; -} - void environment::for_each_constant(std::function const & f) const { smap_foreach(cnstr_get(raw(), 1), [&](object *, object * v) { constant_info cinfo(v, true); @@ -307,7 +257,6 @@ void environment::display_stats() const { } void initialize_environment() { - g_env_ext_class = register_external_object_class(env_ext_finalizer, env_ext_foreach); } void finalize_environment() { diff --git a/src/kernel/environment.h b/src/kernel/environment.h index ccce8ca64d..64456b9905 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -74,23 +74,6 @@ public: /** \brief Extends the current environment with the given declaration */ environment add(declaration const & d, bool check = true) const; - /** \brief Register an environment extension. Every environment - object may contain this extension. The argument \c initial is - the initial value for the new extensions. The extension object - can be retrieved using the given token (unsigned integer) returned - by this method. - - \remark The extension objects are created on demand. - - \see get_extension */ - static unsigned register_extension(environment_extension * initial); - - /** \brief Return the extension with the given id. */ - environment_extension const & get_extension(unsigned extid) const; - - /** \brief Update the environment extension with the given id. */ - environment update(unsigned extid, environment_extension * ext) const; - /** \brief Apply the function \c f to each constant */ void for_each_constant(std::function const & f) const;