diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ca71aa69e..7efd69f9e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -225,8 +225,8 @@ set(LEAN_LIBS ${LEAN_LIBS} library) # set(LEAN_LIBS ${LEAN_LIBS} tactic) add_subdirectory(library/error_handling) set(LEAN_LIBS ${LEAN_LIBS} error_handling) -# add_subdirectory(frontends/lean) -# set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) +add_subdirectory(frontends/lean) +set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) add_subdirectory(frontends/lua) set(LEAN_LIBS ${LEAN_LIBS} leanlua) if("${MULTI_THREAD}" MATCHES "ON") @@ -238,7 +238,7 @@ set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ft set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) add_subdirectory(shell) # add_subdirectory(builtin) -# add_subdirectory(emacs) +add_subdirectory(emacs) add_subdirectory(tests/util) add_subdirectory(tests/util/numerics) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index b7b059c5f..fd01c9118 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -1,7 +1,2 @@ -add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp - parser.cpp parser_imp.cpp parser_expr.cpp parser_error.cpp - parser_imp.cpp parser_cmds.cpp parser_level.cpp parser_tactic.cpp - parser_macros.cpp parser_calc.cpp pp.cpp frontend_elaborator.cpp - register_module.cpp environment_scope.cpp coercion.cpp shell.cpp) - +add_library(lean_frontend register_module.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/coercion.cpp b/src/frontends/lean/coercion.cpp deleted file mode 100644 index 1c76b7fa0..000000000 --- a/src/frontends/lean/coercion.cpp +++ /dev/null @@ -1,19 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/io_state_stream.h" -#include "frontends/lean/coercion.h" -#include "frontends/lean/frontend.h" - -namespace lean { -void coercion_declaration::write(serializer & s) const { - s << "Coercion" << m_coercion; -} -static void read_coercion(environment const & env, io_state const &, deserializer & d) { - add_coercion(env, read_expr(d)); -} -static object_cell::register_deserializer_fn coercion_ds("Coercion", read_coercion); -} diff --git a/src/frontends/lean/coercion.h b/src/frontends/lean/coercion.h deleted file mode 100644 index 666349d2f..000000000 --- a/src/frontends/lean/coercion.h +++ /dev/null @@ -1,24 +0,0 @@ -/* -Copyright (c) 2013 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/object.h" - -namespace lean { -/** - \brief Object for tracking coercion declarations. - This object is mainly used for recording the declaration. -*/ -class coercion_declaration : public neutral_object_cell { - expr m_coercion; -public: - coercion_declaration(expr const & c):m_coercion(c) {} - virtual ~coercion_declaration() {} - virtual char const * keyword() const { return "coercion"; } - expr const & get_coercion() const { return m_coercion; } - virtual void write(serializer & s) const; -}; -} diff --git a/src/frontends/lean/environment_scope.cpp b/src/frontends/lean/environment_scope.cpp deleted file mode 100644 index edc7f95ea..000000000 --- a/src/frontends/lean/environment_scope.cpp +++ /dev/null @@ -1,126 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/list.h" -#include "util/name_set.h" -#include "util/name_map.h" -#include "kernel/environment.h" -#include "kernel/replace_fn.h" -#include "kernel/abstract.h" -#include "library/io_state_stream.h" -#include "frontends/lean/frontend.h" - -namespace lean { -typedef std::vector dependencies; - -struct object_info { - object m_object; - unsigned m_pos; - dependencies m_deps; - expr m_ref; // a reference to this object, it can be a constant or an application containing the dependencies - object_info(object const & obj, unsigned pos, dependencies const & deps, expr const & ref):m_object(obj), m_pos(pos), m_deps(deps), m_ref(ref) {} -}; - -static expr convert(expr const & e, name_map & info_map, name_set & dep_set) { - return replace(e, [&](expr const & e, unsigned) -> expr { - if (is_constant(e)) { - auto it = info_map.find(const_name(e)); - if (it != info_map.end()) { - auto const & info = it->second; - if (info.m_object.is_axiom() || info.m_object.is_var_decl()) - dep_set.insert(const_name(e)); - for (auto const & d : info.m_deps) - dep_set.insert(d); - return info.m_ref; - } - } - return e; - }); -} - -static dependencies mk_dependencies(name_map & info_map, name_set & dep_set) { - dependencies r; - for (auto d : dep_set) r.push_back(d); - std::sort(r.begin(), r.end(), [&](name const & n1, name const & n2) { - return info_map.find(n1)->second.m_pos < info_map.find(n2)->second.m_pos; - }); - return r; -} - -static expr mk_ref(object const & obj, dependencies const & deps) { - if (obj.is_axiom() || obj.is_var_decl()) { - return mk_constant(obj.get_name()); - } else { - buffer args; - args.push_back(mk_constant(obj.get_name())); - for (auto d : deps) args.push_back(mk_constant(d)); - if (args.size() == 1) - return args[0]; - else - return mk_app(args); - } -} - -static expr abstract(bool is_lambda, expr e, name_map & info_map, dependencies const & deps) { - auto it = deps.end(); - auto begin = deps.begin(); - while (it != begin) { - --it; - expr const & type = info_map.find(*it)->second.m_object.get_type(); - if (is_lambda) - e = Fun(*it, type, e); - else - e = Pi(*it, type, e); - } - return e; -} - -static expr Pi(expr e, name_map & info_map, dependencies const & deps) { - return abstract(false, e, info_map, deps); -} - -static expr Fun(expr e, name_map & info_map, dependencies const & deps) { - return abstract(true, e, info_map, deps); -} - -std::vector export_local_objects(environment const & env) { - // TODO(Leo): Revise using Parameters - if (!env->has_parent()) - return std::vector(); - name_map info_map; - name_set dep_set; - unsigned pos = 0; - std::vector new_objects; - auto it = env->begin_local_objects(); - auto end = env->end_local_objects(); - for (; it != end; ++it) { - object const & obj = *it; - if (!obj.is_axiom() && !obj.is_var_decl() && !obj.is_theorem() && !obj.is_definition()) - continue; - if (is_explicit(env, obj.get_name())) - continue; - dep_set.clear(); - if (obj.is_axiom() || obj.is_var_decl()) { - expr new_type = convert(obj.get_type(), info_map, dep_set); - auto new_deps = mk_dependencies(info_map, dep_set); - info_map.insert(mk_pair(obj.get_name(), object_info(obj, pos, new_deps, mk_ref(obj, new_deps)))); - } else { - expr new_type = convert(obj.get_type(), info_map, dep_set); - expr new_val = convert(obj.get_value(), info_map, dep_set); - auto new_deps = mk_dependencies(info_map, dep_set); - new_type = Pi(new_type, info_map, new_deps); - new_val = Fun(new_val, info_map, new_deps); - auto new_obj = obj.is_theorem() ? mk_theorem(obj.get_name(), new_type, new_val) : mk_definition(obj.get_name(), new_type, new_val, obj.get_weight()); - new_objects.push_back(new_obj); - info_map.insert(mk_pair(obj.get_name(), object_info(new_obj, pos, new_deps, mk_ref(new_obj, new_deps)))); - } - pos++; - } - return new_objects; -} -} diff --git a/src/frontends/lean/environment_scope.h b/src/frontends/lean/environment_scope.h deleted file mode 100644 index 29793a9ab..000000000 --- a/src/frontends/lean/environment_scope.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "kernel/environment.h" -namespace lean { -std::vector export_local_objects(environment const & env); -} diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp deleted file mode 100644 index 268720063..000000000 --- a/src/frontends/lean/frontend.cpp +++ /dev/null @@ -1,669 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include "util/thread.h" -#include "util/map.h" -#include "util/sstream.h" -#include "util/exception.h" -#include "util/name_map.h" -#include "util/name_set.h" -#include "kernel/environment.h" -#include "kernel/expr_maps.h" -#include "kernel/expr_sets.h" -#include "kernel/kernel.h" -#include "kernel/io_state.h" -#include "library/io_state_stream.h" -#include "library/expr_pair.h" -#include "library/expr_pair_maps.h" -#include "library/arith/nat.h" -#include "library/arith/int.h" -#include "library/arith/real.h" -#include "frontends/lean/operator_info.h" -#include "frontends/lean/coercion.h" -#include "frontends/lean/frontend.h" -#include "frontends/lean/notation.h" -#include "frontends/lean/pp.h" - -namespace lean { -class mark_implicit_command : public neutral_object_cell { - name m_obj_name; - std::vector m_implicit; -public: - mark_implicit_command(name const & n, unsigned sz, bool const * implicit): - m_obj_name(n), m_implicit(implicit, implicit+sz) {} - virtual ~mark_implicit_command() {} - virtual char const * keyword() const { return "MarkImplicit"; } - virtual void write(serializer & s) const { - unsigned sz = m_implicit.size(); - s << "Imp" << m_obj_name << sz; - for (auto b : m_implicit) - s << b; - } -}; -static void read_mark_implicit(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - buffer implicit; - unsigned num = d.read_unsigned(); - for (unsigned i = 0; i < num; i++) - implicit.push_back(d.read_bool()); - mark_implicit_arguments(env, n, implicit.size(), implicit.data()); -} -static object_cell::register_deserializer_fn mark_implicit_ds("Imp", read_mark_implicit); - -static std::vector g_empty_vector; -/** - \brief Environment extension object for the Lean default frontend. -*/ -struct lean_extension : public environment_extension { - typedef std::pair, name> implicit_info; - // Remark: only named objects are stored in the dictionary. - typedef name_map operator_table; - typedef name_map implicit_table; - typedef name_map precedence_table; - typedef expr_struct_map> expr_to_operators; - typedef expr_pair_struct_map coercion_map; - typedef expr_struct_map> expr_to_coercions; - typedef expr_struct_set coercion_set; - typedef expr_struct_map> inv_aliases; - - operator_table m_nud; // nud table for Pratt's parser - operator_table m_led; // led table for Pratt's parser - // The following table stores the precedence of other operator parts. - // The m_nud and m_led only map the first part of an operator to its definition. - precedence_table m_other_lbp; - expr_to_operators m_expr_to_operators; // map denotations to operators (this is used for pretty printing) - implicit_table m_implicit_table; // track the number of implicit arguments for a symbol. - coercion_map m_coercion_map; // mapping from (given_type, expected_type) -> coercion - coercion_set m_coercion_set; // Set of coercions - expr_to_coercions m_type_coercions; // mapping type -> list (to-type, function) - name_set m_explicit_names; // set of explicit version of constants with implicit parameters - name_map m_aliases; - inv_aliases m_inv_aliases; // inverse map for m_aliases - - lean_extension() { - } - - lean_extension const * get_parent() const { - return environment_extension::get_parent(); - } - - /** \brief Return the nud operator for the given symbol. */ - operator_info find_nud(name const & n) const { - auto it = m_nud.find(n); - if (it != m_nud.end()) - return it->second; - lean_extension const * parent = get_parent(); - if (parent) - return parent->find_nud(n); - else - return operator_info(); - } - - /** \brief Return the led operator for the given symbol. */ - operator_info find_led(name const & n) const { - auto it = m_led.find(n); - if (it != m_led.end()) - return it->second; - lean_extension const * parent = get_parent(); - if (parent) - return parent->find_led(n); - else - return operator_info(); - } - - optional get_other_lbp(name const & n) const { - auto it = m_other_lbp.find(n); - if (it != m_other_lbp.end()) - return some(it->second); - lean_extension const * parent = get_parent(); - if (parent) - return parent->get_other_lbp(n); - else - return optional(); - } - - /** \brief Return the precedence (aka binding power) of the given name. */ - optional get_lbp(name const & n) const { - operator_info info = find_led(n); - if (info) - return some(info.get_precedence()); - else - return get_other_lbp(n); - } - - /** - \brief Return true if the given operator is defined in this - frontend object (parent frontends are ignored). - */ - bool defined_here(operator_info const & n, bool led) const { - if (led) - return m_led.find(n.get_op_name()) != m_led.end(); - else - return m_nud.find(n.get_op_name()) != m_nud.end(); - } - - /** \brief Return the led/nud operator for the given symbol. */ - operator_info find_op(name const & n, bool led) const { - return led ? find_led(n) : find_nud(n); - } - - /** \brief Insert a new led/nud operator. */ - void insert_op(operator_info const & op, bool led) { - if (led) - insert(m_led, op.get_op_name(), op); - else - insert(m_nud, op.get_op_name(), op); - } - - /** \brief Find the operator that is used as notation for the given expression. */ - operator_info find_op_for(expr const & e, bool unicode) const { - auto it = m_expr_to_operators.find(e); - if (it != m_expr_to_operators.end()) { - auto l = it->second; - for (auto op : l) { - if (unicode || op.is_safe_ascii()) - return op; - } - } - lean_extension const * parent = get_parent(); - if (parent) - return parent->find_op_for(e, unicode); - else - return operator_info(); - } - - /** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */ - void remove_bindings(operator_info const & op) { - lean_extension const * parent = get_parent(); - for (expr const & d : op.get_denotations()) { - if (parent && parent->find_op_for(d, true)) { - // parent has an association for d... we must hide it. - insert(m_expr_to_operators, d, list(operator_info())); - } else { - m_expr_to_operators.erase(d); - } - } - } - - /** \brief Add a new entry d -> op in the mapping m_expr_to_operators */ - void insert_expr_to_operator_entry(expr const & d, operator_info const & op) { - list & l = m_expr_to_operators[d]; - l = cons(op, l); - } - - void check_precedence(name const & n, unsigned prec, io_state const & ios) const { - auto old_prec = get_lbp(n); - if (old_prec && *old_prec != prec) - diagnostic(ios) << "The precedence of '" << n << "' changed from " << *old_prec << " to " << prec << ".\n"; - } - - /** \brief Register the new operator in the tables for parsing and pretty printing. */ - void register_new_op(operator_info new_op, expr const & d, bool led, io_state const & ios) { - new_op.add_expr(d); - insert_op(new_op, led); - insert_expr_to_operator_entry(d, new_op); - auto parts = new_op.get_op_name_parts(); - auto prec = new_op.get_precedence(); - if (led) - check_precedence(head(parts), prec, ios); - for (name const & part : tail(parts)) { - check_precedence(part, prec, ios); - m_other_lbp[part] = prec; - } - } - - /** - \brief Two operator (aka notation) denotations are compatible - iff after ignoring all implicit arguments in the prefix and - explicit arguments in the suffix, the remaining implicit arguments - occur in the same positions. - - Let us denote implicit arguments with a '_' and explicit with a '*'. - Then a denotation can be associated with a pattern containing one or more - '_' and '*'. - Two denotations are compatible, if we have the same pattern after - removed the '_' from the prefix and '*' from the suffix. - - Here is an example of compatible denotations - f : Int -> Int -> Int Pattern * * - g : Pi {A : Type}, A -> A -> A Pattern _ * * - h : Pi {A B : Type}, A -> B -> A Pattern _ _ * * - They are compatible, because after we remove the _ from the prefix, and * from the suffix, - all of them reduce to the empty sequence - - Here is another example of compatible denotations: - f : Pi {A : Type} (a : A) {B : Type} (b : B), A Pattern _ * _ * - g : Pi (i : Int) {T : Type} (x : T), T Pattern * _ * - They are compatible, because after we remove the _ from the prefix, and * from the suffix, - we get the same sequence: * _ - - The following two are not compatible - f : Pi {A : Type} (a : A) {B : Type} (b : B), A Pattern _ * _ * - g : Pi {A B : Type} (a : A) (b : B), A Pattern _ _ * * - - Remark: we remove the explicit suffix at mark_implicit_arguments. - */ - bool compatible_denotation(expr const & d1, expr const & d2) { - auto imp1 = get_implicit_arguments(d1); - auto imp2 = get_implicit_arguments(d2); - auto it1 = std::find(imp1.begin(), imp1.end(), false); - auto it2 = std::find(imp2.begin(), imp2.end(), false); - for (; it1 != imp1.end() && it2 != imp2.end() && *it1 == *it2; ++it1, ++it2) {} - return it1 == imp1.end() && it2 == imp2.end(); - } - - /** - \brief Return true iff the existing denotations (aka - overloads) for an operator op are compatible with the new - denotation d. - - The compatibility is only an issue if implicit arguments are - used. If one of the denotations has implicit arguments, then - all of them should have implicit arguments, and the implicit - arguments should occur in the same positions. - */ - bool compatible_denotations(operator_info const & op, expr const & d) { - return std::all_of(op.get_denotations().begin(), op.get_denotations().end(), [&](expr const & prev_d) { return compatible_denotation(prev_d, d); }); - } - - /** - \brief Add a new operator and save information as object. - - If the new operator does not conflict with existing operators, - then we just register it. - If it conflicts, there are two options: - 1) It is an overload (we just add the internal name \c n as - new option. - 2) It is a real conflict, and report the issue in the - diagnostic channel, and override the existing operator (aka notation). - */ - void add_op(operator_info new_op, expr const & d, bool led, environment const & env, io_state const & ios) { - name const & opn = new_op.get_op_name(); - operator_info old_op = find_op(opn, led); - if (!old_op) { - register_new_op(new_op, d, led, ios); - } else if (old_op == new_op) { - if (compatible_denotations(old_op, d)) { - // overload - if (defined_here(old_op, led)) { - old_op.add_expr(d); - insert_expr_to_operator_entry(d, old_op); - } else { - // we must copy the operator because it was defined in - // a parent frontend. - new_op = old_op.copy(); - register_new_op(new_op, d, led, ios); - } - } else { - diagnostic(ios) << "The denotation(s) for the existing notation:\n " << old_op - << "\nhave been replaced with the new denotation:\n " << d - << "\nbecause they conflict on how implicit arguments are used.\n"; - remove_bindings(old_op); - register_new_op(new_op, d, led, ios); - } - } else { - diagnostic(ios) << "Notation has been redefined, the existing notation:\n " << old_op - << "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n"; - remove_bindings(old_op); - register_new_op(new_op, d, led, ios); - } - env->add_neutral_object(new notation_declaration(new_op, d)); - } - - static name mk_explicit_name(name const & n) { - if (n.is_anonymous()) { - throw exception("anonymous names cannot be used in definitions"); - } else if (n.is_numeral()) { - return name(n, "explicit"); - } else { - std::string new_name = "@"; - new_name += n.get_string(); - if (n.is_atomic()) - return name(new_name); - else - return name(n.get_prefix(), new_name.c_str()); - } - } - - void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit, environment const & env) { - if (env->has_children()) - throw exception(sstream() << "failed to mark implicit arguments, frontend object is read-only"); - object const & obj = env->get_object(n); - if (obj.kind() != object_kind::Definition && obj.kind() != object_kind::Postulate && obj.kind() != object_kind::Builtin) - throw exception(sstream() << "failed to mark implicit arguments, the object '" << n << "' is not a definition or postulate"); - if (has_implicit_arguments(n)) - throw exception(sstream() << "the object '" << n << "' already has implicit argument information associated with it"); - name explicit_version = mk_explicit_name(n); - if (env->find_object(explicit_version)) - throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', the frontend already has an object named '" << explicit_version << "'"); - expr const & type = obj.get_type(); - unsigned num_args = 0; - expr it = type; - while (is_pi(it)) { num_args++; it = abst_body(it); } - if (sz > num_args) - throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', object has only " << num_args << " arguments, but trying to mark " << sz << " arguments"); - // remove explicit suffix - while (sz > 0 && !implicit[sz - 1]) sz--; - if (sz == 0) - throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', all arguments are explicit"); - std::vector v(implicit, implicit+sz); - m_implicit_table[n] = mk_pair(v, explicit_version); - expr body = mk_constant(n); - m_explicit_names.insert(explicit_version); - env->add_neutral_object(new mark_implicit_command(n, sz, implicit)); - env->auxiliary_section([&]() { - if (obj.is_axiom() || obj.is_theorem()) { - env->add_theorem(explicit_version, type, body); - } else { - env->add_definition(explicit_version, type, body); - } - }); - } - - bool has_implicit_arguments(name const & n) const { - if (m_implicit_table.find(n) != m_implicit_table.end()) - return true; - lean_extension const * parent = get_parent(); - if (parent) - return parent->has_implicit_arguments(n); - else - return false; - } - - std::vector const & get_implicit_arguments(name const & n) const { - auto it = m_implicit_table.find(n); - if (it != m_implicit_table.end()) - return it->second.first; - lean_extension const * parent = get_parent(); - if (parent) - return parent->get_implicit_arguments(n); - else - return g_empty_vector; - } - - std::vector const & get_implicit_arguments(expr const & n) const { - if (is_constant(n)) - return get_implicit_arguments(const_name(n)); - else - return g_empty_vector; - } - - name const & get_explicit_version(name const & n) const { - auto it = m_implicit_table.find(n); - if (it != m_implicit_table.end()) - return it->second.second; - lean_extension const * parent = get_parent(); - if (parent) - return parent->get_explicit_version(n); - else - return name::anonymous(); - } - - bool is_explicit(name const & n) const { - if (m_explicit_names.find(n) != m_explicit_names.end()) - return true; - lean_extension const * parent = get_parent(); - if (parent) - return parent->is_explicit(n); - else - return false; - } - - /** - \brief It is too expensive to normalize \c t when checking if there is a coercion for it. - So, we just do a 'quick' normalization following a chain of definitions. - */ - expr coercion_type_normalization(expr t, ro_environment const & env) const { - while (true) { - if (is_constant(t)) { - auto obj = env->find_object(const_name(t)); - if (obj && obj->is_definition()) { - t = obj->get_value(); - } else { - return t; - } - } else { - return t; - } - } - } - - void add_coercion(expr const & f, environment const & env) { - expr type = env->type_check(f); - expr norm_type = type; // env->normalize(type); - if (!is_arrow(norm_type)) - throw exception("invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)"); - expr from = coercion_type_normalization(abst_domain(norm_type), env); - expr to = coercion_type_normalization(abst_body(norm_type), env); - if (from == to) - throw exception("invalid coercion declaration, 'from' and 'to' types are the same"); - if (get_coercion_core(from, to)) - throw exception("invalid coercion declaration, frontend already has a coercion for the given types"); - m_coercion_map[expr_pair(from, to)] = f; - m_coercion_set.insert(f); - list l = get_coercions_core(from); - insert(m_type_coercions, from, cons(expr_pair(to, f), l)); - env->add_neutral_object(new coercion_declaration(f)); - } - - optional get_coercion_core(expr const & from_type, expr const & to_type) const { - expr_pair p(from_type, to_type); - auto it = m_coercion_map.find(p); - if (it != m_coercion_map.end()) - return some_expr(it->second); - lean_extension const * parent = get_parent(); - if (parent) - return parent->get_coercion_core(from_type, to_type); - else - return none_expr(); - } - - optional get_coercion(expr const & from_type, expr const & to_type, ro_environment const & env) const { - return get_coercion_core(coercion_type_normalization(from_type, env), - coercion_type_normalization(to_type, env)); - } - - list get_coercions_core(expr const & from_type) const { - auto r = m_type_coercions.find(from_type); - if (r != m_type_coercions.end()) - return r->second; - lean_extension const * parent = get_parent(); - if (parent) - return parent->get_coercions_core(from_type); - else - return list(); - } - - list get_coercions(expr const & from_type, ro_environment const & env) const { - return get_coercions_core(coercion_type_normalization(from_type, env)); - } - - bool is_coercion(expr const & f) const { - if (m_coercion_set.find(f) != m_coercion_set.end()) - return true; - lean_extension const * parent = get_parent(); - return parent && parent->is_coercion(f); - } - - optional get_alias(name const & n) const { - auto it = m_aliases.find(n); - if (it != m_aliases.end()) - return some_expr(it->second); - lean_extension const * parent = get_parent(); - if (parent) - return parent->get_alias(n); - else - return none_expr(); - } - - optional> get_aliased(expr const & e) const { - auto it = m_inv_aliases.find(e); - if (it != m_inv_aliases.end()) - return optional>(it->second); - lean_extension const * parent = get_parent(); - if (parent) - return parent->get_aliased(e); - else - return optional>(); - } - - void add_alias(name const & n, expr const & e, environment const & env) { - if (get_alias(n)) - throw exception(sstream() << "alias '" << n << "' was already defined"); - m_aliases[n] = e; - auto l = get_aliased(e); - if (l) - m_inv_aliases[e] = list(n, *l); - else - m_inv_aliases[e] = list(n); - env->add_neutral_object(new alias_declaration(n, e)); - } -}; - -struct lean_extension_initializer { - unsigned m_extid; - lean_extension_initializer() { - m_extid = environment_cell::register_extension([](){ return std::unique_ptr(new lean_extension()); }); - } -}; - -static lean_extension_initializer g_lean_extension_initializer; - -static lean_extension const & to_ext(ro_environment const & env) { - return env->get_extension(g_lean_extension_initializer.m_extid); -} - -static lean_extension & to_ext(environment const & env) { - return env->get_extension(g_lean_extension_initializer.m_extid); -} - -io_state init_frontend(environment const & env, bool no_kernel) { - io_state ios(mk_pp_formatter(env)); - if (!no_kernel) { - import_kernel(env, ios); - import_nat(env, ios); - } - return ios; -} - -io_state init_test_frontend(environment const & env) { - env->set_trusted_imported(true); - io_state ios = init_frontend(env); - import_int(env, ios); - import_real(env, ios); - return ios; -} - -void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) { - to_ext(env).add_op(infix(opn, p), d, true, env, ios); -} -void add_infixl(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) { - to_ext(env).add_op(infixl(opn, p), d, true, env, ios); -} -void add_infixr(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) { - to_ext(env).add_op(infixr(opn, p), d, true, env, ios); -} -void add_prefix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) { - to_ext(env).add_op(prefix(opn, p), d, false, env, ios); -} -void add_postfix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) { - to_ext(env).add_op(postfix(opn, p), d, true, env, ios); -} -void add_mixfixl(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) { - to_ext(env).add_op(mixfixl(sz, opns, p), d, false, env, ios); -} -void add_mixfixr(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) { - to_ext(env).add_op(mixfixr(sz, opns, p), d, true, env, ios); -} -void add_mixfixc(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) { - to_ext(env).add_op(mixfixc(sz, opns, p), d, false, env, ios); -} -void add_mixfixo(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) { - to_ext(env).add_op(mixfixo(sz, opns, p), d, true, env, ios); -} -operator_info find_op_for(ro_environment const & env, expr const & n, bool unicode) { - operator_info r = to_ext(env).find_op_for(n, unicode); - if (r) { - return r; - } else if (is_constant(n)) { - optional obj = env->find_object(const_name(n)); - if (obj && obj->is_builtin() && obj->get_name() == const_name(n)) { - // n is a constant that is referencing a builtin object. - // If the notation is associated with the builtin object, we should try it. - // TODO(Leo): Remark: in the new approach using .Lean files, the table is populated with constants. - // So, this branch is not really needed anymore. - return to_ext(env).find_op_for(obj->get_value(), unicode); - } else { - return r; - } - } else if (is_value(n)) { - // Check whether the notation was declared for a constant referencing this builtin object. - return to_ext(env).find_op_for(mk_constant(to_value(n).get_name()), unicode); - } else { - return r; - } -} -operator_info find_nud(ro_environment const & env, name const & n) { - return to_ext(env).find_nud(n); -} -operator_info find_led(ro_environment const & env, name const & n) { - return to_ext(env).find_led(n); -} -optional get_lbp(ro_environment const & env, name const & n) { - return to_ext(env).get_lbp(n); -} -void mark_implicit_arguments(environment const & env, name const & n, unsigned sz, bool const * implicit) { - to_ext(env).mark_implicit_arguments(n, sz, implicit, env); -} -void mark_implicit_arguments(environment const & env, name const & n, std::initializer_list const & l) { - mark_implicit_arguments(env, n, l.size(), l.begin()); -} -bool has_implicit_arguments(ro_environment const & env, name const & n) { - return to_ext(env).has_implicit_arguments(n); -} -std::vector const & get_implicit_arguments(ro_environment const & env, name const & n) { - return to_ext(env).get_implicit_arguments(n); -} -std::vector const & get_implicit_arguments(ro_environment const & env, expr const & n) { - if (is_constant(n)) - return get_implicit_arguments(env, const_name(n)); - else if (is_value(n)) - return get_implicit_arguments(env, to_value(n).get_name()); - else - return g_empty_vector; -} -name const & get_explicit_version(ro_environment const & env, name const & n) { - return to_ext(env).get_explicit_version(n); -} -bool is_explicit(ro_environment const & env, name const & n) { - return to_ext(env).is_explicit(n); -} -void add_coercion(environment const & env, expr const & f) { - to_ext(env).add_coercion(f, env); -} -optional get_coercion(ro_environment const & env, expr const & from_type, expr const & to_type) { - return to_ext(env).get_coercion(from_type, to_type, env); -} -list get_coercions(ro_environment const & env, expr const & from_type) { - return to_ext(env).get_coercions(from_type, env); -} -bool is_coercion(ro_environment const & env, expr const & f) { - return to_ext(env).is_coercion(f); -} -optional get_alias(ro_environment const & env, name const & n) { - return to_ext(env).get_alias(n); -} -optional> get_aliased(ro_environment const & env, expr const & e) { - return to_ext(env).get_aliased(e); -} -void add_alias(environment const & env, name const & n, expr const & e) { - to_ext(env).add_alias(n, e, env); -} -} diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h deleted file mode 100644 index 5cfece0f3..000000000 --- a/src/frontends/lean/frontend.h +++ /dev/null @@ -1,170 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "kernel/environment.h" -#include "kernel/io_state.h" -#include "library/expr_pair.h" -#include "frontends/lean/operator_info.h" - -namespace lean { -/** - \brief Load kernel, nat and set pretty printer. -*/ -io_state init_frontend(environment const & env, bool no_kernel = false); - -/* - \brief Load kernel, nat, int, real and set pretty printer. - It is used for testing. -*/ -io_state init_test_frontend(environment const & env); - -/** - @name Notation for parsing and pretty printing. -*/ -/*@{*/ -void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d); -void add_infixl(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d); -void add_infixr(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d); -void add_prefix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d); -void add_postfix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d); -void add_mixfixl(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d); -void add_mixfixr(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d); -void add_mixfixc(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d); -void add_mixfixo(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d); -inline void add_mixfixl(environment const & env, io_state const & ios, std::initializer_list const & l, unsigned p, expr const & d) { - add_mixfixl(env, ios, l.size(), l.begin(), p, d); -} -inline void add_mixfixr(environment const & env, io_state const & ios, std::initializer_list const & l, unsigned p, expr const & d) { - add_mixfixr(env, ios, l.size(), l.begin(), p, d); -} -inline void add_mixfixc(environment const & env, io_state const & ios, std::initializer_list const & l, unsigned p, expr const & d) { - add_mixfixc(env, ios, l.size(), l.begin(), p, d); -} -inline void add_mixfixo(environment const & env, io_state const & ios, std::initializer_list const & l, unsigned p, expr const & d) { - add_mixfixo(env, ios, l.size(), l.begin(), p, d); -} -/** - \brief Return the operator (if one exists) that can appear at - the beginning of a language construct. - - \remark If there isn't a nud operator starting with \c n, then - return the null operator. - - \remark This is used for parsing. -*/ -operator_info find_nud(ro_environment const & env, name const & n); -/** - \brief Return the operator (if one exists) that can appear - inside of a language construct. - - \remark If there isn't a led operator starting with \c n, then - return the null operator. - - \remark This is used for parsing. -*/ -operator_info find_led(ro_environment const & env, name const & n); -/** - \brief Return the precedence (aka binding power) of the given name. -*/ -optional get_lbp(ro_environment const & env, name const & n); -/** - \brief Return the operator (if one exists) associated with the - given expression. - - \remark If an operator is not associated with \c e, then - return the null operator. - - \remark This is used for pretty printing. - - \remark If unicode is false, then only operators containing - safe ASCII chars are considered. -*/ -operator_info find_op_for(ro_environment const & env, expr const & e, bool unicode); -/*@}*/ - -/** - @name Implicit arguments. -*/ -/*@{*/ -/** - \brief Mark the given arguments of \c n as implicit. - The bit-vector array specify the position of the implicit arguments. -*/ -void mark_implicit_arguments(environment const & env, name const & n, unsigned sz, bool const * implicit); -void mark_implicit_arguments(environment const & env, name const & n, std::initializer_list const & l); -/** - \brief Return true iff \c n has implicit arguments -*/ -bool has_implicit_arguments(ro_environment const & env, name const & n); -/** - \brief Return the position of the arguments that are implicit. -*/ -std::vector const & get_implicit_arguments(ro_environment const & env, name const & n); -/** - \brief Return the position of the arguments that are implicit. - \remark If \c n is not a constant, then return the empty vector. -*/ -std::vector const & get_implicit_arguments(ro_environment const & env, expr const & n); -/** - \brief This frontend associates an definition with each - definition (or postulate) that has implicit arguments. The - additional definition has explicit arguments, and it is called - n::explicit. The explicit version can be used when the Lean - frontend can't figure out the value for the implicit - arguments. -*/ -name const & get_explicit_version(ro_environment const & env, name const & n); -/** - \brief Return true iff \c n is the name of the "explicit" - version of an object with implicit arguments -*/ -bool is_explicit(ro_environment const & env, name const & n); -/*@}*/ - - -/** - @name Coercions - - We support a very basic form of coercion. It is an expression - with type T1 -> T2. This expression can be used to convert - an expression of type T1 into an expression of type T2 whenever - T2 is expected, but T1 was provided. -*/ -/*@{*/ -/** - \brief Add a new coercion to the frontend. - It throws an exception if f does not have type T1 -> T2, or if there is already a - coercion from T1 to T2. -*/ -void add_coercion(environment const & env, expr const & f); -/** - \brief Return true iff the given expression is a coercion. That is, it was added using - \c add_coercion. -*/ -bool is_coercion(ro_environment const & env, expr const & f); -/** - \brief Return a coercion from given_type to expected_type if it exists. -*/ -optional get_coercion(ro_environment const & env, expr const & from_type, expr const & to_type); -/** - \brief Return the list of coercions for the given type. - The result is a list of pairs (to_type, function). -*/ -list get_coercions(ro_environment const & env, expr const & from_type); -/*@}*/ - -/** - @name Aliases -*/ -/*@{*/ -optional get_alias(ro_environment const & env, name const & n); -optional> get_aliased(ro_environment const & env, expr const & e); -void add_alias(environment const & env, name const & n, expr const & e); -/*@}*/ -} diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp deleted file mode 100644 index abde40740..000000000 --- a/src/frontends/lean/frontend_elaborator.cpp +++ /dev/null @@ -1,523 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include "util/interrupt.h" -#include "util/freset.h" -#include "kernel/type_checker.h" -#include "kernel/type_checker_justification.h" -#include "kernel/normalizer.h" -#include "kernel/replace_visitor.h" -#include "kernel/unification_constraint.h" -#include "kernel/instantiate.h" -#include "kernel/kernel.h" -#include "library/io_state_stream.h" -#include "library/placeholder.h" -#include "library/elaborator/elaborator.h" -#include "frontends/lean/frontend.h" -#include "frontends/lean/frontend_elaborator.h" - -namespace lean { -static name g_x_name("x"); -static format g_assignment_fmt = format(":="); -static format g_unification_u_fmt = format("\u2248"); -static format g_unification_fmt = format("=?="); - -/** - \brief Internal value used to store choices for the elaborator. - This is a transient value that is only used to setup a problem - for the elaborator. -*/ -struct choice_value : public value { - std::vector m_choices; - choice_value(unsigned num_fs, expr const * fs):m_choices(fs, fs + num_fs) {} - virtual ~choice_value() {} - virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE - virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE - virtual name get_name() const { return name("Choice"); } - virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return false; } // NOLINT - virtual void display(std::ostream & out) const { - out << "(Choice"; - for (auto c : m_choices) { - out << " (" << c << ")"; - } - out << ")"; - } - // Remark: we don't implement the pp methods because the lean::pp_fn formatter - // object has support for formatting choice internal values. -}; - -expr mk_choice(unsigned num_fs, expr const * fs) { - lean_assert(num_fs >= 2); - return mk_value(*(new choice_value(num_fs, fs))); -} - -bool is_choice(expr const & e) { - return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; -} - -choice_value const & to_choice_value(expr const & e) { - lean_assert(is_choice(e)); - return static_cast(to_value(e)); -} - -unsigned get_num_choices(expr const & e) { - return to_choice_value(e).m_choices.size(); -} - -expr const & get_choice(expr const & e, unsigned i) { - return to_choice_value(e).m_choices[i]; -} - -class coercion_justification_cell : public justification_cell { - context m_ctx; - expr m_src; -public: - coercion_justification_cell(context const & c, expr const & src):m_ctx(c), m_src(src) {} - virtual ~coercion_justification_cell() {} - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(m_ctx, instantiate_metavars(menv, m_src), false, opts); - format r; - r += format("Coercion for"); - r += nest(indent, compose(line(), expr_fmt)); - return r; - } - virtual void get_children(buffer &) const {} - virtual optional get_main_expr() const { return some_expr(m_src); } - context const & get_context() const { return m_ctx; } -}; - -class overload_justification_cell : public justification_cell { - context m_ctx; - expr m_app; -public: - overload_justification_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {} - virtual ~overload_justification_cell() {} - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(m_ctx, instantiate_metavars(menv, m_app), false, opts); - format r; - r += format("Overloading at"); - r += nest(indent, compose(line(), expr_fmt)); - return r; - } - virtual void get_children(buffer &) const {} - virtual optional get_main_expr() const { return some_expr(m_app); } - context const & get_context() const { return m_ctx; } - expr const & get_app() const { return m_app; } -}; - - -inline justification mk_coercion_justification(context const & ctx, expr const & e) { - return justification(new coercion_justification_cell(ctx, e)); -} - -inline justification mk_overload_justification(context const & ctx, expr const & app) { - return justification(new overload_justification_cell(ctx, app)); -} - -/** - \brief Actual implementation of the frontend_elaborator. -*/ -class frontend_elaborator::imp { - environment m_env; - type_checker m_type_checker; - normalizer m_normalizer; - metavar_env m_menv; - buffer m_ucs; - // The following mapping is used to store the relationship - // between elaborated expressions and non-elaborated expressions. - // We need that because a frontend may associate line number information - // with the original non-elaborated expressions. - expr_map m_trace; - - /** - \brief Replace placeholders and choices with metavariables. - It also introduce metavariables where coercions are needed. - */ - struct preprocessor : public replace_visitor { - imp & m_ref; - preprocessor(imp & r):m_ref(r) {} - - expr instantiate(expr const & e, expr const & v) { - return ::lean::instantiate(e, v, m_ref.m_menv); - } - - environment const & env() const { return m_ref.m_env; } - - virtual expr visit_constant(expr const & e, context const & ctx) { - if (is_placeholder(e)) { - expr m = m_ref.m_menv->mk_metavar(ctx, visit(const_type(e), ctx)); - m_ref.m_trace[m] = e; - return m; - } else { - return e; - } - } - - /** - \brief Return the type of \c e if possible. - The idea is to use the type to catch the easy cases where we can solve - overloads (aka choices) and coercions during preprocessing. - */ - optional get_type(expr const & e, context const & ctx) { - try { - return some_expr(m_ref.m_type_checker.infer_type(e, ctx)); - } catch (exception &) { - return none_expr(); - } - } - - bool is_convertible(expr const & from, expr const & to) { - try { - return m_ref.m_type_checker.is_convertible(from, to); - } catch (exception &) { - return false; - } - } - - /** - \brief Make sure f_t is a Pi, if it is not, then return none_expr() - */ - optional check_pi(optional const & f_t, context const & ctx) { - if (!f_t || is_pi(*f_t)) { - return f_t; - } else { - expr r = m_ref.m_normalizer(*f_t, ctx, m_ref.m_menv); - if (is_pi(r)) - return some_expr(r); - else - return none_expr(); - } - } - - expr add_coercion_mvar_app(list const & l, expr const & a, expr const & a_t, - context const & ctx, expr const & original_a) { - buffer choices; - expr mvar = m_ref.m_menv->mk_metavar(ctx); - for (auto p : l) { - choices.push_back(p.second); - } - choices.push_back(mk_lambda(g_x_name, a_t, mk_var(0))); // add indentity function - std::reverse(choices.begin(), choices.end()); - m_ref.m_ucs.push_back(mk_choice_constraint(ctx, mvar, choices.size(), choices.data(), - mk_coercion_justification(ctx, original_a))); - return mk_app(mvar, a); - } - - optional find_coercion(list const & l, expr const & to_type) { - for (auto p : l) { - if (p.first == to_type) { - return some_expr(p.second); - } - } - return none_expr(); - } - - /** - \brief Try to solve overload at preprocessing time. - */ - void choose(buffer & f_choices, buffer> & f_choice_types, - buffer const & args, buffer> const & arg_types, - context const & ctx) { - unsigned best_num_coercions = std::numeric_limits::max(); - unsigned num_choices = f_choices.size(); - unsigned num_args = args.size(); - buffer delayed; - buffer matched; - - for (unsigned j = 0; j < num_choices; j++) { - optional f_t = f_choice_types[j]; - unsigned num_coercions = 0; // number of coercions needed by current choice - unsigned num_skipped_args = 0; - unsigned i = 1; - for (; i < num_args; i++) { - f_t = check_pi(f_t, ctx); - if (!f_t) { - // can't process this choice at preprocessing time - delayed.push_back(j); - break; - } else { - expr expected = abst_domain(*f_t); - optional given = arg_types[i]; - if (!given) { - num_skipped_args++; - } else { - if (!has_metavar(expected) && !has_metavar(*given)) { - if (m_ref.m_type_checker.is_convertible(*given, expected, ctx)) { - // compatible - } else if (get_coercion(env(), *given, expected)) { - // compatible if using coercion - num_coercions++; - } else { - // failed, this choice does not work - break; - } - } else { - num_skipped_args++; - } - } - f_t = some_expr(instantiate(abst_body(*f_t), args[i])); - } - } - if (i == num_args) { - if (num_skipped_args > 0) { - // should keep this choice because we could not check all arguments - delayed.push_back(j); - } else if (num_coercions < best_num_coercions) { - // found best choice - best_num_coercions = num_coercions; - matched.clear(); - matched.push_back(j); - } else { - matched.push_back(j); - } - } - } - - matched.append(delayed); - - if (matched.size() == 0) { - // TODO(Leo): must use another exception that stores the choices considered. - // We currently do nothing, and let the elaborator to sign the error - } else { - buffer to_keep; - buffer> to_keep_types; - std::sort(matched.begin(), matched.end()); // we must preserve the original order - for (unsigned i : matched) { - to_keep.push_back(f_choices[i]); - to_keep_types.push_back(f_choice_types[i]); - } - f_choices.clear(); - f_choice_types.clear(); - f_choices.append(to_keep); - f_choice_types.append(to_keep_types); - } - } - - /** - \brief Create a metavariable for representing the choice. - */ - expr mk_overload_mvar(buffer & f_choices, context const & ctx, expr const & src) { - std::reverse(f_choices.begin(), f_choices.end()); - expr mvar = m_ref.m_menv->mk_metavar(ctx); - m_ref.m_ucs.push_back(mk_choice_constraint(ctx, mvar, f_choices.size(), f_choices.data(), - mk_overload_justification(ctx, src))); - return mvar; - } - - virtual expr visit_app(expr const & e, context const & ctx) { - expr f = arg(e, 0); - optional f_t; - buffer args; - buffer> arg_types; - args.push_back(expr()); // placeholder - arg_types.push_back(none_expr()); // placeholder - for (unsigned i = 1; i < num_args(e); i++) { - expr a = arg(e, i); - expr new_a = visit(a, ctx); - optional new_a_t = get_type(new_a, ctx); - args.push_back(new_a); - arg_types.push_back(new_a_t); - } - - if (is_choice(f)) { - buffer f_choices; - buffer> f_choice_types; - unsigned num_alts = get_num_choices(f); - for (unsigned i = 0; i < num_alts; i++) { - expr c = get_choice(f, i); - expr new_c = visit(c, ctx); - optional new_c_t = get_type(new_c, ctx); - f_choices.push_back(new_c); - f_choice_types.push_back(new_c_t); - } - choose(f_choices, f_choice_types, args, arg_types, ctx); - if (f_choices.size() > 1) { - args[0] = mk_overload_mvar(f_choices, ctx, e); - for (unsigned i = 1; i < args.size(); i++) { - if (arg_types[i]) { - list coercions = get_coercions(env(), *(arg_types[i])); - if (coercions) - args[i] = add_coercion_mvar_app(coercions, args[i], *(arg_types[i]), ctx, arg(e, i)); - } - } - return mk_app(args); - } else { - // managed to solve overload at preprocessing time - f = f_choices[0]; - f_t = f_choice_types[0]; - } - } else { - f = visit(f, ctx); - f_t = get_type(f, ctx); - } - - buffer new_args; - new_args.push_back(f); - for (unsigned i = 1; i < num_args(e); i++) { - f_t = check_pi(f_t, ctx); - expr a = arg(e, i); - expr new_a = args[i]; - optional new_a_t = arg_types[i]; - if (new_a_t) { - list coercions = get_coercions(env(), *new_a_t); - if (coercions) { - if (!f_t) { - new_a = add_coercion_mvar_app(coercions, new_a, *new_a_t, ctx, a); - } else { - expr expected = abst_domain(*f_t); - if (!is_convertible(*new_a_t, expected)) { - optional c = find_coercion(coercions, expected); - if (c) { - new_a = mk_app(*c, new_a); // apply coercion - } else { - new_a = add_coercion_mvar_app(coercions, new_a, *new_a_t, ctx, a); - } - } - } - } - } - new_args.push_back(new_a); - if (f_t) - f_t = some_expr(instantiate(abst_body(*f_t), new_a)); - } - return mk_app(new_args); - } - - virtual expr visit_let(expr const & e, context const & ctx) { - lean_assert(is_let(e)); - return update_let(e, [&](optional const & t, expr const & v, expr const & b) { - optional new_t = visit(t, ctx); - expr new_v = visit(v, ctx); - if (new_t) { - optional new_v_t = get_type(new_v, ctx); - if (new_v_t && *new_t != *new_v_t) { - list coercions = get_coercions(env(), *new_v_t); - if (coercions) { - new_v = add_coercion_mvar_app(coercions, new_v, *new_v_t, ctx, v); - } - } - } - { - freset reset(m_cache); - expr new_b = visit(b, extend(ctx, let_name(e), new_t, new_v)); - return std::make_tuple(new_t, new_v, new_b); - } - }); - } - - optional visit(optional const & e, context const & ctx) { - return replace_visitor::visit(e, ctx); - } - - virtual expr visit(expr const & e, context const & ctx) { - check_interrupted(); - expr r = replace_visitor::visit(e, ctx); - if (!is_eqp(r, e)) - m_ref.m_trace[r] = e; - return r; - } - }; - - metavar_env elaborate_core(options const & opts) { - elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data(), opts); - return elb.next(); - } - -public: - imp(environment const & env): - m_env(env), - m_type_checker(m_env), - m_normalizer(m_env) { - } - - std::pair elaborate(expr const & e, options const & opts) { - // std::cout << "Elaborate " << e << "\n"; - clear(); - expr new_e = preprocessor(*this)(e); - // std::cout << "After preprocessing\n" << new_e << "\n"; - if (has_metavar(new_e)) { - m_type_checker.check(new_e, context(), m_menv, m_ucs); - // for (auto c : m_ucs) { - // formatter fmt = mk_simple_formatter(); - // std::cout << c.pp(fmt, options(), nullptr, false) << "\n"; - // } - metavar_env new_menv = elaborate_core(opts); - return mk_pair(new_menv->instantiate_metavars(new_e), new_menv); - } else { - return mk_pair(new_e, metavar_env()); - } - } - - std::tuple elaborate(name const & n, expr const & t, expr const & e, - options const & opts) { - // std::cout << "Elaborate " << t << " : " << e << "\n"; - clear(); - expr new_t = preprocessor(*this)(t); - expr new_e = preprocessor(*this)(e); - // std::cout << "After preprocessing\n" << new_t << "\n" << new_e << "\n"; - if (has_metavar(new_e) || has_metavar(new_t)) { - m_type_checker.check(new_t, context(), m_menv, m_ucs); - expr new_e_t = m_type_checker.check(new_e, context(), m_menv, m_ucs); - m_ucs.push_back(mk_eq_constraint(context(), new_e_t, new_t, - mk_def_type_match_justification(context(), n, e))); - // for (auto c : m_ucs) { - // formatter fmt = mk_simple_formatter(); - // std::cout << c.pp(fmt, options(), nullptr, false) << "\n"; - // } - metavar_env new_menv = elaborate_core(opts); - return std::make_tuple(new_menv->instantiate_metavars(new_t), - new_menv->instantiate_metavars(new_e), - new_menv); - } else { - return std::make_tuple(new_t, new_e, metavar_env()); - } - } - - expr const & get_original(expr const & e) { - expr const * r = &e; - while (true) { - auto it = m_trace.find(*r); - if (it == m_trace.end()) { - return *r; - } else { - r = &(it->second); - } - } - } - - void clear() { - m_menv = metavar_env(); - m_ucs.clear(); - m_trace.clear(); - m_type_checker.clear(); - m_normalizer.clear(); - } - - environment const & get_environment() const { - return m_env; - } -}; - -frontend_elaborator::frontend_elaborator(environment const & env):m_ptr(std::make_shared(env)) {} -frontend_elaborator::~frontend_elaborator() {} -std::pair frontend_elaborator::operator()(expr const & e, options const & opts) { - return m_ptr->elaborate(e, opts); -} -std::tuple frontend_elaborator::operator()(name const & n, expr const & t, expr const & e, - options const & opts) { - return m_ptr->elaborate(n, t, e, opts); -} -expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); } -void frontend_elaborator::clear() { m_ptr->clear(); } -void frontend_elaborator::reset(environment const & env) { m_ptr.reset(new imp(env)); } -environment const & frontend_elaborator::get_environment() const { return m_ptr->get_environment(); } -} diff --git a/src/frontends/lean/frontend_elaborator.h b/src/frontends/lean/frontend_elaborator.h deleted file mode 100644 index f6219e478..000000000 --- a/src/frontends/lean/frontend_elaborator.h +++ /dev/null @@ -1,79 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "kernel/environment.h" -#include "kernel/formatter.h" - -namespace lean { -class frontend; -/** - \brief Expression elaborator for the Lean default frontend, it is responsible for "filling" holes - in terms left by the user. This is the main module resposible for computing - the value of implicit arguments. It is based on the general purpose elaborator defined at - library/elaborator/elaborator.h -*/ -class frontend_elaborator { - class imp; - std::shared_ptr m_ptr; - static void print(imp * ptr); -public: - explicit frontend_elaborator(environment const & env); - ~frontend_elaborator(); - - /** - \brief Elaborate the given expression. - */ - std::pair operator()(expr const & e, options const & opts); - /** - \brief Elaborate the given type and expression. The typeof(e) == t. - This information is used by the elaborator. The result is a new - elaborated type and expression. - */ - std::tuple operator()(name const & n, expr const & t, expr const & e, options const & opts); - - /** - \brief If \c e is an expression instantiated by the elaborator, then it - returns the expression (the one with "holes") used to generate \c e. - Otherwise, it just returns \c e. - */ - expr const & get_original(expr const & e) const; - - environment const & get_environment() const; - - void clear(); - void reset(environment const & env); -}; - -/** - \brief Create a choice expression for the given functions. - It is used to mark which functions can be used in a particular application. - The elaborator decides which one should be used based on the type of the arguments. - - \pre num_fs >= 2 -*/ -expr mk_choice(unsigned num_fs, expr const * fs); -/** - \brief Return true iff \c e is an expression created using \c mk_choice. -*/ -bool is_choice(expr const & e); -/** - \brief Return the number of alternatives in a choice expression. - We have that get_num_choices(mk_choice(n, fs)) == n. - - \pre is_choice(e) -*/ -unsigned get_num_choices(expr const & e); -/** - \brief Return the (i+1)-th alternative of a choice expression. - - \pre is_choice(e) - \pre i < get_num_choices(e) -*/ -expr const & get_choice(expr const & e, unsigned i); -} diff --git a/src/frontends/lean/notation.h b/src/frontends/lean/notation.h deleted file mode 100644 index 757dd568e..000000000 --- a/src/frontends/lean/notation.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -namespace lean { -constexpr unsigned g_heq_precedence = 50; -constexpr unsigned g_arrow_precedence = 25; -constexpr unsigned g_cartesian_product_precedence = 30; -constexpr unsigned g_app_precedence = std::numeric_limits::max(); -} diff --git a/src/frontends/lean/operator_info.cpp b/src/frontends/lean/operator_info.cpp deleted file mode 100644 index ee2c4a08c..000000000 --- a/src/frontends/lean/operator_info.cpp +++ /dev/null @@ -1,231 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/rc.h" -#include "library/io_state_stream.h" -#include "frontends/lean/operator_info.h" -#include "frontends/lean/frontend.h" - -namespace lean { -/** \brief Actual implementation of operator_info */ -struct operator_info::imp { - void dealloc() { delete this; } - MK_LEAN_RC(); - fixity m_fixity; - unsigned m_precedence; - list m_op_parts; // operator parts, > 1 only if the operator is mixfix. - list m_exprs; // possible interpretations for the operator. - - imp(name const & op, fixity f, unsigned p): - m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(cons(op, list())) {} - - imp(unsigned num_parts, name const * parts, fixity f, unsigned p): - m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(to_list(parts, parts + num_parts)) { - lean_assert(num_parts > 0); - } - - imp(imp const & s): - m_rc(1), m_fixity(s.m_fixity), m_precedence(s.m_precedence), m_op_parts(s.m_op_parts), m_exprs(s.m_exprs) { - } - - bool is_eq(imp const & other) const { - return - m_fixity == other.m_fixity && - m_precedence == other.m_precedence && - m_op_parts == other.m_op_parts; - } -}; - -operator_info::operator_info(imp * p):m_ptr(p) {} - -operator_info::operator_info(operator_info const & info):m_ptr(info.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } - -operator_info::operator_info(operator_info && info):m_ptr(info.m_ptr) { info.m_ptr = nullptr; } - -operator_info::~operator_info() { if (m_ptr) m_ptr->dec_ref(); } - -operator_info & operator_info::operator=(operator_info const & s) { LEAN_COPY_REF(s); } - -operator_info & operator_info::operator=(operator_info && s) { LEAN_MOVE_REF(s); } - -void operator_info::add_expr(expr const & d) { lean_assert(m_ptr); m_ptr->m_exprs = cons(d, m_ptr->m_exprs); } - -bool operator_info::is_overloaded() const { return m_ptr && !is_nil(m_ptr->m_exprs) && !is_nil(cdr(m_ptr->m_exprs)); } - -list const & operator_info::get_denotations() const { lean_assert(m_ptr); return m_ptr->m_exprs; } - -fixity operator_info::get_fixity() const { lean_assert(m_ptr); return m_ptr->m_fixity; } - -unsigned operator_info::get_precedence() const { lean_assert(m_ptr); return m_ptr->m_precedence; } - -name const & operator_info::get_op_name() const { lean_assert(m_ptr); return car(m_ptr->m_op_parts); } - -list const & operator_info::get_op_name_parts() const { lean_assert(m_ptr); return m_ptr->m_op_parts; } - -bool operator_info::is_safe_ascii() const { - auto l = get_op_name_parts(); - return std::all_of(l.begin(), l.end(), [](name const & p) { return p.is_safe_ascii(); }); -} - -operator_info operator_info::copy() const { return operator_info(new imp(*m_ptr)); } - -bool operator==(operator_info const & op1, operator_info const & op2) { - if ((op1.m_ptr == nullptr) != (op2.m_ptr == nullptr)) - return false; - if (op1.m_ptr) - return op1.m_ptr->is_eq(*(op2.m_ptr)); - else - return true; -} - -operator_info infix(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Infix, precedence)); -} -operator_info infixr(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Infixr, precedence)); -} -operator_info infixl(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Infixl, precedence)); -} -operator_info prefix(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Prefix, precedence)); -} -operator_info postfix(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Postfix, precedence)); -} -operator_info mixfixl(unsigned num_parts, name const * parts, unsigned precedence) { - lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixl, precedence)); -} -operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence) { - lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixr, precedence)); -} -operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence) { - lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixc, precedence)); -} -operator_info mixfixo(unsigned num_parts, name const * parts, unsigned precedence) { - lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixo, precedence)); -} - -char const * to_string(fixity f) { - switch (f) { - case fixity::Infix: return "infix"; - case fixity::Infixl: return "infixl"; - case fixity::Infixr: return "infixr"; - case fixity::Prefix: return "prefix"; - case fixity::Postfix: return "postfix"; - case fixity::Mixfixl: return "mixfixl"; - case fixity::Mixfixr: return "mixfixr"; - case fixity::Mixfixc: return "mixfixc"; - case fixity::Mixfixo: return "mixfixo"; - } - lean_unreachable(); // LCOV_EXCL_LINE -} - -format pp(operator_info const & o) { - format r; - switch (o.get_fixity()) { - case fixity::Infix: - case fixity::Infixl: - case fixity::Infixr: - r = highlight_command(format(to_string(o.get_fixity()))); - if (o.get_precedence() > 1) - r += format{space(), format(o.get_precedence())}; - r += format{space(), format(o.get_op_name())}; - return r; - case fixity::Prefix: - case fixity::Postfix: - case fixity::Mixfixl: - case fixity::Mixfixr: - case fixity::Mixfixc: - case fixity::Mixfixo: - r = highlight_command(format("notation")); - if (o.get_precedence() > 1) - r += format{space(), format(o.get_precedence())}; - switch (o.get_fixity()) { - case fixity::Prefix: - r += format{space(), format(o.get_op_name()), space(), format("_")}; - return r; - case fixity::Postfix: - r += format{space(), format("_"), space(), format(o.get_op_name())}; - return r; - case fixity::Mixfixl: - for (auto p : o.get_op_name_parts()) - r += format{space(), format(p), space(), format("_")}; - return r; - case fixity::Mixfixr: - for (auto p : o.get_op_name_parts()) - r += format{space(), format("_"), space(), format(p)}; - return r; - case fixity::Mixfixc: { - auto parts = o.get_op_name_parts(); - r += format{space(), format(head(parts))}; - for (auto p : tail(parts)) - r += format{space(), format("_"), space(), format(p)}; - return r; - } - case fixity::Mixfixo: - for (auto p : o.get_op_name_parts()) - r += format{space(), format("_"), space(), format(p)}; - r += format{space(), format("_")}; - return r; - default: lean_unreachable(); // LCOV_EXCL_LINE - } - } - lean_unreachable(); // LCOV_EXCL_LINE -} - -char const * notation_declaration::keyword() const { - return to_string(m_op.get_fixity()); -} - -void notation_declaration::write(serializer & s) const { - auto parts = m_op.get_op_name_parts(); - s << "Notation" << length(parts); - for (auto n : parts) - s << n; - s << static_cast(m_op.get_fixity()) << m_op.get_precedence() << m_expr; -} -static void read_notation(environment const & env, io_state const & ios, deserializer & d) { - buffer parts; - unsigned num = d.read_unsigned(); - for (unsigned i = 0; i < num; i++) - parts.push_back(read_name(d)); - fixity fx = static_cast(d.read_char()); - unsigned p = d.read_unsigned(); - expr e = read_expr(d); - switch (fx) { - case fixity::Infix: lean_assert(parts.size() == 1); add_infix(env, ios, parts[0], p, e); return; - case fixity::Infixl: lean_assert(parts.size() == 1); add_infixl(env, ios, parts[0], p, e); return; - case fixity::Infixr: lean_assert(parts.size() == 1); add_infixr(env, ios, parts[0], p, e); return; - case fixity::Prefix: lean_assert(parts.size() == 1); add_prefix(env, ios, parts[0], p, e); return; - case fixity::Postfix: lean_assert(parts.size() == 1); add_postfix(env, ios, parts[0], p, e); return; - case fixity::Mixfixl: add_mixfixl(env, ios, parts.size(), parts.data(), p, e); return; - case fixity::Mixfixr: add_mixfixr(env, ios, parts.size(), parts.data(), p, e); return; - case fixity::Mixfixc: add_mixfixc(env, ios, parts.size(), parts.data(), p, e); return; - case fixity::Mixfixo: add_mixfixo(env, ios, parts.size(), parts.data(), p, e); return; - } -} -static object_cell::register_deserializer_fn notation_ds("Notation", read_notation); - -std::ostream & operator<<(std::ostream & out, operator_info const & o) { - out << pp(o); - return out; -} - -io_state_stream const & operator<<(io_state_stream const & out, operator_info const & o) { - out.get_stream() << mk_pair(pp(o), out.get_options()); - return out; -} - -char const * alias_declaration::keyword() const { return "alias"; } -void alias_declaration::write(serializer & s) const { s << "alias" << m_name << m_expr; } -static void read_alias(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - expr e = read_expr(d); - add_alias(env, n, e); -} -static object_cell::register_deserializer_fn add_alias_ds("alias", read_alias); -} diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h deleted file mode 100644 index feb5bb115..000000000 --- a/src/frontends/lean/operator_info.h +++ /dev/null @@ -1,143 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "util/name.h" -#include "util/list.h" -#include "util/sexpr/format.h" -#include "kernel/io_state.h" -#include "kernel/object.h" - -namespace lean { -/** - \brief Operator fixity. - Prefix: ID _ - Infix: _ ID _ - Infixl: _ ID _ (left associative) - Infixr: _ ID _ (right associative) - Postfix: _ ID - Mixfixl: ID _ ID _ ... ID _ (has at least two parts) - Mixfixr: _ ID _ ID ... _ ID (has at least two parts) - Mixfixc: ID _ ID _ ... ID _ ID (has at least two parts) - Mixfixo: _ ID _ ... ID _ (has at least two parts) -*/ -enum class fixity { Prefix, Infix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc, Mixfixo }; - -/** - \brief Data-structure for storing user defined operator - information. This information is used during parsing and - pretty-printing. -*/ -class operator_info { - struct imp; - imp * m_ptr; - explicit operator_info(imp * p); -public: - operator_info():m_ptr(nullptr) {} - operator_info(operator_info const & info); - operator_info(operator_info && info); - ~operator_info(); - - operator_info & operator=(operator_info const & o); - operator_info & operator=(operator_info && o); - - friend void swap(operator_info & o1, operator_info & o2) { std::swap(o1.m_ptr, o2.m_ptr); } - - explicit operator bool() const { return m_ptr != nullptr; } - - friend operator_info infix(name const & op, unsigned precedence); - friend operator_info infixl(name const & op, unsigned precedence); - friend operator_info infixr(name const & op, unsigned precedence); - friend operator_info prefix(name const & op, unsigned precedence); - friend operator_info postfix(name const & op, unsigned precedence); - friend operator_info mixfixl(unsigned num_parts, name const * parts, unsigned precedence); - friend operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence); - friend operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence); - friend operator_info mixfixo(unsigned num_parts, name const * parts, unsigned precedence); - - /** \brief Associate a denotation (expression) with this operator. */ - void add_expr(expr const & n); - - /** \brief Return true iff the operator is overloaded. */ - bool is_overloaded() const; - - /** - \brief Return the list of denotations for this operator. - The list has size greater than 1 iff the operator has been - overloaded. - These are the possible interpretations for the operator. - */ - list const & get_denotations() const; - - /** \brief Return the operator fixity. */ - fixity get_fixity() const; - - /** \brief Return the operator precedence. */ - unsigned get_precedence() const; - - /** \brief Return the operator name. For mixfix operators the result corresponds to the first part. */ - name const & get_op_name() const; - - /** \brief Return the operators parts. */ - list const & get_op_name_parts() const; - - /** \brief Return true if all parts of the operator use only safe ASCII characters */ - bool is_safe_ascii() const; - - /** \brief Return a copy of the operator. */ - operator_info copy() const; - - friend bool operator==(operator_info const & op1, operator_info const & op2); - friend bool operator!=(operator_info const & op1, operator_info const & op2) { return !(op1 == op2); } -}; -operator_info infix(name const & op, unsigned precedence); -operator_info infixl(name const & op, unsigned precedence); -operator_info infixr(name const & op, unsigned precedence); -operator_info prefix(name const & op, unsigned precedence); -operator_info postfix(name const & op, unsigned precedence); -operator_info mixfixl(unsigned num_parts, name const * parts, unsigned precedence); -operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence); -operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence); -operator_info mixfixo(unsigned num_parts, name const * parts, unsigned precedence); -inline operator_info mixfixl(std::initializer_list const & l, unsigned precedence) { return mixfixl(l.size(), l.begin(), precedence); } -inline operator_info mixfixr(std::initializer_list const & l, unsigned precedence) { return mixfixr(l.size(), l.begin(), precedence); } -inline operator_info mixfixc(std::initializer_list const & l, unsigned precedence) { return mixfixc(l.size(), l.begin(), precedence); } -inline operator_info mixfixo(std::initializer_list const & l, unsigned precedence) { return mixfixo(l.size(), l.begin(), precedence); } - -format pp(operator_info const & o); -std::ostream & operator<<(std::ostream & out, operator_info const & o); - -io_state_stream const & operator<<(io_state_stream const & out, operator_info const & o); - -/** - \brief Create object for tracking notation/operator declarations. - This object is mainly used for recording the declaration. -*/ -class notation_declaration : public neutral_object_cell { - operator_info m_op; - expr m_expr; -public: - notation_declaration(operator_info const & op, expr const & n):m_op(op), m_expr(n) {} - virtual ~notation_declaration() {} - virtual char const * keyword() const; - operator_info get_op() const { return m_op; } - expr const & get_expr() const { return m_expr; } - virtual void write(serializer & s) const; -}; - -class alias_declaration : public neutral_object_cell { - name m_name; - expr m_expr; -public: - alias_declaration(name const & n, expr const & e):m_name(n), m_expr(e) {} - virtual ~alias_declaration() {} - virtual char const * keyword() const; - name const & get_alias_name() const { return m_name; } - expr const & get_expr() const { return m_expr; } - virtual void write(serializer & s) const; -}; -} diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp deleted file mode 100644 index aa97bc9bd..000000000 --- a/src/frontends/lean/parser.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/sstream.h" -#include "library/io_state_stream.h" -#include "frontends/lean/parser.h" -#include "frontends/lean/pp.h" -#include "frontends/lean/parser_imp.h" - -namespace lean { -parser::parser(environment const & env, io_state const & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions, bool interactive) { - parser_imp::show_prompt(interactive, ios); - m_ptr.reset(new parser_imp(env, ios, in, strm_name, S, use_exceptions, interactive)); - m_ptr->m_this = m_ptr; -} - -parser::~parser() { -} - -bool parser::operator()() { - return m_ptr->parse_commands(); -} - -expr parser::parse_expr() { - return m_ptr->parse_expr_main(); -} - -io_state parser::get_io_state() const { - return m_ptr->m_io_state; -} - -bool parse_commands(environment const & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions, bool interactive) { - parser p(env, ios, in, strm_name, S, use_exceptions, interactive); - bool r = p(); - ios = p.get_io_state(); - return r; -} - -bool parse_commands(environment const & env, io_state & ios, char const * fname, script_state * S, bool use_exceptions, bool interactive) { - std::ifstream in(fname); - if (in.bad() || in.fail()) - throw exception(sstream() << "failed to open file '" << fname << "'"); - return parse_commands(env, ios, in, fname, S, use_exceptions, interactive); -} - -expr parse_expr(environment const & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions) { - parser p(env, ios, in, strm_name, S, use_exceptions); - expr r = p.parse_expr(); - ios = p.get_io_state(); - return r; -} -} diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h deleted file mode 100644 index dfc6e358c..000000000 --- a/src/frontends/lean/parser.h +++ /dev/null @@ -1,37 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "util/lua.h" -#include "kernel/environment.h" -#include "kernel/io_state.h" - -namespace lean { -class script_state; -class parser_imp; -/** \brief Functional object for parsing commands and expressions */ -class parser { -private: - std::shared_ptr m_ptr; -public: - parser(environment const & env, io_state const & st, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions = true, bool interactive = false); - ~parser(); - - /** \brief Parse a sequence of commands */ - bool operator()(); - - /** \brief Parse a single expression */ - expr parse_expr(); - - io_state get_io_state() const; -}; - -bool parse_commands(environment const & env, io_state & st, std::istream & in, char const * strm_name, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false); -bool parse_commands(environment const & env, io_state & st, char const * fname, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false); -expr parse_expr(environment const & env, io_state & st, std::istream & in, char const * strm_name, script_state * S = nullptr, bool use_exceptions = true); -void open_macros(lua_State * L); -} diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp deleted file mode 100644 index 9551a8272..000000000 --- a/src/frontends/lean/parser_calc.cpp +++ /dev/null @@ -1,158 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/kernel.h" -#include "library/placeholder.h" -#include "library/io_state_stream.h" -#include "frontends/lean/parser_calc.h" -#include "frontends/lean/parser_imp.h" -#include "frontends/lean/operator_info.h" -#include "frontends/lean/frontend.h" - -namespace lean { -bool calc_proof_parser::supports(expr const & op1) const { - return - std::find_if(m_supported_operators.begin(), m_supported_operators.end(), [&](op_data const & op2) { - return op1 == op2.m_fn; - }) - != m_supported_operators.end(); -} - -void calc_proof_parser::add_supported_operator(op_data const & op1) { - if (supports(op1.m_fn)) - throw exception("operator already supported in the calculational proof manager"); - m_supported_operators = cons(op1, m_supported_operators); -} - -optional calc_proof_parser::find_trans_data(expr const & op1, expr const & op2) const { - auto it = std::find_if(m_trans_ops.begin(), m_trans_ops.end(), - [&](std::tuple const & entry) { return std::get<0>(entry) == op1 && std::get<1>(entry) == op2; }); - if (it == m_trans_ops.end()) - return optional(); - else - return optional(std::get<2>(*it)); -} - -void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans_data const & d) { - if (!supports(op1) || !supports(op2) || !supports(d.m_rop)) - throw exception("invalid transitivity step in calculational proof manager, operator not supported"); - if (find_trans_data(op1, op2)) - throw exception("transitivity step is already supported in the calculational proof manager"); - if (d.m_num_args < 5) - throw exception("transitivity step must have at least 5 arguments"); - m_trans_ops.emplace_front(op1, op2, d); -} - -calc_proof_parser::calc_proof_parser() { - expr imp = mk_implies_fn(); - expr eq = mk_eq_fn(); - expr neq = mk_neq_fn(); - - add_supported_operator(op_data(imp, 2)); - add_supported_operator(op_data(eq, 3)); - add_supported_operator(op_data(neq, 3)); - add_trans_step(eq, eq, trans_data(mk_trans_fn(), 6, eq)); - add_trans_step(eq, imp, trans_data(mk_eq_imp_trans_fn(), 5, imp)); - add_trans_step(imp, eq, trans_data(mk_imp_eq_trans_fn(), 5, imp)); - add_trans_step(imp, imp, trans_data(mk_imp_trans_fn(), 5, imp)); - add_trans_step(eq, neq, trans_data(mk_eq_ne_trans_fn(), 6, neq)); - add_trans_step(neq, eq, trans_data(mk_ne_eq_trans_fn(), 6, neq)); -} - -optional calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const { - if (!op) - return none_expr(); - for (auto d : op.get_denotations()) { - // TODO(Leo): I'm ignoring overloading. - if (supports(d)) - return some_expr(d); - } - throw parser_error("invalid calculational proof, operator is not supported", p); - return none_expr(); -} - -expr calc_proof_parser::parse_op(parser_imp & imp) const { - environment const & env = imp.get_environment(); - auto p = imp.pos(); - name id = imp.check_identifier_next("invalid calculational proof, identifier expected"); - if (auto r = find_op(find_led(env, id), p)) - return *r; - if (auto r = find_op(find_nud(env, id), p)) - return *r; - expr e = imp.get_name_ref(id, p, false /* do not process implicit args */); - if (!supports(e)) - throw parser_error("invalid calculational proof, operator is not supported", p); - return e; -} - -static expr parse_step_pr(parser_imp & imp, expr const & lhs) { - auto p = imp.pos(); - imp.check_colon_next("invalid calculational proof, ':' expected"); - if (imp.curr_is_lcurly()) { - imp.next(); - expr eq_pr = imp.parse_expr(); - imp.check_rcurly_next("invalid calculational proof, '}' expected"); - // Using axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b. - return imp.save(mk_subst_th(imp.save(mk_placeholder(), p), - imp.save(mk_placeholder(), p), - imp.save(mk_placeholder(), p), - imp.save(mk_placeholder(), p), // let elaborator compute the first four arguments - imp.save(mk_refl_th(imp.save(mk_placeholder(), p), lhs), p), - eq_pr), p); - } else { - return imp.parse_expr(); - } -} - -/** - \brief Parse - - calc expr op expr : proof1 - ... op expr : proof2 - - ... op expr : proofn -*/ -expr calc_proof_parser::parse(parser_imp & imp) const { - auto p = imp.pos(); - expr first = imp.parse_expr(); - if (!is_app(first)) - throw parser_error("invalid calculational proof, first expression must be an application", p); - expr op = arg(first, 0); - if (!supports(op)) - throw parser_error("invalid calculational proof, first expression is not an application of a supported operator", p); - if (num_args(first) < 3) - throw parser_error("invalid calculational proof, first expression must be an application of a binary operator (modulo implicit arguments)", p); - unsigned num = num_args(first); - expr lhs = arg(first, num - 2); - expr rhs = arg(first, num - 1); - expr result = parse_step_pr(imp, lhs); - while (imp.curr() == scanner::token::Ellipsis) { - imp.next(); - p = imp.pos(); - expr new_op = parse_op(imp); - auto tdata = find_trans_data(op, new_op); - if (!tdata) - throw parser_error("invalid calculational proof, operators cannot be combined", p); - expr new_rhs = imp.parse_expr(); - expr step_pr = parse_step_pr(imp, rhs); - buffer args; - args.push_back(tdata->m_fn); - for (unsigned i = 0; i < tdata->m_num_args - 5; i++) { - // transitivity step has implicit arguments - args.push_back(imp.save(mk_placeholder(), p)); - } - args.push_back(lhs); - args.push_back(rhs); - args.push_back(new_rhs); - args.push_back(result); - args.push_back(step_pr); - result = imp.save(mk_app(args), p); - op = tdata->m_rop; - rhs = new_rhs; - } - return result; -} -} diff --git a/src/frontends/lean/parser_calc.h b/src/frontends/lean/parser_calc.h deleted file mode 100644 index 295e95078..000000000 --- a/src/frontends/lean/parser_calc.h +++ /dev/null @@ -1,82 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/list.h" -#include "util/optional.h" -#include "kernel/expr.h" -#include "frontends/lean/parser_types.h" - -namespace lean { -class parser_imp; -class operator_info; -/** - \brief Information for a operator available in the - calculational proof module. It must have at least two arguments. - It may have implicit ones. We assume the implicit arguments - occur in the beginning. -*/ -struct op_data { - expr m_fn; - unsigned m_num_args; - op_data(expr const & f, unsigned n): m_fn(f), m_num_args(n) {} -}; - -/** - \brief Information about a transitivity-like proof step. - - The m_fn function must have at least 5 arguments. - We assume the implicit ones occur in the beginning. - The last five are a, b, c and a proof for 'a op1 b' and 'b op2 c'. - The function m_fn produces a proof for 'a rop b'. - The resultant operator must be in the list of supported operators. -*/ -struct trans_data { - expr m_fn; - unsigned m_num_args; // number of arguments of m_fn . - expr m_rop; // resultant operator - trans_data(expr const & f, unsigned n, expr const & rop): - m_fn (f), m_num_args(n), m_rop(rop) { - } -}; - -/** - \brief Calculational proof support in the Lean parser. - - It parses expression of the form: - - calc expr op expr : proof1 - ... op expr : proof2 - - ... op expr : proofn -*/ -class calc_proof_parser { - /** - \brief List of supported operators in calculational proofs. - */ - list m_supported_operators; - - /** - \brief Maps to operators to the corresponding transitivity operator. - For example, the pair (=, =>) maps to - - Theorem EqImpTrans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c - := assume Ha, MP H2 (EqMP H1 Ha). - */ - list> m_trans_ops; - optional find_trans_data(expr const & op1, expr const & op2) const; - optional find_op(operator_info const & op, pos_info const & p) const; - expr parse_op(parser_imp & imp) const; -public: - calc_proof_parser(); - - bool supports(expr const & op1) const; - void add_supported_operator(op_data const & op); - void add_trans_step(expr const & op1, expr const & op2, trans_data const & d); - - expr parse(parser_imp & p) const; -}; -} diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp deleted file mode 100644 index b81d7269a..000000000 --- a/src/frontends/lean/parser_cmds.cpp +++ /dev/null @@ -1,978 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/sstream.h" -#include "util/lean_path.h" -#include "util/sexpr/option_declarations.h" -#include "kernel/find_fn.h" -#include "kernel/kernel_exception.h" -#include "kernel/normalizer.h" -#include "kernel/type_checker.h" -#include "library/placeholder.h" -#include "library/io_state_stream.h" -#include "library/simplifier/rewrite_rule_set.h" -#include "frontends/lean/parser_imp.h" -#include "frontends/lean/frontend.h" -#include "frontends/lean/pp.h" -#include "frontends/lean/environment_scope.h" - -namespace lean { -// ========================================== -// Builtin commands -static name g_alias_kwd("alias"); -static name g_definition_kwd("definition"); -static name g_variable_kwd("variable"); -static name g_variables_kwd("variables"); -static name g_theorem_kwd("theorem"); -static name g_axiom_kwd("axiom"); -static name g_universe_kwd("universe"); -static name g_eval_kwd("eval"); -static name g_check_kwd("check"); -static name g_infix_kwd("infix"); -static name g_infixl_kwd("infixl"); -static name g_infixr_kwd("infixr"); -static name g_notation_kwd("notation"); -static name g_set_option_kwd("set_option"); -static name g_set_opaque_kwd("set_opaque"); -static name g_options_kwd("options"); -static name g_env_kwd("environment"); -static name g_import_kwd("import"); -static name g_help_kwd("help"); -static name g_coercion_kwd("coercion"); -static name g_exit_kwd("exit"); -static name g_print_kwd("print"); -static name g_pop_kwd("pop_scope"); -static name g_scope_kwd("scope"); -static name g_builtin_kwd("builtin"); -static name g_namespace_kwd("namespace"); -static name g_end_kwd("end"); -static name g_using_kwd("using"); -static name g_rewrite_set_kwd("rewrite_set"); -static name g_add_rewrite_kwd("add_rewrite"); -static name g_enable_rewrite_kwd("enable_rewrite"); -static name g_disable_rewrite_kwd("disable_rewrite"); -/** \brief Table/List with all builtin command keywords */ -static list g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, - g_axiom_kwd, g_universe_kwd, g_eval_kwd, - g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, - g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, - g_import_kwd, g_help_kwd, g_coercion_kwd, - g_exit_kwd, g_print_kwd, g_pop_kwd, g_scope_kwd, g_alias_kwd, g_builtin_kwd, - g_namespace_kwd, g_end_kwd, g_using_kwd, g_rewrite_set_kwd, g_add_rewrite_kwd, - g_enable_rewrite_kwd, g_disable_rewrite_kwd}; -// ========================================== - -list const & parser_imp::get_command_keywords() { - return g_command_keywords; -} - -/** - \brief Register implicit arguments for the definition or - postulate named \c n. The fourth element in the tuple parameters - is a flag indiciating whether the argument is implicit or not. -*/ -void parser_imp::register_implicit_arguments(name const & n, parameter_buffer & parameters) { - bool found = false; - buffer imp_args; - for (unsigned i = 0; i < parameters.size(); i++) { - imp_args.push_back(parameters[i].m_implicit); - if (imp_args.back()) - found = true; - } - if (found) - mark_implicit_arguments(m_env, n, imp_args.size(), imp_args.data()); -} - - -/** \brief Throw an exception if \c e contains a metavariable */ -void parser_imp::check_no_metavar(expr const & e, metavar_env const &, char const * msg) { - if (has_metavar(e)) - throw unsolved_metavar_exception(msg, e); -} - -void parser_imp::check_no_metavar(std::pair const & p, char const * msg) { - check_no_metavar(p.first, p.second, msg); -} - - -/** - \brief Return a fully qualified name (i.e., include current namespace) -*/ -name parser_imp::mk_full_name(name const & n) { - return m_namespace_prefixes.back() + n; -} - -/** \brief Auxiliary method used for parsing definitions and theorems. */ -void parser_imp::parse_def_core(bool is_definition) { - next(); - expr pre_type, pre_val; - name id = check_identifier_next("invalid definition, identifier expected"); - parameter_buffer parameters; - if (curr_is_colon()) { - next(); - pre_type = parse_expr(); - if (!is_definition && curr_is_period()) { - pre_val = save(mk_placeholder(), pos()); - } else { - check_assign_next("invalid definition, ':=' expected"); - pre_val = parse_expr(); - } - } else if (is_definition && curr_is_assign()) { - auto p = pos(); - next(); - pre_type = save(mk_placeholder(), p); - pre_val = parse_expr(); - } else { - mk_scope scope(*this); - parse_definition_parameters(parameters); - expr type_body; - if (curr_is_colon()) { - next(); - type_body = parse_expr(); - } else { - auto p = pos(); - type_body = save(mk_placeholder(), p); - } - pre_type = mk_abstraction(expr_kind::Pi, parameters, type_body); - if (!is_definition && curr_is_period()) { - pre_val = mk_abstraction(expr_kind::Lambda, parameters, mk_placeholder()); - } else { - check_assign_next("invalid definition, ':=' expected"); - expr val_body = parse_expr(); - pre_val = mk_abstraction(expr_kind::Lambda, parameters, val_body); - } - } - auto r = elaborate(id, pre_type, pre_val); - expr type = std::get<0>(r); - expr val = std::get<1>(r); - metavar_env menv = std::get<2>(r); - if (has_metavar(type)) { - type = apply_tactics(type, menv); - val = menv->instantiate_metavars(val); // val may contain metavariables instantiated in the previous step - } - check_no_metavar(type, menv, "invalid definition, type still contains metavariables after elaboration"); - if (has_metavar(val)) - val = apply_tactics(val, menv); - check_no_metavar(val, menv, "invalid definition, value still contains metavariables after elaboration"); - lean_assert(!has_metavar(val)); - name full_id = mk_full_name(id); - if (is_definition) { - m_env->add_definition(full_id, type, val); - if (m_verbose) - regular(m_io_state) << " Defined: " << full_id << endl; - } else { - m_env->add_theorem(full_id, type, val); - if (m_verbose) - regular(m_io_state) << " Proved: " << full_id << endl; - } - register_implicit_arguments(full_id, parameters); -} - -/** - \brief Parse a Definition. It has one of the following two forms: - - 1) 'definition' ID ':' expr ':=' expr - - 2) 'definition' ID parameters ':' expr ':=' expr -*/ -void parser_imp::parse_definition() { - parse_def_core(true); -} - -/** - \brief Parse a Theorem. It has one of the following two forms: - - 1) 'theorem' ID ':' expr ':=' expr - - 2) 'theorem' ID parameters ':' expr ':=' expr -*/ -void parser_imp::parse_theorem() { - parse_def_core(false); -} - -/** \brief Auxiliary method for parsing Variable and axiom declarations. */ -void parser_imp::parse_variable_core(bool is_var) { - next(); - name id = check_identifier_next("invalid variable/axiom declaration, identifier expected"); - expr pre_type; - parameter_buffer parameters; - if (curr_is_colon()) { - next(); - pre_type = parse_expr(); - } else { - mk_scope scope(*this); - parse_var_decl_parameters(parameters); - check_colon_next("invalid variable/axiom declaration, ':' expected"); - expr type_body = parse_expr(); - pre_type = mk_abstraction(expr_kind::Pi, parameters, type_body); - } - auto p = elaborate(pre_type); - expr type = p.first; - metavar_env menv = p.second; - if (has_metavar(type)) - type = apply_tactics(type, menv); - check_no_metavar(type, menv, "invalid variable/axiom, type still contains metavariables after elaboration"); - name full_id = mk_full_name(id); - if (is_var) - m_env->add_var(full_id, type); - else - m_env->add_axiom(full_id, type); - if (m_verbose) - regular(m_io_state) << " Assumed: " << full_id << endl; - register_implicit_arguments(full_id, parameters); -} - -/** \brief Parse one of the two forms: - - 1) 'variable' ID ':' type - - 2) 'variable' ID parameters ':' type -*/ -void parser_imp::parse_variable() { - parse_variable_core(true); -} - -/** \brief Parse the form: - 'variables' ID+ ':' type -*/ -void parser_imp::parse_variables() { - next(); - mk_scope scope(*this); - parameter_buffer parameters; - parse_simple_parameters(parameters, false, false); - for (auto p : parameters) { - name full_id = mk_full_name(p.m_name); - if (m_env->find_object(full_id)) - throw already_declared_exception(m_env, full_id); - } - for (auto p : parameters) { - name full_id = mk_full_name(p.m_name); - expr const & type = p.m_type; - m_env->add_var(full_id, type); - if (m_verbose) - regular(m_io_state) << " Assumed: " << full_id << endl; - } -} - -/** \brief Parse one of the two forms: - - 1) 'axiom' ID ':' type - - 2) 'axiom' ID parameters ':' type -*/ -void parser_imp::parse_axiom() { - parse_variable_core(false); -} - -/** \brief Parse 'Eval' expr */ -void parser_imp::parse_eval() { - next(); - expr v = elaborate(parse_expr()).first; - normalizer norm(m_env); - expr r = norm(v); - regular(m_io_state) << r << endl; -} - -/** \brief Return true iff \c obj is an object that should be ignored by the Show command */ -bool parser_imp::is_hidden_object(object const & obj) const { - return (obj.is_definition() && is_explicit(m_env, obj.get_name())) || !supported_by_pp(obj); -} - -/** \brief Parse - 'print' expr - 'print' Environment [num] - 'print' Environment all - 'print' Options - 'print' [string] -*/ -void parser_imp::parse_print() { - next(); - if (curr() == scanner::token::CommandId) { - name opt_id = curr_name(); - next(); - if (opt_id == g_env_kwd) { - buffer to_display; - bool all = false; - unsigned end = m_env->get_num_objects(false); - unsigned i; - if (curr_is_nat()) { - i = parse_unsigned("invalid argument, value does not fit in a machine integer"); - } else if (curr_is_identifier() && curr_name() == "all") { - next(); - i = std::numeric_limits::max(); - all = true; - } else { - i = std::numeric_limits::max(); - } - unsigned it = end; - unsigned num_imports = 0; - while (it != 0 && i != 0) { - --it; - auto obj = m_env->get_object(it, false); - if (is_begin_import(obj)) { - lean_assert(num_imports > 0); - num_imports--; - if (num_imports == 0) - to_display.push_back(obj); - } else if (is_begin_builtin_import(obj)) { - lean_assert(num_imports > 0); - num_imports--; - } else if (is_end_import(obj)) { - num_imports++; - } else if (is_hidden_object(obj)) { - // skip - } else if (num_imports == 0 || all) { - to_display.push_back(obj); - --i; - } - } - std::reverse(to_display.begin(), to_display.end()); - for (auto obj : to_display) { - if (is_begin_import(obj)) { - regular(m_io_state) << "import \"" << *get_imported_module(obj) << "\"" << endl; - } else { - regular(m_io_state) << obj << endl; - } - } - } else if (opt_id == g_options_kwd) { - regular(m_io_state) << pp(m_io_state.get_options()) << endl; - } else if (opt_id == g_rewrite_set_kwd) { - name rsid; - if (curr_is_identifier()) { - rsid = curr_name(); - next(); - } else { - rsid = get_default_rewrite_rule_set_id(); - } - rewrite_rule_set rs = get_rewrite_rule_set(m_env, rsid); - regular(m_io_state) << rs << endl; - } else { - throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos); - } - } else if (curr() == scanner::token::StringVal) { - std::string msg = curr_string(); - next(); - regular(m_io_state) << msg << endl; - } else { - expr v = elaborate(parse_expr()).first; - regular(m_io_state) << v << endl; - } -} - -/** \brief Parse 'Check' expr */ -void parser_imp::parse_check() { - next(); - auto p = elaborate(parse_expr()); - check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration"); - expr v = p.first; - expr t = type_check(v, m_env); - formatter fmt = m_io_state.get_formatter(); - options opts = m_io_state.get_options(); - unsigned indent = get_pp_indent(opts); - format r = group(format{fmt(v, opts), space(), colon(), nest(indent, compose(line(), fmt(t, opts)))}); - regular(m_io_state) << mk_pair(r, opts) << endl; -} - -/** \brief Return the (optional) precedence of a user-defined operator. */ -unsigned parser_imp::parse_precedence() { - if (curr_is_nat()) { - return parse_unsigned("invalid operator definition, precedence does not fit in a machine integer"); - } else { - return 0; - } -} - -/** \brief Throw an error if the current token is not an identifier. If it is, move to next token. */ -name parser_imp::parse_op_id() { - return check_identifier_next("invalid operator definition, identifier expected"); -} - -/** - \brief Parse prefix/postfix/infix/infixl/infixr user operator - definitions. These definitions have the form: - - - fixity [Num] ID ':' ID -*/ -void parser_imp::parse_op(fixity fx) { - next(); - unsigned prec = parse_precedence(); - name op_id = parse_op_id(); - check_colon_next("invalid operator definition, ':' expected"); - auto name_pos = pos(); - name name_id = check_identifier_next("invalid operator definition, identifier expected"); - expr d = get_name_ref(name_id, name_pos, false); - switch (fx) { - case fixity::Infix: add_infix(m_env, m_io_state, op_id, prec, d); break; - case fixity::Infixl: add_infixl(m_env, m_io_state, op_id, prec, d); break; - case fixity::Infixr: add_infixr(m_env, m_io_state, op_id, prec, d); break; - default: lean_unreachable(); // LCOV_EXCL_LINE - } -} - -/** - \brief Parse notation declaration unified format - - 'notation' [Num] parts ':' ID -*/ -void parser_imp::parse_notation_decl() { - auto p = pos(); - next(); - unsigned prec = parse_precedence(); - bool first = true; - bool prev_placeholder = false; - bool first_placeholder = false; - buffer parts; - while (true) { - if (first) { - if (curr_is_placeholder()) { - prev_placeholder = true; - first_placeholder = true; - next(); - } else { - parts.push_back(check_identifier_next("invalid notation declaration, identifier or '_' expected")); - prev_placeholder = false; - first_placeholder = false; - } - first = false; - } else { - if (curr_is_colon()) { - next(); - if (parts.size() == 0) { - throw parser_error("invalid notation declaration, it must have at least one identifier", p); - } - auto id_pos = pos(); - name name_id = check_identifier_next("invalid notation declaration, identifier expected"); - expr d = get_name_ref(name_id, id_pos, false); - if (parts.size() == 1) { - if (first_placeholder && prev_placeholder) { - // infix: _ ID _ - add_infix(m_env, m_io_state, parts[0], prec, d); - } else if (first_placeholder) { - // postfix: _ ID - add_postfix(m_env, m_io_state, parts[0], prec, d); - } else if (prev_placeholder) { - // prefix: ID _ - add_prefix(m_env, m_io_state, parts[0], prec, d); - } else { - throw parser_error("invalid notation declaration, at least one placeholder expected", p); - } - } else { - if (first_placeholder && prev_placeholder) { - // mixfixo: _ ID ... ID _ - add_mixfixo(m_env, m_io_state, parts.size(), parts.data(), prec, d); - } else if (first_placeholder) { - // mixfixr: _ ID ... ID - add_mixfixr(m_env, m_io_state, parts.size(), parts.data(), prec, d); - } else if (prev_placeholder) { - // mixfixl: ID _ ... ID _ - add_mixfixl(m_env, m_io_state, parts.size(), parts.data(), prec, d); - } else { - // mixfixc: ID _ ... _ ID - add_mixfixc(m_env, m_io_state, parts.size(), parts.data(), prec, d); - } - } - return; - } else { - if (prev_placeholder) { - parts.push_back(check_identifier_next("invalid notation declaration, identifier or ':' expected")); - prev_placeholder = false; - } else { - check_placeholder_next("invalid notation declaration, '_' or ':' expected"); - prev_placeholder = true; - } - } - } - } -} - -/** Parse 'set_option' [id] [value] */ -void parser_imp::parse_set_option() { - next(); - auto id_pos = pos(); - name id = check_identifier_next("invalid set options, identifier (i.e., option name) expected"); - auto decl_it = get_option_declarations().find(id); - if (decl_it == get_option_declarations().end()) { - // add "lean" prefix - name lean_id = name("lean") + id; - decl_it = get_option_declarations().find(lean_id); - if (decl_it == get_option_declarations().end()) { - throw parser_error(sstream() << "unknown option '" << id << "', type 'help options.' for list of available options", id_pos); - } else { - id = lean_id; - } - } - option_kind k = decl_it->second.kind(); - switch (curr()) { - case scanner::token::Id: - if (k != BoolOption) - throw parser_error(sstream() << "invalid option value, given option is not Boolean", pos()); - if (curr_name() == "true") - m_io_state.set_option(id, true); - else if (curr_name() == "false") - m_io_state.set_option(id, false); - else - throw parser_error("invalid Boolean option value, 'true' or 'false' expected", pos()); - next(); - break; - case scanner::token::StringVal: - if (k != StringOption) - throw parser_error("invalid option value, given option is not a string", pos()); - m_io_state.set_option(id, curr_string()); - next(); - break; - case scanner::token::IntVal: - if (k != IntOption && k != UnsignedOption) - throw parser_error("invalid option value, given option is not an integer", pos()); - m_io_state.set_option(id, parse_unsigned("invalid option value, value does not fit in a machine integer")); - break; - case scanner::token::DecimalVal: - if (k != DoubleOption) - throw parser_error("invalid option value, given option is not floating point value", pos()); - m_io_state.set_option(id, parse_double()); - break; - default: - throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", pos()); - } - updt_options(); - if (m_verbose) - regular(m_io_state) << " Set: " << id << endl; -} - -/** Parse 'set_opaque' [id] [true/false] */ -void parser_imp::parse_set_opaque() { - next(); - auto p = pos(); - name id; - if (curr() == scanner::token::Exists) { - id = "exists"; - } else { - check_identifier("invalid set opaque, identifier expected"); - id = curr_name(); - } - next(); - expr d = get_name_ref(id, p, false); - name real_id; - if (is_constant(d)) - real_id = const_name(d); - else if (is_value(d)) - real_id = to_value(d).get_name(); - else - throw parser_error(sstream() << "invalid set opaque, identifier '" << id << "' cannot be set opaque", p); - auto val_pos = pos(); - name val = check_identifier_next("invalid opaque flag, true/false expected"); - if (val == "true") - m_env->set_opaque(real_id, true); - else if (val == "false") - m_env->set_opaque(real_id, false); - else - throw parser_error("invalid opaque flag, true/false expected", val_pos); -} - -optional parser_imp::find_lua_file(std::string const & fname) { - try { - return some(find_file(fname, {".lua"})); - } catch (...) { - return optional(); - } -} - -void parser_imp::parse_import() { - auto p = pos(); - next(); - unsigned num = 0; - while (curr_is_identifier() || curr_is_string()) { - std::string fname; - if (curr_is_identifier()) { - fname = name_to_file(curr_name()); - next(); - } else { - fname = curr_string(); - next(); - } - bool r = false; - if (auto lua_fname = find_lua_file(fname)) { - if (!m_script_state) - throw parser_error(sstream() << "failed to import Lua file '" << *lua_fname << "', parser does not have an intepreter", - m_last_cmd_pos); - r = m_script_state->import_explicit(lua_fname->c_str()); - } else { - r = m_env->import(fname, m_io_state); - } - if (m_verbose && r) { - regular(m_io_state) << " Imported '" << fname << "'" << endl; - } - num++; - } - if (num == 0) - throw parser_error("invalid import command, string (i.e., file name) or identifier expected", p); -} - -void parser_imp::parse_help() { - next(); - if (curr() == scanner::token::CommandId) { - name opt_id = curr_name(); - next(); - if (opt_id == g_options_kwd) { - regular(m_io_state) << "Available options:" << endl; - for (auto p : get_option_declarations()) { - auto opt = p.second; - regular(m_io_state) << " " << opt.get_name() << " (" << opt.kind() << ") " - << opt.get_description() << " (default: " << opt.get_default_value() << ")" << endl; - } - } else { - throw parser_error("invalid help command", m_last_cmd_pos); - } - } else { - regular(m_io_state) << "Available commands:" << endl - << " alias [id] : [expr] define an alias for the given expression" << endl - << " axiom [id] : [type] assert/postulate a new axiom" << endl - << " check [expr] type check the given expression" << endl - << " definition [id] : [type] := [expr] define a new element" << endl - << " end end the current scope/namespace" << endl - << " eval [expr] evaluate the given expression" << endl - << " exit exit" << endl - << " help display this message" << endl - << " help options display available options" << endl - << " help notation describe commands for defining infix, mixfix, postfix operators" << endl - << " import [string] load the given file" << endl - << " pop::scope discard the current scope" << endl - << " print [expr] pretty print the given expression" << endl - << " print Options print current the set of assigned options" << endl - << " print [string] print the given string" << endl - << " print Environment print objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl - << " print Environment [num] show the last num objects in the environment" << endl - << " scope create a scope" << endl - << " set::option [id] [value] set option [id] with value [value]" << endl - << " set::opaque [id] [bool] set the given definition as opaque/transparent" << endl - << " theorem [id] : [type] := [expr] define a new theorem" << endl - << " variable [id] : [type] declare/postulate an element of the given type" << endl - << " universe [id] >= [level] declare a new universe constraint" << endl - << " using [id]_1 [id]_2? create an alias for object starting with the prefix [id]_1 using the [id]_2" << endl; -#if !defined(LEAN_WINDOWS) - regular(m_io_state) << "Type Ctrl-D to exit" << endl; -#endif -} -} - -/** \brief Parse 'Coercion' expr */ -void parser_imp::parse_coercion() { - next(); - expr coercion = parse_expr(); - add_coercion(m_env, coercion); - if (m_verbose) - regular(m_io_state) << " Coercion " << coercion << endl; -} - -void parser_imp::reset_env(environment env) { - m_env = env; - m_elaborator.reset(env); - m_io_state.set_formatter(mk_pp_formatter(env)); -} - -void parser_imp::parse_cmd_macro(name cmd_id, pos_info const & p) { - lean_assert(m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()); - next(); - auto m = m_cmd_macros->find(cmd_id)->second; - macro_arg_stack args; - parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p); -} - -static name g_geq_unicode("\u2265"); // ≥ -static name g_geq(">="); - -void parser_imp::parse_universe() { - next(); - name id = check_identifier_next("invalid universe constraint, identifier expected"); - if (curr_is_identifier()) { - name geq = check_identifier_next("invalid universe constraint, '>=' expected"); - if (geq != g_geq && geq != g_geq_unicode) - throw parser_error("invalid universe constraint, '>=' expected", m_last_cmd_pos); - level lvl = parse_level(); - m_env->add_uvar_cnstr(id, lvl); - } else { - m_env->add_uvar_cnstr(id); - } -} - -void parser_imp::parse_alias() { - next(); - name id = check_identifier_next("invalid alias declaration, identifier expected"); - check_colon_next("invalid alias declaration, ':' expected"); - expr e = parse_expr(); - add_alias(m_env, id, e); -} - -void parser_imp::parse_builtin() { - next(); - auto id_pos = pos(); - name id = check_identifier_next("invalid builtin declaration, identifier expected"); - name full_id = mk_full_name(id); - auto d = get_builtin(full_id); - if (!d) - throw parser_error(sstream() << "unknown builtin '" << full_id << "'", id_pos); - expr b = d->first; - if (d->second) { - m_env->add_builtin_set(b); - return; - } - parameter_buffer parameters; - expr type; - if (curr_is_colon()) { - next(); - auto p = elaborate(parse_expr()); - check_no_metavar(p, "invalid builtin declaration, type still contains metavariables after elaboration"); - type = p.first; - } else { - mk_scope scope(*this); - parse_var_decl_parameters(parameters); - check_colon_next("invalid builtin declaration, ':' expected"); - expr type_body = parse_expr(); - auto p = elaborate(mk_abstraction(expr_kind::Pi, parameters, type_body)); - check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration"); - type = p.first; - } - if (to_value(b).get_type() != type) { - diagnostic(m_io_state) << "Error, builtin expected type: " << to_value(b).get_type() << ", given: " << type << "\n"; - throw parser_error(sstream() << "given type does not match builtin type", id_pos); - } - m_env->add_builtin(d->first); - if (m_verbose) - regular(m_io_state) << " Added: " << full_id << endl; - register_implicit_arguments(full_id, parameters); -} - -void parser_imp::parse_scope() { - next(); - m_scope_kinds.push_back(scope_kind::Scope); - reset_env(m_env->mk_child()); - m_using_decls.push(); -} - -void parser_imp::parse_pop() { - next(); - if (m_scope_kinds.empty()) - throw parser_error("main scope cannot be removed", m_last_cmd_pos); - if (m_scope_kinds.back() != scope_kind::Scope) - throw parser_error("invalid pop command, it is not inside of a scope", m_last_cmd_pos); - if (!m_env->has_parent()) - throw parser_error("main scope cannot be removed", m_last_cmd_pos); - m_scope_kinds.pop_back(); - reset_env(m_env->parent()); - m_using_decls.pop(); - m_script_state->apply([&](lua_State * L) { lua_gc(L, LUA_GCCOLLECT, 0); }); -} - -void parser_imp::parse_namespace() { - next(); - name id = check_identifier_next("invalid namespace declaration, identifier expected"); - m_scope_kinds.push_back(scope_kind::Namespace); - m_namespace_prefixes.push_back(m_namespace_prefixes.back() + id); - m_using_decls.push(); -} - -void parser_imp::parse_end() { - next(); - if (m_scope_kinds.empty()) - throw parser_error("invalid 'end', not inside of a scope or namespace", m_last_cmd_pos); - scope_kind k = m_scope_kinds.back(); - m_scope_kinds.pop_back(); - m_script_state->apply([&](lua_State * L) { lua_gc(L, LUA_GCCOLLECT, 0); }); - switch (k) { - case scope_kind::Scope: { - if (!m_env->has_parent()) - throw parser_error("main scope cannot be removed", m_last_cmd_pos); - auto new_objects = export_local_objects(m_env); - reset_env(m_env->parent()); - for (auto const & obj : new_objects) { - if (obj.is_theorem()) - m_env->add_theorem(obj.get_name(), obj.get_type(), obj.get_value()); - else - m_env->add_definition(obj.get_name(), obj.get_type(), obj.get_value(), obj.is_opaque()); - } - break; - } - case scope_kind::Namespace: - if (m_namespace_prefixes.size() <= 1) - throw parser_error("invalid end namespace command, there are no open namespaces", m_last_cmd_pos); - m_namespace_prefixes.pop_back(); - } - m_using_decls.pop(); -} - -static name replace_prefix(name const & n, name const & prefix, name const & new_prefix) { - if (n == prefix) - return new_prefix; - name p = replace_prefix(n.get_prefix(), prefix, new_prefix); - if (n.is_string()) - return name(p, n.get_string()); - else - return name(p, n.get_numeral()); -} - -void parser_imp::parse_using() { - next(); - name prefix = check_identifier_next("invalid using command, identifier expected"); - name new_prefix; - if (curr_is_identifier()) { - new_prefix = curr_name(); - next(); - } - buffer> to_add; - for (auto it = m_env->begin_objects(); it != m_env->end_objects(); ++it) { - if (it->has_type() && it->has_name() && supported_by_pp(*it) && is_prefix_of(prefix, it->get_name())) { - auto n = replace_prefix(it->get_name(), prefix, new_prefix); - if (!n.is_anonymous()) - to_add.emplace_back(n, it->get_name()); - } - } - for (auto p : to_add) { - auto n = p.first; - if (m_verbose) { - auto it = m_using_decls.find(n); - if (it != m_using_decls.end()) - diagnostic(m_io_state) << "warning: " << n << " will shadow " << it->second << endl; - auto obj = m_env->find_object(n); - if (obj && n != obj->get_name()) - diagnostic(m_io_state) << "warning: " << n << " will shadow " << obj->get_name() << endl; - } - m_using_decls.insert(n, p.second); - } - if (m_verbose) - regular(m_io_state) << " Using: " << prefix; - if (new_prefix) - regular(m_io_state) << " as " << new_prefix; - regular(m_io_state) << endl; -} - -void parser_imp::parse_rewrite_set() { - next(); - name id = check_identifier_next("invalid rewrite set declaration, identifier expected"); - mk_rewrite_rule_set(m_env, id); -} - -void parser_imp::parse_ids_and_rsid(buffer & ids, name & rsid) { - while (curr_is_identifier()) { - auto p = pos(); - name id = curr_name(); - expr d = get_name_ref(id, p, false); - if (is_constant(d)) - ids.push_back(const_name(d)); - else if (is_value(d)) - ids.push_back(to_value(d).get_name()); - else - throw parser_error(sstream() << "'" << id << "' does not name a theorem or axiom", p); - next(); - } - if (ids.empty()) - throw parser_error("invalid command, at least one identifier expected", m_last_cmd_pos); - if (curr_is_colon()) { - next(); - rsid = check_identifier_next("invalid command, rewrite set name expected"); - } else { - rsid = get_default_rewrite_rule_set_id(); - } -} - -void parser_imp::parse_add_rewrite() { - next(); - buffer th_names; - name rsid; - parse_ids_and_rsid(th_names, rsid); - for (auto id : th_names) { - add_rewrite_rules(m_env, rsid, id); - } -} - -void parser_imp::parse_enable_rewrite(bool flag) { - next(); - buffer ids; - name rsid; - parse_ids_and_rsid(ids, rsid); - for (auto id : ids) { - enable_rewrite_rules(m_env, rsid, id, flag); - } -} - -/** \brief Parse a Lean command. */ -bool parser_imp::parse_command() { - m_elaborator.clear(); - m_expr_pos_info.clear(); - m_tactic_hints.clear(); - m_last_cmd_pos = pos(); - name const & cmd_id = curr_name(); - if (cmd_id == g_definition_kwd) { - parse_definition(); - } else if (cmd_id == g_variable_kwd) { - parse_variable(); - } else if (cmd_id == g_variables_kwd) { - parse_variables(); - } else if (cmd_id == g_theorem_kwd) { - parse_theorem(); - } else if (cmd_id == g_axiom_kwd) { - parse_axiom(); - } else if (cmd_id == g_eval_kwd) { - parse_eval(); - } else if (cmd_id == g_print_kwd) { - parse_print(); - } else if (cmd_id == g_check_kwd) { - parse_check(); - } else if (cmd_id == g_infix_kwd) { - parse_op(fixity::Infix); - } else if (cmd_id == g_infixl_kwd) { - parse_op(fixity::Infixl); - } else if (cmd_id == g_infixr_kwd) { - parse_op(fixity::Infixr); - } else if (cmd_id == g_notation_kwd) { - parse_notation_decl(); - } else if (cmd_id == g_set_option_kwd) { - parse_set_option(); - } else if (cmd_id == g_set_opaque_kwd) { - parse_set_opaque(); - } else if (cmd_id == g_import_kwd) { - parse_import(); - } else if (cmd_id == g_help_kwd) { - parse_help(); - } else if (cmd_id == g_coercion_kwd) { - parse_coercion(); - } else if (cmd_id == g_exit_kwd) { - next(); - return false; - } else if (cmd_id == g_scope_kwd) { - parse_scope(); - } else if (cmd_id == g_pop_kwd) { - parse_pop(); - } else if (cmd_id == g_universe_kwd) { - parse_universe(); - } else if (cmd_id == g_alias_kwd) { - parse_alias(); - } else if (cmd_id == g_builtin_kwd) { - parse_builtin(); - } else if (cmd_id == g_namespace_kwd) { - parse_namespace(); - } else if (cmd_id == g_end_kwd) { - parse_end(); - } else if (cmd_id == g_using_kwd) { - parse_using(); - } else if (cmd_id == g_rewrite_set_kwd) { - parse_rewrite_set(); - } else if (cmd_id == g_add_rewrite_kwd) { - parse_add_rewrite(); - } else if (cmd_id == g_enable_rewrite_kwd) { - parse_enable_rewrite(true); - } else if (cmd_id == g_disable_rewrite_kwd) { - parse_enable_rewrite(false); - } else if (m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()) { - parse_cmd_macro(cmd_id, m_last_cmd_pos); - } else { - next(); - throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos); - } - return true; -} -} diff --git a/src/frontends/lean/parser_error.cpp b/src/frontends/lean/parser_error.cpp deleted file mode 100644 index 7948c4e7d..000000000 --- a/src/frontends/lean/parser_error.cpp +++ /dev/null @@ -1,98 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "kernel/for_each_fn.h" -#include "library/io_state_stream.h" -#include "library/parser_nested_exception.h" -#include "library/error_handling/error_handling.h" -#include "frontends/lean/parser_imp.h" - -namespace lean { -void parser_imp::display_error_pos(unsigned line, unsigned pos) { - regular(m_io_state) << m_strm_name << ":" << line << ":"; - if (pos != static_cast(-1)) - regular(m_io_state) << pos << ":"; - regular(m_io_state) << " error:"; -} - -void parser_imp::display_error_pos(pos_info const & p) { display_error_pos(p.first, p.second); } - -void parser_imp::display_error(char const * msg, unsigned line, unsigned pos) { - display_error_pos(line, pos); - regular(m_io_state) << " " << msg << endl; -} - -std::pair parser_imp::lean_pos_info_provider::get_pos_info(expr const & e) const { - expr const & o = m_parser->m_elaborator.get_original(e); - auto it = m_parser->m_expr_pos_info.find(o); - if (it == m_parser->m_expr_pos_info.end()) - return m_pos; - return it->second; -} - -char const * parser_imp::lean_pos_info_provider::get_file_name() const { - return m_parser->m_strm_name.c_str(); -} - -void parser_imp::display_error(tactic_cmd_error const & ex) { - display_error(ex.what(), ex.m_pos.first, ex.m_pos.second); - display_proof_state(ex.m_state); -} - -void parser_imp::display_error(exception const & ex) { - lean_pos_info_provider pos_provider(m_this.lock(), m_last_cmd_pos); - ::lean::display_error(m_io_state, &pos_provider, ex); -} - -void parser_imp::display_error(script_exception const & ex) { - lean_pos_info_provider pos_provider(m_this.lock(), m_last_script_pos); - ::lean::display_error(m_io_state, &pos_provider, ex); -} - -#define CATCH(ShowError, ThrowError) \ -m_found_errors = true; \ -if (!m_use_exceptions && m_show_errors) { ShowError ; } \ -sync(); \ -if (m_use_exceptions) { ThrowError ; } - -/** - \brief Execute the given function \c f, and handle exceptions occurring - when executing \c f. - The parameter \c s is an error synchronization procedure. -*/ -void parser_imp::protected_call(std::function && f, std::function && sync) { - try { - f(); - } catch (tactic_cmd_error & ex) { - CATCH(display_error(ex), - throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second)); - } catch (parser_exception & ex) { - CATCH(regular(m_io_state) << ex.what() << endl, - throw); - } catch (parser_error & ex) { - CATCH(display_error(ex.what(), ex.m_pos.first, ex.m_pos.second), - throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second)); - } catch (interrupted & ex) { - reset_interrupt(); - if (m_verbose) - regular(m_io_state) << "!!!Interrupted!!!" << endl; - sync(); - if (m_use_exceptions) - throw; - } catch (script_exception & ex) { - reset_interrupt(); - CATCH(display_error(ex), - throw parser_nested_exception(std::shared_ptr(ex.clone()), - std::shared_ptr(new lean_pos_info_provider(m_this.lock(), m_last_script_pos)))); - } catch (exception & ex) { - reset_interrupt(); - CATCH(display_error(ex), - throw parser_nested_exception(std::shared_ptr(ex.clone()), - std::shared_ptr(new lean_pos_info_provider(m_this.lock(), m_last_cmd_pos)))); - } -} -} diff --git a/src/frontends/lean/parser_error.h b/src/frontends/lean/parser_error.h deleted file mode 100644 index 053917308..000000000 --- a/src/frontends/lean/parser_error.h +++ /dev/null @@ -1,32 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/exception.h" -#include "kernel/expr.h" -#include "kernel/context.h" -#include "library/tactic/proof_state.h" -#include "frontends/lean/parser_types.h" - -namespace lean { -/** \brief Exception used to track parsing erros, it does not leak outside of this class. */ -struct parser_error : public exception { - pos_info m_pos; - parser_error(char const * msg, pos_info const & p):exception(msg), m_pos(p) {} - parser_error(sstream const & msg, pos_info const & p):exception(msg), m_pos(p) {} - virtual exception * clone() const { return new parser_error(m_msg.c_str(), m_pos); } - virtual void rethrow() const { throw *this; } -}; - -/** \brief Exception used to report error in the tactic frontend available in the Lean parser. */ -struct tactic_cmd_error : public parser_error { - proof_state m_state; - tactic_cmd_error(char const * msg, pos_info const & p, proof_state const & s):parser_error(msg, p), m_state(s) {} - tactic_cmd_error(sstream const & msg, pos_info const & p, proof_state const & s):parser_error(msg, p), m_state(s) {} - virtual exception * clone() const { return new tactic_cmd_error(m_msg.c_str(), m_pos, m_state); } - virtual void rethrow() const { throw *this; } -}; -} diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp deleted file mode 100644 index 0c642e214..000000000 --- a/src/frontends/lean/parser_expr.cpp +++ /dev/null @@ -1,1112 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include "util/flet.h" -#include "util/sstream.h" -#include "kernel/for_each_fn.h" -#include "kernel/free_vars.h" -#include "kernel/kernel.h" -#include "library/placeholder.h" -#include "library/io_state_stream.h" -#include "library/arith/nat.h" -#include "library/arith/int.h" -#include "library/arith/real.h" -#include "frontends/lean/parser_imp.h" -#include "frontends/lean/frontend.h" -#include "frontends/lean/notation.h" -#include "frontends/lean/parser_calc.h" - -namespace lean { -// A name that can't be created by the user. -// It is used as placeholder for parsing A -> B expressions which -// are syntax sugar for (Pi (_ : A), B) -static name g_unused = name::mk_internal_unique_name(); -static name g_calc("calc"); - -/** - \brief Return the size of the implicit vector associated with the given denotation. -*/ -unsigned parser_imp::get_implicit_vector_size(expr const & d) { - return get_implicit_arguments(m_env, d).size(); -} - -/** - \brief Return a vector \c v that is the implicit vector for some \c d in \c ds, - and v.size() == min{get_implicit_vector_size(d) | d in ds} -*/ -std::vector const & parser_imp::get_smallest_implicit_vector(list const & ds) { - std::vector const * r = nullptr; - unsigned m = std::numeric_limits::max(); - for (expr const & d : ds) { - std::vector const & v = get_implicit_arguments(m_env, d); - unsigned s = v.size(); - if (s == 0) { - return v; - } else if (s < m) { - r = &v; - m = s; - } - } - lean_assert(r); - return *r; -} - -/** - \brief Return min{get_implicit_vector_size(d) | d in ds} -*/ -unsigned parser_imp::get_smallest_implicit_vector_size(list const & ds) { - return get_smallest_implicit_vector(ds).size(); -} - -/** - \brief Return the function associated with the given operator. - If the operator has been overloaded, it returns a choice expression - of the form (choice f_1 f_2 ... f_k) where f_i's are different options. - After we finish parsing, the elaborator - resolve/decide which f_i should be used. -*/ -expr parser_imp::mk_fun(operator_info const & op, pos_info const & pos) { - list const & fs = op.get_denotations(); - lean_assert(!is_nil(fs)); - auto it = fs.begin(); - expr r = *it; - ++it; - if (it == fs.end()) { - return r; - } else { - unsigned min_sz = get_smallest_implicit_vector_size(fs); - buffer alternatives; - auto add_alternative = [&](expr const & d) { - unsigned sz = get_implicit_vector_size(d); - if (sz > min_sz) { - // must fill the difference with placeholders - buffer aux; - aux.push_back(d); - for (unsigned i = min_sz; i < sz; i++) - aux.push_back(save(mk_placeholder(), pos)); - alternatives.push_back(mk_app(aux)); - } else { - alternatives.push_back(d); - } - }; - add_alternative(r); - for (; it != fs.end(); ++it) - add_alternative(*it); - return mk_choice(alternatives.size(), alternatives.data()); - } -} - -/** - \brief Create an application for the given operator and - (explicit) arguments. -*/ -expr parser_imp::mk_application(operator_info const & op, pos_info const & pos, unsigned num_args, expr const * args) { - buffer new_args; - expr f = save(mk_fun(op, pos), pos); - new_args.push_back(f); - // See lean_frontend.cpp for the definition of compatible denotations. - auto imp_args = get_smallest_implicit_vector(op.get_denotations()); - unsigned i = 0; - for (unsigned j = 0; j < imp_args.size(); j++) { - if (imp_args[j]) { - new_args.push_back(save(mk_placeholder(), pos)); - } else { - if (i >= num_args) - throw parser_error(sstream() << "unexpected number of arguments for denotation with implicit arguments, it expects " << num_args << " explicit argument(s)", pos); - new_args.push_back(args[i]); - i++; - } - } - for (; i < num_args; i++) - new_args.push_back(args[i]); - return save(mk_app(new_args), pos); -} - -expr parser_imp::mk_application(operator_info const & op, pos_info const & pos, std::initializer_list const & l) { - return mk_application(op, pos, l.size(), l.begin()); -} -expr parser_imp::mk_application(operator_info const & op, pos_info const & pos, expr const & arg) { - return mk_application(op, pos, 1, &arg); -} -expr parser_imp::mk_application(operator_info const & op, pos_info const & pos, buffer const & args) { - return mk_application(op, pos, args.size(), args.data()); -} - -/** \brief Parse a user defined prefix operator. */ -expr parser_imp::parse_prefix(operator_info const & op) { - auto p = pos(); - return mk_application(op, p, parse_expr(op.get_precedence())); -} - -/** \brief Parse a user defined postfix operator. */ -expr parser_imp::parse_postfix(expr const & left, operator_info const & op, pos_info const & op_pos) { - return mk_application(op, op_pos, left); -} - -/** \brief Parse a user defined infix operator. */ -expr parser_imp::parse_infix(expr const & left, operator_info const & op, pos_info const & op_pos) { - expr right = parse_expr(op.get_precedence()+1); - return mk_application(op, op_pos, {left, right}); -} - -/** \brief Parse a user defined infix-left operator. */ -expr parser_imp::parse_infixl(expr const & left, operator_info const & op, pos_info const & op_pos) { - expr right = parse_expr(op.get_precedence()); - return mk_application(op, op_pos, {left, right}); -} - -/** \brief Parse a user defined infix-right operator. */ -expr parser_imp::parse_infixr(expr const & left, operator_info const & op, pos_info const & op_pos) { - expr right = parse_expr(op.get_precedence()-1); - return mk_application(op, op_pos, {left, right}); -} - -/** - \brief Throws an error if the current token is not an identifier named \c op_part. - If it is, move to the next toke. The error message assumes - this method has been used when parsing mixfix operators. -*/ -void parser_imp::check_op_part(name const & op_part) { - if (!curr_is_identifier() || curr_name() != op_part) - throw parser_error(sstream() << "invalid mixfix operator application, '" << op_part << "' expected", pos()); - next(); -} - -/** - \brief Auxiliary function for #parse_mixfixl and #parse_mixfixo - - It parses (ID _)* -*/ -void parser_imp::parse_mixfix_args(list const & ops, unsigned prec, buffer & args) { - auto it = ops.begin(); - ++it; - while (it != ops.end()) { - check_op_part(*it); - args.push_back(parse_expr(prec)); - ++it; - } -} - -/** \brief Parse user defined mixfixl operator. It has the form: ID _ ... ID _ */ -expr parser_imp::parse_mixfixl(operator_info const & op) { - auto p = pos(); - buffer args; - args.push_back(parse_expr(op.get_precedence())); - parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); - return mk_application(op, p, args); -} - -/** \brief Parse user defined mixfixr operator. It has the form: _ ID ... _ ID */ -expr parser_imp::parse_mixfixr(expr const & left, operator_info const & op, pos_info const & op_pos) { - buffer args; - args.push_back(left); - auto parts = op.get_op_name_parts(); - auto it = parts.begin(); - ++it; - while (it != parts.end()) { - args.push_back(parse_expr(op.get_precedence())); - check_op_part(*it); - ++it; - } - return mk_application(op, op_pos, args); -} - -/** \brief Parse user defined mixfixr operator. It has the form: _ ID ... _ ID _ */ -expr parser_imp::parse_mixfixo(expr const & left, operator_info const & op, pos_info const & op_pos) { - buffer args; - args.push_back(left); - args.push_back(parse_expr(op.get_precedence())); - parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); - return mk_application(op, op_pos, args); -} - -/** \brief Parse user defined mixfixc operator. It has the form: ID _ ID ... _ ID */ -expr parser_imp::parse_mixfixc(operator_info const & op) { - auto p = pos(); - buffer args; - args.push_back(parse_expr(op.get_precedence())); - list const & ops = op.get_op_name_parts(); - auto it = ops.begin(); - ++it; - while (true) { - check_op_part(*it); - ++it; - if (it == ops.end()) - return mk_application(op, p, args); - args.push_back(parse_expr(op.get_precedence())); - } -} - -expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit_args) { - auto it = m_using_decls.find(id); - if (it != m_using_decls.end()) { - return get_name_ref(it->second, p, implicit_args); - } else { - lean_assert(!m_namespace_prefixes.empty()); - auto it = m_namespace_prefixes.end(); - auto begin = m_namespace_prefixes.begin(); - while (it != begin) { - --it; - name nid = *it + id; - optional obj = m_env->find_object(nid); - if (obj) { - expr f = obj->is_builtin() ? obj->get_value() : mk_constant(obj->get_name()); - object_kind k = obj->kind(); - if (k == object_kind::Definition || k == object_kind::Postulate || k == object_kind::Builtin) { - if (implicit_args && has_implicit_arguments(m_env, obj->get_name())) { - std::vector const & imp_args = get_implicit_arguments(m_env, obj->get_name()); - buffer args; - pos_info p = pos(); - args.push_back(save(f, p)); - for (unsigned i = 0; i < imp_args.size(); i++) { - if (imp_args[i]) { - args.push_back(save(mk_placeholder(), pos())); - } else { - args.push_back(parse_expr(g_app_precedence)); - } - } - return mk_app(args); - } else { - return f; - } - } else { - throw parser_error(sstream() << "invalid object reference, object '" << nid << "' is not an expression.", p); - } - } else if (!m_check_identifiers) { - return mk_constant(nid); - } - } - } - throw parser_error(sstream() << "unknown identifier '" << id << "'", p); -} - -void parser_imp::propagate_position(expr const & e, pos_info p) { - for_each(e, [&](expr const & e, unsigned) { - if (m_expr_pos_info.find(e) == m_expr_pos_info.end()) { - save(e, p); - return true; - } else { - return false; // do not search children... - } - }); -} - -bool parser_imp::is_curr_begin_expr() const { - switch (curr()) { - case scanner::token::RightParen: - case scanner::token::RightCurlyBracket: - case scanner::token::Colon: - case scanner::token::Comma: - case scanner::token::Period: - case scanner::token::CommandId: - case scanner::token::Eof: - case scanner::token::ScriptBlock: - case scanner::token::In: - return false; - default: - return true; - } -} - -bool parser_imp::is_curr_begin_tactic() const { - switch (curr()) { - case scanner::token::LeftParen: case scanner::token::Id: return true; - default: return false; - } -} - -/** - \brief Parse a macro implemented in Lua -*/ -parser_imp::macro_result parser_imp::parse_macro(list const & arg_kinds, luaref const & fn, unsigned prec, macro_arg_stack & args, - pos_info const & p) { - if (arg_kinds) { - auto k = head(arg_kinds); - switch (k) { - case macro_arg_kind::Expr: { - expr e = parse_expr(prec); - args.emplace_back(k, &e); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Exprs: { - buffer exprs; - while (is_curr_begin_expr()) { - exprs.push_back(parse_expr(prec)); - } - args.emplace_back(k, &exprs); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Parameters: { - mk_scope scope(*this); - parameter_buffer parameters; - parse_expr_parameters(parameters); - args.emplace_back(k, ¶meters); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Comma: - check_comma_next("invalid macro, ',' expected"); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - case macro_arg_kind::Assign: - check_comma_next("invalid macro, ':=' expected"); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - case macro_arg_kind::String: { - std::string str = check_string_next("invalid macro, string expected"); - args.emplace_back(k, &str); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Int: { - unsigned i = parse_unsigned("invalid macro argument, value does not fit in a machine integer"); - args.emplace_back(k, &i); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Id: { - name n = curr_name(); - next(); - args.emplace_back(k, &n); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Ids: { - buffer ns; - args.emplace_back(k, &ns); - while (curr_is_identifier()) { - ns.push_back(curr_name()); - next(); - } - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Tactic: { - tactic t = parse_tactic_expr(); - args.emplace_back(k, &t); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - } - case macro_arg_kind::Tactics: { - buffer tactics; - while (is_curr_begin_tactic()) { - tactics.push_back(parse_tactic_expr()); - } - args.emplace_back(k, &tactics); - return parse_macro(tail(arg_kinds), fn, prec, args, p); - }} - lean_unreachable(); - } else { - // All arguments have been parsed, then call Lua procedure fn. - m_last_script_pos = p; - return using_script([&](lua_State * L) { - fn.push(); - push_environment(L, m_env); - for (auto p : args) { - macro_arg_kind k = p.first; - void * arg = p.second; - switch (k) { - case macro_arg_kind::Expr: - push_expr(L, *static_cast(arg)); - break; - case macro_arg_kind::Exprs: { - auto const & exprs = *static_cast*>(arg); - lua_newtable(L); - int i = 1; - for (auto e : exprs) { - push_expr(L, e); - lua_rawseti(L, -2, i); - i = i + 1; - } - break; - } - case macro_arg_kind::Parameters: { - parameter_buffer const & parameters = *static_cast(arg); - lua_newtable(L); - int i = 1; - for (auto const & p : parameters) { - lua_newtable(L); - push_name(L, p.m_name); - lua_rawseti(L, -2, 1); - push_expr(L, p.m_type); - lua_rawseti(L, -2, 2); - lua_rawseti(L, -2, i); - i = i + 1; - } - break; - } - case macro_arg_kind::Id: - push_name(L, *static_cast(arg)); - break; - case macro_arg_kind::Ids: { - buffer const & ids = *static_cast*>(arg); - lua_newtable(L); - int i = 1; - for (auto const & id : ids) { - push_name(L, id); - lua_rawseti(L, -2, i); - i = i + 1; - } - break; - } - case macro_arg_kind::String: - lua_pushstring(L, static_cast(arg)->c_str()); - break; - case macro_arg_kind::Int: - lua_pushinteger(L, *static_cast(arg)); - break; - case macro_arg_kind::Tactic: - push_tactic(L, *static_cast(arg)); - break; - case macro_arg_kind::Tactics: { - auto const & tactics = *static_cast*>(arg); - lua_newtable(L); - int i = 1; - for (auto t : tactics) { - push_tactic(L, t); - lua_rawseti(L, -2, i); - i = i + 1; - } - break; - } - default: - lean_unreachable(); - } - } - pcall(L, args.size() + 1, 1, 0); - if (is_expr(L, -1)) { - expr r = to_expr(L, -1); - lua_pop(L, 1); - propagate_position(r, p); - return macro_result(r); - } else if (is_tactic(L, -1)) { - tactic t = to_tactic(L, -1); - lua_pop(L, 1); - return macro_result(t); - } else { - lua_pop(L, 1); - return macro_result(); - } - }); - } -} - -expr parser_imp::parse_expr_macro(name const & id, pos_info const & p) { - lean_assert(m_expr_macros && m_expr_macros->find(id) != m_expr_macros->end()); - auto m = m_expr_macros->find(id)->second; - macro_arg_stack args; - auto r = parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p); - if (r.m_expr) { - return *(r.m_expr); - } else { - throw parser_error("failed to execute macro, unexpected result type", p); - } -} - -expr parser_imp::parse_calc() { - return get_calc_proof_parser().parse(*this); -} - -/** - \brief Parse an identifier that has a "null denotation" (See - paper: "Top down operator precedence"). A nud identifier is a - token that appears at the beginning of a language construct. - In Lean, local declarations (i.e., local functions), user - defined prefix, mixfixl and mixfixc operators, and global - functions can begin a language construct. -*/ -expr parser_imp::parse_nud_id() { - auto p = pos(); - name id = curr_name(); - next(); - auto it = m_local_decls.find(id); - if (it != m_local_decls.end()) { - return save(mk_var(m_num_local_decls - it->second - 1), p); - } else if (m_expr_macros && m_expr_macros->find(id) != m_expr_macros->end()) { - return parse_expr_macro(id, p); - } else if (auto alias = get_alias(m_env, id)) { - return save(*alias, p); - } else if (id == g_calc) { - return parse_calc(); - } else { - operator_info op = find_nud(m_env, id); - if (op) { - switch (op.get_fixity()) { - case fixity::Prefix: return parse_prefix(op); - case fixity::Mixfixl: return parse_mixfixl(op); - case fixity::Mixfixc: return parse_mixfixc(op); - default: lean_unreachable(); // LCOV_EXCL_LINE - } - } else { - return save(get_name_ref(id, p), p); - } - } -} - -/** - \brief Parse an identifier that has a "left denotation" (See - paper: "Top down operator precedence"). A left identifier is a - token that appears inside of a construct (to left of the rest - of the construct). In Lean, local declarations (i.e., function - application arguments), user defined infix, infixl, infixr, - mixfixr and global values (as function application arguments) - can appear inside of a construct. -*/ -expr parser_imp::parse_led_id(expr const & left) { - auto p = pos(); - auto p2 = pos_of(left, p); - name id = curr_name(); - next(); - auto it = m_local_decls.find(id); - if (it != m_local_decls.end()) { - return save(mk_app(left, save(mk_var(m_num_local_decls - it->second - 1), p)), p2); - } else if (m_expr_macros && m_expr_macros->find(id) != m_expr_macros->end()) { - return save(mk_app(left, parse_expr_macro(id, p)), p2); - } else if (auto alias = get_alias(m_env, id)) { - return save(mk_app(left, save(*alias, p)), p2); - } else if (id == g_calc) { - return save(mk_app(left, parse_calc()), p2); - } else { - operator_info op = find_led(m_env, id); - if (op) { - switch (op.get_fixity()) { - case fixity::Infix: return parse_infix(left, op, p); - case fixity::Infixl: return parse_infixl(left, op, p); - case fixity::Infixr: return parse_infixr(left, op, p); - case fixity::Mixfixr: return parse_mixfixr(left, op, p); - case fixity::Mixfixo: return parse_mixfixo(left, op, p); - case fixity::Postfix: return parse_postfix(left, op, p); - default: lean_unreachable(); // LCOV_EXCL_LINE - } - } else { - return save(mk_app(left, save(get_name_ref(id, p), p)), p2); - } - } -} - -/** \brief Parse expr '==' expr. */ -expr parser_imp::parse_heq(expr const & left) { - auto p = pos(); - next(); - expr right = parse_expr(g_heq_precedence); - return save(mk_heq(left, right), p); -} - -/** \brief Parse expr '->' expr. */ -expr parser_imp::parse_arrow(expr const & left) { - auto p = pos(); - next(); - mk_scope scope(*this); - register_binding(g_unused); - // The -1 is a trick to get right associativity in Pratt's parsers - expr right = parse_expr(g_arrow_precedence-1); - return save(mk_arrow(left, right), p); -} - -/** \brief Parse expr '#' expr. */ -expr parser_imp::parse_cartesian_product(expr const & left) { - auto p = pos(); - next(); - mk_scope scope(*this); - register_binding(g_unused); - // The -1 is a trick to get right associativity in Pratt's parsers - expr right = parse_expr(g_cartesian_product_precedence-1); - return save(mk_cartesian_product(left, right), p); -} - -/** \brief Parse '(' expr ')'. */ -expr parser_imp::parse_lparen() { - auto p = pos(); - next(); - expr r = curr() == scanner::token::Type ? parse_type(true) : parse_expr(); - check_rparen_next("invalid expression, ')' expected"); - return save(r, p); -} - -/** - \brief Parse a sequence of identifiers ID*. Store the - result in \c result. -*/ -void parser_imp::parse_names(buffer> & result) { - while (curr_is_identifier()) { - result.emplace_back(pos(), curr_name()); - next(); - } -} - -/** \brief Register the name \c n as a local declaration. */ -void parser_imp::register_binding(name const & n) { - unsigned lvl = m_num_local_decls; - m_local_decls.insert(n, lvl); - m_num_local_decls++; - lean_assert(m_local_decls.find(n)->second == lvl); -} - -/** - \brief Parse ID ... ID ':' expr, where the expression - represents the type of the identifiers. - - \remark If \c implicit_decl is true, then the parameters should be - marked as implicit. This flag is set to true, for example, - when we are parsing definitions such as: - Definition f {A : Type} (a b : A), A := ... - The {A : Type} is considered an implicit argument declaration. - - \remark If \c suppress_type is true, then the type doesn't - need to be provided. That is, we automatically include a placeholder. -*/ -void parser_imp::parse_simple_parameters(parameter_buffer & result, bool implicit_decl, bool suppress_type) { - buffer> names; - parse_names(names); - optional type; - if (!suppress_type) { - check_colon_next("invalid binder, ':' expected"); - type = parse_expr(); - } else if (curr_is_colon()) { - next(); - type = parse_expr(); - } - unsigned sz = result.size(); - result.resize(sz + names.size()); - for (std::pair const & n : names) register_binding(n.second); - unsigned i = names.size(); - while (i > 0) { - --i; - expr arg_type; - if (type) - arg_type = lift_free_vars(*type, i); - else - arg_type = save(mk_placeholder(), names[i].first); - result[sz + i] = parameter(names[i].first, names[i].second, arg_type, implicit_decl); - } -} - -void parser_imp::parse_parameters(parameter_buffer & result, bool implicit_decls, bool suppress_type) { - if (curr_is_identifier()) { - parse_simple_parameters(result, false, suppress_type); - } else { - // (ID ... ID : type) ... (ID ... ID : type) - if (implicit_decls) { - if (!curr_is_lparen() && !curr_is_lcurly()) - throw parser_error("invalid binder, '(', '{' or identifier expected", pos()); - } else { - if (!curr_is_lparen()) - throw parser_error("invalid binder, '(' or identifier expected", pos()); - } - bool implicit = curr_is_lcurly(); - next(); - parse_simple_parameters(result, implicit, suppress_type); - if (!implicit) - check_rparen_next("invalid binder, ')' expected"); - else - check_rcurly_next("invalid binder, '}' expected"); - while (curr_is_lparen() || (implicit_decls && curr_is_lcurly())) { - bool implicit = curr_is_lcurly(); - next(); - parse_simple_parameters(result, implicit, suppress_type); - if (!implicit) - check_rparen_next("invalid binder, ')' expected"); - else - check_rcurly_next("invalid binder, '}' expected"); - } - } -} - -void parser_imp::parse_expr_parameters(parameter_buffer & result) { - parse_parameters(result, false, true); -} - -void parser_imp::parse_var_decl_parameters(parameter_buffer & result) { - parse_parameters(result, true, false); -} - -void parser_imp::parse_definition_parameters(parameter_buffer & result) { - parse_parameters(result, true, true); -} - -/** - \brief Create a lambda/Pi abstraction, using the giving binders - and body. -*/ -expr parser_imp::mk_abstraction(expr_kind k, parameter_buffer const & parameters, expr const & body) { - expr result = body; - unsigned i = parameters.size(); - while (i > 0) { - --i; - pos_info p = parameters[i].m_pos; - switch (k) { - case expr_kind::Lambda: result = save(mk_lambda(parameters[i].m_name, parameters[i].m_type, result), p); break; - case expr_kind::Pi: result = save(mk_pi(parameters[i].m_name, parameters[i].m_type, result), p); break; - case expr_kind::Sigma: result = save(mk_sigma(parameters[i].m_name, parameters[i].m_type, result), p); break; - default: lean_unreachable(); break; - } - } - return result; -} - -/** \brief Parse lambda/Pi abstraction. */ -expr parser_imp::parse_abstraction(expr_kind k) { - next(); - mk_scope scope(*this); - parameter_buffer parameters; - parse_expr_parameters(parameters); - check_comma_next("invalid abstraction, ',' expected"); - expr result = parse_expr(); - return mk_abstraction(k, parameters, result); -} - -/** \brief Parse lambda abstraction. */ -expr parser_imp::parse_lambda() { - return parse_abstraction(expr_kind::Lambda); -} - -/** \brief Parse Pi abstraction. */ -expr parser_imp::parse_pi() { - return parse_abstraction(expr_kind::Pi); -} - -/** \brief Parse Sigma type */ -expr parser_imp::parse_sig() { - return parse_abstraction(expr_kind::Sigma); -} - -/** \brief Parse exists */ -expr parser_imp::parse_exists() { - next(); - mk_scope scope(*this); - parameter_buffer parameters; - parse_expr_parameters(parameters); - check_comma_next("invalid exists, ',' expected"); - expr result = parse_expr(); - unsigned i = parameters.size(); - while (i > 0) { - --i; - pos_info p = parameters[i].m_pos; - expr lambda = save(mk_lambda(parameters[i].m_name, parameters[i].m_type, result), p); - result = save(mk_exists(parameters[i].m_type, lambda), p); - } - return result; -} - -/** \brief Parse Let expression. */ -expr parser_imp::parse_let() { - next(); - mk_scope scope(*this); - buffer, expr>> parameters; - while (true) { - auto p = pos(); - name id = check_identifier_next("invalid let expression, identifier expected"); - optional type; - if (curr_is_colon()) { - next(); - type = parse_expr(); - } - check_assign_next("invalid let expression, ':=' expected"); - expr val = parse_expr(); - register_binding(id); - parameters.emplace_back(p, id, type, val); - if (curr_is_in()) { - next(); - expr r = parse_expr(); - unsigned i = parameters.size(); - while (i > 0) { - --i; - auto p = std::get<0>(parameters[i]); - r = save(mk_let(std::get<1>(parameters[i]), std::get<2>(parameters[i]), std::get<3>(parameters[i]), r), p); - } - return r; - } else { - check_comma_next("invalid let expression, ',' or 'in' expected"); - } - } -} - -/** \brief Parse a natural/integer number value. */ -expr parser_imp::parse_nat_int() { - auto p = pos(); - mpz v = m_scanner.get_num_val().get_numerator(); - expr r = v >= 0 ? mk_nat_value(v) : mk_int_value(v); - r = save(r, p); - next(); - return r; -} - -expr parser_imp::parse_decimal() { - auto p = pos(); - expr r = save(mk_real_value(m_scanner.get_num_val()), p); - next(); - return r; -} - -expr parser_imp::parse_string() { - // TODO(Leo) - not_implemented_yet(); -} - -/** \brief Parse 'Type' and 'Type' level expressions. */ -expr parser_imp::parse_type(bool level_expected) { - auto p = pos(); - next(); - if (level_expected) { - if (curr() == scanner::token::RightParen) { - return save(Type(), p); - } else if (curr() == scanner::token::Arrow) { - return parse_arrow(save(Type(), p)); - } else if (curr() == scanner::token::CartesianProduct) { - return parse_cartesian_product(save(Type(), p)); - } else { - return save(mk_type(parse_level()), p); - } - } else { - return save(Type(), p); - } -} - -expr parser_imp::parse_pair() { - auto p = pos(); - next(); - buffer args; - expr first = parse_expr(g_app_precedence); - expr second = parse_expr(g_app_precedence); - expr type; - if (curr_is_colon()) { - next(); - type = parse_expr(); - } else { - type = save(mk_placeholder(), p); - } - return save(mk_pair(first, second, type), p); -} - -expr parser_imp::parse_proj(bool first) { - auto p = pos(); - next(); - expr t = parse_expr(g_app_precedence); - if (first) - return save(mk_proj1(t), p); - else - return save(mk_proj2(t), p); -} - -/** \brief Parse \c _ a hole that must be filled by the elaborator. */ -expr parser_imp::parse_placeholder() { - auto p = pos(); - next(); - return save(mk_placeholder(), p); -} - -tactic parser_imp::parse_tactic_macro(name tac_id, pos_info const & p) { - lean_assert(m_tactic_macros && m_tactic_macros->find(tac_id) != m_tactic_macros->end()); - next(); - auto m = m_tactic_macros->find(tac_id)->second; - macro_arg_stack args; - flet set(m_check_identifiers, false); - auto r = parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p); - if (r.m_tactic) { - return *(r.m_tactic); - } else { - throw parser_error("failed to execute macro, unexpected result type, a tactic was expected", p); - } -} - -/** \brief Parse a tactic expression, it can be - - 1) A Lua Script Block expression that returns a tactic - 2) '(' expr ')' where expr is a proof term - 3) identifier that is the name of a tactic or proof term. -*/ -tactic parser_imp::parse_tactic_expr() { - auto p = pos(); - if (curr() == scanner::token::ScriptBlock) { - parse_script_expr(); - return using_script([&](lua_State * L) { - if (is_tactic(L, -1)) - return to_tactic(L, -1); - else - throw parser_error("invalid script-block, it must return a tactic", p); - }); - } else if (curr_is_identifier() && m_tactic_macros && m_tactic_macros->find(curr_name()) != m_tactic_macros->end()) { - return parse_tactic_macro(curr_name(), p); - } else if (curr_is_lparen()) { - next(); - tactic r = parse_tactic_expr(); - check_rparen_next("invalid tactic, ')' expected"); - return r; - } else { - name n = check_identifier_next("invalid tactic, identifier, tactic macro, '(', or 'script-block' expected"); - return using_script([&](lua_State * L) { - lua_getglobal(L, n.to_string().c_str()); - try { - if (is_tactic(L, -1)) { - tactic t = to_tactic(L, -1); - lua_pop(L, 1); - return t; - } else { - throw parser_error(sstream() << "invalid tactic, '" << n << "' is not a tactic in script environment", p); - } - } catch (...) { - lua_pop(L, 1); - throw parser_error(sstream() << "unknown tactic '" << n << "'", p); - } - }); - } -} - -static name g_H_show("H_show"); -static name g_from("from"); - -/** \brief Parse 'show' expr, 'from' expr and 'show' expr, 'by' expr*/ -expr parser_imp::parse_show_expr() { - auto p = pos(); - next(); - expr t = parse_expr(); - check_comma_next("invalid 'show' expression, ',' expected"); - if (curr() == scanner::token::By) { - next(); - tactic tac = parse_tactic_expr(); - expr r = mk_placeholder(some_expr(t)); - m_tactic_hints.insert(mk_pair(r, tac)); - return save(r, p); - } else if (curr_is_identifier() && curr_name() == g_from) { - next(); - expr b = parse_expr(); - return save(mk_let(g_H_show, t, b, Var(0)), p); - } else { - throw parser_error("invalid 'show' expected, 'from' or 'by' expected", p); - } -} - -/** \brief Parse 'have' Id ':' expr, 'from' expr, expr and - 'have' Id ':' expr, 'by' expr, expr -*/ -expr parser_imp::parse_have_expr() { - auto p = pos(); - next(); - mk_scope scope(*this); - name id = check_identifier_next("invalid 'have' expression, identifier expected"); - check_colon_next("invalid 'have' expression, ':' expected"); - expr t = parse_expr(); - check_comma_next("invalid 'have' expression, ',' expected"); - expr val; - if (curr() == scanner::token::By) { - auto p2 = pos(); - next(); - tactic tac = parse_tactic_expr(); - expr r = mk_placeholder(some_expr(t)); - m_tactic_hints.insert(mk_pair(r, tac)); - val = save(r, p2); - } else if (curr_is_identifier() && curr_name() == g_from) { - next(); - val = parse_expr(); - } - check_comma_next("invalid 'have' expression, ',' expected"); - register_binding(id); - expr body = parse_expr(); - return save(mk_let(id, t, val, body), p); -} - -/** \brief Parse 'by' tactic */ -expr parser_imp::parse_by_expr() { - auto p = pos(); - next(); - tactic tac = parse_tactic_expr(); - expr r = mk_placeholder(); - m_tactic_hints.insert(mk_pair(r, tac)); - return save(r, p); -} - -/** - \brief Auxiliary method used when processing the beginning of an expression. -*/ -expr parser_imp::parse_nud() { - switch (curr()) { - case scanner::token::Id: return parse_nud_id(); - case scanner::token::LeftParen: return parse_lparen(); - case scanner::token::Lambda: return parse_lambda(); - case scanner::token::Pi: return parse_pi(); - case scanner::token::Sig: return parse_sig(); - case scanner::token::Exists: return parse_exists(); - case scanner::token::Let: return parse_let(); - case scanner::token::IntVal: return parse_nat_int(); - case scanner::token::DecimalVal: return parse_decimal(); - case scanner::token::StringVal: return parse_string(); - case scanner::token::Placeholder: return parse_placeholder(); - case scanner::token::Type: return parse_type(false); - case scanner::token::Show: return parse_show_expr(); - case scanner::token::Have: return parse_have_expr(); - case scanner::token::By: return parse_by_expr(); - case scanner::token::Pair: return parse_pair(); - case scanner::token::Proj1: return parse_proj(true); - case scanner::token::Proj2: return parse_proj(false); - default: - throw parser_error("invalid expression, unexpected token", pos()); - } -} - -/** - \brief Create a new application and associate position of left with the resultant expression. -*/ -expr parser_imp::mk_app_left(expr const & left, expr const & arg) { - if (is_type(left)) - throw parser_error("Type is not a function, use '(Type )' for specifying a particular type universe", pos()); - auto it = m_expr_pos_info.find(left); - lean_assert(it != m_expr_pos_info.end()); - return save(mk_app(left, arg), it->second); -} - -/** - \brief Auxiliary method used when processing the 'inside' of an expression. -*/ -expr parser_imp::parse_led(expr const & left) { - switch (curr()) { - case scanner::token::Id: return parse_led_id(left); - case scanner::token::Arrow: return parse_arrow(left); - case scanner::token::HEq: return parse_heq(left); - case scanner::token::CartesianProduct: return parse_cartesian_product(left); - case scanner::token::LeftParen: return mk_app_left(left, parse_lparen()); - case scanner::token::IntVal: return mk_app_left(left, parse_nat_int()); - case scanner::token::DecimalVal: return mk_app_left(left, parse_decimal()); - case scanner::token::StringVal: return mk_app_left(left, parse_string()); - case scanner::token::Placeholder: return mk_app_left(left, parse_placeholder()); - case scanner::token::Type: return mk_app_left(left, parse_type(false)); - default: return left; - } -} - -/** \brief Return the binding power of the current token (when parsing expression). */ -unsigned parser_imp::curr_lbp() { - switch (curr()) { - case scanner::token::Id: { - name const & id = curr_name(); - auto it = m_local_decls.find(id); - if (it != m_local_decls.end()) { - return g_app_precedence; - } else if (m_expr_macros && m_expr_macros->find(id) != m_expr_macros->end()) { - return m_expr_macros->find(id)->second.m_precedence; - } else { - optional prec = get_lbp(m_env, id); - if (prec) - return *prec; - else - return g_app_precedence; - } - } - case scanner::token::Arrow : return g_arrow_precedence; - case scanner::token::CartesianProduct: return g_cartesian_product_precedence; - case scanner::token::HEq: return g_heq_precedence; - case scanner::token::LeftParen: case scanner::token::IntVal: case scanner::token::DecimalVal: - case scanner::token::StringVal: case scanner::token::Type: case scanner::token::Placeholder: - return g_app_precedence; - default: - return 0; - } -} - -/** \brief Parse an expression */ -expr parser_imp::parse_expr(unsigned rbp) { - expr left = parse_nud(); - while (rbp < curr_lbp()) { - left = parse_led(left); - } - return left; -} -} diff --git a/src/frontends/lean/parser_imp.cpp b/src/frontends/lean/parser_imp.cpp deleted file mode 100644 index f41beee28..000000000 --- a/src/frontends/lean/parser_imp.cpp +++ /dev/null @@ -1,238 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "library/io_state_stream.h" -#include "library/parser_nested_exception.h" -#include "frontends/lean/parser_imp.h" -#include "frontends/lean/parser_macros.h" -#include "frontends/lean/parser_calc.h" - -#ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS -#define LEAN_DEFAULT_PARSER_SHOW_ERRORS true -#endif - -namespace lean { -// ========================================== -// Parser configuration options -static name g_parser_show_errors {"lean", "parser", "show_errors"}; - -RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel"); - -bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); } -// ========================================== - -void parser_imp::code_with_callbacks(std::function && f) { - m_script_state->apply([&](lua_State * L) { - set_io_state set1(L, m_io_state); - set_environment set2(L, m_env); - m_script_state->exec_unprotected([&]() { - f(); - }); - }); -} - -parser_imp::mk_scope::mk_scope(parser_imp & fn): - m_fn(fn), - m_scope(fn.m_local_decls), - m_old_num_local_decls(fn.m_num_local_decls) { -} - -parser_imp::mk_scope::~mk_scope() { - m_fn.m_num_local_decls = m_old_num_local_decls; -} - -calc_proof_parser & parser_imp::get_calc_proof_parser() { - if (!m_calc_proof_parser) - m_calc_proof_parser.reset(new calc_proof_parser()); - return *m_calc_proof_parser; -} - -pos_info parser_imp::pos_of(expr const & e, pos_info default_pos) { - auto it = m_expr_pos_info.find(e); - if (it == m_expr_pos_info.end()) - return default_pos; - else - return it->second; -} - -void parser_imp::check_next(scanner::token t, char const * msg) { - if (curr() == t) - next(); - else - throw parser_error(msg, pos()); -} - -/** - \brief Throws a parser error if the current token is not a - string. If it is, move to the next token. -*/ -std::string parser_imp::check_string_next(char const * msg) { - if (curr() != scanner::token::StringVal) - throw parser_error(msg, pos()); - std::string r = curr_string(); - next(); - return r; -} - -unsigned parser_imp::parse_unsigned(char const * msg) { - lean_assert(curr_is_nat()); - mpz pval = curr_num().get_numerator(); - if (!pval.is_unsigned_int()) { - throw parser_error(msg, pos()); - } else { - unsigned r = pval.get_unsigned_int(); - next(); - return r; - } -} - -double parser_imp::parse_double() { - return 0.0; -} - -[[ noreturn ]] void parser_imp::not_implemented_yet() { - // TODO(Leo) - throw parser_error("not implemented yet", pos()); -} - -void parser_imp::updt_options() { - m_verbose = get_verbose(m_io_state.get_options()); - m_show_errors = get_parser_show_errors(m_io_state.get_options()); -} - -/** - \brief Parse a block of Lua code. If as_expr is true, then - it appends the string "return " in front of the script. -*/ -void parser_imp::parse_script(bool as_expr) { - m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos()); - if (!m_script_state) - throw exception("failed to execute Lua script, parser does not have a Lua interpreter"); - std::string script_code = m_scanner.get_str_val(); - if (as_expr) { - script_code = "return " + script_code; - } - next(); - using_script([&](lua_State * L) { - dostring(L, script_code.c_str()); - }); -} - -void parser_imp::parse_script_expr() { return parse_script(true); } - -std::pair parser_imp::elaborate(expr const & e) { - return m_elaborator(e, m_io_state.get_options()); -} - -std::tuple parser_imp::elaborate(name const & n, expr const & t, expr const & e) { - return m_elaborator(n, t, e, m_io_state.get_options()); -} - -void parser_imp::sync_command() { - // Keep consuming tokens until we find a Command or End-of-file - show_prompt(); - while (curr() != scanner::token::CommandId && curr() != scanner::token::Eof && curr() != scanner::token::Period) - next(); - if (curr_is_period()) - next(); -} - -parser_imp::parser_imp(environment const & env, io_state const & st, std::istream & in, char const * strm_name, - script_state * S, bool use_exceptions, bool interactive): - m_env(env), - m_io_state(st), - m_scanner(in, strm_name), - m_strm_name(strm_name), - m_elaborator(env), - m_use_exceptions(use_exceptions), - m_interactive(interactive), - m_script_state(S), - m_set_parser(m_script_state, this) { - m_namespace_prefixes.push_back(name()); - m_check_identifiers = true; - updt_options(); - m_found_errors = false; - m_num_local_decls = 0; - m_scanner.set_command_keywords(get_command_keywords()); - if (m_script_state) { - m_script_state->apply([&](lua_State * L) { - m_expr_macros = &get_expr_macros(L); - m_tactic_macros = &get_tactic_macros(L); - m_cmd_macros = &get_cmd_macros(L); - for (auto const & p : *m_cmd_macros) { - m_scanner.add_command_keyword(p.first); - } - }); - } else { - m_expr_macros = nullptr; - m_tactic_macros = nullptr; - m_cmd_macros = nullptr; - } - // Initialize m_curr with some value. We need that because scan() - // may fail, and m_curr will remain uninitialized. - // In thi case, Valgrind would report unit var errors. - m_curr = scanner::token::Id; - protected_call([&]() { scan(); }, - [&]() { sync_command(); }); -} - -parser_imp::~parser_imp() {} - -void parser_imp::show_prompt(bool interactive, io_state const & ios) { - if (interactive) { - regular(ios) << "# "; - regular(ios).flush(); - } -} - -void parser_imp::show_prompt() { - show_prompt(m_interactive, m_io_state); -} - -void parser_imp::show_tactic_prompt() { - if (m_interactive) { - regular(m_io_state) << "## "; - regular(m_io_state).flush(); - } -} - -/** \brief Parse a sequence of commands. This method also perform error management. */ -bool parser_imp::parse_commands() { - bool done = false; - while (!done) { - protected_call([&]() { - check_interrupted(); - switch (curr()) { - case scanner::token::CommandId: if (!parse_command()) done = true; break; - case scanner::token::ScriptBlock: parse_script(); break; - case scanner::token::Period: show_prompt(); next(); break; - case scanner::token::Eof: done = true; break; - default: - throw parser_error("Command expected", pos()); - } - }, - [&]() { sync_command(); }); - } - return !m_found_errors; -} - -/** \brief Parse an expression. */ -expr parser_imp::parse_expr_main() { - try { - auto p = elaborate(parse_expr()); - check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration"); - return p.first; - } catch (parser_error & ex) { - throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second); - } catch (exception & ex) { - throw parser_nested_exception(std::shared_ptr(ex.clone()), - std::shared_ptr(new lean_pos_info_provider(m_this.lock(), m_last_cmd_pos))); - } -} -}; diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h deleted file mode 100644 index 4618e0708..000000000 --- a/src/frontends/lean/parser_imp.h +++ /dev/null @@ -1,470 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include -#include "util/name_map.h" -#include "util/scoped_map.h" -#include "util/script_exception.h" -#include "util/script_state.h" -#include "kernel/expr_maps.h" -#include "kernel/io_state.h" -#include "kernel/environment.h" -#include "library/kernel_bindings.h" -#include "library/tactic/tactic.h" -#include "library/elaborator/elaborator_exception.h" -#include "library/unsolved_metavar_exception.h" -#include "frontends/lean/scanner.h" -#include "frontends/lean/parser_types.h" -#include "frontends/lean/parser_error.h" -#include "frontends/lean/operator_info.h" -#include "frontends/lean/frontend_elaborator.h" - -// Lean encodes -// proj1 i t -// as -// proj1 (proj2 (proj2 ... t) ...) -// So, a big \c i may make Lean run out of memory. -// The default limit is 10000. I don't believe anybody needs to create a tuple with -// more than 10000 entries -#ifndef LEAN_MAX_PROJECTION -#define LEAN_MAX_PROJECTION 10000 -#endif - -namespace lean { -class parser_imp; -class calc_proof_parser; - -bool get_parser_verbose(options const & opts); -bool get_parser_show_errors(options const & opts); - -/** \brief Auxiliary object that stores a reference to the parser object inside the Lua State */ -struct set_parser { - script_state::weak_ref m_state; - parser_imp * m_prev; - set_parser(script_state * S, parser_imp * ptr); - ~set_parser(); -}; - -/** - \brief Actual implementation for the default Lean parser - - \remark It is an instance of a Pratt parser - (http://en.wikipedia.org/wiki/Pratt_parser) described in the paper - "Top down operator precedence". This algorithm is super simple, - and it is easy to support user-defined infix/prefix/postfix/mixfix - operators. -*/ -class parser_imp { - friend class parser; - friend int mk_cmd_macro(lua_State * L); - typedef scoped_map local_decls; - typedef name_map builtins; - typedef expr_map expr_pos_info; - typedef expr_map tactic_hints; // a mapping from placeholder to tactic - typedef scoped_map using_decls; - enum class scope_kind { Scope, Namespace }; - - std::weak_ptr m_this; - environment m_env; - io_state m_io_state; - scanner m_scanner; - std::string m_strm_name; // input stream name - frontend_elaborator m_elaborator; - macros const * m_expr_macros; - macros const * m_cmd_macros; - macros const * m_tactic_macros; - scanner::token m_curr; - bool m_use_exceptions; - bool m_interactive; - bool m_found_errors; - local_decls m_local_decls; - unsigned m_num_local_decls; - expr_pos_info m_expr_pos_info; - pos_info m_last_cmd_pos; - pos_info m_last_script_pos; - tactic_hints m_tactic_hints; - using_decls m_using_decls; - std::vector m_namespace_prefixes; - std::vector m_scope_kinds; - std::unique_ptr m_calc_proof_parser; - - - // If true then return error when parsing identifiers and it is not local or global. - // We set this flag off when parsing tactics. The apply_tac may reference - // a hypothesis in the proof state. This hypothesis is not visible until we - // execute the tactic. - bool m_check_identifiers; - - script_state * m_script_state; - set_parser m_set_parser; - - bool m_verbose; - bool m_show_errors; - - template - typename std::result_of::type using_script(F && f) { - return m_script_state->apply([&](lua_State * L) { - set_io_state set1(L, m_io_state); - set_environment set2(L, m_env); - return f(L); - }); - } - - void code_with_callbacks(std::function && f); - - /** - \brief Auxiliar struct for creating/destroying a new scope for - local declarations. - */ - struct mk_scope { - parser_imp & m_fn; - local_decls::mk_scope m_scope; - unsigned m_old_num_local_decls; - mk_scope(parser_imp & fn); - ~mk_scope(); - }; - - calc_proof_parser & get_calc_proof_parser(); - -public: - environment const & get_environment() const { return m_env; } - - /** \brief Return the current position information */ - pos_info pos() const { return mk_pair(m_scanner.get_line(), m_scanner.get_pos()); } - - /** \brief Return the position associated with \c e. If there is none, then return \c default_pos. */ - pos_info pos_of(expr const & e, pos_info default_pos); - - /** \brief Associate position \c p with \c e and return \c e */ - expr save(expr const & e, pos_info p) { m_expr_pos_info[e] = p; return e; } - - /** \brief Read the next token. */ - void scan() { m_curr = m_scanner.scan(); } - /** \brief Return the current token */ - scanner::token curr() const { return m_curr; } - /** \brief Read the next token if the current one is not End-of-file. */ - void next() { if (m_curr != scanner::token::Eof) scan(); } - - /** \brief Return the name associated with the current token. */ - name const & curr_name() const { return m_scanner.get_name_val(); } - /** \brief Return the numeral associated with the current token. */ - mpq const & curr_num() const { return m_scanner.get_num_val(); } - /** \brief Return the string associated with the current token. */ - std::string const & curr_string() const { return m_scanner.get_str_val(); } - /** - \brief Check if the current token is \c t, and move to the - next one. If the current token is not \c t, it throws a parser error. - */ - void check_next(scanner::token t, char const * msg); - - /** \brief Return true iff the current token is an identifier */ - bool curr_is_identifier() const { return curr() == scanner::token::Id; } - /** \brief Return true iff the current token is a string literal */ - bool curr_is_string() const { return curr() == scanner::token::StringVal; } - /** \brief Return true iff the current token is a '_" */ - bool curr_is_placeholder() const { return curr() == scanner::token::Placeholder; } - /** \brief Return true iff the current token is a natural number */ - bool curr_is_nat() const { return curr() == scanner::token::IntVal && m_scanner.get_num_val() >= 0; } - /** \brief Return true iff the current token is a '(' */ - bool curr_is_lparen() const { return curr() == scanner::token::LeftParen; } - /** \brief Return true iff the current token is a '{' */ - bool curr_is_lcurly() const { return curr() == scanner::token::LeftCurlyBracket; } - /** \brief Return true iff the current token is a ':' */ - bool curr_is_colon() const { return curr() == scanner::token::Colon; } - /** \brief Return true iff the current token is a ',' */ - bool curr_is_comma() const { return curr() == scanner::token::Comma; } - /** \brief Return true iff the current token is a ':=' */ - bool curr_is_assign() const { return curr() == scanner::token::Assign; } - /** \brief Return true iff the current token is an 'in' token */ - bool curr_is_in() const { return curr() == scanner::token::In; } - /** \brief Return true iff the current token is '.' */ - bool curr_is_period() const { return curr() == scanner::token::Period; } - /** \brief Throws a parser error if the current token is not an identifier. */ - void check_identifier(char const * msg) { if (!curr_is_identifier()) throw parser_error(msg, pos()); } - /** - \brief Throws a parser error if the current token is not an - identifier. If it is, move to the next token. - */ - name check_identifier_next(char const * msg) { check_identifier(msg); name r = curr_name(); next(); return r; } - /** \brief Throws a parser error if the current token is not '_'. If it is, move to the next token. */ - void check_placeholder_next(char const * msg) { check_next(scanner::token::Placeholder, msg); } - /** \brief Throws a parser error if the current token is not ':'. If it is, move to the next token. */ - void check_colon_next(char const * msg) { check_next(scanner::token::Colon, msg); } - /** \brief Throws a parser error if the current token is not ','. If it is, move to the next token. */ - void check_comma_next(char const * msg) { check_next(scanner::token::Comma, msg); } - /** \brief Throws a parser error if the current token is not ')'. If it is, move to the next token. */ - void check_rparen_next(char const * msg) { check_next(scanner::token::RightParen, msg); } - /** \brief Throws a parser error if the current token is not '}'. If it is, move to the next token. */ - void check_rcurly_next(char const * msg) { check_next(scanner::token::RightCurlyBracket, msg); } - /** \brief Throws a parser error if the current token is not ':='. If it is, move to the next token. */ - void check_assign_next(char const * msg) { check_next(scanner::token::Assign, msg); } - /** \brief Throws a parser error if the current token is not '.'. If it is, move to the next token. */ - void check_period_next(char const * msg) { check_next(scanner::token::Period, msg); } - - std::string check_string_next(char const * msg); - - /** - @name Error handling - */ - /*@{*/ -private: - void display_error_pos(unsigned line, unsigned pos); - void display_error_pos(pos_info const & p); - void display_error(char const * msg, unsigned line, unsigned pos); - - struct lean_pos_info_provider : public pos_info_provider { - std::shared_ptr m_parser; - pos_info m_pos; - lean_pos_info_provider(std::shared_ptr const & p, pos_info const & pos):m_parser(p), m_pos(pos) {} - virtual std::pair get_pos_info(expr const & e) const; - virtual std::pair get_some_pos() const { return m_pos; } - virtual char const * get_file_name() const; - }; - - void display_error(tactic_cmd_error const & ex); - void display_error(script_exception const & ex); - void display_error(exception const & ex); -public: - void protected_call(std::function && f, std::function && sync); - /*@}*/ - -public: - unsigned parse_unsigned(char const * msg); - double parse_double(); - -private: - [[ noreturn ]] void not_implemented_yet(); - void updt_options(); - void parse_script(bool as_expr = false); - void parse_script_expr(); - - /** - @name Elaborator interface - */ - /*@{*/ -private: - std::pair elaborate(expr const & e); - std::tuple elaborate(name const & n, expr const & t, expr const & e); - /*@}*/ - - - /** - @name Parse Universe levels - */ - /*@{*/ -private: - level parse_level_max(); - level parse_level_nud_id(); - level parse_level_nud_int(); - level parse_level_lparen(); - level parse_level_nud(); - level parse_level_led_plus(level const & left); - level parse_level_led_cup(level const & left); - level parse_level_led(level const & left); - unsigned curr_level_lbp(); -public: - /** \brief Parse a universe level */ - level parse_level(unsigned rbp = 0); - /*@}*/ - - - /** - @name Parse Expressions - */ - /*@{*/ -private: - unsigned get_implicit_vector_size(expr const & d); - std::vector const & get_smallest_implicit_vector(list const & ds); - unsigned get_smallest_implicit_vector_size(list const & ds); - expr mk_fun(operator_info const & op, pos_info const & pos); - expr mk_application(operator_info const & op, pos_info const & pos, unsigned num_args, expr const * args); - expr mk_application(operator_info const & op, pos_info const & pos, std::initializer_list const & l); - expr mk_application(operator_info const & op, pos_info const & pos, expr const & arg); - expr mk_application(operator_info const & op, pos_info const & pos, buffer const & args); - expr parse_prefix(operator_info const & op); - expr parse_postfix(expr const & left, operator_info const & op, pos_info const & op_pos); - expr parse_infix(expr const & left, operator_info const & op, pos_info const & op_pos); - expr parse_infixl(expr const & left, operator_info const & op, pos_info const & op_pos); - expr parse_infixr(expr const & left, operator_info const & op, pos_info const & op_pos); - void check_op_part(name const & op_part); - void parse_mixfix_args(list const & ops, unsigned prec, buffer & args); - expr parse_mixfixl(operator_info const & op); - expr parse_mixfixr(expr const & left, operator_info const & op, pos_info const & op_pos); - expr parse_mixfixo(expr const & left, operator_info const & op, pos_info const & op_pos); - expr parse_mixfixc(operator_info const & op); - void propagate_position(expr const & e, pos_info p); - bool is_curr_begin_expr() const; - bool is_curr_begin_tactic() const; - typedef buffer> macro_arg_stack; - struct macro_result { - optional m_expr; - optional m_tactic; - macro_result(expr const & e):m_expr(e) {} - macro_result(tactic const & t):m_tactic(t) {} - macro_result() {} - }; - macro_result parse_macro(list const & arg_kinds, luaref const & fn, unsigned prec, macro_arg_stack & args, - pos_info const & p); - expr parse_expr_macro(name const & id, pos_info const & p); - expr parse_led_id(expr const & left); - expr parse_heq(expr const & left); - expr parse_arrow(expr const & left); - expr parse_cartesian_product(expr const & left); - expr parse_lparen(); - void parse_names(buffer> & result); - void register_binding(name const & n); - void parse_simple_parameters(parameter_buffer & result, bool implicit_decl, bool suppress_type); - expr mk_abstraction(expr_kind k, parameter_buffer const & parameters, expr const & body); - expr parse_abstraction(expr_kind k); - expr parse_lambda(); - expr parse_pi(); - expr parse_sig(); - expr parse_exists(); - expr parse_let(); - expr parse_type(bool level_expected); - expr parse_pair(); - expr parse_proj(bool first); - tactic parse_tactic_macro(name tac_id, pos_info const & p); - expr parse_show_expr(); - expr parse_have_expr(); - expr parse_calc(); - expr parse_nud_id(); - expr parse_nud(); - expr parse_led(expr const & left); - expr mk_app_left(expr const & left, expr const & arg); - unsigned curr_lbp(); - expr parse_nat_int(); - expr parse_decimal(); - expr parse_string(); - expr parse_by_expr(); -public: - /** - \brief Try to find an object (Definition or Postulate) named \c - id in the frontend/environment. If there isn't one, then tries - to check if \c id is a builtin symbol. If it is not throws an error. - - If \c implicit_args is true, then we also parse explicit arguments until - we have a placeholder forall implicit ones. - */ - expr get_name_ref(name const & id, pos_info const & p, bool implicit_args = true); - /** - \brief Parse a sequence of '(' ID ... ID ':' expr ')'. - - This is used when parsing lambda, Pi, forall/exists expressions and - definitions. - - \remark If implicit_decls is true, then we allow declarations - with curly braces. These declarations are used to tag implicit - arguments. Such as: - Definition f {A : Type} (a b : A) : A := ... - - \see parse_simple_parameters - */ - void parse_parameters(parameter_buffer & result, bool implicit_decls, bool suppress_type); - /** \brief Parse parameters for expressions such as: lambda, pi, forall, exists */ - void parse_expr_parameters(parameter_buffer & result); - void parse_var_decl_parameters(parameter_buffer & result); - void parse_definition_parameters(parameter_buffer & result); - /** \brief Parse a tactic expression, it can be - - 1) A Lua Script Block expression that returns a tactic - 2) '(' expr ')' where expr is a proof term - 3) identifier that is the name of a tactic or proof term. - */ - tactic parse_tactic_expr(); - /** \brief Parse \c _ a hole that must be filled by the elaborator. */ - expr parse_placeholder(); - /** \brief Parse an expression */ - expr parse_expr(unsigned rbp = 0); - /*@}*/ - - - /** - @name Tactics - */ - /*@{*/ -private: - /** \brief Return true iff the current token is a tactic command */ - bool curr_is_tactic_cmd() const; - void display_proof_state(proof_state s); - void display_proof_state_if_interactive(proof_state s); - typedef std::vector proof_state_seq_stack; - std::pair apply_tactic(proof_state const & s, tactic const & t, pos_info const & p); - expr mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type); - void back_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s); - void tactic_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s); - expr done_cmd(proof_state const & s, context const & ctx, expr const & expected_type); - expr parse_tactic_cmds(proof_state s, context const & ctx, expr const & expected_type); - std::pair, pos_info> get_tactic_for(expr const & mvar); - std::pair get_metavar_ctx_and_type(expr const & mvar, metavar_env const & menv); - expr apply_tactics(expr const & val, metavar_env & menv); - /*@}*/ - -private: - /** - @name Parse Commands - */ - /*@{*/ - static list const & get_command_keywords(); - void register_implicit_arguments(name const & n, parameter_buffer & parameters); - void check_no_metavar(expr const & e, metavar_env const & menv, char const * msg); - void check_no_metavar(std::pair const & p, char const * msg); - name mk_full_name(name const & n); - void parse_def_core(bool is_definition); - void parse_definition(); - void parse_theorem(); - void parse_variable_core(bool is_var); - void parse_variable(); - void parse_variables(); - void parse_axiom(); - void parse_eval(); - bool is_hidden_object(object const & obj) const; - void parse_print(); - void parse_check(); - unsigned parse_precedence(); - name parse_op_id(); - void parse_op(fixity fx); - void parse_notation_decl(); - void parse_set_option(); - void parse_set_opaque(); - optional find_lua_file(std::string const & fname); - void parse_import(); - void parse_help(); - void parse_coercion(); - void reset_env(environment env); - void parse_scope(); - void parse_pop(); - void parse_cmd_macro(name cmd_id, pos_info const & p); - void parse_universe(); - void parse_alias(); - void parse_builtin(); - void parse_namespace(); - void parse_end(); - void parse_using(); - void parse_rewrite_set(); - void parse_ids_and_rsid(buffer & ids, name & rsid); - void parse_add_rewrite(); - void parse_enable_rewrite(bool flag); - bool parse_command(); - void sync_command(); - /*@}*/ - -public: - parser_imp(environment const & env, io_state const & st, std::istream & in, char const * strm_name, - script_state * S, bool use_exceptions, bool interactive); - ~parser_imp(); - static void show_prompt(bool interactive, io_state const & ios); - void show_prompt(); - void show_tactic_prompt(); - /** \brief Parse a sequence of commands. This method also perform error management. */ - bool parse_commands(); - /** \brief Parse an expression. */ - expr parse_expr_main(); -}; -} diff --git a/src/frontends/lean/parser_level.cpp b/src/frontends/lean/parser_level.cpp deleted file mode 100644 index 2db323683..000000000 --- a/src/frontends/lean/parser_level.cpp +++ /dev/null @@ -1,119 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/io_state_stream.h" -#include "frontends/lean/parser_imp.h" -namespace lean { -// ========================================== -// Support for parsing levels -static name g_max_name("max"); -static name g_cup_name("\u2294"); -static name g_plus_name("+"); -static unsigned g_level_plus_prec = 10; -static unsigned g_level_cup_prec = 5; -// ========================================== - -/* - Parse Universe levels -*/ -level parser_imp::parse_level_max() { - auto p = pos(); - next(); - buffer lvls; - while (curr_is_identifier() || curr_is_nat()) { - lvls.push_back(parse_level()); - } - if (lvls.size() < 2) - throw parser_error("invalid level expression, max must have at least two arguments", p); - level r = lvls[0]; - for (unsigned i = 1; i < lvls.size(); i++) - r = max(r, lvls[i]); - return r; -} - -level parser_imp::parse_level_nud_id() { - name id = curr_name(); - if (id == g_max_name) { - return parse_level_max(); - } else { - next(); - return m_env->get_uvar(id); - } -} - -level parser_imp::parse_level_nud_int() { - auto p = pos(); - mpz val = curr_num().get_numerator(); - next(); - if (val < 0) - throw parser_error("invalid level expression, value is negative", p); - if (!val.is_unsigned_int()) - throw parser_error("invalid level expression, value does not fit in a machine integer", p); - return level() + val.get_unsigned_int(); -} - -level parser_imp::parse_level_lparen() { - next(); - level r = parse_level(); - check_rparen_next("invalid level expression, ')' expected"); - return r; -} - -level parser_imp::parse_level_nud() { - switch (curr()) { - case scanner::token::Id: return parse_level_nud_id(); - case scanner::token::IntVal: return parse_level_nud_int(); - case scanner::token::LeftParen: return parse_level_lparen(); - default: - throw parser_error("invalid level expression", pos()); - } -} - -level parser_imp::parse_level_led_plus(level const & left) { - auto p = pos(); - next(); - level right = parse_level(g_level_plus_prec); - if (!is_lift(right) || !lift_of(right).is_bottom()) - throw parser_error("invalid level expression, right hand side of '+' (aka universe lift operator) must be a numeral", p); - return left + lift_offset(right); -} - -level parser_imp::parse_level_led_cup(level const & left) { - next(); - level right = parse_level(g_level_cup_prec); - return max(left, right); -} - -level parser_imp::parse_level_led(level const & left) { - switch (curr()) { - case scanner::token::Id: - if (curr_name() == g_plus_name) return parse_level_led_plus(left); - else if (curr_name() == g_cup_name) return parse_level_led_cup(left); - default: - throw parser_error("invalid level expression", pos()); - } -} - -unsigned parser_imp::curr_level_lbp() { - switch (curr()) { - case scanner::token::Id: { - name const & id = curr_name(); - if (id == g_plus_name) return g_level_plus_prec; - else if (id == g_cup_name) return g_level_cup_prec; - else return 0; - } - default: return 0; - } -} - -level parser_imp::parse_level(unsigned rbp) { - level left = parse_level_nud(); - while (rbp < curr_level_lbp()) { - left = parse_level_led(left); - } - return left; -} -} diff --git a/src/frontends/lean/parser_macros.cpp b/src/frontends/lean/parser_macros.cpp deleted file mode 100644 index 6c36a4ae2..000000000 --- a/src/frontends/lean/parser_macros.cpp +++ /dev/null @@ -1,143 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/io_state_stream.h" -#include "frontends/lean/parser_imp.h" -#include "frontends/lean/notation.h" - -namespace lean { -static char g_set_parser_key; -/** \brief Return a reference to the parser object */ -parser_imp * get_parser(lua_State * L) { - lua_pushlightuserdata(L, static_cast(&g_set_parser_key)); - lua_gettable(L, LUA_REGISTRYINDEX); - if (lua_islightuserdata(L, -1)) { - auto r = static_cast(lua_touserdata(L, -1)); - lua_pop(L, 1); - return r; - } - lua_pop(L, 1); - return nullptr; -} - -set_parser::set_parser(script_state * S, parser_imp * ptr) { - if (S) { - m_state = S->to_weak_ref(); - S->apply([&](lua_State * L) { - m_prev = get_parser(L); - lua_pushlightuserdata(L, static_cast(&g_set_parser_key)); - lua_pushlightuserdata(L, ptr); - lua_settable(L, LUA_REGISTRYINDEX); - }); - } -} -set_parser::~set_parser() { - if (!m_state.expired()) { - script_state S(m_state); - S.apply([&](lua_State * L) { - lua_pushlightuserdata(L, static_cast(&g_set_parser_key)); - lua_pushlightuserdata(L, m_prev); - lua_settable(L, LUA_REGISTRYINDEX); - }); - } -} - -static char g_parser_expr_macros_key; -static char g_parser_tactic_macros_key; -static char g_parser_cmd_macros_key; -DECL_UDATA(macros) - -macros & get_macros(lua_State * L, char * key) { - lua_pushlightuserdata(L, static_cast(key)); - lua_gettable(L, LUA_REGISTRYINDEX); - if (lua_isnil(L, -1)) { - lua_pop(L, 1); - lua_pushlightuserdata(L, static_cast(key)); - push_macros(L, macros()); - lua_settable(L, LUA_REGISTRYINDEX); - lua_pushlightuserdata(L, static_cast(key)); - lua_gettable(L, LUA_REGISTRYINDEX); - } - lean_assert(is_macros(L, -1)); - macros & r = to_macros(L, -1); - lua_pop(L, 1); - return r; -} - -macros & get_expr_macros(lua_State * L) { return get_macros(L, &g_parser_expr_macros_key); } -macros & get_tactic_macros(lua_State * L) { return get_macros(L, &g_parser_tactic_macros_key); } -macros & get_cmd_macros(lua_State * L) { return get_macros(L, &g_parser_cmd_macros_key); } - -void mk_macro(lua_State * L, macros & mtable) { - int nargs = lua_gettop(L); - name macro_name = to_name_ext(L, 1); - unsigned prec = nargs == 4 ? lua_tointeger(L, 4) : g_app_precedence; - luaL_checktype(L, 3, LUA_TFUNCTION); // user-fun - buffer arg_kind_buffer; - int n = objlen(L, 2); - for (int i = 1; i <= n; i++) { - lua_rawgeti(L, 2, i); - arg_kind_buffer.push_back(static_cast(luaL_checkinteger(L, -1))); - lua_pop(L, 1); - } - list arg_kinds = to_list(arg_kind_buffer.begin(), arg_kind_buffer.end()); - mtable.insert(mk_pair(macro_name, macro(arg_kinds, luaref(L, 3), prec))); -} - -int mk_macro(lua_State * L) { - mk_macro(L, get_expr_macros(L)); - return 0; -} - -int mk_cmd_macro(lua_State * L) { - mk_macro(L, get_cmd_macros(L)); - name macro_name = to_name_ext(L, 1); - parser_imp * ptr = get_parser(L); - if (!ptr) - throw exception("invalid cmd_macro, it is not in the context of a Lean parser"); - // Make sure macro_name is a CommandId. - ptr->m_scanner.add_command_keyword(macro_name); - if (ptr->m_curr == scanner::token::Id && ptr->curr_name() == macro_name) { - ptr->m_curr = scanner::token::CommandId; - } - return 0; -} - -int mk_tactic_macro(lua_State * L) { - mk_macro(L, get_tactic_macros(L)); - return 0; -} - -static const struct luaL_Reg macros_m[] = { - {"__gc", macros_gc}, // never throws - {0, 0} -}; - -void open_macros(lua_State * L) { - luaL_newmetatable(L, macros_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, macros_m, 0); - SET_GLOBAL_FUN(macros_pred, "is_macros"); - SET_GLOBAL_FUN(mk_macro, "macro"); - SET_GLOBAL_FUN(mk_cmd_macro, "cmd_macro"); - SET_GLOBAL_FUN(mk_tactic_macro, "tactic_macro"); - - lua_newtable(L); - SET_ENUM("Expr", macro_arg_kind::Expr); - SET_ENUM("Exprs", macro_arg_kind::Exprs); - SET_ENUM("Parameters", macro_arg_kind::Parameters); - SET_ENUM("Id", macro_arg_kind::Id); - SET_ENUM("Ids", macro_arg_kind::Ids); - SET_ENUM("String", macro_arg_kind::String); - SET_ENUM("Int", macro_arg_kind::Int); - SET_ENUM("Comma", macro_arg_kind::Comma); - SET_ENUM("Assign", macro_arg_kind::Assign); - SET_ENUM("Tactic", macro_arg_kind::Tactic); - SET_ENUM("Tactics", macro_arg_kind::Tactics); - lua_setglobal(L, "macro_arg"); -} -} diff --git a/src/frontends/lean/parser_macros.h b/src/frontends/lean/parser_macros.h deleted file mode 100644 index 0f8800280..000000000 --- a/src/frontends/lean/parser_macros.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/lua.h" -#include "frontends/lean/parser_types.h" -namespace lean { -macros & get_expr_macros(lua_State * L); -macros & get_tactic_macros(lua_State * L); -macros & get_cmd_macros(lua_State * L); -} diff --git a/src/frontends/lean/parser_tactic.cpp b/src/frontends/lean/parser_tactic.cpp deleted file mode 100644 index 035a76dc6..000000000 --- a/src/frontends/lean/parser_tactic.cpp +++ /dev/null @@ -1,295 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "kernel/for_each_fn.h" -#include "kernel/type_checker.h" -#include "kernel/type_checker_justification.h" -#include "kernel/unification_constraint.h" -#include "library/io_state_stream.h" -#include "library/expr_lt.h" -#include "library/elaborator/elaborator.h" -#include "frontends/lean/parser_imp.h" - -namespace lean { -static name g_apply("apply"); -static name g_done("done"); -static name g_back("back"); -static name g_abort("abort"); -static name g_assumption("assumption"); -static list g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumption }; - -bool parser_imp::curr_is_tactic_cmd() const { - return curr_is_identifier() && std::find(g_tactic_cmds.begin(), g_tactic_cmds.end(), curr_name()) != g_tactic_cmds.end(); -} - -void parser_imp::display_proof_state(proof_state s) { - regular(m_io_state) << "Proof state:\n" << s << endl; -} - -void parser_imp::display_proof_state_if_interactive(proof_state s) { - if (m_interactive) - display_proof_state(s); -} - -/** - \brief Apply tactic \c t to state \c s. - When \c t succeeds, it returns the head and tail of the output state sequence. - Throws an exception if the tactic fails, and use \c p to sign the error position. -*/ -std::pair parser_imp::apply_tactic(proof_state const & s, tactic const & t, pos_info const & p) { - proof_state_seq::maybe_pair r; - code_with_callbacks([&]() { - // t may have call-backs we should set ios in the script_state - proof_state_seq seq = t(m_env, m_io_state, s); - r = seq.pull(); - }); - if (r) { - return mk_pair(r->first, r->second); - } else { - throw tactic_cmd_error("tactic failed", p, s); - } -} - -/** - \brief Try to create a proof for the input state \c s. - It basically applies the proof_builder if \c s does not contain - any goals left. The position information is used to throw an exception - if \c s is not a final state. - - The resultant proof must have type \c expected_type in the context \c ctx. -*/ -expr parser_imp::mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type) { - if (s.is_proof_final_state()) { - assignment a(s.get_menv().copy()); - proof_map m; - expr pr = s.get_proof_builder()(m, a); - if (has_metavar(pr)) { - // Some tactics generate metavariables that can only be instantiated by type inference elaboration. - // Example: apply_tactic. - metavar_env menv = s.get_menv().copy(); - buffer ucs; - expr pr_type = type_checker(m_env).check(pr, ctx, menv, ucs); - ucs.push_back(mk_convertible_constraint(ctx, pr_type, expected_type, mk_type_match_justification(ctx, expected_type, pr))); - elaborator elb(m_env, menv, ucs.size(), ucs.data(), m_io_state.get_options()); - metavar_env new_menv = elb.next(); - pr = new_menv->instantiate_metavars(pr); - if (has_metavar(pr)) - throw exception("synthesized proof object has unsolved metavars"); - } - return pr; - } else { - throw tactic_cmd_error("failed to create proof for the following proof state", p, s); - } -} - -/** - \brief Execute the \c back (backtrack) tactic command. It - succeeds if the stack \c stack contains proof states. When it - succeeds, \c s is updated with the next state in the state - sequence on the top of \c stack. The new state is also removed - from the stack. -*/ -void parser_imp::back_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) { - auto p = pos(); - next(); - while (!stack.empty()) { - check_interrupted(); - lazy_list seq = stack.back(); - stack.pop_back(); - proof_state_seq::maybe_pair r; - code_with_callbacks([&]() { - r = seq.pull(); - }); - if (r) { - stack.push_back(r->second); - s = r->first; - return; - } - } - throw tactic_cmd_error("failed to backtrack", p, s); -} - -/** - \brief Execute the tactic. - This command just applies the tactic to the input state \c s. - If it succeeds, \c s is assigned to the head of the output - state sequence produced by the tactic. The rest/tail of the - output state sequence is stored on the top of the stack \c - stack. -*/ -void parser_imp::tactic_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) { - auto tac_pos = pos(); - tactic t = parse_tactic_expr(); - auto r = apply_tactic(s, t, tac_pos); - s = r.first; - stack.push_back(r.second); -} - -/** - \brief Execute the \c done tactic command. It succeeds if - a proof for \c s can be built. -*/ -expr parser_imp::done_cmd(proof_state const & s, context const & ctx, expr const & expected_type) { - auto p = pos(); - next(); - return mk_proof_for(s, p, ctx, expected_type); -} - -/** - \brief Parse tactic command sequence for solving input state \c s. - - The proof for \c s must have type \c expected_type in the context \c ctx. -*/ -expr parser_imp::parse_tactic_cmds(proof_state s, context const & ctx, expr const & expected_type) { - proof_state_seq_stack stack; - optional pr; - enum class status { Continue, Done, Eof, Abort }; - status st = status::Continue; - while (st == status::Continue) { - protected_call( - [&]() { - auto p = pos(); - check_interrupted(); - name id; - switch (curr()) { - case scanner::token::Period: - display_proof_state_if_interactive(s); - show_tactic_prompt(); - next(); - break; - case scanner::token::Eof: - st = status::Eof; - break; - case scanner::token::Id: - id = curr_name(); - if (id == g_back) { - back_cmd(stack, s); - } else if (id == g_done) { - pr = done_cmd(s, ctx, expected_type); - if (pr) - st = status::Done; - } else if (id == g_abort) { - next(); - st = status::Abort; - } else { - tactic_cmd(stack, s); - } - break; - case scanner::token::ScriptBlock: - tactic_cmd(stack, s); - break; - case scanner::token::CommandId: - st = status::Abort; - break; - default: - next(); - throw tactic_cmd_error("invalid tactic command, identifier expected", p, s); - } - }, - [&]() { - // Keep consuming tokens until we find a Command or End-of-file or Tactic command - show_tactic_prompt(); - while (curr() != scanner::token::CommandId && curr() != scanner::token::Eof && - curr() != scanner::token::Period && !curr_is_tactic_cmd()) - next(); - if (curr_is_period()) - next(); - }); - } - switch (st) { - case status::Done: return *pr; - case status::Eof: throw tactic_cmd_error("invalid tactic command, unexpected end of file", pos(), s); - case status::Abort: throw tactic_cmd_error("failed to prove theorem, proof has been aborted", pos(), s); - default: lean_unreachable(); // LCOV_EXCL_LINE - } -} - -/** - \brief Return a 'hint' tactic (if it exists) for the given metavariable. - If the metavariable is not associated with any hint, then return the - null tactic. The method also returns the position of the hint. -*/ -std::pair, pos_info> parser_imp::get_tactic_for(expr const & mvar) { - expr placeholder = m_elaborator.get_original(mvar); - auto it = m_tactic_hints.find(placeholder); - if (it != m_tactic_hints.end()) { - return mk_pair(some_tactic(it->second), pos_of(placeholder, pos())); - } else { - return mk_pair(none_tactic(), pos_of(placeholder, pos())); - } -} - -std::pair parser_imp::get_metavar_ctx_and_type(expr const & mvar, metavar_env const & menv) { - expr mvar_type = menv->instantiate_metavars(menv->get_type(mvar)); - buffer new_entries; - for (auto e : menv->get_context(mvar)) { - optional d = e.get_domain(); - optional b = e.get_body(); - if (d) d = menv->instantiate_metavars(*d); - if (b) b = menv->instantiate_metavars(*b); - if (d) - new_entries.emplace_back(e.get_name(), *d, b); - else - new_entries.emplace_back(e.get_name(), d, *b); - } - context mvar_ctx(new_entries.size(), new_entries.data()); - return mk_pair(mvar_type, mvar_ctx); -} - - -/** - \brief Try to fill the 'holes' in \c val using tactics. - The metavar_env \c menv contains the definition of the metavariables occurring in \c val. - - If a 'hole' is associated with a "hint tactic" ('show-by' and 'by' constructs), - then this will be the tactic used to "fill" the hole. Otherwise, - a tactic command sequence is expected in the input stream being parsed. -*/ -expr parser_imp::apply_tactics(expr const & val, metavar_env & menv) { - buffer mvars; - for_each(val, [&](expr const & e, unsigned) { - if (is_metavar(e)) { - expr m = e; - if (has_local_context(m)) - m = mk_metavar(metavar_name(m)); - if (std::find(mvars.begin(), mvars.end(), m) == mvars.end()) - mvars.push_back(m); - } - return true; - }); - std::sort(mvars.begin(), mvars.end(), [](expr const & e1, expr const & e2) { return is_lt(e1, e2, false); }); - for (auto mvar : mvars) { - auto p = get_metavar_ctx_and_type(mvar, menv); - expr mvar_type = p.first; - context mvar_ctx = p.second; - if (has_metavar(mvar_type)) - throw unsolved_metavar_exception(sstream() << "failed to synthesize metavars, type of " << metavar_name(mvar) << " still contains metavariables", val); - try { - proof_state s = to_proof_state(m_env, mvar_ctx, mvar_type); - std::pair, pos_info> hint_and_pos = get_tactic_for(mvar); - if (hint_and_pos.first) { - // metavariable has an associated tactic hint - s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first; - menv->assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type)); - } else { - if (curr_is_period()) { - display_proof_state_if_interactive(s); - show_tactic_prompt(); - next(); - } - expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type); - menv->assign(mvar, mvar_val); - } - } catch (type_is_not_proposition_exception &) { - throw unsolved_metavar_exception(sstream() << "failed to synthesize metavar " << metavar_name(mvar) << ", it could not be synthesized by type inference and its type is not a proposition", - val); - } - } - return menv->instantiate_metavars(val); -} -} diff --git a/src/frontends/lean/parser_types.h b/src/frontends/lean/parser_types.h deleted file mode 100644 index d172e3529..000000000 --- a/src/frontends/lean/parser_types.h +++ /dev/null @@ -1,37 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "util/name.h" -#include "util/buffer.h" -#include "util/list.h" -#include "util/luaref.h" -#include "util/name_map.h" -#include "kernel/expr.h" - -namespace lean { -typedef std::pair pos_info; -/** \brief Parameter data */ -struct parameter { - pos_info m_pos; - name m_name; - expr m_type; - bool m_implicit; - parameter(pos_info const & p, name const & n, expr const & t, bool i):m_pos(p), m_name(n), m_type(t), m_implicit(i) {} - parameter():m_pos(0, 0), m_implicit(false) {} -}; -typedef buffer parameter_buffer; - -enum class macro_arg_kind { Expr, Exprs, Parameters, Id, Ids, Int, String, Comma, Assign, Tactic, Tactics }; -struct macro { - list m_arg_kinds; - luaref m_fn; - unsigned m_precedence; - macro(list const & as, luaref const & fn, unsigned prec):m_arg_kinds(as), m_fn(fn), m_precedence(prec) {} -}; -typedef name_map macros; -} diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp deleted file mode 100644 index 711deccd8..000000000 --- a/src/frontends/lean/pp.cpp +++ /dev/null @@ -1,1521 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include -#include "util/scoped_map.h" -#include "util/exception.h" -#include "util/scoped_set.h" -#include "util/sexpr/options.h" -#include "util/interrupt.h" -#include "kernel/context.h" -#include "kernel/for_each_fn.h" -#include "kernel/find_fn.h" -#include "kernel/occurs.h" -#include "kernel/kernel.h" -#include "kernel/free_vars.h" -#include "kernel/replace_fn.h" -#include "library/context_to_lambda.h" -#include "library/placeholder.h" -#include "library/io_state_stream.h" -#include "frontends/lean/notation.h" -#include "frontends/lean/pp.h" -#include "frontends/lean/frontend.h" -#include "frontends/lean/coercion.h" -#include "frontends/lean/frontend_elaborator.h" - -#ifndef LEAN_DEFAULT_PP_MAX_DEPTH -#define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits::max() -#endif - -#ifndef LEAN_DEFAULT_PP_MAX_STEPS -#define LEAN_DEFAULT_PP_MAX_STEPS std::numeric_limits::max() -#endif - -#ifndef LEAN_DEFAULT_PP_NOTATION -#define LEAN_DEFAULT_PP_NOTATION true -#endif - -#ifndef LEAN_DEFAULT_PP_IMPLICIT -#define LEAN_DEFAULT_PP_IMPLICIT false -#endif - -#ifndef LEAN_DEFAULT_PP_COERCION -#define LEAN_DEFAULT_PP_COERCION false -#endif - -#ifndef LEAN_DEFAULT_PP_EXTRA_LETS -#define LEAN_DEFAULT_PP_EXTRA_LETS true -#endif - -#ifndef LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT -#define LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT 20 -#endif - -#ifndef LEAN_DEFAULT_PP_DEFINITION_VALUE -#define LEAN_DEFAULT_PP_DEFINITION_VALUE true -#endif - -namespace lean { -static format g_Type_fmt = highlight_builtin(format("Type")); -static format g_lambda_n_fmt = highlight_keyword(format("\u03BB")); -static format g_Pi_n_fmt = highlight_keyword(format("\u2200")); -static format g_lambda_fmt = highlight_keyword(format("fun")); -static format g_Pi_fmt = highlight_keyword(format("forall")); -static format g_arrow_n_fmt = highlight_keyword(format("\u2192")); -static format g_arrow_fmt = highlight_keyword(format("->")); -static format g_exists_n_fmt = highlight_keyword(format("\u2203")); -static format g_exists_fmt = highlight_keyword(format("exists")); -static format g_ellipsis_n_fmt= highlight(format("\u2026")); -static format g_ellipsis_fmt = highlight(format("...")); -static format g_let_fmt = highlight_keyword(format("let")); -static format g_in_fmt = highlight_keyword(format("in")); -static format g_pair_fmt = highlight_keyword(format("pair")); -static format g_proj1_fmt = highlight_keyword(format("proj1")); -static format g_proj2_fmt = highlight_keyword(format("proj2")); -static format g_assign_fmt = highlight_keyword(format(":=")); -static format g_geq_fmt = format("\u2265"); -static format g_lift_fmt = highlight_keyword(format("lift")); -static format g_inst_fmt = highlight_keyword(format("inst")); -static format g_sig_fmt = highlight_keyword(format("sig")); -static format g_heq_fmt = highlight_keyword(format("==")); -static format g_cartesian_product_fmt = highlight_keyword(format("#")); -static format g_cartesian_product_n_fmt = highlight_keyword(format("\u2A2F")); - -static name g_pp_max_depth {"lean", "pp", "max_depth"}; -static name g_pp_max_steps {"lean", "pp", "max_steps"}; -static name g_pp_implicit {"lean", "pp", "implicit"}; -static name g_pp_notation {"lean", "pp", "notation"}; -static name g_pp_extra_lets {"lean", "pp", "extra_lets"}; -static name g_pp_alias_min_weight {"lean", "pp", "alias_min_weight"}; -static name g_pp_coercion {"lean", "pp", "coercion"}; -static name g_pp_def_value {"lean", "pp", "definition_value"}; - -RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(lean pretty printer) maximum expression depth, after that it will use ellipsis"); -RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, "(lean pretty printer) maximum number of visited expressions, after that it will use ellipsis"); -RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, "(lean pretty printer) display implicit parameters"); -RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION, "(lean pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"); -RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION, "(lean pretty printer) display coercions"); -RegisterBoolOption(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS, "(lean pretty printer) introduce extra let expressions when displaying shared terms"); -RegisterUnsignedOption(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT, "(lean pretty printer) mimimal weight (approx. size) of a term to be considered a shared term"); -RegisterBoolOption(g_pp_def_value, LEAN_DEFAULT_PP_DEFINITION_VALUE, "(lean pretty printer) display definition/theorem value (i.e., the actual definition)"); - -unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } -unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } -bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); } -bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); } -bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); } -bool get_pp_extra_lets(options const & opts) { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); } -unsigned get_pp_alias_min_weight(options const & opts) { return opts.get_unsigned(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT); } -bool get_pp_def_value(options const & opts) { return opts.get_bool(g_pp_def_value, LEAN_DEFAULT_PP_DEFINITION_VALUE); } - -// ======================================= -// Prefixes for naming local aliases (auxiliary local decls) -static name g_a("a"); -static name g_b("b"); -static name g_c("c"); -// ======================================= - -/** - \brief Return a fresh name for the given abstraction or let. - By fresh, we mean a name that is not used for any constant in - abst_body(e). - - The resultant name is based on abst_name(e). -*/ -name get_unused_name(expr const & e) { - lean_assert(is_abstraction(e) || is_let(e)); - name const & n = is_abstraction(e) ? abst_name(e) : let_name(e); - name n1 = n; - unsigned i = 1; - expr const & b = is_abstraction(e) ? abst_body(e) : let_body(e); - while (occurs(n1, b)) { - n1 = name(n, i); - i++; - } - return n1; -} - -/** - \brief Replace free variable \c 0 in \c a with the name \c n. - - \remark Metavariable context is ignored. -*/ -expr replace_var_with_name(expr const & a, name const & n) { - expr c = mk_constant(n); - return replace(a, [=](expr const & m, unsigned offset) -> expr { - if (is_var(m)) { - unsigned vidx = var_idx(m); - if (vidx >= offset) - return vidx == offset ? c : mk_var(vidx - 1); - } - return m; - }); -} - -bool is_notation_decl(object const & obj) { - return dynamic_cast(obj.cell()); -} - -bool is_coercion_decl(object const & obj) { - return dynamic_cast(obj.cell()); -} - -bool is_alias_decl(object const & obj) { - return dynamic_cast(obj.cell()); -} - -bool supported_by_pp(object const & obj) { - return obj.kind() != object_kind::Neutral || is_notation_decl(obj) || is_coercion_decl(obj) || is_alias_decl(obj) || is_set_opaque(obj); -} - -/** \brief Functional object for pretty printing expressions */ -class pp_fn { - typedef scoped_map local_aliases; - typedef std::vector> local_aliases_defs; - typedef scoped_set local_names; - ro_environment m_env; - // State - local_aliases m_local_aliases; - local_aliases_defs m_local_aliases_defs; - local_names m_local_names; - unsigned m_num_steps; - name m_aux; - expr_map m_num_occs; - // Configuration - unsigned m_indent; - unsigned m_max_depth; - unsigned m_max_steps; - bool m_implict; //!< if true show implicit arguments - bool m_unicode; //!< if true use unicode chars - bool m_coercion; //!< if true show coercions - bool m_notation; //!< if true use notation - bool m_extra_lets; //!< introduce extra let-expression to cope with sharing. - unsigned m_alias_min_weight; //!< minimal weight for creating an alias - - // Create a scope for local definitions - struct mk_scope { - pp_fn & m_fn; - unsigned m_old_size; - expr_map m_num_occs; - - void update_num_occs(expr const & e) { - buffer todo; - todo.push_back(e); - while (!todo.empty()) { - expr e = todo.back(); - todo.pop_back(); - unsigned & n = m_num_occs[e]; - n++; - // we do not visit other composite expressions such as Let, Lambda and Pi, since they create new scopes - if (n == 1 && is_app(e)) { - for (unsigned i = 0; i < num_args(e); i++) - todo.push_back(arg(e, i)); - } - } - } - - mk_scope(pp_fn & fn, expr const & e):m_fn(fn), m_old_size(fn.m_local_aliases_defs.size()) { - m_fn.m_local_aliases.push(); - update_num_occs(e); - swap(m_fn.m_num_occs, m_num_occs); - } - ~mk_scope() { - lean_assert(m_old_size <= m_fn.m_local_aliases_defs.size()); - m_fn.m_local_aliases.pop(); - m_fn.m_local_aliases_defs.resize(m_old_size); - swap(m_fn.m_num_occs, m_num_occs); - } - }; - - bool has_several_occs(expr const & e) const { - auto it = m_num_occs.find(e); - if (it != m_num_occs.end()) - return it->second > 1; - else - return false; - } - - format nest(unsigned i, format const & f) { return ::lean::nest(i, f); } - - typedef std::pair result; - - bool is_coercion(expr const & e) { - return is_app(e) && num_args(e) == 2 && ::lean::is_coercion(m_env, arg(e, 0)); - } - - /** - \brief Return true iff \c e is an atomic operation. - */ - bool is_atomic(expr const & e) { - if (auto aliased_list = get_aliased(m_env, e)) { - if (m_unicode || std::any_of(aliased_list->begin(), aliased_list->end(), [](name const & a) { return a.is_safe_ascii(); })) - return true; - } - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: - return true; - case expr_kind::Value: - return to_value(e).is_atomic_pp(m_unicode, m_coercion); - case expr_kind::MetaVar: - return !metavar_lctx(e); - case expr_kind::App: - if (!m_coercion && is_coercion(e)) - return is_atomic(arg(e, 1)); - else - return false; - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: - case expr_kind::Sigma: case expr_kind::Pair: case expr_kind::Proj: - case expr_kind::HEq: - return false; - } - return false; - } - - result mk_result(format const & fmt, unsigned depth) { - return mk_pair(fmt, depth); - } - - result pp_ellipsis() { - return mk_result(m_unicode ? g_ellipsis_n_fmt : g_ellipsis_fmt, 1); - } - - result pp_var(expr const & e) { - unsigned vidx = var_idx(e); - return mk_result(compose(format("#"), format(vidx)), 1); - } - - bool has_implicit_arguments(name const & n) const { - return ::lean::has_implicit_arguments(m_env, n) && m_local_names.find(n) == m_local_names.end(); - } - - result pp_value(expr const & e) { - value const & v = to_value(e); - if (has_implicit_arguments(v.get_name())) { - return mk_result(format(get_explicit_version(m_env, v.get_name())), 1); - } else { - return mk_result(v.pp(m_unicode, m_coercion), 1); - } - } - - result pp_constant(expr const & e) { - name const & n = const_name(e); - if (is_placeholder(e)) { - return mk_result(format("_"), 1); - } else if (is_exists_fn(e)) { - // use alias when exists is used as a function symbol - return mk_result(format("Exists"), 1); - } else if (has_implicit_arguments(n)) { - return mk_result(format(get_explicit_version(m_env, n)), 1); - } else { - optional obj = m_env->find_object(const_name(e)); - if (obj && obj->is_builtin() && obj->get_name() == const_name(e)) { - // e is a constant that is referencing a builtin object. - return pp_value(obj->get_value()); - } else { - return mk_result(format(n), 1); - } - } - } - - result pp_type(expr const & e) { - if (e == Type()) { - return mk_result(g_Type_fmt, 1); - } else { - return mk_result(paren(format{g_Type_fmt, space(), ::lean::pp(ty_level(e), m_unicode)}), 1); - } - } - - /** - \brief Pretty print given expression and put parenthesis around - it IF the pp of the expression is not a simple name. - */ - result pp_child_with_paren(expr const & e, unsigned depth) { - result r = pp(e, depth + 1); - if (is_name(r.first)) { - // We do not add a parenthis if the format object is just - // a name. This can happen when \c e is a complicated - // expression, but an alias is created for it. - return r; - } else { - return mk_result(paren(r.first), r.second); - } - } - - /** - \brief Pretty print given expression and put parenthesis around - it if it is not atomic. - */ - result pp_child(expr const & e, unsigned depth) { - if (is_atomic(e)) - return pp(e, depth + 1); - else - return pp_child_with_paren(e, depth); - } - - bool is_exists_expr(expr const & e) { - return is_app(e) && arg(e, 0) == mk_exists_fn() && num_args(e) == 3; - } - - /** - \brief Collect nested quantifiers, and instantiate - variables with unused names. Store in \c r the selected names - and associated domains. Return the body of the sequence of - nested quantifiers. - */ - expr collect_nested_quantifiers(expr const & e, buffer> & r) { - lean_assert(is_exists_expr(e)); - if (is_lambda(arg(e, 2))) { - expr lambda = arg(e, 2); - name n1 = get_unused_name(lambda); - m_local_names.insert(n1); - r.emplace_back(n1, abst_domain(lambda)); - expr b = replace_var_with_name(abst_body(lambda), n1); - if (is_exists_expr(b)) - return collect_nested_quantifiers(b, r); - else - return b; - } else { - // Quantifier is not in normal form. That is, it might be - // (exists t p) where p is not a lambda - // abstraction - // So, we put it in normal form - // (exists t (fun x : t, p x)) - expr new_body = mk_lambda("x", arg(e, 1), mk_app(lift_free_vars(arg(e, 2), 1), mk_var(0))); - expr normal_form = mk_app(arg(e, 0), arg(e, 1), new_body); - return collect_nested_quantifiers(normal_form, r); - } - } - - /** \brief Auxiliary function for pretty printing exists formulas */ - result pp_exists(expr const & e, unsigned depth) { - buffer> nested; - expr b = collect_nested_quantifiers(e, nested); - format head; - if (m_unicode) - head = g_exists_n_fmt; - else - head = g_exists_fmt; - format sep = comma(); - expr domain0 = nested[0].second; - // TODO(Leo): the following code is very similar to pp_abstraction - if (std::all_of(nested.begin() + 1, nested.end(), [&](std::pair const & p) { return p.second == domain0; })) { - // Domain of all binders is the same - format names = pp_bnames(nested.begin(), nested.end(), false); - result p_domain = pp_scoped_child(domain0, depth); - result p_body = pp_scoped_child(b, depth); - format sig = format{names, space(), colon(), space(), p_domain.first}; - format r_format = group(nest(m_indent, format{head, space(), sig, sep, line(), p_body.first})); - return mk_result(r_format, p_domain.second + p_body.second + 1); - } else { - auto it = nested.begin(); - auto end = nested.end(); - unsigned r_weight = 1; - // PP binders in blocks (names ... : type) - bool first = true; - format bindings; - while (it != end) { - auto it2 = it; - ++it2; - while (it2 != end && it2->second == it->second) { - ++it2; - } - result p_domain = pp_scoped_child(it->second, depth); - r_weight += p_domain.second; - format block = group(nest(m_indent, format{lp(), pp_bnames(it, it2, true), space(), colon(), space(), p_domain.first, rp()})); - if (first) { - bindings = block; - first = false; - } else { - bindings += compose(line(), block); - } - it = it2; - } - result p_body = pp_scoped_child(b, depth); - format r_format = group(nest(m_indent, format{head, space(), group(bindings), sep, line(), p_body.first})); - return mk_result(r_format, r_weight + p_body.second); - } - } - - operator_info find_op_for(expr const & e) const { - if (is_constant(e) && m_local_names.find(const_name(e)) != m_local_names.end()) - return operator_info(); - else - return ::lean::find_op_for(m_env, e, m_unicode); - } - - /** - \brief Return the operator associated with \c e. - Return the null operator if there is none. - - We say \c e has an operator associated with it, if: - - 1) \c e is associated with an operator. - - 2) It is an application, and the function is associated with an - operator. - */ - operator_info get_operator(expr const & e) { - operator_info op = find_op_for(e); - if (op) - return op; - else if (is_app(e)) - return find_op_for(arg(e, 0)); - else - return operator_info(); - } - - /** - \brief Return the precedence of the given expression - */ - unsigned get_operator_precedence(expr const & e) { - operator_info op = get_operator(e); - if (op) { - return op.get_precedence(); - } else if (is_arrow(e)) { - return g_arrow_precedence; - } else if (is_cartesian(e)) { - return g_cartesian_product_precedence; - } else if (is_lambda(e) || is_pi(e) || is_let(e) || is_exists(e) || is_sigma(e) || is_dep_pair(e)) { - return 0; - } else if (is_heq(e)) { - return g_heq_precedence; - } else { - return g_app_precedence; - } - } - - /** - \brief Return true iff the given expression has the given fixity. - */ - bool has_fixity(expr const & e, fixity fx) { - operator_info op = get_operator(e); - if (op) { - return op.get_fixity() == fx; - } else if (is_arrow(e)) { - return fixity::Infixr == fx; - } else { - return false; - } - } - - /** - \brief Pretty print the child of an infix, prefix, postfix or - mixfix operator. It will add parethesis when needed. - */ - result pp_mixfix_child(operator_info const & op, expr const & e, unsigned depth) { - if (is_atomic(e)) { - return pp(e, depth + 1); - } else { - if (op.get_precedence() < get_operator_precedence(e)) - return pp(e, depth + 1); - else - return pp_child_with_paren(e, depth); - } - } - - /** - \brief Pretty print the child of an associative infix - operator. It will add parethesis when needed. - */ - result pp_infix_child(operator_info const & op, expr const & e, unsigned depth, fixity fx) { - if (is_atomic(e)) { - return pp(e, depth + 1); - } else { - unsigned e_prec = get_operator_precedence(e); - if (op.get_precedence() < e_prec) - return pp(e, depth + 1); - else if (op.get_precedence() == e_prec && has_fixity(e, fx)) - return pp(e, depth + 1); - else - return pp_child_with_paren(e, depth); - } - } - - result mk_infix(operator_info const & op, result const & lhs, result const & rhs) { - unsigned r_weight = lhs.second + rhs.second + 1; - format r_format = group(format{lhs.first, space(), format(op.get_op_name()), line(), rhs.first}); - return mk_result(r_format, r_weight); - } - - /** - \brief Wrapper for accessing the explicit arguments of an - application and its function. - - \remark If show_implicit is true, then we show the explicit - arguments even if the function has implicit arguments. - - \remark We also show the implicit arguments, if the - application does not have the necessary number of - arguments. - - \remark When we expose the implicit arguments, we use the - explicit version of the function. So, the user can - understand the pretty printed term. - */ - struct application { - expr const & m_app; - expr m_f; - std::vector const * m_implicit_args; - bool m_notation_enabled; - - static bool has_implicit_arguments(pp_fn const & owner, expr const & f) { - return - (is_constant(f) && owner.has_implicit_arguments(const_name(f))) || - (is_value(f) && owner.has_implicit_arguments(to_value(f).get_name())); - } - - application(expr const & e, pp_fn const & owner, bool show_implicit):m_app(e) { - ro_environment const & env = owner.m_env; - expr const & f = arg(e, 0); - if (has_implicit_arguments(owner, f)) { - name const & n = is_constant(f) ? const_name(f) : to_value(f).get_name(); - m_implicit_args = &(get_implicit_arguments(env, n)); - if (show_implicit || num_args(e) - 1 < m_implicit_args->size()) { - // we are showing implicit arguments, thus we do - // not need the bit-mask for implicit arguments - m_implicit_args = nullptr; - // we use the explicit name of f, to make it clear - // that we are exposing implicit arguments - m_f = mk_constant(get_explicit_version(env, n)); - m_notation_enabled = false; - } else { - m_f = f; - m_notation_enabled = true; - } - } else { - m_f = f; - m_implicit_args = nullptr; - m_notation_enabled = true; - } - } - - unsigned get_num_args() const { - if (m_implicit_args) { - unsigned r = 0; - for (unsigned i = 0; i < num_args(m_app) - 1; i++) { - // Remark: we need the test i >= m_implicit_args because the application - // m_app may contain more arguments than the declaration of m_f. - // Example: - // m_f was declared as - // Pi {A : Type} (a : A) : A - // Thus m_implicit_args has size 2, and contains {true, false} - // indicating that the first argument is implicit. - // Then, the actuall application is: - // f (Int -> Int) g 10 - // Assuming g has type Int -> Int. - // This application is fine and has type Int. - // We should not print the argument (Int -> Int) since it is - // implicit. - // We should view the application above as: - // (f (Int -> Int) g) 10 - // So, the arguments at position >= m_implicit_args->size() - // are explicit by default. - if (i >= m_implicit_args->size() || !(*m_implicit_args)[i]) - r++; - } - return r; - } else { - return num_args(m_app) - 1; - } - } - - expr const & get_arg(unsigned i) const { - lean_assert(i < get_num_args()); - if (m_implicit_args) { - unsigned n = num_args(m_app); - for (unsigned j = 1; j < n; j++) { - // See comment in get_num_args() - if (j - 1 >= m_implicit_args->size() || !(*m_implicit_args)[j-1]) { - // explicit argument found - if (i == 0) - return arg(m_app, j); - --i; - } - } - lean_unreachable(); // LCOV_EXCL_LINE - } else { - return arg(m_app, i + 1); - } - } - - expr const & get_function() const { - return m_f; - } - - bool notation_enabled() const { - return m_notation_enabled; - } - }; - - /** \brief Return true if the application \c app has the number of arguments expected by the operator \c op. */ - bool has_expected_num_args(application const & app, operator_info const & op) { - switch (op.get_fixity()) { - case fixity::Infix: case fixity::Infixl: case fixity::Infixr: - return app.get_num_args() == 2; - case fixity::Prefix: case fixity::Postfix: - return app.get_num_args() == 1; - case fixity::Mixfixl: case fixity::Mixfixr: - return app.get_num_args() == length(op.get_op_name_parts()); - case fixity::Mixfixc: - return app.get_num_args() == length(op.get_op_name_parts()) - 1; - case fixity::Mixfixo: - return app.get_num_args() == length(op.get_op_name_parts()) + 1; - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - /** - \brief Pretty print an application. - */ - result pp_app(expr const & e, unsigned depth) { - if (!m_coercion && is_coercion(e)) - return pp(arg(e, 1), depth); - application app(e, *this, m_implict || has_metavar(e)); - operator_info op; - if (m_notation && app.notation_enabled() && (op = get_operator(e)) && has_expected_num_args(app, op)) { - result p_arg; - format r_format; - unsigned sz; - unsigned r_weight = 1; - switch (op.get_fixity()) { - case fixity::Infix: - return mk_infix(op, pp_mixfix_child(op, app.get_arg(0), depth), pp_mixfix_child(op, app.get_arg(1), depth)); - case fixity::Infixr: - return mk_infix(op, pp_mixfix_child(op, app.get_arg(0), depth), pp_infix_child(op, app.get_arg(1), depth, fixity::Infixr)); - case fixity::Infixl: - return mk_infix(op, pp_infix_child(op, app.get_arg(0), depth, fixity::Infixl), pp_mixfix_child(op, app.get_arg(1), depth)); - case fixity::Prefix: - p_arg = pp_infix_child(op, app.get_arg(0), depth, fixity::Prefix); - sz = op.get_op_name().size(); - return mk_result(group(format{format(op.get_op_name()), nest(sz+1, format{line(), p_arg.first})}), - p_arg.second + 1); - case fixity::Postfix: - p_arg = pp_mixfix_child(op, app.get_arg(0), depth); - return mk_result(group(format{p_arg.first, space(), format(op.get_op_name())}), - p_arg.second + 1); - case fixity::Mixfixr: case fixity::Mixfixo: { - // _ ID ... _ ID - // _ ID ... _ ID _ - list parts = op.get_op_name_parts(); - auto it = parts.begin(); - unsigned num = app.get_num_args(); - for (unsigned i = 0; i < num; i++) { - result p_arg = pp_mixfix_child(op, app.get_arg(i), depth); - if (i == num - 1) { - if (op.get_fixity() == fixity::Mixfixo) - r_format += p_arg.first; - else - r_format += format{p_arg.first, space(), format(*it)}; - } else { - r_format += format{p_arg.first, space(), format(*it), line()}; - ++it; - } - r_weight += p_arg.second; - } - return mk_result(group(r_format), r_weight); - } - case fixity::Mixfixl: case fixity::Mixfixc: { - // ID _ ... _ - // ID _ ... _ ID - list parts = op.get_op_name_parts(); - auto it = parts.begin(); - unsigned num = app.get_num_args(); - for (unsigned i = 0; i < num; i++) { - result p_arg = pp_mixfix_child(op, app.get_arg(i), depth); - unsigned sz = it->size(); - if (i > 0) r_format += space(); - r_format += format{format(*it), nest(sz+1, format{line(), p_arg.first})}; - r_weight += p_arg.second; - ++it; - } - if (it != parts.end()) { - // it is Mixfixc - r_format += format{space(), format(*it)}; - } - return mk_result(group(r_format), r_weight); - }} - lean_unreachable(); // LCOV_EXCL_LINE - } else if (m_notation && is_exists_expr(e)) { - return pp_exists(e, depth); - } else { - // standard function application - expr const & f = app.get_function(); - result p; - bool is_const = is_constant(f) && !is_exists_fn(f); - if (is_const) - p = mk_result(format(const_name(f)), 1); - else if (is_choice(f)) - p = pp_child(f, depth); - else if (is_value(f)) - p = mk_result(to_value(f).pp(m_unicode, m_coercion), 1); - else - p = pp_child(f, depth); - bool simple = is_const && const_name(f).size() <= m_indent + 4; - unsigned indent = simple ? const_name(f).size()+1 : m_indent; - format r_format = p.first; - unsigned r_weight = p.second; - unsigned num = app.get_num_args(); - for (unsigned i = 0; i < num; i++) { - result p_arg = pp_child(app.get_arg(i), depth); - r_format += format{i == 0 && simple ? space() : line(), p_arg.first}; - r_weight += p_arg.second; - } - return mk_result(group(nest(indent, r_format)), r_weight); - } - } - - /** - \brief Collect nested Lambdas (or Pis), and instantiate - variables with unused names. Store in \c r the selected names - and associated domains. Return the body of the sequence of - Lambda (of Pis). - - \remark The argument B is only relevant when processing - condensed definitions. \see pp_abstraction_core. - */ - std::pair> collect_nested(expr const & e, optional T, expr_kind k, buffer> & r) { - if (e.kind() == k && (!T || is_abstraction(*T))) { - name n1 = get_unused_name(e); - m_local_names.insert(n1); - r.emplace_back(n1, abst_domain(e)); - expr b = replace_var_with_name(abst_body(e), n1); - if (T) - T = some_expr(replace_var_with_name(abst_body(*T), n1)); - return collect_nested(b, T, k, r); - } else { - return mk_pair(e, T); - } - } - - result pp_scoped_child(expr const & e, unsigned depth, unsigned prec = 0) { - if (is_atomic(e)) { - return pp(e, depth + 1, true); - } else { - mk_scope s(*this, e); - result r = pp(e, depth + 1, true); - if (m_local_aliases_defs.size() == s.m_old_size) { - if (prec <= get_operator_precedence(e)) - return r; - else - return mk_result(paren(r.first), r.second); - } else { - format r_format = g_let_fmt; - unsigned r_weight = 2; - unsigned begin = s.m_old_size; - unsigned end = m_local_aliases_defs.size(); - for (unsigned i = begin; i < end; i++) { - auto b = m_local_aliases_defs[i]; - name const & n = b.first; - format beg = i == begin ? space() : line(); - format sep = i < end - 1 ? comma() : format(); - r_format += nest(3 + 1, format{beg, format(n), space(), g_assign_fmt, nest(n.size() + 1 + 2 + 1, format{space(), b.second, sep})}); - // we do not store the alias definitin real weight. We know it is at least m_alias_min_weight - r_weight += m_alias_min_weight + 1; - } - r_format += format{line(), g_in_fmt, space(), nest(2 + 1, r.first)}; - r_weight += r.second; - return mk_pair(group(r_format), r_weight); - } - } - } - - result pp_arrow_child(expr const & e, unsigned depth) { - return pp_scoped_child(e, depth, g_arrow_precedence + 1); - } - - result pp_arrow_body(expr const & e, unsigned depth) { - return pp_scoped_child(e, depth, g_arrow_precedence); - } - - result pp_cartesian_child(expr const & e, unsigned depth) { - return pp_scoped_child(e, depth, g_cartesian_product_precedence + 1); - } - - result pp_cartesian_body(expr const & e, unsigned depth) { - return pp_scoped_child(e, depth, g_cartesian_product_precedence); - } - - template - format pp_bnames(It const & begin, It const & end, bool use_line) { - auto it = begin; - format r = format(it->first); - ++it; - for (; it != end; ++it) { - r += compose(use_line ? line() : space(), format(it->first)); - } - return r; - } - - bool is_implicit(std::vector const * implicit_args, unsigned arg_pos) { - return implicit_args && arg_pos < implicit_args->size() && (*implicit_args)[arg_pos]; - } - - /** - \brief Auxiliary method for computing where Pi can be pretty printed as an arrow. - Examples: - Pi x : Int, Pi y : Int, Int ===> return 0 - Pi A : Type, Pi x : A, Pi y : A, A ===> return 1 - Pi A : Type, Pi x : Int, A ===> return 1 - Pi A : Type, Pi x : Int, x > 0 ===> return UINT_MAX (there is no tail that can be printed as a arrow) - - If \c e is not Pi, it returns UINT_MAX - */ - unsigned get_arrow_starting_at(expr e) { - if (!is_pi(e)) - return std::numeric_limits::max(); - unsigned pos = 0; - while (is_pi(e)) { - expr e2 = abst_body(e); - unsigned num_vars = 1; - bool ok = true; - while (true) { - if (has_free_var(e2, 0, num_vars)) { - ok = false; - break; - } - if (is_pi(e2)) { - e2 = abst_body(e2); - } else { - break; - } - } - if (ok) { - return pos; - } - e = abst_body(e); - pos++; - } - return std::numeric_limits::max(); - } - - /** - \brief Pretty print Lambdas, Pis and compact definitions. - When T != 0, it is a compact definition. - A compact definition is of the form - - Defintion Name Pi(x : A), B := Lambda (x : A), C - - it is printed as - - Defintion Name (x : A) : B := C - - This method only generates the - (x : A) : B := C - for compact definitions. - - \remark if T != 0, then T is Pi(x : A), B - */ - result pp_abstraction_core(expr const & e, unsigned depth, optional T, - std::vector const * implicit_args = nullptr) { - if (is_arrow(e) && !implicit_args) { - lean_assert(!T); - result p_lhs = pp_arrow_child(abst_domain(e), depth); - result p_rhs = pp_arrow_body(abst_body(e), depth); - format r_format = group(format{p_lhs.first, space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_rhs.first}); - return mk_result(r_format, p_lhs.second + p_rhs.second + 1); - } else if (is_cartesian(e) && !implicit_args) { - lean_assert(!T); - result p_lhs = pp_cartesian_child(abst_domain(e), depth); - result p_rhs = pp_cartesian_body(abst_body(e), depth); - format r_format = group(format{p_lhs.first, space(), m_unicode ? g_cartesian_product_n_fmt : g_cartesian_product_fmt, - line(), p_rhs.first}); - return mk_result(r_format, p_lhs.second + p_rhs.second + 1); - } else { - unsigned arrow_starting_at = get_arrow_starting_at(e); - buffer> nested; - auto p = collect_nested(e, T, e.kind(), nested); - expr b = p.first; - T = p.second; - unsigned head_indent = m_indent; - format head; - if (!T && !implicit_args) { - if (m_unicode) { - head = is_lambda(e) ? g_lambda_n_fmt : (is_pi(e) ? g_Pi_n_fmt : g_sig_fmt); - head_indent = is_sigma(e) ? 4 : 2; - } else { - head = is_lambda(e) ? g_lambda_fmt : (is_pi(e) ? g_Pi_fmt : g_sig_fmt); - head_indent = is_pi(e) ? 3 : 4; - } - } - format body_sep; - if (T) { - format T_f = pp_scoped_child(*T, 0).first; - body_sep = format{space(), colon(), space(), T_f, space(), g_assign_fmt}; - } else if (implicit_args) { - // This is a little hack to pretty print Variable and - // Axiom declarations that contain implicit arguments - body_sep = compose(space(), colon()); - } else { - body_sep = comma(); - } - if (!nested.empty() && - std::all_of(nested.begin() + 1, nested.end(), [&](std::pair const & p) { - return p.second == nested[0].second; }) && - !implicit_args) { - // Domain of all binders is the same - expr domain0 = nested[0].second; - format names = pp_bnames(nested.begin(), nested.end(), false); - result p_domain = pp_scoped_child(domain0, depth); - result p_body = pp_scoped_child(b, depth); - format sig = format{names, space(), colon(), space(), p_domain.first}; - if (T) - sig = format{lp(), sig, rp()}; - format r_format = group(nest(head_indent, format{head, space(), sig, body_sep, line(), p_body.first})); - return mk_result(r_format, p_domain.second + p_body.second + 1); - } else { - auto it = nested.begin(); - auto end = nested.end(); - unsigned r_weight = 1; - unsigned arg_pos = 0; - // PP binders in blocks (names ... : type) - bool first = true; - format bindings; - while (it != end) { - auto it2 = it; - ++it2; - bool implicit = is_implicit(implicit_args, arg_pos); - ++arg_pos; - if (!implicit_args && arg_pos > arrow_starting_at) { - // The rest is an arrow - // We do not use arrow pp when implicit_args marks are used. - format block; - bool first_domain = true; - for (; it != end; ++it) { - result p_domain = pp_arrow_child(it->second, depth); - r_weight += p_domain.second; - if (first_domain) { - first_domain = false; - block = p_domain.first; - } else { - block += format{space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_domain.first}; - } - } - result p_body = pp_arrow_child(b, depth); - r_weight += p_body.second; - block += format{space(), m_unicode ? g_arrow_n_fmt : g_arrow_fmt, line(), p_body.first}; - block = group(block); - format r_format = group(nest(head_indent, format{head, space(), group(bindings), body_sep, line(), block})); - return mk_result(r_format, r_weight); - } - // Continue with standard encoding - while (it2 != end && it2->second == it->second && implicit == is_implicit(implicit_args, arg_pos)) { - ++it2; - ++arg_pos; - } - result p_domain = pp_scoped_child(it->second, depth); - r_weight += p_domain.second; - format const & par_open = implicit ? lcurly() : lp(); - format const & par_close = implicit ? rcurly() : rp(); - format block = group(nest(m_indent, format{par_open, pp_bnames(it, it2, true), space(), colon(), space(), p_domain.first, par_close})); - if (first) { - bindings = block; - first = false; - } else { - bindings += compose(line(), block); - } - it = it2; - } - result p_body = pp_scoped_child(b, depth); - format r_format = group(nest(head_indent, format{head, space(), group(bindings), body_sep, line(), p_body.first})); - return mk_result(r_format, r_weight + p_body.second); - } - } - } - - result pp_abstraction(expr const & e, unsigned depth) { - return pp_abstraction_core(e, depth, none_expr()); - } - - expr collect_nested_let(expr const & e, buffer, expr>> & bindings) { - if (is_let(e)) { - name n1 = get_unused_name(e); - m_local_names.insert(n1); - bindings.emplace_back(n1, let_type(e), let_value(e)); - expr b = replace_var_with_name(let_body(e), n1); - return collect_nested_let(b, bindings); - } else { - return e; - } - } - - result pp_let(expr const & e, unsigned depth) { - buffer, expr>> bindings; - expr body = collect_nested_let(e, bindings); - unsigned r_weight = 2; - format r_format = g_let_fmt; - unsigned sz = bindings.size(); - for (unsigned i = 0; i < sz; i++) { - auto b = bindings[i]; - name const & n = std::get<0>(b); - format beg = i == 0 ? space() : line(); - format sep = i < sz - 1 ? comma() : format(); - result p_def = pp_scoped_child(std::get<2>(b), depth+1); - optional const & type = std::get<1>(b); - if (type) { - result p_type = pp_scoped_child(*type, depth+1); - r_format += nest(3 + 1, compose(beg, group(format{format(n), space(), - colon(), nest(n.size() + 1 + 1 + 1, compose(space(), p_type.first)), space(), g_assign_fmt, - nest(m_indent, format{line(), p_def.first, sep})}))); - r_weight += p_type.second + p_def.second; - } else { - r_format += nest(3 + 1, format{beg, format(n), space(), g_assign_fmt, nest(n.size() + 1 + 2 + 1, format{space(), p_def.first, sep})}); - r_weight += p_def.second; - } - } - result p_body = pp_scoped_child(body, depth+1); - r_weight += p_body.second; - r_format += format{line(), g_in_fmt, space(), nest(2 + 1, p_body.first)}; - return mk_pair(group(r_format), r_weight); - } - - result pp_choice(expr const & e, unsigned depth) { - lean_assert(is_choice(e)); - unsigned num = get_num_choices(e); - format r_format; - unsigned r_weight = 0; - for (unsigned i = 0; i < num; i++) { - if (i > 0) - r_format += format{space(), format("|"), line()}; - expr const & c = get_choice(e, i); - result p_c = pp_child(c, depth); - r_weight += p_c.second; - r_format += p_c.first; - } - return mk_result(r_format, r_weight+1); - } - - result pp_metavar(expr const & a, unsigned depth) { - format mv_fmt = compose(format("?"), format(metavar_name(a))); - if (metavar_lctx(a)) { - format ctx_fmt; - bool first = true; - unsigned r_weight = 1; - for (local_entry const & e : metavar_lctx(a)) { - format e_fmt; - if (e.is_lift()) { - e_fmt = format{g_lift_fmt, colon(), format(e.s()), space(), format(e.n())}; - } else { - lean_assert(e.is_inst()); - auto p_e = pp_child_with_paren(e.v(), depth); - r_weight += p_e.second; - e_fmt = format{g_inst_fmt, colon(), format(e.s()), space(), nest(m_indent, p_e.first)}; - } - if (first) { - ctx_fmt = e_fmt; - first = false; - } else { - ctx_fmt += format{comma(), line(), e_fmt}; - } - } - return mk_result(group(compose(mv_fmt, nest(m_indent, format{lsb(), ctx_fmt, rsb()}))), r_weight); - } else { - return mk_result(mv_fmt, 1); - } - } - - result pp_pair(expr a, unsigned depth) { - buffer args; - unsigned indent = 5; - format r_format = g_pair_fmt; - unsigned r_weight = 1; - - auto f_r = pp_child(pair_first(a), depth); - auto s_r = pp_child(pair_second(a), depth); - r_format += nest(indent, compose(line(), f_r.first)); - r_format += nest(indent, compose(line(), s_r.first)); - r_weight += f_r.second + s_r.second; - - expr t = pair_type(a); - if (!is_cartesian(t)) { - auto t_r = pp_child(t, depth); - r_format += nest(indent, compose(line(), format{colon(), space(), t_r.first})); - r_weight += t_r.second; - } - return result(group(r_format), r_weight); - } - - result pp_proj(expr a, unsigned depth) { - unsigned i = 0; - bool first = proj_first(a); - while (is_proj(proj_arg(a)) && !proj_first(proj_arg(a))) { - a = proj_arg(a); - i++; - } - auto arg_r = pp_child(proj_arg(a), depth); - unsigned indent = 6; - format r_format = first ? g_proj1_fmt : g_proj2_fmt; - unsigned r_weight = 1 + arg_r.second;; - if (i > 0) - r_format += format{space(), format(i)}; - r_format += nest(indent, compose(line(), arg_r.first)); - return result(group(r_format), r_weight); - } - - result pp_heq(expr const & a, unsigned depth) { - result p_lhs = pp_child(heq_lhs(a), depth); - result p_rhs = pp_child(heq_rhs(a), depth); - format r_format = group(format{p_lhs.first, space(), g_heq_fmt, line(), p_rhs.first}); - return mk_result(r_format, p_lhs.second + p_rhs.second + 1); - } - - result pp(expr const & e, unsigned depth, bool main = false) { - check_system("pretty printer"); - if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) { - return pp_ellipsis(); - } else { - m_num_steps++; - if (auto aliased_list = get_aliased(m_env, e)) { - if (m_unicode) { - return mk_result(format(head(*aliased_list)), 1); - } else { - for (auto n : *aliased_list) { - if (n.is_safe_ascii()) - return mk_result(format(n), 1); - } - } - } - if (m_extra_lets && has_several_occs(e)) { - auto it = m_local_aliases.find(e); - if (it != m_local_aliases.end()) - return mk_result(format(it->second), 1); - } - result r; - if (is_choice(e)) { - return pp_choice(e, depth); - } else { - switch (e.kind()) { - case expr_kind::Var: r = pp_var(e); break; - case expr_kind::Constant: r = pp_constant(e); break; - case expr_kind::Value: r = pp_value(e); break; - case expr_kind::App: r = pp_app(e, depth); break; - case expr_kind::Lambda: - case expr_kind::Sigma: - case expr_kind::Pi: r = pp_abstraction(e, depth); break; - case expr_kind::Type: r = pp_type(e); break; - case expr_kind::Let: r = pp_let(e, depth); break; - case expr_kind::MetaVar: r = pp_metavar(e, depth); break; - case expr_kind::HEq: r = pp_heq(e, depth); break; - case expr_kind::Pair: r = pp_pair(e, depth); break; - case expr_kind::Proj: r = pp_proj(e, depth); break; - } - } - if (!main && m_extra_lets && has_several_occs(e) && r.second > m_alias_min_weight) { - name new_aux = name(m_aux, m_local_aliases_defs.size()+1); - m_local_aliases.insert(e, new_aux); - m_local_aliases_defs.emplace_back(new_aux, r.first); - return mk_result(format(new_aux), 1); - } - return r; - } - } - - void set_options(options const & opts) { - m_indent = get_pp_indent(opts); - m_max_depth = get_pp_max_depth(opts); - m_max_steps = get_pp_max_steps(opts); - m_implict = get_pp_implicit(opts); - m_unicode = get_pp_unicode(opts); - m_coercion = get_pp_coercion(opts); - m_notation = get_pp_notation(opts); - m_extra_lets = get_pp_extra_lets(opts); - m_alias_min_weight = get_pp_alias_min_weight(opts); - } - - bool uses_prefix(expr const & e, name const & prefix) { - return static_cast(find(e, [&](expr const & e) { - return - (is_constant(e) && is_prefix_of(prefix, const_name(e))) || - (is_abstraction(e) && is_prefix_of(prefix, abst_name(e))) || - (is_let(e) && is_prefix_of(prefix, let_name(e))); - })); - } - - name find_unused_prefix(expr const & e) { - if (!uses_prefix(e, g_a)) { - return g_a; - } else if (!uses_prefix(e, g_b)) { - return g_b; - } else { - unsigned i = 1; - name n(g_c, i); - while (uses_prefix(e, n)) { - i++; - n = name(g_c, i); - } - return n; - } - } - - void init(expr const & e) { - m_local_aliases.clear(); - m_local_aliases_defs.clear(); - m_num_steps = 0; - m_aux = find_unused_prefix(e); - } - -public: - pp_fn(ro_environment const & env, options const & opts): - m_env(env) { - set_options(opts); - m_num_steps = 0; - } - - format operator()(expr const & e) { - init(e); - return pp_scoped_child(e, 0).first; - } - - format pp_definition(expr const & v, expr const & t, std::vector const * implicit_args) { - init(mk_app(v, t)); - return pp_abstraction_core(v, 0, some_expr(t), implicit_args).first; - } - - format pp_pi_with_implicit_args(expr const & e, std::vector const & implicit_args) { - init(e); - return pp_abstraction_core(e, 0, none_expr(), &implicit_args).first; - } - - void register_local(name const & n) { - m_local_names.insert(n); - } -}; - -class pp_formatter_cell : public formatter_cell { - ro_environment m_env; - - format pp(expr const & e, options const & opts) { - pp_fn fn(m_env, opts); - return fn(e); - } - - format pp(context const & c, expr const & e, bool include_e, options const & opts) { - pp_fn fn(m_env, opts); - unsigned indent = get_pp_indent(opts); - format r; - bool first = true; - expr c2 = context_to_lambda(c, e); - while (is_fake_context(c2)) { - check_interrupted(); - name n1 = get_unused_name(c2); - fn.register_local(n1); - format entry = format(n1); - optional domain = fake_context_domain(c2); - optional val = fake_context_value(c2); - if (domain) - entry += format{space(), colon(), space(), fn(*domain)}; - if (val) - entry += format{space(), g_assign_fmt, nest(indent, format{line(), fn(*val)})}; - if (first) { - r = group(entry); - first = false; - } else { - r += format{comma(), line(), group(entry)}; - } - c2 = replace_var_with_name(fake_context_rest(c2), n1); - } - if (include_e) { - if (!first) { - bool unicode = get_pp_unicode(opts); - format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); - r += format{line(), turnstile, space(), fn(c2)}; - } else { - r = fn(c2); - } - return group(r); - } else { - return group(r); - } - } - - format pp_definition(char const * kwd, name const & n, expr const & t, expr const & v, options const & opts) { - unsigned indent = get_pp_indent(opts); - bool def_value = get_pp_def_value(opts); - format def_fmt; - if (def_value) { - def_fmt = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), - pp(t, opts), space(), g_assign_fmt, line(), pp(v, opts)}; - } else { - // suppress the actual definition - def_fmt = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), pp(t, opts)}; - } - return group(nest(indent, def_fmt)); - } - - format pp_compact_definition(char const * kwd, name const & n, expr const & t, expr const & v, options const & opts) { - expr it1 = t; - expr it2 = v; - while (is_pi(it1) && is_lambda(it2)) { - check_interrupted(); - if (abst_domain(it1) != abst_domain(it2)) - return pp_definition(kwd, n, t, v, opts); - it1 = abst_body(it1); - it2 = abst_body(it2); - } - if (!is_lambda(v) || is_pi(it1)) { - return pp_definition(kwd, n, t, v, opts); - } else { - lean_assert(is_lambda(v)); - std::vector const * implicit_args = nullptr; - if (has_implicit_arguments(m_env, n)) - implicit_args = &(get_implicit_arguments(m_env, n)); - pp_fn fn(m_env, opts); - format def_fmt; - bool def_value = get_pp_def_value(opts); - if (def_value) - def_fmt = fn.pp_definition(v, t, implicit_args); - else if (implicit_args) - def_fmt = fn.pp_pi_with_implicit_args(t, *implicit_args); - else - def_fmt = format{space(), colon(), space(), pp(t, opts)}; - return format{highlight_command(format(kwd)), space(), format(n), def_fmt}; - } - } - - format pp_uvar_cnstr(object const & obj, options const & opts) { - bool unicode = get_pp_unicode(opts); - return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), format(unicode ? "\u2265" : ">="), space(), ::lean::pp(obj.get_cnstr_level(), unicode)}; - } - - format pp_postulate(object const & obj, options const & opts) { - char const * kwd = obj.keyword(); - name const & n = obj.get_name(); - format r = format{highlight_command(format(kwd)), space(), format(n)}; - if (has_implicit_arguments(m_env, n)) { - pp_fn fn(m_env, opts); - r += fn.pp_pi_with_implicit_args(obj.get_type(), get_implicit_arguments(m_env, n)); - } else { - r += format{space(), colon(), space(), pp(obj.get_type(), opts)}; - } - return r; - } - - format pp_builtin_set(object const & obj, options const &) { - char const * kwd = obj.keyword(); - name const & n = obj.get_name(); - return format{highlight_command(format(kwd)), space(), format(n)}; - } - - format pp_definition(object const & obj, options const & opts) { - if (is_explicit(m_env, obj.get_name())) { - // Hide implicit arguments when pretty printing the - // explicit version on an object. - // We do that because otherwise it looks like a recursive definition. - options new_opts = update(opts, g_pp_implicit, false); - return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), new_opts); - } else { - return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts); - } - } - - format pp_notation_decl(object const & obj, options const & opts) { - notation_declaration const & n = *static_cast(obj.cell()); - expr const & d = n.get_expr(); - format d_fmt = is_constant(d) ? format(const_name(d)) : pp(d, opts); - return format{::lean::pp(n.get_op()), space(), colon(), space(), d_fmt}; - } - - format pp_coercion_decl(object const & obj, options const & opts) { - unsigned indent = get_pp_indent(opts); - coercion_declaration const & n = *static_cast(obj.cell()); - expr const & c = n.get_coercion(); - return group(format{highlight_command(format(n.keyword())), nest(indent, format({line(), pp(c, opts)}))}); - } - - format pp_alias_decl(object const & obj, options const & opts) { - alias_declaration const & alias_decl = *static_cast(obj.cell()); - name const & n = alias_decl.get_alias_name(); - expr const & d = alias_decl.get_expr(); - format d_fmt = is_constant(d) ? format(const_name(d)) : pp(d, opts); - return format{highlight_command(format(alias_decl.keyword())), space(), ::lean::pp(n), space(), colon(), space(), d_fmt}; - } - - format pp_set_opaque(object const & obj) { - return format{highlight_command(format(obj.keyword())), space(), format(get_set_opaque_id(obj)), space(), - format(get_set_opaque_flag(obj) ? "true" : "false")}; - } -public: - pp_formatter_cell(ro_environment const & env): - m_env(env) { - } - - virtual format operator()(expr const & e, options const & opts) { - return pp(e, opts); - } - - virtual format operator()(context const & c, options const & opts) { - return pp(c, Type(), false, opts); - } - - virtual format operator()(context const & c, expr const & e, bool format_ctx, options const & opts) { - if (format_ctx) { - return pp(c, e, true, opts); - } else { - pp_fn fn(m_env, opts); - expr c2 = context_to_lambda(c, e); - while (is_fake_context(c2)) { - check_interrupted(); - name n1 = get_unused_name(c2); - fn.register_local(n1); - expr const & rest = fake_context_rest(c2); - c2 = replace_var_with_name(rest, n1); - } - return fn(c2); - } - } - - virtual format operator()(object const & obj, options const & opts) { - switch (obj.kind()) { - case object_kind::UVarConstraint: return pp_uvar_cnstr(obj, opts); - case object_kind::Postulate: return pp_postulate(obj, opts); - case object_kind::Definition: return pp_definition(obj, opts); - case object_kind::Builtin: return pp_postulate(obj, opts); - case object_kind::BuiltinSet: return pp_builtin_set(obj, opts); - case object_kind::Neutral: - if (is_notation_decl(obj)) { - return pp_notation_decl(obj, opts); - } else if (is_coercion_decl(obj)) { - return pp_coercion_decl(obj, opts); - } else if (is_alias_decl(obj)) { - return pp_alias_decl(obj, opts); - } else if (is_set_opaque(obj)) { - return pp_set_opaque(obj); - } else { - // If the object is not notation or coercion - // declaration, then the object was created in - // different frontend, and we ignore it. - return format("Unknown neutral object"); - } - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - virtual format operator()(ro_environment const & env, options const & opts) { - format r; - bool first = true; - auto it = env->begin_objects(); - auto end = env->end_objects(); - for (; it != end; ++it) { - check_interrupted(); - auto obj = *it; - if (supported_by_pp(obj)) { - if (first) first = false; else r += line(); - r += operator()(obj, opts); - } - } - return r; - } - - virtual optional get_environment() const { return optional(m_env); } -}; - -formatter mk_pp_formatter(ro_environment const & env) { - return mk_formatter(pp_formatter_cell(env)); -} -} diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h deleted file mode 100644 index d007c247a..000000000 --- a/src/frontends/lean/pp.h +++ /dev/null @@ -1,19 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/sexpr/options.h" -#include "kernel/context.h" -#include "kernel/formatter.h" - -namespace lean { -class frontend; -class environment; -formatter mk_pp_formatter(ro_environment const & env); -std::ostream & operator<<(std::ostream & out, frontend const & fe); -/** \brief Return true iff the given object is supported by this pretty printer. */ -bool supported_by_pp(object const & obj); -} diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp index 35b3d0aaf..b034ecd02 100644 --- a/src/frontends/lean/register_module.cpp +++ b/src/frontends/lean/register_module.cpp @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -7,161 +7,11 @@ Author: Leonardo de Moura #include #include "util/lua.h" #include "util/script_state.h" -#include "util/sexpr/options.h" -#include "kernel/io_state.h" -#include "library/kernel_bindings.h" -#include "library/io_state_stream.h" -#include "frontends/lean/parser.h" -#include "frontends/lean/frontend.h" -#include "frontends/lean/pp.h" namespace lean { -/** \see parse_lean_expr */ -static int parse_lean_expr_core(lua_State * L, rw_shared_environment const & env, io_state & st) { - char const * src = luaL_checkstring(L, 1); - std::istringstream in(src); - script_state S = to_script_state(L); - expr r; - S.exec_unprotected([&]() { - r = parse_expr(env, st, in, "[string]", &S); - }); - return push_expr(L, r); +void open_frontend_lean(lua_State *) { + // TODO(Leo) } - -/** \see parse_lean_expr */ -static int parse_lean_expr_core(lua_State * L, rw_shared_environment const & env) { - io_state * io = get_io_state(L); - if (io == nullptr) { - io_state s(get_global_options(L), mk_pp_formatter(env)); - return parse_lean_expr_core(L, env, s); - } else { - return parse_lean_expr_core(L, env, *io); - } -} - -static int parse_lean_expr(lua_State * L) { - /* - The parse_lean_expr function in the Lua API supports different calling arguments: - 1. (string) : simplest form, it is just a string in Lean default syntax. - The string is parsed using the global environment in the Lua registry. - If the Lua registry does not contain an environment, then commands fails. - - It also uses the global state object in the registry. If there is no - state object, it will tries to create one using the global options and formatter - in the registry. - - It returns a Lean expression. - - 2. (string, env) : similar to the previous one, but the environment is explicitly - provided. - - 3. (string, env, options, formatter?) : Everything is explicitly provided in this - version. We also support a variation where the formmater is omitted. - */ - int nargs = get_nonnil_top(L); - if (nargs == 1) { - rw_shared_environment env(L); // get global environment - return parse_lean_expr_core(L, env); - } else { - rw_shared_environment env(L, 2); - if (nargs == 2) { - return parse_lean_expr_core(L, env); - } else { - options opts = to_options(L, 3); - formatter fmt = nargs == 3 ? mk_pp_formatter(env) : to_formatter(L, 4); - io_state st(opts, fmt); - return parse_lean_expr_core(L, env, st); - } - } -} - -/** \see parse_lean_cmds */ -static void parse_lean_cmds_core(lua_State * L, rw_shared_environment const & env, io_state & st) { - char const * src = luaL_checkstring(L, 1); - std::istringstream in(src); - script_state S = to_script_state(L); - S.exec_unprotected([&]() { - parse_commands(env, st, in, "[string]", &S); - }); -} - -/** \see parse_lean_cmds */ -static void parse_lean_cmds_core(lua_State * L, rw_shared_environment const & env) { - io_state * io = get_io_state(L); - if (io == nullptr) { - io_state s(get_global_options(L), mk_pp_formatter(env)); - parse_lean_cmds_core(L, env, s); - set_global_options(L, s.get_options()); - } else { - parse_lean_cmds_core(L, env, *io); - set_global_options(L, io->get_options()); - } -} - -static int parse_lean_cmds(lua_State * L) { - /* - The parse_lean_cmds function reads a sequence of Lean commands from the input string. - The supported calling arguments are equal to the ones used in parse_lean_expr. - The main difference is the function result. When calling with explicit options - the function returns an updated set of options. Otherwise it does not return anything. - */ - int nargs = get_nonnil_top(L); - if (nargs == 1) { - rw_shared_environment env(L); // get global environment - parse_lean_cmds_core(L, env); - return 0; - } else { - rw_shared_environment env(L, 2); - if (nargs == 2) { - parse_lean_cmds_core(L, env); - return 0; - } else { - options opts = to_options(L, 3); - formatter fmt = nargs == 3 ? mk_pp_formatter(env) : to_formatter(L, 4); - io_state st(opts, fmt); - parse_lean_cmds_core(L, env, st); - push_options(L, st.get_options()); - return 1; - } - } -} - -static bool g_default_trust_imported = false; - -void set_default_trust_imported_for_lua(bool f) { - g_default_trust_imported = f; -} - -static int mk_environment(lua_State * L) { - int nargs = lua_gettop(L); - environment env; - if (nargs == 0) - env->set_trusted_imported(g_default_trust_imported); - else - env->set_trusted_imported(lua_toboolean(L, 1)); - io_state ios = init_frontend(env); - return push_environment(L, env); -} - -static int mk_lean_formatter(lua_State * L) { - return push_formatter(L, mk_pp_formatter(to_environment(L, 1))); -} - -static int is_explicit(lua_State * L) { - ro_shared_environment env(L, 1); - lua_pushboolean(L, is_explicit(env, to_name_ext(L, 2))); - return 1; -} - -void open_frontend_lean(lua_State * L) { - open_macros(L); - SET_GLOBAL_FUN(mk_environment, "environment"); - SET_GLOBAL_FUN(mk_lean_formatter, "lean_formatter"); - SET_GLOBAL_FUN(parse_lean_expr, "parse_lean"); - SET_GLOBAL_FUN(parse_lean_cmds, "parse_lean_cmds"); - SET_GLOBAL_FUN(is_explicit, "is_explicit"); -} - void register_frontend_lean_module() { script_state::register_module(open_frontend_lean); } diff --git a/src/frontends/lean/register_module.h b/src/frontends/lean/register_module.h index c1e6bea4a..c231e6daf 100644 --- a/src/frontends/lean/register_module.h +++ b/src/frontends/lean/register_module.h @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -9,5 +9,4 @@ Author: Leonardo de Moura namespace lean { void open_frontend_lean(lua_State * L); void register_frontend_lean_module(); -void set_default_trust_imported_for_lua(bool f); } diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp deleted file mode 100644 index 3f72b73c8..000000000 --- a/src/frontends/lean/scanner.cpp +++ /dev/null @@ -1,487 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "util/debug.h" -#include "util/exception.h" -#include "frontends/lean/scanner.h" - -namespace lean { - -static name g_lambda_unicode("\u03BB"); -static name g_pi_unicode("\u2200"); -static name g_arrow_unicode("\u2192"); -static name g_lambda_name("fun"); -static name g_type_name("Type"); -static name g_pi_name("forall"); -static name g_let_name("let"); -static name g_in_name("in"); -static name g_heq_name("=="); -static name g_arrow_name("->"); -static name g_exists_name("exists"); -static name g_Exists_name("Exists"); -static name g_exists_unicode("\u2203"); -static name g_placeholder_name("_"); -static name g_using_name("using"); -static name g_have_name("have"); -static name g_show_name("show"); -static name g_by_name("by"); -static name g_sig_name("sig"); -static name g_pair_name("pair"); -static name g_proj1_name("proj1"); -static name g_proj2_name("proj2"); -static name g_cartesian_product_unicode("\u2A2F"); -static name g_cartesian_product("#"); - -static char g_normalized[256]; - -/** \brief Auxiliary class for initializing global variable \c g_normalized. */ -class init_normalized_table { - void set(int i, char v) { g_normalized[static_cast(i)] = v; } -public: - init_normalized_table() { - // by default all characters are in group c, - for (int i = 0; i <= 255; i++) - set(i, 'c'); - - // digits normalize to '0' - for (int i = '0'; i <= '9'; i++) - set(i, '0'); - - // characters that can be used to create ids of group a - for (int i = 'a'; i <= 'z'; i++) - set(i, 'a'); - for (int i = 'A'; i <= 'Z'; i++) - set(i, 'a'); - - set('_', 'a'); - set('\'', 'a'); - set('@', 'a'); - set('-', '-'); - - // characters that can be used to create ids of group b - for (unsigned char b : {'=', '<', '>', '^', '|', '&', '~', '+', '*', '/', '\\', '$', '%', '?', ';', '[', ']', '#'}) - set(b, 'b'); - - // punctuation - set('(', '('); - set(')', ')'); - set('{', '{'); - set('}', '}'); - set(':', ':'); - set('.', '.'); - set(',', ','); - - // spaces - set(' ', ' '); - set('\t', ' '); - set('\r', ' '); - - // new line - set('\n', '\n'); - - // double quotes for strings - set('\"', '\"'); - - // eof - set(255, -1); - } -}; - -static init_normalized_table g_init_normalized_table; - -char normalize(char c) { - return g_normalized[static_cast(c)]; -} - -scanner::scanner(std::istream& stream, char const * strm_name): - m_spos(0), - m_curr(0), - m_line(1), - m_pos(0), - m_stream(stream), - m_stream_name(strm_name), - m_script_line(1), - m_script_pos(0) { - next(); -} - -scanner::~scanner() { -} - -void scanner::add_command_keyword(name const & n) { - m_commands = cons(n, m_commands); -} - -void scanner::throw_exception(char const * msg) { - throw parser_exception(msg, m_stream_name.c_str(), m_line, m_spos); -} - -void scanner::next() { - lean_assert(m_curr != EOF); - m_curr = m_stream.get(); - m_spos++; -} - -bool scanner::check_next(char c) { - lean_assert(m_curr != EOF); - bool r = m_stream.get() == c; - m_stream.unget(); - return r; -} - -bool scanner::check_next_is_digit() { - lean_assert(m_curr != EOF); - char c = m_stream.get(); - bool r = '0' <= c && c <= '9'; - m_stream.unget(); - return r; -} - -void scanner::read_single_line_comment() { - while (true) { - if (curr() == '\n') { - new_line(); - next(); - return; - } else if (curr() == EOF) { - return; - } else { - next(); - } - } -} - -bool scanner::is_command(name const & n) const { - return std::any_of(m_commands.begin(), m_commands.end(), [&](name const & c) { return c == n; }); -} - -/** \brief Auxiliary function for #read_a_symbol */ -name scanner::mk_name(name const & curr, std::string const & buf, bool only_digits) { - if (curr.is_anonymous()) { - lean_assert(!only_digits); - return name(buf.c_str()); - } else if (only_digits) { - mpz val(buf.c_str()); - if (!val.is_unsigned_int()) - throw_exception("invalid hierarchical name, numeral is too big"); - return name(curr, val.get_unsigned_int()); - } else { - return name(curr, buf.c_str()); - } -} - -scanner::token scanner::read_a_symbol() { - lean_assert(normalize(curr()) == 'a'); - m_buffer.clear(); - m_buffer += curr(); - m_name_val = name(); - next(); - bool only_digits = false; - while (true) { - if (normalize(curr()) == 'a') { - if (only_digits) - throw_exception("invalid hierarchical name, digit expected"); - m_buffer += curr(); - next(); - } else if (normalize(curr()) == '0') { - m_buffer += curr(); - next(); - } else if (curr() == ':' && check_next(':')) { - next(); - lean_assert(curr() == ':'); - next(); - m_name_val = mk_name(m_name_val, m_buffer, only_digits); - m_buffer.clear(); - only_digits = (normalize(curr()) == '0'); - } else { - m_name_val = mk_name(m_name_val, m_buffer, only_digits); - if (m_name_val == g_lambda_name) { - return token::Lambda; - } else if (m_name_val == g_pi_name) { - return token::Pi; - } else if (m_name_val == g_exists_name) { - return token::Exists; - } else if (m_name_val == g_type_name) { - return token::Type; - } else if (m_name_val == g_let_name) { - return token::Let; - } else if (m_name_val == g_in_name) { - return token::In; - } else if (m_name_val == g_sig_name) { - return token::Sig; - } else if (m_name_val == g_pair_name) { - return token::Pair; - } else if (m_name_val == g_proj1_name) { - return token::Proj1; - } else if (m_name_val == g_proj2_name) { - return token::Proj2; - } else if (m_name_val == g_placeholder_name) { - return token::Placeholder; - } else if (m_name_val == g_have_name) { - return token::Have; - } else if (m_name_val == g_show_name) { - return token::Show; - } else if (m_name_val == g_by_name) { - return token::By; - } else if (m_name_val == g_Exists_name) { - m_name_val = g_exists_name; - return token::Id; - } else { - return is_command(m_name_val) ? token::CommandId : token::Id; - } - } - } -} - -scanner::token scanner::read_b_symbol(char prev) { - lean_assert(normalize(curr()) == 'b' || curr() == '-'); - m_buffer.clear(); - if (prev != 0) - m_buffer += prev; - m_buffer += curr(); - next(); - while (true) { - if (normalize(curr()) == 'b' || curr() == '-') { - m_buffer += curr(); - next(); - } else { - m_name_val = name(m_buffer.c_str()); - if (m_name_val == g_arrow_name) - return token::Arrow; - else if (m_name_val == g_cartesian_product) - return token::CartesianProduct; - else if (m_name_val == g_heq_name) - return token::HEq; - else - return token::Id; - } - } -} - -scanner::token scanner::read_c_symbol() { - lean_assert(normalize(curr()) == 'c'); - m_buffer.clear(); - m_buffer += curr(); - next(); - while (true) { - if (normalize(curr()) == 'c') { - m_buffer += curr(); - next(); - } else { - m_name_val = name(m_buffer.c_str()); - if (m_name_val == g_arrow_unicode) - return token::Arrow; - if (m_name_val == g_cartesian_product_unicode) - return token::CartesianProduct; - else if (m_name_val == g_lambda_unicode) - return token::Lambda; - else if (m_name_val == g_pi_unicode) - return token::Pi; - else if (m_name_val == g_exists_unicode) - return token::Exists; - else - return token::Id; - } - } -} - -scanner::token scanner::read_number(bool pos) { - lean_assert('0' <= curr() && curr() <= '9'); - mpq q(1); - m_num_val = curr() - '0'; - next(); - bool is_decimal = false; - - while (true) { - char c = curr(); - if ('0' <= c && c <= '9') { - m_num_val = 10*m_num_val + (c - '0'); - if (is_decimal) - q *= 10; - next(); - } else if (c == '.') { - // Num. is not a decimal. It should be at least Num.0 - if (check_next_is_digit()) { - if (is_decimal) - break; - is_decimal = true; - next(); - } else { - break; - } - } else { - break; - } - } - if (is_decimal) - m_num_val /= q; - if (!pos) - m_num_val.neg(); - return is_decimal ? token::DecimalVal : token::IntVal; -} - -scanner::token scanner::read_string() { - lean_assert(curr() == '\"'); - next(); - m_buffer.clear(); - while (true) { - char c = curr(); - if (c == EOF) { - throw_exception("unexpected end of string"); - } else if (c == '\"') { - next(); - return token::StringVal; - } else if (c == '\n') { - new_line(); - } else if (c == '\\') { - next(); - c = curr(); - if (c == EOF) - throw_exception("unexpected end of string"); - if (c != '\\' && c != '\"' && c != 'n') - throw_exception("invalid escape sequence"); - if (c == 'n') - c = '\n'; - } - m_buffer += c; - next(); - } -} - -scanner::token scanner::read_script_block() { - m_script_line = m_line; - m_script_pos = m_pos; - m_buffer.clear(); - while (true) { - char c1 = curr(); - if (c1 == EOF) - throw_exception("unexpected end of script"); - next(); - if (c1 == '*') { - char c2 = curr(); - if (c2 == EOF) - throw_exception("unexpected end of script"); - next(); - if (c2 == ')') { - return token::ScriptBlock; - } else { - if (c2 == '\n') - new_line(); - m_buffer += c1; - m_buffer += c2; - } - } else { - if (c1 == '\n') - new_line(); - m_buffer += c1; - } - } -} - -scanner::token scanner::scan() { - while (true) { - char c = curr(); - m_pos = m_spos; - switch (normalize(c)) { - case ' ': next(); break; - case '\n': next(); new_line(); break; - case ':': next(); - if (curr() == '=') { - next(); - return token::Assign; - } else { - return token::Colon; - } - case ',': next(); return token::Comma; - case '.': - next(); - if (curr() == '.') { - next(); - if (curr() != '.') - throw_exception("invalid character sequence, '...' ellipsis expected"); - next(); - return token::Ellipsis; - } else { - return token::Period; - } - case '(': - next(); - if (curr() == '*') { - next(); - return read_script_block(); - } else { - return token::LeftParen; - } - case ')': next(); return token::RightParen; - case '{': next(); return token::LeftCurlyBracket; - case '}': next(); return token::RightCurlyBracket; - case 'a': return read_a_symbol(); - case 'b': return read_b_symbol(0); - case 'c': return read_c_symbol(); - case '-': - next(); - if (normalize(curr()) == '0') { - return read_number(false); - } else if (curr() == '-') { - read_single_line_comment(); - break; - } else if (normalize(curr()) == 'b') { - return read_b_symbol('-'); - } else { - m_name_val = name("-"); - return token::Id; - } - break; - case '0': return read_number(true); - case '\"': return read_string(); - case -1: return token::Eof; - default: lean_unreachable(); // LCOV_EXCL_LINE - } - } -} - -std::ostream & operator<<(std::ostream & out, scanner::token const & t) { - switch (t) { - case scanner::token::LeftParen: out << "("; break; - case scanner::token::RightParen: out << ")"; break; - case scanner::token::LeftCurlyBracket: out << "{"; break; - case scanner::token::RightCurlyBracket: out << "}"; break; - case scanner::token::Colon: out << ":"; break; - case scanner::token::Comma: out << ","; break; - case scanner::token::Period: out << "."; break; - case scanner::token::Lambda: out << g_lambda_unicode; break; - case scanner::token::Pi: out << g_pi_unicode; break; - case scanner::token::Exists: out << g_exists_unicode; break; - case scanner::token::Arrow: out << g_arrow_unicode; break; - case scanner::token::Let: out << "let"; break; - case scanner::token::In: out << "in"; break; - case scanner::token::Id: out << "Id"; break; - case scanner::token::CommandId: out << "CId"; break; - case scanner::token::IntVal: out << "Int"; break; - case scanner::token::DecimalVal: out << "Dec"; break; - case scanner::token::StringVal: out << "String"; break; - case scanner::token::Assign: out << ":="; break; - case scanner::token::Type: out << "Type"; break; - case scanner::token::Sig: out << "sig"; break; - case scanner::token::Proj1: out << "proj1"; break; - case scanner::token::Proj2: out << "proj2"; break; - case scanner::token::Pair: out << "pair"; break; - case scanner::token::Placeholder: out << "_"; break; - case scanner::token::ScriptBlock: out << "Script"; break; - case scanner::token::CartesianProduct: out << "#"; break; - case scanner::token::Have: out << "have"; break; - case scanner::token::Show: out << "show"; break; - case scanner::token::By: out << "by"; break; - case scanner::token::Ellipsis: out << "..."; break; - case scanner::token::HEq: out << "=="; break; - case scanner::token::Eof: out << "EOF"; break; - } - return out; -} -} diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h deleted file mode 100644 index 1698e9704..000000000 --- a/src/frontends/lean/scanner.h +++ /dev/null @@ -1,80 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include -#include "util/name.h" -#include "util/list.h" -#include "util/numerics/mpq.h" - -namespace lean { -/** - \brief Lean scanner. -*/ -class scanner { -public: - enum class token { - LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow, - HEq, Sig, Pair, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder, - Have, Show, By, ScriptBlock, Ellipsis, CartesianProduct, Eof - }; -protected: - int m_spos; // position in the current line of the stream - char m_curr; // current char; - - int m_line; // line - int m_pos; // start position of the token - std::istream & m_stream; - std::string m_stream_name; - - int m_script_line; // hack for saving beginning of script block line and pos - int m_script_pos; - - mpq m_num_val; - name m_name_val; - std::string m_buffer; - - list m_commands; - - void throw_exception(char const * msg); - char curr() const { return m_curr; } - void new_line() { m_line++; m_spos = 0; } - void next(); - bool check_next(char c); - bool check_next_is_digit(); - void read_single_line_comment(); - name mk_name(name const & curr, std::string const & buf, bool only_digits); - token read_a_symbol(); - token read_b_symbol(char prev); - token read_c_symbol(); - token read_number(bool pos); - token read_string(); - token read_script_block(); - bool is_command(name const & n) const; - -public: - scanner(std::istream& stream, char const * strm_name); - ~scanner(); - - /** \brief Register a new command keyword. */ - void add_command_keyword(name const & n); - void set_command_keywords(list const & l) { m_commands = l; } - - int get_line() const { return m_line; } - int get_pos() const { return m_pos; } - token scan(); - - name const & get_name_val() const { return m_name_val; } - mpq const & get_num_val() const { return m_num_val; } - std::string const & get_str_val() const { return m_buffer; } - - int get_script_block_line() const { return m_script_line; } - int get_script_block_pos() const { return m_script_pos; } -}; -std::ostream & operator<<(std::ostream & out, scanner::token const & t); -} diff --git a/src/frontends/lean/shell.cpp b/src/frontends/lean/shell.cpp deleted file mode 100644 index 8be492d96..000000000 --- a/src/frontends/lean/shell.cpp +++ /dev/null @@ -1,110 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#ifdef LEAN_USE_READLINE -#include -#include -#include -#include -#include -#include -#endif -#include -#include "frontends/lean/shell.h" -#include "frontends/lean/pp.h" - -namespace lean { -#ifdef LEAN_USE_READLINE -// Hackish wrapper for implementing a streambuf on top of the readline library -class readline_streambuf : public std::streambuf { - std::string m_buffer; - std::streamsize m_curr; - std::streamsize m_high; -protected: - virtual int_type underflow() { - while (m_curr == m_high) { - char * line = readline(""); - if (!line) { - // EOF received - return traits_type::eof(); - } else if (strlen(line) == 0) { - // ignore blank line - m_buffer.push_back('\n'); - free(line); - } else { - add_history(line); - m_buffer += line; - m_buffer.push_back('\n'); - free(line); - m_high = m_buffer.size(); - } - } - - return traits_type::to_int_type(m_buffer[m_curr]); - } - - virtual int_type uflow() { - int_type r = underflow(); - if (r != traits_type::eof()) - m_curr++; - return r; - } - - virtual int_type pbackfail(int_type c) { - if (m_curr == 0) - return traits_type::eof(); - m_curr--; - if (c != traits_type::eof()) - m_buffer[m_curr] = c; - return traits_type::eof() + 1; // something different from eof() - } - - virtual std::streamsize showmanyc() { - return m_high - m_curr; - } - -public: - readline_streambuf(): - m_curr(0), m_high(0) { - setbuf(0, 0); - } -}; - -struct readline_config { - FILE * m_devnull; - readline_config() { - // By default, the readline library echos the input in the standard output. - // We can change this behavior by setting rl_outstream to /dev/null - m_devnull = fopen("/dev/null", "a"); - rl_outstream = m_devnull; - } - ~readline_config() { - fclose(m_devnull); - } -}; -static readline_config g_readline_config; -#endif - -shell::shell(environment const & env, io_state const & ios, script_state * S):m_env(env), m_io_state(ios), m_script_state(S) { -} - -shell::shell(environment const & env, script_state * S):m_env(env), m_io_state(mk_pp_formatter(m_env)), m_script_state(S) { -} - -shell::~shell() { -} - -bool shell::operator()() { -#ifdef LEAN_USE_READLINE - readline_streambuf buf; - std::istream is(&buf); - parser p(m_env, m_io_state, is, "[stdin]", m_script_state, false, true); -#else - parser p(m_env, m_io_state, std::cin, "[stdin]", m_script_state, false, true); -#endif - return p(); -} -} diff --git a/src/frontends/lean/shell.h b/src/frontends/lean/shell.h deleted file mode 100644 index 1309f9329..000000000 --- a/src/frontends/lean/shell.h +++ /dev/null @@ -1,24 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "frontends/lean/parser.h" - -namespace lean { -/** \brief Implements the Read Eval Print loop */ -class shell { - environment m_env; - io_state m_io_state; - script_state * m_script_state; -public: - shell(environment const & env, io_state const & st, script_state * S); - shell(environment const & env, script_state * S); - ~shell(); - - bool operator()(); - io_state get_io_state() const { return m_io_state; } -}; -}