Restructure format, add group and flatten
This commit is contained in:
Soonho Kong
parent
71638a8ad4
commit
03b1ce643e
2 changed files with 147 additions and 165 deletions
|
|
@ -5,121 +5,92 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Author: Soonho Kong
|
Author: Soonho Kong
|
||||||
*/
|
*/
|
||||||
#include <cstring>
|
#include <cstring>
|
||||||
#include "rc.h"
|
|
||||||
#include "hash.h"
|
|
||||||
#include "sexpr.h"
|
#include "sexpr.h"
|
||||||
#include "format.h"
|
#include "format.h"
|
||||||
#include "name.h"
|
|
||||||
#include "mpz.h"
|
|
||||||
#include "mpq.h"
|
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
|
std::ostream & layout(std::ostream & out, sexpr const & s) {
|
||||||
|
if(is_cons(s)) {
|
||||||
|
sexpr v = cdr(s);
|
||||||
|
|
||||||
struct format_cell {
|
switch (to_int(car(s))) {
|
||||||
void dealloc();
|
case format::format_kind::NIL:
|
||||||
MK_LEAN_RC()
|
out << "NIL";
|
||||||
format_kind m_kind;
|
break;
|
||||||
sexpr m_value;
|
case format::format_kind::NEST:
|
||||||
format_cell(format_kind k):m_rc(1), m_kind(k) {}
|
out << "NEST("
|
||||||
format_cell(char const * v):
|
<< car(v)
|
||||||
format_cell(format_kind::TEXT) {
|
<< ", ";
|
||||||
m_value = sexpr(v);
|
layout(out, cdr(v));
|
||||||
}
|
out << ")";
|
||||||
format_cell(std::string const & v):
|
break;
|
||||||
format_cell(format_kind::TEXT) {
|
case format::format_kind::COMPOSE:
|
||||||
m_value = sexpr(v);
|
out << "COMPOSE(";
|
||||||
}
|
layout(out, car(v));
|
||||||
format_cell(int v):
|
out << ", ";
|
||||||
format_cell(format_kind::TEXT) {
|
layout(out, cdr(v));
|
||||||
m_value = sexpr(v);
|
out << ")";
|
||||||
}
|
break;
|
||||||
format_cell(double v):
|
case format::format_kind::CHOICE:
|
||||||
format_cell(format_kind::TEXT) {
|
out << "CHOICE(";
|
||||||
m_value = sexpr(v);
|
layout(out, car(v));
|
||||||
}
|
out << ", ";
|
||||||
format_cell(name const & v):
|
layout(out, cdr(v));
|
||||||
format_cell(format_kind::TEXT) {
|
out << ")";
|
||||||
m_value = sexpr(v);
|
break;
|
||||||
}
|
case format::format_kind::LINE:
|
||||||
format_cell(mpz const & v):
|
out << "LINE()";
|
||||||
format_cell(format_kind::TEXT) {
|
break;
|
||||||
m_value = sexpr(v);
|
}
|
||||||
}
|
} else {
|
||||||
format_cell(mpq const & v):
|
out << s;
|
||||||
format_cell(format_kind::TEXT) {
|
|
||||||
m_value = sexpr(v);
|
|
||||||
}
|
|
||||||
format_cell(format_cell const * h, format_cell const * t):
|
|
||||||
format_cell(format_kind::COMPOSE) {
|
|
||||||
m_value = sexpr(h->m_value, h->m_value);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
void format_cell::dealloc() {
|
|
||||||
switch (m_kind) {
|
|
||||||
case format_kind::NIL: lean_unreachable(); break;
|
|
||||||
case format_kind::INDENT: delete this; break;
|
|
||||||
case format_kind::COMPOSE: delete this; break;
|
|
||||||
case format_kind::CHOICE: delete this; break;
|
|
||||||
case format_kind::LINE: delete this; break;
|
|
||||||
case format_kind::TEXT: delete this; break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
format::format(char const * v):m_ptr(new format_cell(v)) {}
|
|
||||||
format::format(std::string const & v):m_ptr(new format_cell(v)) {}
|
|
||||||
format::format(int v):m_ptr(new format_cell(v)) {}
|
|
||||||
format::format(double v):m_ptr(new format_cell(v)) {}
|
|
||||||
format::format(name const & v):m_ptr(new format_cell(v)) {}
|
|
||||||
format::format(mpz const & v):m_ptr(new format_cell(v)) {}
|
|
||||||
format::format(mpq const & v):m_ptr(new format_cell(v)) {}
|
|
||||||
format::format(format const & h, format const & t):m_ptr(new format_cell(h.m_ptr, t.m_ptr)) {}
|
|
||||||
format::format(format const & s):m_ptr(s.m_ptr) {
|
|
||||||
if (m_ptr)
|
|
||||||
m_ptr->inc_ref();
|
|
||||||
}
|
|
||||||
format::format(format && s):m_ptr(s.m_ptr) {
|
|
||||||
s.m_ptr = 0;
|
|
||||||
}
|
|
||||||
format::~format() {
|
|
||||||
if (m_ptr)
|
|
||||||
m_ptr->dec_ref();
|
|
||||||
}
|
|
||||||
|
|
||||||
format_kind format::kind() const { return m_ptr ? m_ptr->m_kind : format_kind::NIL; }
|
|
||||||
std::string const & format::get_string() const { return m_ptr->m_value.get_string(); }
|
|
||||||
|
|
||||||
unsigned format::hash() const { return m_ptr == nullptr ? 23 : m_ptr->m_value.hash(); }
|
|
||||||
|
|
||||||
format & format::operator=(format const & f) {
|
|
||||||
if (f.m_ptr)
|
|
||||||
f.m_ptr->inc_ref();
|
|
||||||
if (m_ptr)
|
|
||||||
m_ptr->dec_ref();
|
|
||||||
m_ptr = f.m_ptr;
|
|
||||||
return *this;
|
|
||||||
}
|
|
||||||
|
|
||||||
format & format::operator=(format && f) {
|
|
||||||
if (m_ptr)
|
|
||||||
m_ptr->dec_ref();
|
|
||||||
m_ptr = f.m_ptr;
|
|
||||||
f.m_ptr = 0;
|
|
||||||
return *this;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::ostream & operator<<(std::ostream & out, format const & s) {
|
|
||||||
switch (s.kind()) {
|
|
||||||
case format_kind::NIL: out << "nil"; break;
|
|
||||||
case format_kind::INDENT: out << "nil"; break;
|
|
||||||
case format_kind::TEXT: out << "TODO"; break;
|
|
||||||
case format_kind::COMPOSE: out << "TODO"; break;
|
|
||||||
case format_kind::CHOICE: out << "TODO"; break;
|
|
||||||
case format_kind::LINE: out << "TODO"; break;
|
|
||||||
}
|
}
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
std::ostream & operator<<(std::ostream & out, format const & f) {
|
||||||
|
return layout(out, f.m_value);
|
||||||
}
|
}
|
||||||
|
|
||||||
void pp(lean::format const & n) { std::cout << n << "\n"; }
|
sexpr flatten(sexpr const & s) {
|
||||||
|
if(is_cons(s)) {
|
||||||
|
sexpr v = cdr(s);
|
||||||
|
switch (to_int(car(s))) {
|
||||||
|
case format::format_kind::NIL:
|
||||||
|
/* flatten NIL = NIL */
|
||||||
|
return s;
|
||||||
|
|
||||||
|
case format::format_kind::NEST:
|
||||||
|
/* flatten (NEST i x) = flatten x */
|
||||||
|
return flatten(cdr(v));
|
||||||
|
|
||||||
|
case format::format_kind::COMPOSE:
|
||||||
|
/* flatten (x <> y) = flatten x <> flatten y */
|
||||||
|
return sexpr(format::format_kind::COMPOSE,
|
||||||
|
sexpr(flatten(car(v)),
|
||||||
|
flatten(cdr(v))));
|
||||||
|
|
||||||
|
case format::format_kind::CHOICE:
|
||||||
|
/* flatten (x <|> y) = flatten x */
|
||||||
|
return flatten(car(v));
|
||||||
|
|
||||||
|
case format::format_kind::LINE:
|
||||||
|
return sexpr(" ");
|
||||||
|
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return s;
|
||||||
|
}
|
||||||
|
|
||||||
|
format flatten(format const & f){
|
||||||
|
return format(flatten(f.m_value));
|
||||||
|
}
|
||||||
|
|
||||||
|
format group(format const & f) {
|
||||||
|
return choice(flatten(f), f);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
void pp(lean::format const & n) { std::cout << "pp" << "\n"; }
|
||||||
|
|
|
||||||
|
|
@ -5,86 +5,97 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Author: Soonho Kong
|
Author: Soonho Kong
|
||||||
*/
|
*/
|
||||||
#pragma once
|
#pragma once
|
||||||
|
#include "sexpr.h"
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
class name;
|
|
||||||
class mpq;
|
|
||||||
class mpz;
|
|
||||||
struct format_cell;
|
|
||||||
|
|
||||||
enum class format_kind { NIL, INDENT, COMPOSE, CHOICE, LINE, TEXT };
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
\brief Simple LISP-like S-expressions.
|
\brief Format
|
||||||
1. Atoms: nil, string, int, name, mpz or mpq
|
|
||||||
2. Pair: (x . y) where x and y are S-expressions.
|
|
||||||
|
|
||||||
S-expressions are used for tracking configuration options, statistics, etc.
|
uses `sexpr` as an internal representation.
|
||||||
|
|
||||||
|
nil = nil sexpr
|
||||||
|
text s = ("TEXT" s )
|
||||||
|
nest f = ("NEST" f )
|
||||||
|
choice f1 f2 = ("CHOICE" f1 f2)
|
||||||
|
compose f1 f2 = ("COMPOSE" f1 f2)
|
||||||
|
line = ("LINE")
|
||||||
|
nest n f = ("NEST" n f)
|
||||||
|
|
||||||
Remark: this datastructure does not allow destructive updates.
|
|
||||||
*/
|
*/
|
||||||
|
|
||||||
class format {
|
class format {
|
||||||
format_cell* m_ptr;
|
sexpr m_value;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
format():m_ptr(nullptr) {}
|
enum format_kind { NIL, NEST, COMPOSE, CHOICE, LINE, TEXT };
|
||||||
explicit format(char const * v);
|
|
||||||
explicit format(std::string const & v);
|
format():m_value(sexpr()) {}
|
||||||
explicit format(int v);
|
explicit format(sexpr const & v):m_value(v) {}
|
||||||
explicit format(double v);
|
explicit format(char const * v):m_value(v) {}
|
||||||
explicit format(name const & v);
|
explicit format(std::string const & v):m_value(v) {}
|
||||||
explicit format(mpz const & v);
|
explicit format(int v):m_value(v) {}
|
||||||
explicit format(mpq const & v);
|
explicit format(double v):m_value(v) {}
|
||||||
format(format const & h, format const & t);
|
explicit format(name const & v):m_value(v) {}
|
||||||
template<typename T>
|
explicit format(mpz const & v):m_value(v) {}
|
||||||
format(T const & h, format const & t):format(format(h), t) {}
|
explicit format(mpq const & v):m_value(v) {}
|
||||||
template<typename T1, typename T2>
|
format(format const & f1, format const & f2) {
|
||||||
format(T1 const & h, T2 const & t):format(format(h), format(t)) {}
|
m_value = sexpr(sexpr(COMPOSE), sexpr(f1.m_value, f2.m_value));
|
||||||
format(format const & s);
|
|
||||||
format(format && s);
|
|
||||||
template<typename T>
|
|
||||||
format(std::initializer_list<T> const & l):format() {
|
|
||||||
auto it = l.end();
|
|
||||||
while (it != l.begin()) {
|
|
||||||
--it;
|
|
||||||
*this = format(*it, *this);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
~format();
|
format(format const & f):m_value(f.m_value) {}
|
||||||
|
|
||||||
format_kind kind() const;
|
format_kind kind() const {
|
||||||
|
if(is_nil(m_value)) {
|
||||||
|
return NIL;
|
||||||
|
}
|
||||||
|
if(is_cons(m_value)) {
|
||||||
|
/* CHOICE, COMPOSE, LINE, NEST */
|
||||||
|
return static_cast<format_kind>(to_int(car(m_value)));
|
||||||
|
}
|
||||||
|
return TEXT;
|
||||||
|
}
|
||||||
|
|
||||||
friend bool is_nil(format const & s) { return s.m_ptr == nullptr; }
|
unsigned hash() const { return m_value.hash(); }
|
||||||
|
|
||||||
std::string const & get_string() const;
|
|
||||||
|
|
||||||
unsigned hash() const;
|
|
||||||
|
|
||||||
format & operator=(format const & s);
|
format & operator=(format const & s);
|
||||||
format & operator=(format&& s);
|
format & operator=(format&& s);
|
||||||
template<typename T>
|
template<typename T>
|
||||||
format & operator=(T const & v) { return operator=(format(v)); }
|
format & operator=(T const & v) { return operator=(format(v)); }
|
||||||
|
|
||||||
friend void swap(format & a, format & b) { std::swap(a.m_ptr, b.m_ptr); }
|
std::ostream & display(std::ostream & out, sexpr const & s);
|
||||||
|
friend std::ostream & operator<<(std::ostream & out, format const & f);
|
||||||
|
|
||||||
// Pointer equality
|
friend format compose(format const & f1, format const & f2) {
|
||||||
friend bool eqp(format const & a, format const & b) { return a.m_ptr == b.m_ptr; }
|
return format(f1, f2);
|
||||||
|
}
|
||||||
|
friend format choice(format const & f1, format const & f2) {
|
||||||
|
return format(sexpr(sexpr(CHOICE), sexpr(f1.m_value, f2.m_value)));
|
||||||
|
}
|
||||||
|
friend format nest(int i, format const & f) {
|
||||||
|
return format(sexpr(sexpr(NEST), sexpr(sexpr(i), f.m_value)));
|
||||||
|
}
|
||||||
|
|
||||||
friend std::ostream & operator<<(std::ostream & out, format const & s);
|
friend bool is_compose(format const & f) {
|
||||||
|
return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::COMPOSE;
|
||||||
|
}
|
||||||
|
friend bool is_nest(format const & f) {
|
||||||
|
return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::NEST;
|
||||||
|
}
|
||||||
|
friend bool is_text(format const & f) {
|
||||||
|
return !is_cons(f.m_value);
|
||||||
|
}
|
||||||
|
friend bool is_line(format const & f) {
|
||||||
|
return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::LINE;
|
||||||
|
}
|
||||||
|
friend bool is_choice(format const & f) {
|
||||||
|
return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::CHOICE;
|
||||||
|
}
|
||||||
|
|
||||||
|
friend format flatten(format const & f);
|
||||||
};
|
};
|
||||||
|
|
||||||
inline format compose(format const & head, format const & tail) { return format(head, tail); }
|
inline format line() {
|
||||||
inline format choice(format const & head, format const & tail) { return format(head, tail); }
|
return format(sexpr(format::format_kind::LINE));
|
||||||
inline format indent(format const & f, unsigned i) { return f; }
|
}
|
||||||
inline format line(format const & f) { return f; }
|
|
||||||
|
|
||||||
inline bool is_compose(format const & s) { return s.kind() != format_kind::COMPOSE; }
|
|
||||||
inline bool is_indent(format const & s) { return s.kind() == format_kind::INDENT; }
|
|
||||||
inline bool is_text(format const & s) { return s.kind() == format_kind::TEXT; }
|
|
||||||
inline bool is_line(format const & s) { return s.kind() == format_kind::LINE; }
|
|
||||||
inline bool is_choice(format const & s) { return s.kind() == format_kind::CHOICE; }
|
|
||||||
|
|
||||||
inline std::string const & to_string(format const & s) { return s.get_string(); }
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue