From 6e3a6ff40fd8064c60163f7367d6cbcfd0044dc6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Aug 2018 09:09:37 -0700 Subject: [PATCH] feat(library/noncomputable): mark all VM builtins as computable --- src/library/noncomputable.cpp | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index 85d62f6ff2..26f19940ae 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/quote.h" #include "library/constants.h" +#include "library/vm/vm.h" // TODO(Leo): move inline attribute declaration to library #include "library/compiler/inliner.h" namespace lean { @@ -62,17 +63,10 @@ struct noncomputable_modification : public modification { } }; -// TODO(Leo): implement better support for extending this set of builtin constants static bool is_builtin_extra(name const & n) { return - n == get_io_core_name() || n == get_sorry_ax_name() || - n == get_monad_io_impl_name() || - n == get_monad_io_terminal_impl_name() || - n == get_monad_io_file_system_impl_name() || - n == get_monad_io_environment_impl_name() || - n == get_monad_io_process_impl_name() || - n == get_monad_io_random_impl_name(); + is_vm_builtin_function(n); } static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ext, name const & n) {