michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add methods for creating infix, prefix, postfix operators in the frontend object

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-15 08:52:10 -07:00
parent 577256fedc
commit 2b7834c5fc
7 changed files with 77 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/frontend/frontend.cpp
View file

@ -24,8 +24,23 @@ public:
static char const * g_keyword;
virtual char const * keyword() const { return g_keyword; }
virtual format pp(environment const &) const {
// TODO
return format();
char const * cmd;
switch (m_op.get_fixity()) {
case fixity::Infixl: cmd = "Infixl"; break;
case fixity::Infixr: cmd = "Infixr"; break;
case fixity::Prefix: cmd = "Prefix"; break;
case fixity::Postfix: cmd = "Postfix"; break;
case fixity::Mixfixl: cmd = "Mixfixl"; break;
case fixity::Mixfixr: cmd = "Mixfixr"; break;
case fixity::Mixfixc: cmd = "Mixfixc"; break;
}
format r = highlight_command(format(cmd));
if (m_op.get_precedence() != 0)
r += format{space(), format(m_op.get_precedence())};
for (auto p : m_op.get_op_name_parts())
r += format{space(), format(p)};
r += format{space(), format(m_name)};
return r;
}
};
char const * notation_declaration::g_keyword = "Notation";
@ -167,6 +182,22 @@ struct frontend::imp {
m_env.add_anonymous_object(new notation_declaration(new_op, n));
}
void add_infixl(name const & opn, unsigned precedence, name const & n) {
add_op(infixl(opn, precedence), n, true);
}
void add_infixr(name const & opn, unsigned precedence, name const & n) {
add_op(infixr(opn, precedence), n, true);
}
void add_prefix(name const & opn, unsigned precedence, name const & n) {
add_op(prefix(opn, precedence), n, false);
}
void add_postfix(name const & opn, unsigned precedence, name const & n) {
add_op(postfix(opn, precedence), n, true);
}
imp():
m_num_children(0) {
}
@ -221,5 +252,12 @@ environment const & frontend::env() const { return m_imp->m_env; }
level frontend::add_uvar(name const & n, level const & l) { return m_imp->m_env.add_uvar(n, l); }
level frontend::add_uvar(name const & n) { return m_imp->m_env.add_uvar(n); }
level frontend::get_uvar(name const & n) const { return m_imp->m_env.get_uvar(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::display(std::ostream & out) const { m_imp->m_env.display(out); }
}

10
src/frontend/frontend.h
View file

@ -50,6 +50,16 @@ public:
level add_uvar(name const & n);
level get_uvar(name const & n) const;
// =======================================
// Notation
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);
// =======================================
/** \brief Display universal variable constraints and objects stored in this environment and its parents. */
void display(std::ostream & out) const;
};
inline std::ostream & operator<<(std::ostream & out, frontend const & f) { f.display(out); return out; }
}

25
src/frontend/operator_info.cpp
View file

@ -14,27 +14,25 @@ struct operator_info::imp {
void dealloc() { delete this; }
MK_LEAN_RC();
fixity m_fixity;
associativity m_assoc; // Relevant only for infix operators.
unsigned m_precedence;
list<name> m_op_parts; // operator parts, > 1 only if the operator is mixfix.
list<name> m_names; // internal names, > 1 only if the operator is overloaded.
imp(name const & op, fixity f, associativity a, unsigned p):
m_rc(1), m_fixity(f), m_assoc(a), m_precedence(p), m_op_parts(cons(op, list<name>())) {}
imp(name const & op, fixity f, unsigned p):
m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(cons(op, list<name>())) {}
imp(unsigned num_parts, name const * parts, fixity f, unsigned p):
m_rc(1), m_fixity(f), m_assoc(associativity::None), m_precedence(p), m_op_parts(it2list<name, name const *>(parts, parts + num_parts)) {
m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(it2list<name, name const *>(parts, parts + num_parts)) {
lean_assert(num_parts > 0);
}
imp(imp const & s):
m_rc(1), m_fixity(s.m_fixity), m_assoc(s.m_assoc), 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_names(s.m_names) {
}
bool is_eq(imp const & other) const {
return
m_fixity == other.m_fixity &&
m_assoc == other.m_assoc &&
m_precedence == other.m_precedence &&
m_op_parts == other.m_op_parts;
}
@ -61,8 +59,6 @@ list<name> const & operator_info::get_internal_names() const { lean_assert(m_ptr
fixity operator_info::get_fixity() const { lean_assert(m_ptr); return m_ptr->m_fixity; }
associativity operator_info::get_associativity() const { lean_assert(m_ptr); return m_ptr->m_assoc; }
unsigned operator_info::get_precedence() const { lean_assert(m_ptr); return m_ptr->m_precedence; }
name const & operator_info::get_op_name() const { lean_assert(m_ptr); return car(m_ptr->m_op_parts); }
@ -81,16 +77,16 @@ bool operator==(operator_info const & op1, operator_info const & op2) {
}
operator_info infixr(name const & op, unsigned precedence) {
return operator_info(new operator_info::imp(op, fixity::Infix, associativity::Right, precedence));
return operator_info(new operator_info::imp(op, fixity::Infixr, precedence));
}
operator_info infixl(name const & op, unsigned precedence) {
return operator_info(new operator_info::imp(op, fixity::Infix, associativity::Left, precedence));
return operator_info(new operator_info::imp(op, fixity::Infixl, precedence));
}
operator_info prefix(name const & op, unsigned precedence) {
return operator_info(new operator_info::imp(op, fixity::Prefix, associativity::None, precedence));
return operator_info(new operator_info::imp(op, fixity::Prefix, precedence));
}
operator_info postfix(name const & op, unsigned precedence) {
return operator_info(new operator_info::imp(op, fixity::Postfix, associativity::None, precedence));
return operator_info(new operator_info::imp(op, fixity::Postfix, precedence));
}
operator_info mixfixl(unsigned num_parts, name const * parts, unsigned precedence) {
lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixl, precedence));
@ -107,7 +103,8 @@ static char const * g_arrow = "\u21a6";
format pp(operator_info const & o) {
format r;
switch (o.get_fixity()) {
case fixity::Infix: r = format(o.get_associativity() == associativity::Left ? "Infixl" : "Infixr"); break;
case fixity::Infixl: r = format("Infixl"); break;
case fixity::Infixr: r = format("Infixr"); break;
case fixity::Prefix: r = format("Prefix"); break;
case fixity::Postfix: r = format("Postfix"); break;
case fixity::Mixfixl:
@ -121,7 +118,7 @@ format pp(operator_info const & o) {
r += format{format(o.get_precedence()), space()};
switch (o.get_fixity()) {
case fixity::Infix: case fixity::Prefix: case fixity::Postfix:
case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix:
r += pp(o.get_op_name()); break;
case fixity::Mixfixl:
for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")};

10
src/frontend/operator_info.h
View file

@ -13,15 +13,14 @@ namespace lean {
/**
\brief Operator fixity.
Prefix: ID _
Infix: _ ID _ (can be left or right associative)
Infixl: _ ID _ (left associative)
Infixr: _ ID _ (right associative)
Postfix: _ ID
Mixfixl: ID _ ID _ ... ID _ (has at least two parts)
Mixfixr: _ ID _ ID ... _ ID (has at least two parts)
Mixfixc: ID _ ID _ ... ID _ ID (has at least two parts)
*/
enum class fixity { Prefix, Infix, Postfix, Mixfixl, Mixfixr, Mixfixc };
enum class associativity { Left, Right, None };
enum class fixity { Prefix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc };
/**
\brief Data-structure for storing user defined operator
@ -72,9 +71,6 @@ public:
/** \brief Return the operator fixity. */
fixity get_fixity() const;
/** \brief Return the operator associativity. */
associativity get_associativity() const;
/** \brief Return the operator precedence. */
unsigned get_precedence() const;

14
src/kernel/environment.cpp
View file

@ -341,17 +341,13 @@ struct environment::imp {
}
}
void display_objects(std::ostream & out, environment const & env) const {
for (object const * obj : m_objects) {
out << obj->pp(env) << "\n";
}
}
/** \brief Display universal variable constraints and objects stored in this environment and its parents. */
void display(std::ostream & out, environment const & env) const {
if (has_parent())
m_parent->display(out, env);
display_objects(out, env);
for (object const * obj : m_objects) {
out << obj->pp(env) << "\n";
}
}
imp():
@ -480,10 +476,6 @@ object const & environment::get_object(unsigned i) const {
return *(m_imp->m_objects[i]);
}
void environment::display_objects(std::ostream & out) const {
m_imp->display_objects(out, *this);
}
void environment::display(std::ostream & out) const {
m_imp->display(out, *this);
}

6
src/kernel/environment.h
View file

@ -158,14 +158,8 @@ public:
object_iterator end_objects() const { return object_iterator(*this, get_num_objects()); }
// =======================================
// =======================================
// Pretty printing
/** \brief Display all objects stored in the environment */
void display_objects(std::ostream & out) const;
/** \brief Display universal variable constraints and objects stored in this environment and its parents. */
void display(std::ostream & out) const;
// =======================================
};
inline std::ostream & operator<<(std::ostream & out, environment const & env) { env.display(out); return out; }
}

13
src/tests/frontend/frontend.cpp
View file

@ -22,8 +22,7 @@ static void tst2() {
operator_info op1 = infixl(name("and"), 10);
operator_info op2 = infixr(name("implies"), 20);
lean_assert(op1.get_precedence() == 10);
lean_assert(op1.get_associativity() == associativity::Left);
lean_assert(op1.get_fixity() == fixity::Infix);
lean_assert(op1.get_fixity() == fixity::Infixl);
op1.add_internal_name(name{"Bool","And"});
operator_info op3 = infixl(name("+"), 10);
op3.add_internal_name(name{"Int", "plus"});
@ -35,7 +34,7 @@ static void tst2() {
std::cout << op4.get_internal_names() << "\n";
lean_assert(length(op3.get_internal_names()) == 2);
lean_assert(length(op4.get_internal_names()) == 3);
lean_assert(op4.get_fixity() == fixity::Infix);
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);
lean_assert(postfix("!", 20).get_fixity() == fixity::Postfix);
@ -47,8 +46,16 @@ static void tst2() {
std::cout << mixfixc({"if", "then", "else", "endif"}, 10) << "\n";
}
static void tst3() {
frontend f;
f.add_infixl("+", 10, name{"Int", "add"});
f.add_infixl("-", 10, name{"Int", "sub"});
std::cout << f;
}
int main() {
tst1();
tst2();
tst3();
return has_violations() ? 1 : 0;
}