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

chore(*): remove more stuff

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-23 15:27:12 -07:00
parent c21555240a
commit 17ae59b5b0
16 changed files with 6 additions and 951 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/meta/default.lean
View file

@ -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

116
library/init/meta/environment.lean
View file

@ -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⟩

2
library/init/meta/interaction_monad.lean
View file

@ -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

3
library/init/meta/tactic.lean
View file

@ -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.

2
src/frontends/lean/CMakeLists.txt
View file

@ -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)

3
src/frontends/lean/init_module.cpp
View file

@ -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();

125
src/frontends/lean/user_notation.cpp
View file

@ -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<modification const> deserialize(deserializer & d) {
return std::make_shared<user_notation_modification>(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<user_notation_modification>(d));
} else {
return add_user_notation(env, d, prio, persistent);
}
}));
}
void finalize_user_notation() {
user_notation_modification::finalize();
}
}

12
src/frontends/lean/user_notation.h
View file

@ -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();
}

13
src/library/tactic/tactic_state.cpp
View file

@ -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<unsigned>(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<name> 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);

4
src/library/vm/CMakeLists.txt
View file

@ -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)

6
src/library/vm/init_module.cpp
View file

@ -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();

1
src/library/vm/interaction_state_imp.h
View file

@ -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"

288
src/library/vm/vm_environment.cpp
View file

@ -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 <string>
#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<vm_environment*>(to_external(o));
}
environment const & to_env(vm_obj const & o) {
lean_vm_check(dynamic_cast<vm_environment*>(to_external(o)));
return static_cast<vm_environment*>(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<inductive::intro_rule> to_list_intro_rule(vm_obj const & cnstrs) {
if (is_simple(cnstrs))
return list<inductive::intro_rule>();
else
return list<inductive::intro_rule>(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<bool>(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<bool>(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<bool>(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<bool>(is_recursive_datatype(to_env(env), to_name(n))));
}
vm_obj environment_constructors_of(vm_obj const & env, vm_obj const & n) {
buffer<name> 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<bool>(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<name> 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<name> 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<name> 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<std::string> 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_info> 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() {
}
}

17
src/library/vm/vm_environment.h
View file

@ -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();
}

342
src/library/vm/vm_parser.cpp
View file

@ -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 <string>
#include <iostream>
#include <vector>
#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<lean_parser_state>;
typedef interaction_monad<lean_parser_state> 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<vm_obj> 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<expr> 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<vm_decl_attributes*>(to_external(o)));
return static_cast<vm_decl_attributes*>(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<std::string> 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<vm_obj>([&]() {
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<vm_obj>(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<expr> 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() {
}
}

20
src/library/vm/vm_parser.h
View file

@ -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<vm_obj> 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();
}