1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     format.cpp
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 #include "ast/format.h"
20 #include "ast/recurse_expr_def.h"
21 
22 namespace format_ns {
23 
24     class format_decl_plugin : public decl_plugin {
25     protected:
26         sort *       m_format_sort;
27         symbol       m_nil;
28         symbol       m_string;
29         symbol       m_indent;
30         symbol       m_compose;
31         symbol       m_choice;
32         symbol       m_line_break;
33         symbol       m_line_break_ext;
34 
set_manager(ast_manager * m,family_id id)35         void set_manager(ast_manager * m, family_id id) override {
36             SASSERT(m->is_format_manager());
37             decl_plugin::set_manager(m, id);
38 
39             m_format_sort = m->mk_sort(symbol("format"), sort_info(id, FORMAT_SORT));
40             m->inc_ref(m_format_sort);
41         }
42 
43     public:
format_decl_plugin()44         format_decl_plugin():
45             m_format_sort(nullptr),
46             m_nil("nil"),
47             m_string("string"),
48             m_indent("indent"),
49             m_compose("compose"),
50             m_choice("choice"),
51             m_line_break("cr"),
52             m_line_break_ext("cr++") {
53         }
54 
~format_decl_plugin()55         ~format_decl_plugin() override {}
56 
finalize()57         void finalize() override {
58             if (m_format_sort)
59                 m_manager->dec_ref(m_format_sort);
60         }
61 
mk_fresh()62         decl_plugin * mk_fresh() override {
63             return alloc(format_decl_plugin);
64         }
65 
mk_sort(decl_kind k,unsigned num_parameters,parameter const * parameters)66         sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override {
67             SASSERT(k == FORMAT_SORT);
68             return m_format_sort;
69         }
70 
mk_func_decl(decl_kind k,unsigned num_parameters,parameter const * parameters,unsigned arity,sort * const * domain,sort * range)71         func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
72                                  unsigned arity, sort * const * domain, sort * range) override {
73             switch (k) {
74             case OP_NIL:
75                 return m_manager->mk_func_decl(m_nil, arity, domain, m_format_sort,
76                                                func_decl_info(m_family_id, OP_NIL));
77             case OP_STRING:
78                 return m_manager->mk_func_decl(m_string, arity, domain, m_format_sort,
79                                                func_decl_info(m_family_id, OP_STRING, num_parameters, parameters));
80             case OP_INDENT:
81                 return m_manager->mk_func_decl(m_indent, arity, domain, m_format_sort,
82                                                func_decl_info(m_family_id, OP_INDENT, num_parameters, parameters));
83             case OP_COMPOSE:
84                 return m_manager->mk_func_decl(m_compose, arity, domain, m_format_sort,
85                                                func_decl_info(m_family_id, OP_COMPOSE));
86             case OP_CHOICE:
87                 return m_manager->mk_func_decl(m_choice, arity, domain, m_format_sort,
88                                                func_decl_info(m_family_id, OP_CHOICE));
89             case OP_LINE_BREAK:
90                 return m_manager->mk_func_decl(m_line_break, arity, domain, m_format_sort,
91                                                func_decl_info(m_family_id, OP_LINE_BREAK));
92 
93             case OP_LINE_BREAK_EXT:
94                 return m_manager->mk_func_decl(m_line_break_ext, arity, domain, m_format_sort,
95                                                func_decl_info(m_family_id, OP_LINE_BREAK_EXT, num_parameters, parameters));
96             default:
97                 return nullptr;
98             }
99         }
100     };
101 
get_format_family_id(ast_manager & m)102     family_id get_format_family_id(ast_manager & m) {
103         symbol f("format");
104         if (!fm(m).has_plugin(f))
105             fm(m).register_plugin(f, alloc(format_decl_plugin));
106         return fm(m).mk_family_id(f);
107     }
108 
fid(ast_manager & m)109     static family_id fid(ast_manager & m) {
110         return get_format_family_id(m);
111     }
112 
fsort(ast_manager & m)113     sort * fsort(ast_manager & m) {
114         return fm(m).mk_sort(fid(m), FORMAT_SORT);
115     }
116 
117     struct flat_visitor {
118         ast_manager & m_manager;
119         family_id     m_fid;
120 
flat_visitorformat_ns::flat_visitor121         flat_visitor(ast_manager & m):
122             m_manager(fm(m)),
123             m_fid(fid(m)) {
124             SASSERT(m_manager.is_format_manager());
125         }
126 
visitformat_ns::flat_visitor127         format * visit(var *) { UNREACHABLE(); return nullptr; }
visitformat_ns::flat_visitor128         format * visit(quantifier * q, format *, format * const *, format * const *) { UNREACHABLE(); return nullptr; }
visitformat_ns::flat_visitor129         format * visit(format * n, format * const * children) {
130             if (is_app_of(n, m_fid, OP_LINE_BREAK))
131                 return mk_string(m_manager, " ");
132             else if (is_app_of(n, m_fid, OP_LINE_BREAK_EXT))
133                 return mk_string(m_manager, n->get_decl()->get_parameter(0).get_symbol().bare_str());
134             else if (is_app_of(n, m_fid, OP_CHOICE))
135                 return to_app(n->get_arg(0));
136             else
137                 return m_manager.mk_app(n->get_decl(), n->get_num_args(), (expr *const*) children);
138         }
139     };
140 
flat(ast_manager & m,format * f)141     format * flat(ast_manager & m, format * f) {
142         flat_visitor v(m);
143         recurse_expr<format *, flat_visitor, true, true> r(v);
144         return r(f);
145     }
146 
mk_string(ast_manager & m,char const * str)147     format * mk_string(ast_manager & m, char const * str) {
148         symbol s(str);
149         parameter p(s);
150         return fm(m).mk_app(fid(m), OP_STRING, 1, &p, 0, nullptr);
151     }
152 
mk_int(ast_manager & m,int i)153     format * mk_int(ast_manager & m, int i) {
154         char buffer[128];
155         SPRINTF_D(buffer, i);
156         return mk_string(m, buffer);
157     }
158 
mk_unsigned(ast_manager & m,unsigned u)159     format * mk_unsigned(ast_manager & m, unsigned u) {
160         char buffer[128];
161         SPRINTF_U(buffer, u);
162         return mk_string(m, buffer);
163     }
164 
mk_indent(ast_manager & m,unsigned i,format * f)165     format * mk_indent(ast_manager & m, unsigned i, format * f) {
166         parameter p(i);
167         expr * e = static_cast<expr*>(f);
168         return fm(m).mk_app(fid(m), OP_INDENT, 1, &p, 1, &e);
169     }
170 
mk_line_break(ast_manager & m)171     format * mk_line_break(ast_manager & m) {
172         return fm(m).mk_app(fid(m), OP_LINE_BREAK);
173     }
174 
mk_choice(ast_manager & m,format * f1,format * f2)175     format * mk_choice(ast_manager & m, format * f1, format * f2) {
176         return fm(m).mk_app(fid(m), OP_CHOICE, f1, f2);
177     }
178 
mk_group(ast_manager & m,format * f)179     format * mk_group(ast_manager & m, format * f) {
180         return mk_choice(m, flat(m, f), f);
181     }
182 
mk_compose(ast_manager & m,unsigned num_children,format * const * children)183     format * mk_compose(ast_manager & m, unsigned num_children, format * const * children) {
184         return fm(m).mk_app(fid(m), OP_COMPOSE, num_children, (expr * const *) children);
185     }
186 
mk_compose(ast_manager & m,format * f1,format * f2)187     format * mk_compose(ast_manager & m, format * f1, format * f2) {
188         return fm(m).mk_app(fid(m), OP_COMPOSE, f1, f2);
189     }
190 
mk_compose(ast_manager & m,format * f1,format * f2,format * f3)191     format * mk_compose(ast_manager & m, format * f1, format * f2, format * f3) {
192         return fm(m).mk_app(fid(m), OP_COMPOSE, f1, f2, f3);
193     }
194 
mk_compose(ast_manager & m,format * f1,format * f2,format * f3,format * f4)195     format * mk_compose(ast_manager & m, format * f1, format * f2, format * f3, format * f4) {
196         expr * f[4] = { f1, f2, f3, f4 };
197         return fm(m).mk_app(fid(m), OP_COMPOSE, 4, f);
198     }
199 
mk_nil(ast_manager & m)200     format * mk_nil(ast_manager & m) {
201         return fm(m).mk_app(fid(m), OP_NIL);
202     }
203 
204 };
205