1
1
use crate :: merkle:: common:: { MerkleRoot , TypeMerkleRoot } ;
2
2
use crate :: merkle:: tmr:: Tmr ;
3
+ use crate :: util:: replace_to_buffer;
3
4
use std:: collections:: VecDeque ;
4
5
use std:: iter:: FromIterator ;
5
6
use std:: { cell:: RefCell , cmp, fmt, rc:: Rc , sync:: Arc } ;
@@ -128,6 +129,65 @@ pub(crate) enum VariableType {
128
129
Product ( RcVar , RcVar ) ,
129
130
}
130
131
132
+ impl VariableType {
133
+ fn uncompressed_display < W : fmt:: Write > ( & self , w : & mut W ) -> fmt:: Result {
134
+ match self {
135
+ VariableType :: Unit => w. write_str ( "1" ) ,
136
+ VariableType :: Sum ( a, b) => {
137
+ w. write_str ( "(" ) ?;
138
+ a. borrow ( ) . inner . uncompressed_display ( w) ?;
139
+ w. write_str ( " + " ) ?;
140
+ b. borrow ( ) . inner . uncompressed_display ( w) ?;
141
+ w. write_str ( ")" )
142
+ }
143
+ VariableType :: Product ( a, b) => {
144
+ w. write_str ( "(" ) ?;
145
+ a. borrow ( ) . inner . uncompressed_display ( w) ?;
146
+ w. write_str ( " × " ) ?;
147
+ b. borrow ( ) . inner . uncompressed_display ( w) ?;
148
+ w. write_str ( ")" )
149
+ }
150
+ // Uncomment to use intermediate compression: more allocation of smaller strings
151
+ // VariableType::Sum(a, b) => write!(w, "({} + {})", a, b),
152
+ // VariableType::Product(a, b) => write!(w, "({} × {})", a, b),
153
+ }
154
+ }
155
+ }
156
+
157
+ fn into_compressed_display ( mut buffer1 : String ) -> String {
158
+ let mut buffer2 = String :: with_capacity ( buffer1. len ( ) ) ;
159
+
160
+ replace_to_buffer ( & buffer1, & mut buffer2, "(1 + 1)" , "2" ) ;
161
+ buffer1. clear ( ) ;
162
+ replace_to_buffer ( & buffer2, & mut buffer1, "(2 × 2)" , "2^2" ) ;
163
+ buffer2. clear ( ) ;
164
+ replace_to_buffer ( & buffer1, & mut buffer2, "(2^2 × 2^2)" , "2^4" ) ;
165
+ buffer1. clear ( ) ;
166
+ replace_to_buffer ( & buffer2, & mut buffer1, "(2^4 × 2^4)" , "2^8" ) ;
167
+ buffer2. clear ( ) ;
168
+ replace_to_buffer ( & buffer1, & mut buffer2, "(2^8 × 2^8)" , "2^16" ) ;
169
+ buffer1. clear ( ) ;
170
+ replace_to_buffer ( & buffer2, & mut buffer1, "(2^16 × 2^16)" , "2^32" ) ;
171
+ buffer2. clear ( ) ;
172
+ replace_to_buffer ( & buffer1, & mut buffer2, "(2^32 × 2^32)" , "2^64" ) ;
173
+ buffer1. clear ( ) ;
174
+ replace_to_buffer ( & buffer2, & mut buffer1, "(2^64 × 2^64)" , "2^128" ) ;
175
+ buffer2. clear ( ) ;
176
+ replace_to_buffer ( & buffer1, & mut buffer2, "(2^128 × 2^128)" , "2^256" ) ;
177
+
178
+ buffer2
179
+ }
180
+
181
+ impl fmt:: Display for VariableType {
182
+ fn fmt ( & self , f : & mut fmt:: Formatter ) -> fmt:: Result {
183
+ let mut buffer1 = String :: new ( ) ;
184
+ self . uncompressed_display ( & mut buffer1) ?;
185
+ let buffer2 = into_compressed_display ( buffer1) ;
186
+
187
+ write ! ( f, "{}" , buffer2)
188
+ }
189
+ }
190
+
131
191
/// Variable that can be cheaply cloned and internally mutated
132
192
pub ( crate ) type RcVar = Rc < RefCell < Variable > > ;
133
193
@@ -182,6 +242,16 @@ impl fmt::Debug for Variable {
182
242
}
183
243
}
184
244
245
+ impl fmt:: Display for Variable {
246
+ fn fmt ( & self , f : & mut fmt:: Formatter ) -> fmt:: Result {
247
+ let mut buffer1 = String :: new ( ) ;
248
+ self . inner . uncompressed_display ( & mut buffer1) ?;
249
+ let buffer2 = into_compressed_display ( buffer1) ;
250
+
251
+ write ! ( f, "{}" , buffer2)
252
+ }
253
+ }
254
+
185
255
/// Unification variable without metadata (see [`Variable`])
186
256
#[ derive( Clone ) ]
187
257
pub ( crate ) enum VariableInner {
@@ -208,6 +278,19 @@ impl fmt::Debug for VariableInner {
208
278
}
209
279
}
210
280
281
+ impl VariableInner {
282
+ fn uncompressed_display < W : fmt:: Write > ( & self , w : & mut W ) -> fmt:: Result {
283
+ match self {
284
+ VariableInner :: Free ( id) => w. write_str ( id) ,
285
+ VariableInner :: Bound ( ty, _) => ty. uncompressed_display ( w) ,
286
+ // Uncomment to use intermediate compression: more allocation of smaller strings
287
+ // VariableInner::Bound(ty, _) => write!(w, "{}", ty),
288
+ VariableInner :: EqualTo ( parent) => parent. borrow ( ) . inner . uncompressed_display ( w) ,
289
+ VariableInner :: Finalized ( ty) => write ! ( w, "{}" , ty) ,
290
+ }
291
+ }
292
+ }
293
+
211
294
/// Factory for creating free variables with fresh names.
212
295
/// Identifiers are assigned sequentially as follows:
213
296
/// `A`, `B`, `C`, ... `Z`, `AA`, `AB`, `AC`, ...
0 commit comments