From 17ae59b5b0d00ed75868b4ee1d04d60f04f61caa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Aug 2018 15:27:12 -0700 Subject: [PATCH] chore(*): remove more stuff --- library/init/meta/default.lean | 3 +- library/init/meta/environment.lean | 116 -------- library/init/meta/interaction_monad.lean | 2 +- library/init/meta/tactic.lean | 3 +- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/init_module.cpp | 3 - src/frontends/lean/user_notation.cpp | 125 --------- src/frontends/lean/user_notation.h | 12 - src/library/tactic/tactic_state.cpp | 13 - src/library/vm/CMakeLists.txt | 4 +- src/library/vm/init_module.cpp | 6 - src/library/vm/interaction_state_imp.h | 1 - src/library/vm/vm_environment.cpp | 288 ------------------- src/library/vm/vm_environment.h | 17 -- src/library/vm/vm_parser.cpp | 342 ----------------------- src/library/vm/vm_parser.h | 20 -- 16 files changed, 6 insertions(+), 951 deletions(-) delete mode 100644 library/init/meta/environment.lean delete mode 100644 src/frontends/lean/user_notation.cpp delete mode 100644 src/frontends/lean/user_notation.h delete mode 100644 src/library/vm/vm_environment.cpp delete mode 100644 src/library/vm/vm_environment.h delete mode 100644 src/library/vm/vm_parser.cpp delete mode 100644 src/library/vm/vm_parser.h diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index 86a6c1e07a..cb085ef630 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -5,5 +5,4 @@ Authors: Leonardo de Moura -/ prelude import init.meta.name init.meta.options init.meta.format -import init.meta.level init.meta.expr init.meta.environment -import init.meta.tactic +import init.meta.level init.meta.expr init.meta.tactic diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean deleted file mode 100644 index 2fab4616ca..0000000000 --- a/library/init/meta/environment.lean +++ /dev/null @@ -1,116 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -prelude -import init.meta.declaration init.meta.expr init.meta.exceptional init.data.option.basic - -meta constant environment : Type - -namespace environment -/-- -Information for a projection declaration -- `cname` is the name of the constructor associated with the projection. -- `nparams` is the number of constructor parameters -- `idx` is the parameter being projected by this projection -- `is_class` is tt iff this is a class projection. --/ -structure projection_info := -(cname : name) -(nparams : nat) -(idx : nat) -(is_class : bool) - -/-- Create a standard environment using the given trust level -/ -meta constant mk_std : nat → environment -/-- Return the trust level of the given environment -/ -meta constant trust_lvl : environment → nat --- /-- Add a new declaration to the environment -/ --- meta constant add : environment → declaration → exceptional environment -/-- Retrieve a declaration from the environment -/ -meta constant get : environment → name → exceptional constant_info -meta def contains (env : environment) (d : name) : bool := -match env.get d with -| exceptional.success _ := tt -| exceptional.exception _ _ := ff - -/-- Register the given name as a namespace, making it available to the `open` command -/ -meta constant add_namespace : environment → name → environment -/-- Return tt iff the given name is a namespace -/ -meta constant is_namespace : environment → name → bool -/-- Add a new inductive datatype to the environment - name, universe parameters, number of parameters, type, constructors (name and type), is_meta -/ -meta constant add_inductive : environment → name → list name → nat → expr → list (name × expr) → bool → - exceptional environment -/-- Return tt iff the given name is an inductive datatype -/ -meta constant is_inductive : environment → name → bool -/-- Return tt iff the given name is a constructor -/ -meta constant is_constructor : environment → name → bool -/-- Return tt iff the given name is a recursor -/ -meta constant is_recursor : environment → name → bool -/-- Return tt iff the given name is a recursive inductive datatype -/ -meta constant is_recursive : environment → name → bool -/-- Return the name of the inductive datatype of the given constructor. -/ -meta constant inductive_type_of : environment → name → option name -/-- Return the constructors of the inductive datatype with the given name -/ -meta constant constructors_of : environment → name → list name -/-- Return the recursor of the given inductive datatype -/ -meta constant recursor_of : environment → name → option name -/-- Return the number of parameters of the inductive datatype -/ -meta constant inductive_num_params : environment → name → nat -/-- Return the number of indices of the inductive datatype -/ -meta constant inductive_num_indices : environment → name → nat -/-- Return tt iff the inductive datatype recursor supports dependent elimination -/ -meta constant inductive_dep_elim : environment → name → bool -/-- Return tt iff the given name is a generalized inductive datatype -/ -meta constant is_ginductive : environment → name → bool -meta constant is_projection : environment → name → option projection_info -/-- Fold over declarations in the environment -/ -meta constant fold {α :Type} : environment → α → (constant_info → α → α) → α -/-- `relation_info env n` returns some value if n is marked as a relation in the given environment. - the tuple contains: total number of arguments of the relation, lhs position and rhs position. -/ -meta constant relation_info : environment → name → option (nat × nat × nat) -/-- `refl_for env R` returns the name of the reflexivity theorem for the relation R -/ -meta constant refl_for : environment → name → option name -/-- `symm_for env R` returns the name of the symmetry theorem for the relation R -/ -meta constant symm_for : environment → name → option name -/-- `trans_for env R` returns the name of the transitivity theorem for the relation R -/ -meta constant trans_for : environment → name → option name -/-- `decl_olean env d` returns the name of the .olean file where d was defined. - The result is none if d was not defined in an imported file. -/ -meta constant decl_olean : environment → name → option string -/-- `decl_pos env d` returns the source location of d if available. -/ -meta constant decl_pos : environment → name → option pos -/-- Return the fields of the structure with the given name, or `none` if it is not a structure -/ -meta constant structure_fields : environment → name → option (list name) -meta constant fingerprint : environment → nat -open lean.expr - -meta def is_constructor_app (env : environment) (e : expr) : bool := -is_constant (get_app_fn e) && is_constructor env (const_name (get_app_fn e)) - -meta def is_refl_app (env : environment) (e : expr) : option (name × expr × expr) := -match (refl_for env (const_name (get_app_fn e))) with -| (some n) := - if get_app_num_args e ≥ 2 - then some (n, app_arg (app_fn e), app_arg e) - else none -| none := none - -/-- Return true if 'n' has been declared in the current file -/ -meta def in_current_file (env : environment) (n : name) : bool := -(env.decl_olean n).is_none && env.contains n - -meta def is_definition (env : environment) (n : name) : bool := -match env.get n with -| exceptional.success (lean.constant_info.defn_info _) := tt -| _ := ff - -end environment - -meta instance : has_repr environment := -⟨λ e, "[environment]"⟩ - -meta instance : inhabited environment := -⟨environment.mk_std 0⟩ diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean index 13bdac5311..184923069d 100644 --- a/library/init/meta/interaction_monad.lean +++ b/library/init/meta/interaction_monad.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich prelude import init.function init.data.option.basic init.util import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail -import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment +import init.data.nat.div init.meta.exceptional init.meta.format import init.meta.pexpr init.data.repr init.data.string.basic init.data.to_string universes u v diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 1aef2a8a5b..68dc57bae0 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.function init.data.option.basic init.util import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail -import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment +import init.data.nat.div init.meta.exceptional init.meta.format import init.meta.pexpr init.data.repr init.data.string.basic init.meta.interaction_monad meta constant tactic_state : Type @@ -14,7 +14,6 @@ meta constant tactic_state : Type universes u v namespace tactic_state -meta constant env : tactic_state → environment /-- Format the given tactic state. If `target_lhs_only` is true and the target is of the form `lhs ~ rhs`, where `~` is a simplification relation, then only the `lhs` is displayed. diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index abb5605188..6c55416bf5 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -8,4 +8,4 @@ init_module.cpp type_util.cpp decl_attributes.cpp prenum.cpp print_cmd.cpp elaborator.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp brackets.cpp info_manager.cpp json.cpp module_parser.cpp -interactive.cpp completion.cpp user_notation.cpp typed_expr.cpp choice.cpp) +interactive.cpp completion.cpp typed_expr.cpp choice.cpp) diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index bd177fd79a..f8bd619194 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -28,7 +28,6 @@ Author: Leonardo de Moura #include "frontends/lean/choice.h" #include "frontends/lean/interactive.h" #include "frontends/lean/completion.h" -#include "frontends/lean/user_notation.h" namespace lean { void initialize_frontend_lean_module() { @@ -56,10 +55,8 @@ void initialize_frontend_lean_module() { initialize_brackets(); initialize_interactive(); initialize_completion(); - initialize_user_notation(); } void finalize_frontend_lean_module() { - finalize_user_notation(); finalize_completion(); finalize_interactive(); finalize_brackets(); diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp deleted file mode 100644 index a2228c07ba..0000000000 --- a/src/frontends/lean/user_notation.cpp +++ /dev/null @@ -1,125 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Sebastian Ullrich -*/ -#include "kernel/abstract.h" -#include "library/constants.h" -#include "library/attribute_manager.h" -#include "library/scoped_ext.h" -#include "library/tactic/elaborator_exception.h" -#include "library/string.h" -#include "library/vm/vm_expr.h" -#include "library/vm/vm_parser.h" -#include "library/quote.h" -#include "frontends/lean/elaborator.h" - -namespace lean { -static environment add_user_notation(environment const & env, name const & d, unsigned prio, bool persistent) { - auto type = env.get(d).get_type(); - bool is_nud = true; - name tk; - if (is_binding(type) && is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) { - auto const & parser = app_arg(binding_domain(type)); - if (is_app_of(parser, get_lean3_parser_pexpr_name(), 1)) { - is_nud = false; - type = binding_body(type); - } - } - if (is_binding(type) && is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) { - auto const & parser = app_arg(binding_domain(type)); - if (is_app_of(parser, get_lean3_parser_tk_name(), 1)) { - if (auto lit = to_string(app_arg(parser))) { - tk = *lit; - type = binding_body(type); - } else { - throw elaborator_exception(app_arg(parser), - "invalid user-defined notation, token must be a name literal"); - } - } - } - if (!tk) { - throw exception("invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` " - "parameter, optionally preceded by `interactive.parse lean.parser.pexpr` parameter"); - } - - expr t = type; - while (is_pi(t)) { t = binding_body(t); } - if (!is_app_of(t, get_lean3_parser_name(), 1)) { - throw exception("invalid user-defined notation, must return type `lean.parser p`"); - } - - expr dummy = mk_true(); - persistence persist = persistent ? persistence::file : persistence::scope; - - return add_notation(env, notation_entry(is_nud, {notation::transition(tk, notation::mk_ext_action( - [=](parser & p, unsigned num, expr const * args, pos_info const & pos) -> expr { - lean_always_assert(num == (is_nud ? 0 : 1)); - expr parser = mk_constant(d); - if (!is_nud) - parser = mk_app(parser, mk_pexpr_quote(args[0])); - // `parse (tk c)` arg - parser = mk_app(parser, mk_constant(get_unit_star_name())); - for (expr t = type; is_pi(t); t = binding_body(t)) { - expr arg_type = binding_domain(t); - if (is_app_of(arg_type, get_interactive_parse_name())) { - parser = mk_app(parser, parse_interactive_param(p, arg_type)); - } else { - expr e = p.parse_expr(get_max_prec()); - if (has_loose_bvars(e) || has_local(e)) { - throw elaborator_exception(e, "invalid argument to user-defined notation, must be closed term"); - } - parser = mk_app(parser, e); - } - } - parser = p.elaborate("_user_notation", {}, parser).first; - try { - return to_expr(run_parser(p, parser)); - } catch (formatted_exception const & ex) { - if (ex.get_pos() && *ex.get_pos() >= pos) { - throw; - } else { - throw formatted_exception(some(pos), ex.pp()); - } - } - }))}, mk_bvar(0), /* overload */ persistent, prio, notation_entry_group::Main, /* parse_only */ true), persist); -} - -struct user_notation_modification : public modification { - LEAN_MODIFICATION("USR_NOTATION") - - name m_name; - - user_notation_modification() {} - user_notation_modification(name const & name) : m_name(name) {} - - void perform(environment & env) const override { - unsigned prio = get_attribute(env, "user_notation").get_prio(env, m_name); - env = add_user_notation(env, m_name, prio, /* persistent */ true); - } - - void serialize(serializer & s) const override { - s << m_name; - } - - static std::shared_ptr deserialize(deserializer & d) { - return std::make_shared(read_name(d)); - } -}; -void initialize_user_notation() { - user_notation_modification::init(); - register_system_attribute(basic_attribute( - "user_notation", "user-defined notation", - [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) { - if (persistent) { - return module::add_and_perform(env, std::make_shared(d)); - } else { - return add_user_notation(env, d, prio, persistent); - } - })); -} -void finalize_user_notation() { - user_notation_modification::finalize(); -} -} diff --git a/src/frontends/lean/user_notation.h b/src/frontends/lean/user_notation.h deleted file mode 100644 index 5ffd339de6..0000000000 --- a/src/frontends/lean/user_notation.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Sebastian Ullrich -*/ -#pragma once - -namespace lean { -void initialize_user_notation(); -void finalize_user_notation(); -} diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index d78e6ce498..5d17e2629d 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -20,7 +20,6 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" #include "library/aux_definition.h" #include "library/inductive_compiler/ginductive.h" -#include "library/vm/vm_environment.h" #include "library/vm/vm_exceptional.h" #include "library/vm/vm_format.h" #include "library/vm/vm_string.h" @@ -265,10 +264,6 @@ vm_obj to_obj(transparency_mode m) { return mk_vm_simple(static_cast(m)); } -vm_obj tactic_state_env(vm_obj const & s) { - return to_obj(tactic::to_state(s).env()); -} - vm_obj tactic_state_to_format(vm_obj const & s, vm_obj const & target_lhs_only) { return to_obj(tactic::to_state(s).pp_core(to_bool(target_lhs_only))); } @@ -716,12 +711,6 @@ vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) { } } -vm_obj tactic_set_env(vm_obj const & _env, vm_obj const & _s) { - tactic_state const & s = tactic::to_state(_s); - environment const & new_env = to_env(_env); - return tactic::mk_success(set_env(s, new_env)); -} - vm_obj tactic_open_namespaces(vm_obj const & s) { environment env = tactic::to_state(s).env(); buffer b; @@ -974,7 +963,6 @@ vm_obj tactic_frozen_local_instances(vm_obj const & s0) { } void initialize_tactic_state() { - DECLARE_VM_BUILTIN(name({"tactic_state", "env"}), tactic_state_env); DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr); DECLARE_VM_BUILTIN(name({"tactic_state", "to_format"}), tactic_state_to_format); DECLARE_VM_BUILTIN(name({"tactic_state", "get_options"}), tactic_state_get_options); @@ -1008,7 +996,6 @@ void initialize_tactic_state() { DECLARE_VM_BUILTIN(name({"tactic", "is_trace_enabled_for"}), tactic_is_trace_enabled_for); DECLARE_VM_BUILTIN(name({"tactic", "instantiate_mvars"}), tactic_instantiate_mvars); DECLARE_VM_BUILTIN(name({"tactic", "add_decl"}), tactic_add_decl); - DECLARE_VM_BUILTIN(name({"tactic", "set_env"}), tactic_set_env); DECLARE_VM_BUILTIN(name({"tactic", "doc_string"}), tactic_doc_string); DECLARE_VM_BUILTIN(name({"tactic", "add_doc_string"}), tactic_add_doc_string); DECLARE_VM_BUILTIN(name({"tactic", "module_doc_strings"}), tactic_module_doc_strings); diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 5860983903..55d3b6b551 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp vm_options.cpp vm_format.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp - vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp - vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp) + vm_declaration.cpp vm_list.cpp vm_pexpr.cpp + vm_int.cpp init_module.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 9c88cb9473..459981fc6e 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -18,8 +18,6 @@ Author: Leonardo de Moura #include "library/vm/vm_list.h" #include "library/vm/vm_exceptional.h" #include "library/vm/vm_declaration.h" -#include "library/vm/vm_environment.h" -#include "library/vm/vm_parser.h" #include "library/vm/vm_array.h" #include "library/vm/vm_string.h" #include "library/vm/vm_platform.h" @@ -40,8 +38,6 @@ void initialize_vm_core_module() { initialize_vm_list(); initialize_vm_exceptional(); initialize_vm_declaration(); - initialize_vm_environment(); - initialize_vm_parser(); initialize_vm_array(); initialize_vm_string(); initialize_vm_platform(); @@ -51,8 +47,6 @@ void finalize_vm_core_module() { finalize_vm_platform(); finalize_vm_string(); finalize_vm_array(); - finalize_vm_parser(); - finalize_vm_environment(); finalize_vm_declaration(); finalize_vm_exceptional(); finalize_vm_list(); diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index 1d29173ff1..db355e2436 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -14,7 +14,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich #include "library/message_builder.h" #include "library/time_task.h" #include "library/vm/interaction_state.h" -#include "library/vm/vm_environment.h" #include "library/vm/vm_exceptional.h" #include "library/vm/vm_format.h" #include "library/vm/vm_string.h" diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp deleted file mode 100644 index cc7b04bad0..0000000000 --- a/src/library/vm/vm_environment.cpp +++ /dev/null @@ -1,288 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "kernel/old_type_checker.h" -#include "kernel/inductive/inductive.h" -#include "kernel/standard_kernel.h" -#include "library/module.h" -#include "library/scoped_ext.h" -#include "library/class.h" -#include "library/projection.h" -#include "library/util.h" -#include "library/fingerprint.h" -#include "library/relation_manager.h" -#include "library/inductive_compiler/ginductive.h" -#include "library/vm/vm_nat.h" -#include "library/vm/vm_name.h" -#include "library/vm/vm_option.h" -#include "library/vm/vm_string.h" -#include "library/vm/vm_expr.h" -#include "library/vm/vm_declaration.h" -#include "library/vm/vm_exceptional.h" -#include "library/vm/vm_list.h" -#include "library/vm/vm_pos_info.h" -#include "frontends/lean/structure_cmd.h" - -namespace lean { -struct vm_environment : public vm_external { - environment m_val; - vm_environment(environment const & v):m_val(v) {} - virtual ~vm_environment() {} - virtual void dealloc() override { delete this; } - virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_environment(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new vm_environment(m_val); } -}; - -bool is_env(vm_obj const & o) { - return is_external(o) && dynamic_cast(to_external(o)); -} - -environment const & to_env(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(to_external(o))->m_val; -} - -vm_obj to_obj(environment const & n) { - return mk_vm_external(new vm_environment(n)); -} - -vm_obj environment_mk_std(vm_obj const & l) { - return to_obj(mk_environment(force_to_unsigned(l, 0))); -} - -vm_obj environment_trust_lvl(vm_obj const & env) { - return mk_vm_nat(to_env(env).trust_lvl()); -} - -/* -vm_obj environment_add(vm_obj const & env, vm_obj const & decl) { - try { - return mk_vm_exceptional_success(to_obj(module::add(to_env(env), check(to_env(env), to_declaration(decl))))); - } catch (throwable & ex) { - return mk_vm_exceptional_exception(std::current_exception()); - } -} -*/ - -vm_obj environment_get(vm_obj const & env, vm_obj const & n) { - try { - return mk_vm_exceptional_success(to_obj(to_env(env).get(to_name(n)))); - } catch (throwable & ex) { - return mk_vm_exceptional_exception(std::current_exception()); - } -} - -static list to_list_intro_rule(vm_obj const & cnstrs) { - if (is_simple(cnstrs)) - return list(); - else - return list(mk_local(to_name(cfield(cfield(cnstrs, 0), 0)), - to_expr(cfield(cfield(cnstrs, 0), 1))), - to_list_intro_rule(cfield(cnstrs, 1))); -} - -vm_obj environment_add_inductive(vm_obj const & env, vm_obj const & n, vm_obj const & ls, vm_obj const & num, - vm_obj const & type, vm_obj const & cnstrs, vm_obj const & is_meta) { - try { - environment new_env = module::add_inductive(to_env(env), - inductive::inductive_decl(to_name(n), - to_names(ls), - force_to_unsigned(num, 0), - to_expr(type), - to_list_intro_rule(cnstrs)), - !to_bool(is_meta)); - return mk_vm_exceptional_success(to_obj(new_env)); - } catch (throwable & ex) { - return mk_vm_exceptional_exception(std::current_exception()); - } -} - -vm_obj environment_is_inductive(vm_obj const & env, vm_obj const & n) { - return mk_vm_bool(static_cast(inductive::is_inductive_decl(to_env(env), to_name(n)))); -} - -vm_obj environment_is_constructor(vm_obj const & env, vm_obj const & n) { - return mk_vm_bool(static_cast(inductive::is_intro_rule(to_env(env), to_name(n)))); -} - -vm_obj environment_inductive_type_of(vm_obj const & env, vm_obj const & n) { - if (auto I = inductive::is_intro_rule(to_env(env), to_name(n))) - return mk_vm_some(to_obj(*I)); - else - return mk_vm_none(); -} - -vm_obj environment_is_recursor(vm_obj const & env, vm_obj const & n) { - return mk_vm_bool(static_cast(inductive::is_elim_rule(to_env(env), to_name(n)))); -} - -vm_obj environment_is_recursive(vm_obj const & env, vm_obj const & n) { - return mk_vm_bool(static_cast(is_recursive_datatype(to_env(env), to_name(n)))); -} - -vm_obj environment_constructors_of(vm_obj const & env, vm_obj const & n) { - buffer ns; - get_intro_rule_names(to_env(env), to_name(n), ns); - return to_obj(names(ns)); -} - -vm_obj environment_recursor_of(vm_obj const & env, vm_obj const & n) { - if (auto I = inductive::is_elim_rule(to_env(env), to_name(n))) - return mk_vm_some(to_obj(*I)); - else - return mk_vm_none(); -} - -vm_obj environment_inductive_num_params(vm_obj const & env, vm_obj const & n) { - if (auto r = inductive::get_num_params(to_env(env), to_name(n))) - return mk_vm_nat(*r); - else - return mk_vm_nat(0); -} - -vm_obj environment_inductive_num_indices(vm_obj const & env, vm_obj const & n) { - if (auto r = inductive::get_num_indices(to_env(env), to_name(n))) - return mk_vm_nat(*r); - else - return mk_vm_nat(0); -} - -vm_obj environment_inductive_dep_elim(vm_obj const & env, vm_obj const & n) { - return mk_vm_bool(inductive::has_dep_elim(to_env(env), to_name(n))); -} - -vm_obj environment_is_ginductive(vm_obj const & env, vm_obj const & n) { - return mk_vm_bool(static_cast(is_ginductive(to_env(env), to_name(n)))); -} - -vm_obj environment_fold(vm_obj const &, vm_obj const & env, vm_obj const & a, vm_obj const & fn) { - vm_obj r = a; - to_env(env).for_each_constant([&](constant_info const & info) { - r = invoke(fn, to_obj(info), r); - }); - return r; -} - -vm_obj environment_relation_info(vm_obj const & env, vm_obj const & n) { - if (relation_info const * info = get_relation_info(to_env(env), to_name(n))) { - vm_obj r = mk_vm_pair(mk_vm_nat(info->get_arity()), mk_vm_pair(mk_vm_nat(info->get_lhs_pos()), mk_vm_nat(info->get_rhs_pos()))); - return mk_vm_some(r); - } else { - return mk_vm_none(); - } -} - -vm_obj environment_refl_for(vm_obj const & env, vm_obj const & n) { - if (optional r = get_refl_info(to_env(env), to_name(n))) { - return mk_vm_some(to_obj(*r)); - } else { - return mk_vm_none(); - } -} - -vm_obj environment_trans_for(vm_obj const & env, vm_obj const & n) { - if (optional r = get_trans_info(to_env(env), to_name(n))) { - return mk_vm_some(to_obj(*r)); - } else { - return mk_vm_none(); - } -} - -vm_obj environment_symm_for(vm_obj const & env, vm_obj const & n) { - if (optional r = get_symm_info(to_env(env), to_name(n))) { - return mk_vm_some(to_obj(*r)); - } else { - return mk_vm_none(); - } -} - -vm_obj environment_decl_olean(vm_obj const & env, vm_obj const & n) { - if (optional olean = get_decl_olean(to_env(env), to_name(n))) { - return mk_vm_some(to_obj(*olean)); - } else { - return mk_vm_none(); - } -} - -vm_obj environment_decl_pos(vm_obj const & env, vm_obj const & n) { - if (optional pos = get_decl_pos_info(to_env(env), to_name(n))) { - return mk_vm_some(to_obj(*pos)); - } else { - return mk_vm_none(); - } -} - -vm_obj environment_add_namespace(vm_obj const & env, vm_obj const & n) { - return to_obj(add_namespace(to_env(env), to_name(n))); -} - -vm_obj environment_is_namespace(vm_obj const & env, vm_obj const & n) { - return mk_vm_bool(is_namespace(to_env(env), to_name(n))); -} - -vm_obj environment_structure_fields(vm_obj const & env, vm_obj const & n) { - if (is_structure(to_env(env), to_name(n))) { - return mk_vm_some(to_obj(get_structure_fields(to_env(env), to_name(n)))); - } else { - return mk_vm_none(); - } -} - -/* -structure projection_info := -(cname : name) -(nparams : nat) -(idx : nat) -(is_class : bool) -*/ -vm_obj environment_is_projection(vm_obj const & env, vm_obj const & n) { - if (auto info = get_projection_info(to_env(env), to_name(n))) { - return mk_vm_some(mk_vm_constructor(0, to_obj(info->m_constructor), mk_vm_nat(info->m_nparams), - mk_vm_nat(info->m_i), mk_vm_bool(info->m_inst_implicit))); - } else { - return mk_vm_none(); - } -} - -vm_obj environment_fingerprint(vm_obj const & env) { - return mk_vm_nat(mpz(get_fingerprint(to_env(env)))); -} - -void initialize_vm_environment() { - DECLARE_VM_BUILTIN(name({"environment", "mk_std"}), environment_mk_std); - DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}), environment_trust_lvl); - // DECLARE_VM_BUILTIN(name({"environment", "add"}), environment_add); - DECLARE_VM_BUILTIN(name({"environment", "get"}), environment_get); - DECLARE_VM_BUILTIN(name({"environment", "fold"}), environment_fold); - DECLARE_VM_BUILTIN(name({"environment", "add_inductive"}), environment_add_inductive); - DECLARE_VM_BUILTIN(name({"environment", "is_inductive"}), environment_is_inductive); - DECLARE_VM_BUILTIN(name({"environment", "is_constructor"}), environment_is_constructor); - DECLARE_VM_BUILTIN(name({"environment", "is_recursor"}), environment_is_recursor); - DECLARE_VM_BUILTIN(name({"environment", "is_recursive"}), environment_is_recursive); - DECLARE_VM_BUILTIN(name({"environment", "inductive_type_of"}), environment_inductive_type_of); - DECLARE_VM_BUILTIN(name({"environment", "constructors_of"}), environment_constructors_of); - DECLARE_VM_BUILTIN(name({"environment", "recursor_of"}), environment_recursor_of); - DECLARE_VM_BUILTIN(name({"environment", "inductive_num_params"}), environment_inductive_num_params); - DECLARE_VM_BUILTIN(name({"environment", "inductive_num_indices"}), environment_inductive_num_indices); - DECLARE_VM_BUILTIN(name({"environment", "inductive_dep_elim"}), environment_inductive_dep_elim); - DECLARE_VM_BUILTIN(name({"environment", "add_namespace"}), environment_add_namespace); - DECLARE_VM_BUILTIN(name({"environment", "is_namespace"}), environment_is_namespace); - DECLARE_VM_BUILTIN(name({"environment", "is_ginductive"}), environment_is_ginductive); - DECLARE_VM_BUILTIN(name({"environment", "is_projection"}), environment_is_projection); - DECLARE_VM_BUILTIN(name({"environment", "relation_info"}), environment_relation_info); - DECLARE_VM_BUILTIN(name({"environment", "refl_for"}), environment_refl_for); - DECLARE_VM_BUILTIN(name({"environment", "symm_for"}), environment_symm_for); - DECLARE_VM_BUILTIN(name({"environment", "trans_for"}), environment_trans_for); - DECLARE_VM_BUILTIN(name({"environment", "decl_olean"}), environment_decl_olean); - DECLARE_VM_BUILTIN(name({"environment", "decl_pos"}), environment_decl_pos); - DECLARE_VM_BUILTIN(name({"environment", "structure_fields"}), environment_structure_fields); - DECLARE_VM_BUILTIN(name({"environment", "fingerprint"}), environment_fingerprint); -} - -void finalize_vm_environment() { -} -} diff --git a/src/library/vm/vm_environment.h b/src/library/vm/vm_environment.h deleted file mode 100644 index fee1d20235..0000000000 --- a/src/library/vm/vm_environment.h +++ /dev/null @@ -1,17 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/environment.h" -#include "library/vm/vm.h" - -namespace lean { -bool is_env(vm_obj const & o); -environment const & to_env(vm_obj const & o); -vm_obj to_obj(environment const & n); -void initialize_vm_environment(); -void finalize_vm_environment(); -} diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp deleted file mode 100644 index 8be2a9cc96..0000000000 --- a/src/library/vm/vm_parser.cpp +++ /dev/null @@ -1,342 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Sebastian Ullrich -*/ -#include "library/vm/vm_parser.h" -#include -#include -#include -#include "runtime/utf8.h" -#include "library/constants.h" -#include "library/explicit.h" -#include "library/num.h" -#include "library/quote.h" -#include "library/trace.h" -#include "library/vm/interaction_state_imp.h" -#include "library/tactic/elaborate.h" -#include "library/vm/vm_string.h" -#include "library/vm/vm_options.h" -#include "library/vm/vm_environment.h" -#include "library/vm/vm_expr.h" -#include "library/vm/vm_nat.h" -#include "library/vm/vm_name.h" -#include "library/vm/vm_pos_info.h" -#include "frontends/lean/info_manager.h" -#include "frontends/lean/elaborator.h" -#include "frontends/lean/decl_util.h" -#include "frontends/lean/parser.h" -#include "frontends/lean/inductive_cmds.h" - -namespace lean { - -struct lean_parser_state { - parser * m_p; -}; - -bool is_ts_safe(lean_parser_state const &) { return false; } -template struct interaction_monad; -typedef interaction_monad lean_parser; - -#define TRY try { -#define CATCH } catch (break_at_pos_exception const & ex) { throw; }\ - catch (exception const & ex) { return lean_parser::mk_exception(std::current_exception(), s); } - -vm_obj run_parser(parser & p, expr const & spec, buffer const & args) { - type_context_old ctx(p.env(), p.get_options()); - auto r = lean_parser::evaluator(ctx, p.get_options())(spec, args, lean_parser_state {&p}); - return lean_parser::get_success_value(r); -} - -expr parse_interactive_param(parser & p, expr const & param_ty) { - lean_assert(is_app_of(param_ty, get_interactive_parse_name())); - buffer param_args; - get_app_args(param_ty, param_args); - // alpha, has_reflect alpha, parser alpha - lean_assert(param_args.size() == 3); - if (has_loose_bvars(param_args[2])) { - throw elaborator_exception(param_args[2], "error running user-defined parser: must be closed expression"); - } - try { - vm_obj vm_parsed = run_parser(p, param_args[2]); - type_context_old ctx(p.env()); - name n("_reflect"); - lean_parser::evaluator eval(ctx, p.get_options()); - auto env = eval.compile(n, param_args[1]); - vm_state S(env, p.get_options()); - auto vm_res = S.invoke(n, vm_parsed); - expr r = to_expr(vm_res); - if (is_app_of(r, get_pexpr_subst_name())) { - return r; // HACK - } else { - return mk_as_is(r); - } - } catch (exception & ex) { - if (!p.has_error_recovery()) throw; - p.mk_message(ERROR).set_exception(ex).report(); - return p.mk_sorry(p.pos(), true); - } -} - -struct vm_decl_attributes : public vm_external { - decl_attributes m_val; - vm_decl_attributes(decl_attributes const & v):m_val(v) {} - virtual ~vm_decl_attributes() {} - virtual void dealloc() override { delete this; } - virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_decl_attributes(m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new vm_decl_attributes(m_val); } -}; - -static decl_attributes const & to_decl_attributes(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(to_external(o))->m_val; -} - -static vm_obj to_obj(decl_attributes const & n) { - return mk_vm_external(new vm_decl_attributes(n)); -} - -static vm_obj to_obj(decl_modifiers const & mods) { - return mk_vm_constructor(0, { - mk_vm_bool(mods.m_is_private), - mk_vm_bool(mods.m_is_protected), - mk_vm_bool(mods.m_is_meta), - mk_vm_bool(mods.m_is_mutual), - mk_vm_bool(mods.m_is_noncomputable), - }); -} - -vm_obj to_obj(cmd_meta const & meta) { - return mk_vm_constructor(0, { - to_obj(meta.m_attrs), - to_obj(meta.m_modifiers), - to_obj(meta.m_doc_string) - }); -} - -decl_modifiers to_decl_modifiers(vm_obj const & o) { - lean_always_assert(cidx(o) == 0); - decl_modifiers mods; - if (to_bool(cfield(o, 0))) { - mods.m_is_private = true; - } - if (to_bool(cfield(o, 1))) { - mods.m_is_protected = true; - } - if (to_bool(cfield(o, 2))) { - mods.m_is_meta = true; - } - if (to_bool(cfield(o, 3))) { - mods.m_is_mutual = true; - } - if (to_bool(cfield(o, 4))) { - mods.m_is_noncomputable = true; - } - return mods; -} - -cmd_meta to_cmd_meta(vm_obj const & o) { - lean_always_assert(cidx(o) == 0); - optional doc_string; - if (!is_none(cfield(o, 2))) { - doc_string = some(to_string(get_some_value(cfield(o, 2)))); - } - return {to_decl_attributes(cfield(o, 0)), to_decl_modifiers(cfield(o, 1)), doc_string}; -} - -vm_obj vm_parser_state_env(vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - return to_obj(s.m_p->env()); -} - -vm_obj vm_parser_state_options(vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - return to_obj(s.m_p->get_options()); -} - -vm_obj vm_parser_state_cur_pos(vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - return to_obj(s.m_p->pos()); -} - -vm_obj vm_parser_set_env(vm_obj const & vm_env, vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - s.m_p->set_env(to_env(vm_env)); - return lean_parser::mk_success(s); -} - -vm_obj vm_parser_ident(vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - TRY; - auto _ = s.m_p->no_error_recovery_scope(); - name ident = s.m_p->check_id_next("identifier expected"); - return lean_parser::mk_success(to_obj(ident), s); - CATCH; -} - -vm_obj vm_parser_small_nat(vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - TRY; - auto _ = s.m_p->no_error_recovery_scope(); - unsigned n = s.m_p->parse_small_nat(); - return lean_parser::mk_success(mk_vm_nat(n), s); - CATCH; -} - -vm_obj vm_parser_tk(vm_obj const & vm_tk, vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - TRY; - name tk = to_string(vm_tk); - if (!s.m_p->curr_is_token(tk)) - throw parser_error(sstream() << "'" << tk << "' expected", s.m_p->pos()); - s.m_p->next(); - return lean_parser::mk_success(s); - CATCH; -} - -vm_obj vm_parser_pexpr(vm_obj const & vm_rbp, vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - TRY; - /* The macro used to encode pattern matching and recursive equations - currently stores whether it is meta or not. - This information is retrieved from a thread local object. - In tactic blocks, we allow untrusted code even if the surrounding declaration is non meta. - We use the auxiliary class `meta_definition_scope` to temporarily update the thread local object. - A quoted expression occurring in a tactic should use the original flag. - The auxiliary class `restore_decl_meta_scope` is used to restore it. - - Remark: I realize this is hackish, but it addresses the issue raised at #1890. - */ - restore_decl_meta_scope scope; - auto rbp = to_unsigned(vm_rbp); - if (auto e = s.m_p->maybe_parse_expr(rbp)) { - return lean_parser::mk_success(to_obj(*e), s); - } else { - throw parser_error(sstream() << "expression expected", s.m_p->pos()); - } - CATCH; -} - -vm_obj vm_parser_skip_info(vm_obj const &, vm_obj const & vm_p, vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - return s.m_p->without_break_at_pos([&]() { - return invoke(vm_p, o); - }); -} - -vm_obj vm_parser_set_goal_info_pos(vm_obj const &, vm_obj const & vm_p, vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - auto pos = s.m_p->pos(); - try { - return invoke(vm_p, o); - } catch (break_at_pos_exception & ex) { - ex.report_goal_pos(pos); - throw; - } -} - -vm_obj vm_parser_with_input(vm_obj const &, vm_obj const & vm_p, vm_obj const & vm_input, vm_obj const & o) { - auto const & s = lean_parser::to_state(o); - std::string input = to_string(vm_input); - std::istringstream strm(input); - vm_obj vm_state; pos_info pos; - auto _ = s.m_p->no_error_recovery_scope(); - TRY; - std::tie(vm_state, pos) = s.m_p->with_input(strm, [&]() { - return invoke(vm_p, o); - }); - CATCH; - - if (lean_parser::is_result_exception(vm_state)) { - return vm_state; - } - auto vm_res = lean_parser::get_success_value(vm_state); - - // figure out remaining string from end position - pos_info pos2 = {1, 0}; - unsigned spos = 0; - while (pos2 < pos) { - lean_assert(spos < input.size()); - if (input[spos] == '\n') { - pos2.first++; - pos2.second = 0; - } else { - pos2.second++; - } - spos += get_utf8_size(input[spos]); - } - - vm_res = mk_vm_pair(vm_res, to_obj(input.substr(spos))); - return lean_parser::mk_success(vm_res, lean_parser::get_success_state(vm_state)); -} -static vm_obj vm_parser_command_like(vm_obj const & vm_s) { - auto s = lean_parser::to_state(vm_s); - TRY; - s.m_p->parse_command_like(); - return lean_parser::mk_success(s); - CATCH; -} - - -static vm_obj interactive_decl_attributes_apply(vm_obj const & vm_attrs, vm_obj const & vm_n, vm_obj const & vm_s) { - auto s = lean_parser::to_state(vm_s); - TRY; - auto env = to_decl_attributes(vm_attrs).apply(s.m_p->env(), get_dummy_ios(), to_name(vm_n)); - s.m_p->set_env(env); - return lean_parser::mk_success({s.m_p}); - CATCH; -} - -static vm_obj interactive_parse_binders(vm_obj const & vm_rbp, vm_obj const & vm_s) { - auto s = lean_parser::to_state(vm_s); - TRY; - buffer binders; - s.m_p->parse_binders(binders, to_unsigned(vm_rbp)); - return lean_parser::mk_success(to_obj(binders), s); - CATCH; -} - -static vm_obj vm_parser_of_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & vm_s) { - auto s = lean_parser::to_state(vm_s); - tactic_state ts = mk_tactic_state_for(s.m_p->env(), s.m_p->get_options(), name("_parser_of_tactic"), - metavar_context(), local_context(), mk_true()); - try { - vm_obj r = invoke(tac, to_obj(ts)); - if (tactic::is_result_success(r)) { - vm_obj a = tactic::get_success_value(r); - tactic_state new_ts = tactic::to_state(tactic::get_success_state(r)); - s.m_p->set_env(new_ts.env()); - return lean_parser::mk_success(a, s); - } else { - /* Remark: the following command relies on the fact that - `tactic` and `parser` are both implemented using interaction_monad */ - return lean_parser::update_exception_state(r, s); - } - } catch (exception & ex) { - return lean_parser::mk_exception(std::current_exception(), s); - } -} - -void initialize_vm_parser() { - DECLARE_VM_BUILTIN(name({"lean3", "parser_state", "env"}), vm_parser_state_env); - DECLARE_VM_BUILTIN(name({"lean3", "parser_state", "options"}), vm_parser_state_options); - DECLARE_VM_BUILTIN(name({"lean3", "parser_state", "cur_pos"}), vm_parser_state_cur_pos); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "ident"}), vm_parser_ident); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "command_like"}), vm_parser_command_like); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "small_nat"}), vm_parser_small_nat); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "set_env"}), vm_parser_set_env); - DECLARE_VM_BUILTIN(get_lean3_parser_tk_name(), vm_parser_tk); - DECLARE_VM_BUILTIN(get_lean3_parser_pexpr_name(), vm_parser_pexpr); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "skip_info"}), vm_parser_skip_info); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "set_goal_info_pos"}), vm_parser_set_goal_info_pos); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "with_input"}), vm_parser_with_input); - DECLARE_VM_BUILTIN(name({"lean3", "parser", "of_tactic"}), vm_parser_of_tactic); - DECLARE_VM_BUILTIN(name({"interactive", "decl_attributes", "apply"}), interactive_decl_attributes_apply); - DECLARE_VM_BUILTIN(name({"interactive", "parse_binders"}), interactive_parse_binders); -} - -void finalize_vm_parser() { -} - -} diff --git a/src/library/vm/vm_parser.h b/src/library/vm/vm_parser.h deleted file mode 100644 index e7da1f8a46..0000000000 --- a/src/library/vm/vm_parser.h +++ /dev/null @@ -1,20 +0,0 @@ -/* -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Sebastian Ullrich -*/ -#pragma once -#include "library/vm/vm.h" -#include "frontends/lean/parser.h" - -namespace lean { -vm_obj run_parser(parser & p, expr const & spec, buffer const & args = {}); -expr parse_interactive_param(parser & p, expr const & param_ty); - -vm_obj to_obj(cmd_meta const & meta); - -void initialize_vm_parser(); -void finalize_vm_parser(); -} -