| 3538 | }; |
| 3539 | if is_utf8_byte_size { |
| 3540 | let n = Nat::from(s.len() as u64); |
| 3541 | let addr = Address::hash(&n.to_le_bytes()); |
| 3542 | return Ok(Some(self.intern(KExpr::nat(n, addr)))); |
| 3543 | } |
| 3544 | if is_to_byte_array { |
| 3545 | if s.is_empty() { |
| 3546 | return Ok(Some(self.intern(KExpr::cnst( |
| 3547 | self.prims.byte_array_empty.clone(), |
| 3548 | Box::new([]), |
| 3549 | )))); |
| 3550 | } |
| 3551 | return Ok(None); |
| 3552 | } |
| 3553 | |
| 3554 | let codepoint = s.chars().last().map_or(65u32, u32::from); |
| 3555 | Ok(Some(self.char_of_nat_expr(u64::from(codepoint)))) |
| 3556 | } |
| 3557 | |
| 3558 | /// WHNF both arguments with the shared fuel-capped policy and require |
| 3559 | /// both to be `Str` literals. |
| 3560 | fn two_string_lit_args( |
| 3561 | &mut self, |
| 3562 | a: &KExpr<M>, |
| 3563 | b: &KExpr<M>, |
| 3564 | ) -> Result<Option<(String, String)>, TcError<M>> { |
| 3565 | let Some(wa) = self.whnf_prim_arg(a)? else { |
| 3566 | return Ok(None); |
| 3567 | }; |
| 3568 | let ExprData::Str(sa, _, _) = wa.data() else { |
| 3569 | return Ok(None); |
| 3570 | }; |
| 3571 | let sa = sa.clone(); |
| 3572 | let Some(wb) = self.whnf_prim_arg(b)? else { |
| 3573 | return Ok(None); |
| 3574 | }; |
| 3575 | let ExprData::Str(sb, _, _) = wb.data() else { |
| 3576 | return Ok(None); |
| 3577 | }; |
| 3578 | Ok(Some((sa, sb.clone()))) |
| 3579 | } |
| 3580 | |
| 3581 | /// `String.decEq` on two EQUAL literals → `Decidable.isTrue prop |
| 3582 | /// (Eq.refl.{1} String lit)`. Mirrors `try_reduce_decidable`'s Nat |
| 3583 | /// shape: the proposition is recovered from the inferred type |
| 3584 | /// (`Decidable prop`), and the witness is proof-irrelevant, so any |
| 3585 | /// well-typed inhabitant is defeq-indistinguishable from the one |
| 3586 | /// structural reduction would build. |
| 3587 | fn try_reduce_string_dec_eq( |
| 3588 | &mut self, |
| 3589 | e: &KExpr<M>, |
| 3590 | args: &[KExpr<M>], |
| 3591 | ) -> Result<Option<KExpr<M>>, TcError<M>> { |
| 3592 | let Some((sa, sb)) = self.two_string_lit_args(&args[0], &args[1])? else { |
| 3593 | return Ok(None); |
| 3594 | }; |
| 3595 | if sa != sb { |
| 3596 | return Ok(None); |
| 3597 | } |