From 887f696f6687ae01d7ec5601526c48934ee6dfb9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 23:15:37 -0700 Subject: [PATCH] Factor duplicate code. Add more comments Signed-off-by: Leonardo de Moura --- src/kernel/arith/arith.cpp | 155 ++++++-------------------------- src/kernel/builtin.cpp | 23 ++--- src/kernel/expr.cpp | 22 ++--- src/kernel/expr.h | 14 +-- src/kernel/level.h | 3 + src/kernel/value.h | 33 +++++++ src/library/context_to_lambda.h | 4 - src/library/formatter.h | 7 +- src/library/printer.cpp | 4 + src/util/list.h | 3 + src/util/name.h | 19 +++- src/util/sexpr/sexpr.h | 3 + 12 files changed, 119 insertions(+), 171 deletions(-) create mode 100644 src/kernel/value.h diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp index 5796211e1..ddda46505 100644 --- a/src/kernel/arith/arith.cpp +++ b/src/kernel/arith/arith.cpp @@ -7,28 +7,15 @@ Author: Leonardo de Moura #include "builtin.h" #include "arith.h" #include "abstract.h" +#include "value.h" #include "environment.h" namespace lean { -/** \brief Base class for Nat, Int and Real types */ -class num_type_value : public value { - name m_name; -public: - num_type_value(char const * name):m_name(name) {} - virtual ~num_type_value() {} - virtual expr get_type() const { return Type(); } - virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } -}; - // ======================================= // Natural numbers -class nat_type_value : public num_type_value { +class nat_type_value : public type_value { public: - nat_type_value():num_type_value("Nat") {} - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + nat_type_value():type_value("Nat") {} }; expr const Nat = mk_value(*(new nat_type_value())); expr mk_nat_type() { return Nat; } @@ -39,7 +26,7 @@ public: nat_value_value(mpz const & v):m_val(v) { lean_assert(v >= 0); } virtual ~nat_value_value() {} virtual expr get_type() const { return Nat; } - virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; } + virtual name get_name() const { return name{"Nat", "numeral"}; } virtual bool operator==(value const & other) const { nat_value_value const * _other = dynamic_cast(&other); return _other && _other->m_val == m_val; @@ -64,17 +51,9 @@ mpz const & nat_value_numeral(expr const & e) { } template -class nat_bin_op : public value { - expr m_type; - name m_name; +class nat_bin_op : public const_value { public: - nat_bin_op() { - m_type = Nat >> (Nat >> Nat); - m_name = name("Nat", Name); - } - virtual ~nat_bin_op() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + nat_bin_op():const_value(name("Nat", Name), Nat >> (Nat >> Nat)) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) { r = mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2]))); @@ -83,9 +62,6 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; constexpr char nat_add_name[] = "add"; @@ -98,17 +74,9 @@ struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 typedef nat_bin_op nat_mul_value; MK_BUILTIN(nat_mul_fn, nat_mul_value); -class nat_le_value : public value { - expr m_type; - name m_name; +class nat_le_value : public const_value { public: - nat_le_value() { - m_type = Nat >> (Nat >> Bool); - m_name = name{"Nat", "le"}; - } - virtual ~nat_le_value() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) { r = mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2])); @@ -117,9 +85,6 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; MK_BUILTIN(nat_le_fn, nat_le_value); @@ -133,10 +98,9 @@ MK_CONSTANT(nat_id_fn, name({"Nat", "id"})); // ======================================= // Integers -class int_type_value : public num_type_value { +class int_type_value : public type_value { public: - int_type_value():num_type_value("Int") {} - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + int_type_value():type_value("Int") {} }; expr const Int = mk_value(*(new int_type_value())); expr mk_int_type() { return Int; } @@ -147,7 +111,7 @@ public: int_value_value(mpz const & v):m_val(v) {} virtual ~int_value_value() {} virtual expr get_type() const { return Int; } - virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; } + virtual name get_name() const { return name{"Int", "numeral"}; } virtual bool operator==(value const & other) const { int_value_value const * _other = dynamic_cast(&other); return _other && _other->m_val == m_val; @@ -172,17 +136,9 @@ mpz const & int_value_numeral(expr const & e) { } template -class int_bin_op : public value { - expr m_type; - name m_name; +class int_bin_op : public const_value { public: - int_bin_op() { - m_type = Int >> (Int >> Int); - m_name = name("Int", Name); - } - virtual ~int_bin_op() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + int_bin_op():const_value(name("Int", Name), Int >> (Int >> Int)) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) { r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2]))); @@ -191,9 +147,6 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; constexpr char int_add_name[] = "add"; @@ -218,17 +171,9 @@ struct int_div_eval { typedef int_bin_op int_div_value; MK_BUILTIN(int_div_fn, int_div_value); -class int_le_value : public value { - expr m_type; - name m_name; +class int_le_value : public const_value { public: - int_le_value() { - m_type = Int >> (Int >> Bool); - m_name = name{"Int", "le"}; - } - virtual ~int_le_value() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) { r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2])); @@ -237,9 +182,6 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; MK_BUILTIN(int_le_fn, int_le_value); @@ -255,10 +197,9 @@ MK_CONSTANT(int_gt_fn, name({"Int", "gt"})); // ======================================= // Reals -class real_type_value : public num_type_value { +class real_type_value : public type_value { public: - real_type_value():num_type_value("Real") {} - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + real_type_value():type_value("Real") {} }; expr const Real = mk_value(*(new real_type_value())); expr mk_real_type() { return Real; } @@ -269,7 +210,7 @@ public: real_value_value(mpq const & v):m_val(v) {} virtual ~real_value_value() {} virtual expr get_type() const { return Real; } - virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; } + virtual name get_name() const { return name{"Real", "numeral"}; } virtual bool operator==(value const & other) const { real_value_value const * _other = dynamic_cast(&other); return _other && _other->m_val == m_val; @@ -294,17 +235,9 @@ mpq const & real_value_numeral(expr const & e) { } template -class real_bin_op : public value { - expr m_type; - name m_name; +class real_bin_op : public const_value { public: - real_bin_op() { - m_type = Real >> (Real >> Real); - m_name = name("Real", Name); - } - virtual ~real_bin_op() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + real_bin_op():const_value(name("Real", Name), Real >> (Real >> Real)) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) { r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2]))); @@ -313,9 +246,6 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; constexpr char real_add_name[] = "add"; @@ -340,17 +270,9 @@ struct real_div_eval { typedef real_bin_op real_div_value; MK_BUILTIN(real_div_fn, real_div_value); -class real_le_value : public value { - expr m_type; - name m_name; +class real_le_value : public const_value { public: - real_le_value() { - m_type = Real >> (Real >> Bool); - m_name = name{"Real", "le"}; - } - virtual ~real_le_value() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) { r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2])); @@ -359,9 +281,6 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; MK_BUILTIN(real_le_fn, real_le_value); @@ -393,17 +312,9 @@ MK_CONSTANT(csch_fn, name("csch")); // ======================================= // Coercions -class nat_to_int_value : public value { - expr m_type; - name m_name; +class nat_to_int_value : public const_value { public: - nat_to_int_value() { - m_type = Nat >> Int; - m_name = "nat_to_int"; - } - virtual ~nat_to_int_value() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + nat_to_int_value():const_value("nat_to_int", Nat >> Int) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 2 && is_nat_value(args[1])) { r = mk_int_value(nat_value_numeral(args[1])); @@ -412,23 +323,12 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; MK_BUILTIN(nat_to_int_fn, nat_to_int_value); -class int_to_real_value : public value { - expr m_type; - name m_name; +class int_to_real_value : public const_value { public: - int_to_real_value() { - m_type = Int >> Real; - m_name = "int_to_real"; - } - virtual ~int_to_real_value() {} - virtual expr get_type() const { return m_type; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } + int_to_real_value():const_value("int_to_real", Int >> Real) {} virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 2 && is_int_value(args[1])) { r = mk_real_value(mpq(int_value_numeral(args[1]))); @@ -437,9 +337,6 @@ public: return false; } } - virtual void display(std::ostream & out) const { out << m_name; } - virtual format pp() const { return format(m_name); } - virtual unsigned hash() const { return m_name.hash(); } }; MK_BUILTIN(int_to_real_fn, int_to_real_value); MK_CONSTANT(nat_to_real_fn, name("nat_to_real")); diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index c1c8f62b2..c8b6758f3 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -63,11 +63,7 @@ class bool_type_value : public value { public: virtual ~bool_type_value() {} virtual expr get_type() const { return Type(); } - virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } - virtual void display(std::ostream & out) const { out << g_Bool_name; } - virtual format pp() const { return g_Bool_fmt; } - virtual unsigned hash() const { return g_Bool_name.hash(); } + virtual name get_name() const { return g_Bool_name; } }; expr const Bool = mk_value(*(new bool_type_value())); expr mk_bool_type() { return Bool; } @@ -79,22 +75,21 @@ static char const * g_true_u_str = "\u22A4"; static char const * g_false_u_str = "\u22A5"; static format g_true_u_fmt(g_true_u_str); static format g_false_u_fmt(g_false_u_str); -static char const * g_true_str = "true"; -static char const * g_false_str = "false"; -static format g_true_fmt(g_true_str); -static format g_false_fmt(g_false_str); +static name g_true_name("true"); +static name g_false_name("false"); +static format g_true_fmt(g_true_name); +static format g_false_fmt(g_false_name); class bool_value_value : public value { bool m_val; public: bool_value_value(bool v):m_val(v) {} virtual ~bool_value_value() {} virtual expr get_type() const { return Bool; } - virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; } + virtual name get_name() const { return m_val ? g_true_name : g_false_name; } virtual bool operator==(value const & other) const { bool_value_value const * _other = dynamic_cast(&other); return _other && _other->m_val == m_val; } - virtual void display(std::ostream & out) const { out << (m_val ? g_true_str : g_false_str); } virtual format pp(bool unicode) const { if (unicode) return m_val ? g_true_u_fmt : g_false_u_fmt; @@ -102,7 +97,6 @@ public: return m_val ? g_true_fmt : g_false_fmt; } virtual format pp() const { return pp(true); } - virtual unsigned hash() const { return m_val ? 3 : 5; } bool get_val() const { return m_val; } }; expr const True = mk_value(*(new bool_value_value(true))); @@ -139,6 +133,7 @@ public: } virtual ~ite_fn_value() {} virtual expr get_type() const { return m_type; } + virtual name get_name() const { return g_ite_name; } virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { if (num_args == 5 && is_bool_value(args[2])) { if (to_bool(args[2])) @@ -153,10 +148,6 @@ public: return false; } } - virtual bool operator==(value const & other) const { return dynamic_cast(&other) != nullptr; } - virtual void display(std::ostream & out) const { out << g_ite_name; } - virtual format pp() const { return g_ite_fmt; } - virtual unsigned hash() const { return g_ite_name.hash(); } }; MK_BUILTIN(ite_fn, ite_fn_value); // ======================================= diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index bbc22c668..071ef1333 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -80,33 +80,33 @@ expr_eq::expr_eq(expr const & lhs, expr const & rhs): m_lhs(lhs), m_rhs(rhs) { } -expr_eq::~expr_eq() { -} +expr_eq::~expr_eq() {} expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b): expr_cell(k, ::lean::hash(t.hash(), b.hash())), m_name(n), m_domain(t), m_body(b) { } -expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e): - expr_abstraction(expr_kind::Lambda, n, t, e) {} -expr_pi::expr_pi(name const & n, expr const & t, expr const & e): - expr_abstraction(expr_kind::Pi, n, t, e) {} - +expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {} +expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {} expr_type::expr_type(level const & l): expr_cell(expr_kind::Type, l.hash()), m_level(l) { } -expr_type::~expr_type() { -} +expr_type::~expr_type() {} expr_let::expr_let(name const & n, expr const & v, expr const & b): expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash())), m_name(n), m_value(v), m_body(b) { } -expr_let::~expr_let() { -} +expr_let::~expr_let() {} +bool value::normalize(unsigned num_args, expr const * args, expr & r) const { return false; } +void value::display(std::ostream & out) const { out << get_name(); } +bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); } +format value::pp() const { return format(get_name()); } +format value::pp(bool unicode) const { return pp(); } +unsigned value::hash() const { return get_name().hash(); } expr_value::expr_value(value & v): expr_cell(expr_kind::Value, v.hash()), m_val(v) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 00f52bda0..349c675ba 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -204,12 +204,13 @@ public: value():m_rc(0) {} virtual ~value() {} virtual expr get_type() const = 0; - virtual bool normalize(unsigned num_args, expr const * args, expr & r) const = 0; - virtual bool operator==(value const & other) const = 0; - virtual void display(std::ostream & out) const = 0; - virtual format pp() const = 0; - virtual format pp(bool unicode) const { return pp(); } - virtual unsigned hash() const = 0; + virtual name get_name() const = 0; + virtual bool normalize(unsigned num_args, expr const * args, expr & r) const; + virtual bool operator==(value const & other) const; + virtual void display(std::ostream & out) const; + virtual format pp() const; + virtual format pp(bool unicode) const; + virtual unsigned hash() const; }; /** \brief Semantic attachments */ class expr_value : public expr_cell { @@ -223,7 +224,6 @@ public: }; // ======================================= - // ======================================= // Testers inline bool is_var(expr_cell * e) { return e->kind() == expr_kind::Var; } diff --git a/src/kernel/level.h b/src/kernel/level.h index 2eb1f4800..a59c898a5 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -63,10 +63,13 @@ inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar; } inline bool is_lift(level const & l) { return kind(l) == level_kind::Lift; } inline bool is_max (level const & l) { return kind(l) == level_kind::Max; } +/** \brief Return a */ inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); } inline level const * max_end_levels(level const & l) { return max_begin_levels(l) + max_size(l); } +/** \brief Pretty print the given level expression, unicode characters are used if \c unicode is \c true. */ format pp(level const & l, bool unicode); +/** \brief Pretty print the given level expression using the given configuration options. */ format pp(level const & l, options const & opts = options()); } void print(lean::level const & l); diff --git a/src/kernel/value.h b/src/kernel/value.h new file mode 100644 index 000000000..628b50790 --- /dev/null +++ b/src/kernel/value.h @@ -0,0 +1,33 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "expr.h" + +namespace lean { +// Some value subclasses that capture common implementation patterns. +class named_value : public value { + name m_name; +public: + named_value(name const & n):m_name(n) {} + virtual ~named_value() {} + virtual name get_name() const { return m_name; } +}; + +class const_value : public named_value { + expr m_type; +public: + const_value(name const & n, expr const & t):named_value(n), m_type(t) {} + virtual ~const_value() {} + virtual expr get_type() const { return m_type; } +}; + +class type_value : public named_value { +public: + type_value(name const & n):named_value(n) {} + virtual expr get_type() const { return Type(); } +}; +} diff --git a/src/library/context_to_lambda.h b/src/library/context_to_lambda.h index 175764d68..0f2618bf8 100644 --- a/src/library/context_to_lambda.h +++ b/src/library/context_to_lambda.h @@ -23,14 +23,12 @@ namespace lean { value V_i, then we just use (fake T_i). */ expr context_to_lambda(context const & c, expr const & e); - /** \brief Return true if \c e is a fake context created using context_to_lambda. (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) */ bool is_fake_context(expr const & e); - /** \brief Return the name n_1 of the head of the (fake) context (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) @@ -38,7 +36,6 @@ bool is_fake_context(expr const & e); \pre is_fake_context(e) */ name const & fake_context_name(expr const & e); - /** \brief Return the domain T_1 of the head of the (fake) context (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) @@ -46,7 +43,6 @@ name const & fake_context_name(expr const & e); \pre is_fake_context(e) */ expr const & fake_context_domain(expr const & e); - /** \brief Return the value V_1 of the head of the (fake) context (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) diff --git a/src/library/formatter.h b/src/library/formatter.h index 254eff420..6bbdb18a2 100644 --- a/src/library/formatter.h +++ b/src/library/formatter.h @@ -38,6 +38,9 @@ public: virtual void set_interrupt(bool flag) {} }; class kernel_exception; +/** + \brief Smart-pointer for the actual formatter object (aka \c formatter_cell). +*/ class formatter { std::shared_ptr m_cell; public: @@ -52,6 +55,8 @@ public: format operator()(kernel_exception const & ex, options const & opts = options()); void set_interrupt(bool flag) { m_cell->set_interrupt(flag); } }; - +/** + \brief Create a simple formatter object based on #printer class. +*/ formatter mk_simple_formatter(); } diff --git a/src/library/printer.cpp b/src/library/printer.cpp index a995deb83..b5645fead 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -21,6 +21,10 @@ bool is_atomic(expr const & e) { return false; } +/** + \brief Very basic printer for expressions. + It is mainly used when debugging code. +*/ struct print_expr_fn { std::ostream & m_out; diff --git a/src/util/list.h b/src/util/list.h index e950851f6..d19158a64 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -43,13 +43,16 @@ public: list & operator=(list const & s) { LEAN_COPY_REF(list, s); } list & operator=(list && s) { LEAN_MOVE_REF(list, s); } + /** \brief Return true iff it is not the empty/nil list. */ operator bool() const { return m_ptr != nullptr; } friend bool is_nil(list const & l) { return l.m_ptr == nullptr; } friend T const & head(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_head; } friend list const & tail(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_tail; } + /** \brief Pointer equality. Return true iff \c l1 and \c l2 point to the same memory location. */ friend bool is_eqp(list const & l1, list const & l2) { return l1.m_ptr == l2.m_ptr; } + /** \brief Structural equality. */ friend bool operator==(list const & l1, list const & l2) { cell * it1 = l1.m_ptr; cell * it2 = l2.m_ptr; diff --git a/src/util/name.h b/src/util/name.h index ecb39eddf..ad869c280 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -26,6 +26,11 @@ public: name(name const & prefix, unsigned k); name(name const & other); name(name && other); + /** + \brief Create a hierarchical name using the given strings. + Example: name{"foo", "bla", "tst"} creates the hierarchical + name foo::bla::tst. + */ name(std::initializer_list const & l); ~name(); static name const & anonymous(); @@ -37,7 +42,9 @@ public: friend bool operator!=(name const & a, name const & b) { return !(a == b); } friend bool operator==(name const & a, char const * b); friend bool operator!=(name const & a, char const * b) { return !(a == b); } - // total order on hierarchical names. + /** + \brief Total order on hierarchical names. + */ friend int cmp(name const & a, name const & b) { return cmp(a.m_ptr, b.m_ptr); } friend bool operator<(name const & a, name const & b) { return cmp(a, b) < 0; } friend bool operator>(name const & a, name const & b) { return cmp(a, b) > 0; } @@ -48,12 +55,18 @@ public: bool is_string() const { return kind() == name_kind::STRING; } bool is_numeral() const { return kind() == name_kind::NUMERAL; } unsigned get_numeral() const; + /** + \brief If the tail of the given hierarchical name is a string, then it returns this string. + \pre is_string() + */ char const * get_string() const; bool is_atomic() const; - name get_prefix() const; /** - \brief Convert this hierarchical name into a string. + \brief Return the prefix of a hierarchical name + \pre !is_atomic() */ + name get_prefix() const; + /** \brief Convert this hierarchical name into a string. */ std::string to_string() const; /** \brief Size of the this name (in characters). */ size_t size() const; diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h index e2ee2f701..eb2a6f09f 100644 --- a/src/util/sexpr/sexpr.h +++ b/src/util/sexpr/sexpr.h @@ -144,6 +144,9 @@ template inline bool operator==(T const & a, sexpr const & b) { retu inline bool operator!=(sexpr const & a, sexpr const & b) { return !(a == b); } template inline bool operator!=(sexpr const & a, T const & b) { return !(a == b); } template inline bool operator!=(T const & a, sexpr const & b) { return !(a == b); } +/** + \brief Total order on S-expressions. +*/ int cmp(sexpr const & a, sexpr const & b); inline bool operator<(sexpr const & a, sexpr const & b) { return cmp(a, b) < 0; } inline bool operator>(sexpr const & a, sexpr const & b) { return cmp(a, b) > 0; }