/* Copyright (c) 2014 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/flet.h" #include "util/script_state.h" #include "util/name_map.h" #include "util/exception.h" #include "util/thread_script_state.h" #include "util/script_exception.h" #include "util/worker_queue.h" #include "util/name_generator.h" #include "kernel/environment.h" #include "kernel/expr_maps.h" #include "library/io_state.h" #include "library/io_state_stream.h" #include "library/kernel_bindings.h" #include "library/definition_cache.h" #include "library/declaration_index.h" #include "frontends/lean/scanner.h" #include "frontends/lean/elaborator_context.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/parser_config.h" #include "frontends/lean/parser_pos_provider.h" #include "frontends/lean/theorem_queue.h" #include "frontends/lean/info_manager.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 throwable * clone() const { return new parser_error(m_msg.c_str(), m_pos); } virtual void rethrow() const { throw *this; } }; struct interrupt_parser {}; typedef local_decls local_expr_decls; typedef local_decls local_level_decls; typedef environment local_environment; /** \brief Extra data needed to be saved when we execute parser::push_local_scope */ struct parser_scope_stack_elem { optional m_options; name_set m_level_variables; name_set m_variables; name_set m_include_vars; unsigned m_num_undef_ids; parser_scope_stack_elem(optional const & o, name_set const & lvs, name_set const & vs, name_set const & ivs, unsigned num_undef_ids): m_options(o), m_level_variables(lvs), m_variables(vs), m_include_vars(ivs), m_num_undef_ids(num_undef_ids) {} }; typedef list parser_scope_stack; /** \brief Snapshot of the state of the Lean parser */ struct snapshot { environment m_env; local_level_decls m_lds; local_expr_decls m_eds; name_set m_lvars; // subset of m_lds that is tagged as level variable name_set m_vars; // subset of m_eds that is tagged as variable name_set m_include_vars; // subset of m_eds that must be included options m_options; parser_scope_stack m_parser_scope_stack; unsigned m_line; snapshot():m_line(0) {} snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {} snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds, name_set const & lvars, name_set const & vars, name_set const & includes, options const & opts, parser_scope_stack const & pss, unsigned line): m_env(env), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes), m_options(opts), m_parser_scope_stack(pss), m_line(line) {} }; typedef std::vector snapshot_vector; enum class keep_theorem_mode { All, DiscardImported, DiscardAll }; enum class undef_id_behavior { Error, AssumeConstant, AssumeLocal }; class parser { environment m_env; io_state m_ios; name_generator m_ngen; bool m_verbose; bool m_use_exceptions; bool m_show_errors; unsigned m_num_threads; scanner m_scanner; scanner::token_kind m_curr; local_level_decls m_local_level_decls; local_expr_decls m_local_decls; name_set m_level_variables; name_set m_variables; // subset of m_local_decls that is marked as variables name_set m_include_vars; // subset of m_local_decls that is marked as include parser_scope_stack m_parser_scope_stack; pos_info m_last_cmd_pos; pos_info m_last_script_pos; unsigned m_next_tag_idx; bool m_found_errors; bool m_used_sorry; pos_info_table m_pos_table; // By default, when the parser finds a unknown identifier, it signs an error. // When the following flag is true, it creates a constant. // This flag is when we are trying to parse mutually recursive declarations. undef_id_behavior m_undef_id_behavior; optional m_has_num; optional m_has_string; optional m_has_tactic_decls; // We process theorems in parallel theorem_queue m_theorem_queue; // info support snapshot_vector * m_snapshot_vector; info_manager * m_info_manager; info_manager m_pre_info_manager; // type information before elaboration // cache support definition_cache * m_cache; // index support declaration_index * m_index; keep_theorem_mode m_keep_theorem_mode; // curr command token name m_cmd_token; buffer m_undef_ids; void display_warning_pos(unsigned line, unsigned pos); void display_warning_pos(pos_info p); void display_error_pos(unsigned line, unsigned pos); void display_error_pos(pos_info p); void display_error(char const * msg, unsigned line, unsigned pos); void display_error(char const * msg, pos_info p); void display_error(throwable const & ex); void display_error(script_exception const & ex); void throw_parser_exception(char const * msg, pos_info p); void throw_nested_exception(throwable & ex, pos_info p); void sync_command(); void protected_call(std::function && f, std::function && sync); template typename std::result_of::type using_script(F && f) { try { script_state S = get_thread_script_state(); set_io_state set1(S, m_ios); set_environment set2(S, m_env); return f(S.get_state()); } catch (script_nested_exception & ex) { ex.get_exception().rethrow(); } } tag get_tag(expr e); expr copy_with_new_pos(expr const & e, pos_info p); expr propagate_levels(expr const & e, levels const & ls); cmd_table const & cmds() const { return get_cmd_table(env()); } parse_table const & nud() const { return get_nud_table(env()); } parse_table const & led() const { return get_led_table(env()); } unsigned curr_level_lbp() const; level parse_max_imax(bool is_max); level parse_level_id(); level parse_level_nud(); level parse_level_led(level left); void parse_imports(); void parse_command(); void parse_script(bool as_expr = false); bool parse_commands(); unsigned curr_lbp() const; expr parse_notation(parse_table t, expr * left); expr parse_nud_notation(); expr parse_led_notation(expr left); expr parse_nud(); expr parse_id(); expr parse_numeral_expr(); expr parse_decimal_expr(); expr parse_string_expr(); expr parse_binder_core(binder_info const & bi, unsigned rbp); void parse_binder_block(buffer & r, binder_info const & bi, unsigned rbp); void parse_binders_core(buffer & r, buffer * nentries, bool & last_block_delimited, unsigned rbp); local_environment parse_binders(buffer & r, buffer * nentries, bool & last_block_delimited, bool allow_empty, unsigned rbp); bool parse_local_notation_decl(buffer * entries); friend environment section_cmd(parser & p); friend environment context_cmd(parser & p); friend environment namespace_cmd(parser & p); friend environment end_scoped_cmd(parser & p); void push_local_scope(bool save_options = false); void pop_local_scope(); void save_snapshot(); void save_overload(expr const & e); void save_overload_notation(list const & as, pos_info const & p); void save_type_info(expr const & e); void save_pre_info_data(); void save_identifier_info(pos_info const & p, name const & full_id); void commit_info(unsigned line); elaborator_context mk_elaborator_context(pos_info_provider const & pp, bool check_unassigned = true); elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp); elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp); public: parser(environment const & env, io_state const & ios, std::istream & strm, char const * str_name, bool use_exceptions = false, unsigned num_threads = 1, snapshot const * s = nullptr, snapshot_vector * sv = nullptr, info_manager * im = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); ~parser(); void set_cache(definition_cache * c) { m_cache = c; } void cache_definition(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value); /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */ optional> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value); void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); } bool are_info_lines_valid(unsigned start_line, unsigned end_line) const; bool collecting_info() const { return m_info_manager; } void remove_proof_state_info(pos_info const & start, pos_info const & end); void set_index(declaration_index * i) { m_index = i; } void add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t); void add_ref_index(name const & n, pos_info const & pos); void add_abbrev_index(name const & a, name const & d); environment const & env() const { return m_env; } io_state const & ios() const { return m_ios; } local_level_decls const & get_local_level_decls() const { return m_local_level_decls; } local_expr_decls const & get_local_expr_decls() const { return m_local_decls; } bool has_tactic_decls(); expr mk_by(expr const & t, pos_info const & pos); bool keep_new_thms() const { return m_keep_theorem_mode != keep_theorem_mode::DiscardAll; } void updt_options(); options get_options() const { return m_ios.get_options(); } template void set_option(name const & n, T const & v) { m_ios.set_option(n, v); } name mk_fresh_name() { return m_ngen.next(); } name_generator mk_ngen() { return m_ngen.mk_child(); } /** \brief Return the current position information */ pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); } expr save_pos(expr e, pos_info p); expr rec_save_pos(expr const & e, pos_info p); pos_info pos_of(expr const & e, pos_info default_pos) const; pos_info pos_of(expr const & e) const { return pos_of(e, pos()); } pos_info cmd_pos() const { return m_last_cmd_pos; } name const & get_cmd_token() const { return m_cmd_token; } void set_line(unsigned p) { return m_scanner.set_line(p); } expr mk_app(expr fn, expr arg, pos_info const & p); expr mk_app(std::initializer_list const & args, pos_info const & p); unsigned num_threads() const { return m_num_threads; } void add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v); /** \brief Read the next token. */ void scan() { m_curr = m_scanner.scan(m_env); } /** \brief Return the current token */ scanner::token_kind curr() const { return m_curr; } /** \brief Return true iff the current token is an identifier */ bool curr_is_identifier() const { return curr() == scanner::token_kind::Identifier; } /** \brief Return true iff the current token is a numeral */ bool curr_is_numeral() const { return curr() == scanner::token_kind::Numeral; } /** \brief Return true iff the current token is a string */ bool curr_is_string() const { return curr() == scanner::token_kind::String; } /** \brief Return true iff the current token is a keyword */ bool curr_is_keyword() const { return curr() == scanner::token_kind::Keyword; } /** \brief Return true iff the current token is a keyword */ bool curr_is_command() const { return curr() == scanner::token_kind::CommandKeyword; } /** \brief Return true iff the current token is EOF */ bool curr_is_eof() const { return curr() == scanner::token_kind::Eof; } /** \brief Return true iff the current token is a keyword */ bool curr_is_quoted_symbol() const { return curr() == scanner::token_kind::QuotedSymbol; } /** \brief Return true iff the current token is a keyword named \c tk or an identifier named \c tk */ bool curr_is_token_or_id(name const & tk) const; /** \brief Return true iff the current token is a command, EOF, period or script block */ bool curr_is_command_like() const; /** \brief Read the next token if the current one is not End-of-file. */ void next() { if (m_curr != scanner::token_kind::Eof) scan(); } /** \brief Return true iff the current token is a keyword (or command keyword) named \c tk */ bool curr_is_token(name const & tk) const; /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */ void check_token_next(name const & tk, char const * msg); void check_token_or_id_next(name const & tk, char const * msg); /** \brief Check if the current token is an identifier, if it is return it and move to next token, otherwise throw an exception. */ name check_id_next(char const * msg); /** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token, otherwise throw an exception. */ name check_atomic_id_next(char const * msg); /** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */ name check_constant_next(char const * msg); mpq const & get_num_val() const { return m_scanner.get_num_val(); } name const & get_name_val() const { return m_scanner.get_name_val(); } std::string const & get_str_val() const { return m_scanner.get_str_val(); } token_info const & get_token_info() const { return m_scanner.get_token_info(); } std::string const & get_stream_name() const { return m_scanner.get_stream_name(); } io_state_stream regular_stream() const { return regular(env(), ios()); } io_state_stream diagnostic_stream() const { return diagnostic(env(), ios()); } unsigned get_small_nat(); unsigned parse_small_nat(); double parse_double(); bool parse_local_notation_decl() { return parse_local_notation_decl(nullptr); } level parse_level(unsigned rbp = 0); expr parse_binder(unsigned rbp); local_environment parse_binders(buffer & r, bool & last_block_delimited) { unsigned rbp = 0; bool allow_empty = false; return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp); } local_environment parse_binders(buffer & r, unsigned rbp) { bool tmp; bool allow_empty = false; return parse_binders(r, nullptr, tmp, allow_empty, rbp); } local_environment parse_optional_binders(buffer & r) { bool tmp; bool allow_empty = true; unsigned rbp = 0; return parse_binders(r, nullptr, tmp, allow_empty, rbp); } local_environment parse_binders(buffer & r, buffer & nentries) { bool tmp; bool allow_empty = false; unsigned rbp = 0; return parse_binders(r, &nentries, tmp, allow_empty, rbp); } optional parse_optional_binder_info(); binder_info parse_binder_info(); void parse_close_binder_info(optional const & bi); void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional(bi)); } /** \brief Convert an identifier into an expression (constant or local constant) based on the current scope */ expr id_to_expr(name const & id, pos_info const & p); expr parse_expr(unsigned rbp = 0); /** \brief Parse an (optionally) qualified expression. If the input is of the form : , then return the pair (some(id), expr). Otherwise, parse the next expression and return (none, expr). */ pair, expr> parse_qualified_expr(unsigned rbp = 0); expr parse_led(expr left); expr parse_scoped_expr(unsigned num_params, expr const * ps, local_environment const & lenv, unsigned rbp = 0); expr parse_scoped_expr(buffer const & ps, local_environment const & lenv, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), lenv, rbp); } expr parse_scoped_expr(unsigned num_params, expr const * ps, unsigned rbp = 0) { return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp); } expr parse_scoped_expr(buffer const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); } struct local_scope { parser & m_p; environment m_env; local_scope(parser & p, bool save_options = false); local_scope(parser & p, environment const & env); local_scope(parser & p, optional const & env); ~local_scope(); }; bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); } void add_local_level(name const & n, level const & l, bool is_variable = false); void add_local_expr(name const & n, expr const & p, bool is_variable = false); void add_local(expr const & p) { return add_local_expr(local_pp_name(p), p); } bool is_local_decl(expr const & l) const { return is_local(l) && m_local_decls.contains(local_pp_name(l)); } bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); } bool is_local_variable(name const & n) const { return m_variables.contains(n); } bool is_local_variable(expr const & e) const { return is_local_variable(local_pp_name(e)); } void include_variable(name const & n) { m_include_vars.insert(n); } void omit_variable(name const & n) { m_include_vars.erase(n); } bool is_include_variable(name const & n) const { return m_include_vars.contains(n); } void get_include_variables(buffer & vars) const; /** \brief Position of the local level declaration named \c n in the sequence of local level decls. */ unsigned get_local_level_index(name const & n) const; /** \brief Position of the local declaration named \c n in the sequence of local decls. */ unsigned get_local_index(name const & n) const; unsigned get_local_index(expr const & e) const { return get_local_index(local_pp_name(e)); } /** \brief Return the local parameter named \c n */ expr const * get_local(name const & n) const { return m_local_decls.find(n); } /** \brief Return local declarations as a list of local constants. */ list locals_to_context() const; /** \brief Return all local declarations and aliases */ list> const & get_local_entries() const { return m_local_decls.get_entries(); } /** \brief Return all local level declarations */ list> const & get_local_level_entries() const { return m_local_level_decls.get_entries(); } /** \brief By default, when the parser finds a unknown identifier, it signs an error. These scope objects temporarily change this behavior. In any scope where this object is declared, the parse creates a constant/local even when the identifier is unknown. This behavior is useful when we are trying to parse mutually recursive declarations and tactics. */ struct undef_id_to_const_scope : public flet { undef_id_to_const_scope(parser & p); }; struct undef_id_to_local_scope : public flet { undef_id_to_local_scope(parser &); }; /** \brief Return the size of the stack of undefined local constants */ unsigned get_num_undef_ids() const { return m_undef_ids.size(); } /** \brief Return the i-th undefined local constants */ expr const & get_undef_id(unsigned i) const { return m_undef_ids[i]; } /** \brief Elaborate \c e, and tolerate metavariables in the result. */ std::tuple elaborate_relaxed(expr const & e, list const & ctx = list()); /** \brief Elaborate \c e, and ensure it is a type. */ std::tuple elaborate_type(expr const & e, list const & ctx = list(), bool clear_pre_info = true); /** \brief Elaborate \c e in the given environment. */ std::tuple elaborate_at(environment const & env, expr const & e); /** \brief Elaborate \c e (making sure the result does not have metavariables). */ std::tuple elaborate(expr const & e) { return elaborate_at(m_env, e); } /** \brief Elaborate the definition n : t := v */ std::tuple elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque); /** \brief Elaborate the definition n : t := v in the given environment*/ std::tuple elaborate_definition_at(environment const & env, local_level_decls const & lls, name const & n, expr const & t, expr const & v, bool is_opaque); expr mk_sorry(pos_info const & p); bool used_sorry() const { return m_used_sorry; } void declare_sorry(); parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); } void display_information_pos(pos_info p); /** parse all commands in the input stream */ bool operator()() { return parse_commands(); } }; bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr, declaration_index * index = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr, declaration_index * index = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); void initialize_parser(); void finalize_parser(); }