(
&self,
id: &KId<M>,
field: u64,
wval: &KExpr<M>,
ctor_params: Option<usize>,
result: Option<&KExpr<M>>,
)
| 157 | || *addr == p.nat_shift_right.addr |
| 158 | || *addr == p.nat_beq.addr |
| 159 | || *addr == p.nat_ble.addr |
| 160 | { |
| 161 | return PrimFamily::Nat; |
| 162 | } |
| 163 | if *addr == p.nat_dec_le.addr |
| 164 | || *addr == p.nat_dec_eq.addr |
| 165 | || *addr == p.nat_dec_lt.addr |
| 166 | || *addr == p.int_dec_le.addr |
| 167 | || *addr == p.int_dec_eq.addr |
| 168 | || *addr == p.int_dec_lt.addr |
| 169 | { |
| 170 | return PrimFamily::Decidable; |
| 171 | } |
| 172 | if *addr == p.bit_vec_to_nat.addr |
| 173 | || *addr == p.bit_vec_ult.addr |
| 174 | || *addr == p.decidable_decide.addr |
| 175 | { |
| 176 | return PrimFamily::BitVec; |
| 177 | } |
| 178 | if *addr == p.punit_size_of_1.addr |
| 179 | || *addr == p.subtype_val.addr |
| 180 | || *addr == p.size_of_size_of.addr |
| 181 | || *addr == p.system_platform_num_bits.addr |
| 182 | || *addr == p.reduce_bool.addr |
| 183 | || *addr == p.reduce_nat.addr |
| 184 | { |
| 185 | return PrimFamily::Native; |
| 186 | } |
| 187 | if *addr == p.string_back.addr |
| 188 | || *addr == p.string_legacy_back.addr |
| 189 | || *addr == p.string_utf8_byte_size.addr |
| 190 | || *addr == p.string_to_byte_array.addr |
| 191 | || *addr == p.string_of_list.addr |
| 192 | || *addr == p.string_mk.addr |
| 193 | || *addr == p.string_append.addr |
| 194 | || *addr == p.string_dec_eq.addr |
| 195 | { |
| 196 | return PrimFamily::Str; |
| 197 | } |
| 198 | PrimFamily::Other |
| 199 | } |
| 200 | |
| 201 | impl<M: KernelMode> TypeChecker<'_, M> { |
| 202 | fn dump_whnf_fuel( |
| 203 | &self, |
| 204 | phase: &str, |
no test coverage detected