feat(frontends/lean): add parser interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/CMakeLists.txt

@@ -1,4 +1,5 @@
 add_library(lean_frontend register_module.cpp token_table.cpp
-scanner.cpp parse_table.cpp parser_config.cpp)
+scanner.cpp parse_table.cpp cmd_table.cpp parser_config.cpp parser.cpp
+parser_pos_provider.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/cmd_table.cpp

@@ -0,0 +1,19 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "frontends/lean/cmd_table.h"
+
+namespace lean {
+cmd_table get_builtin_cmds() {
+    // TODO(Leo)
+    return cmd_table();
+}
+
+tactic_cmd_table get_builtin_tactic_cmds() {
+    // TODO(Leo)
+    return tactic_cmd_table();
+}
+}

src/frontends/lean/cmd_table.h

@@ -0,0 +1,54 @@
+/*
+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 <string>
+#include <functional>
+#include "kernel/environment.h"
+
+namespace lean {
+class tactic {};  // TODO(Leo): remove after tactic framework is ported to Lean 0.2
+
+class parser;
+
+typedef std::function<environment(parser&)> command_fn;
+void register_builtin_cmd(char const * name, char const * descr, command_fn const & fn);
+
+typedef std::function<tactic(parser&)> tactic_command_fn;
+void register_builtin_cmd(char const * name, char const * descr, tactic_command_fn const & fn);
+
+template<typename F>
+struct register_builtin_cmd_tmpl {
+    register_builtin_cmd_tmpl(char const * name, char const * descr, F const & fn) {
+        register_builtin_cmd(name, descr, fn);
+    }
+};
+
+typedef register_builtin_cmd_tmpl<command_fn>        register_builtin_cmd_fn;
+typedef register_builtin_cmd_tmpl<tactic_command_fn> register_builtin_tactic_fn;
+
+template<typename F>
+struct cmd_info_tmpl {
+    name        m_name;
+    std::string m_descr;
+    F           m_fn;
+public:
+    cmd_info_tmpl(name const & n, char const * d, F const & fn):
+        m_name(n), m_descr(d), m_fn(fn) {}
+    name const & get_name() const { return m_name; }
+    std::string const & get_descr() const { return m_descr; }
+    F const & get_fn() const { return m_fn; }
+};
+
+typedef cmd_info_tmpl<command_fn>        cmd_info;
+typedef cmd_info_tmpl<tactic_command_fn> tactic_cmd_info;
+
+typedef rb_map<name, cmd_info,        name_quick_cmp> cmd_table;
+typedef rb_map<name, tactic_cmd_info, name_quick_cmp> tactic_cmd_table;
+
+cmd_table        get_builtin_cmds();
+tactic_cmd_table get_builtin_tactic_cmds();
+}

src/frontends/lean/parse_table.h

@@ -12,9 +12,9 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 
 namespace lean {
-class parser_context;
+class parser;
 namespace notation {
-typedef std::function<expr(parser_context &, unsigned, expr const *)> parse_fn;
+typedef std::function<expr(parser &, unsigned, expr const *)> parse_fn;
 
 enum class action_kind { Skip, Expr, Exprs, Binder, Binders, ScopedExpr, Ext };
 struct action_cell;

src/frontends/lean/parser.cpp

@@ -0,0 +1,150 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/interrupt.h"
+#include "util/script_exception.h"
+#include "library/io_state_stream.h"
+#include "library/parser_nested_exception.h"
+#include "library/error_handling/error_handling.h"
+#include "frontends/lean/parser.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); }
+// ==========================================
+
+parser::parser(environment const & env, io_state const & ios,
+               std::istream & strm, char const * strm_name,
+               script_state * ss, bool use_exceptions):
+    m_env(env), m_ios(ios), m_ss(ss),
+    m_verbose(true), m_use_exceptions(use_exceptions),
+    m_scanner(strm, strm_name), m_pos_table(std::make_shared<pos_info_table>()) {
+    m_found_errors = false;
+    updt_options();
+    m_next_tag_idx = 0;
+    m_curr = scanner::token_kind::Identifier;
+    protected_call([&]() { scan(); },
+                   [&]() { sync_command(); });
+}
+
+void parser::updt_options() {
+    m_verbose = get_verbose(m_ios.get_options());
+    m_show_errors = get_parser_show_errors(m_ios.get_options());
+}
+
+void parser::display_error_pos(unsigned line, unsigned pos) {
+    regular(m_env, m_ios) << get_stream_name() << ":" << line << ":";
+    if (pos != static_cast<unsigned>(-1))
+        regular(m_env, m_ios) << pos << ":";
+    regular(m_env, m_ios) << " error:";
+}
+void parser::display_error_pos(pos_info p) { display_error_pos(p.first, p.second); }
+
+void parser::display_error(char const * msg, unsigned line, unsigned pos) {
+    display_error_pos(line, pos);
+    regular(m_env, m_ios) << " " << msg << endl;
+}
+
+void parser::display_error(char const * msg, pos_info p) {
+    display_error(msg, p.first, p.second);
+}
+
+void parser::display_error(exception const & ex) {
+    parser_pos_provider pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos);
+    ::lean::display_error(regular(m_env, m_ios), &pos_provider, ex);
+}
+
+void parser::throw_parser_exception(char const * msg, pos_info p) {
+    throw parser_exception(msg, get_stream_name().c_str(), p.first, p.second);
+}
+
+void parser::throw_nested_exception(exception & ex, pos_info p) {
+    throw parser_nested_exception(std::shared_ptr<exception>(ex.clone()),
+                                  std::make_shared<parser_pos_provider>(m_pos_table, get_stream_name(), p));
+}
+
+#define CATCH(ShowError, ThrowError)                    \
+m_found_errors = true;                                  \
+if (!m_use_exceptions && m_show_errors) { ShowError ; } \
+sync();                                                 \
+if (m_use_exceptions) { ThrowError ; }
+
+void parser::protected_call(std::function<void()> && f, std::function<void()> && 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_env, m_ios) << ex.what() << endl,
+              throw);
+    } catch (parser_error & ex) {
+        CATCH(display_error(ex.what(), ex.m_pos),
+              throw_parser_exception(ex.what(), ex.m_pos));
+    } catch (interrupted & ex) {
+        reset_interrupt();
+        if (m_verbose)
+            regular(m_env, m_ios) << "!!!Interrupted!!!" << endl;
+        sync();
+        if (m_use_exceptions)
+            throw;
+    } catch (script_exception & ex) {
+         reset_interrupt();
+         CATCH(display_error(ex), throw_nested_exception(ex, m_last_script_pos));
+    } catch (exception & ex) {
+         reset_interrupt();
+         CATCH(display_error(ex), throw_nested_exception(ex, m_last_cmd_pos));
+    }
+}
+
+void parser::sync_command() {
+    // Keep consuming tokens until we find a Command or End-of-file
+    while (curr() != scanner::token_kind::CommandKeyword && curr() != scanner::token_kind::Eof)
+        next();
+}
+
+tag parser::get_tag(expr e) {
+    tag t = e.get_tag();
+    if (t == nulltag) {
+        t = m_next_tag_idx;
+        e.set_tag(t);
+        m_next_tag_idx++;
+    }
+    return t;
+}
+
+void parser::save_pos(expr e, pos_info p) {
+    m_pos_table->insert(mk_pair(get_tag(e), p));
+}
+
+expr parser::parse_expr(unsigned /* rbp */) {
+    // TODO(Leo):
+    return expr();
+}
+
+expr parser::parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp) {
+    local_decls::mk_scope scope(m_local_decls);
+    for (unsigned i = 0; i < num_locals; i++) {
+        lean_assert(is_local(locals[i]));
+        m_local_decls.insert(local_pp_name(locals[i]), local_entry(locals[i], m_local_decls.size()));
+    }
+    return parse_expr(rbp);
+}
+
+tactic parser::parse_tactic(unsigned /* rbp */) {
+    // TODO(Leo):
+    return tactic();
+}
+}

src/frontends/lean/parser.h

@@ -0,0 +1,117 @@
+/*
+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 <string>
+#include <utility>
+#include <vector>
+#include "util/scoped_map.h"
+#include "util/script_state.h"
+#include "util/name_map.h"
+#include "util/exception.h"
+#include "kernel/environment.h"
+#include "kernel/expr_maps.h"
+#include "library/io_state.h"
+#include "frontends/lean/scanner.h"
+#include "frontends/lean/cmd_table.h"
+#include "frontends/lean/parser_pos_provider.h"
+
+namespace lean {
+struct parameter {
+    pos_info    m_pos;
+    name        m_name;
+    expr        m_type;
+    binder_info m_bi;
+    parameter(pos_info const & p, name const & n, expr const & t, binder_info const & bi):
+        m_pos(p), m_name(n), m_type(t), m_bi(bi) {}
+    parameter():m_pos(0, 0) {}
+};
+
+/** \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; }
+};
+
+class parser {
+    typedef std::pair<expr, unsigned> local_entry;
+    typedef scoped_map<name, local_entry, name_hash, name_eq> local_decls;
+
+    environment             m_env;
+    io_state                m_ios;
+    script_state *          m_ss;
+    bool                    m_verbose;
+    bool                    m_use_exceptions;
+    bool                    m_show_errors;
+
+    scanner                 m_scanner;
+    scanner::token_kind     m_curr;
+    local_decls             m_local_decls;
+    pos_info                m_last_cmd_pos;
+    pos_info                m_last_script_pos;
+    unsigned                m_next_tag_idx;
+    bool                    m_found_errors;
+    pos_info_table_ptr      m_pos_table;
+
+    enum class scope_kind { Scope, Namespace, Structure };
+    std::vector<name>       m_namespace_prefixes;
+    std::vector<scope_kind> m_scope_kinds;
+
+    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(exception const & ex);
+    void throw_parser_exception(char const * msg, pos_info p);
+    void throw_nested_exception(exception & ex, pos_info p);
+
+    void sync_command();
+    void protected_call(std::function<void()> && f, std::function<void()> && sync);
+
+    tag get_tag(expr e);
+
+    void updt_options();
+public:
+    parser(environment const & env, io_state const & ios,
+           std::istream & strm, char const * str_name,
+           script_state * ss = nullptr, bool use_exceptions = false);
+
+    environment const & env() const { return m_env; }
+    io_state const & ios() const { return m_ios; }
+    script_state * ss() const { return m_ss; }
+
+    parameter parse_binder();
+    void parse_binders(buffer<parameter> & r);
+
+    expr parse_expr(unsigned rbp = 0);
+    expr parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp = 0);
+
+    tactic parse_tactic(unsigned rbp = 0);
+
+    /** \brief Return the current position information */
+    pos_info pos() const { return mk_pair(m_scanner.get_line(), m_scanner.get_pos()); }
+    void save_pos(expr e, pos_info p);
+
+    /** \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 Read the next token if the current one is not End-of-file. */
+    void next() { if (m_curr != scanner::token_kind::Eof) scan(); }
+
+    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(); }
+
+    /** parse all commands in the input stream */
+    bool operator()();
+};
+}

src/frontends/lean/parser_config.cpp

@@ -7,14 +7,15 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser_config.h"
 
 namespace lean {
+parser_config::parser_config() {
+    m_tokens      = mk_default_token_table();
+    m_cmds        = get_builtin_cmds();
+    m_tactic_cmds = get_builtin_tactic_cmds();
+}
+
 struct parser_ext : public environment_extension {
     // Configuration for a Pratt's parser
-    token_table m_tokens;
-    parse_table m_nud;
-    parse_table m_led;
-    parser_ext() {
-        m_tokens = mk_default_token_table();
-    }
+    parser_config m_cfg;
 };
 
 struct parser_ext_reg {
@@ -29,41 +30,13 @@ static environment update(environment const & env, parser_ext const & ext) {
     return env.update(g_ext.m_ext_id, std::make_shared<parser_ext>(ext));
 }
 
-token_table const & get_token_table(environment const & env) {
-    return get_extension(env).m_tokens;
+parser_config const & get_parser_config(environment const & env) {
+    return get_extension(env).m_cfg;
 }
 
-parse_table const & get_nud_parse_table(environment const & env) {
-    return get_extension(env).m_nud;
-}
-
-parse_table const & get_led_parse_table(environment const & env) {
-    return get_extension(env).m_led;
-}
-
-environment update_token_table(environment const & env, token_table const & t) {
+environment update_parser_config(environment const & env, parser_config const & c) {
     parser_ext ext = get_extension(env);
-    ext.m_tokens = t;
-    return update(env, ext);
-}
-
-environment update_nud_parse_table(environment const & env, parse_table const & t) {
-    parser_ext ext = get_extension(env);
-    ext.m_nud = t;
-    return update(env, ext);
-}
-
-environment update_led_parse_table(environment const & env, parse_table const & t) {
-    parser_ext ext = get_extension(env);
-    ext.m_led = t;
-    return update(env, ext);
-}
-
-environment update_parse_config(environment const & env, token_table const & tk, parse_table const & nud, parse_table const & led) {
-    parser_ext ext = get_extension(env);
-    ext.m_tokens = tk;
-    ext.m_nud    = nud;
-    ext.m_led    = led;
+    ext.m_cfg = c;
     return update(env, ext);
 }
 }

src/frontends/lean/parser_config.h

@@ -8,14 +8,18 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/parse_table.h"
+#include "frontends/lean/cmd_table.h"
 
 namespace lean {
-token_table const & get_token_table(environment const & env);
-parse_table const & get_nud_parse_table(environment const & env);
-parse_table const & get_led_parse_table(environment const & env);
+struct parser_config {
+    token_table      m_tokens;
+    parse_table      m_nud;
+    parse_table      m_led;
+    cmd_table        m_cmds;
+    tactic_cmd_table m_tactic_cmds;
+    parser_config();
+};
 
-environment update_token_table(environment const & env, token_table const & t);
-environment update_nud_parse_table(environment const & env, parse_table const & t);
-environment update_led_parse_table(environment const & env, parse_table const & t);
-environment update_parse_config(environment const & env, token_table const & tk, parse_table const & nud, parse_table const & led);
+parser_config const & get_parser_config(environment const & env);
+environment update_parser_config(environment const & env, parser_config const & c);
 }

src/frontends/lean/parser_pos_provider.cpp

@@ -0,0 +1,37 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <utility>
+#include <string>
+#include "frontends/lean/parser_pos_provider.h"
+
+namespace lean {
+parser_pos_provider::parser_pos_provider(pos_info_table_ptr const & pos_table,
+                                                   std::string const & strm_name, pos_info const & some_pos):
+    m_pos_table(pos_table), m_strm_name(strm_name), m_pos(some_pos) {}
+
+parser_pos_provider::~parser_pos_provider() {}
+
+std::pair<unsigned, unsigned> parser_pos_provider::get_pos_info(expr const & e) const {
+    if (!m_pos_table)
+        return get_some_pos();
+    tag t = e.get_tag();
+    if (t == nulltag)
+        return get_some_pos();
+    auto it = m_pos_table->find(t);
+    if (it == m_pos_table->end())
+        return get_some_pos();
+    return it->second;
+}
+
+std::pair<unsigned, unsigned> parser_pos_provider::get_some_pos() const {
+    return m_pos;
+}
+
+char const * parser_pos_provider::get_file_name() const {
+    return m_strm_name.c_str();
+}
+}

src/frontends/lean/parser_pos_provider.h

@@ -0,0 +1,30 @@
+/*
+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 <string>
+#include <utility>
+#include <memory>
+#include <unordered_map>
+#include "kernel/pos_info_provider.h"
+
+namespace lean {
+typedef std::pair<unsigned, unsigned> pos_info;
+typedef std::unordered_map<unsigned, pos_info> pos_info_table;
+typedef std::shared_ptr<pos_info_table> pos_info_table_ptr;
+
+class parser_pos_provider : public pos_info_provider {
+    pos_info_table_ptr m_pos_table;
+    std::string        m_strm_name;
+    pos_info           m_pos;
+public:
+    parser_pos_provider(pos_info_table_ptr const & pos_table, std::string const & strm_name, pos_info const & some_pos);
+    virtual ~parser_pos_provider();
+    virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const;
+    virtual std::pair<unsigned, unsigned> get_some_pos() const;
+    virtual char const * get_file_name() const;
+};
+}

src/frontends/lean/scanner.cpp

@@ -280,7 +280,7 @@ static name g_begin_comment_tk("--");
 static name g_begin_comment_block_tk("(--");
 
 auto scanner::scan(environment const & env) -> token_kind {
-    m_tokens = &get_token_table(env);
+    m_tokens = &get_parser_config(env).m_tokens;
     while (true) {
         char c = curr();
         m_pos  = m_spos;

src/frontends/lean/scanner.h

@@ -72,6 +72,8 @@ public:
     name const & get_name_val() const { return m_name_val; }
     std::string const & get_str_val() const { return m_buffer; }
     token_info const & get_token_info() const { lean_assert(m_token_info); return *m_token_info; }
+
+    std::string const & get_stream_name() const { return m_stream_name; }
 };
 std::ostream & operator<<(std::ostream & out, scanner::token_kind k);
 }

src/tests/frontends/lean/scanner.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <sstream>
+#include <string>
 #include "util/test.h"
 #include "util/escaped.h"
 #include "util/exception.h"
@@ -14,6 +15,16 @@ using namespace lean;
 
 #define tk scanner::token_kind
 
+token_table const & get_token_table(environment const & env) {
+    return get_parser_config(env).m_tokens;
+}
+
+environment update_token_table(environment const & env, token_table const & t) {
+    parser_config cfg = get_parser_config(env);
+    cfg.m_tokens = t;
+    return update_parser_config(env, cfg);
+}
+
 static void scan(char const * str, environment const & env = environment()) {
     std::istringstream in(str);
     scanner s(in, "[string]");