- (width, element_type) = random.choice([
- (4, 'i64'), (8, 'i32'), (16, 'i16'), (32, 'i8'),
- (4, 'f64'), (8, 'f32')])
+ width_map={'i64': 4, 'i32': 8, 'i16': 16, 'i8': 32, 'f64': 4, 'f32': 8}
+ (width, element_type) = random.choice(
+ [(width_map[t], t) for t in element_types])