feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces

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

src/emacs/lean-mode.el

@@ -24,7 +24,7 @@
 (define-generic-mode
     'lean-mode     ;; name of the mode to create
   '("--")          ;; comments start with
-  '("import" "definition" "parameter" "parameters" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords
+  '("import" "definition" "parameter" "parameters" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "precedence" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords
   '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
     ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)

src/frontends/lean/CMakeLists.txt

@@ -1,6 +1,6 @@
 add_library(lean_frontend register_module.cpp token_table.cpp
 scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
 parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp
-builtin_exprs.cpp interactive.cpp)
+builtin_exprs.cpp interactive.cpp notation_cmd.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_cmds.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/private.h"
 #include "library/locals.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/notation_cmd.h"
 
 namespace lean {
 static name g_raw("raw");
@@ -322,6 +323,11 @@ cmd_table init_cmd_table() {
     add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd));
     add_cmd(r, cmd_info("theorem",      "add new theorem", theorem_cmd));
     add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));
+    add_cmd(r, cmd_info("precedence",   "set token left binding power", precedence_cmd));
+    add_cmd(r, cmd_info("infixl",       "declare a new infix (left) notation", infixl_cmd));
+    add_cmd(r, cmd_info("infix",        "declare a new infix (left) notation", infixl_cmd));
+    add_cmd(r, cmd_info("infixr",       "declare a new infix (right) notation", infixr_cmd));
+    add_cmd(r, cmd_info("postfix",      "declare a new postfix notation", postfix_cmd));
     add_cmd(r, cmd_info("#setline",     "modify the current line number, it only affects error/report messages", set_line_cmd));
     return r;
 }

src/frontends/lean/builtin_exprs.cpp

@@ -30,17 +30,17 @@ parse_table init_nud_table() {
     action Binders(mk_binders_action());
     expr x0 = mk_var(0);
     parse_table r;
-    r.add({transition("Bool", Skip)}, Bool);
+    r = r.add({transition("Bool", Skip)}, mk_Bool());
-    r.add({transition("(", Expr), transition(")", Skip)}, x0);
+    r = r.add({transition("(", Expr), transition(")", Skip)}, x0);
-    r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
+    r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
-    r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
+    r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
-    r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
+    r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
     return r;
 }
 
 parse_table init_led_table() {
     parse_table r(false);
-    r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(0), Var(2)));
+    r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(0), Var(2)));
     return r;
 }
 }

src/frontends/lean/notation_cmd.cpp

@@ -0,0 +1,96 @@
+/*
+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 <limits>
+#include <string>
+#include "frontends/lean/parser.h"
+
+namespace lean {
+static name g_max("max");
+static name g_colon(":");
+
+static std::string parse_symbol(parser & p, char const * msg) {
+    name n;
+    if (p.curr_is_identifier() || p.curr_is_quoted_symbol()) {
+        n = p.get_name_val();
+    } else if (p.curr_is_keyword()) {
+        n = p.get_token_info().value();
+    } else {
+        throw parser_error(msg, p.pos());
+    }
+    p.next();
+    return n.to_string();
+}
+
+static optional<unsigned> parse_optional_precedence(parser & p) {
+    if (p.curr_is_numeral()) {
+        return optional<unsigned>(p.parse_small_nat());
+    } else if (p.curr_is_token_or_id(g_max)) {
+        p.next();
+        return optional<unsigned>(std::numeric_limits<unsigned>::max());
+    } else {
+        return optional<unsigned>();
+    }
+}
+
+static unsigned parse_precedence(parser & p, char const * msg) {
+    auto r = parse_optional_precedence(p);
+    if (!r)
+        throw parser_error(msg, p.pos());
+    return *r;
+}
+
+environment precedence_cmd(parser & p) {
+    std::string tk = parse_symbol(p, "invalid precedence declaration, quoted symbol or identifier expected");
+    p.check_token_next(g_colon, "invalid precedence declaration, ':' expected");
+    unsigned prec = parse_precedence(p, "invalid precedence declaration, numeral or 'max' expected");
+    return add_token(p.env(), tk.c_str(), prec);
+}
+
+enum class mixfix_kind { infixl, infixr, postfix };
+
+using notation::mk_expr_action;
+using notation::mk_skip_action;
+using notation::transition;
+
+environment mixfix_cmd(parser & p, mixfix_kind k) {
+    std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
+    optional<unsigned> prec = parse_optional_precedence(p);
+    environment env = p.env();
+    if (!prec) {
+        prec = get_precedence(get_token_table(env), tk.c_str());
+    } else if (prec != get_precedence(get_token_table(env), tk.c_str())) {
+        env = add_token(env, tk.c_str(), *prec);
+    }
+
+    if (!prec)
+        throw parser_error("invalid notation declaration, precedence was not provided, and it is not set for the given symbol, "
+                           "solution: use the 'precedence' command", p.pos());
+    if (k == mixfix_kind::infixr && *prec == 0)
+        throw parser_error("invalid infixr declaration, precedence must be greater than zero", p.pos());
+    p.check_token_next(g_colon, "invalid notation declaration, ':' expected");
+    expr f = p.parse_expr();
+    char const * tks = tk.c_str();
+    switch (k) {
+    case mixfix_kind::infixl:
+        return add_led_notation(env, {transition(tks, mk_expr_action(*prec))}, mk_app(f, Var(0), Var(1)));
+    case mixfix_kind::infixr:
+        return add_led_notation(env, {transition(tks, mk_expr_action(*prec-1))}, mk_app(f, Var(0), Var(1)));
+    case mixfix_kind::postfix:
+        return add_led_notation(env, {transition(tks, mk_skip_action())}, mk_app(f, Var(0)));
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+
+environment infixl_cmd(parser & p) { return mixfix_cmd(p, mixfix_kind::infixl); }
+environment infixr_cmd(parser & p) { return mixfix_cmd(p, mixfix_kind::infixr); }
+environment postfix_cmd(parser & p) { return mixfix_cmd(p, mixfix_kind::postfix); }
+
+environment notation_cmd(parser & p) {
+    // TODO(Leo)
+    return p.env();
+}
+}

src/frontends/lean/notation_cmd.h

@@ -0,0 +1,16 @@
+/*
+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 "kernel/environment.h"
+namespace lean {
+class parser;
+environment precedence_cmd(parser & p);
+environment notation_cmd(parser & p);
+environment infixl_cmd(parser & p);
+environment infixr_cmd(parser & p);
+environment postfix_cmd(parser & p);
+}

src/frontends/lean/parse_table.cpp

@@ -59,7 +59,7 @@ struct ext_action_cell : public action_cell {
 };
 
 action::action(action_cell * ptr):m_ptr(ptr) { lean_assert(ptr); }
-action::action():action(g_skip_action) {}
+action::action():action(mk_skip_action()) {}
 action::action(action const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
 action::action(action && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
 action::~action() { if (m_ptr) m_ptr->dec_ref(); }
@@ -128,13 +128,21 @@ void action_cell::dealloc() {
     }
 }
 
-action action::g_skip_action(new action_cell(action_kind::Skip));
+action mk_skip_action() {
-action action::g_binder_action(new action_cell(action_kind::Binder));
+    static optional<action> r;
-action action::g_binders_action(new action_cell(action_kind::Binders));
+    if (!r) r = action(new action_cell(action_kind::Skip));
-
+    return *r;
-action mk_skip_action() { return action::g_skip_action; }
+}
-action mk_binder_action() { return action::g_binder_action; }
+action mk_binder_action() {
-action mk_binders_action() { return action::g_binders_action; }
+    static optional<action> r;
+    if (!r) r = action(new action_cell(action_kind::Binder));
+    return *r;
+}
+action mk_binders_action() {
+    static optional<action> r;
+    if (!r) r = action(new action_cell(action_kind::Binders));
+    return *r;
+}
 action mk_expr_action(unsigned rbp) { return action(new expr_action_cell(rbp)); }
 action mk_exprs_action(name const & sep, expr const & rec, expr const & ini, bool right, unsigned rbp) {
     if (get_free_var_range(rec) > 2)
@@ -205,7 +213,7 @@ static void validate_transitions(bool nud, unsigned num, transition const * ts,
 }
 
 parse_table parse_table::add_core(unsigned num, transition const * ts, expr const & a, bool overload) const {
-    parse_table r(*this);
+    parse_table r(new cell(*m_ptr));
     if (num == 0) {
         if (!overload)
             r.m_ptr->m_accept = list<expr>(a);

src/frontends/lean/parser.cpp

@@ -119,11 +119,11 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
         if (m_use_exceptions)
             throw;
     } catch (script_exception & ex) {
-         reset_interrupt();
+        reset_interrupt();
-         CATCH(display_error(ex), throw_nested_exception(ex, m_last_script_pos));
+        CATCH(display_error(ex), throw_nested_exception(ex, m_last_script_pos));
     } catch (exception & ex) {
-         reset_interrupt();
+        reset_interrupt();
-         CATCH(display_error(ex), throw_nested_exception(ex, m_last_cmd_pos));
+        CATCH(display_error(ex), throw_nested_exception(ex, m_last_cmd_pos));
     }
 }
 
@@ -619,12 +619,12 @@ expr parser::parse_notation(parse_table t, expr * left) {
 }
 
 expr parser::parse_nud_notation() {
-    return parse_notation(cfg().m_nud, nullptr);
+    return parse_notation(nud(), nullptr);
 }
 
 expr parser::parse_led_notation(expr left) {
-    if (cfg().m_led.find(get_token_info().value()))
+    if (led().find(get_token_info().value()))
-        return parse_notation(cfg().m_led, &left);
+        return parse_notation(led(), &left);
     else
         return mk_app(left, parse_nud_notation(), pos_of(left));
 }
@@ -712,6 +712,7 @@ unsigned parser::curr_lbp() const {
         return 0;
     case scanner::token_kind::Identifier:     case scanner::token_kind::Numeral:
     case scanner::token_kind::Decimal:        case scanner::token_kind::String:
+    case scanner::token_kind::QuotedSymbol:
         return std::numeric_limits<unsigned>::max();
     }
     lean_unreachable(); // LCOV_EXCL_LINE

src/frontends/lean/parser.h

@@ -91,12 +91,9 @@ class parser {
 
     void updt_options();
 
-    parser_config const & cfg() const { return get_parser_config(env()); }
+    cmd_table const & cmds() const { return get_cmd_table(env()); }
-    cmd_table const & cmds() const { return cfg().m_cmds; }
+    parse_table const & nud() const { return get_nud_table(env()); }
-    parse_table const & nud() const { return cfg().m_nud; }
+    parse_table const & led() const { return get_led_table(env()); }
-    parse_table const & led() const { return cfg().m_led; }
-    /** \brief Return true if 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;
 
     unsigned curr_level_lbp() const;
     level parse_max_imax(bool is_max);
@@ -153,6 +150,14 @@ public:
     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_quoted_symbol() const { return curr() == scanner::token_kind::QuotedSymbol; }
+    /** \brief Return true if 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 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 */

src/frontends/lean/parser_config.cpp

@@ -4,42 +4,228 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
+#include "library/scoped_ext.h"
+#include "library/kernel_serializer.h"
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/builtin_cmds.h"
 #include "frontends/lean/builtin_tactic_cmds.h"
 
 namespace lean {
-parser_config::parser_config() {
+using notation::transition;
-    m_tokens      = mk_default_token_table();
+using notation::action;
-    m_nud         = get_builtin_nud_table();
+using notation::action_kind;
-    m_led         = get_builtin_led_table();
-    m_cmds        = get_builtin_cmds();
-    m_tactic_cmds = get_builtin_tactic_cmds();
-}
 
-struct parser_ext : public environment_extension {
+struct token_entry {
-    // Configuration for a Pratt's parser
+    std::string m_token;
-    parser_config m_cfg;
+    unsigned    m_prec;
+    token_entry(std::string const & tk, unsigned prec):m_token(tk), m_prec(prec) {}
 };
 
-struct parser_ext_reg {
+struct token_state {
+    token_table m_table;
+    token_state() { m_table = mk_default_token_table(); }
+};
+
+struct token_config {
+    typedef token_state  state;
+    typedef token_entry  entry;
+    static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
+        s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
+    }
+    static name const & get_class_name() {
+        static name g_class_name("token");
+        return g_class_name;
+    }
+    static std::string const & get_serialization_key() {
+        static std::string g_key("tk");
+        return g_key;
+    }
+    static void  write_entry(serializer & s, entry const & e) {
+        s << e.m_token.c_str() << e.m_prec;
+    }
+    static entry read_entry(deserializer & d) {
+        std::string tk = d.read_string();
+        unsigned prec  = d.read_unsigned();
+        return entry(tk, prec);
+    }
+};
+
+template class scoped_ext<token_config>;
+typedef scoped_ext<token_config> token_ext;
+
+environment add_token(environment const & env, char const * val, unsigned prec) {
+    return token_ext::add_entry(env, get_dummy_ios(), token_entry(val, prec));
+}
+
+token_table const & get_token_table(environment const & env) {
+    return token_ext::get_state(env).m_table;
+}
+
+serializer & operator<<(serializer & s, action const & a) {
+    s << static_cast<char>(a.kind());
+    switch (a.kind()) {
+    case action_kind::Skip: case action_kind::Binder: case action_kind::Binders:
+        break;
+    case action_kind::Expr:
+        s << a.rbp();
+        break;
+    case action_kind::Exprs:
+        s << a.get_sep() << a.get_rec() << a.get_initial() << a.is_fold_right() << a.rbp();
+        break;
+    case action_kind::ScopedExpr:
+        s << a.get_rec() << a.rbp() << a.use_lambda_abstraction();
+        break;
+    case action_kind::Ext:
+        lean_unreachable();
+    }
+    return s;
+}
+
+action read_action(deserializer & d) {
+    action_kind k = static_cast<action_kind>(d.read_char());
+    unsigned rbp;
+    switch (k) {
+    case action_kind::Skip:
+        return notation::mk_skip_action();
+    case action_kind::Binder:
+        return notation::mk_binder_action();
+    case action_kind::Binders:
+        return notation::mk_binders_action();
+    case action_kind::Expr:
+        d >> rbp;
+        return notation::mk_expr_action(rbp);
+    case action_kind::Exprs: {
+        name sep; expr rec, ini; bool is_fold_right;
+        d >> sep >> rec >> ini >> is_fold_right >> rbp;
+        return notation::mk_exprs_action(sep, rec, ini, is_fold_right, rbp);
+    }
+    case action_kind::ScopedExpr: {
+        expr rec; bool use_lambda_abstraction;
+        d >> rec >> rbp >> use_lambda_abstraction;
+        return notation::mk_scoped_expr_action(rec, rbp, use_lambda_abstraction);
+    }
+    case action_kind::Ext:
+        break;
+    }
+    lean_unreachable();
+}
+
+serializer & operator<<(serializer & s, transition const & t) {
+    s << t.get_token() << t.get_action();
+    return s;
+}
+
+transition read_transition(deserializer & d) {
+    name   n = read_name(d);
+    action a = read_action(d);
+    return transition(n, a);
+}
+
+struct notation_state {
+    parse_table      m_nud;
+    parse_table      m_led;
+    notation_state() {
+        m_nud = get_builtin_nud_table();
+        m_led = get_builtin_led_table();
+    }
+};
+
+struct notation_entry {
+    bool             m_is_nud;
+    list<transition> m_transitions;
+    expr             m_expr;
+    notation_entry():m_is_nud(true) {}
+    notation_entry(bool is_nud, list<transition> const & ts, expr const & e):
+        m_is_nud(is_nud), m_transitions(ts), m_expr(e) {}
+};
+
+struct notation_config {
+    typedef notation_state  state;
+    typedef notation_entry  entry;
+    static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
+        buffer<transition> ts;
+        to_buffer(e.m_transitions, ts);
+        if (e.m_is_nud)
+            s.m_nud = s.m_nud.add(ts.size(), ts.data(), e.m_expr, true);
+        else
+            s.m_led = s.m_led.add(ts.size(), ts.data(), e.m_expr, true);
+    }
+    static name const & get_class_name() {
+        static name g_class_name("notation");
+        return g_class_name;
+    }
+    static std::string const & get_serialization_key() {
+        static std::string g_key("nota");
+        return g_key;
+    }
+    static void  write_entry(serializer & s, entry const & e) {
+        s << e.m_is_nud << e.m_expr;
+        s << length(e.m_transitions);
+        for (auto const & t : e.m_transitions)
+            s << t;
+    }
+    static entry read_entry(deserializer & d) {
+        bool is_nud; expr e;
+        d >> is_nud >> e;
+        unsigned sz;
+        d >> sz;
+        buffer<transition> ts;
+        for (unsigned i = 0; i < sz; i++)
+            ts.push_back(read_transition(d));
+        return entry(is_nud, to_list(ts.begin(), ts.end()), e);
+    }
+};
+
+template class scoped_ext<notation_config>;
+typedef scoped_ext<notation_config> notation_ext;
+
+environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a) {
+    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(true, to_list(ts, ts+num), a));
+}
+
+environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a) {
+    return notation_ext::add_entry(env, get_dummy_ios(), notation_entry(false, to_list(ts, ts+num), a));
+}
+
+environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a) {
+    return add_nud_notation(env, ts.size(), ts.begin(), a);
+}
+
+environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a) {
+    return add_led_notation(env, ts.size(), ts.begin(), a);
+}
+
+parse_table const & get_nud_table(environment const & env) {
+    return notation_ext::get_state(env).m_nud;
+}
+
+parse_table const & get_led_table(environment const & env) {
+    return notation_ext::get_state(env).m_led;
+}
+
+struct cmd_ext : public environment_extension {
+    cmd_table        m_cmds;
+    tactic_cmd_table m_tactic_cmds;
+    cmd_ext() {
+        m_cmds        = get_builtin_cmds();
+        m_tactic_cmds = get_builtin_tactic_cmds();
+    }
+};
+
+struct cmd_ext_reg {
     unsigned m_ext_id;
-    parser_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<parser_ext>()); }
+    cmd_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<cmd_ext>()); }
 };
-static parser_ext_reg g_ext;
+static cmd_ext_reg g_ext;
-static parser_ext const & get_extension(environment const & env) {
+static cmd_ext const & get_extension(environment const & env) {
-    return static_cast<parser_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<cmd_ext const &>(env.get_extension(g_ext.m_ext_id));
 }
-static environment update(environment const & env, parser_ext const & ext) {
+cmd_table const & get_cmd_table(environment const & env) {
-    return env.update(g_ext.m_ext_id, std::make_shared<parser_ext>(ext));
+    return get_extension(env).m_cmds;
 }
-parser_config const & get_parser_config(environment const & env) {
+tactic_cmd_table const & get_tactic_cmd_table(environment const & env) {
-    return get_extension(env).m_cfg;
+    return get_extension(env).m_tactic_cmds;
-}
-environment update_parser_config(environment const & env, parser_config const & c) {
-    parser_ext ext = get_extension(env);
-    ext.m_cfg = c;
-    return update(env, ext);
 }
 }

src/frontends/lean/parser_config.h

@@ -11,15 +11,14 @@ Author: Leonardo de Moura
 #include "frontends/lean/cmd_table.h"
 
 namespace lean {
-struct parser_config {
+environment add_token(environment const & env, char const * val, unsigned prec);
-    token_table      m_tokens;
+environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a);
-    parse_table      m_nud;
+environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a);
-    parse_table      m_led;
+environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a);
-    cmd_table        m_cmds;
+environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a);
-    tactic_cmd_table m_tactic_cmds;
+token_table const & get_token_table(environment const & env);
-    parser_config();
+parse_table const & get_nud_table(environment const & env);
-};
+parse_table const & get_led_table(environment const & env);
-
+cmd_table const & get_cmd_table(environment const & env);
-parser_config const & get_parser_config(environment const & env);
+tactic_cmd_table const & get_tactic_cmd_table(environment const & env);
-environment update_parser_config(environment const & env, parser_config const & c);
 }

src/frontends/lean/scanner.cpp

@@ -22,12 +22,16 @@ void scanner::next() {
     m_spos++;
 }
 
-void scanner::check_not_eof(char const * error_msg) const {
+void scanner::check_not_eof(char const * error_msg) {
     if (curr() == EOF) throw_exception(error_msg);
 }
 
-[[ noreturn ]] void scanner::throw_exception(char const * msg) const {
+[[ noreturn ]] void scanner::throw_exception(char const * msg) {
-    throw parser_exception(msg, m_stream_name.c_str(), m_sline, m_spos);
+    unsigned line = m_sline;
+    unsigned pos  = m_spos;
+    while (curr() != EOF && !std::isspace(curr()))
+        next();
+    throw parser_exception(msg, m_stream_name.c_str(), line, pos);
 }
 
 auto scanner::read_string() -> token_kind {
@@ -56,6 +60,27 @@ auto scanner::read_string() -> token_kind {
     }
 }
 
+auto scanner::read_quoted_symbol() -> token_kind {
+    lean_assert(curr() == '`');
+    next();
+    if (std::isdigit(curr()))
+        throw_exception("first character of a quoted symbols cannot be a digit");
+    m_buffer.clear();
+    while (true) {
+        check_not_eof("unexpected quoted identifier");
+        char c = curr();
+        next();
+        if (c == '`') {
+            m_name_val = name(m_buffer.c_str());
+            return token_kind::QuotedSymbol;
+        } else if (c != ' ' && c != '\"' && c != '\n' && c != '\t') {
+            m_buffer += c;
+        } else {
+            throw_exception("invalid quoted symbol, invalid character");
+        }
+    }
+}
+
 bool scanner::is_next_digit() {
     lean_assert(curr() != EOF);
     char c = m_stream.get();
@@ -225,7 +250,6 @@ auto scanner::read_key_cmd_id() -> token_kind {
         if (info)
             key_size = 1;
     }
-
     std::string & id_part = m_buffer;
     bool is_id = is_id_first(c);
     unsigned id_size = 0;
@@ -285,7 +309,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_parser_config(env).m_tokens;
+    m_tokens = &get_token_table(env);
     while (true) {
         char c = curr();
         m_pos  = m_spos;
@@ -299,6 +323,8 @@ auto scanner::scan(environment const & env) -> token_kind {
             break;
         case '\"':
             return read_string();
+        case '`':
+            return read_quoted_symbol();
         case -1:
             return token_kind::Eof;
         default:

src/frontends/lean/scanner.h

@@ -22,7 +22,7 @@ namespace lean {
 */
 class scanner {
 public:
-    enum class token_kind {Keyword, CommandKeyword, ScriptBlock, Identifier, Numeral, Decimal, String, Eof};
+    enum class token_kind {Keyword, CommandKeyword, ScriptBlock, Identifier, Numeral, Decimal, String, QuotedSymbol, Eof};
 protected:
     token_table const * m_tokens;
     std::istream &      m_stream;
@@ -41,13 +41,13 @@ protected:
     std::string         m_buffer;
     std::string         m_aux_buffer;
 
-    [[ noreturn ]] void throw_exception(char const * msg) const;
+    [[ noreturn ]] void throw_exception(char const * msg);
     void next();
     char curr() const { return m_curr; }
     char curr_next() { char c = curr(); next(); return c; }
     void new_line() { m_sline++; m_spos = 0; }
     void update_line() { if (curr() == '\n') new_line(); }
-    void check_not_eof(char const * error_msg) const;
+    void check_not_eof(char const * error_msg);
     bool is_next_digit();
     bool is_next_id_rest();
     void move_back(std::streamoff offset);
@@ -60,6 +60,7 @@ protected:
     token_kind read_number();
     token_kind read_script_block();
     token_kind read_key_cmd_id();
+    token_kind read_quoted_symbol();
 
 public:
     scanner(std::istream & strm, char const * strm_name = nullptr);

src/frontends/lean/token_table.cpp

@@ -32,6 +32,10 @@ token_table const * find(token_table const & s, char c) {
 token_info const * value_of(token_table const & s) {
     return s.value();
 }
+optional<unsigned> get_precedence(token_table const & s, char const * token) {
+    auto it = find(s, token);
+    return it ? optional<unsigned>(it->precedence()) : optional<unsigned>();
+}
 void for_each(token_table const & s, std::function<void(char const *, token_info const &)> const & fn) {
     s.for_each([&](unsigned num, char const * keys, token_info const & info) {
             buffer<char> str;
@@ -61,7 +65,7 @@ token_table init_token_table() {
                                "variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
-                               "#setline", nullptr};
+                               "precedence", "infixl", "infixr", "infix", "postfix", "#setline", nullptr};
 
     std::pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/frontends/lean/token_table.h

@@ -35,6 +35,7 @@ token_table add_token(token_table const & s, char const * token, unsigned prec =
 token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec = 0);
 void for_each(token_table const & s, std::function<void(char const *, token_info const&)> const & fn);
 token_table const * find(token_table const & s, char c);
+optional<unsigned> get_precedence(token_table const & s, char const * token);
 token_info const * value_of(token_table const & s);
 void open_token_table(lua_State * L);
 }

src/kernel/expr.cpp

@@ -417,10 +417,20 @@ expr mk_pi(unsigned sz, expr const * domain, expr const & range) {
     return r;
 }
 
-expr Bool = mk_sort(mk_level_zero());
+expr mk_Bool() {
-expr Type = mk_sort(mk_level_one());
+    static optional<expr> Bool;
-expr mk_Bool() { return Bool; }
+    if (!Bool) Bool = mk_sort(mk_level_zero());
-expr mk_Type() { return Type; }
+    return *Bool;
+}
+
+expr mk_Type() {
+    static optional<expr> Type;
+    if (!Type) Type = mk_sort(mk_level_one());
+    return *Type;
+}
+
+expr Bool = mk_Bool();
+expr Type = mk_Type();
 
 unsigned get_depth(expr const & e) {
     switch (e.kind()) {

src/kernel/level.cpp

@@ -241,15 +241,15 @@ level mk_param_univ(name const & n) { return level(new level_param_core(level_ki
 level mk_global_univ(name const & n) { return level(new level_param_core(level_kind::Global, n)); }
 level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
 
-static std::unique_ptr<level> g_zero_ptr;
-static std::unique_ptr<level> g_one_ptr;
 level const & mk_level_zero() {
-    if (!g_zero_ptr) g_zero_ptr.reset(new level(new level_cell(level_kind::Zero, 7u)));
+    static optional<level> r;
-    return *g_zero_ptr;
+    if (!r) r = level(new level_cell(level_kind::Zero, 7u));
+    return *r;
 }
 level const & mk_level_one() {
-    if (!g_one_ptr) g_one_ptr.reset(new level(mk_succ(mk_level_zero())));
+    static optional<level> r;
-    return *g_one_ptr;
+    if (!r) r = mk_succ(mk_level_zero());
+    return *r;
 }
 // Force g_one_ptr and g_zero_ptr to be created at initialization time.
 // Purpose: avoid any kind of synchronization at mk_level_zero and mk_level_one

src/library/coercion.cpp

@@ -66,7 +66,7 @@ struct coercion_info {
         m_fun(f), m_fun_type(f_type), m_level_params(ls), m_num_args(num), m_to(cls) {}
 };
 
-struct coercion_state : public environment_extension {
+struct coercion_state {
     rb_map<name, list<coercion_info>, name_quick_cmp>         m_coercion_info;
     // m_from and m_to contain "direct" coercions
     rb_map<name, list<coercion_class>, name_quick_cmp>        m_from;

src/library/io_state.cpp

@@ -8,6 +8,11 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 
 namespace lean {
+static io_state g_dummy_ios(mk_simple_formatter());
+io_state const & get_dummy_ios() {
+    return g_dummy_ios;
+}
+
 io_state::io_state(formatter const & fmt):
     m_formatter(fmt),
     m_regular_channel(std::make_shared<stdout_channel>()),

src/library/io_state.h

@@ -41,4 +41,6 @@ public:
         set_options(get_options().update(n, v));
     }
 };
+/** \brief Return a dummy io_state that is meant to be used in contexts that require an io_state, but it is not really used */
+io_state const & get_dummy_ios();
 }

src/library/scoped_ext.cpp

@@ -69,8 +69,9 @@ environment push_scope(environment const & env, io_state const & ios, name const
     ext.m_namespaces = list<name>(new_n, ext.m_namespaces);
     ext.m_in_section = list<bool>(n.is_anonymous(), ext.m_in_section);
     environment r = update(env, ext);
-    for (auto const & t : get_exts())
+    for (auto const & t : get_exts()) {
         r = std::get<2>(t)(r);
+    }
     if (!n.is_anonymous())
         r = using_namespace(r, ios, n);
     return r;
@@ -83,8 +84,9 @@ environment pop_scope(environment const & env) {
     ext.m_namespaces = tail(ext.m_namespaces);
     ext.m_in_section = tail(ext.m_in_section);
     environment r = update(env, ext);
-    for (auto const & t : get_exts())
+    for (auto const & t : get_exts()) {
         r = std::get<3>(t)(r);
+    }
     return r;
 }
 

src/tests/frontends/lean/scanner.cpp

@@ -15,16 +15,6 @@ 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]");
@@ -108,15 +98,13 @@ static void check_keyword(char const * str, name const & expected, environment c
 static void tst1() {
     environment env;
     token_table s = get_token_table(env);
-    s = add_token(s, "+", "plus");
+    env = add_token(env, "+", 0);
-    s = add_token(s, "=", "eq");
+    env = add_token(env, "=", 0);
-    env = update_token_table(env, s);
     scan_success("a..a");
     check("a..a", {tk::Identifier, tk::Keyword, tk::Keyword, tk::Identifier});
     check("Type.{0}", {tk::Keyword, tk::Keyword, tk::Numeral, tk::Keyword});
-    s = add_token(s, "ab+cde", "weird1");
+    env = add_token(env, "ab+cde", 0);
-    s = add_token(s, "+cd", "weird2");
+    env = add_token(env, "+cd", 0);
-    env = update_token_table(env, s);
     scan_success("ab+cd", env);
     check("ab+cd", {tk::Identifier, tk::Keyword}, env);
     scan_success("ab+cde", env);
@@ -150,11 +138,9 @@ static void tst2() {
     scan_error("***");
     environment env;
     token_table s = mk_default_token_table();
-    s = add_token(s, "***", "tplus");
+    env = add_token(env, "***", 0);
-    env = update_token_table(env, s);
+    check_keyword("***", "***", env);
-    check_keyword("***", "tplus", env);
+    env = add_token(env, "+", 0);
-    s = add_token(s, "+", "plus");
-    env = update_token_table(env, s);
     check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
     check("-- testing", {});
     check("(-- testing --)", {});
@@ -165,8 +151,7 @@ static void tst2() {
     check("int -> int", {tk::Identifier, tk::Keyword, tk::Identifier});
     check("int->int", {tk::Identifier, tk::Keyword, tk::Identifier});
     check_keyword("->", "->");
-    s = add_token(s, "-+->", "arrow");
+    env = add_token(env, "-+->", 0);
-    env = update_token_table(env, s);
     check("Int -+-> Int", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
     check("x := 10", {tk::Identifier, tk::Keyword, tk::Numeral});
     check("{x}", {tk::Keyword, tk::Identifier, tk::Keyword});

tests/lean/t9.lean

@@ -0,0 +1,20 @@
+precedence `+` : 65
+precedence `*` : 75
+precedence `=` : 50
+precedence `≃` : 50
+variable N : Type.{1}
+variable a : N
+variable b : N
+variable add : N → N → N
+variable mul : N → N → N
+namespace foo
+  infixl + : add
+  infixl * : mul
+  check a+b*a
+end
+-- Notation is not avaiable outside the namespace
+check a+b*a
+namespace foo
+  -- Notation is restored
+  check a+b*a
+end

tests/lean/t9.lean.expected.out

@@ -0,0 +1,3 @@
+add a (mul b a) : N
+t9.lean:16:8: error: invalid expression
+add a (mul b a) : N