@@ -10,9 +10,8 @@ use std::marker::PhantomData;
10
10
use std:: sync:: Arc ;
11
11
12
12
use super :: {
13
- Constructible , Converter , CoreConstructible , DisconnectConstructible , Hide , Inner ,
14
- JetConstructible , Marker , NoWitness , Node , Redeem , RedeemData , RedeemNode ,
15
- WitnessConstructible ,
13
+ Converter , CoreConstructible , DisconnectConstructible , Inner , JetConstructible , Marker ,
14
+ NoWitness , Node , Redeem , RedeemData , RedeemNode , WitnessConstructible ,
16
15
} ;
17
16
18
17
/// ID used to share [`WitnessNode`]s.
@@ -45,112 +44,11 @@ impl<J: Jet> Marker for Witness<J> {
45
44
pub type WitnessNode < J > = Node < Witness < J > > ;
46
45
47
46
impl < J : Jet > WitnessNode < J > {
48
- /// Creates a copy of the node (and its entire DAG with the prune bit set)
49
- #[ must_use]
50
- pub fn pruned ( & self ) -> Arc < Self > {
51
- let new_data = WitnessData {
52
- must_prune : true ,
53
- ..self . data . clone ( )
54
- } ;
55
- Arc :: new ( WitnessNode {
56
- data : new_data,
57
- cmr : self . cmr ,
58
- inner : self
59
- . inner
60
- . as_ref ( )
61
- . map ( Arc :: clone)
62
- . map_disconnect ( Option :: < Arc < _ > > :: clone)
63
- . map_witness ( Option :: < Value > :: clone) ,
64
- } )
65
- }
66
-
67
47
/// Accessor for the node's arrow
68
48
pub fn arrow ( & self ) -> & Arrow {
69
49
& self . data . arrow
70
50
}
71
51
72
- /// Whether the "must prune" bit is set on this node
73
- pub fn must_prune ( & self ) -> bool {
74
- self . data . must_prune
75
- }
76
-
77
- pub fn prune_and_retype ( & self ) -> Arc < Self > {
78
- struct Retyper < J > {
79
- inference_context : types:: Context ,
80
- phantom : PhantomData < J > ,
81
- }
82
-
83
- impl < J : Jet > Converter < Witness < J > , Witness < J > > for Retyper < J > {
84
- type Error = types:: Error ;
85
- fn convert_witness (
86
- & mut self ,
87
- _: & PostOrderIterItem < & WitnessNode < J > > ,
88
- wit : & Option < Value > ,
89
- ) -> Result < Option < Value > , Self :: Error > {
90
- Ok ( Option :: < Value > :: clone ( wit) )
91
- }
92
-
93
- fn prune_case (
94
- & mut self ,
95
- _: & PostOrderIterItem < & WitnessNode < J > > ,
96
- left : & Arc < WitnessNode < J > > ,
97
- right : & Arc < WitnessNode < J > > ,
98
- ) -> Result < Hide , Self :: Error > {
99
- // If either child is marked as pruned, we hide it, which will cause this
100
- // case node to become an assertl or assertr, potentially reducing the size
101
- // of types since there will be fewer constraints to unify.
102
- //
103
- // If both children are marked pruned, this function will only hide the left
104
- // one. This doesn't matter; in this case the node itself will be marked as
105
- // pruned and eventually get dropped.
106
- if left. cached_data ( ) . must_prune {
107
- Ok ( Hide :: Left )
108
- } else if right. cached_data ( ) . must_prune {
109
- Ok ( Hide :: Right )
110
- } else {
111
- Ok ( Hide :: Neither )
112
- }
113
- }
114
-
115
- fn convert_disconnect (
116
- & mut self ,
117
- _: & PostOrderIterItem < & WitnessNode < J > > ,
118
- maybe_converted : Option < & Arc < WitnessNode < J > > > ,
119
- _: & Option < Arc < WitnessNode < J > > > ,
120
- ) -> Result < Option < Arc < WitnessNode < J > > > , Self :: Error > {
121
- Ok ( maybe_converted. map ( Arc :: clone) )
122
- }
123
-
124
- fn convert_data (
125
- & mut self ,
126
- data : & PostOrderIterItem < & WitnessNode < J > > ,
127
- inner : Inner < & Arc < WitnessNode < J > > , J , & Option < Arc < WitnessNode < J > > > , & Option < Value > > ,
128
- ) -> Result < WitnessData < J > , Self :: Error > {
129
- let converted_inner = inner
130
- . map ( |node| node. cached_data ( ) )
131
- . map_witness ( Option :: < Value > :: clone) ;
132
- // This next line does the actual retyping.
133
- let mut retyped =
134
- WitnessData :: from_inner ( & self . inference_context , converted_inner) ?;
135
- // Sometimes we set the prune bit on nodes without setting that
136
- // of their children; in this case the prune bit inferred from
137
- // `converted_inner` will be incorrect.
138
- if data. node . data . must_prune {
139
- retyped. must_prune = true ;
140
- }
141
- Ok ( retyped)
142
- }
143
- }
144
-
145
- // FIXME after running the `ReTyper` we should run a `WitnessShrinker` which
146
- // shrinks the witness data in case the ReTyper shrank its types.
147
- self . convert :: < InternalSharing , _ , _ > ( & mut Retyper {
148
- inference_context : types:: Context :: new ( ) ,
149
- phantom : PhantomData ,
150
- } )
151
- . expect ( "type inference won't fail if it succeeded before" )
152
- }
153
-
154
52
/// Finalize the witness program as an unpruned redeem program.
155
53
///
156
54
/// Witness nodes must be populated with sufficient data,
@@ -250,7 +148,6 @@ impl<J: Jet> WitnessNode<J> {
250
148
#[ derive( Clone , Debug ) ]
251
149
pub struct WitnessData < J > {
252
150
arrow : Arrow ,
253
- must_prune : bool ,
254
151
/// This isn't really necessary, but it helps type inference if every
255
152
/// struct has a \<J\> parameter, since it forces the choice of jets to
256
153
/// be consistent without the user needing to specify it too many times.
@@ -261,55 +158,48 @@ impl<J> CoreConstructible for WitnessData<J> {
261
158
fn iden ( inference_context : & types:: Context ) -> Self {
262
159
WitnessData {
263
160
arrow : Arrow :: iden ( inference_context) ,
264
- must_prune : false ,
265
161
phantom : PhantomData ,
266
162
}
267
163
}
268
164
269
165
fn unit ( inference_context : & types:: Context ) -> Self {
270
166
WitnessData {
271
167
arrow : Arrow :: unit ( inference_context) ,
272
- must_prune : false ,
273
168
phantom : PhantomData ,
274
169
}
275
170
}
276
171
277
172
fn injl ( child : & Self ) -> Self {
278
173
WitnessData {
279
174
arrow : Arrow :: injl ( & child. arrow ) ,
280
- must_prune : child. must_prune ,
281
175
phantom : PhantomData ,
282
176
}
283
177
}
284
178
285
179
fn injr ( child : & Self ) -> Self {
286
180
WitnessData {
287
181
arrow : Arrow :: injr ( & child. arrow ) ,
288
- must_prune : child. must_prune ,
289
182
phantom : PhantomData ,
290
183
}
291
184
}
292
185
293
186
fn take ( child : & Self ) -> Self {
294
187
WitnessData {
295
188
arrow : Arrow :: take ( & child. arrow ) ,
296
- must_prune : child. must_prune ,
297
189
phantom : PhantomData ,
298
190
}
299
191
}
300
192
301
193
fn drop_ ( child : & Self ) -> Self {
302
194
WitnessData {
303
195
arrow : Arrow :: drop_ ( & child. arrow ) ,
304
- must_prune : child. must_prune ,
305
196
phantom : PhantomData ,
306
197
}
307
198
}
308
199
309
200
fn comp ( left : & Self , right : & Self ) -> Result < Self , types:: Error > {
310
201
Ok ( WitnessData {
311
202
arrow : Arrow :: comp ( & left. arrow , & right. arrow ) ?,
312
- must_prune : left. must_prune || right. must_prune ,
313
203
phantom : PhantomData ,
314
204
} )
315
205
}
@@ -320,31 +210,27 @@ impl<J> CoreConstructible for WitnessData<J> {
320
210
// pruned is the case node itself pruned.
321
211
Ok ( WitnessData {
322
212
arrow : Arrow :: case ( & left. arrow , & right. arrow ) ?,
323
- must_prune : left. must_prune && right. must_prune ,
324
213
phantom : PhantomData ,
325
214
} )
326
215
}
327
216
328
217
fn assertl ( left : & Self , right : Cmr ) -> Result < Self , types:: Error > {
329
218
Ok ( WitnessData {
330
219
arrow : Arrow :: assertl ( & left. arrow , right) ?,
331
- must_prune : left. must_prune ,
332
220
phantom : PhantomData ,
333
221
} )
334
222
}
335
223
336
224
fn assertr ( left : Cmr , right : & Self ) -> Result < Self , types:: Error > {
337
225
Ok ( WitnessData {
338
226
arrow : Arrow :: assertr ( left, & right. arrow ) ?,
339
- must_prune : right. must_prune ,
340
227
phantom : PhantomData ,
341
228
} )
342
229
}
343
230
344
231
fn pair ( left : & Self , right : & Self ) -> Result < Self , types:: Error > {
345
232
Ok ( WitnessData {
346
233
arrow : Arrow :: pair ( & left. arrow , & right. arrow ) ?,
347
- must_prune : left. must_prune || right. must_prune ,
348
234
phantom : PhantomData ,
349
235
} )
350
236
}
@@ -353,15 +239,13 @@ impl<J> CoreConstructible for WitnessData<J> {
353
239
// Fail nodes always get pruned.
354
240
WitnessData {
355
241
arrow : Arrow :: fail ( inference_context, entropy) ,
356
- must_prune : true ,
357
242
phantom : PhantomData ,
358
243
}
359
244
}
360
245
361
246
fn const_word ( inference_context : & types:: Context , word : Word ) -> Self {
362
247
WitnessData {
363
248
arrow : Arrow :: const_word ( inference_context, word) ,
364
- must_prune : false ,
365
249
phantom : PhantomData ,
366
250
}
367
251
}
@@ -376,17 +260,15 @@ impl<J: Jet> DisconnectConstructible<Option<Arc<WitnessNode<J>>>> for WitnessDat
376
260
let right = right. as_ref ( ) ;
377
261
Ok ( WitnessData {
378
262
arrow : Arrow :: disconnect ( & left. arrow , & right. map ( |n| n. arrow ( ) ) ) ?,
379
- must_prune : left. must_prune || right. map ( |n| n. must_prune ( ) ) . unwrap_or ( false ) ,
380
263
phantom : PhantomData ,
381
264
} )
382
265
}
383
266
}
384
267
385
268
impl < J > WitnessConstructible < Option < Value > > for WitnessData < J > {
386
- fn witness ( inference_context : & types:: Context , witness : Option < Value > ) -> Self {
269
+ fn witness ( inference_context : & types:: Context , _witness : Option < Value > ) -> Self {
387
270
WitnessData {
388
271
arrow : Arrow :: witness ( inference_context, NoWitness ) ,
389
- must_prune : witness. is_none ( ) ,
390
272
phantom : PhantomData ,
391
273
}
392
274
}
@@ -396,7 +278,6 @@ impl<J: Jet> JetConstructible<J> for WitnessData<J> {
396
278
fn jet ( inference_context : & types:: Context , jet : J ) -> Self {
397
279
WitnessData {
398
280
arrow : Arrow :: jet ( inference_context, jet) ,
399
- must_prune : false ,
400
281
phantom : PhantomData ,
401
282
}
402
283
}
0 commit comments