chore(checker): remove leanchecker
This commit is contained in:
Leonardo de Moura
parent
2a79da1ab6
commit
45da5872e6
8 changed files with 0 additions and 715 deletions
|
|
@ -399,7 +399,6 @@ add_subdirectory(kernel)
|
|||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:kernel>)
|
||||
add_subdirectory(kernel/inductive)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:inductive>)
|
||||
add_subdirectory(checker)
|
||||
add_subdirectory(library)
|
||||
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
|
||||
add_subdirectory(library/tactic)
|
||||
|
|
|
|||
|
|
@ -1,5 +0,0 @@
|
|||
add_executable(leanchecker checker.cpp text_import.cpp simple_pp.cpp
|
||||
$<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime> $<TARGET_OBJECTS:sexpr>
|
||||
$<TARGET_OBJECTS:kernel> $<TARGET_OBJECTS:inductive>)
|
||||
target_link_libraries(leanchecker ${EXTRA_LIBS})
|
||||
install(TARGETS leanchecker DESTINATION bin)
|
||||
|
|
@ -1,138 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Gabriel Ebner
|
||||
*/
|
||||
#include <fstream>
|
||||
#include "runtime/sstream.h"
|
||||
#include "util/init_module.h"
|
||||
#include "util/test.h"
|
||||
#include "util/sexpr/init_module.h"
|
||||
#include "kernel/init_module.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "kernel/standard_kernel.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
#include "library/formatter.h"
|
||||
#include "checker/text_import.h"
|
||||
#include "checker/simple_pp.h"
|
||||
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
#include <emscripten.h>
|
||||
#endif
|
||||
|
||||
using namespace lean; // NOLINT
|
||||
|
||||
struct checker_print_fn {
|
||||
std::ostream & m_out;
|
||||
environment m_env;
|
||||
lowlevel_notations m_notations;
|
||||
std::unordered_set<name, name_hash> m_already_printed;
|
||||
|
||||
checker_print_fn(std::ostream & out, environment const & env, lowlevel_notations const & nots) :
|
||||
m_out(out), m_env(env), m_notations(nots) {}
|
||||
|
||||
format pp(expr const & e) {
|
||||
return simple_pp(m_env, e, m_notations);
|
||||
}
|
||||
|
||||
void print_decl(declaration const & d) {
|
||||
format fn = compose_many({simple_pp(d.get_name()), space(), format(":"), space(), pp(d.get_type())});
|
||||
|
||||
if (d.is_definition() && !d.is_theorem()) {
|
||||
m_out << compose_many({format("def"), space(), fn, space(), format(":="), line(), pp(d.get_value()), line()});
|
||||
} else {
|
||||
format cmd(d.is_theorem() ? "theorem" : (d.is_axiom() ? "axiom" : "constant"));
|
||||
m_out << compose_many({cmd, space(), fn, line()});
|
||||
}
|
||||
}
|
||||
|
||||
void print_axioms(declaration const & decl) {
|
||||
print_axioms(decl.get_type());
|
||||
if (decl.is_definition()) print_axioms(decl.get_value());
|
||||
}
|
||||
|
||||
void print_axioms(expr const & ex) {
|
||||
for_each(ex, [&] (expr const & e, unsigned) {
|
||||
if (is_constant(e) && !m_already_printed.count(const_name(e))) {
|
||||
auto decl = m_env.get(const_name(e));
|
||||
m_already_printed.insert(decl.get_name());
|
||||
print_axioms(decl);
|
||||
if (decl.is_constant_assumption() && !m_env.is_builtin(decl.get_name()))
|
||||
print_decl(decl);
|
||||
}
|
||||
return true;
|
||||
});
|
||||
}
|
||||
|
||||
void handle_cmdline_args(buffer<name> const & ns) {
|
||||
for (auto & n : ns) print_axioms(m_env.get(n));
|
||||
for (auto & n : ns) print_decl(m_env.get(n));
|
||||
}
|
||||
};
|
||||
|
||||
int main(int argc, char ** argv) {
|
||||
#if defined(LEAN_EMSCRIPTEN)
|
||||
EM_ASM(
|
||||
try {
|
||||
// emscripten cannot mount all of / in the vfs,
|
||||
// we can only mount subdirectories...
|
||||
FS.mount(NODEFS, { root: '/home' }, '/home');
|
||||
FS.mkdir('/root');
|
||||
FS.mount(NODEFS, { root: '/root' }, '/root');
|
||||
|
||||
FS.chdir(process.cwd());
|
||||
} catch (e) {
|
||||
console.log(e);
|
||||
});
|
||||
#endif
|
||||
|
||||
if (argc < 2) {
|
||||
std::cout << "usage: leanchecker export.out lemma_to_print" << std::endl;
|
||||
return 1;
|
||||
}
|
||||
|
||||
struct initer {
|
||||
initer() {
|
||||
save_stack_info();
|
||||
initialize_util_module();
|
||||
initialize_sexpr_module();
|
||||
initialize_kernel_module();
|
||||
initialize_inductive_module();
|
||||
}
|
||||
~initer() {
|
||||
finalize_inductive_module();
|
||||
finalize_kernel_module();
|
||||
finalize_sexpr_module();
|
||||
finalize_util_module();
|
||||
}
|
||||
} initer;
|
||||
|
||||
try {
|
||||
std::ifstream in(argv[1]);
|
||||
if (!in) throw exception(sstream() << "file not found: " << argv[1]);
|
||||
|
||||
unsigned trust_lvl = 0;
|
||||
auto env = mk_environment(trust_lvl);
|
||||
lowlevel_notations notations;
|
||||
import_from_text(in, env, notations);
|
||||
|
||||
buffer<name> to_print;
|
||||
for (int i = 2; i < argc; i++)
|
||||
to_print.push_back(string_to_name(argv[i]));
|
||||
|
||||
checker_print_fn(std::cout, env, notations).handle_cmdline_args(to_print);
|
||||
|
||||
unsigned num_decls = 0;
|
||||
env.for_each_declaration([&] (declaration const &) { num_decls++; });
|
||||
std::cout << "checked " << num_decls << " declarations" << std::endl;
|
||||
|
||||
return 0;
|
||||
} catch (throwable & ex) {
|
||||
std::cerr << ex.what() << std::endl;
|
||||
return 1;
|
||||
} catch (std::exception & ex) {
|
||||
std::cerr << ex.what() << std::endl;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,311 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Gabriel Ebner
|
||||
*/
|
||||
#include "checker/simple_pp.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/old_type_checker.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
format compose_many(std::initializer_list<format> const & fmts) {
|
||||
format res;
|
||||
bool first = true;
|
||||
for (auto & fmt : fmts) {
|
||||
if (first) {
|
||||
res = fmt;
|
||||
first = false;
|
||||
} else {
|
||||
res = compose(res, fmt);
|
||||
}
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
static format pp_name(name n) {
|
||||
bool last = true;
|
||||
format fmt;
|
||||
while (n) {
|
||||
auto limb = n.is_numeral() ? format(n.get_numeral()) : format(n.get_string());
|
||||
fmt = last ? limb : compose_many({limb, format("."), fmt});
|
||||
last = false;
|
||||
n = n.get_prefix();
|
||||
}
|
||||
return last ? format("[anonymous]") : fmt;
|
||||
}
|
||||
|
||||
struct simple_pp_fn {
|
||||
old_type_checker m_tc;
|
||||
lowlevel_notations m_notations;
|
||||
unsigned m_indent = 0;
|
||||
|
||||
simple_pp_fn(environment const & env, lowlevel_notations const & notations) :
|
||||
m_tc(env), m_notations(notations) {}
|
||||
|
||||
static constexpr unsigned MAX_PRIO = 1024;
|
||||
struct result {
|
||||
format m_fmt;
|
||||
unsigned m_prio;
|
||||
|
||||
result(format const & fmt, unsigned prio) : m_fmt(fmt), m_prio(prio) {}
|
||||
result(format const & fmt) : m_fmt(fmt), m_prio(MAX_PRIO) {}
|
||||
|
||||
result maybe_paren() const { return maybe_paren(MAX_PRIO); }
|
||||
result maybe_paren(unsigned new_prio) const {
|
||||
if (m_prio < new_prio) {
|
||||
return paren(m_fmt);
|
||||
} else {
|
||||
return *this;
|
||||
}
|
||||
}
|
||||
|
||||
operator format() const { return m_fmt; }
|
||||
};
|
||||
|
||||
result pp_meta(name const & n) {
|
||||
return compose(format("?"), pp_name(n));
|
||||
}
|
||||
|
||||
result pp_level(level const & l) {
|
||||
switch (l.kind()) {
|
||||
case level_kind::Zero: return format("0");
|
||||
case level_kind::Succ: return result(compose(pp_level(succ_of(l)).maybe_paren(1), format("+1")), 0);
|
||||
case level_kind::Max:
|
||||
return result(compose_many({format("max"), space(),
|
||||
pp_level(max_lhs(l)).maybe_paren(1),
|
||||
pp_level(max_rhs(l)).maybe_paren(1)}), 0);
|
||||
case level_kind::IMax:
|
||||
return result(compose_many({format("imax"), space(),
|
||||
pp_level(imax_lhs(l)).maybe_paren(1),
|
||||
pp_level(imax_rhs(l)).maybe_paren(1)}), 0);
|
||||
case level_kind::Param: return pp_name(param_id(l));
|
||||
case level_kind::Meta: return pp_meta(meta_id(l));
|
||||
}
|
||||
lean_unreachable();
|
||||
}
|
||||
|
||||
result pp_var(expr const & e) {
|
||||
return compose(format("#"), format(var_idx(e)));
|
||||
}
|
||||
|
||||
result pp_sort(expr const & e) {
|
||||
if (sort_level(e) == mk_level_zero()) {
|
||||
return format("Prop");
|
||||
} else if (sort_level(e) == mk_level_one()) {
|
||||
return format("Type");
|
||||
} else if (is_succ(sort_level(e))) {
|
||||
return compose_many({format("Type"), space(), pp_level(succ_of(sort_level(e))).maybe_paren()});
|
||||
} else {
|
||||
return compose_many({format("Sort"), space(), pp_level(sort_level(e)).maybe_paren()});
|
||||
}
|
||||
}
|
||||
|
||||
result pp_const(expr const & e) {
|
||||
return pp_name(const_name(e));
|
||||
}
|
||||
|
||||
result pp_meta(expr const & e) {
|
||||
return pp_meta(mlocal_name(e));
|
||||
}
|
||||
|
||||
result pp_local(expr const & e) {
|
||||
return pp_name(mlocal_pp_name(e));
|
||||
}
|
||||
|
||||
bool is_implicit(expr const & f) {
|
||||
if (!closed(f)) {
|
||||
// the Lean type checker assumes expressions are closed.
|
||||
return false;
|
||||
}
|
||||
try {
|
||||
expr t = m_tc.relaxed_whnf(m_tc.infer(f));
|
||||
if (is_pi(t)) {
|
||||
binder_info bi = binding_info(t);
|
||||
return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit();
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
} catch (exception &) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
expr get_explicit_args(expr e, buffer<expr> & args) {
|
||||
while (is_app(e)) {
|
||||
if (!is_implicit(app_fn(e))) {
|
||||
args.push_back(app_arg(e));
|
||||
}
|
||||
e = app_fn(e);
|
||||
}
|
||||
std::reverse(args.begin(), args.end());
|
||||
return e;
|
||||
}
|
||||
|
||||
result pp_app(expr const & e) {
|
||||
buffer<expr> args;
|
||||
auto fn = get_explicit_args(e, args);
|
||||
|
||||
if (is_constant(fn)) {
|
||||
auto it = m_notations.find(const_name(fn));
|
||||
if (it != m_notations.end()) {
|
||||
format fmt;
|
||||
auto prec = it->second.m_prec;
|
||||
if (it->second.m_kind == lowlevel_notation_kind::Postfix && args.size() == 1) {
|
||||
fmt = compose_many({pp(args[0]).maybe_paren(prec), format(it->second.m_token)});
|
||||
}
|
||||
if (it->second.m_kind == lowlevel_notation_kind::Prefix && args.size() == 1) {
|
||||
fmt = compose_many({format(it->second.m_token), pp(args[0]).maybe_paren(prec)});
|
||||
}
|
||||
if (it->second.m_kind == lowlevel_notation_kind::Infix && args.size() == 2) {
|
||||
fmt = compose_many({pp(args[0]).maybe_paren(prec),
|
||||
format(it->second.m_token),
|
||||
pp(args[1]).maybe_paren(prec)});
|
||||
}
|
||||
if (!fmt.is_nil_fmt())
|
||||
return result(group(fmt), it->second.m_prec-1);
|
||||
}
|
||||
}
|
||||
|
||||
format fmt = pp(fn).maybe_paren();
|
||||
for (auto & arg : args) {
|
||||
fmt = compose_many({fmt, space(), pp(arg).maybe_paren()});
|
||||
}
|
||||
return result(group(fmt), MAX_PRIO-1);
|
||||
}
|
||||
|
||||
std::unordered_set<name, name_hash> used_names;
|
||||
name get_unused(name n) {
|
||||
if (!used_names.count(n)) return n;
|
||||
|
||||
n = n.get_subscript_base();
|
||||
for (unsigned i = 1;; i++) {
|
||||
auto n_i = n.append_after(i);
|
||||
if (!used_names.count(n_i))
|
||||
return n_i;
|
||||
}
|
||||
}
|
||||
|
||||
struct local_const {
|
||||
simple_pp_fn * m_fn;
|
||||
name m_pp_name;
|
||||
expr m_lc;
|
||||
|
||||
local_const(simple_pp_fn * fn, name pp_name, expr const & domain, binder_info const & bi) : m_fn(fn) {
|
||||
m_pp_name = m_fn->get_unused(pp_name);
|
||||
m_fn->used_names.insert(m_pp_name);
|
||||
m_lc = mk_local(m_pp_name, m_pp_name, domain, bi);
|
||||
m_fn->m_tc.push_local(m_pp_name, domain, bi);
|
||||
}
|
||||
~local_const() {
|
||||
m_fn->used_names.erase(m_pp_name);
|
||||
m_fn->m_tc.pop_local();
|
||||
}
|
||||
|
||||
expr const & domain() const { return mlocal_type(m_lc); }
|
||||
|
||||
local_const(simple_pp_fn * fn, expr const & binder) :
|
||||
local_const(fn, binding_name(binder), binding_domain(binder), binding_info(binder)) {}
|
||||
};
|
||||
|
||||
void mark_used_const_names(expr const & e) {
|
||||
for_each(e, [&] (expr const & c, unsigned) {
|
||||
if (is_constant(c))
|
||||
used_names.insert(const_name(c));
|
||||
return true;
|
||||
});
|
||||
}
|
||||
|
||||
format wrap_binder(std::initializer_list<format> const & fmts, binder_info const & bi) {
|
||||
auto fmt = compose_many(fmts);
|
||||
if (bi.is_implicit()) {
|
||||
return compose_many({format("{"), fmt, format("}")});
|
||||
} else if (bi.is_strict_implicit()) {
|
||||
return compose_many({format("{{"), fmt, format("}}")});
|
||||
} else if (bi.is_inst_implicit()) {
|
||||
return compose_many({format("["), fmt, format("]")});
|
||||
} else {
|
||||
return fmt;
|
||||
}
|
||||
}
|
||||
|
||||
result pp_lambda(expr const & e) {
|
||||
local_const lc(this, e);
|
||||
return result(group(compose_many({format("λ"), space(),
|
||||
wrap_binder({pp(lc.m_lc), space(), format(":"), space(),
|
||||
pp(binding_domain(e)).maybe_paren(1)}, binding_info(e)),
|
||||
format(","), space(), pp(instantiate(binding_body(e), lc.m_lc))})), 0);
|
||||
}
|
||||
|
||||
result pp_pi(expr e) {
|
||||
if (!has_free_vars(binding_body(e))) {
|
||||
// implication
|
||||
return result(group(compose_many({pp(binding_domain(e)).maybe_paren(25), space(), format("->"),
|
||||
space(), pp(binding_body(e)).maybe_paren(24)})), 24);
|
||||
} else {
|
||||
auto bi = binding_info(e);
|
||||
auto ty = binding_domain(e);
|
||||
|
||||
buffer<local_const> lcs;
|
||||
do {
|
||||
lcs.emplace_back(this, e);
|
||||
e = instantiate(binding_body(e), lcs.back().m_lc);
|
||||
} while (is_pi(e) && has_free_vars(binding_body(e)) &&
|
||||
binding_info(e) == bi &&
|
||||
m_tc.is_def_eq(binding_domain(e), ty));
|
||||
|
||||
format bound_vars;
|
||||
for (auto & lc : lcs) {
|
||||
if (!bound_vars.is_nil_fmt()) bound_vars = compose(bound_vars, space());
|
||||
bound_vars = compose_many({bound_vars, pp_name(lc.m_pp_name)});
|
||||
}
|
||||
|
||||
auto fmt = compose_many({format("Π"), space(),
|
||||
wrap_binder({bound_vars, space(), format(":"), space(),
|
||||
pp(ty).maybe_paren(1)}, bi),
|
||||
format(","), space(), pp(e)});
|
||||
return result(group(fmt), 0);
|
||||
}
|
||||
}
|
||||
|
||||
result pp_macro(expr const &) {
|
||||
return format("[macro]");
|
||||
}
|
||||
|
||||
result pp_let(expr const & e) {
|
||||
local_const lc(this, let_name(e), let_type(e), binder_info());
|
||||
return result(group(compose_many({format("let"), space(), pp(lc.m_lc), space(), format(":"), space(),
|
||||
pp(let_type(e)).maybe_paren(1), space(), format(":="), space(), pp(let_value(e)), format(","),
|
||||
space(), pp(instantiate(let_body(e), lc.m_lc))})), 0);
|
||||
}
|
||||
|
||||
result pp(expr const & e) {
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Var: return pp_var(e);
|
||||
case expr_kind::Sort: return pp_sort(e);
|
||||
case expr_kind::Constant: return pp_const(e);
|
||||
case expr_kind::Meta: return pp_meta(e);
|
||||
case expr_kind::Local: return pp_local(e);
|
||||
case expr_kind::App: return pp_app(e);
|
||||
case expr_kind::Lambda: return pp_lambda(e);
|
||||
case expr_kind::Pi: return pp_pi(e);
|
||||
case expr_kind::Macro: return pp_macro(e);
|
||||
case expr_kind::Let: return pp_let(e);
|
||||
}
|
||||
lean_unreachable();
|
||||
}
|
||||
};
|
||||
|
||||
format simple_pp(name const & n) {
|
||||
return pp_name(n);
|
||||
}
|
||||
|
||||
format simple_pp(environment const & env, expr const & e, lowlevel_notations const & notations) {
|
||||
simple_pp_fn fn(env, notations);
|
||||
fn.mark_used_const_names(e);
|
||||
return fn.pp(e);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Gabriel Ebner
|
||||
*/
|
||||
#pragma once
|
||||
#include "kernel/environment.h"
|
||||
#include "checker/text_import.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
format compose_many(std::initializer_list<format> const & fmts);
|
||||
|
||||
format simple_pp(name const & n);
|
||||
format simple_pp(environment const & env, expr const & e, lowlevel_notations const & notations);
|
||||
|
||||
}
|
||||
|
|
@ -1,208 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Gabriel Ebner
|
||||
*/
|
||||
#include <string>
|
||||
#include <iostream>
|
||||
#include <unordered_map>
|
||||
#include "runtime/sstream.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "kernel/old_type_checker.h"
|
||||
#include "kernel/quot.h"
|
||||
#include "checker/text_import.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
struct text_importer {
|
||||
std::unordered_map<unsigned, expr> m_expr;
|
||||
std::unordered_map<unsigned, name> m_name;
|
||||
std::unordered_map<unsigned, level> m_level;
|
||||
|
||||
lowlevel_notations m_notations;
|
||||
|
||||
environment m_env;
|
||||
|
||||
text_importer(environment const & env) : m_env(env) {
|
||||
m_level[0] = {};
|
||||
m_name[0] = {};
|
||||
}
|
||||
|
||||
levels read_levels(std::istream & in) {
|
||||
unsigned idx;
|
||||
buffer<level> ls;
|
||||
while (in >> idx) {
|
||||
ls.push_back(m_level.at(idx));
|
||||
}
|
||||
return levels(ls);
|
||||
}
|
||||
|
||||
level_param_names read_level_params(std::istream & in) {
|
||||
unsigned idx;
|
||||
buffer<name> ls;
|
||||
while (in >> idx) {
|
||||
ls.push_back(m_name.at(idx));
|
||||
}
|
||||
return names(ls);
|
||||
}
|
||||
|
||||
void handle_ind(std::istream & in) {
|
||||
unsigned num_params, name_idx, type_idx, num_intros;
|
||||
in >> num_params >> name_idx >> type_idx >> num_intros;
|
||||
|
||||
buffer<inductive::intro_rule> intros;
|
||||
for (unsigned i = 0; i < num_intros; i++) {
|
||||
unsigned name_idx, type_idx; in >> name_idx >> type_idx;
|
||||
intros.push_back(inductive::mk_intro_rule(m_name.at(name_idx), m_expr.at(type_idx)));
|
||||
}
|
||||
|
||||
auto ls = read_level_params(in);
|
||||
|
||||
inductive::inductive_decl decl(m_name.at(name_idx), ls, num_params, m_expr.at(type_idx), to_list(intros));
|
||||
m_env = inductive::add_inductive(m_env, decl, false).first;
|
||||
}
|
||||
|
||||
void handle_def(std::istream & in) {
|
||||
unsigned name_idx, type_idx, val_idx;
|
||||
in >> name_idx >> type_idx >> val_idx;
|
||||
auto ls = read_level_params(in);
|
||||
|
||||
auto decl =
|
||||
old_type_checker(m_env).is_prop(m_expr.at(type_idx)) ?
|
||||
mk_theorem(m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx)) :
|
||||
mk_definition(m_env, m_name.at(name_idx), ls, m_expr.at(type_idx), m_expr.at(val_idx), true, false);
|
||||
|
||||
m_env = m_env.add(check(m_env, decl));
|
||||
}
|
||||
|
||||
void handle_ax(std::istream & in) {
|
||||
unsigned name_idx, type_idx;
|
||||
in >> name_idx >> type_idx;
|
||||
auto ls = read_level_params(in);
|
||||
m_env = m_env.add(check(m_env, mk_axiom(m_name.at(name_idx), ls, m_expr.at(type_idx))));
|
||||
}
|
||||
|
||||
void handle_notation(std::istream & in, lowlevel_notation_kind kind) {
|
||||
unsigned name_idx, prec;
|
||||
in >> name_idx >> prec;
|
||||
|
||||
std::string token;
|
||||
std::getline(in, token);
|
||||
if (!token.empty() && token.front())
|
||||
token.erase(token.begin());
|
||||
if (!token.empty() && token.back() == '\n')
|
||||
token.erase(token.end() - 1);
|
||||
|
||||
m_notations[m_name.at(name_idx)] = { kind, token, prec };
|
||||
}
|
||||
|
||||
binder_info read_binder_info(std::string const & tok) {
|
||||
if (tok == "#BI") {
|
||||
return mk_implicit_binder_info();
|
||||
} else if (tok == "#BS") {
|
||||
return mk_strict_implicit_binder_info();
|
||||
} else if (tok == "#BC") {
|
||||
return mk_inst_implicit_binder_info();
|
||||
} else if (tok == "#BD") {
|
||||
return {};
|
||||
} else {
|
||||
throw exception(sstream() << "unknown binder info: " << tok);
|
||||
}
|
||||
}
|
||||
|
||||
void handle_line(std::string const & line) {
|
||||
std::istringstream in(line);
|
||||
|
||||
unsigned idx;
|
||||
std::string cmd;
|
||||
in >> cmd;
|
||||
if (cmd == "#IND") {
|
||||
handle_ind(in);
|
||||
} else if (cmd == "#DEF") {
|
||||
handle_def(in);
|
||||
} else if (cmd == "#AX") {
|
||||
handle_ax(in);
|
||||
} else if (cmd == "#QUOT") {
|
||||
m_env = m_env.add_quot();
|
||||
} else if (cmd == "#PREFIX") {
|
||||
handle_notation(in, lowlevel_notation_kind::Prefix);
|
||||
} else if (cmd == "#POSTFIX") {
|
||||
handle_notation(in, lowlevel_notation_kind::Postfix);
|
||||
} else if (cmd == "#INFIX") {
|
||||
handle_notation(in, lowlevel_notation_kind::Infix);
|
||||
} else if (std::istringstream(cmd) >> idx) {
|
||||
std::string kind;
|
||||
in >> kind;
|
||||
|
||||
if (kind == "#NS") {
|
||||
unsigned p; std::string limb; in >> p >> std::skipws >> limb;
|
||||
m_name[idx] = name(m_name.at(p), limb.c_str());
|
||||
} else if (kind == "#NI") {
|
||||
unsigned p, limb; in >> p >> limb;
|
||||
m_name[idx] = name(m_name.at(p), limb);
|
||||
} else if (kind == "#US") {
|
||||
unsigned l1; in >> l1;
|
||||
m_level[idx] = mk_succ(m_level.at(l1));
|
||||
} else if (kind == "#UM") {
|
||||
unsigned l1, l2; in >> l1 >> l2;
|
||||
m_level[idx] = mk_max(m_level.at(l1), m_level.at(l2));
|
||||
} else if (kind == "#UIM") {
|
||||
unsigned l1, l2; in >> l1 >> l2;
|
||||
m_level[idx] = mk_imax(m_level.at(l1), m_level.at(l2));
|
||||
} else if (kind == "#UP") {
|
||||
unsigned i1; in >> i1;
|
||||
m_level[idx] = mk_param_univ(m_name.at(i1));
|
||||
} else if (kind == "#EV") {
|
||||
unsigned v; in >> v;
|
||||
m_expr[idx] = mk_var(v);
|
||||
} else if (kind == "#ES") {
|
||||
unsigned l; in >> l;
|
||||
m_expr[idx] = mk_sort(m_level.at(l));
|
||||
} else if (kind == "#EC") {
|
||||
unsigned n; in >> n;
|
||||
auto ls = read_levels(in);
|
||||
m_expr[idx] = mk_constant(m_name.at(n), ls);
|
||||
} else if (kind == "#EA") {
|
||||
unsigned e1, e2; in >> e1 >> e2;
|
||||
m_expr[idx] = mk_app(m_expr.at(e1), m_expr.at(e2));
|
||||
} else if (kind == "#EZ") {
|
||||
unsigned n, t, v, b; in >> n >> t >> v >> b;
|
||||
m_expr[idx] = mk_let(m_name.at(n), m_expr.at(t), m_expr.at(v), m_expr.at(b));
|
||||
} else if (kind == "#EL") {
|
||||
unsigned n, t, e; std::string b; in >> b >> n >> t >> e;
|
||||
m_expr[idx] = mk_lambda(m_name.at(n), m_expr.at(t), m_expr.at(e), read_binder_info(b));
|
||||
} else if (kind == "#EP") {
|
||||
unsigned n, t, e; std::string b; in >> b >> n >> t >> e;
|
||||
m_expr[idx] = mk_pi(m_name.at(n), m_expr.at(t), m_expr.at(e), read_binder_info(b));
|
||||
} else {
|
||||
throw exception(sstream() << "unknown term definition kind: " << kind);
|
||||
}
|
||||
} else {
|
||||
throw exception(sstream() << "unknown command: " << cmd);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void import_from_text(std::istream & in, environment & env, lowlevel_notations & notations) {
|
||||
text_importer importer(env);
|
||||
|
||||
std::string line;
|
||||
unsigned line_num = 0;
|
||||
while (std::getline(in, line)) {
|
||||
line_num++;
|
||||
try {
|
||||
importer.handle_line(line);
|
||||
} catch (throwable & t) {
|
||||
throw exception(sstream() << "line " << line_num << ": " << t.what());
|
||||
} catch (std::exception & e) {
|
||||
throw exception(sstream() << "line " << line_num << ": " << e.what());
|
||||
}
|
||||
}
|
||||
|
||||
env = importer.m_env;
|
||||
notations = std::move(importer.m_notations);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Gabriel Ebner
|
||||
*/
|
||||
#pragma once
|
||||
#include <iostream>
|
||||
#include <unordered_map>
|
||||
#include <string>
|
||||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
enum class lowlevel_notation_kind {
|
||||
Prefix, Postfix, Infix,
|
||||
};
|
||||
struct lowlevel_notation_info {
|
||||
lowlevel_notation_kind m_kind;
|
||||
std::string m_token;
|
||||
unsigned m_prec;
|
||||
};
|
||||
|
||||
using lowlevel_notations = std::unordered_map<name, lowlevel_notation_info, name_hash>;
|
||||
|
||||
void import_from_text(std::istream & in, environment & env, lowlevel_notations & notations);
|
||||
|
||||
}
|
||||
|
|
@ -61,12 +61,6 @@ else()
|
|||
endif()
|
||||
endif()
|
||||
|
||||
add_test(NAME leanchecker
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
|
||||
COMMAND bash "${LEAN_SOURCE_DIR}/cmake/run_checker.sh" "${CMAKE_CROSSCOMPILING_EMULATOR}"
|
||||
"$<TARGET_FILE:lean>" "$<TARGET_FILE:leanchecker>" "${CMAKE_CURRENT_BINARY_DIR}/library_export.out"
|
||||
"${LEAN_SOURCE_DIR}/../library")
|
||||
|
||||
# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
|
||||
# add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
|
||||
add_test(lean_help1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --help)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue