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

Factor duplicate code. Add more comments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-03 23:15:37 -07:00
parent 0c071d43af
commit 887f696f66
12 changed files with 119 additions and 171 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

155
src/kernel/arith/arith.cpp
View file

@ -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<nat_type_value const*>(&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<nat_value_value const*>(&other);
return _other && _other->m_val == m_val;
@ -64,17 +51,9 @@ mpz const & nat_value_numeral(expr const & e) {
}
template<char const * Name, typename F>
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<nat_bin_op const*>(&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_name, nat_mul_eval> 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<nat_le_value const*>(&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<int_type_value const*>(&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<int_value_value const*>(&other);
return _other && _other->m_val == m_val;
@ -172,17 +136,9 @@ mpz const & int_value_numeral(expr const & e) {
}
template<char const * Name, typename F>
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<int_bin_op const*>(&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_name, int_div_eval> 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<int_le_value const*>(&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<real_type_value const*>(&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<real_value_value const*>(&other);
return _other && _other->m_val == m_val;
@ -294,17 +235,9 @@ mpq const & real_value_numeral(expr const & e) {
}
template<char const * Name, typename F>
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<real_bin_op const*>(&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_name, real_div_eval> 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<real_le_value const*>(&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<nat_to_int_value const*>(&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<int_to_real_value const*>(&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"));

23
src/kernel/builtin.cpp
View file

@ -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<bool_type_value const*>(&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<bool_value_value const*>(&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<ite_fn_value const*>(&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);
// =======================================

22
src/kernel/expr.cpp
View file

@ -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) {

14
src/kernel/expr.h
View file

@ -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; }

3
src/kernel/level.h
View file

@ -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);

33
src/kernel/value.h Normal file
View file

@ -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(); }
};
}

4
src/library/context_to_lambda.h
View file

@ -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))

7
src/library/formatter.h
View file

@ -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<formatter_cell> 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();
}

4
src/library/printer.cpp
View file

@ -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;

3
src/util/list.h
View file

@ -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;

19
src/util/name.h
View file

@ -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: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical
name <tt>foo::bla::tst</tt>.
*/
name(std::initializer_list<char const *> 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;

3
src/util/sexpr/sexpr.h
View file

@ -144,6 +144,9 @@ template<typename T> inline bool operator==(T const & a, sexpr const & b) { retu
inline bool operator!=(sexpr const & a, sexpr const & b) { return !(a == b); }
template<typename T> inline bool operator!=(sexpr const & a, T const & b) { return !(a == b); }
template<typename T> 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; }