From f5e0150db38afd17d1532553f651b73a68c01489 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Aug 2013 17:25:15 -0700 Subject: [PATCH] Allow notation to be associated with arbitrary expression (instead of only constants). Signed-off-by: Leonardo de Moura --- examples/ex3.lean | 2 +- src/frontend/builtin_notation.cpp | 22 ++++----- src/frontend/frontend.cpp | 77 ++++++++++++++++--------------- src/frontend/frontend.h | 70 +++++++++++++++++++--------- src/frontend/operator_info.cpp | 19 ++------ src/frontend/operator_info.h | 21 ++++----- src/frontend/parser.cpp | 39 ++++++++-------- src/frontend/pp.cpp | 20 ++++---- src/tests/frontend/frontend.cpp | 24 +++++----- src/tests/frontend/parser.cpp | 4 +- 10 files changed, 156 insertions(+), 142 deletions(-) diff --git a/examples/ex3.lean b/examples/ex3.lean index ea1f4d8b5..cbf2e2a59 100644 --- a/examples/ex3.lean +++ b/examples/ex3.lean @@ -1,5 +1,5 @@ Definition xor (x y : Bool) : Bool := (not x) = y -Infixr 50 ⊕ xor +Infixr 50 ⊕ : xor Show xor true false Eval xor true true Eval xor true false diff --git a/src/frontend/builtin_notation.cpp b/src/frontend/builtin_notation.cpp index aaa9f58e7..9a9a31cdc 100644 --- a/src/frontend/builtin_notation.cpp +++ b/src/frontend/builtin_notation.cpp @@ -12,16 +12,16 @@ namespace lean { \brief Initialize builtin notation. */ void init_builtin_notation(frontend & f) { - f.add_prefix("\u00ac", 40, const_name(mk_not_fn())); - f.add_infixr("&&", 35, const_name(mk_and_fn())); - f.add_infixr("/\\", 35, const_name(mk_and_fn())); - f.add_infixr("\u2227", 35, const_name(mk_and_fn())); - f.add_infixr("||", 30, const_name(mk_or_fn())); - f.add_infixr("\\/", 30, const_name(mk_or_fn())); - f.add_infixr("\u2228", 30, const_name(mk_or_fn())); - f.add_infixr("=>", 25, const_name(mk_implies_fn())); - f.add_infixr("\u21D2", 25, const_name(mk_implies_fn())); - f.add_infixr("<=>", 25, const_name(mk_iff_fn())); - f.add_infixr("\u21D4", 25, const_name(mk_iff_fn())); + f.add_prefix("\u00ac", 40, mk_not_fn()); + f.add_infixr("&&", 35, mk_and_fn()); + f.add_infixr("/\\", 35, mk_and_fn()); + f.add_infixr("\u2227", 35, mk_and_fn()); + f.add_infixr("||", 30, mk_or_fn()); + f.add_infixr("\\/", 30, mk_or_fn()); + f.add_infixr("\u2228", 30, mk_or_fn()); + f.add_infixr("=>", 25, mk_implies_fn()); + f.add_infixr("\u21D2", 25, mk_implies_fn()); + f.add_infixr("<=>", 25, mk_iff_fn()); + f.add_infixr("\u21D4", 25, mk_iff_fn()); } } diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index ddc945f81..672dd2dbf 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -19,12 +19,13 @@ struct frontend::imp { // Remark: only named objects are stored in the dictionary. typedef std::unordered_map operator_table; typedef std::unordered_map implicit_table; + typedef std::unordered_map> expr_to_operator; std::atomic m_num_children; std::shared_ptr m_parent; environment m_env; operator_table m_nud; // nud table for Pratt's parser operator_table m_led; // led table for Pratt's parser - operator_table m_name_to_operator; // map internal names to operators (this is used for pretty printing) + expr_to_operator m_expr_to_operator; // map denotations to operators (this is used for pretty printing) implicit_table m_implicit_table; // track the number of implicit arguments for a symbol. bool has_children() const { return m_num_children > 0; } @@ -79,13 +80,13 @@ struct frontend::imp { insert(m_nud, op.get_op_name(), op); } - /** \brief Find the operator that is used as notation for the given internal symbol. */ - operator_info find_op_for(name const & n) const { - auto it = m_name_to_operator.find(n); - if (it != m_name_to_operator.end()) + /** \brief Find the operator that is used as notation for the given expression. */ + operator_info find_op_for(expr const & e) const { + auto it = m_expr_to_operator.find(e); + if (it != m_expr_to_operator.end()) return it->second; else if (has_parent()) - return m_parent->find_op_for(n); + return m_parent->find_op_for(e); else return operator_info(); } @@ -98,23 +99,23 @@ struct frontend::imp { // TODO } - /** \brief Remove all internal operators that are associated with the given operator symbol (aka notation) */ + /** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */ void remove_bindings(operator_info const & op) { - for (name const & n : op.get_internal_names()) { - if (has_parent() && m_parent->find_op_for(n)) { - // parent has a binding for n... we must hide it. - insert(m_name_to_operator, n, operator_info()); + for (expr const & d : op.get_exprs()) { + if (has_parent() && m_parent->find_op_for(d)) { + // parent has an association for d... we must hide it. + insert(m_expr_to_operator, d, operator_info()); } else { - m_name_to_operator.erase(n); + m_expr_to_operator.erase(d); } } } /** \brief Register the new operator in the tables for parsing and pretty printing. */ - void register_new_op(operator_info new_op, name const & n, bool led) { - new_op.add_internal_name(n); + void register_new_op(operator_info new_op, expr const & d, bool led) { + new_op.add_expr(d); insert_op(new_op, led); - insert(m_name_to_operator, n, new_op); + insert(m_expr_to_operator, d, new_op); } /** @@ -128,37 +129,37 @@ struct frontend::imp { 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, name const & n, bool led) { + void add_op(operator_info new_op, expr const & d, bool led) { name const & opn = new_op.get_op_name(); operator_info old_op = find_op(opn, led); if (!old_op) { - register_new_op(new_op, n, led); + register_new_op(new_op, d, led); } else if (old_op == new_op) { // overload if (defined_here(old_op, led)) { - old_op.add_internal_name(n); + old_op.add_expr(d); } else { // we must copy the operator because it was defined in // a parent frontend. new_op = old_op.copy(); - register_new_op(new_op, n, led); + register_new_op(new_op, d, led); } } else { report_op_redefined(old_op, new_op); remove_bindings(old_op); - register_new_op(new_op, n, led); + register_new_op(new_op, d, led); } - m_env.add_neutral_object(new notation_declaration(new_op, n)); + m_env.add_neutral_object(new notation_declaration(new_op, d)); } - void add_infix(name const & opn, unsigned p, name const & n) { add_op(infix(opn, p), n, true); } - void add_infixl(name const & opn, unsigned p, name const & n) { add_op(infixl(opn, p), n, true); } - void add_infixr(name const & opn, unsigned p, name const & n) { add_op(infixr(opn, p), n, true); } - void add_prefix(name const & opn, unsigned p, name const & n) { add_op(prefix(opn, p), n, false); } - void add_postfix(name const & opn, unsigned p, name const & n) { add_op(postfix(opn, p), n, true); } - void add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixl(sz, opns, p), n, false); } - void add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixr(sz, opns, p), n, true); } - void add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixc(sz, opns, p), n, false); } + void add_infix(name const & opn, unsigned p, expr const & d) { add_op(infix(opn, p), d, true); } + void add_infixl(name const & opn, unsigned p, expr const & d) { add_op(infixl(opn, p), d, true); } + void add_infixr(name const & opn, unsigned p, expr const & d) { add_op(infixr(opn, p), d, true); } + void add_prefix(name const & opn, unsigned p, expr const & d) { add_op(prefix(opn, p), d, false); } + void add_postfix(name const & opn, unsigned p, expr const & d) { add_op(postfix(opn, p), d, true); } + void add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixl(sz, opns, p), d, false); } + void add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixr(sz, opns, p), d, true); } + void add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixc(sz, opns, p), d, false); } imp(frontend & fe): m_num_children(0) { @@ -211,15 +212,15 @@ frontend::object_iterator frontend::end_objects() const { return m_imp->m_env.en frontend::object_iterator frontend::begin_local_objects() const { return m_imp->m_env.begin_local_objects(); } frontend::object_iterator frontend::end_local_objects() const { return m_imp->m_env.end_local_objects(); } -void frontend::add_infix(name const & opn, unsigned p, name const & n) { m_imp->add_infix(opn, p, n); } -void frontend::add_infixl(name const & opn, unsigned p, name const & n) { m_imp->add_infixl(opn, p, n); } -void frontend::add_infixr(name const & opn, unsigned p, name const & n) { m_imp->add_infixr(opn, p, n); } -void frontend::add_prefix(name const & opn, unsigned p, name const & n) { m_imp->add_prefix(opn, p, n); } -void frontend::add_postfix(name const & opn, unsigned p, name const & n) { m_imp->add_postfix(opn, p, n); } -void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixl(sz, opns, p, n); } -void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixr(sz, opns, p, n); } -void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixc(sz, opns, p, n); } -operator_info frontend::find_op_for(name const & n) const { return m_imp->find_op_for(n); } +void frontend::add_infix(name const & opn, unsigned p, expr const & d) { m_imp->add_infix(opn, p, d); } +void frontend::add_infixl(name const & opn, unsigned p, expr const & d) { m_imp->add_infixl(opn, p, d); } +void frontend::add_infixr(name const & opn, unsigned p, expr const & d) { m_imp->add_infixr(opn, p, d); } +void frontend::add_prefix(name const & opn, unsigned p, expr const & d) { m_imp->add_prefix(opn, p, d); } +void frontend::add_postfix(name const & opn, unsigned p, expr const & d) { m_imp->add_postfix(opn, p, d); } +void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixl(sz, opns, p, d); } +void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixr(sz, opns, p, d); } +void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixc(sz, opns, p, d); } +operator_info frontend::find_op_for(expr const & n) const { return m_imp->find_op_for(n); } operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); } operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); } } diff --git a/src/frontend/frontend.h b/src/frontend/frontend.h index c307145aa..79a31602f 100644 --- a/src/frontend/frontend.h +++ b/src/frontend/frontend.h @@ -23,8 +23,10 @@ public: frontend(); ~frontend(); - // ======================================= - // Parent/Child frontend management + /** + @name Parent/Child frontend management. + */ + /*@{*/ /** \brief Create a child environment. This frontend object will only allow "read-only" operations until all children frontend @@ -40,14 +42,16 @@ public: /** \brief Return parent frontend */ frontend parent() const; - // ======================================= + /*@}*/ + /** + @name Environment API + */ + /*@{*/ /** \brief Coercion frontend -> environment. */ environment const & get_environment() const; operator environment const &() const { return get_environment(); } - // ======================================= - // Environment API level add_uvar(name const & n, level const & l); level add_uvar(name const & n); level get_uvar(name const & n) const; @@ -64,30 +68,50 @@ public: object_iterator end_objects() const; object_iterator begin_local_objects() const; object_iterator end_local_objects() const; - // ======================================= + /*@}*/ - // ======================================= - // Notation - void add_infix(name const & opn, unsigned precedence, name const & n); - void add_infixl(name const & opn, unsigned precedence, name const & n); - void add_infixr(name const & opn, unsigned precedence, name const & n); - void add_prefix(name const & opn, unsigned precedence, name const & n); - void add_postfix(name const & opn, unsigned precedence, name const & n); - void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, name const & n); - void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, name const & n); - void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, name const & n); /** - \brief Return the operator (if it exists) associated with the - given internal name. - - \remark If an operator is not associated with \c n, then - return the null operator. + @name Notation for parsing and pretty printing. */ - operator_info find_op_for(name const & n) const; + /*@{*/ + void add_infix(name const & opn, unsigned precedence, expr const & d); + void add_infixl(name const & opn, unsigned precedence, expr const & d); + void add_infixr(name const & opn, unsigned precedence, expr const & d); + void add_prefix(name const & opn, unsigned precedence, expr const & d); + void add_postfix(name const & opn, unsigned precedence, expr const & d); + void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, expr const & d); + void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, expr const & d); + void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, expr const & d); + /** + \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. + */ + operator_info find_op_for(expr const & e) const; + /** + \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(name const & n) const; + /** + \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(name const & n) const; - // ======================================= + /*@}*/ }; } diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp index b98c5df4c..c5a23c0a1 100644 --- a/src/frontend/operator_info.cpp +++ b/src/frontend/operator_info.cpp @@ -16,7 +16,7 @@ struct operator_info::imp { fixity m_fixity; unsigned m_precedence; list m_op_parts; // operator parts, > 1 only if the operator is mixfix. - list m_names; // internal names, > 1 only if the operator is overloaded. + 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())) {} @@ -27,7 +27,7 @@ struct operator_info::imp { } 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_names(s.m_names) { + 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 { @@ -51,11 +51,11 @@ operator_info & operator_info::operator=(operator_info const & s) { LEAN_COPY_RE operator_info & operator_info::operator=(operator_info && s) { LEAN_MOVE_REF(operator_info, s); } -void operator_info::add_internal_name(name const & n) { lean_assert(m_ptr); m_ptr->m_names = cons(n, m_ptr->m_names); } +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_names) && !is_nil(cdr(m_ptr->m_names)); } +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_internal_names() const { lean_assert(m_ptr); return m_ptr->m_names; } +list const & operator_info::get_exprs() 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; } @@ -134,13 +134,4 @@ std::ostream & operator<<(std::ostream & out, operator_info const & o) { out << pp(o); return out; } - -format pp(notation_declaration const & n) { - return format{pp(n.get_op()), space(), format(n.get_internal_name())}; -} - -std::ostream & operator<<(std::ostream & out, notation_declaration const & n) { - out << pp(n); - return out; -} } diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h index bfcc195c9..37fe73c93 100644 --- a/src/frontend/operator_info.h +++ b/src/frontend/operator_info.h @@ -28,7 +28,6 @@ enum class fixity { Prefix, Infix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mi \brief Data-structure for storing user defined operator information. This information is used during parsing and pretty-printing. - */ class operator_info { struct imp; @@ -56,20 +55,19 @@ public: friend operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence); friend operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence); - /** \brief Associate an internal name for this operator. */ - void add_internal_name(name const & n); + /** \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 internal names for this operator. + \brief Return the list of expressions for this operator. The list has size greater than 1 iff the operator has been overloaded. - Internal names are the real names used to identify the operator - in the kernel. + These are the possible interpretations for the operator. */ - list const & get_internal_names() const; + list const & get_exprs() const; /** \brief Return the operator fixity. */ fixity get_fixity() const; @@ -110,15 +108,12 @@ std::ostream & operator<<(std::ostream & out, operator_info const & o); */ class notation_declaration : public neutral_object_cell { operator_info m_op; - name m_name; + expr m_expr; public: - notation_declaration(operator_info const & op, name const & n):m_op(op), m_name(n) {} + 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; } - name const & get_internal_name() const { return m_name; } + expr const & get_expr() const { return m_expr; } }; - -format pp(notation_declaration const & n); -std::ostream & operator<<(std::ostream & out, notation_declaration const & n); } diff --git a/src/frontend/parser.cpp b/src/frontend/parser.cpp index ac53f6332..772f8d23c 100644 --- a/src/frontend/parser.cpp +++ b/src/frontend/parser.cpp @@ -288,13 +288,13 @@ class parser_fn { resolve/decide which f_i should be used. */ expr mk_fun(operator_info const & op) { - list const & fs = op.get_internal_names(); + list const & fs = op.get_exprs(); lean_assert(!is_nil(fs)); auto it = fs.begin(); - expr r = mk_constant(*it); + expr r = *it; ++it; for (; it != fs.end(); ++it) - r = mk_app(g_overload, mk_constant(*it), r); + r = mk_app(g_overload, *it, r); return r; } @@ -870,19 +870,20 @@ class parser_fn { \brief Parse prefix/postfix/infix/infixl/infixr user operator definitions. These definitions have the form: - - fixity [Num] ID ID + - fixity [Num] ID ':' expr */ void parse_op(fixity fx) { next(); unsigned prec = parse_precedence(); name op_id = parse_op_id(); - name id = parse_op_id(); + check_colon_next("invalid operator definition, ':' expected"); + expr d = parse_expr(); switch (fx) { - case fixity::Prefix: m_frontend.add_prefix(op_id, prec, id); break; - case fixity::Postfix: m_frontend.add_postfix(op_id, prec, id); break; - case fixity::Infix: m_frontend.add_infix(op_id, prec, id); break; - case fixity::Infixl: m_frontend.add_infixl(op_id, prec, id); break; - case fixity::Infixr: m_frontend.add_infixr(op_id, prec, id); break; + case fixity::Prefix: m_frontend.add_prefix(op_id, prec, d); break; + case fixity::Postfix: m_frontend.add_postfix(op_id, prec, d); break; + case fixity::Infix: m_frontend.add_infix(op_id, prec, d); break; + case fixity::Infixl: m_frontend.add_infixl(op_id, prec, d); break; + case fixity::Infixr: m_frontend.add_infixr(op_id, prec, d); break; default: lean_unreachable(); break; } } @@ -891,7 +892,7 @@ class parser_fn { \brief Parse mixfix/mixfixl/mixfixr user operator definition. These definitions have the form: - - fixity [NUM] ID ID+ ID + - fixity [NUM] ID ID+ ':' ID */ void parse_mixfix_op(fixity fx) { next(); @@ -899,16 +900,16 @@ class parser_fn { buffer parts; parts.push_back(parse_op_id()); parts.push_back(parse_op_id()); - name id = parse_op_id(); - while (curr_is_identifier()) { - parts.push_back(id); - id = curr_name(); - next(); + while (!curr_is_colon()) { + parts.push_back(parse_op_id()); } + lean_assert(curr_is_colon()); + next(); + expr d = parse_expr(); switch (fx) { - case fixity::Mixfixl: m_frontend.add_mixfixl(parts.size(), parts.data(), prec, id); break; - case fixity::Mixfixr: m_frontend.add_mixfixr(parts.size(), parts.data(), prec, id); break; - case fixity::Mixfixc: m_frontend.add_mixfixc(parts.size(), parts.data(), prec, id); break; + case fixity::Mixfixl: m_frontend.add_mixfixl(parts.size(), parts.data(), prec, d); break; + case fixity::Mixfixr: m_frontend.add_mixfixr(parts.size(), parts.data(), prec, d); break; + case fixity::Mixfixc: m_frontend.add_mixfixc(parts.size(), parts.data(), prec, d); break; default: lean_unreachable(); break; } } diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp index 9066c2129..a9dfb01d7 100644 --- a/src/frontend/pp.cpp +++ b/src/frontend/pp.cpp @@ -179,20 +179,21 @@ class pp_fn { /** \brief Return the operator associated with \c e. - Return the nil operator if there is none. + Return the null operator if there is none. We say \c e has an operator associated with it, if: - 1) It is a constant and there is an operator associated with it. + 1) \c e is associated with an operator. - 2) It is an application, and the function is a constant \c c with an - operator associated with \c c. + 2) It is an application, and the function is associated with an + operator. */ operator_info get_operator(expr const & e) { - if (is_constant(e)) - return m_frontend.find_op_for(const_name(e)); - else if (is_app(e) && is_constant(arg(e, 0))) - return m_frontend.find_op_for(const_name(arg(e, 0))); + operator_info op = m_frontend.find_op_for(e); + if (op) + return op; + else if (is_app(e)) + return m_frontend.find_op_for(arg(e, 0)); else return operator_info(); } @@ -866,7 +867,8 @@ class pp_formatter_cell : public formatter_cell { } format pp_notation_decl(object const & obj) { - return ::lean::pp(*(static_cast(obj.cell()))); + notation_declaration const & n = *(static_cast(obj.cell())); + return format{::lean::pp(n.get_op()), space(), colon(), space(), pp(n.get_expr())}; } public: diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp index 8f45c70f7..b6921a95f 100644 --- a/src/tests/frontend/frontend.cpp +++ b/src/tests/frontend/frontend.cpp @@ -28,17 +28,17 @@ static void tst2() { operator_info op2 = infixr(name("implies"), 20); lean_assert(op1.get_precedence() == 10); lean_assert(op1.get_fixity() == fixity::Infixl); - op1.add_internal_name(name{"Bool","And"}); + op1.add_expr(mk_and_fn()); operator_info op3 = infixl(name("+"), 10); - op3.add_internal_name(name{"Int", "plus"}); - op3.add_internal_name(name{"Real", "plus"}); - std::cout << op3.get_internal_names() << "\n"; - lean_assert(length(op3.get_internal_names()) == 2); + op3.add_expr(Const(name{"Int", "plus"})); + op3.add_expr(Const(name{"Real", "plus"})); + std::cout << op3.get_exprs() << "\n"; + lean_assert(length(op3.get_exprs()) == 2); operator_info op4 = op3.copy(); - op4.add_internal_name(name{"Complex", "plus"}); - std::cout << op4.get_internal_names() << "\n"; - lean_assert(length(op3.get_internal_names()) == 2); - lean_assert(length(op4.get_internal_names()) == 3); + op4.add_expr(Const(name{"Complex", "plus"})); + std::cout << op4.get_exprs() << "\n"; + lean_assert(length(op3.get_exprs()) == 2); + lean_assert(length(op4.get_exprs()) == 3); lean_assert(op4.get_fixity() == fixity::Infixl); lean_assert(op4.get_op_name() == op3.get_op_name()); lean_assert(prefix("tst", 20).get_fixity() == fixity::Prefix); @@ -120,7 +120,7 @@ static void tst7() { static void tst8() { frontend fe; formatter fmt = mk_pp_formatter(fe); - fe.add_infixl("<-$->", 10, const_name(mk_refl_fn())); + fe.add_infixl("<-$->", 10, mk_refl_fn()); std::cout << fmt(fe.find_object("Trivial")) << "\n"; } @@ -152,9 +152,9 @@ static void tst9() { bool found = false; std::for_each(f.begin_objects(), f.end_objects(), [&](object const & obj) { if (obj.has_name() && obj.get_name() == "y") found = true; }); lean_assert(found); - f.add_postfix("!", 10, "factorial"); + f.add_postfix("!", 10, Const("factorial")); name parts[] = {"if", "then", "else"}; - f.add_mixfixl(3, parts, 10, "if"); + f.add_mixfixl(3, parts, 10, Const("if")); } static void tst10() { diff --git a/src/tests/frontend/parser.cpp b/src/tests/frontend/parser.cpp index dc27241dd..594c8b7a1 100644 --- a/src/tests/frontend/parser.cpp +++ b/src/tests/frontend/parser.cpp @@ -32,8 +32,8 @@ static void tst1() { parse(fe, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x"); parse(fe, "Eval true && true"); parse(fe, "Show true && false Eval true && false"); - parse(fe, "Infixl 35 & and Show true & false & false Eval true & false"); - parse(fe, "Mixfixc 100 if then fi implies Show if true then false fi"); + parse(fe, "Infixl 35 & : and Show true & false & false Eval true & false"); + parse(fe, "Mixfixc 100 if then fi : implies Show if true then false fi"); parse(fe, "Show Pi (A : Type), A -> A"); parse(fe, "Check Pi (A : Type), A -> A"); }