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

feat(util/name): add name_pair, and lex order

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-17 13:09:29 -07:00
parent f9d81c24d3
commit 50806314d4
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/util/name.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <iostream> #include <iostream>
#include <functional> #include <functional>
#include <algorithm> #include <algorithm>
#include <utility>
#include "util/lua.h" #include "util/lua.h"
#include "util/serializer.h" #include "util/serializer.h"
#include "util/optional.h" #include "util/optional.h"
@ -167,6 +168,15 @@ inline bool independent(name const & a, name const & b) {
return !is_prefix_of(a, b) && !is_prefix_of(b, a); return !is_prefix_of(a, b) && !is_prefix_of(b, a);
} }
typedef std::pair<name, name> name_pair;
struct name_pair_quick_cmp {
int operator()(name_pair const & p1, name_pair const & p2) const {
int r = cmp(p1.first, p2.first);
if (r != 0) return r;
return cmp(p1.second, p2.second);
}
};
serializer & operator<<(serializer & s, name const & n); serializer & operator<<(serializer & s, name const & n);
name read_name(deserializer & d); name read_name(deserializer & d);
inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; } inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; }