1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 format.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-01-20. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 #include <string> 21 22 #include "ast/ast.h" 23 24 namespace format_ns { 25 typedef app format; 26 27 typedef app_ref format_ref; 28 29 enum format_sort_kind { 30 FORMAT_SORT 31 }; 32 33 enum format_op_kind { 34 OP_NIL, 35 OP_STRING, 36 OP_INDENT, 37 OP_COMPOSE, 38 OP_CHOICE, 39 OP_LINE_BREAK, 40 OP_LINE_BREAK_EXT 41 }; 42 43 struct f2f { 44 format * operator()(format * f) { return f; } 45 }; 46 47 /** 48 \brief Return the "format manager" associated with the given ast_manager. 49 */ 50 inline ast_manager & fm(ast_manager & m) { 51 return m.get_format_manager(); 52 } 53 54 family_id get_format_family_id(ast_manager & m); 55 56 format * mk_string(ast_manager & m, char const * str); 57 static inline format * mk_string(ast_manager & m, const std::string & str) { return mk_string(m, str.c_str()); } 58 format * mk_int(ast_manager & m, int i); 59 format * mk_unsigned(ast_manager & m, unsigned u); 60 format * mk_indent(ast_manager & m, unsigned i, format * f); 61 format * mk_line_break(ast_manager & m); 62 format * mk_group(ast_manager & m, format * f); 63 format * mk_compose(ast_manager & m, unsigned num_children, format * const * children); 64 format * mk_compose(ast_manager & m, format * f1, format * f2); 65 format * mk_compose(ast_manager & m, format * f1, format * f2, format * f3); 66 format * mk_compose(ast_manager & m, format * f1, format * f2, format * f3, format * f4); 67 format * mk_nil(ast_manager & m); 68 format * mk_choice(ast_manager & m, format * f1, format * f2); 69 70 template<typename It, typename ToDoc> 71 format * mk_seq(ast_manager & m, It const & begin, It const & end, ToDoc proc) { 72 app_ref_buffer children(fm(m)); 73 for (It it = begin; it != end; ++it) { 74 format * curr = proc(*it); 75 if (curr->get_decl_kind() != OP_NIL) { 76 children.push_back(mk_line_break(m)); 77 children.push_back(curr); 78 } 79 } 80 return mk_compose(m, children.size(), children.c_ptr()); 81 } 82 83 /** 84 (header elem_1 85 elem_2 86 ... 87 elem_n) 88 */ 89 template<typename It, typename ToDoc> 90 format * mk_seq1(ast_manager & m, It const & begin, It const & end, ToDoc proc, char const * header, 91 char const * lp = "(", char const * rp = ")") { 92 if (begin == end) 93 return mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_string(m, rp)); 94 unsigned indent = static_cast<unsigned>(strlen(lp) + strlen(header) + 1); 95 It it = begin; 96 format * first = proc(*it); 97 ++it; 98 return mk_group(m, mk_compose(m, 99 mk_string(m, lp), 100 mk_string(m, header), 101 mk_indent(m, indent, 102 mk_compose(m, 103 mk_string(m, " "), 104 first, 105 mk_seq(m, it, end, proc), 106 mk_string(m, rp))))); 107 } 108 109 template<typename It, typename ToDoc> 110 static inline format * mk_seq1(ast_manager & m, It const & begin, It const & end, ToDoc proc, const std::string &header, 111 char const * lp = "(", char const * rp = ")") { 112 return mk_seq1(m, begin, end, proc, header.c_str(), lp, rp); 113 } 114 115 #define FORMAT_DEFAULT_INDENT 2 116 117 /** 118 (header 119 elem_1 120 ... 121 elem_n) 122 */ 123 template<typename It, typename ToDoc> 124 format * mk_seq2(ast_manager & m, It const & begin, It const & end, ToDoc proc, char const * header, 125 unsigned indent = FORMAT_DEFAULT_INDENT, char const * lp = "(", char const * rp = ")") { 126 127 if (begin == end) 128 return mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_string(m, rp)); 129 return mk_group(m, mk_compose(m, 130 mk_indent(m, static_cast<unsigned>(strlen(lp)), 131 mk_compose(m, mk_string(m, lp), mk_string(m, header))), 132 mk_indent(m, indent, 133 mk_compose(m, mk_seq(m, begin, end, proc), mk_string(m, rp))))); 134 } 135 136 /** 137 (header elem_1 138 ... 139 elem_i 140 elem_{i+1} 141 ... 142 elem_n) 143 */ 144 template<typename It, typename ToDoc> 145 format * mk_seq3(ast_manager & m, It const & begin, It const & end, ToDoc proc, char const * header, unsigned i = 1, 146 unsigned indent = FORMAT_DEFAULT_INDENT, char const * lp = "(", char const * rp = ")") { 147 SASSERT(i >= 1); 148 if (begin == end) 149 return mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_string(m, rp)); 150 unsigned idx = 0; 151 It end1 = begin; 152 for (;end1 != end && idx < i; ++end1, ++idx) 153 ; 154 It it = begin; 155 format * first = proc(*it); 156 ++it; 157 return mk_group(m, 158 mk_compose(m, 159 mk_compose(m, mk_string(m, lp), mk_string(m, header)), 160 mk_group(m, mk_indent(m, static_cast<unsigned>(strlen(header) + strlen(lp) + 1), 161 mk_compose(m, mk_string(m, " "), first, 162 mk_seq(m, it, end1, proc)))), 163 mk_indent(m, indent, mk_seq(m, end1, end, proc)), 164 mk_string(m, rp))); 165 } 166 167 /** 168 (elem_1 169 elem_2 170 ... 171 elem_n) 172 */ 173 template<typename It, typename ToDoc> 174 format * mk_seq4(ast_manager & m, It const & begin, It const & end, ToDoc proc, unsigned indent = FORMAT_DEFAULT_INDENT, 175 char const * lp = "(", char const * rp = ")") { 176 if (begin == end) 177 return mk_compose(m, mk_string(m, lp), mk_string(m, rp)); 178 unsigned indent1 = static_cast<unsigned>(strlen(lp)); 179 It it = begin; 180 format * first = proc(*it); 181 ++it; 182 return mk_group(m, mk_compose(m, 183 mk_indent(m, indent1, mk_compose(m, mk_string(m, lp), first)), 184 mk_indent(m, indent, mk_compose(m, 185 mk_seq(m, it, end, proc), 186 mk_string(m, rp))))); 187 } 188 189 /** 190 (elem_1 191 elem_2 192 ... 193 elem_n) 194 */ 195 template<typename It, typename ToDoc> 196 format * mk_seq5(ast_manager & m, It const & begin, It const & end, ToDoc proc, 197 char const * lp = "(", char const * rp = ")") { 198 return mk_seq4(m, begin, end, proc, static_cast<unsigned>(strlen(lp)), lp, rp); 199 } 200 201 }; 202 203 204