@@ -25,8 +25,8 @@ use std::borrow::Cow;
25
25
use std:: cell:: RefCell ;
26
26
use std:: fmt;
27
27
use std:: hash:: { Hash , Hasher } ;
28
- use std:: rc:: Rc ;
29
28
use std:: ops:: Deref ;
29
+ use std:: rc:: Rc ;
30
30
31
31
/// Quint values that hold sets are immutable, use `GenericHashSet` immutable
32
32
/// structure to hold them
@@ -187,7 +187,7 @@ impl Eq for ValueInner {}
187
187
188
188
impl Deref for Value {
189
189
type Target = ValueInner ;
190
-
190
+
191
191
fn deref ( & self ) -> & Self :: Target {
192
192
& self . 0
193
193
}
@@ -198,55 +198,55 @@ impl Value {
198
198
pub fn int ( n : i64 ) -> Self {
199
199
Value ( Rc :: new ( ValueInner :: Int ( n) ) )
200
200
}
201
-
201
+
202
202
pub fn bool ( b : bool ) -> Self {
203
203
Value ( Rc :: new ( ValueInner :: Bool ( b) ) )
204
204
}
205
-
205
+
206
206
pub fn str ( s : Str ) -> Self {
207
207
Value ( Rc :: new ( ValueInner :: Str ( s) ) )
208
208
}
209
-
209
+
210
210
pub fn set ( s : ImmutableSet < Value > ) -> Self {
211
211
Value ( Rc :: new ( ValueInner :: Set ( s) ) )
212
212
}
213
-
213
+
214
214
pub fn tuple ( t : ImmutableVec < Value > ) -> Self {
215
215
Value ( Rc :: new ( ValueInner :: Tuple ( t) ) )
216
216
}
217
-
217
+
218
218
pub fn record ( r : ImmutableMap < QuintName , Value > ) -> Self {
219
219
Value ( Rc :: new ( ValueInner :: Record ( r) ) )
220
220
}
221
-
221
+
222
222
pub fn map ( m : ImmutableMap < Value , Value > ) -> Self {
223
223
Value ( Rc :: new ( ValueInner :: Map ( m) ) )
224
224
}
225
-
225
+
226
226
pub fn list ( l : ImmutableVec < Value > ) -> Self {
227
227
Value ( Rc :: new ( ValueInner :: List ( l) ) )
228
228
}
229
-
229
+
230
230
pub fn lambda ( registers : Vec < Rc < RefCell < EvalResult > > > , body : CompiledExpr ) -> Self {
231
231
Value ( Rc :: new ( ValueInner :: Lambda ( registers, body) ) )
232
232
}
233
-
233
+
234
234
pub fn variant ( name : QuintName , value : Value ) -> Self {
235
235
Value ( Rc :: new ( ValueInner :: Variant ( name, value) ) )
236
236
}
237
-
237
+
238
238
pub fn interval ( start : i64 , end : i64 ) -> Self {
239
239
Value ( Rc :: new ( ValueInner :: Interval ( start, end) ) )
240
240
}
241
-
241
+
242
242
pub fn cross_product ( values : Vec < Value > ) -> Self {
243
243
Value ( Rc :: new ( ValueInner :: CrossProduct ( values) ) )
244
244
}
245
-
245
+
246
246
pub fn power_set ( value : Value ) -> Self {
247
247
Value ( Rc :: new ( ValueInner :: PowerSet ( value) ) )
248
248
}
249
-
249
+
250
250
pub fn map_set ( a : Value , b : Value ) -> Self {
251
251
Value ( Rc :: new ( ValueInner :: MapSet ( a, b) ) )
252
252
}
@@ -260,7 +260,9 @@ impl Value {
260
260
ValueInner :: Map ( map) => map. len ( ) ,
261
261
ValueInner :: List ( elems) => elems. len ( ) ,
262
262
ValueInner :: Interval ( start, end) => ( end - start + 1 ) . try_into ( ) . unwrap ( ) ,
263
- ValueInner :: CrossProduct ( sets) => sets. iter ( ) . fold ( 1 , |acc, set| acc * set. cardinality ( ) ) ,
263
+ ValueInner :: CrossProduct ( sets) => {
264
+ sets. iter ( ) . fold ( 1 , |acc, set| acc * set. cardinality ( ) )
265
+ }
264
266
ValueInner :: PowerSet ( value) => {
265
267
// 2^(cardinality of value)
266
268
2_usize . pow ( value. cardinality ( ) . try_into ( ) . unwrap ( ) )
@@ -314,7 +316,9 @@ impl Value {
314
316
. zip ( supersets)
315
317
. all ( |( subset, superset) | subset. subseteq ( superset) )
316
318
}
317
- ( ValueInner :: PowerSet ( subset) , ValueInner :: PowerSet ( superset) ) => subset. subseteq ( superset) ,
319
+ ( ValueInner :: PowerSet ( subset) , ValueInner :: PowerSet ( superset) ) => {
320
+ subset. subseteq ( superset)
321
+ }
318
322
(
319
323
ValueInner :: MapSet ( subset_domain, subset_range) ,
320
324
ValueInner :: MapSet ( superset_domain, superset_range) ,
@@ -374,7 +378,9 @@ impl Value {
374
378
pub fn as_set ( & self ) -> Cow < ' _ , ImmutableSet < Value > > {
375
379
match self . 0 . as_ref ( ) {
376
380
ValueInner :: Set ( set) => Cow :: Borrowed ( set) ,
377
- ValueInner :: Interval ( start, end) => Cow :: Owned ( ( * start..=* end) . map ( Value :: int) . collect ( ) ) ,
381
+ ValueInner :: Interval ( start, end) => {
382
+ Cow :: Owned ( ( * start..=* end) . map ( Value :: int) . collect ( ) )
383
+ }
378
384
ValueInner :: CrossProduct ( sets) => {
379
385
let size = self . cardinality ( ) ;
380
386
if size == 0 {
0 commit comments